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 HaskKinds.
11 Require Import HaskCoreLiterals.
12 Require Import HaskCoreVars.
13 Require Import HaskCoreTypes.
14 Require Import HaskCore.
15 Require Import HaskWeakVars.
16 Require Import HaskWeakTypes.
17 Require Import HaskWeak.
18 Require Import HaskCoreToWeak.
20 Variable mkCoreLet : @CoreBind CoreVar -> @CoreExpr CoreVar -> @CoreExpr CoreVar.
21 Extract Inlined Constant mkCoreLet => "MkCore.mkCoreLet".
23 Variable sortAlts : forall {a}{b}, list (@triple AltCon a b) -> list (@triple AltCon a b).
24 Extract Inlined Constant sortAlts => "sortAlts".
25 Implicit Arguments sortAlts [[a][b]].
27 Variable mkUnsafeCoercion : CoreType -> CoreType -> CoreCoercion.
28 Extract Inlined Constant mkUnsafeCoercion => "Coercion.mkUnsafeCoercion".
30 (* Coercion and Type are actually the same thing in GHC, but we don't tell Coq about that. This lets us get around it. *)
31 Variable coreCoercionsAreReallyTypes : CoreCoercion -> CoreType.
32 Extract Inlined Constant coreCoercionsAreReallyTypes => "(\x -> x)".
34 Definition weakCoercionToCoreCoercion (wc:WeakCoercion) : CoreCoercion :=
35 mkUnsafeCoercion (weakTypeToCoreType (fst (weakCoercionTypes wc))) (weakTypeToCoreType (snd (weakCoercionTypes wc))).
37 Fixpoint weakExprToCoreExpr (me:WeakExpr) : @CoreExpr CoreVar :=
39 | WEVar (weakExprVar v _) => CoreEVar v
40 | WELit lit => CoreELit lit
41 | WEApp e1 e2 => CoreEApp (weakExprToCoreExpr e1) (weakExprToCoreExpr e2)
42 | WETyApp e t => CoreEApp (weakExprToCoreExpr e ) (CoreEType (weakTypeToCoreType t))
43 | WECoApp e co => CoreEApp (weakExprToCoreExpr e )
44 (CoreEType (coreCoercionsAreReallyTypes (weakCoercionToCoreCoercion co)))
45 | WENote n e => CoreENote n (weakExprToCoreExpr e )
46 | WELam (weakExprVar ev _ ) e => CoreELam ev (weakExprToCoreExpr e )
47 | WETyLam (weakTypeVar tv _ ) e => CoreELam tv (weakExprToCoreExpr e )
48 | WECoLam (weakCoerVar cv _ _ _) e => CoreELam cv (weakExprToCoreExpr e )
49 | WECast e co => CoreECast (weakExprToCoreExpr e ) (weakCoercionToCoreCoercion co)
50 | WEBrak v (weakTypeVar ec _) e t => fold_left CoreEApp
51 ((CoreEType (TyVarTy ec))::
52 (CoreEType (weakTypeToCoreType t))::
53 (weakExprToCoreExpr e)::
56 | WEEsc v (weakTypeVar ec _) e t => fold_left CoreEApp
57 ((CoreEType (TyVarTy ec))::
58 (CoreEType (weakTypeToCoreType t))::
59 (weakExprToCoreExpr e)::
62 | WELet (weakExprVar v _) ve e => mkCoreLet (CoreNonRec v (weakExprToCoreExpr ve)) (weakExprToCoreExpr e)
63 | WECase vscrut e tbranches tc types alts =>
64 CoreECase (weakExprToCoreExpr e) vscrut (weakTypeToCoreType tbranches)
66 fix mkCaseBranches (alts:Tree
67 ??(AltCon*list WeakTypeVar*list WeakCoerVar*list WeakExprVar*WeakExpr)) :=
70 | T_Branch b1 b2 => app (mkCaseBranches b1) (mkCaseBranches b2)
71 | T_Leaf (Some (ac,tvars,cvars,evars,e)) =>
74 (map (fun v:WeakTypeVar => weakVarToCoreVar v) tvars)
75 (map (fun v:WeakCoerVar => weakVarToCoreVar v) cvars))
76 (map (fun v:WeakExprVar => weakVarToCoreVar v) evars))
77 (weakExprToCoreExpr e))::nil
80 | WELetRec mlr e => CoreELet (CoreRec
81 ((fix mkLetBindings (mlr:Tree ??(WeakExprVar * WeakExpr)) :=
84 | T_Leaf (Some (weakExprVar cv _,e)) => (cv,(weakExprToCoreExpr e))::nil
85 | T_Branch b1 b2 => app (mkLetBindings b1) (mkLetBindings b2)
87 (weakExprToCoreExpr e)
90 Definition weakTypeOfWeakExpr (we:WeakExpr) : ???WeakType :=
91 coreTypeToWeakType (coreTypeOfCoreExpr (weakExprToCoreExpr we)).
93 Instance weakExprToString : ToString WeakExpr :=
94 { toString := fun we => toString (weakExprToCoreExpr we) }.