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 nat2string          : nat         -> string.        Extract Inlined Constant nat2string            => "nat2string".
  13
  14 (* Figure 7: production κ, ι *)
  15 Inductive Kind : Type :=
  16   | KindType         : Kind                      (* ★  - the kind of boxed types*)
  17   | KindTypeFunction : Kind  -> Kind  -> Kind    (* ⇛ *)
  18   | KindUnliftedType : Kind                      (* not in the paper - this is the kind of unboxed non-tuple types *)
  19   | KindUnboxedTuple : Kind                      (* not in the paper - this is the kind of unboxed tuples *)
  20   | KindArgType      : Kind                      (* not in the paper - this is the lub of KindType and KindUnliftedType *)
  21   | KindOpenType     : Kind                      (* not in the paper - kind of all types (lifted, boxed, whatever) *).
  22
  23 Notation "'★'"   := KindType.
  24 Notation "a ⇛ b" := (KindTypeFunction a b).
  25
  26 Instance KindEqDecidable : EqDecidable Kind.
  27   apply Build_EqDecidable.
  28   induction v1.
  29     destruct v2; try (right; intro q; inversion q; fail) ; left ; auto.
  30     destruct v2; try (right; intro q; inversion q; fail) ; auto.
  31       destruct (IHv1_1 v2_1); destruct (IHv1_2 v2_2); subst; auto;
  32       right; intro; subst; inversion H; subst; apply n; auto.
  33     destruct v2; try (right; intro q; inversion q; fail) ; left ; auto.
  34     destruct v2; try (right; intro q; inversion q; fail) ; left ; auto.
  35     destruct v2; try (right; intro q; inversion q; fail) ; left ; auto.
  36     destruct v2; try (right; intro q; inversion q; fail) ; left ; auto.
  37   Defined.
  38