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 natToString : nat -> string. Extract Inlined Constant natToString => "natToString".
13 Instance NatToStringInstance : ToString nat := { toString := natToString }.
15 (* Figure 7: production κ, ι *)
16 Inductive Kind : Type :=
17 | KindType : Kind (* ★ - the kind of coercions and the kind of types inhabited by [boxed] values *)
18 | KindTypeFunction : Kind -> Kind -> Kind (* ⇛ - type-function-space; things of kind X⇛Y are NOT inhabited by expressions*)
19 | KindUnliftedType : Kind (* not in the paper - this is the kind of unboxed non-tuple types *)
20 | KindUnboxedTuple : Kind (* not in the paper - this is the kind of unboxed tuples *)
21 | KindArgType : Kind (* not in the paper - this is the lub of KindType and KindUnliftedType *)
22 | KindOpenType : Kind (* not in the paper - kind of all types (lifted, boxed, whatever) *).
24 Open Scope string_scope.
25 Fixpoint kindToString (k:Kind) : string :=
28 | KindTypeFunction KindType k2 => "*=>"+++kindToString k2
29 | KindTypeFunction k1 k2 => "("+++kindToString k1+++")=>"+++kindToString k2
30 | KindUnliftedType => "#"
31 | KindUnboxedTuple => "(#)"
35 Instance KindToString : ToString Kind := { toString := kindToString }.
37 Notation "'★'" := KindType.
38 Notation "a ⇛ b" := (KindTypeFunction a b).
40 Instance KindEqDecidable : EqDecidable Kind.
41 apply Build_EqDecidable.
43 destruct v2; try (right; intro q; inversion q; fail) ; left ; auto.
44 destruct v2; try (right; intro q; inversion q; fail) ; auto.
45 destruct (IHv1_1 v2_1); destruct (IHv1_2 v2_2); subst; auto;
46 right; intro; subst; inversion H; subst; apply n; auto.
47 destruct v2; try (right; intro q; inversion q; fail) ; left ; auto.
48 destruct v2; try (right; intro q; inversion q; fail) ; left ; auto.
49 destruct v2; try (right; intro q; inversion q; fail) ; left ; auto.
50 destruct v2; try (right; intro q; inversion q; fail) ; left ; auto.