aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--doc/sphinx/proof-engine/tactics.rst2
-rw-r--r--kernel/cbytegen.ml27
-rw-r--r--kernel/esubst.ml10
-rw-r--r--kernel/esubst.mli6
-rw-r--r--kernel/univ.ml47
-rw-r--r--kernel/univ.mli13
-rw-r--r--plugins/ssr/ssripats.ml10
-rw-r--r--plugins/ssr/ssrparser.ml413
-rw-r--r--test-suite/bugs/closed/6956.v13
-rw-r--r--test-suite/output/ssr_clear.out3
-rw-r--r--test-suite/output/ssr_clear.v6
-rw-r--r--toplevel/coqtop.ml25
12 files changed, 93 insertions, 82 deletions
diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst
index da34e3b55b..2af73c28e5 100644
--- a/doc/sphinx/proof-engine/tactics.rst
+++ b/doc/sphinx/proof-engine/tactics.rst
@@ -1635,7 +1635,7 @@ analysis on inductive or co-inductive objects (see :ref:`TODO-4.5`).
.. tacv:: elim @term using @term
.. tacv:: elim @term using @term with @bindings_list
- Allows the user to give explicitly an elimination predicate :n:`@term` that
+ Allows the user to give explicitly an induction principle :n:`@term` that
is not the standard one for the underlying inductive type of :n:`@term`. The
:n:`@bindings_list` clause allows instantiating premises of the type of
:n:`@term`.
diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml
index 0766f49b39..70dc6867ac 100644
--- a/kernel/cbytegen.ml
+++ b/kernel/cbytegen.ml
@@ -500,22 +500,19 @@ let rec compile_lam env reloc lam sz cont =
| Lsort (Sorts.Prop _ as s) ->
compile_structured_constant reloc (Const_sort s) sz cont
| Lsort (Sorts.Type u) ->
- (* We separate global and local universes in [u]. The former will be part
- of the structured constant, while the later (if any) will be applied as
- arguments. *)
- let open Univ in begin
- let u,s = Universe.compact u in
- (* We assume that [Universe.type0m] is a neutral element for [Universe.sup] *)
- let compile_get_univ reloc idx sz cont =
- set_max_stack_size sz;
- compile_fv_elem reloc (FVuniv_var idx) sz cont
- in
- if List.is_empty s then
- compile_structured_constant reloc (Const_sort (Sorts.Type u)) sz cont
- else
- comp_app compile_structured_constant compile_get_univ reloc
+ (* We represent universes as a global constant with local universes
+ "compacted", i.e. as [u arg0 ... argn] where we will substitute (after
+ evaluation) [Var 0,...,Var n] with values of [arg0,...,argn] *)
+ let u,s = Univ.compact_univ u in
+ let compile_get_univ reloc idx sz cont =
+ set_max_stack_size sz;
+ compile_fv_elem reloc (FVuniv_var idx) sz cont
+ in
+ if List.is_empty s then
+ compile_structured_constant reloc (Const_sort (Sorts.Type u)) sz cont
+ else
+ comp_app compile_structured_constant compile_get_univ reloc
(Const_sort (Sorts.Type u)) (Array.of_list s) sz cont
- end
| Llet (id,def,body) ->
compile_lam env reloc def sz
diff --git a/kernel/esubst.ml b/kernel/esubst.ml
index a11a0dc00c..91cc645233 100644
--- a/kernel/esubst.ml
+++ b/kernel/esubst.ml
@@ -19,6 +19,8 @@ open Util
(*********************)
(* Explicit lifts and basic operations *)
+(* Invariant to preserve in this module: no lift contains two consecutive
+ [ELSHFT] nor two consecutive [ELLFT]. *)
type lift =
| ELID
| ELSHFT of lift * int (* ELSHFT(l,n) == lift of n, then apply lift l *)
@@ -28,15 +30,15 @@ type lift =
let el_id = ELID
(* compose a relocation of magnitude n *)
-let rec el_shft_rec n = function
- | ELSHFT(el,k) -> el_shft_rec (k+n) el
+let el_shft_rec n = function
+ | ELSHFT(el,k) -> ELSHFT(el,k+n)
| el -> ELSHFT(el,n)
let el_shft n el = if Int.equal n 0 then el else el_shft_rec n el
(* cross n binders *)
-let rec el_liftn_rec n = function
+let el_liftn_rec n = function
| ELID -> ELID
- | ELLFT(k,el) -> el_liftn_rec (n+k) el
+ | ELLFT(k,el) -> ELLFT(n+k, el)
| el -> ELLFT(n, el)
let el_liftn n el = if Int.equal n 0 then el else el_liftn_rec n el
diff --git a/kernel/esubst.mli b/kernel/esubst.mli
index b82d6fdf02..a674c425a7 100644
--- a/kernel/esubst.mli
+++ b/kernel/esubst.mli
@@ -56,7 +56,11 @@ val comp : ('a subs * 'a -> 'a) -> 'a subs -> 'a subs -> 'a subs
(** {6 Compact representation } *)
(** Compact representation of explicit relocations
- [ELSHFT(l,n)] == lift of [n], then apply [lift l].
- - [ELLFT(n,l)] == apply [l] to de Bruijn > [n] i.e under n binders. *)
+ - [ELLFT(n,l)] == apply [l] to de Bruijn > [n] i.e under n binders.
+
+ Invariant ensured by the private flag: no lift contains two consecutive
+ [ELSHFT] nor two consecutive [ELLFT].
+*)
type lift = private
| ELID
| ELSHFT of lift * int
diff --git a/kernel/univ.ml b/kernel/univ.ml
index be21381b71..ea3a522953 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -490,39 +490,6 @@ struct
in
List.fold_right (fun a acc -> aux a acc) u []
- (** [max_var_pred p u] returns the maximum variable level in [u] satisfying
- [p], -1 if not found *)
- let rec max_var_pred p u =
- let open Level in
- match u with
- | [] -> -1
- | (v, _) :: u ->
- match var_index v with
- | Some i when p i -> max i (max_var_pred p u)
- | _ -> max_var_pred p u
-
- let rec remap_var u i j =
- let open Level in
- match u with
- | [] -> []
- | (v, incr) :: u when var_index v = Some i ->
- (Level.var j, incr) :: remap_var u i j
- | _ :: u -> remap_var u i j
-
- let rec compact u max_var i =
- if i >= max_var then (u,[]) else
- let j = max_var_pred (fun j -> j < i) u in
- if Int.equal i (j+1) then
- let (u,s) = compact u max_var (i+1) in
- (u, i :: s)
- else
- let (u,s) = compact (remap_var u i j) max_var (i+1) in
- (u, j+1 :: s)
-
- let compact u =
- let max_var = max_var_pred (fun _ -> true) u in
- compact u max_var 0
-
(* Returns the formal universe that is greater than the universes u and v.
Used to type the products. *)
let sup x y = merge_univs x y
@@ -1208,6 +1175,20 @@ let abstract_cumulativity_info (univs, variance) =
let subst, univs = abstract_universes univs in
subst, (univs, variance)
+let rec compact_univ s vars i u =
+ match u with
+ | [] -> (s, List.rev vars)
+ | (lvl, _) :: u ->
+ match Level.var_index lvl with
+ | Some k when not (LMap.mem lvl s) ->
+ let lvl' = Level.var i in
+ compact_univ (LMap.add lvl lvl' s) (k :: vars) (i+1) u
+ | _ -> compact_univ s vars i u
+
+let compact_univ u =
+ let (s, s') = compact_univ LMap.empty [] 0 u in
+ (subst_univs_level_universe s u, s')
+
(** Pretty-printing *)
let pr_constraints prl = Constraint.pr prl
diff --git a/kernel/univ.mli b/kernel/univ.mli
index 629d83fb86..aaed899bf4 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -128,12 +128,6 @@ sig
val map : (Level.t * int -> 'a) -> t -> 'a list
- (** [compact u] remaps local variables in [u] such that their indices become
- consecutive. It returns the new universe and the mapping.
- Example: compact [(Var 0, i); (Prop, 0); (Var 2; j))] =
- [(Var 0,i); (Prop, 0); (Var 1; j)], [0; 2]
- *)
- val compact : t -> t * int list
end
type universe = Universe.t
@@ -504,6 +498,13 @@ val abstract_cumulativity_info : CumulativityInfo.t -> Instance.t * ACumulativit
val make_abstract_instance : AUContext.t -> Instance.t
+(** [compact_univ u] remaps local variables in [u] such that their indices become
+ consecutive. It returns the new universe and the mapping.
+ Example: compact_univ [(Var 0, i); (Prop, 0); (Var 2; j))] =
+ [(Var 0,i); (Prop, 0); (Var 1; j)], [0; 2]
+*)
+val compact_univ : Universe.t -> Universe.t * int list
+
(** {6 Pretty-printing of universes. } *)
val pr_constraint_type : constraint_type -> Pp.t
diff --git a/plugins/ssr/ssripats.ml b/plugins/ssr/ssripats.ml
index 42566575c0..7897cb1700 100644
--- a/plugins/ssr/ssripats.ml
+++ b/plugins/ssr/ssripats.ml
@@ -133,6 +133,12 @@ let intro_clear ids future_ipats =
isCLR_PUSHL clear_ids
end
+let tacCHECK_HYPS_EXIST hyps = Goal.enter begin fun gl ->
+ let ctx = Goal.hyps gl in
+ List.iter (Ssrcommon.check_hyp_exists ctx) hyps;
+ tclUNIT ()
+end
+
(** [=> []] *****************************************************************)
let tac_case t =
Goal.enter begin fun _ ->
@@ -229,7 +235,9 @@ let rec ipat_tac1 future_ipats ipat : unit tactic =
| IPatNoop -> tclUNIT ()
| IPatSimpl Nop -> tclUNIT ()
- | IPatClear ids -> intro_clear (List.map Ssrcommon.hyp_id ids) future_ipats
+ | IPatClear ids ->
+ tacCHECK_HYPS_EXIST ids <*>
+ intro_clear (List.map Ssrcommon.hyp_id ids) future_ipats
| IPatSimpl (Simpl n) ->
V82.tactic ~nf_evars:false (Ssrequality.simpltac (Simpl n))
diff --git a/plugins/ssr/ssrparser.ml4 b/plugins/ssr/ssrparser.ml4
index 0d82a9f096..5f39674407 100644
--- a/plugins/ssr/ssrparser.ml4
+++ b/plugins/ssr/ssrparser.ml4
@@ -585,21 +585,10 @@ let pr_ssripat _ _ _ = pr_ipat
let pr_ssripats _ _ _ = pr_ipats
let pr_ssriorpat _ _ _ = pr_iorpat
-(*
-let intern_ipat ist ipat =
- let rec check_pat = function
- | IPatClear clr -> ignore (List.map (intern_hyp ist) clr)
- | IPatCase iorpat -> List.iter (List.iter check_pat) iorpat
- | IPatDispatch iorpat -> List.iter (List.iter check_pat) iorpat
- | IPatInj iorpat -> List.iter (List.iter check_pat) iorpat
- | _ -> () in
- check_pat ipat; ipat
-*)
-
let intern_ipat ist =
map_ipat
(fun id -> id)
- (intern_hyp ist) (* TODO: check with ltac, old code was ignoring the result *)
+ (intern_hyp ist)
(glob_ast_closure_term ist)
let intern_ipats ist = List.map (intern_ipat ist)
diff --git a/test-suite/bugs/closed/6956.v b/test-suite/bugs/closed/6956.v
new file mode 100644
index 0000000000..ee21adbbfd
--- /dev/null
+++ b/test-suite/bugs/closed/6956.v
@@ -0,0 +1,13 @@
+(** Used to trigger an anomaly with VM compilation *)
+
+Set Universe Polymorphism.
+
+Inductive t A : nat -> Type :=
+| nil : t A 0
+| cons : forall (h : A) (n : nat), t A n -> t A (S n).
+
+Definition case0 {A} (P : t A 0 -> Type) (H : P (nil A)) v : P v :=
+match v with
+| nil _ => H
+| _ => fun devil => False_ind (@IDProp) devil
+end.
diff --git a/test-suite/output/ssr_clear.out b/test-suite/output/ssr_clear.out
new file mode 100644
index 0000000000..1515954060
--- /dev/null
+++ b/test-suite/output/ssr_clear.out
@@ -0,0 +1,3 @@
+The command has indeed failed with message:
+Ltac call to "move (ssrmovearg) (ssrclauses)" failed.
+No assumption is named NO_SUCH_NAME
diff --git a/test-suite/output/ssr_clear.v b/test-suite/output/ssr_clear.v
new file mode 100644
index 0000000000..573ec47e0b
--- /dev/null
+++ b/test-suite/output/ssr_clear.v
@@ -0,0 +1,6 @@
+Require Import ssreflect.
+
+Example foo : True -> True.
+Proof.
+Fail move=> {NO_SUCH_NAME}.
+Abort.
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index a08cfa9f48..0dabed6b71 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -315,16 +315,24 @@ let check_vio_tasks opts =
(* vio files *)
let schedule_vio opts =
- (* We must add update the loadpath here as the scheduling process
- happens outside of the STM *)
- let iload_path = build_load_path opts in
- List.iter Mltop.add_coq_path iload_path;
-
if opts.vio_checking then
Vio_checking.schedule_vio_checking opts.vio_files_j opts.vio_files
else
Vio_checking.schedule_vio_compilation opts.vio_files_j opts.vio_files
+let do_vio opts =
+ (* We must initialize the loadpath here as the vio scheduling
+ process happens outside of the STM *)
+ if opts.vio_files <> [] || opts.vio_tasks <> [] then
+ let iload_path = build_load_path opts in
+ List.iter Mltop.add_coq_path iload_path;
+
+ (* Vio compile pass *)
+ if opts.vio_files <> [] then schedule_vio opts;
+ (* Vio task pass *)
+ if opts.vio_tasks <> [] then check_vio_tasks opts
+
+
(******************************************************************************)
(* Color Options *)
(******************************************************************************)
@@ -483,10 +491,9 @@ let init_toplevel arglist =
end else begin
try
compile_files opts;
- (* Vio compile pass *)
- if opts.vio_files <> [] then schedule_vio opts;
- (* Vio task pass *)
- check_vio_tasks opts;
+ (* Careful this will modify the load-path and state so after
+ this point some stuff may not be safe anymore. *)
+ do_vio opts;
(* Allow the user to output an arbitrary state *)
outputstate opts;
None, opts
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-01 02:06:04 +0000