1 (*********************************************************************************************************************************)
2 (* HaskCore: basically GHC's CoreSyn.Expr imported into Coqland *)
3 (*********************************************************************************************************************************)
5 Generalizable All Variables.
6 Require Import Preamble.
7 Require Import General.
8 Require Import Coq.Strings.String.
9 Require Import HaskGeneral.
10 Require Import HaskLiterals.
11 Require Import HaskCoreTypes.
12 Require Import HaskCoreVars.
14 (* this type must extract to EXACTLY match TypeRep.Type *)
15 Inductive CoreExpr (b:Type) :=
16 | CoreEVar : CoreVar -> CoreExpr b
17 | CoreELit : HaskLiteral -> CoreExpr b
18 | CoreEApp : CoreExpr b -> CoreExpr b -> CoreExpr b
19 | CoreELam : b -> CoreExpr b -> CoreExpr b
20 | CoreELet : CoreBind b -> CoreExpr b -> CoreExpr b
21 | CoreECase : CoreExpr b -> b -> CoreType -> list (@triple AltCon (list b) (CoreExpr b)) -> CoreExpr b
22 | CoreECast : CoreExpr b -> CoreCoercion -> CoreExpr b
23 | CoreENote : Note -> CoreExpr b -> CoreExpr b
24 | CoreEType : CoreType -> CoreExpr b
25 with CoreBind (b:Type) :=
26 | CoreNonRec : b -> CoreExpr b -> CoreBind b
27 | CoreRec : list (b * CoreExpr b) -> CoreBind b.
28 Extract Inductive CoreExpr =>
39 Extract Inductive CoreBind =>
40 "CoreSyn.Bind" [ "CoreSyn.NonRec" "CoreSyn.Rec" ].
42 (* extracts the Name from a CoreVar *)
43 Variable coreVarCoreName : CoreVar -> CoreName. Extract Inlined Constant coreVarCoreName => "Var.varName".
45 Variable coretype_eq_dec : forall (c1 c2:CoreType), sumbool (eq c1 c2) (not (eq c1 c2)).
46 Extract Inlined Constant coretype_eq_dec => "Type.coreEqType".
48 Extract Constant ArrowTyCon => "Type.funTyCon". (* Figure 7, (->) *)
49 Extract Constant CoFunConst => "TyCon.TyCon". Extraction Implicit CoFunConst [ 1 ].
50 Extract Constant TyFunConst => "TyCon.TyCon". Extraction Implicit TyFunConst [ 1 ].
52 (*Extract Inlined Constant getDataCons => "TyCon.tyConDataCons".*)
53 Variable mkTyConApp : forall n, TyCon n -> list CoreType -> CoreType.
54 Extract Inlined Constant mkTyConApp => "Type.mkTyConApp".
56 (* the magic wired-in name for the modal type introduction form *)
57 Variable hetmet_brak_name : CoreName. Extract Inlined Constant hetmet_brak_name => "PrelNames.hetmet_brak_name".
59 (* the magic wired-in name for the modal type elimination form *)
60 Variable hetmet_esc_name : CoreName. Extract Inlined Constant hetmet_esc_name => "PrelNames.hetmet_esc_name".
62 (* detects our crude Core-encoding of modal type introduction/elimination forms *)
63 Definition isBrak (ce:CoreExpr CoreVar) : ??CoreVar :=
65 | (CoreEApp (CoreEApp (CoreEVar v) (CoreEType (TyVarTy ec))) (CoreEType tbody))
66 => if coreName_eq hetmet_brak_name (coreVarCoreName v) then Some ec else None
69 Definition isEsc (ce:CoreExpr CoreVar) : ??CoreVar :=
71 | (CoreEApp (CoreEApp (CoreEVar v) (CoreEType (TyVarTy ec))) (CoreEType tbody))
72 => if coreName_eq hetmet_esc_name (coreVarCoreName v) then Some ec else None