1 (*********************************************************************************************************************************)
2 (* HaskLiterals: 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 HaskGeneral.
11 (* Since GHC is written in Haskell, compile-time Haskell constants are represented using Haskell (Prelude) types *)
12 Variable HaskInt : Type. Extract Inlined Constant HaskInt => "Prelude.Int".
13 Variable HaskChar : Type. Extract Inlined Constant HaskChar => "Prelude.Char".
14 Variable HaskFastString : Type. Extract Inlined Constant HaskFastString => "FastString.FastString".
15 Variable HaskInteger : Type. Extract Inlined Constant HaskInteger => "Prelude.Integer".
16 Variable HaskRational : Type. Extract Inlined Constant HaskRational => "Prelude.Rational".
18 (* This type extracts exactly onto GHC's Literal.Literal type *)
19 Inductive HaskLiteral :=
20 | HaskMachChar : HaskChar -> HaskLiteral
21 | HaskMachStr : HaskFastString -> HaskLiteral
22 | HaskMachNullAddr : HaskLiteral
23 | HaskMachInt : HaskInteger -> HaskLiteral
24 | HaskMachInt64 : HaskInteger -> HaskLiteral
25 | HaskMachWord : HaskInteger -> HaskLiteral
26 | HaskMachWord64 : HaskInteger -> HaskLiteral
27 | HaskMachFloat : HaskRational -> HaskLiteral
28 | HaskMachDouble : HaskRational -> HaskLiteral
29 | HaskMachLabel : HaskFastString -> option HaskInt -> HaskFunctionOrData -> HaskLiteral
30 with HaskFunctionOrData : Type := HaskIsFunction | HaskIsData.
32 Extract Inductive HaskLiteral => "Literal.Literal"
35 "Literal.MachNullAddr"
42 "Literal.MachLabel" ].
43 Extract Inductive HaskFunctionOrData =>
44 "BasicTypes.FunctionOrData" [ "BasicTypes.IsFunction" "BasicTypes.IsData" ].
46 (* the TyCons for each of the literals above *)
47 Variable addrPrimTyCon : TyCon 0. Extract Inlined Constant addrPrimTyCon => "TysPrim.addrPrimTyCon".
48 Variable intPrimTyCon : TyCon 0. Extract Inlined Constant intPrimTyCon => "TysPrim.intPrimTyCon".
49 Variable wordPrimTyCon : TyCon 0. Extract Inlined Constant wordPrimTyCon => "TysPrim.wordPrimTyCon".
50 Variable int64PrimTyCon : TyCon 0. Extract Inlined Constant int64PrimTyCon => "TysPrim.int64PrimTyCon".
51 Variable word64PrimTyCon : TyCon 0. Extract Inlined Constant word64PrimTyCon => "TysPrim.word64PrimTyCon".
52 Variable floatPrimTyCon : TyCon 0. Extract Inlined Constant floatPrimTyCon => "TysPrim.floatPrimTyCon".
53 Variable doublePrimTyCon : TyCon 0. Extract Inlined Constant doublePrimTyCon => "TysPrim.doublePrimTyCon".
54 Variable charPrimTyCon : TyCon 0. Extract Inlined Constant charPrimTyCon => "TysPrim.charPrimTyCon".
56 (* retrieves the TyCon for a given Literal *)
57 Definition haskLiteralToTyCon (lit:HaskLiteral) : TyCon 0 :=
59 | HaskMachNullAddr => addrPrimTyCon
60 | HaskMachChar _ => charPrimTyCon
61 | HaskMachStr _ => addrPrimTyCon
62 | HaskMachInt _ => intPrimTyCon
63 | HaskMachWord _ => wordPrimTyCon
64 | HaskMachInt64 _ => int64PrimTyCon
65 | HaskMachWord64 _ => word64PrimTyCon
66 | HaskMachFloat _ => floatPrimTyCon
67 | HaskMachDouble _ => doublePrimTyCon
68 | HaskMachLabel _ _ _ => addrPrimTyCon
71 Variable haskLiteralToString : HaskLiteral -> string. Extract Inlined Constant haskLiteralToString => "outputableToString".
73 (* because Haskell's 3-tuples (triples) are distinct from both ((x,y),z) and (x,(y,z)), we need a new type: *)
74 Inductive triple {A B C:Type} :=
75 | mkTriple : A -> B -> C -> triple.
76 Notation "a ** b ** c" := (mkTriple a b c) (at level 20).
77 Extract Inductive triple => "(,,)" [ "(,,)" ].
80 | DataAlt : forall {n:nat}(tc:TyCon n){m q r:nat}, @DataCon n tc m q r -> AltCon
81 | LitAlt : HaskLiteral -> AltCon
83 Extract Inductive AltCon =>
84 "CoreSyn.AltCon" [ "CoreSyn.DataAlt" "CoreSyn.LitAlt" "CoreSyn.DEFAULT" ].