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".
31 Variable hetmet_kappa_name : CoreName. Extract Inlined Constant hetmet_kappa_name => "PrelNames.hetmet_kappa_name".
32 Variable hetmet_kappa_app_name: CoreName.
33 Extract Inlined Constant hetmet_kappa_app_name => "PrelNames.hetmet_kappa_app_name".
35 Definition mkTyFunApplication (tf:TyFun)(lwt:list WeakType) : ???WeakType :=
36 split_list lwt (length (fst (tyFunKind tf))) >>=
38 let (args,rest) := argsrest in
39 OK (fold_left (fun x y => WAppTy x y) rest (WTyFunApp tf args)).
41 (* a hack to evade the guardedness check of Fixpoint *)
42 Variable coreTypeToWeakTypeCheat' : CoreType -> ???WeakType.
43 Extract Inlined Constant coreTypeToWeakTypeCheat' => "coreTypeToWeakType'".
45 Fixpoint coreTypeToWeakType' (ct:CoreType) : ???WeakType :=
47 | TyVarTy cv => match coreVarToWeakVar cv with
48 | CVTWVR_EVar ct => Error "encountered expression variable in a type"
49 | CVTWVR_TyVar k => OK (WTyVarTy (weakTypeVar cv k))
50 | CVTWVR_CoVar t1 t2 => Error "encountered coercion variable in a type"
53 | AppTy t1 t2 => coreTypeToWeakType' t2 >>= fun t2' => coreTypeToWeakType' t1 >>= fun t1' => OK (WAppTy t1' t2')
56 let recurse := ((fix rec tl := match tl with
58 | a::b => coreTypeToWeakType' a >>= fun a' => rec b >>= fun b' => OK (a'::b')
60 in match tyConOrTyFun tc_ with
61 | inr tf => recurse >>= fun recurse' => mkTyFunApplication tf recurse'
62 | inl tc => if eqd_dec tc ModalBoxTyCon
64 | ((TyVarTy ec)::tbody::nil) =>
65 match coreVarToWeakVar ec with
66 | CVTWVR_EVar ct => Error "encountered expression variable in a modal box type"
67 | CVTWVR_CoVar t1 t2 => Error "encountered coercion variable in a modal box type"
68 | CVTWVR_TyVar k => coreTypeToWeakType' tbody >>= fun tbody' =>
69 OK (WCodeTy (weakTypeVar ec k) tbody')
71 | _ => Error ("mis-applied modal box tycon: " +++ toString ct)
73 else let tc' := if eqd_dec tc ArrowTyCon
76 in recurse >>= fun recurse' => OK (fold_left (fun x y => WAppTy x y) recurse' tc')
78 | FunTy (PredTy (EqPred t1 t2)) t3 => coreTypeToWeakType' t1 >>= fun t1' =>
79 coreTypeToWeakType' t2 >>= fun t2' =>
80 coreTypeToWeakType' t3 >>= fun t3' =>
81 OK (WCoFunTy t1' t2' t3')
82 | FunTy t1 t2 => coreTypeToWeakType' t1 >>= fun t1' =>
83 coreTypeToWeakType' t2 >>= fun t2' =>
84 OK (WAppTy (WAppTy WFunTyCon t1') t2')
85 | ForAllTy cv t => match coreVarToWeakVar cv with
86 | CVTWVR_EVar ct => Error "encountered expression variable in a type abstraction"
87 | CVTWVR_TyVar k => coreTypeToWeakType' t >>= fun t' => OK (WForAllTy (weakTypeVar cv k) t')
88 | CVTWVR_CoVar t1 t2 => coreTypeToWeakTypeCheat' t1 >>= fun t1' =>
89 coreTypeToWeakTypeCheat' t2 >>= fun t2' =>
90 coreTypeToWeakType' t >>= fun t3' =>
91 OK (WCoFunTy t1' t2' t3')
93 | PredTy (ClassP cl lct) => ((fix rec tl := match tl with
95 | a::b => coreTypeToWeakType' a >>= fun a' =>
96 rec b >>= fun b' => OK (a'::b')
97 end) lct) >>= fun lct' => OK (WClassP cl lct')
98 | PredTy (IParam ipn ct) => coreTypeToWeakType' ct >>= fun ct' => OK (WIParam ipn ct')
99 | PredTy (EqPred _ _) => Error "hit a bare EqPred"
102 Definition coreTypeToWeakType t :=
103 addErrorMessage ("during coreTypeToWeakType on " +++ toString t +++ eol) (coreTypeToWeakType' (coreViewDeep t)).
105 Definition coreVarToWeakVar' (cv:CoreVar) : ???WeakVar :=
106 addErrorMessage ("during coreVarToWeakVar on " +++ toString cv +++ eol)
107 match coreVarToWeakVar cv with
108 | CVTWVR_EVar ct => coreTypeToWeakType ct >>= fun t' => OK (WExprVar (weakExprVar cv t'))
109 | CVTWVR_TyVar k => OK (WTypeVar (weakTypeVar cv k))
110 | CVTWVR_CoVar t1 t2 =>
111 (* this will choke if given a coercion-between-coercions (EqPred (EqPred c1 c2) (EqPred c3 c4)) *)
112 addErrorMessage ("with t2=" +++ toString t2 +++ eol)
113 ((coreTypeToWeakType t2) >>= fun t2' =>
114 addErrorMessage ("with t1=" +++ toString t1 +++ eol)
115 (coreTypeToWeakType t1) >>= fun t1' =>
116 OK (WCoerVar (weakCoerVar cv t1' t2')))
118 Definition tyConTyVars (tc:CoreTyCon) :=
119 filter (map (fun x => match coreVarToWeakVar' x with OK (WTypeVar v) => Some v | _ => None end) (getTyConTyVars_ tc)).
121 Definition tyConKind (tc:TyCon) : list Kind := map (fun (x:WeakTypeVar) => x:Kind) (tyConTyVars tc).
123 (* detects our crude Core-encoding of modal type introduction/elimination forms *)
124 Definition isBrak (ce:@CoreExpr CoreVar) : ??(WeakExprVar * WeakTypeVar * CoreType) :=
126 | (CoreEApp (CoreEApp (CoreEVar v) (CoreEType (TyVarTy ec))) (CoreEType tbody))
127 => if coreName_eq hetmet_brak_name (coreVarCoreName v) then
128 match coreVarToWeakVar' ec with
129 | OK (WTypeVar tv) => match coreVarToWeakVar' v with
130 | OK (WExprVar v') => Some (v',tv,tbody)
138 Definition isEsc (ce:@CoreExpr CoreVar) : ??(WeakExprVar * WeakTypeVar * CoreType) :=
140 | (CoreEApp (CoreEApp (CoreEVar v) (CoreEType (TyVarTy ec))) (CoreEType tbody))
141 => if coreName_eq hetmet_esc_name (coreVarCoreName v) then
142 match coreVarToWeakVar' ec with
143 | OK (WTypeVar tv) => match coreVarToWeakVar' v with
144 | OK (WExprVar v') => Some (v',tv,tbody)
152 Definition isKappa (ce:@CoreExpr CoreVar) : bool :=
161 => if coreName_eq hetmet_kappa_name (coreVarCoreName v) then true else false
165 Definition isKappaApp (ce:@CoreExpr CoreVar) : bool :=
167 | (CoreEApp (CoreEApp
174 => if coreName_eq hetmet_kappa_app_name (coreVarCoreName v) then true else false
178 Definition isCSP (ce:@CoreExpr CoreVar) : ??(WeakExprVar * WeakTypeVar * CoreType) :=
180 | (CoreEApp (CoreEApp (CoreEVar v) (CoreEType (TyVarTy ec))) (CoreEType tbody))
181 => if coreName_eq hetmet_csp_name (coreVarCoreName v) then
182 match coreVarToWeakVar' ec with
183 | OK (WTypeVar tv) => match coreVarToWeakVar' v with
184 | OK (WExprVar v') => Some (v',tv,tbody)
192 (* if this is a (WAppTy (WAppTy ... (WTyCon tc) .. ) .. ), return (tc,[...]) *)
193 Fixpoint expectTyConApp (wt:WeakType)(acc:list WeakType) : ???(TyCon * list WeakType) :=
195 | WTyCon tc => OK (tc,acc)
196 | WAppTy t1 t2 => expectTyConApp t1 (t2::acc)
197 | WTyFunApp tc tys => Error ("expectTyConApp encountered TyFunApp: " +++ toString wt)
198 | _ => Error ("expectTyConApp encountered " +++ toString wt)
201 (* expects to see an EType with a coercion payload *)
202 Definition coreExprToWeakCoercion t1 t2 (ce:@CoreExpr CoreVar) : ???WeakCoercion :=
204 | CoreEType t => (*OK (coreCoercionToWeakCoercion t)*) OK (WCoUnsafe t1 t2)
205 | _ => Error ("coreExprToWeakCoercion got a " +++ toString ce)
208 (* expects to see an EType *)
209 Definition coreExprToWeakType (ce:@CoreExpr CoreVar) : ???WeakType :=
211 | CoreEType t => coreTypeToWeakType t
212 | _ => Error ("coreExprToWeakType got a " +++ toString ce)
215 Fixpoint coreExprToWeakExpr (ce:@CoreExpr CoreVar) : ???WeakExpr :=
217 | CoreELit lit => OK (WELit lit)
218 | CoreENote n e => coreExprToWeakExpr e >>= fun e' => OK (WENote n e')
219 | CoreEType t => Error "encountered CoreEType in a position where an Expr should have been"
220 | CoreECoercion co => Error "encountered CoreECoercion in a position where an Expr should have been"
221 | CoreECast e co => coreExprToWeakExpr e >>= fun e' =>
222 let (ct1,ct2) := coercionKind co
223 in coreTypeToWeakType ct1 >>= fun t1 =>
224 coreTypeToWeakType ct2 >>= fun t2 =>
225 OK (WECast e' (WCoUnsafe t1 t2))
227 | CoreEVar v => coreVarToWeakVar' v >>= fun v' => match v' with
228 | WExprVar ev => OK (WEVar ev)
229 | WTypeVar _ => Error "found a type variable inside an EVar!"
230 | WCoerVar _ => Error "found a coercion variable inside an EVar!"
233 | CoreEApp e1 e2 => match isBrak e1 with
235 coreExprToWeakExpr e2 >>= fun e' =>
236 coreTypeToWeakType t >>= fun t' =>
237 OK (WEBrak v tv e' t')
238 | None => match isEsc e1 with
240 coreExprToWeakExpr e2 >>= fun e' =>
241 coreTypeToWeakType t >>= fun t' =>
242 OK (WEEsc v tv e' t')
243 | None => match isCSP e1 with
245 coreExprToWeakExpr e2 >>= fun e' =>
246 coreTypeToWeakType t >>= fun t' =>
247 OK (WECSP v tv e' t')
252 | CoreELam v e => match coreVarToWeakVar' v with
253 | OK (WExprVar ev) =>
254 coreExprToWeakExpr e >>= fun e' =>
260 else if isKappaApp e1
262 | (CoreEApp (CoreEApp (CoreEApp (CoreEApp _ _) _) _) e1') =>
263 coreExprToWeakExpr e1' >>= fun e1'' =>
264 coreExprToWeakExpr e2 >>= fun e2'' =>
265 OK (WEKappaApp e1'' e2'')
270 coreExprToWeakExpr e1 >>= fun e1' =>
273 coreTypeToWeakType t >>= fun t' =>
275 | _ => coreExprToWeakExpr e2
276 >>= fun e2' => OK (WEApp e1' e2')
282 | CoreELam v e => coreVarToWeakVar' v >>= fun v' => match v' with
283 | WExprVar ev => coreExprToWeakExpr e >>= fun e' => OK (WELam ev e')
284 | WTypeVar tv => coreExprToWeakExpr e >>= fun e' => OK (WETyLam tv e')
285 | WCoerVar cv => coreExprToWeakExpr e >>= fun e' => OK (WECoLam cv e')
288 | CoreELet (CoreNonRec v ve) e => coreVarToWeakVar' v >>= fun v' => match v' with
289 | WExprVar ev => coreExprToWeakExpr ve >>= fun ve' =>
290 coreExprToWeakExpr e >>= fun e' => OK (WELet ev ve' e')
291 | WTypeVar tv => match e with
292 | CoreEType t => coreExprToWeakExpr e >>= fun e' =>
293 coreExprToWeakType ve >>= fun ty' =>
294 OK (WETyApp (WETyLam tv e') ty')
295 | _ => Error "saw (ELet <tyvar> e) where e!=EType"
297 | WCoerVar (weakCoerVar cv t1 t2) =>
298 coreExprToWeakExpr e >>= fun e' =>
299 coreExprToWeakCoercion t1 t2 ve >>= fun co' =>
300 OK (WECoApp (WECoLam (weakCoerVar cv t1 t2) e') co')
303 | CoreELet (CoreRec rb) e =>
304 ((fix coreExprToWeakExprList (cel:list (CoreVar * (@CoreExpr CoreVar))) : ???(list (WeakExprVar * WeakExpr)) :=
307 | (v',e')::t => coreExprToWeakExprList t >>= fun t' =>
308 coreVarToWeakVar' v' >>= fun v'' => match v'' with
309 | WExprVar ev => coreExprToWeakExpr e' >>= fun e' => OK ((ev,e')::t')
310 | WTypeVar _ => Error "found a type variable in a recursive let"
311 | WCoerVar _ => Error "found a coercion variable in a recursive let"
313 end) rb) >>= fun rb' =>
314 coreExprToWeakExpr e >>= fun e' =>
315 OK (WELetRec (unleaves' rb') e')
317 | CoreECase e v tbranches alts =>
318 coreVarToWeakVar' v >>= fun v' => match v' with
319 | WTypeVar _ => Error "found a type variable in a case"
320 | WCoerVar _ => Error "found a coercion variable in a case"
322 coreTypeToWeakType (coreTypeOfCoreExpr e) >>= fun te' =>
323 expectTyConApp te' nil >>= fun tca =>
324 let (tc,lt) := tca:(TyCon * list WeakType) in
325 ((fix mkBranches (branches: list (@triple CoreAltCon (list CoreVar) (@CoreExpr CoreVar)))
326 : ???(list (WeakAltCon*list WeakTypeVar*list WeakCoerVar*list WeakExprVar*WeakExpr)) :=
329 | (mkTriple alt vars e)::rest =>
330 mkBranches rest >>= fun rest' =>
331 coreExprToWeakExpr e >>= fun e' =>
333 | DEFAULT => OK ((WeakDEFAULT,nil,nil,nil,e')::rest')
334 | LitAlt lit => OK ((WeakLitAlt lit,nil,nil,nil,e')::rest')
335 | DataAlt dc => let vars := map coreVarToWeakVar' vars in
336 OK (((WeakDataAlt dc),
337 (filter (map (fun x => match x with OK (WTypeVar v) => Some v | _ => None end) vars)),
338 (filter (map (fun x => match x with OK (WCoerVar v) => Some v | _ => None end) vars)),
339 (filter (map (fun x => match x with OK (WExprVar v) => Some v | _ => None end) vars)),
344 coreExprToWeakExpr e >>= fun scrutinee =>
345 coreTypeToWeakType tbranches >>= fun tbranches' =>
346 OK (WECase ev scrutinee tbranches' tc lt (unleaves branches))