aboutsummaryrefslogtreecommitdiff
path: root/engine
diff options
context:
space:
mode:
Diffstat (limited to 'engine')
-rw-r--r--engine/dune6
-rw-r--r--engine/eConstr.ml90
-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/ftactic.ml2
-rw-r--r--engine/ftactic.mli2
-rw-r--r--engine/namegen.ml6
-rw-r--r--engine/proofview.mli4
-rw-r--r--engine/termops.ml55
-rw-r--r--engine/termops.mli38
-rw-r--r--engine/uState.ml20
-rw-r--r--engine/uState.mli2
-rw-r--r--engine/univNames.ml92
-rw-r--r--engine/univNames.mli18
-rw-r--r--engine/universes.ml5
-rw-r--r--engine/universes.mli10
18 files changed, 248 insertions, 119 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..8ab3ce821e 100644
--- a/engine/eConstr.ml
+++ b/engine/eConstr.ml
@@ -14,7 +14,23 @@ open Names
open Constr
open Context
-include Evd.MiniEConstr
+module ESorts = struct
+ include Evd.MiniEConstr.ESorts
+
+ let equal sigma s1 s2 =
+ Sorts.equal (kind sigma s1) (kind sigma s2)
+end
+
+module EInstance = struct
+ include Evd.MiniEConstr.EInstance
+
+ let equal sigma i1 i2 =
+ Univ.Instance.equal (kind sigma i1) (kind sigma i2)
+end
+
+include (Evd.MiniEConstr : module type of Evd.MiniEConstr
+ with module ESorts := ESorts
+ and module EInstance := EInstance)
type types = t
type constr = t
@@ -259,7 +275,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 +322,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 +345,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
@@ -427,23 +462,27 @@ let compare_gen k eq_inst eq_sort eq_constr nargs c1 c2 =
(c1 == c2) || Constr.compare_head_gen_with k k eq_inst eq_sort eq_constr nargs c1 c2
let eq_constr sigma c1 c2 =
- let kind c = kind_upto sigma c in
+ let kind c = kind sigma c in
+ let eq_inst _ _ i1 i2 = EInstance.equal sigma i1 i2 in
+ let eq_sorts s1 s2 = ESorts.equal sigma s1 s2 in
let rec eq_constr nargs c1 c2 =
- compare_gen kind (fun _ _ -> Univ.Instance.equal) Sorts.equal eq_constr nargs c1 c2
+ compare_gen kind eq_inst eq_sorts eq_constr nargs c1 c2
in
- eq_constr 0 (unsafe_to_constr c1) (unsafe_to_constr c2)
+ eq_constr 0 c1 c2
let eq_constr_nounivs sigma c1 c2 =
- let kind c = kind_upto sigma c in
+ let kind c = kind sigma c in
let rec eq_constr nargs c1 c2 =
compare_gen kind (fun _ _ _ _ -> true) (fun _ _ -> true) eq_constr nargs c1 c2
in
- eq_constr 0 (unsafe_to_constr c1) (unsafe_to_constr c2)
+ eq_constr 0 c1 c2
let compare_constr sigma cmp c1 c2 =
- let kind c = kind_upto sigma c in
- let cmp nargs c1 c2 = cmp (of_constr c1) (of_constr c2) in
- compare_gen kind (fun _ _ -> Univ.Instance.equal) Sorts.equal cmp 0 (unsafe_to_constr c1) (unsafe_to_constr c2)
+ let kind c = kind sigma c in
+ let eq_inst _ _ i1 i2 = EInstance.equal sigma i1 i2 in
+ let eq_sorts s1 s2 = ESorts.equal sigma s1 s2 in
+ let cmp nargs c1 c2 = cmp c1 c2 in
+ compare_gen kind eq_inst eq_sorts cmp 0 c1 c2
let compare_cumulative_instances cv_pb nargs_ok variances u u' cstrs =
let open UnivProblem in
@@ -495,10 +534,10 @@ let cmp_constructors (mind, ind, cns as spec) nargs u1 u2 cstrs =
cstrs (Univ.Instance.to_array u1) (Univ.Instance.to_array u2)
let eq_universes env sigma cstrs cv_pb ref nargs l l' =
- if Univ.Instance.is_empty l then (assert (Univ.Instance.is_empty l'); true)
+ if EInstance.is_empty l then (assert (EInstance.is_empty l'); true)
else
- let l = Evd.normalize_universe_instance sigma l
- and l' = Evd.normalize_universe_instance sigma l' in
+ let l = EInstance.kind sigma l
+ and l' = EInstance.kind sigma l' in
let open GlobRef in
let open UnivProblem in
match ref with
@@ -516,7 +555,7 @@ let eq_universes env sigma cstrs cv_pb ref nargs l l' =
let test_constr_universes env sigma leq m n =
let open UnivProblem in
- let kind c = kind_upto sigma c in
+ let kind c = kind sigma c in
if m == n then Some Set.empty
else
let cstrs = ref Set.empty in
@@ -524,16 +563,16 @@ let test_constr_universes env sigma leq m n =
let eq_universes ref nargs l l' = eq_universes env sigma cstrs Reduction.CONV ref nargs l l'
and leq_universes ref nargs l l' = eq_universes env sigma cstrs cv_pb ref nargs l l' in
let eq_sorts s1 s2 =
- let s1 = ESorts.kind sigma (ESorts.make s1) in
- let s2 = ESorts.kind sigma (ESorts.make s2) in
+ let s1 = ESorts.kind sigma s1 in
+ let s2 = ESorts.kind sigma s2 in
if Sorts.equal s1 s2 then true
else (cstrs := Set.add
(UEq (Sorts.univ_of_sort s1,Sorts.univ_of_sort s2)) !cstrs;
true)
in
let leq_sorts s1 s2 =
- let s1 = ESorts.kind sigma (ESorts.make s1) in
- let s2 = ESorts.kind sigma (ESorts.make s2) in
+ let s1 = ESorts.kind sigma s1 in
+ let s2 = ESorts.kind sigma s2 in
if Sorts.equal s1 s2 then true
else
(cstrs := Set.add
@@ -554,16 +593,16 @@ let test_constr_universes env sigma leq m n =
if res then Some !cstrs else None
let eq_constr_universes env sigma m n =
- test_constr_universes env sigma false (unsafe_to_constr m) (unsafe_to_constr n)
+ test_constr_universes env sigma false m n
let leq_constr_universes env sigma m n =
- test_constr_universes env sigma true (unsafe_to_constr m) (unsafe_to_constr n)
+ test_constr_universes env sigma true m n
let compare_head_gen_proj env sigma equ eqs eqc' nargs m n =
- let kind c = kind_upto sigma c in
- match kind_upto sigma m, kind_upto sigma n with
+ let kind c = kind sigma c in
+ match kind m, kind n with
| Proj (p, c), App (f, args)
| App (f, args), Proj (p, c) ->
- (match kind_upto sigma f with
+ (match kind f with
| Const (p', u) when Constant.equal (Projection.constant p) p' ->
let npars = Projection.npars p in
if Array.length args == npars + 1 then
@@ -579,6 +618,8 @@ let eq_constr_universes_proj env sigma m n =
let cstrs = ref Set.empty in
let eq_universes ref l l' = eq_universes env sigma cstrs Reduction.CONV ref l l' in
let eq_sorts s1 s2 =
+ let s1 = ESorts.kind sigma s1 in
+ let s2 = ESorts.kind sigma s2 in
if Sorts.equal s1 s2 then true
else
(cstrs := Set.add
@@ -588,7 +629,7 @@ let eq_constr_universes_proj env sigma m n =
let rec eq_constr' nargs m n =
m == n || compare_head_gen_proj env sigma eq_universes eq_sorts eq_constr' nargs m n
in
- let res = eq_constr' 0 (unsafe_to_constr m) (unsafe_to_constr n) in
+ let res = eq_constr' 0 m n in
if res then Some !cstrs else None
let universes_of_constr sigma c =
@@ -794,6 +835,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/ftactic.ml b/engine/ftactic.ml
index e23a03c0c7..b371884ba4 100644
--- a/engine/ftactic.ml
+++ b/engine/ftactic.ml
@@ -61,7 +61,7 @@ let nf_enter f =
(fun gl ->
gl >>= fun gl ->
Proofview.Goal.normalize gl >>= fun nfgl ->
- Proofview.V82.wrap_exceptions (fun () -> f nfgl))
+ Proofview.V82.wrap_exceptions (fun () -> f nfgl)) [@warning "-3"]
let enter f =
bind goals
diff --git a/engine/ftactic.mli b/engine/ftactic.mli
index 6c389b2d67..3c4fa6f4e8 100644
--- a/engine/ftactic.mli
+++ b/engine/ftactic.mli
@@ -42,6 +42,8 @@ val run : 'a t -> ('a -> unit Proofview.tactic) -> unit Proofview.tactic
(** {5 Focussing} *)
val nf_enter : (Proofview.Goal.t -> 'a t) -> 'a t
+[@@ocaml.deprecated "Normalization is enforced by EConstr, please use [enter]"]
+
(** Enter a goal. The resulting tactic is focussed. *)
val enter : (Proofview.Goal.t -> 'a t) -> 'a t
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..0bb3229a9b 100644
--- a/engine/proofview.mli
+++ b/engine/proofview.mli
@@ -497,6 +497,7 @@ module Goal : sig
(** Normalises the argument goal. *)
val normalize : t -> t tactic
+ [@@ocaml.deprecated "Normalization is enforced by EConstr, [normalize] is not needed anymore"]
(** [concl], [hyps], [env] and [sigma] given a goal [gl] return
respectively the conclusion of [gl], the hypotheses of [gl], the
@@ -514,6 +515,7 @@ module Goal : sig
the current goal is also given as an argument to [t]. The goal
is normalised with respect to evars. *)
val nf_enter : (t -> unit tactic) -> unit tactic
+ [@@ocaml.deprecated "Normalization is enforced by EConstr, please use [enter]"]
(** Like {!nf_enter}, but does not normalize the goal beforehand. *)
val enter : (t -> unit tactic) -> unit tactic
@@ -532,7 +534,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..efe1525c9a 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -22,6 +22,8 @@ module RelDecl = Context.Rel.Declaration
module NamedDecl = Context.Named.Declaration
module CompactedDecl = Context.Compacted.Declaration
+module Internal = struct
+
(* Sorts and sort family *)
let print_sort = function
@@ -49,6 +51,8 @@ let pr_puniverses p u =
if Univ.Instance.is_empty u then p
else p ++ str"(*" ++ Univ.Instance.pr UnivNames.pr_with_global_universes u ++ str"*)"
+(* Minimalistic constr printer, typically for debugging *)
+
let rec pr_constr c = match kind c with
| Rel n -> str "#"++int n
| Meta n -> str "Meta(" ++ int n ++ str ")"
@@ -96,12 +100,16 @@ let rec pr_constr c = match kind c with
cut() ++ str":=" ++ pr_constr bd) (Array.to_list fixl)) ++
str"}")
-let term_printer = ref (fun _env _sigma c -> pr_constr (EConstr.Unsafe.to_constr c))
+let debug_print_constr c = pr_constr EConstr.Unsafe.(to_constr c)
+let debug_print_constr_env env sigma c = pr_constr EConstr.(to_constr sigma c)
+let term_printer = ref debug_print_constr_env
+
let print_constr_env env sigma t = !term_printer env sigma t
let print_constr t =
let env = Global.env () in
let evd = Evd.from_env env in
!term_printer env evd t
+
let set_print_constr f = term_printer := f
module EvMap = Evar.Map
@@ -715,10 +723,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 +752,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 +773,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 +788,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 +796,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
@@ -1507,3 +1543,6 @@ let env_rel_context_chop k env =
let ctx1,ctx2 = List.chop k rels in
push_rel_context ctx2 (reset_with_named_context (named_context_val env) env),
ctx1
+end
+
+include Internal
diff --git a/engine/termops.mli b/engine/termops.mli
index 80988989f1..aa0f837938 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
@@ -307,12 +311,40 @@ val pr_metaset : Metaset.t -> Pp.t
val pr_evar_universe_context : UState.t -> Pp.t
val pr_evd_level : evar_map -> Univ.Level.t -> Pp.t
-(** debug printer: do not use to display terms to the casual user... *)
+module Internal : sig
-val set_print_constr : (env -> Evd.evar_map -> constr -> Pp.t) -> unit
-val print_constr : constr -> Pp.t
+(** NOTE: to print terms you always want to use functions in
+ Printer, not these ones which are for very special cases. *)
+
+(** debug printers: print raw form for terms, both with
+ evar-substitution and without. *)
+val debug_print_constr : constr -> Pp.t
+val debug_print_constr_env : env -> evar_map -> constr -> Pp.t
+
+(** Pretty-printer hook: [print_constr_env env sigma c] will pretty
+ print c if the pretty printing layer has been linked into the Coq
+ binary. *)
val print_constr_env : env -> Evd.evar_map -> constr -> Pp.t
+
+(** [set_print_constr f] sets f to be the pretty printer *)
+val set_print_constr : (env -> Evd.evar_map -> constr -> Pp.t) -> unit
+
+(** Printers for contexts *)
val print_named_context : env -> Pp.t
val pr_rel_decl : env -> Constr.rel_declaration -> Pp.t
val print_rel_context : env -> Pp.t
val print_env : env -> Pp.t
+
+val print_constr : constr -> Pp.t
+[@@deprecated "use print_constr_env"]
+
+end
+
+val print_constr : constr -> Pp.t
+[@@deprecated "use Internal.print_constr_env"]
+
+val print_constr_env : env -> Evd.evar_map -> constr -> Pp.t
+[@@deprecated "use Internal.print_constr_env"]
+
+val print_rel_context : env -> Pp.t
+[@@deprecated "use Internal.print_rel_context"]
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..70cdd3a2db 100644
--- a/engine/univNames.ml
+++ b/engine/univNames.ml
@@ -8,10 +8,9 @@
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
+open Util
open Names
open Univ
-open Globnames
-open Nametab
let qualid_of_level l =
@@ -31,44 +30,48 @@ let pr_with_global_universes l = Libnames.pr_qualid (qualid_of_level l)
(** Global universe information outside the kernel, to handle
polymorphic universe names in sections that have to be discharged. *)
-let universe_map = (Summary.ref UnivIdMap.empty ~name:"global universe info" : bool Nametab.UnivIdMap.t ref)
-
-let add_global_universe u p =
- match Level.name u with
- | Some n -> universe_map := Nametab.UnivIdMap.add n p !universe_map
- | None -> ()
-
-let is_polymorphic l =
- match Level.name l with
- | Some n ->
- (try Nametab.UnivIdMap.find n !universe_map
- with Not_found -> false)
- | None -> false
-
(** Local universe names of polymorphic references *)
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 =
+let universe_binders_of_global ref : Id.t list =
try
- let l = Refmap.find ref !universe_binders_table in l
- with Not_found -> Names.Id.Map.empty
+ let l = GlobRef.Map.find ref !universe_binders_table in l
+ with Not_found -> []
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
if ref == ref' then orig else ref', l
+let name_universe lvl =
+ (** Best-effort naming from the string representation of the level. This is
+ completely hackish and should be solved in upper layers instead. *)
+ Id.of_string_soft (Level.to_string lvl)
+
let discharge_ubinder (_,(ref,l)) =
+ (** Expand polymorphic binders with the section context *)
+ let info = Lib.section_segment_of_reference ref in
+ let sec_inst = Array.to_list (Instance.to_array (info.Lib.abstr_subst)) in
+ let map lvl = match Level.name lvl with
+ | None -> (* Having Prop/Set/Var as section universes makes no sense *)
+ assert false
+ | Some na ->
+ try
+ let qid = Nametab.shortest_qualid_of_universe na in
+ snd (Libnames.repr_qualid qid)
+ with Not_found -> name_universe lvl
+ in
+ let l = List.map map sec_inst @ l in
Some (Lib.discharge_global ref, l)
-let ubinder_obj : GlobRef.t * universe_binders -> Libobject.obj =
+let ubinder_obj : GlobRef.t * Id.t list -> Libobject.obj =
let open Libobject in
declare_object { (default_object "universe binder") with
cache_function = cache_ubinder;
@@ -79,28 +82,35 @@ let ubinder_obj : GlobRef.t * universe_binders -> Libobject.obj =
rebuild_function = (fun x -> x); }
let register_universe_binders ref ubinders =
- (* Add the polymorphic (section) universes *)
- let ubinders = UnivIdMap.fold (fun lvl poly ubinders ->
- let qid = Nametab.shortest_qualid_of_universe lvl in
- let level = Level.make (fst lvl) (snd lvl) in
- if poly then Id.Map.add (snd (Libnames.repr_qualid qid)) level ubinders
- else ubinders)
- !universe_map ubinders
+ (** TODO: change the API to register a [Name.t list] instead. This is the last
+ part of the code that depends on the internal representation of names in
+ abstract contexts, but removing it requires quite a rework of the
+ callers. *)
+ let univs = AUContext.instance (Global.universes_of_global ref) in
+ let revmap = Id.Map.fold (fun id lvl accu -> LMap.add lvl id accu) ubinders LMap.empty in
+ let map lvl =
+ try LMap.find lvl revmap
+ with Not_found -> name_universe lvl
in
- if not (Id.Map.is_empty ubinders)
- then Lib.add_anonymous_leaf (ubinder_obj (ref,ubinders))
+ let ubinders = Array.map_to_list map (Instance.to_array univs) in
+ if not (List.is_empty ubinders) then Lib.add_anonymous_leaf (ubinder_obj (ref, ubinders))
type univ_name_list = Names.lname list
-let universe_binders_with_opt_names ref levels = function
- | None -> universe_binders_of_global ref
+let universe_binders_with_opt_names ref names =
+ let orig = universe_binders_of_global ref in
+ let udecl = match names with
+ | None -> orig
| Some udecl ->
- if Int.equal(List.length levels) (List.length udecl)
- then
- List.fold_left2 (fun acc { CAst.v = na} lvl -> match na with
- | Anonymous -> acc
- | Name na -> Names.Id.Map.add na lvl acc)
- empty_binders udecl levels
- else
+ try
+ List.map2 (fun orig {CAst.v = na} ->
+ match na with
+ | Anonymous -> orig
+ | Name id -> id) orig udecl
+ with Invalid_argument _ ->
+ let len = List.length orig in
CErrors.user_err ~hdr:"universe_binders_with_opt_names"
- Pp.(str "Universe instance should have length " ++ int (List.length levels))
+ Pp.(str "Universe instance should have length " ++ int len)
+ in
+ let fold i acc na = Names.Id.Map.add na (Level.var i) acc in
+ List.fold_left_i fold 0 empty_binders udecl
diff --git a/engine/univNames.mli b/engine/univNames.mli
index 837beac267..bd4062ade4 100644
--- a/engine/univNames.mli
+++ b/engine/univNames.mli
@@ -13,13 +13,6 @@ open Univ
val pr_with_global_universes : Level.t -> Pp.t
val qualid_of_level : Level.t -> Libnames.qualid
-(** Global universe information outside the kernel, to handle
- polymorphic universes in sections that have to be discharged. *)
-val add_global_universe : Level.t -> Decl_kinds.polymorphic -> unit
-
-(** Is [lvl] a global polymorphic universe? (ie section polymorphic universe) *)
-val is_polymorphic : Level.t -> bool
-
(** Local universe name <-> level mapping *)
type universe_binders = Univ.Level.t Names.Id.Map.t
@@ -27,15 +20,14 @@ type universe_binders = Univ.Level.t Names.Id.Map.t
val empty_binders : universe_binders
val register_universe_binders : Names.GlobRef.t -> universe_binders -> unit
-val universe_binders_of_global : Names.GlobRef.t -> universe_binders
type univ_name_list = Names.lname list
-(** [universe_binders_with_opt_names ref u l]
+(** [universe_binders_with_opt_names ref l]
- If [l] is [Some univs] return the universe binders naming the levels of [u] by [univs] (skipping Anonymous).
- May error if the lengths mismatch.
+ If [l] is [Some univs] return the universe binders naming the bound levels
+ of [ref] by [univs] (skipping Anonymous). May error if the lengths mismatch.
- Otherwise return [universe_binders_of_global ref]. *)
+ Otherwise return the bound universe names registered for [ref]. *)
val universe_binders_with_opt_names : Names.GlobRef.t ->
- Univ.Level.t list -> univ_name_list option -> universe_binders
+ univ_name_list option -> universe_binders
diff --git a/engine/universes.ml b/engine/universes.ml
index ee9668433c..5d0157b2db 100644
--- a/engine/universes.ml
+++ b/engine/universes.ml
@@ -19,14 +19,9 @@ type univ_name_list = UnivNames.univ_name_list
let pr_with_global_universes = UnivNames.pr_with_global_universes
let reference_of_level = UnivNames.qualid_of_level
-let add_global_universe = UnivNames.add_global_universe
-
-let is_polymorphic = UnivNames.is_polymorphic
-
let empty_binders = UnivNames.empty_binders
let register_universe_binders = UnivNames.register_universe_binders
-let universe_binders_of_global = UnivNames.universe_binders_of_global
let universe_binders_with_opt_names = UnivNames.universe_binders_with_opt_names
diff --git a/engine/universes.mli b/engine/universes.mli
index ad937471e9..0d3bae4c95 100644
--- a/engine/universes.mli
+++ b/engine/universes.mli
@@ -25,12 +25,6 @@ val pr_with_global_universes : Level.t -> Pp.t
val reference_of_level : Level.t -> Libnames.qualid
[@@ocaml.deprecated "Use [UnivNames.qualid_of_level]"]
-val add_global_universe : Level.t -> Decl_kinds.polymorphic -> unit
-[@@ocaml.deprecated "Use [UnivNames.add_global_universe]"]
-
-val is_polymorphic : Level.t -> bool
-[@@ocaml.deprecated "Use [UnivNames.is_polymorphic]"]
-
type universe_binders = UnivNames.universe_binders
[@@ocaml.deprecated "Use [UnivNames.universe_binders]"]
@@ -39,14 +33,12 @@ val empty_binders : universe_binders
val register_universe_binders : Globnames.global_reference -> universe_binders -> unit
[@@ocaml.deprecated "Use [UnivNames.register_universe_binders]"]
-val universe_binders_of_global : Globnames.global_reference -> universe_binders
-[@@ocaml.deprecated "Use [UnivNames.universe_binders_of_global]"]
type univ_name_list = UnivNames.univ_name_list
[@@ocaml.deprecated "Use [UnivNames.univ_name_list]"]
val universe_binders_with_opt_names : Globnames.global_reference ->
- Univ.Level.t list -> univ_name_list option -> universe_binders
+ univ_name_list option -> universe_binders
[@@ocaml.deprecated "Use [UnivNames.universe_binders_with_opt_names]"]
(** ****** Deprecated: moved to [UnivGen] *)
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-01 05:41:48 +0000