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