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 Fixpoint kindToLatexMath (k:Kind) : LatexMath :=
  42   match k with
  43   | ★                            => rawLatexMath "\star"
  44   | ★  ⇛ k2                      => (rawLatexMath "\star\Rightarrow ")+++kindToLatexMath k2
  45   | k1 ⇛ k2                      => (rawLatexMath "(")+++kindToLatexMath k1+++(rawLatexMath ")\Rightarrow ")+++kindToLatexMath k2
  46   | KindUnliftedType             => rawLatexMath "\text{\tt{\#}}"
  47   | KindUnboxedTuple             => rawLatexMath "\text{\tt{(\#)}}"
  48   | KindArgType                  => rawLatexMath "\text{\tt{??}}"
  49   | KindOpenType                 => rawLatexMath "\text{\tt{?}}"
  50   end.
  51 Instance KindToLatexMath : ToLatexMath Kind := { toLatexMath := kindToLatexMath }.
  52
  53 Instance KindEqDecidable : EqDecidable Kind.
  54   apply Build_EqDecidable.
  55   induction v1.
  56     destruct v2; try (right; intro q; inversion q; fail) ; left ; auto.
  57     destruct v2; try (right; intro q; inversion q; fail) ; auto.
  58       destruct (IHv1_1 v2_1); destruct (IHv1_2 v2_2); subst; auto;
  59       right; intro; subst; inversion H; subst; apply n; auto.
  60     destruct v2; try (right; intro q; inversion q; fail) ; left ; auto.
  61     destruct v2; try (right; intro q; inversion q; fail) ; left ; auto.
  62     destruct v2; try (right; intro q; inversion q; fail) ; left ; auto.
  63     destruct v2; try (right; intro q; inversion q; fail) ; left ; auto.
  64   Defined.
  65
  66 (* splits a kind into a list of arguments and a result *)
  67 Fixpoint splitKind (k:Kind) : ((list Kind) * Kind) :=
  68   match k with
  69     | a ⇛ b => let (args,res) := splitKind b in ((a::args),res)
  70     | _     => (nil, k)
  71   end.
  72