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