X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=src%2FHaskCoreLiterals.v;fp=src%2FHaskCoreLiterals.v;h=24432ee22c327acdc7d83e13001420e736f45f43;hb=8c26722a1ee110077968a8a166eb7130266b2035;hp=d332ccf619004687e8ebc1b9d30beed207d3375f;hpb=b8f6adf700fa3c67feefaea3d2cf5c4626300489;p=coq-hetmet.git

diff --git a/src/HaskCoreLiterals.v b/src/HaskCoreLiterals.v
index d332ccf..24432ee 100644
--- a/src/HaskCoreLiterals.v
+++ b/src/HaskCoreLiterals.v
@@ -45,6 +45,7 @@ Extract Inductive HaskFunctionOrData =>
   "BasicTypes.FunctionOrData" [ "BasicTypes.IsFunction" "BasicTypes.IsData" ].
 
 Variable haskLiteralToString  : HaskLiteral -> string.    Extract Inlined Constant haskLiteralToString     => "outputableToString".
+Instance HaskLiteralToString : ToString HaskLiteral := { toString := haskLiteralToString }.
 
 (* because Haskell's 3-tuples (triples) are distinct from both ((x,y),z) and (x,(y,z)), we need a new type: *)
 Inductive triple {A B C:Type} :=
@@ -52,6 +53,13 @@ Inductive triple {A B C:Type} :=
 Notation "a ** b ** c" := (mkTriple a b c) (at level 20).
 Extract Inductive triple => "(,,)" [ "(,,)" ].
 
+Inductive AltCon :=
+| DataAlt : CoreDataCon -> AltCon
+| LitAlt  : HaskLiteral -> AltCon
+| DEFAULT :                AltCon.
+Extract Inductive AltCon =>
+  "CoreSyn.AltCon" [ "CoreSyn.DataAlt" "CoreSyn.LitAlt" "CoreSyn.DEFAULT" ].
+
 (* the TyCons for each of the literals above *)
 Variable addrPrimTyCon       : TyCon.   Extract Inlined Constant addrPrimTyCon   => "TysPrim.addrPrimTyCon".
 Variable intPrimTyCon        : TyCon.   Extract Inlined Constant intPrimTyCon    => "TysPrim.intPrimTyCon".
@@ -76,10 +84,3 @@ match lit with
   | HaskMachDouble _    => doublePrimTyCon
   | HaskMachLabel _ _ _ => addrPrimTyCon
 end.
-
-Inductive AltCon :=
-| DataAlt : CoreDataCon -> AltCon
-| LitAlt  : HaskLiteral -> AltCon
-| DEFAULT :                AltCon.
-Extract Inductive AltCon =>
-  "CoreSyn.AltCon" [ "CoreSyn.DataAlt" "CoreSyn.LitAlt" "CoreSyn.DEFAULT" ].