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.
18 (* this distinguishes SystemFC "type functions" (true) which are always fully applied from "type constructors" which aren't *)
19 Variable isFamilyTyCon : TyCon -> bool. Extract Inlined Constant isFamilyTyCon => "TyCon.isFamilyTyCon".
22 Axiom tycons_distinct : ~(ArrowTyCon=ModalBoxTyCon).
24 Variable coreVarToWeakVar : CoreVar -> WeakVar. Extract Inlined Constant coreVarToWeakVar => "coreVarToWeakVar".
26 Fixpoint coreTypeToWeakType (ct:CoreType) : ???WeakType :=
28 | TyVarTy cv => match coreVarToWeakVar cv with
29 | WExprVar _ => Error "encountered expression variable in a type"
30 | WTypeVar tv => OK (WTyVarTy tv)
31 | WCoerVar _ => Error "encountered coercion variable in a type"
34 | AppTy t1 t2 => coreTypeToWeakType t2 >>= fun t2' => coreTypeToWeakType t1 >>= fun t1' => OK (WAppTy t1' t2')
37 let recurse := ((fix rec tl := match tl with
39 | a::b => coreTypeToWeakType a >>= fun a' => rec b >>= fun b' => OK (a'::b')
41 in if (isFamilyTyCon tc)
42 then recurse >>= fun recurse' => OK (WTyFunApp tc recurse')
43 else if eqd_dec tc ModalBoxTyCon
45 | ((TyVarTy ec)::tbody::nil) =>
46 match coreVarToWeakVar ec with
47 | WTypeVar ec' => coreTypeToWeakType tbody >>= fun tbody' => OK (WCodeTy ec' tbody')
48 | WExprVar _ => Error "encountered expression variable in a modal box type"
49 | WCoerVar _ => Error "encountered coercion variable in a modal box type"
51 | _ => Error "mis-applied modal box tycon"
53 else let tc' := if eqd_dec tc ArrowTyCon
56 in recurse >>= fun recurse' => OK (fold_left (fun x y => WAppTy x y) recurse' tc')
57 | FunTy (PredTy (EqPred t1 t2)) t3 => coreTypeToWeakType t1 >>= fun t1' =>
58 coreTypeToWeakType t2 >>= fun t2' =>
59 coreTypeToWeakType t3 >>= fun t3' =>
60 OK (WCoFunTy t1' t2' t3')
61 | FunTy t1 t2 => coreTypeToWeakType t1 >>= fun t1' =>
62 coreTypeToWeakType t2 >>= fun t2' =>
63 OK (WAppTy (WAppTy WFunTyCon t1') t2')
64 | ForAllTy cv t => match coreVarToWeakVar cv with
65 | WExprVar _ => Error "encountered expression variable in a type"
66 | WTypeVar tv => coreTypeToWeakType t >>= fun t' => OK (WForAllTy tv t')
67 | WCoerVar _ => Error "encountered coercion variable in a type"
69 | PredTy (ClassP cl lct) => ((fix rec tl := match tl with
71 | a::b => coreTypeToWeakType a >>= fun a' =>
72 rec b >>= fun b' => OK (a'::b')
73 end) lct) >>= fun lct' => OK (WClassP cl lct')
74 | PredTy (IParam ipn ct) => coreTypeToWeakType ct >>= fun ct' => OK (WIParam ipn ct')
75 | PredTy (EqPred _ _) => Error "hit a bare EqPred"
78 (* detects our crude Core-encoding of modal type introduction/elimination forms *)
79 Definition isBrak (ce:@CoreExpr CoreVar) : ??(WeakTypeVar * CoreType) :=
81 | (CoreEApp (CoreEApp (CoreEVar v) (CoreEType (TyVarTy ec))) (CoreEType tbody))
82 => if coreName_eq hetmet_brak_name (coreVarCoreName v) then
83 match coreVarToWeakVar v with
85 | WTypeVar tv => Some (tv,tbody)
90 Definition isEsc (ce:@CoreExpr CoreVar) : ??(WeakTypeVar * CoreType) :=
92 | (CoreEApp (CoreEApp (CoreEVar v) (CoreEType (TyVarTy ec))) (CoreEType tbody))
93 => if coreName_eq hetmet_esc_name (coreVarCoreName v) then
94 match coreVarToWeakVar v with
96 | WTypeVar tv => Some (tv,tbody)
102 Definition coreCoercionToWeakCoercion (cc:CoreCoercion) : ???WeakCoercion :=
103 let (t1,t2) := coreCoercionKind cc
104 in coreTypeToWeakType t1 >>= fun t1' =>
105 coreTypeToWeakType t2 >>= fun t2' =>
106 OK (weakCoercion t1' t2' cc).
108 Fixpoint coreExprToWeakExpr (ce:@CoreExpr CoreVar) : ???WeakExpr :=
110 | CoreELit lit => OK (WELit lit)
111 | CoreENote n e => coreExprToWeakExpr e >>= fun e' => OK (WENote n e')
112 | CoreEType t => Error "encountered CoreEType in a position where an Expr should have been"
113 | CoreECast e co => coreExprToWeakExpr e >>= fun e' =>
114 coreCoercionToWeakCoercion co >>= fun co' =>
117 | CoreEVar v => match coreVarToWeakVar v with
118 | WExprVar ev => OK (WEVar ev)
119 | WTypeVar _ => Error "found a type variable inside an EVar!"
120 | WCoerVar _ => Error "found a coercion variable inside an EVar!"
123 | CoreEApp e1 e2 => match isBrak e1 with
125 coreExprToWeakExpr e2 >>= fun e' =>
126 coreTypeToWeakType t >>= fun t' =>
128 | None => match isEsc e1 with
130 coreExprToWeakExpr e2 >>= fun e' =>
131 coreTypeToWeakType t >>= fun t' =>
133 | None => coreExprToWeakExpr e1 >>= fun e1' =>
136 coreTypeToWeakType t >>= fun t' =>
138 | _ => coreExprToWeakExpr e2 >>= fun e2' => OK (WEApp e1' e2')
143 | CoreELam v e => match coreVarToWeakVar v with
144 | WExprVar ev => coreExprToWeakExpr e >>= fun e' => OK (WELam ev e')
145 | WTypeVar tv => coreExprToWeakExpr e >>= fun e' => OK (WETyLam tv e')
146 | WCoerVar cv => coreExprToWeakExpr e >>= fun e' => OK (WECoLam cv e')
149 | CoreELet (CoreNonRec v ve) e => match coreVarToWeakVar v with
150 | WExprVar ev => coreExprToWeakExpr ve >>= fun ve' =>
151 coreExprToWeakExpr e >>= fun e' => OK (WELet ev ve' e')
152 | WTypeVar _ => match e with
153 | CoreEType t => Error "saw a type-let"
154 | _ => Error "saw (ELet <tyvar> e) where e!=EType"
156 | WCoerVar _ => Error "saw an (ELet <coercionVar>)"
159 | CoreELet (CoreRec rb) e =>
160 ((fix coreExprToWeakExprList (cel:list (CoreVar * (@CoreExpr CoreVar))) : ???(list (WeakExprVar * WeakExpr)) :=
163 | (v',e')::t => coreExprToWeakExprList t >>= fun t' =>
164 match coreVarToWeakVar v' with
165 | WExprVar ev => coreExprToWeakExpr e' >>= fun e' => OK ((ev,e')::t')
166 | WTypeVar _ => Error "found a type variable in a recursive let"
167 | WCoerVar _ => Error "found a coercion variable in a recursive let"
169 end) rb) >>= fun rb' =>
170 coreExprToWeakExpr e >>= fun e' =>
171 OK (WELetRec (unleaves' rb') e')
173 | CoreECase e v tbranches alts =>
174 match coreVarToWeakVar v with
175 | WTypeVar _ => Error "found a type variable in a case"
176 | WCoerVar _ => Error "found a coercion variable in a case"
178 coreExprToWeakExpr e >>= fun e' =>
179 weakTypeOfWeakExpr e' >>= fun te' =>
180 (match isTyConApp te' nil with None => Error "expectTyConApp encountered strange type" | Some x => OK x end)
182 let (tc,lt) := tca in
183 ((fix mkBranches (branches: list (@triple AltCon (list CoreVar) (@CoreExpr CoreVar)))
184 : ???(list (AltCon*list WeakTypeVar*list WeakCoerVar*list WeakExprVar*WeakExpr)) :=
187 | (mkTriple alt vars e)::rest =>
188 mkBranches rest >>= fun rest' =>
189 coreExprToWeakExpr e >>= fun e' =>
191 | DEFAULT => OK ((DEFAULT,nil,nil,nil,e')::rest')
192 | LitAlt lit => OK ((LitAlt lit,nil,nil,nil,e')::rest')
193 | DataAlt dc => let vars := map coreVarToWeakVar vars in
195 (General.filter (map (fun x => match x with WTypeVar v => Some v | _ => None end) vars)),
196 (General.filter (map (fun x => match x with WCoerVar v => Some v | _ => None end) vars)),
197 (General.filter (map (fun x => match x with WExprVar v => Some v | _ => None end) vars)),
202 coreExprToWeakExpr e >>= fun scrutinee =>
203 coreTypeToWeakType tbranches >>= fun tbranches' =>
204 OK (WELet ev scrutinee (WECase (WEVar ev) tbranches' tc lt (unleaves branches)))