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 | KindStar : Kind (* ★ - the kind of coercions and the kind of types inhabited by [boxed] values *)
18 | KindArrow : 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 KindStar and KindUnliftedType *)
22 | KindOpenType : Kind (* not in the paper - kind of all types (lifted, boxed, whatever) *)
25 Open Scope string_scope.
26 Fixpoint kindToString (k:Kind) : string :=
29 | KindArrow KindStar k2 => "*=>"+++kindToString k2
30 | KindArrow k1 k2 => "("+++kindToString k1+++")=>"+++kindToString k2
31 | KindUnliftedType => "#"
32 | KindUnboxedTuple => "(#)"
36 Instance KindToString : ToString Kind := { toString := kindToString }.
38 Notation "'★'" := KindStar.
39 Notation "a ⇛ b" := (KindArrow a b).
41 Instance KindEqDecidable : EqDecidable Kind.
42 apply Build_EqDecidable.
44 destruct v2; try (right; intro q; inversion q; fail) ; left ; auto.
45 destruct v2; try (right; intro q; inversion q; fail) ; auto.
46 destruct (IHv1_1 v2_1); destruct (IHv1_2 v2_2); subst; auto;
47 right; intro; subst; inversion H; subst; apply n; 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.
51 destruct v2; try (right; intro q; inversion q; fail) ; left ; auto.
54 (* splits a kind into a list of arguments and a result *)
55 Fixpoint splitKind (k:Kind) : ((list Kind) * Kind) :=
57 | a ⇛ b => let (args,res) := splitKind b in ((a::args),res)