+++ /dev/null
-(*********************************************************************************************************************************)
-(* HaskLiteralsAndTyCons: representation of compile-time constants (literals) *)
-(*********************************************************************************************************************************)
-
-Generalizable All Variables.
-Require Import Preamble.
-Require Import General.
-Require Import Coq.Strings.String.
-Require Import HaskKinds.
-
-Variable CoreDataCon : Type. Extract Inlined Constant CoreDataCon => "DataCon.DataCon".
-
-(* once again, we pull the trick of having multiple Coq types map to a single Haskell type to provide stronger typing *)
-Variable TyCon : Type. Extract Inlined Constant TyCon => "TyCon.TyCon".
-Variable TyFun : Type. Extract Inlined Constant TyFun => "TyCon.TyCon".
-
-(* Since GHC is written in Haskell, compile-time Haskell constants are represented using Haskell (Prelude) types *)
-Variable HaskInt : Type. Extract Inlined Constant HaskInt => "Prelude.Int".
-Variable HaskChar : Type. Extract Inlined Constant HaskChar => "Prelude.Char".
-Variable HaskFastString : Type. Extract Inlined Constant HaskFastString => "FastString.FastString".
-Variable HaskInteger : Type. Extract Inlined Constant HaskInteger => "Prelude.Integer".
-Variable HaskRational : Type. Extract Inlined Constant HaskRational => "Prelude.Rational".
-
-Variable CoreName : Type. Extract Inlined Constant CoreName => "Name.Name".
-Variable Class_ : Type. Extract Inlined Constant Class_ => "Class.Class".
-Variable CoreIPName : Type -> Type. Extract Constant CoreIPName "’a" => "BasicTypes.IPName".
- Extraction Inline CoreIPName.
-
-(* This type extracts exactly onto GHC's Literal.Literal type *)
-Inductive HaskLiteral :=
-| HaskMachChar : HaskChar -> HaskLiteral
-| HaskMachStr : HaskFastString -> HaskLiteral
-| HaskMachNullAddr : HaskLiteral
-| HaskMachInt : HaskInteger -> HaskLiteral
-| HaskMachInt64 : HaskInteger -> HaskLiteral
-| HaskMachWord : HaskInteger -> HaskLiteral
-| HaskMachWord64 : HaskInteger -> HaskLiteral
-| HaskMachFloat : HaskRational -> HaskLiteral
-| HaskMachDouble : HaskRational -> HaskLiteral
-| HaskMachLabel : HaskFastString -> option HaskInt -> HaskFunctionOrData -> HaskLiteral
-with HaskFunctionOrData : Type := HaskIsFunction | HaskIsData.
-
-Extract Inductive HaskLiteral => "Literal.Literal"
- [ "Literal.MachChar"
- "Literal.MachStr"
- "Literal.MachNullAddr"
- "Literal.MachInt"
- "Literal.MachInt64"
- "Literal.MachWord"
- "Literal.MachWord64"
- "Literal.MachFloat"
- "Literal.MachDouble"
- "Literal.MachLabel" ].
-Extract Inductive HaskFunctionOrData =>
- "BasicTypes.FunctionOrData" [ "BasicTypes.IsFunction" "BasicTypes.IsData" ].
-
-Variable haskLiteralToString : HaskLiteral -> string. Extract Inlined Constant haskLiteralToString => "outputableToString".
-Instance HaskLiteralToString : ToString HaskLiteral := { toString := haskLiteralToString }.
-
-(* the TyCons for each of the literals above *)
-Variable addrPrimTyCon : TyCon. Extract Inlined Constant addrPrimTyCon => "TysPrim.addrPrimTyCon".
-Variable intPrimTyCon : TyCon. Extract Inlined Constant intPrimTyCon => "TysPrim.intPrimTyCon".
-Variable wordPrimTyCon : TyCon. Extract Inlined Constant wordPrimTyCon => "TysPrim.wordPrimTyCon".
-Variable int64PrimTyCon : TyCon. Extract Inlined Constant int64PrimTyCon => "TysPrim.int64PrimTyCon".
-Variable word64PrimTyCon : TyCon. Extract Inlined Constant word64PrimTyCon => "TysPrim.word64PrimTyCon".
-Variable floatPrimTyCon : TyCon. Extract Inlined Constant floatPrimTyCon => "TysPrim.floatPrimTyCon".
-Variable doublePrimTyCon : TyCon. Extract Inlined Constant doublePrimTyCon => "TysPrim.doublePrimTyCon".
-Variable charPrimTyCon : TyCon. Extract Inlined Constant charPrimTyCon => "TysPrim.charPrimTyCon".
-
-(* retrieves the TyCon for a given Literal *)
-Definition haskLiteralToTyCon (lit:HaskLiteral) : TyCon :=
-match lit with
- | HaskMachNullAddr => addrPrimTyCon
- | HaskMachChar _ => charPrimTyCon
- | HaskMachStr _ => addrPrimTyCon
- | HaskMachInt _ => intPrimTyCon
- | HaskMachWord _ => wordPrimTyCon
- | HaskMachInt64 _ => int64PrimTyCon
- | HaskMachWord64 _ => word64PrimTyCon
- | HaskMachFloat _ => floatPrimTyCon
- | HaskMachDouble _ => doublePrimTyCon
- | HaskMachLabel _ _ _ => addrPrimTyCon
-end.
-
-Variable tyConToString : TyCon -> string. Extract Inlined Constant tyConToString => "outputableToString".
-Variable tyFunToString : TyFun -> string. Extract Inlined Constant tyFunToString => "outputableToString".
-Instance TyConToString : ToString TyCon := { toString := tyConToString }.
-Instance TyFunToString : ToString TyFun := { toString := tyFunToString }.
-Instance TyConToLatex : ToLatex TyCon := { toLatex := fun x => toLatex (toString x) }.
-Instance TyFunToLatex : ToLatex TyCon := { toLatex := fun x => toLatex (toString x) }.
-
-Variable ModalBoxTyCon : TyCon. Extract Inlined Constant ModalBoxTyCon => "TysWiredIn.hetMetCodeTypeTyCon".
-Variable PairTyCon : TyFun. Extract Inlined Constant PairTyCon => "TysWiredIn.pairTyCon".
-Variable UnitTyCon : TyFun. Extract Inlined Constant UnitTyCon => "TysWiredIn.unitTyCon".
-Variable ArrowTyCon : TyCon. Extract Constant ArrowTyCon => "Type.funTyCon".
projects / coq-hetmet.git / blobdiff