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".
49 (* because Haskell's 3-tuples (triples) are distinct from both ((x,y),z) and (x,(y,z)), we need a new type: *)
50 Inductive triple {A B C:Type} :=
51 | mkTriple : A -> B -> C -> triple.
52 Notation "a ** b ** c" := (mkTriple a b c) (at level 20).
53 Extract Inductive triple => "(,,)" [ "(,,)" ].
55 (* the TyCons for each of the literals above *)
56 Variable addrPrimTyCon : TyCon. Extract Inlined Constant addrPrimTyCon => "TysPrim.addrPrimTyCon".
57 Variable intPrimTyCon : TyCon. Extract Inlined Constant intPrimTyCon => "TysPrim.intPrimTyCon".
58 Variable wordPrimTyCon : TyCon. Extract Inlined Constant wordPrimTyCon => "TysPrim.wordPrimTyCon".
59 Variable int64PrimTyCon : TyCon. Extract Inlined Constant int64PrimTyCon => "TysPrim.int64PrimTyCon".
60 Variable word64PrimTyCon : TyCon. Extract Inlined Constant word64PrimTyCon => "TysPrim.word64PrimTyCon".
61 Variable floatPrimTyCon : TyCon. Extract Inlined Constant floatPrimTyCon => "TysPrim.floatPrimTyCon".
62 Variable doublePrimTyCon : TyCon. Extract Inlined Constant doublePrimTyCon => "TysPrim.doublePrimTyCon".
63 Variable charPrimTyCon : TyCon. Extract Inlined Constant charPrimTyCon => "TysPrim.charPrimTyCon".
65 (* retrieves the TyCon for a given Literal *)
66 Definition haskLiteralToTyCon (lit:HaskLiteral) : TyCon :=
68 | HaskMachNullAddr => addrPrimTyCon
69 | HaskMachChar _ => charPrimTyCon
70 | HaskMachStr _ => addrPrimTyCon
71 | HaskMachInt _ => intPrimTyCon
72 | HaskMachWord _ => wordPrimTyCon
73 | HaskMachInt64 _ => int64PrimTyCon
74 | HaskMachWord64 _ => word64PrimTyCon
75 | HaskMachFloat _ => floatPrimTyCon
76 | HaskMachDouble _ => doublePrimTyCon
77 | HaskMachLabel _ _ _ => addrPrimTyCon
81 | DataAlt : CoreDataCon -> AltCon
82 | LitAlt : HaskLiteral -> AltCon
84 Extract Inductive AltCon =>
85 "CoreSyn.AltCon" [ "CoreSyn.DataAlt" "CoreSyn.LitAlt" "CoreSyn.DEFAULT" ].