src/HaskWeakToStrong.v

   1 (*********************************************************************************************************************************)
   2 (* HaskWeakToStrong: convert HaskWeak to HaskStrong                                                                              *)
   3 (*********************************************************************************************************************************)
   4
   5 Generalizable All Variables.
   6 Require Import Preamble.
   7 Require Import General.
   8 Require Import NaturalDeduction.
   9 Require Import Coq.Strings.String.
  10 Require Import Coq.Lists.List.
  11 Require Import Coq.Init.Specif.
  12 Require Import HaskKinds.
  13 Require Import HaskLiterals.
  14 Require Import HaskTyCons.
  15 Require Import HaskWeakTypes.
  16 Require Import HaskWeakVars.
  17 Require Import HaskWeak.
  18 Require Import HaskWeakToCore.
  19 Require Import HaskStrongTypes.
  20 Require Import HaskStrong.
  21 Require Import HaskCoreVars.
  22 Require Import HaskCoreTypes.
  23
  24 Open Scope string_scope.
  25 Definition TyVarResolver Γ   := forall wt:WeakTypeVar, ???(HaskTyVar Γ wt).
  26 Definition CoVarResolver Γ Δ := forall wt:WeakCoerVar, ???(HaskCoVar Γ Δ).
  27
  28 Definition upφ {Γ}(tv:WeakTypeVar)(φ:TyVarResolver Γ) : TyVarResolver ((tv:Kind)::Γ).
  29   unfold TyVarResolver.
  30   refine (fun tv' =>
  31     if eqd_dec tv tv'
  32     then let fresh := @FreshHaskTyVar Γ tv in OK _
  33     else φ tv' >>= fun tv'' => OK (fun TV ite => tv'' TV (weakITE ite))).
  34   rewrite <- _H; apply fresh.
  35   Defined.
  36
  37 Definition upφ' {Γ}(tvs:list WeakTypeVar)(φ:TyVarResolver Γ)
  38   : (TyVarResolver (app (map (fun tv:WeakTypeVar => tv:Kind) tvs) Γ)).
  39   induction tvs.
  40   apply φ.
  41   simpl.
  42   apply upφ.
  43   apply IHtvs.
  44   Defined.
  45
  46 Definition substPhi {Γ:TypeEnv}(κ κ':Kind)(θ:HaskType Γ κ) : HaskType (κ::Γ) κ' -> HaskType Γ κ'.
  47   intro ht.
  48   refine (substT _ θ).
  49   clear θ.
  50   unfold HaskType in ht.
  51   intros.
  52   apply ht.
  53   apply ICons; [ idtac | apply env ].
  54   apply X.
  55   Defined.
  56
  57 Definition substφ {Γ:TypeEnv}(lk:list Kind)(θ:IList _ (fun κ => HaskType Γ κ) lk){κ} : HaskType (app lk Γ) κ -> HaskType Γ κ.
  58   induction lk.
  59   intro q; apply q.
  60   simpl.
  61   intro q.
  62   apply IHlk.
  63   inversion θ; subst; auto.
  64   inversion θ; subst.
  65   eapply substPhi.
  66   eapply weakT'.
  67   apply X.
  68   apply q.
  69   Defined.
  70
  71 (* this is a StrongAltCon plus some stuff we know about StrongAltCons which we've built ourselves *)
  72 Record StrongAltConPlusJunk {tc:TyCon} :=
  73 { sacpj_sac : @StrongAltCon tc
  74 ; sacpj_φ   : forall Γ          (φ:TyVarResolver Γ  ),  (TyVarResolver (sac_Γ sacpj_sac Γ))
  75 ; sacpj_ψ   : forall Γ Δ atypes (ψ:CoVarResolver Γ Δ), CoVarResolver _ (sac_Δ sacpj_sac Γ atypes (weakCK'' Δ))
  76 }.
  77 Implicit Arguments StrongAltConPlusJunk [ ].
  78 Coercion sacpj_sac : StrongAltConPlusJunk >-> StrongAltCon.
  79
  80 (* yes, I know, this is really clumsy *)
  81 Variable emptyφ : TyVarResolver nil.
  82   Extract Inlined Constant emptyφ => "(\x -> Prelude.error ""encountered unbound tyvar!"")".
  83
  84 Definition mkPhi (lv:list WeakTypeVar)
  85   : (TyVarResolver (map (fun x:WeakTypeVar => x:Kind) lv)).
  86   set (upφ'(Γ:=nil) lv emptyφ) as φ'.
  87   rewrite <- app_nil_end in φ'.
  88   apply φ'.
  89   Defined.
  90
  91 Definition dataConExKinds dc := vec_map (fun x:WeakTypeVar => (x:Kind)) (list2vec (dataConExTyVars dc)).
  92 Definition tyConKinds     tc := vec_map (fun x:WeakTypeVar => (x:Kind)) (list2vec (tyConTyVars tc)).
  93
  94 Definition fixkind {κ}(tv:WeakTypeVar) := weakTypeVar tv κ.
  95 Notation " ` x " := (@fixkind _ x) (at level 100).
  96
  97 Ltac matchThings T1 T2 S :=
  98   destruct (eqd_dec T1 T2) as [matchTypeVars_pf|];
  99    [ idtac | apply (Error (S +++ toString T1 +++ " " +++ toString T2)) ].
 100
 101 Definition mkTAll' {κ}{Γ} : HaskType (κ :: Γ) ★ -> (forall TV (ite:InstantiatedTypeEnv TV Γ), TV κ -> RawHaskType TV ★).
 102   intros.
 103   unfold InstantiatedTypeEnv in ite.
 104   apply X.
 105   apply (X0::::ite).
 106   Defined.
 107
 108 Definition mkTAll {κ}{Γ} : HaskType (κ :: Γ) ★ -> HaskType Γ ★.
 109   intro.
 110   unfold HaskType.
 111   intros.
 112   apply (TAll κ).
 113   eapply mkTAll'.
 114   apply X.
 115   apply X0.
 116   Defined.
 117
 118 Definition weakTypeToType : forall {Γ:TypeEnv}(φ:TyVarResolver Γ)(t:WeakType), ???(HaskTypeOfSomeKind Γ).
 119   refine (fix weakTypeToType {Γ:TypeEnv}(φ:TyVarResolver Γ)(t:WeakType) {struct t} : ???(HaskTypeOfSomeKind Γ) :=
 120   addErrorMessage ("weakTypeToType " +++ toString t)
 121   match t with
 122     | WFunTyCon         => let case_WFunTyCon := tt in OK (haskTypeOfSomeKind (fun TV ite => TArrow))
 123     | WTyCon      tc    => let case_WTyCon := tt    in _
 124     | WClassP   c lt    => let case_WClassP := tt   in Error "weakTypeToType: WClassP not implemented"
 125     | WIParam _ ty      => let case_WIParam := tt   in Error "weakTypeToType: WIParam not implemented"
 126     | WAppTy  t1 t2     => let case_WAppTy := tt    in weakTypeToType _ φ t1 >>= fun t1' => weakTypeToType _ φ t2 >>= fun t2' => _
 127     | WTyVarTy  v       => let case_WTyVarTy := tt  in φ v >>= fun v' => _
 128     | WForAllTy wtv t   => let case_WForAllTy := tt in weakTypeToType _ (upφ wtv φ) t >>= fun t => _
 129     | WCodeTy ec tbody  => let case_WCodeTy := tt   in weakTypeToType _ φ tbody
 130                                  >>= fun tbody' => φ (@fixkind ECKind ec) >>= fun ec' => _
 131     | WCoFunTy t1 t2 t3 => let case_WCoFunTy := tt  in
 132       weakTypeToType _ φ t1 >>= fun t1' =>
 133       weakTypeToType _ φ t2 >>= fun t2' =>
 134       weakTypeToType _ φ t3 >>= fun t3' => _
 135     | WTyFunApp   tc lt =>
 136       ((fix weakTypeListToTypeList (lk:list Kind) (lt:list WeakType)
 137         { struct lt } : ???(forall TV (ite:InstantiatedTypeEnv TV Γ), @RawHaskTypeList TV lk) :=
 138         match lt with
 139           | nil    => match lk as LK return ???(forall TV (ite:InstantiatedTypeEnv TV Γ), @RawHaskTypeList TV LK) with
 140                         | nil => OK (fun TV _ => TyFunApp_nil)
 141                         | _   => Error "WTyFunApp not applied to enough types"
 142                       end
 143           | tx::lt' => weakTypeToType Γ φ tx >>= fun t' =>
 144                         match lk as LK return ???(forall TV (ite:InstantiatedTypeEnv TV Γ), @RawHaskTypeList TV LK) with
 145                           | nil    => Error ("WTyFunApp applied to too many types"(* +++ eol +++
 146                                              "  tyCon= "           +++ toString tc +++ eol +++
 147                                              "  tyConKindArgs= "   +++ toString (fst (tyFunKind tc)) +++ eol +++
 148                                              "  tyConKindResult= " +++ toString (snd (tyFunKind tc)) +++ eol +++
 149                                              "  types= "           +++ toString lt +++ eol*))
 150                           | k::lk' => weakTypeListToTypeList lk' lt' >>= fun rhtl' =>
 151                                         let case_weakTypeListToTypeList := tt in _
 152                         end
 153         end
 154       ) (fst (tyFunKind tc)) lt) >>= fun lt' => let case_WTyFunApp := tt in  _
 155   end ); clear weakTypeToType.
 156   apply ConcatenableString.
 157
 158   destruct case_WTyVarTy.
 159     apply (addErrorMessage "case_WTyVarTy").
 160     apply OK.
 161     exact (haskTypeOfSomeKind (fun TV env => TVar (v' TV env))).
 162
 163   destruct case_WAppTy.
 164     apply (addErrorMessage "case_WAppTy").
 165     destruct t1' as  [k1' t1'].
 166     destruct t2' as [k2' t2'].
 167     set ("tried to apply type "+++toString t1'+++" of kind "+++toString k1'+++" to type "+++
 168       toString t2'+++" of kind "+++toString k2') as err.
 169     destruct k1';
 170       try (matchThings k1'1 k2' "Kind mismatch in WAppTy: ";
 171         subst; apply OK; apply (haskTypeOfSomeKind (fun TV env => TApp (t1' TV env) (t2' TV env))));
 172       apply (Error ("Kind mismatch in WAppTy: "+++err)).
 173
 174   destruct case_weakTypeListToTypeList.
 175     apply (addErrorMessage "case_weakTypeListToTypeList").
 176     destruct t' as [ k' t' ].
 177     matchThings k k' "Kind mismatch in weakTypeListToTypeList".
 178     subst.
 179     apply (OK (fun TV ite => TyFunApp_cons _ _ (t' TV ite) (rhtl' TV ite))).
 180
 181   destruct case_WTyFunApp.
 182     apply (addErrorMessage "case_WTyFunApp").
 183     apply OK.
 184     eapply haskTypeOfSomeKind.
 185     unfold HaskType; intros.
 186     apply (TyFunApp tc (fst (tyFunKind tc)) (snd (tyFunKind tc))).
 187     apply lt'.
 188     apply X.
 189
 190   destruct case_WTyCon.
 191     apply (addErrorMessage "case_WTyCon").
 192     apply OK.
 193     eapply haskTypeOfSomeKind.
 194     unfold HaskType; intros.
 195     apply (TCon tc).
 196
 197   destruct case_WCodeTy.
 198     apply (addErrorMessage "case_WCodeTy").
 199     destruct tbody'.
 200     matchThings κ ★ "Kind mismatch in WCodeTy: ".
 201     apply OK.
 202     eapply haskTypeOfSomeKind.
 203     unfold HaskType; intros.
 204     apply TCode.
 205     apply (TVar (ec' TV X)).
 206     subst.
 207     apply h.
 208     apply X.
 209
 210   destruct case_WCoFunTy.
 211     apply (addErrorMessage "case_WCoFunTy").
 212     destruct t1' as [ k1' t1' ].
 213     destruct t2' as [ k2' t2' ].
 214     destruct t3' as [ k3' t3' ].
 215     matchThings k1' k2' "Kind mismatch in arguments of WCoFunTy".
 216     subst.
 217     matchThings k3' ★ "Kind mismatch in result of WCoFunTy".
 218     subst.
 219     apply OK.
 220     apply (haskTypeOfSomeKind (t1' ∼∼ t2' ⇒ t3')).
 221
 222   destruct case_WForAllTy.
 223     apply (addErrorMessage "case_WForAllTy").
 224     destruct t1.
 225     matchThings ★  κ "Kind mismatch in WForAllTy: ".
 226     subst.
 227     apply OK.
 228     apply (@haskTypeOfSomeKind _ ★).
 229     apply (@mkTAll wtv).
 230     apply h.
 231     Defined.
 232
 233 (* information about a datacon/literal/default which is common to all instances of a branch with that tag *)
 234 Section StrongAltCon.
 235   Context (tc : TyCon)(dc:DataCon tc).
 236
 237 Definition weakTypeToType' {Γ} : IList Kind (HaskType Γ) (vec2list (tyConKinds tc))
 238  -> WeakType → ???(HaskType (app (vec2list (dataConExKinds dc)) Γ) ★).
 239   intro avars.
 240   intro ct.
 241   apply (addErrorMessage "weakTypeToType'").
 242   set (ilmap (@weakT' _ (vec2list (dataConExKinds dc))) avars) as avars'.
 243   set (@substφ _ _ avars') as q.
 244   set (upφ' (tyConTyVars tc)  (mkPhi (dataConExTyVars dc))) as φ'.
 245   set (@weakTypeToType _ φ' ct) as t.
 246   destruct t as [|t]; try apply (Error error_message).
 247   destruct t as [tk t].
 248   matchThings tk ★ "weakTypeToType'".
 249   subst.
 250   apply OK.
 251   set (@weakT'' _ Γ _ t) as t'.
 252   set (@lamer _ _ _ _ t') as t''.
 253   fold (tyConKinds tc) in t''.
 254   fold (dataConExKinds dc) in t''.
 255   apply q.
 256   clear q.
 257   unfold tyConKinds.
 258   unfold dataConExKinds.
 259   rewrite <- vec2list_map_list2vec.
 260   rewrite <- vec2list_map_list2vec.
 261   rewrite vec2list_list2vec.
 262   rewrite vec2list_list2vec.
 263   apply t''.
 264   Defined.
 265
 266 Definition mkStrongAltCon : @StrongAltCon tc.
 267   refine
 268    {| sac_altcon      := WeakDataAlt dc
 269     ; sac_numCoerVars := length (dataConCoerKinds dc)
 270     ; sac_numExprVars := length (dataConFieldTypes dc)
 271     ; sac_ekinds      := dataConExKinds dc
 272     ; sac_coercions   := fun Γ avars => let case_sac_coercions := tt in _
 273     ; sac_types       := fun Γ avars => let case_sac_types := tt in _
 274     |}.
 275
 276   destruct case_sac_coercions.
 277     refine (vec_map _ (list2vec (dataConCoerKinds dc))).
 278     intro.
 279     destruct X.
 280     unfold tyConKind in avars.
 281     set (@weakTypeToType' Γ) as q.
 282     unfold tyConKinds in q.
 283     rewrite <- vec2list_map_list2vec in q.
 284     rewrite vec2list_list2vec in q.
 285     apply (
 286       match
 287         q avars w >>= fun t1 =>
 288         q avars w0 >>= fun t2 =>
 289           OK (mkHaskCoercionKind t1 t2)
 290       with
 291         | Error s => Prelude_error s
 292         | OK y => y
 293       end).
 294
 295   destruct case_sac_types.
 296     refine (vec_map _ (list2vec (dataConFieldTypes dc))).
 297     intro X.
 298     unfold tyConKind in avars.
 299     set (@weakTypeToType' Γ) as q.
 300     unfold tyConKinds in q.
 301     rewrite <- vec2list_map_list2vec in q.
 302     rewrite vec2list_list2vec in q.
 303     set (q avars X) as y.
 304     apply (match y with
 305              | Error s =>Prelude_error s
 306              | OK y' => y'
 307            end).
 308     Defined.
 309
 310
 311 Lemma weakCV' : forall {Γ}{Δ} Γ',
 312    HaskCoVar Γ Δ
 313    -> HaskCoVar (app Γ' Γ) (weakCK'' Δ).
 314   intros.
 315   unfold HaskCoVar in *.
 316   intros; apply (X TV CV).
 317   apply ilist_chop' in env; auto.
 318   unfold InstantiatedCoercionEnv in *.
 319   unfold weakCK'' in cenv.
 320   destruct Γ'.
 321   rewrite <- map_preserves_length in cenv.
 322   apply cenv.
 323   rewrite <- map_preserves_length in cenv.
 324   apply cenv.
 325   Defined.
 326
 327 Definition mkStrongAltConPlusJunk : StrongAltConPlusJunk tc.
 328     refine
 329      {| sacpj_sac     := mkStrongAltCon
 330       ; sacpj_φ       := fun Γ φ => (fun htv => φ htv >>= fun htv' => OK (weakV' htv'))
 331       ; sacpj_ψ       :=
 332       fun Γ Δ avars ψ => (fun htv => ψ htv >>= fun htv' => OK (_ (weakCV' (vec2list (sac_ekinds mkStrongAltCon)) htv')))
 333       |}.
 334     intro.
 335     unfold sac_Γ.
 336     unfold HaskCoVar in *.
 337     intros.
 338     apply (x TV CV env).
 339     simpl in cenv.
 340     unfold sac_Δ in *.
 341     unfold InstantiatedCoercionEnv in *.
 342     apply vec_chop' in cenv.
 343     apply cenv.
 344     Defined.
 345
 346   Lemma weakCK'_nil_inert : forall Γ Δ, (@weakCK'' Γ (@nil Kind)) Δ = Δ.
 347     intros.
 348     induction Δ.
 349     reflexivity.
 350     simpl.
 351     rewrite IHΔ.
 352     reflexivity.
 353     Qed.
 354
 355 End StrongAltCon.
 356
 357 Definition mkStrongAltConPlusJunk' (tc : TyCon)(alt:WeakAltCon) : ???(@StrongAltConPlusJunk tc).
 358   destruct alt.
 359   set (c:DataCon _) as dc.
 360   set ((dataConTyCon c):TyCon) as tc' in *.
 361   set (eqd_dec tc tc') as eqpf; destruct eqpf;
 362     [ idtac
 363       | apply (Error ("in a case of tycon "+++toString tc+++", found a branch with datacon "+++toString (dc:CoreDataCon))) ]; subst.
 364   apply OK.
 365   eapply mkStrongAltConPlusJunk.
 366   simpl in *.
 367   apply dc.
 368
 369   apply OK; refine {| sacpj_sac := {|
 370                      sac_ekinds  := vec_nil ; sac_coercions := fun _ _ => vec_nil ; sac_types := fun _ _ => vec_nil
 371                     ; sac_altcon := WeakLitAlt h
 372                     |} |}.
 373             intro; intro φ; apply φ.
 374             intro; intro; intro; intro ψ. simpl. unfold sac_Γ; simpl. unfold sac_Δ; simpl.
 375             rewrite weakCK'_nil_inert. apply ψ.
 376   apply OK; refine {| sacpj_sac := {|
 377                      sac_ekinds := vec_nil ; sac_coercions := fun _ _ => vec_nil ; sac_types := fun _ _ => vec_nil
 378                       ; sac_altcon := WeakDEFAULT |} |}.
 379             intro; intro φ; apply φ.
 380             intro; intro; intro; intro ψ. simpl. unfold sac_Γ; simpl. unfold sac_Δ; simpl.
 381             rewrite weakCK'_nil_inert. apply ψ.
 382 Defined.
 383
 384 Definition weakExprVarToWeakType : WeakExprVar -> WeakType :=
 385   fun wev => match wev with weakExprVar _ t => t end.
 386   Coercion weakExprVarToWeakType : WeakExprVar >-> WeakType.
 387
 388 Variable weakCoercionToHaskCoercion : forall Γ Δ κ, WeakCoercion -> HaskCoercion Γ Δ κ.
 389
 390 Definition weakψ {Γ}{Δ:CoercionEnv Γ} {κ}(ψ:WeakCoerVar -> ???(HaskCoVar Γ Δ)) :
 391   WeakCoerVar -> ???(HaskCoVar Γ (κ::Δ)).
 392   intros.
 393   refine (ψ X >>= _).
 394   unfold HaskCoVar.
 395   intros.
 396   apply OK.
 397   intros.
 398   inversion cenv; auto.
 399   Defined.
 400
 401 (* attempt to "cast" an expression by simply checking if it already had the desired type, and failing otherwise *)
 402 Definition castExpr (we:WeakExpr)(err_msg:string) {Γ} {Δ} {ξ} {τ} τ' (e:@Expr _ CoreVarEqDecidable Γ Δ ξ τ)
 403   : ???(@Expr _ CoreVarEqDecidable Γ Δ ξ τ').
 404   apply (addErrorMessage ("castExpr " +++ err_msg)).
 405   intros.
 406   destruct τ  as [τ  l].
 407   destruct τ' as [τ' l'].
 408   destruct (eqd_dec l l'); [ idtac
 409     | apply (Error ("level mismatch in castExpr, invoked by "+++err_msg+++eol+++
 410                     "  got: " +++(fold_left (fun x y => y+++","+++y) (map (toString ○ haskTyVarToType) l) "")+++eol+++
 411                     "  wanted: "+++(fold_left (fun x y => x+++","+++y) (map (toString ○ haskTyVarToType) l') "")
 412     )) ].
 413   destruct (eqd_dec τ τ'); [ idtac
 414     | apply (Error ("type mismatch in castExpr, invoked by "+++err_msg+++eol+++
 415                     "  got: " +++toString τ+++eol+++
 416                     "  wanted: "+++toString τ'
 417     )) ].
 418   subst.
 419   apply OK.
 420   apply e.
 421   Defined.
 422
 423 Definition coVarKind (wcv:WeakCoerVar) : Kind :=
 424   match wcv with weakCoerVar _ t _ => (kindOfCoreType (weakTypeToCoreType t)) end.
 425   Coercion coVarKind : WeakCoerVar >-> Kind.
 426
 427 Definition weakTypeToTypeOfKind : forall {Γ:TypeEnv}(φ:TyVarResolver Γ)(t:WeakType)(κ:Kind), ???(HaskType Γ κ).
 428   intros.
 429   set (weakTypeToType φ t) as wt.
 430   destruct wt; try apply (Error error_message).
 431   destruct h.
 432   matchThings κ κ0 ("Kind mismatch in weakTypeToTypeOfKind in ").
 433   subst.
 434   apply OK.
 435   apply h.
 436   Defined.
 437
 438 Fixpoint varsTypes {Γ}(t:Tree ??(WeakExprVar * WeakExpr))(φ:TyVarResolver Γ) : Tree ??(CoreVar * HaskType Γ ★) :=
 439   match t with
 440     | T_Leaf None            => []
 441     | T_Leaf (Some (wev,e))  => match weakTypeToTypeOfKind φ wev ★ with
 442                                   | OK    t' => [((wev:CoreVar),t')]
 443                                   | _        => []
 444                                 end
 445     | T_Branch b1 b2         => (varsTypes b1 φ),,(varsTypes b2 φ)
 446   end.
 447
 448 Fixpoint mkAvars {Γ}(wtl:list WeakType)(lk:list Kind)(φ:TyVarResolver Γ) : ???(IList Kind (HaskType Γ) lk) :=
 449 match lk as LK return ???(IList Kind (HaskType Γ) LK) with
 450   | nil => match wtl with
 451              | nil => OK INil
 452              | _   => Error "length mismatch in mkAvars"
 453            end
 454   | k::lk' => match wtl with
 455                 | nil => Error "length mismatch in mkAvars"
 456                 | wt::wtl' =>
 457                   weakTypeToTypeOfKind φ wt k >>= fun t =>
 458                     mkAvars wtl' lk' φ >>= fun rest =>
 459                     OK (ICons _ _ t rest)
 460               end
 461 end.
 462
 463 Fixpoint update_ig (ig:CoreVar -> bool) (vars:list CoreVar) : CoreVar -> bool :=
 464   match vars with
 465     | nil => ig
 466     | v::vars' =>
 467       fun v' =>
 468         if eqd_dec v v'
 469           then false
 470             else update_ig ig vars' v'
 471   end.
 472
 473 (* does the specified variable occur free in the expression? *)
 474 Fixpoint doesWeakVarOccur (wev:WeakExprVar)(me:WeakExpr) : bool :=
 475   match me with
 476     | WELit    _        => false
 477     | WEVar    cv       => if eqd_dec (wev:CoreVar) (cv:CoreVar) then true else false
 478     | WECast   e co     =>                            doesWeakVarOccur wev e
 479     | WENote   n e      =>                            doesWeakVarOccur wev e
 480     | WETyApp  e t      =>                            doesWeakVarOccur wev e
 481     | WECoApp  e co     =>                            doesWeakVarOccur wev e
 482     | WEBrak _ ec e _   =>                            doesWeakVarOccur wev e
 483     | WEEsc  _ ec e _   =>                            doesWeakVarOccur wev e
 484     | WECSP  _ ec e _   =>                            doesWeakVarOccur wev e
 485     | WELet    cv e1 e2 => doesWeakVarOccur wev e1 || (if eqd_dec (wev:CoreVar) (cv:CoreVar)then false else doesWeakVarOccur wev e2)
 486     | WEApp    e1 e2    => doesWeakVarOccur wev e1 || doesWeakVarOccur wev e2
 487     | WELam    cv e     => if eqd_dec (wev:CoreVar) (cv:CoreVar) then false else doesWeakVarOccur wev e
 488     | WETyLam  cv e     => doesWeakVarOccur wev e
 489     | WECoLam  cv e     => doesWeakVarOccur wev e
 490     | WECase vscrut escrut tbranches tc avars alts =>
 491       doesWeakVarOccur wev escrut ||
 492       if eqd_dec (wev:CoreVar) (vscrut:CoreVar) then false else
 493         ((fix doesWeakVarOccurAlts alts {struct alts} : bool :=
 494           match alts with
 495             | T_Leaf  None                                         => false
 496             | T_Leaf (Some (WeakDEFAULT,_,_,_,e))                      => doesWeakVarOccur wev e
 497             | T_Leaf (Some (WeakLitAlt lit,_,_,_,e))                   => doesWeakVarOccur wev e
 498             | T_Leaf (Some ((WeakDataAlt dc), tvars, cvars, evars,e))  => doesWeakVarOccur wev e  (* FIXME!!! *)
 499             | T_Branch b1 b2                                       => doesWeakVarOccurAlts b1 || doesWeakVarOccurAlts b2
 500           end) alts)
 501     | WELetRec mlr e =>
 502       doesWeakVarOccur wev e ||
 503       (fix doesWeakVarOccurLetRec (mlr:Tree ??(WeakExprVar * WeakExpr)) : bool :=
 504       match mlr with
 505         | T_Leaf None          => false
 506         | T_Leaf (Some (cv,e)) => if eqd_dec (wev:CoreVar) (cv:CoreVar) then false else doesWeakVarOccur wev e
 507         | T_Branch b1 b2       => doesWeakVarOccurLetRec b1 || doesWeakVarOccurLetRec b2
 508       end) mlr
 509   end.
 510 Fixpoint doesWeakVarOccurAlts (wev:WeakExprVar)
 511   (alts:Tree ??(WeakAltCon * list WeakTypeVar * list WeakCoerVar * list WeakExprVar * WeakExpr)) : bool :=
 512   match alts with
 513     | T_Leaf  None                                             => false
 514     | T_Leaf (Some (WeakDEFAULT,_,_,_,e))                      => doesWeakVarOccur wev e
 515     | T_Leaf (Some (WeakLitAlt lit,_,_,_,e))                   => doesWeakVarOccur wev e
 516     | T_Leaf (Some ((WeakDataAlt dc), tvars, cvars, evars,e))  => doesWeakVarOccur wev e  (* FIXME!!! *)
 517     | T_Branch b1 b2                                           => doesWeakVarOccurAlts wev b1 || doesWeakVarOccurAlts wev b2
 518   end.
 519
 520 Definition checkDistinct :
 521   forall {V}(EQ:EqDecidable V)(lv:list V), ???(distinct lv).
 522   intros.
 523   set (distinct_decidable lv) as q.
 524   destruct q.
 525   exact (OK d).
 526   exact (Error "checkDistinct failed").
 527   Defined.
 528
 529 (* FIXME: check the kind of the type of the weakexprvar to support >0 *)
 530 Definition mkGlobal Γ (τ:HaskType Γ ★) (wev:WeakExprVar) : Global Γ.
 531   refine {| glob_kinds := nil |}.
 532   apply wev.
 533   intros.
 534   apply τ.
 535   Defined.
 536
 537 Definition weakExprToStrongExpr : forall
 538     (Γ:TypeEnv)
 539     (Δ:CoercionEnv Γ)
 540     (φ:TyVarResolver Γ)
 541     (ψ:CoVarResolver Γ Δ)
 542     (ξ:CoreVar -> LeveledHaskType Γ ★)
 543     (ig:CoreVar -> bool)
 544     (τ:HaskType Γ ★)
 545     (lev:HaskLevel Γ),
 546     WeakExpr -> ???(@Expr _ CoreVarEqDecidable Γ Δ ξ (τ @@ lev) ).
 547   refine ((
 548     fix weakExprToStrongExpr
 549     (Γ:TypeEnv)
 550     (Δ:CoercionEnv Γ)
 551     (φ:TyVarResolver Γ)
 552     (ψ:CoVarResolver Γ Δ)
 553     (ξ:CoreVar -> LeveledHaskType Γ ★)
 554     (ig:CoreVar -> bool)
 555     (τ:HaskType Γ ★)
 556     (lev:HaskLevel Γ)
 557     (we:WeakExpr) : ???(@Expr _ CoreVarEqDecidable Γ Δ ξ (τ @@ lev) )  :=
 558     addErrorMessage ("in weakExprToStrongExpr " +++ toString we)
 559     match we with
 560
 561     | WEVar   v                         => if ig v
 562                                               then OK ((EGlobal Γ Δ ξ (mkGlobal Γ τ v) INil lev) : Expr Γ Δ ξ (τ@@lev))
 563                                               else castExpr we ("WEVar "+++toString (v:CoreVar)) (τ @@ lev) (EVar Γ Δ ξ v)
 564
 565     | WELit   lit                       => castExpr we ("WELit "+++toString lit) (τ @@ lev) (ELit Γ Δ ξ lit lev)
 566
 567     | WELam   ev ebody                  => weakTypeToTypeOfKind φ ev ★ >>= fun tv =>
 568                                              weakTypeOfWeakExpr ebody >>= fun tbody =>
 569                                                weakTypeToTypeOfKind φ tbody ★ >>= fun tbody' =>
 570                                                  let ξ' := update_ξ ξ lev (((ev:CoreVar),tv)::nil) in
 571                                                  let ig' := update_ig ig ((ev:CoreVar)::nil) in
 572                                                    weakExprToStrongExpr Γ Δ φ ψ ξ' ig' tbody' lev ebody >>= fun ebody' =>
 573                                                      castExpr we "WELam" (τ@@lev) (ELam Γ Δ ξ tv tbody' lev ev ebody')
 574
 575     | WEBrak  _ ec e tbody              => φ (`ec) >>= fun ec' =>
 576                                              weakTypeToTypeOfKind φ tbody ★ >>= fun tbody' =>
 577                                                weakExprToStrongExpr Γ Δ φ ψ ξ ig tbody' ((ec')::lev) e >>= fun e' =>
 578                                                  castExpr we "WEBrak" (τ@@lev) (EBrak Γ Δ ξ ec' tbody' lev e')
 579
 580     | WEEsc   _ ec e tbody              => φ ec >>= fun ec'' =>
 581                                            weakTypeToTypeOfKind φ tbody ★ >>= fun tbody' =>
 582                                            match lev with
 583                                              | nil       => Error "ill-leveled escapification"
 584                                              | ec'::lev' => weakExprToStrongExpr Γ Δ φ ψ ξ ig (<[ ec' |- tbody' ]>) lev' e
 585                                                >>= fun e' => castExpr we "WEEsc" (τ@@lev) (EEsc Γ Δ ξ ec' tbody' lev' e')
 586                                            end
 587
 588     | WECSP   _ ec e tbody              => Error "FIXME: CSP not supported beyond HaskWeak stage"
 589
 590     | WENote  n e                       => weakExprToStrongExpr Γ Δ φ ψ ξ ig τ lev e >>= fun e' => OK (ENote _ _ _ _ n e')
 591
 592     | WELet   v ve  ebody               => weakTypeToTypeOfKind φ v ★  >>= fun tv =>
 593                                              weakExprToStrongExpr Γ Δ φ ψ ξ ig tv lev ve >>= fun ve' =>
 594                                                weakExprToStrongExpr Γ Δ φ ψ (update_ξ ξ lev (((v:CoreVar),tv)::nil))
 595                                                     (update_ig ig ((v:CoreVar)::nil)) τ lev ebody
 596                                                >>= fun ebody' =>
 597                                                  OK (ELet _ _ _ tv _ lev (v:CoreVar) ve' ebody')
 598
 599     | WEApp   e1 e2                     => weakTypeOfWeakExpr e2 >>= fun t2 =>
 600                                              weakTypeToTypeOfKind φ t2 ★ >>= fun t2' =>
 601                                                weakExprToStrongExpr Γ Δ φ ψ ξ ig t2' lev e2 >>= fun e2' =>
 602                                                  weakExprToStrongExpr Γ Δ φ ψ ξ ig (t2'--->τ) lev e1 >>= fun e1' =>
 603                                                    OK (EApp _ _ _ _ _ _ e1' e2')
 604
 605     | WETyLam tv e                      => let φ' := upφ tv φ in
 606                                              weakTypeOfWeakExpr e >>= fun te =>
 607                                                weakTypeToTypeOfKind φ' te ★ >>= fun τ' =>
 608                                                  weakExprToStrongExpr _ (weakCE Δ) φ'
 609                                                    (fun x => (ψ x) >>= fun y => OK (weakCV y)) (weakLT○ξ) ig _ (weakL lev) e
 610                                                      >>= fun e' => castExpr we "WETyLam2" _ (ETyLam Γ Δ ξ tv (mkTAll' τ') lev e')
 611
 612     | WETyApp e t                       => weakTypeOfWeakExpr e >>= fun te =>
 613                                            match te with
 614                                              | WForAllTy wtv te' =>
 615                                                let φ' := upφ wtv φ in
 616                                                  weakTypeToTypeOfKind φ' te' ★ >>= fun te'' =>
 617                                                    weakExprToStrongExpr Γ Δ φ ψ ξ ig (mkTAll te'') lev e >>= fun e' =>
 618                                                      weakTypeToTypeOfKind φ t (wtv:Kind) >>= fun t' =>
 619                                                        castExpr we "WETyApp" _ (ETyApp Γ Δ wtv (mkTAll' te'') t' ξ lev e')
 620                                              | _                 => Error ("weakTypeToType: WETyApp body with type "+++toString te)
 621                                            end
 622
 623     | WECoApp e co                     => weakTypeOfWeakExpr e >>= fun te =>
 624                                            match te with
 625                                              | WCoFunTy t1 t2 t3 =>
 626                                                weakTypeToType φ t1 >>= fun t1' =>
 627                                                  match t1' with
 628                                                    haskTypeOfSomeKind κ t1'' =>
 629                                                    weakTypeToTypeOfKind φ t2 κ >>= fun t2'' =>
 630                                                      weakTypeToTypeOfKind φ t3 ★ >>= fun t3'' =>
 631                                                        weakExprToStrongExpr Γ Δ φ ψ ξ ig (t1'' ∼∼ t2'' ⇒ τ) lev e >>= fun e' =>
 632                                                          castExpr we "WECoApp" _ e' >>= fun e'' =>
 633                                                            OK (ECoApp Γ Δ κ t1'' t2''
 634                                                              (weakCoercionToHaskCoercion _ _ _ co) τ ξ lev e'')
 635                                                  end
 636                                              | _                 => Error ("weakTypeToType: WECoApp body with type "+++toString te)
 637                                            end
 638
 639     | WECoLam cv e                      => let (_,t1,t2) := cv in
 640                                            weakTypeOfWeakExpr e >>= fun te =>
 641                                              weakTypeToTypeOfKind φ te ★ >>= fun te' =>
 642                                                weakTypeToTypeOfKind φ t1 cv >>= fun t1' =>
 643                                                  weakTypeToTypeOfKind φ t2 cv >>= fun t2' =>
 644                                                    weakExprToStrongExpr Γ (_ :: Δ) φ (weakψ ψ) ξ ig te' lev e >>= fun e' =>
 645                                                      castExpr we "WECoLam" _ (ECoLam Γ Δ cv te' t1' t2' ξ lev e')
 646
 647     | WECast  e co                      => let (t1,t2) := weakCoercionTypes co in
 648                                              weakTypeToTypeOfKind φ t1 ★ >>= fun t1' =>
 649                                                weakTypeToTypeOfKind φ t2 ★ >>= fun t2' =>
 650                                                    weakExprToStrongExpr Γ Δ φ ψ ξ ig t1' lev e >>= fun e' =>
 651                                                      castExpr we "WECast" _
 652                                                        (ECast Γ Δ ξ t1' t2' (weakCoercionToHaskCoercion _ _ _ co) lev e')
 653
 654     | WELetRec rb   e                   =>
 655       let ξ' := update_ξ ξ lev _ in
 656       let ig' := update_ig ig (map (fun x:(WeakExprVar*_) => (fst x):CoreVar) (leaves rb)) in
 657       let binds :=
 658         (fix binds (t:Tree ??(WeakExprVar * WeakExpr))
 659           : ???(ELetRecBindings Γ Δ ξ' lev (varsTypes t φ)) :=
 660         match t with
 661           | T_Leaf None           => let case_nil := tt in OK (ELR_nil _ _ _ _)
 662           | T_Leaf (Some (wev,e)) => let case_some := tt in (fun e' => _) (fun τ => weakExprToStrongExpr Γ Δ φ ψ ξ' ig' τ lev e)
 663           | T_Branch b1 b2        =>
 664             binds b1 >>= fun b1' =>
 665               binds b2 >>= fun b2' =>
 666                 OK (ELR_branch Γ Δ ξ' lev _ _ b1' b2')
 667         end) rb
 668       in binds >>= fun binds' =>
 669          checkDistinct CoreVarEqDecidable (map (@fst _ _) (leaves (varsTypes rb φ))) >>= fun rb_distinct =>
 670            weakExprToStrongExpr Γ Δ φ ψ ξ' ig' τ lev e >>= fun e' =>
 671              OK (ELetRec Γ Δ ξ lev τ _ _ binds' e')
 672
 673     | WECase vscrut escrut tbranches tc avars alts =>
 674         weakTypeOfWeakExpr escrut >>= fun tscrut =>
 675           weakTypeToTypeOfKind φ tscrut ★ >>= fun tscrut' =>
 676             if doesWeakVarOccurAlts vscrut alts
 677             then Error "encountered a Case which actually used its binder - these should have been desugared away!!"
 678             else mkAvars avars (tyConKind tc) φ >>= fun avars' =>
 679                 weakTypeToTypeOfKind φ tbranches ★  >>= fun tbranches' =>
 680                   (fix mkTree (t:Tree ??(WeakAltCon*list WeakTypeVar*list WeakCoerVar*list WeakExprVar*WeakExpr)) : ???(Tree
 681                       ??{ sac : _ & {scb : StrongCaseBranchWithVVs CoreVar CoreVarEqDecidable tc avars' sac &
 682                         Expr (sac_Γ sac Γ) (sac_Δ sac Γ avars' (weakCK'' Δ))(scbwv_ξ scb ξ lev)(weakLT' (tbranches' @@  lev))}}) :=
 683                     match t with
 684                       | T_Leaf None           => OK []
 685                       | T_Leaf (Some (ac,extyvars,coervars,exprvars,ebranch)) =>
 686                         mkStrongAltConPlusJunk' tc ac >>= fun sac =>
 687                           list2vecOrFail (map (fun ev:WeakExprVar => ev:CoreVar) exprvars) _ (fun _ _ => "WECase")
 688                           >>= fun exprvars' =>
 689                             (let case_pf := tt in _) >>= fun pf =>
 690                             let scb := @Build_StrongCaseBranchWithVVs CoreVar CoreVarEqDecidable tc Γ avars' sac exprvars' pf in
 691                               weakExprToStrongExpr (sac_Γ sac Γ) (sac_Δ sac Γ avars' (weakCK'' Δ)) (sacpj_φ sac _ φ)
 692                               (sacpj_ψ sac _ _ avars' ψ)
 693                               (scbwv_ξ scb ξ lev)
 694                               (update_ig ig (map (@fst _ _) (vec2list (scbwv_varstypes scb))))
 695                               (weakT' tbranches') (weakL' lev) ebranch >>= fun ebranch' =>
 696                                 let case_case := tt in OK [ _ ]
 697                       | T_Branch b1 b2        =>
 698                         mkTree b1 >>= fun b1' =>
 699                           mkTree b2 >>= fun b2' =>
 700                             OK (b1',,b2')
 701                     end) alts >>= fun tree =>
 702
 703                     weakExprToStrongExpr Γ Δ φ ψ ξ ig (caseType tc avars') lev escrut >>= fun escrut' =>
 704                       castExpr we "ECase" (τ@@lev) (ECase Γ Δ ξ lev tc tbranches' avars' escrut' tree)
 705     end)); try clear binds; try apply ConcatenableString.
 706
 707     destruct case_some.
 708     apply (addErrorMessage "case_some").
 709       simpl.
 710       destruct (weakTypeToTypeOfKind φ wev ★); try apply (Error error_message).
 711       matchThings h (unlev (ξ' wev)) "LetRec".
 712       destruct wev.
 713       rewrite matchTypeVars_pf.
 714       clear matchTypeVars_pf.
 715       set (e' (unlev (ξ' (weakExprVar c w)))) as e''.
 716       destruct e''; try apply (Error error_message).
 717       apply OK.
 718       apply ELR_leaf.
 719       unfold ξ'.
 720       simpl.
 721       induction (leaves (varsTypes rb φ)).
 722         simpl; auto.
 723         destruct (ξ c).
 724         simpl.
 725       apply e1.
 726       rewrite mapleaves.
 727       apply rb_distinct.
 728
 729     destruct case_pf.
 730       set (distinct_decidable (vec2list exprvars')) as dec.
 731       destruct dec; [ idtac | apply (Error "malformed HaskWeak: case branch with variables repeated") ].
 732       apply OK; auto.
 733
 734     destruct case_case.
 735       exists sac.
 736       exists scb.
 737       apply ebranch'.
 738
 739     Defined.
 740