1 (*********************************************************************************************************************************)
2 (* HaskLiteralsAndTyCons: 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.
11 Variable CoreDataCon : Type. Extract Inlined Constant CoreDataCon => "DataCon.DataCon".
13 (* once again, we pull the trick of having multiple Coq types map to a single Haskell type to provide stronger typing *)
14 Variable TyCon : Type. Extract Inlined Constant TyCon => "TyCon.TyCon".
15 Variable TyFun : Type. Extract Inlined Constant TyFun => "TyCon.TyCon".
17 (* Since GHC is written in Haskell, compile-time Haskell constants are represented using Haskell (Prelude) types *)
18 Variable HaskInt : Type. Extract Inlined Constant HaskInt => "Prelude.Int".
19 Variable HaskChar : Type. Extract Inlined Constant HaskChar => "Prelude.Char".
20 Variable HaskFastString : Type. Extract Inlined Constant HaskFastString => "FastString.FastString".
21 Variable HaskInteger : Type. Extract Inlined Constant HaskInteger => "Prelude.Integer".
22 Variable HaskRational : Type. Extract Inlined Constant HaskRational => "Prelude.Rational".
24 Variable CoreName : Type. Extract Inlined Constant CoreName => "Name.Name".
25 Variable Class_ : Type. Extract Inlined Constant Class_ => "Class.Class".
26 Variable CoreIPName : Type -> Type. Extract Constant CoreIPName "’a" => "BasicTypes.IPName".
27 Extraction Inline CoreIPName.
29 (* This type extracts exactly onto GHC's Literal.Literal type *)
30 Inductive HaskLiteral :=
31 | HaskMachChar : HaskChar -> HaskLiteral
32 | HaskMachStr : HaskFastString -> HaskLiteral
33 | HaskMachNullAddr : HaskLiteral
34 | HaskMachInt : HaskInteger -> HaskLiteral
35 | HaskMachInt64 : HaskInteger -> HaskLiteral
36 | HaskMachWord : HaskInteger -> HaskLiteral
37 | HaskMachWord64 : HaskInteger -> HaskLiteral
38 | HaskMachFloat : HaskRational -> HaskLiteral
39 | HaskMachDouble : HaskRational -> HaskLiteral
40 | HaskMachLabel : HaskFastString -> option HaskInt -> HaskFunctionOrData -> HaskLiteral
41 with HaskFunctionOrData : Type := HaskIsFunction | HaskIsData.
43 Extract Inductive HaskLiteral => "Literal.Literal"
46 "Literal.MachNullAddr"
53 "Literal.MachLabel" ].
54 Extract Inductive HaskFunctionOrData =>
55 "BasicTypes.FunctionOrData" [ "BasicTypes.IsFunction" "BasicTypes.IsData" ].
57 Variable haskLiteralToString : HaskLiteral -> string. Extract Inlined Constant haskLiteralToString => "outputableToString".
58 Instance HaskLiteralToString : ToString HaskLiteral := { toString := haskLiteralToString }.
60 (* the TyCons for each of the literals above *)
61 Variable addrPrimTyCon : TyCon. Extract Inlined Constant addrPrimTyCon => "TysPrim.addrPrimTyCon".
62 Variable intPrimTyCon : TyCon. Extract Inlined Constant intPrimTyCon => "TysPrim.intPrimTyCon".
63 Variable wordPrimTyCon : TyCon. Extract Inlined Constant wordPrimTyCon => "TysPrim.wordPrimTyCon".
64 Variable int64PrimTyCon : TyCon. Extract Inlined Constant int64PrimTyCon => "TysPrim.int64PrimTyCon".
65 Variable word64PrimTyCon : TyCon. Extract Inlined Constant word64PrimTyCon => "TysPrim.word64PrimTyCon".
66 Variable floatPrimTyCon : TyCon. Extract Inlined Constant floatPrimTyCon => "TysPrim.floatPrimTyCon".
67 Variable doublePrimTyCon : TyCon. Extract Inlined Constant doublePrimTyCon => "TysPrim.doublePrimTyCon".
68 Variable charPrimTyCon : TyCon. Extract Inlined Constant charPrimTyCon => "TysPrim.charPrimTyCon".
70 (* retrieves the TyCon for a given Literal *)
71 Definition haskLiteralToTyCon (lit:HaskLiteral) : TyCon :=
73 | HaskMachNullAddr => addrPrimTyCon
74 | HaskMachChar _ => charPrimTyCon
75 | HaskMachStr _ => addrPrimTyCon
76 | HaskMachInt _ => intPrimTyCon
77 | HaskMachWord _ => wordPrimTyCon
78 | HaskMachInt64 _ => int64PrimTyCon
79 | HaskMachWord64 _ => word64PrimTyCon
80 | HaskMachFloat _ => floatPrimTyCon
81 | HaskMachDouble _ => doublePrimTyCon
82 | HaskMachLabel _ _ _ => addrPrimTyCon
85 Variable tyConToString : TyCon -> string. Extract Inlined Constant tyConToString => "outputableToString".
86 Variable tyFunToString : TyFun -> string. Extract Inlined Constant tyFunToString => "outputableToString".
87 Instance TyConToString : ToString TyCon := { toString := tyConToString }.
88 Instance TyFunToString : ToString TyFun := { toString := tyFunToString }.