X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskKinds.v;h=3539e953ab946166f39e094c64d0157a5a4281d8;hp=b063b56083bff811a0eb160f0d80a599d7fe4b47;hb=ec8ee5cde986e5b38bcae38cda9e63eba94f1d9f;hpb=bcb16a7fa1ff772f12807c4587609fd756b7762e

diff --git a/src/HaskKinds.v b/src/HaskKinds.v
index b063b56..3539e95 100644
--- a/src/HaskKinds.v
+++ b/src/HaskKinds.v
@@ -1,5 +1,5 @@
 (*********************************************************************************************************************************)
-(* 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.
@@ -8,20 +8,46 @@ Require Import General.
 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.
@@ -36,3 +62,10 @@ Instance KindEqDecidable : EqDecidable Kind.
     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.
+