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