X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskLiteralsAndTyCons.v;h=38e7f95c84297c52a84e343f316682a849b459b4;hp=0592f3abbdc1beb8dd823f467c56ace10dbcde4a;hb=75a0b52b9937ab6b68ed98cc24281bc9153e96b9;hpb=94d7c55025f5df750ce213172c5d2441b5a210e1

diff --git a/src/HaskLiteralsAndTyCons.v b/src/HaskLiteralsAndTyCons.v
index 0592f3a..38e7f95 100644
--- a/src/HaskLiteralsAndTyCons.v
+++ b/src/HaskLiteralsAndTyCons.v
@@ -15,16 +15,16 @@ Variable TyCon           : Type.                      Extract Inlined Constant T
 Variable TyFun           : Type.                      Extract Inlined Constant TyFun                => "TyCon.TyCon".
 
 (* Since GHC is written in Haskell, compile-time Haskell constants are represented using Haskell (Prelude) types *)
-Variable HaskInt                 : Type.      Extract Inlined Constant HaskInt             => "Prelude.Int".
-Variable HaskChar                : Type.      Extract Inlined Constant HaskChar            => "Prelude.Char".
-Variable HaskFastString          : Type.      Extract Inlined Constant HaskFastString      => "FastString.FastString".
-Variable HaskInteger             : Type.      Extract Inlined Constant HaskInteger         => "Prelude.Integer".
-Variable HaskRational            : Type.      Extract Inlined Constant HaskRational        => "Prelude.Rational".
+Variable HaskInt         : Type.                      Extract Inlined Constant HaskInt               => "Prelude.Int".
+Variable HaskChar        : Type.                      Extract Inlined Constant HaskChar              => "Prelude.Char".
+Variable HaskFastString  : Type.                      Extract Inlined Constant HaskFastString        => "FastString.FastString".
+Variable HaskInteger     : Type.                      Extract Inlined Constant HaskInteger           => "Prelude.Integer".
+Variable HaskRational    : Type.                      Extract Inlined Constant HaskRational          => "Prelude.Rational".
 
-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 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.
 
 (* This type extracts exactly onto GHC's Literal.Literal type *)
 Inductive HaskLiteral :=
@@ -86,6 +86,10 @@ Variable tyConToString   : TyCon   -> string.     Extract Inlined Constant tyCon
 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".