src/HaskCoreVars.v

   1 (*********************************************************************************************************************************)
   2 (* HaskCoreVars: basically GHC's Var.Var imported into Coqland                                                                   *)
   3 (*********************************************************************************************************************************)
   4
   5 Generalizable All Variables.
   6 Require Import Preamble.
   7 Require Import General.
   8 Require Import Coq.Strings.String.
   9 Require Import HaskLiteralsAndTyCons.
  10
  11 (* GHC uses a single type for expression variables, type variables, and coercion variables; this is that type *)
  12 Variable CoreVar            : Type.                                               Extract Inlined Constant CoreVar    => "Var.Var".
  13 Variable coreVar_eq         : forall (a b:CoreVar), sumbool (a=b) (not (a=b)).    Extract Inlined Constant coreVar_eq => "(==)".
  14 Variable coreVarToString    : CoreVar      -> string.             Extract Inlined Constant coreVarToString => "outputableToString".
  15 Instance CoreVarEqDecidable : EqDecidable CoreVar := { eqd_dec  := coreVar_eq      }.
  16 Instance CoreVarToString    : ToString CoreVar    := { toString := coreVarToString }.
  17
  18 Variable CoreTyCon       : Type.                      Extract Inlined Constant CoreTyCon            => "TyCon.TyCon".
  19
  20 (* because Haskell's 3-tuples (triples) are distinct from both ((x,y),z) and (x,(y,z)), we need a new type: *)
  21 Inductive triple {A B C:Type} :=
  22 | mkTriple : A -> B -> C -> triple.
  23 Notation "a ** b ** c" := (mkTriple a b c) (at level 20).
  24 Extract Inductive triple => "(,,)" [ "(,,)" ].
  25
  26 Inductive CoreAltCon :=
  27 | DataAlt : CoreDataCon -> CoreAltCon
  28 | LitAlt  : HaskLiteral -> CoreAltCon
  29 | DEFAULT :                CoreAltCon.
  30 Extract Inductive CoreAltCon =>
  31   "CoreSyn.AltCon" [ "CoreSyn.DataAlt" "CoreSyn.LitAlt" "CoreSyn.DEFAULT" ].