src/HaskLiterals.v

   1 (*********************************************************************************************************************************)
   2 (* HaskLiterals: 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 HaskGeneral.
  10
  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".
  17
  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.
  31
  32 Extract Inductive HaskLiteral => "Literal.Literal"
  33   [ "Literal.MachChar"
  34     "Literal.MachStr"
  35     "Literal.MachNullAddr"
  36     "Literal.MachInt"
  37     "Literal.MachInt64"
  38     "Literal.MachWord"
  39     "Literal.MachWord64"
  40     "Literal.MachFloat"
  41     "Literal.MachDouble"
  42     "Literal.MachLabel" ].
  43 Extract Inductive HaskFunctionOrData =>
  44   "BasicTypes.FunctionOrData" [ "BasicTypes.IsFunction" "BasicTypes.IsData" ].
  45
  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".
  55
  56 (* retrieves the TyCon for a given Literal *)
  57 Definition haskLiteralToTyCon (lit:HaskLiteral) : TyCon 0 :=
  58 match lit with
  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
  69 end.
  70
  71 Variable haskLiteralToString  : HaskLiteral -> string.    Extract Inlined Constant haskLiteralToString     => "outputableToString".
  72
  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 => "(,,)" [ "(,,)" ].
  78
  79 Inductive AltCon :=
  80 | DataAlt : forall {n:nat}(tc:TyCon n){m q r:nat}, @DataCon n tc m q r -> AltCon
  81 | LitAlt  : HaskLiteral -> AltCon
  82 | DEFAULT :            AltCon.
  83 Extract Inductive AltCon =>
  84   "CoreSyn.AltCon" [ "CoreSyn.DataAlt" "CoreSyn.LitAlt" "CoreSyn.DEFAULT" ].
  85