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 getSourceAndTargetTypesOfCoercion : CoreCoercion -> (CoreType * CoreType).
22 Extract Inlined Constant getSourceAndTargetTypesOfCoercion => "getSourceAndTargetTypesOfCoercion".
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 | CoreECast e co => coreExprToWeakExpr e >>= fun e' =>
192 let (ct1,ct2) := getSourceAndTargetTypesOfCoercion co
193 in coreTypeToWeakType ct1 >>= fun t1 =>
194 coreTypeToWeakType ct2 >>= fun t2 =>
195 OK (WECast e' (WCoUnsafe t1 t2))
197 | CoreEVar v => coreVarToWeakVar' v >>= fun v' => match v' with
198 | WExprVar ev => OK (WEVar ev)
199 | WTypeVar _ => Error "found a type variable inside an EVar!"
200 | WCoerVar _ => Error "found a coercion variable inside an EVar!"
203 | CoreEApp e1 e2 => match isBrak e1 with
205 coreExprToWeakExpr e2 >>= fun e' =>
206 coreTypeToWeakType t >>= fun t' =>
207 OK (WEBrak v tv e' t')
208 | None => match isEsc e1 with
210 coreExprToWeakExpr e2 >>= fun e' =>
211 coreTypeToWeakType t >>= fun t' =>
212 OK (WEEsc v tv e' t')
213 | None => match isCSP e1 with
215 coreExprToWeakExpr e2 >>= fun e' =>
216 coreTypeToWeakType t >>= fun t' =>
217 OK (WECSP v tv e' t')
218 | None => coreExprToWeakExpr e1 >>= fun e1' =>
221 coreTypeToWeakType t >>= fun t' =>
223 | _ => coreExprToWeakExpr e2
224 >>= fun e2' => OK (WEApp e1' e2')
230 | CoreELam v e => coreVarToWeakVar' v >>= fun v' => match v' with
231 | WExprVar ev => coreExprToWeakExpr e >>= fun e' => OK (WELam ev e')
232 | WTypeVar tv => coreExprToWeakExpr e >>= fun e' => OK (WETyLam tv e')
233 | WCoerVar cv => coreExprToWeakExpr e >>= fun e' => OK (WECoLam cv e')
236 | CoreELet (CoreNonRec v ve) e => coreVarToWeakVar' v >>= fun v' => match v' with
237 | WExprVar ev => coreExprToWeakExpr ve >>= fun ve' =>
238 coreExprToWeakExpr e >>= fun e' => OK (WELet ev ve' e')
239 | WTypeVar tv => match e with
240 | CoreEType t => coreExprToWeakExpr e >>= fun e' =>
241 coreExprToWeakType ve >>= fun ty' =>
242 OK (WETyApp (WETyLam tv e') ty')
243 | _ => Error "saw (ELet <tyvar> e) where e!=EType"
245 | WCoerVar (weakCoerVar cv t1 t2) =>
246 coreExprToWeakExpr e >>= fun e' =>
247 coreExprToWeakCoercion t1 t2 ve >>= fun co' =>
248 OK (WECoApp (WECoLam (weakCoerVar cv t1 t2) e') co')
251 | CoreELet (CoreRec rb) e =>
252 ((fix coreExprToWeakExprList (cel:list (CoreVar * (@CoreExpr CoreVar))) : ???(list (WeakExprVar * WeakExpr)) :=
255 | (v',e')::t => coreExprToWeakExprList t >>= fun t' =>
256 coreVarToWeakVar' v' >>= fun v'' => match v'' with
257 | WExprVar ev => coreExprToWeakExpr e' >>= fun e' => OK ((ev,e')::t')
258 | WTypeVar _ => Error "found a type variable in a recursive let"
259 | WCoerVar _ => Error "found a coercion variable in a recursive let"
261 end) rb) >>= fun rb' =>
262 coreExprToWeakExpr e >>= fun e' =>
263 OK (WELetRec (unleaves' rb') e')
265 | CoreECase e v tbranches alts =>
266 coreVarToWeakVar' v >>= fun v' => match v' with
267 | WTypeVar _ => Error "found a type variable in a case"
268 | WCoerVar _ => Error "found a coercion variable in a case"
270 coreTypeToWeakType (coreTypeOfCoreExpr e) >>= fun te' =>
271 expectTyConApp te' nil >>= fun tca =>
272 let (tc,lt) := tca:(TyCon * list WeakType) in
273 ((fix mkBranches (branches: list (@triple CoreAltCon (list CoreVar) (@CoreExpr CoreVar)))
274 : ???(list (WeakAltCon*list WeakTypeVar*list WeakCoerVar*list WeakExprVar*WeakExpr)) :=
277 | (mkTriple alt vars e)::rest =>
278 mkBranches rest >>= fun rest' =>
279 coreExprToWeakExpr e >>= fun e' =>
281 | DEFAULT => OK ((WeakDEFAULT,nil,nil,nil,e')::rest')
282 | LitAlt lit => OK ((WeakLitAlt lit,nil,nil,nil,e')::rest')
283 | DataAlt dc => let vars := map coreVarToWeakVar' vars in
284 OK (((WeakDataAlt dc),
285 (filter (map (fun x => match x with OK (WTypeVar v) => Some v | _ => None end) vars)),
286 (filter (map (fun x => match x with OK (WCoerVar v) => Some v | _ => None end) vars)),
287 (filter (map (fun x => match x with OK (WExprVar v) => Some v | _ => None end) vars)),
292 coreExprToWeakExpr e >>= fun scrutinee =>
293 coreTypeToWeakType tbranches >>= fun tbranches' =>
294 OK (WECase ev scrutinee tbranches' tc lt (unleaves branches))