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 HaskGeneral.
10 Require Import HaskLiterals.
11 Require Import HaskCoreVars.
12 Require Import HaskCoreTypes.
13 Require Import HaskCore.
14 Require Import HaskWeakVars.
15 Require Import HaskWeak.
17 Variable coreVarToWeakVar : CoreVar -> WeakVar. Extract Inlined Constant coreVarToWeakVar => "coreVarToWeakVar".
19 (* detects our crude Core-encoding of modal type introduction/elimination forms *)
20 Definition isBrak (ce:@CoreExpr CoreVar) : ??(WeakTypeVar * CoreType) :=
22 | (CoreEApp (CoreEApp (CoreEVar v) (CoreEType (TyVarTy ec))) (CoreEType tbody))
23 => if coreName_eq hetmet_brak_name (coreVarCoreName v) then
24 match coreVarToWeakVar v with
26 | WTypeVar tv => Some (tv,tbody)
31 Definition isEsc (ce:@CoreExpr CoreVar) : ??(WeakTypeVar * CoreType) :=
33 | (CoreEApp (CoreEApp (CoreEVar v) (CoreEType (TyVarTy ec))) (CoreEType tbody))
34 => if coreName_eq hetmet_esc_name (coreVarCoreName v) then
35 match coreVarToWeakVar v with
37 | WTypeVar tv => Some (tv,tbody)
43 Definition coreCoercionToWeakCoercion (cc:CoreCoercion) : WeakCoercion :=
44 let (t1,t2) := coreCoercionKind cc
45 in weakCoercion t1 t2 cc.
47 Fixpoint coreExprToWeakExpr (ce:@CoreExpr CoreVar) : ???WeakExpr :=
49 | CoreELit lit => OK (WELit lit)
50 | CoreENote n e => coreExprToWeakExpr e >>= fun e' => OK (WENote n e')
51 | CoreEType t => Error "encountered CoreEType in a position where an Expr should have been"
52 | CoreECast e co => coreExprToWeakExpr e >>= fun e' =>
53 OK (WECast e' (coreCoercionToWeakCoercion co))
55 | CoreEVar v => match coreVarToWeakVar v with
56 | WExprVar ev => OK (WEVar ev)
57 | WTypeVar _ => Error "found a type variable inside an EVar!"
58 | WCoerVar _ => Error "found a coercion variable inside an EVar!"
61 | CoreEApp e1 e2 => match isBrak e1 with
62 | Some (tv,t) => coreExprToWeakExpr e2 >>= fun e' => OK (WEBrak tv e' t)
63 | None => match isEsc e1 with
64 | Some (tv,t) => coreExprToWeakExpr e2 >>= fun e' => OK (WEEsc tv e' t)
65 | None => coreExprToWeakExpr e1 >>= fun e1' =>
67 | CoreEType t => OK (WETyApp e1' t)
68 | _ => coreExprToWeakExpr e2 >>= fun e2' => OK (WEApp e1' e2')
73 | CoreELam v e => match coreVarToWeakVar v with
74 | WExprVar ev => coreExprToWeakExpr e >>= fun e' => OK (WELam ev e')
75 | WTypeVar tv => coreExprToWeakExpr e >>= fun e' => OK (WETyLam tv e')
76 | WCoerVar cv => coreExprToWeakExpr e >>= fun e' => OK (WECoLam cv e')
79 | CoreELet (CoreNonRec v ve) e => match coreVarToWeakVar v with
80 | WExprVar ev => coreExprToWeakExpr ve >>= fun ve' =>
81 coreExprToWeakExpr e >>= fun e' => OK (WELet ev ve' e')
82 | WTypeVar _ => match e with
83 | CoreEType t => Error "saw a type-let"
84 | _ => Error "saw (ELet <tyvar> e) where e!=EType"
86 | WCoerVar _ => Error "saw an (ELet <coercionVar>)"
89 | CoreELet (CoreRec rb) e =>
90 ((fix coreExprToWeakExprList (cel:list (CoreVar * (@CoreExpr CoreVar))) : ???(list (WeakExprVar * WeakExpr)) :=
93 | (v',e')::t => coreExprToWeakExprList t >>= fun t' =>
94 match coreVarToWeakVar v' with
95 | WExprVar ev => coreExprToWeakExpr e' >>= fun e' => OK ((ev,e')::t')
96 | WTypeVar _ => Error "found a type variable in a recursive let"
97 | WCoerVar _ => Error "found a coercion variable in a recursive let"
99 end) rb) >>= fun rb' =>
100 coreExprToWeakExpr e >>= fun e' =>
101 OK (WELetRec (unleaves' rb') e')
103 | CoreECase e v tbranches alts =>
104 match coreVarToWeakVar v with
105 | WTypeVar _ => Error "found a type variable in a case"
106 | WCoerVar _ => Error "found a coercion variable in a case"
109 >>= fun e' => coreTypeOfWeakExpr e' >>= fun te' =>
111 | TyConApp _ tc lt =>
112 ((fix mkBranches (branches: list (@triple AltCon (list CoreVar) (@CoreExpr CoreVar)))
113 : ???(list (AltCon*list WeakVar*WeakExpr)) :=
116 | (mkTriple alt vars e)::rest =>
117 mkBranches rest >>= fun rest' =>
118 coreExprToWeakExpr e >>= fun e' =>
120 | DEFAULT => OK ((DEFAULT,nil,e')::rest')
121 | LitAlt lit => OK ((LitAlt lit,nil,e')::rest')
122 | DataAlt _ _ _ _ tc' dc => OK (((DataAlt _ dc),(map coreVarToWeakVar vars),e')::rest')
125 >>= fun branches => coreExprToWeakExpr e
127 list2vecOrError lt _ >>= fun lt' =>
128 OK (WELet ev scrutinee (WECase (WEVar ev) tbranches tc lt' (unleaves branches)))
129 | _ => Error "found a case whose scrutinee's type wasn't a TyConApp"