; bind tbranches' = @typeToWeakType Γ _ tbranches ite
; bind escrut' = exprToWeakExpr χ escrut ite
; bind branches' =
- ((fix caseBranches (tree:Tree ??{scb : StrongCaseBranchWithVVs VV _ _ _ & Expr _ _ _ _ })
+ ((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 (scb,e) := x in
+ | 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 _ ★
varstypes)
; let χ' := update_χ' χ exprvars in
bind e'' = exprToWeakExpr χ' e (snd evars_ite)
- ; return [(sac_altcon scb, vec2list (fst evars_ite), nil, (map (@snd _ _) exprvars), e'')]
+ ; 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')
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 e => fun ite => bind t' = typeToWeakType (unlev (ξ' v)) ite
+ | 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')]
Fixpoint strongExprToWeakExpr (us:UniqSupply){Γ}{Δ}{ξ}{τ}(exp:@Expr _ eqVV Γ Δ ξ τ)
(ite:InstantiatedTypeEnv (fun _ => WeakTypeVar) Γ)
: ???WeakExpr :=
- match exprToWeakExpr (fun v => Error ("unbound variable " +++ v)) exp ite with
+ match exprToWeakExpr (fun v => Error ("unbound variable " +++ toString v)) exp ite with
uniqM f => f us >>= fun x => OK (snd x)
end.