src/HaskKinds.v

   1 (*********************************************************************************************************************************)
   2 (* HaskKinds:  Definitions shared by all four representations (Core, Weak, Strong, Proof)                                        *)
   3 (*********************************************************************************************************************************)
   4
   5 Generalizable All Variables.
   6 Require Import Preamble.
   7 Require Import General.
   8 Require Import Coq.Strings.String.
   9 Open Scope nat_scope.
  10
  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 }.
  14
  15 (* Figure 7: production κ, ι *)
  16 Inductive Kind : Type :=
  17   | KindType          : Kind                      (* ★  - the kind of coercions and the kind of types inhabited by [boxed] values *)
  18   | KindTypeFunction  : 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 KindType and KindUnliftedType *)
  22   | KindOpenType      : Kind                      (* not in the paper - kind of all types (lifted, boxed, whatever) *).
  23
  24 Open Scope string_scope.
  25 Fixpoint kindToString (k:Kind) : string :=
  26   match k with
  27   | KindType                     => "*"
  28   | KindTypeFunction KindType k2 => "*=>"+++kindToString k2
  29   | KindTypeFunction k1 k2       => "("+++kindToString k1+++")=>"+++kindToString k2
  30   | KindUnliftedType             => "#"
  31   | KindUnboxedTuple             => "(#)"
  32   | KindArgType                  => "??"
  33   | KindOpenType                 => "?"
  34   end.
  35 Instance KindToString : ToString Kind := { toString := kindToString }.
  36
  37 Notation "'★'"   := KindType.
  38 Notation "a ⇛ b" := (KindTypeFunction a b).
  39
  40 Instance KindEqDecidable : EqDecidable Kind.
  41   apply Build_EqDecidable.
  42   induction v1.
  43     destruct v2; try (right; intro q; inversion q; fail) ; left ; auto.
  44     destruct v2; try (right; intro q; inversion q; fail) ; auto.
  45       destruct (IHv1_1 v2_1); destruct (IHv1_2 v2_2); subst; auto;
  46       right; intro; subst; inversion H; subst; apply n; auto.
  47     destruct v2; try (right; intro q; inversion q; fail) ; left ; auto.
  48     destruct v2; try (right; intro q; inversion q; fail) ; left ; auto.
  49     destruct v2; try (right; intro q; inversion q; fail) ; left ; auto.
  50     destruct v2; try (right; intro q; inversion q; fail) ; left ; auto.
  51   Defined.
  52
  53 (* splits a kind into a list of arguments and a result *)
  54 Fixpoint splitKind (k:Kind) : ((list Kind) * Kind) :=
  55   match k with
  56     | a ⇛ b => let (args,res) := splitKind b in ((a::args),res)
  57     | _     => (nil, k)
  58   end.
  59