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