src/HaskWeakToStrong.v

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