diff options
Diffstat (limited to 'engine')
| -rw-r--r-- | engine/evd.ml | 5 | ||||
| -rw-r--r-- | engine/evd.mli | 2 | ||||
| -rw-r--r-- | engine/uState.ml | 29 | ||||
| -rw-r--r-- | engine/uState.mli | 2 | ||||
| -rw-r--r-- | engine/univMinim.ml | 43 |
5 files changed, 32 insertions, 49 deletions
diff --git a/engine/evd.ml b/engine/evd.ml index c570f75c6b..e85cbc96b2 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -987,11 +987,6 @@ let check_constraints evd csts = let fix_undefined_variables evd = { evd with universes = UState.fix_undefined_variables evd.universes } -let refresh_undefined_universes evd = - let uctx', subst = UState.refresh_undefined_univ_variables evd.universes in - let evd' = cmap (subst_univs_level_constr subst) {evd with universes = uctx'} in - evd', subst - let nf_univ_variables evd = let subst, uctx' = UState.normalize_variables evd.universes in let evd' = {evd with universes = uctx'} in diff --git a/engine/evd.mli b/engine/evd.mli index 679173ca72..3f17e63034 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -643,8 +643,6 @@ val nf_univ_variables : evar_map -> evar_map * Univ.universe_subst val fix_undefined_variables : evar_map -> evar_map -val refresh_undefined_universes : evar_map -> evar_map * Univ.universe_level_subst - (** Universe minimization *) val minimize_universes : evar_map -> evar_map diff --git a/engine/uState.ml b/engine/uState.ml index d4cb59da26..ca0a21acf7 100644 --- a/engine/uState.ml +++ b/engine/uState.ml @@ -718,35 +718,6 @@ let fix_undefined_variables uctx = { uctx with univ_variables = vars'; univ_algebraic = algs' } -let refresh_undefined_univ_variables uctx = - let subst, ctx' = UnivGen.fresh_universe_context_set_instance uctx.local in - let subst_fn u = subst_univs_level_level subst u in - let alg = LSet.fold (fun u acc -> LSet.add (subst_fn u) acc) - uctx.univ_algebraic LSet.empty - in - let vars = - LMap.fold - (fun u v acc -> - LMap.add (subst_fn u) - (Option.map (subst_univs_level_universe subst) v) acc) - uctx.univ_variables LMap.empty - in - let weak = UPairSet.fold (fun (u,v) acc -> UPairSet.add (subst_fn u, subst_fn v) acc) uctx.weak_constraints UPairSet.empty in - let lbound = uctx.universes_lbound in - let declare g = LSet.fold (fun u g -> UGraph.add_universe u ~lbound ~strict:false g) - (ContextSet.levels ctx') g in - let initial = declare uctx.initial_universes in - let univs = declare UGraph.initial_universes in - let uctx' = {names = uctx.names; - local = ctx'; - seff_univs = uctx.seff_univs; - univ_variables = vars; univ_algebraic = alg; - universes = univs; - universes_lbound = lbound; - initial_universes = initial; - weak_constraints = weak; } in - uctx', subst - let minimize uctx = let open UnivMinim in let lbound = uctx.universes_lbound in diff --git a/engine/uState.mli b/engine/uState.mli index 45a0f9964e..607c6c9452 100644 --- a/engine/uState.mli +++ b/engine/uState.mli @@ -154,8 +154,6 @@ val abstract_undefined_variables : t -> t val fix_undefined_variables : t -> t -val refresh_undefined_univ_variables : t -> t * Univ.universe_level_subst - (** Universe minimization *) val minimize : t -> t diff --git a/engine/univMinim.ml b/engine/univMinim.ml index 4dd7fe7e70..1c7e716fc2 100644 --- a/engine/univMinim.ml +++ b/engine/univMinim.ml @@ -85,12 +85,33 @@ let lower_of_list l = type lbound = { enforce : bool; alg : bool; lbound: Universe.t; lower : lowermap } -exception Found of Level.t * lowermap -let find_inst insts v = - try LMap.iter (fun k {enforce;alg;lbound=v';lower} -> - if not alg && enforce && Universe.equal v' v then raise (Found (k, lower))) - insts; raise Not_found - with Found (f,l) -> (f,l) +module LBMap : +sig + type t = private { lbmap : lbound LMap.t; lbrev : (Level.t * lowermap) Universe.Map.t } + val empty : t + val add : Level.t -> lbound -> t -> t +end = +struct + type t = { lbmap : lbound LMap.t; lbrev : (Level.t * lowermap) Universe.Map.t } + (* lbrev is uniquely given from lbmap as a partial reverse mapping *) + let empty = { lbmap = LMap.empty; lbrev = Universe.Map.empty } + let add u bnd m = + let lbmap = LMap.add u bnd m.lbmap in + let lbrev = + if not bnd.alg && bnd.enforce then + match Universe.Map.find bnd.lbound m.lbrev with + | (v, _) -> + if Level.compare u v <= 0 then + Universe.Map.add bnd.lbound (u, bnd.lower) m.lbrev + else m.lbrev + | exception Not_found -> + Universe.Map.add bnd.lbound (u, bnd.lower) m.lbrev + else m.lbrev + in + { lbmap; lbrev } +end + +let find_inst insts v = Universe.Map.find v insts.LBMap.lbrev let compute_lbound left = (* The universe variable was not fixed yet. @@ -114,11 +135,11 @@ let instantiate_with_lbound u lbound lower ~alg ~enforce (ctx, us, algs, insts, let inst = Universe.make u in let cstrs' = enforce_leq lbound inst cstrs in (ctx, us, LSet.remove u algs, - LMap.add u {enforce;alg;lbound;lower} insts, cstrs'), + LBMap.add u {enforce;alg;lbound;lower} insts, cstrs'), {enforce; alg; lbound=inst; lower} else (* Actually instantiate *) (Univ.LSet.remove u ctx, Univ.LMap.add u (Some lbound) us, algs, - LMap.add u {enforce;alg;lbound;lower} insts, cstrs), + LBMap.add u {enforce;alg;lbound;lower} insts, cstrs), {enforce; alg; lbound; lower} type constraints_map = (Univ.constraint_type * Univ.LMap.key) list Univ.LMap.t @@ -180,10 +201,10 @@ let minimize_univ_variables ctx us algs left right cstrs = let lbounds = match compute_lbound (List.map (fun (d,l) -> d, Universe.make l) lower) with | None -> lbounds - | Some lbound -> LMap.add r {enforce=true; alg=false; lbound; lower=lower_of_list lower} + | Some lbound -> LBMap.add r {enforce=true; alg=false; lbound; lower=lower_of_list lower} lbounds in (Univ.LMap.remove r left, lbounds)) - left (left, Univ.LMap.empty) + left (left, LBMap.empty) in let rec instance (ctx, us, algs, insts, cstrs as acc) u = let acc, left, lower = @@ -256,7 +277,7 @@ let minimize_univ_variables ctx us algs left right cstrs = with UpperBoundedAlg -> enforce_uppers (acc, {enforce=true; alg=false; lbound=Universe.make u; lower}) and aux (ctx, us, algs, seen, cstrs as acc) u = - try acc, LMap.find u seen + try acc, LMap.find u seen.LBMap.lbmap with Not_found -> instance acc u in LMap.fold (fun u v (ctx, us, algs, seen, cstrs as acc) -> |