diff options
| author |  Matthieu Sozeau <mattam@mattam.org> | 2017-07-31 16:49:06 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <mattam@mattam.org> | 2017-09-19 10:28:03 +0200 |
| commit | 8966c9241207b6f5d4ee38508246ee97ed006e72 (patch) | |
| tree | 774d61f09e653e084c9fc1c1b5fd01996ab09a76 /engine | |
| parent | d9e54d65cc808eab2908beb7a7a2c96005118ace (diff) | |
proof_global: cleanup and comment close_proof
evd: Move constrain_variables to an operation on UState
Necessary to check universe declarations correctly for deferred proofs
in particular.
Diffstat (limited to 'engine')
| -rw-r--r-- | engine/evd.mli | 2 | ||||
| -rw-r--r-- | engine/uState.ml | 28 | ||||
| -rw-r--r-- | engine/uState.mli | 2 |
3 files changed, 20 insertions, 12 deletions
diff --git a/engine/evd.mli b/engine/evd.mli index 76fa69e31..8c3771cd9 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -493,7 +493,7 @@ val empty_evar_universe_context : evar_universe_context val union_evar_universe_context : evar_universe_context -> evar_universe_context -> evar_universe_context val evar_universe_context_subst : evar_universe_context -> Universes.universe_opt_subst -val constrain_variables : Univ.LSet.t -> evar_universe_context -> Univ.constraints +val constrain_variables : Univ.LSet.t -> evar_universe_context -> evar_universe_context val evar_universe_context_of_binders : diff --git a/engine/uState.ml b/engine/uState.ml index 312502491..979a9b086 100644 --- a/engine/uState.ml +++ b/engine/uState.ml @@ -101,16 +101,6 @@ let initial_graph ctx = ctx.uctx_initial_universes let algebraics ctx = ctx.uctx_univ_algebraic -let constrain_variables diff ctx = - Univ.LSet.fold - (fun l cstrs -> - try - match Univ.LMap.find l ctx.uctx_univ_variables with - | Some u -> Univ.Constraint.add (l, Univ.Eq, Option.get (Univ.Universe.level u)) cstrs - | None -> cstrs - with Not_found | Option.IsNone -> cstrs) - diff Univ.Constraint.empty - let add_uctx_names ?loc s l (names, names_rev) = (UNameMap.add s l names, Univ.LMap.add l { uname = Some s; uloc = loc } names_rev) @@ -242,6 +232,24 @@ let add_universe_constraints ctx cstrs = uctx_univ_variables = vars; uctx_universes = UGraph.merge_constraints local' ctx.uctx_universes } +let constrain_variables diff ctx = + let univs, local = ctx.uctx_local in + let univs, vars, local = + Univ.LSet.fold + (fun l (univs, vars, cstrs) -> + try + match Univ.LMap.find l vars with + | Some u -> + (Univ.LSet.add l univs, + Univ.LMap.remove l vars, + Univ.Constraint.add (l, Univ.Eq, Option.get (Univ.Universe.level u)) cstrs) + | None -> (univs, vars, cstrs) + with Not_found | Option.IsNone -> (univs, vars, cstrs)) + diff (univs, ctx.uctx_univ_variables, local) + in + { ctx with uctx_local = (univs, local); uctx_univ_variables = vars } + + let pr_uctx_level uctx = let map, map_rev = uctx.uctx_names in fun l -> diff --git a/engine/uState.mli b/engine/uState.mli index ba0305869..0b67bb71f 100644 --- a/engine/uState.mli +++ b/engine/uState.mli @@ -108,7 +108,7 @@ val is_sort_variable : t -> Sorts.t -> Univ.Level.t option val normalize_variables : t -> Univ.universe_subst * t -val constrain_variables : Univ.LSet.t -> t -> Univ.constraints +val constrain_variables : Univ.LSet.t -> t -> t val abstract_undefined_variables : t -> t |