src/HaskWeakTypes.v

   1 (*********************************************************************************************************************************)
   2 (* HaskWeakTypes: types HaskWeak                                                                                                 *)
   3 (*********************************************************************************************************************************)
   4
   5 Generalizable All Variables.
   6 Require Import Preamble.
   7 Require Import General.
   8 Require Import Coq.Strings.String.
   9 Require Import Coq.Lists.List.
  10 Require Import HaskKinds.
  11 Require Import HaskLiterals.
  12 Require Import HaskTyCons.
  13 Require Import HaskCoreVars.
  14
  15 (* a WeakTypeVar merely wraps a CoreVar and includes its Kind *)
  16 Inductive WeakTypeVar := weakTypeVar : CoreVar -> Kind -> WeakTypeVar.
  17
  18 (*
  19  * WeakType is much like CoreType, but:
  20  *   1. avoids mutually-inductive definitions
  21  *   2. gives special cases for the tycons which have their own typing rules so we can pattern-match on them
  22  *   3. separates type functions from type constructors, and uses a normal "AppTy" for applying the latter
  23  *)
  24 Inductive WeakType :=
  25 | WTyVarTy  : WeakTypeVar                                      -> WeakType
  26 | WAppTy    : WeakType            ->                  WeakType -> WeakType
  27 | WTyFunApp : TyFun               ->             list WeakType -> WeakType
  28 | WTyCon    : TyCon                                            -> WeakType
  29 | WFunTyCon :                                                     WeakType    (* never use (WTyCon ArrowCon);    always use this! *)
  30 | WCodeTy   : WeakTypeVar         ->                  WeakType -> WeakType    (* never use the raw tycon *)
  31 | WCoFunTy  : WeakType            -> WeakType      -> WeakType -> WeakType
  32 | WForAllTy : WeakTypeVar         ->                  WeakType -> WeakType
  33 | WClassP   : Class_              ->             list WeakType -> WeakType
  34 | WIParam   : CoreIPName CoreName ->                  WeakType -> WeakType.
  35
  36 (* EqDecidable instances for WeakType *)
  37 Instance WeakTypeVarEqDecidable : EqDecidable WeakTypeVar.
  38   apply Build_EqDecidable.
  39   intros.
  40   destruct v1 as [cv1 k1].
  41   destruct v2 as [cv2 k2].
  42   destruct (eqd_dec cv1 cv2); subst.
  43     destruct (eqd_dec k1 k2); subst.
  44     left; auto.
  45     right; intro; apply n; inversion H; subst; auto.
  46     right; intro; apply n; inversion H; subst; auto.
  47     Defined.
  48
  49 (* a WeakCoerVar just wraps a CoreVar and tags it with the pair of types amongst which it coerces *)
  50 Inductive WeakCoerVar := weakCoerVar : CoreVar -> WeakType -> WeakType -> WeakCoerVar.
  51
  52 Inductive WeakCoercion : Type :=
  53 | WCoVar          : WeakCoerVar                                   -> WeakCoercion (* g      *)
  54 | WCoType         : WeakType                                      -> WeakCoercion (* τ      *)
  55 | WCoApp          : WeakCoercion -> WeakCoercion                  -> WeakCoercion (* γ γ    *)
  56 | WCoAppT         : WeakCoercion -> WeakType                      -> WeakCoercion (* γ@v    *)
  57 | WCoAll          : Kind  -> (WeakTypeVar -> WeakCoercion)        -> WeakCoercion (* ∀a:κ.γ *)
  58 | WCoSym          : WeakCoercion                                  -> WeakCoercion (* sym    *)
  59 | WCoComp         : WeakCoercion -> WeakCoercion                  -> WeakCoercion (* ◯      *)
  60 | WCoLeft         : WeakCoercion                                  -> WeakCoercion (* left   *)
  61 | WCoRight        : WeakCoercion                                  -> WeakCoercion (* right  *)
  62 | WCoUnsafe       : WeakType -> WeakType                          -> WeakCoercion (* unsafe *)
  63 (*| WCoCFApp        : ∀ n, CoFunConst n -> vec WeakCoercion n       -> WeakCoercion (* C   γⁿ *)*)
  64 (*| WCoTFApp        : ∀ n, TyFunConst n -> vec WeakCoercion n       -> WeakCoercion (* S_n γⁿ *)*)
  65 .
  66
  67 Fixpoint weakCoercionTypes (wc:WeakCoercion) : WeakType * WeakType :=
  68 match wc with
  69 | WCoVar     (weakCoerVar _ t1 t2)   => (WFunTyCon,WFunTyCon)   (* FIXME!!! *)
  70 | WCoType    t                       => (WFunTyCon,WFunTyCon)   (* FIXME!!! *)
  71 | WCoApp     c1 c2                   => (WFunTyCon,WFunTyCon)   (* FIXME!!! *)
  72 | WCoAppT    c t                     => (WFunTyCon,WFunTyCon)   (* FIXME!!! *)
  73 | WCoAll     k f                     => (WFunTyCon,WFunTyCon)   (* FIXME!!! *)
  74 | WCoSym     c                       => let (t2,t1) := weakCoercionTypes c in (t1,t2)
  75 | WCoComp    c1 c2                   => (WFunTyCon,WFunTyCon)   (* FIXME!!! *)
  76 | WCoLeft    c                       => (WFunTyCon,WFunTyCon)   (* FIXME!!! *)
  77 | WCoRight   c                       => (WFunTyCon,WFunTyCon)   (* FIXME!!! *)
  78 | WCoUnsafe  t1 t2                   => (t1,t2)
  79 end.
  80
  81
  82 (* this is a trick to allow circular definitions, post-extraction *)
  83 Variable weakTypeToString : WeakType -> string.
  84     Extract Inlined Constant weakTypeToString => "(coreTypeToString . weakTypeToCoreType)".
  85 Instance WeakTypeToString : ToString WeakType := { toString := weakTypeToString }.
  86
  87 Variable tyConToCoreTyCon : TyCon  -> CoreTyCon.           Extract Inlined Constant tyConToCoreTyCon  => "(\x -> x)".
  88 Variable tyFunToCoreTyCon : TyFun  -> CoreTyCon.           Extract Inlined Constant tyFunToCoreTyCon  => "(\x -> x)".
  89 Coercion tyConToCoreTyCon : TyCon >-> CoreTyCon.
  90 Coercion tyFunToCoreTyCon : TyFun >-> CoreTyCon.