src/HaskGeneral.v

   1 (*********************************************************************************************************************************)
   2 (* HaskGeneral:  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 (* all Figure references are to the System FC1 paper *)
  12
  13 (* Figure 1: production T; index is the number of type constructors *)
  14 Variable TyCon      : nat -> Type.               Extract Inlined Constant TyCon => "TyCon.TyCon".
  15
  16 (* Figure 1: production "K" *)
  17 Variable DataCon    :  ∀n, TyCon n
  18                                  -> nat          (* number of existential tyvars associated with this datacon *)
  19                                  -> nat          (* number of coercion variables associated with this datacon *)
  20                                  -> nat          (* number of value variables (fields) associated with this datacon *)
  21                                  -> Type.        Extract Inlined Constant DataCon => "DataCon.DataCon".
  22
  23 Variable CoFunConst            : nat -> Type.    (* production "C";  extracts to TyCon.TyCon  *)
  24 Variable TyFunConst            : nat -> Type.    (* production "Sn"; extracts to TyCon.TyCon *)
  25
  26 (* magic TyCons *)
  27 Variable ArrowTyCon            : TyCon 2.        (* the TyCon for (->), the regular old function-space type constructor *)
  28 Variable CoercionTyCon         : TyCon 2.        (* the TyCon for (+>), the coercion type constructor *)
  29 Variable hetMetCodeTypeTyCon   : TyCon 2.        Extract Inlined Constant hetMetCodeTypeTyCon => "TysWiredIn.hetMetCodeTypeTyCon".
  30 Variable Class_                : nat -> Type.    Extract Inlined Constant Class_     => "Class.Class".
  31 Variable classTyCon : ∀ n, Class_ n -> TyCon n.  Extract Inlined Constant classTyCon => "Class.classTyCon".
  32 Variable Note                  : Type.           Extract Inlined Constant Note       => "CoreSyn.Note".
  33 Implicit Arguments DataCon [ [n] ].
  34
  35 (* Figure 7: production κ, ι *)
  36 Inductive Kind : Type :=
  37   | KindType         : Kind                      (* ★  - the kind of boxed types*)
  38   | KindTypeFunction : Kind  -> Kind  -> Kind    (* ⇛ *)
  39   | KindUnliftedType : Kind                      (* not in the paper - this is the kind of unboxed non-tuple types *)
  40   | KindUnboxedTuple : Kind                      (* not in the paper - this is the kind of unboxed tuples *)
  41   | KindArgType      : Kind                      (* not in the paper - this is the lub of KindType and KindUnliftedType *)
  42   | KindOpenType     : Kind                      (* not in the paper - kind of all types (lifted, boxed, whatever) *).
  43
  44 Notation "'★'"   := KindType.
  45 Notation "a ⇛ b" := (KindTypeFunction a b).
  46
  47 Instance KindEqDecidable : EqDecidable Kind.
  48   apply Build_EqDecidable.
  49   induction v1.
  50     destruct v2; try (right; intro q; inversion q; fail) ; left ; auto.
  51     destruct v2; try (right; intro q; inversion q; fail) ; auto.
  52       destruct (IHv1_1 v2_1); destruct (IHv1_2 v2_2); subst; auto;
  53       right; intro; subst; inversion H; subst; apply n; auto.
  54     destruct v2; try (right; intro q; inversion q; fail) ; left ; auto.
  55     destruct v2; try (right; intro q; inversion q; fail) ; left ; auto.
  56     destruct v2; try (right; intro q; inversion q; fail) ; left ; auto.
  57     destruct v2; try (right; intro q; inversion q; fail) ; left ; auto.
  58   Defined.
  59
  60 Variable tyConToString       : forall n, TyCon n -> string.  Extract Inlined Constant tyConToString         => "outputableToString".
  61 Variable tyFunToString       : ∀ n, TyFunConst n -> string.  Extract Inlined Constant tyFunToString         => "outputableToString".
  62 Variable coFunToString       : ∀ n, CoFunConst n -> string.  Extract Inlined Constant coFunToString         => "outputableToString".
  63 Variable natTostring         : nat->string.                  Extract Inlined Constant natTostring           => "natTostring".
  64
  65
  66 Axiom    tycons_distinct       : ~(ArrowTyCon=hetMetCodeTypeTyCon).
  67 (* GHC provides decision procedures for equality on its primitive types; we tell Coq to blindly trust them *)
  68 Variable tyCon_eq   : forall {k}(n1 n2:TyCon k),  sumbool (n1=n2) (not (n1=n2)).
  69     Extract Inlined Constant tyCon_eq   => "(==)".
  70 Variable dataCon_eq : forall {n}{tc:TyCon n}{q}{r}{s}(n1 n2:DataCon tc q r s),  sumbool (n1=n2) (not (n1=n2)).
  71     Extract Inlined Constant dataCon_eq => "(==)".
  72 Instance TyConEqDecidable {n} : EqDecidable (TyCon n) := { eqd_dec            := tyCon_eq }.
  73 Instance DataConEqDecidable {n}{tc:TyCon n}{a}{b}{c} : EqDecidable (@DataCon _ tc a b c) := { eqd_dec            := dataCon_eq }.