diff options
| -rw-r--r-- | engine/uState.ml | 3 | ||||
| -rw-r--r-- | kernel/names.ml | 1 | ||||
| -rw-r--r-- | kernel/names.mli | 1 | ||||
| -rw-r--r-- | library/goptions.ml | 19 | ||||
| -rw-r--r-- | library/goptions.mli | 28 | ||||
| -rw-r--r-- | pretyping/classops.ml | 2 | ||||
| -rw-r--r-- | pretyping/detyping.ml | 2 | ||||
| -rw-r--r-- | pretyping/detyping.mli | 2 | ||||
| -rw-r--r-- | test-suite/Makefile | 29 | ||||
| -rw-r--r-- | test-suite/README.md | 4 | ||||
| -rw-r--r-- | test-suite/bugs/closed/bug_10161.v | 8 | ||||
| -rw-r--r-- | theories/Vectors/VectorDef.v | 3 | ||||
| -rwxr-xr-x | user-contrib/Ltac2/Bool.v | 63 | ||||
| -rw-r--r-- | user-contrib/Ltac2/Control.v | 26 | ||||
| -rwxr-xr-x[-rw-r--r--] | user-contrib/Ltac2/Init.v | 8 | ||||
| -rw-r--r-- | user-contrib/Ltac2/Int.v | 15 | ||||
| -rw-r--r-- | user-contrib/Ltac2/List.v | 598 | ||||
| -rw-r--r-- | user-contrib/Ltac2/Option.v | 60 | ||||
| -rw-r--r-- | vernac/search.ml | 14 |
19 files changed, 841 insertions, 45 deletions
diff --git a/engine/uState.ml b/engine/uState.ml index bd61112f08..5ed016e0d0 100644 --- a/engine/uState.ml +++ b/engine/uState.ml @@ -214,7 +214,8 @@ let process_universe_constraints ctx cstrs = | Inr l, Inl r | Inl r, Inr l -> let alg = LSet.mem l ctx.uctx_univ_algebraic in let inst = univ_level_rem l r r in - if alg then (instantiate_variable l inst vars; local) + if alg && not (LSet.mem l (Universe.levels inst)) then + (instantiate_variable l inst vars; local) else let lu = Universe.make l in if univ_level_mem l r then diff --git a/kernel/names.ml b/kernel/names.ml index 655bf50087..85dc8267bb 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -671,6 +671,7 @@ module InductiveOrdered_env = struct let compare = ind_user_ord end +module Indset = Set.Make(InductiveOrdered) module Indmap = Map.Make(InductiveOrdered) module Indmap_env = Map.Make(InductiveOrdered_env) diff --git a/kernel/names.mli b/kernel/names.mli index 44e8dd4a83..65c5d6c139 100644 --- a/kernel/names.mli +++ b/kernel/names.mli @@ -481,6 +481,7 @@ type constructor = inductive (* designates the inductive type *) * int (* the index of the constructor BEWARE: indexing starts from 1. *) +module Indset : CSig.SetS with type elt = inductive module Indmap : CSig.MapS with type key = inductive module Constrmap : CSig.MapS with type key = constructor module Indmap_env : CSig.MapS with type key = inductive diff --git a/library/goptions.ml b/library/goptions.ml index e25672ccf2..c7024ca81d 100644 --- a/library/goptions.ml +++ b/library/goptions.ml @@ -53,9 +53,9 @@ module MakeTable = functor (A : sig type t - type key - val compare : t -> t -> int - val table : (string * key table_of_A) list ref + type key + module Set : CSig.SetS with type elt = t + val table : (string * key table_of_A) list ref val encode : Environ.env -> key -> t val subst : substitution -> t -> t val printer : t -> Pp.t @@ -74,7 +74,7 @@ module MakeTable = if String.List.mem_assoc nick !A.table then user_err Pp.(str "Sorry, this table name (" ++ str nick ++ str ") is already used.") - module MySet = Set.Make (struct type t = A.t let compare = A.compare end) + module MySet = A.Set let t = Summary.ref MySet.empty ~name:nick @@ -119,8 +119,9 @@ module MakeTable = } let _ = A.table := (nick, table_of_A)::!A.table - let active c = MySet.mem c !t - let elements () = MySet.elements !t + + let v () = !t + let active x = A.Set.mem x !t end let string_table = ref [] @@ -138,7 +139,7 @@ module StringConvert = functor (A : StringConvertArg) -> struct type t = string type key = string - let compare = String.compare + module Set = CString.Set let table = string_table let encode _env x = x let subst _ x = x @@ -158,7 +159,7 @@ let get_ref_table k = String.List.assoc (nickname k) !ref_table module type RefConvertArg = sig type t - val compare : t -> t -> int + module Set : CSig.SetS with type elt = t val encode : Environ.env -> qualid -> t val subst : substitution -> t -> t val printer : t -> Pp.t @@ -171,7 +172,7 @@ module RefConvert = functor (A : RefConvertArg) -> struct type t = A.t type key = qualid - let compare = A.compare + module Set = A.Set let table = ref_table let encode = A.encode let subst = A.subst diff --git a/library/goptions.mli b/library/goptions.mli index 2989221975..29af196654 100644 --- a/library/goptions.mli +++ b/library/goptions.mli @@ -70,8 +70,8 @@ module MakeStringTable : val member_message : string -> bool -> Pp.t end) -> sig + val v : unit -> CString.Set.t val active : string -> bool - val elements : unit -> string list end (** The functor [MakeRefTable] declares a new table of objects of type @@ -87,19 +87,19 @@ end module MakeRefTable : functor (A : sig - type t - val compare : t -> t -> int - val encode : Environ.env -> qualid -> t - val subst : substitution -> t -> t - val printer : t -> Pp.t - val key : option_name - val title : string - val member_message : t -> bool -> Pp.t - end) -> - sig - val active : A.t -> bool - val elements : unit -> A.t list - end + type t + module Set : CSig.SetS with type elt = t + val encode : Environ.env -> qualid -> t + val subst : substitution -> t -> t + val printer : t -> Pp.t + val key : option_name + val title : string + val member_message : t -> bool -> Pp.t + end) -> +sig + val v : unit -> A.Set.t + val active : A.t -> bool +end (** {6 Options. } *) diff --git a/pretyping/classops.ml b/pretyping/classops.ml index edad06777e..f5fffc4c1c 100644 --- a/pretyping/classops.ml +++ b/pretyping/classops.ml @@ -441,7 +441,7 @@ let coercion_of_reference r = module CoercionPrinting = struct type t = coe_typ - let compare = GlobRef.Ordered.compare + module Set = GlobRef.Set let encode _env = coercion_of_reference let subst = subst_coe_typ let printer x = Nametab.pr_global_env Id.Set.empty x diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 2c31aafb70..0daf1ab531 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -182,7 +182,7 @@ module PrintingInductiveMake = end) -> struct type t = inductive - let compare = ind_ord + module Set = Indset let encode = Test.encode let subst subst obj = subst_ind subst obj let printer ind = Nametab.pr_global_env Id.Set.empty (IndRef ind) diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli index ed2bb97513..cc9f520583 100644 --- a/pretyping/detyping.mli +++ b/pretyping/detyping.mli @@ -91,7 +91,7 @@ module PrintingInductiveMake : end) -> sig type t = Names.inductive - val compare : t -> t -> int + module Set = Indset val encode : Environ.env -> Libnames.qualid -> Names.inductive val subst : substitution -> t -> t val printer : t -> Pp.t diff --git a/test-suite/Makefile b/test-suite/Makefile index ec61f60791..c0bdb29fab 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -97,7 +97,7 @@ COMPLEXITY := $(if $(bogomips),complexity) BUGS := bugs/opened bugs/closed INTERACTIVE := interactive UNIT_TESTS := unit-tests -VSUBSYSTEMS := prerequisite success failure $(BUGS) output \ +VSUBSYSTEMS := prerequisite success failure $(BUGS) output output-coqtop \ output-modulo-time $(INTERACTIVE) micromega $(COMPLEXITY) modules stm \ coqdoc ssr arithmetic ltac2 @@ -164,6 +164,7 @@ summary: $(call summary_dir, "Failure tests", failure); \ $(call summary_dir, "Bugs tests", bugs); \ $(call summary_dir, "Output tests", output); \ + $(call summary_dir, "Output tests with coqtop", output-coqtop); \ $(call summary_dir, "Output (modulo time changes) tests", output-modulo-time); \ $(call summary_dir, "Interactive tests", interactive); \ $(call summary_dir, "Micromega tests", micromega); \ @@ -425,8 +426,32 @@ $(addsuffix .log,$(wildcard output/*.v)): %.v.log: %.v %.out $(PREREQUISITELOG) fi; \ } > "$@" +$(addsuffix .log,$(wildcard output-coqtop/*.v)): %.v.log: %.v %.out $(PREREQUISITELOG) + @echo "TEST $< $(call get_coq_prog_args_in_parens,"$<")" + $(HIDE){ \ + echo $(call log_intro,$<); \ + output=$*.out.real; \ + $(coqtop) < "$<" $(call get_coq_prog_args,"$<") 2>&1 \ + | grep -v "Welcome to Coq" \ + | grep -v "\[Loading ML file" \ + | grep -v "Skipping rcfile loading" \ + | grep -v "^<W>" \ + | sed 's/File "[^"]*"/File "stdin"/' \ + > $$output; \ + diff -u --strip-trailing-cr $*.out $$output 2>&1; R=$$?; times; \ + if [ $$R = 0 ]; then \ + echo $(log_success); \ + echo " $<...Ok"; \ + rm $$output; \ + else \ + echo $(log_failure); \ + echo " $<...Error! (unexpected output)"; \ + $(FAIL); \ + fi; \ + } > "$@" + .PHONY: approve-output -approve-output: output +approve-output: output output-coqtop $(HIDE)for f in output/*.out.real; do \ mv "$$f" "$${f%.real}"; \ echo "Updated $${f%.real}!"; \ diff --git a/test-suite/README.md b/test-suite/README.md index e81da0830f..a2d5905710 100644 --- a/test-suite/README.md +++ b/test-suite/README.md @@ -76,7 +76,9 @@ The error "(bug seems to be opened, please check)" when running compile. There are also output tests in [`output`](output) which consist of a `.v` file -and a `.out` file with the expected output. +and a `.out` file with the expected output. Output tests in this directory are +run with coqc in -test-mode. Output tests in [`output-coqtop`](output-coqtop) +work the same way, but are run with coqtop. There are unit tests of OCaml code in [`unit-tests`](unit-tests). These tests are contained in `.ml` files, and rely on the `OUnit` unit-test framework, as diff --git a/test-suite/bugs/closed/bug_10161.v b/test-suite/bugs/closed/bug_10161.v new file mode 100644 index 0000000000..3d262b89fe --- /dev/null +++ b/test-suite/bugs/closed/bug_10161.v @@ -0,0 +1,8 @@ +Inductive SwitchT (A : Type) : Type := +| switchT : forall T, SwitchT T -> SwitchT A. + +Set Printing Universes. + +Fail Inductive UseSwitchT := +| useSwitchT : SwitchT UseSwitchT -> UseSwitchT. +(* used to stack overflow, should be univ inconsistency cannot satisfy u = u+1 *) diff --git a/theories/Vectors/VectorDef.v b/theories/Vectors/VectorDef.v index 3bed8c1e40..20a8581d46 100644 --- a/theories/Vectors/VectorDef.v +++ b/theories/Vectors/VectorDef.v @@ -217,8 +217,7 @@ End BASES. Local Notation "v [@ p ]" := (nth v p) (at level 1). Section ITERATORS. -(** * Here are special non dependent useful instantiation of induction -schemes *) +(** * Here are special non dependent useful instantiation of induction schemes *) (** Uniform application on the arguments of the vector *) Definition map {A} {B} (f : A -> B) : forall {n} (v:t A n), t B n := diff --git a/user-contrib/Ltac2/Bool.v b/user-contrib/Ltac2/Bool.v new file mode 100755 index 0000000000..d808436e13 --- /dev/null +++ b/user-contrib/Ltac2/Bool.v @@ -0,0 +1,63 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +Require Import Ltac2.Init. + +Ltac2 and x y := + match x with + | true => y + | false => false + end. + +Ltac2 or x y := + match x with + | true => true + | false => y + end. + +Ltac2 impl x y := + match x with + | true => y + | false => true + end. + +Ltac2 neg x := + match x with + | true => false + | false => true + end. + +Ltac2 xor x y := + match x with + | true + => match y with + | true => false + | false => true + end + | false + => match y with + | true => true + | false => false + end + end. + +Ltac2 eq x y := + match x with + | true + => match y with + | true => true + | false => false + end + | false + => match y with + | true => false + | false => true + end + end. diff --git a/user-contrib/Ltac2/Control.v b/user-contrib/Ltac2/Control.v index 19530b224b..8f35e1a279 100644 --- a/user-contrib/Ltac2/Control.v +++ b/user-contrib/Ltac2/Control.v @@ -9,6 +9,7 @@ (************************************************************************) Require Import Ltac2.Init. +Require Ltac2.Message. (** Panic *) @@ -76,3 +77,28 @@ Ltac2 @ external abstract : ident option -> (unit -> unit) -> unit := "ltac2" "a Ltac2 @ external check_interrupt : unit -> unit := "ltac2" "check_interrupt". (** For internal use. *) + +(** Assertions throwing exceptions and short form throws *) + +Ltac2 throw_invalid_argument (msg : string) := + Control.throw (Invalid_argument (Some (Message.of_string msg))). + +Ltac2 throw_out_of_bounds (msg : string) := + Control.throw (Out_of_bounds (Some (Message.of_string msg))). + +Ltac2 assert_valid_argument (msg : string) (test : bool) := + match test with + | true => () + | false => throw_invalid_argument msg + end. + +Ltac2 assert_bounds (msg : string) (test : bool) := + match test with + | true => () + | false => throw_out_of_bounds msg + end. + +(** Short form backtracks *) + +Ltac2 backtrack_tactic_failure (msg : string) := + Control.zero (Tactic_failure (Some (Message.of_string msg))). diff --git a/user-contrib/Ltac2/Init.v b/user-contrib/Ltac2/Init.v index 93468f302e..88454ff2fb 100644..100755 --- a/user-contrib/Ltac2/Init.v +++ b/user-contrib/Ltac2/Init.v @@ -53,7 +53,7 @@ Ltac2 Type err. Ltac2 Type exn ::= [ Internal (err) ]. (** Wrapper around the errors raised by Coq implementation. *) -Ltac2 Type exn ::= [ Out_of_bounds ]. +Ltac2 Type exn ::= [ Out_of_bounds (message option) ]. (** Used for bound checking, e.g. with String and Array. *) Ltac2 Type exn ::= [ Not_focussed ]. @@ -65,8 +65,14 @@ Ltac2 Type exn ::= [ Not_focussed ]. Ltac2 Type exn ::= [ Not_found ]. (** Used when something is missing. *) +Ltac2 Type exn ::= [ No_value ]. +(** Used for empty lists, None options and the like. *) + Ltac2 Type exn ::= [ Match_failure ]. (** Used to signal a pattern didn't match a term. *) +Ltac2 Type exn ::= [ Invalid_argument (message option) ]. +(** Used to signal that an invalid argument was passed to a tactic. *) + Ltac2 Type exn ::= [ Tactic_failure (message option) ]. (** Generic error for tactic failure. *) diff --git a/user-contrib/Ltac2/Int.v b/user-contrib/Ltac2/Int.v index ac48a3328f..60aafcd37d 100644 --- a/user-contrib/Ltac2/Int.v +++ b/user-contrib/Ltac2/Int.v @@ -18,3 +18,18 @@ Ltac2 @ external add : int -> int -> int := "ltac2" "int_add". Ltac2 @ external sub : int -> int -> int := "ltac2" "int_sub". Ltac2 @ external mul : int -> int -> int := "ltac2" "int_mul". Ltac2 @ external neg : int -> int := "ltac2" "int_neg". + +Ltac2 lt (x : int) (y : int) := equal (compare x y) -1. +Ltac2 gt (x : int) (y : int) := equal (compare x y) 1. +Ltac2 le (x : int) (y : int) := + (* we might use [lt x (add y 1)], but that has the wrong behavior on MAX_INT *) + match equal x y with + | true => true + | false => lt x y + end. +Ltac2 ge (x : int) (y : int) := + (* we might use [lt (add x 1) y], but that has the wrong behavior on MAX_INT *) + match equal x y with + | true => true + | false => gt x y + end. diff --git a/user-contrib/Ltac2/List.v b/user-contrib/Ltac2/List.v new file mode 100644 index 0000000000..89e14445ef --- /dev/null +++ b/user-contrib/Ltac2/List.v @@ -0,0 +1,598 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(* The interface is an extended version of OCaml stdlib/list.ml. *) + +(**************************************************************************) +(* *) +(* OCaml *) +(* *) +(* Xavier Leroy, projet Cristal, INRIA Rocquencourt *) +(* *) +(* Copyright 1996 Institut National de Recherche en Informatique et *) +(* en Automatique. *) +(* *) +(* All rights reserved. This file is distributed under the terms of *) +(* the GNU Lesser General Public License version 2.1, with the *) +(* special exception on linking described in the file LICENSE. *) +(* *) +(**************************************************************************) + +Require Import Ltac2.Init. +Require Ltac2.Int. +Require Ltac2.Control. +Require Ltac2.Bool. +Require Ltac2.Message. + +Ltac2 rec length (ls : 'a list) := + match ls with + | [] => 0 + | _ :: xs => Int.add 1 (length xs) + end. + +Ltac2 rec compare_lengths (ls1 : 'a list) (ls2 : 'b list) := + match ls1 with + | [] + => match ls2 with + | [] => 0 + | _ :: _ => -1 + end + | _ :: ls1 + => match ls2 with + | [] => 1 + | _ :: ls2 => compare_lengths ls1 ls2 + end + end. + +Ltac2 rec compare_length_with (ls : 'a list) (n : int) := + match Int.lt n 0 with + | true => 1 + | false + => match ls with + | [] => Int.compare 0 n + | _ :: ls => compare_length_with ls (Int.sub n 1) + end + end. + +Ltac2 cons (x : 'a) (xs : 'a list) := + x :: xs. + +(* Since Ltac-2 distinguishes between backtracking and fatal exceptions, + we provide option and default variants of functions which throw in the + OCaml stdlib. *) + +Ltac2 hd_opt (ls : 'a list) := + match ls with + | [] => None + | x :: xs => Some x + end. + +Ltac2 hd (ls : 'a list) := + match ls with + | [] => Control.throw_invalid_argument "List.hd" + | x :: xs => x + end. + +Ltac2 tl (ls : 'a list) := + match ls with + | [] => [] + | x :: xs => xs + end. + +Ltac2 rec last_opt (ls : 'a list) := + match ls with + | [] => None + | x :: xs + => match xs with + | [] => Some x + | _ :: _ => last_opt xs + end + end. + +Ltac2 last (ls : 'a list) := + match last_opt ls with + | None => Control.throw_invalid_argument "List.last" + | Some v => v + end. + +Ltac2 rec removelast (ls : 'a list) := + match ls with + | [] => [] + | x :: xs + => match xs with + | [] => [] + | _ :: _ => x :: removelast xs + end + end. + +Ltac2 rec nth_opt_aux (ls : 'a list) (n : int) := + match ls with + | [] => None + | x :: xs + => match Int.equal n 0 with + | true => Some x + | false => nth_opt_aux xs (Int.sub n 1) + end + end. + +Ltac2 nth_opt (ls : 'a list) (n : int) := + Control.assert_valid_argument "List.nth" (Int.ge n 0); + nth_opt_aux ls n. + +Ltac2 nth (ls : 'a list) (n : int) := + match nth_opt ls n with + | Some v => v + | None => Control.throw_out_of_bounds "List.nth" + end. + +Ltac2 rec rev_append (l1 : 'a list) (l2 : 'a list) := + match l1 with + | [] => l2 + | a :: l => rev_append l (a :: l2) + end. + +Ltac2 rev l := rev_append l []. + +Ltac2 rec append ls1 ls2 := + match ls1 with + | [] => ls2 + | x :: xs => x :: append xs ls2 + end. + +Ltac2 rec concat (ls : 'a list list) := + match ls with + | [] => [] + | x :: xs => append x (concat xs) + end. + +Ltac2 flatten (ls : 'a list list) := concat ls. + +Ltac2 rec iter (f : 'a -> unit) (ls : 'a list) := + match ls with + | [] => () + | l :: ls => f l; iter f ls + end. + +Ltac2 rec iteri_aux (i : int) (f : int -> 'a -> unit) (ls : 'a list) := + match ls with + | [] => () + | l :: ls => f i l; iteri_aux (Int.add i 1) f ls + end. + +Ltac2 iteri (f : int -> 'a -> unit) (ls : 'a list) := + iteri_aux 0 f ls. + +Ltac2 rec map (f : 'a -> 'b) (ls : 'a list) := + match ls with + | [] => [] + | l :: ls => f l :: map f ls + end. + +Ltac2 rec mapi_aux (i : int) (f : int -> 'a -> 'b) (ls : 'a list) := + match ls with + | [] => [] + | l :: ls => f i l :: mapi_aux (Int.add i 1) f ls + end. + +Ltac2 mapi (f : int -> 'a -> 'b) (ls : 'a list) := + mapi_aux 0 f ls. + +Ltac2 rec flat_map (f : 'a -> 'b list) (xs : 'a list) := + match xs with + | [] => [] + | x :: xs => append (f x) (flat_map f xs) + end. + +(* from the OCaml std lib *) +Ltac2 rev_map (f : 'a -> 'b) (ls : 'a list) := + let rec rmap_f accu ls := + match ls with + | [] => accu + | a::l => rmap_f (f a :: accu) l + end in + rmap_f [] ls. + +Ltac2 rec fold_right (f : 'a -> 'b -> 'b) (a : 'b) (ls : 'a list) := + match ls with + | [] => a + | l :: ls => f l (fold_right f a ls) + end. + +Ltac2 rec fold_left (f : 'a -> 'b -> 'a) (xs : 'b list) (a : 'a) := + match xs with + | [] => a + | x :: xs => fold_left f xs (f a x) + end. + +Ltac2 rec iter2 (f : 'a -> 'b -> unit) (ls1 : 'a list) (ls2 : 'b list) := + match ls1 with + | [] + => match ls2 with + | [] => () + | _ :: _ => Control.throw_invalid_argument "List.iter2" + end + | l1 :: ls1 + => match ls2 with + | [] => Control.throw_invalid_argument "List.iter2" + | l2 :: ls2 + => f l1 l2; iter2 f ls1 ls2 + end + end. + +Ltac2 rec map2 (f : 'a -> 'b -> 'c) (ls1 : 'a list) (ls2 : 'b list) := + match ls1 with + | [] + => match ls2 with + | [] => [] + | _ :: _ => Control.throw_invalid_argument "List.map2" + end + | l1 :: ls1 + => match ls2 with + | [] => Control.throw_invalid_argument "List.map2" + | l2 :: ls2 + => f l1 l2 :: map2 f ls1 ls2 + end + end. + +(* from the OCaml std lib *) +Ltac2 rev_map2 (f : 'a -> 'b -> 'c) (ls1 : 'a list) (ls2 : 'b list) := + let rec rmap2_f accu ls1 ls2 := + match ls1 with + | [] + => match ls2 with + | [] => accu + | _ :: _ => Control.throw_invalid_argument "List.rev_map2" + end + | l1 :: ls1 + => match ls2 with + | [] => Control.throw_invalid_argument "List.rev_map2" + | l2 :: ls2 + => rmap2_f (f l1 l2 :: accu) ls1 ls2 + end + end in + rmap2_f [] ls1 ls2. + +Ltac2 rec fold_right2 (f : 'a -> 'b -> 'c -> 'c) (a : 'c) (ls1 : 'a list) (ls2 : 'b list) := + match ls1 with + | [] + => match ls2 with + | [] => a + | _ :: _ => Control.throw_invalid_argument "List.fold_right2" + end + | l1 :: ls1 + => match ls2 with + | [] => Control.throw_invalid_argument "List.fold_right2" + | l2 :: ls2 + => f l1 l2 (fold_right2 f a ls1 ls2) + end + end. + +Ltac2 rec fold_left2 (f : 'a -> 'b -> 'c -> 'a) (ls1 : 'b list) (ls2 : 'c list) (a : 'a) := + match ls1 with + | [] + => match ls2 with + | [] => a + | _ :: _ => Control.throw_invalid_argument "List.fold_left2" + end + | l1 :: ls1 + => match ls2 with + | [] => Control.throw_invalid_argument "List.fold_left2" + | l2 :: ls2 + => fold_left2 f ls1 ls2 (f a l1 l2) + end + end. + +Ltac2 rec for_all f ls := + match ls with + | [] => true + | x :: xs => match f x with + | true => for_all f xs + | false => false + end + end. + +(* we would call this [exists] a la OCaml's [List.exists], but that's a syntax error, so instead we name it exist *) +Ltac2 rec exist f ls := + match ls with + | [] => false + | x :: xs => match f x with + | true => true + | false => exist f xs + end + end. + +Ltac2 rec for_all2 f xs ys := + match xs with + | [] => match ys with + | [] => true + | y :: ys' => Control.throw_invalid_argument "List.for_all2" + end + | x :: xs' + => match ys with + | [] => Control.throw_invalid_argument "List.for_all2" + | y :: ys' + => match f x y with + | true => for_all2 f xs' ys' + | false => false + end + end + end. + +Ltac2 rec exist2 f xs ys := + match xs with + | [] => match ys with + | [] => false + | y :: ys' => Control.throw_invalid_argument "List.exist2" + end + | x :: xs' + => match ys with + | [] => Control.throw_invalid_argument "List.exist2" + | y :: ys' + => match f x y with + | true => true + | false => exist2 f xs' ys' + end + end + end. + +Ltac2 rec find_opt f xs := + match xs with + | [] => None + | x :: xs => match f x with + | true => Some x + | false => find_opt f xs + end + end. + +Ltac2 find f xs := + match find_opt f xs with + | Some v => v + | None => Control.throw Not_found + end. + +Ltac2 rec find_rev_opt f xs := + match xs with + | [] => None + | x :: xs => match find_rev_opt f xs with + | Some v => Some v + | None => match f x with + | true => Some x + | false => None + end + end + end. + +Ltac2 find_rev f xs := + match find_rev_opt f xs with + | Some v => v + | None => Control.throw Not_found + end. + +Ltac2 mem (eq : 'a -> 'a -> bool) (a : 'a) (ls : 'a list) := + exist (eq a) ls. + +Ltac2 rec filter f xs := + match xs with + | [] => [] + | x :: xs + => match f x with + | true => x :: filter f xs + | false => filter f xs + end + end. + +Ltac2 rec filter_out f xs := + filter (fun x => Bool.neg (f x)) xs. + +Ltac2 find_all (f : 'a -> bool) (ls : 'a list) := filter f ls. + +Ltac2 remove (eqb : 'a -> 'a -> bool) (x : 'a) (ls : 'a list) := + filter_out (eqb x) ls. + +Ltac2 count_occ (eqb : 'a -> 'a -> bool) (x : 'a) (ls : 'a list) := + length (filter (eqb x) ls). + +(* from the Coq stdlib *) +Ltac2 rec list_power (ls1 : 'a list) (ls2 : 'b list) := + match ls1 with + | [] => [] :: [] + | x :: t + => flat_map (fun f => map (fun y => (x, y) :: f) ls2) + (list_power t ls2) + end. + +Ltac2 rec partition (f : 'a -> bool) (l : 'a list) := + match l with + | [] => ([], []) + | x :: tl + => let (g, d) := partition f tl in + match f x with + | true => ((x::g), d) + | false => (g, (x::d)) + end + end. + +(* from the Coq stdlib *) +(** [list_prod] has the same signature as [combine], but unlike + [combine], it adds every possible pairs, not only those at the + same position. *) + +Ltac2 rec list_prod (ls1 : 'a list) (ls2 : 'b list) := + match ls1 with + | [] => [] + | x :: t + => append (map (fun y => (x, y)) ls2) (list_prod t ls2) + end. + +Ltac2 rec firstn (n : int) (ls : 'a list) := + Control.assert_valid_argument "List.firstn" (Int.ge n 0); + match Int.equal n 0 with + | true => [] + | false + => match ls with + | [] => Control.throw_out_of_bounds "List.firstn" + | x :: xs + => x :: firstn (Int.sub n 1) xs + end + end. + +Ltac2 rec skipn (n : int) (ls : 'a list) := + Control.assert_valid_argument "List.skipn" (Int.ge n 0); + match Int.equal n 0 with + | true => ls + | false + => match ls with + | [] => Control.throw_out_of_bounds "List.skipn" + | x :: xs + => skipn (Int.sub n 1) xs + end + end. + +Ltac2 lastn (n : int) (ls : 'a list) := + let l := length ls in + Control.assert_valid_argument "List.lastn" (Int.ge n 0); + Control.assert_bounds "List.lastn" (Int.le n l); + skipn (Int.sub l n). + +Ltac2 rec nodup (eqb : 'a -> 'a -> bool) (ls : 'a list) := + match ls with + | [] => [] + | x :: xs + => match mem eqb x xs with + | true => nodup eqb xs + | false => x :: nodup eqb xs + end + end. + +(* seq start 1 last = start :: start + 1 :: ... :: (last - 1) *) +Ltac2 rec seq (start : int) (step : int) (last : int) := + match Int.lt (Int.sub last start) step with + | true + => [] + | false + => start :: seq (Int.add start step) step last + end. + +Ltac2 init (len : int) (f : int -> 'a) := + Control.assert_valid_argument "List.init" (Int.ge len 0); + map f (seq 0 1 len). + +Ltac2 repeat (x : 'a) (n : 'int) := + init n (fun _ => x). + +Ltac2 assoc (eqk : 'k -> 'k -> bool) (k : 'k) (l : ('k * 'v) list) := + let eq_key kv := let (k', _) := kv in eqk k k' in + let (_, v) := find eq_key l in + v. + +Ltac2 assoc_opt (eqk : 'k -> 'k -> bool) (k : 'k) (l : ('k * 'v) list) := + let eq_key kv := let (k', _) := kv in eqk k k' in + match find_opt eq_key l with + | Some kv => let (_, v) := kv in Some v + | None => None + end. + +Ltac2 mem_assoc (eqk : 'k -> 'k -> bool) (k : 'k) (l : ('k * 'v) list) := + let eq_key kv := let (k', _) := kv in eqk k k' in + exist eq_key l. + +Ltac2 remove_assoc (eqk : 'k -> 'k -> bool) (k : 'k) (l : ('k * 'v) list) := + let eq_key kv := let (k', _) := kv in eqk k k' in + filter_out eq_key l. + +Ltac2 rec split (ls : ('a * 'b) list) := + match ls with + | [] => ([], []) + | xy :: tl + => let (x, y) := xy in + let (left, right) := split tl in + ((x::left), (y::right)) + end. + +Ltac2 rec combine (ls1 : 'a list) (ls2 : 'b list) := + match ls1 with + | [] + => match ls2 with + | [] => [] + | _ :: _ => Control.throw_invalid_argument "List.combine" + end + | x :: xs + => match ls2 with + | y :: ys + => (x, y) :: combine xs ys + | [] => Control.throw_invalid_argument "List.combine" + end + end. + +Ltac2 enumerate (ls : 'a list) := + combine (seq 0 1 (length ls)) ls. + +(* from Coq stdlib *) +Ltac2 rec merge (cmp : 'a -> 'a -> int) (l1 : 'a list) (l2 : 'b list) := + let rec merge_aux l2 := + match l1 with + | [] => l2 + | a1 :: l1' + => match l2 with + | [] => l1 + | a2 :: l2' + => match Int.le (cmp a1 a2) 0 with + | true => a1 :: merge cmp l1' l2 + | false => a2 :: merge_aux l2' + end + end + end in + merge_aux l2. + +Ltac2 rec merge_list_to_stack cmp stack l := + match stack with + | [] => [Some l] + | l' :: stack' + => match l' with + | None => Some l :: stack' + | Some l' + => None :: merge_list_to_stack cmp stack' (merge cmp l' l) + end + end. + +Ltac2 rec merge_stack cmp stack := + match stack with + | [] => [] + | l :: stack' + => match l with + | None => merge_stack cmp stack' + | Some l => merge cmp l (merge_stack cmp stack') + end + end. + +Ltac2 rec iter_merge cmp stack l := + match l with + | [] => merge_stack cmp stack + | a::l' => iter_merge cmp (merge_list_to_stack cmp stack [a]) l' + end. + +Ltac2 sort cmp l := iter_merge cmp [] l. + +(* TODO: maybe replace this with a faster implementation *) +Ltac2 sort_uniq (cmp : 'a -> 'a -> int) (l : 'a list) := + let rec uniq l := + match l with + | [] => [] + | x1 :: xs + => match xs with + | [] => x1 :: xs + | x2 :: _ + => match Int.equal (cmp x1 x2) 0 with + | true => uniq xs + | false => x1 :: uniq xs + end + end + end in + uniq (sort cmp l). diff --git a/user-contrib/Ltac2/Option.v b/user-contrib/Ltac2/Option.v new file mode 100644 index 0000000000..584d84ddb5 --- /dev/null +++ b/user-contrib/Ltac2/Option.v @@ -0,0 +1,60 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(* Some of the below functions are inspired by ocaml-extlib *) + +Require Import Ltac2.Init. +Require Import Ltac2.Control. + +Ltac2 may (f : 'a -> unit) (ov : 'a option) := + match ov with + | Some v => f v + | None => () + end. + +Ltac2 map (f : 'a -> 'b) (ov : 'a option) := + match ov with + | Some v => Some (f v) + | None => None + end. + +Ltac2 default (def : 'a) (ov : 'a option) := + match ov with + | Some v => v + | None => def + end. + +Ltac2 map_default (f : 'a -> 'b) (def : 'b) (ov : 'a option) := + match ov with + | Some v => f v + | None => def + end. + +Ltac2 get (ov : 'a option) := + match ov with + | Some v => v + | None => Control.throw No_value + end. + +Ltac2 get_bt (ov : 'a option) := + match ov with + | Some v => v + | None => Control.zero No_value + end. + +Ltac2 bind (x : 'a option) (f : 'a -> 'b option) := + match x with + | Some x => f x + | None => None + end. + +Ltac2 ret (x : 'a) := Some x. + +Ltac2 lift (f : 'a -> 'b) (x : 'a option) := map f x. diff --git a/vernac/search.ml b/vernac/search.ml index d9ab76b11b..a7f1dd33c2 100644 --- a/vernac/search.ml +++ b/vernac/search.ml @@ -200,12 +200,10 @@ let full_name_of_reference ref = DirPath.to_string dir ^ "." ^ Id.to_string id (** Whether a reference is blacklisted *) -let blacklist_filter_aux () = - let l = SearchBlacklist.elements () in - fun ref env typ -> +let blacklist_filter ref env typ = let name = full_name_of_reference ref in let is_not_bl str = not (String.string_contains ~where:name ~what:str) in - List.for_all is_not_bl l + CString.Set.for_all is_not_bl (SearchBlacklist.v ()) let module_filter (mods, outside) ref env typ = let sp = Nametab.path_of_global ref in @@ -227,7 +225,6 @@ let search_about_filter query gr env typ = match query with (** SearchPattern *) let search_pattern ?pstate gopt pat mods pr_search = - let blacklist_filter = blacklist_filter_aux () in let filter ref env typ = module_filter mods ref env typ && pattern_filter pat ref env (Evd.from_env env) (* FIXME *) (EConstr.of_constr typ) && @@ -251,7 +248,6 @@ let rewrite_pat2 pat = let search_rewrite ?pstate gopt pat mods pr_search = let pat1 = rewrite_pat1 pat in let pat2 = rewrite_pat2 pat in - let blacklist_filter = blacklist_filter_aux () in let filter ref env typ = module_filter mods ref env typ && (pattern_filter pat1 ref env (Evd.from_env env) (* FIXME *) (EConstr.of_constr typ) || @@ -266,7 +262,6 @@ let search_rewrite ?pstate gopt pat mods pr_search = (** Search *) let search_by_head ?pstate gopt pat mods pr_search = - let blacklist_filter = blacklist_filter_aux () in let filter ref env typ = module_filter mods ref env typ && head_filter pat ref env (Evd.from_env env) (* FIXME *) (EConstr.of_constr typ) && @@ -280,7 +275,6 @@ let search_by_head ?pstate gopt pat mods pr_search = (** SearchAbout *) let search_about ?pstate gopt items mods pr_search = - let blacklist_filter = blacklist_filter_aux () in let filter ref env typ = let eqb b1 b2 = if b1 then b2 else not b2 in module_filter mods ref env typ && @@ -324,7 +318,6 @@ let interface_search ?pstate = let (name, tpe, subtpe, mods, blacklist) = extract_flags [] [] [] [] false flags in - let blacklist_filter = blacklist_filter_aux () in let filter_function ref env constr = let id = Names.Id.to_string (Nametab.basename_of_global ref) in let path = Libnames.dirpath (Nametab.path_of_global ref) in @@ -378,6 +371,3 @@ let interface_search ?pstate = in let () = generic_search ?pstate glnum iter in !ans - -let blacklist_filter ref env typ = - blacklist_filter_aux () ref env typ |