1 (*********************************************************************************************************************************)
2 (* HaskWeakToCore: convert HaskWeak to HaskCore *)
3 (*********************************************************************************************************************************)
5 Generalizable All Variables.
6 Require Import Preamble.
7 Require Import General.
8 Require Import Coq.Strings.String.
9 Require Import Coq.Lists.List.
10 Require Import HaskKinds.
11 Require Import HaskLiteralsAndTyCons.
12 Require Import HaskCoreVars.
13 Require Import HaskCoreTypes.
14 Require Import HaskCore.
15 Require Import HaskWeakVars.
16 Require Import HaskWeakTypes.
17 Require Import HaskWeak.
18 Require Import HaskCoreToWeak.
20 Variable mkCoreLet : @CoreBind CoreVar -> @CoreExpr CoreVar -> @CoreExpr CoreVar.
21 Extract Inlined Constant mkCoreLet => "MkCore.mkCoreLet".
23 Variable sortAlts : forall {a}{b}, list (@triple CoreAltCon a b) -> list (@triple CoreAltCon a b).
24 Extract Inlined Constant sortAlts => "sortAlts".
25 Implicit Arguments sortAlts [[a][b]].
27 Variable mkUnsafeCoercion : CoreType -> CoreType -> CoreCoercion.
28 Extract Inlined Constant mkUnsafeCoercion => "Coercion.mkUnsafeCoercion".
30 (* Coercion and Type are actually the same thing in GHC, but we don't tell Coq about that. This lets us get around it. *)
31 Variable coreCoercionsAreReallyTypes : CoreCoercion -> CoreType.
32 Extract Inlined Constant coreCoercionsAreReallyTypes => "(\x -> x)".
34 Variable ModalBoxTyCon : TyCon. Extract Inlined Constant ModalBoxTyCon => "TysWiredIn.hetMetCodeTypeTyCon".
35 Variable ArrowTyCon : TyCon. Extract Constant ArrowTyCon => "Type.funTyCon".
37 Definition weakAltConToCoreAltCon (wa:WeakAltCon) : CoreAltCon :=
39 | WeakDataAlt cdc => DataAlt cdc
40 | WeakLitAlt lit => LitAlt lit
41 | WeakDEFAULT => DEFAULT
44 Fixpoint weakTypeToCoreType (wt:WeakType) : CoreType :=
46 | WTyVarTy (weakTypeVar v _) => TyVarTy v
47 | WAppTy (WAppTy WFunTyCon t1) t2 => FunTy (weakTypeToCoreType t1) (weakTypeToCoreType t2)
48 | WAppTy t1 t2 => match (weakTypeToCoreType t1) with
49 | TyConApp tc tys => TyConApp tc (app tys ((weakTypeToCoreType t2)::nil))
50 | t1' => AppTy t1' (weakTypeToCoreType t2)
52 | WTyCon tc => TyConApp tc nil
53 | WTyFunApp tf lt => TyConApp tf (map weakTypeToCoreType lt)
54 | WClassP c lt => PredTy (ClassP c (map weakTypeToCoreType lt))
55 | WIParam n ty => PredTy (IParam n (weakTypeToCoreType ty))
56 | WForAllTy (weakTypeVar wtv _) t => ForAllTy wtv (weakTypeToCoreType t)
57 | WFunTyCon => TyConApp ArrowTyCon nil
58 | WCodeTy (weakTypeVar ec _) t => TyConApp ModalBoxTyCon ((TyVarTy ec)::(weakTypeToCoreType t)::nil)
59 | WCoFunTy t1 t2 t3 => FunTy (PredTy (EqPred (weakTypeToCoreType t1) (weakTypeToCoreType t2)))
60 (weakTypeToCoreType t3)
63 Definition weakCoercionToCoreCoercion (wc:WeakCoercion) : CoreCoercion :=
64 mkUnsafeCoercion (weakTypeToCoreType (fst (weakCoercionTypes wc))) (weakTypeToCoreType (snd (weakCoercionTypes wc))).
66 Fixpoint weakExprToCoreExpr (me:WeakExpr) : @CoreExpr CoreVar :=
68 | WEVar (weakExprVar v _) => CoreEVar v
69 | WELit lit => CoreELit lit
70 | WEApp e1 e2 => CoreEApp (weakExprToCoreExpr e1) (weakExprToCoreExpr e2)
71 | WETyApp e t => CoreEApp (weakExprToCoreExpr e ) (CoreEType (weakTypeToCoreType t))
72 | WECoApp e co => CoreEApp (weakExprToCoreExpr e )
73 (CoreEType (coreCoercionsAreReallyTypes (weakCoercionToCoreCoercion co)))
74 | WENote n e => CoreENote n (weakExprToCoreExpr e )
75 | WELam (weakExprVar ev _ ) e => CoreELam ev (weakExprToCoreExpr e )
76 | WETyLam (weakTypeVar tv _ ) e => CoreELam tv (weakExprToCoreExpr e )
77 | WECoLam (weakCoerVar cv _ _ _) e => CoreELam cv (weakExprToCoreExpr e )
78 | WECast e co => CoreECast (weakExprToCoreExpr e ) (weakCoercionToCoreCoercion co)
79 | WEBrak v (weakTypeVar ec _) e t => fold_left CoreEApp
80 ((CoreEType (TyVarTy ec))::
81 (CoreEType (weakTypeToCoreType t))::
82 (weakExprToCoreExpr e)::
85 | WEEsc v (weakTypeVar ec _) e t => fold_left CoreEApp
86 ((CoreEType (TyVarTy ec))::
87 (CoreEType (weakTypeToCoreType t))::
88 (weakExprToCoreExpr e)::
91 | WECSP v (weakTypeVar ec _) e t => fold_left CoreEApp
92 ((CoreEType (TyVarTy ec))::
93 (CoreEType (weakTypeToCoreType t))::
94 (weakExprToCoreExpr e)::
97 | WELet (weakExprVar v _) ve e => mkCoreLet (CoreNonRec v (weakExprToCoreExpr ve)) (weakExprToCoreExpr e)
98 | WECase vscrut escrut tbranches tc types alts =>
99 CoreECase (weakExprToCoreExpr escrut) vscrut (weakTypeToCoreType tbranches)
101 fix mkCaseBranches (alts:Tree
102 ??(WeakAltCon*list WeakTypeVar*list WeakCoerVar*list WeakExprVar*WeakExpr)) :=
105 | T_Branch b1 b2 => app (mkCaseBranches b1) (mkCaseBranches b2)
106 | T_Leaf (Some (ac,tvars,cvars,evars,e)) =>
107 (mkTriple (weakAltConToCoreAltCon ac)
109 (map (fun v:WeakTypeVar => weakVarToCoreVar v) tvars)
110 (map (fun v:WeakCoerVar => weakVarToCoreVar v) cvars))
111 (map (fun v:WeakExprVar => weakVarToCoreVar v) evars))
112 (weakExprToCoreExpr e))::nil
115 | WELetRec mlr e => CoreELet (CoreRec
116 ((fix mkLetBindings (mlr:Tree ??(WeakExprVar * WeakExpr)) :=
119 | T_Leaf (Some (weakExprVar cv _,e)) => (cv,(weakExprToCoreExpr e))::nil
120 | T_Branch b1 b2 => app (mkLetBindings b1) (mkLetBindings b2)
122 (weakExprToCoreExpr e)
125 Definition weakTypeOfWeakExpr (we:WeakExpr) : ???WeakType :=
126 coreTypeToWeakType (coreTypeOfCoreExpr (weakExprToCoreExpr we)).
128 Instance weakExprToString : ToString WeakExpr :=
129 { toString := fun we => toString (weakExprToCoreExpr we) }.