From: Adam Megacz <megacz@cs.berkeley.edu>
Date: Tue, 15 Mar 2011 01:27:32 +0000 (-0700)
Subject: change names of Kind constructors to be more informative
X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=commitdiff_plain;h=3d56944e3882ec751fa99b4476a013c4d86fd0f8

change names of Kind constructors to be more informative
---

diff --git a/src/HaskKinds.v b/src/HaskKinds.v
index b5cc2ff..54a1f64 100644
--- a/src/HaskKinds.v
+++ b/src/HaskKinds.v
@@ -14,19 +14,20 @@ Instance NatToStringInstance : ToString nat := { toString := natToString }.
 
 (* Figure 7: production κ, ι *)
 Inductive Kind : Type := 
-  | KindType          : Kind                      (* ★  - the kind of coercions and the kind of types inhabited by [boxed] values *)
-  | KindTypeFunction  : Kind  -> Kind  -> Kind    (* ⇛  - type-function-space; things of kind X⇛Y are NOT inhabited by expressions*)
+  | 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 KindType and KindUnliftedType *)
-  | KindOpenType      : Kind                      (* not in the paper - kind of all types (lifted, boxed, whatever) *).
+  | 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) *)
+  .
 
 Open Scope string_scope.
 Fixpoint kindToString (k:Kind) : string :=
   match k with
-  | KindType                     => "*"
-  | KindTypeFunction KindType k2 => "*=>"+++kindToString k2
-  | KindTypeFunction k1 k2       => "("+++kindToString k1+++")=>"+++kindToString k2
+  | KindStar                     => "*"
+  | KindArrow KindStar k2        => "*=>"+++kindToString k2
+  | KindArrow k1 k2              => "("+++kindToString k1+++")=>"+++kindToString k2
   | KindUnliftedType             => "#"
   | KindUnboxedTuple             => "(#)"
   | KindArgType                  => "??"
@@ -34,8 +35,8 @@ Fixpoint kindToString (k:Kind) : string :=
   end.
 Instance KindToString : ToString Kind := { toString := kindToString }.
 
-Notation "'★'"   := KindType.
-Notation "a ⇛ b" := (KindTypeFunction a b).
+Notation "'★'"   := KindStar.
+Notation "a ⇛ b" := (KindArrow a b).
 
 Instance KindEqDecidable : EqDecidable Kind.
   apply Build_EqDecidable.
diff --git a/src/HaskProofToLatex.v b/src/HaskProofToLatex.v
index 7624c31..be5cb31 100644
--- a/src/HaskProofToLatex.v
+++ b/src/HaskProofToLatex.v
@@ -26,9 +26,9 @@ Section ToLatex.
 
   Fixpoint kind2latex (k:Kind) : string :=
     match k with
-    | KindType                     => "\star"
-    | KindTypeFunction KindType k2 => "\star\Rightarrow "+++kind2latex k2
-    | KindTypeFunction k1 k2       => "("+++kind2latex k1+++")\Rightarrow "+++kind2latex k2
+    | KindStar                     => "\star"
+    | KindArrow KindStar k2 => "\star\Rightarrow "+++kind2latex k2
+    | KindArrow k1 k2       => "("+++kind2latex k1+++")\Rightarrow "+++kind2latex k2
     | KindUnliftedType             => "\text{\tt{\#}}"
     | KindUnboxedTuple             => "\text{\tt{(\#)}}"
     | KindArgType                  => "\text{\tt{??}}"
diff --git a/src/HaskStrongTypes.v b/src/HaskStrongTypes.v
index 9bc4219..f849be1 100644
--- a/src/HaskStrongTypes.v
+++ b/src/HaskStrongTypes.v
@@ -74,7 +74,7 @@ Instance DataConEqDecidable : forall tc, EqDecidable (@DataCon tc).
   right; auto.
   Defined.
 
-Definition tyConKind' tc := fold_right KindTypeFunction ★ (tyConKind tc).
+Definition tyConKind' tc := fold_right KindArrow ★ (tyConKind tc).
 
 (* types prefixed with "Raw" are NOT binder-polymorphic; they have had their PHOAS parameter instantiated already *)
 Section Raw.
@@ -185,7 +185,7 @@ Definition HaskTApp {Γ}{κ}(σ:forall TV (env:@InstantiatedTypeEnv TV Γ), TV 
   := fun TV env => σ TV env (cv TV env).
 Definition HaskBrak {Γ}(v:HaskTyVar Γ ★)(t:HaskType Γ ★) : HaskType Γ ★:=
   fun TV env => @TCode TV (TVar (v TV env)) (t TV env).
-Definition HaskTCon {Γ}(tc:TyCon) : HaskType Γ (fold_right KindTypeFunction ★ (tyConKind tc))
+Definition HaskTCon {Γ}(tc:TyCon) : HaskType Γ (fold_right KindArrow ★ (tyConKind tc))
   := fun TV ite => TCon tc.
 Definition HaskAppT {Γ}{κ₁}{κ₂}(t1:HaskType Γ (κ₂⇛κ₁))(t2:HaskType Γ κ₂) : HaskType Γ κ₁ :=
   fun TV ite => TApp (t1 TV ite) (t2 TV ite).
@@ -336,11 +336,11 @@ Definition weakF {Γ:TypeEnv}{κ}{κ₂}(f:forall TV (env:@InstantiatedTypeEnv T
 
 Fixpoint caseType0 {Γ}(lk:list Kind) :
   IList _ (HaskType Γ) lk ->
-  HaskType Γ (fold_right KindTypeFunction ★ lk) ->
+  HaskType Γ (fold_right KindArrow ★ lk) ->
   HaskType Γ ★ :=
   match lk as LK return
     IList _ (HaskType Γ) LK ->
-    HaskType Γ (fold_right KindTypeFunction ★ LK) ->
+    HaskType Γ (fold_right KindArrow ★ LK) ->
     HaskType Γ ★ 
   with
   | nil    => fun _     ht => ht