X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskCore.v;h=13a263ed89ef83f0fd4d75aac97b4229de569377;hp=3d5f860c073a34019f467f3d8b55bda6ac60b4ea;hb=5cb97fa6ed28f55ca888bdadc4f145396cc02236;hpb=bcb16a7fa1ff772f12807c4587609fd756b7762e

diff --git a/src/HaskCore.v b/src/HaskCore.v
index 3d5f860..13a263e 100644
--- a/src/HaskCore.v
+++ b/src/HaskCore.v
@@ -7,7 +7,8 @@ Require Import Preamble.
 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.
 
@@ -18,10 +19,11 @@ 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
+| CoreECoercion : CoreCoercion                  -> CoreExpr
 with      CoreBind {b:Type} :=
 | CoreNonRec : b -> CoreExpr         -> CoreBind  
 | CoreRec    : list (b * CoreExpr  ) -> CoreBind.
@@ -35,17 +37,14 @@ Extract Inductive CoreExpr =>
       "CoreSyn.Case"
       "CoreSyn.Cast"
       "CoreSyn.Note"
-      "CoreSyn.Type" ].
+      "CoreSyn.Type"
+      "CoreSyn.Coercion"
+   ].
 Extract Inductive CoreBind =>
   "CoreSyn.Bind" [ "CoreSyn.NonRec" "CoreSyn.Rec" ].
 
-(* extracts the Name from a CoreVar *)
-Variable coreVarCoreName    : CoreVar -> CoreName.   Extract Inlined Constant coreVarCoreName  => "Var.varName".
-
-(* the magic wired-in name for the modal type introduction form *)
-Variable hetmet_brak_name   : CoreName.              Extract Inlined Constant hetmet_brak_name => "PrelNames.hetmet_brak_name".
-
-(* the magic wired-in name for the modal type elimination form *)
-Variable hetmet_esc_name    : CoreName.              Extract Inlined Constant hetmet_esc_name  => "PrelNames.hetmet_esc_name".
-
+Variable coreExprToString : @CoreExpr CoreVar -> string.  Extract Inlined Constant coreExprToString => "outputableToString".
+Instance CoreExprToString : ToString (@CoreExpr CoreVar) := { toString := coreExprToString }.
 
+Variable coreTypeOfCoreExpr    : @CoreExpr CoreVar -> CoreType.
+  Extract Inlined Constant coreTypeOfCoreExpr => "CoreUtils.exprType".