diff options
Diffstat (limited to 'engine')
| -rw-r--r-- | engine/namegen.ml | 25 | ||||
| -rw-r--r-- | engine/namegen.mli | 4 | ||||
| -rw-r--r-- | engine/uState.ml | 54 | ||||
| -rw-r--r-- | engine/univMinim.ml | 19 |
4 files changed, 48 insertions, 54 deletions
diff --git a/engine/namegen.ml b/engine/namegen.ml index db72dc8ec3..a67ff6965b 100644 --- a/engine/namegen.ml +++ b/engine/namegen.ml @@ -208,25 +208,18 @@ let it_mkLambda_or_LetIn_name env sigma b hyps = (* Introduce a mode where auto-generated names are mangled to test dependence of scripts on auto-generated names *) -let mangle_names = ref false - -let _ = Goptions.( - declare_bool_option - { optdepr = false; - optname = "mangle auto-generated names"; - optkey = ["Mangle";"Names"]; - optread = (fun () -> !mangle_names); - optwrite = (:=) mangle_names; }) +let get_mangle_names = + Goptions.declare_bool_option_and_ref + ~depr:false + ~name:"mangle auto-generated names" + ~key:["Mangle";"Names"] + ~value:false let mangle_names_prefix = ref (Id.of_string "_0") -let set_prefix x = mangle_names_prefix := forget_subscript x -let set_mangle_names_mode x = begin - set_prefix x; - mangle_names := true - end +let set_prefix x = mangle_names_prefix := forget_subscript x -let _ = Goptions.( +let () = Goptions.( declare_string_option { optdepr = false; optname = "mangled names prefix"; @@ -238,7 +231,7 @@ let _ = Goptions.( with CErrors.UserError _ -> CErrors.user_err Pp.(str ("Not a valid identifier: \"" ^ x ^ "\"."))) end }) -let mangle_id id = if !mangle_names then !mangle_names_prefix else id +let mangle_id id = if get_mangle_names () then !mangle_names_prefix else id (* Looks for next "good" name by lifting subscript *) diff --git a/engine/namegen.mli b/engine/namegen.mli index a53c3a0d1f..3722cbed24 100644 --- a/engine/namegen.mli +++ b/engine/namegen.mli @@ -125,7 +125,3 @@ val rename_bound_vars_as_displayed : val compute_displayed_name_in_gen : (evar_map -> int -> 'a -> bool) -> evar_map -> Id.Set.t -> Name.t -> 'a -> Name.t * Id.Set.t - -val set_mangle_names_mode : Id.t -> unit -(** Turn on mangled names mode and with the given prefix. - @raise UserError if the argument is invalid as an identifier. *) diff --git a/engine/uState.ml b/engine/uState.ml index 5747ae2ad4..6aecc368e6 100644 --- a/engine/uState.ml +++ b/engine/uState.ml @@ -441,11 +441,13 @@ let restrict_universe_context (univs, csts) keep = if LSet.is_empty removed then univs, csts else let allunivs = Constraint.fold (fun (u,_,v) all -> LSet.add u (LSet.add v all)) csts univs in - let g = UGraph.empty_universes in - let g = LSet.fold UGraph.add_universe_unconstrained allunivs g in + let g = UGraph.initial_universes in + let g = LSet.fold (fun v g -> if Level.is_small v then g else UGraph.add_universe v false g) allunivs g in let g = UGraph.merge_constraints csts g in - let allkept = LSet.diff allunivs removed in + let allkept = LSet.union (UGraph.domain UGraph.initial_universes) (LSet.diff allunivs removed) in let csts = UGraph.constraints_for ~kept:allkept g in + let csts = Constraint.filter (fun (l,d,r) -> + not ((Level.is_set l && d == Le) || (Level.is_prop l && d == Lt && Level.is_set r))) csts in (LSet.inter univs keep, csts) let restrict ctx vars = @@ -575,25 +577,33 @@ let add_global_univ uctx u = uctx_universes = univs } let make_flexible_variable ctx ~algebraic u = - let {uctx_local = cstrs; uctx_univ_variables = uvars; uctx_univ_algebraic = avars} = ctx in - let uvars' = Univ.LMap.add u None uvars in - let avars' = - if algebraic then - let uu = Univ.Universe.make u in - let substu_not_alg u' v = - Option.cata (fun vu -> Univ.Universe.equal uu vu && not (Univ.LSet.mem u' avars)) false v - in - let has_upper_constraint () = - Univ.Constraint.exists - (fun (l,d,r) -> d == Univ.Lt && Univ.Level.equal l u) - (Univ.ContextSet.constraints cstrs) - in - if not (Univ.LMap.exists substu_not_alg uvars || has_upper_constraint ()) - then Univ.LSet.add u avars else avars - else avars - in - {ctx with uctx_univ_variables = uvars'; - uctx_univ_algebraic = avars'} + let open Univ in + let {uctx_local = cstrs; uctx_univ_variables = uvars; + uctx_univ_algebraic = avars; uctx_universes=g; } = ctx in + assert (try LMap.find u uvars == None with Not_found -> true); + match UGraph.choose (fun v -> not (Level.equal u v) && (algebraic || not (LSet.mem v avars))) g u with + | Some v -> + let uvars' = LMap.add u (Some (Universe.make v)) uvars in + { ctx with uctx_univ_variables = uvars'; } + | None -> + let uvars' = LMap.add u None uvars in + let avars' = + if algebraic then + let uu = Universe.make u in + let substu_not_alg u' v = + Option.cata (fun vu -> Universe.equal uu vu && not (LSet.mem u' avars)) false v + in + let has_upper_constraint () = + Constraint.exists + (fun (l,d,r) -> d == Lt && Level.equal l u) + (ContextSet.constraints cstrs) + in + if not (LMap.exists substu_not_alg uvars || has_upper_constraint ()) + then LSet.add u avars else avars + else avars + in + {ctx with uctx_univ_variables = uvars'; + uctx_univ_algebraic = avars'} let make_nonalgebraic_variable ctx u = { ctx with uctx_univ_algebraic = Univ.LSet.remove u ctx.uctx_univ_algebraic } diff --git a/engine/univMinim.ml b/engine/univMinim.ml index f10e6d2ec1..e20055b133 100644 --- a/engine/univMinim.ml +++ b/engine/univMinim.ml @@ -12,17 +12,12 @@ open Univ open UnivSubst (* To disallow minimization to Set *) -let set_minimization = ref true -let is_set_minimization () = !set_minimization - -let _ = - Goptions.(declare_bool_option - { optdepr = false; - optname = "minimization to Set"; - optkey = ["Universe";"Minimization";"ToSet"]; - optread = is_set_minimization; - optwrite = (:=) set_minimization }) - +let get_set_minimization = + Goptions.declare_bool_option_and_ref + ~depr:false + ~name:"minimization to Set" + ~key:["Universe";"Minimization";"ToSet"] + ~value:true (** Simplification *) @@ -278,7 +273,7 @@ let normalize_context_set g ctx us algs weak = let smallles, csts = Constraint.partition (fun (l,d,r) -> d == Le && Level.is_small l) csts in - let smallles = if is_set_minimization () + let smallles = if get_set_minimization () then Constraint.filter (fun (l,d,r) -> LSet.mem r ctx) smallles else Constraint.empty in |