Commit f660e98d authored by Andrei Paskevich's avatar Andrei Paskevich
Browse files

Dexpr: rebase "old" in variants to the upper function

parent 791dfe49
......@@ -880,17 +880,27 @@ let add_label ({pvm = pvm; old = old} as env) l =
let ht = Hpv.create 3 in
{ env with old = Mstr.add l (pvm, ht) old }, ht
let create_pre pvm preold old pl =
let pl = List.map to_fmla pl in
let fvs = List.fold_left t_freevars Mvs.empty pl in
let rebase_old pvm preold old fvs =
let rebase v (_,{pv_vs = o}) sbs =
if not (Mvs.mem o fvs) then sbs else match preold with
| Some preold ->
Mvs.add o (t_var (find_old pvm preold v).pv_vs) sbs
| None -> raise (UnboundLabel "'0") in
let sbs = Hpv.fold rebase old Mvs.empty in
Hpv.fold rebase old Mvs.empty
let rebase_pre pvm preold old pl =
let pl = List.map to_fmla pl in
let fvs = List.fold_left t_freevars Mvs.empty pl in
let sbs = rebase_old pvm preold old fvs in
List.map (t_subst sbs) pl
let rebase_variant pvm preold old varl =
let add s (t,_) = t_freevars s t in
let fvs = List.fold_left add Mvs.empty varl in
let sbs = rebase_old pvm preold old fvs in
let conv (t,rel) = t_subst sbs t, rel in
List.map conv varl
let get_oldies old =
Hpv.fold (fun v (_,o) sbs -> Mpv.add o v sbs) old Mpv.empty
......@@ -922,7 +932,7 @@ let cty_of_spec env bl dsp dity =
let dsp = get_later env dsp ty in
let _, eff = effect_of_dspec dsp in
let eff = eff_strong eff in
let p = create_pre env.pvm preold old dsp.ds_pre in
let p = rebase_pre env.pvm preold old dsp.ds_pre in
let q = create_post ty dsp.ds_post in
let xq = create_xpost dsp.ds_xpost in
create_cty bl p q xq (get_oldies old) eff ity
......@@ -1193,7 +1203,8 @@ and lambda uloc env pvl dsp dvl de =
let env, old = add_label env "'0" in
let dsp = get_later env dsp ty in
let dvl = get_later env dvl in
let p = create_pre env.pvm preold old dsp.ds_pre in
let dvl = rebase_variant env.pvm preold old dvl in
let p = rebase_pre env.pvm preold old dsp.ds_pre in
let q = create_post ty dsp.ds_post in
let xq = create_xpost dsp.ds_xpost in
c_fun pvl p q xq (get_oldies old) e, dsp, dvl
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment