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 HaskKinds.
10 Require Import HaskCoreLiterals.
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
17 | CoreELit : HaskLiteral -> CoreExpr
18 | CoreEApp : CoreExpr -> CoreExpr -> CoreExpr
19 | CoreELam : b -> CoreExpr -> CoreExpr
20 | CoreELet : CoreBind -> CoreExpr -> CoreExpr
21 | CoreECase : CoreExpr -> b -> CoreType -> list (@triple AltCon (list b) CoreExpr) -> CoreExpr
22 | CoreECast : CoreExpr -> CoreCoercion -> CoreExpr
23 | CoreENote : Note -> CoreExpr -> CoreExpr
24 | CoreEType : CoreType -> CoreExpr
25 with CoreBind {b:Type} :=
26 | CoreNonRec : b -> CoreExpr -> CoreBind
27 | CoreRec : list (b * CoreExpr ) -> CoreBind.
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 (* the magic wired-in name for the modal type introduction form *)
46 Variable hetmet_brak_name : CoreName. Extract Inlined Constant hetmet_brak_name => "PrelNames.hetmet_brak_name".
48 (* the magic wired-in name for the modal type elimination form *)
49 Variable hetmet_esc_name : CoreName. Extract Inlined Constant hetmet_esc_name => "PrelNames.hetmet_esc_name".
51 Variable coreExprToString : @CoreExpr CoreVar -> string. Extract Inlined Constant coreExprToString => "outputableToString".
53 Instance CoreExprToString : ToString (@CoreExpr CoreVar) :=
54 { toString := coreExprToString }.