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 *)
47 Fixpoint getWeakExprFreeVars (me:WeakExpr) : list WeakExprVar :=
51 | WECast e co => getWeakExprFreeVars e
52 | WENote n e => getWeakExprFreeVars e
53 | WETyApp e t => getWeakExprFreeVars e
54 | WECoApp e co => getWeakExprFreeVars e
55 | WEBrak ec e _ => getWeakExprFreeVars e
56 | WEEsc ec e _ => getWeakExprFreeVars e
57 | WELet cv e1 e2 => mergeDistinctLists (getWeakExprFreeVars e1) (removeFromDistinctList cv (getWeakExprFreeVars e2))
58 | WEApp e1 e2 => mergeDistinctLists (getWeakExprFreeVars e1) (getWeakExprFreeVars e2)
59 | WELam cv e => @removeFromDistinctList _ WeakExprVarEqDecidable cv (getWeakExprFreeVars e)
60 | WETyLam cv e => getWeakExprFreeVars e
61 | WECoLam cv e => getWeakExprFreeVars e
63 (* the messy fixpoints below are required by Coq's termination conditions; trust me, I tried to get rid of them *)
64 | WECase scrutinee tbranches tc type_params alts =>
65 mergeDistinctLists (getWeakExprFreeVars scrutinee) (
66 ((fix getWeakExprFreeVarsAlts (alts:Tree ??(AltCon*list WeakTypeVar*list WeakCoerVar*list WeakExprVar*WeakExpr))
67 {struct alts} : list WeakExprVar :=
70 | T_Leaf (Some (DEFAULT,_,_,_,e)) => getWeakExprFreeVars e
71 | T_Leaf (Some (LitAlt lit,_,_,_,e)) => getWeakExprFreeVars e
72 | T_Leaf (Some ((DataAlt dc), tvars, cvars, evars,e)) => removeFromDistinctList' evars (getWeakExprFreeVars e)
73 | T_Branch b1 b2 => mergeDistinctLists (getWeakExprFreeVarsAlts b1) (getWeakExprFreeVarsAlts b2)
75 | WELetRec mlr e => (fix removeVarsLetRec (mlr:Tree ??(WeakExprVar * WeakExpr))(cvl:list WeakExprVar) :=
78 | T_Leaf (Some (cv,e)) => removeFromDistinctList cv cvl
79 | T_Branch b1 b2 => removeVarsLetRec b1 (removeVarsLetRec b2 cvl)
80 end) mlr (mergeDistinctLists (getWeakExprFreeVars e)
81 ((fix getWeakExprFreeVarsLetRec (mlr:Tree ??(WeakExprVar * WeakExpr)) :=
84 | T_Leaf (Some (cv,e)) => getWeakExprFreeVars e
85 | T_Branch b1 b2 => mergeDistinctLists (getWeakExprFreeVarsLetRec b1) (getWeakExprFreeVarsLetRec b2)
89 (* wrap lambdas around an expression until it has no free expression variables *)
90 Definition makeClosedExpression : WeakExpr -> WeakExpr :=
91 fun me => (fix closeExpression (me:WeakExpr)(cvl:list WeakExprVar) :=
94 | cv::cvl' => WELam cv (closeExpression me cvl')
95 end) me (getWeakExprFreeVars me).
97 Definition weakTypeOfLiteral (lit:HaskLiteral) : WeakType :=
98 (WTyCon (haskLiteralToTyCon lit)).
100 (* calculate the CoreType of a WeakExpr *)
101 Fixpoint weakTypeOfWeakExpr (ce:WeakExpr) : ???WeakType :=
103 | WEVar (weakExprVar v t) => OK t
104 | WELit lit => OK (weakTypeOfLiteral lit)
105 | WEApp e1 e2 => weakTypeOfWeakExpr e1 >>= fun t' =>
107 | (WAppTy (WAppTy WFunTyCon t1) t2) => OK t2
108 | _ => Error ("found non-function type "+++t'+++" in EApp")
110 | WETyApp e t => weakTypeOfWeakExpr e >>= fun te =>
112 | WForAllTy v ct => OK (replaceWeakTypeVar ct v t)
113 | _ => Error ("found non-forall type "+++te+++" in ETyApp")
115 | WECoApp e co => weakTypeOfWeakExpr e >>= fun te =>
117 | WCoFunTy t1 t2 t => OK t
118 | _ => Error ("found non-coercion type "+++te+++" in ETyApp")
120 | WELam (weakExprVar ev vt) e => weakTypeOfWeakExpr e >>= fun t' => OK (WAppTy (WAppTy WFunTyCon vt) t')
121 | WETyLam tv e => weakTypeOfWeakExpr e >>= fun t' => OK (WForAllTy tv t')
122 | WECoLam (weakCoerVar cv φ₁ φ₂) e => weakTypeOfWeakExpr e >>= fun t' => OK (WCoFunTy φ₁ φ₂ t')
123 | WELet ev ve e => weakTypeOfWeakExpr e
124 | WELetRec rb e => weakTypeOfWeakExpr e
125 | WENote n e => weakTypeOfWeakExpr e
126 | WECast e (weakCoercion t1 t2 _) => OK t2
127 | WECase scrutinee tbranches tc type_params alts => OK tbranches
129 (* note that we willfully ignore the type stashed in WEBrak/WEEsc here *)
130 | WEBrak ec e _ => weakTypeOfWeakExpr e >>= fun t' => OK (WCodeTy ec t')
131 | WEEsc ec e _ => weakTypeOfWeakExpr e >>= fun t' =>
133 | (WAppTy (WAppTy WCodeTyCon (WTyVarTy ec')) t'') =>
134 if eqd_dec ec ec' then OK t''
135 else Error "level mismatch in escapification"
136 | _ => Error "ill-typed escapification"