(*********************************************************************************************************************************)
-(* HaskKinds: Definitions shared by all four representations (Core, Weak, Strong, Proof) *)
+(* HaskKinds: Definitions shared by all four representations (Core, Weak, Strong, Proof) *)
(*********************************************************************************************************************************)
Generalizable All Variables.
Require Import Coq.Strings.String.
Open Scope nat_scope.
-Variable Note : Type. Extract Inlined Constant Note => "CoreSyn.Note".
-Variable nat2string : nat -> string. Extract Inlined Constant nat2string => "nat2string".
+Variable Note : Type. Extract Inlined Constant Note => "CoreSyn.Note".
+Variable natToString : nat -> string. Extract Inlined Constant natToString => "natToString".
+Instance NatToStringInstance : ToString nat := { toString := natToString }.
-(* Figure 7: production κ, ι *)
Inductive Kind : Type :=
- | KindType : Kind (* ★ - the kind of boxed types*)
- | KindTypeFunction : Kind -> Kind -> Kind (* ⇛ *)
- | KindUnliftedType : Kind (* not in the paper - this is the kind of unboxed non-tuple types *)
- | KindUnboxedTuple : Kind (* not in the paper - this is the kind of unboxed tuples *)
- | KindArgType : Kind (* not in the paper - this is the lub of KindType and KindUnliftedType *)
- | KindOpenType : Kind (* not in the paper - kind of all types (lifted, boxed, whatever) *).
+ | KindStar : Kind (* ★ - the kind of coercions and the kind of types inhabited by [boxed] values *)
+ | KindArrow : Kind -> Kind -> Kind (* ⇛ - type-function-space; things of kind X⇛Y are NOT inhabited by expressions*)
+ | KindUnliftedType : Kind (* not in the paper - this is the kind of unboxed non-tuple types *)
+ | KindUnboxedTuple : Kind (* not in the paper - this is the kind of unboxed tuples *)
+ | KindArgType : Kind (* not in the paper - this is the lub of KindStar and KindUnliftedType *)
+ | KindOpenType : Kind (* not in the paper - kind of all types (lifted, boxed, whatever) *)
+ .
-Notation "'★'" := KindType.
-Notation "a ⇛ b" := (KindTypeFunction a b).
+Open Scope string_scope.
+Fixpoint kindToString (k:Kind) : string :=
+ match k with
+ | KindStar => "*"
+ | KindArrow KindStar k2 => "*=>"+++kindToString k2
+ | KindArrow k1 k2 => "("+++kindToString k1+++")=>"+++kindToString k2
+ | KindUnliftedType => "#"
+ | KindUnboxedTuple => "(#)"
+ | KindArgType => "??"
+ | KindOpenType => "?"
+ end.
+Instance KindToString : ToString Kind := { toString := kindToString }.
+
+Notation "'★'" := KindStar.
+Notation "a ⇛ b" := (KindArrow a b).
+
+Fixpoint kindToLatexMath (k:Kind) : LatexMath :=
+ match k with
+ | ★ => rawLatexMath "\star"
+ | ★ ⇛ k2 => (rawLatexMath "\star\Rightarrow ")+++kindToLatexMath k2
+ | k1 ⇛ k2 => (rawLatexMath "(")+++kindToLatexMath k1+++(rawLatexMath ")\Rightarrow ")+++kindToLatexMath k2
+ | KindUnliftedType => rawLatexMath "\text{\tt{\#}}"
+ | KindUnboxedTuple => rawLatexMath "\text{\tt{(\#)}}"
+ | KindArgType => rawLatexMath "\text{\tt{??}}"
+ | KindOpenType => rawLatexMath "\text{\tt{?}}"
+ end.
+Instance KindToLatexMath : ToLatexMath Kind := { toLatexMath := kindToLatexMath }.
Instance KindEqDecidable : EqDecidable Kind.
apply Build_EqDecidable.
destruct v2; try (right; intro q; inversion q; fail) ; left ; auto.
Defined.
+(* splits a kind into a list of arguments and a result *)
+Fixpoint splitKind (k:Kind) : ((list Kind) * Kind) :=
+ match k with
+ | a ⇛ b => let (args,res) := splitKind b in ((a::args),res)
+ | _ => (nil, k)
+ end.
+