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 coreCoercionToWeakCoercion : CoreCoercion -> WeakCoercion.
22 Extract Inlined Constant coreCoercionToWeakCoercion => "coreCoercionToWeakCoercion".
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 Fixpoint coreTypeToWeakType' (ct:CoreType) : ???WeakType :=
40 | TyVarTy cv => match coreVarToWeakVar cv with
41 | WExprVar _ => Error "encountered expression variable in a type"
42 | WTypeVar tv => OK (WTyVarTy tv)
43 | WCoerVar _ => Error "encountered coercion variable in a type"
46 | AppTy t1 t2 => coreTypeToWeakType' t2 >>= fun t2' => coreTypeToWeakType' t1 >>= fun t1' => OK (WAppTy t1' t2')
49 let recurse := ((fix rec tl := match tl with
51 | a::b => coreTypeToWeakType' a >>= fun a' => rec b >>= fun b' => OK (a'::b')
53 in match tyConOrTyFun tc_ with
54 | inr tf => recurse >>= fun recurse' => mkTyFunApplication tf recurse'
55 | inl tc => if eqd_dec tc ModalBoxTyCon
57 | ((TyVarTy ec)::tbody::nil) =>
58 match coreVarToWeakVar ec with
59 | WTypeVar ec' => coreTypeToWeakType' tbody >>= fun tbody' => OK (WCodeTy ec' tbody')
60 | WExprVar _ => Error "encountered expression variable in a modal box type"
61 | WCoerVar _ => Error "encountered coercion variable in a modal box type"
63 | _ => Error ("mis-applied modal box tycon: " +++ toString ct)
65 else let tc' := if eqd_dec tc ArrowTyCon
68 in recurse >>= fun recurse' => OK (fold_left (fun x y => WAppTy x y) recurse' tc')
70 | FunTy (PredTy (EqPred t1 t2)) t3 => coreTypeToWeakType' t1 >>= fun t1' =>
71 coreTypeToWeakType' t2 >>= fun t2' =>
72 coreTypeToWeakType' t3 >>= fun t3' =>
73 OK (WCoFunTy t1' t2' t3')
74 | FunTy t1 t2 => coreTypeToWeakType' t1 >>= fun t1' =>
75 coreTypeToWeakType' t2 >>= fun t2' =>
76 OK (WAppTy (WAppTy WFunTyCon t1') t2')
77 | ForAllTy cv t => match coreVarToWeakVar cv with
78 | WExprVar _ => Error "encountered expression variable in a type abstraction"
79 | WTypeVar tv => coreTypeToWeakType' t >>= fun t' => OK (WForAllTy tv t')
80 | WCoerVar (weakCoerVar v t1' t2') =>
81 coreTypeToWeakType' t >>= fun t3' =>
82 OK (WCoFunTy t1' t2' t3')
84 | PredTy (ClassP cl lct) => ((fix rec tl := match tl with
86 | a::b => coreTypeToWeakType' a >>= fun a' =>
87 rec b >>= fun b' => OK (a'::b')
88 end) lct) >>= fun lct' => OK (WClassP cl lct')
89 | PredTy (IParam ipn ct) => coreTypeToWeakType' ct >>= fun ct' => OK (WIParam ipn ct')
90 | PredTy (EqPred _ _) => Error "hit a bare EqPred"
93 Definition coreTypeToWeakType t :=
94 addErrorMessage ("during coreTypeToWeakType on " +++ toString t +++ eol) (coreTypeToWeakType' (coreViewDeep t)).
96 (* detects our crude Core-encoding of modal type introduction/elimination forms *)
97 Definition isBrak (ce:@CoreExpr CoreVar) : ??(WeakExprVar * WeakTypeVar * CoreType) :=
99 | (CoreEApp (CoreEApp (CoreEVar v) (CoreEType (TyVarTy ec))) (CoreEType tbody))
100 => if coreName_eq hetmet_brak_name (coreVarCoreName v) then
101 match coreVarToWeakVar ec with
104 | WTypeVar tv => match coreVarToWeakVar v with
105 | WExprVar v' => Some (v',tv,tbody)
112 Definition isEsc (ce:@CoreExpr CoreVar) : ??(WeakExprVar * WeakTypeVar * CoreType) :=
114 | (CoreEApp (CoreEApp (CoreEVar v) (CoreEType (TyVarTy ec))) (CoreEType tbody))
115 => if coreName_eq hetmet_esc_name (coreVarCoreName v) then
116 match coreVarToWeakVar ec with
118 | WTypeVar tv => match coreVarToWeakVar v with
119 | WExprVar v' => Some (v',tv,tbody)
127 Definition isCSP (ce:@CoreExpr CoreVar) : ??(WeakExprVar * WeakTypeVar * CoreType) :=
129 | (CoreEApp (CoreEApp (CoreEVar v) (CoreEType (TyVarTy ec))) (CoreEType tbody))
130 => if coreName_eq hetmet_csp_name (coreVarCoreName v) then
131 match coreVarToWeakVar ec with
133 | WTypeVar tv => match coreVarToWeakVar v with
134 | WExprVar v' => Some (v',tv,tbody)
142 (* if this is a (WAppTy (WAppTy ... (WTyCon tc) .. ) .. ), return (tc,[...]) *)
143 Fixpoint expectTyConApp (wt:WeakType)(acc:list WeakType) : ???(TyCon * list WeakType) :=
145 | WTyCon tc => OK (tc,acc)
146 | WAppTy t1 t2 => expectTyConApp t1 (t2::acc)
147 | WTyFunApp tc tys => Error ("expectTyConApp encountered TyFunApp: " +++ toString wt)
148 | _ => Error ("expectTyConApp encountered " +++ toString wt)
151 Fixpoint coreExprToWeakExpr (ce:@CoreExpr CoreVar) : ???WeakExpr :=
153 | CoreELit lit => OK (WELit lit)
154 | CoreENote n e => coreExprToWeakExpr e >>= fun e' => OK (WENote n e')
155 | CoreEType t => Error "encountered CoreEType in a position where an Expr should have been"
156 | CoreECast e co => coreExprToWeakExpr e >>= fun e' =>
157 OK (WECast e' (coreCoercionToWeakCoercion co))
159 | CoreEVar v => match coreVarToWeakVar v with
160 | WExprVar ev => OK (WEVar ev)
161 | WTypeVar _ => Error "found a type variable inside an EVar!"
162 | WCoerVar _ => Error "found a coercion variable inside an EVar!"
165 | CoreEApp e1 e2 => match isBrak e1 with
167 coreExprToWeakExpr e2 >>= fun e' =>
168 coreTypeToWeakType t >>= fun t' =>
169 OK (WEBrak v tv e' t')
170 | None => match isEsc e1 with
172 coreExprToWeakExpr e2 >>= fun e' =>
173 coreTypeToWeakType t >>= fun t' =>
174 OK (WEEsc v tv e' t')
175 | None => match isCSP e1 with
177 coreExprToWeakExpr e2 >>= fun e' =>
178 coreTypeToWeakType t >>= fun t' =>
179 OK (WECSP v tv e' t')
180 | None => coreExprToWeakExpr e1 >>= fun e1' =>
183 coreTypeToWeakType t >>= fun t' =>
185 | _ => coreExprToWeakExpr e2
186 >>= fun e2' => OK (WEApp e1' e2')
192 | CoreELam v e => match coreVarToWeakVar v with
193 | WExprVar ev => coreExprToWeakExpr e >>= fun e' => OK (WELam ev e')
194 | WTypeVar tv => coreExprToWeakExpr e >>= fun e' => OK (WETyLam tv e')
195 | WCoerVar cv => coreExprToWeakExpr e >>= fun e' => OK (WECoLam cv e')
198 | CoreELet (CoreNonRec v ve) e => match coreVarToWeakVar v with
199 | WExprVar ev => coreExprToWeakExpr ve >>= fun ve' =>
200 coreExprToWeakExpr e >>= fun e' => OK (WELet ev ve' e')
201 | WTypeVar _ => match e with
202 | CoreEType t => Error "saw a type-let"
203 | _ => Error "saw (ELet <tyvar> e) where e!=EType"
205 | WCoerVar _ => Error "saw an (ELet <coercionVar>)"
208 | CoreELet (CoreRec rb) e =>
209 ((fix coreExprToWeakExprList (cel:list (CoreVar * (@CoreExpr CoreVar))) : ???(list (WeakExprVar * WeakExpr)) :=
212 | (v',e')::t => coreExprToWeakExprList t >>= fun t' =>
213 match coreVarToWeakVar v' with
214 | WExprVar ev => coreExprToWeakExpr e' >>= fun e' => OK ((ev,e')::t')
215 | WTypeVar _ => Error "found a type variable in a recursive let"
216 | WCoerVar _ => Error "found a coercion variable in a recursive let"
218 end) rb) >>= fun rb' =>
219 coreExprToWeakExpr e >>= fun e' =>
220 OK (WELetRec (unleaves' rb') e')
222 | CoreECase e v tbranches alts =>
223 match coreVarToWeakVar v with
224 | WTypeVar _ => Error "found a type variable in a case"
225 | WCoerVar _ => Error "found a coercion variable in a case"
227 coreTypeToWeakType (coreTypeOfCoreExpr e) >>= fun te' =>
228 expectTyConApp te' nil >>= fun tca =>
229 let (tc,lt) := tca:(TyCon * list WeakType) in
230 ((fix mkBranches (branches: list (@triple CoreAltCon (list CoreVar) (@CoreExpr CoreVar)))
231 : ???(list (WeakAltCon*list WeakTypeVar*list WeakCoerVar*list WeakExprVar*WeakExpr)) :=
234 | (mkTriple alt vars e)::rest =>
235 mkBranches rest >>= fun rest' =>
236 coreExprToWeakExpr e >>= fun e' =>
238 | DEFAULT => OK ((WeakDEFAULT,nil,nil,nil,e')::rest')
239 | LitAlt lit => OK ((WeakLitAlt lit,nil,nil,nil,e')::rest')
240 | DataAlt dc => let vars := map coreVarToWeakVar vars in
241 OK (((WeakDataAlt dc),
242 (filter (map (fun x => match x with WTypeVar v => Some v | _ => None end) vars)),
243 (filter (map (fun x => match x with WCoerVar v => Some v | _ => None end) vars)),
244 (filter (map (fun x => match x with WExprVar v => Some v | _ => None end) vars)),
249 coreExprToWeakExpr e >>= fun scrutinee =>
250 coreTypeToWeakType tbranches >>= fun tbranches' =>
251 OK (WECase ev scrutinee tbranches' tc lt (unleaves branches))