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