1 (*********************************************************************************************************************************)
2 (* HaskGeneral: Definitions shared by all four representations (Core, Weak, Strong, Proof) *)
3 (*********************************************************************************************************************************)
5 Generalizable All Variables.
6 Require Import Preamble.
7 Require Import General.
8 Require Import Coq.Strings.String.
11 (* all Figure references are to the System FC1 paper *)
13 (* Figure 1: production T; index is the number of type constructors *)
14 Variable TyCon : nat -> Type. Extract Inlined Constant TyCon => "TyCon.TyCon".
16 (* Figure 1: production "K" *)
17 Variable DataCon : ∀n, TyCon n
18 -> nat (* number of existential tyvars associated with this datacon *)
19 -> nat (* number of coercion variables associated with this datacon *)
20 -> nat (* number of value variables (fields) associated with this datacon *)
21 -> Type. Extract Inlined Constant DataCon => "DataCon.DataCon".
23 Variable CoFunConst : nat -> Type. (* production "C"; extracts to TyCon.TyCon *)
24 Variable TyFunConst : nat -> Type. (* production "Sn"; extracts to TyCon.TyCon *)
27 Variable ArrowTyCon : TyCon 2. (* the TyCon for (->), the regular old function-space type constructor *)
28 Variable CoercionTyCon : TyCon 2. (* the TyCon for (+>), the coercion type constructor *)
29 Variable hetMetCodeTypeTyCon : TyCon 2. Extract Inlined Constant hetMetCodeTypeTyCon => "TysWiredIn.hetMetCodeTypeTyCon".
30 Variable Class_ : nat -> Type. Extract Inlined Constant Class_ => "Class.Class".
31 Variable classTyCon : ∀ n, Class_ n -> TyCon n. Extract Inlined Constant classTyCon => "Class.classTyCon".
32 Variable Note : Type. Extract Inlined Constant Note => "CoreSyn.Note".
33 Implicit Arguments DataCon [ [n] ].
35 (* Figure 7: production κ, ι *)
36 Inductive Kind : Type :=
37 | KindType : Kind (* ★ - the kind of boxed types*)
38 | KindTypeFunction : Kind -> Kind -> Kind (* ⇛ *)
39 | KindUnliftedType : Kind (* not in the paper - this is the kind of unboxed non-tuple types *)
40 | KindUnboxedTuple : Kind (* not in the paper - this is the kind of unboxed tuples *)
41 | KindArgType : Kind (* not in the paper - this is the lub of KindType and KindUnliftedType *)
42 | KindOpenType : Kind (* not in the paper - kind of all types (lifted, boxed, whatever) *).
44 Notation "'★'" := KindType.
45 Notation "a ⇛ b" := (KindTypeFunction a b).
47 Variable tyConToString : forall n, TyCon n -> string. Extract Inlined Constant tyConToString => "outputableToString".
48 Variable tyFunToString : ∀ n, TyFunConst n -> string. Extract Inlined Constant tyFunToString => "outputableToString".
49 Variable coFunToString : ∀ n, CoFunConst n -> string. Extract Inlined Constant coFunToString => "outputableToString".
50 Variable natTostring : nat->string. Extract Inlined Constant natTostring => "natTostring".
53 Axiom tycons_distinct : ~(ArrowTyCon=hetMetCodeTypeTyCon).
54 (* GHC provides decision procedures for equality on its primitive types; we tell Coq to blindly trust them *)
55 Variable tyCon_eq : forall {k}(n1 n2:TyCon k), sumbool (n1=n2) (not (n1=n2)).
56 Extract Inlined Constant tyCon_eq => "(==)".
57 Variable dataCon_eq : forall {n}{tc:TyCon n}{q}{r}{s}(n1 n2:DataCon tc q r s), sumbool (n1=n2) (not (n1=n2)).
58 Extract Inlined Constant dataCon_eq => "(==)".
59 Axiom tyCon_eq_reflexive : forall `(tc:TyCon n), (tyCon_eq tc tc) = (left _ (refl_equal tc)).
60 Axiom dataCon_eq_reflexive : forall `(tc:@DataCon y z q r p) , (dataCon_eq tc tc) = (left _ (refl_equal tc)).
62 Instance TyConEqDecidable {n} : EqDecidable (TyCon n) :=
64 ; eqd_dec_reflexive := tyCon_eq_reflexive
67 Instance DataConEqDecidable {n}{tc:TyCon n}{a}{b}{c} : EqDecidable (@DataCon _ tc a b c) :=
68 { eqd_dec := dataCon_eq
69 ; eqd_dec_reflexive := dataCon_eq_reflexive