1 (*********************************************************************************************************************************)
2 (* HaskCoreLiterals: representation of compile-time constants (literals) *)
3 (*********************************************************************************************************************************)
5 Generalizable All Variables.
6 Require Import Preamble.
7 Require Import General.
8 Require Import Coq.Strings.String.
9 Require Import HaskKinds.
10 Require Import HaskCoreTypes.
12 (* Since GHC is written in Haskell, compile-time Haskell constants are represented using Haskell (Prelude) types *)
13 Variable HaskInt : Type. Extract Inlined Constant HaskInt => "Prelude.Int".
14 Variable HaskChar : Type. Extract Inlined Constant HaskChar => "Prelude.Char".
15 Variable HaskFastString : Type. Extract Inlined Constant HaskFastString => "FastString.FastString".
16 Variable HaskInteger : Type. Extract Inlined Constant HaskInteger => "Prelude.Integer".
17 Variable HaskRational : Type. Extract Inlined Constant HaskRational => "Prelude.Rational".
19 (* This type extracts exactly onto GHC's Literal.Literal type *)
20 Inductive HaskLiteral :=
21 | HaskMachChar : HaskChar -> HaskLiteral
22 | HaskMachStr : HaskFastString -> HaskLiteral
23 | HaskMachNullAddr : HaskLiteral
24 | HaskMachInt : HaskInteger -> HaskLiteral
25 | HaskMachInt64 : HaskInteger -> HaskLiteral
26 | HaskMachWord : HaskInteger -> HaskLiteral
27 | HaskMachWord64 : HaskInteger -> HaskLiteral
28 | HaskMachFloat : HaskRational -> HaskLiteral
29 | HaskMachDouble : HaskRational -> HaskLiteral
30 | HaskMachLabel : HaskFastString -> option HaskInt -> HaskFunctionOrData -> HaskLiteral
31 with HaskFunctionOrData : Type := HaskIsFunction | HaskIsData.
33 Extract Inductive HaskLiteral => "Literal.Literal"
36 "Literal.MachNullAddr"
43 "Literal.MachLabel" ].
44 Extract Inductive HaskFunctionOrData =>
45 "BasicTypes.FunctionOrData" [ "BasicTypes.IsFunction" "BasicTypes.IsData" ].
47 Variable haskLiteralToString : HaskLiteral -> string. Extract Inlined Constant haskLiteralToString => "outputableToString".
48 Instance HaskLiteralToString : ToString HaskLiteral := { toString := haskLiteralToString }.
50 (* because Haskell's 3-tuples (triples) are distinct from both ((x,y),z) and (x,(y,z)), we need a new type: *)
51 Inductive triple {A B C:Type} :=
52 | mkTriple : A -> B -> C -> triple.
53 Notation "a ** b ** c" := (mkTriple a b c) (at level 20).
54 Extract Inductive triple => "(,,)" [ "(,,)" ].
57 | DataAlt : CoreDataCon -> AltCon
58 | LitAlt : HaskLiteral -> AltCon
60 Extract Inductive AltCon =>
61 "CoreSyn.AltCon" [ "CoreSyn.DataAlt" "CoreSyn.LitAlt" "CoreSyn.DEFAULT" ].
63 (* the TyCons for each of the literals above *)
64 Variable addrPrimTyCon : TyCon. Extract Inlined Constant addrPrimTyCon => "TysPrim.addrPrimTyCon".
65 Variable intPrimTyCon : TyCon. Extract Inlined Constant intPrimTyCon => "TysPrim.intPrimTyCon".
66 Variable wordPrimTyCon : TyCon. Extract Inlined Constant wordPrimTyCon => "TysPrim.wordPrimTyCon".
67 Variable int64PrimTyCon : TyCon. Extract Inlined Constant int64PrimTyCon => "TysPrim.int64PrimTyCon".
68 Variable word64PrimTyCon : TyCon. Extract Inlined Constant word64PrimTyCon => "TysPrim.word64PrimTyCon".
69 Variable floatPrimTyCon : TyCon. Extract Inlined Constant floatPrimTyCon => "TysPrim.floatPrimTyCon".
70 Variable doublePrimTyCon : TyCon. Extract Inlined Constant doublePrimTyCon => "TysPrim.doublePrimTyCon".
71 Variable charPrimTyCon : TyCon. Extract Inlined Constant charPrimTyCon => "TysPrim.charPrimTyCon".
73 (* retrieves the TyCon for a given Literal *)
74 Definition haskLiteralToTyCon (lit:HaskLiteral) : TyCon :=
76 | HaskMachNullAddr => addrPrimTyCon
77 | HaskMachChar _ => charPrimTyCon
78 | HaskMachStr _ => addrPrimTyCon
79 | HaskMachInt _ => intPrimTyCon
80 | HaskMachWord _ => wordPrimTyCon
81 | HaskMachInt64 _ => int64PrimTyCon
82 | HaskMachWord64 _ => word64PrimTyCon
83 | HaskMachFloat _ => floatPrimTyCon
84 | HaskMachDouble _ => doublePrimTyCon
85 | HaskMachLabel _ _ _ => addrPrimTyCon