X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskCoreTypes.v;fp=src%2FHaskCoreTypes.v;h=4a7a056598bef9986e5aaa29795c69628588d7f2;hp=a5671964fc86f5486b5600682c6af0acb962da19;hb=bcb16a7fa1ff772f12807c4587609fd756b7762e;hpb=8282f5a7639dbe862bba29d3170d58b81bbb1446

diff --git a/src/HaskCoreTypes.v b/src/HaskCoreTypes.v
index a567196..4a7a056 100644
--- a/src/HaskCoreTypes.v
+++ b/src/HaskCoreTypes.v
@@ -6,49 +6,62 @@ Generalizable All Variables.
 Require Import Preamble.
 Require Import General.
 Require Import Coq.Strings.String.
-Require Import HaskGeneral.
-Require Import HaskLiterals.
+Require Import Coq.Lists.List.
+Require Import HaskKinds.
 Require Import HaskCoreVars.
 
-Variable CoreName           : Type.                                               Extract Inlined Constant CoreName => "Name.Name".
-Variable coreName_eq        : forall (a b:CoreName),   sumbool (a=b) (not (a=b)). Extract Inlined Constant coreName_eq => "(==)".
-Axiom    coreName_eq_refl   : ∀ v, (coreName_eq v v)=(left _ (refl_equal v)).
-Instance CoreNameEqDecidable : EqDecidable CoreName :=
-{ eqd_dec            := coreName_eq
-}.
-
-Inductive CoreIPName        : Type -> Type := .                               Extract Inductive CoreIPName => "CoreSyn.IPName" [ ].
+Variable TyCon               : Type.                      Extract Inlined Constant TyCon                 => "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 CoreCoFunConst      : Type.                      Extract Inlined Constant TyCon                 => "TyCon.TyCon".
+Variable CoreTyFunConst      : Type.                      Extract Inlined Constant TyCon                 => "TyCon.TyCon".
+Variable Class_              : Type.                      Extract Inlined Constant Class_                => "Class.Class".
+Variable classTyCon          : Class_ -> TyCon.           Extract Inlined Constant classTyCon            => "Class.classTyCon".
+Variable tyConToString       : TyCon      -> string.      Extract Inlined Constant tyConToString         => "outputableToString".
+Variable dataConToString     : CoreDataCon-> string.      Extract Inlined Constant dataConToString       => "outputableToString".
+Variable tyFunToString       : CoreTyFunConst -> string.  Extract Inlined Constant tyFunToString         => "outputableToString".
+Variable coFunToString       : CoreCoFunConst -> string.  Extract Inlined Constant coFunToString         => "outputableToString".
+Variable natTostring         : nat->string.               Extract Inlined Constant natTostring           => "natTostring".
+Variable CoreIPName          : Type -> Type.
+   Extract Constant CoreIPName "’a"        => "BasicTypes.IPName".
+   Extraction Inline CoreIPName.
 
 (* this exracts onto TypeRep.Type, on the nose *)
 Inductive CoreType :=
-| TyVarTy  :             CoreVar                   -> CoreType
-| AppTy    :             CoreType ->      CoreType -> CoreType   (* first arg must be AppTy or TyVarTy*)
-| TyConApp : forall {n}, TyCon n  -> list CoreType -> CoreType
-| FunTy    :             CoreType ->      CoreType -> CoreType   (* technically redundant since we have FunTyCon *)
-| ForAllTy :             CoreVar  ->      CoreType -> CoreType
-| PredTy   :             PredType                  -> CoreType
+| TyVarTy  : CoreVar                    -> CoreType
+| AppTy    : CoreType  ->      CoreType -> CoreType   (* first arg must be AppTy or TyVarTy*)
+| TyConApp : TyCon -> list CoreType -> CoreType
+| FunTy    : CoreType  ->      CoreType -> CoreType   (* technically redundant since we have FunTyCon *)
+| ForAllTy : CoreVar   ->      CoreType -> CoreType
+| PredTy   : PredType                   -> CoreType
 with PredType :=
-| ClassP   : forall {n}, Class_ n            -> list CoreType -> PredType
-| IParam   :             CoreIPName CoreName -> CoreType      -> PredType
-| EqPred   :             CoreType            -> CoreType      -> PredType.
+| ClassP   : Class_              -> list CoreType -> PredType
+| IParam   : CoreIPName CoreName -> CoreType      -> PredType
+| EqPred   : CoreType            -> CoreType      -> PredType.
 Extract Inductive CoreType =>
    "TypeRep.Type" [ "TypeRep.TyVarTy" "TypeRep.AppTy" "TypeRep.TyConApp" "TypeRep.FunTy" "TypeRep.ForAllTy" "TypeRep.PredTy" ].
 Extract Inductive PredType =>
    "TypeRep.PredType" [ "TypeRep.ClassP" "TypeRep.IParam" "TypeRep.EqPred" ].
 
+(* GHC provides decision procedures for equality on its primitive types; we tell Coq to blindly trust them *)
+Variable tyCon_eq            : EqDecider TyCon.           Extract Inlined Constant tyCon_eq              => "(==)".
+Variable dataCon_eq          : EqDecider CoreDataCon.     Extract Inlined Constant dataCon_eq            => "(==)".
+Variable coreName_eq         : EqDecider CoreName.        Extract Inlined Constant coreName_eq           => "(==)".
+Variable coretype_eq_dec     : EqDecider CoreType.        Extract Inlined Constant coretype_eq_dec       => "checkTypeEquality".
+Instance CoreTypeEqDecidable : EqDecidable CoreType    := { eqd_dec := coretype_eq_dec }.
+Instance TyConEqDecidable    : EqDecidable TyCon       := { eqd_dec := tyCon_eq }.
+Instance DataConEqDecidable  : EqDecidable CoreDataCon := { eqd_dec := dataCon_eq }.
+Instance CoreNameEqDecidable : EqDecidable CoreName    := { eqd_dec := coreName_eq }.
+
+(*
 Variable coreTypeToString      : CoreType     -> string.    Extract Inlined Constant coreTypeToString       => "outputableToString".
-Variable coreNameToString      : CoreName     -> string.    Extract Inlined Constant coreNameToString       => "outputableToString".
+*)
+Variable coreTypeToString      : CoreType     -> string.
+    Extract Inlined Constant coreTypeToString       => "showType".
 
-Variable CoreCoercion          : Type.                      Extract Inlined Constant CoreCoercion           => "Coercion.Coercion".
+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 coretype_eq_dec : forall (c1 c2:CoreType), sumbool (eq c1 c2) (not (eq c1 c2)).
-  Extract Inlined Constant coretype_eq_dec => "Type.coreEqType".
-  Instance CoreTypeEqDecidable : EqDecidable CoreType.
-    apply Build_EqDecidable.
-    apply coretype_eq_dec.
-    Defined.
+Variable coreCoercionKind : CoreCoercion -> CoreType*CoreType. Extract Inlined Constant coreCoercionKind => "Coercion.coercionKind".
+Variable kindOfCoreType    : CoreType -> Kind.    Extract Inlined Constant kindOfCoreType => "(coreKindToKind . Coercion.typeKind)".
 
-Variable kindOfCoreType : CoreType -> Kind.      Extract Inlined Constant kindOfCoreType => "(coreKindToKind . Coercion.typeKind)".