update for new GHC coercion representation

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

diff --git a/src/HaskCoreTypes.v b/src/HaskCoreTypes.v
index ea4a02a..79ab342 100644 (file)
--- a/src/HaskCoreTypes.v
+++ b/src/HaskCoreTypes.v
@@ -9,19 +9,15 @@ Require Import Coq.Strings.String.
 Require Import Coq.Lists.List.
 Require Import HaskKinds.
 Require Import HaskCoreVars.
 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.
+Variable CoreCoercionCoAxiom : Type.  Extract Inlined Constant CoreCoercionCoAxiom => "Coercion.CoAxiom".
+Variable Int : Type.                  Extract Inlined Constant Int => "Prelude.Int".

 
 

-   Extract Constant CoreIPName "’a"        => "BasicTypes.IPName".
-   Extraction Inline CoreIPName.
+Variable classTyCon          : Class_ -> CoreTyCon.       Extract Inlined Constant classTyCon            => "Class.classTyCon".
+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 :=
 
 (* this exracts onto TypeRep.Type, on the nose *)
 Inductive CoreType :=

@@ -40,34 +36,55 @@ Extract Inductive CoreType =>
 Extract Inductive PredType =>
    "TypeRep.PredType" [ "TypeRep.ClassP" "TypeRep.IParam" "TypeRep.EqPred" ].
 
 Extract Inductive PredType =>
    "TypeRep.PredType" [ "TypeRep.ClassP" "TypeRep.IParam" "TypeRep.EqPred" ].
 

-Variable coreTypeToString      : CoreType     -> string.    Extract Inlined Constant coreTypeToString       => "showType".
+Inductive CoreCoercion : Type :=
+    CoreCoercionRefl        : CoreType                                 -> CoreCoercion
+  | CoreCoercionTyConAppCo  : CoreTyCon    -> list CoreCoercion        -> CoreCoercion
+  | CoreCoercionAppCo       : CoreCoercion -> CoreCoercion             -> CoreCoercion
+  | CoreCoercionForAllCo    : CoreVar      -> CoreCoercion             -> CoreCoercion
+  | CoreCoercionCoVarCo     : CoreVar                                  -> CoreCoercion
+  | CoreCoercionAxiomInstCo : CoreCoercionCoAxiom -> list CoreCoercion -> CoreCoercion
+  | CoreCoercionUnsafeCo    : CoreType -> CoreType                     -> CoreCoercion
+  | CoreCoercionSymCo       : CoreCoercion                             -> CoreCoercion
+  | CoreCoercionTransCo     : CoreCoercion -> CoreCoercion             -> CoreCoercion
+  | CoreCoercionNthCo       : Int -> CoreCoercion                      -> CoreCoercion
+  | CoreCoercionInstCo      : CoreCoercion -> CoreType                 -> CoreCoercion.
+
+Extract Inductive CoreCoercion =>
+  "Coercion.Coercion" [
+  "Coercion.Refl"
+  "Coercion.TyConAppCo"
+  "Coercion.AppCo"
+  "Coercion.ForAllCo"
+  "Coercion.CoVarCo"
+  "Coercion.AxiomInstCo"
+  "Coercion.UnsafeCo"
+  "Coercion.SymCo"
+  "Coercion.TransCo"
+  "Coercion.NthCo"
+  "Coercion.InstCo" ].
+

 Variable coreNameToString      : CoreName     -> string.    Extract Inlined Constant coreNameToString       => "outputableToString".
 Variable coreCoercionToString  : CoreCoercion -> string.    Extract Inlined Constant coreCoercionToString   => "outputableToString".
 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 kindOfCoreType    : CoreType -> Kind.    Extract Inlined Constant kindOfCoreType => "(coreKindToKind . Coercion.typeKind)".
-
-(* 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 coreCoercionKind : Kind -> CoreType*CoreType.
+  Extract Inlined Constant coreCoercionKind => "(Coercion.coercionKind . kindToCoreKind)".
+Variable kindOfCoreType   : CoreType -> Kind.   Extract Inlined Constant kindOfCoreType   => "(coreKindToKind . Kind.typeKind)".
+Variable coreTypeToString : CoreType -> string. Extract Inlined Constant coreTypeToString => "(outputableToString . coreViewDeep)".
+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 *)
 
 (* 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          => "(==)".
-Variable tyCon_eq            : EqDecider TyCon.           Extract Inlined Constant tyCon_eq              => "(==)".
-Variable tyFun_eq            : EqDecider TyFun.           Extract Inlined Constant tyFun_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 CoreTyConEqDecidable: EqDecidable CoreTyCon   := { eqd_dec := coreTyCon_eq }.
-Instance TyConEqDecidable    : EqDecidable TyCon       := { eqd_dec := tyCon_eq }.
-Instance TyFunEqDecidable    : EqDecidable TyFun       := { eqd_dec := tyFun_eq }.
-Instance DataConEqDecidable  : EqDecidable CoreDataCon := { eqd_dec := dataCon_eq }.
-Instance CoreNameEqDecidable : EqDecidable CoreName    := { eqd_dec := coreName_eq }.
-
-
+Variable coreTyCon_eq         : EqDecider CoreTyCon.       Extract Inlined Constant coreTyCon_eq          => "(==)".
+Variable tyCon_eq             : EqDecider TyCon.           Extract Inlined Constant tyCon_eq              => "(==)".
+Variable tyFun_eq             : EqDecider TyFun.           Extract Inlined Constant tyFun_eq              => "(==)".
+Variable dataCon_eq           : EqDecider CoreDataCon.     Extract Inlined Constant dataCon_eq            => "(==)".
+Variable coreName_eq          : EqDecider CoreName.        Extract Inlined Constant coreName_eq           => "(==)".
+Instance CoreTyConEqDecidable : EqDecidable CoreTyCon   := { eqd_dec := coreTyCon_eq }.
+Instance TyConEqDecidable     : EqDecidable TyCon       := { eqd_dec := tyCon_eq }.
+Instance TyFunEqDecidable     : EqDecidable TyFun       := { eqd_dec := tyFun_eq }.
+Instance DataConEqDecidable   : EqDecidable CoreDataCon := { eqd_dec := dataCon_eq }.
+Instance CoreNameEqDecidable  : EqDecidable CoreName    := { eqd_dec := coreName_eq }.
+Instance CoreTypeToString     : ToString CoreType       := { toString := coreTypeToString }.
+Instance CoreNameToString     : ToString CoreName       := { toString := coreNameToString }.
+Instance CoreCoercionToString : ToString CoreCoercion   := { toString := coreCoercionToString }.
+Instance CoreDataConToString  : ToString CoreDataCon    := { toString := coreDataConToString }.
+Instance CoreTyConToString    : ToString CoreTyCon      := { toString := coreTyConToString }.

 
 

-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 }.