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