1 (*********************************************************************************************************************************)
2 (* HaskKinds: 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 Variable Note : Type. Extract Inlined Constant Note => "CoreSyn.Note".
12 Variable nat2string : nat -> string. Extract Inlined Constant nat2string => "nat2string".
14 (* Figure 7: production κ, ι *)
15 Inductive Kind : Type :=
16 | KindType : Kind (* ★ - the kind of boxed types*)
17 | KindTypeFunction : Kind -> Kind -> Kind (* ⇛ *)
18 | KindUnliftedType : Kind (* not in the paper - this is the kind of unboxed non-tuple types *)
19 | KindUnboxedTuple : Kind (* not in the paper - this is the kind of unboxed tuples *)
20 | KindArgType : Kind (* not in the paper - this is the lub of KindType and KindUnliftedType *)
21 | KindOpenType : Kind (* not in the paper - kind of all types (lifted, boxed, whatever) *).
23 Notation "'★'" := KindType.
24 Notation "a ⇛ b" := (KindTypeFunction a b).
26 Instance KindEqDecidable : EqDecidable Kind.
27 apply Build_EqDecidable.
29 destruct v2; try (right; intro q; inversion q; fail) ; left ; auto.
30 destruct v2; try (right; intro q; inversion q; fail) ; auto.
31 destruct (IHv1_1 v2_1); destruct (IHv1_2 v2_2); subst; auto;
32 right; intro; subst; inversion H; subst; apply n; auto.
33 destruct v2; try (right; intro q; inversion q; fail) ; left ; auto.
34 destruct v2; try (right; intro q; inversion q; fail) ; left ; auto.
35 destruct v2; try (right; intro q; inversion q; fail) ; left ; auto.
36 destruct v2; try (right; intro q; inversion q; fail) ; left ; auto.