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 Inductive Kind : Type :=
16 | KindStar : Kind (* ★ - the kind of coercions and the kind of types inhabited by [boxed] values *)
17 | KindArrow : Kind -> Kind -> Kind (* ⇛ - type-function-space; things of kind X⇛Y are NOT inhabited by expressions*)
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 KindStar and KindUnliftedType *)
21 | 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 | KindArrow KindStar k2 => "*=>"+++kindToString k2
29 | KindArrow k1 k2 => "("+++kindToString k1+++")=>"+++kindToString k2
30 | KindUnliftedType => "#"
31 | KindUnboxedTuple => "(#)"
35 Instance KindToString : ToString Kind := { toString := kindToString }.
37 Notation "'★'" := KindStar.
38 Notation "a ⇛ b" := (KindArrow a b).
40 (* the kind of environment classifiers *)
41 Definition ECKind := ★ ⇛ ★ ⇛ ★.
44 Fixpoint kindToLatexMath (k:Kind) : LatexMath :=
46 | ★ => rawLatexMath "\star"
47 | ★ ⇛ k2 => (rawLatexMath "\star\Rightarrow ")+++kindToLatexMath k2
48 | k1 ⇛ k2 => (rawLatexMath "(")+++kindToLatexMath k1+++(rawLatexMath ")\Rightarrow ")+++kindToLatexMath k2
49 | KindUnliftedType => rawLatexMath "\text{\tt{\#}}"
50 | KindUnboxedTuple => rawLatexMath "\text{\tt{(\#)}}"
51 | KindArgType => rawLatexMath "\text{\tt{??}}"
52 | KindOpenType => rawLatexMath "\text{\tt{?}}"
54 Instance KindToLatexMath : ToLatexMath Kind := { toLatexMath := kindToLatexMath }.
56 Instance KindEqDecidable : EqDecidable Kind.
57 apply Build_EqDecidable.
59 destruct v2; try (right; intro q; inversion q; fail) ; left ; auto.
60 destruct v2; try (right; intro q; inversion q; fail) ; auto.
61 destruct (IHv1_1 v2_1); destruct (IHv1_2 v2_2); subst; auto;
62 right; intro; subst; inversion H; subst; apply n; auto.
63 destruct v2; try (right; intro q; inversion q; fail) ; left ; auto.
64 destruct v2; try (right; intro q; inversion q; fail) ; left ; auto.
65 destruct v2; try (right; intro q; inversion q; fail) ; left ; auto.
66 destruct v2; try (right; intro q; inversion q; fail) ; left ; auto.
69 (* splits a kind into a list of arguments and a result *)
70 Fixpoint splitKind (k:Kind) : ((list Kind) * Kind) :=
72 | a ⇛ b => let (args,res) := splitKind b in ((a::args),res)