aboutsummaryrefslogtreecommitdiff
path: root/engine
diff options
context:
space:
mode:
Diffstat (limited to 'engine')
-rw-r--r--engine/eConstr.mli12
-rw-r--r--engine/evar_kinds.ml3
-rw-r--r--engine/evarutil.ml8
-rw-r--r--engine/evarutil.mli23
-rw-r--r--engine/namegen.ml12
-rw-r--r--engine/namegen.mli10
-rw-r--r--engine/proofview.ml2
-rw-r--r--engine/termops.ml11
-rw-r--r--engine/termops.mli5
-rw-r--r--engine/uState.ml2
-rw-r--r--engine/uState.mli4
-rw-r--r--engine/univNames.ml2
-rw-r--r--engine/univNames.mli2
13 files changed, 65 insertions, 31 deletions
diff --git a/engine/eConstr.mli b/engine/eConstr.mli
index b0e834b2e7..e9d3e782bc 100644
--- a/engine/eConstr.mli
+++ b/engine/eConstr.mli
@@ -182,9 +182,21 @@ val destCoFix : Evd.evar_map -> t -> (t, t) pcofixpoint
val decompose_app : Evd.evar_map -> t -> t * t list
+(** Pops lambda abstractions until there are no more, skipping casts. *)
val decompose_lam : Evd.evar_map -> t -> (Name.t * t) list * t
+
+(** Pops lambda abstractions and letins until there are no more, skipping casts. *)
val decompose_lam_assum : Evd.evar_map -> t -> rel_context * t
+
+(** Pops [n] lambda abstractions, and pop letins only if needed to
+ expose enough lambdas, skipping casts.
+
+ @raise UserError if the term doesn't have enough lambdas. *)
val decompose_lam_n_assum : Evd.evar_map -> int -> t -> rel_context * t
+
+(** Pops [n] lambda abstractions and letins, skipping casts.
+
+ @raise UserError if the term doesn't have enough lambdas/letins. *)
val decompose_lam_n_decls : Evd.evar_map -> int -> t -> rel_context * t
val compose_lam : (Name.t * t) list -> t -> t
diff --git a/engine/evar_kinds.ml b/engine/evar_kinds.ml
index 6e123d6429..12e2fda8e2 100644
--- a/engine/evar_kinds.ml
+++ b/engine/evar_kinds.ml
@@ -9,7 +9,6 @@
(************************************************************************)
open Names
-open Misctypes
(** The kinds of existential variable *)
@@ -18,7 +17,7 @@ open Misctypes
type obligation_definition_status = Define of bool | Expand
-type matching_var_kind = FirstOrderPatVar of patvar | SecondOrderPatVar of patvar
+type matching_var_kind = FirstOrderPatVar of Id.t | SecondOrderPatVar of Id.t
type subevar_kind = Domain | Codomain | Body
diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index 648f960354..82be4791fc 100644
--- a/engine/evarutil.ml
+++ b/engine/evarutil.ml
@@ -436,12 +436,12 @@ let new_pure_evar_full evd evi =
(evd, evk)
let new_pure_evar?(src=default_source) ?(filter = Filter.identity) ?candidates ?(store = Store.empty) ?naming ?(principal=false) sign evd typ =
- let default_naming = Misctypes.IntroAnonymous in
+ let default_naming = IntroAnonymous in
let naming = Option.default default_naming naming in
let name = match naming with
- | Misctypes.IntroAnonymous -> None
- | Misctypes.IntroIdentifier id -> Some id
- | Misctypes.IntroFresh id ->
+ | IntroAnonymous -> None
+ | IntroIdentifier id -> Some id
+ | IntroFresh id ->
let has_name id = try let _ = Evd.evar_key id evd in true with Not_found -> false in
let id = Namegen.next_ident_away_from id has_name in
Some id
diff --git a/engine/evarutil.mli b/engine/evarutil.mli
index f271c14ea2..c17f3d1683 100644
--- a/engine/evarutil.mli
+++ b/engine/evarutil.mli
@@ -12,6 +12,7 @@ open Names
open Constr
open Evd
open Environ
+open Namegen
open EConstr
(** This module provides useful higher-level functions for evar manipulation. *)
@@ -27,7 +28,7 @@ val mk_new_meta : unit -> constr
val new_evar_from_context :
?src:Evar_kinds.t Loc.located -> ?filter:Filter.t ->
?candidates:constr list -> ?store:Store.t ->
- ?naming:Misctypes.intro_pattern_naming_expr ->
+ ?naming:intro_pattern_naming_expr ->
?principal:bool ->
named_context_val -> evar_map -> types -> evar_map * EConstr.t
@@ -40,14 +41,14 @@ type naming_mode =
val new_evar :
?src:Evar_kinds.t Loc.located -> ?filter:Filter.t ->
?candidates:constr list -> ?store:Store.t ->
- ?naming:Misctypes.intro_pattern_naming_expr ->
+ ?naming:intro_pattern_naming_expr ->
?principal:bool -> ?hypnaming:naming_mode ->
env -> evar_map -> types -> evar_map * EConstr.t
val new_pure_evar :
?src:Evar_kinds.t Loc.located -> ?filter:Filter.t ->
?candidates:constr list -> ?store:Store.t ->
- ?naming:Misctypes.intro_pattern_naming_expr ->
+ ?naming:intro_pattern_naming_expr ->
?principal:bool ->
named_context_val -> evar_map -> types -> evar_map * Evar.t
@@ -57,7 +58,7 @@ val new_pure_evar_full : evar_map -> evar_info -> evar_map * Evar.t
them during type-checking and unification. *)
val new_type_evar :
?src:Evar_kinds.t Loc.located -> ?filter:Filter.t ->
- ?naming:Misctypes.intro_pattern_naming_expr ->
+ ?naming:intro_pattern_naming_expr ->
?principal:bool -> ?hypnaming:naming_mode ->
env -> evar_map -> rigid ->
evar_map * (constr * Sorts.t)
@@ -79,7 +80,7 @@ val new_global : evar_map -> GlobRef.t -> evar_map * constr
as a telescope) is [sign] *)
val new_evar_instance :
?src:Evar_kinds.t Loc.located -> ?filter:Filter.t -> ?candidates:constr list ->
- ?store:Store.t -> ?naming:Misctypes.intro_pattern_naming_expr ->
+ ?store:Store.t -> ?naming:intro_pattern_naming_expr ->
?principal:bool ->
named_context_val -> evar_map -> types ->
constr list -> evar_map * constr
@@ -262,21 +263,21 @@ val meta_counter_summary_tag : int Summary.Dyn.tag
val e_new_evar :
env -> evar_map ref -> ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t ->
?candidates:constr list -> ?store:Store.t ->
- ?naming:Misctypes.intro_pattern_naming_expr ->
+ ?naming: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 ->
+ ?naming: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/namegen.ml b/engine/namegen.ml
index c069ec5a06..23c6911396 100644
--- a/engine/namegen.ml
+++ b/engine/namegen.ml
@@ -29,6 +29,18 @@ open Context.Rel.Declaration
module RelDecl = Context.Rel.Declaration
+(** General evar naming using intro patterns *)
+type intro_pattern_naming_expr =
+ | IntroIdentifier of Id.t
+ | IntroFresh of Id.t
+ | IntroAnonymous
+
+let intro_pattern_naming_eq nam1 nam2 = match nam1, nam2 with
+| IntroAnonymous, IntroAnonymous -> true
+| IntroIdentifier id1, IntroIdentifier id2 -> Names.Id.equal id1 id2
+| IntroFresh id1, IntroFresh id2 -> Names.Id.equal id1 id2
+| _ -> false
+
(**********************************************************************)
(* Conventional names *)
diff --git a/engine/namegen.mli b/engine/namegen.mli
index 1b70ef68dd..a53c3a0d1f 100644
--- a/engine/namegen.mli
+++ b/engine/namegen.mli
@@ -15,6 +15,16 @@ open Environ
open Evd
open EConstr
+(** General evar naming using intro patterns *)
+type intro_pattern_naming_expr =
+ | IntroIdentifier of Id.t
+ | IntroFresh of Id.t
+ | IntroAnonymous
+
+(** Equalities on [intro_pattern_naming] *)
+val intro_pattern_naming_eq :
+ intro_pattern_naming_expr -> intro_pattern_naming_expr -> bool
+
(*********************************************************************
Conventional default names *)
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 0c567754ad..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
diff --git a/engine/termops.mli b/engine/termops.mli
index 6e63539ca3..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) ->
diff --git a/engine/uState.ml b/engine/uState.ml
index 643c621fd5..0e3ecdbf5f 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -312,7 +312,7 @@ type ('a, 'b) gen_universe_decl = {
univdecl_extensible_constraints : bool (* Can new constraints be added *) }
type universe_decl =
- (Misctypes.lident list, Univ.Constraint.t) gen_universe_decl
+ (lident list, Univ.Constraint.t) gen_universe_decl
let default_univ_decl =
{ univdecl_instance = [];
diff --git a/engine/uState.mli b/engine/uState.mli
index e2f25642e5..e7e5b39e09 100644
--- a/engine/uState.mli
+++ b/engine/uState.mli
@@ -26,7 +26,7 @@ val empty : t
val make : UGraph.t -> t
-val make_with_initial_binders : UGraph.t -> Misctypes.lident list -> t
+val make_with_initial_binders : UGraph.t -> lident list -> t
val is_empty : t -> bool
@@ -145,7 +145,7 @@ type ('a, 'b) gen_universe_decl = {
univdecl_extensible_constraints : bool (* Can new constraints be added *) }
type universe_decl =
- (Misctypes.lident list, Univ.Constraint.t) gen_universe_decl
+ (lident list, Univ.Constraint.t) gen_universe_decl
val default_univ_decl : universe_decl
diff --git a/engine/univNames.ml b/engine/univNames.ml
index 6e59a7c9e6..6ffb4bcf0d 100644
--- a/engine/univNames.ml
+++ b/engine/univNames.ml
@@ -89,7 +89,7 @@ let register_universe_binders ref ubinders =
if not (Id.Map.is_empty ubinders)
then Lib.add_anonymous_leaf (ubinder_obj (ref,ubinders))
-type univ_name_list = Misctypes.lname list
+type univ_name_list = Names.lname list
let universe_binders_with_opt_names ref levels = function
| None -> universe_binders_of_global ref
diff --git a/engine/univNames.mli b/engine/univNames.mli
index e3bc3193d8..c19aa19d50 100644
--- a/engine/univNames.mli
+++ b/engine/univNames.mli
@@ -29,7 +29,7 @@ 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 = Misctypes.lname list
+type univ_name_list = Names.lname list
(** [universe_binders_with_opt_names ref u l]
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-29 22:49:56 +0000