Require Import Preamble.
Require Import General.
Require Import Coq.Strings.String.
-Require Import HaskGeneral.
+Require Import HaskKinds.
+Require Import HaskTyCons.
(* 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".
(* This type extracts exactly onto GHC's Literal.Literal type *)
Inductive HaskLiteral :=
Extract Inductive HaskFunctionOrData =>
"BasicTypes.FunctionOrData" [ "BasicTypes.IsFunction" "BasicTypes.IsData" ].
+Variable haskLiteralToString : HaskLiteral -> string. Extract Inlined Constant haskLiteralToString => "outputableToString".
+Instance HaskLiteralToString : ToString HaskLiteral := { toString := haskLiteralToString }.
+
(* the TyCons for each of the literals above *)
-Variable addrPrimTyCon : TyCon 0. Extract Inlined Constant addrPrimTyCon => "TysPrim.addrPrimTyCon".
-Variable intPrimTyCon : TyCon 0. Extract Inlined Constant intPrimTyCon => "TysPrim.intPrimTyCon".
-Variable wordPrimTyCon : TyCon 0. Extract Inlined Constant wordPrimTyCon => "TysPrim.wordPrimTyCon".
-Variable int64PrimTyCon : TyCon 0. Extract Inlined Constant int64PrimTyCon => "TysPrim.int64PrimTyCon".
-Variable word64PrimTyCon : TyCon 0. Extract Inlined Constant word64PrimTyCon => "TysPrim.word64PrimTyCon".
-Variable floatPrimTyCon : TyCon 0. Extract Inlined Constant floatPrimTyCon => "TysPrim.floatPrimTyCon".
-Variable doublePrimTyCon : TyCon 0. Extract Inlined Constant doublePrimTyCon => "TysPrim.doublePrimTyCon".
-Variable charPrimTyCon : TyCon 0. Extract Inlined Constant charPrimTyCon => "TysPrim.charPrimTyCon".
+Variable addrPrimTyCon : TyCon. Extract Inlined Constant addrPrimTyCon => "TysPrim.addrPrimTyCon".
+Variable intPrimTyCon : TyCon. Extract Inlined Constant intPrimTyCon => "TysPrim.intPrimTyCon".
+Variable wordPrimTyCon : TyCon. Extract Inlined Constant wordPrimTyCon => "TysPrim.wordPrimTyCon".
+Variable int64PrimTyCon : TyCon. Extract Inlined Constant int64PrimTyCon => "TysPrim.int64PrimTyCon".
+Variable word64PrimTyCon : TyCon. Extract Inlined Constant word64PrimTyCon => "TysPrim.word64PrimTyCon".
+Variable floatPrimTyCon : TyCon. Extract Inlined Constant floatPrimTyCon => "TysPrim.floatPrimTyCon".
+Variable doublePrimTyCon : TyCon. Extract Inlined Constant doublePrimTyCon => "TysPrim.doublePrimTyCon".
+Variable charPrimTyCon : TyCon. Extract Inlined Constant charPrimTyCon => "TysPrim.charPrimTyCon".
(* retrieves the TyCon for a given Literal *)
-Definition haskLiteralToTyCon (lit:HaskLiteral) : TyCon 0 :=
+Definition haskLiteralToTyCon (lit:HaskLiteral) : TyCon :=
match lit with
| HaskMachNullAddr => addrPrimTyCon
| HaskMachChar _ => charPrimTyCon
| HaskMachDouble _ => doublePrimTyCon
| HaskMachLabel _ _ _ => addrPrimTyCon
end.
-
-Variable haskLiteralToString : HaskLiteral -> string. Extract Inlined Constant haskLiteralToString => "outputableToString".
-
-(* 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} :=
-| mkTriple : A -> B -> C -> triple.
-Notation "a ** b ** c" := (mkTriple a b c) (at level 20).
-Extract Inductive triple => "(,,)" [ "(,,)" ].
-
-Inductive AltCon :=
-| DataAlt : forall {n:nat}(tc:TyCon n){m q r:nat}, @DataCon n tc m q r -> AltCon
-| LitAlt : HaskLiteral -> AltCon
-| DEFAULT : AltCon.
-Extract Inductive AltCon =>
- "CoreSyn.AltCon" [ "CoreSyn.DataAlt" "CoreSyn.LitAlt" "CoreSyn.DEFAULT" ].
-