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 Fixpoint kindToLatex (k:Kind) : Latex :=
44 | ★ ⇛ k2 => (latex "\star\Rightarrow ")+=+kindToLatex k2
45 | k1 ⇛ k2 => (latex "(")+=+kindToLatex k1+=+(latex ")\Rightarrow ")+=+kindToLatex k2
46 | KindUnliftedType => latex "\text{\tt{\#}}"
47 | KindUnboxedTuple => latex "\text{\tt{(\#)}}"
48 | KindArgType => latex "\text{\tt{??}}"
49 | KindOpenType => latex "\text{\tt{?}}"
51 Instance KindToLatex : ToLatex Kind := { toLatex := kindToLatex }.
53 Instance KindEqDecidable : EqDecidable Kind.
54 apply Build_EqDecidable.
56 destruct v2; try (right; intro q; inversion q; fail) ; left ; auto.
57 destruct v2; try (right; intro q; inversion q; fail) ; auto.
58 destruct (IHv1_1 v2_1); destruct (IHv1_2 v2_2); subst; auto;
59 right; intro; subst; inversion H; subst; apply n; auto.
60 destruct v2; try (right; intro q; inversion q; fail) ; left ; auto.
61 destruct v2; try (right; intro q; inversion q; fail) ; left ; auto.
62 destruct v2; try (right; intro q; inversion q; fail) ; left ; auto.
63 destruct v2; try (right; intro q; inversion q; fail) ; left ; auto.
66 (* splits a kind into a list of arguments and a result *)
67 Fixpoint splitKind (k:Kind) : ((list Kind) * Kind) :=
69 | a ⇛ b => let (args,res) := splitKind b in ((a::args),res)