X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskCoreTypes.v;h=4babf3654e91181bdec260e265d0bf8210e54b31;hp=33ed7a7782de7cb89279d5d6ff3867e4c14f4aa9;hb=68f41d71d573b422b04ed3f4a3eb3ab41de09a79;hpb=e4a70787c40d9fa1c009e966d09a85ee2120092a

diff --git a/src/HaskCoreTypes.v b/src/HaskCoreTypes.v
index 33ed7a7..4babf36 100644
--- a/src/HaskCoreTypes.v
+++ b/src/HaskCoreTypes.v
@@ -9,17 +9,13 @@ Require Import Coq.Strings.String.
 Require Import Coq.Lists.List.
 Require Import HaskKinds.
 Require Import HaskCoreVars.
+Require Import HaskLiterals.
+Require Import HaskTyCons.
 
-Variable CoreTyCon           : Type.                      Extract Inlined Constant CoreTyCon             => "TyCon.TyCon".
-Variable CoreDataCon         : Type.                      Extract Inlined Constant CoreDataCon           => "DataCon.DataCon".
-Variable CoreName            : Type.                      Extract Inlined Constant CoreName              => "Name.Name".
 Variable CoreCoercion        : Type.                      Extract Inlined Constant CoreCoercion          => "Coercion.Coercion".
-Variable Class_              : Type.                      Extract Inlined Constant Class_                => "Class.Class".
 Variable classTyCon          : Class_ -> CoreTyCon.       Extract Inlined Constant classTyCon            => "Class.classTyCon".
-Variable tyConToString       : CoreTyCon      -> string.  Extract Inlined Constant tyConToString         => "outputableToString".
-Variable dataConToString     : CoreDataCon-> string.      Extract Inlined Constant dataConToString       => "outputableToString".
-Variable CoreIPName          : Type -> Type.              Extract         Constant CoreIPName "’a"       => "BasicTypes.IPName".
-                                                          Extraction Inline CoreIPName.
+Variable coreTyConToString   : CoreTyCon   -> string.     Extract Inlined Constant coreTyConToString     => "outputableToString".
+Variable coreDataConToString : CoreDataCon -> string.     Extract Inlined Constant coreDataConToString   => "outputableToString".
 
 (* this exracts onto TypeRep.Type, on the nose *)
 Inductive CoreType :=
@@ -40,13 +36,11 @@ Extract Inductive PredType =>
 
 Variable coreNameToString      : CoreName     -> string.    Extract Inlined Constant coreNameToString       => "outputableToString".
 Variable coreCoercionToString  : CoreCoercion -> string.    Extract Inlined Constant coreCoercionToString   => "outputableToString".
-Variable coreCoercionKind : CoreCoercion -> CoreType*CoreType. Extract Inlined Constant coreCoercionKind => "Coercion.coercionKind".
+Variable coreCoercionKind : Kind -> CoreType*CoreType.
+  Extract Inlined Constant coreCoercionKind => "(Coercion.coercionKind . kindToCoreKind)".
 Variable kindOfCoreType   : CoreType -> Kind.   Extract Inlined Constant kindOfCoreType   => "(coreKindToKind . Coercion.typeKind)".
 Variable coreTypeToString : CoreType -> string. Extract Inlined Constant coreTypeToString => "(outputableToString . coreViewDeep)".
-
-(* once again, we pull the trick of having multiple Coq types map to a single Haskell type to provide stronger typing *)
-Variable TyCon           : Type.                         Extract Inlined Constant TyCon             => "TyCon.TyCon".
-Variable TyFun           : Type.                         Extract Inlined Constant TyFun             => "TyCon.TyCon".
+Variable setVarType       : CoreVar -> CoreType -> CoreVar. Extract Inlined Constant setVarType       => "Var.setVarType".
 
 (* GHC provides decision procedures for equality on its primitive types; we tell Coq to blindly trust them *)
 Variable coreTyCon_eq         : EqDecider CoreTyCon.       Extract Inlined Constant coreTyCon_eq          => "(==)".
@@ -62,5 +56,6 @@ Instance CoreNameEqDecidable  : EqDecidable CoreName    := { eqd_dec := coreName
 Instance CoreTypeToString     : ToString CoreType       := { toString := coreTypeToString }.
 Instance CoreNameToString     : ToString CoreName       := { toString := coreNameToString }.
 Instance CoreCoercionToString : ToString CoreCoercion   := { toString := coreCoercionToString }.
-Instance CoreDataConToString  : ToString CoreDataCon    := { toString := dataConToString }.
-Instance CoreTyConToString    : ToString CoreTyCon      := { toString := tyConToString }.
+Instance CoreDataConToString  : ToString CoreDataCon    := { toString := coreDataConToString }.
+Instance CoreTyConToString    : ToString CoreTyCon      := { toString := coreTyConToString }.
+