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 *)
33 (* calculation. The CoreVar argument is the GlobalVar for the hetmet_brak *)
34 (* or hetmet_esc identifier *)
35 | WEBrak : CoreVar -> WeakTypeVar -> WeakExpr -> WeakType -> WeakExpr
36 | WEEsc : CoreVar -> WeakTypeVar -> WeakExpr -> WeakType -> WeakExpr
38 | WECase : forall (vscrut:WeakExprVar)
42 (type_params:list WeakType)
43 (alts : Tree ??(AltCon*list WeakTypeVar*list WeakCoerVar*list WeakExprVar*WeakExpr)),
46 (* calculate the free WeakVar's in a WeakExpr *)
48 Fixpoint getWeakExprFreeVars (me:WeakExpr) : list WeakExprVar :=
52 | WECast e co => getWeakExprFreeVars e
53 | WENote n e => getWeakExprFreeVars e
54 | WETyApp e t => getWeakExprFreeVars e
55 | WECoApp e co => getWeakExprFreeVars e
56 | WEBrak ec e _ => getWeakExprFreeVars e
57 | WEEsc ec e _ => getWeakExprFreeVars e
58 | WELet cv e1 e2 => mergeDistinctLists (getWeakExprFreeVars e1) (removeFromDistinctList cv (getWeakExprFreeVars e2))
59 | WEApp e1 e2 => mergeDistinctLists (getWeakExprFreeVars e1) (getWeakExprFreeVars e2)
60 | WELam cv e => @removeFromDistinctList _ WeakExprVarEqDecidable cv (getWeakExprFreeVars e)
61 | WETyLam cv e => getWeakExprFreeVars e
62 | WECoLam cv e => getWeakExprFreeVars e
64 (* the messy fixpoints below are required by Coq's termination conditions; trust me, I tried to get rid of them *)
65 | WECase scrutinee tbranches tc type_params alts =>
66 mergeDistinctLists (getWeakExprFreeVars scrutinee) (
67 ((fix getWeakExprFreeVarsAlts (alts:Tree ??(AltCon*list WeakTypeVar*list WeakCoerVar*list WeakExprVar*WeakExpr))
68 {struct alts} : list WeakExprVar :=
71 | T_Leaf (Some (DEFAULT,_,_,_,e)) => getWeakExprFreeVars e
72 | T_Leaf (Some (LitAlt lit,_,_,_,e)) => getWeakExprFreeVars e
73 | T_Leaf (Some ((DataAlt dc), tvars, cvars, evars,e)) => removeFromDistinctList' evars (getWeakExprFreeVars e)
74 | T_Branch b1 b2 => mergeDistinctLists (getWeakExprFreeVarsAlts b1) (getWeakExprFreeVarsAlts b2)
76 | WELetRec mlr e => (fix removeVarsLetRec (mlr:Tree ??(WeakExprVar * WeakExpr))(cvl:list WeakExprVar) :=
79 | T_Leaf (Some (cv,e)) => removeFromDistinctList cv cvl
80 | T_Branch b1 b2 => removeVarsLetRec b1 (removeVarsLetRec b2 cvl)
81 end) mlr (mergeDistinctLists (getWeakExprFreeVars e)
82 ((fix getWeakExprFreeVarsLetRec (mlr:Tree ??(WeakExprVar * WeakExpr)) :=
85 | T_Leaf (Some (cv,e)) => getWeakExprFreeVars e
86 | T_Branch b1 b2 => mergeDistinctLists (getWeakExprFreeVarsLetRec b1) (getWeakExprFreeVarsLetRec b2)
90 (* wrap lambdas around an expression until it has no free expression variables *)
91 Definition makeClosedExpression : WeakExpr -> WeakExpr :=
92 fun me => (fix closeExpression (me:WeakExpr)(cvl:list WeakExprVar) :=
95 | cv::cvl' => WELam cv (closeExpression me cvl')
96 end) me (getWeakExprFreeVars me).
98 Definition weakTypeOfLiteral (lit:HaskLiteral) : WeakType :=
99 (WTyCon (haskLiteralToTyCon lit)).
101 (* calculate the CoreType of a WeakExpr *)
102 Fixpoint weakTypeOfWeakExpr (ce:WeakExpr) : ???WeakType :=
104 | WEVar (weakExprVar v t) => OK t
105 | WELit lit => OK (weakTypeOfLiteral lit)
106 | WEApp e1 e2 => weakTypeOfWeakExpr e1 >>= fun t' =>
108 | (WAppTy (WAppTy WFunTyCon t1) t2) => OK t2
109 | _ => Error ("found non-function type "+++t'+++" in EApp")
111 | WETyApp e t => weakTypeOfWeakExpr e >>= fun te =>
113 | WForAllTy v ct => OK (replaceWeakTypeVar ct v t)
114 | _ => Error ("found non-forall type "+++te+++" in ETyApp")
116 | WECoApp e co => weakTypeOfWeakExpr e >>= fun te =>
118 | WCoFunTy t1 t2 t => OK t
119 | _ => Error ("found non-coercion type "+++te+++" in ETyApp")
121 | WELam (weakExprVar ev vt) e => weakTypeOfWeakExpr e >>= fun t' => OK (WAppTy (WAppTy WFunTyCon vt) t')
122 | WETyLam tv e => weakTypeOfWeakExpr e >>= fun t' => OK (WForAllTy tv t')
123 | WECoLam (weakCoerVar cv _ φ₁ φ₂) e => weakTypeOfWeakExpr e >>= fun t' => OK (WCoFunTy φ₁ φ₂ t')
124 | WELet ev ve e => weakTypeOfWeakExpr e
125 | WELetRec rb e => weakTypeOfWeakExpr e
126 | WENote n e => weakTypeOfWeakExpr e
127 | WECast e (weakCoercion _ t1 t2 _) => OK t2
128 | WECase vscrut scrutinee tbranches tc type_params alts => OK tbranches
130 (* note that we willfully ignore the type stashed in WEBrak/WEEsc here *)
131 | WEBrak _ ec e _ => weakTypeOfWeakExpr e >>= fun t' => OK (WCodeTy ec t')
132 | WEEsc _ ec e _ => weakTypeOfWeakExpr e >>= fun t' =>
134 | (WAppTy (WAppTy WCodeTyCon (WTyVarTy ec')) t'') =>
135 if eqd_dec ec ec' then OK t''
136 else Error "level mismatch in escapification"
137 | _ => Error "ill-typed escapification"