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 tc (fst (tyFunKind tc)) (snd (tyFunKind tc))).
 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 (* FIXME: check the kind of the type of the weakexprvar to support >0 *)
 523 Definition mkGlobal Γ (τ:HaskType Γ ★) (wev:WeakExprVar) : Global Γ.
 524   refine {| glob_kinds := nil |}.
 525   apply wev.
 526   intros.
 527   apply τ.
 528   Defined.
 529
 530 Definition weakExprToStrongExpr : forall
 531     (Γ:TypeEnv)
 532     (Δ:CoercionEnv Γ)
 533     (φ:TyVarResolver Γ)
 534     (ψ:CoVarResolver Γ Δ)
 535     (ξ:CoreVar -> LeveledHaskType Γ ★)
 536     (ig:CoreVar -> bool)
 537     (τ:HaskType Γ ★)
 538     (lev:HaskLevel Γ),
 539     WeakExpr -> ???(@Expr _ CoreVarEqDecidable Γ Δ ξ (τ @@ lev) ).
 540   refine ((
 541     fix weakExprToStrongExpr
 542     (Γ:TypeEnv)
 543     (Δ:CoercionEnv Γ)
 544     (φ:TyVarResolver Γ)
 545     (ψ:CoVarResolver Γ Δ)
 546     (ξ:CoreVar -> LeveledHaskType Γ ★)
 547     (ig:CoreVar -> bool)
 548     (τ:HaskType Γ ★)
 549     (lev:HaskLevel Γ)
 550     (we:WeakExpr) : ???(@Expr _ CoreVarEqDecidable Γ Δ ξ (τ @@ lev) )  :=
 551     addErrorMessage ("in weakExprToStrongExpr " +++ toString we)
 552     match we with
 553
 554     | WEVar   v                         => if ig v
 555                                               then OK ((EGlobal Γ Δ ξ (mkGlobal Γ τ v) INil lev) : Expr Γ Δ ξ (τ@@lev))
 556                                               else castExpr we ("WEVar "+++toString (v:CoreVar)) (τ @@ lev) (EVar Γ Δ ξ v)
 557
 558     | WELit   lit                       => castExpr we ("WELit "+++toString lit) (τ @@ lev) (ELit Γ Δ ξ lit lev)
 559
 560     | WELam   ev ebody                  => weakTypeToTypeOfKind φ ev ★ >>= fun tv =>
 561                                              weakTypeOfWeakExpr ebody >>= fun tbody =>
 562                                                weakTypeToTypeOfKind φ tbody ★ >>= fun tbody' =>
 563                                                  let ξ' := update_ξ ξ lev (((ev:CoreVar),tv)::nil) in
 564                                                  let ig' := update_ig ig ((ev:CoreVar)::nil) in
 565                                                    weakExprToStrongExpr Γ Δ φ ψ ξ' ig' tbody' lev ebody >>= fun ebody' =>
 566                                                      castExpr we "WELam" (τ@@lev) (ELam Γ Δ ξ tv tbody' lev ev ebody')
 567
 568     | WEBrak  _ ec e tbody              => φ (`ec) >>= fun ec' =>
 569                                              weakTypeToTypeOfKind φ tbody ★ >>= fun tbody' =>
 570                                                weakExprToStrongExpr Γ Δ φ ψ ξ ig tbody' ((ec')::lev) e >>= fun e' =>
 571                                                  castExpr we "WEBrak" (τ@@lev) (EBrak Γ Δ ξ ec' tbody' lev e')
 572
 573     | WEEsc   _ ec e tbody              => φ ec >>= fun ec'' =>
 574                                            weakTypeToTypeOfKind φ tbody ★ >>= fun tbody' =>
 575                                            match lev with
 576                                              | nil       => Error "ill-leveled escapification"
 577                                              | ec'::lev' => weakExprToStrongExpr Γ Δ φ ψ ξ ig (<[ ec' |- tbody' ]>) lev' e
 578                                                >>= fun e' => castExpr we "WEEsc" (τ@@lev) (EEsc Γ Δ ξ ec' tbody' lev' e')
 579                                            end
 580
 581     | WECSP   _ ec e tbody              => Error "FIXME: CSP not supported beyond HaskWeak stage"
 582
 583     | WENote  n e                       => weakExprToStrongExpr Γ Δ φ ψ ξ ig τ lev e >>= fun e' => OK (ENote _ _ _ _ n e')
 584
 585     | WELet   v ve  ebody               => weakTypeToTypeOfKind φ v ★  >>= fun tv =>
 586                                              weakExprToStrongExpr Γ Δ φ ψ ξ ig tv lev ve >>= fun ve' =>
 587                                                weakExprToStrongExpr Γ Δ φ ψ (update_ξ ξ lev (((v:CoreVar),tv)::nil))
 588                                                     (update_ig ig ((v:CoreVar)::nil)) τ lev ebody
 589                                                >>= fun ebody' =>
 590                                                  OK (ELet _ _ _ tv _ lev (v:CoreVar) ve' ebody')
 591
 592     | WEApp   e1 e2                     => weakTypeOfWeakExpr e2 >>= fun t2 =>
 593                                              weakTypeToTypeOfKind φ t2 ★ >>= fun t2' =>
 594                                                weakExprToStrongExpr Γ Δ φ ψ ξ ig t2' lev e2 >>= fun e2' =>
 595                                                  weakExprToStrongExpr Γ Δ φ ψ ξ ig (t2'--->τ) lev e1 >>= fun e1' =>
 596                                                    OK (EApp _ _ _ _ _ _ e1' e2')
 597
 598     | WETyLam tv e                      => let φ' := upφ tv φ in
 599                                              weakTypeOfWeakExpr e >>= fun te =>
 600                                                weakTypeToTypeOfKind φ' te ★ >>= fun τ' =>
 601                                                  weakExprToStrongExpr _ (weakCE Δ) φ'
 602                                                    (fun x => (ψ x) >>= fun y => OK (weakCV y)) (weakLT○ξ) ig _ (weakL lev) e
 603                                                      >>= fun e' => castExpr we "WETyLam2" _ (ETyLam Γ Δ ξ tv (mkTAll' τ') lev e')
 604
 605     | WETyApp e t                       => weakTypeOfWeakExpr e >>= fun te =>
 606                                            match te with
 607                                              | WForAllTy wtv te' =>
 608                                                let φ' := upφ wtv φ in
 609                                                  weakTypeToTypeOfKind φ' te' ★ >>= fun te'' =>
 610                                                    weakExprToStrongExpr Γ Δ φ ψ ξ ig (mkTAll te'') lev e >>= fun e' =>
 611                                                      weakTypeToTypeOfKind φ t (wtv:Kind) >>= fun t' =>
 612                                                        castExpr we "WETyApp" _ (ETyApp Γ Δ wtv (mkTAll' te'') t' ξ lev e')
 613                                              | _                 => Error ("weakTypeToType: WETyApp body with type "+++toString te)
 614                                            end
 615
 616     | WECoApp e co                     => weakTypeOfWeakExpr e >>= fun te =>
 617                                            match te with
 618                                              | WCoFunTy t1 t2 t3 =>
 619                                                weakTypeToType φ t1 >>= fun t1' =>
 620                                                  match t1' with
 621                                                    haskTypeOfSomeKind κ t1'' =>
 622                                                    weakTypeToTypeOfKind φ t2 κ >>= fun t2'' =>
 623                                                      weakTypeToTypeOfKind φ t3 ★ >>= fun t3'' =>
 624                                                        weakExprToStrongExpr Γ Δ φ ψ ξ ig (t1'' ∼∼ t2'' ⇒ τ) lev e >>= fun e' =>
 625                                                          castExpr we "WECoApp" _ e' >>= fun e'' =>
 626                                                            OK (ECoApp Γ Δ κ t1'' t2''
 627                                                              (weakCoercionToHaskCoercion _ _ _ co) τ ξ lev e'')
 628                                                  end
 629                                              | _                 => Error ("weakTypeToType: WECoApp body with type "+++toString te)
 630                                            end
 631
 632     | WECoLam cv e                      => let (_,_,t1,t2) := cv in
 633                                            weakTypeOfWeakExpr e >>= fun te =>
 634                                              weakTypeToTypeOfKind φ te ★ >>= fun te' =>
 635                                                weakTypeToTypeOfKind φ t1 cv >>= fun t1' =>
 636                                                  weakTypeToTypeOfKind φ t2 cv >>= fun t2' =>
 637                                                    weakExprToStrongExpr Γ (_ :: Δ) φ (weakψ ψ) ξ ig te' lev e >>= fun e' =>
 638                                                      castExpr we "WECoLam" _ (ECoLam Γ Δ cv te' t1' t2' ξ lev e')
 639
 640     | WECast  e co                      => let (t1,t2) := weakCoercionTypes co in
 641                                              weakTypeToTypeOfKind φ t1 ★ >>= fun t1' =>
 642                                                weakTypeToTypeOfKind φ t2 ★ >>= fun t2' =>
 643                                                    weakExprToStrongExpr Γ Δ φ ψ ξ ig t1' lev e >>= fun e' =>
 644                                                      castExpr we "WECast" _
 645                                                        (ECast Γ Δ ξ t1' t2' (weakCoercionToHaskCoercion _ _ _ co) lev e')
 646
 647     | WELetRec rb   e                   =>
 648       let ξ' := update_ξ ξ lev _ in
 649       let ig' := update_ig ig (map (fun x:(WeakExprVar*_) => (fst x):CoreVar) (leaves rb)) in
 650       let binds :=
 651         (fix binds (t:Tree ??(WeakExprVar * WeakExpr))
 652           : ???(ELetRecBindings Γ Δ ξ' lev (varsTypes t φ)) :=
 653         match t with
 654           | T_Leaf None           => let case_nil := tt in OK (ELR_nil _ _ _ _)
 655           | T_Leaf (Some (wev,e)) => let case_some := tt in (fun e' => _) (fun τ => weakExprToStrongExpr Γ Δ φ ψ ξ' ig' τ lev e)
 656           | T_Branch b1 b2        =>
 657             binds b1 >>= fun b1' =>
 658               binds b2 >>= fun b2' =>
 659                 OK (ELR_branch Γ Δ ξ' lev _ _ b1' b2')
 660         end) rb
 661       in binds >>= fun binds' =>
 662          checkDistinct CoreVarEqDecidable (map (@fst _ _) (leaves (varsTypes rb φ))) >>= fun rb_distinct =>
 663            weakExprToStrongExpr Γ Δ φ ψ ξ' ig' τ lev e >>= fun e' =>
 664              OK (ELetRec Γ Δ ξ lev τ _ _ binds' e')
 665
 666     | WECase vscrut escrut tbranches tc avars alts =>
 667         weakTypeOfWeakExpr escrut >>= fun tscrut =>
 668           weakTypeToTypeOfKind φ tscrut ★ >>= fun tscrut' =>
 669             if doesWeakVarOccurAlts vscrut alts
 670             then Error "encountered a Case which actually used its binder - these should have been desugared away!!"
 671             else mkAvars avars (tyConKind tc) φ >>= fun avars' =>
 672                 weakTypeToTypeOfKind φ tbranches ★  >>= fun tbranches' =>
 673                   (fix mkTree (t:Tree ??(WeakAltCon*list WeakTypeVar*list WeakCoerVar*list WeakExprVar*WeakExpr)) : ???(Tree
 674                       ??{ sac : _ & {scb : StrongCaseBranchWithVVs CoreVar CoreVarEqDecidable tc avars' sac &
 675                         Expr (sac_Γ sac Γ) (sac_Δ sac Γ avars' (weakCK'' Δ))(scbwv_ξ scb ξ lev)(weakLT' (tbranches' @@  lev))}}) :=
 676                     match t with
 677                       | T_Leaf None           => OK []
 678                       | T_Leaf (Some (ac,extyvars,coervars,exprvars,ebranch)) =>
 679                         mkStrongAltConPlusJunk' tc ac >>= fun sac =>
 680                           list2vecOrFail (map (fun ev:WeakExprVar => ev:CoreVar) exprvars) _ (fun _ _ => "WECase")
 681                           >>= fun exprvars' =>
 682                             (let case_pf := tt in _) >>= fun pf =>
 683                             let scb := @Build_StrongCaseBranchWithVVs CoreVar CoreVarEqDecidable tc Γ avars' sac exprvars' pf in
 684                               weakExprToStrongExpr (sac_Γ sac Γ) (sac_Δ sac Γ avars' (weakCK'' Δ)) (sacpj_φ sac _ φ)
 685                               (sacpj_ψ sac _ _ avars' ψ)
 686                               (scbwv_ξ scb ξ lev)
 687                               (update_ig ig (map (@fst _ _) (vec2list (scbwv_varstypes scb))))
 688                               (weakT' tbranches') (weakL' lev) ebranch >>= fun ebranch' =>
 689                                 let case_case := tt in OK [ _ ]
 690                       | T_Branch b1 b2        =>
 691                         mkTree b1 >>= fun b1' =>
 692                           mkTree b2 >>= fun b2' =>
 693                             OK (b1',,b2')
 694                     end) alts >>= fun tree =>
 695
 696                     weakExprToStrongExpr Γ Δ φ ψ ξ ig (caseType tc avars') lev escrut >>= fun escrut' =>
 697                       castExpr we "ECase" (τ@@lev) (ECase Γ Δ ξ lev tc tbranches' avars' escrut' tree)
 698     end)); try clear binds; try apply ConcatenableString.
 699
 700     destruct case_some.
 701     apply (addErrorMessage "case_some").
 702       simpl.
 703       destruct (weakTypeToTypeOfKind φ wev ★); try apply (Error error_message).
 704       matchThings h (unlev (ξ' wev)) "LetRec".
 705       destruct wev.
 706       rewrite matchTypeVars_pf.
 707       clear matchTypeVars_pf.
 708       set (e' (unlev (ξ' (weakExprVar c w)))) as e''.
 709       destruct e''; try apply (Error error_message).
 710       apply OK.
 711       apply ELR_leaf.
 712       unfold ξ'.
 713       simpl.
 714       induction (leaves (varsTypes rb φ)).
 715         simpl; auto.
 716         destruct (ξ c).
 717         simpl.
 718       apply e1.
 719       rewrite mapleaves.
 720       apply rb_distinct.
 721
 722     destruct case_pf.
 723       set (distinct_decidable (vec2list exprvars')) as dec.
 724       destruct dec; [ idtac | apply (Error "malformed HaskWeak: case branch with variables repeated") ].
 725       apply OK; auto.
 726
 727     destruct case_case.
 728       exists sac.
 729       exists scb.
 730       apply ebranch'.
 731
 732     Defined.
 733