aboutsummaryrefslogtreecommitdiff
path: root/engine
diff options
context:
space:
mode:
Diffstat (limited to 'engine')
-rw-r--r--engine/evarutil.mli8
-rw-r--r--engine/proofview.ml2
-rw-r--r--engine/termops.ml18
-rw-r--r--engine/termops.mli6
-rw-r--r--engine/univops.ml85
-rw-r--r--engine/univops.mli5
6 files changed, 35 insertions, 89 deletions
diff --git a/engine/evarutil.mli b/engine/evarutil.mli
index f271c14ea2..f83f262b4a 100644
--- a/engine/evarutil.mli
+++ b/engine/evarutil.mli
@@ -264,19 +264,19 @@ val e_new_evar :
?candidates:constr list -> ?store:Store.t ->
?naming:Misctypes.intro_pattern_naming_expr ->
?principal:bool -> ?hypnaming:naming_mode -> types -> constr
-[@@ocaml.deprecated "Use [Evd.new_evar]"]
+[@@ocaml.deprecated "Use [Evarutil.new_evar]"]
val e_new_type_evar : env -> evar_map ref ->
?src:Evar_kinds.t Loc.located -> ?filter:Filter.t ->
?naming:Misctypes.intro_pattern_naming_expr ->
?principal:bool -> ?hypnaming:naming_mode -> rigid -> constr * Sorts.t
-[@@ocaml.deprecated "Use [Evd.new_type_evar]"]
+[@@ocaml.deprecated "Use [Evarutil.new_type_evar]"]
val e_new_Type : ?rigid:rigid -> env -> evar_map ref -> constr
-[@@ocaml.deprecated "Use [Evd.new_Type]"]
+[@@ocaml.deprecated "Use [Evarutil.new_Type]"]
val e_new_global : evar_map ref -> GlobRef.t -> constr
-[@@ocaml.deprecated "Use [Evd.new_global]"]
+[@@ocaml.deprecated "Use [Evarutil.new_global]"]
val e_nf_evars_and_universes : evar_map ref -> (Constr.constr -> Constr.constr) * UnivSubst.universe_opt_subst
[@@ocaml.deprecated "Use Evd.minimize_universes and nf_evars_universes"]
diff --git a/engine/proofview.ml b/engine/proofview.ml
index fdb0a215d3..b4afb6415e 100644
--- a/engine/proofview.ml
+++ b/engine/proofview.ml
@@ -39,7 +39,7 @@ let proofview p =
let compact el ({ solution } as pv) =
let nf c = Evarutil.nf_evar solution c in
- let nf0 c = EConstr.Unsafe.to_constr (Evarutil.nf_evar solution (EConstr.of_constr c)) in
+ let nf0 c = EConstr.(to_constr solution (of_constr c)) in
let size = Evd.fold (fun _ _ i -> i+1) solution 0 in
let new_el = List.map (fun (t,ty) -> nf t, nf ty) el in
let pruned_solution = Evd.drop_all_defined solution in
diff --git a/engine/termops.ml b/engine/termops.ml
index 51fc592897..eacc36107c 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -781,24 +781,23 @@ let map_constr_with_full_binders sigma g f l cstr =
let fold_constr_with_full_binders sigma g f n acc c =
let open RelDecl in
- let inj c = EConstr.Unsafe.to_constr c in
match EConstr.kind sigma c with
| (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _
| Construct _) -> acc
| Cast (c,_, t) -> f n (f n acc c) t
- | Prod (na,t,c) -> f (g (LocalAssum (na, inj t)) n) (f n acc t) c
- | Lambda (na,t,c) -> f (g (LocalAssum (na, inj t)) n) (f n acc t) c
- | LetIn (na,b,t,c) -> f (g (LocalDef (na, inj b, inj t)) n) (f n (f n acc b) t) c
+ | Prod (na,t,c) -> f (g (LocalAssum (na, t)) n) (f n acc t) c
+ | Lambda (na,t,c) -> f (g (LocalAssum (na, t)) n) (f n acc t) c
+ | LetIn (na,b,t,c) -> f (g (LocalDef (na, b, t)) n) (f n (f n acc b) t) c
| App (c,l) -> Array.fold_left (f n) (f n acc c) l
| Proj (p,c) -> f n acc c
| Evar (_,l) -> Array.fold_left (f n) acc l
| Case (_,p,c,bl) -> Array.fold_left (f n) (f n (f n acc p) c) bl
| Fix (_,(lna,tl,bl)) ->
- let n' = CArray.fold_left2 (fun c n t -> g (LocalAssum (n, inj t)) c) n lna tl in
+ let n' = CArray.fold_left2 (fun c n t -> g (LocalAssum (n, t)) c) n lna tl in
let fd = Array.map2 (fun t b -> (t,b)) tl bl in
Array.fold_left (fun acc (t,b) -> f n' (f n acc t) b) acc fd
| CoFix (_,(lna,tl,bl)) ->
- let n' = CArray.fold_left2 (fun c n t -> g (LocalAssum (n, inj t)) c) n lna tl in
+ let n' = CArray.fold_left2 (fun c n t -> g (LocalAssum (n, t)) c) n lna tl in
let fd = Array.map2 (fun t b -> (t,b)) tl bl in
Array.fold_left (fun acc (t,b) -> f n' (f n acc t) b) acc fd
@@ -857,6 +856,13 @@ let occur_meta_or_existential sigma c =
| _ -> EConstr.iter sigma occrec c
in try occrec c; false with Occur -> true
+let occur_metavariable sigma m c =
+ let rec occrec c = match EConstr.kind sigma c with
+ | Meta m' -> if Int.equal m m' then raise Occur
+ | _ -> EConstr.iter sigma occrec c
+ in
+ try occrec c; false with Occur -> true
+
let occur_evar sigma n c =
let rec occur_rec c = match EConstr.kind sigma c with
| Evar (sp,_) when Evar.equal sp n -> raise Occur
diff --git a/engine/termops.mli b/engine/termops.mli
index bb3cbb6a82..2554940314 100644
--- a/engine/termops.mli
+++ b/engine/termops.mli
@@ -75,8 +75,9 @@ val fold_constr_with_binders : Evd.evar_map ->
('a -> 'a) -> ('a -> 'b -> constr -> 'b) -> 'a -> 'b -> constr -> 'b
val fold_constr_with_full_binders : Evd.evar_map ->
- (Context.Rel.Declaration.t -> 'a -> 'a) -> ('a -> 'b -> constr -> 'b) ->
- 'a -> 'b -> constr -> 'b
+ (rel_declaration -> 'a -> 'a) ->
+ ('a -> 'b -> constr -> 'b) ->
+ 'a -> 'b -> constr -> 'b
val iter_constr_with_full_binders : Evd.evar_map ->
(rel_declaration -> 'a -> 'a) ->
@@ -94,6 +95,7 @@ exception Occur
val occur_meta : Evd.evar_map -> constr -> bool
val occur_existential : Evd.evar_map -> constr -> bool
val occur_meta_or_existential : Evd.evar_map -> constr -> bool
+val occur_metavariable : Evd.evar_map -> metavariable -> constr -> bool
val occur_evar : Evd.evar_map -> Evar.t -> constr -> bool
val occur_var : env -> Evd.evar_map -> Id.t -> constr -> bool
val occur_var_in_decl :
diff --git a/engine/univops.ml b/engine/univops.ml
index 76dbaa250a..3fd518490a 100644
--- a/engine/univops.ml
+++ b/engine/univops.ml
@@ -35,79 +35,14 @@ let universes_of_constr env c =
| _ -> Constr.fold aux s c
in aux LSet.empty c
-type graphnode = {
- mutable up : constraint_type LMap.t;
- mutable visited : bool
-}
-
-let merge_types d d0 =
- match d, d0 with
- | _, Lt | Lt, _ -> Lt
- | Le, _ | _, Le -> Le
- | Eq, Eq -> Eq
-
-let merge_up d b up =
- let find = try Some (LMap.find b up) with Not_found -> None in
- match find with
- | Some d0 ->
- let d = merge_types d d0 in
- if d == d0 then up else LMap.add b d up
- | None -> LMap.add b d up
-
-let add_up a d b graph =
- let node, graph =
- try LMap.find a graph, graph
- with Not_found ->
- let node = { up = LMap.empty; visited = false } in
- node, LMap.add a node graph
- in
- node.up <- merge_up d b node.up;
- graph
-
-(* for each node transitive close until you find a non removable, discard the rest *)
-let transitive_close removable graph =
- let rec do_node a node =
- if not node.visited
- then
- let keepup =
- LMap.fold (fun b d keepup ->
- if not (LSet.mem b removable)
- then merge_up d b keepup
- else
- begin
- match LMap.find b graph with
- | bnode ->
- do_node b bnode;
- LMap.fold (fun k d' keepup ->
- merge_up (merge_types d d') k keepup)
- bnode.up keepup
- | exception Not_found -> keepup
- end
- )
- node.up LMap.empty
- in
- node.up <- keepup;
- node.visited <- true
- in
- LMap.iter do_node graph
-
-let restrict_universe_context (univs,csts) keep =
- let removable = LSet.diff univs keep in
- let (csts, rem) =
- Constraint.fold (fun (a,d,b as cst) (csts, rem) ->
- if LSet.mem a removable || LSet.mem b removable
- then (csts, add_up a d b rem)
- else (Constraint.add cst csts, rem))
- csts (Constraint.empty, LMap.empty)
- in
- transitive_close removable rem;
- let csts =
- LMap.fold (fun a node csts ->
- if LSet.mem a removable
- then csts
- else
- LMap.fold (fun b d csts -> Constraint.add (a,d,b) csts)
- node.up csts)
- rem csts
- in
+let restrict_universe_context (univs, csts) keep =
+ let removed = LSet.diff univs keep in
+ 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.merge_constraints csts g in
+ let allkept = LSet.diff allunivs removed in
+ let csts = UGraph.constraints_for ~kept:allkept g in
(LSet.inter univs keep, csts)
diff --git a/engine/univops.mli b/engine/univops.mli
index d1585414c1..0b37ab975d 100644
--- a/engine/univops.mli
+++ b/engine/univops.mli
@@ -14,5 +14,8 @@ open Univ
(** The universes of monomorphic constants appear. *)
val universes_of_constr : Environ.env -> constr -> LSet.t
-(** Shrink a universe context to a restricted set of variables *)
+(** [restrict_universe_context (univs,csts) keep] restricts [univs] to
+ the universes in [keep]. The constraints [csts] are adjusted so
+ that transitive constraints between remaining universes (those in
+ [keep] and those not in [univs]) are preserved. *)
val restrict_universe_context : ContextSet.t -> LSet.t -> ContextSet.t
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-02 04:53:34 +0000