1 (*********************************************************************************************************************************)
2 (* HaskCoreToWeak: convert HaskCore to HaskWeak *)
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 HaskLiteralsAndTyCons.
11 Require Import HaskCoreVars.
12 Require Import HaskCoreTypes.
13 Require Import HaskCore.
14 Require Import HaskWeakVars.
15 Require Import HaskWeakTypes.
16 Require Import HaskWeak.
18 Variable ModalBoxTyCon : TyCon. Extract Inlined Constant ModalBoxTyCon => "TysWiredIn.hetMetCodeTypeTyCon".
19 Variable ArrowTyCon : TyCon. Extract Constant ArrowTyCon => "Type.funTyCon".
21 Variable tyConOrTyFun : CoreTyCon -> sum TyCon TyFun. Extract Inlined Constant tyConOrTyFun => "tyConOrTyFun".
22 Variable coreViewDeep : CoreType -> CoreType. Extract Inlined Constant coreViewDeep => "coreViewDeep".
23 Variable coreCoercionToWeakCoercion : CoreCoercion -> WeakCoercion.
24 Extract Inlined Constant coreCoercionToWeakCoercion => "coreCoercionToWeakCoercion".
26 (* extracts the Name from a CoreVar *)
27 Variable coreVarCoreName : CoreVar -> CoreName. Extract Inlined Constant coreVarCoreName => "Var.varName".
29 (* the magic wired-in name for the modal type introduction/elimination forms *)
30 Variable hetmet_brak_name : CoreName. Extract Inlined Constant hetmet_brak_name => "PrelNames.hetmet_brak_name".
31 Variable hetmet_esc_name : CoreName. Extract Inlined Constant hetmet_esc_name => "PrelNames.hetmet_esc_name".
32 Variable hetmet_csp_name : CoreName. Extract Inlined Constant hetmet_csp_name => "PrelNames.hetmet_csp_name".
34 Fixpoint coreTypeToWeakType' (ct:CoreType) : ???WeakType :=
36 | TyVarTy cv => match coreVarToWeakVar cv with
37 | WExprVar _ => Error "encountered expression variable in a type"
38 | WTypeVar tv => OK (WTyVarTy tv)
39 | WCoerVar _ => Error "encountered coercion variable in a type"
42 | AppTy t1 t2 => coreTypeToWeakType' t2 >>= fun t2' => coreTypeToWeakType' t1 >>= fun t1' => OK (WAppTy t1' t2')
45 let recurse := ((fix rec tl := match tl with
47 | a::b => coreTypeToWeakType' a >>= fun a' => rec b >>= fun b' => OK (a'::b')
49 in match tyConOrTyFun tc_ with
50 | inr tf => recurse >>= fun recurse' => OK (WTyFunApp tf recurse')
51 | inl tc => if eqd_dec tc ModalBoxTyCon
53 | ((TyVarTy ec)::tbody::nil) =>
54 match coreVarToWeakVar ec with
55 | WTypeVar ec' => coreTypeToWeakType' tbody >>= fun tbody' => OK (WCodeTy ec' tbody')
56 | WExprVar _ => Error "encountered expression variable in a modal box type"
57 | WCoerVar _ => Error "encountered coercion variable in a modal box type"
59 | _ => Error ("mis-applied modal box tycon: " +++ ct)
61 else let tc' := if eqd_dec tc ArrowTyCon
64 in recurse >>= fun recurse' => OK (fold_left (fun x y => WAppTy x y) recurse' tc')
66 | FunTy (PredTy (EqPred t1 t2)) t3 => coreTypeToWeakType' t1 >>= fun t1' =>
67 coreTypeToWeakType' t2 >>= fun t2' =>
68 coreTypeToWeakType' t3 >>= fun t3' =>
69 OK (WCoFunTy t1' t2' t3')
70 | FunTy t1 t2 => coreTypeToWeakType' t1 >>= fun t1' =>
71 coreTypeToWeakType' t2 >>= fun t2' =>
72 OK (WAppTy (WAppTy WFunTyCon t1') t2')
73 | ForAllTy cv t => match coreVarToWeakVar cv with
74 | WExprVar _ => Error "encountered expression variable in a type"
75 | WTypeVar tv => coreTypeToWeakType' t >>= fun t' => OK (WForAllTy tv t')
76 | WCoerVar _ => Error "encountered coercion variable in a type"
78 | PredTy (ClassP cl lct) => ((fix rec tl := match tl with
80 | a::b => coreTypeToWeakType' a >>= fun a' =>
81 rec b >>= fun b' => OK (a'::b')
82 end) lct) >>= fun lct' => OK (WClassP cl lct')
83 | PredTy (IParam ipn ct) => coreTypeToWeakType' ct >>= fun ct' => OK (WIParam ipn ct')
84 | PredTy (EqPred _ _) => Error "hit a bare EqPred"
87 Fixpoint coreTypeToWeakType t := addErrorMessage "coreTypeToWeakType" (coreTypeToWeakType' (coreViewDeep t)).
89 (* detects our crude Core-encoding of modal type introduction/elimination forms *)
90 Definition isBrak (ce:@CoreExpr CoreVar) : ??(WeakExprVar * WeakTypeVar * CoreType) :=
92 | (CoreEApp (CoreEApp (CoreEVar v) (CoreEType (TyVarTy ec))) (CoreEType tbody))
93 => if coreName_eq hetmet_brak_name (coreVarCoreName v) then
94 match coreVarToWeakVar ec with
97 | WTypeVar tv => match coreVarToWeakVar v with
98 | WExprVar v' => Some (v',tv,tbody)
105 Definition isEsc (ce:@CoreExpr CoreVar) : ??(WeakExprVar * WeakTypeVar * CoreType) :=
107 | (CoreEApp (CoreEApp (CoreEVar v) (CoreEType (TyVarTy ec))) (CoreEType tbody))
108 => if coreName_eq hetmet_esc_name (coreVarCoreName v) then
109 match coreVarToWeakVar ec with
111 | WTypeVar tv => match coreVarToWeakVar v with
112 | WExprVar v' => Some (v',tv,tbody)
120 Definition isCSP (ce:@CoreExpr CoreVar) : ??(WeakExprVar * WeakTypeVar * CoreType) :=
122 | (CoreEApp (CoreEApp (CoreEVar v) (CoreEType (TyVarTy ec))) (CoreEType tbody))
123 => if coreName_eq hetmet_csp_name (coreVarCoreName v) then
124 match coreVarToWeakVar ec with
126 | WTypeVar tv => match coreVarToWeakVar v with
127 | WExprVar v' => Some (v',tv,tbody)
135 (* if this is a (WAppTy (WAppTy ... (WTyCon tc) .. ) .. ), return (tc,[...]) *)
136 Fixpoint expectTyConApp (wt:WeakType)(acc:list WeakType) : ???(TyCon * list WeakType) :=
138 | WTyCon tc => OK (tc,acc)
139 | WAppTy t1 t2 => expectTyConApp t1 (t2::acc)
140 | WTyFunApp tc tys => Error ("expectTyConApp encountered TyFunApp: " +++ wt)
141 | _ => Error ("expectTyConApp encountered " +++ wt)
144 Fixpoint coreExprToWeakExpr (ce:@CoreExpr CoreVar) : ???WeakExpr :=
146 | CoreELit lit => OK (WELit lit)
147 | CoreENote n e => coreExprToWeakExpr e >>= fun e' => OK (WENote n e')
148 | CoreEType t => Error "encountered CoreEType in a position where an Expr should have been"
149 | CoreECast e co => coreExprToWeakExpr e >>= fun e' =>
150 OK (WECast e' (coreCoercionToWeakCoercion co))
152 | CoreEVar v => match coreVarToWeakVar v with
153 | WExprVar ev => OK (WEVar ev)
154 | WTypeVar _ => Error "found a type variable inside an EVar!"
155 | WCoerVar _ => Error "found a coercion variable inside an EVar!"
158 | CoreEApp e1 e2 => match isBrak e1 with
160 coreExprToWeakExpr e2 >>= fun e' =>
161 coreTypeToWeakType t >>= fun t' =>
162 OK (WEBrak v tv e' t')
163 | None => match isEsc e1 with
165 coreExprToWeakExpr e2 >>= fun e' =>
166 coreTypeToWeakType t >>= fun t' =>
167 OK (WEEsc v tv e' t')
168 | None => match isCSP e1 with
170 coreExprToWeakExpr e2 >>= fun e' =>
171 coreTypeToWeakType t >>= fun t' =>
172 OK (WECSP v tv e' t')
173 | None => coreExprToWeakExpr e1 >>= fun e1' =>
176 coreTypeToWeakType t >>= fun t' =>
178 | _ => coreExprToWeakExpr e2
179 >>= fun e2' => OK (WEApp e1' e2')
185 | CoreELam v e => match coreVarToWeakVar v with
186 | WExprVar ev => coreExprToWeakExpr e >>= fun e' => OK (WELam ev e')
187 | WTypeVar tv => coreExprToWeakExpr e >>= fun e' => OK (WETyLam tv e')
188 | WCoerVar cv => coreExprToWeakExpr e >>= fun e' => OK (WECoLam cv e')
191 | CoreELet (CoreNonRec v ve) e => match coreVarToWeakVar v with
192 | WExprVar ev => coreExprToWeakExpr ve >>= fun ve' =>
193 coreExprToWeakExpr e >>= fun e' => OK (WELet ev ve' e')
194 | WTypeVar _ => match e with
195 | CoreEType t => Error "saw a type-let"
196 | _ => Error "saw (ELet <tyvar> e) where e!=EType"
198 | WCoerVar _ => Error "saw an (ELet <coercionVar>)"
201 | CoreELet (CoreRec rb) e =>
202 ((fix coreExprToWeakExprList (cel:list (CoreVar * (@CoreExpr CoreVar))) : ???(list (WeakExprVar * WeakExpr)) :=
205 | (v',e')::t => coreExprToWeakExprList t >>= fun t' =>
206 match coreVarToWeakVar v' with
207 | WExprVar ev => coreExprToWeakExpr e' >>= fun e' => OK ((ev,e')::t')
208 | WTypeVar _ => Error "found a type variable in a recursive let"
209 | WCoerVar _ => Error "found a coercion variable in a recursive let"
211 end) rb) >>= fun rb' =>
212 coreExprToWeakExpr e >>= fun e' =>
213 OK (WELetRec (unleaves' rb') e')
215 | CoreECase e v tbranches alts =>
216 match coreVarToWeakVar v with
217 | WTypeVar _ => Error "found a type variable in a case"
218 | WCoerVar _ => Error "found a coercion variable in a case"
220 coreTypeToWeakType (coreTypeOfCoreExpr e) >>= fun te' =>
221 coreExprToWeakExpr e >>= fun e' =>
222 expectTyConApp te' nil >>= fun tca =>
223 let (tc,lt) := tca in
224 ((fix mkBranches (branches: list (@triple CoreAltCon (list CoreVar) (@CoreExpr CoreVar)))
225 : ???(list (WeakAltCon*list WeakTypeVar*list WeakCoerVar*list WeakExprVar*WeakExpr)) :=
228 | (mkTriple alt vars e)::rest =>
229 mkBranches rest >>= fun rest' =>
230 coreExprToWeakExpr e >>= fun e' =>
232 | DEFAULT => OK ((WeakDEFAULT,nil,nil,nil,e')::rest')
233 | LitAlt lit => OK ((WeakLitAlt lit,nil,nil,nil,e')::rest')
234 | DataAlt dc => let vars := map coreVarToWeakVar vars in
235 OK (((WeakDataAlt dc),
236 (General.filter (map (fun x => match x with WTypeVar v => Some v | _ => None end) vars)),
237 (General.filter (map (fun x => match x with WCoerVar v => Some v | _ => None end) vars)),
238 (General.filter (map (fun x => match x with WExprVar v => Some v | _ => None end) vars)),
243 coreExprToWeakExpr e >>= fun scrutinee =>
244 coreTypeToWeakType tbranches >>= fun tbranches' =>
245 OK (WECase ev scrutinee tbranches' tc lt (unleaves branches))