- | WECase vscrut e tbranches tc avars alts =>
- mkAvars avars (tyConKind tc) φ >>= fun avars' =>
- weakTypeToType'' φ tbranches ★ >>= fun tbranches' =>
- let ξ' := update_ξ ξ (((vscrut:CoreVar), _ @@lev)::nil) in
-(fix mkTree (t:Tree ??(AltCon*list WeakTypeVar*list WeakCoerVar*list WeakExprVar*WeakExpr)) : ???(Tree
- ??{scb
- : StrongCaseBranchWithVVs CoreVar CoreVarEqDecidable tc avars'
- &
- Expr (sac_Γ scb Γ) (sac_Δ scb Γ avars' (weakCK'' Δ))
- (scbwv_ξ scb ξ' lev) (weakLT' (tbranches' @@ lev))}) :=
- match t with
- | T_Leaf None => OK []
- | T_Leaf (Some (ac,extyvars,coervars,exprvars,ebranch)) =>
- mkStrongAltConPlusJunk' tc ac >>= fun sac =>
- list2vecOrFail (map (fun ev:WeakExprVar => ev:CoreVar) exprvars) _ (fun _ _ => "WECase") >>= fun exprvars' =>
- let scb := @Build_StrongCaseBranchWithVVs CoreVar CoreVarEqDecidable tc Γ avars' sac exprvars' in
- weakExprToStrongExpr (sac_Γ scb Γ) (sac_Δ scb Γ avars' (weakCK'' Δ)) (sacpj_φ sac _ φ) (sacpj_ψ sac _ _ avars' ψ)
- (scbwv_ξ scb ξ' lev) (weakT' tbranches') (weakL' lev) ebranch >>= fun ebranch' =>
- let case_case := tt in OK [ _ ]
- | T_Branch b1 b2 =>
- mkTree b1 >>= fun b1' =>
- mkTree b2 >>= fun b2' =>
- OK (b1',,b2')
- end
-) alts >>= fun tree =>
- weakExprToStrongExpr Γ Δ φ ψ ξ (caseType tc avars') lev e >>= fun e' =>
- castExpr "ECaseScrut" _ (EVar Γ Δ ξ' vscrut) >>= fun evar =>
- castExpr "ECase" _ (ECase Γ Δ ξ' lev tc tbranches' avars' evar tree) >>= fun ecase' =>
- OK (ELet _ _ _ _ _ lev (vscrut:CoreVar) e' ecase')
+ | WECase vscrut ve tbranches tc avars alts =>
+ weakTypeToTypeOfKind φ (vscrut:WeakType) ★ >>= fun tv =>
+ weakExprToStrongExpr Γ Δ φ ψ ξ tv lev ve >>= fun ve' =>
+ let ξ' := update_ξ ξ (((vscrut:CoreVar),tv@@lev)::nil) in
+ mkAvars avars (tyConKind tc) φ >>= fun avars' =>
+ weakTypeToTypeOfKind φ tbranches ★ >>= fun tbranches' =>
+ (fix mkTree (t:Tree ??(WeakAltCon*list WeakTypeVar*list WeakCoerVar*list WeakExprVar*WeakExpr)) : ???(Tree
+ ??{scb : StrongCaseBranchWithVVs CoreVar CoreVarEqDecidable tc avars' &
+ Expr (sac_Γ scb Γ) (sac_Δ scb Γ avars' (weakCK'' Δ))(scbwv_ξ scb ξ' lev)(weakLT' (tbranches' @@ lev))}) :=
+ match t with
+ | T_Leaf None => OK []
+ | T_Leaf (Some (ac,extyvars,coervars,exprvars,ebranch)) =>
+ mkStrongAltConPlusJunk' tc ac >>= fun sac =>
+ list2vecOrFail (map (fun ev:WeakExprVar => ev:CoreVar) exprvars) _ (fun _ _ => "WECase")
+ >>= fun exprvars' =>
+ let scb := @Build_StrongCaseBranchWithVVs CoreVar CoreVarEqDecidable tc Γ avars' sac exprvars' in
+ weakExprToStrongExpr (sac_Γ scb Γ) (sac_Δ scb Γ avars' (weakCK'' Δ)) (sacpj_φ sac _ φ)
+ (sacpj_ψ sac _ _ avars' ψ)
+ (scbwv_ξ scb ξ' lev) (weakT' tbranches') (weakL' lev) ebranch >>= fun ebranch' =>
+ let case_case := tt in OK [ _ ]
+ | T_Branch b1 b2 =>
+ mkTree b1 >>= fun b1' =>
+ mkTree b2 >>= fun b2' =>
+ OK (b1',,b2')
+ end) alts >>= fun tree =>
+ castExpr we "ECaseScrut" _ (EVar Γ Δ ξ' vscrut) >>= fun escrut =>
+ castExpr we "ECase" _ (ECase Γ Δ ξ' lev tc tbranches' avars' escrut tree)
+ >>= fun ecase' => OK (ELet _ _ _ tv _ lev (vscrut:CoreVar) ve' ecase')
+
+
+