src/HaskLiteralsAndTyCons.v

   1 (*********************************************************************************************************************************)
   2 (* HaskLiteralsAndTyCons: representation of compile-time constants (literals)                                                    *)
   3 (*********************************************************************************************************************************)
   4
   5 Generalizable All Variables.
   6 Require Import Preamble.
   7 Require Import General.
   8 Require Import Coq.Strings.String.
   9 Require Import HaskKinds.
  10
  11 Variable CoreDataCon     : Type.                      Extract Inlined Constant CoreDataCon          => "DataCon.DataCon".
  12
  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".
  16
  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".
  23
  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.
  28
  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.
  42
  43 Extract Inductive HaskLiteral => "Literal.Literal"
  44   [ "Literal.MachChar"
  45     "Literal.MachStr"
  46     "Literal.MachNullAddr"
  47     "Literal.MachInt"
  48     "Literal.MachInt64"
  49     "Literal.MachWord"
  50     "Literal.MachWord64"
  51     "Literal.MachFloat"
  52     "Literal.MachDouble"
  53     "Literal.MachLabel" ].
  54 Extract Inductive HaskFunctionOrData =>
  55   "BasicTypes.FunctionOrData" [ "BasicTypes.IsFunction" "BasicTypes.IsData" ].
  56
  57 Variable haskLiteralToString : HaskLiteral -> string.    Extract Inlined Constant haskLiteralToString     => "outputableToString".
  58 Instance HaskLiteralToString : ToString HaskLiteral := { toString := haskLiteralToString }.
  59
  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".
  69
  70 (* retrieves the TyCon for a given Literal *)
  71 Definition haskLiteralToTyCon (lit:HaskLiteral) : TyCon :=
  72 match lit with
  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
  83 end.
  84
  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 }.
  89 Instance TyConToLatex    : ToLatex  TyCon := { toLatex  := fun x => toLatex (toString x) }.
  90 Instance TyFunToLatex    : ToLatex  TyCon := { toLatex  := fun x => toLatex (toString x) }.
  91
  92 Variable ModalBoxTyCon   : TyCon.        Extract Inlined Constant ModalBoxTyCon => "TysWiredIn.hetMetCodeTypeTyCon".
  93 Variable ArrowTyCon      : TyCon.        Extract Constant ArrowTyCon    => "Type.funTyCon".