minor cleanups, deleted dead code, eliminated use of (==) on CoreType

[coq-hetmet.git] / src / HaskKinds.v

diff --git a/src/HaskKinds.v b/src/HaskKinds.v
index 583bb86..b5cc2ff 100644 (file)
--- a/src/HaskKinds.v
+++ b/src/HaskKinds.v
@@ -29,7 +29,7 @@ Fixpoint kindToString (k:Kind) : string :=
   | KindTypeFunction k1 k2       => "("+++kindToString k1+++")=>"+++kindToString k2
   | KindUnliftedType             => "#"
   | KindUnboxedTuple             => "(#)"
-  | KindArgType                  => "?"
+  | KindArgType                  => "??"
   | KindOpenType                 => "?"
   end.
 Instance KindToString : ToString Kind := { toString := kindToString }.
@@ -50,3 +50,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.
+