1 (*********************************************************************************************************************************)
2 (* HaskWeakToCore: convert HaskWeak to HaskCore *)
3 (*********************************************************************************************************************************)
5 Generalizable All Variables.
6 Require Import Preamble.
7 Require Import General.
8 Require Import Coq.Strings.String.
9 Require Import Coq.Lists.List.
10 Require Import HaskGeneral.
11 Require Import HaskLiterals.
12 Require Import HaskCoreVars.
13 Require Import HaskCoreTypes.
14 Require Import HaskCore.
15 Require Import HaskWeakVars.
16 Require Import HaskWeak.
18 Variable mkCoreLet : @CoreBind CoreVar -> @CoreExpr CoreVar -> @CoreExpr CoreVar.
19 Extract Inlined Constant mkCoreLet => "MkCore.mkCoreLet".
21 Variable sortAlts : forall {a}{b}, list (@triple AltCon a b) -> list (@triple AltCon a b).
22 Extract Inlined Constant mkCoreLet => "sortAlts".
23 Implicit Arguments sortAlts [[a][b]].
25 Variable unsafeCoerce : CoreCoercion.
26 Extract Inlined Constant unsafeCoerce => "Coercion.unsafeCoerce".
28 (* Coercion and Type are actually the same thing in GHC, but we don't tell Coq about that. This lets us get around it. *)
29 Variable coreCoercionsAreReallyTypes : CoreCoercion -> CoreType.
30 Extract Inlined Constant coreCoercionsAreReallyTypes => "(\x -> x)".
32 (* a dummy variable which is never referenced but needed for a binder *)
33 Variable dummyVariable : CoreVar.
35 Definition weakVarToCoreVar (wv:WeakVar) : CoreVar :=
37 | WExprVar (weakExprVar v _ ) => v
38 | WTypeVar (weakTypeVar v _ ) => v
39 | WCoerVar (weakCoerVar v _ _ ) => v
42 Section HaskWeakToCore.
44 (* the CoreVar for the "magic" bracket/escape identifiers must be created from within one of the monads *)
45 Context (hetmet_brak_var : CoreVar).
46 Context (hetmet_esc_var : CoreVar).
48 Definition weakCoercionToCoreCoercion : WeakCoercion -> CoreCoercion :=
49 fun _ => unsafeCoerce.
51 Fixpoint weakExprToCoreExpr (me:WeakExpr) : @CoreExpr CoreVar :=
53 | WEVar (weakExprVar v _) => CoreEVar v
54 | WELit lit => CoreELit lit
55 | WEApp e1 e2 => CoreEApp (weakExprToCoreExpr e1) (weakExprToCoreExpr e2)
56 | WETyApp e t => CoreEApp (weakExprToCoreExpr e ) (CoreEType t)
57 | WECoApp e co => CoreEApp (weakExprToCoreExpr e )
58 (CoreEType (coreCoercionsAreReallyTypes (weakCoercionToCoreCoercion co)))
59 | WENote n e => CoreENote n (weakExprToCoreExpr e )
60 | WELam (weakExprVar ev _ ) e => CoreELam ev (weakExprToCoreExpr e )
61 | WETyLam (weakTypeVar tv _ ) e => CoreELam tv (weakExprToCoreExpr e )
62 | WECoLam (weakCoerVar cv _ _) e => CoreELam cv (weakExprToCoreExpr e )
63 | WECast e co => CoreECast (weakExprToCoreExpr e ) (weakCoercionToCoreCoercion co)
64 | WEBrak (weakTypeVar ec _) e t => CoreEApp (CoreEApp (CoreEVar hetmet_brak_var) (CoreEType (TyVarTy ec))) (CoreEType t)
65 | WEEsc (weakTypeVar ec _) e t => CoreEApp (CoreEApp (CoreEVar hetmet_esc_var) (CoreEType (TyVarTy ec))) (CoreEType t)
66 | WELet (weakExprVar v _) ve e => mkCoreLet (CoreNonRec v (weakExprToCoreExpr ve)) (weakExprToCoreExpr e)
67 | WECase e tbranches n tc types alts => CoreECase (weakExprToCoreExpr e) dummyVariable tbranches
69 fix mkCaseBranches (alts:Tree ??(AltCon*list WeakVar*WeakExpr)) :=
72 | T_Branch b1 b2 => app (mkCaseBranches b1) (mkCaseBranches b2)
73 | T_Leaf (Some (ac,lwv,e)) =>
74 (mkTriple ac (map weakVarToCoreVar lwv) (weakExprToCoreExpr e))::nil
77 | WELetRec mlr e => CoreELet (CoreRec
78 ((fix mkLetBindings (mlr:Tree ??(WeakExprVar * WeakExpr)) :=
81 | T_Leaf (Some (weakExprVar cv _,e)) => (cv,(weakExprToCoreExpr e))::nil
82 | T_Branch b1 b2 => app (mkLetBindings b1) (mkLetBindings b2)
84 (weakExprToCoreExpr e)