diff options
Diffstat (limited to 'engine/uState.ml')
| -rw-r--r-- | engine/uState.ml | 36 |
1 files changed, 24 insertions, 12 deletions
diff --git a/engine/uState.ml b/engine/uState.ml index d532129dc5..00649ce042 100644 --- a/engine/uState.ml +++ b/engine/uState.ml @@ -39,7 +39,7 @@ type t = uctx_weak_constraints : UPairSet.t } -let initial_sprop_cumulative = UGraph.make_sprop_cumulative UGraph.initial_universes +let initial_sprop_cumulative = UGraph.set_cumulative_sprop true UGraph.initial_universes let empty = { uctx_names = UNameMap.empty, LMap.empty; @@ -57,11 +57,11 @@ let elaboration_sprop_cumul = ~key:["Elaboration";"StrictProp";"Cumulativity"] ~value:true let make ~lbound u = - let u = if elaboration_sprop_cumul () then UGraph.make_sprop_cumulative u else u in - { empty with - uctx_universes = u; - uctx_universes_lbound = lbound; - uctx_initial_universes = u} + let u = UGraph.set_cumulative_sprop (elaboration_sprop_cumul ()) u in + { empty with + uctx_universes = u; + uctx_universes_lbound = lbound; + uctx_initial_universes = u} let is_empty ctx = ContextSet.is_empty ctx.uctx_local && @@ -176,8 +176,11 @@ let instantiate_variable l b v = exception UniversesDiffer -let drop_weak_constraints = ref false - +let drop_weak_constraints = + Goptions.declare_bool_option_and_ref + ~depr:false + ~key:["Cumulativity";"Weak";"Constraints"] + ~value:false let process_universe_constraints ctx cstrs = let open UnivSubst in @@ -270,7 +273,7 @@ let process_universe_constraints ctx cstrs = | ULub (l, r) -> equalize_variables true (Universe.make l) l (Universe.make r) r local | UWeak (l, r) -> - if not !drop_weak_constraints then weak := UPairSet.add (l,r) !weak; local + if not (drop_weak_constraints ()) then weak := UPairSet.add (l,r) !weak; local | UEq (l, r) -> equalize_universes l r local in let local = @@ -524,6 +527,14 @@ let demote_seff_univs univs uctx = let seff = LSet.union uctx.uctx_seff_univs univs in { uctx with uctx_seff_univs = seff } +let demote_global_univs env uctx = + let env_ugraph = Environ.universes env in + let global_univs = UGraph.domain env_ugraph in + let global_constraints, _ = UGraph.constraints_of_universes env_ugraph in + let promoted_uctx = + ContextSet.(of_set global_univs |> add_constraints global_constraints) in + { uctx with uctx_local = ContextSet.diff uctx.uctx_local promoted_uctx } + let merge_seff uctx ctx' = let levels = ContextSet.levels ctx' in let declare g = @@ -544,10 +555,11 @@ let emit_side_effects eff u = merge_seff u uctx let update_sigma_env uctx env = - let univs = UGraph.make_sprop_cumulative (Environ.universes env) in + let univs = UGraph.set_cumulative_sprop (elaboration_sprop_cumul()) (Environ.universes env) in let eunivs = - { uctx with uctx_initial_universes = univs; - uctx_universes = univs } + { uctx with + uctx_initial_universes = univs; + uctx_universes = univs } in merge_seff eunivs eunivs.uctx_local |