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   | KindStar          : Kind                      (* ★  - the kind of coercions and the kind of types inhabited by [boxed] values *)
  18   | KindArrow         : 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 KindStar and KindUnliftedType *)
  22   | KindOpenType      : Kind                      (* not in the paper - kind of all types (lifted, boxed, whatever) *)
  23   .
  24
  25 Open Scope string_scope.
  26 Fixpoint kindToString (k:Kind) : string :=
  27   match k with
  28   | KindStar                     => "*"
  29   | KindArrow KindStar k2        => "*=>"+++kindToString k2
  30   | KindArrow k1 k2              => "("+++kindToString k1+++")=>"+++kindToString k2
  31   | KindUnliftedType             => "#"
  32   | KindUnboxedTuple             => "(#)"
  33   | KindArgType                  => "??"
  34   | KindOpenType                 => "?"
  35   end.
  36 Instance KindToString : ToString Kind := { toString := kindToString }.
  37
  38 Notation "'★'"   := KindStar.
  39 Notation "a ⇛ b" := (KindArrow a b).
  40
  41 Instance KindEqDecidable : EqDecidable Kind.
  42   apply Build_EqDecidable.
  43   induction v1.
  44     destruct v2; try (right; intro q; inversion q; fail) ; left ; auto.
  45     destruct v2; try (right; intro q; inversion q; fail) ; auto.
  46       destruct (IHv1_1 v2_1); destruct (IHv1_2 v2_2); subst; auto;
  47       right; intro; subst; inversion H; subst; apply n; 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     destruct v2; try (right; intro q; inversion q; fail) ; left ; auto.
  52   Defined.
  53
  54 (* splits a kind into a list of arguments and a result *)
  55 Fixpoint splitKind (k:Kind) : ((list Kind) * Kind) :=
  56   match k with
  57     | a ⇛ b => let (args,res) := splitKind b in ((a::args),res)
  58     | _     => (nil, k)
  59   end.
  60