Require Import General.
Require Import Coq.Strings.String.
Require Import HaskKinds.
-Require Import HaskCoreLiterals.
+Require Import HaskLiterals.
+Require Import HaskTyCons.
Require Import HaskCoreTypes.
Require Import HaskCoreVars.
| CoreEApp : CoreExpr -> CoreExpr -> CoreExpr
| CoreELam : b -> CoreExpr -> CoreExpr
| CoreELet : CoreBind -> CoreExpr -> CoreExpr
-| CoreECase : CoreExpr -> b -> CoreType -> list (@triple AltCon (list b) CoreExpr) -> CoreExpr
+| CoreECase : CoreExpr -> b -> CoreType -> list (@triple CoreAltCon (list b) CoreExpr) -> CoreExpr
| CoreECast : CoreExpr -> CoreCoercion -> CoreExpr
| CoreENote : Note -> CoreExpr -> CoreExpr
| CoreEType : CoreType -> CoreExpr
+| CoreECoercion : CoreCoercion -> CoreExpr
with CoreBind {b:Type} :=
| CoreNonRec : b -> CoreExpr -> CoreBind
| CoreRec : list (b * CoreExpr ) -> CoreBind.
"CoreSyn.Case"
"CoreSyn.Cast"
"CoreSyn.Note"
- "CoreSyn.Type" ].
+ "CoreSyn.Type"
+ "CoreSyn.Coercion"
+ ].
Extract Inductive CoreBind =>
"CoreSyn.Bind" [ "CoreSyn.NonRec" "CoreSyn.Rec" ].
Variable coreExprToString : @CoreExpr CoreVar -> string. Extract Inlined Constant coreExprToString => "outputableToString".
-Instance CoreExprToString : ToString (@CoreExpr CoreVar) := { toString := coreExprToString }.
\ No newline at end of file
+Instance CoreExprToString : ToString (@CoreExpr CoreVar) := { toString := coreExprToString }.
+
+Variable coreTypeOfCoreExpr : @CoreExpr CoreVar -> CoreType.
+ Extract Inlined Constant coreTypeOfCoreExpr => "CoreUtils.exprType".