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