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