ToString instance for HaskCore

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

diff --git a/src/HaskCore.v b/src/HaskCore.v
index 64699fd..244139a 100644 (file)
--- a/src/HaskCore.v
+++ b/src/HaskCore.v
@@ -6,8 +6,8 @@ Generalizable All Variables.
 Require Import Preamble.
 Require Import General.
 Require Import Coq.Strings.String.
-Require Import HaskGeneral.
-Require Import HaskLiterals.
+Require Import HaskKinds.
+Require Import HaskCoreLiterals.
 Require Import HaskCoreTypes.
 Require Import HaskCoreVars.
 
@@ -42,18 +42,13 @@ Extract Inductive CoreBind =>
 (* extracts the Name from a CoreVar *)
 Variable coreVarCoreName    : CoreVar -> CoreName.   Extract Inlined Constant coreVarCoreName  => "Var.varName".
 
-Extract Constant ArrowTyCon           => "Type.funTyCon".     (* Figure 7, (->) *)
-Extract Constant CoFunConst           => "TyCon.TyCon".                        Extraction Implicit CoFunConst [ 1 ].
-Extract Constant TyFunConst           => "TyCon.TyCon".                        Extraction Implicit TyFunConst [ 1 ].
-
-(*Extract Inlined Constant getDataCons => "TyCon.tyConDataCons".*)
-Variable mkTyConApp : forall n, TyCon n -> list CoreType -> CoreType.
-  Extract Inlined Constant mkTyConApp => "Type.mkTyConApp".
-
 (* 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 }.
\ No newline at end of file