reshuffle definitions in an attempt to iron out inter-file dependenceies

[coq-hetmet.git] / src / HaskCore.v

diff --git a/src/HaskCore.v b/src/HaskCore.v
index abd1428..9024828 100644 (file)
--- a/src/HaskCore.v
+++ b/src/HaskCore.v
@@ -7,7 +7,7 @@ Require Import Preamble.
 Require Import General.
 Require Import Coq.Strings.String.
 Require Import HaskKinds.
-Require Import HaskCoreLiterals.
+Require Import HaskLiteralsAndTyCons.
 Require Import HaskCoreTypes.
 Require Import HaskCoreVars.
 
@@ -18,7 +18,7 @@ Inductive CoreExpr {b:Type} :=
 | 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
@@ -40,4 +40,7 @@ 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".