Commit 1af04b98 authored by François Bobot's avatar François Bobot
Browse files

term : use MInt.translate to simplify bnd_inst

parent 99d1849f
...@@ -764,7 +764,9 @@ let bnd_find i m = ...@@ -764,7 +764,9 @@ let bnd_find i m =
try Mint.find i m with Not_found -> raise UnboundIndex try Mint.find i m with Not_found -> raise UnboundIndex
let bnd_inst m nv { bv_bound = d ; bv_open = b ; bv_defer = s } = let bnd_inst m nv { bv_bound = d ; bv_open = b ; bv_defer = s } =
let s = Sint.fold (fun i -> Mint.add (i + d) (bnd_find i m)) b s in let m = Mint.inter (fun _ () x -> Some x) b m in
let m = Mint.translate ((+) d) m in
let s = Mint.union (fun _ _ _ -> assert false) m s in
{ bv_bound = d + nv ; bv_open = Sint.empty ; bv_defer = s } { bv_bound = d + nv ; bv_open = Sint.empty ; bv_defer = s }
let rec t_inst m nv t = t_label_copy t (match t.t_node with let rec t_inst m nv t = t_label_copy t (match t.t_node with
......
Supports Markdown
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