diff options
66 files changed, 1623 insertions, 1148 deletions
diff --git a/.github/PULL_REQUEST_TEMPLATE.md b/.github/PULL_REQUEST_TEMPLATE.md index 86c15f6e8..4a8606a38 100644 --- a/.github/PULL_REQUEST_TEMPLATE.md +++ b/.github/PULL_REQUEST_TEMPLATE.md @@ -10,6 +10,9 @@ Fixes / closes #???? +<!-- If there is a user-visible change in coqc/coqtop/coqchk/coq_makefile behavior and testing is not prohibitively expensive: --> +<!-- (Otherwise, remove this line.) --> +- [ ] Added / updated test-suite <!-- If this is a feature pull request / breaks compatibility: --> <!-- (Otherwise, remove these lines.) --> - [ ] Corresponding documentation was added / updated (including any warning and error messages added / removed / modified). @@ -23,6 +23,8 @@ Tactics - Option "Ltac Debug" now applies also to terms built using Ltac functions. +- Deprecated the Implicit Tactic family of commands. + Tools - Coq_makefile lets one override or extend the following variables from @@ -125,7 +127,7 @@ Tactics profiling, and "Set NativeCompute Profile Filename" customizes the profile filename. - The tactic "omega" is now aware of the bodies of context variables - such as "x := 5 : Z" (see BZ#148). This could be disabled via + such as "x := 5 : Z" (see #1362). This could be disabled via Unset Omega UseLocalDefs. - The tactic "romega" is also aware now of the bodies of context variables. - The tactic "zify" resp. "omega with N" is now aware of N.pred. @@ -310,7 +312,7 @@ Improvements around some error messages. Many bug fixes including two important ones: -- BZ#5730: CoqIDE becomes unresponsive on file open. +- Bug #5730: CoqIDE becomes unresponsive on file open. - coq_makefile: make sure compile flags for Coq and coq_makefile are in sync (in particular, make sure the `-safe-string` option is used to compile plugins). @@ -360,7 +362,7 @@ Tactics which behave like the corresponding variants with no "e" but turn unresolved implicit arguments into existential variables, on the shelf, rather than failing. -- Tactic injection has become more powerful (closes BZ#4890) and its +- Tactic injection has become more powerful (closes bug #4890) and its documentation has been updated. - New variants of the `first` and `solve` tacticals that do not rely on parsing rules, meant to define tactic notations. @@ -406,7 +408,7 @@ Standard Library file ChoiceFacts.v. - New lemmas about iff and about orders on positive and Z. - New lemmas on powerRZ. -- Strengthened statement of JMeq_eq_dep (closes BZ#4912). +- Strengthened statement of JMeq_eq_dep (closes bug #4912). - The BigN, BigZ, BigZ libraries are no longer part of the Coq standard library, they are now provided by a separate repository https://github.com/coq/bignums @@ -481,12 +483,12 @@ XML Protocol and internal changes See dev/doc/changes.txt -Many bugfixes including BZ#1859, BZ#2884, BZ#3613, BZ#3943, BZ#3994, -BZ#4250, BZ#4709, BZ#4720, BZ#4824, BZ#4844, BZ#4911, BZ#5026, BZ#5233, -BZ#5275, BZ#5315, BZ#5336, BZ#5360, BZ#5390, BZ#5414, BZ#5417, BZ#5420, -BZ#5439, BZ#5449, BZ#5475, BZ#5476, BZ#5482, BZ#5501, BZ#5507, BZ#5520, -BZ#5523, BZ#5524, BZ#5553, BZ#5577, BZ#5578, BZ#5589, BZ#5597, BZ#5598, -BZ#5607, BZ#5618, BZ#5619, BZ#5620, BZ#5641, BZ#5648, BZ#5651, BZ#5671. +Many bugfixes including #1859, #2884, #3613, #3943, #3994, +#4250, #4709, #4720, #4824, #4844, #4911, #5026, #5233, +#5275, #5315, #5336, #5360, #5390, #5414, #5417, #5420, +#5439, #5449, #5475, #5476, #5482, #5501, #5507, #5520, +#5523, #5524, #5553, #5577, #5578, #5589, #5597, #5598, +#5607, #5618, #5619, #5620, #5641, #5648, #5651, #5671. Many bugfixes on OS X and Windows (now the test-suite passes on these platforms too). @@ -2662,7 +2664,7 @@ Tactics a registered setoid equality before starting to reduce in H. This is unlikely to break any script. Should this happen nonetheless, one can insert manually some "unfold ... in H" before rewriting. -- Fixed various bugs about (setoid) rewrite ... in ... (in particular BZ#1101) +- Fixed various bugs about (setoid) rewrite ... in ... (in particular bug #5941) - "rewrite ... in" now accepts a clause as place where to rewrite instead of juste a simple hypothesis name. For instance: rewrite H in H1,H2 |- * means rewrite H in H1; rewrite H in H2; rewrite H @@ -3239,11 +3241,11 @@ Incompatibilities Bugs - Improved localisation of errors in Syntactic Definitions -- Induction principle creation failure in presence of let-in fixed (BZ#238) -- Inversion bugs fixed (BZ#212 and BZ#220) -- Omega bug related to Set fixed (BZ#180) -- Type-checking inefficiency of nested destructuring let-in fixed (BZ#216) -- Improved handling of let-in during holes resolution phase (BZ#239) +- Induction principle creation failure in presence of let-in fixed (#1459) +- Inversion bugs fixed (#1427 and #1437) +- Omega bug related to Set fixed (#1384) +- Type-checking inefficiency of nested destructuring let-in fixed (#1435) +- Improved handling of let-in during holes resolution phase (#1460) Efficiency @@ -3256,18 +3258,18 @@ Changes from V7.3 to V7.3.1 Bug fixes - Corrupted Field tactic and Match Context tactic construction fixed - - Checking of names already existing in Assert added (BZ#182) - - Invalid argument bug in Exact tactic solved (BZ#183) - - Colliding bound names bug fixed (BZ#202) - - Wrong non-recursivity test for Record fixed (BZ#189) - - Out of memory/seg fault bug related to parametric inductive fixed (BZ#195) + - Checking of names already existing in Assert added (#1386) + - Invalid argument bug in Exact tactic solved (#1387) + - Colliding bound names bug fixed (#1412) + - Wrong non-recursivity test for Record fixed (#1394) + - Out of memory/seg fault bug related to parametric inductive fixed (#1404) - Setoid_replace/Setoid_rewrite bug wrt "==" fixed Misc - Ocaml version >= 3.06 is needed to compile Coq from sources - Simplification of fresh names creation strategy for Assert, Pose and - LetTac (BZ#192) + LetTac (#1402) Changes from V7.2 to V7.3 ========================= diff --git a/checker/closure.ml b/checker/closure.ml index 66e69f225..b9ae4daa8 100644 --- a/checker/closure.ml +++ b/checker/closure.ml @@ -754,7 +754,7 @@ let rec knr info m stk = | (_,args,s) -> (m,args@s)) | FCoFix _ when red_set info.i_flags fIOTA -> (match strip_update_shift_app m stk with - (_, args, (((ZcaseT _)::_) as stk')) -> + (_, args, (((ZcaseT _|Zproj _)::_) as stk')) -> let (fxe,fxbd) = contract_fix_vect m.term in knit info fxe fxbd (args@stk') | (_,args,s) -> (m,args@s)) diff --git a/clib/cList.ml b/clib/cList.ml index 7621793d4..646e39d23 100644 --- a/clib/cList.ml +++ b/clib/cList.ml @@ -19,25 +19,31 @@ sig val compare : 'a cmp -> 'a list cmp val equal : 'a eq -> 'a list eq val is_empty : 'a list -> bool - val init : int -> (int -> 'a) -> 'a list val mem_f : 'a eq -> 'a -> 'a list -> bool - val add_set : 'a eq -> 'a -> 'a list -> 'a list - val eq_set : 'a eq -> 'a list -> 'a list -> bool - val intersect : 'a eq -> 'a list -> 'a list -> 'a list - val union : 'a eq -> 'a list -> 'a list -> 'a list - val unionq : 'a list -> 'a list -> 'a list - val subtract : 'a eq -> 'a list -> 'a list -> 'a list - val subtractq : 'a list -> 'a list -> 'a list + val for_all_i : (int -> 'a -> bool) -> int -> 'a list -> bool + val for_all2eq : ('a -> 'b -> bool) -> 'a list -> 'b list -> bool + val prefix_of : 'a eq -> 'a list -> 'a list -> bool val interval : int -> int -> int list val make : int -> 'a -> 'a list + val addn : int -> 'a -> 'a list -> 'a list + val init : int -> (int -> 'a) -> 'a list + val append : 'a list -> 'a list -> 'a list + val concat : 'a list list -> 'a list + val flatten : 'a list list -> 'a list val assign : 'a list -> int -> 'a -> 'a list - val distinct : 'a list -> bool - val distinct_f : 'a cmp -> 'a list -> bool - val duplicates : 'a eq -> 'a list -> 'a list + val filter : ('a -> bool) -> 'a list -> 'a list val filter2 : ('a -> 'b -> bool) -> 'a list -> 'b list -> 'a list * 'b list + val filteri : + (int -> 'a -> bool) -> 'a list -> 'a list + val filter_with : bool list -> 'a list -> 'a list + val smartfilter : ('a -> bool) -> 'a list -> 'a list + [@@ocaml.deprecated "Same as [filter]"] val map_filter : ('a -> 'b option) -> 'a list -> 'b list val map_filter_i : (int -> 'a -> 'b option) -> 'a list -> 'b list - val filter_with : bool list -> 'a list -> 'a list + val partitioni : + (int -> 'a -> bool) -> 'a list -> 'a list * 'a list + val map : ('a -> 'b) -> 'a list -> 'b list + val map2 : ('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list val smartmap : ('a -> 'a) -> 'a list -> 'a list [@@ocaml.deprecated "Same as [Smart.map]"] val map_left : ('a -> 'b) -> 'a list -> 'b list @@ -48,18 +54,13 @@ sig ('a -> 'b -> 'c -> 'd) -> 'a list -> 'b list -> 'c list -> 'd list val map4 : ('a -> 'b -> 'c -> 'd -> 'e) -> 'a list -> 'b list -> 'c list -> 'd list -> 'e list - val filteri : - (int -> 'a -> bool) -> 'a list -> 'a list - val partitioni : - (int -> 'a -> bool) -> 'a list -> 'a list * 'a list val map_of_array : ('a -> 'b) -> 'a array -> 'b list - val smartfilter : ('a -> bool) -> 'a list -> 'a list - [@@ocaml.deprecated "Same as [Smart.map]"] + val map_append : ('a -> 'b list) -> 'a list -> 'b list + val map_append2 : ('a -> 'b -> 'c list) -> 'a list -> 'b list -> 'c list val extend : bool list -> 'a -> 'a list -> 'a list val count : ('a -> bool) -> 'a list -> int val index : 'a eq -> 'a -> 'a list -> int val index0 : 'a eq -> 'a -> 'a list -> int - val iteri : (int -> 'a -> unit) -> 'a list -> unit val fold_left_until : ('c -> 'a -> 'c CSig.until) -> 'c -> 'a list -> 'c val fold_right_i : (int -> 'a -> 'b -> 'b) -> int -> 'a list -> 'b -> 'b val fold_left_i : (int -> 'a -> 'b -> 'a) -> int -> 'a -> 'b list -> 'a @@ -67,62 +68,68 @@ sig ('a -> 'b -> 'b list -> 'a) -> 'b list -> 'a -> 'a val fold_left3 : ('a -> 'b -> 'c -> 'd -> 'a) -> 'a -> 'b list -> 'c list -> 'd list -> 'a val fold_left2_set : exn -> ('a -> 'b -> 'c -> 'b list -> 'c list -> 'a) -> 'a -> 'b list -> 'c list -> 'a - val for_all_i : (int -> 'a -> bool) -> int -> 'a list -> bool + val fold_left_map : ('a -> 'b -> 'a * 'c) -> 'a -> 'b list -> 'a * 'c list + val fold_right_map : ('b -> 'a -> 'c * 'a) -> 'b list -> 'a -> 'c list * 'a + val fold_left2_map : ('a -> 'b -> 'c -> 'a * 'd) -> 'a -> 'b list -> 'c list -> 'a * 'd list + val fold_right2_map : ('b -> 'c -> 'a -> 'd * 'a) -> 'b list -> 'c list -> 'a -> 'd list * 'a + val fold_left3_map : ('a -> 'b -> 'c -> 'd -> 'a * 'e) -> 'a -> 'b list -> 'c list -> 'd list -> 'a * 'e list + val fold_left4_map : ('a -> 'b -> 'c -> 'd -> 'e -> 'a * 'r) -> 'a -> 'b list -> 'c list -> 'd list -> 'e list -> 'a * 'r list + val fold_map : ('a -> 'b -> 'a * 'c) -> 'a -> 'b list -> 'a * 'c list + [@@ocaml.deprecated "Same as [fold_left_map]"] + val fold_map' : ('b -> 'a -> 'c * 'a) -> 'b list -> 'a -> 'c list * 'a + [@@ocaml.deprecated "Same as [fold_right_map]"] val except : 'a eq -> 'a -> 'a list -> 'a list val remove : 'a eq -> 'a -> 'a list -> 'a list val remove_first : ('a -> bool) -> 'a list -> 'a list val extract_first : ('a -> bool) -> 'a list -> 'a list * 'a - val insert : ('a -> 'a -> bool) -> 'a -> 'a list -> 'a list - val for_all2eq : ('a -> 'b -> bool) -> 'a list -> 'b list -> bool - val sep_last : 'a list -> 'a * 'a list val find_map : ('a -> 'b option) -> 'a list -> 'b - val uniquize : 'a list -> 'a list - val sort_uniquize : 'a cmp -> 'a list -> 'a list - val merge_uniq : ('a -> 'a -> int) -> 'a list -> 'a list -> 'a list - val subset : 'a list -> 'a list -> bool - val chop : int -> 'a list -> 'a list * 'a list exception IndexOutOfRange val goto : int -> 'a list -> 'a list * 'a list val split_when : ('a -> bool) -> 'a list -> 'a list * 'a list - val split3 : ('a * 'b * 'c) list -> 'a list * 'b list * 'c list - val firstn : int -> 'a list -> 'a list + val sep_last : 'a list -> 'a * 'a list + val drop_last : 'a list -> 'a list val last : 'a list -> 'a val lastn : int -> 'a list -> 'a list + val chop : int -> 'a list -> 'a list * 'a list + val firstn : int -> 'a list -> 'a list val skipn : int -> 'a list -> 'a list val skipn_at_least : int -> 'a list -> 'a list - val addn : int -> 'a -> 'a list -> 'a list - val prefix_of : 'a eq -> 'a list -> 'a list -> bool val drop_prefix : 'a eq -> 'a list -> 'a list -> 'a list - val drop_last : 'a list -> 'a list - val map_append : ('a -> 'b list) -> 'a list -> 'b list - val map_append2 : ('a -> 'b -> 'c list) -> 'a list -> 'b list -> 'c list + val insert : ('a -> 'a -> bool) -> 'a -> 'a list -> 'a list val share_tails : 'a list -> 'a list -> 'a list * 'a list * 'a list - val fold_left_map : ('a -> 'b -> 'a * 'c) -> 'a -> 'b list -> 'a * 'c list - val fold_right_map : ('b -> 'a -> 'c * 'a) -> 'b list -> 'a -> 'c list * 'a - val fold_left2_map : ('a -> 'b -> 'c -> 'a * 'd) -> 'a -> 'b list -> 'c list -> 'a * 'd list - val fold_right2_map : ('b -> 'c -> 'a -> 'd * 'a) -> 'b list -> 'c list -> 'a -> 'd list * 'a - val fold_left3_map : ('a -> 'b -> 'c -> 'd -> 'a * 'e) -> 'a -> 'b list -> 'c list -> 'd list -> 'a * 'e list - val fold_left4_map : ('a -> 'b -> 'c -> 'd -> 'e -> 'a * 'r) -> 'a -> 'b list -> 'c list -> 'd list -> 'e list -> 'a * 'r list - val fold_map : ('a -> 'b -> 'a * 'c) -> 'a -> 'b list -> 'a * 'c list - [@@ocaml.deprecated "Same as [fold_left_map]"] - val fold_map' : ('b -> 'a -> 'c * 'a) -> 'b list -> 'a -> 'c list * 'a - [@@ocaml.deprecated "Same as [fold_right_map]"] val map_assoc : ('a -> 'b) -> ('c * 'a) list -> ('c * 'b) list val assoc_f : 'a eq -> 'a -> ('a * 'b) list -> 'b val remove_assoc_f : 'a eq -> 'a -> ('a * 'b) list -> ('a * 'b) list val mem_assoc_f : 'a eq -> 'a -> ('a * 'b) list -> bool + val factorize_left : 'a eq -> ('a * 'b) list -> ('a * 'b list) list + val split : ('a * 'b) list -> 'a list * 'b list + val combine : 'a list -> 'b list -> ('a * 'b) list + val split3 : ('a * 'b * 'c) list -> 'a list * 'b list * 'c list + val combine3 : 'a list -> 'b list -> 'c list -> ('a * 'b * 'c) list + val add_set : 'a eq -> 'a -> 'a list -> 'a list + val eq_set : 'a eq -> 'a list -> 'a list -> bool + val subset : 'a list -> 'a list -> bool + val merge_set : 'a cmp -> 'a list -> 'a list -> 'a list + val intersect : 'a eq -> 'a list -> 'a list -> 'a list + val union : 'a eq -> 'a list -> 'a list -> 'a list + val unionq : 'a list -> 'a list -> 'a list + val subtract : 'a eq -> 'a list -> 'a list -> 'a list + val subtractq : 'a list -> 'a list -> 'a list + val merge_uniq : ('a -> 'a -> int) -> 'a list -> 'a list -> 'a list + val distinct : 'a list -> bool + val distinct_f : 'a cmp -> 'a list -> bool + val duplicates : 'a eq -> 'a list -> 'a list + val uniquize : 'a list -> 'a list + val sort_uniquize : 'a cmp -> 'a list -> 'a list val cartesian : ('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list val cartesians : ('a -> 'b -> 'b) -> 'b -> 'a list list -> 'b list val combinations : 'a list list -> 'a list list - val combine3 : 'a list -> 'b list -> 'c list -> ('a * 'b * 'c) list val cartesians_filter : ('a -> 'b -> 'b option) -> 'b -> 'a list list -> 'b list - val factorize_left : 'a eq -> ('a * 'b) list -> ('a * 'b list) list module Smart : sig val map : ('a -> 'a) -> 'a list -> 'a list - val filter : ('a -> bool) -> 'a list -> 'a list end module type MonoS = sig @@ -149,71 +156,71 @@ type 'a cell = { external cast : 'a cell -> 'a list = "%identity" -let rec map_loop f p = function -| [] -> () -| x :: l -> - let c = { head = f x; tail = [] } in - p.tail <- cast c; - map_loop f c l +(** Extensions and redefinitions of OCaml Stdlib *) -let map f = function -| [] -> [] -| x :: l -> - let c = { head = f x; tail = [] } in - map_loop f c l; - cast c +(** {6 Equality, testing} *) -let rec map2_loop f p l1 l2 = match l1, l2 with -| [], [] -> () -| x :: l1, y :: l2 -> - let c = { head = f x y; tail = [] } in - p.tail <- cast c; - map2_loop f c l1 l2 -| _ -> invalid_arg "List.map2" +let rec compare cmp l1 l2 = + if l1 == l2 then 0 else + match l1,l2 with + | [], [] -> 0 + | _::_, [] -> 1 + | [], _::_ -> -1 + | x1::l1, x2::l2 -> + match cmp x1 x2 with + | 0 -> compare cmp l1 l2 + | c -> c -let map2 f l1 l2 = match l1, l2 with -| [], [] -> [] -| x :: l1, y :: l2 -> - let c = { head = f x y; tail = [] } in - map2_loop f c l1 l2; - cast c -| _ -> invalid_arg "List.map2" +let rec equal cmp l1 l2 = + l1 == l2 || + match l1, l2 with + | [], [] -> true + | x1 :: l1, x2 :: l2 -> cmp x1 x2 && equal cmp l1 l2 + | _ -> false -let rec map_of_array_loop f p a i l = - if Int.equal i l then () - else - let c = { head = f (Array.unsafe_get a i); tail = [] } in - p.tail <- cast c; - map_of_array_loop f c a (i + 1) l +let is_empty = function + | [] -> true + | _ -> false -let map_of_array f a = - let l = Array.length a in - if Int.equal l 0 then [] - else - let c = { head = f (Array.unsafe_get a 0); tail = [] } in - map_of_array_loop f c a 1 l; - cast c +let mem_f cmp x l = + List.exists (cmp x) l -let rec append_loop p tl = function -| [] -> p.tail <- tl -| x :: l -> - let c = { head = x; tail = [] } in - p.tail <- cast c; - append_loop c tl l +let for_all_i p = + let rec for_all_p i = function + | [] -> true + | a::l -> p i a && for_all_p (i+1) l + in + for_all_p -let append l1 l2 = match l1 with -| [] -> l2 -| x :: l -> - let c = { head = x; tail = [] } in - append_loop c l2 l; - cast c +let for_all2eq f l1 l2 = + try List.for_all2 f l1 l2 with Invalid_argument _ -> false -let rec copy p = function -| [] -> p -| x :: l -> - let c = { head = x; tail = [] } in - p.tail <- cast c; - copy c l +let prefix_of cmp prefl l = + let rec prefrec = function + | (h1::t1, h2::t2) -> cmp h1 h2 && prefrec (t1,t2) + | ([], _) -> true + | _ -> false + in + prefrec (prefl,l) + +(** {6 Creating lists} *) + +let interval n m = + let rec interval_n (l,m) = + if n > m then l else interval_n (m::l, pred m) + in + interval_n ([], m) + +let addn n v = + let rec aux n l = + if Int.equal n 0 then l + else aux (pred n) (v :: l) + in + if n < 0 then invalid_arg "List.addn" + else aux n + +let make n v = + addn n v [] let rec init_loop len f p i = if Int.equal i len then () @@ -230,9 +237,30 @@ let init len f = init_loop len f c 1; cast c +let rec append_loop p tl = function + | [] -> p.tail <- tl + | x :: l -> + let c = { head = x; tail = [] } in + p.tail <- cast c; + append_loop c tl l + +let append l1 l2 = match l1 with + | [] -> l2 + | x :: l -> + let c = { head = x; tail = [] } in + append_loop c l2 l; + cast c + +let rec copy p = function + | [] -> p + | x :: l -> + let c = { head = x; tail = [] } in + p.tail <- cast c; + copy c l + let rec concat_loop p = function -| [] -> () -| x :: l -> concat_loop (copy p x) l + | [] -> () + | x :: l -> concat_loop (copy p x) l let concat l = let dummy = { head = Obj.magic 0; tail = [] } in @@ -241,214 +269,308 @@ let concat l = let flatten = concat -let rec split_loop p q = function -| [] -> () -| (x, y) :: l -> - let cl = { head = x; tail = [] } in - let cr = { head = y; tail = [] } in - p.tail <- cast cl; - q.tail <- cast cr; - split_loop cl cr l - -let split = function -| [] -> [], [] -| (x, y) :: l -> - let cl = { head = x; tail = [] } in - let cr = { head = y; tail = [] } in - split_loop cl cr l; - (cast cl, cast cr) +(** {6 Lists as arrays} *) -let rec combine_loop p l1 l2 = match l1, l2 with -| [], [] -> () -| x :: l1, y :: l2 -> - let c = { head = (x, y); tail = [] } in - p.tail <- cast c; - combine_loop c l1 l2 -| _ -> invalid_arg "List.combine" +let assign l n e = + let rec assrec stk l i = match l, i with + | (h :: t, 0) -> List.rev_append stk (e :: t) + | (h :: t, n) -> assrec (h :: stk) t (pred n) + | ([], _) -> failwith "List.assign" + in + assrec [] l n -let combine l1 l2 = match l1, l2 with -| [], [] -> [] -| x :: l1, y :: l2 -> - let c = { head = (x, y); tail = [] } in - combine_loop c l1 l2; - cast c -| _ -> invalid_arg "List.combine" +(** {6 Filtering} *) let rec filter_loop f p = function -| [] -> () -| x :: l -> - if f x then - let c = { head = x; tail = [] } in - let () = p.tail <- cast c in - filter_loop f c l - else - filter_loop f p l + | [] -> () + | x :: l' as l -> + let b = f x in + filter_loop f p l'; + if b then if p.tail == l' then p.tail <- l else p.tail <- x :: p.tail -let filter f l = - let c = { head = Obj.magic 0; tail = [] } in - filter_loop f c l; - c.tail +let rec filter f = function + | [] -> [] + | x :: l' as l -> + if f x then + let c = { head = x; tail = [] } in + filter_loop f c l'; + if c.tail == l' then l else cast c + else + filter f l' -(** FIXME: Already present in OCaml 4.00 *) +let rec filter2_loop f p q l1 l2 = match l1, l2 with + | [], [] -> () + | x :: l1', y :: l2' -> + let b = f x y in + filter2_loop f p q l1' l2'; + if b then + if p.tail == l1' then begin + p.tail <- l1; + q.tail <- l2 + end + else begin + p.tail <- x :: p.tail; + q.tail <- y :: q.tail + end + | _ -> invalid_arg "List.filter2" + +let rec filter2 f l1 l2 = match l1, l2 with + | [], [] -> ([],[]) + | x1 :: l1', x2 :: l2' -> + let b = f x1 x2 in + if b then + let c1 = { head = x1; tail = [] } in + let c2 = { head = x2; tail = [] } in + filter2_loop f c1 c2 l1' l2'; + if c1.tail == l1' then (l1, l2) else (cast c1, cast c2) + else + filter2 f l1' l2' + | _ -> invalid_arg "List.filter2" -let rec map_i_loop f i p = function -| [] -> () -| x :: l -> - let c = { head = f i x; tail = [] } in - p.tail <- cast c; - map_i_loop f (succ i) c l +let filteri p = + let rec filter_i_rec i = function + | [] -> [] + | x :: l -> let l' = filter_i_rec (succ i) l in if p i x then x :: l' else l' + in + filter_i_rec 0 -let map_i f i = function -| [] -> [] -| x :: l -> - let c = { head = f i x; tail = [] } in - map_i_loop f (succ i) c l; - cast c +let smartfilter = filter (* Alias *) -(** Extensions of OCaml Stdlib *) +let rec filter_with_loop filter p l = match filter, l with + | [], [] -> () + | b :: filter, x :: l' -> + filter_with_loop filter p l'; + if b then if p.tail == l' then p.tail <- l else p.tail <- x :: p.tail + | _ -> invalid_arg "List.filter_with" -let rec compare cmp l1 l2 = - if l1 == l2 then 0 else - match l1,l2 with - [], [] -> 0 - | _::_, [] -> 1 - | [], _::_ -> -1 - | x1::l1, x2::l2 -> - (match cmp x1 x2 with - | 0 -> compare cmp l1 l2 - | c -> c) +let rec filter_with filter l = match filter, l with + | [], [] -> [] + | b :: filter, x :: l' -> + if b then + let c = { head = x; tail = [] } in + filter_with_loop filter c l'; + if c.tail == l' then l else cast c + else filter_with filter l' + | _ -> invalid_arg "List.filter_with" -let rec equal cmp l1 l2 = - l1 == l2 || - match l1, l2 with - | [], [] -> true - | x1 :: l1, x2 :: l2 -> - cmp x1 x2 && equal cmp l1 l2 - | _ -> false +let rec map_filter_loop f p = function + | [] -> () + | x :: l -> + match f x with + | None -> map_filter_loop f p l + | Some y -> + let c = { head = y; tail = [] } in + p.tail <- cast c; + map_filter_loop f c l -let is_empty = function -| [] -> true -| _ -> false +let rec map_filter f = function + | [] -> [] + | x :: l' -> + match f x with + | None -> map_filter f l' + | Some y -> + let c = { head = y; tail = [] } in + map_filter_loop f c l'; + cast c -let mem_f cmp x l = List.exists (cmp x) l +let rec map_filter_i_loop f i p = function + | [] -> () + | x :: l -> + match f i x with + | None -> map_filter_i_loop f (succ i) p l + | Some y -> + let c = { head = y; tail = [] } in + p.tail <- cast c; + map_filter_i_loop f (succ i) c l -let intersect cmp l1 l2 = - filter (fun x -> mem_f cmp x l2) l1 +let rec map_filter_i_loop' f i = function + | [] -> [] + | x :: l' -> + match f i x with + | None -> map_filter_i_loop' f (succ i) l' + | Some y -> + let c = { head = y; tail = [] } in + map_filter_i_loop f (succ i) c l'; + cast c -let union cmp l1 l2 = - let rec urec = function - | [] -> l2 - | a::l -> if mem_f cmp a l2 then urec l else a::urec l +let map_filter_i f l = + map_filter_i_loop' f 0 l + +let partitioni p = + let rec aux i = function + | [] -> [], [] + | x :: l -> + let (l1, l2) = aux (succ i) l in + if p i x then (x :: l1, l2) + else (l1, x :: l2) in - urec l1 + aux 0 -let subtract cmp l1 l2 = - if is_empty l2 then l1 - else List.filter (fun x -> not (mem_f cmp x l2)) l1 +(** {6 Applying functorially} *) -let unionq l1 l2 = union (==) l1 l2 -let subtractq l1 l2 = subtract (==) l1 l2 +let rec map_loop f p = function + | [] -> () + | x :: l -> + let c = { head = f x; tail = [] } in + p.tail <- cast c; + map_loop f c l -let interval n m = - let rec interval_n (l,m) = - if n > m then l else interval_n (m::l, pred m) - in - interval_n ([], m) +let map f = function + | [] -> [] + | x :: l -> + let c = { head = f x; tail = [] } in + map_loop f c l; + cast c -let addn n v = - let rec aux n l = - if Int.equal n 0 then l - else aux (pred n) (v :: l) - in - if n < 0 then invalid_arg "List.addn" - else aux n +let rec map2_loop f p l1 l2 = match l1, l2 with + | [], [] -> () + | x :: l1, y :: l2 -> + let c = { head = f x y; tail = [] } in + p.tail <- cast c; + map2_loop f c l1 l2 + | _ -> invalid_arg "List.map2" -let make n v = addn n v [] +let map2 f l1 l2 = match l1, l2 with + | [], [] -> [] + | x :: l1, y :: l2 -> + let c = { head = f x y; tail = [] } in + map2_loop f c l1 l2; + cast c + | _ -> invalid_arg "List.map2" -let assign l n e = - let rec assrec stk l i = match l, i with - | ((h::t), 0) -> List.rev_append stk (e :: t) - | ((h::t), n) -> assrec (h :: stk) t (pred n) - | ([], _) -> failwith "List.assign" - in - assrec [] l n +(** Like OCaml [List.mapi] but tail-recursive *) + +let rec map_i_loop f i p = function + | [] -> () + | x :: l -> + let c = { head = f i x; tail = [] } in + p.tail <- cast c; + map_i_loop f (succ i) c l + +let map_i f i = function + | [] -> [] + | x :: l -> + let c = { head = f i x; tail = [] } in + map_i_loop f (succ i) c l; + cast c let map_left = map let map2_i f i l1 l2 = let rec map_i i = function | ([], []) -> [] - | ((h1::t1), (h2::t2)) -> let v = f i h1 h2 in v :: map_i (succ i) (t1,t2) + | (h1 :: t1, h2 :: t2) -> let v = f i h1 h2 in v :: map_i (succ i) (t1,t2) | (_, _) -> invalid_arg "map2_i" in map_i i (l1,l2) -let map3 f l1 l2 l3 = - let rec map = function - | ([], [], []) -> [] - | ((h1::t1), (h2::t2), (h3::t3)) -> let v = f h1 h2 h3 in v::map (t1,t2,t3) - | (_, _, _) -> invalid_arg "map3" - in - map (l1,l2,l3) +let rec map3_loop f p l1 l2 l3 = match l1, l2, l3 with + | [], [], [] -> () + | x :: l1, y :: l2, z :: l3 -> + let c = { head = f x y z; tail = [] } in + p.tail <- cast c; + map3_loop f c l1 l2 l3 + | _ -> invalid_arg "List.map3" -let map4 f l1 l2 l3 l4 = - let rec map = function - | ([], [], [], []) -> [] - | ((h1::t1), (h2::t2), (h3::t3), (h4::t4)) -> let v = f h1 h2 h3 h4 in v::map (t1,t2,t3,t4) - | (_, _, _, _) -> invalid_arg "map4" - in - map (l1,l2,l3,l4) +let map3 f l1 l2 l3 = match l1, l2, l3 with + | [], [], [] -> [] + | x :: l1, y :: l2, z :: l3 -> + let c = { head = f x y z; tail = [] } in + map3_loop f c l1 l2 l3; + cast c + | _ -> invalid_arg "List.map3" + +let rec map4_loop f p l1 l2 l3 l4 = match l1, l2, l3, l4 with + | [], [], [], [] -> () + | x :: l1, y :: l2, z :: l3, t :: l4 -> + let c = { head = f x y z t; tail = [] } in + p.tail <- cast c; + map4_loop f c l1 l2 l3 l4 + | _ -> invalid_arg "List.map4" + +let map4 f l1 l2 l3 l4 = match l1, l2, l3, l4 with + | [], [], [], [] -> [] + | x :: l1, y :: l2, z :: l3, t :: l4 -> + let c = { head = f x y z t; tail = [] } in + map4_loop f c l1 l2 l3 l4; + cast c + | _ -> invalid_arg "List.map4" + +let rec map_of_array_loop f p a i l = + if Int.equal i l then () + else + let c = { head = f (Array.unsafe_get a i); tail = [] } in + p.tail <- cast c; + map_of_array_loop f c a (i + 1) l + +let map_of_array f a = + let l = Array.length a in + if Int.equal l 0 then [] + else + let c = { head = f (Array.unsafe_get a 0); tail = [] } in + map_of_array_loop f c a 1 l; + cast c + +let map_append f l = flatten (map f l) + +let map_append2 f l1 l2 = flatten (map2 f l1 l2) let rec extend l a l' = match l,l' with - | true::l, b::l' -> b :: extend l a l' - | false::l, l' -> a :: extend l a l' + | true :: l, b :: l' -> b :: extend l a l' + | false :: l, l' -> a :: extend l a l' | [], [] -> [] | _ -> invalid_arg "extend" let count f l = let rec aux acc = function | [] -> acc - | h :: t -> if f h then aux (acc + 1) t else aux acc t in + | h :: t -> if f h then aux (acc + 1) t else aux acc t + in aux 0 l +(** {6 Finding position} *) + let rec index_f f x l n = match l with -| [] -> raise Not_found -| y :: l -> if f x y then n else index_f f x l (succ n) + | [] -> raise Not_found + | y :: l -> if f x y then n else index_f f x l (succ n) let index f x l = index_f f x l 1 let index0 f x l = index_f f x l 0 +(** {6 Folding} *) + let fold_left_until f accu s = let rec aux accu = function | [] -> accu - | x :: xs -> match f accu x with CSig.Stop x -> x | CSig.Cont i -> aux i xs in + | x :: xs -> match f accu x with CSig.Stop x -> x | CSig.Cont i -> aux i xs + in aux accu s let fold_right_i f i l = let rec it_f i l a = match l with | [] -> a - | b::l -> f (i-1) b (it_f (i-1) l a) + | b :: l -> f (i-1) b (it_f (i-1) l a) in it_f (List.length l + i) l let fold_left_i f = let rec it_list_f i a = function | [] -> a - | b::l -> it_list_f (i+1) (f i a b) l + | b :: l -> it_list_f (i+1) (f i a b) l in it_list_f let rec fold_left3 f accu l1 l2 l3 = match (l1, l2, l3) with - ([], [], []) -> accu - | (a1::l1, a2::l2, a3::l3) -> fold_left3 f (f accu a1 a2 a3) l1 l2 l3 + | ([], [], []) -> accu + | (a1 :: l1, a2 :: l2, a3 :: l3) -> fold_left3 f (f accu a1 a2 a3) l1 l2 l3 | (_, _, _) -> invalid_arg "List.fold_left3" let rec fold_left4 f accu l1 l2 l3 l4 = match (l1, l2, l3, l4) with - ([], [], [], []) -> accu - | (a1::l1, a2::l2, a3::l3, a4::l4) -> fold_left4 f (f accu a1 a2 a3 a4) l1 l2 l3 l4 + | ([], [], [], []) -> accu + | (a1 :: l1, a2 :: l2, a3 :: l3, a4 :: l4) -> fold_left4 f (f accu a1 a2 a3 a4) l1 l2 l3 l4 | (_,_, _, _) -> invalid_arg "List.fold_left4" (* [fold_right_and_left f [a1;...;an] hd = @@ -466,214 +588,103 @@ let rec fold_left4 f accu l1 l2 l3 l4 = let fold_right_and_left f l hd = let rec aux tl = function | [] -> hd - | a::l -> let hd = aux (a::tl) l in f hd a tl - in aux [] l + | a :: l -> let hd = aux (a :: tl) l in f hd a tl + in + aux [] l (* Match sets as lists according to a matching function, also folding a side effect *) let rec fold_left2_set e f x l1 l2 = match l1 with - | a1::l1 -> - let rec find seen = function - | [] -> raise e - | a2::l2 -> - try fold_left2_set e f (f x a1 a2 l1 l2) l1 (List.rev_append seen l2) - with e' when e' = e -> find (a2::seen) l2 in - find [] l2 + | a1 :: l1 -> + let rec find seen = function + | [] -> raise e + | a2 :: l2 -> + try fold_left2_set e f (f x a1 a2 l1 l2) l1 (List.rev_append seen l2) + with e' when e' = e -> find (a2 :: seen) l2 in + find [] l2 | [] -> - if l2 = [] then x else raise e + if l2 = [] then x else raise e -let iteri f l = fold_left_i (fun i _ x -> f i x) 0 () l +(* Poor man's monadic map *) +let rec fold_left_map f e = function + | [] -> (e,[]) + | h :: t -> + let e',h' = f e h in + let e'',t' = fold_left_map f e' t in + e'',h' :: t' -let for_all_i p = - let rec for_all_p i = function - | [] -> true - | a::l -> p i a && for_all_p (i+1) l +let fold_map = fold_left_map + +(* (* tail-recursive version of the above function *) +let fold_left_map f e l = + let g (e,b') h = + let (e',h') = f e h in + (e',h'::b') in - for_all_p + let (e',lrev) = List.fold_left g (e,[]) l in + (e',List.rev lrev) +*) + +(* The same, based on fold_right, with the effect accumulated on the right *) +let fold_right_map f l e = + List.fold_right (fun x (l,e) -> let (y,e) = f x e in (y::l,e)) l ([],e) + +let fold_map' = fold_right_map + +let on_snd f (x,y) = (x,f y) + +let fold_left2_map f e l l' = + on_snd List.rev @@ + List.fold_left2 (fun (e,l) x x' -> + let (e,y) = f e x x' in + (e, y::l) + ) (e, []) l l' + +let fold_right2_map f l l' e = + List.fold_right2 (fun x x' (l,e) -> let (y,e) = f x x' e in (y::l,e)) l l' ([],e) + +let fold_left3_map f e l l' l'' = + on_snd List.rev @@ + fold_left3 (fun (e,l) x x' x'' -> let (e,y) = f e x x' x'' in (e,y::l)) (e,[]) l l' l'' + +let fold_left4_map f e l1 l2 l3 l4 = + on_snd List.rev @@ + fold_left4 (fun (e,l) x1 x2 x3 x4 -> let (e,y) = f e x1 x2 x3 x4 in (e,y::l)) (e,[]) l1 l2 l3 l4 + +(** {6 Splitting} *) -let except cmp x l = List.filter (fun y -> not (cmp x y)) l +let except cmp x l = + List.filter (fun y -> not (cmp x y)) l let remove = except (* Alias *) let rec remove_first p = function - | b::l when p b -> l - | b::l -> b::remove_first p l + | b :: l when p b -> l + | b :: l -> b :: remove_first p l | [] -> raise Not_found let extract_first p li = let rec loop rev_left = function | [] -> raise Not_found - | x::right -> + | x :: right -> if p x then List.rev_append rev_left right, x else loop (x :: rev_left) right - in loop [] li + in + loop [] li let insert p v l = let rec insrec = function | [] -> [v] - | h::tl -> if p v h then v::h::tl else h::insrec tl + | h :: tl -> if p v h then v :: h :: tl else h :: insrec tl in insrec l -let add_set cmp x l = if mem_f cmp x l then l else x :: l - -(** List equality up to permutation (but considering multiple occurrences) *) - -let eq_set cmp l1 l2 = - let rec aux l1 = function - | [] -> is_empty l1 - | a::l2 -> aux (remove_first (cmp a) l1) l2 in - try aux l1 l2 with Not_found -> false - -let for_all2eq f l1 l2 = - try List.for_all2 f l1 l2 with Invalid_argument _ -> false - -let filteri p = - let rec filter_i_rec i = function - | [] -> [] - | x::l -> let l' = filter_i_rec (succ i) l in if p i x then x::l' else l' - in - filter_i_rec 0 - -let partitioni p = - let rec aux i = function - | [] -> [], [] - | x :: l -> - let (l1, l2) = aux (succ i) l in - if p i x then (x :: l1, l2) - else (l1, x :: l2) - in aux 0 - -let rec sep_last = function - | [] -> failwith "sep_last" - | hd::[] -> (hd,[]) - | hd::tl -> let (l,tl) = sep_last tl in (l,hd::tl) - let rec find_map f = function -| [] -> raise Not_found -| x :: l -> - match f x with - | None -> find_map f l - | Some y -> y - -(* FIXME: we should avoid relying on the generic hash function, - just as we'd better avoid Pervasives.compare *) - -let uniquize l = - let visited = Hashtbl.create 23 in - let rec aux acc changed = function - | h::t -> if Hashtbl.mem visited h then aux acc true t else - begin - Hashtbl.add visited h h; - aux (h::acc) changed t - end - | [] -> if changed then List.rev acc else l - in aux [] false l - -(** [sort_uniquize] might be an alternative to the hashtbl-based - [uniquize], when the order of the elements is irrelevant *) - -let rec uniquize_sorted cmp = function - | a::b::l when Int.equal (cmp a b) 0 -> uniquize_sorted cmp (a::l) - | a::l -> a::uniquize_sorted cmp l - | [] -> [] - -let sort_uniquize cmp l = uniquize_sorted cmp (List.sort cmp l) - -(* FIXME: again, generic hash function *) - -let distinct l = - let visited = Hashtbl.create 23 in - let rec loop = function - | h::t -> - if Hashtbl.mem visited h then false - else - begin - Hashtbl.add visited h h; - loop t - end - | [] -> true - in loop l - -let distinct_f cmp l = - let rec loop = function - | a::b::_ when Int.equal (cmp a b) 0 -> false - | a::l -> loop l - | [] -> true - in loop (List.sort cmp l) - -let rec merge_uniq cmp l1 l2 = - match l1, l2 with - | [], l2 -> l2 - | l1, [] -> l1 - | h1 :: t1, h2 :: t2 -> - let c = cmp h1 h2 in - if Int.equal c 0 - then h1 :: merge_uniq cmp t1 t2 - else if c <= 0 - then h1 :: merge_uniq cmp t1 l2 - else h2 :: merge_uniq cmp l1 t2 - -let rec duplicates cmp = function - | [] -> [] - | x::l -> - let l' = duplicates cmp l in - if mem_f cmp x l then add_set cmp x l' else l' - -let rec filter2_loop f p q l1 l2 = match l1, l2 with -| [], [] -> () -| x :: l1, y :: l2 -> - if f x y then - let c1 = { head = x; tail = [] } in - let c2 = { head = y; tail = [] } in - let () = p.tail <- cast c1 in - let () = q.tail <- cast c2 in - filter2_loop f c1 c2 l1 l2 - else - filter2_loop f p q l1 l2 -| _ -> invalid_arg "List.filter2" - -let filter2 f l1 l2 = - let c1 = { head = Obj.magic 0; tail = [] } in - let c2 = { head = Obj.magic 0; tail = [] } in - filter2_loop f c1 c2 l1 l2; - (c1.tail, c2.tail) - -let rec map_filter_loop f p = function - | [] -> () + | [] -> raise Not_found | x :: l -> match f x with - | None -> map_filter_loop f p l - | Some y -> - let c = { head = y; tail = [] } in - p.tail <- cast c; - map_filter_loop f c l - -let map_filter f l = - let c = { head = Obj.magic 0; tail = [] } in - map_filter_loop f c l; - c.tail - -let rec map_filter_i_loop f i p = function - | [] -> () - | x :: l -> - match f i x with - | None -> map_filter_i_loop f (succ i) p l - | Some y -> - let c = { head = y; tail = [] } in - p.tail <- cast c; - map_filter_i_loop f (succ i) c l - -let map_filter_i f l = - let c = { head = Obj.magic 0; tail = [] } in - map_filter_i_loop f 0 c l; - c.tail - -let rec filter_with filter l = match filter, l with -| [], [] -> [] -| true :: filter, x :: l -> x :: filter_with filter l -| false :: filter, _ :: l -> filter_with filter l -| _ -> invalid_arg "List.filter_with" + | None -> find_map f l + | Some y -> y (* FIXME: again, generic hash function *) @@ -682,7 +693,7 @@ let subset l1 l2 = List.iter (fun x -> Hashtbl.add t2 x ()) l2; let rec look = function | [] -> true - | x::ll -> try Hashtbl.find t2 x; look ll with Not_found -> false + | x :: ll -> try Hashtbl.find t2 x; look ll with Not_found -> false in look l1 @@ -694,7 +705,7 @@ exception IndexOutOfRange let goto n l = let rec goto i acc = function | tl when Int.equal i 0 -> (acc, tl) - | h::t -> goto (pred i) (h::acc) t + | h :: t -> goto (pred i) (h :: acc) t | [] -> raise IndexOutOfRange in goto n [] l @@ -715,29 +726,36 @@ let chop n l = let split_when p = let rec split_when_loop x y = match y with - | [] -> (List.rev x,[]) - | (a::l) -> if (p a) then (List.rev x,y) else split_when_loop (a::x) l + | [] -> (List.rev x,[]) + | (a :: l) -> if (p a) then (List.rev x,y) else split_when_loop (a :: x) l in split_when_loop [] -let rec split3 = function - | [] -> ([], [], []) - | (x,y,z)::l -> - let (rx, ry, rz) = split3 l in (x::rx, y::ry, z::rz) - let firstn n l = let rec aux acc n l = match n, l with | 0, _ -> List.rev acc - | n, h::t -> aux (h::acc) (pred n) t + | n, h :: t -> aux (h :: acc) (pred n) t | _ -> failwith "firstn" in aux [] n l +let rec sep_last = function + | [] -> failwith "sep_last" + | hd :: [] -> (hd,[]) + | hd :: tl -> let (l,tl) = sep_last tl in (l,hd :: tl) + +(* Drop the last element of a list *) + +let rec drop_last = function + | [] -> failwith "drop_last" + | hd :: [] -> [] + | hd :: tl -> hd :: drop_last tl + let rec last = function | [] -> failwith "List.last" - | [x] -> x - | _ :: l -> last l + | hd :: [] -> hd + | _ :: tl -> last tl let lastn n l = let len = List.length l in @@ -749,96 +767,216 @@ let lastn n l = let rec skipn n l = match n,l with | 0, _ -> l | _, [] -> failwith "List.skipn" - | n, _::l -> skipn (pred n) l + | n, _ :: l -> skipn (pred n) l let skipn_at_least n l = - try skipn n l with Failure _ -> [] - -let prefix_of cmp prefl l = - let rec prefrec = function - | (h1::t1, h2::t2) -> cmp h1 h2 && prefrec (t1,t2) - | ([], _) -> true - | _ -> false - in - prefrec (prefl,l) + try skipn n l with Failure _ when n >= 0 -> [] (** if [l=p++t] then [drop_prefix p l] is [t] else [l] *) let drop_prefix cmp p l = let rec drop_prefix_rec = function - | (h1::tp, h2::tl) when cmp h1 h2 -> drop_prefix_rec (tp,tl) + | (h1 :: tp, h2 :: tl) when cmp h1 h2 -> drop_prefix_rec (tp,tl) | ([], tl) -> tl | _ -> l in drop_prefix_rec (p,l) -let map_append f l = List.flatten (List.map f l) - -let map_append2 f l1 l2 = List.flatten (List.map2 f l1 l2) - let share_tails l1 l2 = let rec shr_rev acc = function - | ((x1::l1), (x2::l2)) when x1 == x2 -> shr_rev (x1::acc) (l1,l2) - | (l1,l2) -> (List.rev l1, List.rev l2, acc) + | (x1 :: l1, x2 :: l2) when x1 == x2 -> shr_rev (x1 :: acc) (l1,l2) + | (l1, l2) -> (List.rev l1, List.rev l2, acc) in shr_rev [] (List.rev l1, List.rev l2) -(* Poor man's monadic map *) -let rec fold_left_map f e = function - | [] -> (e,[]) - | h::t -> - let e',h' = f e h in - let e'',t' = fold_left_map f e' t in - e'',h'::t' +(** {6 Association lists} *) -let fold_map = fold_left_map +let map_assoc f = List.map (fun (x,a) -> (x,f a)) -(* (* tail-recursive version of the above function *) -let fold_map f e l = - let g (e,b') h = - let (e',h') = f e h in - (e',h'::b') +let rec assoc_f f a = function + | (x, e) :: xs -> if f a x then e else assoc_f f a xs + | [] -> raise Not_found + +let remove_assoc_f f a l = + try remove_first (fun (x,_) -> f a x) l with Not_found -> l + +let mem_assoc_f f a l = List.exists (fun (x,_) -> f a x) l + +(** {6 Operations on lists of tuples} *) + +let rec split_loop p q = function + | [] -> () + | (x, y) :: l -> + let cl = { head = x; tail = [] } in + let cr = { head = y; tail = [] } in + p.tail <- cast cl; + q.tail <- cast cr; + split_loop cl cr l + +let split = function + | [] -> [], [] + | (x, y) :: l -> + let cl = { head = x; tail = [] } in + let cr = { head = y; tail = [] } in + split_loop cl cr l; + (cast cl, cast cr) + +let rec combine_loop p l1 l2 = match l1, l2 with + | [], [] -> () + | x :: l1, y :: l2 -> + let c = { head = (x, y); tail = [] } in + p.tail <- cast c; + combine_loop c l1 l2 + | _ -> invalid_arg "List.combine" + +let combine l1 l2 = match l1, l2 with + | [], [] -> [] + | x :: l1, y :: l2 -> + let c = { head = (x, y); tail = [] } in + combine_loop c l1 l2; + cast c + | _ -> invalid_arg "List.combine" + +let rec split3_loop p q r = function + | [] -> () + | (x, y, z) :: l -> + let cp = { head = x; tail = [] } in + let cq = { head = y; tail = [] } in + let cr = { head = z; tail = [] } in + p.tail <- cast cp; + q.tail <- cast cq; + r.tail <- cast cr; + split3_loop cp cq cr l + +let split3 = function + | [] -> [], [], [] + | (x, y, z) :: l -> + let cp = { head = x; tail = [] } in + let cq = { head = y; tail = [] } in + let cr = { head = z; tail = [] } in + split3_loop cp cq cr l; + (cast cp, cast cq, cast cr) + +let rec combine3_loop p l1 l2 l3 = match l1, l2, l3 with + | [], [], [] -> () + | x :: l1, y :: l2, z :: l3 -> + let c = { head = (x, y, z); tail = [] } in + p.tail <- cast c; + combine3_loop c l1 l2 l3 + | _ -> invalid_arg "List.combine3" + +let combine3 l1 l2 l3 = match l1, l2, l3 with + | [], [], [] -> [] + | x :: l1, y :: l2, z :: l3 -> + let c = { head = (x, y, z); tail = [] } in + combine3_loop c l1 l2 l3; + cast c + | _ -> invalid_arg "List.combine3" + +(** {6 Operations on lists seen as sets, preserving uniqueness of elements} *) + +(** Add an element, preserving uniqueness of elements *) + +let add_set cmp x l = + if mem_f cmp x l then l else x :: l + +(** List equality up to permutation (but considering multiple occurrences) *) + +let eq_set cmp l1 l2 = + let rec aux l1 = function + | [] -> is_empty l1 + | a :: l2 -> aux (remove_first (cmp a) l1) l2 in - let (e',lrev) = List.fold_left g (e,[]) l in - (e',List.rev lrev) -*) + try aux l1 l2 with Not_found -> false -(* The same, based on fold_right, with the effect accumulated on the right *) -let fold_right_map f l e = - List.fold_right (fun x (l,e) -> let (y,e) = f x e in (y::l,e)) l ([],e) +let rec merge_set cmp l1 l2 = match l1, l2 with + | [], l2 -> l2 + | l1, [] -> l1 + | h1 :: t1, h2 :: t2 -> + let c = cmp h1 h2 in + if Int.equal c 0 + then h1 :: merge_set cmp t1 t2 + else if c <= 0 + then h1 :: merge_set cmp t1 l2 + else h2 :: merge_set cmp l1 t2 -let fold_map' = fold_right_map +let merge_uniq = merge_set -let on_snd f (x,y) = (x,f y) +let intersect cmp l1 l2 = + filter (fun x -> mem_f cmp x l2) l1 -let fold_left2_map f e l l' = - on_snd List.rev @@ - List.fold_left2 (fun (e,l) x x' -> - let (e,y) = f e x x' in - (e, y::l) - ) (e, []) l l' +let union cmp l1 l2 = + let rec urec = function + | [] -> l2 + | a :: l -> if mem_f cmp a l2 then urec l else a :: urec l + in + urec l1 -let fold_right2_map f l l' e = - List.fold_right2 (fun x x' (l,e) -> let (y,e) = f x x' e in (y::l,e)) l l' ([],e) +let subtract cmp l1 l2 = + if is_empty l2 then l1 + else List.filter (fun x -> not (mem_f cmp x l2)) l1 -let fold_left3_map f e l l' l'' = - on_snd List.rev @@ - fold_left3 (fun (e,l) x x' x'' -> let (e,y) = f e x x' x'' in (e,y::l)) (e,[]) l l' l'' +let unionq l1 l2 = union (==) l1 l2 +let subtractq l1 l2 = subtract (==) l1 l2 -let fold_left4_map f e l1 l2 l3 l4 = - on_snd List.rev @@ - fold_left4 (fun (e,l) x1 x2 x3 x4 -> let (e,y) = f e x1 x2 x3 x4 in (e,y::l)) (e,[]) l1 l2 l3 l4 +(** {6 Uniqueness and duplication} *) -let map_assoc f = List.map (fun (x,a) -> (x,f a)) +(* FIXME: we should avoid relying on the generic hash function, + just as we'd better avoid Pervasives.compare *) -let rec assoc_f f a = function - | (x, e) :: xs -> if f a x then e else assoc_f f a xs - | [] -> raise Not_found +let distinct l = + let visited = Hashtbl.create 23 in + let rec loop = function + | h :: t -> + if Hashtbl.mem visited h then false + else + begin + Hashtbl.add visited h h; + loop t + end + | [] -> true + in + loop l -let remove_assoc_f f a l = - try remove_first (fun (x,_) -> f a x) l with Not_found -> l +let distinct_f cmp l = + let rec loop = function + | a :: b :: _ when Int.equal (cmp a b) 0 -> false + | a :: l -> loop l + | [] -> true + in loop (List.sort cmp l) -let mem_assoc_f f a l = List.exists (fun (x,_) -> f a x) l +(* FIXME: again, generic hash function *) + +let uniquize l = + let visited = Hashtbl.create 23 in + let rec aux acc changed = function + | h :: t -> if Hashtbl.mem visited h then aux acc true t else + begin + Hashtbl.add visited h h; + aux (h :: acc) changed t + end + | [] -> if changed then List.rev acc else l + in + aux [] false l + +(** [sort_uniquize] might be an alternative to the hashtbl-based + [uniquize], when the order of the elements is irrelevant *) + +let rec uniquize_sorted cmp = function + | a :: b :: l when Int.equal (cmp a b) 0 -> uniquize_sorted cmp (a :: l) + | a :: l -> a :: uniquize_sorted cmp l + | [] -> [] + +let sort_uniquize cmp l = + uniquize_sorted cmp (List.sort cmp l) + +let rec duplicates cmp = function + | [] -> [] + | x :: l -> + let l' = duplicates cmp l in + if mem_f cmp x l then add_set cmp x l' else l' + +(** {6 Cartesian product} *) (* A generic cartesian product: for any operator (**), [cartesian (**) [x1;x2] [y1;y2] = [x1**y1; x1**y2; x2**y1; x2**y1]], @@ -855,15 +993,9 @@ let cartesians op init ll = (* combinations [[a;b];[c;d]] gives [[a;c];[a;d];[b;c];[b;d]] *) -let combinations l = cartesians (fun x l -> x::l) [] l +let combinations l = + cartesians (fun x l -> x :: l) [] l -let rec combine3 x y z = - match x, y, z with - | [], [], [] -> [] - | (x :: xs), (y :: ys), (z :: zs) -> - (x, y, z) :: combine3 xs ys zs - | _, _, _ -> invalid_arg "List.combine3" - (* Keep only those products that do not return None *) let cartesian_filter op l1 l2 = @@ -874,43 +1006,34 @@ let cartesian_filter op l1 l2 = let cartesians_filter op init ll = List.fold_right (cartesian_filter op) ll [init] -(* Drop the last element of a list *) - -let rec drop_last = function - | [] -> assert false - | hd :: [] -> [] - | hd :: tl -> hd :: drop_last tl - (* Factorize lists of pairs according to the left argument *) let rec factorize_left cmp = function - | (a,b)::l -> + | (a,b) :: l -> let al,l' = partition (fun (a',_) -> cmp a a') l in - (a,(b::List.map snd al)) :: factorize_left cmp l' + (a,(b :: List.map snd al)) :: factorize_left cmp l' | [] -> [] module Smart = struct - let rec map f l = match l with - [] -> l - | h::tl -> - let h' = f h and tl' = map f tl in - if h'==h && tl'==tl then l - else h'::tl' - - let rec filter f l = match l with - [] -> l - | h::tl -> - let tl' = filter f tl in - if f h then - if tl' == tl then l - else h :: tl' - else tl' + let rec map_loop f p = function + | [] -> () + | x :: l' as l -> + let x' = f x in + map_loop f p l'; + if x' == x && !p == l' then p := l else p := x' :: !p + + let map f = function + | [] -> [] + | x :: l' as l -> + let p = ref [] in + let x' = f x in + map_loop f p l'; + if x' == x && !p == l' then l else x' :: !p end let smartmap = Smart.map -let smartfilter = Smart.filter module type MonoS = sig type elt diff --git a/clib/cList.mli b/clib/cList.mli index b3c151098..d080ebca2 100644 --- a/clib/cList.mli +++ b/clib/cList.mli @@ -18,33 +18,31 @@ module type ExtS = sig include S + (** {6 Equality, testing} *) + val compare : 'a cmp -> 'a list cmp (** Lexicographic order on lists. *) val equal : 'a eq -> 'a list eq - (** Lifts equality to list type. *) + (** Lift equality to list type. *) val is_empty : 'a list -> bool - (** Checks whether a list is empty *) - - val init : int -> (int -> 'a) -> 'a list - (** [init n f] constructs the list [f 0; ... ; f (n - 1)]. *) + (** Check whether a list is empty *) val mem_f : 'a eq -> 'a -> 'a list -> bool - (* Same as [List.mem], for some specific equality *) + (** Same as [List.mem], for some specific equality *) - val add_set : 'a eq -> 'a -> 'a list -> 'a list - (** [add_set x l] adds [x] in [l] if it is not already there, or returns [l] - otherwise. *) + val for_all_i : (int -> 'a -> bool) -> int -> 'a list -> bool + (** Same as [List.for_all] but with an index *) - val eq_set : 'a eq -> 'a list eq - (** Test equality up to permutation (but considering multiple occurrences) *) + val for_all2eq : ('a -> 'b -> bool) -> 'a list -> 'b list -> bool + (** Same as [List.for_all2] but returning [false] when of different length *) - val intersect : 'a eq -> 'a list -> 'a list -> 'a list - val union : 'a eq -> 'a list -> 'a list -> 'a list - val unionq : 'a list -> 'a list -> 'a list - val subtract : 'a eq -> 'a list -> 'a list -> 'a list - val subtractq : 'a list -> 'a list -> 'a list + val prefix_of : 'a eq -> 'a list eq + (** [prefix_of eq l1 l2] returns [true] if [l1] is a prefix of [l2], [false] + otherwise. It uses [eq] to compare elements *) + + (** {6 Creating lists} *) val interval : int -> int -> int list (** [interval i j] creates the list [[i; i + 1; ...; j]], or [[]] when @@ -52,27 +50,66 @@ sig val make : int -> 'a -> 'a list (** [make n x] returns a list made of [n] times [x]. Raise - [Invalid_argument "List.make"] if [n] is negative. *) + [Invalid_argument _] if [n] is negative. *) - val assign : 'a list -> int -> 'a -> 'a list - (** [assign l i x] sets the [i]-th element of [l] to [x], starting from [0]. *) + val addn : int -> 'a -> 'a list -> 'a list + (** [addn n x l] adds [n] times [x] on the left of [l]. *) - val distinct : 'a list -> bool - (** Return [true] if all elements of the list are distinct. *) + val init : int -> (int -> 'a) -> 'a list + (** [init n f] constructs the list [f 0; ... ; f (n - 1)]. Raise + [Invalid_argument _] if [n] is negative *) - val distinct_f : 'a cmp -> 'a list -> bool + val append : 'a list -> 'a list -> 'a list + (** Like OCaml's [List.append] but tail-recursive. *) - val duplicates : 'a eq -> 'a list -> 'a list - (** Return the list of unique elements which appear at least twice. Elements - are kept in the order of their first appearance. *) + val concat : 'a list list -> 'a list + (** Like OCaml's [List.concat] but tail-recursive. *) + + val flatten : 'a list list -> 'a list + (** Synonymous of [concat] *) + + (** {6 Lists as arrays} *) + + val assign : 'a list -> int -> 'a -> 'a list + (** [assign l i x] sets the [i]-th element of [l] to [x], starting + from [0]. Raise [Failure _] if [i] is out of range. *) + + (** {6 Filtering} *) + + val filter : ('a -> bool) -> 'a list -> 'a list + (** Like OCaml [List.filter] but tail-recursive and physically returns + the original list if the predicate holds for all elements. *) val filter2 : ('a -> 'b -> bool) -> 'a list -> 'b list -> 'a list * 'b list + (** Like [List.filter] but with 2 arguments, raise [Invalid_argument _] + if the lists are not of same length. *) + + val filteri : (int -> 'a -> bool) -> 'a list -> 'a list + (** Like [List.filter] but with an index starting from [0] *) + + val filter_with : bool list -> 'a list -> 'a list + (** [filter_with bl l] selects elements of [l] whose corresponding element in + [bl] is [true]. Raise [Invalid_argument _] if sizes differ. *) + + val smartfilter : ('a -> bool) -> 'a list -> 'a list + [@@ocaml.deprecated "Same as [filter]"] + val map_filter : ('a -> 'b option) -> 'a list -> 'b list + (** Like [map] but keeping only non-[None] elements *) + val map_filter_i : (int -> 'a -> 'b option) -> 'a list -> 'b list + (** Like [map_filter] but with an index starting from [0] *) - val filter_with : bool list -> 'a list -> 'a list - (** [filter_with b a] selects elements of [a] whose corresponding element in - [b] is [true]. Raise [Invalid_argument _] when sizes differ. *) + val partitioni : (int -> 'a -> bool) -> 'a list -> 'a list * 'a list + (** Like [List.partition] but with an index starting from [0] *) + + (** {6 Applying functorially} *) + + val map : ('a -> 'b) -> 'a list -> 'b list + (** Like OCaml [List.map] but tail-recursive *) + + val map2 : ('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list + (** Like OCaml [List.map2] but tail-recursive *) val smartmap : ('a -> 'a) -> 'a list -> 'a list [@@ocaml.deprecated "Same as [Smart.map]"] @@ -81,27 +118,39 @@ sig (** As [map] but ensures the left-to-right order of evaluation. *) val map_i : (int -> 'a -> 'b) -> int -> 'a list -> 'b list - (** As [map] but with the index, which starts from [0]. *) + (** Like OCaml [List.mapi] but tail-recursive. Alternatively, like + [map] but with an index *) val map2_i : (int -> 'a -> 'b -> 'c) -> int -> 'a list -> 'b list -> 'c list + (** Like [map2] but with an index *) + val map3 : ('a -> 'b -> 'c -> 'd) -> 'a list -> 'b list -> 'c list -> 'd list + (** Like [map] but for 3 lists. *) + val map4 : ('a -> 'b -> 'c -> 'd -> 'e) -> 'a list -> 'b list -> 'c list -> 'd list -> 'e list - val filteri : (int -> 'a -> bool) -> 'a list -> 'a list - val partitioni : (int -> 'a -> bool) -> 'a list -> 'a list * 'a list + (** Like [map] but for 4 lists. *) val map_of_array : ('a -> 'b) -> 'a array -> 'b list (** [map_of_array f a] behaves as [List.map f (Array.to_list a)] *) - val smartfilter : ('a -> bool) -> 'a list -> 'a list - [@@ocaml.deprecated "Same as [Smart.filter]"] + val map_append : ('a -> 'b list) -> 'a list -> 'b list + (** [map_append f [x1; ...; xn]] returns [f x1 @ ... @ f xn]. *) + + val map_append2 : ('a -> 'b -> 'c list) -> 'a list -> 'b list -> 'c list + (** Like [map_append] but for two lists; raises [Invalid_argument _] + if the two lists do not have the same length. *) val extend : bool list -> 'a -> 'a list -> 'a list -(** [extend l a [a1..an]] assumes that the number of [true] in [l] is [n]; + (** [extend l a [a1..an]] assumes that the number of [true] in [l] is [n]; it extends [a1..an] by inserting [a] at the position of [false] in [l] *) + val count : ('a -> bool) -> 'a list -> int + (** Count the number of elements satisfying a predicate *) + + (** {6 Finding position} *) val index : 'a eq -> 'a -> 'a list -> int (** [index] returns the 1st index of an element in a list (counting from 1). *) @@ -109,29 +158,65 @@ sig val index0 : 'a eq -> 'a -> 'a list -> int (** [index0] behaves as [index] except that it starts counting at 0. *) - val iteri : (int -> 'a -> unit) -> 'a list -> unit - (** As [iter] but with the index argument (starting from 0). *) + (** {6 Folding} *) val fold_left_until : ('c -> 'a -> 'c CSig.until) -> 'c -> 'a list -> 'c (** acts like [fold_left f acc s] while [f] returns [Cont acc']; it stops returning [c] as soon as [f] returns [Stop c]. *) val fold_right_i : (int -> 'a -> 'b -> 'b) -> int -> 'a list -> 'b -> 'b + (** Like [List.fold_right] but with an index *) + val fold_left_i : (int -> 'a -> 'b -> 'a) -> int -> 'a -> 'b list -> 'a - val fold_right_and_left : - ('a -> 'b -> 'b list -> 'a) -> 'b list -> 'a -> 'a + (** Like [List.fold_left] but with an index *) + + val fold_right_and_left : ('b -> 'a -> 'a list -> 'b) -> 'a list -> 'b -> 'b + (** [fold_right_and_left f [a1;...;an] hd] is + [f (f (... (f (f hd an [an-1;...;a1]) an-1 [an-2;...;a1]) ...) a2 [a1]) a1 []] *) + val fold_left3 : ('a -> 'b -> 'c -> 'd -> 'a) -> 'a -> 'b list -> 'c list -> 'd list -> 'a + (** Like [List.fold_left] but for 3 lists; raise [Invalid_argument _] if + not all lists of the same size *) + val fold_left2_set : exn -> ('a -> 'b -> 'c -> 'b list -> 'c list -> 'a) -> 'a -> 'b list -> 'c list -> 'a (** Fold sets, i.e. lists up to order; the folding function tells when elements match by returning a value and raising the given exception otherwise; sets should have the same size; raise the given exception if no pairing of the two sets is found;; complexity in O(n^2) *) - val fold_left2_set : exn -> ('a -> 'b -> 'c -> 'b list -> 'c list -> 'a) -> 'a -> 'b list -> 'c list -> 'a - val for_all_i : (int -> 'a -> bool) -> int -> 'a list -> bool + val fold_left_map : ('a -> 'b -> 'a * 'c) -> 'a -> 'b list -> 'a * 'c list + (** [fold_left_map f e_0 [a1;...;an]] is [e_n,[k_1...k_n]] + where [(e_i,k_i)] is [f e_{i-1} ai] for each i<=n *) + + val fold_right_map : ('b -> 'a -> 'c * 'a) -> 'b list -> 'a -> 'c list * 'a + (** Same, folding on the right *) + + val fold_left2_map : ('a -> 'b -> 'c -> 'a * 'd) -> 'a -> 'b list -> 'c list -> 'a * 'd list + (** Same with two lists, folding on the left *) + + val fold_right2_map : ('b -> 'c -> 'a -> 'd * 'a) -> 'b list -> 'c list -> 'a -> 'd list * 'a + (** Same with two lists, folding on the right *) + + val fold_left3_map : ('a -> 'b -> 'c -> 'd -> 'a * 'e) -> 'a -> 'b list -> 'c list -> 'd list -> 'a * 'e list + (** Same with three lists, folding on the left *) + + val fold_left4_map : ('a -> 'b -> 'c -> 'd -> 'e -> 'a * 'r) -> 'a -> 'b list -> 'c list -> 'd list -> 'e list -> 'a * 'r list + (** Same with four lists, folding on the left *) + + val fold_map : ('a -> 'b -> 'a * 'c) -> 'a -> 'b list -> 'a * 'c list + [@@ocaml.deprecated "Same as [fold_left_map]"] + + val fold_map' : ('b -> 'a -> 'c * 'a) -> 'b list -> 'a -> 'c list * 'a + [@@ocaml.deprecated "Same as [fold_right_map]"] + + (** {6 Splitting} *) + val except : 'a eq -> 'a -> 'a list -> 'a list + (** [except eq a l] Remove all occurrences of [a] in [l] *) + val remove : 'a eq -> 'a -> 'a list -> 'a list + (** Alias of [except] *) val remove_first : ('a -> bool) -> 'a list -> 'a list (** Remove the first element satisfying a predicate, or raise [Not_found] *) @@ -140,35 +225,10 @@ sig (** Remove and return the first element satisfying a predicate, or raise [Not_found] *) - val insert : ('a -> 'a -> bool) -> 'a -> 'a list -> 'a list - (** Insert at the (first) position so that if the list is ordered wrt to the - total order given as argument, the order is preserved *) - - val for_all2eq : ('a -> 'b -> bool) -> 'a list -> 'b list -> bool - val sep_last : 'a list -> 'a * 'a list - val find_map : ('a -> 'b option) -> 'a list -> 'b (** Returns the first element that is mapped to [Some _]. Raise [Not_found] if there is none. *) - val uniquize : 'a list -> 'a list - (** Return the list of elements without duplicates. - This is the list unchanged if there was none. *) - - val sort_uniquize : 'a cmp -> 'a list -> 'a list - (** Return a sorted and de-duplicated version of a list, - according to some comparison function. *) - - val merge_uniq : 'a cmp -> 'a list -> 'a list -> 'a list - (** Merge two sorted lists and preserves the uniqueness property. *) - - val subset : 'a list -> 'a list -> bool - - val chop : int -> 'a list -> 'a list * 'a list - (** [chop i l] splits [l] into two lists [(l1,l2)] such that - [l1++l2=l] and [l1] has length [i]. It raises [Failure] when [i] - is negative or greater than the length of [l] *) - exception IndexOutOfRange val goto: int -> 'a list -> 'a list * 'a list (** [goto i l] splits [l] into two lists [(l1,l2)] such that @@ -176,95 +236,174 @@ sig [IndexOutOfRange] when [i] is negative or greater than the length of [l]. *) - val split_when : ('a -> bool) -> 'a list -> 'a list * 'a list - val split3 : ('a * 'b * 'c) list -> 'a list * 'b list * 'c list - val firstn : int -> 'a list -> 'a list + (** [split_when p l] splits [l] into two lists [(l1,a::l2)] such that + [l1++(a::l2)=l], [p a=true] and [p b = false] for every element [b] of [l1]. + if there is no such [a], then it returns [(l,[])] instead. *) + + val sep_last : 'a list -> 'a * 'a list + (** [sep_last l] returns [(a,l')] such that [l] is [l'@[a]]. + It raises [Failure _] if the list is empty. *) + + val drop_last : 'a list -> 'a list + (** Remove the last element of the list. It raises [Failure _] if the + list is empty. This is the second part of [sep_last]. *) + val last : 'a list -> 'a + (** Return the last element of the list. It raises [Failure _] if the + list is empty. This is the first part of [sep_last]. *) + val lastn : int -> 'a list -> 'a list + (** [lastn n l] returns the [n] last elements of [l]. It raises + [Failure _] if [n] is less than 0 or larger than the length of [l] *) + + val chop : int -> 'a list -> 'a list * 'a list + (** [chop i l] splits [l] into two lists [(l1,l2)] such that + [l1++l2=l] and [l1] has length [i]. It raises [Failure _] when + [i] is negative or greater than the length of [l]. *) + + val firstn : int -> 'a list -> 'a list + (** [firstn n l] Returns the [n] first elements of [l]. It raises + [Failure _] if [n] negative or too large. This is the first part + of [chop]. *) + val skipn : int -> 'a list -> 'a list + (** [skipn n l] drops the [n] first elements of [l]. It raises + [Failure _] if [n] is less than 0 or larger than the length of [l]. + This is the second part of [chop]. *) + val skipn_at_least : int -> 'a list -> 'a list + (** Same as [skipn] but returns [] if [n] is larger than the list of + the list. *) - val addn : int -> 'a -> 'a list -> 'a list - (** [addn n x l] adds [n] times [x] on the left of [l]. *) + val drop_prefix : 'a eq -> 'a list -> 'a list -> 'a list + (** [drop_prefix eq l1 l] returns [l2] if [l=l1++l2] else return [l]. *) + + val insert : 'a eq -> 'a -> 'a list -> 'a list + (** Insert at the (first) position so that if the list is ordered wrt to the + total order given as argument, the order is preserved *) + + val share_tails : 'a list -> 'a list -> 'a list * 'a list * 'a list + (** [share_tails l1 l2] returns [(l1',l2',l)] such that [l1] is + [l1'@l] and [l2] is [l2'@l] and [l] is maximal amongst all such + decompositions*) + + (** {6 Association lists} *) + + val map_assoc : ('a -> 'b) -> ('c * 'a) list -> ('c * 'b) list + (** Applies a function on the codomain of an association list *) + + val assoc_f : 'a eq -> 'a -> ('a * 'b) list -> 'b + (** Like [List.assoc] but using the equality given as argument *) + + val remove_assoc_f : 'a eq -> 'a -> ('a * 'b) list -> ('a * 'b) list + (** Remove first matching element; unchanged if no such element *) + + val mem_assoc_f : 'a eq -> 'a -> ('a * 'b) list -> bool + (** Like [List.mem_assoc] but using the equality given as argument *) - val prefix_of : 'a eq -> 'a list -> 'a list -> bool - (** [prefix_of l1 l2] returns [true] if [l1] is a prefix of [l2], [false] + val factorize_left : 'a eq -> ('a * 'b) list -> ('a * 'b list) list + (** Create a list of associations from a list of pairs *) + + (** {6 Operations on lists of tuples} *) + + val split : ('a * 'b) list -> 'a list * 'b list + (** Like OCaml's [List.split] but tail-recursive. *) + + val combine : 'a list -> 'b list -> ('a * 'b) list + (** Like OCaml's [List.combine] but tail-recursive. *) + + val split3 : ('a * 'b * 'c) list -> 'a list * 'b list * 'c list + (** Like [split] but for triples *) + + val combine3 : 'a list -> 'b list -> 'c list -> ('a * 'b * 'c) list + (** Like [combine] but for triples *) + + (** {6 Operations on lists seen as sets, preserving uniqueness of elements} *) + + val add_set : 'a eq -> 'a -> 'a list -> 'a list + (** [add_set x l] adds [x] in [l] if it is not already there, or returns [l] otherwise. *) - val drop_prefix : 'a eq -> 'a list -> 'a list -> 'a list - (** [drop_prefix p l] returns [t] if [l=p++t] else return [l]. *) + val eq_set : 'a eq -> 'a list eq + (** Test equality up to permutation. It respects multiple occurrences + and thus works also on multisets. *) - val drop_last : 'a list -> 'a list + val subset : 'a list eq + (** Tell if a list is a subset of another up to permutation. It expects + each element to occur only once. *) - val map_append : ('a -> 'b list) -> 'a list -> 'b list - (** [map_append f [x1; ...; xn]] returns [(f x1)@(f x2)@...@(f xn)]. *) + val merge_set : 'a cmp -> 'a list -> 'a list -> 'a list + (** Merge two sorted lists and preserves the uniqueness property. *) - val map_append2 : ('a -> 'b -> 'c list) -> 'a list -> 'b list -> 'c list - (** As [map_append]. Raises [Invalid_argument _] if the two lists don't have - the same length. *) + val intersect : 'a eq -> 'a list -> 'a list -> 'a list + (** Return the intersection of two lists, assuming and preserving + uniqueness of elements *) - val share_tails : 'a list -> 'a list -> 'a list * 'a list * 'a list + val union : 'a eq -> 'a list -> 'a list -> 'a list + (** Return the union of two lists, assuming and preserving + uniqueness of elements *) - val fold_left_map : ('a -> 'b -> 'a * 'c) -> 'a -> 'b list -> 'a * 'c list - (** [fold_left_map f e_0 [l_1...l_n] = e_n,[k_1...k_n]] - where [(e_i,k_i)=f e_{i-1} l_i] *) + val unionq : 'a list -> 'a list -> 'a list + (** [union] specialized to physical equality *) - val fold_right_map : ('b -> 'a -> 'c * 'a) -> 'b list -> 'a -> 'c list * 'a - (** Same, folding on the right *) + val subtract : 'a eq -> 'a list -> 'a list -> 'a list + (** Remove from the first list all elements from the second list. *) - val fold_left2_map : ('a -> 'b -> 'c -> 'a * 'd) -> 'a -> 'b list -> 'c list -> 'a * 'd list - (** Same with two lists, folding on the left *) + val subtractq : 'a list -> 'a list -> 'a list + (** [subtract] specialized to physical equality *) - val fold_right2_map : ('b -> 'c -> 'a -> 'd * 'a) -> 'b list -> 'c list -> 'a -> 'd list * 'a - (** Same with two lists, folding on the right *) + val merge_uniq : 'a cmp -> 'a list -> 'a list -> 'a list + (** [@@ocaml.deprecated "Same as [merge_set]"] *) - val fold_left3_map : ('a -> 'b -> 'c -> 'd -> 'a * 'e) -> 'a -> 'b list -> 'c list -> 'd list -> 'a * 'e list - (** Same with three lists, folding on the left *) + (** {6 Uniqueness and duplication} *) - val fold_left4_map : ('a -> 'b -> 'c -> 'd -> 'e -> 'a * 'r) -> 'a -> 'b list -> 'c list -> 'd list -> 'e list -> 'a * 'r list - (** Same with four lists, folding on the left *) + val distinct : 'a list -> bool + (** Return [true] if all elements of the list are distinct. *) - val fold_map : ('a -> 'b -> 'a * 'c) -> 'a -> 'b list -> 'a * 'c list - [@@ocaml.deprecated "Same as [fold_left_map]"] + val distinct_f : 'a cmp -> 'a list -> bool + (** Like [distinct] but using the equality given as argument *) - val fold_map' : ('b -> 'a -> 'c * 'a) -> 'b list -> 'a -> 'c list * 'a - [@@ocaml.deprecated "Same as [fold_right_map]"] + val duplicates : 'a eq -> 'a list -> 'a list + (** Return the list of unique elements which appear at least twice. Elements + are kept in the order of their first appearance. *) - val map_assoc : ('a -> 'b) -> ('c * 'a) list -> ('c * 'b) list - val assoc_f : 'a eq -> 'a -> ('a * 'b) list -> 'b - val remove_assoc_f : 'a eq -> 'a -> ('a * 'b) list -> ('a * 'b) list - val mem_assoc_f : 'a eq -> 'a -> ('a * 'b) list -> bool + val uniquize : 'a list -> 'a list + (** Return the list of elements without duplicates. + This is the list unchanged if there was none. *) + + val sort_uniquize : 'a cmp -> 'a list -> 'a list + (** Return a sorted version of a list without duplicates + according to some comparison function. *) + + (** {6 Cartesian product} *) val cartesian : ('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list - (** A generic cartesian product: for any operator (**), + (** A generic binary cartesian product: for any operator (**), [cartesian (**) [x1;x2] [y1;y2] = [x1**y1; x1**y2; x2**y1; x2**y1]], and so on if there are more elements in the lists. *) val cartesians : ('a -> 'b -> 'b) -> 'b -> 'a list list -> 'b list - (** [cartesians] is an n-ary cartesian product: it iterates - [cartesian] over a list of lists. *) + (** [cartesians op init l] is an n-ary cartesian product: it builds + the list of all [op a1 .. (op an init) ..] for [a1], ..., [an] in + the product of the elements of the lists *) val combinations : 'a list list -> 'a list list - (** combinations [[a;b];[c;d]] returns [[a;c];[a;d];[b;c];[b;d]] *) - - val combine3 : 'a list -> 'b list -> 'c list -> ('a * 'b * 'c) list + (** [combinations l] returns the list of [n_1] * ... * [n_p] tuples + [[a11;...;ap1];...;[a1n_1;...;apn_pd]] whenever [l] is a list + [[a11;..;a1n_1];...;[ap1;apn_p]]; otherwise said, it is + [cartesians (::) [] l] *) val cartesians_filter : ('a -> 'b -> 'b option) -> 'b -> 'a list list -> 'b list - (** Keep only those products that do not return None *) - - val factorize_left : 'a eq -> ('a * 'b) list -> ('a * 'b list) list + (** Like [cartesians op init l] but keep only the tuples for which + [op] returns [Some _] on all the elements of the tuple. *) module Smart : sig val map : ('a -> 'a) -> 'a list -> 'a list (** [Smart.map f [a1...an] = List.map f [a1...an]] but if for all i [f ai == ai], then [Smart.map f l == l] *) - - val filter : ('a -> bool) -> 'a list -> 'a list - (** [Smart.filter f [a1...an] = List.filter f [a1...an]] but if for all i - [f ai = true], then [Smart.filter f l == l] *) end module type MonoS = sig diff --git a/clib/cMap.ml b/clib/cMap.ml index f6e52594b..54a8b2585 100644 --- a/clib/cMap.ml +++ b/clib/cMap.ml @@ -35,9 +35,9 @@ sig val fold_left : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b val fold_right : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b val smartmap : ('a -> 'a) -> 'a t -> 'a t - (** [@@ocaml.deprecated "Same as [Smart.map]"] *) + [@@ocaml.deprecated "Same as [Smart.map]"] val smartmapi : (key -> 'a -> 'a) -> 'a t -> 'a t - (** [@@ocaml.deprecated "Same as [Smart.mapi]"] *) + [@@ocaml.deprecated "Same as [Smart.mapi]"] val height : 'a t -> int module Smart : sig @@ -66,9 +66,9 @@ sig val fold_left : (M.t -> 'a -> 'b -> 'b) -> 'a map -> 'b -> 'b val fold_right : (M.t -> 'a -> 'b -> 'b) -> 'a map -> 'b -> 'b val smartmap : ('a -> 'a) -> 'a map -> 'a map - (** [@@ocaml.deprecated "Same as [Smart.map]"] *) + [@@ocaml.deprecated "Same as [Smart.map]"] val smartmapi : (M.t -> 'a -> 'a) -> 'a map -> 'a map - (** [@@ocaml.deprecated "Same as [Smart.mapi]"] *) + [@@ocaml.deprecated "Same as [Smart.mapi]"] val height : 'a map -> int module Smart : sig diff --git a/clib/cMap.mli b/clib/cMap.mli index b45effb95..127bf23ab 100644 --- a/clib/cMap.mli +++ b/clib/cMap.mli @@ -58,10 +58,10 @@ sig (** Folding keys in decreasing order. *) val smartmap : ('a -> 'a) -> 'a t -> 'a t - (** [@@ocaml.deprecated "Same as [Smart.map]"] *) + [@@ocaml.deprecated "Same as [Smart.map]"] val smartmapi : (key -> 'a -> 'a) -> 'a t -> 'a t - (** [@@ocaml.deprecated "Same as [Smart.mapi]"] *) + [@@ocaml.deprecated "Same as [Smart.mapi]"] val height : 'a t -> int (** An indication of the logarithmic size of a map *) diff --git a/configure.ml b/configure.ml index 45c3bb67a..933143e68 100644 --- a/configure.ml +++ b/configure.ml @@ -33,7 +33,7 @@ let cprintf s = cfprintf stdout s let ceprintf s = cfprintf stderr s let die msg = ceprintf "%s%s%s\nConfiguration script failed!" red msg reset; exit 1 -let warn s = cprintf ("%sWarning: " ^^ s ^^ "%s") yellow reset +let warn s = kfprintf (fun oc -> cfprintf oc "%s" reset) stdout ("%sWarning: " ^^ s) yellow let s2i = int_of_string let i2s = string_of_int diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh index ecc45735f..508dcf5fb 100644 --- a/dev/build/windows/makecoq_mingw.sh +++ b/dev/build/windows/makecoq_mingw.sh @@ -480,19 +480,19 @@ function make_sed { ##### LIBPNG ##### function make_libpng { - build_conf_make_inst http://prdownloads.sourceforge.net/libpng libpng-1.6.18 tar.gz true + build_conf_make_inst http://prdownloads.sourceforge.net/libpng libpng-1.6.34 tar.gz true } ##### PIXMAN ##### function make_pixman { - build_conf_make_inst http://cairographics.org/releases pixman-0.32.8 tar.gz true + build_conf_make_inst http://cairographics.org/releases pixman-0.34.0 tar.gz true } ##### FREETYPE ##### function make_freetype { - build_conf_make_inst http://sourceforge.net/projects/freetype/files/freetype2/2.6.1 freetype-2.6.1 tar.bz2 true + build_conf_make_inst http://sourceforge.net/projects/freetype/files/freetype2/2.9.1 freetype-2.9.1 tar.bz2 true } ##### EXPAT ##### @@ -508,7 +508,7 @@ function make_fontconfig { make_expat # CONFIGURE PARAMETERS # build/install fails without --disable-docs - build_conf_make_inst http://www.freedesktop.org/software/fontconfig/release fontconfig-2.11.94 tar.gz true --disable-docs + build_conf_make_inst http://www.freedesktop.org/software/fontconfig/release fontconfig-2.12.93 tar.gz true --disable-docs } ##### ICONV ##### @@ -588,8 +588,7 @@ function make_glib { make_gettext make_libffi make_libpcre - # build_conf_make_inst http://ftp.gnome.org/pub/gnome/sources/glib/2.46 glib-2.46.0 tar.xz true - build_conf_make_inst http://ftp.gnome.org/pub/gnome/sources/glib/2.47 glib-2.47.5 tar.xz true + build_conf_make_inst http://ftp.gnome.org/pub/gnome/sources/glib/2.57 glib-2.57.1 tar.xz true } ##### ATK ##### @@ -597,7 +596,7 @@ function make_glib { function make_atk { make_gettext make_glib - build_conf_make_inst http://ftp.gnome.org/pub/gnome/sources/atk/2.18 atk-2.18.0 tar.xz true + build_conf_make_inst http://ftp.gnome.org/pub/gnome/sources/atk/2.29 atk-2.29.1 tar.xz true } ##### PIXBUF ##### @@ -610,7 +609,7 @@ function make_gdk-pixbuf { # CONFIGURE PARAMETERS # --with-included-loaders=yes statically links the image file format handlers # This avoids "Cannot open pixbuf loader module file '/usr/x86_64-w64-mingw32/sys-root/mingw/lib/gdk-pixbuf-2.0/2.10.0/loaders.cache': No such file or directory" - build_conf_make_inst http://ftp.gnome.org/pub/GNOME/sources/gdk-pixbuf/2.32 gdk-pixbuf-2.32.1 tar.xz true --with-included-loaders=yes + build_conf_make_inst http://ftp.gnome.org/pub/GNOME/sources/gdk-pixbuf/2.36 gdk-pixbuf-2.36.12 tar.xz true --with-included-loaders=yes } ##### CAIRO ##### @@ -621,7 +620,7 @@ function make_cairo { make_glib make_pixman make_fontconfig - build_conf_make_inst http://cairographics.org/releases cairo-1.14.2 tar.xz true + build_conf_make_inst http://cairographics.org/releases rcairo-1.15.13 tar.xz true } ##### PANGO ##### @@ -630,7 +629,7 @@ function make_pango { make_cairo make_glib make_fontconfig - build_conf_make_inst http://ftp.gnome.org/pub/GNOME/sources/pango/1.38 pango-1.38.0 tar.xz true + build_conf_make_inst http://ftp.gnome.org/pub/GNOME/sources/pango/1.42 pango-1.42.1 tar.xz true } ##### GTK2 ##### @@ -647,7 +646,7 @@ function make_gtk2 { make_pango make_gdk-pixbuf make_cairo - build_conf_make_inst http://ftp.gnome.org/pub/gnome/sources/gtk+/2.24 gtk+-2.24.28 tar.xz patch_gtk2 + build_conf_make_inst http://ftp.gnome.org/pub/gnome/sources/gtk+/2.24 gtk+-2.24.32 tar.xz patch_gtk2 fi } @@ -660,7 +659,7 @@ function make_gtk3 { make_gdk-pixbuf make_cairo make_libepoxy - build_conf_make_inst http://ftp.gnome.org/pub/gnome/sources/gtk+/3.16 gtk+-3.16.7 tar.xz true + build_conf_make_inst http://ftp.gnome.org/pub/gnome/sources/gtk+/3.22 gtk+-3.22.30 tar.xz true # make all incl. tests and examples runs through fine # make install fails with issue with @@ -740,7 +739,7 @@ function install_flexlink { # An alternative is to first build an OCaml without shared library support and build flexlink with it function get_flex_dll_link_bin { - if build_prep http://alain.frisch.fr/flexdll flexdll-bin-0.34 zip 1 ; then + if build_prep https://github.com/alainfrisch/flexdll/releases/download/0.37/ flexdll-bin-0.37 zip 1 ; then install_flexdll install_flexlink build_post @@ -750,7 +749,7 @@ function get_flex_dll_link_bin { # Build flexdll and flexlink from sources after building OCaml function make_flex_dll_link { - if build_prep http://alain.frisch.fr/flexdll flexdll-0.34 tar.gz ; then + if build_prep https://github.com/alainfrisch/flexdll/releases/download/0.37/ flexdll-bin-0.37 zip ; then if [ "$TARGET_ARCH" == "i686-w64-mingw32" ]; then # shellcheck disable=SC2086 log1 make $MAKE_OPT build_mingw flexlink.exe @@ -791,11 +790,10 @@ function make_ln { function make_ocaml { get_flex_dll_link_bin - if build_prep http://caml.inria.fr/pub/distrib/ocaml-4.02 ocaml-4.02.3 tar.gz 1 ; then - # if build_prep http://caml.inria.fr/pub/distrib/ocaml-4.01 ocaml-4.01.0 tar.gz 1 ; then - # See README.win32 - cp config/m-nt.h config/m.h - cp config/s-nt.h config/s.h + if build_prep http://caml.inria.fr/pub/distrib/ocaml-4.06 ocaml-4.06.1 tar.gz 1 ; then + # See README.win32.adoc + cp config/m-nt.h byterun/caml/m.h + cp config/s-nt.h byterun/caml/s.h if [ "$TARGET_ARCH" == "i686-w64-mingw32" ]; then cp config/Makefile.mingw config/Makefile elif [ "$TARGET_ARCH" == "x86_64-w64-mingw32" ]; then @@ -831,9 +829,9 @@ function make_ocaml { # 4.01 installs these files, 4.02 doesn't. So delete them and copy them from the sources. rm -f ./*.txt cp LICENSE "$PREFIXOCAML/license_readme/ocaml/License.txt" - cp INSTALL "$PREFIXOCAML/license_readme/ocaml/Install.txt" - cp README "$PREFIXOCAML/license_readme/ocaml/ReadMe.txt" - cp README.win32 "$PREFIXOCAML/license_readme/ocaml/ReadMeWin32.txt" + cp INSTALL.adoc "$PREFIXOCAML/license_readme/ocaml/Install.txt" + cp README.adoc "$PREFIXOCAML/license_readme/ocaml/ReadMe.txt" + cp README.win32.adoc "$PREFIXOCAML/license_readme/ocaml/ReadMeWin32.txt" cp VERSION "$PREFIXOCAML/license_readme/ocaml/Version.txt" cp Changes "$PREFIXOCAML/license_readme/ocaml/Changes.txt" fi @@ -854,16 +852,30 @@ function make_ocaml_tools { ##### OCAML EXTRA LIBRARIES ##### function make_ocaml_libs { + make_num make_findlib make_lablgtk # make_stdint } +##### Ocaml num library ##### +function make_num { + make_ocaml + # We need this commit due to windows fixed, IMHO this is better than patching v1.1. + if build_prep https://github.com/ocaml/num/archive/ 7dd5e935aaa2b902585b3b2d0e55ad9b2442fff0 zip 1 num-1.1-7d; then + log2 make all + # log2 make test + log2 make install + log2 make clean + build_post + fi +} + ##### FINDLIB Ocaml library manager ##### function make_findlib { make_ocaml - if build_prep https://opam.ocaml.org/archives ocamlfind.1.5.6+opam tar.gz 1 ; then + if build_prep https://opam.ocaml.org/archives ocamlfind.1.8.0+opam tar.gz 1 ; then logn configure ./configure -bindir "$PREFIXOCAML\\bin" -sitelib "$PREFIXOCAML\\libocaml\\site-lib" -config "$PREFIXOCAML\\etc\\findlib.conf" # Note: findlib doesn't support -j 8, so don't pass MAKE_OPT log2 make all @@ -900,7 +912,7 @@ function make_camlp4 { if ! command camlp4 ; then make_ocaml make_findlib - if build_prep https://github.com/ocaml/camlp4/archive 4.02+6 tar.gz 1 camlp4-4.02+6 ; then + if build_prep https://github.com/ocaml/camlp4/archive 4.06+2 tar.gz 1 camlp4-4.06+2 ; then # See https://github.com/ocaml/camlp4/issues/41#issuecomment-112018910 logn configure ./configure # Note: camlp4 doesn't support -j 8, so don't pass MAKE_OPT @@ -917,7 +929,8 @@ function make_camlp4 { function make_camlp5 { make_ocaml make_findlib - if build_prep http://camlp5.gforge.inria.fr/distrib/src camlp5-6.14 tgz 1 ; then + + if build_prep https://github.com/camlp5/camlp5/archive rel705 tar.gz 1 camlp5-rel705; then logn configure ./configure # Somehow my virus scanner has the boot.new/SAVED directory locked after the move for a second => repeat until success sed -i 's/mv boot.new boot/until mv boot.new boot; do sleep 1; done/' Makefile @@ -944,10 +957,10 @@ function make_camlp5 { function make_lablgtk { make_ocaml make_findlib - make_camlp4 # required by lablgtk-2.18.3 and lablgtk-2.18.5 + # make_camlp4 # required by lablgtk-2.18.3 and lablgtk-2.18.5 make_gtk2 make_gtk_sourceview2 - if build_prep https://forge.ocamlcore.org/frs/download.php/1479 lablgtk-2.18.3 tar.gz 1 ; then + if build_prep https://forge.ocamlcore.org/frs/download.php/1726 lablgtk-2.18.6 tar.gz 1 ; then # configure should be fixed to search for $TARGET_ARCH-pkg-config.exe cp "/bin/$TARGET_ARCH-pkg-config.exe" bin_special/pkg-config.exe logn configure ./configure --build="$BUILD" --host="$HOST" --target="$TARGET" --prefix="$PREFIXOCAML" @@ -1130,8 +1143,10 @@ function copy_coq_license { function make_coq { make_ocaml - make_lablgtk + make_num + make_findlib make_camlp5 + make_lablgtk if case $COQ_VERSION in # e.g. git-v8.6 => download from https://github.com/coq/coq/archive/v8.6.zip diff --git a/dev/build/windows/patches_coq/lablgtk-2.18.6.patch b/dev/build/windows/patches_coq/lablgtk-2.18.6.patch new file mode 100644 index 000000000..23c303135 --- /dev/null +++ b/dev/build/windows/patches_coq/lablgtk-2.18.6.patch @@ -0,0 +1,101 @@ +diff/patch file created on Wed, Apr 25, 2018 11:08:05 AM with: +difftar-folder.sh ../coq-msoegtrop/dev/build/windows/source_cache/lablgtk-2.18.3.tar.gz lablgtk-2.18.3 1 +TARFILE= ../coq-msoegtrop/dev/build/windows/source_cache/lablgtk-2.18.3.tar.gz +FOLDER= lablgtk-2.18.3 +TARSTRIP= 1 +TARPREFIX= lablgtk-2.18.3/ +ORIGFOLDER= lablgtk-2.18.3.orig +--- lablgtk-2.18.3.orig/configure 2014-10-29 08:51:05.000000000 +0100 ++++ lablgtk-2.18.3/configure 2018-04-25 10:58:54.454501600 +0200 +@@ -2667,7 +2667,7 @@ + fi + + +-if test "`$OCAMLFIND printconf stdlib`" != "`$CAMLC -where`"; then ++if test "`$OCAMLFIND printconf stdlib | tr '\\' '/'`" != "`$CAMLC -where | tr '\\' '/'`"; then + { $as_echo "$as_me:${as_lineno-$LINENO}: WARNING: Ignoring ocamlfind" >&5 + $as_echo "$as_me: WARNING: Ignoring ocamlfind" >&2;} + OCAMLFIND=no +--- lablgtk-2.18.3.orig/src/glib.mli 2014-10-29 08:51:06.000000000 +0100 ++++ lablgtk-2.18.3/src/glib.mli 2018-04-25 10:58:54.493555500 +0200 +@@ -75,6 +75,7 @@ + type condition = [ `ERR | `HUP | `IN | `NVAL | `OUT | `PRI] + type id + val channel_of_descr : Unix.file_descr -> channel ++ val channel_of_descr_socket : Unix.file_descr -> channel + val add_watch : + cond:condition list -> callback:(condition list -> bool) -> ?prio:int -> channel -> id + val remove : id -> unit +--- lablgtk-2.18.3.orig/src/glib.ml 2014-10-29 08:51:06.000000000 +0100 ++++ lablgtk-2.18.3/src/glib.ml 2018-04-25 10:58:54.479543500 +0200 +@@ -72,6 +72,8 @@ + type id + external channel_of_descr : Unix.file_descr -> channel + = "ml_g_io_channel_unix_new" ++ external channel_of_descr_socket : Unix.file_descr -> channel ++ = "ml_g_io_channel_unix_new_socket" + external remove : id -> unit = "ml_g_source_remove" + external add_watch : + cond:condition list -> callback:(condition list -> bool) -> ?prio:int -> channel -> id +--- lablgtk-2.18.3.orig/src/Makefile 2014-10-29 08:51:06.000000000 +0100 ++++ lablgtk-2.18.3/src/Makefile 2018-04-25 10:58:54.506522500 +0200 +@@ -461,9 +461,9 @@ + do rm -f "$(BINDIR)"/$$f; done + + lablgtk.cma liblablgtk2$(XA): $(COBJS) $(MLOBJS) +- $(LIBRARIAN) -o lablgtk -oc lablgtk2 $^ $(GTKLIBS) ++ $(LIBRARIAN) -ldopt "-link -Wl,-s" -o lablgtk -oc lablgtk2 $^ $(GTKLIBS) + lablgtk.cmxa: $(COBJS) $(MLOBJS:.cmo=.cmx) +- $(LIBRARIAN) -o lablgtk -oc lablgtk2 $^ $(GTKLIBS) ++ $(LIBRARIAN) -ldopt "-link -Wl,-s" -o lablgtk -oc lablgtk2 $^ $(GTKLIBS) + lablgtk.cmxs: DYNLINKLIBS=$(GTK_LIBS) + + lablgtkgl.cma liblablgtkgl2$(XA): $(GLCOBJS) $(GLMLOBJS) +--- lablgtk-2.18.3.orig/src/ml_glib.c 2014-10-29 08:51:06.000000000 +0100 ++++ lablgtk-2.18.3/src/ml_glib.c 2018-04-25 10:58:54.539535600 +0200 +@@ -25,6 +25,8 @@ + #include <string.h> + #include <locale.h> + #ifdef _WIN32 ++/* to kill a #warning: include winsock2.h before windows.h */ ++#include <winsock2.h> + #include "win32.h" + #include <wtypes.h> + #include <io.h> +@@ -38,6 +40,11 @@ + #include <caml/callback.h> + #include <caml/threads.h> + ++#ifdef _WIN32 ++/* for Socket_val */ ++#include <caml/unixsupport.h> ++#endif ++ + #include "wrappers.h" + #include "ml_glib.h" + #include "glib_tags.h" +@@ -325,14 +332,23 @@ + + #ifndef _WIN32 + ML_1 (g_io_channel_unix_new, Int_val, Val_GIOChannel_noref) ++CAMLprim value ml_g_io_channel_unix_new_socket (value arg1) { ++ return Val_GIOChannel_noref (g_io_channel_unix_new (Int_val (arg1))); ++} + + #else + CAMLprim value ml_g_io_channel_unix_new(value wh) + { + return Val_GIOChannel_noref +- (g_io_channel_unix_new ++ (g_io_channel_win32_new_fd + (_open_osfhandle((long)*(HANDLE*)Data_custom_val(wh), O_BINARY))); + } ++ ++CAMLprim value ml_g_io_channel_unix_new_socket(value wh) ++{ ++ return Val_GIOChannel_noref ++ (g_io_channel_win32_new_socket(Socket_val(wh))); ++} + #endif + + static gboolean ml_g_io_channel_watch(GIOChannel *s, GIOCondition c, diff --git a/dev/ci/appveyor.sh b/dev/ci/appveyor.sh index c72705c7f..7bf9ad8c9 100644 --- a/dev/ci/appveyor.sh +++ b/dev/ci/appveyor.sh @@ -1,9 +1,15 @@ #!/bin/bash + set -e -x + +APPVEYOR_OPAM_SWITCH=4.06.1+mingw64c + wget https://github.com/fdopen/opam-repository-mingw/releases/download/0.0.0.1/opam64.tar.xz tar -xf opam64.tar.xz bash opam64/install.sh -opam init -a mingw https://github.com/fdopen/opam-repository-mingw.git --comp 4.02.3+mingw64c --switch 4.02.3+mingw64c + +opam init -a mingw https://github.com/fdopen/opam-repository-mingw.git --comp $APPVEYOR_OPAM_SWITCH --switch $APPVEYOR_OPAM_SWITCH eval "$(opam config env)" -opam install -y ocamlfind camlp5 ounit +opam install -y num ocamlfind camlp5 ounit + cd "$APPVEYOR_BUILD_FOLDER" && ./configure -local && make && make byte && make -C test-suite all INTERACTIVE= && make validate diff --git a/dev/ci/user-overlays/07099-ppedrot-unification-returns-option.sh b/dev/ci/user-overlays/07099-ppedrot-unification-returns-option.sh new file mode 100644 index 000000000..e6c48d10a --- /dev/null +++ b/dev/ci/user-overlays/07099-ppedrot-unification-returns-option.sh @@ -0,0 +1,4 @@ +if [ "$CI_PULL_REQUEST" = "7099" ] || [ "$CI_BRANCH" = "unification-returns-option" ]; then + Equations_CI_BRANCH=unification-returns-option + Equations_CI_GITURL=https://github.com/ppedrot/Coq-Equations +fi diff --git a/dev/ci/user-overlays/07495-gares-elpi-test-bug.sh b/dev/ci/user-overlays/07495-gares-elpi-test-bug.sh new file mode 100644 index 000000000..6939ead2b --- /dev/null +++ b/dev/ci/user-overlays/07495-gares-elpi-test-bug.sh @@ -0,0 +1,8 @@ +if [ "$CI_PULL_REQUEST" = "7495" ] || [ "$CI_BRANCH" = "fix-restrict" ]; then + + # this branch contains a commit not present on coq-master that triggers + # the universe restriction bug #7472 + Elpi_CI_BRANCH=overlay-7495 + Elpi_CI_GITURL=https://github.com/LPCIC/coq-elpi.git + +fi diff --git a/dev/doc/changes.md b/dev/doc/changes.md index 4838dd734..bb8189efc 100644 --- a/dev/doc/changes.md +++ b/dev/doc/changes.md @@ -28,6 +28,10 @@ Proof engine should indicate what the canonical form is. An important change is the move of `Globnames.global_reference` to `Names.GlobRef.t`. +- Unification API returns `evar_map option` instead of `bool * evar_map` + with the guarantee that the `evar_map` was unchanged if the boolean + was false. + ML Libraries used by Coq - Introduction of a "Smart" module for collecting "smart*" functions, e.g. diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst index 6ea1c162f..ff5d352c9 100644 --- a/doc/sphinx/language/gallina-extensions.rst +++ b/doc/sphinx/language/gallina-extensions.rst @@ -2240,6 +2240,7 @@ This option (off by default) activates the full display of how the context of an existential variable is instantiated at each of the occurrences of the existential variable. +.. _tactics-in-terms: Solving existential variables using tactics ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ diff --git a/doc/sphinx/practical-tools/utilities.rst b/doc/sphinx/practical-tools/utilities.rst index 59a88771a..5dba92429 100644 --- a/doc/sphinx/practical-tools/utilities.rst +++ b/doc/sphinx/practical-tools/utilities.rst @@ -139,7 +139,19 @@ Here we describe only few of them. can be extended by including other paths in which ``*.cm*`` files are searched. For example ``COQ_SRC_SUBDIRS+=user-contrib/Unicoq`` lets you build a plugin containing OCaml code that depends on the - OCaml code of ``Unicoq``. + OCaml code of ``Unicoq`` +:COQFLAGS: + override the flags passed to ``coqc``. By default ``-q``. +:COQEXTRAFLAGS: + extend the flags passed to ``coqc`` +:COQCHKFLAGS: + override the flags passed to ``coqchk``. By default ``-silent -o``. +:COQCHKEXTRAFLAGS: + extend the flags passed to ``coqchk`` +:COQDOCFLAGS: + override the flags passed to ``coqdoc``. By default ``-interpolate -utf8``. +:COQDOCEXTRAFLAGS: + extend the flags passed to ``coqdoc`` **Rule extension** diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index da4c3f9d7..90ca0da43 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -879,14 +879,6 @@ quantification or an implication. This is equivalent to :n:`clear @ident. ... clear @ident.` -.. tacv:: clearbody @ident - :name: clearbody - - This tactic expects :n:`@ident` to be a local definition then clears its - body. Otherwise said, this tactic turns a definition into an assumption. - -.. exn:: @ident is not a local definition. - .. tacv:: clear - {+ @ident} This tactic clears all the hypotheses except the ones depending in the @@ -901,6 +893,15 @@ quantification or an implication. This clears the hypothesis :n:`@ident` and all the hypotheses that depend on it. +.. tacv:: clearbody {+ @ident} + :name: clearbody + + This tactic expects :n:`{+ @ident}` to be local definitions and clears their + respective bodies. + In other words, it turns the given definitions into assumptions. + +.. exn:: @ident is not a local definition. + .. tacn:: revert {+ @ident} :name: revert @@ -2867,8 +2868,8 @@ the conversion in hypotheses :n:`{+ @ident}`. .. coqtop:: all Definition fcomp A B C f (g : A -> B) (x : A) : C := f (g x). - Notation "f \o g" := (fcomp f g) (at level 50). Arguments fcomp {A B C} f g x /. + Notation "f \o g" := (fcomp f g) (at level 50). After that command the expression :g:`(f \o g)` is left untouched by ``simpl`` while :g:`((f \o g) t)` is reduced to :g:`(f (g t))`. @@ -3702,19 +3703,24 @@ Setting implicit automation tactics time the term argument of a tactic has one of its holes not fully resolved. - .. example:: + .. deprecated:: 8.9 - .. coqtop:: all + This command is deprecated. Use :ref:`typeclasses <typeclasses>` or + :ref:`tactics-in-terms <tactics-in-terms>` instead. - Parameter quo : nat -> forall n:nat, n<>0 -> nat. - Notation "x // y" := (quo x y _) (at level 40). - Declare Implicit Tactic assumption. - Goal forall n m, m<>0 -> { q:nat & { r | q * m + r = n } }. - intros. - exists (n // m). + .. example:: + + .. coqtop:: all + + Parameter quo : nat -> forall n:nat, n<>0 -> nat. + Notation "x // y" := (quo x y _) (at level 40). + Declare Implicit Tactic assumption. + Goal forall n m, m<>0 -> { q:nat & { r | q * m + r = n } }. + intros. + exists (n // m). - The tactic ``exists (n // m)`` did not fail. The hole was solved - by ``assumption`` so that it behaved as ``exists (quo n m H)``. + The tactic ``exists (n // m)`` did not fail. The hole was solved + by ``assumption`` so that it behaved as ``exists (quo n m H)``. .. _decisionprocedures: diff --git a/engine/termops.ml b/engine/termops.ml index 51fc59289..0c567754a 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -857,6 +857,13 @@ let occur_meta_or_existential sigma c = | _ -> EConstr.iter sigma occrec c in try occrec c; false with Occur -> true +let occur_metavariable sigma m c = + let rec occrec c = match EConstr.kind sigma c with + | Meta m' -> if Int.equal m m' then raise Occur + | _ -> EConstr.iter sigma occrec c + in + try occrec c; false with Occur -> true + let occur_evar sigma n c = let rec occur_rec c = match EConstr.kind sigma c with | Evar (sp,_) when Evar.equal sp n -> raise Occur diff --git a/engine/termops.mli b/engine/termops.mli index bb3cbb6a8..6e63539ca 100644 --- a/engine/termops.mli +++ b/engine/termops.mli @@ -94,6 +94,7 @@ exception Occur val occur_meta : Evd.evar_map -> constr -> bool val occur_existential : Evd.evar_map -> constr -> bool val occur_meta_or_existential : Evd.evar_map -> constr -> bool +val occur_metavariable : Evd.evar_map -> metavariable -> constr -> bool val occur_evar : Evd.evar_map -> Evar.t -> constr -> bool val occur_var : env -> Evd.evar_map -> Id.t -> constr -> bool val occur_var_in_decl : diff --git a/engine/univops.ml b/engine/univops.ml index 76dbaa250..3fd518490 100644 --- a/engine/univops.ml +++ b/engine/univops.ml @@ -35,79 +35,14 @@ let universes_of_constr env c = | _ -> Constr.fold aux s c in aux LSet.empty c -type graphnode = { - mutable up : constraint_type LMap.t; - mutable visited : bool -} - -let merge_types d d0 = - match d, d0 with - | _, Lt | Lt, _ -> Lt - | Le, _ | _, Le -> Le - | Eq, Eq -> Eq - -let merge_up d b up = - let find = try Some (LMap.find b up) with Not_found -> None in - match find with - | Some d0 -> - let d = merge_types d d0 in - if d == d0 then up else LMap.add b d up - | None -> LMap.add b d up - -let add_up a d b graph = - let node, graph = - try LMap.find a graph, graph - with Not_found -> - let node = { up = LMap.empty; visited = false } in - node, LMap.add a node graph - in - node.up <- merge_up d b node.up; - graph - -(* for each node transitive close until you find a non removable, discard the rest *) -let transitive_close removable graph = - let rec do_node a node = - if not node.visited - then - let keepup = - LMap.fold (fun b d keepup -> - if not (LSet.mem b removable) - then merge_up d b keepup - else - begin - match LMap.find b graph with - | bnode -> - do_node b bnode; - LMap.fold (fun k d' keepup -> - merge_up (merge_types d d') k keepup) - bnode.up keepup - | exception Not_found -> keepup - end - ) - node.up LMap.empty - in - node.up <- keepup; - node.visited <- true - in - LMap.iter do_node graph - -let restrict_universe_context (univs,csts) keep = - let removable = LSet.diff univs keep in - let (csts, rem) = - Constraint.fold (fun (a,d,b as cst) (csts, rem) -> - if LSet.mem a removable || LSet.mem b removable - then (csts, add_up a d b rem) - else (Constraint.add cst csts, rem)) - csts (Constraint.empty, LMap.empty) - in - transitive_close removable rem; - let csts = - LMap.fold (fun a node csts -> - if LSet.mem a removable - then csts - else - LMap.fold (fun b d csts -> Constraint.add (a,d,b) csts) - node.up csts) - rem csts - in +let restrict_universe_context (univs, csts) keep = + let removed = LSet.diff univs keep in + if LSet.is_empty removed then univs, csts + else + let allunivs = Constraint.fold (fun (u,_,v) all -> LSet.add u (LSet.add v all)) csts univs in + let g = UGraph.empty_universes in + let g = LSet.fold UGraph.add_universe_unconstrained allunivs g in + let g = UGraph.merge_constraints csts g in + let allkept = LSet.diff allunivs removed in + let csts = UGraph.constraints_for ~kept:allkept g in (LSet.inter univs keep, csts) diff --git a/engine/univops.mli b/engine/univops.mli index d1585414c..0b37ab975 100644 --- a/engine/univops.mli +++ b/engine/univops.mli @@ -14,5 +14,8 @@ open Univ (** The universes of monomorphic constants appear. *) val universes_of_constr : Environ.env -> constr -> LSet.t -(** Shrink a universe context to a restricted set of variables *) +(** [restrict_universe_context (univs,csts) keep] restricts [univs] to + the universes in [keep]. The constraints [csts] are adjusted so + that transitive constraints between remaining universes (those in + [keep] and those not in [univs]) are preserved. *) val restrict_universe_context : ContextSet.t -> LSet.t -> ContextSet.t diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 1691ff6d8..848180743 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -1141,9 +1141,18 @@ let check_number_of_pattern loc n l = if not (Int.equal n p) then raise (InternalizationError (loc,BadPatternsNumber (n,p))) let check_or_pat_variables loc ids idsl = - if List.exists (fun ids' -> not (List.eq_set (fun {loc;v=id} {v=id'} -> Id.equal id id') ids ids')) idsl then - user_err ?loc (str - "The components of this disjunctive pattern must bind the same variables.") + let eq_id {v=id} {v=id'} = Id.equal id id' in + (* Collect remaining patterns which do not have the same variables as the first pattern *) + let idsl = List.filter (fun ids' -> not (List.eq_set eq_id ids ids')) idsl in + match idsl with + | ids'::_ -> + (* Look for an [id] which is either in [ids] and not in [ids'] or in [ids'] and not in [ids] *) + let ids'' = List.subtract eq_id ids ids' in + let ids'' = if ids'' = [] then List.subtract eq_id ids' ids else ids'' in + user_err ?loc + (strbrk "The components of this disjunctive pattern must bind the same variables (" ++ + Id.print (List.hd ids'').v ++ strbrk " is not bound in all patterns).") + | [] -> () (** Use only when params were NOT asked to the user. @return if letin are included *) diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml index 4da5f0f38..1d8861cbc 100644 --- a/kernel/cClosure.ml +++ b/kernel/cClosure.ml @@ -1051,7 +1051,12 @@ let norm_val info tab v = let inject c = mk_clos (subs_id 0) c -let whd_stack infos tab m stk = +let whd_stack infos tab m stk = match m.norm with +| Whnf | Norm -> + (** No need to perform [kni] nor to unlock updates because + every head subterm of [m] is [Whnf] or [Norm] *) + knh infos m stk +| Red | Cstr -> let k = kni infos tab m stk in let () = if !share then ignore (fapp_stack k) in (* to unlock Zupdates! *) k diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml index 8b61ed0c5..6db75c89a 100644 --- a/kernel/nativelambda.ml +++ b/kernel/nativelambda.ml @@ -296,15 +296,17 @@ let is_value lc = match lc with | Lval _ -> true | Lmakeblock(_,_,_,args) when Array.is_empty args -> true + | Luint (UintVal _) -> true | _ -> false - + let get_value lc = match lc with | Lval v -> v - | Lmakeblock(_,_,tag,args) when Array.is_empty args -> + | Lmakeblock(_,_,tag,args) when Array.is_empty args -> Nativevalues.mk_int tag + | Luint (UintVal i) -> Nativevalues.mk_uint i | _ -> raise Not_found - + let make_args start _end = Array.init (start - _end + 1) (fun i -> Lrel (Anonymous, start - i)) diff --git a/kernel/reduction.ml b/kernel/reduction.ml index 8ca596d48..f4af31386 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -648,25 +648,24 @@ let check_leq univs u u' = let check_sort_cmp_universes env pb s0 s1 univs = let open Sorts in - match (s0,s1) with + if not (type_in_type env) then + match (s0,s1) with | (Prop c1, Prop c2) when is_cumul pb -> begin match c1, c2 with - | Null, _ | _, Pos -> () (* Prop <= Set *) - | _ -> raise NotConvertible + | Null, _ | _, Pos -> () (* Prop <= Set *) + | _ -> raise NotConvertible end | (Prop c1, Prop c2) -> if c1 != c2 then raise NotConvertible | (Prop c1, Type u) -> - if not (type_in_type env) then - let u0 = univ_of_sort s0 in - (match pb with - | CUMUL -> check_leq univs u0 u - | CONV -> check_eq univs u0 u) + let u0 = univ_of_sort s0 in + (match pb with + | CUMUL -> check_leq univs u0 u + | CONV -> check_eq univs u0 u) | (Type u, Prop c) -> raise NotConvertible | (Type u1, Type u2) -> - if not (type_in_type env) then - (match pb with - | CUMUL -> check_leq univs u1 u2 - | CONV -> check_eq univs u1 u2) + (match pb with + | CUMUL -> check_leq univs u1 u2 + | CONV -> check_eq univs u1 u2) let checked_sort_cmp_universes env pb s0 s1 univs = check_sort_cmp_universes env pb s0 s1 univs; univs @@ -699,25 +698,25 @@ let infer_leq (univs, cstrs as cuniv) u u' = let infer_cmp_universes env pb s0 s1 univs = let open Sorts in - match (s0,s1) with + if type_in_type env then univs + else + match (s0,s1) with | (Prop c1, Prop c2) when is_cumul pb -> begin match c1, c2 with - | Null, _ | _, Pos -> univs (* Prop <= Set *) - | _ -> raise NotConvertible + | Null, _ | _, Pos -> univs (* Prop <= Set *) + | _ -> raise NotConvertible end | (Prop c1, Prop c2) -> if c1 == c2 then univs else raise NotConvertible | (Prop c1, Type u) -> let u0 = univ_of_sort s0 in - (match pb with - | CUMUL -> infer_leq univs u0 u - | CONV -> infer_eq univs u0 u) + (match pb with + | CUMUL -> infer_leq univs u0 u + | CONV -> infer_eq univs u0 u) | (Type u, Prop c) -> raise NotConvertible | (Type u1, Type u2) -> - if not (type_in_type env) then - (match pb with - | CUMUL -> infer_leq univs u1 u2 - | CONV -> infer_eq univs u1 u2) - else univs + (match pb with + | CUMUL -> infer_leq univs u1 u2 + | CONV -> infer_eq univs u1 u2) let infer_convert_instances ~flex u u' (univs,cstrs) = let cstrs' = diff --git a/kernel/uGraph.ml b/kernel/uGraph.ml index e6b27077b..4a9467de5 100644 --- a/kernel/uGraph.ml +++ b/kernel/uGraph.ml @@ -503,7 +503,7 @@ let insert_edge strict ucan vcan g = let () = cleanup_universes g in raise e -let add_universe vlev strict g = +let add_universe_gen vlev g = try let _arcv = UMap.find vlev g.entries in raise AlreadyDeclared @@ -520,8 +520,14 @@ let add_universe vlev strict g = } in let entries = UMap.add vlev (Canonical v) g.entries in - let g = { entries; index = g.index - 1; n_nodes = g.n_nodes + 1; n_edges = g.n_edges } in - insert_edge strict (get_set_arc g) v g + { entries; index = g.index - 1; n_nodes = g.n_nodes + 1; n_edges = g.n_edges }, v + +let add_universe vlev strict g = + let g, v = add_universe_gen vlev g in + insert_edge strict (get_set_arc g) v g + +let add_universe_unconstrained vlev g = + fst (add_universe_gen vlev g) exception Found_explanation of explanation @@ -696,6 +702,9 @@ let enforce_univ_lt u v g = error_inconsistency Lt u v (get_explanation false v u g) let empty_universes = + { entries = UMap.empty; index = 0; n_nodes = 0; n_edges = 0 } + +let initial_universes = let set_arc = Canonical { univ = Level.set; ltle = LMap.empty; @@ -718,9 +727,6 @@ let empty_universes = let empty = { entries; index = (-2); n_nodes = 2; n_edges = 0 } in enforce_univ_lt Level.prop Level.set empty -(* Prop = Set is forbidden here. *) -let initial_universes = empty_universes - let is_initial_universes g = UMap.equal (==) g.entries initial_universes.entries let enforce_constraint cst g = @@ -780,6 +786,42 @@ let constraints_of_universes g = let csts = UMap.fold constraints_of g.entries Constraint.empty in csts, UF.partition uf +(* domain g.entries = kept + removed *) +let constraints_for ~kept g = + (* rmap: partial map from canonical universes to kept universes *) + let rmap, csts = LSet.fold (fun u (rmap,csts) -> + let arcu = repr g u in + if LSet.mem arcu.univ kept then + LMap.add arcu.univ arcu.univ rmap, enforce_eq_level u arcu.univ csts + else + match LMap.find arcu.univ rmap with + | v -> rmap, enforce_eq_level u v csts + | exception Not_found -> LMap.add arcu.univ u rmap, csts) + kept (LMap.empty,Constraint.empty) + in + let rec add_from u csts todo = match todo with + | [] -> csts + | (v,strict)::todo -> + let v = repr g v in + (match LMap.find v.univ rmap with + | v -> + let d = if strict then Lt else Le in + let csts = Constraint.add (u,d,v) csts in + add_from u csts todo + | exception Not_found -> + (* v is not equal to any kept universe *) + let todo = LMap.fold (fun v' strict' todo -> + (v',strict || strict') :: todo) + v.ltle todo + in + add_from u csts todo) + in + LSet.fold (fun u csts -> + let arc = repr g u in + LMap.fold (fun v strict csts -> add_from u csts [v,strict]) + arc.ltle csts) + kept csts + (** [sort_universes g] builds a totally ordered universe graph. The output graph should imply the input graph (and the implication will be strict most of the time), but is not necessarily minimal. diff --git a/kernel/uGraph.mli b/kernel/uGraph.mli index cca2eb472..e6dd629e4 100644 --- a/kernel/uGraph.mli +++ b/kernel/uGraph.mli @@ -49,13 +49,15 @@ exception AlreadyDeclared val add_universe : Level.t -> bool -> t -> t +(** Add a universe without (Prop,Set) <= u *) +val add_universe_unconstrained : Level.t -> t -> t + (** {6 Pretty-printing of universes. } *) val pr_universes : (Level.t -> Pp.t) -> t -> Pp.t (** The empty graph of universes *) val empty_universes : t -[@@ocaml.deprecated "Use UGraph.initial_universes"] val sort_universes : t -> t @@ -64,6 +66,12 @@ val sort_universes : t -> t of the universes into equivalence classes. *) val constraints_of_universes : t -> Constraint.t * LSet.t list +(** [constraints_for ~kept g] returns the constraints about the + universes [kept] in [g] up to transitivity. + + eg if [g] is [a <= b <= c] then [constraints_for ~kept:{a, c} g] is [a <= c]. *) +val constraints_for : kept:LSet.t -> t -> Constraint.t + val check_subtype : AUContext.t check_function (** [check_subtype univ ctx1 ctx2] checks whether [ctx2] is an instance of [ctx1]. *) diff --git a/plugins/firstorder/unify.ml b/plugins/firstorder/unify.ml index 06f56d06e..d63fe9d79 100644 --- a/plugins/firstorder/unify.ml +++ b/plugins/firstorder/unify.ml @@ -56,12 +56,12 @@ let unif evd t1 t2= | Meta i,_ -> let t=subst_meta !sigma nt2 in if Int.Set.is_empty (free_rels evd t) && - not (dependent evd (EConstr.mkMeta i) t) then + not (occur_metavariable evd i t) then bind i t else raise (UFAIL(nt1,nt2)) | _,Meta i -> let t=subst_meta !sigma nt1 in if Int.Set.is_empty (free_rels evd t) && - not (dependent evd (EConstr.mkMeta i) t) then + not (occur_metavariable evd i t) then bind i t else raise (UFAIL(nt1,nt2)) | Cast(_,_,_),_->Queue.add (strip_outer_cast evd nt1,nt2) bige | _,Cast(_,_,_)->Queue.add (nt1,strip_outer_cast evd nt2) bige diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4 index c5254b37c..cb7183638 100644 --- a/plugins/ltac/extratactics.ml4 +++ b/plugins/ltac/extratactics.ml4 @@ -285,77 +285,6 @@ VERNAC COMMAND FUNCTIONAL EXTEND HintRewrite CLASSIFIED BY classify_hint END (**********************************************************************) -(* Hint Resolve *) - -open EConstr -open Vars -open Coqlib - -let project_hint ~poly pri l2r r = - let gr = Smartlocate.global_with_alias r in - let env = Global.env() in - let sigma = Evd.from_env env in - let sigma, c = Evd.fresh_global env sigma gr in - let t = Retyping.get_type_of env sigma c in - let t = - Tacred.reduce_to_quantified_ref env sigma (Lazy.force coq_iff_ref) t in - let sign,ccl = decompose_prod_assum sigma t in - let (a,b) = match snd (decompose_app sigma ccl) with - | [a;b] -> (a,b) - | _ -> assert false in - let p = - if l2r then build_coq_iff_left_proj () else build_coq_iff_right_proj () in - let sigma, p = Evd.fresh_global env sigma p in - let c = Reductionops.whd_beta sigma (mkApp (c, Context.Rel.to_extended_vect mkRel 0 sign)) in - let c = it_mkLambda_or_LetIn - (mkApp (p,[|mkArrow a (lift 1 b);mkArrow b (lift 1 a);c|])) sign in - let id = - Nameops.add_suffix (Nametab.basename_of_global gr) ("_proj_" ^ (if l2r then "l2r" else "r2l")) - in - let ctx = Evd.const_univ_entry ~poly sigma in - let c = EConstr.to_constr sigma c in - let c = Declare.declare_definition ~internal:Declare.InternalTacticRequest id (c,ctx) in - let info = {Typeclasses.hint_priority = pri; hint_pattern = None} in - (info,false,true,Hints.PathAny, Hints.IsGlobRef (Globnames.ConstRef c)) - -let add_hints_iff ~atts l2r lc n bl = - let open Vernacinterp in - Hints.add_hints ~local:(Locality.make_module_locality atts.locality) bl - (Hints.HintsResolveEntry (List.map (project_hint ~poly:atts.polymorphic n l2r) lc)) - -VERNAC COMMAND FUNCTIONAL EXTEND HintResolveIffLR CLASSIFIED AS SIDEFF - [ "Hint" "Resolve" "->" ne_global_list(lc) natural_opt(n) - ":" preident_list(bl) ] -> - [ fun ~atts ~st -> begin - add_hints_iff ~atts true lc n bl; - st - end - ] -| [ "Hint" "Resolve" "->" ne_global_list(lc) natural_opt(n) ] -> - [ fun ~atts ~st -> begin - add_hints_iff ~atts true lc n ["core"]; - st - end - ] -END - -VERNAC COMMAND FUNCTIONAL EXTEND HintResolveIffRL CLASSIFIED AS SIDEFF - [ "Hint" "Resolve" "<-" ne_global_list(lc) natural_opt(n) - ":" preident_list(bl) ] -> - [ fun ~atts ~st -> begin - add_hints_iff ~atts false lc n bl; - st - end - ] -| [ "Hint" "Resolve" "<-" ne_global_list(lc) natural_opt(n) ] -> - [ fun ~atts ~st -> begin - add_hints_iff ~atts false lc n ["core"]; - st - end - ] -END - -(**********************************************************************) (* Refine *) open EConstr @@ -594,10 +523,16 @@ let inImplicitTactic : glob_tactic_expr option -> obj = subst_function = subst_implicit_tactic; classify_function = (fun o -> Dispose)} +let warn_deprecated_implicit_tactic = + CWarnings.create ~name:"deprecated-implicit-tactic" ~category:"deprecated" + (fun () -> strbrk "Implicit tactics are deprecated") + let declare_implicit_tactic tac = + let () = warn_deprecated_implicit_tactic () in Lib.add_anonymous_leaf (inImplicitTactic (Some (Tacintern.glob_tactic tac))) let clear_implicit_tactic () = + let () = warn_deprecated_implicit_tactic () in Lib.add_anonymous_leaf (inImplicitTactic None) VERNAC COMMAND EXTEND ImplicitTactic CLASSIFIED AS SIDEFF diff --git a/pretyping/cases.ml b/pretyping/cases.ml index ee7c39982..1edce17bd 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -574,7 +574,7 @@ let dependent_decl sigma a = let rec dep_in_tomatch sigma n = function | (Pushed _ | Alias _ | NonDepAlias) :: l -> dep_in_tomatch sigma n l - | Abstract (_,d) :: l -> dependent_decl sigma (mkRel n) d || dep_in_tomatch sigma (n+1) l + | Abstract (_,d) :: l -> RelDecl.exists (fun c -> not (noccurn sigma n c)) d || dep_in_tomatch sigma (n+1) l | [] -> false let dependencies_in_rhs sigma nargs current tms eqns = @@ -1704,9 +1704,11 @@ let abstract_tycon ?loc env evdref subst tycon extenv t = List.map_i (fun i _ -> if Int.List.mem i vl then u else mkRel i) 1 (rel_context extenv) in - let rel_filter = - List.map (fun a -> not (isRel !evdref a) || dependent !evdref a u - || Int.Set.mem (destRel !evdref a) depvl) inst in + let map a = match EConstr.kind !evdref a with + | Rel n -> not (noccurn !evdref n u) || Int.Set.mem n depvl + | _ -> true + in + let rel_filter = List.map map inst in let named_filter = List.map (fun d -> local_occur_var !evdref (NamedDecl.get_id d) u) (named_context extenv) in @@ -1848,7 +1850,7 @@ let build_inversion_problem loc env sigma tms t = (* [pb] is the auxiliary pattern-matching serving as skeleton for the return type of the original problem Xi *) let s' = Retyping.get_sort_of env sigma t in - let sigma, s = Evd.new_sort_variable univ_flexible_alg sigma in + let sigma, s = Evd.new_sort_variable univ_flexible sigma in let sigma = Evd.set_leq_sort env sigma s' s in let evdref = ref sigma in let pb = @@ -1937,8 +1939,8 @@ let prepare_predicate_from_arsign_tycon env sigma loc tomatchs arsign c = List.fold_right2 (fun (tm, tmtype) sign (subst, len) -> let signlen = List.length sign in match EConstr.kind sigma tm with - | Rel n when dependent sigma tm c - && Int.equal signlen 1 (* The term to match is not of a dependent type itself *) -> + | Rel n when Int.equal signlen 1 && not (noccurn sigma n c) + (* The term to match is not of a dependent type itself *) -> ((n, len) :: subst, len - signlen) | Rel n when signlen > 1 (* The term is of a dependent type, maybe some variable in its type appears in the tycon. *) -> @@ -1949,13 +1951,13 @@ let prepare_predicate_from_arsign_tycon env sigma loc tomatchs arsign c = List.fold_left (fun (subst, len) arg -> match EConstr.kind sigma arg with - | Rel n when dependent sigma arg c -> + | Rel n when not (noccurn sigma n c) -> ((n, len) :: subst, pred len) | _ -> (subst, pred len)) (subst, len) realargs in let subst = - if dependent sigma tm c && List.for_all (isRel sigma) realargs + if not (noccurn sigma n c) && List.for_all (isRel sigma) realargs then (n, len) :: subst else subst in (subst, pred len)) | _ -> (subst, len - signlen)) diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml index 22da5315f..2bc603a90 100644 --- a/pretyping/constr_matching.ml +++ b/pretyping/constr_matching.ml @@ -59,7 +59,7 @@ let warn_meta_collision = strbrk " and a metavariable of same name.") -let constrain sigma n (ids, m) (names, terms as subst) = +let constrain sigma n (ids, m) ((names,seen as names_seen), terms as subst) = let open EConstr in try let (ids', m') = Id.Map.find n terms in @@ -67,19 +67,21 @@ let constrain sigma n (ids, m) (names, terms as subst) = else raise PatternMatchingFailure with Not_found -> let () = if Id.Map.mem n names then warn_meta_collision n in - (names, Id.Map.add n (ids, m) terms) + (names_seen, Id.Map.add n (ids, m) terms) -let add_binders na1 na2 binding_vars (names, terms as subst) = +let add_binders na1 na2 binding_vars ((names,seen), terms as subst) = match na1, na2 with | Name id1, Name id2 when Id.Set.mem id1 binding_vars -> if Id.Map.mem id1 names then let () = Glob_ops.warn_variable_collision id1 in - (names, terms) + subst else + let id2 = Namegen.next_ident_away id2 seen in let names = Id.Map.add id1 id2 names in + let seen = Id.Set.add id2 seen in let () = if Id.Map.mem id1 terms then warn_meta_collision id1 in - (names, terms) + ((names,seen), terms) | _ -> subst let rec build_lambda sigma vars ctx m = match vars with @@ -413,13 +415,15 @@ let matches_core env sigma allow_bound_rels | PFix _ | PCoFix _| PEvar _), _ -> raise PatternMatchingFailure in - sorec [] env (Id.Map.empty, Id.Map.empty) pat c + sorec [] env ((Id.Map.empty,Id.Set.empty), Id.Map.empty) pat c let matches_core_closed env sigma pat c = let names, subst = matches_core env sigma false pat c in - (names, Id.Map.map snd subst) + (fst names, Id.Map.map snd subst) -let extended_matches env sigma = matches_core env sigma true +let extended_matches env sigma pat c = + let (names,_), subst = matches_core env sigma true pat c in + names, subst let matches env sigma pat c = snd (matches_core_closed env sigma (Id.Set.empty,pat) c) diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 062136ff5..6d08f66c1 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -366,13 +366,10 @@ let rec evar_conv_x ts env evd pbty term1 term2 = let ground_test = if is_ground_term evd term1 && is_ground_term evd term2 then ( let e = - try - let evd, b = infer_conv ~catch_incon:false ~pb:pbty ~ts:(fst ts) - env evd term1 term2 - in - if b then Success evd - else UnifFailure (evd, ConversionFailed (env,term1,term2)) - with Univ.UniverseInconsistency e -> UnifFailure (evd, UnifUnivInconsistency e) + match infer_conv ~catch_incon:false ~pb:pbty ~ts:(fst ts) env evd term1 term2 with + | Some evd -> Success evd + | None -> UnifFailure (evd, ConversionFailed (env,term1,term2)) + | exception Univ.UniverseInconsistency e -> UnifFailure (evd, UnifUnivInconsistency e) in match e with | UnifFailure (evd, e) when not (is_ground_env evd env) -> None diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index b7eaff078..aefae1ecc 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -525,7 +525,7 @@ let is_unification_pattern_meta env evd nb m l t = match Option.List.map map l with | Some l -> begin match find_unification_pattern_args env evd l t with - | Some _ as x when not (dependent evd (mkMeta m) t) -> x + | Some _ as x when not (occur_metavariable evd m t) -> x | _ -> None end | None -> @@ -1068,8 +1068,14 @@ let do_restrict_hyps evd (evk,args as ev) filter candidates = let postpone_non_unique_projection env evd pbty (evk,argsv as ev) sols rhs = let rhs = expand_vars_in_term env evd rhs in - let filter = - restrict_upon_filter evd evk + let filter a = match EConstr.kind evd a with + | Rel n -> not (noccurn evd n rhs) + | Var id -> + local_occur_var evd id rhs + || List.exists (fun (id', _) -> Id.equal id id') sols + | _ -> true + in + let filter = restrict_upon_filter evd evk filter argsv in (* Keep only variables that occur in rhs *) (* This is not safe: is the variable is a local def, its body *) (* may contain references to variables that are removed, leading to *) @@ -1077,9 +1083,6 @@ let postpone_non_unique_projection env evd pbty (evk,argsv as ev) sols rhs = (* that says that the body is hidden. Note that expand_vars_in_term *) (* expands only rels and vars aliases, not rels or vars bound to an *) (* arbitrary complex term *) - (fun a -> not (isRel evd a || isVar evd a) - || dependent evd a rhs || List.exists (fun (id,_) -> isVarId evd id a) sols) - argsv in let filter = closure_of_filter evd evk filter in let candidates = extract_candidates sols in match candidates with diff --git a/pretyping/nativenorm.mli b/pretyping/nativenorm.mli index 67b7a2a40..4997d0bf0 100644 --- a/pretyping/nativenorm.mli +++ b/pretyping/nativenorm.mli @@ -25,4 +25,4 @@ val native_norm : env -> evar_map -> constr -> types -> constr (** Conversion with inference of universe constraints *) val native_infer_conv : ?pb:conv_pb -> env -> evar_map -> constr -> constr -> - evar_map * bool + evar_map option diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 92f87ab95..b2507b5f2 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -1082,9 +1082,9 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre let cj = pretype empty_tycon env evdref lvar c in let cty = nf_evar !evdref cj.uj_type and tval = nf_evar !evdref tval in if not (occur_existential !evdref cty || occur_existential !evdref tval) then - let (evd,b) = Reductionops.vm_infer_conv env.ExtraEnv.env !evdref cty tval in - if b then (evdref := evd; cj, tval) - else + match Reductionops.vm_infer_conv env.ExtraEnv.env !evdref cty tval with + | Some evd -> (evdref := evd; cj, tval) + | None -> error_actual_type ?loc env.ExtraEnv.env !evdref cj tval (ConversionFailed (env.ExtraEnv.env,cty,tval)) else user_err ?loc (str "Cannot check cast with vm: " ++ @@ -1093,9 +1093,9 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre let cj = pretype empty_tycon env evdref lvar c in let cty = nf_evar !evdref cj.uj_type and tval = nf_evar !evdref tval in begin - let (evd,b) = Nativenorm.native_infer_conv env.ExtraEnv.env !evdref cty tval in - if b then (evdref := evd; cj, tval) - else + match Nativenorm.native_infer_conv env.ExtraEnv.env !evdref cty tval with + | Some evd -> (evdref := evd; cj, tval) + | None -> error_actual_type ?loc env.ExtraEnv.env !evdref cj tval (ConversionFailed (env.ExtraEnv.env,cty,tval)) end diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 6fde86837..7fb1a0a57 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -1348,11 +1348,10 @@ let infer_conv_gen conv_fun ?(catch_incon=true) ?(pb=Reduction.CUMUL) ?(ts=full_transparent_state) env sigma x y = (** FIXME *) try - let b, sigma = - let ans = - if pb == Reduction.CUMUL then + let ans = match pb with + | Reduction.CUMUL -> EConstr.leq_constr_universes env sigma x y - else + | Reduction.CONV -> EConstr.eq_constr_universes env sigma x y in let ans = match ans with @@ -1362,20 +1361,17 @@ let infer_conv_gen conv_fun ?(catch_incon=true) ?(pb=Reduction.CUMUL) with Univ.UniverseInconsistency _ | Evd.UniversesDiffer -> None in match ans with - | None -> false, sigma - | Some sigma -> true, sigma - in - if b then sigma, true - else + | Some sigma -> ans + | None -> let x = EConstr.Unsafe.to_constr x in let y = EConstr.Unsafe.to_constr y in let sigma' = conv_fun pb ~l2r:false sigma ts env (sigma, sigma_univ_state) x y in - sigma', true + Some sigma' with - | Reduction.NotConvertible -> sigma, false - | Univ.UniverseInconsistency _ when catch_incon -> sigma, false + | Reduction.NotConvertible -> None + | Univ.UniverseInconsistency _ when catch_incon -> None | e when is_anomaly e -> report_anomaly e let infer_conv = infer_conv_gen (fun pb ~l2r sigma -> diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index ad280d9f3..9256fa7ce 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.mli @@ -277,13 +277,13 @@ val check_conv : ?pb:conv_pb -> ?ts:transparent_state -> env -> evar_map -> con otherwise returns false in that case. *) val infer_conv : ?catch_incon:bool -> ?pb:conv_pb -> ?ts:transparent_state -> - env -> evar_map -> constr -> constr -> evar_map * bool + env -> evar_map -> constr -> constr -> evar_map option (** Conversion with inference of universe constraints *) val set_vm_infer_conv : (?pb:conv_pb -> env -> evar_map -> constr -> constr -> - evar_map * bool) -> unit + evar_map option) -> unit val vm_infer_conv : ?pb:conv_pb -> env -> evar_map -> constr -> constr -> - evar_map * bool + evar_map option (** [infer_conv_gen] behaves like [infer_conv] but is parametrized by a @@ -291,7 +291,7 @@ conversion function. Used to pretype vm and native casts. *) val infer_conv_gen : (conv_pb -> l2r:bool -> evar_map -> transparent_state -> (Constr.constr, evar_map) Reduction.generic_conversion_function) -> ?catch_incon:bool -> ?pb:conv_pb -> ?ts:transparent_state -> env -> - evar_map -> constr -> constr -> evar_map * bool + evar_map -> constr -> constr -> evar_map option (** {6 Special-Purpose Reduction Functions } *) diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 62bee5a36..a8a4003dc 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -579,16 +579,16 @@ let constr_cmp pb env sigma flags t u = in match cstrs with | Some cstrs -> - begin try Evd.add_universe_constraints sigma cstrs, true - with Univ.UniverseInconsistency _ -> sigma, false + begin try Some (Evd.add_universe_constraints sigma cstrs) + with Univ.UniverseInconsistency _ -> None | Evd.UniversesDiffer -> if is_rigid_head sigma flags t then - try Evd.add_universe_constraints sigma (force_eqs cstrs), true - with Univ.UniverseInconsistency _ -> sigma, false - else sigma, false + try Some (Evd.add_universe_constraints sigma (force_eqs cstrs)) + with Univ.UniverseInconsistency _ -> None + else None end | None -> - sigma, false + None let do_reduce ts (env, nb) sigma c = Stack.zip sigma (fst (whd_betaiota_deltazeta_for_iota_state @@ -623,9 +623,9 @@ let check_compatibility env pbty flags (sigma,metasubst,evarsubst : subst0) tyM | None -> sigma | Some n -> if is_ground_term sigma m && is_ground_term sigma n then - let sigma, b = infer_conv ~pb:pbty ~ts:flags.modulo_delta_types env sigma m n in - if b then sigma - else error_cannot_unify env sigma (m,n) + match infer_conv ~pb:pbty ~ts:flags.modulo_delta_types env sigma m n with + | Some sigma -> sigma + | None -> error_cannot_unify env sigma (m,n) else sigma @@ -698,7 +698,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e if k2 < k1 then sigma,(k1,cN,stN)::metasubst,evarsubst else sigma,(k2,cM,stM)::metasubst,evarsubst | Meta k, _ - when not (dependent sigma cM cN) (* helps early trying alternatives *) -> + when not (occur_metavariable sigma k cN) (* helps early trying alternatives *) -> let sigma = if opt.with_types && flags.check_applied_meta_types then (try @@ -718,7 +718,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e evarsubst) else error_cannot_unify_local curenv sigma (m,n,cN) | _, Meta k - when not (dependent sigma cN cM) (* helps early trying alternatives *) -> + when not (occur_metavariable sigma k cM) (* helps early trying alternatives *) -> let sigma = if opt.with_types && flags.check_applied_meta_types then (try @@ -740,11 +740,12 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e | Evar (evk,_ as ev), Evar (evk',_) when not (Evar.Set.mem evk flags.frozen_evars) && Evar.equal evk evk' -> - let sigma',b = constr_cmp cv_pb env sigma flags cM cN in - if b then - sigma',metasubst,evarsubst - else + begin match constr_cmp cv_pb env sigma flags cM cN with + | Some sigma -> + sigma, metasubst, evarsubst + | None -> sigma,metasubst,((curenv,ev,cN)::evarsubst) + end | Evar (evk,_ as ev), _ when not (Evar.Set.mem evk flags.frozen_evars) && not (occur_evar sigma evk cN) -> @@ -837,6 +838,26 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e with ex when precatchable_exception ex -> reduce curenvnb pb opt substn cM cN) + | Fix ((ln1,i1),(lna1,tl1,bl1)), Fix ((ln2,i2),(_,tl2,bl2)) when + Int.equal i1 i2 && Array.equal Int.equal ln1 ln2 -> + (try + let opt' = {opt with at_top = true; with_types = false} in + let curenvnb' = Array.fold_right2 (fun na t -> push (na,t)) lna1 tl1 curenvnb in + Array.fold_left2 (unirec_rec curenvnb' CONV opt') + (Array.fold_left2 (unirec_rec curenvnb CONV opt') substn tl1 tl2) bl1 bl2 + with ex when precatchable_exception ex -> + reduce curenvnb pb opt substn cM cN) + + | CoFix (i1,(lna1,tl1,bl1)), CoFix (i2,(_,tl2,bl2)) when + Int.equal i1 i2 -> + (try + let opt' = {opt with at_top = true; with_types = false} in + let curenvnb' = Array.fold_right2 (fun na t -> push (na,t)) lna1 tl1 curenvnb in + Array.fold_left2 (unirec_rec curenvnb' CONV opt') + (Array.fold_left2 (unirec_rec curenvnb CONV opt') substn tl1 tl2) bl1 bl2 + with ex when precatchable_exception ex -> + reduce curenvnb pb opt substn cM cN) + | App (f1,l1), _ when (isMeta sigma f1 && use_metas_pattern_unification sigma flags nb l1 || use_evars_pattern_unification flags && isAllowedEvar sigma flags f1) -> @@ -922,9 +943,9 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e and unify_not_same_head curenvnb pb opt (sigma, metas, evars as substn : subst0) cM cN = try canonical_projections curenvnb pb opt cM cN substn with ex when precatchable_exception ex -> - let sigma', b = constr_cmp cv_pb env sigma flags cM cN in - if b then (sigma', metas, evars) - else + match constr_cmp cv_pb env sigma flags cM cN with + | Some sigma -> (sigma, metas, evars) + | None -> try reduce curenvnb pb opt substn cM cN with ex when precatchable_exception ex -> let (f1,l1) = @@ -981,12 +1002,13 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e (* Renounce, maybe metas/evars prevents typing *) sigma else sigma in - let sigma, b = infer_conv ~pb ~ts:convflags curenv sigma m1 n1 in - if b then Some (sigma, metasubst, evarsubst) - else - if is_ground_term sigma m1 && is_ground_term sigma n1 then - error_cannot_unify curenv sigma (cM,cN) - else None + match infer_conv ~pb ~ts:convflags curenv sigma m1 n1 with + | Some sigma -> + Some (sigma, metasubst, evarsubst) + | None -> + if is_ground_term sigma m1 && is_ground_term sigma n1 then + error_cannot_unify curenv sigma (cM,cN) + else None in match res with | Some substn -> substn @@ -1089,11 +1111,13 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e then None else - let sigma, b = match flags.modulo_conv_on_closed_terms with + let ans = match flags.modulo_conv_on_closed_terms with | Some convflags -> infer_conv ~pb:cv_pb ~ts:convflags env sigma m n | _ -> constr_cmp cv_pb env sigma flags m n in - if b then Some sigma - else if (match flags.modulo_conv_on_closed_terms, flags.modulo_delta with + match ans with + | Some sigma -> ans + | None -> + if (match flags.modulo_conv_on_closed_terms, flags.modulo_delta with | Some (cv_id, cv_k), (dl_id, dl_k) -> Id.Pred.subset dl_id cv_id && Cpred.subset dl_k cv_k | None,(dl_id, dl_k) -> @@ -1391,7 +1415,7 @@ let w_merge env with_types flags (evd,metas,evars : subst0) = and mimick_undefined_evar evd flags hdc nargs sp = let ev = Evd.find_undefined evd sp in - let sp_env = Global.env_of_context ev.evar_hyps in + let sp_env = Global.env_of_context (evar_filtered_hyps ev) in let (evd', c) = applyHead sp_env evd nargs hdc in let (evd'',mc,ec) = unify_0 sp_env evd' CUMUL flags @@ -1500,7 +1524,8 @@ let indirectly_dependent sigma c d decls = it is needed otherwise, as e.g. when abstracting over "2" in "forall H:0=2, H=H:>(0=1+1) -> 0=2." where there is now obvious way to see that the second hypothesis depends indirectly over 2 *) - List.exists (fun d' -> dependent_in_decl sigma (EConstr.mkVar (NamedDecl.get_id d')) d) decls + let open Context.Named.Declaration in + List.exists (fun d' -> exists (fun c -> Termops.local_occur_var sigma (NamedDecl.get_id d') c) d) decls let finish_evar_resolution ?(flags=Pretyping.all_and_fail_flags) env current_sigma (pending,c) = let sigma = Pretyping.solve_remaining_evars flags env current_sigma pending in @@ -1582,8 +1607,10 @@ let make_pattern_test from_prefix_of_ind is_correct_type env sigma (pending,c) = let merge_fun c1 c2 = match c1, c2 with | Some (evd,c1,x), Some (_,c2,_) -> - let (evd,b) = infer_conv ~pb:CONV env evd c1 c2 in - if b then Some (evd, c1, x) else raise (NotUnifiable None) + begin match infer_conv ~pb:CONV env evd c1 c2 with + | Some evd -> Some (evd, c1, x) + | None -> raise (NotUnifiable None) + end | Some _, None -> c1 | None, Some _ -> c2 | None, None -> None in @@ -1900,10 +1927,11 @@ let secondOrderAbstraction env evd flags typ (p, oplist) = let (evd',cllist) = w_unify_to_subterm_list env evd flags p oplist typ in let typp = Typing.meta_type evd' p in let evd',(pred,predtyp) = abstract_list_all env evd' typp typ cllist in - let evd', b = infer_conv ~pb:CUMUL env evd' predtyp typp in - if not b then + match infer_conv ~pb:CUMUL env evd' predtyp typp with + | None -> error_wrong_abstraction_type env evd' (Evd.meta_name evd p) pred typp predtyp; + | Some evd' -> w_merge env false flags.merge_unify_flags (evd',[p,pred,(Conv,TypeProcessed)],[]) diff --git a/proofs/logic.ml b/proofs/logic.ml index 218b2671e..95c30d815 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -309,9 +309,10 @@ let check_meta_variables env sigma c = let check_conv_leq_goal env sigma arg ty conclty = if !check then - let evm, b = Reductionops.infer_conv env sigma (EConstr.of_constr ty) (EConstr.of_constr conclty) in - if b then evm - else raise (RefinerError (env, sigma, BadType (arg,ty,conclty))) + let ans = Reductionops.infer_conv env sigma (EConstr.of_constr ty) (EConstr.of_constr conclty) in + match ans with + | Some evm -> evm + | None -> raise (RefinerError (env, sigma, BadType (arg,ty,conclty))) else sigma exception Stop of EConstr.t list diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 998efdd6d..c105116ff 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -649,17 +649,6 @@ module Search = struct Evd.add sigma gl evi') sigma goals - let fail_if_nonclass info = - Proofview.Goal.enter begin fun gl -> - let sigma = Proofview.Goal.sigma gl in - if is_class_type sigma (Proofview.Goal.concl gl) then - Proofview.tclUNIT () - else (if !typeclasses_debug > 1 then - Feedback.msg_debug (pr_depth info.search_depth ++ - str": failure due to non-class subgoal " ++ - pr_ev sigma (Proofview.Goal.goal gl)); - Proofview.tclZERO NoApplicableEx) end - (** The general hint application tactic. tac1 + tac2 .... The choice of OR or ORELSE is determined depending on the dependencies of the goal and the unique/Prop @@ -798,13 +787,8 @@ module Search = struct in if path_matches derivs [] then aux e tl else - let filter = - if false (* in 8.6, still allow non-class subgoals - info.search_only_classes *) then fail_if_nonclass info - else Proofview.tclUNIT () - in ortac - (with_shelf (tac <*> filter) >>= fun s -> + (with_shelf tac >>= fun s -> let i = !idx in incr idx; result s i None) (fun e' -> if CErrors.noncritical (fst e') then @@ -868,12 +852,9 @@ module Search = struct let search_tac_gl ?st only_classes dep hints depth i sigma gls gl : unit Proofview.tactic = let open Proofview in - if false (* In 8.6, still allow non-class goals only_classes && not (is_class_type sigma (Goal.concl gl)) *) then - Tacticals.New.tclZEROMSG (str"Not a subgoal for a class") - else - let dep = dep || Proofview.unifiable sigma (Goal.goal gl) gls in - let info = make_autogoal ?st only_classes dep (cut_of_hints hints) i gl in - search_tac hints depth 1 info + let dep = dep || Proofview.unifiable sigma (Goal.goal gl) gls in + let info = make_autogoal ?st only_classes dep (cut_of_hints hints) i gl in + search_tac hints depth 1 info let search_tac ?(st=full_transparent_state) only_classes dep hints depth = let open Proofview in diff --git a/tactics/equality.ml b/tactics/equality.ml index f9e06391a..d7e697aed 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -1808,9 +1808,9 @@ let subst_all ?(flags=default_subst_tactic_flags) () = (* J.F.: added to prevent failure on goal containing x=x as an hyp *) if EConstr.eq_constr sigma x y then Proofview.tclUNIT () else match EConstr.kind sigma x, EConstr.kind sigma y with - | Var x', _ when not (dependent sigma x y) && not (is_evaluable env (EvalVarRef x')) -> + | Var x', _ when not (Termops.local_occur_var sigma x' y) && not (is_evaluable env (EvalVarRef x')) -> subst_one flags.rewrite_dependent_proof x' (hyp,y,true) - | _, Var y' when not (dependent sigma y x) && not (is_evaluable env (EvalVarRef y')) -> + | _, Var y' when not (Termops.local_occur_var sigma y' x) && not (is_evaluable env (EvalVarRef y')) -> subst_one flags.rewrite_dependent_proof y' (hyp,x,false) | _ -> Proofview.tclUNIT () diff --git a/tactics/hints.ml b/tactics/hints.ml index a86103d57..d49c8aaa5 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -167,6 +167,7 @@ type hint_mode = type hints_expr = | HintsResolve of (hint_info_expr * bool * reference_or_constr) list + | HintsResolveIFF of bool * reference list * int option | HintsImmediate of reference_or_constr list | HintsUnfold of reference list | HintsTransparency of reference list * bool @@ -672,7 +673,7 @@ struct let add_list env sigma l db = List.fold_left (fun db k -> add_one env sigma k db) db l - let remove_sdl p sdl = List.Smart.filter p sdl + let remove_sdl p sdl = List.filter p sdl let remove_he st p se = let sl1' = remove_sdl p se.sentry_nopat in @@ -684,7 +685,7 @@ struct let filter (_, h) = match h.name with PathHints [gr] -> not (List.mem_f GlobRef.equal gr grs) | _ -> true in let hintmap = Constr_map.map (remove_he db.hintdb_state filter) db.hintdb_map in - let hintnopat = List.Smart.filter (fun (ge, sd) -> filter sd) db.hintdb_nopat in + let hintnopat = List.filter (fun (ge, sd) -> filter sd) db.hintdb_nopat in { db with hintdb_map = hintmap; hintdb_nopat = hintnopat } let remove_one gr db = remove_list [gr] db @@ -1290,6 +1291,35 @@ let prepare_hint check (poly,local) env init (sigma,c) = else (Lib.add_anonymous_leaf (input_context_set diff); IsConstr (c', Univ.ContextSet.empty)) +let project_hint ~poly pri l2r r = + let open EConstr in + let open Coqlib in + let gr = Smartlocate.global_with_alias r in + let env = Global.env() in + let sigma = Evd.from_env env in + let sigma, c = Evd.fresh_global env sigma gr in + let t = Retyping.get_type_of env sigma c in + let t = + Tacred.reduce_to_quantified_ref env sigma (Lazy.force coq_iff_ref) t in + let sign,ccl = decompose_prod_assum sigma t in + let (a,b) = match snd (decompose_app sigma ccl) with + | [a;b] -> (a,b) + | _ -> assert false in + let p = + if l2r then build_coq_iff_left_proj () else build_coq_iff_right_proj () in + let sigma, p = Evd.fresh_global env sigma p in + let c = Reductionops.whd_beta sigma (mkApp (c, Context.Rel.to_extended_vect mkRel 0 sign)) in + let c = it_mkLambda_or_LetIn + (mkApp (p,[|mkArrow a (lift 1 b);mkArrow b (lift 1 a);c|])) sign in + let id = + Nameops.add_suffix (Nametab.basename_of_global gr) ("_proj_" ^ (if l2r then "l2r" else "r2l")) + in + let ctx = Evd.const_univ_entry ~poly sigma in + let c = EConstr.to_constr sigma c in + let c = Declare.declare_definition ~internal:Declare.InternalTacticRequest id (c,ctx) in + let info = {Typeclasses.hint_priority = pri; hint_pattern = None} in + (info,false,true,PathAny, IsGlobRef (Globnames.ConstRef c)) + let interp_hints poly = fun h -> let env = Global.env () in @@ -1319,6 +1349,8 @@ let interp_hints poly = in match h with | HintsResolve lhints -> HintsResolveEntry (List.map fres lhints) + | HintsResolveIFF (l2r, lc, n) -> + HintsResolveEntry (List.map (project_hint ~poly n l2r) lc) | HintsImmediate lhints -> HintsImmediateEntry (List.map fi lhints) | HintsUnfold lhints -> HintsUnfoldEntry (List.map fr lhints) | HintsTransparency (lhints, b) -> @@ -1379,12 +1411,10 @@ let expand_constructor_hints env sigma lems = (* builds a hint database from a constr signature *) (* typically used with (lid, ltyp) = pf_hyps_types <some goal> *) -let add_hint_lemmas env sigma eapply lems hint_db = +let constructor_hints env sigma eapply lems = let lems = expand_constructor_hints env sigma lems in - let hintlist' = - List.map_append (fun (poly, lem) -> - make_resolves env sigma (eapply,true,false) empty_hint_info poly lem) lems in - Hint_db.add_list env sigma hintlist' hint_db + List.map_append (fun (poly, lem) -> + make_resolves env sigma (eapply,true,false) empty_hint_info poly lem) lems let make_local_hint_db env sigma ts eapply lems = let map c = c env sigma in @@ -1395,8 +1425,9 @@ let make_local_hint_db env sigma ts eapply lems = | Some ts -> ts in let hintlist = List.map_append (make_resolve_hyp env sigma) sign in - add_hint_lemmas env sigma eapply lems - (Hint_db.add_list env sigma hintlist (Hint_db.empty ts false)) + Hint_db.empty ts false + |> Hint_db.add_list env sigma hintlist + |> Hint_db.add_list env sigma (constructor_hints env sigma eapply lems) let make_local_hint_db env sigma ?ts eapply lems = make_local_hint_db env sigma ts eapply lems diff --git a/tactics/hints.mli b/tactics/hints.mli index 7ef7f0185..e958f986e 100644 --- a/tactics/hints.mli +++ b/tactics/hints.mli @@ -83,6 +83,7 @@ type hint_mode = type hints_expr = | HintsResolve of (hint_info_expr * bool * reference_or_constr) list + | HintsResolveIFF of bool * Libnames.reference list * int option | HintsImmediate of reference_or_constr list | HintsUnfold of Libnames.reference list | HintsTransparency of Libnames.reference list * bool diff --git a/tactics/inv.ml b/tactics/inv.ml index 28cfd57a2..339abbc2e 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -469,7 +469,7 @@ let raw_inversion inv_kind id status names = make_inv_predicate env evdref indf realargs id status concl in let sigma = !evdref in let (cut_concl,case_tac) = - if status != NoDep && (dependent sigma c concl) then + if status != NoDep && (local_occur_var sigma id concl) then Reductionops.beta_applist sigma (elim_predicate, realargs@[c]), case_then_using else diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 58c62af85..d7888f6ca 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -158,9 +158,9 @@ let convert_concl ?(check=true) ty k = let sigma = if check then begin ignore (Typing.unsafe_type_of env sigma ty); - let sigma,b = Reductionops.infer_conv env sigma ty conclty in - if not b then error "Not convertible."; - sigma + match Reductionops.infer_conv env sigma ty conclty with + | None -> error "Not convertible." + | Some sigma -> sigma end else sigma in let (sigma, x) = Evarutil.new_evar env sigma ~principal:true ~store ty in let ans = if k == DEFAULTcast then x else mkCast(x,k,conclty) in @@ -186,11 +186,10 @@ let convert_hyp_no_check = convert_hyp ~check:false let convert_gen pb x y = Proofview.Goal.enter begin fun gl -> - try - let sigma, b = Tacmach.New.pf_apply (Reductionops.infer_conv ~pb) gl x y in - if b then Proofview.Unsafe.tclEVARS sigma - else Tacticals.New.tclFAIL 0 (str "Not convertible") - with (* Reduction.NotConvertible *) _ -> + match Tacmach.New.pf_apply (Reductionops.infer_conv ~pb) gl x y with + | Some sigma -> Proofview.Unsafe.tclEVARS sigma + | None -> Tacticals.New.tclFAIL 0 (str "Not convertible") + | exception _ -> (** FIXME: Sometimes an anomaly is raised from conversion *) Tacticals.New.tclFAIL 0 (str "Not convertible") end @@ -796,15 +795,15 @@ let check_types env sigma mayneedglobalcheck deep newc origc = let t2 = Retyping.get_type_of env sigma origc in let sigma, t2 = Evarsolve.refresh_universes ~onlyalg:true (Some false) env sigma t2 in - let sigma, b = infer_conv ~pb:Reduction.CUMUL env sigma t1 t2 in - if not b then + match infer_conv ~pb:Reduction.CUMUL env sigma t1 t2 with + | None -> if isSort sigma (whd_all env sigma t1) && isSort sigma (whd_all env sigma t2) then (mayneedglobalcheck := true; sigma) else user_err ~hdr:"convert-check-hyp" (str "Types are incompatible.") - else sigma + | Some sigma -> sigma end else if not (isSort sigma (whd_all env sigma t1)) then @@ -815,9 +814,9 @@ let check_types env sigma mayneedglobalcheck deep newc origc = let change_and_check cv_pb mayneedglobalcheck deep t env sigma c = let (sigma, t') = t sigma in let sigma = check_types env sigma mayneedglobalcheck deep t' c in - let sigma, b = infer_conv ~pb:cv_pb env sigma t' c in - if not b then user_err ~hdr:"convert-check-hyp" (str "Not convertible."); - (sigma, t') + match infer_conv ~pb:cv_pb env sigma t' c with + | None -> user_err ~hdr:"convert-check-hyp" (str "Not convertible."); + | Some sigma -> (sigma, t') (* Use cumulativity only if changing the conclusion not a subterm *) let change_on_subterm cv_pb deep t where env sigma c = @@ -1934,16 +1933,19 @@ let assumption = let t = NamedDecl.get_type decl in let concl = Proofview.Goal.concl gl in let sigma = Tacmach.New.project gl in - let (sigma, is_same_type) = - if only_eq then (sigma, EConstr.eq_constr sigma t concl) + let ans = + if only_eq then + if EConstr.eq_constr sigma t concl then Some sigma + else None else let env = Proofview.Goal.env gl in infer_conv env sigma t concl in - if is_same_type then + match ans with + | Some sigma -> (Proofview.Unsafe.tclEVARS sigma) <*> exact_no_check (mkVar (NamedDecl.get_id decl)) - else arec gl only_eq rest + | None -> arec gl only_eq rest in let assumption_tac gl = let hyps = Proofview.Goal.hyps gl in diff --git a/tactics/term_dnet.mli b/tactics/term_dnet.mli index 2c748f9c9..7bce57789 100644 --- a/tactics/term_dnet.mli +++ b/tactics/term_dnet.mli @@ -26,7 +26,7 @@ open Mod_subst The results returned here are perfect, since post-filtering is done inside here. - See lib/dnet.mli for more details. + See tactics/dnet.mli for more details. *) (** Identifiers to store (right hand side of the association) *) diff --git a/test-suite/bugs/closed/4403.v b/test-suite/bugs/closed/4403.v new file mode 100644 index 000000000..a80f38fe2 --- /dev/null +++ b/test-suite/bugs/closed/4403.v @@ -0,0 +1,3 @@ +(* -*- coq-prog-args: ("-type-in-type"); -*- *) + +Definition some_prop : Prop := Type. diff --git a/test-suite/bugs/closed/4882.v b/test-suite/bugs/closed/4882.v deleted file mode 100644 index 8c26af708..000000000 --- a/test-suite/bugs/closed/4882.v +++ /dev/null @@ -1,50 +0,0 @@ - -Definition Foo {T}{a : T} : T := a. - -Module A. - - Declare Implicit Tactic eauto. - - Goal forall A (x : A), A. - intros. - apply Foo. (* Check defined evars are normalized *) - (* Qed. *) - Abort. - -End A. - -Module B. - - Definition Foo {T}{a : T} : T := a. - - Declare Implicit Tactic eassumption. - - Goal forall A (x : A), A. - intros. - apply Foo. - (* Qed. *) - Abort. - -End B. - -Module C. - - Declare Implicit Tactic first [exact True|assumption]. - - Goal forall (x : True), True. - intros. - apply (@Foo _ _). - Qed. - -End C. - -Module D. - - Declare Implicit Tactic assumption. - - Goal forall A (x : A), A. - intros. - exact _. - Qed. - -End D. diff --git a/test-suite/bugs/closed/5539.v b/test-suite/bugs/closed/5539.v new file mode 100644 index 000000000..48e5568e9 --- /dev/null +++ b/test-suite/bugs/closed/5539.v @@ -0,0 +1,15 @@ +Set Universe Polymorphism. + +Inductive D : nat -> Type := +| DO : D O +| DS n : D n -> D (S n). + +Fixpoint follow (n : nat) : D n -> Prop := + match n with + | O => fun d => let 'DO := d in True + | S n' => fun d => (let 'DS _ d' := d in fun f => f d') (follow n') + end. + +Definition step (n : nat) (d : D n) (H : follow n d) : + follow (S n) (DS n d) + := H. diff --git a/test-suite/bugs/closed/6770.v b/test-suite/bugs/closed/6770.v new file mode 100644 index 000000000..9bcc74083 --- /dev/null +++ b/test-suite/bugs/closed/6770.v @@ -0,0 +1,7 @@ +Section visibility. + + Let Fixpoint by_proof (n:nat) : True. + Proof. exact I. Defined. +End visibility. + +Fail Check by_proof. diff --git a/test-suite/bugs/closed/7011.v b/test-suite/bugs/closed/7011.v new file mode 100644 index 000000000..296e4e11e --- /dev/null +++ b/test-suite/bugs/closed/7011.v @@ -0,0 +1,16 @@ +(* Fix and Cofix were missing in tactic unification *) + +Goal exists e, (fix foo (n : nat) : nat := match n with O => e | S n' => foo n' end) + = (fix foo (n : nat) : nat := match n with O => O | S n' => foo n' end). +Proof. + eexists. + reflexivity. +Qed. + +CoInductive stream := cons : nat -> stream -> stream. + +Goal exists e, (cofix foo := cons e foo) = (cofix foo := cons 0 foo). +Proof. + eexists. + reflexivity. +Qed. diff --git a/test-suite/bugs/closed/7113.v b/test-suite/bugs/closed/7113.v new file mode 100644 index 000000000..976e60f20 --- /dev/null +++ b/test-suite/bugs/closed/7113.v @@ -0,0 +1,10 @@ +Require Import Program.Tactics. +Section visibility. + + (* used to anomaly *) + Program Let Fixpoint ev' (n : nat) : bool := _. + Next Obligation. exact true. Qed. + + Check ev'. +End visibility. +Fail Check ev'. diff --git a/test-suite/bugs/closed/7195.v b/test-suite/bugs/closed/7195.v new file mode 100644 index 000000000..ea97747ac --- /dev/null +++ b/test-suite/bugs/closed/7195.v @@ -0,0 +1,12 @@ +(* A disjoint-names condition was missing when matching names in Ltac + pattern-matching *) + +Goal True. + let x := (eval cbv beta zeta in (fun P => let Q := P in fun P => P + Q)) in + unify x (fun a b => b + a); (* success *) + let x' := lazymatch x with + | (fun (a : ?A) (b : ?B) => ?k) + => constr:(fun (a : A) (b : B) => k) + end in + unify x x'. +Abort. diff --git a/test-suite/bugs/closed/7392.v b/test-suite/bugs/closed/7392.v new file mode 100644 index 000000000..cf465c658 --- /dev/null +++ b/test-suite/bugs/closed/7392.v @@ -0,0 +1,9 @@ +Inductive R : nat -> Prop := ER : forall n, R n -> R (S n). + +Goal (forall (n : nat), R n -> False) -> True -> False. +Proof. +intros H0 H1. +eapply H0. +clear H1. +apply ER. +simpl. diff --git a/test-suite/coqchk/bug_7539.v b/test-suite/coqchk/bug_7539.v new file mode 100644 index 000000000..74ebe9290 --- /dev/null +++ b/test-suite/coqchk/bug_7539.v @@ -0,0 +1,26 @@ +Set Primitive Projections. + +CoInductive Stream : Type := Cons { tl : Stream }. + +Fixpoint Str_nth_tl (n:nat) (s:Stream) : Stream := + match n with + | O => s + | S m => Str_nth_tl m (tl s) + end. + +CoInductive EqSt (s1 s2: Stream) : Prop := eqst { + eqst_tl : EqSt (tl s1) (tl s2); +}. + +Axiom EqSt_reflex : forall (s : Stream), EqSt s s. + +CoFixpoint map (s:Stream) : Stream := Cons (map (tl s)). + +Lemma Str_nth_tl_map : forall n s, EqSt (Str_nth_tl n (map s)) (map (Str_nth_tl n s)). +Proof. +induction n. ++ intros; apply EqSt_reflex. ++ cbn; intros s; apply IHn. +Qed. + +Definition boom : forall s, tl (map s) = map (tl s) := fun s => eq_refl. diff --git a/test-suite/output/Arguments_renaming.out b/test-suite/output/Arguments_renaming.out index e73312c67..c0b04eb53 100644 --- a/test-suite/output/Arguments_renaming.out +++ b/test-suite/output/Arguments_renaming.out @@ -1,6 +1,5 @@ The command has indeed failed with message: -To rename arguments the "rename" flag must be specified. -Argument A renamed to B. +Flag "rename" expected to rename A into B. File "stdin", line 2, characters 0-25: Warning: This command is just asserting the names of arguments of identity. If this is what you want add ': assert' to silence the warning. If you want @@ -113,5 +112,4 @@ Argument z cannot be declared implicit. The command has indeed failed with message: Extra arguments: y. The command has indeed failed with message: -To rename arguments the "rename" flag must be specified. -Argument A renamed to R. +Flag "rename" expected to rename A into R. diff --git a/test-suite/success/Fixpoint.v b/test-suite/success/Fixpoint.v index 5fc703cf0..efb32ef6f 100644 --- a/test-suite/success/Fixpoint.v +++ b/test-suite/success/Fixpoint.v @@ -91,3 +91,33 @@ apply Cons2. exact b. apply (ex1 (S n) (negb b)). Defined. + +Section visibility. + + Let Fixpoint imm (n:nat) : True := I. + + Let Fixpoint by_proof (n:nat) : True. + Proof. exact I. Defined. +End visibility. + +Fail Check imm. +Fail Check by_proof. + +Module Import mod_local. + Fixpoint imm_importable (n:nat) : True := I. + + Local Fixpoint imm_local (n:nat) : True := I. + + Fixpoint by_proof_importable (n:nat) : True. + Proof. exact I. Defined. + + Local Fixpoint by_proof_local (n:nat) : True. + Proof. exact I. Defined. +End mod_local. + +Check imm_importable. +Fail Check imm_local. +Check mod_local.imm_local. +Check by_proof_importable. +Fail Check by_proof_local. +Check mod_local.by_proof_local. diff --git a/test-suite/success/ImplicitTactic.v b/test-suite/success/ImplicitTactic.v deleted file mode 100644 index d8fa3043d..000000000 --- a/test-suite/success/ImplicitTactic.v +++ /dev/null @@ -1,16 +0,0 @@ -(* A Wiedijk-Cruz-Filipe style tactic for solving implicit arguments *) - -(* Declare a term expression with a hole *) -Parameter quo : nat -> forall n:nat, n<>0 -> nat. -Notation "x / y" := (quo x y _) : nat_scope. - -(* Declare the tactic for resolving implicit arguments still - unresolved after type-checking; it must complete the subgoal to - succeed *) -Declare Implicit Tactic assumption. - -Goal forall n d, d<>0 -> { q:nat & { r:nat | d * q + r = n }}. -intros. -(* Here, assumption is used to solve the implicit argument of quo *) -exists (n / d). - diff --git a/theories/Logic/Diaconescu.v b/theories/Logic/Diaconescu.v index 3317766c9..66e82ddbf 100644 --- a/theories/Logic/Diaconescu.v +++ b/theories/Logic/Diaconescu.v @@ -234,8 +234,6 @@ Qed. (** An alternative more concise proof can be done by directly using the guarded relational choice *) -Declare Implicit Tactic auto. - Lemma proof_irrel_rel_choice_imp_eq_dec' : a1=a2 \/ ~a1=a2. Proof. assert (decide: forall x:A, x=a1 \/ x=a2 -> diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml index ea731b34c..b5b8697d2 100644 --- a/vernac/comFixpoint.ml +++ b/vernac/comFixpoint.ml @@ -254,7 +254,7 @@ let declare_fixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) ind Some (List.map (Option.cata (EConstr.of_constr %> Tactics.exact_no_check) Tacticals.New.tclIDTAC) fixdefs) in let evd = Evd.from_ctx ctx in - Lemmas.start_proof_with_initialization (Global,poly,DefinitionBody Fixpoint) + Lemmas.start_proof_with_initialization (local,poly,DefinitionBody Fixpoint) evd pl (Some(false,indexes,init_tac)) thms None (Lemmas.mk_hook (fun _ _ -> ())) else begin (* We shortcut the proof process *) diff --git a/vernac/g_proofs.ml4 b/vernac/g_proofs.ml4 index 56229c765..a3806ff68 100644 --- a/vernac/g_proofs.ml4 +++ b/vernac/g_proofs.ml4 @@ -98,15 +98,8 @@ GEXTEND Gram VernacCreateHintDb (id, b) | IDENT "Remove"; IDENT "Hints"; ids = LIST1 global; dbnames = opt_hintbases -> VernacRemoveHints (dbnames, ids) - | IDENT "Hint"; h = hint; - dbnames = opt_hintbases -> + | IDENT "Hint"; h = hint; dbnames = opt_hintbases -> VernacHints (dbnames, h) - (* Declare "Resolve" explicitly so as to be able to later extend with - "Resolve ->" and "Resolve <-" *) - | IDENT "Hint"; IDENT "Resolve"; lc = LIST1 reference_or_constr; - info = hint_info; dbnames = opt_hintbases -> - VernacHints (dbnames, - HintsResolve (List.map (fun x -> (info, true, x)) lc)) ] ]; reference_or_constr: [ [ r = global -> HintsReference r @@ -115,6 +108,10 @@ GEXTEND Gram hint: [ [ IDENT "Resolve"; lc = LIST1 reference_or_constr; info = hint_info -> HintsResolve (List.map (fun x -> (info, true, x)) lc) + | IDENT "Resolve"; "->"; lc = LIST1 global; n = OPT natural -> + HintsResolveIFF (true, lc, n) + | IDENT "Resolve"; "<-"; lc = LIST1 global; n = OPT natural -> + HintsResolveIFF (false, lc, n) | IDENT "Immediate"; lc = LIST1 reference_or_constr -> HintsImmediate lc | IDENT "Transparent"; lc = LIST1 global -> HintsTransparency (lc, true) | IDENT "Opaque"; lc = LIST1 global -> HintsTransparency (lc, false) diff --git a/vernac/g_vernac.ml4 b/vernac/g_vernac.ml4 index dd8149d0a..b6523981c 100644 --- a/vernac/g_vernac.ml4 +++ b/vernac/g_vernac.ml4 @@ -631,8 +631,8 @@ GEXTEND Gram t = class_rawexpr -> VernacCoercion (CAst.make ~loc:!@loc @@ ByNotation ntn, s, t) - | IDENT "Context"; c = binders -> - VernacContext c + | IDENT "Context"; c = LIST1 binder -> + VernacContext (List.flatten c) | IDENT "Instance"; namesup = instance_name; ":"; expl = [ "!" -> Decl_kinds.Implicit | -> Decl_kinds.Explicit ] ; t = operconstr LEVEL "200"; diff --git a/vernac/obligations.ml b/vernac/obligations.ml index 1a3b1f39b..00f1760c2 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -565,9 +565,8 @@ let declare_mutual_definition l = List.iter (Metasyntax.add_notation_interpretation (Global.env())) first.prg_notations; Declare.recursive_message (fixkind != IsCoFixpoint) indexes fixnames; let gr = List.hd kns in - let kn = match gr with GlobRef.ConstRef kn -> kn | _ -> assert false in Lemmas.call_hook fix_exn first.prg_hook local gr first.prg_ctx; - List.iter progmap_remove l; kn + List.iter progmap_remove l; gr let decompose_lam_prod c ty = let open Context.Rel.Declaration in @@ -774,8 +773,8 @@ let update_obls prg obls rem = let progs = List.map (fun x -> get_info (ProgMap.find x !from_prg)) prg'.prg_deps in if List.for_all (fun x -> obligations_solved x) progs then let kn = declare_mutual_definition progs in - Defined (GlobRef.ConstRef kn) - else Dependent) + Defined kn + else Dependent) let is_defined obls x = not (Option.is_empty obls.(x).obl_body) @@ -962,7 +961,7 @@ and obligation (user_num, name, typ) tac = let num = pred user_num in let prg = get_prog_err name in let obls, rem = prg.prg_obligations in - if num < Array.length obls then + if num >= 0 && num < Array.length obls then let obl = obls.(num) in match obl.obl_body with None -> solve_obligation prg num tac diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml index 7aff758e9..5490b9ce5 100644 --- a/vernac/ppvernac.ml +++ b/vernac/ppvernac.ml @@ -200,6 +200,9 @@ open Pputils keyword "Resolve " ++ prlist_with_sep sep (fun (info, _, c) -> pr_reference_or_constr pr_c c ++ pr_hint_info pr_pat info) l + | HintsResolveIFF (l2r, l, n) -> + keyword "Resolve " ++ str (if l2r then "->" else "<-") + ++ prlist_with_sep sep pr_reference l | HintsImmediate l -> keyword "Immediate" ++ spc() ++ prlist_with_sep sep (fun c -> pr_reference_or_constr pr_c c) l diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 9a7f59085..7f6270df1 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -1131,15 +1131,16 @@ let vernac_arguments ~atts reference args more_implicits nargs_for_red flags = let names = rename prev_names names in let renaming_specified = Option.has_some !example_renaming in - if !rename_flag_required && not rename_flag then - user_err ~hdr:"vernac_declare_arguments" - (strbrk "To rename arguments the \"rename\" flag must be specified." - ++ spc () ++ - match !example_renaming with - | None -> mt () - | Some (o,n) -> - str "Argument " ++ Name.print o ++ - str " renamed to " ++ Name.print n ++ str "."); + if !rename_flag_required && not rename_flag then begin + let msg = + match !example_renaming with + | None -> + strbrk "To rename arguments the \"rename\" flag must be specified." + | Some (o,n) -> + strbrk "Flag \"rename\" expected to rename " ++ Name.print o ++ + strbrk " into " ++ Name.print n ++ str "." + in user_err ~hdr:"vernac_declare_arguments" msg + end; let duplicate_names = List.duplicates Name.equal (List.filter ((!=) Anonymous) names) diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml index 74355e1a7..9e8dfc4f8 100644 --- a/vernac/vernacexpr.ml +++ b/vernac/vernacexpr.ml @@ -106,13 +106,13 @@ type comment = type reference_or_constr = Hints.reference_or_constr = | HintsReference of reference | HintsConstr of constr_expr -[@@ocaml.deprecated "Please use [Hints.hints_expr]"] +[@@ocaml.deprecated "Please use [Hints.reference_or_constr]"] type hint_mode = Hints.hint_mode = | ModeInput (* No evars *) | ModeNoHeadEvar (* No evar at the head *) | ModeOutput (* Anything *) -[@@ocaml.deprecated "Please use [Hints.hints_expr]"] +[@@ocaml.deprecated "Please use [Hints.hint_mode]"] type 'a hint_info_gen = 'a Typeclasses.hint_info_gen = { hint_priority : int option; @@ -124,6 +124,7 @@ type hint_info_expr = Hints.hint_info_expr type hints_expr = Hints.hints_expr = | HintsResolve of (Hints.hint_info_expr * bool * Hints.reference_or_constr) list + | HintsResolveIFF of bool * reference list * int option | HintsImmediate of Hints.reference_or_constr list | HintsUnfold of reference list | HintsTransparency of reference list * bool |