diff options
68 files changed, 1365 insertions, 962 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). diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 05d2c635a..a6eed661e 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -342,6 +342,9 @@ ci-mtac2: ci-pidetop: <<: *ci-template +ci-quickchick: + <<: *ci-template-flambda + ci-sf: <<: *ci-template diff --git a/Makefile.ci b/Makefile.ci index ce725d19d..7f63157fa 100644 --- a/Makefile.ci +++ b/Makefile.ci @@ -17,6 +17,7 @@ CI_TARGETS=ci-bignums \ ci-cpdt \ ci-cross-crypto \ ci-elpi \ + ci-ext-lib \ ci-equations \ ci-fcsl-pcm \ ci-fiat-crypto \ @@ -31,6 +32,7 @@ CI_TARGETS=ci-bignums \ ci-math-comp \ ci-mtac2 \ ci-pidetop \ + ci-quickchick \ ci-sf \ ci-tlc \ ci-unimath \ @@ -50,6 +52,8 @@ ci-math-classes: ci-bignums ci-corn: ci-math-classes +ci-quickchick: ci-ext-lib + ci-formal-topology: ci-corn # Generic rule, we use make to ease travis integration with mixed rules diff --git a/checker/cic.mli b/checker/cic.mli index c4b00d0dc..27e2a479f 100644 --- a/checker/cic.mli +++ b/checker/cic.mli @@ -241,7 +241,7 @@ type constant_body = { const_type : constr; const_body_code : to_patch_substituted; const_universes : constant_universes; - const_proj : projection_body option; + const_proj : bool; const_inline_code : bool; const_typing_flags : typing_flags; } 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/checker/environ.ml b/checker/environ.ml index bbd043c8e..809150cea 100644 --- a/checker/environ.ml +++ b/checker/environ.ml @@ -7,6 +7,7 @@ open Declarations type globals = { env_constants : constant_body Cmap_env.t; + env_projections : projection_body Cmap_env.t; env_inductives : mutual_inductive_body Mindmap_env.t; env_inductives_eq : KerName.t KNmap.t; env_modules : module_body MPmap.t; @@ -34,6 +35,7 @@ let empty_oracle = { let empty_env = { env_globals = { env_constants = Cmap_env.empty; + env_projections = Cmap_env.empty; env_inductives = Mindmap_env.empty; env_inductives_eq = KNmap.empty; env_modules = MPmap.empty; @@ -165,12 +167,10 @@ let evaluable_constant cst env = with Not_found | NotEvaluableConst _ -> false let is_projection cst env = - not (Option.is_empty (lookup_constant cst env).const_proj) + (lookup_constant cst env).const_proj let lookup_projection p env = - match (lookup_constant (Projection.constant p) env).const_proj with - | Some pb -> pb - | None -> anomaly ("lookup_projection: constant is not a projection.") + Cmap_env.find (Projection.constant p) env.env_globals.env_projections (* Mutual Inductives *) let scrape_mind env kn= @@ -194,6 +194,13 @@ let add_mind kn mib env = Printf.ksprintf anomaly ("Inductive %s is already defined.") (MutInd.to_string kn); let new_inds = Mindmap_env.add kn mib env.env_globals.env_inductives in + let new_projections = match mib.mind_record with + | None | Some None -> env.env_globals.env_projections + | Some (Some (id, kns, pbs)) -> + Array.fold_left2 (fun projs kn pb -> + Cmap_env.add kn pb projs) + env.env_globals.env_projections kns pbs + in let kn1,kn2 = MutInd.user kn, MutInd.canonical kn in let new_inds_eq = if KerName.equal kn1 kn2 then env.env_globals.env_inductives_eq @@ -201,8 +208,9 @@ let add_mind kn mib env = KNmap.add kn1 kn2 env.env_globals.env_inductives_eq in let new_globals = { env.env_globals with - env_inductives = new_inds; - env_inductives_eq = new_inds_eq} in + env_inductives = new_inds; + env_projections = new_projections; + env_inductives_eq = new_inds_eq} in { env with env_globals = new_globals } diff --git a/checker/environ.mli b/checker/environ.mli index 81da83875..4a7597249 100644 --- a/checker/environ.mli +++ b/checker/environ.mli @@ -5,6 +5,7 @@ open Cic type globals = { env_constants : constant_body Cmap_env.t; + env_projections : projection_body Cmap_env.t; env_inductives : mutual_inductive_body Mindmap_env.t; env_inductives_eq : KerName.t KNmap.t; env_modules : module_body MPmap.t; diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml index 7685863ea..ca9581167 100644 --- a/checker/mod_checking.ml +++ b/checker/mod_checking.ml @@ -47,13 +47,8 @@ let check_constant_declaration env kn cb = let () = match body_of_constant cb with | Some bd -> - (match cb.const_proj with - | None -> let j = infer envty bd in - conv_leq envty j ty - | Some pb -> - let env' = add_constant kn cb env' in - let j = infer env' bd in - conv_leq envty j ty) + let j = infer envty bd in + conv_leq envty j ty | None -> () in let env = diff --git a/checker/values.ml b/checker/values.ml index 1ac8d7cef..f7ab95fe2 100644 --- a/checker/values.ml +++ b/checker/values.ml @@ -15,7 +15,7 @@ To ensure this file is up-to-date, 'make' now compares the md5 of cic.mli with a copy we maintain here: -MD5 c4fdf8a846aed45c27b5acb1add7d1c6 checker/cic.mli +MD5 92de14d7bf9134532e8a0cff5618bd50 checker/cic.mli *) @@ -240,7 +240,7 @@ let v_cb = v_tuple "constant_body" v_constr; Any; v_const_univs; - Opt v_projbody; + v_bool; v_bool; v_typing_flags|] 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/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh index 5c882ee85..87d837b38 100755 --- a/dev/ci/ci-basic-overlay.sh +++ b/dev/ci/ci-basic-overlay.sh @@ -170,3 +170,15 @@ ######################################################################## : "${pidetop_CI_BRANCH:=v8.9}" : "${pidetop_CI_GITURL:=https://bitbucket.org/coqpide/pidetop.git}" + +######################################################################## +# ext-lib +######################################################################## +: "${ext_lib_CI_BRANCH:=master}" +: "${ext_lib_CI_GITURL:=https://github.com/coq-ext-lib/coq-ext-lib.git}" + +######################################################################## +# quickchick +######################################################################## +: "${quickchick_CI_BRANCH:=master}" +: "${quickchick_CI_GITURL:=https://github.com/QuickChick/QuickChick.git}" diff --git a/dev/ci/ci-common.sh b/dev/ci/ci-common.sh index f867fd189..5b5cbd11a 100644 --- a/dev/ci/ci-common.sh +++ b/dev/ci/ci-common.sh @@ -8,6 +8,7 @@ export NJOBS if [ -n "${GITLAB_CI}" ]; then + export OCAMLPATH="$PWD/_install_ci/lib:$OCAMLPATH" export COQBIN="$PWD/_install_ci/bin" export CI_BRANCH="$CI_COMMIT_REF_NAME" if [[ ${CI_BRANCH#pr-} =~ ^[0-9]*$ ]] @@ -27,6 +28,7 @@ else CI_BRANCH="$(git rev-parse --abbrev-ref HEAD)" export CI_BRANCH fi + export OCAMLPATH="$PWD:$OCAMLPATH" export COQBIN="$PWD/bin" fi export PATH="$COQBIN:$PATH" diff --git a/dev/ci/ci-ext-lib.sh b/dev/ci/ci-ext-lib.sh new file mode 100755 index 000000000..cf212c2fb --- /dev/null +++ b/dev/ci/ci-ext-lib.sh @@ -0,0 +1,16 @@ +#!/usr/bin/env bash + +ci_dir="$(dirname "$0")" + +# This script could be included inside other ones +# Let's avoid to source ci-common twice in this case +if [ -z "${CI_BUILD_DIR}" ]; +then + . "${ci_dir}/ci-common.sh" +fi + +ext_lib_CI_DIR="${CI_BUILD_DIR}/ExtLib" + +git_checkout "${ext_lib_CI_BRANCH}" "${ext_lib_CI_GITURL}" "${ext_lib_CI_DIR}" + +( cd "${ext_lib_CI_DIR}" && make && make install) diff --git a/dev/ci/ci-pidetop.sh b/dev/ci/ci-pidetop.sh index 2ac4d2167..32cba0808 100755 --- a/dev/ci/ci-pidetop.sh +++ b/dev/ci/ci-pidetop.sh @@ -12,13 +12,11 @@ git_checkout "${pidetop_CI_BRANCH}" "${pidetop_CI_GITURL}" "${pidetop_CI_DIR}" # `-local`. We need to improve this divergence but if we use Dune this # "local" oddity goes away automatically so not bothering... if [ -d "$COQBIN/../lib/coq" ]; then - COQOCAMLLIB="$COQBIN/../lib/" COQLIB="$COQBIN/../lib/coq/" else - COQOCAMLLIB="$COQBIN/../" COQLIB="$COQBIN/../" fi -( cd "${pidetop_CI_DIR}" && OCAMLPATH="$COQOCAMLLIB" jbuilder build @install ) +( cd "${pidetop_CI_DIR}" && jbuilder build @install ) echo -en '4\nexit' | "$pidetop_CI_DIR/_build/install/default/bin/pidetop" -coqlib "$COQLIB" -main-channel stdfds diff --git a/dev/ci/ci-quickchick.sh b/dev/ci/ci-quickchick.sh new file mode 100755 index 000000000..fc39e2685 --- /dev/null +++ b/dev/ci/ci-quickchick.sh @@ -0,0 +1,18 @@ +#!/usr/bin/env bash + +ci_dir="$(dirname "$0")" + +# This script could be included inside other ones +# Let's avoid to source ci-common twice in this case +if [ -z "${CI_BUILD_DIR}" ]; +then + . "${ci_dir}/ci-common.sh" +fi + +quickchick_CI_DIR="${CI_BUILD_DIR}/Quickchick" + +install_ssreflect + +git_checkout "${quickchick_CI_BRANCH}" "${quickchick_CI_GITURL}" "${quickchick_CI_DIR}" + +( cd "${quickchick_CI_DIR}" && make && make install) diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index da4c3f9d7..29e0b34bc 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))`. 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/interp/constrintern.ml b/interp/constrintern.ml index 45c0e9c42..848180743 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -999,7 +999,7 @@ let intern_qualid qid intern env ntnvars us args = match intern_extended_global_of_qualid qid with | TrueGlobal ref -> (DAst.make ?loc @@ GRef (ref, us)), true, args | SynDef sp -> - let (ids,c) = Syntax_def.search_syntactic_definition sp in + let (ids,c) = Syntax_def.search_syntactic_definition ?loc sp in let nids = List.length ids in if List.length args < nids then error_not_enough_arguments ?loc; let args1,args2 = List.chop nids args in @@ -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/interp/syntax_def.ml b/interp/syntax_def.ml index 47faa5885..a4f20fd73 100644 --- a/interp/syntax_def.ml +++ b/interp/syntax_def.ml @@ -96,13 +96,13 @@ let warn_compatibility_notation = CWarnings.(create ~name:"compatibility-notation" ~category:"deprecated" ~default:Enabled pr_compat_warning) -let verbose_compat kn def = function +let verbose_compat ?loc kn def = function | Some v when Flags.version_strictly_greater v -> - warn_compatibility_notation (kn, def, v) + warn_compatibility_notation ?loc (kn, def, v) | _ -> () -let search_syntactic_definition kn = +let search_syntactic_definition ?loc kn = let pat,v = KNmap.find kn !syntax_table in let def = out_pat pat in - verbose_compat kn def v; + verbose_compat ?loc kn def v; def diff --git a/interp/syntax_def.mli b/interp/syntax_def.mli index 1933b8a9a..c5b6655ff 100644 --- a/interp/syntax_def.mli +++ b/interp/syntax_def.mli @@ -18,4 +18,4 @@ type syndef_interpretation = (Id.t * subscopes) list * notation_constr val declare_syntactic_definition : bool -> Id.t -> Flags.compat_version option -> syndef_interpretation -> unit -val search_syntactic_definition : KerName.t -> syndef_interpretation +val search_syntactic_definition : ?loc:Loc.t -> KerName.t -> syndef_interpretation 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/clambda.ml b/kernel/clambda.ml index 8389dd326..b722e4200 100644 --- a/kernel/clambda.ml +++ b/kernel/clambda.ml @@ -708,12 +708,10 @@ let rec lambda_of_constr env c = Lcofix(init, (names, ltypes, lbodies)) | Proj (p,c) -> - let kn = Projection.constant p in - let cb = lookup_constant kn env.global_env in - let pb = Option.get cb.const_proj in + let pb = lookup_projection p env.global_env in let n = pb.proj_arg in let lc = lambda_of_constr env c in - Lproj (n,kn,lc) + Lproj (n,Projection.constant p,lc) and lambda_of_app env f args = match Constr.kind f with diff --git a/kernel/cooking.ml b/kernel/cooking.ml index 6f4541e95..5783453e6 100644 --- a/kernel/cooking.ml +++ b/kernel/cooking.ml @@ -156,7 +156,7 @@ type inline = bool type result = { cook_body : constant_def; cook_type : types; - cook_proj : projection_body option; + cook_proj : bool; cook_universes : constant_universes; cook_inline : inline; cook_context : Context.Named.t option; @@ -227,28 +227,10 @@ let cook_constant ~hcons env { from = cb; info } = hyps) hyps ~init:cb.const_hyps in let typ = abstract_constant_type (expmod cb.const_type) hyps in - let projection pb = - let c' = abstract_constant_body (expmod pb.proj_body) hyps in - let etab = abstract_constant_body (expmod (fst pb.proj_eta)) hyps in - let etat = abstract_constant_body (expmod (snd pb.proj_eta)) hyps in - let ((mind, _), _), n' = - try - let c' = share_univs cache (IndRef (pb.proj_ind,0)) Univ.Instance.empty modlist in - match kind c' with - | App (f,l) -> (destInd f, Array.length l) - | Ind ind -> ind, 0 - | _ -> assert false - with Not_found -> (((pb.proj_ind,0),Univ.Instance.empty), 0) - in - let ctx, ty' = decompose_prod_n (n' + pb.proj_npars + 1) typ in - { proj_ind = mind; proj_npars = pb.proj_npars + n'; proj_arg = pb.proj_arg; - proj_eta = etab, etat; - proj_type = ty'; proj_body = c' } - in { cook_body = body; cook_type = typ; - cook_proj = Option.map projection cb.const_proj; + cook_proj = cb.const_proj; cook_universes = univs; cook_inline = cb.const_inline_code; cook_context = Some const_hyps; diff --git a/kernel/cooking.mli b/kernel/cooking.mli index 7bd0ae566..0d907f3de 100644 --- a/kernel/cooking.mli +++ b/kernel/cooking.mli @@ -21,7 +21,7 @@ type inline = bool type result = { cook_body : constant_def; cook_type : types; - cook_proj : projection_body option; + cook_proj : bool; cook_universes : constant_universes; cook_inline : inline; cook_context : Context.Named.t option; diff --git a/kernel/declarations.ml b/kernel/declarations.ml index b7427d20a..913c13173 100644 --- a/kernel/declarations.ml +++ b/kernel/declarations.ml @@ -87,7 +87,7 @@ type constant_body = { const_type : types; const_body_code : Cemitcodes.to_patch_substituted option; const_universes : constant_universes; - const_proj : projection_body option; + const_proj : bool; const_inline_code : bool; const_typing_flags : typing_flags; (** The typing options which were used for diff --git a/kernel/declareops.ml b/kernel/declareops.ml index 832d478b3..75c0e5b4c 100644 --- a/kernel/declareops.ml +++ b/kernel/declareops.ml @@ -94,14 +94,13 @@ let subst_const_body sub cb = else let body' = subst_const_def sub cb.const_body in let type' = subst_const_type sub cb.const_type in - let proj' = Option.Smart.map (subst_const_proj sub) cb.const_proj in if body' == cb.const_body && type' == cb.const_type - && proj' == cb.const_proj then cb + then cb else { const_hyps = []; const_body = body'; const_type = type'; - const_proj = proj'; + const_proj = cb.const_proj; const_body_code = Option.map (Cemitcodes.subst_to_patch_subst sub) cb.const_body_code; const_universes = cb.const_universes; diff --git a/kernel/environ.ml b/kernel/environ.ml index c3e7cec75..fb89576dd 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -52,6 +52,7 @@ type mind_key = mutual_inductive_body * link_info ref type globals = { env_constants : constant_key Cmap_env.t; + env_projections : projection_body Cmap_env.t; env_inductives : mind_key Mindmap_env.t; env_modules : module_body MPmap.t; env_modtypes : module_type_body MPmap.t} @@ -108,6 +109,7 @@ let empty_rel_context_val = { let empty_env = { env_globals = { env_constants = Cmap_env.empty; + env_projections = Cmap_env.empty; env_inductives = Mindmap_env.empty; env_modules = MPmap.empty; env_modtypes = MPmap.empty}; @@ -485,14 +487,10 @@ let type_in_type_constant cst env = not (lookup_constant cst env).const_typing_flags.check_universes let lookup_projection cst env = - match (lookup_constant (Projection.constant cst) env).const_proj with - | Some pb -> pb - | None -> anomaly (Pp.str "lookup_projection: constant is not a projection.") + Cmap_env.find (Projection.constant cst) env.env_globals.env_projections let is_projection cst env = - match (lookup_constant cst env).const_proj with - | Some _ -> true - | None -> false + (lookup_constant cst env).const_proj (* Mutual Inductives *) let polymorphic_ind (mind,i) env = @@ -514,11 +512,18 @@ let template_polymorphic_pind (ind,u) env = if not (Univ.Instance.is_empty u) then false else template_polymorphic_ind ind env -let add_mind_key kn mind_key env = +let add_mind_key kn (mind, _ as mind_key) env = let new_inds = Mindmap_env.add kn mind_key env.env_globals.env_inductives in + let new_projections = match mind.mind_record with + | None | Some None -> env.env_globals.env_projections + | Some (Some (id, kns, pbs)) -> + Array.fold_left2 (fun projs kn pb -> + Cmap_env.add kn pb projs) + env.env_globals.env_projections kns pbs + in let new_globals = { env.env_globals with - env_inductives = new_inds } in + env_inductives = new_inds; env_projections = new_projections; } in { env with env_globals = new_globals } let add_mind kn mib env = diff --git a/kernel/environ.mli b/kernel/environ.mli index fc45ce0e3..8928b32f1 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -48,6 +48,7 @@ type mind_key = mutual_inductive_body * link_info ref type globals = { env_constants : constant_key Cmap_env.t; + env_projections : projection_body Cmap_env.t; env_inductives : mind_key Mindmap_env.t; env_modules : module_body MPmap.t; env_modtypes : module_type_body MPmap.t diff --git a/kernel/inductive.ml b/kernel/inductive.ml index 9bed598bb..090acdf16 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -803,9 +803,7 @@ let rec subterm_specif renv stack t = (* We take the subterm specs of the constructor of the record *) let wf_args = (dest_subterms wf).(0) in (* We extract the tree of the projected argument *) - let kn = Projection.constant p in - let cb = lookup_constant kn renv.env in - let pb = Option.get cb.const_proj in + let pb = lookup_projection p renv.env in let n = pb.proj_arg in spec_of_tree (List.nth wf_args n) | Dead_code -> Dead_code diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml index 0cd0ad46c..036cd4847 100644 --- a/kernel/nativecode.ml +++ b/kernel/nativecode.ml @@ -1859,7 +1859,7 @@ and compile_named env sigma univ auxdefs id = let compile_constant env sigma prefix ~interactive con cb = match cb.const_proj with - | None -> + | false -> let no_univs = match cb.const_universes with | Monomorphic_const _ -> true @@ -1903,7 +1903,8 @@ let compile_constant env sigma prefix ~interactive con cb = if interactive then LinkedInteractive prefix else Linked prefix end - | Some pb -> + | true -> + let pb = lookup_projection (Projection.make con false) env in let mind = pb.proj_ind in let ind = (mind,0) in let mib = lookup_mind mind env in @@ -2029,11 +2030,12 @@ let rec compile_deps env sigma prefix ~interactive init t = else let comp_stack, (mind_updates, const_updates) = match cb.const_proj, cb.const_body with - | None, Def t -> + | false, Def t -> compile_deps env sigma prefix ~interactive init (Mod_subst.force_constr t) - | Some pb, _ -> - let mind = pb.proj_ind in - compile_mind_deps env prefix ~interactive init mind + | true, _ -> + let pb = lookup_projection (Projection.make c false) env in + let mind = pb.proj_ind in + compile_mind_deps env prefix ~interactive init mind | _ -> init in let code, name = 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/term_typing.ml b/kernel/term_typing.ml index 7352c1882..db1109e75 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -250,7 +250,7 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) = { Cooking.cook_body = Undef nl; cook_type = t; - cook_proj = None; + cook_proj = false; cook_universes = univs; cook_inline = false; cook_context = ctx; @@ -291,7 +291,7 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) = { Cooking.cook_body = def; cook_type = typ; - cook_proj = None; + cook_proj = false; cook_universes = Monomorphic_const univs; cook_inline = c.const_entry_inline_code; cook_context = c.const_entry_secctx; @@ -343,7 +343,7 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) = { Cooking.cook_body = def; cook_type = typ; - cook_proj = None; + cook_proj = false; cook_universes = univs; cook_inline = c.const_entry_inline_code; cook_context = c.const_entry_secctx; @@ -370,7 +370,7 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) = { Cooking.cook_body = Def (Mod_subst.from_val (Constr.hcons term)); cook_type = typ; - cook_proj = Some pb; + cook_proj = true; cook_universes = univs; cook_inline = false; cook_context = None; @@ -458,30 +458,8 @@ let build_constant_declaration kn env result = check declared inferred) lc) in let univs = result.cook_universes in let tps = - let res = - match result.cook_proj with - | None -> Cbytegen.compile_constant_body ~fail_on_error:false env univs def - | Some pb -> - (* The compilation of primitive projections is a bit tricky, because - they refer to themselves (the body of p looks like fun c => - Proj(p,c)). We break the cycle by building an ad-hoc compilation - environment. A cleaner solution would be that kernel projections are - simply Proj(i,c) with i an int and c a constr, but we would have to - get rid of the compatibility layer. *) - let cb = - { const_hyps = hyps; - const_body = def; - const_type = typ; - const_proj = result.cook_proj; - const_body_code = None; - const_universes = univs; - const_inline_code = result.cook_inline; - const_typing_flags = Environ.typing_flags env; - } - in - let env = add_constant kn cb env in - Cbytegen.compile_constant_body ~fail_on_error:false env univs def - in Option.map Cemitcodes.from_val res + let res = Cbytegen.compile_constant_body ~fail_on_error:false env univs def in + Option.map Cemitcodes.from_val res in { const_hyps = hyps; const_body = def; diff --git a/kernel/typeops.ml b/kernel/typeops.ml index fd9cefb2c..325d5cecd 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -528,13 +528,3 @@ let judge_of_case env ci pj cj lfj = let lf, lft = dest_judgev lfj in make_judge (mkCase (ci, (*nf_betaiota*) pj.uj_val, cj.uj_val, lft)) (type_of_case env ci pj.uj_val pj.uj_type cj.uj_val cj.uj_type lf lft) - -let type_of_projection_constant env (p,u) = - let cst = Projection.constant p in - let cb = lookup_constant cst env in - match cb.const_proj with - | Some pb -> - if Declareops.constant_is_polymorphic cb then - Vars.subst_instance_constr u pb.proj_type - else pb.proj_type - | None -> raise (Invalid_argument "type_of_projection: not a projection") diff --git a/kernel/typeops.mli b/kernel/typeops.mli index 85b2cfffd..546f2d2b4 100644 --- a/kernel/typeops.mli +++ b/kernel/typeops.mli @@ -100,8 +100,6 @@ val judge_of_case : env -> case_info -> unsafe_judgment -> unsafe_judgment -> unsafe_judgment array -> unsafe_judgment -val type_of_projection_constant : env -> Projection.t puniverses -> types - val type_of_constant_in : env -> pconstant -> types (** Check that hyps are included in env and fails with error otherwise *) diff --git a/library/heads.ml b/library/heads.ml index 198672a0a..3d5f6a6ff 100644 --- a/library/heads.ml +++ b/library/heads.ml @@ -129,7 +129,7 @@ let compute_head = function let cb = Environ.lookup_constant cst env in let is_Def = function Declarations.Def _ -> true | _ -> false in let body = - if cb.Declarations.const_proj = None && is_Def cb.Declarations.const_body + if not cb.Declarations.const_proj && is_Def cb.Declarations.const_body then Global.body_of_constant cst else None in (match body with diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index cdd698304..5aee70194 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -1066,8 +1066,10 @@ let extract_constant env kn cb = | Undef _ -> warn_info (); mk_typ_ax () | Def c -> (match cb.const_proj with - | None -> mk_typ (get_body c) - | Some pb -> mk_typ (EConstr.of_constr pb.proj_body)) + | false -> mk_typ (get_body c) + | true -> + let pb = lookup_projection (Projection.make kn false) env in + mk_typ (EConstr.of_constr pb.proj_body)) | OpaqueDef c -> add_opaque r; if access_opaque () then mk_typ (get_opaque env c) @@ -1077,8 +1079,10 @@ let extract_constant env kn cb = | Undef _ -> warn_info (); mk_ax () | Def c -> (match cb.const_proj with - | None -> mk_def (get_body c) - | Some pb -> mk_def (EConstr.of_constr pb.proj_body)) + | false -> mk_def (get_body c) + | true -> + let pb = lookup_projection (Projection.make kn false) env in + mk_def (EConstr.of_constr pb.proj_body)) | OpaqueDef c -> add_opaque r; if access_opaque () then mk_def (get_opaque env c) 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..8813c7764 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 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/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/inductiveops.ml b/pretyping/inductiveops.ml index 8e3c33ff7..b1ab2d2b7 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -629,6 +629,10 @@ let type_of_inductive_knowing_conclusion env sigma ((mib,mip),u) conclty = env evdref scl ar.template_level (ctx,ar.template_param_levels) in !evdref, EConstr.of_constr (mkArity (List.rev ctx,scl)) +let type_of_projection_constant env (p,u) = + let pb = lookup_projection p env in + Vars.subst_instance_constr u pb.proj_type + let type_of_projection_knowing_arg env sigma p c ty = let c = EConstr.Unsafe.to_constr c in let IndType(pars,realargs) = @@ -637,7 +641,7 @@ let type_of_projection_knowing_arg env sigma p c ty = raise (Invalid_argument "type_of_projection_knowing_arg_type: not an inductive type") in let (_,u), pars = dest_ind_family pars in - substl (c :: List.rev pars) (Typeops.type_of_projection_constant env (p,u)) + substl (c :: List.rev pars) (type_of_projection_constant env (p,u)) (***********************************************) (* Guard condition *) diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 62bee5a36..5f7faa13e 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -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 @@ -837,6 +837,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) -> @@ -1391,7 +1411,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 +1520,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 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 e32807f4b..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 @@ -294,15 +295,15 @@ let strip_params env sigma c = | App (f, args) -> (match EConstr.kind sigma f with | Const (p,_) -> - let cb = lookup_constant p env in - (match cb.Declarations.const_proj with - | Some pb -> - let n = pb.Declarations.proj_npars in - if Array.length args > n then - mkApp (mkProj (Projection.make p false, args.(n)), - Array.sub args (n+1) (Array.length args - (n + 1))) - else c - | None -> c) + let p = Projection.make p false in + (match lookup_projection p env with + | pb -> + let n = pb.Declarations.proj_npars in + if Array.length args > n then + mkApp (mkProj (p, args.(n)), + Array.sub args (n+1) (Array.length args - (n + 1))) + else c + | exception Not_found -> c) | _ -> c) | _ -> c @@ -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/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/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/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/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/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/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 |