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