1 (*********************************************************************************************************************************)
2 (* HaskCoreToWeak: convert HaskCore to HaskWeak *)
3 (*********************************************************************************************************************************)
5 Generalizable All Variables.
6 Require Import Preamble.
7 Require Import Coq.Lists.List.
8 Require Import General.
9 Require Import HaskKinds.
10 Require Import HaskLiterals.
11 Require Import HaskTyCons.
12 Require Import HaskCoreVars.
13 Require Import HaskCoreTypes.
14 Require Import HaskCore.
15 Require Import HaskWeakVars.
16 Require Import HaskWeakTypes.
17 Require Import HaskWeak.
19 Variable tyConOrTyFun : CoreTyCon -> sum TyCon TyFun. Extract Inlined Constant tyConOrTyFun => "tyConOrTyFun".
20 Variable coreViewDeep : CoreType -> CoreType. Extract Inlined Constant coreViewDeep => "coreViewDeep".
21 Variable coercionKind : CoreCoercion -> (CoreType * CoreType).
22 Extract Inlined Constant coercionKind => "(\x -> Pair.unPair (Coercion.coercionKind x))".
24 (* extracts the Name from a CoreVar *)
25 Variable coreVarCoreName : CoreVar -> CoreName. Extract Inlined Constant coreVarCoreName => "Var.varName".
27 (* the magic wired-in name for the modal type introduction/elimination forms *)
28 Variable hetmet_brak_name : CoreName. Extract Inlined Constant hetmet_brak_name => "PrelNames.hetmet_brak_name".
29 Variable hetmet_esc_name : CoreName. Extract Inlined Constant hetmet_esc_name => "PrelNames.hetmet_esc_name".
30 Variable hetmet_csp_name : CoreName. Extract Inlined Constant hetmet_csp_name => "PrelNames.hetmet_csp_name".
32 Definition mkTyFunApplication (tf:TyFun)(lwt:list WeakType) : ???WeakType :=
33 split_list lwt (length (fst (tyFunKind tf))) >>=
35 let (args,rest) := argsrest in
36 OK (fold_left (fun x y => WAppTy x y) rest (WTyFunApp tf args)).
38 (* a hack to evade the guardedness check of Fixpoint *)
39 Variable coreTypeToWeakTypeCheat' : CoreType -> ???WeakType.
40 Extract Inlined Constant coreTypeToWeakTypeCheat' => "coreTypeToWeakType'".
42 Fixpoint coreTypeToWeakType' (ct:CoreType) : ???WeakType :=
44 | TyVarTy cv => match coreVarToWeakVar cv with
45 | CVTWVR_EVar ct => Error "encountered expression variable in a type"
46 | CVTWVR_TyVar k => OK (WTyVarTy (weakTypeVar cv k))
47 | CVTWVR_CoVar t1 t2 => Error "encountered coercion variable in a type"
50 | AppTy t1 t2 => coreTypeToWeakType' t2 >>= fun t2' => coreTypeToWeakType' t1 >>= fun t1' => OK (WAppTy t1' t2')
53 let recurse := ((fix rec tl := match tl with
55 | a::b => coreTypeToWeakType' a >>= fun a' => rec b >>= fun b' => OK (a'::b')
57 in match tyConOrTyFun tc_ with
58 | inr tf => recurse >>= fun recurse' => mkTyFunApplication tf recurse'
59 | inl tc => if eqd_dec tc ModalBoxTyCon
61 | ((TyVarTy ec)::tbody::nil) =>
62 match coreVarToWeakVar ec with
63 | CVTWVR_EVar ct => Error "encountered expression variable in a modal box type"
64 | CVTWVR_CoVar t1 t2 => Error "encountered coercion variable in a modal box type"
65 | CVTWVR_TyVar k => coreTypeToWeakType' tbody >>= fun tbody' =>
66 OK (WCodeTy (weakTypeVar ec k) tbody')
68 | _ => Error ("mis-applied modal box tycon: " +++ toString ct)
70 else let tc' := if eqd_dec tc ArrowTyCon
73 in recurse >>= fun recurse' => OK (fold_left (fun x y => WAppTy x y) recurse' tc')
75 | FunTy (PredTy (EqPred t1 t2)) t3 => coreTypeToWeakType' t1 >>= fun t1' =>
76 coreTypeToWeakType' t2 >>= fun t2' =>
77 coreTypeToWeakType' t3 >>= fun t3' =>
78 OK (WCoFunTy t1' t2' t3')
79 | FunTy t1 t2 => coreTypeToWeakType' t1 >>= fun t1' =>
80 coreTypeToWeakType' t2 >>= fun t2' =>
81 OK (WAppTy (WAppTy WFunTyCon t1') t2')
82 | ForAllTy cv t => match coreVarToWeakVar cv with
83 | CVTWVR_EVar ct => Error "encountered expression variable in a type abstraction"
84 | CVTWVR_TyVar k => coreTypeToWeakType' t >>= fun t' => OK (WForAllTy (weakTypeVar cv k) t')
85 | CVTWVR_CoVar t1 t2 => coreTypeToWeakTypeCheat' t1 >>= fun t1' =>
86 coreTypeToWeakTypeCheat' t2 >>= fun t2' =>
87 coreTypeToWeakType' t >>= fun t3' =>
88 OK (WCoFunTy t1' t2' t3')
90 | PredTy (ClassP cl lct) => ((fix rec tl := match tl with
92 | a::b => coreTypeToWeakType' a >>= fun a' =>
93 rec b >>= fun b' => OK (a'::b')
94 end) lct) >>= fun lct' => OK (WClassP cl lct')
95 | PredTy (IParam ipn ct) => coreTypeToWeakType' ct >>= fun ct' => OK (WIParam ipn ct')
96 | PredTy (EqPred _ _) => Error "hit a bare EqPred"
99 Definition coreTypeToWeakType t :=
100 addErrorMessage ("during coreTypeToWeakType on " +++ toString t +++ eol) (coreTypeToWeakType' (coreViewDeep t)).
102 Definition coreVarToWeakVar' (cv:CoreVar) : ???WeakVar :=
103 addErrorMessage ("during coreVarToWeakVar on " +++ toString cv +++ eol)
104 match coreVarToWeakVar cv with
105 | CVTWVR_EVar ct => coreTypeToWeakType ct >>= fun t' => OK (WExprVar (weakExprVar cv t'))
106 | CVTWVR_TyVar k => OK (WTypeVar (weakTypeVar cv k))
107 | CVTWVR_CoVar t1 t2 =>
108 (* this will choke if given a coercion-between-coercions (EqPred (EqPred c1 c2) (EqPred c3 c4)) *)
109 addErrorMessage ("with t2=" +++ toString t2 +++ eol)
110 ((coreTypeToWeakType t2) >>= fun t2' =>
111 addErrorMessage ("with t1=" +++ toString t1 +++ eol)
112 (coreTypeToWeakType t1) >>= fun t1' =>
113 OK (WCoerVar (weakCoerVar cv t1' t2')))
115 Definition tyConTyVars (tc:CoreTyCon) :=
116 filter (map (fun x => match coreVarToWeakVar' x with OK (WTypeVar v) => Some v | _ => None end) (getTyConTyVars_ tc)).
118 Definition tyConKind (tc:TyCon) : list Kind := map (fun (x:WeakTypeVar) => x:Kind) (tyConTyVars tc).
120 (* detects our crude Core-encoding of modal type introduction/elimination forms *)
121 Definition isBrak (ce:@CoreExpr CoreVar) : ??(WeakExprVar * WeakTypeVar * CoreType) :=
123 | (CoreEApp (CoreEApp (CoreEVar v) (CoreEType (TyVarTy ec))) (CoreEType tbody))
124 => if coreName_eq hetmet_brak_name (coreVarCoreName v) then
125 match coreVarToWeakVar' ec with
126 | OK (WTypeVar tv) => match coreVarToWeakVar' v with
127 | OK (WExprVar v') => Some (v',tv,tbody)
135 Definition isEsc (ce:@CoreExpr CoreVar) : ??(WeakExprVar * WeakTypeVar * CoreType) :=
137 | (CoreEApp (CoreEApp (CoreEVar v) (CoreEType (TyVarTy ec))) (CoreEType tbody))
138 => if coreName_eq hetmet_esc_name (coreVarCoreName v) then
139 match coreVarToWeakVar' ec with
140 | OK (WTypeVar tv) => match coreVarToWeakVar' v with
141 | OK (WExprVar v') => Some (v',tv,tbody)
149 Definition isCSP (ce:@CoreExpr CoreVar) : ??(WeakExprVar * WeakTypeVar * CoreType) :=
151 | (CoreEApp (CoreEApp (CoreEVar v) (CoreEType (TyVarTy ec))) (CoreEType tbody))
152 => if coreName_eq hetmet_csp_name (coreVarCoreName v) then
153 match coreVarToWeakVar' ec with
154 | OK (WTypeVar tv) => match coreVarToWeakVar' v with
155 | OK (WExprVar v') => Some (v',tv,tbody)
163 (* if this is a (WAppTy (WAppTy ... (WTyCon tc) .. ) .. ), return (tc,[...]) *)
164 Fixpoint expectTyConApp (wt:WeakType)(acc:list WeakType) : ???(TyCon * list WeakType) :=
166 | WTyCon tc => OK (tc,acc)
167 | WAppTy t1 t2 => expectTyConApp t1 (t2::acc)
168 | WTyFunApp tc tys => Error ("expectTyConApp encountered TyFunApp: " +++ toString wt)
169 | _ => Error ("expectTyConApp encountered " +++ toString wt)
172 (* expects to see an EType with a coercion payload *)
173 Definition coreExprToWeakCoercion t1 t2 (ce:@CoreExpr CoreVar) : ???WeakCoercion :=
175 | CoreEType t => (*OK (coreCoercionToWeakCoercion t)*) OK (WCoUnsafe t1 t2)
176 | _ => Error ("coreExprToWeakCoercion got a " +++ toString ce)
179 (* expects to see an EType *)
180 Definition coreExprToWeakType (ce:@CoreExpr CoreVar) : ???WeakType :=
182 | CoreEType t => coreTypeToWeakType t
183 | _ => Error ("coreExprToWeakType got a " +++ toString ce)
186 Fixpoint coreExprToWeakExpr (ce:@CoreExpr CoreVar) : ???WeakExpr :=
188 | CoreELit lit => OK (WELit lit)
189 | CoreENote n e => coreExprToWeakExpr e >>= fun e' => OK (WENote n e')
190 | CoreEType t => Error "encountered CoreEType in a position where an Expr should have been"
191 | CoreECoercion co => Error "encountered CoreECoercion in a position where an Expr should have been"
192 | CoreECast e co => coreExprToWeakExpr e >>= fun e' =>
193 let (ct1,ct2) := coercionKind co
194 in coreTypeToWeakType ct1 >>= fun t1 =>
195 coreTypeToWeakType ct2 >>= fun t2 =>
196 OK (WECast e' (WCoUnsafe t1 t2))
198 | CoreEVar v => coreVarToWeakVar' v >>= fun v' => match v' with
199 | WExprVar ev => OK (WEVar ev)
200 | WTypeVar _ => Error "found a type variable inside an EVar!"
201 | WCoerVar _ => Error "found a coercion variable inside an EVar!"
204 | CoreEApp e1 e2 => match isBrak e1 with
206 coreExprToWeakExpr e2 >>= fun e' =>
207 coreTypeToWeakType t >>= fun t' =>
208 OK (WEBrak v tv e' t')
209 | None => match isEsc e1 with
211 coreExprToWeakExpr e2 >>= fun e' =>
212 coreTypeToWeakType t >>= fun t' =>
213 OK (WEEsc v tv e' t')
214 | None => match isCSP e1 with
216 coreExprToWeakExpr e2 >>= fun e' =>
217 coreTypeToWeakType t >>= fun t' =>
218 OK (WECSP v tv e' t')
219 | None => coreExprToWeakExpr e1 >>= fun e1' =>
222 coreTypeToWeakType t >>= fun t' =>
224 | _ => coreExprToWeakExpr e2
225 >>= fun e2' => OK (WEApp e1' e2')
231 | CoreELam v e => coreVarToWeakVar' v >>= fun v' => match v' with
232 | WExprVar ev => coreExprToWeakExpr e >>= fun e' => OK (WELam ev e')
233 | WTypeVar tv => coreExprToWeakExpr e >>= fun e' => OK (WETyLam tv e')
234 | WCoerVar cv => coreExprToWeakExpr e >>= fun e' => OK (WECoLam cv e')
237 | CoreELet (CoreNonRec v ve) e => coreVarToWeakVar' v >>= fun v' => match v' with
238 | WExprVar ev => coreExprToWeakExpr ve >>= fun ve' =>
239 coreExprToWeakExpr e >>= fun e' => OK (WELet ev ve' e')
240 | WTypeVar tv => match e with
241 | CoreEType t => coreExprToWeakExpr e >>= fun e' =>
242 coreExprToWeakType ve >>= fun ty' =>
243 OK (WETyApp (WETyLam tv e') ty')
244 | _ => Error "saw (ELet <tyvar> e) where e!=EType"
246 | WCoerVar (weakCoerVar cv t1 t2) =>
247 coreExprToWeakExpr e >>= fun e' =>
248 coreExprToWeakCoercion t1 t2 ve >>= fun co' =>
249 OK (WECoApp (WECoLam (weakCoerVar cv t1 t2) e') co')
252 | CoreELet (CoreRec rb) e =>
253 ((fix coreExprToWeakExprList (cel:list (CoreVar * (@CoreExpr CoreVar))) : ???(list (WeakExprVar * WeakExpr)) :=
256 | (v',e')::t => coreExprToWeakExprList t >>= fun t' =>
257 coreVarToWeakVar' v' >>= fun v'' => match v'' with
258 | WExprVar ev => coreExprToWeakExpr e' >>= fun e' => OK ((ev,e')::t')
259 | WTypeVar _ => Error "found a type variable in a recursive let"
260 | WCoerVar _ => Error "found a coercion variable in a recursive let"
262 end) rb) >>= fun rb' =>
263 coreExprToWeakExpr e >>= fun e' =>
264 OK (WELetRec (unleaves' rb') e')
266 | CoreECase e v tbranches alts =>
267 coreVarToWeakVar' v >>= fun v' => match v' with
268 | WTypeVar _ => Error "found a type variable in a case"
269 | WCoerVar _ => Error "found a coercion variable in a case"
271 coreTypeToWeakType (coreTypeOfCoreExpr e) >>= fun te' =>
272 expectTyConApp te' nil >>= fun tca =>
273 let (tc,lt) := tca:(TyCon * list WeakType) in
274 ((fix mkBranches (branches: list (@triple CoreAltCon (list CoreVar) (@CoreExpr CoreVar)))
275 : ???(list (WeakAltCon*list WeakTypeVar*list WeakCoerVar*list WeakExprVar*WeakExpr)) :=
278 | (mkTriple alt vars e)::rest =>
279 mkBranches rest >>= fun rest' =>
280 coreExprToWeakExpr e >>= fun e' =>
282 | DEFAULT => OK ((WeakDEFAULT,nil,nil,nil,e')::rest')
283 | LitAlt lit => OK ((WeakLitAlt lit,nil,nil,nil,e')::rest')
284 | DataAlt dc => let vars := map coreVarToWeakVar' vars in
285 OK (((WeakDataAlt dc),
286 (filter (map (fun x => match x with OK (WTypeVar v) => Some v | _ => None end) vars)),
287 (filter (map (fun x => match x with OK (WCoerVar v) => Some v | _ => None end) vars)),
288 (filter (map (fun x => match x with OK (WExprVar v) => Some v | _ => None end) vars)),
293 coreExprToWeakExpr e >>= fun scrutinee =>
294 coreTypeToWeakType tbranches >>= fun tbranches' =>
295 OK (WECase ev scrutinee tbranches' tc lt (unleaves branches))