X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskStrongToWeak.v;h=8bb52e12f6ee81c217dd02d4ccc323519f395be2;hp=ea768560a6fd44829d5e3173bf43d33807377a1b;hb=489b12c6c491b96c37839610d33fbdf666ee527f;hpb=26733c04106397dc8a10396ce688e908e8d0cde7

diff --git a/src/HaskStrongToWeak.v b/src/HaskStrongToWeak.v
index ea76856..8bb52e1 100644
--- a/src/HaskStrongToWeak.v
+++ b/src/HaskStrongToWeak.v
@@ -10,137 +10,221 @@ Require Import Coq.Strings.String.
 Require Import Coq.Lists.List.
 Require Import Coq.Init.Specif.
 Require Import HaskKinds.
-Require Import HaskCoreLiterals.
-Require Import HaskCoreVars.
+Require Import HaskLiterals.
+Require Import HaskTyCons.
 Require Import HaskWeakTypes.
 Require Import HaskWeakVars.
 Require Import HaskWeak.
+Require Import HaskWeakToCore.
 Require Import HaskStrongTypes.
 Require Import HaskStrong.
 
-Fixpoint mfresh (f:Fresh Kind (fun _ => WeakTypeVar))(lk:list Kind){Γ}(ite:IList _ (fun _ => WeakTypeVar) Γ)
-  : (Fresh Kind (fun _ => WeakTypeVar)) * ((vec WeakTypeVar (length lk)) * (IList _ (fun _ => WeakTypeVar) (app lk Γ))) :=
-  match lk as LK return (Fresh Kind (fun _ => WeakTypeVar)) * ((vec WeakTypeVar (length LK)) *
-                          (IList _ (fun _ => WeakTypeVar) (app LK Γ))) with
-  | nil    => (f,(vec_nil,ite))
-  | k::lk' =>
-    let (f',varsite') := mfresh f lk' ite
-    in  let (vars,ite') := varsite'
-    in  let (v,f'') := next _ _ f' k
-    in (f'',((v:::vars),v::::ite'))
-  end.
+Section HaskStrongToWeak.
 
-Fixpoint rawHaskTypeToWeakType (f:Fresh Kind (fun _ => WeakTypeVar)){κ}(rht:RawHaskType (fun _ => WeakTypeVar) κ)
- {struct rht} : WeakType :=
-match rht with
-  | TVar  _  v                 => WTyVarTy v
-  | TCon      tc              => WTyCon tc
-  | TCoerc _ t1 t2 t3          => WCoFunTy (rawHaskTypeToWeakType f t1) (rawHaskTypeToWeakType f t2) (rawHaskTypeToWeakType f t3)
-  | TArrow                    => WFunTyCon
-  | TApp  _ _  t1 t2             => WAppTy (rawHaskTypeToWeakType f t1) (rawHaskTypeToWeakType f t2)
-  | TAll    k rht'            => let (tv,f') := next _ _ f k in WForAllTy tv (rawHaskTypeToWeakType f' (rht' tv))
-  | TCode   t1 t2             => 
-    match (rawHaskTypeToWeakType f t1) with
-      | WTyVarTy ec => WCodeTy ec (rawHaskTypeToWeakType f t2)
-      | impossible  => impossible  (* TODO: find a way to convince Coq this can't happen *)
-    end
-  | TyFunApp    tfc tls         => WTyFunApp tfc (rawHaskTypeListToWeakType f tls)
-end
-with rawHaskTypeListToWeakType (f:Fresh Kind (fun _ => WeakTypeVar)){κ}(rht:RawHaskTypeList κ) :=
-match rht with
-  | TyFunApp_nil   => nil
-  | TyFunApp_cons  κ kl rht' rhtl' => (rawHaskTypeToWeakType f rht')::(rawHaskTypeListToWeakType f rhtl')
-end.
+  Context (hetmet_brak : WeakExprVar).
+  Context (hetmet_esc  : WeakExprVar).
 
-Definition typeToWeakType (f:Fresh Kind (fun _ => WeakTypeVar))
-  {Γ}{κ}(τ:HaskType Γ κ)(φ:InstantiatedTypeEnv (fun _ => WeakTypeVar) Γ) : WeakType :=
-  rawHaskTypeToWeakType f (τ _ φ).
+  Context (mkWeakTypeVar_ : Unique -> Kind                         -> WeakTypeVar).
+  Context (mkWeakCoerVar_ : Unique -> Kind -> WeakType -> WeakType -> WeakCoerVar).
+  Context (mkWeakExprVar_ : Unique ->         WeakType             -> WeakExprVar).
 
-Variable unsafeCoerce           : WeakCoercion.    Extract Inlined Constant unsafeCoerce => "Coercion.unsafeCoerce".
+  Definition mkWeakTypeVar (k:Kind)                 : UniqM WeakTypeVar := bind u = getU ; return mkWeakTypeVar_ u k.
+  Definition mkWeakCoerVar (k:Kind)(t1 t2:WeakType) : UniqM WeakCoerVar := bind u = getU ; return mkWeakCoerVar_ u k t1 t2.
+  Definition mkWeakExprVar (t:WeakType)             : UniqM WeakExprVar := bind u = getU ; return mkWeakExprVar_ u t.
 
-Definition strongCoercionToWeakCoercion {Γ}{Δ}{ck}(τ:HaskCoercion Γ Δ ck)(φ:InstantiatedTypeEnv (fun _ => WeakTypeVar) Γ)
-  : WeakCoercion := unsafeCoerce.
+  Fixpoint mfresh (lk:list Kind){Γ}(ite:IList _ (fun _ => WeakTypeVar) Γ)
+    : UniqM (((vec WeakTypeVar (length lk)) * (IList _ (fun _ => WeakTypeVar) (app lk Γ)))) :=
+    match lk as LK return UniqM ((vec WeakTypeVar (length LK)) * (IList _ (fun _ => WeakTypeVar) (app LK Γ))) with
+    | nil    => return (vec_nil,ite)
+    | k::lk' => bind v = mkWeakTypeVar k
+              ; bind vars_ite' = mfresh lk' ite
+              ; return ((v:::(fst vars_ite')),v::::(snd vars_ite'))
+    end.
+
+  Fixpoint rawHaskTypeToWeakType {κ}(rht:RawHaskType (fun _ => WeakTypeVar) κ) {struct rht} : UniqM WeakType :=
+  match rht with
+    | TVar  _  v                => return WTyVarTy v
+    | TCon      tc              => return WTyCon tc
+    | TCoerc _ t1 t2 t3         => bind t1' = rawHaskTypeToWeakType t1
+                                 ; bind t2' = rawHaskTypeToWeakType t2
+                                 ; bind t3' = rawHaskTypeToWeakType t3
+                                 ; return WCoFunTy t1' t2' t3'
+    | TArrow                    => return WFunTyCon
+    | TApp  _ _  t1 t2          => bind t1' = rawHaskTypeToWeakType t1
+                                 ; bind t2' = rawHaskTypeToWeakType t2
+                                 ; return WAppTy t1' t2'
+    | TAll    k rht'            => bind tv = mkWeakTypeVar k
+                                 ; bind t' = rawHaskTypeToWeakType (rht' tv)
+                                 ; return WForAllTy tv t'
+    | TCode   t1 t2             => bind t1' = rawHaskTypeToWeakType t1
+                                 ; bind t2' = rawHaskTypeToWeakType t2
+                                 ; match t1' with
+                                     | WTyVarTy ec => return WCodeTy ec t2'
+                                     | _           => failM  "impossible"
+                                   end
+    | TyFunApp    tfc _ _ tls       => bind tls' = rawHaskTypeListToWeakType tls
+                                 ; return WTyFunApp tfc tls'
+  end
+  with rawHaskTypeListToWeakType {κ}(rht:RawHaskTypeList κ) : UniqM (list WeakType) :=
+  match rht with
+    | TyFunApp_nil                   => return nil
+    | TyFunApp_cons  κ kl rht' rhtl' => bind t  = rawHaskTypeToWeakType rht'
+                                      ; bind tl = rawHaskTypeListToWeakType rhtl'
+                                      ; return t::tl
+  end.
+  
+  Definition typeToWeakType {Γ}{κ}(τ:HaskType Γ κ)(φ:InstantiatedTypeEnv (fun _ => WeakTypeVar) Γ) : UniqM WeakType :=
+    rawHaskTypeToWeakType (τ _ φ).
+  
+  Definition updateITE {Γ:TypeEnv}{TV:Kind->Type}{κ}(tv:TV κ)(ite:InstantiatedTypeEnv TV Γ) : InstantiatedTypeEnv TV (κ::Γ)
+    := tv::::ite.
+  
+  Definition updateITE_ {Γ:TypeEnv}{TV:Kind->Type}{κ}{n}(tv:TV κ)(ite:InstantiatedTypeEnv TV Γ)
+    : InstantiatedTypeEnv TV (list_ins n κ Γ).
+    rewrite list_ins_app.
+    rewrite <- (list_take_drop _ Γ n) in ite.
+    apply ilist_app.
+    apply ilist_chop in ite; auto.
+    apply ICons.
+    apply tv.
+    apply ilist_chop' in ite.
+    apply ite.
+    Defined.
+  
+  Definition coercionToWeakCoercion Γ Δ κ t1 t2 ite (γ:@HaskCoercion Γ Δ (@mkHaskCoercionKind Γ κ t1 t2))
+    : UniqM WeakCoercion
+    := bind t1' = @typeToWeakType Γ κ t1 ite
+     ; bind t2' = @typeToWeakType Γ κ t2 ite
+     ; return WCoUnsafe t1' t2'.
+  
+  Fixpoint seqM {a}(l:list (UniqM a)) : UniqM (list a) :=
+    match l with
+      | nil  => return nil
+      | x::y => bind x' = x
+              ; bind y' = seqM y
+              ; return x'::y'
+    end.
+  
+  Context {VV}{eqVV:EqDecidable VV}{toStringVV:ToString VV}.
+  
+  Definition update_chi (χ:VV->???WeakExprVar)(vv:VV)(ev':WeakExprVar) : VV->???WeakExprVar :=
+    fun vv' =>
+      if eqd_dec vv vv'
+      then OK ev'
+      else χ vv'.
 
-(* This can be used to turn HaskStrong's with arbitrary expression variables into HaskStrong's which use WeakExprVar's
- * for their variables; those can subsequently be passed to the following function (strongExprToWeakExpr) *)
-(*
-Definition reindexStrongExpr {VV}{HH}{eqVV:EqDecidable VV}{eqHH:EqDecidable HH}
-  {Γ}{Δ}{ξ}{lev}(exp:@Expr VV eqVV Γ Δ ξ lev) : { ξ' : HH -> LeveledHaskType Γ & @Expr HH eqHH Γ Δ ξ' lev }.
-  Defined.
-  *)
+  Fixpoint update_chi' (χ:VV->???WeakExprVar)(varsexprs:list (VV * WeakExprVar)) : VV->???WeakExprVar :=
+    match varsexprs with
+      | nil => χ
+      | (vv,wev)::rest => update_chi (update_chi' χ rest) vv wev
+    end.
 
-Definition updateITE {Γ:TypeEnv}{TV:Kind->Type}{κ}(tv:TV κ)(ite:InstantiatedTypeEnv TV Γ) : InstantiatedTypeEnv TV (κ::Γ)
-  := tv::::ite.
+  Fixpoint exprToWeakExpr {Γ}{Δ}{ξ}{τ}{l}(χ:VV->???WeakExprVar)(exp:@Expr _ eqVV Γ Δ ξ τ l)
+    : InstantiatedTypeEnv (fun _ => WeakTypeVar) Γ
+    -> UniqM WeakExpr :=
+    match exp as E in @Expr _ _ G D X T L return InstantiatedTypeEnv (fun _ => WeakTypeVar) G -> UniqM WeakExpr with
+    | EVar  Γ' _ ξ' ev              => fun ite => match χ ev with OK v => return WEVar v | Error s => failM s end
+    | EGlobal Γ' _ ξ'   g v lev     => fun ite => bind tv' = mapM (ilist_to_list (ilmap (fun κ x => typeToWeakType x ite) v))
+                                                ; return (fold_left (fun x y => WETyApp x y) tv' (WEVar g))
+    | ELam  Γ'   _ _ tv _ _ cv e    => fun ite => bind tv' = typeToWeakType tv ite
+                                                ; bind ev' = mkWeakExprVar tv'
+                                                ; bind e'  = exprToWeakExpr (update_chi χ cv ev') e ite
+                                                ; return WELam ev' e'
+    | ELet  Γ' _ _ t _ _ ev e1 e2   => fun ite => bind tv' = typeToWeakType t ite
+                                                ; bind e1' = exprToWeakExpr χ e1 ite
+                                                ; bind ev' = mkWeakExprVar tv'
+                                                ; bind e2' = exprToWeakExpr (update_chi χ ev ev') e2 ite
+                                                ; return WELet ev' e1' e2'
+    | ELit  _ _ _ lit _             => fun ite => return WELit lit
+    | EApp  Γ' _ _ _ _ _ e1 e2      => fun ite => bind e1' = exprToWeakExpr χ e1 ite
+                                                ; bind e2' = exprToWeakExpr χ e2 ite
+                                                ; return WEApp e1' e2'
+    | EEsc  Γ' _ _ ec t _ e         => fun ite => bind t' = typeToWeakType t ite
+                                                ; bind e' = exprToWeakExpr χ e ite
+                                                ; return WEEsc hetmet_esc (ec _ ite) e' t'
+    | EBrak Γ' _ _ ec t _ e         => fun ite => bind t' = typeToWeakType t ite
+                                                ; bind e' = exprToWeakExpr χ e ite
+                                                ; return WEBrak hetmet_brak (ec _ ite) e' t'
+    | ENote _ _ _ _ _ n e           => fun ite => bind e' = exprToWeakExpr χ e ite
+                                                ; return WENote n e'
+    | ETyApp  Γ Δ κ σ τ ξ l       e => fun ite => bind t' = typeToWeakType τ ite
+                                                ; bind e' = exprToWeakExpr χ e ite
+                                                ; return WETyApp e' t'
+    | ECoApp Γ Δ κ σ₁ σ₂ γ σ ξ l e  => fun ite => bind e' = exprToWeakExpr χ e ite
+                                                ; bind c' = coercionToWeakCoercion _ _ _ _ _ ite γ
+                                                ; return WECoApp e' c'
+    | ECast Γ Δ ξ t1 t2 γ l e      => fun ite  => bind e' = exprToWeakExpr χ e ite
+                                                ; bind c' = coercionToWeakCoercion _ _ _ _ _ ite γ
+                                                ; return WECast e' c'
+    | ETyLam _ _ _ k _ _ n e        => fun ite => bind tv = mkWeakTypeVar k
+                                                ; bind e' = exprToWeakExpr χ e (updateITE_ tv ite)
+                                                ; return WETyLam tv e'
+    | ECoLam Γ Δ κ σ σ₁ σ₂ ξ l e    => fun ite => bind t1' = typeToWeakType σ₁ ite
+                                                ; bind t2' = typeToWeakType σ₂ ite
+                                                ; bind cv  = mkWeakCoerVar κ t1' t2'
+                                                ; bind e'  = exprToWeakExpr χ e ite
+                                                ; return WECoLam cv e'
+    | ECase Γ Δ ξ l tc tbranches atypes escrut alts => 
+         fun ite => bind tscrut'    = typeToWeakType (caseType tc atypes) ite
+                  ; bind vscrut'    = mkWeakExprVar tscrut'
+                  ; bind tbranches' = @typeToWeakType Γ _ tbranches ite
+                  ; bind escrut'    = exprToWeakExpr χ escrut ite
+                  ; bind branches'  =
+                      ((fix caseBranches (tree:Tree ??{sac : _ & { scb : StrongCaseBranchWithVVs VV _ _ _ sac & Expr _ _ _ _ _ } })
+                            : UniqM (Tree ??(WeakAltCon*list WeakTypeVar*list WeakCoerVar*list WeakExprVar*WeakExpr)) :=
+                            match tree with
+                              | T_Leaf None           => return []
+                              | T_Leaf (Some x)       =>
+                                let (sac,scb_e) := x in
+                                let (scb,e) := scb_e in
+                                let varstypes := vec2list (scbwv_varstypes scb) in
+                                      bind evars_ite = mfresh _ ite
+                                    ; bind exprvars  = seqM (map (fun vt:VV * HaskType _ ★
+                                                                        => bind tleaf = typeToWeakType (snd vt) (snd evars_ite)
+                                                                         ; bind v' = mkWeakExprVar tleaf
+                                                                         ; return ((fst vt),v'))
+                                                                varstypes)
+                                    ; let χ' := update_chi' χ exprvars in
+                                      bind e'' = exprToWeakExpr χ' e (snd evars_ite)
+                                    ; return [(sac_altcon sac, vec2list (fst evars_ite), nil, (map (@snd _ _) exprvars), e'')]
+                              | T_Branch b1 b2        => bind b1' = caseBranches b1
+                                                       ; bind b2' = caseBranches b2
+                                                       ; return (b1',,b2')
+                            end) alts)
+                  ; bind tys = seqM (ilist_to_list (@ilmap _ _
+                                  (fun _ => UniqM WeakType) _ (fun _ t => typeToWeakType t ite) atypes))
+                  ; return WECase vscrut' escrut' tbranches' tc tys branches'
+
+    | ELetRec _ _ _ _ _ vars disti elrb e => fun ite => bind vars' = seqM (map (fun vt:VV * HaskType _ ★
+                                                                        => bind tleaf = typeToWeakType (snd vt) ite
+                                                                         ; bind v' = mkWeakExprVar tleaf
+                                                                         ; return ((fst vt),v'))
+                                                                (leaves vars))
+                                                ; let χ' := update_chi' χ vars' in
+                                                  bind elrb' = exprLetRec2WeakExprLetRec χ' elrb ite
+                                                ; bind e'    = exprToWeakExpr χ' e ite
+                                                ; return WELetRec elrb' e'
+    end
+    with exprLetRec2WeakExprLetRec  {Γ}{Δ}{ξ}{τ}(χ:VV->???WeakExprVar){vars}(elrb:@ELetRecBindings _ eqVV Γ Δ ξ τ vars)
+      : InstantiatedTypeEnv (fun _ => WeakTypeVar) Γ -> UniqM (Tree ??(WeakExprVar * WeakExpr)) :=
+    match elrb as E in ELetRecBindings G D X L V
+       return InstantiatedTypeEnv (fun _ => WeakTypeVar) G -> UniqM (Tree ??(WeakExprVar * WeakExpr)) with
+    | ELR_nil    _ _ _ _           => fun ite => return []
+    | ELR_leaf   _ _ ξ' cv v t e   => fun ite => bind t'  = typeToWeakType t ite
+                                               ; bind e'  = exprToWeakExpr χ e ite
+                                               ; bind v'  = match χ v with Error s => failM s | OK y => return y end
+                                               ; return [(v',e')]
+    | ELR_branch _ _ _ _ _ _ b1 b2 => fun ite => bind b1' = exprLetRec2WeakExprLetRec χ b1 ite
+                                               ; bind b2' = exprLetRec2WeakExprLetRec χ b2 ite
+                                               ; return b1',,b2'
+  end.
 
-Section strongExprToWeakExpr.
 
-  Context (hetmet_brak : CoreVar).
-  Context (hetmet_esc  : CoreVar).
-Axiom FIXME : forall {t}, t.
+  Fixpoint strongExprToWeakExpr (us:UniqSupply){Γ}{Δ}{ξ}{τ}{l}(exp:@Expr _ eqVV Γ Δ ξ τ l)
+    (ite:InstantiatedTypeEnv (fun _ => WeakTypeVar) Γ)
+    : ???WeakExpr :=
+    match exprToWeakExpr (fun v => Error ("unbound variable " +++ toString v)) exp ite with
+      uniqM f => f us >>= fun x => OK (snd x)
+      end.
 
-Fixpoint strongExprToWeakExpr {Γ}{Δ}{ξ}{τ}
-  (ftv:Fresh Kind                (fun _ => WeakTypeVar))
-  (fcv:Fresh (WeakType*WeakType) (fun _ => WeakCoerVar))
-  (exp:@Expr _ CoreVarEqDecidable Γ Δ ξ τ)
-  : InstantiatedTypeEnv (fun _ => WeakTypeVar) Γ -> WeakExpr :=
-match exp as E in @Expr _ _ G D X L return InstantiatedTypeEnv (fun _ => WeakTypeVar) G -> WeakExpr with
-| EVar  Γ' _ ξ' ev              => fun ite => WEVar (weakExprVar ev (@typeToWeakType ftv Γ' ★  (unlev (ξ' ev)) ite))
-| ELit  _ _ _ lit _             => fun ite => WELit lit
-| EApp  Γ' _ _ _ _ _ e1 e2      => fun ite => WEApp (strongExprToWeakExpr ftv fcv e1 ite) (strongExprToWeakExpr ftv fcv e2 ite)
-| ELam  Γ'   _ _ _ t _ cv e     => fun ite => WELam (weakExprVar cv (typeToWeakType ftv t ite)) (strongExprToWeakExpr ftv fcv e ite)
-| ELet  Γ' _ _ t _ _ ev e1 e2   => fun ite => WELet (weakExprVar ev (typeToWeakType ftv t ite)) (strongExprToWeakExpr ftv fcv e1 ite) (strongExprToWeakExpr ftv fcv e2 ite)
-| EEsc  Γ' _ _ ec t _ e         => fun ite => WEEsc  hetmet_esc (ec _ ite) (strongExprToWeakExpr ftv fcv e ite) (typeToWeakType ftv t ite)
-| EBrak Γ' _ _ ec t _ e         => fun ite => WEBrak hetmet_brak (ec _ ite) (strongExprToWeakExpr ftv fcv e ite) (typeToWeakType ftv t ite)
-| ECast Γ Δ ξ t1 t2 γ l e       => fun ite => WECast (strongExprToWeakExpr ftv fcv e ite) (strongCoercionToWeakCoercion γ ite)
-| ENote _ _ _ _ n e             => fun ite => WENote n (strongExprToWeakExpr ftv fcv e ite)
-| ETyApp  Γ Δ κ σ τ ξ l       e => fun ite => WETyApp (strongExprToWeakExpr ftv fcv e ite) (typeToWeakType ftv τ ite)
-| ELetRec _ _ _ _ _ vars elrb e =>fun ite=>WELetRec (exprLetRec2WeakExprLetRec ftv fcv elrb ite)(strongExprToWeakExpr ftv fcv e ite)
-| ECoApp Γ Δ κ σ₁ σ₂ γ σ ξ l e  => fun ite => WECoApp (strongExprToWeakExpr ftv fcv e ite) (strongCoercionToWeakCoercion γ ite)
-| ECase Γ Δ ξ l tc tbranches atypes e alts =>
-  fun ite => WECase
-    (strongExprToWeakExpr ftv fcv e ite)
-    (@typeToWeakType ftv Γ _ tbranches ite)
-    tc
-    (ilist_to_list (@ilmap _ _ (fun _ => WeakType) _ (fun _ t => typeToWeakType ftv t ite) atypes))
-    ((fix caseBranches
-      (tree:Tree ??{ scb : StrongCaseBranchWithVVs _ _ tc atypes
-                            & Expr (sac_Γ scb Γ)
-                                   (sac_Δ scb Γ atypes (weakCK'' Δ))
-                                   (update_ξ (weakLT'○ξ) (vec2list (vec_map
-                                     (fun x => ((fst x),(snd x @@ weakL' l))) (scbwv_varstypes scb))))
-                                   (weakLT' (tbranches@@l)) })
-      : Tree ??(AltCon * list WeakTypeVar * list WeakCoerVar * list WeakExprVar * WeakExpr) :=
-      match tree with
-        | T_Leaf None     => []
-        | T_Leaf (Some x) => let (scb,e) := x in
-          let (ftv',evarsite') := mfresh ftv _ ite in
-          let fcv' :=  fcv in
-            let (evars,ite') := evarsite' in
-            [(sac_altcon scb,
-              vec2list evars,
-              nil (*FIXME*),
-              map (fun vt => weakExprVar (fst vt) (typeToWeakType ftv' (snd vt) ite')) (vec2list (scbwv_varstypes scb)),
-              strongExprToWeakExpr ftv' fcv' e ite'
-            )]
-        | T_Branch b1 b2  => (caseBranches b1),,(caseBranches b2)
-      end
-    ) alts)
-| ETyLam _ _ _ k _ _ e          => fun ite =>
-  let (tv,ftv') := next _ _ ftv k in WETyLam tv (strongExprToWeakExpr ftv' fcv e (updateITE tv ite))
-| ECoLam Γ Δ κ σ σ₁ σ₂ ξ l e => fun ite =>
-  let t1' := typeToWeakType ftv σ₁ ite in 
-  let t2' := typeToWeakType ftv σ₂ ite in
-  let (cv,fcv') := next _ _ fcv (t1',t2') in WECoLam cv (strongExprToWeakExpr ftv fcv' e ite)
-end
-with exprLetRec2WeakExprLetRec {Γ}{Δ}{ξ}{τ}{vars}
-  (ftv:Fresh Kind                (fun _ => WeakTypeVar))
-  (fcv:Fresh (WeakType*WeakType) (fun _ => WeakCoerVar))
-  (elrb:@ELetRecBindings _ CoreVarEqDecidable Γ Δ ξ τ vars)
-  : InstantiatedTypeEnv (fun _ => WeakTypeVar) Γ -> Tree ??(WeakExprVar * WeakExpr) :=
-match elrb as E in ELetRecBindings G D X L V
-   return InstantiatedTypeEnv (fun _ => WeakTypeVar) G -> Tree ??(WeakExprVar * WeakExpr) with
-| ELR_nil    _ _ _ _           => fun ite => []
-| ELR_leaf   _ _ ξ' cv v e    => fun ite => [((weakExprVar v (typeToWeakType ftv (unlev (ξ' v)) ite)),(strongExprToWeakExpr ftv fcv e ite))]
-| ELR_branch _ _ _ _ _ _ b1 b2 => fun ite => (exprLetRec2WeakExprLetRec ftv fcv b1 ite),, (exprLetRec2WeakExprLetRec ftv fcv b2 ite)
-end.
-End strongExprToWeakExpr.
\ No newline at end of file
+End HaskStrongToWeak.