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