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