X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=src%2FHaskTyCons.v;fp=src%2FHaskTyCons.v;h=617cd59e832e0046d881f83427657485ef1cdacc;hb=1c1cdb9014f409248ca96b677503719916b2b477;hp=0000000000000000000000000000000000000000;hpb=35d3a59796735e5341389fa6a145f62dcea9c3fc;p=coq-hetmet.git

diff --git a/src/HaskTyCons.v b/src/HaskTyCons.v
new file mode 100644
index 0000000..617cd59
--- /dev/null
+++ b/src/HaskTyCons.v
@@ -0,0 +1,32 @@
+(*********************************************************************************************************************************)
+(* HaskTyCons: representation of type constructors, type functions, and data constructors                                        *)
+(*********************************************************************************************************************************)
+
+Generalizable All Variables.
+Require Import Preamble.
+Require Import General.
+Require Import Coq.Strings.String.
+Require Import HaskKinds.
+
+Variable CoreDataCon     : Type.                      Extract Inlined Constant CoreDataCon          => "DataCon.DataCon".
+
+(* 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 CoreName        : Type.                      Extract Inlined Constant CoreName              => "Name.Name".
+Variable Class_          : Type.                      Extract Inlined Constant Class_                => "Class.Class".
+Variable CoreIPName      : Type -> Type.              Extract         Constant CoreIPName "’a"       => "BasicTypes.IPName".
+                                                      Extraction Inline CoreIPName.
+
+Variable tyConToString   : TyCon   -> string.     Extract Inlined Constant tyConToString         => "outputableToString".
+Variable tyFunToString   : TyFun   -> string.     Extract Inlined Constant tyFunToString         => "outputableToString".
+Instance TyConToString   : ToString TyCon := { toString := tyConToString }.
+Instance TyFunToString   : ToString TyFun := { toString := tyFunToString }.
+Instance TyConToLatex    : ToLatex  TyCon := { toLatex  := fun x => toLatex (toString x) }.
+Instance TyFunToLatex    : ToLatex  TyCon := { toLatex  := fun x => toLatex (toString x) }.
+
+Variable ModalBoxTyCon   : TyCon.        Extract Inlined Constant ModalBoxTyCon => "TysWiredIn.hetMetCodeTypeTyCon".
+Variable PairTyCon       : TyFun.        Extract Inlined Constant PairTyCon     => "TysWiredIn.pairTyCon".
+Variable UnitTyCon       : TyFun.        Extract Inlined Constant UnitTyCon     => "TysWiredIn.unitTyCon".
+Variable ArrowTyCon      : TyCon.        Extract Constant ArrowTyCon    => "Type.funTyCon".