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 HaskLiterals.
11 Require Import HaskTyCons.
12 Require Import HaskCoreTypes.
13 Require Import HaskCoreVars.
15 (* this type must extract to EXACTLY match TypeRep.Type *)
16 Inductive CoreExpr {b:Type} :=
17 | CoreEVar : CoreVar -> CoreExpr
18 | CoreELit : HaskLiteral -> CoreExpr
19 | CoreEApp : CoreExpr -> CoreExpr -> CoreExpr
20 | CoreELam : b -> CoreExpr -> CoreExpr
21 | CoreELet : CoreBind -> CoreExpr -> CoreExpr
22 | CoreECase : CoreExpr -> b -> CoreType -> list (@triple CoreAltCon (list b) CoreExpr) -> CoreExpr
23 | CoreECast : CoreExpr -> CoreCoercion -> CoreExpr
24 | CoreENote : Note -> CoreExpr -> CoreExpr
25 | CoreEType : CoreType -> CoreExpr
26 | CoreECoercion : CoreCoercion -> CoreExpr
27 with CoreBind {b:Type} :=
28 | CoreNonRec : b -> CoreExpr -> CoreBind
29 | CoreRec : list (b * CoreExpr ) -> CoreBind.
30 Extract Inductive CoreExpr =>
43 Extract Inductive CoreBind =>
44 "CoreSyn.Bind" [ "CoreSyn.NonRec" "CoreSyn.Rec" ].
46 Variable coreExprToString : @CoreExpr CoreVar -> string. Extract Inlined Constant coreExprToString => "outputableToString".
47 Instance CoreExprToString : ToString (@CoreExpr CoreVar) := { toString := coreExprToString }.
49 Variable coreTypeOfCoreExpr : @CoreExpr CoreVar -> CoreType.
50 Extract Inlined Constant coreTypeOfCoreExpr => "CoreUtils.exprType".