1 (*********************************************************************************************************************************)
2 (* HaskCoreToWeak: convert HaskCore to HaskWeak *)
3 (*********************************************************************************************************************************)
5 Generalizable All Variables.
6 Require Import Preamble.
7 Require Import General.
8 Require Import HaskGeneral.
9 Require Import HaskLiterals.
10 Require Import HaskCoreVars.
11 Require Import HaskCoreTypes.
12 Require Import HaskCore.
13 Require Import HaskWeak.
15 Fixpoint coreExprToWeakExpr (ce:CoreExpr CoreVar) : ???WeakExpr :=
17 | CoreELit lit => OK (WELit lit)
18 | CoreENote n e => coreExprToWeakExpr e >>= fun e' => OK (WENote n e')
19 | CoreEType t => Error "encountered CoreEType in a position where an Expr should have been"
20 | CoreECast e co => coreExprToWeakExpr e >>= fun e' => OK (WECast e' co)
22 | CoreEVar v => match coreVarSort v with
23 | CoreExprVar _ => OK (WEVar v)
24 | CoreTypeVar _ => Error "found a type variable inside an EVar!"
25 | CoreCoerVar _ => Error "found a coercion variable inside an EVar!"
28 | CoreEApp e1 e2 => match isBrak e1 with
29 | Some tv => coreExprToWeakExpr e2 >>= fun e' => OK (WEBrak tv e')
30 | None => match isEsc e1 with
31 | Some tv => coreExprToWeakExpr e2 >>= fun e' => OK (WEEsc tv e')
32 | None => coreExprToWeakExpr e1 >>= fun e1' =>
34 | CoreEType t => OK (WETyApp e1' t)
35 | _ => coreExprToWeakExpr e2 >>= fun e2' => OK (WEApp e1' e2')
40 | CoreELam v e => match coreVarSort v with
41 | CoreExprVar _ => coreExprToWeakExpr e >>= fun e' => OK (WELam v e')
42 | CoreTypeVar _ => coreExprToWeakExpr e >>= fun e' => OK (WETyLam v e')
43 | CoreCoerVar _ => coreExprToWeakExpr e >>= fun e' => OK (WECoLam v e')
46 | CoreELet (CoreNonRec v ve) e => match coreVarSort v with
47 | CoreExprVar _ => coreExprToWeakExpr ve >>= fun ve' =>
48 coreExprToWeakExpr e >>= fun e' => OK (WELet v ve' e')
49 | CoreTypeVar _ => match e with
50 | CoreEType t => Error "saw a type-let"
51 | _ => Error "saw (ELet <tyvar> e) where e!=EType"
53 | CoreCoerVar _ => Error "saw an (ELet <coercionVar>)"
56 | CoreELet (CoreRec rb) e =>
57 ((fix coreExprToWeakExprList (cel:list (CoreVar * (CoreExpr CoreVar))) : ???(list (CoreVar * WeakExpr)) :=
60 | (v',e')::t => coreExprToWeakExprList t >>= fun t' =>
61 match coreVarSort v' with
62 | CoreExprVar _ => coreExprToWeakExpr e' >>= fun e' => OK ((v',e')::t')
63 | CoreTypeVar _ => Error "found a type variable in a recursive let"
64 | CoreCoerVar _ => Error "found a coercion variable in a recursive let"
66 end) rb) >>= fun rb' =>
67 coreExprToWeakExpr e >>= fun e' =>
68 OK (WELetRec (unleaves' rb') e')
70 | CoreECase e v tbranches alts =>
72 >>= fun e' => coreTypeOfWeakExpr e' >>= fun te' =>
75 ((fix mkBranches (branches: list (@triple AltCon (list CoreVar) (CoreExpr CoreVar)))
76 : ???(list (AltCon*list CoreVar*WeakExpr)) :=
79 | (mkTriple alt vars e)::rest =>
82 coreExprToWeakExpr e >>= fun e' =>
84 | DEFAULT => OK ((DEFAULT,nil,e')::rest')
85 | LitAlt lit => OK ((LitAlt lit,nil,e')::rest')
86 | DataAlt _ _ _ _ tc' dc => OK (((DataAlt _ dc),vars,e')::rest')
89 >>= fun branches => coreExprToWeakExpr e
91 list2vecOrError lt _ >>= fun lt' =>
92 OK (WELet v scrutinee (WECase (WEVar v) tbranches tc lt' (unleaves branches)))
93 | _ => Error "found a case whose scrutinee's type wasn't a TyConApp"