1 (*********************************************************************************************************************************)
2 (* HaskWeak: a non-dependently-typed but Coq-friendly version of HaskCore *)
3 (*********************************************************************************************************************************)
5 Generalizable All Variables.
6 Require Import Preamble.
7 Require Import General.
8 Require Import Coq.Lists.List.
9 Require Import HaskKinds.
10 Require Import HaskCoreLiterals.
11 Require Import HaskCoreVars.
12 Require Import HaskCoreTypes.
13 Require Import HaskCoreTypes.
14 Require Import HaskWeakVars.
15 Require Import HaskWeakTypes.
18 | WEVar : WeakExprVar -> WeakExpr
19 | WELit : HaskLiteral -> WeakExpr
20 | WELet : WeakExprVar -> WeakExpr -> WeakExpr -> WeakExpr
21 | WELetRec : Tree ??(WeakExprVar * WeakExpr) -> WeakExpr -> WeakExpr
22 | WECast : WeakExpr -> WeakCoercion -> WeakExpr
23 | WENote : Note -> WeakExpr -> WeakExpr
24 | WEApp : WeakExpr -> WeakExpr -> WeakExpr
25 | WETyApp : WeakExpr -> WeakType -> WeakExpr
26 | WECoApp : WeakExpr -> WeakCoercion -> WeakExpr
27 | WELam : WeakExprVar -> WeakExpr -> WeakExpr
28 | WETyLam : WeakTypeVar -> WeakExpr -> WeakExpr
29 | WECoLam : WeakCoerVar -> WeakExpr -> WeakExpr
31 (* the WeakType argument in WEBrak/WEEsc is used only when going back *)
32 (* from Weak to Core; it lets us dodge a possibly-failing type *)
34 | WEBrak : WeakTypeVar -> WeakExpr -> WeakType -> WeakExpr
35 | WEEsc : WeakTypeVar -> WeakExpr -> WeakType -> WeakExpr
37 (* note that HaskWeak "Case" does not bind a variable; coreExprToWeakExpr adds a let-binder *)
38 | WECase : forall (scrutinee:WeakExpr)
41 (type_params:list WeakType)
42 (alts : Tree ??(AltCon*list WeakTypeVar*list WeakCoerVar*list WeakExprVar*WeakExpr)),
45 (* calculate the free WeakVar's in a WeakExpr *)
46 Fixpoint getWeakExprFreeVars (me:WeakExpr) : list WeakExprVar :=
50 | WECast e co => getWeakExprFreeVars e
51 | WENote n e => getWeakExprFreeVars e
52 | WETyApp e t => getWeakExprFreeVars e
53 | WECoApp e co => getWeakExprFreeVars e
54 | WEBrak ec e _ => getWeakExprFreeVars e
55 | WEEsc ec e _ => getWeakExprFreeVars e
56 | WELet cv e1 e2 => mergeDistinctLists (getWeakExprFreeVars e1) (removeFromDistinctList cv (getWeakExprFreeVars e2))
57 | WEApp e1 e2 => mergeDistinctLists (getWeakExprFreeVars e1) (getWeakExprFreeVars e2)
58 | WELam cv e => @removeFromDistinctList _ WeakExprVarEqDecidable cv (getWeakExprFreeVars e)
59 | WETyLam cv e => getWeakExprFreeVars e
60 | WECoLam cv e => getWeakExprFreeVars e
62 (* the messy fixpoints below are required by Coq's termination conditions; trust me, I tried to get rid of them *)
63 | WECase scrutinee tbranches tc type_params alts =>
64 mergeDistinctLists (getWeakExprFreeVars scrutinee) (
65 ((fix getWeakExprFreeVarsAlts (alts:Tree ??(AltCon*list WeakTypeVar*list WeakCoerVar*list WeakExprVar*WeakExpr))
66 {struct alts} : list WeakExprVar :=
69 | T_Leaf (Some (DEFAULT,_,_,_,e)) => getWeakExprFreeVars e
70 | T_Leaf (Some (LitAlt lit,_,_,_,e)) => getWeakExprFreeVars e
71 | T_Leaf (Some ((DataAlt dc), tvars, cvars, evars,e)) => removeFromDistinctList' evars (getWeakExprFreeVars e)
72 | T_Branch b1 b2 => mergeDistinctLists (getWeakExprFreeVarsAlts b1) (getWeakExprFreeVarsAlts b2)
74 | WELetRec mlr e => (fix removeVarsLetRec (mlr:Tree ??(WeakExprVar * WeakExpr))(cvl:list WeakExprVar) :=
77 | T_Leaf (Some (cv,e)) => removeFromDistinctList cv cvl
78 | T_Branch b1 b2 => removeVarsLetRec b1 (removeVarsLetRec b2 cvl)
79 end) mlr (mergeDistinctLists (getWeakExprFreeVars e)
80 ((fix getWeakExprFreeVarsLetRec (mlr:Tree ??(WeakExprVar * WeakExpr)) :=
83 | T_Leaf (Some (cv,e)) => getWeakExprFreeVars e
84 | T_Branch b1 b2 => mergeDistinctLists (getWeakExprFreeVarsLetRec b1) (getWeakExprFreeVarsLetRec b2)
88 (* wrap lambdas around an expression until it has no free expression variables *)
89 Definition makeClosedExpression : WeakExpr -> WeakExpr :=
90 fun me => (fix closeExpression (me:WeakExpr)(cvl:list WeakExprVar) :=
93 | cv::cvl' => WELam cv (closeExpression me cvl')
94 end) me (getWeakExprFreeVars me).
96 Definition weakTypeOfLiteral (lit:HaskLiteral) : WeakType :=
97 (WTyCon (haskLiteralToTyCon lit)).
99 (* calculate the CoreType of a WeakExpr *)
100 Fixpoint weakTypeOfWeakExpr (ce:WeakExpr) : ???WeakType :=
102 | WEVar (weakExprVar v t) => OK t
103 | WELit lit => OK (weakTypeOfLiteral lit)
104 | WEApp e1 e2 => weakTypeOfWeakExpr e1 >>= fun t' =>
106 | (WAppTy (WAppTy WFunTyCon t1) t2) => OK t2
107 | _ => Error ("found non-function type "+++(weakTypeToString t')+++" in EApp")
109 | WETyApp e t => weakTypeOfWeakExpr e >>= fun te =>
111 | WForAllTy v ct => OK (replaceWeakTypeVar ct v t)
112 | _ => Error ("found non-forall type "+++(weakTypeToString te)+++" in ETyApp")
114 | WECoApp e co => weakTypeOfWeakExpr e >>= fun te =>
116 | WCoFunTy t1 t2 t => OK t
117 | _ => Error ("found non-coercion type "+++(weakTypeToString te)+++" in ETyApp")
119 | WELam (weakExprVar ev vt) e => weakTypeOfWeakExpr e >>= fun t' => OK (WAppTy (WAppTy WFunTyCon vt) t')
120 | WETyLam tv e => weakTypeOfWeakExpr e >>= fun t' => OK (WForAllTy tv t')
121 | WECoLam (weakCoerVar cv φ₁ φ₂) e => weakTypeOfWeakExpr e >>= fun t' => OK (WCoFunTy φ₁ φ₂ t')
122 | WELet ev ve e => weakTypeOfWeakExpr e
123 | WELetRec rb e => weakTypeOfWeakExpr e
124 | WENote n e => weakTypeOfWeakExpr e
125 | WECast e (weakCoercion t1 t2 _) => OK t2
126 | WECase scrutinee tbranches tc type_params alts => OK tbranches
128 (* note that we willfully ignore the type stashed in WEBrak/WEEsc here *)
129 | WEBrak ec e _ => weakTypeOfWeakExpr e >>= fun t' => OK (WCodeTy ec t')
130 | WEEsc ec e _ => weakTypeOfWeakExpr e >>= fun t' =>
132 | (WAppTy (WAppTy WCodeTyCon (WTyVarTy ec')) t'') =>
133 if eqd_dec ec ec' then OK t''
134 else Error "level mismatch in escapification"
135 | _ => Error "ill-typed escapification"