aboutsummaryrefslogtreecommitdiff
path: root/engine
diff options
context:
space:
mode:
Diffstat (limited to 'engine')
-rw-r--r--engine/dune6
-rw-r--r--engine/eConstr.ml22
-rw-r--r--engine/eConstr.mli7
-rw-r--r--engine/evarutil.ml4
-rw-r--r--engine/evd.ml4
-rw-r--r--engine/evd.mli2
-rw-r--r--engine/namegen.ml6
-rw-r--r--engine/proofview.mli2
-rw-r--r--engine/termops.ml42
-rw-r--r--engine/termops.mli4
-rw-r--r--engine/uState.ml20
-rw-r--r--engine/uState.mli2
-rw-r--r--engine/univNames.ml7
13 files changed, 101 insertions, 27 deletions
diff --git a/engine/dune b/engine/dune
new file mode 100644
index 0000000000..e2b7ab9c87
--- /dev/null
+++ b/engine/dune
@@ -0,0 +1,6 @@
+(library
+ (name engine)
+ (synopsis "Coq's Tactic Engine")
+ (public_name coq.engine)
+ (wrapped false)
+ (libraries library))
diff --git a/engine/eConstr.ml b/engine/eConstr.ml
index 3dc1933a14..2913645c1c 100644
--- a/engine/eConstr.ml
+++ b/engine/eConstr.ml
@@ -259,7 +259,17 @@ let decompose_prod_n_assum sigma n c =
let existential_type = Evd.existential_type
-let map sigma f c = match kind sigma c with
+let map_under_context f n c =
+ let f c = unsafe_to_constr (f (of_constr c)) in
+ of_constr (Constr.map_under_context f n (unsafe_to_constr c))
+let map_branches f ci br =
+ let f c = unsafe_to_constr (f (of_constr c)) in
+ of_constr_array (Constr.map_branches f ci (unsafe_to_constr_array br))
+let map_return_predicate f ci p =
+ let f c = unsafe_to_constr (f (of_constr c)) in
+ of_constr (Constr.map_return_predicate f ci (unsafe_to_constr p))
+
+let map_gen userview sigma f c = match kind sigma c with
| (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _
| Construct _) -> c
| Cast (b,k,t) ->
@@ -296,6 +306,12 @@ let map sigma f c = match kind sigma c with
let l' = Array.Smart.map f l in
if l'==l then c
else mkEvar (e, l')
+ | Case (ci,p,b,bl) when userview ->
+ let b' = f b in
+ let p' = map_return_predicate f ci p in
+ let bl' = map_branches f ci bl in
+ if b'==b && p'==p && bl'==bl then c
+ else mkCase (ci, p', b', bl')
| Case (ci,p,b,bl) ->
let b' = f b in
let p' = f p in
@@ -313,6 +329,9 @@ let map sigma f c = match kind sigma c with
if tl'==tl && bl'==bl then c
else mkCoFix (ln,(lna,tl',bl'))
+let map_user_view = map_gen true
+let map = map_gen false
+
let map_with_binders sigma g f l c0 = match kind sigma c0 with
| (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _
| Construct _) -> c0
@@ -794,6 +813,7 @@ struct
let to_sorts = ESorts.unsafe_to_sorts
let to_instance = EInstance.unsafe_to_instance
let to_constr = unsafe_to_constr
+let to_constr_array = unsafe_to_constr_array
let to_rel_decl = unsafe_to_rel_decl
let to_named_decl = unsafe_to_named_decl
let to_named_context =
diff --git a/engine/eConstr.mli b/engine/eConstr.mli
index ecb36615f3..f897448557 100644
--- a/engine/eConstr.mli
+++ b/engine/eConstr.mli
@@ -224,7 +224,11 @@ val compare_constr : Evd.evar_map -> (t -> t -> bool) -> t -> t -> bool
(** {6 Iterators} *)
val map : Evd.evar_map -> (t -> t) -> t -> t
+val map_user_view : Evd.evar_map -> (t -> t) -> t -> t
val map_with_binders : Evd.evar_map -> ('a -> 'a) -> ('a -> t -> t) -> 'a -> t -> t
+val map_under_context : (t -> t) -> int -> t -> t
+val map_branches : (t -> t) -> case_info -> t array -> t array
+val map_return_predicate : (t -> t) -> case_info -> t -> t
val iter : Evd.evar_map -> (t -> unit) -> t -> unit
val iter_with_binders : Evd.evar_map -> ('a -> 'a) -> ('a -> t -> unit) -> 'a -> t -> unit
val iter_with_full_binders : Evd.evar_map -> (rel_declaration -> 'a -> 'a) -> ('a -> t -> unit) -> 'a -> t -> unit
@@ -315,6 +319,9 @@ sig
val to_constr : t -> Constr.t
(** Physical identity. Does not care for defined evars. *)
+ val to_constr_array : t array -> Constr.t array
+ (** Physical identity. Does not care for defined evars. *)
+
val to_rel_decl : (t, types) Context.Rel.Declaration.pt -> (Constr.t, Constr.types) Context.Rel.Declaration.pt
(** Physical identity. Does not care for defined evars. *)
diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index b77bf55d8d..b1d880b0ad 100644
--- a/engine/evarutil.ml
+++ b/engine/evarutil.ml
@@ -284,8 +284,8 @@ type csubst = {
csubst_rev : subst_val Id.Map.t;
(** Reverse mapping of the substitution *)
}
-(** This type represent a name substitution for the named and De Bruijn parts of
- a environment. For efficiency we also store the reverse substitution.
+(** This type represents a name substitution for the named and De Bruijn parts of
+ an environment. For efficiency we also store the reverse substitution.
Invariant: all identifiers in the codomain of [csubst_var] and [csubst_rel]
must be pairwise distinct. *)
diff --git a/engine/evd.ml b/engine/evd.ml
index d1c7fef738..d7b03a84f1 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -774,7 +774,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 rigid evd.universes ctx'}
+ {evd with universes = UState.merge ?loc ~sideff ~extend:true rigid evd.universes ctx'}
let merge_universe_subst evd subst =
{evd with universes = UState.merge_subst evd.universes subst }
@@ -1267,7 +1267,9 @@ module MiniEConstr = struct
let kind_of_type sigma c = Term.kind_of_type (whd_evar sigma c)
let of_kind = Constr.of_kind
let of_constr c = c
+ let of_constr_array v = v
let unsafe_to_constr c = c
+ let unsafe_to_constr_array v = v
let unsafe_eq = Refl
let to_constr ?(abort_on_undefined_evars=true) sigma c =
diff --git a/engine/evd.mli b/engine/evd.mli
index db2bd4eedf..1a5614988d 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -657,10 +657,12 @@ module MiniEConstr : sig
val of_kind : (t, t, ESorts.t, EInstance.t) Constr.kind_of_term -> t
val of_constr : Constr.t -> t
+ val of_constr_array : Constr.t array -> t array
val to_constr : ?abort_on_undefined_evars:bool -> evar_map -> t -> Constr.t
val unsafe_to_constr : t -> Constr.t
+ val unsafe_to_constr_array : t array -> Constr.t array
val unsafe_eq : (t, Constr.t) eq
diff --git a/engine/namegen.ml b/engine/namegen.ml
index 978f33b683..2a59b914db 100644
--- a/engine/namegen.ml
+++ b/engine/namegen.ml
@@ -258,15 +258,15 @@ let restart_subscript id =
forget_subscript id
let visible_ids sigma (nenv, c) =
- let accu = ref (Refset_env.empty, Int.Set.empty, Id.Set.empty) in
+ let accu = ref (GlobRef.Set_env.empty, Int.Set.empty, Id.Set.empty) in
let rec visible_ids n c = match EConstr.kind sigma c with
| Const _ | Ind _ | Construct _ | Var _ as c ->
let (gseen, vseen, ids) = !accu in
let g = global_of_constr c in
- if not (Refset_env.mem g gseen) then
+ if not (GlobRef.Set_env.mem g gseen) then
begin
try
- let gseen = Refset_env.add g gseen in
+ let gseen = GlobRef.Set_env.add g gseen in
let short = shortest_qualid_of_global Id.Set.empty g in
let dir, id = repr_qualid short in
let ids = if DirPath.is_empty dir then Id.Set.add id ids else ids in
diff --git a/engine/proofview.mli b/engine/proofview.mli
index 970bf67732..a9666e4f90 100644
--- a/engine/proofview.mli
+++ b/engine/proofview.mli
@@ -532,7 +532,7 @@ module Goal : sig
(** Compatibility: avoid if possible *)
val goal : t -> Evar.t
- val print : t -> Goal.goal Evd.sigma
+ val print : t -> Evar.t Evd.sigma
end
diff --git a/engine/termops.ml b/engine/termops.ml
index e4c8ae66bc..156d1370e3 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -715,10 +715,26 @@ let map_constr_with_binders_left_to_right sigma g f l c =
then c
else mkCoFix (ln,(lna,tl',bl'))
+let map_under_context_with_full_binders sigma g f l n d =
+ let open EConstr in
+ let f l c = Unsafe.to_constr (f l (of_constr c)) in
+ let g d l = g (of_rel_decl d) l in
+ let d = EConstr.Unsafe.to_constr (EConstr.whd_evar sigma d) in
+ EConstr.of_constr (Constr.map_under_context_with_full_binders g f l n d)
+
+let map_branches_with_full_binders sigma g f l ci bl =
+ let tags = Array.map List.length ci.ci_pp_info.cstr_tags in
+ let bl' = Array.map2 (map_under_context_with_full_binders sigma g f l) tags bl in
+ if Array.for_all2 (==) bl' bl then bl else bl'
+
+let map_return_predicate_with_full_binders sigma g f l ci p =
+ let n = List.length ci.ci_pp_info.ind_tags in
+ let p' = map_under_context_with_full_binders sigma g f l n p in
+ if p' == p then p else p'
+
(* strong *)
-let map_constr_with_full_binders sigma g f l cstr =
+let map_constr_with_full_binders_gen userview sigma g f l cstr =
let open EConstr in
- let open RelDecl in
match EConstr.kind sigma cstr with
| (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _
| Construct _) -> cstr
@@ -728,16 +744,16 @@ let map_constr_with_full_binders sigma g f l cstr =
if c==c' && t==t' then cstr else mkCast (c', k, t')
| Prod (na,t,c) ->
let t' = f l t in
- let c' = f (g (LocalAssum (na, t)) l) c in
+ let c' = f (g (RelDecl.LocalAssum (na, t)) l) c in
if t==t' && c==c' then cstr else mkProd (na, t', c')
| Lambda (na,t,c) ->
let t' = f l t in
- let c' = f (g (LocalAssum (na, t)) l) c in
+ let c' = f (g (RelDecl.LocalAssum (na, t)) l) c in
if t==t' && c==c' then cstr else mkLambda (na, t', c')
| LetIn (na,b,t,c) ->
let b' = f l b in
let t' = f l t in
- let c' = f (g (LocalDef (na, b, t)) l) c in
+ let c' = f (g (RelDecl.LocalDef (na, b, t)) l) c in
if b==b' && t==t' && c==c' then cstr else mkLetIn (na, b', t', c')
| App (c,al) ->
let c' = f l c in
@@ -749,6 +765,12 @@ let map_constr_with_full_binders sigma g f l cstr =
| Evar (e,al) ->
let al' = Array.map (f l) al in
if Array.for_all2 (==) al al' then cstr else mkEvar (e, al')
+ | Case (ci,p,c,bl) when userview ->
+ let p' = map_return_predicate_with_full_binders sigma g f l ci p in
+ let c' = f l c in
+ let bl' = map_branches_with_full_binders sigma g f l ci bl in
+ if p==p' && c==c' && bl'==bl then cstr else
+ mkCase (ci, p', c', bl')
| Case (ci,p,c,bl) ->
let p' = f l p in
let c' = f l c in
@@ -758,7 +780,7 @@ let map_constr_with_full_binders sigma g f l cstr =
| Fix (ln,(lna,tl,bl)) ->
let tl' = Array.map (f l) tl in
let l' =
- Array.fold_left2 (fun l na t -> g (LocalAssum (na, t)) l) l lna tl in
+ Array.fold_left2 (fun l na t -> g (RelDecl.LocalAssum (na, t)) l) l lna tl in
let bl' = Array.map (f l') bl in
if Array.for_all2 (==) tl tl' && Array.for_all2 (==) bl bl'
then cstr
@@ -766,12 +788,18 @@ let map_constr_with_full_binders sigma g f l cstr =
| CoFix(ln,(lna,tl,bl)) ->
let tl' = Array.map (f l) tl in
let l' =
- Array.fold_left2 (fun l na t -> g (LocalAssum (na, t)) l) l lna tl in
+ Array.fold_left2 (fun l na t -> g (RelDecl.LocalAssum (na, t)) l) l lna tl in
let bl' = Array.map (f l') bl in
if Array.for_all2 (==) tl tl' && Array.for_all2 (==) bl bl'
then cstr
else mkCoFix (ln,(lna,tl',bl'))
+let map_constr_with_full_binders sigma g f =
+ map_constr_with_full_binders_gen false sigma g f
+
+let map_constr_with_full_binders_user_view sigma g f =
+ map_constr_with_full_binders_gen true sigma g f
+
(* [fold_constr_with_binders g f n acc c] folds [f n] on the immediate
subterms of [c] starting from [acc] and proceeding from left to
right according to the usual representation of the constructions as
diff --git a/engine/termops.mli b/engine/termops.mli
index 80988989f1..b967bb6abb 100644
--- a/engine/termops.mli
+++ b/engine/termops.mli
@@ -63,6 +63,10 @@ val map_constr_with_full_binders :
Evd.evar_map ->
(rel_declaration -> 'a -> 'a) ->
('a -> constr -> constr) -> 'a -> constr -> constr
+val map_constr_with_full_binders_user_view :
+ Evd.evar_map ->
+ (rel_declaration -> 'a -> 'a) ->
+ ('a -> constr -> constr) -> 'a -> constr -> constr
(** [fold_constr_with_binders g f n acc c] folds [f n] on the immediate
subterms of [c] starting from [acc] and proceeding from left to
diff --git a/engine/uState.ml b/engine/uState.ml
index 0791e4c277..29cb3c9bcc 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -430,10 +430,17 @@ let univ_rigid = UnivRigid
let univ_flexible = UnivFlexible false
let univ_flexible_alg = UnivFlexible true
-let merge ?loc sideff rigid uctx ctx' =
+(** ~sideff indicates that it is ok to redeclare a universe.
+ ~extend also merges the universe context in the local constraint structures
+ and not only in the graph. This depends if the
+ 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 open Univ in
let levels = ContextSet.levels ctx' in
- let uctx = if sideff then uctx else
+ let uctx =
+ if not extend then uctx else
match rigid with
| UnivRigid -> uctx
| UnivFlexible b ->
@@ -448,9 +455,8 @@ let merge ?loc sideff rigid uctx ctx' =
else { uctx with uctx_univ_variables = uvars' }
in
let uctx_local =
- if sideff then uctx.uctx_local
- else ContextSet.append ctx' uctx.uctx_local
- in
+ if not extend then uctx.uctx_local
+ else ContextSet.append ctx' uctx.uctx_local in
let declare g =
LSet.fold (fun u g ->
try UGraph.add_universe u false g
@@ -479,7 +485,7 @@ let merge_subst uctx s =
let emit_side_effects eff u =
let uctxs = Safe_typing.universes_of_private eff in
- List.fold_left (merge true univ_rigid) u uctxs
+ List.fold_left (merge ~sideff:true ~extend:false univ_rigid) u uctxs
let new_univ_variable ?loc rigid name
({ uctx_local = ctx; uctx_univ_variables = uvars; uctx_univ_algebraic = avars} as uctx) =
@@ -668,7 +674,7 @@ let update_sigma_env uctx env =
{ uctx with uctx_initial_universes = univs;
uctx_universes = univs }
in
- merge true univ_rigid eunivs eunivs.uctx_local
+ merge ~sideff:true ~extend:false univ_rigid eunivs eunivs.uctx_local
let pr_weak prl {uctx_weak_constraints=weak} =
let open Pp in
diff --git a/engine/uState.mli b/engine/uState.mli
index a59e61b894..f833508ebf 100644
--- a/engine/uState.mli
+++ b/engine/uState.mli
@@ -103,7 +103,7 @@ val univ_rigid : rigid
val univ_flexible : rigid
val univ_flexible_alg : rigid
-val merge : ?loc:Loc.t -> bool -> rigid -> t -> Univ.ContextSet.t -> t
+val merge : ?loc:Loc.t -> sideff:bool -> extend: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
diff --git a/engine/univNames.ml b/engine/univNames.ml
index a688401741..e861913de2 100644
--- a/engine/univNames.ml
+++ b/engine/univNames.ml
@@ -10,7 +10,6 @@
open Names
open Univ
-open Globnames
open Nametab
@@ -51,15 +50,15 @@ type universe_binders = Univ.Level.t Names.Id.Map.t
let empty_binders = Id.Map.empty
-let universe_binders_table = Summary.ref Refmap.empty ~name:"universe binders"
+let universe_binders_table = Summary.ref GlobRef.Map.empty ~name:"universe binders"
let universe_binders_of_global ref : universe_binders =
try
- let l = Refmap.find ref !universe_binders_table in l
+ let l = GlobRef.Map.find ref !universe_binders_table in l
with Not_found -> Names.Id.Map.empty
let cache_ubinder (_,(ref,l)) =
- universe_binders_table := Refmap.add ref l !universe_binders_table
+ universe_binders_table := GlobRef.Map.add ref l !universe_binders_table
let subst_ubinder (subst,(ref,l as orig)) =
let ref' = fst (Globnames.subst_global subst ref) in
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-02 00:34:33 +0000