1 (*********************************************************************************************************************************)
2 (* HaskCoreVars: basically GHC's Var.Var imported into Coqland *)
3 (*********************************************************************************************************************************)
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.
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 }.
19 Variable CoreTyCon : Type. Extract Inlined Constant CoreTyCon => "TyCon.TyCon".
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 => "(,,)" [ "(,,)" ].
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" ].