(*********************************************************************************************************************************)
-(* HaskLiterals: representation of compile-time constants (literals) *)
+(* HaskCoreLiterals: representation of compile-time constants (literals) *)
(*********************************************************************************************************************************)
Generalizable All Variables.
Require Import Preamble.
Require Import General.
Require Import Coq.Strings.String.
-Require Import HaskGeneral.
+Require Import HaskKinds.
+Require Import HaskCoreTypes.
(* 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".
Extract Inductive HaskFunctionOrData =>
"BasicTypes.FunctionOrData" [ "BasicTypes.IsFunction" "BasicTypes.IsData" ].
+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 => "(,,)" [ "(,,)" ].
+
(* 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
| 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
+| DataAlt : CoreDataCon -> AltCon
| LitAlt : HaskLiteral -> AltCon
-| DEFAULT : AltCon.
+| DEFAULT : AltCon.
Extract Inductive AltCon =>
"CoreSyn.AltCon" [ "CoreSyn.DataAlt" "CoreSyn.LitAlt" "CoreSyn.DEFAULT" ].
-