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 Inductive Kind : Type :=
  16   | KindStar          : Kind                      (* ★  - the kind of coercions and the kind of types inhabited by [boxed] values *)
  17   | KindArrow         : Kind  -> Kind  -> Kind    (* ⇛  - type-function-space; things of kind X⇛Y are NOT inhabited by expressions*)
  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 KindStar and KindUnliftedType *)
  21   | KindOpenType      : Kind                      (* not in the paper - kind of all types (lifted, boxed, whatever) *)
  22   .
  23
  24 Open Scope string_scope.
  25 Fixpoint kindToString (k:Kind) : string :=
  26   match k with
  27   | KindStar                     => "*"
  28   | KindArrow KindStar k2        => "*=>"+++kindToString k2
  29   | KindArrow 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 "'★'"   := KindStar.
  38 Notation "a ⇛ b" := (KindArrow a b).
  39
  40 (* the kind of environment classifiers *)
  41 Definition ECKind := ★ ⇛ ★ ⇛ ★.
  42 Opaque ECKind.
  43
  44 Fixpoint kindToLatexMath (k:Kind) : LatexMath :=
  45   match k with
  46   | ★                            => rawLatexMath "\star"
  47   | ★  ⇛ k2                      => (rawLatexMath "\star\Rightarrow ")+++kindToLatexMath k2
  48   | k1 ⇛ k2                      => (rawLatexMath "(")+++kindToLatexMath k1+++(rawLatexMath ")\Rightarrow ")+++kindToLatexMath k2
  49   | KindUnliftedType             => rawLatexMath "\text{\tt{\#}}"
  50   | KindUnboxedTuple             => rawLatexMath "\text{\tt{(\#)}}"
  51   | KindArgType                  => rawLatexMath "\text{\tt{??}}"
  52   | KindOpenType                 => rawLatexMath "\text{\tt{?}}"
  53   end.
  54 Instance KindToLatexMath : ToLatexMath Kind := { toLatexMath := kindToLatexMath }.
  55
  56 Instance KindEqDecidable : EqDecidable Kind.
  57   apply Build_EqDecidable.
  58   induction v1.
  59     destruct v2; try (right; intro q; inversion q; fail) ; left ; auto.
  60     destruct v2; try (right; intro q; inversion q; fail) ; auto.
  61       destruct (IHv1_1 v2_1); destruct (IHv1_2 v2_2); subst; auto;
  62       right; intro; subst; inversion H; subst; apply n; auto.
  63     destruct v2; try (right; intro q; inversion q; fail) ; left ; auto.
  64     destruct v2; try (right; intro q; inversion q; fail) ; left ; auto.
  65     destruct v2; try (right; intro q; inversion q; fail) ; left ; auto.
  66     destruct v2; try (right; intro q; inversion q; fail) ; left ; auto.
  67   Defined.
  68
  69 (* splits a kind into a list of arguments and a result *)
  70 Fixpoint splitKind (k:Kind) : ((list Kind) * Kind) :=
  71   match k with
  72     | a ⇛ b => let (args,res) := splitKind b in ((a::args),res)
  73     | _     => (nil, k)
  74   end.
  75