diff options
Diffstat (limited to 'engine')
| -rw-r--r-- | engine/evarutil.ml | 12 | ||||
| -rw-r--r-- | engine/evd.ml | 13 | ||||
| -rw-r--r-- | engine/evd.mli | 4 | ||||
| -rw-r--r-- | engine/proofview.ml | 2 | ||||
| -rw-r--r-- | engine/uState.ml | 106 | ||||
| -rw-r--r-- | engine/uState.mli | 4 |
6 files changed, 83 insertions, 58 deletions
diff --git a/engine/evarutil.ml b/engine/evarutil.ml index c946125d3f..5444d88e47 100644 --- a/engine/evarutil.ml +++ b/engine/evarutil.ml @@ -661,26 +661,26 @@ let clear_hyps2_in_evi env sigma hyps t concl ids = (* spiwack: a few functions to gather evars on which goals depend. *) let queue_set q is_dependent set = Evar.Set.iter (fun a -> Queue.push (is_dependent,a) q) set -let queue_term evm q is_dependent c = - queue_set q is_dependent (evars_of_term evm c) +let queue_term q is_dependent c = + queue_set q is_dependent (evar_nodes_of_term c) let process_dependent_evar q acc evm is_dependent e = let evi = Evd.find evm e in (* Queues evars appearing in the types of the goal (conclusion, then hypotheses), they are all dependent. *) - queue_term evm q true evi.evar_concl; + queue_term q true evi.evar_concl; List.iter begin fun decl -> let open NamedDecl in - queue_term evm q true (NamedDecl.get_type decl); + queue_term q true (NamedDecl.get_type decl); match decl with | LocalAssum _ -> () - | LocalDef (_,b,_) -> queue_term evm q true b + | LocalDef (_,b,_) -> queue_term q true b end (EConstr.named_context_of_val evi.evar_hyps); match evi.evar_body with | Evar_empty -> if is_dependent then Evar.Map.add e None acc else acc | Evar_defined b -> - let subevars = evars_of_term evm b in + let subevars = evar_nodes_of_term b in (* evars appearing in the definition of an evar [e] are marked as dependent when [e] is dependent itself: if [e] is a non-dependent goal, then, unless they are reach from another diff --git a/engine/evd.ml b/engine/evd.ml index 6a721a1a8a..f051334f69 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -864,7 +864,7 @@ let universe_subst evd = UState.subst evd.universes let merge_context_set ?loc ?(sideff=false) rigid evd ctx' = - {evd with universes = UState.merge ?loc ~sideff ~extend:true rigid evd.universes ctx'} + {evd with universes = UState.merge ?loc ~sideff rigid evd.universes ctx'} let merge_universe_subst evd subst = {evd with universes = UState.merge_subst evd.universes subst } @@ -1403,7 +1403,16 @@ end let evars_of_term evd c = let rec evrec acc c = - match MiniEConstr.kind evd c with + let c = MiniEConstr.whd_evar evd c in + match kind c with + | Evar (n, l) -> Evar.Set.add n (Array.fold_left evrec acc l) + | _ -> Constr.fold evrec acc c + in + evrec Evar.Set.empty c + +let evar_nodes_of_term c = + let rec evrec acc c = + match kind c with | Evar (n, l) -> Evar.Set.add n (Array.fold_left evrec acc l) | _ -> Constr.fold evrec acc c in diff --git a/engine/evd.mli b/engine/evd.mli index 132f7bc745..5ab53947f7 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -509,6 +509,10 @@ val loc_of_conv_pb : evar_map -> evar_constraint -> Loc.t option val evars_of_term : evar_map -> econstr -> Evar.Set.t (** including evars in instances of evars *) +val evar_nodes_of_term : econstr -> Evar.Set.t + (** same as evars_of_term but also including defined evars. + For use in printing dependent evars *) + val evars_of_named_context : evar_map -> (econstr, etypes) Context.Named.pt -> Evar.Set.t val evars_of_filtered_evar_info : evar_map -> evar_info -> Evar.Set.t diff --git a/engine/proofview.ml b/engine/proofview.ml index 1f076470c1..d6f5aab1d1 100644 --- a/engine/proofview.ml +++ b/engine/proofview.ml @@ -1247,7 +1247,7 @@ module V82 = struct let top_evars initial { solution=sigma; } = let evars_of_initial (c,_) = - Evar.Set.elements (Evd.evars_of_term sigma c) + Evar.Set.elements (Evd.evar_nodes_of_term c) in CList.flatten (CList.map evars_of_initial initial) diff --git a/engine/uState.ml b/engine/uState.ml index cb40e6eadd..af714f6282 100644 --- a/engine/uState.ml +++ b/engine/uState.ml @@ -178,6 +178,7 @@ exception UniversesDiffer let drop_weak_constraints = ref false + let process_universe_constraints ctx cstrs = let open UnivSubst in let open UnivProblem in @@ -236,22 +237,21 @@ let process_universe_constraints ctx cstrs = else match cst with | ULe (l, r) -> - if UGraph.check_leq univs l r then - (* Keep Prop/Set <= var around if var might be instantiated by prop or set - later. *) - match Universe.level l, Universe.level r with - | Some l, Some r -> - Constraint.add (l, Le, r) local - | _ -> local - else - begin match Universe.level r with - | None -> user_err Pp.(str "Algebraic universe on the right") - | Some r' -> - if Level.is_small r' then + begin match Univ.Universe.level r with + | None -> + if UGraph.check_leq univs l r then local + else user_err Pp.(str "Algebraic universe on the right") + | Some r' -> + if Level.is_small r' then if not (Universe.is_levels l) - then + then (* l contains a +1 and r=r' small so l <= r impossible *) raise (UniverseInconsistency (Le, l, r, None)) else + if UGraph.check_leq univs l r then match Univ.Universe.level l with + | Some l -> + Univ.Constraint.add (l, Le, r') local + | None -> local + else let levels = Universe.levels l in let fold l' local = let l = Universe.make l' in @@ -260,8 +260,12 @@ let process_universe_constraints ctx cstrs = else raise (UniverseInconsistency (Le, l, r, None)) in LSet.fold fold levels local - else - enforce_leq l r local + else + match Univ.Universe.level l with + | Some l -> + Univ.Constraint.add (l, Le, r') local + | None -> + if UGraph.check_leq univs l r then local else enforce_leq l r local end | ULub (l, r) -> equalize_variables true (Universe.make l) l (Universe.make r) r local @@ -459,14 +463,6 @@ let restrict ctx vars = let uctx' = restrict_universe_context ~lbound:ctx.uctx_universes_lbound ctx.uctx_local vars in { ctx with uctx_local = uctx' } -let demote_seff_univs universes uctx = - let open Entries in - match universes with - | Polymorphic_entry _ -> uctx - | Monomorphic_entry (univs, _) -> - let seff = LSet.union uctx.uctx_seff_univs univs in - { uctx with uctx_seff_univs = seff } - type rigid = | UnivRigid | UnivFlexible of bool (** Is substitution by an algebraic ok? *) @@ -481,10 +477,9 @@ let univ_flexible_alg = UnivFlexible true context we merge comes from a side effect that is already inlined or defined separately. In the later case, there is no extension, see [emit_side_effects] for example. *) -let merge ?loc ~sideff ~extend rigid uctx ctx' = +let merge ?loc ~sideff rigid uctx ctx' = let levels = ContextSet.levels ctx' in let uctx = - if not extend then uctx else match rigid with | UnivRigid -> uctx | UnivFlexible b -> @@ -493,25 +488,23 @@ let merge ?loc ~sideff ~extend rigid uctx ctx' = else LMap.add u None accu in let uvars' = LSet.fold fold levels uctx.uctx_univ_variables in - if b then - { uctx with uctx_univ_variables = uvars'; - uctx_univ_algebraic = LSet.union uctx.uctx_univ_algebraic levels } - else { uctx with uctx_univ_variables = uvars' } + if b then + { uctx with uctx_univ_variables = uvars'; + uctx_univ_algebraic = LSet.union uctx.uctx_univ_algebraic levels } + else { uctx with uctx_univ_variables = uvars' } in - let uctx_local = - if not extend then uctx.uctx_local - else ContextSet.append ctx' uctx.uctx_local in + let uctx_local = ContextSet.append ctx' uctx.uctx_local in let declare g = LSet.fold (fun u g -> - try UGraph.add_universe ~lbound:uctx.uctx_universes_lbound ~strict:false u g - with UGraph.AlreadyDeclared when sideff -> g) - levels g + try UGraph.add_universe ~lbound:uctx.uctx_universes_lbound ~strict:false u g + with UGraph.AlreadyDeclared when sideff -> g) + levels g in let uctx_names = let fold u accu = let modify _ info = match info.uloc with - | None -> { info with uloc = loc } - | Some _ -> info + | None -> { info with uloc = loc } + | Some _ -> info in try LMap.modify u modify accu with Not_found -> LMap.add u { uname = None; uloc = loc } accu @@ -527,9 +520,38 @@ let merge ?loc ~sideff ~extend rigid uctx ctx' = let merge_subst uctx s = { uctx with uctx_univ_variables = LMap.subst_union uctx.uctx_univ_variables s } +let demote_seff_univs (univs,_) uctx = + let seff = LSet.union uctx.uctx_seff_univs univs in + { uctx with uctx_seff_univs = seff } + +let merge_seff uctx ctx' = + let levels = ContextSet.levels ctx' in + let declare g = + LSet.fold (fun u g -> + try UGraph.add_universe ~lbound:uctx.uctx_universes_lbound ~strict:false u g + with UGraph.AlreadyDeclared -> g) + levels g + in + let initial = declare uctx.uctx_initial_universes in + let univs = declare uctx.uctx_universes in + let uctx_universes = UGraph.merge_constraints (ContextSet.constraints ctx') univs in + { uctx with uctx_universes; + uctx_initial_universes = initial } + let emit_side_effects eff u = let uctxs = Safe_typing.universes_of_private eff in - List.fold_left (merge ~sideff:true ~extend:false univ_rigid) u uctxs + List.fold_left (fun u uctx -> + let u = demote_seff_univs uctx u in + merge_seff u uctx) + u uctxs + +let update_sigma_env uctx env = + let univs = UGraph.make_sprop_cumulative (Environ.universes env) in + let eunivs = + { uctx with uctx_initial_universes = univs; + uctx_universes = univs } + in + merge_seff eunivs eunivs.uctx_local let new_univ_variable ?loc rigid name ({ uctx_local = ctx; uctx_univ_variables = uvars; uctx_univ_algebraic = avars} as uctx) = @@ -726,14 +748,6 @@ let minimize uctx = let universe_of_name uctx s = UNameMap.find s (fst uctx.uctx_names) -let update_sigma_env uctx env = - let univs = UGraph.make_sprop_cumulative (Environ.universes env) in - let eunivs = - { uctx with uctx_initial_universes = univs; - uctx_universes = univs } - in - merge ~sideff:true ~extend:false univ_rigid eunivs eunivs.uctx_local - let pr_weak prl {uctx_weak_constraints=weak} = let open Pp in prlist_with_sep fnl (fun (u,v) -> prl u ++ str " ~ " ++ prl v) (UPairSet.elements weak) diff --git a/engine/uState.mli b/engine/uState.mli index 52e48c4eeb..7cb2f49780 100644 --- a/engine/uState.mli +++ b/engine/uState.mli @@ -100,8 +100,6 @@ val restrict_universe_context : lbound:Univ.Level.t -> ContextSet.t -> LSet.t -> universes are preserved. *) val restrict : t -> Univ.LSet.t -> t -val demote_seff_univs : Entries.universes_entry -> t -> t - type rigid = | UnivRigid | UnivFlexible of bool (** Is substitution by an algebraic ok? *) @@ -110,7 +108,7 @@ val univ_rigid : rigid val univ_flexible : rigid val univ_flexible_alg : rigid -val merge : ?loc:Loc.t -> sideff:bool -> extend:bool -> rigid -> t -> Univ.ContextSet.t -> t +val merge : ?loc:Loc.t -> sideff:bool -> rigid -> t -> Univ.ContextSet.t -> t val merge_subst : t -> UnivSubst.universe_opt_subst -> t val emit_side_effects : Safe_typing.private_constants -> t -> t |