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