aboutsummaryrefslogtreecommitdiff
path: root/engine
diff options
context:
space:
mode:
Diffstat (limited to 'engine')
-rw-r--r--engine/eConstr.ml1
-rw-r--r--engine/evarutil.ml16
-rw-r--r--engine/evd.ml14
-rw-r--r--engine/evd.mli4
-rw-r--r--engine/ftactic.ml4
-rw-r--r--engine/logic_monad.ml2
-rw-r--r--engine/logic_monad.mli5
-rw-r--r--engine/namegen.ml2
-rw-r--r--engine/nameops.mli1
-rw-r--r--engine/proofview.ml14
-rw-r--r--engine/proofview.mli7
-rw-r--r--engine/termops.ml22
-rw-r--r--engine/uState.ml6
-rw-r--r--engine/univMinim.ml15
-rw-r--r--engine/univNames.ml4
15 files changed, 66 insertions, 51 deletions
diff --git a/engine/eConstr.ml b/engine/eConstr.ml
index 96f1ce5e60..24d161d00a 100644
--- a/engine/eConstr.ml
+++ b/engine/eConstr.ml
@@ -606,6 +606,7 @@ let subst_var subst c = of_constr (Vars.subst_var subst (to_constr c))
let subst_univs_level_constr subst c =
of_constr (Vars.subst_univs_level_constr subst (to_constr c))
+
(** Operations that dot NOT commute with evar-normalization *)
let noccurn sigma n term =
let rec occur_rec n c = match kind sigma c with
diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index 69ee5223c4..db56d0628f 100644
--- a/engine/evarutil.ml
+++ b/engine/evarutil.ml
@@ -155,7 +155,7 @@ let is_ground_env = memo is_ground_env
exception NoHeadEvar
let head_evar sigma c =
- (** FIXME: this breaks if using evar-insensitive code *)
+ (* FIXME: this breaks if using evar-insensitive code *)
let c = EConstr.Unsafe.to_constr c in
let rec hrec c = match kind c with
| Evar (evk,_) -> evk
@@ -288,7 +288,7 @@ let empty_csubst = {
}
let csubst_subst { csubst_len = k; csubst_var = v; csubst_rel = s } c =
- (** Safe because this is a substitution *)
+ (* Safe because this is a substitution *)
let c = EConstr.Unsafe.to_constr c in
let rec subst n c = match Constr.kind c with
| Rel m ->
@@ -318,7 +318,7 @@ let update_var src tgt subst =
in
match cur with
| None ->
- (** Missing keys stand for identity substitution [src ↦ src] *)
+ (* Missing keys stand for identity substitution [src ↦ src] *)
let csubst_var = Id.Map.add src (Constr.mkVar tgt) subst.csubst_var in
let csubst_rev = Id.Map.add tgt (SVar src) subst.csubst_rev in
{ subst with csubst_var; csubst_rev }
@@ -366,8 +366,8 @@ let push_rel_decl_to_named_context
about this whole name generation problem. *)
if Flags.is_program_mode () then next_name_away na avoid
else
- (** id_of_name_using_hdchar only depends on the rel context which is empty
- here *)
+ (* id_of_name_using_hdchar only depends on the rel context which is empty
+ here *)
next_ident_away (id_of_name_using_hdchar empty_env sigma (RelDecl.get_type decl) na) avoid
in
match extract_if_neq id na with
@@ -540,8 +540,8 @@ let restrict_evar evd evk filter ?src candidates =
| Some [] -> raise (ClearDependencyError (*FIXME*)(Id.of_string "blah", (NoCandidatesLeft evk), None))
| _ ->
let evd, evk' = Evd.restrict evk filter ?candidates ?src evd in
- (** Mark new evar as future goal, removing previous one,
- circumventing Proofview.advance but making Proof.run_tactic catch these. *)
+ (* Mark new evar as future goal, removing previous one,
+ circumventing Proofview.advance but making Proof.run_tactic catch these. *)
let future_goals = Evd.save_future_goals evd in
let future_goals = Evd.filter_future_goals (fun evk' -> not (Evar.equal evk evk')) future_goals in
let evd = Evd.restore_future_goals evd future_goals in
@@ -779,7 +779,7 @@ let cached_evar_of_hyp cache sigma decl accu = match cache with
let r =
try Id.Map.find id cache.cache
with Not_found ->
- (** Dummy value *)
+ (* Dummy value *)
let r = ref (NamedDecl.LocalAssum (id, EConstr.mkProp), Evar.Set.empty) in
let () = cache.cache <- Id.Map.add id r cache.cache in
r
diff --git a/engine/evd.ml b/engine/evd.ml
index 6345046431..7bc3be87a4 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -89,8 +89,8 @@ struct
| Some f2 -> normalize (CList.filter_with f1 f2)
let apply_subfilter_array filter subfilter =
- (** In both cases we statically know that the argument will contain at
- least one [false] *)
+ (* In both cases we statically know that the argument will contain at
+ least one [false] *)
match filter with
| None -> Some (Array.to_list subfilter)
| Some f ->
@@ -395,7 +395,7 @@ let rename evk id (evtoid, idtoev) =
let reassign_name_defined evk evk' (evtoid, idtoev as names) =
let id = try Some (EvMap.find evk evtoid) with Not_found -> None in
match id with
- | None -> names (** evk' must not be defined *)
+ | None -> names (* evk' must not be defined *)
| Some id ->
(EvMap.add evk' id (EvMap.remove evk evtoid),
Id.Map.add id evk' (Id.Map.remove id idtoev))
@@ -416,7 +416,7 @@ type evar_flags =
typeclass_evars : Evar.Set.t }
type evar_map = {
- (** Existential variables *)
+ (* Existential variables *)
defn_evars : evar_info EvMap.t;
undf_evars : evar_info EvMap.t;
evar_names : EvNames.t;
@@ -520,7 +520,7 @@ let inherit_evar_flags evar_flags evk evk' =
let remove_evar_flags evk evar_flags =
{ typeclass_evars = Evar.Set.remove evk evar_flags.typeclass_evars;
obligation_evars = Evar.Set.remove evk evar_flags.obligation_evars;
- (** Restriction information is kept. *)
+ (* Restriction information is kept. *)
restricted_evars = evar_flags.restricted_evars }
(** New evars *)
@@ -1341,14 +1341,14 @@ module MiniEConstr = struct
| None -> c
end
| App (f, args) when isEvar f ->
- (** Enforce smart constructor invariant on applications *)
+ (* Enforce smart constructor invariant on applications *)
let ev = destEvar f in
begin match safe_evar_value sigma ev with
| None -> c
| Some f -> whd_evar sigma (mkApp (f, args))
end
| Cast (c0, k, t) when isEvar c0 ->
- (** Enforce smart constructor invariant on casts. *)
+ (* Enforce smart constructor invariant on casts. *)
let ev = destEvar c0 in
begin match safe_evar_value sigma ev with
| None -> c
diff --git a/engine/evd.mli b/engine/evd.mli
index 0a8d1f3287..7560d68805 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -86,7 +86,7 @@ type evar_body =
type evar_info = {
evar_concl : econstr;
(** Type of the evar. *)
- evar_hyps : named_context_val; (** TODO econstr? *)
+ evar_hyps : named_context_val; (* TODO econstr? *)
(** Context of the evar. *)
evar_body : evar_body;
(** Optional content of the evar. *)
@@ -546,6 +546,7 @@ val univ_flexible_alg : rigid
type 'a in_evar_universe_context = 'a * UState.t
val restrict_universe_context : evar_map -> Univ.LSet.t -> evar_map
+
(** Raises Not_found if not a name for a universe in this map. *)
val universe_of_name : evar_map -> Id.t -> Univ.Level.t
@@ -567,6 +568,7 @@ val make_nonalgebraic_variable : evar_map -> Univ.Level.t -> evar_map
val is_sort_variable : evar_map -> Sorts.t -> Univ.Level.t option
(** [is_sort_variable evm s] returns [Some u] or [None] if [s] is
not a local sort variable declared in [evm] *)
+
val is_flexible_level : evar_map -> Univ.Level.t -> bool
(* val normalize_universe_level : evar_map -> Univ.Level.t -> Univ.Level.t *)
diff --git a/engine/ftactic.ml b/engine/ftactic.ml
index b371884ba4..ac0344148a 100644
--- a/engine/ftactic.ml
+++ b/engine/ftactic.ml
@@ -29,8 +29,8 @@ let bind (type a) (type b) (m : a t) (f : a -> b t) : b t = m >>= function
| Depends l ->
let f arg = f arg >>= function
| Uniform x ->
- (** We dispatch the uniform result on each goal under focus, as we know
- that the [m] argument was actually dependent. *)
+ (* We dispatch the uniform result on each goal under focus, as we know
+ that the [m] argument was actually dependent. *)
Proofview.Goal.goals >>= fun goals ->
let ans = List.map (fun g -> (g,x)) goals in
Proofview.tclUNIT ans
diff --git a/engine/logic_monad.ml b/engine/logic_monad.ml
index 4afa817b27..e0c24f049f 100644
--- a/engine/logic_monad.ml
+++ b/engine/logic_monad.ml
@@ -28,8 +28,10 @@
from the IO monad ([Proofview] catches errors in its compatibility
layer, and when lifting goal-level expressions). *)
exception Exception of exn
+
(** This exception is used to signal abortion in [timeout] functions. *)
exception Timeout
+
(** This exception is used by the tactics to signal failure by lack of
successes, rather than some other exceptions (like system
interrupts). *)
diff --git a/engine/logic_monad.mli b/engine/logic_monad.mli
index 545334ce9a..3e57baab26 100644
--- a/engine/logic_monad.mli
+++ b/engine/logic_monad.mli
@@ -28,8 +28,10 @@
from the IO monad ([Proofview] catches errors in its compatibility
layer, and when lifting goal-level expressions). *)
exception Exception of exn
+
(** This exception is used to signal abortion in [timeout] functions. *)
exception Timeout
+
(** This exception is used by the tactics to signal failure by lack of
successes, rather than some other exceptions (like system
interrupts). *)
@@ -51,8 +53,10 @@ module NonLogical : sig
val ref : 'a -> 'a ref t
(** [Pervasives.(:=)] *)
+
val (:=) : 'a ref -> 'a -> unit t
(** [Pervasives.(!)] *)
+
val (!) : 'a ref -> 'a t
val read_line : string t
@@ -67,6 +71,7 @@ module NonLogical : sig
(** [Pervasives.raise]. Except that exceptions are wrapped with
{!Exception}. *)
val raise : ?info:Exninfo.info -> exn -> 'a t
+
(** [try ... with ...] but restricted to {!Exception}. *)
val catch : 'a t -> (Exninfo.iexn -> 'a t) -> 'a t
val timeout : int -> 'a t -> 'a t
diff --git a/engine/namegen.ml b/engine/namegen.ml
index a67ff6965b..018eca1ba2 100644
--- a/engine/namegen.ml
+++ b/engine/namegen.ml
@@ -358,7 +358,7 @@ let next_name_away_with_default_using_types default na avoid t =
let next_name_away = next_name_away_with_default default_non_dependent_string
let make_all_name_different env sigma =
- (** FIXME: this is inefficient, but only used in printing *)
+ (* FIXME: this is inefficient, but only used in printing *)
let avoid = ref (ids_of_named_context_val (named_context_val env)) in
let sign = named_context_val env in
let rels = rel_context env in
diff --git a/engine/nameops.mli b/engine/nameops.mli
index 8a93fad8cc..a5308904f5 100644
--- a/engine/nameops.mli
+++ b/engine/nameops.mli
@@ -16,6 +16,7 @@ val make_ident : string -> int option -> Id.t
val repr_ident : Id.t -> string * int option
val atompart_of_id : Id.t -> string (** remove trailing digits *)
+
val root_of_id : Id.t -> Id.t (** remove trailing digits, ' and _ *)
val add_suffix : Id.t -> string -> Id.t
diff --git a/engine/proofview.ml b/engine/proofview.ml
index 304b2dff84..8c15579bb0 100644
--- a/engine/proofview.ml
+++ b/engine/proofview.ml
@@ -660,9 +660,9 @@ let unifiable_delayed g l =
let free_evars sigma l =
let cache = Evarutil.create_undefined_evars_cache () in
let map ev =
- (** Computes the set of evars appearing in the hypotheses, the conclusion or
- the body of the evar_info [evi]. Note: since we want to use it on goals,
- the body is actually supposed to be empty. *)
+ (* Computes the set of evars appearing in the hypotheses, the conclusion or
+ the body of the evar_info [evi]. Note: since we want to use it on goals,
+ the body is actually supposed to be empty. *)
let evi = Evd.find sigma ev in
let fevs = lazy (Evarutil.filtered_undefined_evars_of_evar_info ~cache sigma evi) in
(ev, fevs)
@@ -672,9 +672,9 @@ let free_evars sigma l =
let free_evars_with_state sigma l =
let cache = Evarutil.create_undefined_evars_cache () in
let map ev =
- (** Computes the set of evars appearing in the hypotheses, the conclusion or
- the body of the evar_info [evi]. Note: since we want to use it on goals,
- the body is actually supposed to be empty. *)
+ (* Computes the set of evars appearing in the hypotheses, the conclusion or
+ the body of the evar_info [evi]. Note: since we want to use it on goals,
+ the body is actually supposed to be empty. *)
let ev = drop_state ev in
let evi = Evd.find sigma ev in
let fevs = lazy (Evarutil.filtered_undefined_evars_of_evar_info ~cache sigma evi) in
@@ -1157,7 +1157,7 @@ module Goal = struct
let sigma = step.solution in
let map goal =
match cleared_alias sigma goal with
- | None -> None (** ppedrot: Is this check really necessary? *)
+ | None -> None (* ppedrot: Is this check really necessary? *)
| Some goal ->
let gl =
Env.get >>= fun env ->
diff --git a/engine/proofview.mli b/engine/proofview.mli
index cda4808a23..28e793f0fc 100644
--- a/engine/proofview.mli
+++ b/engine/proofview.mli
@@ -398,6 +398,7 @@ val tclPROGRESS : 'a tactic -> 'a tactic
val tclCHECKINTERRUPT : unit tactic
exception Timeout
+
(** [tclTIMEOUT n t] can have only one success.
In case of timeout if fails with [tclZERO Timeout]. *)
val tclTIMEOUT : int -> 'a tactic -> 'a tactic
@@ -517,8 +518,8 @@ module Goal : sig
(** Like {!nf_enter}, but does not normalize the goal beforehand. *)
val enter : (t -> unit tactic) -> unit tactic
- (** Like {!enter}, but assumes exactly one goal under focus, raising *)
- (** a fatal error otherwise. *)
+ (** Like {!enter}, but assumes exactly one goal under focus, raising
+ a fatal error otherwise. *)
val enter_one : ?__LOC__:string -> (t -> 'a tactic) -> 'a tactic
(** Recover the list of current goals under focus, without evar-normalization.
@@ -612,8 +613,10 @@ module Notations : sig
(** {!tclBIND} *)
val (>>=) : 'a tactic -> ('a -> 'b tactic) -> 'b tactic
+
(** {!tclTHEN} *)
val (<*>) : unit tactic -> 'a tactic -> 'a tactic
+
(** {!tclOR}: [t1+t2] = [tclOR t1 (fun _ -> t2)]. *)
val (<+>) : 'a tactic -> 'a tactic -> 'a tactic
diff --git a/engine/termops.ml b/engine/termops.ml
index 98300764df..137770d8f0 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -197,8 +197,8 @@ let compute_evar_dependency_graph sigma =
let evar_dependency_closure n sigma =
let open Evd in
- (** Create the DAG of depth [n] representing the recursive dependencies of
- undefined evars. *)
+ (* Create the DAG of depth [n] representing the recursive dependencies of
+ undefined evars. *)
let graph = compute_evar_dependency_graph sigma in
let rec aux n curr accu =
if Int.equal n 0 then Evar.Set.union curr accu
@@ -209,9 +209,9 @@ let evar_dependency_closure n sigma =
Evar.Set.union deps accu
with Not_found -> accu
in
- (** Consider only the newly added evars *)
+ (* Consider only the newly added evars *)
let ncurr = Evar.Set.fold fold curr Evar.Set.empty in
- (** Merge the others *)
+ (* Merge the others *)
let accu = Evar.Set.union curr accu in
aux (n - 1) ncurr accu
in
@@ -261,13 +261,13 @@ let print_env_short env sigma =
let pr_evar_constraints sigma pbs =
let pr_evconstr (pbty, env, t1, t2) =
let env =
- (** We currently allow evar instances to refer to anonymous de
- Bruijn indices, so we protect the error printing code in this
- case by giving names to every de Bruijn variable in the
- rel_context of the conversion problem. MS: we should rather
- stop depending on anonymous variables, they can be used to
- indicate independency. Also, this depends on a strategy for
- naming/renaming. *)
+ (* We currently allow evar instances to refer to anonymous de
+ Bruijn indices, so we protect the error printing code in this
+ case by giving names to every de Bruijn variable in the
+ rel_context of the conversion problem. MS: we should rather
+ stop depending on anonymous variables, they can be used to
+ indicate independency. Also, this depends on a strategy for
+ naming/renaming. *)
Namegen.make_all_name_different env sigma
in
print_env_short env sigma ++ spc () ++ str "|-" ++ spc () ++
diff --git a/engine/uState.ml b/engine/uState.ml
index 185283225c..6969d2ba44 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -197,7 +197,7 @@ let process_universe_constraints ctx cstrs =
| Some l -> Inr l
in
let equalize_variables fo l l' r r' local =
- (** Assumes l = [l',0] and r = [r',0] *)
+ (* Assumes l = [l',0] and r = [r',0] *)
let () =
if is_local l' then
instantiate_variable l' r vars
@@ -235,8 +235,8 @@ let process_universe_constraints ctx cstrs =
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. *)
+ (* Keep Prop/Set <= var around if var might be instantiated by prop or set
+ later. *)
match Univ.Universe.level l, Univ.Universe.level r with
| Some l, Some r ->
Univ.Constraint.add (l, Univ.Le, r) local
diff --git a/engine/univMinim.ml b/engine/univMinim.ml
index e20055b133..1619ac3d34 100644
--- a/engine/univMinim.ml
+++ b/engine/univMinim.ml
@@ -32,15 +32,15 @@ let add_list_map u t map =
let choose_canonical ctx flexible algs s =
let global = LSet.diff s ctx in
let flexible, rigid = LSet.partition flexible (LSet.inter s ctx) in
- (** If there is a global universe in the set, choose it *)
+ (* If there is a global universe in the set, choose it *)
if not (LSet.is_empty global) then
let canon = LSet.choose global in
canon, (LSet.remove canon global, rigid, flexible)
- else (** No global in the equivalence class, choose a rigid one *)
+ else (* No global in the equivalence class, choose a rigid one *)
if not (LSet.is_empty rigid) then
let canon = LSet.choose rigid in
canon, (global, LSet.remove canon rigid, flexible)
- else (** There are only flexible universes in the equivalence
+ else (* There are only flexible universes in the equivalence
class, choose a non-algebraic. *)
let algs, nonalgs = LSet.partition (fun x -> LSet.mem x algs) flexible in
if not (LSet.is_empty nonalgs) then
@@ -94,8 +94,8 @@ let find_inst insts v =
with Found (f,l) -> (f,l)
let compute_lbound left =
- (** The universe variable was not fixed yet.
- Compute its level using its lower bound. *)
+ (* The universe variable was not fixed yet.
+ Compute its level using its lower bound. *)
let sup l lbound =
match lbound with
| None -> Some l
@@ -154,9 +154,10 @@ let not_lower lower (d,l) =
* constraints we must keep it. *)
compare_constraint_type d d' > 0
with Not_found ->
- (** No constraint existing on l *) true) l
+ (* No constraint existing on l *) true) l
exception UpperBoundedAlg
+
(** [enforce_uppers upper lbound cstrs] interprets [upper] as upper
constraints to [lbound], adding them to [cstrs].
@@ -269,7 +270,7 @@ module UPairSet = Set.Make (UPairs)
let normalize_context_set g ctx us algs weak =
let (ctx, csts) = ContextSet.levels ctx, ContextSet.constraints ctx in
- (** Keep the Prop/Set <= i constraints separate for minimization *)
+ (* Keep the Prop/Set <= i constraints separate for minimization *)
let smallles, csts =
Constraint.partition (fun (l,d,r) -> d == Le && Level.is_small l) csts
in
diff --git a/engine/univNames.ml b/engine/univNames.ml
index 19705f9d36..7e6ed5e4c0 100644
--- a/engine/univNames.ml
+++ b/engine/univNames.ml
@@ -35,8 +35,8 @@ type universe_binders = Univ.Level.t Names.Id.Map.t
let empty_binders = Id.Map.empty
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. *)
+ (* 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 compute_instance_binders inst ubinders =
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 16:06:34 +0000