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