src/HaskStrongTypes.v

   1 (*********************************************************************************************************************************)
   2 (* HaskStrongTypes: representation of types and coercions for HaskStrong                                                         *)
   3 (*********************************************************************************************************************************)
   4
   5 Generalizable All Variables.
   6 Require Import Preamble.
   7 Require Import Coq.Strings.String.
   8 Require Import Coq.Lists.List.
   9 Require Import General.
  10 Require Import HaskKinds.
  11 Require Import HaskLiterals.
  12 Require Import HaskTyCons.
  13 Require Import HaskCoreTypes.
  14 Require Import HaskCoreVars.
  15 Require Import HaskWeakTypes.
  16 Require Import HaskWeakVars.
  17 Require Import HaskWeak.
  18 Require Import HaskCoreToWeak.
  19
  20 Variable dataConTyCon      : CoreDataCon -> TyCon.         Extract Inlined Constant dataConTyCon      => "DataCon.dataConTyCon".
  21 Variable dataConExVars_    : CoreDataCon -> list CoreVar.  Extract Inlined Constant dataConExVars_    => "DataCon.dataConExTyVars".
  22 Variable dataConEqTheta_   : CoreDataCon -> list PredType. Extract Inlined Constant dataConEqTheta_   => "DataCon.dataConEqTheta".
  23 Variable dataConOrigArgTys_: CoreDataCon -> list CoreType. Extract Inlined Constant dataConOrigArgTys_=>"DataCon.dataConOrigArgTys".
  24
  25 Definition dataConExTyVars cdc :=
  26   filter (map (fun x => match coreVarToWeakVar x with WTypeVar v => Some v | _ => None end) (dataConExVars_ cdc)).
  27   Opaque dataConExTyVars.
  28 Definition dataConCoerKinds cdc :=
  29   filter (map (fun x => match x with EqPred t1 t2 =>
  30                           match (
  31                             coreTypeToWeakType t1 >>= fun t1' =>
  32                               coreTypeToWeakType t2 >>= fun t2' =>
  33                                 OK (t1',t2'))
  34                           with OK z => Some z
  35                             | _ => None
  36                           end
  37                           | _ => None
  38                         end) (dataConEqTheta_ cdc)).
  39   Opaque dataConCoerKinds.
  40 Definition dataConFieldTypes cdc :=
  41   filter (map (fun x => match coreTypeToWeakType x with
  42                           | OK z => Some z
  43                           | _ => None
  44                         end) (dataConOrigArgTys_ cdc)).
  45
  46 Definition tyConNumKinds (tc:TyCon) := length (tyConTyVars tc).
  47   Coercion tyConNumKinds : TyCon >-> nat.
  48
  49 Inductive DataCon : TyCon -> Type :=
  50   mkDataCon : forall cdc:CoreDataCon, DataCon (dataConTyCon cdc).
  51   Definition dataConToCoreDataCon `(dc:DataCon tc) : CoreDataCon := match dc with mkDataCon cdc => cdc end.
  52   Coercion mkDataCon : CoreDataCon >-> DataCon.
  53   Coercion dataConToCoreDataCon : DataCon >-> CoreDataCon.
  54   (*Opaque DataCon.*)
  55
  56 Definition tyConKind' tc := fold_right KindArrow ★ (tyConKind tc).
  57
  58 (* types prefixed with "Raw" are NOT binder-polymorphic; they have had their PHOAS parameter instantiated already *)
  59 Section Raw.
  60
  61   (* TV is the PHOAS type which stands for type variables of System FC *)
  62   Context {TV:Kind -> Type}.
  63
  64   (* Figure 7: ρ, σ, τ, ν *)
  65   Inductive RawHaskType : Kind -> Type :=
  66   | TVar           : ∀ κ, TV κ                                              -> RawHaskType κ                     (* a        *)
  67   | TCon           : ∀ tc,                                                     RawHaskType (tyConKind' tc)       (* T        *)
  68   | TArrow         :                                                           RawHaskType (★ ⇛★ ⇛★ )            (* (->)     *)
  69   | TCoerc         : ∀ κ, RawHaskType κ -> RawHaskType κ -> RawHaskType ★   -> RawHaskType ★                     (* (+>)     *)
  70   | TApp           : ∀ κ₁ κ₂, RawHaskType (κ₂⇛κ₁)        -> RawHaskType κ₂  -> RawHaskType κ₁                    (* φ φ      *)
  71   | TAll           : ∀ κ,                          (TV κ -> RawHaskType ★)  -> RawHaskType ★                     (* ∀a:κ.φ   *)
  72   | TCode          : RawHaskType ECKind                  -> RawHaskType ★   -> RawHaskType ★                     (* from λ^α *)
  73   | TyFunApp       : forall (tf:TyFun) kl k, RawHaskTypeList kl             -> RawHaskType k                     (* S_n      *)
  74   with RawHaskTypeList : list Kind -> Type :=
  75   | TyFunApp_nil   : RawHaskTypeList nil
  76   | TyFunApp_cons  : ∀ κ kl, RawHaskType κ -> RawHaskTypeList kl -> RawHaskTypeList (κ::kl).
  77
  78   (* the "kind" of a coercion is a pair of types *)
  79   Inductive RawCoercionKind : Type :=
  80     mkRawCoercionKind : ∀ κ, RawHaskType κ -> RawHaskType κ -> RawCoercionKind.
  81
  82   (* Figure 7: γ, δ; CV is the PHOAS type which stands for coercion variables of System FC *)
  83   Inductive RawHaskCoer {CV:Type} : RawCoercionKind -> Prop := .
  84   (*
  85    *  This has been disabled until we manage to reconcile SystemFC's
  86    *  coercions with what GHC actually implements (they are not the
  87    *  same!)
  88    *
  89   | CoVar          : CV                                           -> RawHaskCoer (* g      *)
  90   | CoType         : RawHaskType                                  -> RawHaskCoer (* τ      *)
  91   | CoApp          : RawHaskCoer -> RawHaskCoer                   -> RawHaskCoer (* γ γ    *)
  92   | CoAppT         : RawHaskCoer -> RawHaskType                   -> RawHaskCoer (* γ@v    *)
  93   | CoCFApp        : ∀ n, CoFunConst n -> vec RawHaskCoer n       -> RawHaskCoer (* C   γⁿ *)
  94   | CoTFApp        : ∀ n, TyFunConst n -> vec RawHaskCoer n       -> RawHaskCoer (* S_n γⁿ *)
  95   | CoAll          : Kind  -> (TV -> RawHaskCoer)                 -> RawHaskCoer (* ∀a:κ.γ *)
  96   | CoSym          : RawHaskCoer                                  -> RawHaskCoer (* sym    *)
  97   | CoComp         : RawHaskCoer -> RawHaskCoer                   -> RawHaskCoer (* ◯      *)
  98   | CoLeft         : RawHaskCoer                                  -> RawHaskCoer (* left   *)
  99   | CoRight        : RawHaskCoer                                  -> RawHaskCoer (* right  *).
 100   *)
 101 End Raw.
 102
 103 Implicit Arguments TCon   [ [TV] ].
 104 Implicit Arguments TyFunApp [ [TV] ].
 105 Implicit Arguments RawHaskType  [ ].
 106 Implicit Arguments RawHaskCoer  [ ].
 107 Implicit Arguments RawCoercionKind [ ].
 108 Implicit Arguments TVar [ [TV] [κ] ].
 109 Implicit Arguments TCoerc [ [TV] [κ] ].
 110 Implicit Arguments TApp   [ [TV] [κ₁] [κ₂] ].
 111 Implicit Arguments TAll   [ [TV] ].
 112
 113 Notation "t1 ---> t2"        := (fun TV env => (TApp (TApp TArrow (t1 TV env)) (t2 TV env))).
 114 Notation "φ₁ ∼∼ φ₂ ⇒ φ₃"     := (fun TV env => TCoerc (φ₁ TV env) (φ₂ TV env) (φ₃ TV env)).
 115
 116 (* Kind and Coercion Environments *)
 117 (*
 118  *  In System FC, the environment consists of three components, each of
 119  *  whose well-formedness depends on all of those prior to it:
 120  *
 121  *    1. (TypeEnv)        The list of free type     variables and their kinds
 122  *    2. (CoercionEnv)    The list of free coercion variables and the pair of types between which it witnesses coercibility
 123  *    3. (Tree ??CoreVar) The list of free value    variables and the type of each one
 124  *)
 125
 126 Definition TypeEnv                                                         := list Kind.
 127 Definition InstantiatedTypeEnv     (TV:Kind->Type)         (Γ:TypeEnv)     := IList _ TV Γ.
 128 Definition HaskCoercionKind                    (Γ:TypeEnv)                 := ∀ TV, InstantiatedTypeEnv TV Γ -> @RawCoercionKind TV.
 129 Definition CoercionEnv             (Γ:TypeEnv)                             := list (HaskCoercionKind Γ).
 130 Definition InstantiatedCoercionEnv (TV:Kind->Type) CV       (Γ:TypeEnv)(Δ:CoercionEnv Γ):= vec CV (length Δ).
 131
 132 (* A (HaskXX Γ) is an XX which is valid in environments of shape Γ; they are always PHOAS-uninstantiated *)
 133 Definition HaskTyVar (Γ:TypeEnv) κ :=  forall TV    (env:@InstantiatedTypeEnv TV Γ), TV κ.
 134 Definition HaskCoVar Γ Δ           :=  forall TV CV (env:@InstantiatedTypeEnv TV Γ)(cenv:@InstantiatedCoercionEnv TV CV Γ Δ), CV.
 135 Definition HaskLevel (Γ:TypeEnv)   :=  list (HaskTyVar Γ ECKind).
 136 Definition HaskType  (Γ:TypeEnv) κ := ∀ TV, @InstantiatedTypeEnv TV Γ -> RawHaskType TV κ.
 137 Definition haskTyVarToType {Γ}{κ}(htv:HaskTyVar Γ κ) : HaskType Γ κ := fun TV ite => TVar (htv TV ite).
 138
 139 Inductive HaskTypeOfSomeKind (Γ:TypeEnv) :=
 140   haskTypeOfSomeKind : ∀ κ, HaskType Γ κ -> HaskTypeOfSomeKind Γ.
 141   Implicit Arguments haskTypeOfSomeKind [ [Γ] [κ] ].
 142   Definition kindOfHaskTypeOfSomeKind {Γ}(htosk:HaskTypeOfSomeKind Γ) :=
 143     match htosk with
 144       haskTypeOfSomeKind κ _ => κ
 145     end.
 146   Coercion kindOfHaskTypeOfSomeKind : HaskTypeOfSomeKind >-> Kind.
 147   Definition haskTypeOfSomeKindToHaskType {Γ}(htosk:HaskTypeOfSomeKind Γ) : HaskType Γ htosk :=
 148     match htosk as H return HaskType Γ H with
 149       haskTypeOfSomeKind _ ht => ht
 150       end.
 151   Coercion haskTypeOfSomeKindToHaskType : HaskTypeOfSomeKind >-> HaskType.
 152
 153 Definition HaskCoercion Γ Δ (hk:HaskCoercionKind Γ) := forall TV CV (ite:@InstantiatedTypeEnv TV Γ),
 154     @InstantiatedCoercionEnv TV CV Γ Δ -> @RawHaskCoer TV CV (hk TV ite).
 155 Inductive  LeveledHaskType (Γ:TypeEnv) κ := mkLeveledHaskType : HaskType Γ κ -> HaskLevel Γ -> LeveledHaskType Γ κ.
 156
 157 Definition FreshHaskTyVar {Γ}(κ:Kind) : HaskTyVar (κ::Γ) κ := fun TV env => ilist_head env.
 158 Definition HaskTAll {Γ}(κ:Kind)(σ:forall TV (env:@InstantiatedTypeEnv TV Γ), TV κ -> RawHaskType TV ★) : HaskType Γ ★
 159   := fun TV env => TAll κ (σ TV env).
 160 Definition HaskTApp {Γ}{κ}(σ:forall TV (env:@InstantiatedTypeEnv TV Γ), TV κ -> RawHaskType TV ★)
 161   (cv:HaskTyVar Γ κ) : HaskType Γ ★
 162   := fun TV env => σ TV env (cv TV env).
 163 Definition HaskBrak {Γ}(v:HaskTyVar Γ ECKind)(t:HaskType Γ ★) : HaskType Γ ★:=
 164   fun TV env => @TCode TV (TVar (v TV env)) (t TV env).
 165 Definition HaskTCon {Γ}(tc:TyCon) : HaskType Γ (fold_right KindArrow ★ (tyConKind tc))
 166   := fun TV ite => TCon tc.
 167 Definition HaskAppT {Γ}{κ₁}{κ₂}(t1:HaskType Γ (κ₂⇛κ₁))(t2:HaskType Γ κ₂) : HaskType Γ κ₁ :=
 168   fun TV ite => TApp (t1 TV ite) (t2 TV ite).
 169 Definition mkHaskCoercionKind {Γ}{κ}(t1:HaskType Γ κ)(t2:HaskType Γ κ) : HaskCoercionKind Γ :=
 170  fun TV ite => mkRawCoercionKind _ (t1 TV ite) (t2 TV ite).
 171
 172 Section Flatten.
 173   Context {TV:Kind -> Type }.
 174 Fixpoint flattenT {κ} (exp: RawHaskType (fun k => RawHaskType TV k) κ) : RawHaskType TV κ :=
 175      match exp with
 176     | TVar    _  x        => x
 177     | TAll     _ y        => TAll   _  (fun v => flattenT  (y (TVar v)))
 178     | TApp   _ _ x y      => TApp      (flattenT  x) (flattenT  y)
 179     | TCon       tc       => TCon      tc
 180     | TCoerc _ t1 t2 t    => TCoerc    (flattenT  t1) (flattenT  t2)   (flattenT  t)
 181     | TArrow              => TArrow
 182     | TCode      v e      => TCode     (flattenT  v) (flattenT  e)
 183     | TyFunApp  tfc kl k lt => TyFunApp tfc kl k (flattenTyFunApp _ lt)
 184     end
 185     with flattenTyFunApp (lk:list Kind)(exp:@RawHaskTypeList (fun k => RawHaskType TV k) lk) : @RawHaskTypeList TV lk :=
 186     match exp in @RawHaskTypeList _ LK return @RawHaskTypeList TV LK with
 187     | TyFunApp_nil               => TyFunApp_nil
 188     | TyFunApp_cons  κ kl t rest => TyFunApp_cons _ _ (flattenT  t) (flattenTyFunApp _ rest)
 189     end.
 190 End Flatten.
 191
 192 (* PHOAS substitution on types *)
 193 Definition substT {Γ}{κ₁}{κ₂}(exp:forall TV (env:@InstantiatedTypeEnv TV Γ), TV κ₁ -> RawHaskType TV κ₂)(v:@HaskType Γ κ₁)
 194   : @HaskType Γ κ₂ :=
 195   fun TV env =>
 196     flattenT (exp (fun k => RawHaskType TV k) (ilmap (fun κ tv => TVar tv) env) (v TV env)).
 197
 198 Notation "t @@  l" := (@mkLeveledHaskType _ _ t l) (at level 20).
 199 Notation "t @@@ l" := (mapOptionTree (fun t' => t' @@ l) t) (at level 20).
 200 Notation "'<[' a '|-' t ']>'" := (@HaskBrak _ a t).
 201
 202 Definition unlev {Γ}{κ}(lht:LeveledHaskType Γ κ) :=
 203   match lht with t@@l => t end.
 204
 205 Structure Global Γ :=
 206 { glob_wv    : WeakExprVar
 207 ; glob_kinds : list Kind
 208 ; glob_tf    : IList _ (fun κ => HaskType Γ κ) glob_kinds -> HaskType Γ ★
 209 }.
 210 Coercion glob_tf : Global >-> Funclass.
 211 Coercion glob_wv : Global >-> WeakExprVar.
 212
 213
 214
 215
 216
 217 (* yeah, things are kind of messy below this point *)
 218
 219
 220 Definition unAddKindFromInstantiatedTypeEnv {Γ:TypeEnv}{κ:Kind}{TV:Kind->Type}(ite:InstantiatedTypeEnv TV (κ::Γ))
 221   := ilist_tail ite.
 222 Definition addKindToCoercionEnv (Γ:TypeEnv)(Δ:CoercionEnv Γ)(κ:Kind) : CoercionEnv (κ::Γ) :=
 223   map (fun f => (fun TV ite => f TV (unAddKindFromInstantiatedTypeEnv ite))) Δ.
 224 Definition addKindToInstantiatedTypeEnv {Γ:TypeEnv}{TV:Kind->Type}(env:InstantiatedTypeEnv TV Γ)(κ:Kind)(tv:TV κ)
 225   : InstantiatedTypeEnv TV (κ::Γ) := tv::::env.
 226 Definition addKindToInstantiatedCoercionEnv {Γ:TypeEnv}{Δ}{TV:Kind->Type}{CV:Type}
 227   (env:InstantiatedCoercionEnv TV CV Γ Δ)(κ:Kind)(tv:TV κ)
 228   : InstantiatedCoercionEnv TV CV (κ::Γ) (addKindToCoercionEnv Γ Δ κ).
 229     simpl.
 230     unfold InstantiatedCoercionEnv.
 231     unfold addKindToCoercionEnv.
 232     simpl.
 233     rewrite <- map_preserves_length.
 234     apply env.
 235     Defined.
 236 Definition coercionEnvContainsCoercion {Γ}{Δ}{TV:Kind->Type}{CV:Type}(ite:InstantiatedTypeEnv TV Γ)
 237   (ice:InstantiatedCoercionEnv TV CV Γ Δ)(cv:CV)(ck:RawCoercionKind TV)
 238   := @vec_In _ _ (cv,ck) (vec_zip ice (vec_map (fun f => f TV ite) (list2vec Δ))).
 239 Definition addCoercionToCoercionEnv {Γ}(Δ:CoercionEnv Γ)(κ:HaskCoercionKind Γ) : CoercionEnv Γ :=
 240   κ::Δ.
 241 Definition addCoercionToInstantiatedCoercionEnv {Γ}{Δ}{κ}{TV CV}(ice:InstantiatedCoercionEnv TV CV Γ Δ)(cv:CV)
 242   : InstantiatedCoercionEnv TV CV Γ (addCoercionToCoercionEnv Δ κ).
 243   simpl.
 244   unfold addCoercionToCoercionEnv; simpl.
 245   unfold InstantiatedCoercionEnv; simpl.
 246   apply vec_cons; auto.
 247   Defined.
 248 (* the various "weak" functions turn a HaskXX-in-Γ into a HaskXX-in-(κ::Γ) *)
 249 Definition weakITE  {Γ:TypeEnv}{κ}{TV}(ite:InstantiatedTypeEnv TV (κ::Γ)) : InstantiatedTypeEnv TV Γ
 250   := ilist_tail ite.
 251 Definition weakITE' {Γ:TypeEnv}{κ}{TV}(ite:InstantiatedTypeEnv TV (app κ Γ)) : InstantiatedTypeEnv TV Γ.
 252   induction κ; auto. apply IHκ. inversion ite; subst. apply X0. Defined.
 253 Definition weakCE   {Γ:TypeEnv}{κ}(Δ:CoercionEnv Γ) : CoercionEnv (κ::Γ)
 254   := map (fun x => (fun tv ite => x tv (weakITE ite))) Δ.
 255 Definition weakV  {Γ:TypeEnv}{κ}{κv}(cv':HaskTyVar Γ κv) : HaskTyVar (κ::Γ) κv
 256   := fun TV ite => (cv' TV (weakITE ite)).
 257 Definition weakV' {Γ:TypeEnv}{κ}{κv}(cv':HaskTyVar Γ κv) : HaskTyVar (app κ Γ) κv.
 258   induction κ; auto. apply weakV; auto. Defined.
 259 Definition weakT {Γ:TypeEnv}{κ}{κ₂}(lt:HaskType Γ κ₂) : HaskType (κ::Γ) κ₂
 260   := fun TV ite => lt TV (weakITE ite).
 261 Definition weakL  {Γ}{κ}(lt:HaskLevel Γ) : HaskLevel (κ::Γ)
 262   := map weakV lt.
 263 Definition weakT' {Γ}{κ}{κ₂}(lt:HaskType Γ κ₂) : HaskType (app κ Γ) κ₂.
 264   induction κ; auto. apply weakT; auto. Defined.
 265 Definition weakT'' {Γ}{κ}{κ₂}(lt:HaskType Γ κ₂) : HaskType (app Γ κ) κ₂.
 266   unfold HaskType in *.
 267   unfold InstantiatedTypeEnv in *.
 268   intros.
 269   apply ilist_chop in X.
 270   apply lt.
 271   apply X.
 272   Defined.
 273 Definition lamer {a}{b}{c}{κ}(lt:HaskType (app (app a  b) c) κ) : HaskType (app a (app b c)) κ.
 274   rewrite <- ass_app in lt.
 275   exact lt.
 276   Defined.
 277 Definition weakL' {Γ}{κ}(lev:HaskLevel Γ) : HaskLevel (app κ Γ).
 278   induction κ; auto. apply weakL; auto. Defined.
 279 Definition weakLT {Γ}{κ}{κ₂}(lt:LeveledHaskType Γ κ₂) : LeveledHaskType (κ::Γ) κ₂
 280   := match lt with t @@ l => weakT t @@ weakL l end.
 281 Definition weakLT' {Γ}{κ}{κ₂}(lt:LeveledHaskType Γ κ₂) : LeveledHaskType (app κ Γ) κ₂
 282   := match lt with t @@ l => weakT' t @@ weakL' l end.
 283 Definition weakCE' {Γ:TypeEnv}{κ}(Δ:CoercionEnv Γ) : CoercionEnv (app κ Γ).
 284   induction κ; auto. apply weakCE; auto. Defined.
 285 Definition weakICE  {Γ:TypeEnv}{κ}{Δ:CoercionEnv Γ}{TV}{CV}(ice:InstantiatedCoercionEnv TV CV (κ::Γ) (weakCE Δ))
 286   : InstantiatedCoercionEnv TV CV Γ Δ.
 287   intros.
 288   unfold InstantiatedCoercionEnv; intros.
 289   unfold InstantiatedCoercionEnv in ice.
 290   unfold weakCE in ice.
 291   simpl in ice.
 292   rewrite <- map_preserves_length in ice.
 293   apply ice.
 294   Defined.
 295 Definition weakCK {Γ}{κ}(hck:HaskCoercionKind Γ) : HaskCoercionKind (κ::Γ).
 296   unfold HaskCoercionKind in *.
 297   intros.
 298   apply hck; clear hck.
 299   inversion X; subst; auto.
 300   Defined.
 301 Definition weakCK' {Γ}{κ}(hck:HaskCoercionKind Γ) : HaskCoercionKind (app κ Γ).
 302   induction κ; auto.
 303   apply weakCK.
 304   apply IHκ.
 305   Defined.
 306 Definition weakCK'' {Γ}{κ}(hck:list (HaskCoercionKind Γ)) : list (HaskCoercionKind (app κ Γ)) :=
 307   map weakCK' hck.
 308 Definition weakCV {Γ}{Δ}{κ}(cv':HaskCoVar Γ Δ) : HaskCoVar (κ::Γ) (weakCE Δ) :=
 309   fun TV CV ite ice => (cv' TV CV (weakITE ite) (weakICE ice)).
 310 Definition weakF {Γ:TypeEnv}{κ}{κ₂}(f:forall TV (env:@InstantiatedTypeEnv TV Γ), TV κ -> RawHaskType TV κ₂) :
 311   forall TV (env:@InstantiatedTypeEnv TV (κ::Γ)), TV κ -> RawHaskType TV κ₂
 312   := fun TV ite tv => (f TV (weakITE ite) tv).
 313
 314 Fixpoint caseType0 {Γ}(lk:list Kind) :
 315   IList _ (HaskType Γ) lk ->
 316   HaskType Γ (fold_right KindArrow ★ lk) ->
 317   HaskType Γ ★ :=
 318   match lk as LK return
 319     IList _ (HaskType Γ) LK ->
 320     HaskType Γ (fold_right KindArrow ★ LK) ->
 321     HaskType Γ ★
 322   with
 323   | nil    => fun _     ht => ht
 324   | k::lk' => fun tlist ht => caseType0 lk' (ilist_tail tlist) (fun TV env => TApp (ht TV env) (ilist_head tlist TV env))
 325   end.
 326
 327 Definition caseType {Γ}(tc:TyCon)(atypes:IList _ (HaskType Γ) (tyConKind tc)) : HaskType Γ ★ :=
 328   caseType0 (tyConKind tc) atypes (fun TV env => TCon tc).
 329
 330 (* like a GHC DataCon, but using PHOAS representation for types and coercions *)
 331 Record StrongAltCon {tc:TyCon} :=
 332 { sac_tc          := tc
 333 ; sac_altcon      :  WeakAltCon
 334 ; sac_numExTyVars :  nat
 335 ; sac_numCoerVars :  nat
 336 ; sac_numExprVars :  nat
 337 ; sac_ekinds      :  vec Kind sac_numExTyVars
 338 ; sac_kinds       := app (tyConKind tc) (vec2list sac_ekinds)
 339 ; sac_Γ           := fun Γ => app (vec2list sac_ekinds) Γ
 340 ; sac_coercions   :  forall Γ (atypes:IList _ (HaskType Γ) (tyConKind tc)), vec (HaskCoercionKind (sac_Γ Γ)) sac_numCoerVars
 341 ; sac_types       :  forall Γ (atypes:IList _ (HaskType Γ) (tyConKind tc)), vec (HaskType (sac_Γ Γ) ★) sac_numExprVars
 342 ; sac_Δ           := fun    Γ (atypes:IList _ (HaskType Γ) (tyConKind tc)) Δ => app (vec2list (sac_coercions Γ atypes)) Δ
 343 }.
 344 Coercion sac_tc     : StrongAltCon >-> TyCon.
 345 Coercion sac_altcon : StrongAltCon >-> WeakAltCon.
 346
 347
 348 Definition kindOfType {Γ}{κ}(ht:@HaskType Γ κ) : ???Kind := OK κ.
 349
 350 Axiom literal_tycons_are_of_ordinary_kind : forall lit, tyConKind (haskLiteralToTyCon lit) = nil.
 351
 352 Definition literalType (lit:HaskLiteral){Γ} : HaskType Γ ★.
 353   set (fun TV (ite:InstantiatedTypeEnv TV Γ) => @TCon TV (haskLiteralToTyCon lit)) as z.
 354   unfold tyConKind' in z.
 355   rewrite literal_tycons_are_of_ordinary_kind in z.
 356   unfold HaskType.
 357   apply z.
 358   Defined.
 359
 360 Notation "a ∼∼∼ b" := (@mkHaskCoercionKind _ _ a b) (at level 18).
 361
 362 Fixpoint update_ξ
 363   `{EQD_VV:EqDecidable VV}{Γ}
 364    (ξ:VV -> LeveledHaskType Γ ★)
 365    (lev:HaskLevel Γ)
 366    (vt:list (VV * HaskType Γ ★))
 367    : VV -> LeveledHaskType Γ ★ :=
 368   match vt with
 369     | nil => ξ
 370     | (v,τ)::tl => fun v' => if eqd_dec v v' then τ @@ lev else (update_ξ ξ lev tl) v'
 371   end.
 372
 373 Lemma update_ξ_lemma0 `{EQD_VV:EqDecidable VV} : forall Γ ξ (lev:HaskLevel Γ)(varstypes:list (VV*_)) v,
 374   not (In v (map (@fst _ _) varstypes)) ->
 375   (update_ξ ξ lev varstypes) v = ξ v.
 376   intros.
 377   induction varstypes.
 378   reflexivity.
 379   simpl.
 380   destruct a.
 381   destruct (eqd_dec v0 v).
 382   subst.
 383   simpl in  H.
 384   assert False.
 385   apply H.
 386   auto.
 387   inversion H0.
 388   apply IHvarstypes.
 389   unfold not; intros.
 390   apply H.
 391   simpl.
 392   auto.
 393   Defined.
 394
 395
 396 (***************************************************************************************************)
 397 (* Well-Formedness of Types and Coercions                                                          *)
 398 (* also represents production "S_n:κ" of Γ because these can only wind up in Γ via rule (Type) *)
 399 Inductive TypeFunctionDecl (tfc:TyCon)(vk:vec Kind tfc) : Type :=
 400   mkTFD : Kind -> TypeFunctionDecl tfc vk.
 401
 402 (*
 403 Section WFCo.
 404   Context {TV:Kind->Type}.
 405   Context {CV:Type}.
 406
 407   (* local notations *)
 408   Notation "ienv '⊢ᴛy' σ : κ"              := (@WellKinded_RawHaskType TV _ ienv σ κ).
 409   Notation "env  ∋  cv : t1 ∼ t2 : Γ : t"  := (@coercionEnvContainsCoercion Γ _ TV CV t env cv (@mkRawCoercionKind _ t1 t2))
 410                  (at level 20, t1 at level 99, t2 at level 99, t at level 99).
 411   Reserved Notation "ice '⊢ᴄᴏ' γ : a '∼' b : Δ : Γ : ite"
 412         (at level 20, γ at level 99, b at level 99, Δ at level 99, ite at level 99, Γ at level 99).
 413
 414   (* Figure 8, lower half *)
 415   Inductive WFCoercion:forall Γ (Δ:CoercionEnv Γ),
 416     @InstantiatedTypeEnv TV Γ ->
 417     @InstantiatedCoercionEnv TV CV Γ Δ ->
 418     @RawHaskCoer TV CV -> @RawCoercionKind TV -> Prop :=
 419   | CoTVar':∀ Γ Δ t e c σ τ,
 420     (@coercionEnvContainsCoercion Γ _ TV CV t e c (@mkRawCoercionKind _ σ τ)) -> e⊢ᴄᴏ CoVar c : σ ∼ τ  : Δ : Γ : t
 421   | CoRefl :∀ Γ Δ t e   τ κ,                                         t ⊢ᴛy τ :κ    -> e⊢ᴄᴏ CoType τ    :         τ ∼ τ  : Δ :Γ: t
 422   | Sym    :∀ Γ Δ t e γ σ τ,                            (e⊢ᴄᴏ γ : σ ∼ τ : Δ : Γ:t)  -> e⊢ᴄᴏ CoSym  γ    :         τ ∼ σ  : Δ :Γ: t
 423   | Trans  :∀ Γ Δ t e γ₁ γ₂ σ₁ σ₂ σ₃,(e⊢ᴄᴏ γ₁:σ₁∼σ₂:Δ:Γ:t) -> (e⊢ᴄᴏ γ₂:σ₂∼σ₃:Δ:Γ:t) -> e⊢ᴄᴏ CoComp γ₁ γ₂:        σ₁ ∼ σ₃ : Δ :Γ: t
 424   | Left   :∀ Γ Δ t e γ σ₁ σ₂ τ₁ τ₂,(e⊢ᴄᴏ γ : TApp σ₁ σ₂ ∼ TApp τ₁ τ₂ :Δ:Γ:t    )  -> e⊢ᴄᴏ CoLeft  γ   :        σ₁ ∼ τ₁ : Δ :Γ: t
 425   | Right  :∀ Γ Δ t e γ σ₁ σ₂ τ₁ τ₂,(e⊢ᴄᴏ γ : TApp σ₁ σ₂ ∼ TApp τ₁ τ₂ :Δ:Γ:t   )   -> e⊢ᴄᴏ CoRight γ   :        σ₂ ∼ τ₂ : Δ :Γ: t
 426   (*
 427   | SComp  :∀ Γ Δ t e γ n S σ τ κ,
 428             ListWFCo Γ Δ t e γ σ τ -> t ⊢ᴛy TyFunApp(n:=n) S σ : κ  -> e⊢ᴄᴏ CoTFApp S γ : TyFunApp S σ∼TyFunApp S τ : Δ : Γ : t
 429   | CoAx   :∀ Γ Δ t e n C κ γ, forall (σ₁:vec TV n) (σ₂:vec TV n), forall (ax:@AxiomDecl n C κ TV),
 430     ListWFCo                              Γ Δ t e γ (map TVar (vec2list σ₁)) (map TVar (vec2list σ₂)) ->
 431     ListWellKinded_RawHaskType TV Γ t   (map TVar (vec2list σ₁))            (vec2list κ)  ->
 432     ListWellKinded_RawHaskType TV Γ t   (map TVar (vec2list σ₂))            (vec2list κ)  ->
 433     e⊢ᴄᴏ CoCFApp C γ : axd_σ _ _ _ ax σ₁ ∼ axd_τ _ _ _ ax σ₂ : Δ : Γ : t
 434   *)
 435   | WFCoAll  : forall Γ Δ κ (t:InstantiatedTypeEnv TV Γ) (e:InstantiatedCoercionEnv TV CV (κ::Γ) (weakCE Δ)) γ σ τ    ,
 436       (∀ a,           e ⊢ᴄᴏ (        γ a) : (       σ a) ∼ (       τ a) : _ : _ : (t + a : κ))
 437       ->    weakICE e ⊢ᴄᴏ (CoAll κ γ  ) : (TAll κ σ  ) ∼ (TAll κ τ  ) : Δ : Γ :  t
 438   | Comp   :forall Γ Δ t e γ₁ γ₂ σ₁ σ₂ τ₁ τ₂ κ,
 439             (t ⊢ᴛy TApp σ₁ σ₂:κ)->
 440             (e⊢ᴄᴏ γ₁:σ₁∼τ₁:Δ:Γ:t)->
 441             (e⊢ᴄᴏ γ₂:σ₂∼τ₂:Δ:Γ:t) ->
 442             e⊢ᴄᴏ (CoApp γ₁ γ₂) : (TApp σ₁ σ₂) ∼ (TApp τ₁ τ₂) : Δ:Γ:t
 443   | CoInst :forall Γ Δ t e σ τ κ γ (v:∀ TV, InstantiatedTypeEnv TV Γ -> RawHaskType TV),
 444           t ⊢ᴛy v TV t : κ  ->
 445             (e⊢ᴄᴏ γ:HaskTAll κ σ _ t ∼ HaskTAll κ τ _ t:Δ:Γ:t) ->
 446             e⊢ᴄᴏ CoAppT γ (v TV t) : substT σ v TV t ∼substT τ v TV t : Δ : Γ : t
 447   with ListWFCo  : forall Γ (Δ:CoercionEnv Γ),
 448      @InstantiatedTypeEnv TV Γ ->
 449      InstantiatedCoercionEnv TV CV Γ Δ ->
 450      list (RawHaskCoer TV CV) -> list (RawHaskType TV) -> list (RawHaskType TV) -> Prop :=
 451   | LWFCo_nil  : ∀ Γ Δ t e ,                                                            ListWFCo Γ Δ t e nil     nil     nil
 452   | LWFCo_cons : ∀ Γ Δ t e a b c la lb lc, (e⊢ᴄᴏ a : b∼c : Δ : Γ : t )->
 453     ListWFCo Γ Δ t e la lb lc -> ListWFCo Γ Δ t e (a::la) (b::lb) (c::lc)
 454   where "ice '⊢ᴄᴏ' γ : a '∼' b : Δ : Γ : ite" := (@WFCoercion Γ Δ ite ice γ (@mkRawCoercionKind _ a b)).
 455 End WFCo.
 456
 457 Definition WFCCo (Γ:TypeEnv)(Δ:CoercionEnv Γ)(γ:HaskCoercion Γ Δ)(a b:HaskType Γ) :=
 458   forall {TV CV:Type}(env:@InstantiatedTypeEnv TV Γ)(cenv:InstantiatedCoercionEnv TV CV Γ Δ),
 459     @WFCoercion _ _ Γ Δ env cenv (γ TV CV env cenv) (@mkRawCoercionKind _ (a TV env) (b TV env)).
 460     Notation "Δ '⊢ᴄᴏ' γ : a '∼' b" := (@WFCCo _ Δ γ a b).
 461 *)
 462
 463
 464
 465
 466 (* Decidable equality on PHOAS types *)
 467 Fixpoint compareT (n:nat){κ₁}(t1:@RawHaskType (fun _ => nat) κ₁){κ₂}(t2:@RawHaskType (fun _ => nat) κ₂) : bool :=
 468 match t1 with
 469 | TVar    _  x     => match t2 with TVar _ x' => if eqd_dec x x' then true else false | _ => false end
 470 | TAll     _ y     => match t2 with TAll _ y' => compareT (S n) (y n) (y' n)          | _ => false end
 471 | TApp   _ _ x y   => match t2 with TApp _ _ x' y' => if compareT n x x' then compareT n y y' else false | _ => false end
 472 | TCon       tc    => match t2 with TCon tc' => if eqd_dec tc tc' then true else false | _ => false end
 473 | TArrow           => match t2 with TArrow => true | _ => false end
 474 | TCode      ec t  => match t2 with TCode ec' t' => if compareT n ec ec' then compareT n t t' else false | _ => false end
 475 | TCoerc _ t1 t2 t => match t2 with TCoerc _ t1' t2' t' => compareT n t1 t1' && compareT n t2 t2' && compareT n t t' | _ =>false end
 476 | TyFunApp tfc kl k lt  => match t2 with TyFunApp tfc' kl' k' lt' => eqd_dec tfc tfc' && compareTL n lt lt' | _ => false end
 477 end
 478 with compareTL (n:nat){κ₁}(t1:@RawHaskTypeList (fun _ => nat) κ₁){κ₂}(t2:@RawHaskTypeList (fun _ => nat) κ₂) : bool :=
 479 match t1 with
 480 | TyFunApp_nil              => match t2 with TyFunApp_nil => true | _ => false end
 481 | TyFunApp_cons κ kl t r => match t2 with | TyFunApp_cons κ' kl' t' r' => compareT n t t' && compareTL n r r' | _ => false end
 482 end.
 483
 484 Fixpoint count' (lk:list Kind)(n:nat) : IList _ (fun _ => nat) lk :=
 485 match lk as LK return IList _ _ LK with
 486   | nil    => INil
 487   | h::t   => n::::(count' t (S n))
 488 end.
 489
 490 Definition compareHT Γ κ (ht1 ht2:HaskType Γ κ) :=
 491   compareT (length Γ) (ht1 (fun _ => nat) (count' Γ O)) (ht2 (fun _ => nat) (count' Γ O)).
 492
 493 (* The PHOAS axioms
 494  *
 495  * This is not provable in Coq's logic because the Coq function space
 496  * is "too big" - although its only definable inhabitants are Coq
 497  * functions, it is not provable in Coq that all function space
 498  * inhabitants are definable (i.e. there are no "exotic" inhabitants).
 499  * This is actually an important feature of Coq: it lets us reason
 500  * about properties of non-computable (non-recursive) functions since
 501  * any property proven to hold for the entire function space will hold
 502  * even for those functions.  However when representing binding
 503  * structure using functions we would actually prefer the smaller
 504  * function-space of *definable* functions only.  These two axioms
 505  * assert that. *)
 506 Axiom compareHT_decides : forall Γ κ (ht1 ht2:HaskType Γ κ),
 507   if compareHT Γ κ ht1 ht2
 508   then ht1=ht2
 509   else ht1≠ht2.
 510 Axiom compareVars : forall Γ κ (htv1 htv2:HaskTyVar Γ κ),
 511   if compareHT _ _ (haskTyVarToType htv1) (haskTyVarToType htv2)
 512   then htv1=htv2
 513   else htv1≠htv2.
 514
 515 (* using the axioms, we can now create an EqDecidable instance for HaskType, HaskTyVar, and HaskLevel *)
 516 Instance haskTypeEqDecidable Γ κ : EqDecidable (HaskType Γ κ).
 517   apply Build_EqDecidable.
 518   intros.
 519   set (compareHT_decides _ _ v1 v2) as z.
 520   set (compareHT Γ κ v1 v2) as q.
 521   destruct q as [ ] _eqn; unfold q in *; rewrite Heqb in *.
 522     left; auto.
 523     right; auto.
 524     Defined.
 525
 526 Instance haskTyVarEqDecidable Γ κ : EqDecidable (HaskTyVar Γ κ).
 527   apply Build_EqDecidable.
 528   intros.
 529   set (compareVars _ _ v1 v2) as z.
 530   set (compareHT Γ κ (haskTyVarToType v1) (haskTyVarToType v2)) as q.
 531   destruct q as [ ] _eqn; unfold q in *; rewrite Heqb in *.
 532     left; auto.
 533     right; auto.
 534     Defined.
 535
 536 Instance haskLevelEqDecidable Γ : EqDecidable (HaskLevel Γ).
 537   apply Build_EqDecidable.
 538   intros.
 539   unfold HaskLevel in *.
 540   apply (eqd_dec v1 v2).
 541   Defined.
 542
 543
 544
 545
 546
 547 (* ToString instance for PHOAS types *)
 548 Fixpoint typeToString' (needparens:bool)(n:nat){κ}(t:RawHaskType (fun _ => nat) κ) {struct t} : string :=
 549     match t with
 550     | TVar    _ v          => "tv" +++ toString v
 551     | TCon    tc           => toString tc
 552     | TCoerc _ t1 t2   t   => "("+++typeToString' false n t1+++"~"
 553                                   +++typeToString' false n t2+++")=>"
 554                                   +++typeToString' needparens n t
 555     | TApp  _ _  t1 t2     =>
 556       match t1 with
 557         | TApp _ _ TArrow t1 =>
 558                      if needparens
 559                      then "("+++(typeToString' true n t1)+++"->"+++(typeToString' true n t2)+++")"
 560                      else (typeToString' true n t1)+++"->"+++(typeToString' true n t2)
 561         | _ =>
 562                      if needparens
 563                      then "("+++(typeToString' true n t1)+++" "+++(typeToString' false n t2)+++")"
 564                      else (typeToString' true n t1)+++" "+++(typeToString' false n t2)
 565       end
 566     | TArrow => "(->)"
 567     | TAll   k f           => let alpha := "tv"+++ toString n
 568                               in "(forall "+++ alpha +++ ":"+++ toString k +++")"+++
 569                                    typeToString' false (S n) (f n)
 570     | TCode  ec t          => "<["+++(typeToString' true n t)+++"]>@"+++(typeToString' false n ec)
 571     | TyFunApp   tfc kl k lt    => toString tfc+++ "_" +++ toString n+++" ["+++
 572       (fold_left (fun x y => " \  "+++x+++y) (typeList2string false n lt) "")+++"]"
 573   end
 574   with typeList2string (needparens:bool)(n:nat){κ}(t:RawHaskTypeList κ) {struct t} : list string :=
 575   match t with
 576   | TyFunApp_nil                 => nil
 577   | TyFunApp_cons  κ kl rhk rhkl => (typeToString' needparens n rhk)::(typeList2string needparens n rhkl)
 578   end.
 579
 580 Definition typeToString {Γ}{κ}(ht:HaskType Γ κ) : string :=
 581   typeToString' false (length Γ) (ht (fun _ => nat) (count' Γ O)).
 582
 583 Instance TypeToStringInstance {Γ} {κ} : ToString (HaskType Γ κ) :=
 584   { toString := typeToString }.