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 HaskKinds.
10 Require Import HaskTyCons.
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 (* the TyCons for each of the literals above *)
51 Variable addrPrimTyCon : TyCon. Extract Inlined Constant addrPrimTyCon => "TysPrim.addrPrimTyCon".
52 Variable intPrimTyCon : TyCon. Extract Inlined Constant intPrimTyCon => "TysPrim.intPrimTyCon".
53 Variable wordPrimTyCon : TyCon. Extract Inlined Constant wordPrimTyCon => "TysPrim.wordPrimTyCon".
54 Variable int64PrimTyCon : TyCon. Extract Inlined Constant int64PrimTyCon => "TysPrim.int64PrimTyCon".
55 Variable word64PrimTyCon : TyCon. Extract Inlined Constant word64PrimTyCon => "TysPrim.word64PrimTyCon".
56 Variable floatPrimTyCon : TyCon. Extract Inlined Constant floatPrimTyCon => "TysPrim.floatPrimTyCon".
57 Variable doublePrimTyCon : TyCon. Extract Inlined Constant doublePrimTyCon => "TysPrim.doublePrimTyCon".
58 Variable charPrimTyCon : TyCon. Extract Inlined Constant charPrimTyCon => "TysPrim.charPrimTyCon".
60 (* retrieves the TyCon for a given Literal *)
61 Definition haskLiteralToTyCon (lit:HaskLiteral) : TyCon :=
63 | HaskMachNullAddr => addrPrimTyCon
64 | HaskMachChar _ => charPrimTyCon
65 | HaskMachStr _ => addrPrimTyCon
66 | HaskMachInt _ => intPrimTyCon
67 | HaskMachWord _ => wordPrimTyCon
68 | HaskMachInt64 _ => int64PrimTyCon
69 | HaskMachWord64 _ => word64PrimTyCon
70 | HaskMachFloat _ => floatPrimTyCon
71 | HaskMachDouble _ => doublePrimTyCon
72 | HaskMachLabel _ _ _ => addrPrimTyCon