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 HaskCoreLiterals.
11 Require Import HaskCoreVars.
12 Require Import HaskCoreTypes.
13 Require Import HaskCore.
14 Require Import HaskWeakVars.
15 Require Import HaskWeakTypes.
16 Require Import HaskWeak.
17 Require Import HaskWeakToCore.
19 Axiom tycons_distinct : ~(ArrowTyCon=ModalBoxTyCon).
20 Variable tyConOrTyFun : CoreTyCon -> sum TyCon TyFun. Extract Inlined Constant tyConOrTyFun => "tyConOrTyFun".
22 Fixpoint coreTypeToWeakType' (ct:CoreType) : ???WeakType :=
24 | TyVarTy cv => match coreVarToWeakVar cv with
25 | WExprVar _ => Error "encountered expression variable in a type"
26 | WTypeVar tv => OK (WTyVarTy tv)
27 | WCoerVar _ => Error "encountered coercion variable in a type"
30 | AppTy t1 t2 => coreTypeToWeakType' t2 >>= fun t2' => coreTypeToWeakType' t1 >>= fun t1' => OK (WAppTy t1' t2')
33 let recurse := ((fix rec tl := match tl with
35 | a::b => coreTypeToWeakType' a >>= fun a' => rec b >>= fun b' => OK (a'::b')
37 in match tyConOrTyFun tc_ with
38 | inr tf => recurse >>= fun recurse' => OK (WTyFunApp tf recurse')
39 | inl tc => if eqd_dec tc ModalBoxTyCon
41 | ((TyVarTy ec)::tbody::nil) =>
42 match coreVarToWeakVar ec with
43 | WTypeVar ec' => coreTypeToWeakType' tbody >>= fun tbody' => OK (WCodeTy ec' tbody')
44 | WExprVar _ => Error "encountered expression variable in a modal box type"
45 | WCoerVar _ => Error "encountered coercion variable in a modal box type"
47 | _ => Error "mis-applied modal box tycon"
49 else let tc' := if eqd_dec tc ArrowTyCon
52 in recurse >>= fun recurse' => OK (fold_left (fun x y => WAppTy x y) recurse' tc')
54 | FunTy (PredTy (EqPred t1 t2)) t3 => coreTypeToWeakType' t1 >>= fun t1' =>
55 coreTypeToWeakType' t2 >>= fun t2' =>
56 coreTypeToWeakType' t3 >>= fun t3' =>
57 OK (WCoFunTy t1' t2' t3')
58 | FunTy t1 t2 => coreTypeToWeakType' t1 >>= fun t1' =>
59 coreTypeToWeakType' t2 >>= fun t2' =>
60 OK (WAppTy (WAppTy WFunTyCon t1') t2')
61 | ForAllTy cv t => match coreVarToWeakVar cv with
62 | WExprVar _ => Error "encountered expression variable in a type"
63 | WTypeVar tv => coreTypeToWeakType' t >>= fun t' => OK (WForAllTy tv t')
64 | WCoerVar _ => Error "encountered coercion variable in a type"
66 | PredTy (ClassP cl lct) => ((fix rec tl := match tl with
68 | a::b => coreTypeToWeakType' a >>= fun a' =>
69 rec b >>= fun b' => OK (a'::b')
70 end) lct) >>= fun lct' => OK (WClassP cl lct')
71 | PredTy (IParam ipn ct) => coreTypeToWeakType' ct >>= fun ct' => OK (WIParam ipn ct')
72 | PredTy (EqPred _ _) => Error "hit a bare EqPred"
75 Variable coreViewDeep : CoreType -> CoreType. Extract Inlined Constant coreViewDeep => "coreViewDeep".
76 Definition coreTypeToWeakType t := coreTypeToWeakType' (coreViewDeep t).
78 Definition weakTypeOfWeakExpr (we:WeakExpr) : ???WeakType :=
79 coreTypeToWeakType (coreTypeOfCoreExpr (weakExprToCoreExpr we)).
81 (* detects our crude Core-encoding of modal type introduction/elimination forms *)
82 Definition isBrak (ce:@CoreExpr CoreVar) : ??(CoreVar * WeakTypeVar * CoreType) :=
84 | (CoreEApp (CoreEApp (CoreEVar v) (CoreEType (TyVarTy ec))) (CoreEType tbody))
85 => if coreName_eq hetmet_brak_name (coreVarCoreName v) then
86 match coreVarToWeakVar ec with
88 | WTypeVar tv => Some (v,tv,tbody)
93 Definition isEsc (ce:@CoreExpr CoreVar) : ??(CoreVar * WeakTypeVar * CoreType) :=
95 | (CoreEApp (CoreEApp (CoreEVar v) (CoreEType (TyVarTy ec))) (CoreEType tbody))
96 => if coreName_eq hetmet_esc_name (coreVarCoreName v) then
97 match coreVarToWeakVar ec with
99 | WTypeVar tv => Some (v,tv,tbody)
105 Definition coreCoercionToWeakCoercion (cc:CoreCoercion) : ???WeakCoercion :=
106 let (t1,t2) := coreCoercionKind cc
107 in coreTypeToWeakType t1 >>= fun t1' =>
108 coreTypeToWeakType t2 >>= fun t2' =>
109 OK (weakCoercion (kindOfCoreType t1) t1' t2' cc).
111 Fixpoint coreExprToWeakExpr (ce:@CoreExpr CoreVar) : ???WeakExpr :=
113 | CoreELit lit => OK (WELit lit)
114 | CoreENote n e => coreExprToWeakExpr e >>= fun e' => OK (WENote n e')
115 | CoreEType t => Error "encountered CoreEType in a position where an Expr should have been"
116 | CoreECast e co => coreExprToWeakExpr e >>= fun e' =>
117 coreCoercionToWeakCoercion co >>= fun co' =>
120 | CoreEVar v => match coreVarToWeakVar v with
121 | WExprVar ev => OK (WEVar ev)
122 | WTypeVar _ => Error "found a type variable inside an EVar!"
123 | WCoerVar _ => Error "found a coercion variable inside an EVar!"
126 | CoreEApp e1 e2 => match isBrak e1 with
128 coreExprToWeakExpr e2 >>= fun e' =>
129 coreTypeToWeakType t >>= fun t' =>
130 OK (WEBrak v tv e' t')
131 | None => match isEsc e1 with
133 coreExprToWeakExpr e2 >>= fun e' =>
134 coreTypeToWeakType t >>= fun t' =>
135 OK (WEEsc v tv e' t')
136 | None => coreExprToWeakExpr e1 >>= fun e1' =>
139 coreTypeToWeakType t >>= fun t' =>
141 | _ => coreExprToWeakExpr e2 >>= fun e2' => OK (WEApp e1' e2')
146 | CoreELam v e => match coreVarToWeakVar v with
147 | WExprVar ev => coreExprToWeakExpr e >>= fun e' => OK (WELam ev e')
148 | WTypeVar tv => coreExprToWeakExpr e >>= fun e' => OK (WETyLam tv e')
149 | WCoerVar cv => coreExprToWeakExpr e >>= fun e' => OK (WECoLam cv e')
152 | CoreELet (CoreNonRec v ve) e => match coreVarToWeakVar v with
153 | WExprVar ev => coreExprToWeakExpr ve >>= fun ve' =>
154 coreExprToWeakExpr e >>= fun e' => OK (WELet ev ve' e')
155 | WTypeVar _ => match e with
156 | CoreEType t => Error "saw a type-let"
157 | _ => Error "saw (ELet <tyvar> e) where e!=EType"
159 | WCoerVar _ => Error "saw an (ELet <coercionVar>)"
162 | CoreELet (CoreRec rb) e =>
163 ((fix coreExprToWeakExprList (cel:list (CoreVar * (@CoreExpr CoreVar))) : ???(list (WeakExprVar * WeakExpr)) :=
166 | (v',e')::t => coreExprToWeakExprList t >>= fun t' =>
167 match coreVarToWeakVar v' with
168 | WExprVar ev => coreExprToWeakExpr e' >>= fun e' => OK ((ev,e')::t')
169 | WTypeVar _ => Error "found a type variable in a recursive let"
170 | WCoerVar _ => Error "found a coercion variable in a recursive let"
172 end) rb) >>= fun rb' =>
173 coreExprToWeakExpr e >>= fun e' =>
174 OK (WELetRec (unleaves' rb') e')
176 | CoreECase e v tbranches alts =>
177 match coreVarToWeakVar v with
178 | WTypeVar _ => Error "found a type variable in a case"
179 | WCoerVar _ => Error "found a coercion variable in a case"
181 coreExprToWeakExpr e >>= fun e' =>
182 weakTypeOfWeakExpr e' >>= fun te' =>
183 (match isTyConApp te' nil with None => Error "expectTyConApp encountered strange type" | Some x => OK x end)
185 let (tc,lt) := tca in
186 ((fix mkBranches (branches: list (@triple AltCon (list CoreVar) (@CoreExpr CoreVar)))
187 : ???(list (AltCon*list WeakTypeVar*list WeakCoerVar*list WeakExprVar*WeakExpr)) :=
190 | (mkTriple alt vars e)::rest =>
191 mkBranches rest >>= fun rest' =>
192 coreExprToWeakExpr e >>= fun e' =>
194 | DEFAULT => OK ((DEFAULT,nil,nil,nil,e')::rest')
195 | LitAlt lit => OK ((LitAlt lit,nil,nil,nil,e')::rest')
196 | DataAlt dc => let vars := map coreVarToWeakVar vars in
198 (General.filter (map (fun x => match x with WTypeVar v => Some v | _ => None end) vars)),
199 (General.filter (map (fun x => match x with WCoerVar v => Some v | _ => None end) vars)),
200 (General.filter (map (fun x => match x with WExprVar v => Some v | _ => None end) vars)),
205 coreExprToWeakExpr e >>= fun scrutinee =>
206 coreTypeToWeakType tbranches >>= fun tbranches' =>
207 OK (WECase ev scrutinee tbranches' tc lt (unleaves branches))