diff options
81 files changed, 1368 insertions, 1777 deletions
diff --git a/.github/CODEOWNERS b/.github/CODEOWNERS index 2ca827492..782efb5be 100644 --- a/.github/CODEOWNERS +++ b/.github/CODEOWNERS @@ -51,19 +51,21 @@ # each time someone modifies the dev changelog /doc/ @maximedenes -# Secondary maintainer @silene +# Secondary maintainer @silene @Zimmi48 /man/ @silene # Secondary maintainer @maximedenes ########## Coqchk ########## -/checker/ @barras -# Secondary maintainer @maximedenes +/checker/ @ppedrot +/test-suite/coqchk/ @ppedrot +# Secondary maintainers @maximedenes ########## Coq lib ########## /clib/ @ppedrot +/test-suite/unit-tests/clib/ @ppedrot # Secondary maintainer @ejgallego /lib/ @ejgallego @@ -90,6 +92,7 @@ ########## CoqIDE ########## /ide/ @ppedrot +/test-suite/ide/ @ppedrot # Secondary maintainer @gares ########## Interpretation ########## @@ -100,7 +103,7 @@ ########## Kernel ########## /kernel/ @maximedenes -# Secondary maintainer @barras +# Secondary maintainers @barras @ppedrot /kernel/byterun/ @maximedenes # Secondary maintainer @silene @@ -146,7 +149,8 @@ /plugins/ltac/ @ppedrot # Secondary maintainer @herbelin -/plugins/micromega/ @fajb +/plugins/micromega/ @fajb +/test-suite/micromega/ @fajb # Secondary maintainer @bgregoir /plugins/nsatz/ @thery @@ -162,7 +166,8 @@ /plugins/ssrmatching/ @gares # Secondary maintainer @maximedenes -/plugins/ssr/ @gares +/plugins/ssr/ @gares +/test-suite/ssr/ @gares # Secondary maintainer @maximedenes /plugins/syntax/ @ppedrot @@ -190,14 +195,21 @@ ########## STM ########## -/stm/ @gares -# Secondary maintainer @ejgallego +/stm/ @gares +/test-suite/interactive/ @gares +/test-suite/stm/ @gares +/test-suite/vio/ @gares +# Secondary maintainer @ejgallego ########## Tactics ########## /tactics/ @ppedrot # Secondary maintainer @mattam82 +/tactics/class_tactics.* @mattam82 +/test-suite/typeclasses/ @mattam82 +# Secondary maintainer @ppedrot + ########## Standard library ########## /theories/Arith/ @letouzey @@ -276,14 +288,14 @@ ########## Tools ########## -/tools/coqdoc/ @silene +/tools/coqdoc/ @silene +/test-suite/coqdoc/ @silene # Secondary maintainer @mattam82 -/tools/coq_makefile* @gares -# Secondary maintainer @silene - -/tools/CoqMakefile* @gares -# Secondary maintainer @silene +/tools/coq_makefile* @gares +/tools/CoqMakefile* @gares +/test-suite/coq-makefile/ @gares +# Secondary maintainer @silene /tools/coqdep* @ppedrot # Secondary maintainer @maximedenes @@ -291,7 +303,8 @@ /tools/coq_tex* @silene # Secondary maintainer @gares -/tools/coqwc* @silene +/tools/coqwc* @silene +/test-suite/coqwc/ @silene # Secondary maintainer @gares ########## Toplevel ########## @@ -322,9 +335,24 @@ /Makefile.ci @ejgallego # Secondary maintainer @SkySkimmer +# This file belongs to the doc /Makefile.doc @maximedenes # Secondary maintainer @silene +########## Test suite ########## + +/test-suite/Makefile @gares +/test-suite/_CoqProject @gares +/test-suite/README.md @gares +# Secondary maintainer @SkySkimmer + +/test-suite/save-logs @SkySkimmer + +/test-suite/complexity/ @herbelin + +/test-suite/unit-tests/src/ @jfehrle +# Secondary maintainer @SkySkimmer + ########## Developer tools ########## /dev/tools/backport-pr.sh @Zimmi48 @@ -7,6 +7,22 @@ Tactics Use with Set Default Goal Selector to force focusing before tactics are called. +- The undocumented "nameless" forms `fix N`, `cofix` that were + deprecated in 8.8 have been removed from LTAC's syntax; please use + `fix ident N/cofix ident` to explicitely name the (co)fixpoint + hypothesis to be introduced. + +- Introduction tactics "intro"/"intros" on a goal which is an + existential variable now force a refinement of the goal into a + dependent product rather than failing. + +- Support for fix/cofix added in Ltac "match" and "lazymatch". + +- Ltac backtraces now include trace information about tactics + called by OCaml-defined tactics. + +- Option "Ltac Debug" now applies also to terms built using Ltac functions. + Tools - Coq_makefile lets one override or extend the following variables from @@ -22,20 +38,6 @@ Vernacular Commands By default, they are disabled and produce an error. The deprecation warning which used to occur when using nested proofs has been removed. -Tactics - -- Introduction tactics "intro"/"intros" on a goal which is an - existential variable now force a refinement of the goal into a - dependent product rather than failing. - -Tactic language - -- Support for fix/cofix added in Ltac "match" and "lazymatch". - -- Ltac backtraces now include trace information about tactics - called by OCaml-defined tactics. -- Option "Ltac Debug" now applies also to terms built using Ltac functions. - Coq binaries and process model - Before 8.9, Coq distributed a single `coqtop` binary and a set of @@ -67,9 +69,9 @@ Tools Tactic language -- The undocumented "nameless" forms `fix N`, `cofix N` have been - deprecated; please use `fix/cofix ident N` to explicitely name - hypothesis to be introduced. +- The undocumented "nameless" forms `fix N`, `cofix` have been + deprecated; please use `fix ident N /cofix ident` to explicitely + name the (co)fixpoint hypothesis to be introduced. Documentation diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index 7fb976ee0..7b2229cb7 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -60,6 +60,20 @@ The sources for the [Coq reference manual](https://coq.inria.fr/distrib/current/ You may also contribute to the informal documentation available in [Cocorico](https://github.com/coq/coq/wiki) (the Coq wiki), and the [Coq FAQ](https://github.com/coq/coq/wiki/The-Coq-FAQ). Both of these are editable by anyone with a GitHub account. +## Following the development + +If you want to follow the development activity around Coq, you are encouraged +to subscribe to the [Coqdev mailing list](https://sympa.inria.fr/sympa/info/coqdev). +This mailing list has reasonably low traffic. + +You may also choose to use GitHub feature to +["watch" this repository](https://github.com/coq/coq/subscription), but be +advised that this means receiving a very large number of notifications. +GitHub gives [some advice](https://blog.github.com/2017-07-18-managing-large-numbers-of-github-notifications/#prioritize-the-notifications-you-receive) +on how to configure your e-mail client to filter these notifications. +A possible alternative is to deactivate e-mail notifications and manage your +GitHub web notifications using a tool such as [Octobox](http://octobox.io/). + ## Contributing outside this repository There are many useful ways to contribute to the Coq ecosystem that don't involve the Coq repository. diff --git a/Makefile.build b/Makefile.build index 036a3126b..b85418243 100644 --- a/Makefile.build +++ b/Makefile.build @@ -557,7 +557,7 @@ $(FAKEIDE): $(call bestobj, $(FAKEIDECMO)) | $(IDETOP) $(SHOW)'OCAMLBEST -o $@' $(HIDE)$(call bestocaml, -I ide -I ide/protocol -package str -package dynlink) -$(FAKEIDEBYTE): $(FAKEIDECMO) | $(IDETOPLOOPCMA) +$(FAKEIDEBYTE): $(FAKEIDECMO) | $(IDETOPBYTE) $(SHOW)'OCAMLC -o $@' $(HIDE)$(call ocamlbyte, -I ide -package str,unix,threads) diff --git a/Makefile.doc b/Makefile.doc index 41ae11b86..4670c79ec 100644 --- a/Makefile.doc +++ b/Makefile.doc @@ -55,7 +55,7 @@ endif sphinx: $(SPHINX_DEPS) $(SHOW)'SPHINXBUILD doc/sphinx' - $(HIDE)COQBIN="$(PWD)/bin" $(SPHINXBUILD) -W -b html $(ALLSPHINXOPTS) doc/sphinx $(SPHINXBUILDDIR)/html + $(HIDE)COQBIN="$(abspath bin)" $(SPHINXBUILD) -W -b html $(ALLSPHINXOPTS) doc/sphinx $(SPHINXBUILDDIR)/html @echo @echo "Build finished. The HTML pages are in $(SPHINXBUILDDIR)/html." diff --git a/checker/declarations.ml b/checker/declarations.ml index 2fe930dca..e1d2cf6d1 100644 --- a/checker/declarations.ml +++ b/checker/declarations.ml @@ -231,7 +231,7 @@ let rec map_kn f f' c = in let p' = func p in let ct' = func ct in - let l' = Array.smartmap func l in + let l' = Array.Smart.map func l in if (ci.ci_ind==ci_ind && p'==p && l'==l && ct'==ct)then c else @@ -260,21 +260,21 @@ let rec map_kn f f' c = else LetIn (na, b', t', ct') | App (ct,l) -> let ct' = func ct in - let l' = Array.smartmap func l in + let l' = Array.Smart.map func l in if (ct'== ct && l'==l) then c else App (ct',l') | Evar (e,l) -> - let l' = Array.smartmap func l in + let l' = Array.Smart.map func l in if (l'==l) then c else Evar (e,l') | Fix (ln,(lna,tl,bl)) -> - let tl' = Array.smartmap func tl in - let bl' = Array.smartmap func bl in + let tl' = Array.Smart.map func tl in + let bl' = Array.Smart.map func bl in if (bl == bl'&& tl == tl') then c else Fix (ln,(lna,tl',bl')) | CoFix(ln,(lna,tl,bl)) -> - let tl' = Array.smartmap func tl in - let bl' = Array.smartmap func bl in + let tl' = Array.Smart.map func tl in + let bl' = Array.Smart.map func bl in if (bl == bl'&& tl == tl') then c else CoFix (ln,(lna,tl',bl')) | _ -> c @@ -480,7 +480,7 @@ let dest_subterms p = let (_,cstrs) = Rtree.dest_node p in Array.map (fun t -> Array.to_list (snd (Rtree.dest_node t))) cstrs -let subst_wf_paths sub p = Rtree.smartmap (subst_recarg sub) p +let subst_wf_paths sub p = Rtree.Smart.map (subst_recarg sub) p let eq_recarg r1 r2 = match r1, r2 with | Norec, Norec -> true @@ -513,7 +513,7 @@ let subst_decl_arity f g sub ar = let subst_rel_declaration sub = Term.map_rel_decl (subst_mps sub) -let subst_rel_context sub = List.smartmap (subst_rel_declaration sub) +let subst_rel_context sub = List.Smart.map (subst_rel_declaration sub) let constant_is_polymorphic cb = match cb.const_universes with @@ -544,10 +544,10 @@ let subst_mind_packet sub mbp = mind_consnrealdecls = mbp.mind_consnrealdecls; mind_consnrealargs = mbp.mind_consnrealargs; mind_typename = mbp.mind_typename; - mind_nf_lc = Array.smartmap (subst_mps sub) mbp.mind_nf_lc; + mind_nf_lc = Array.Smart.map (subst_mps sub) mbp.mind_nf_lc; mind_arity_ctxt = subst_rel_context sub mbp.mind_arity_ctxt; mind_arity = subst_ind_arity sub mbp.mind_arity; - mind_user_lc = Array.smartmap (subst_mps sub) mbp.mind_user_lc; + mind_user_lc = Array.Smart.map (subst_mps sub) mbp.mind_user_lc; mind_nrealargs = mbp.mind_nrealargs; mind_nrealdecls = mbp.mind_nrealdecls; mind_kelim = mbp.mind_kelim; @@ -560,7 +560,7 @@ let subst_mind_packet sub mbp = let subst_mind sub mib = { mib with mind_params_ctxt = map_rel_context (subst_mps sub) mib.mind_params_ctxt; - mind_packets = Array.smartmap (subst_mind_packet sub) mib.mind_packets } + mind_packets = Array.Smart.map (subst_mind_packet sub) mib.mind_packets } (* Modules *) @@ -599,7 +599,7 @@ and subst_body : 'a. (_ -> 'a -> 'a) -> _ -> 'a generic_module_body -> 'a generi mod_mp = subst_mp sub mb.mod_mp; mod_expr = subst_impl sub mb.mod_expr; mod_type = subst_signature sub mb.mod_type; - mod_type_alg = Option.smartmap (subst_expression sub) mb.mod_type_alg } + mod_type_alg = Option.Smart.map (subst_expression sub) mb.mod_type_alg } and subst_module sub mb = subst_body (fun sub e -> implem_map (subst_signature sub) (subst_expression sub) e) sub mb diff --git a/checker/indtypes.ml b/checker/indtypes.ml index f403834f5..916934a81 100644 --- a/checker/indtypes.ml +++ b/checker/indtypes.ml @@ -598,16 +598,18 @@ let check_subtyping cumi paramsctxt env inds = let check_inductive env kn mib = Flags.if_verbose Feedback.msg_notice (str " checking ind: " ++ MutInd.print kn); (* check mind_constraints: should be consistent with env *) - let ind_ctx = + let env0 = match mib.mind_universes with - | Monomorphic_ind _ -> Univ.UContext.empty (** Already in the global environment *) - | Polymorphic_ind auctx -> Univ.AUContext.repr auctx + | Monomorphic_ind _ -> env + | Polymorphic_ind auctx -> + let uctx = Univ.AUContext.repr auctx in + Environ.push_context uctx env | Cumulative_ind cumi -> - Univ.AUContext.repr (Univ.ACumulativityInfo.univ_context cumi) + let uctx = Univ.AUContext.repr (Univ.ACumulativityInfo.univ_context cumi) in + Environ.push_context uctx env in - let env = Environ.push_context ind_ctx env in (** Locally set the oracle for further typechecking *) - let env0 = Environ.set_oracle env mib.mind_typing_flags.conv_oracle in + let env0 = Environ.set_oracle env0 mib.mind_typing_flags.conv_oracle in (* check mind_record : TODO ? check #constructor = 1 ? *) (* check mind_finite : always OK *) (* check mind_ntypes *) diff --git a/checker/term.ml b/checker/term.ml index 0236f7867..509634bdb 100644 --- a/checker/term.ml +++ b/checker/term.ml @@ -243,7 +243,7 @@ let map_rel_decl f = function LocalDef (n, body', typ') let map_rel_context f = - List.smartmap (map_rel_decl f) + List.Smart.map (map_rel_decl f) let extended_rel_list n hyps = let rec reln l p = function diff --git a/checker/univ.ml b/checker/univ.ml index 7d285b6fe..15673736f 100644 --- a/checker/univ.ml +++ b/checker/univ.ml @@ -314,7 +314,7 @@ struct let for_all = List.for_all - let smartmap = List.smartmap + let smart_map = List.Smart.map end @@ -911,12 +911,12 @@ struct let is_empty x = Int.equal (Array.length x) 0 let subst_fn fn t = - let t' = CArray.smartmap fn t in + let t' = CArray.Smart.map fn t in if t' == t then t else t' let subst s t = let t' = - CArray.smartmap (fun x -> try LMap.find x s with Not_found -> x) t + CArray.Smart.map (fun x -> try LMap.find x s with Not_found -> x) t in if t' == t then t else t' let pr = @@ -952,11 +952,11 @@ let subst_instance_level s l = | _ -> l let subst_instance_instance s i = - Array.smartmap (fun l -> subst_instance_level s l) i + Array.Smart.map (fun l -> subst_instance_level s l) i let subst_instance_universe s u = let f x = Universe.Expr.map (fun u -> subst_instance_level s u) x in - let u' = Universe.smartmap f u in + let u' = Universe.smart_map f u in if u == u' then u else Universe.sort u' @@ -1097,7 +1097,7 @@ let subst_univs_level_level subst l = let subst_univs_level_universe subst u = let f x = Universe.Expr.map (fun u -> subst_univs_level_level subst u) x in - let u' = Universe.smartmap f u in + let u' = Universe.smart_map f u in if u == u' then u else Universe.sort u' diff --git a/clib/cArray.ml b/clib/cArray.ml index 071f4689b..b26dae729 100644 --- a/clib/cArray.ml +++ b/clib/cArray.ml @@ -50,7 +50,9 @@ sig val map_of_list : ('a -> 'b) -> 'a list -> 'b array val chop : int -> 'a array -> 'a array * 'a array val smartmap : ('a -> 'a) -> 'a array -> 'a array + [@@ocaml.deprecated "Same as [Smart.map]"] val smartfoldmap : ('r -> 'a -> 'r * 'a) -> 'r -> 'a array -> 'r * 'a array + [@@ocaml.deprecated "Same as [Smart.fold_left_map]"] val map2 : ('a -> 'b -> 'c) -> 'a array -> 'b array -> 'c array val map2_i : (int -> 'a -> 'b -> 'c) -> 'a array -> 'b array -> 'c array val map3 : @@ -72,6 +74,25 @@ sig val rev_of_list : 'a list -> 'a array val rev_to_list : 'a array -> 'a list val filter_with : bool list -> 'a array -> 'a array + module Smart : + sig + val map : ('a -> 'a) -> 'a array -> 'a array + val map2 : ('a -> 'b -> 'b) -> 'a array -> 'b array -> 'b array + val fold_left_map : ('a -> 'b -> 'a * 'b) -> 'a -> 'b array -> 'a * 'b array + val fold_left2_map : ('a -> 'b -> 'c -> 'a * 'c) -> 'a -> 'b array -> 'c array -> 'a * 'c array + end + module Fun1 : + sig + val map : ('r -> 'a -> 'b) -> 'r -> 'a array -> 'b array + val smartmap : ('r -> 'a -> 'a) -> 'r -> 'a array -> 'a array + [@@ocaml.deprecated "Same as [Fun1.Smart.map]"] + val iter : ('r -> 'a -> unit) -> 'r -> 'a array -> unit + val iter2 : ('r -> 'a -> 'b -> unit) -> 'r -> 'a array -> 'b array -> unit + module Smart : + sig + val map : ('r -> 'a -> 'a) -> 'r -> 'a array -> 'a array + end + end end include Array @@ -326,72 +347,6 @@ let chop n v = if n > vlen then failwith "Array.chop"; (Array.sub v 0 n, Array.sub v n (vlen-n)) -(* If none of the elements is changed by f we return ar itself. - The while loop looks for the first such an element. - If found, we break here and the new array is produced, - but f is not re-applied to elements that are already checked *) -let smartmap f (ar : 'a array) = - let len = Array.length ar in - let i = ref 0 in - let break = ref true in - let temp = ref None in - while !break && (!i < len) do - let v = Array.unsafe_get ar !i in - let v' = f v in - if v == v' then incr i - else begin - break := false; - temp := Some v'; - end - done; - if !i < len then begin - (** The array is not the same as the original one *) - let ans : 'a array = Array.copy ar in - let v = match !temp with None -> assert false | Some x -> x in - Array.unsafe_set ans !i v; - incr i; - while !i < len do - let v = Array.unsafe_get ans !i in - let v' = f v in - if v != v' then Array.unsafe_set ans !i v'; - incr i - done; - ans - end else ar - -(** Same as [smartmap] but threads a state meanwhile *) -let smartfoldmap f accu (ar : 'a array) = - let len = Array.length ar in - let i = ref 0 in - let break = ref true in - let r = ref accu in - (** This variable is never accessed unset *) - let temp = ref None in - while !break && (!i < len) do - let v = Array.unsafe_get ar !i in - let (accu, v') = f !r v in - r := accu; - if v == v' then incr i - else begin - break := false; - temp := Some v'; - end - done; - if !i < len then begin - let ans : 'a array = Array.copy ar in - let v = match !temp with None -> assert false | Some x -> x in - Array.unsafe_set ans !i v; - incr i; - while !i < len do - let v = Array.unsafe_get ar !i in - let (accu, v') = f !r v in - r := accu; - if v != v' then Array.unsafe_set ans !i v'; - incr i - done; - !r, ans - end else !r, ar - let map2 f v1 v2 = let len1 = Array.length v1 in let len2 = Array.length v2 in @@ -508,29 +463,53 @@ let rev_to_list a = let filter_with filter v = Array.of_list (CList.filter_with filter (Array.to_list v)) -module Fun1 = +module Smart = struct - let map f arg v = match v with - | [| |] -> [| |] - | _ -> - let len = Array.length v in - let x0 = Array.unsafe_get v 0 in - let ans = Array.make len (f arg x0) in - for i = 1 to pred len do - let x = Array.unsafe_get v i in - Array.unsafe_set ans i (f arg x) + (* If none of the elements is changed by f we return ar itself. + The while loop looks for the first such an element. + If found, we break here and the new array is produced, + but f is not re-applied to elements that are already checked *) + let map f (ar : 'a array) = + let len = Array.length ar in + let i = ref 0 in + let break = ref true in + let temp = ref None in + while !break && (!i < len) do + let v = Array.unsafe_get ar !i in + let v' = f v in + if v == v' then incr i + else begin + break := false; + temp := Some v'; + end done; - ans + if !i < len then begin + (** The array is not the same as the original one *) + let ans : 'a array = Array.copy ar in + let v = match !temp with None -> assert false | Some x -> x in + Array.unsafe_set ans !i v; + incr i; + while !i < len do + let v = Array.unsafe_get ans !i in + let v' = f v in + if v != v' then Array.unsafe_set ans !i v'; + incr i + done; + ans + end else ar - let smartmap f arg (ar : 'a array) = + let map2 f aux_ar ar = let len = Array.length ar in + let aux_len = Array.length aux_ar in + let () = if not (Int.equal len aux_len) then invalid_arg "Array.Smart.map2" in let i = ref 0 in let break = ref true in let temp = ref None in while !break && (!i < len) do let v = Array.unsafe_get ar !i in - let v' = f arg v in + let w = Array.unsafe_get aux_ar !i in + let v' = f w v in if v == v' then incr i else begin break := false; @@ -545,13 +524,105 @@ struct incr i; while !i < len do let v = Array.unsafe_get ans !i in - let v' = f arg v in + let w = Array.unsafe_get aux_ar !i in + let v' = f w v in if v != v' then Array.unsafe_set ans !i v'; incr i done; ans end else ar + (** Same as [Smart.map] but threads a state meanwhile *) + let fold_left_map f accu (ar : 'a array) = + let len = Array.length ar in + let i = ref 0 in + let break = ref true in + let r = ref accu in + (** This variable is never accessed unset *) + let temp = ref None in + while !break && (!i < len) do + let v = Array.unsafe_get ar !i in + let (accu, v') = f !r v in + r := accu; + if v == v' then incr i + else begin + break := false; + temp := Some v'; + end + done; + if !i < len then begin + let ans : 'a array = Array.copy ar in + let v = match !temp with None -> assert false | Some x -> x in + Array.unsafe_set ans !i v; + incr i; + while !i < len do + let v = Array.unsafe_get ar !i in + let (accu, v') = f !r v in + r := accu; + if v != v' then Array.unsafe_set ans !i v'; + incr i + done; + !r, ans + end else !r, ar + + (** Same as [Smart.map2] but threads a state meanwhile *) + let fold_left2_map f accu aux_ar ar = + let len = Array.length ar in + let aux_len = Array.length aux_ar in + let () = if not (Int.equal len aux_len) then invalid_arg "Array.Smart.fold_left2_map" in + let i = ref 0 in + let break = ref true in + let r = ref accu in + (** This variable is never accessed unset *) + let temp = ref None in + while !break && (!i < len) do + let v = Array.unsafe_get ar !i in + let w = Array.unsafe_get aux_ar !i in + let (accu, v') = f !r w v in + r := accu; + if v == v' then incr i + else begin + break := false; + temp := Some v'; + end + done; + if !i < len then begin + let ans : 'a array = Array.copy ar in + let v = match !temp with None -> assert false | Some x -> x in + Array.unsafe_set ans !i v; + incr i; + while !i < len do + let v = Array.unsafe_get ar !i in + let w = Array.unsafe_get aux_ar !i in + let (accu, v') = f !r w v in + r := accu; + if v != v' then Array.unsafe_set ans !i v'; + incr i + done; + !r, ans + end else !r, ar + +end + +(* Deprecated aliases *) +let smartmap = Smart.map +let smartfoldmap = Smart.fold_left_map + +module Fun1 = +struct + + let map f arg v = match v with + | [| |] -> [| |] + | _ -> + let len = Array.length v in + let x0 = Array.unsafe_get v 0 in + let ans = Array.make len (f arg x0) in + for i = 1 to pred len do + let x = Array.unsafe_get v i in + Array.unsafe_set ans i (f arg x) + done; + ans + let iter f arg v = let len = Array.length v in for i = 0 to pred len do @@ -559,4 +630,50 @@ struct f arg x done + let iter2 f arg v1 v2 = + let len1 = Array.length v1 in + let len2 = Array.length v2 in + let () = if not (Int.equal len2 len1) then invalid_arg "Array.Fun1.iter2" in + for i = 0 to pred len1 do + let x1 = uget v1 i in + let x2 = uget v2 i in + f arg x1 x2 + done + + module Smart = + struct + + let map f arg (ar : 'a array) = + let len = Array.length ar in + let i = ref 0 in + let break = ref true in + let temp = ref None in + while !break && (!i < len) do + let v = Array.unsafe_get ar !i in + let v' = f arg v in + if v == v' then incr i + else begin + break := false; + temp := Some v'; + end + done; + if !i < len then begin + (** The array is not the same as the original one *) + let ans : 'a array = Array.copy ar in + let v = match !temp with None -> assert false | Some x -> x in + Array.unsafe_set ans !i v; + incr i; + while !i < len do + let v = Array.unsafe_get ans !i in + let v' = f arg v in + if v != v' then Array.unsafe_set ans !i v'; + incr i + done; + ans + end else ar + + end + + let smartmap = Smart.map + end diff --git a/clib/cArray.mli b/clib/cArray.mli index 9c2f521f4..8bf33f82f 100644 --- a/clib/cArray.mli +++ b/clib/cArray.mli @@ -83,13 +83,14 @@ sig Raise [Failure "Array.chop"] if [i] is not a valid index. *) val smartmap : ('a -> 'a) -> 'a array -> 'a array - (** [smartmap f a] behaves as [map f a] but returns [a] instead of a copy when - [f x == x] for all [x] in [a]. *) + [@@ocaml.deprecated "Same as [Smart.map]"] val smartfoldmap : ('r -> 'a -> 'r * 'a) -> 'r -> 'a array -> 'r * 'a array - (** Same as [smartmap] but threads an additional state left-to-right. *) + [@@ocaml.deprecated "Same as [Smart.fold_left_map]"] val map2 : ('a -> 'b -> 'c) -> 'a array -> 'b array -> 'c array + (** See also [Smart.map2] *) + val map2_i : (int -> 'a -> 'b -> 'c) -> 'a array -> 'b array -> 'c array val map3 : ('a -> 'b -> 'c -> 'd) -> 'a array -> 'b array -> 'c array -> 'd array @@ -102,13 +103,13 @@ sig val fold_left_map : ('a -> 'b -> 'a * 'c) -> 'a -> 'b array -> 'a * 'c array (** [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] *) + where [(e_i,k_i)=f e_{i-1} l_i]; see also [Smart.fold_left_map] *) val fold_right_map : ('a -> 'c -> 'b * 'c) -> 'a array -> 'c -> 'b array * 'c (** Same, folding on the right *) val fold_left2_map : ('a -> 'b -> 'c -> 'a * 'd) -> 'a -> 'b array -> 'c array -> 'a * 'd array - (** Same with two arrays, folding on the left *) + (** Same with two arrays, folding on the left; see also [Smart.fold_left2_map] *) val fold_right2_map : ('a -> 'b -> 'c -> 'd * 'c) -> 'a array -> 'b array -> 'c -> 'd array * 'c (** Same with two arrays, folding on the left *) @@ -137,23 +138,57 @@ sig (** [filter_with b a] selects elements of [a] whose corresponding element in [b] is [true]. Raise [Invalid_argument _] when sizes differ. *) + module Smart : + sig + val map : ('a -> 'a) -> 'a array -> 'a array + (** [Smart.map f a] behaves as [map f a] but returns [a] instead of a copy when + [f x == x] for all [x] in [a]. *) + + val map2 : ('a -> 'b -> 'b) -> 'a array -> 'b array -> 'b array + (** [Smart.map2 f a b] behaves as [map2 f a b] but returns [a] instead of a copy when + [f x y == y] for all [x] in [a] and [y] in [b] pointwise. *) + + val fold_left_map : ('a -> 'b -> 'a * 'b) -> 'a -> 'b array -> 'a * 'b array + (** [Smart.fold_left_mapf a b] behaves as [fold_left_map] but + returns [b] as second component instead of a copy of [b] when + the output array is pointwise the same as the input array [b] *) + + val fold_left2_map : ('a -> 'b -> 'c -> 'a * 'c) -> 'a -> 'b array -> 'c array -> 'a * 'c array + (** [Smart.fold_left2_map f a b c] behaves as [fold_left2_map] but + returns [c] as second component instead of a copy of [c] when + the output array is pointwise the same as the input array [c] *) + + end + (** The functions defined in this module are optimized specializations + of the main ones, when the returned array is of same type as one of + the original array. *) + + module Fun1 : + sig + val map : ('r -> 'a -> 'b) -> 'r -> 'a array -> 'b array + (** [Fun1.map f x v = map (f x) v] *) + + val smartmap : ('r -> 'a -> 'a) -> 'r -> 'a array -> 'a array + [@@ocaml.deprecated "Same as [Fun1.Smart.map]"] + + val iter : ('r -> 'a -> unit) -> 'r -> 'a array -> unit + (** [Fun1.iter f x v = iter (f x) v] *) + + val iter2 : ('r -> 'a -> 'b -> unit) -> 'r -> 'a array -> 'b array -> unit + (** [Fun1.iter2 f x v1 v2 = iter (f x) v1 v2] *) + + module Smart : + sig + val map : ('r -> 'a -> 'a) -> 'r -> 'a array -> 'a array + (** [Fun1.Smart.map f x v = Smart.map (f x) v] *) + end + + end + (** The functions defined in this module are the same as the main ones, except + that they are all higher-order, and their function arguments have an + additional parameter. This allows us to prevent closure creation in critical + cases. *) + end include ExtS - -module Fun1 : -sig - val map : ('r -> 'a -> 'b) -> 'r -> 'a array -> 'b array - (** [Fun1.map f x v = map (f x) v] *) - - val smartmap : ('r -> 'a -> 'a) -> 'r -> 'a array -> 'a array - (** [Fun1.smartmap f x v = smartmap (f x) v] *) - - val iter : ('r -> 'a -> unit) -> 'r -> 'a array -> unit - (** [Fun1.iter f x v = iter (f x) v] *) - -end -(** The functions defined in this module are the same as the main ones, except - that they are all higher-order, and their function arguments have an - additional parameter. This allows us to prevent closure creation in critical - cases. *) diff --git a/clib/cList.ml b/clib/cList.ml index 8727f4696..7621793d4 100644 --- a/clib/cList.ml +++ b/clib/cList.ml @@ -39,6 +39,7 @@ sig val map_filter_i : (int -> 'a -> 'b option) -> 'a list -> 'b list val filter_with : bool list -> 'a list -> 'a list val smartmap : ('a -> 'a) -> 'a list -> 'a list + [@@ocaml.deprecated "Same as [Smart.map]"] val map_left : ('a -> 'b) -> 'a list -> 'b list val map_i : (int -> 'a -> 'b) -> int -> 'a list -> 'b list val map2_i : @@ -53,6 +54,7 @@ sig (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 extend : bool list -> 'a -> 'a list -> 'a list val count : ('a -> bool) -> 'a list -> int val index : 'a eq -> 'a -> 'a list -> int @@ -117,6 +119,12 @@ sig ('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 type elt val equal : elt list -> elt list -> bool @@ -365,13 +373,6 @@ let assign l n e = in assrec [] l n -let rec smartmap f l = match l with - [] -> l - | h::tl -> - let h' = f h and tl' = smartmap f tl in - if h'==h && tl'==tl then l - else h'::tl' - let map_left = map let map2_i f i l1 l2 = @@ -398,15 +399,6 @@ let map4 f l1 l2 l3 l4 = in map (l1,l2,l3,l4) -let rec smartfilter f l = match l with - [] -> l - | h::tl -> - let tl' = smartfilter f tl in - if f h then - if tl' == tl then l - else h :: tl' - else tl' - 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' @@ -896,6 +888,30 @@ let rec factorize_left cmp = function (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' + +end + +let smartmap = Smart.map +let smartfilter = Smart.filter + module type MonoS = sig type elt val equal : elt list -> elt list -> bool diff --git a/clib/cList.mli b/clib/cList.mli index fd6d6a158..b3c151098 100644 --- a/clib/cList.mli +++ b/clib/cList.mli @@ -75,8 +75,7 @@ sig [b] is [true]. Raise [Invalid_argument _] when sizes differ. *) val smartmap : ('a -> 'a) -> 'a list -> 'a list - (** [smartmap f [a1...an] = List.map f [a1...an]] but if for all i - [f ai == ai], then [smartmap f l == l] *) + [@@ocaml.deprecated "Same as [Smart.map]"] val map_left : ('a -> 'b) -> 'a list -> 'b list (** As [map] but ensures the left-to-right order of evaluation. *) @@ -97,8 +96,7 @@ sig (** [map_of_array f a] behaves as [List.map f (Array.to_list a)] *) val smartfilter : ('a -> bool) -> 'a list -> 'a list - (** [smartfilter f [a1...an] = List.filter f [a1...an]] but if for all i - [f ai = true], then [smartfilter f l == l] *) + [@@ocaml.deprecated "Same as [Smart.filter]"] val extend : bool list -> 'a -> 'a list -> 'a list (** [extend l a [a1..an]] assumes that the number of [true] in [l] is [n]; @@ -258,6 +256,17 @@ sig val factorize_left : 'a eq -> ('a * 'b) list -> ('a * 'b list) list + 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 type elt val equal : elt list -> elt list -> bool diff --git a/clib/cMap.ml b/clib/cMap.ml index 373e3f8fd..f6e52594b 100644 --- a/clib/cMap.ml +++ b/clib/cMap.ml @@ -35,8 +35,15 @@ 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]"] *) val smartmapi : (key -> 'a -> 'a) -> 'a t -> 'a t + (** [@@ocaml.deprecated "Same as [Smart.mapi]"] *) val height : 'a t -> int + module Smart : + sig + val map : ('a -> 'a) -> 'a t -> 'a t + val mapi : (key -> 'a -> 'a) -> 'a t -> 'a t + end module Unsafe : sig val map : (key -> 'a -> key * 'b) -> 'a t -> 'b t @@ -59,8 +66,15 @@ 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]"] *) val smartmapi : (M.t -> 'a -> 'a) -> 'a map -> 'a map + (** [@@ocaml.deprecated "Same as [Smart.mapi]"] *) val height : 'a map -> int + module Smart : + sig + val map : ('a -> 'a) -> 'a map -> 'a map + val mapi : (M.t -> 'a -> 'a) -> 'a map -> 'a map + end module Unsafe : sig val map : (M.t -> 'a -> M.t * 'b) -> 'a map -> 'b map @@ -154,28 +168,36 @@ struct let accu = f k v (fold_right f r accu) in fold_right f l accu - let rec smartmap f (s : 'a map) = match map_prj s with - | MEmpty -> map_inj MEmpty - | MNode (l, k, v, r, h) -> - let l' = smartmap f l in - let r' = smartmap f r in - let v' = f v in - if l == l' && r == r' && v == v' then s - else map_inj (MNode (l', k, v', r', h)) - - let rec smartmapi f (s : 'a map) = match map_prj s with - | MEmpty -> map_inj MEmpty - | MNode (l, k, v, r, h) -> - let l' = smartmapi f l in - let r' = smartmapi f r in - let v' = f k v in - if l == l' && r == r' && v == v' then s - else map_inj (MNode (l', k, v', r', h)) - let height s = match map_prj s with | MEmpty -> 0 | MNode (_, _, _, _, h) -> h + module Smart = + struct + + let rec map f (s : 'a map) = match map_prj s with + | MEmpty -> map_inj MEmpty + | MNode (l, k, v, r, h) -> + let l' = map f l in + let r' = map f r in + let v' = f v in + if l == l' && r == r' && v == v' then s + else map_inj (MNode (l', k, v', r', h)) + + let rec mapi f (s : 'a map) = match map_prj s with + | MEmpty -> map_inj MEmpty + | MNode (l, k, v, r, h) -> + let l' = mapi f l in + let r' = mapi f r in + let v' = f k v in + if l == l' && r == r' && v == v' then s + else map_inj (MNode (l', k, v', r', h)) + + end + + let smartmap = Smart.map + let smartmapi = Smart.mapi + module Unsafe = struct diff --git a/clib/cMap.mli b/clib/cMap.mli index bb0019bb8..b45effb95 100644 --- a/clib/cMap.mli +++ b/clib/cMap.mli @@ -58,14 +58,23 @@ sig (** Folding keys in decreasing order. *) val smartmap : ('a -> 'a) -> 'a t -> 'a t - (** As [map] but tries to preserve sharing. *) + (** [@@ocaml.deprecated "Same as [Smart.map]"] *) val smartmapi : (key -> 'a -> 'a) -> 'a t -> 'a t - (** As [mapi] but tries to preserve sharing. *) + (** [@@ocaml.deprecated "Same as [Smart.mapi]"] *) val height : 'a t -> int (** An indication of the logarithmic size of a map *) + module Smart : + sig + val map : ('a -> 'a) -> 'a t -> 'a t + (** As [map] but tries to preserve sharing. *) + + val mapi : (key -> 'a -> 'a) -> 'a t -> 'a t + (** As [mapi] but tries to preserve sharing. *) + end + module Unsafe : sig val map : (key -> 'a -> key * 'b) -> 'a t -> 'b t diff --git a/clib/hMap.ml b/clib/hMap.ml index 37f867c6b..b2cf47430 100644 --- a/clib/hMap.ml +++ b/clib/hMap.ml @@ -383,13 +383,21 @@ struct let m = Map.set k x m in Int.Map.set h m s - let smartmap f s = - let fs m = Map.smartmap f m in - Int.Map.smartmap fs s + module Smart = + struct + + let map f s = + let fs m = Map.Smart.map f m in + Int.Map.Smart.map fs s + + let mapi f s = + let fs m = Map.Smart.mapi f m in + Int.Map.Smart.map fs s + + end - let smartmapi f s = - let fs m = Map.smartmapi f m in - Int.Map.smartmap fs s + let smartmap = Smart.map + let smartmapi = Smart.mapi let height s = Int.Map.height s diff --git a/clib/option.ml b/clib/option.ml index 32fe2fc5f..7a3d5f934 100644 --- a/clib/option.ml +++ b/clib/option.ml @@ -100,12 +100,6 @@ let map f = function | Some y -> Some (f y) | _ -> None -(** [smartmap f x] does the same as [map f x] except that it tries to share - some memory. *) -let smartmap f = function - | Some y as x -> let y' = f y in if y' == y then x else Some y' - | _ -> None - (** [fold_left f a x] is [f a y] if [x] is [Some y], and [a] otherwise. *) let fold_left f a = function | Some y -> f a y @@ -176,6 +170,21 @@ let lift2 f x y = | _,_ -> None +(** {6 Smart operations} *) + +module Smart = +struct + + (** [Smart.map f x] does the same as [map f x] except that it tries to share + some memory. *) + let map f = function + | Some y as x -> let y' = f y in if y' == y then x else Some y' + | _ -> None + +end + +let smartmap = Smart.map + (** {6 Operations with Lists} *) module List = diff --git a/clib/option.mli b/clib/option.mli index 14fa9da38..8f82bf090 100644 --- a/clib/option.mli +++ b/clib/option.mli @@ -75,9 +75,8 @@ val iter2 : ('a -> 'b -> unit) -> 'a option -> 'b option -> unit (** [map f x] is [None] if [x] is [None] and [Some (f y)] if [x] is [Some y]. *) val map : ('a -> 'b) -> 'a option -> 'b option -(** [smartmap f x] does the same as [map f x] except that it tries to share - some memory. *) val smartmap : ('a -> 'a) -> 'a option -> 'a option +[@@ocaml.deprecated "Same as [Smart.map]"] (** [fold_left f a x] is [f a y] if [x] is [Some y], and [a] otherwise. *) val fold_left : ('b -> 'a -> 'b) -> 'b -> 'a option -> 'b @@ -123,6 +122,16 @@ val lift_left : ('a -> 'b -> 'c) -> 'a option -> 'b -> 'c option [Some w]. It is [None] otherwise. *) val lift2 : ('a -> 'b -> 'c) -> 'a option -> 'b option -> 'c option +(** {6 Smart operations} *) + +module Smart : +sig + + (** [Smart.map f x] does the same as [map f x] except that it tries to share + some memory. *) + val map : ('a -> 'a) -> 'a option -> 'a option + +end (** {6 Operations with Lists} *) diff --git a/dev/ci/README.md b/dev/ci/README.md index ed3442e0d..697a160ca 100644 --- a/dev/ci/README.md +++ b/dev/ci/README.md @@ -107,19 +107,32 @@ there are some. You can also run one CI target locally (using `make ci-somedev`). -Whenever your PR breaks tested developments, you should either adapt it -so that it doesn't, or provide a branch fixing these developments (or at -least work with the author of the development / other Coq developers to -prepare these fixes). Then, add an overlay in -[`dev/ci/user-overlays`](/dev/ci/user-overlays) (see the README there) -as part of your PR. - -The process to merge your PR is then to submit PRs to the external -development repositories, merge the latter first (if the fixes are -backward-compatible), and merge the PR on Coq then. - See also [`test-suite/README.md`](/test-suite/README.md) for information about adding new tests to the test-suite. +### Breaking changes + +When your PR breaks an external project we test in our CI, you must prepare a +patch (or ask someone to prepare a patch) to fix the project: + +1. Fork the external project, create a new branch, push a commit adapting + the project to your changes. +2. Test your pull request with your adapted version of the external project by + adding an overlay file to your pull request (cf. + [`dev/ci/user-overlays/README.md`](/dev/ci/user-overlays/README.md)). +3. Fixes to external libraries (pure Coq projects) *must* be backward + compatible (i.e. they should also work with the development version of Coq, + and the latest stable version). This will allow you to open a PR on the + external project repository to have your changes merged *before* your PR on + Coq can be integrated. + + On the other hand, patches to plugins (projects linking to the Coq ML API) + can very rarely be made backward compatible and plugins we test will + generally have a dedicated branch per Coq version. + You can still open a pull request but the merging will be requested by the + developer who merges the PR on Coq. There are plans to improve this, cf. + [#6724](https://github.com/coq/coq/issues/6724). + +Moreover your PR must absolutely update the [`CHANGES`](/CHANGES) file. Advanced GitLab CI information ------------------------------ diff --git a/dev/ci/ci-fiat-crypto.sh b/dev/ci/ci-fiat-crypto.sh index feabf72d4..48a1366ab 100755 --- a/dev/ci/ci-fiat-crypto.sh +++ b/dev/ci/ci-fiat-crypto.sh @@ -11,4 +11,4 @@ git_checkout "${fiat_crypto_CI_BRANCH}" "${fiat_crypto_CI_GITURL}" "${fiat_crypt fiat_crypto_CI_TARGETS1="printlite lite lite-display" fiat_crypto_CI_TARGETS2="print-nobigmem nobigmem nonautogenerated-specific nonautogenerated-specific-display" -( cd "${fiat_crypto_CI_DIR}" && make ${fiat_crypto_CI_TARGETS1} && make ${fiat_crypto_CI_TARGETS2} ) +( cd "${fiat_crypto_CI_DIR}" && make ${fiat_crypto_CI_TARGETS1} && make -j 1 ${fiat_crypto_CI_TARGETS2} ) diff --git a/dev/ci/user-overlays/07196-ejgallego-tactics+push_fix_naming_out.sh b/dev/ci/user-overlays/07196-ejgallego-tactics+push_fix_naming_out.sh new file mode 100644 index 000000000..ea9cd8ee0 --- /dev/null +++ b/dev/ci/user-overlays/07196-ejgallego-tactics+push_fix_naming_out.sh @@ -0,0 +1,21 @@ +if [ "$CI_PULL_REQUEST" = "7196" ] || [ "$CI_BRANCH" = "tactics+push_fix_naming_out" ] || [ "$CI_BRANCH" = "pr-7196" ]; then + + # Needed overlays: https://gitlab.com/coq/coq/pipelines/21244550 + # + # equations + # ltac2 + + # The below developments should instead use a backwards compatible fix. + # + # color + # iris-lambda-rust + # math-classes + # formal-topology + + ltac2_CI_BRANCH=tactics+push_fix_naming_out + ltac2_CI_GITURL=https://github.com/ejgallego/ltac2 + + Equations_CI_BRANCH=tactics+push_fix_naming_out + Equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations + +fi diff --git a/dev/ci/user-overlays/README.md b/dev/ci/user-overlays/README.md index a7474e324..aec2dfe0a 100644 --- a/dev/ci/user-overlays/README.md +++ b/dev/ci/user-overlays/README.md @@ -1,8 +1,21 @@ # Add overlays for your pull requests in this directory -An overlay is a file containing very simple logic to test whether we are currently building a specific pull request or git branch (useful so that overlays work on your own fork) and which changes some of the variables whose default can be found in [`ci-basic-overlay.sh`](/dev/ci/ci-basic-overlay.sh). +When your pull request breaks an external project we test in our CI and you +have prepared a branch with the fix, you can add an "overlay" to your pull +request to test it with the adapted version of the external project. -The name of your overlay file should be of the form `five_digit_PR_number-GitHub_handle-branch_name.sh`. +An overlay is a file which defines where to look for the patched version so that +testing is possible. It redefines some variables from +[`ci-basic-overlay.sh`](/dev/ci/ci-basic-overlay.sh): +give the name of your branch using a `_CI_BRANCH` variable and the location of +your fork using a `_CI_GITURL` variable. + +Moreover, the file contains very simple logic to test the pull request number +or branch name and apply it only in this case. + +The name of your overlay file should start with a five-digit pull request +number, followed by a dash, anything (for instance your GitHub nickname +and the branch name), then a `.sh` extension (`[0-9]{5}-[a-zA-Z0-9-_]+.sh`). Example: `00669-maximedenes-ssr-merge.sh` containing diff --git a/dev/doc/MERGING.md b/dev/doc/MERGING.md index a466124c1..65457b63a 100644 --- a/dev/doc/MERGING.md +++ b/dev/doc/MERGING.md @@ -1,8 +1,8 @@ # Merging changes in Coq -This document describes how patches (submitted as pull requests -on the `master` branch) should be -merged into the main repository (https://github.com/coq/coq). +This document describes how patches, submitted as pull requests (PRs) on the +`master` branch, should be merged into the main repository +(https://github.com/coq/coq). ## Code owners @@ -10,8 +10,8 @@ The [CODEOWNERS](/.github/CODEOWNERS) file describes, for each part of the system, two owners. One is the principal maintainer of the component, the other is the secondary maintainer. -When a pull request is submitted, GitHub will automatically ask the principal -maintainer for a review. If the pull request touches several parts, all the +When a PR is submitted, GitHub will automatically ask the principal +maintainer for a review. If the PR touches several parts, all the corresponding principal maintainers will be asked for a review. Maintainers are never assigned as reviewer on their own PRs. @@ -43,10 +43,31 @@ A maintainer is expected to be reasonably reactive, but no specific timeframe is given for reviewing. (*) In case a component is touched in a trivial way (adding/removing one file in -a `Makefile`, etc), or by applying a systematic process (global renaming, -deprecationg propagation, etc) that has been reviewed globally, the assignee can +a `Makefile`, etc), or by applying a systematic refactoring process (global +renaming for instance) that has been reviewed globally, the assignee can say in a comment they think a review is not required and proceed with the merge. +### Breaking changes + +If the PR breaks compatibility of some external projects in CI, then fixes to +those external projects should have been prepared (cf. the relevant sub-section +in the [CI README](/dev/ci/README.md#Breaking-changes) and the PR can be tested +with these fixes thanks to ["overlays"](/dev/ci/user-overlays/README.md). + +Moreover the PR must absolutely update the [`CHANGES`](/CHANGES) file. + +If overlays are missing, ask the author to prepare them and label the PR with +the [needs: overlay](https://github.com/coq/coq/labels/needs%3A%20overlay) label. + +When fixes are ready, there are two cases to consider: + +- For patches that are backward compatible (best scenario), you should get the + external project maintainers to integrate them before merging the PR. +- For patches that are not backward compatible (which is often the case when + patching plugins after an update to the Coq API), you can proceed to merge + the PR and then notify the external project maintainers they can merge the + patch. + ## Merging Once all reviewers approved the PR, the assignee is expected to check that CI @@ -89,22 +110,6 @@ DON'T USE the GitHub interface for merging, since it will prevent the automated backport script from operating properly, generates bad commit messages, and a messy history when there are conflicts. -### What to do if the PR has overlays - -If the PR breaks compatibility of some developments in CI, then the author must -have prepared overlays for these developments (see [`dev/ci/README.md`](/dev/ci/README.md)) -and the PR must absolutely update the `CHANGES` file. - -There are two cases to consider: - -- If the patch is backward compatible (best scenario), then you should get - upstream maintainers to integrate it before merging the PR. -- If the patch is not backward compatible (which is often the case when - patching plugins after an update to the Coq API), then you can proceed to - merge the PR and then notify upstream they can merge the patch. This is a - less preferable scenario because it is probably going to create - spurious CI failures for unrelated PRs. - ### Merge script dependencies The merge script passes option `-S` to `git merge` to ensure merge commits diff --git a/dev/doc/changes.md b/dev/doc/changes.md index ff448abe8..774a77c8a 100644 --- a/dev/doc/changes.md +++ b/dev/doc/changes.md @@ -28,6 +28,13 @@ Proof engine should indicate what the canonical form is. An important change is the move of `Globnames.global_reference` to `Names.GlobRef.t`. +ML Libraries used by Coq + +- Introduction of a "Smart" module for collecting "smart*" functions, e.g. + Array.Smart.map. +- Uniformization of some names, e.g. Array.Smart.fold_left_map instead + of Array.smartfoldmap. + ### Unit testing The test suite now allows writing unit tests against OCaml code in the Coq diff --git a/dev/doc/release-process.md b/dev/doc/release-process.md new file mode 100644 index 000000000..1821a181f --- /dev/null +++ b/dev/doc/release-process.md @@ -0,0 +1,100 @@ +# Release process # + +## As soon as the previous version branched off master ## + +- [ ] Create a new issue to track the release process where you can copy-paste + the present checklist. +- [ ] Change the version name to the next major version and the magic numbers + (see [#7008](https://github.com/coq/coq/pull/7008/files)). +- [ ] Put the corresponding alpha tag using `git tag -s`. + The `VX.X+alpha` tag marks the first commit to be in `master` and not in the + branch of the previous version. +- [ ] Create the `X.X+beta1` milestone if it did not already exist. +- [ ] Decide the release calendar with the team (freeze date, beta date, final + release date) and put this information in the milestone (using the + description and due date fields). + +## About one month before the beta ## + +- [ ] Create the `X.X.0` milestone and set its due date. +- [ ] Send an announcement of the upcoming freeze on Coqdev and ask people to + remove from the beta milestone what they already know won't be ready on time + (possibly postponing to the `X.X.0` milestone for minor bug fixes, + infrastructure and documentation updates). +- [ ] Determine which issues should / must be fixed before the beta, add them + to the beta milestone, possibly with a + ["priority: blocker"](https://github.com/coq/coq/labels/priority%3A%20blocker) + label. Make sure that all these issues are assigned (and that the assignee + provides an ETA). +- [ ] Ping the development coordinator (**@mattam82**) to get him started on + the update to the Credits chapter of the reference manual. + See also [#7058](https://github.com/coq/coq/issues/7058). + The command to get the list of contributors for this version is + `git shortlog -s -n VX.X+alpha..master | cut -f2 | sort -k 2` + (the ordering is approximative as it will misplace people with middle names). + +## On the date of the feature freeze ## + +- [ ] Create the new version branch `vX.X` and + [protect it](https://github.com/coq/coq/settings/branches) + (activate the "Protect this branch", "Require pull request reviews before + merging" and "Restrict who can push to this branch" guards). +- [ ] Remove all remaining unmerged feature PRs from the beta milestone. +- [ ] Start a new project to track PR backporting. The proposed model is to + have a "X.X-only PRs" column for the rare PRs on the stable branch, a + "Request X.X inclusion" column for the PRs that were merged in `master` that + are to be considered for backporting, a "Waiting for CI" column to put the + PRs in the process of being backported, and "Shipped in ..." columns to put + what was backported. (The release manager is the person responsible for + merging PRs that target the version branch and backporting appropriate PRs + that are merged into `master`). + A message to **@coqbot** in the milestone description tells it to + automatically add merged PRs to the "Request X.X inclusion" column. +- [ ] Delay non-blocking issues to the appropriate milestone and ensure + blocking issues are solved. If required to solve some blocking issues, + it is possible to revert some feature PRs in the version branch only. + +## Before the beta release date ## + +- [ ] Ensure the Credits chapter has been updated. +- [ ] Ensure an empty `CompatXX.v` file has been created. +- [ ] Ensure that an appropriate version of the plugins we will distribute with + Coq has been tagged. +- [ ] Have some people test the recently auto-generated Windows and MacOS + packages. +- [ ] Change the version name from alpha to beta1 (see + [#7009](https://github.com/coq/coq/pull/7009/files)). + We generally do not update the magic numbers at this point. +- [ ] Put the `VX.X+beta1` tag using `git tag -s`. + +### These steps are the same for all releases (beta, final, patch-level) ### + +- [ ] Send an e-mail on Coqdev announcing that the tag has been put so that + package managers can start preparing package updates. +- [ ] Draft a release on GitHub. +- [ ] Get **@maximedenes** to sign the Windows and MacOS packages and + upload them on GitHub. +- [ ] Prepare a page of news on the website with the link to the GitHub release + (see [coq/www#63](https://github.com/coq/www/pull/63)). +- [ ] Upload the new version of the reference manual to the website. + *TODO: setup some continuous deployment for this.* +- [ ] Merge the website update, publish the release + and send annoucement e-mails. +- [ ] Ping **@Zimmi48** to publish a new version on Zenodo. + *TODO: automate this.* +- [ ] Close the milestone + +## At the final release time ## + +- [ ] Change the version name to X.X.0 and the magic numbers (see + [#7271](https://github.com/coq/coq/pull/7271/files)). +- [ ] Put the `VX.X.0` tag. + +Repeat the generic process documented above for all releases. + +- [ ] Switch the default version of the reference manual on the website. + +## At the patch-level release time ## + +We generally do not update the magic numbers at this point (see +[`2881a18`](https://github.com/coq/coq/commit/2881a18)). diff --git a/doc/sphinx/README.rst b/doc/sphinx/README.rst index 5f2f21f2b..3036fac81 100644 --- a/doc/sphinx/README.rst +++ b/doc/sphinx/README.rst @@ -22,6 +22,7 @@ Our Coq domain define multiple `objects`_. Each object has a *signature* (think matching :n:`@pattern` in the current goal. .. exn:: Too few occurrences + :undocumented: Objects are automatically collected into indices, and can be linked to using the role version of the object's directive. For example, you could link to the tactic variant above using ``:tacv:`simpl_at```, and to its exception using ``:exn:`Too few occurrences```. @@ -31,6 +32,8 @@ Names (link targets) are auto-generated for most simple objects, though they can - Vernacs (commands) have their name set to the first word of their signature. For example, the auto-generated name of ``Axiom @ident : @term`` is ``Axiom``, and a link to it would take the form ``:cmd:`Axiom```. - Vernac variants, tactic notations, and tactic variants do not have a default name. +Most objects should have a body (i.e. a block of indented text following the signature, called “contents” in Sphinx terms). Undocumented objects should have the `:undocumented:` flag instead, as shown above. + Notations --------- @@ -291,6 +294,64 @@ In addition to the objects and directives above, the ``coqrst`` Sphinx plugin de <http://www.sphinx-doc.org/en/stable/markup/para.html#directive-productionlist>`_ and reference its tokens using ``:token:`…```. +Common mistakes +=============== + +Improper nesting +---------------- + +DO + .. code:: + + .. cmd:: Foo @bar + + Foo the first instance of :token:`bar`\ s. + + .. cmdv:: Foo All + + Foo all the :token:`bar`\ s in + the current context + +DON'T + .. code:: + + .. cmd:: Foo @bar + + Foo the first instance of :token:`bar`\ s. + + .. cmdv:: Foo All + + Foo all the :token:`bar`\ s in + the current context + +You can set the ``report_undocumented_coq_objects`` setting in ``conf.py`` to ``"info"`` or ``"warning"`` to get a list of all Coq objects without a description. + +Overusing ``:token:`` +--------------------- + +DO + .. code:: + + This is equivalent to :n:`Axiom @ident : @term`. + +DON'T + .. code:: + + This is equivalent to ``Axiom`` :token`ident` : :token:`term`. + +Omitting annotations +-------------------- + +DO + .. code:: + + .. tacv:: assert @form as @intro_pattern + +DON'T + .. code:: + + .. tacv:: assert form as intro_pattern + Tips and tricks =============== diff --git a/doc/sphinx/README.template.rst b/doc/sphinx/README.template.rst index 203251abf..f90efa995 100644 --- a/doc/sphinx/README.template.rst +++ b/doc/sphinx/README.template.rst @@ -22,6 +22,7 @@ Our Coq domain define multiple `objects`_. Each object has a *signature* (think matching :n:`@pattern` in the current goal. .. exn:: Too few occurrences + :undocumented: Objects are automatically collected into indices, and can be linked to using the role version of the object's directive. For example, you could link to the tactic variant above using ``:tacv:`simpl_at```, and to its exception using ``:exn:`Too few occurrences```. @@ -31,6 +32,8 @@ Names (link targets) are auto-generated for most simple objects, though they can - Vernacs (commands) have their name set to the first word of their signature. For example, the auto-generated name of ``Axiom @ident : @term`` is ``Axiom``, and a link to it would take the form ``:cmd:`Axiom```. - Vernac variants, tactic notations, and tactic variants do not have a default name. +Most objects should have a body (i.e. a block of indented text following the signature, called “contents” in Sphinx terms). Undocumented objects should have the `:undocumented:` flag instead, as shown above. + Notations --------- @@ -83,6 +86,64 @@ In addition to the objects and directives above, the ``coqrst`` Sphinx plugin de [ROLES] +Common mistakes +=============== + +Improper nesting +---------------- + +DO + .. code:: + + .. cmd:: Foo @bar + + Foo the first instance of :token:`bar`\ s. + + .. cmdv:: Foo All + + Foo all the :token:`bar`\ s in + the current context + +DON'T + .. code:: + + .. cmd:: Foo @bar + + Foo the first instance of :token:`bar`\ s. + + .. cmdv:: Foo All + + Foo all the :token:`bar`\ s in + the current context + +You can set the ``report_undocumented_coq_objects`` setting in ``conf.py`` to ``"info"`` or ``"warning"`` to get a list of all Coq objects without a description. + +Overusing ``:token:`` +--------------------- + +DO + .. code:: + + This is equivalent to :n:`Axiom @ident : @term`. + +DON'T + .. code:: + + This is equivalent to ``Axiom`` :token`ident` : :token:`term`. + +Omitting annotations +-------------------- + +DO + .. code:: + + .. tacv:: assert @form as @intro_pattern + +DON'T + .. code:: + + .. tacv:: assert form as intro_pattern + Tips and tricks =============== diff --git a/doc/sphinx/biblio.bib b/doc/sphinx/biblio.bib index aeb45611e..3e988709c 100644 --- a/doc/sphinx/biblio.bib +++ b/doc/sphinx/biblio.bib @@ -3,47 +3,6 @@ @String{lnai = "Lecture Notes in Artificial Intelligence"} @String{SV = "{Sprin-ger-Verlag}"} -@InProceedings{Aud91, - author = {Ph. Audebaud}, - booktitle = {Proceedings of the sixth Conf. on Logic in Computer Science.}, - publisher = {IEEE}, - title = {Partial {Objects} in the {Calculus of Constructions}}, - year = {1991} -} - -@PhDThesis{Aud92, - author = {Ph. Audebaud}, - school = {{Universit\'e} Bordeaux I}, - title = {Extension du Calcul des Constructions par Points fixes}, - year = {1992} -} - -@InProceedings{Audebaud92b, - author = {Ph. Audebaud}, - booktitle = {{Proceedings of the 1992 Workshop on Types for Proofs and Programs}}, - editor = {{B. Nordstr\"om and K. Petersson and G. Plotkin}}, - note = {Also Research Report LIP-ENS-Lyon}, - pages = {21--34}, - title = {{CC+ : an extension of the Calculus of Constructions with fixpoints}}, - year = {1992} -} - -@InProceedings{Augustsson85, - author = {L. Augustsson}, - title = {{Compiling Pattern Matching}}, - booktitle = {Conference Functional Programming and -Computer Architecture}, - year = {1985} -} - -@Article{BaCo85, - author = {J.L. Bates and R.L. Constable}, - journal = {ACM transactions on Programming Languages and Systems}, - title = {Proofs as {Programs}}, - volume = {7}, - year = {1985} -} - @Book{Bar81, author = {H.P. Barendregt}, publisher = {North-Holland}, @@ -51,55 +10,6 @@ Computer Architecture}, year = {1981} } -@TechReport{Bar91, - author = {H. Barendregt}, - institution = {Catholic University Nijmegen}, - note = {In Handbook of Logic in Computer Science, Vol II}, - number = {91-19}, - title = {Lambda {Calculi with Types}}, - year = {1991} -} - -@Article{BeKe92, - author = {G. Bellin and J. Ketonen}, - journal = {Theoretical Computer Science}, - pages = {115--142}, - title = {A decision procedure revisited : Notes on direct logic, linear logic and its implementation}, - volume = {95}, - year = {1992} -} - -@Book{Bee85, - author = {M.J. Beeson}, - publisher = SV, - title = {Foundations of Constructive Mathematics, Metamathematical Studies}, - year = {1985} -} - -@Book{Bis67, - author = {E. Bishop}, - publisher = {McGraw-Hill}, - title = {Foundations of Constructive Analysis}, - year = {1967} -} - -@Book{BoMo79, - author = {R.S. Boyer and J.S. Moore}, - key = {BoMo79}, - publisher = {Academic Press}, - series = {ACM Monograph}, - title = {A computational logic}, - year = {1979} -} - -@MastersThesis{Bou92, - author = {S. Boutin}, - month = sep, - school = {{Universit\'e Paris 7}}, - title = {Certification d'un compilateur {ML en Coq}}, - year = {1992} -} - @InProceedings{Bou97, title = {Using reflection to build efficient and certified decision procedure s}, @@ -112,15 +22,6 @@ s}, year = {1997} } -@PhDThesis{Bou97These, - author = {S. Boutin}, - title = {R\'eflexions sur les quotients}, - school = {Paris 7}, - year = 1997, - type = {th\`ese d'Universit\'e}, - month = apr -} - @Article{Bru72, author = {N.J. de Bruijn}, journal = {Indag. Math.}, @@ -129,121 +30,6 @@ s}, year = {1972} } - -@InCollection{Bru80, - author = {N.J. de Bruijn}, - booktitle = {to H.B. Curry : Essays on Combinatory Logic, Lambda Calculus and Formalism.}, - editor = {J.P. Seldin and J.R. Hindley}, - publisher = {Academic Press}, - title = {A survey of the project {Automath}}, - year = {1980} -} - -@TechReport{COQ93, - author = {G. Dowek and A. Felty and H. Herbelin and G. Huet and C. Murthy and C. Parent and C. Paulin-Mohring and B. Werner}, - institution = {INRIA}, - month = may, - number = {154}, - title = {{The Coq Proof Assistant User's Guide Version 5.8}}, - year = {1993} -} - -@TechReport{COQ02, - author = {The Coq Development Team}, - institution = {INRIA}, - month = Feb, - number = {255}, - title = {{The Coq Proof Assistant Reference Manual Version 7.2}}, - year = {2002} -} - -@TechReport{CPar93, - author = {C. Parent}, - institution = {Ecole {Normale} {Sup\'erieure} de {Lyon}}, - month = oct, - note = {Also in~\cite{Nijmegen93}}, - number = {93-29}, - title = {Developing certified programs in the system {Coq}- {The} {Program} tactic}, - year = {1993} -} - -@PhDThesis{CPar95, - author = {C. Parent}, - school = {Ecole {Normale} {Sup\'erieure} de {Lyon}}, - title = {{Synth\`ese de preuves de programmes dans le Calcul des Constructions Inductives}}, - year = {1995} -} - -@Book{Caml, - author = {P. Weis and X. Leroy}, - publisher = {InterEditions}, - title = {Le langage Caml}, - year = {1993} -} - -@InProceedings{ChiPotSimp03, - author = {Laurent Chicli and Lo\"{\i}c Pottier and Carlos Simpson}, - title = {Mathematical Quotients and Quotient Types in Coq}, - booktitle = {TYPES}, - crossref = {DBLP:conf/types/2002}, - year = {2002} -} - -@TechReport{CoC89, - author = {Projet Formel}, - institution = {INRIA}, - number = {110}, - title = {{The Calculus of Constructions. Documentation and user's guide, Version 4.10}}, - year = {1989} -} - -@InProceedings{CoHu85a, - author = {Th. Coquand and G. Huet}, - address = {Linz}, - booktitle = {EUROCAL'85}, - publisher = SV, - series = LNCS, - title = {{Constructions : A Higher Order Proof System for Mechanizing Mathematics}}, - volume = {203}, - year = {1985} -} - -@InProceedings{CoHu85b, - author = {Th. Coquand and G. Huet}, - booktitle = {Logic Colloquium'85}, - editor = {The Paris Logic Group}, - publisher = {North-Holland}, - title = {{Concepts Math\'ematiques et Informatiques formalis\'es dans le Calcul des Constructions}}, - year = {1987} -} - -@Article{CoHu86, - author = {Th. Coquand and G. Huet}, - journal = {Information and Computation}, - number = {2/3}, - title = {The {Calculus of Constructions}}, - volume = {76}, - year = {1988} -} - -@InProceedings{CoPa89, - author = {Th. Coquand and C. Paulin-Mohring}, - booktitle = {Proceedings of Colog'88}, - editor = {P. Martin-L\"of and G. Mints}, - publisher = SV, - series = LNCS, - title = {Inductively defined types}, - volume = {417}, - year = {1990} -} - -@Book{Con86, - author = {R.L. {Constable et al.}}, - publisher = {Prentice-Hall}, - title = {{Implementing Mathematics with the Nuprl Proof Development System}}, - year = {1986} -} - @PhDThesis{Coq85, author = {Th. Coquand}, month = jan, @@ -261,24 +47,6 @@ s}, year = {1986} } -@InProceedings{Coq90, - author = {Th. Coquand}, - booktitle = {Logic and Computer Science}, - editor = {P. Oddifredi}, - note = {INRIA Research Report 1088, also in~\cite{CoC89}}, - publisher = {Academic Press}, - title = {{Metamathematical Investigations of a Calculus of Constructions}}, - year = {1990} -} - -@InProceedings{Coq91, - author = {Th. Coquand}, - booktitle = {Proceedings 9th Int. Congress of Logic, Methodology and Philosophy of Science}, - title = {{A New Paradox in Type Theory}}, - month = {August}, - year = {1991} -} - @InProceedings{Coq92, author = {Th. Coquand}, title = {{Pattern Matching with Dependent Types}}, @@ -286,49 +54,18 @@ s}, booktitle = {Proceedings of the 1992 Workshop on Types for Proofs and Programs} } -@InProceedings{Coquand93, - author = {Th. Coquand}, - booktitle = {Types for Proofs and Programs}, - editor = {H. Barendregt and T. Nipokow}, - publisher = SV, - series = LNCS, - title = {{Infinite objects in Type Theory}}, - volume = {806}, - year = {1993}, - pages = {62-78} -} - -@inproceedings{Corbineau08types, - author = {P. Corbineau}, - title = {A Declarative Language for the Coq Proof Assistant}, - editor = {M. Miculan and I. Scagnetto and F. Honsell}, - booktitle = {TYPES '07, Cividale del Friuli, Revised Selected Papers}, - publisher = {Springer}, - series = LNCS, - volume = {4941}, - year = {2007}, - pages = {69-84}, - ee = {http://dx.doi.org/10.1007/978-3-540-68103-8_5}, -} - -@PhDThesis{Cor97, - author = {C. Cornes}, - month = nov, - school = {{Universit\'e Paris 7}}, - title = {Conception d'un langage de haut niveau de représentation de preuves}, - type = {Th\`ese de Doctorat}, - year = {1997} -} - -@MastersThesis{Cou94a, - author = {J. Courant}, - month = sep, - school = {DEA d'Informatique, ENS Lyon}, - title = {Explicitation de preuves par r\'ecurrence implicite}, - year = {1994} +@InProceedings{DBLP:conf/types/CornesT95, + author = {Cristina Cornes and + Delphine Terrasse}, + title = {Automating Inversion of Inductive Predicates in Coq}, + booktitle = {TYPES}, + year = {1995}, + pages = {85-104}, + crossref = {DBLP:conf/types/1995}, + bibsource = {DBLP, http://dblp.uni-trier.de} } -@book{Cur58, +@Book{Cur58, author = {Haskell B. Curry and Robert Feys and William Craig}, title = {Combinatory Logic}, volume = 1, @@ -337,17 +74,40 @@ s}, note = {{\S{9E}}}, } -@InProceedings{Del99, - author = {Delahaye, D.}, - title = {Information Retrieval in a Coq Proof Library using - Type Isomorphisms}, - booktitle = {Proceedings of TYPES '99, L\"okeberg}, - publisher = SV, - series = lncs, - year = {1999}, - url = - "\\{\sf ftp://ftp.inria.fr/INRIA/Projects/coq/David.Delahaye/papers/}"# - "{\sf TYPES99-SIsos.ps.gz}" +@Article{CSlessadhoc, + author = {Gonthier, Georges and Ziliani, Beta and Nanevski, Aleksandar and Dreyer, Derek}, + title = {How to Make Ad Hoc Proof Automation Less Ad Hoc}, + journal = {SIGPLAN Not.}, + issue_date = {September 2011}, + volume = {46}, + number = {9}, + month = sep, + year = {2011}, + issn = {0362-1340}, + pages = {163--175}, + numpages = {13}, + url = {http://doi.acm.org/10.1145/2034574.2034798}, + doi = {10.1145/2034574.2034798}, + acmid = {2034798}, + publisher = {ACM}, + address = {New York, NY, USA}, + keywords = {canonical structures, coq, custom proof automation, hoare type theory, interactive theorem proving, tactics, type classes}, +} + +@InProceedings{CSwcu, + hal_id = {hal-00816703}, + url = {http://hal.inria.fr/hal-00816703}, + title = {{Canonical Structures for the working Coq user}}, + author = {Mahboubi, Assia and Tassi, Enrico}, + booktitle = {{ITP 2013, 4th Conference on Interactive Theorem Proving}}, + publisher = {Springer}, + pages = {19-34}, + address = {Rennes, France}, + volume = {7998}, + editor = {Sandrine Blazy and Christine Paulin and David Pichardie }, + series = {LNCS }, + doi = {10.1007/978-3-642-39634-2\_5 }, + year = {2013}, } @InProceedings{Del00, @@ -361,99 +121,7 @@ s}, pages = {85--95}, month = {November}, year = {2000}, - url = - "{\sf ftp://ftp.inria.fr/INRIA/Projects/coq/David.Delahaye/papers/}"# - "{\sf LPAR2000-ltac.ps.gz}" -} - -@InProceedings{DelMay01, - author = {Delahaye, D. and Mayero, M.}, - title = {{\tt Field}: une proc\'edure de d\'ecision pour les nombres r\'eels en {\Coq}}, - booktitle = {Journ\'ees Francophones des Langages Applicatifs, Pontarlier}, - publisher = {INRIA}, - month = {Janvier}, - year = {2001}, - url = - "\\{\sf ftp://ftp.inria.fr/INRIA/Projects/coq/David.Delahaye/papers/}"# - "{\sf JFLA2000-Field.ps.gz}" -} - -@TechReport{Dow90, - author = {G. Dowek}, - institution = {INRIA}, - number = {1283}, - title = {Naming and Scoping in a Mathematical Vernacular}, - type = {Research Report}, - year = {1990} -} - -@Article{Dow91a, - author = {G. Dowek}, - journal = {Compte-Rendus de l'Acad\'emie des Sciences}, - note = {The undecidability of Third Order Pattern Matching in Calculi with Dependent Types or Type Constructors}, - number = {12}, - pages = {951--956}, - title = {L'Ind\'ecidabilit\'e du Filtrage du Troisi\`eme Ordre dans les Calculs avec Types D\'ependants ou Constructeurs de Types}, - volume = {I, 312}, - year = {1991} -} - -@InProceedings{Dow91b, - author = {G. Dowek}, - booktitle = {Proceedings of Mathematical Foundation of Computer Science}, - note = {Also INRIA Research Report}, - pages = {151--160}, - publisher = SV, - series = LNCS, - title = {A Second Order Pattern Matching Algorithm in the Cube of Typed $\lambda$-calculi}, - volume = {520}, - year = {1991} -} - -@PhDThesis{Dow91c, - author = {G. Dowek}, - month = dec, - school = {Universit\'e Paris 7}, - title = {D\'emonstration automatique dans le Calcul des Constructions}, - year = {1991} -} - -@Article{Dow92a, - author = {G. Dowek}, - title = {The Undecidability of Pattern Matching in Calculi where Primitive Recursive Functions are Representable}, - year = 1993, - journal = {Theoretical Computer Science}, - volume = 107, - number = 2, - pages = {349-356} -} - -@Article{Dow94a, - author = {G. Dowek}, - journal = {Annals of Pure and Applied Logic}, - volume = {69}, - pages = {135--155}, - title = {Third order matching is decidable}, - year = {1994} -} - -@InProceedings{Dow94b, - author = {G. Dowek}, - booktitle = {Proceedings of the second international conference on typed lambda calculus and applications}, - title = {Lambda-calculus, Combinators and the Comprehension Schema}, - year = {1995} -} - -@InProceedings{Dyb91, - author = {P. Dybjer}, - booktitle = {Logical Frameworks}, - editor = {G. Huet and G. Plotkin}, - pages = {59--79}, - publisher = {Cambridge University Press}, - title = {Inductive sets and families in {Martin-Löf's} - Type Theory and their set-theoretic semantics: An inversion principle for {Martin-L\"of's} type theory}, - volume = {14}, - year = {1991} + url = {http://www.lirmm.fr/\%7Edelahaye/papers/ltac\%20(LPAR\%2700).pdf} } @Article{Dyc92, @@ -466,75 +134,6 @@ s}, year = {1992} } -@MastersThesis{Fil94, - author = {J.-C. Filli\^atre}, - month = sep, - school = {DEA d'Informatique, ENS Lyon}, - title = {Une proc\'edure de d\'ecision pour le Calcul des Pr\'edicats Direct. Étude et impl\'ementation dans le syst\`eme {\Coq}}, - year = {1994} -} - -@TechReport{Filliatre95, - author = {J.-C. Filli\^atre}, - institution = {LIP-ENS-Lyon}, - title = {A decision procedure for Direct Predicate Calculus}, - type = {Research report}, - number = {96--25}, - year = {1995} -} - -@Article{Filliatre03jfp, - author = {J.-C. Filliâtre}, - title = {Verification of Non-Functional Programs - using Interpretations in Type Theory}, - journal = jfp, - volume = 13, - number = 4, - pages = {709--745}, - month = jul, - year = 2003, - note = {[English translation of \cite{Filliatre99}]}, - url = {http://www.lri.fr/~filliatr/ftp/publis/jphd.ps.gz}, - topics = {team, lri}, - type_publi = {irevcomlec} -} - -@PhDThesis{Filliatre99, - author = {J.-C. Filli\^atre}, - title = {Preuve de programmes imp\'eratifs en th\'eorie des types}, - type = {Thèse de Doctorat}, - school = {Universit\'e Paris-Sud}, - year = 1999, - month = {July}, - url = {\url{http://www.lri.fr/~filliatr/ftp/publis/these.ps.gz}} -} - -@Unpublished{Filliatre99c, - author = {J.-C. Filli\^atre}, - title = {{Formal Proof of a Program: Find}}, - month = {January}, - year = 2000, - note = {Submitted to \emph{Science of Computer Programming}}, - url = {\url{http://www.lri.fr/~filliatr/ftp/publis/find.ps.gz}} -} - -@InProceedings{FilliatreMagaud99, - author = {J.-C. Filli\^atre and N. Magaud}, - title = {Certification of sorting algorithms in the system {\Coq}}, - booktitle = {Theorem Proving in Higher Order Logics: - Emerging Trends}, - year = 1999, - url = {\url{http://www.lri.fr/~filliatr/ftp/publis/Filliatre-Magaud.ps.gz}} -} - -@Unpublished{Fle90, - author = {E. Fleury}, - month = jul, - note = {Rapport de Stage}, - title = {Implantation des algorithmes de {Floyd et de Dijkstra} dans le {Calcul des Constructions}}, - year = {1990} -} - @Book{Fourier, author = {Jean-Baptiste-Joseph Fourier}, publisher = {Gauthier-Villars}, @@ -554,13 +153,6 @@ s}, year = {1994} } -@PhDThesis{Gim96, - author = {E. Gim\'enez}, - title = {Un calcul des constructions infinies et son application \'a la v\'erification de syst\`emes communicants}, - school = {\'Ecole Normale Sup\'erieure de Lyon}, - year = {1996} -} - @TechReport{Gim98, author = {E. Gim\'enez}, title = {A Tutorial on Recursive Types in Coq}, @@ -591,21 +183,6 @@ s}, year = {1995} } -@InProceedings{Gir70, - author = {J.-Y. Girard}, - booktitle = {Proceedings of the 2nd Scandinavian Logic Symposium}, - publisher = {North-Holland}, - title = {Une extension de l'interpr\'etation de {G\"odel} \`a l'analyse, et son application \`a l'\'elimination des coupures dans l'analyse et la th\'eorie des types}, - year = {1970} -} - -@PhDThesis{Gir72, - author = {J.-Y. Girard}, - school = {Universit\'e Paris~7}, - title = {Interpr\'etation fonctionnelle et \'elimination des coupures de l'arithm\'etique d'ordre sup\'erieur}, - year = {1972} -} - @Book{Gir89, author = {J.-Y. Girard and Y. Lafont and P. Taylor}, publisher = {Cambridge University Press}, @@ -614,32 +191,6 @@ s}, year = {1989} } -@TechReport{Har95, - author = {John Harrison}, - title = {Metatheory and Reflection in Theorem Proving: A Survey and Critique}, - institution = {SRI International Cambridge Computer Science Research Centre,}, - year = 1995, - type = {Technical Report}, - number = {CRC-053}, - abstract = {http://www.cl.cam.ac.uk/users/jrh/papers.html} -} - -@MastersThesis{Hir94, - author = {D. Hirschkoff}, - month = sep, - school = {DEA IARFA, Ecole des Ponts et Chauss\'ees, Paris}, - title = {Écriture d'une tactique arithm\'etique pour le syst\`eme {\Coq}}, - year = {1994} -} - -@InProceedings{HofStr98, - author = {Martin Hofmann and Thomas Streicher}, - title = {The groupoid interpretation of type theory}, - booktitle = {Proceedings of the meeting Twenty-five years of constructive type theory}, - publisher = {Oxford University Press}, - year = {1998} -} - @InCollection{How80, author = {W.A. Howard}, booktitle = {to H.B. Curry : Essays on Combinatory Logic, Lambda Calculus and Formalism.}, @@ -650,27 +201,6 @@ s}, year = {1980} } -@InProceedings{Hue87tapsoft, - author = {G. Huet}, - title = {Programming of Future Generation Computers}, - booktitle = {Proceedings of TAPSOFT87}, - series = LNCS, - volume = 249, - pages = {276--286}, - year = 1987, - publisher = SV -} - -@InProceedings{Hue87, - author = {G. Huet}, - booktitle = {Programming of Future Generation Computers}, - editor = {K. Fuchi and M. Nivat}, - note = {Also in \cite{Hue87tapsoft}}, - publisher = {Elsevier Science}, - title = {Induction Principles Formalized in the {Calculus of Constructions}}, - year = {1988} -} - @InProceedings{Hue88, author = {G. Huet}, booktitle = {A perspective in Theoretical Computer Science. Commemorative Volume for Gift Siromoney}, @@ -680,112 +210,17 @@ s}, year = {1989} } -@Unpublished{Hue88b, - author = {G. Huet}, - title = {Extending the Calculus of Constructions with Type:Type}, - year = 1988, - note = {Unpublished} -} - -@Book{Hue89, - editor = {G. Huet}, - publisher = {Addison-Wesley}, - series = {The UT Year of Programming Series}, - title = {Logical Foundations of Functional Programming}, - year = {1989} -} - -@InProceedings{Hue92, - author = {G. Huet}, - booktitle = {Proceedings of 12th FST/TCS Conference, New Delhi}, - pages = {229--240}, - publisher = SV, - series = LNCS, - title = {The Gallina Specification Language : A case study}, - volume = {652}, - year = {1992} -} - -@Article{Hue94, - author = {G. Huet}, - journal = {J. Functional Programming}, - pages = {371--394}, - publisher = {Cambridge University Press}, - title = {Residual theory in $\lambda$-calculus: a formal development}, - volume = {4,3}, - year = {1994} -} - -@InCollection{HuetLevy79, - author = {G. Huet and J.-J. L\'{e}vy}, - title = {Call by Need Computations in Non-Ambigous -Linear Term Rewriting Systems}, - note = {Also research report 359, INRIA, 1979}, - booktitle = {Computational Logic, Essays in Honor of -Alan Robinson}, - editor = {J.-L. Lassez and G. Plotkin}, - publisher = {The MIT press}, - year = {1991} -} - -@Article{KeWe84, - author = {J. Ketonen and R. Weyhrauch}, - journal = {Theoretical Computer Science}, - pages = {297--307}, - title = {A decidable fragment of {P}redicate {C}alculus}, - volume = {32}, - year = {1984} -} - -@Book{Kle52, - author = {S.C. Kleene}, - publisher = {North-Holland}, - series = {Bibliotheca Mathematica}, - title = {Introduction to Metamathematics}, - year = {1952} -} - -@Book{Kri90, - author = {J.-L. Krivine}, - publisher = {Masson}, - series = {Etudes et recherche en informatique}, - title = {Lambda-calcul {types et mod\`eles}}, - year = {1990} -} - -@Book{LE92, - editor = {G. Huet and G. Plotkin}, - publisher = {Cambridge University Press}, - title = {Logical Environments}, - year = {1992} -} - -@Book{LF91, - editor = {G. Huet and G. Plotkin}, - publisher = {Cambridge University Press}, - title = {Logical Frameworks}, - year = {1991} -} - -@Article{Laville91, - author = {A. Laville}, - title = {Comparison of Priority Rules in Pattern -Matching and Term Rewriting}, - journal = {Journal of Symbolic Computation}, - volume = {11}, - pages = {321--347}, - year = {1991} -} - -@InProceedings{LePa94, - author = {F. Leclerc and C. Paulin-Mohring}, - booktitle = {{Types for Proofs and Programs, Types' 93}}, - editor = {H. Barendregt and T. Nipkow}, - publisher = SV, - series = {LNCS}, - title = {{Programming with Streams in Coq. A case study : The Sieve of Eratosthenes}}, - volume = {806}, - year = {1994} +@Article{LeeWerner11, + author = {Gyesik Lee and + Benjamin Werner}, + title = {Proof-irrelevant model of {CC} with predicative induction + and judgmental equality}, + journal = {Logical Methods in Computer Science}, + volume = {7}, + number = {4}, + year = {2011}, + ee = {http://dx.doi.org/10.2168/LMCS-7(4:5)2011}, + bibsource = {DBLP, http://dblp.uni-trier.de} } @TechReport{Leroy90, @@ -805,14 +240,7 @@ Matching and Term Rewriting}, url = {draft at \url{http://www.irif.fr/~letouzey/download/extraction2002.pdf}} } -@PhDThesis{Luo90, - author = {Z. Luo}, - title = {An Extended Calculus of Constructions}, - school = {University of Edinburgh}, - year = {1990} -} - -@inproceedings{Luttik97specificationof, +@InProceedings{Luttik97specificationof, author = {Sebastiaan P. Luttik and Eelco Visser}, booktitle = {2nd International Workshop on the Theory and Practice of Algebraic Specifications (ASF+SDF'97), Electronic Workshops in Computing}, publisher = {Springer-Verlag}, @@ -820,92 +248,15 @@ Matching and Term Rewriting}, year = {1997} } -@Book{MaL84, - author = {{P. Martin-L\"of}}, - publisher = {Bibliopolis}, - series = {Studies in Proof Theory}, - title = {Intuitionistic Type Theory}, - year = {1984} -} - -@Article{MaSi94, - author = {P. Manoury and M. Simonot}, - title = {Automatizing Termination Proofs of Recursively Defined Functions.}, - journal = {TCS}, - volume = {135}, - number = {2}, - year = {1994}, - pages = {319-343}, -} - -@InProceedings{Miquel00, - author = {A. Miquel}, - title = {A Model for Impredicative Type Systems with Universes, -Intersection Types and Subtyping}, - booktitle = {{Proceedings of the 15th Annual IEEE Symposium on Logic in Computer Science (LICS'00)}}, - publisher = {IEEE Computer Society Press}, - year = {2000} -} - -@PhDThesis{Miquel01a, - author = {A. Miquel}, - title = {Le Calcul des Constructions implicite: syntaxe et s\'emantique}, - month = {dec}, - school = {{Universit\'e Paris 7}}, - year = {2001} -} - -@InProceedings{Miquel01b, - author = {A. Miquel}, - title = {The Implicit Calculus of Constructions: Extending Pure Type Systems with an Intersection Type Binder and Subtyping}, - booktitle = {{Proceedings of the fifth International Conference on Typed Lambda Calculi and Applications (TLCA01), Krakow, Poland}}, - publisher = SV, - series = {LNCS}, - number = 2044, - year = {2001} -} - -@InProceedings{MiWer02, - author = {A. Miquel and B. Werner}, - title = {The Not So Simple Proof-Irrelevant Model of CC}, - booktitle = {TYPES}, - year = {2002}, - pages = {240-258}, - ee = {http://link.springer.de/link/service/series/0558/bibs/2646/26460240.htm}, - crossref = {DBLP:conf/types/2002}, - bibsource = {DBLP, http://dblp.uni-trier.de} -} - -@proceedings{DBLP:conf/types/2002, - editor = {H. Geuvers and F. Wiedijk}, - title = {Types for Proofs and Programs, Second International Workshop, - TYPES 2002, Berg en Dal, The Netherlands, April 24-28, 2002, - Selected Papers}, - booktitle = {TYPES}, - publisher = SV, - series = LNCS, - volume = {2646}, - year = {2003}, - isbn = {3-540-14031-X}, - bibsource = {DBLP, http://dblp.uni-trier.de} -} - -@InProceedings{Moh89a, - author = {C. Paulin-Mohring}, - address = {Austin}, - booktitle = {Sixteenth Annual ACM Symposium on Principles of Programming Languages}, - month = jan, - publisher = {ACM}, - title = {Extracting ${F}_{\omega}$'s programs from proofs in the {Calculus of Constructions}}, - year = {1989} -} - -@PhDThesis{Moh89b, - author = {C. Paulin-Mohring}, - month = jan, - school = {{Universit\'e Paris 7}}, - title = {Extraction de programmes dans le {Calcul des Constructions}}, - year = {1989} +@InProceedings{DBLP:conf/types/McBride00, + author = {Conor McBride}, + title = {Elimination with a Motive}, + booktitle = {TYPES}, + year = {2000}, + pages = {197-216}, + ee = {http://link.springer.de/link/service/series/0558/bibs/2277/22770197.htm}, + crossref = {DBLP:conf/types/2000}, + bibsource = {DBLP, http://dblp.uni-trier.de} } @InProceedings{Moh93, @@ -920,14 +271,6 @@ Intersection Types and Subtyping}, year = {1993} } -@Book{Moh97, - author = {C. Paulin-Mohring}, - month = jan, - publisher = {{ENS Lyon}}, - title = {{Le syst\`eme Coq. \mbox{Th\`ese d'habilitation}}}, - year = {1997} -} - @MastersThesis{Mun94, author = {C. Muñoz}, month = sep, @@ -936,73 +279,6 @@ Intersection Types and Subtyping}, year = {1994} } -@PhDThesis{Mun97d, - author = {C. Mu{\~{n}}oz}, - title = {Un calcul de substitutions pour la repr\'esentation - de preuves partielles en th\'eorie de types}, - school = {Universit\'e Paris 7}, - year = {1997}, - note = {Version en anglais disponible comme rapport de - recherche INRIA RR-3309}, - type = {Th\`ese de Doctorat} -} - -@Book{NoPS90, - author = {B. {Nordstr\"om} and K. Peterson and J. Smith}, - booktitle = {Information Processing 83}, - publisher = {Oxford Science Publications}, - series = {International Series of Monographs on Computer Science}, - title = {Programming in {Martin-L\"of's} Type Theory}, - year = {1990} -} - -@Article{Nor88, - author = {B. {Nordstr\"om}}, - journal = {BIT}, - title = {Terminating General Recursion}, - volume = {28}, - year = {1988} -} - -@Book{Odi90, - editor = {P. Odifreddi}, - publisher = {Academic Press}, - title = {Logic and Computer Science}, - year = {1990} -} - -@InProceedings{PaMS92, - author = {M. Parigot and P. Manoury and M. Simonot}, - address = {St. Petersburg, Russia}, - booktitle = {Logic Programming and automated reasoning}, - editor = {A. Voronkov}, - month = jul, - number = {624}, - publisher = SV, - series = {LNCS}, - title = {{ProPre : A Programming language with proofs}}, - year = {1992} -} - -@Article{PaWe92, - author = {C. Paulin-Mohring and B. Werner}, - journal = {Journal of Symbolic Computation}, - pages = {607--640}, - title = {{Synthesis of ML programs in the system Coq}}, - volume = {15}, - year = {1993} -} - -@Article{Par92, - author = {M. Parigot}, - journal = {Theoretical Computer Science}, - number = {2}, - pages = {335--356}, - title = {{Recursive Programming with Proofs}}, - volume = {94}, - year = {1992} -} - @InProceedings{Parent95b, author = {C. Parent}, booktitle = {{Mathematics of Program Construction'95}}, @@ -1014,14 +290,16 @@ the Calculus of Inductive Constructions}}, year = {1995} } -@InProceedings{Prasad93, - author = {K.V. Prasad}, - booktitle = {{Proceedings of CONCUR'93}}, - publisher = SV, - series = {LNCS}, - title = {{Programming with broadcasts}}, - volume = {715}, - year = {1993} +@Misc{Pcoq, + author = {Lemme Team}, + title = {Pcoq a graphical user-interface for {Coq}}, + note = {\url{http://www-sop.inria.fr/lemme/pcoq/}} +} + +@Misc{ProofGeneral, + author = {David Aspinall}, + title = {Proof General}, + note = {\url{https://proofgeneral.github.io/}} } @Book{RC95, @@ -1034,15 +312,6 @@ the Calculus of Inductive Constructions}}, note = {ISBN-0-8176-3763-X} } -@TechReport{Rou92, - author = {J. Rouyer}, - institution = {INRIA}, - month = nov, - number = {1795}, - title = {{Développement de l'Algorithme d'Unification dans le Calcul des Constructions}}, - year = {1992} -} - @Article{Rushby98, title = {Subtypes for Specifications: Predicate Subtyping in {PVS}}, @@ -1055,115 +324,7 @@ the Calculus of Inductive Constructions}}, year = 1998 } -@TechReport{Saibi94, - author = {A. Sa\"{\i}bi}, - institution = {INRIA}, - month = dec, - number = {2345}, - title = {{Axiomatization of a lambda-calculus with explicit-substitutions in the Coq System}}, - year = {1994} -} - - -@MastersThesis{Ter92, - author = {D. Terrasse}, - month = sep, - school = {IARFA}, - title = {{Traduction de TYPOL en COQ. Application \`a Mini ML}}, - year = {1992} -} - -@TechReport{ThBeKa92, - author = {L. Th\'ery and Y. Bertot and G. Kahn}, - institution = {INRIA Sophia}, - month = may, - number = {1684}, - title = {Real theorem provers deserve real user-interfaces}, - type = {Research Report}, - year = {1992} -} - -@Book{TrDa89, - author = {A.S. Troelstra and D. van Dalen}, - publisher = {North-Holland}, - series = {Studies in Logic and the foundations of Mathematics, volumes 121 and 123}, - title = {Constructivism in Mathematics, an introduction}, - year = {1988} -} - -@PhDThesis{Wer94, - author = {B. Werner}, - school = {Universit\'e Paris 7}, - title = {Une th\'eorie des constructions inductives}, - type = {Th\`ese de Doctorat}, - year = {1994} -} - -@PhDThesis{Bar99, - author = {B. Barras}, - school = {Universit\'e Paris 7}, - title = {Auto-validation d'un système de preuves avec familles inductives}, - type = {Th\`ese de Doctorat}, - year = {1999} -} - -@Unpublished{ddr98, - author = {D. de Rauglaudre}, - title = {Camlp4 version 1.07.2}, - year = {1998}, - note = {In Camlp4 distribution} -} - -@Article{dowek93, - author = {G. Dowek}, - title = {{A Complete Proof Synthesis Method for the Cube of Type Systems}}, - journal = {Journal Logic Computation}, - volume = {3}, - number = {3}, - pages = {287--315}, - month = {June}, - year = {1993} -} - -@InProceedings{manoury94, - author = {P. Manoury}, - title = {{A User's Friendly Syntax to Define -Recursive Functions as Typed $\lambda-$Terms}}, - booktitle = {{Types for Proofs and Programs, TYPES'94}}, - series = {LNCS}, - volume = {996}, - month = jun, - year = {1994} -} - -@TechReport{maranget94, - author = {L. Maranget}, - institution = {INRIA}, - number = {2385}, - title = {{Two Techniques for Compiling Lazy Pattern Matching}}, - year = {1994} -} - -@InProceedings{puel-suarez90, - author = {L.Puel and A. Su\'arez}, - booktitle = {{Conference Lisp and Functional Programming}}, - series = {ACM}, - publisher = SV, - title = {{Compiling Pattern Matching by Term -Decomposition}}, - year = {1990} -} - -@MastersThesis{saidi94, - author = {H. Saidi}, - month = sep, - school = {DEA d'Informatique Fondamentale, Universit\'e Paris 7}, - title = {R\'esolution d'\'equations dans le syst\`eme T - de G\"odel}, - year = {1994} -} - -@inproceedings{sozeau06, +@InProceedings{sozeau06, author = {Matthieu Sozeau}, title = {Subset Coercions in {C}oq}, year = {2007}, @@ -1174,7 +335,7 @@ Decomposition}}, series = {LNCS} } -@inproceedings{sozeau08, +@InProceedings{sozeau08, Author = {Matthieu Sozeau and Nicolas Oury}, booktitle = {TPHOLs'08}, Pdf = {http://www.lri.fr/~sozeau/research/publications/drafts/classes.pdf}, @@ -1182,87 +343,7 @@ Decomposition}}, Year = {2008}, } -@Misc{streicher93semantical, - author = {T. Streicher}, - title = {Semantical Investigations into Intensional Type Theory}, - note = {Habilitationsschrift, LMU Munchen.}, - year = {1993} -} - -@Misc{Pcoq, - author = {Lemme Team}, - title = {Pcoq a graphical user-interface for {Coq}}, - note = {\url{http://www-sop.inria.fr/lemme/pcoq/}} -} - -@Misc{ProofGeneral, - author = {David Aspinall}, - title = {Proof General}, - note = {\url{https://proofgeneral.github.io/}} -} - -@InCollection{wadler87, - author = {P. Wadler}, - title = {Efficient Compilation of Pattern Matching}, - booktitle = {The Implementation of Functional Programming -Languages}, - editor = {S.L. Peyton Jones}, - publisher = {Prentice-Hall}, - year = {1987} -} - -@inproceedings{DBLP:conf/types/CornesT95, - author = {Cristina Cornes and - Delphine Terrasse}, - title = {Automating Inversion of Inductive Predicates in Coq}, - booktitle = {TYPES}, - year = {1995}, - pages = {85-104}, - crossref = {DBLP:conf/types/1995}, - bibsource = {DBLP, http://dblp.uni-trier.de} -} -@proceedings{DBLP:conf/types/1995, - editor = {Stefano Berardi and - Mario Coppo}, - title = {Types for Proofs and Programs, International Workshop TYPES'95, - Torino, Italy, June 5-8, 1995, Selected Papers}, - booktitle = {TYPES}, - publisher = {Springer}, - series = {Lecture Notes in Computer Science}, - volume = {1158}, - year = {1996}, - isbn = {3-540-61780-9}, - bibsource = {DBLP, http://dblp.uni-trier.de} -} - -@inproceedings{DBLP:conf/types/McBride00, - author = {Conor McBride}, - title = {Elimination with a Motive}, - booktitle = {TYPES}, - year = {2000}, - pages = {197-216}, - ee = {http://link.springer.de/link/service/series/0558/bibs/2277/22770197.htm}, - crossref = {DBLP:conf/types/2000}, - bibsource = {DBLP, http://dblp.uni-trier.de} -} - -@proceedings{DBLP:conf/types/2000, - editor = {Paul Callaghan and - Zhaohui Luo and - James McKinna and - Robert Pollack}, - title = {Types for Proofs and Programs, International Workshop, TYPES - 2000, Durham, UK, December 8-12, 2000, Selected Papers}, - booktitle = {TYPES}, - publisher = {Springer}, - series = {Lecture Notes in Computer Science}, - volume = {2277}, - year = {2002}, - isbn = {3-540-43287-6}, - bibsource = {DBLP, http://dblp.uni-trier.de} -} - -@INPROCEEDINGS{sugar, +@InProceedings{sugar, author = {Alessandro Giovini and Teo Mora and Gianfranco Niesi and Lorenzo Robbiano and Carlo Traverso}, title = {"One sugar cube, please" or Selection strategies in the Buchberger algorithm}, booktitle = { Proceedings of the ISSAC'91, ACM Press}, @@ -1271,38 +352,7 @@ Languages}, publisher = {} } -@article{LeeWerner11, - author = {Gyesik Lee and - Benjamin Werner}, - title = {Proof-irrelevant model of {CC} with predicative induction - and judgmental equality}, - journal = {Logical Methods in Computer Science}, - volume = {7}, - number = {4}, - year = {2011}, - ee = {http://dx.doi.org/10.2168/LMCS-7(4:5)2011}, - bibsource = {DBLP, http://dblp.uni-trier.de} -} - -@Comment{cross-references, must be at end} - -@Book{Bastad92, - editor = {B. Nordstr\"om and K. Petersson and G. Plotkin}, - publisher = {Available by ftp at site ftp.inria.fr}, - title = {Proceedings of the 1992 Workshop on Types for Proofs and Programs}, - year = {1992} -} - -@Book{Nijmegen93, - editor = {H. Barendregt and T. Nipkow}, - publisher = SV, - series = LNCS, - title = {Types for Proofs and Programs}, - volume = {806}, - year = {1994} -} - -@article{TheOmegaPaper, +@Article{TheOmegaPaper, author = "W. Pugh", title = "The Omega test: a fast and practical integer programming algorithm for dependence analysis", journal = "Communication of the ACM", @@ -1310,43 +360,15 @@ Languages}, year = "1992", } -@inproceedings{CSwcu, - hal_id = {hal-00816703}, - url = {http://hal.inria.fr/hal-00816703}, - title = {{Canonical Structures for the working Coq user}}, - author = {Mahboubi, Assia and Tassi, Enrico}, - booktitle = {{ITP 2013, 4th Conference on Interactive Theorem Proving}}, - publisher = {Springer}, - pages = {19-34}, - address = {Rennes, France}, - volume = {7998}, - editor = {Sandrine Blazy and Christine Paulin and David Pichardie }, - series = {LNCS }, - doi = {10.1007/978-3-642-39634-2\_5 }, - year = {2013}, -} - -@article{CSlessadhoc, - author = {Gonthier, Georges and Ziliani, Beta and Nanevski, Aleksandar and Dreyer, Derek}, - title = {How to Make Ad Hoc Proof Automation Less Ad Hoc}, - journal = {SIGPLAN Not.}, - issue_date = {September 2011}, - volume = {46}, - number = {9}, - month = sep, - year = {2011}, - issn = {0362-1340}, - pages = {163--175}, - numpages = {13}, - url = {http://doi.acm.org/10.1145/2034574.2034798}, - doi = {10.1145/2034574.2034798}, - acmid = {2034798}, - publisher = {ACM}, - address = {New York, NY, USA}, - keywords = {canonical structures, coq, custom proof automation, hoare type theory, interactive theorem proving, tactics, type classes}, +@PhDThesis{Wer94, + author = {B. Werner}, + school = {Universit\'e Paris 7}, + title = {Une th\'eorie des constructions inductives}, + type = {Th\`ese de Doctorat}, + year = {1994} } -@inproceedings{CompiledStrongReduction, +@InProceedings{CompiledStrongReduction, author = {Benjamin Gr{\'{e}}goire and Xavier Leroy}, editor = {Mitchell Wand and @@ -1365,7 +387,7 @@ Languages}, bibsource = {dblp computer science bibliography, http://dblp.org} } -@inproceedings{FullReduction, +@InProceedings{FullReduction, author = {Mathieu Boespflug and Maxime D{\'{e}}n{\`{e}}s and Benjamin Gr{\'{e}}goire}, diff --git a/doc/sphinx/conf.py b/doc/sphinx/conf.py index 1f7dd9d68..f65400e88 100755 --- a/doc/sphinx/conf.py +++ b/doc/sphinx/conf.py @@ -51,6 +51,10 @@ extensions = [ 'coqrst.coqdomain' ] +# Change this to "info" or "warning" to get notifications about undocumented Coq +# objects (objects with no contents). +report_undocumented_coq_objects = None + # Add any paths that contain templates here, relative to this directory. templates_path = ['_templates'] diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index 3835524f0..da4c3f9d7 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -2398,35 +2398,35 @@ simply :g:`t=u` dropping the implicit type of :g:`t` and :g:`u`. .. tacn:: rewrite @term :name: rewrite -This tactic applies to any goal. The type of :n:`@term` must have the form + This tactic applies to any goal. The type of :token:`term` must have the form -``forall (x``:sub:`1` ``:A``:sub:`1` ``) ... (x``:sub:`n` ``:A``:sub:`n` ``). eq term``:sub:`1` ``term``:sub:`2` ``.`` + ``forall (x``:sub:`1` ``:A``:sub:`1` ``) ... (x``:sub:`n` ``:A``:sub:`n` ``). eq term``:sub:`1` ``term``:sub:`2` ``.`` -where :g:`eq` is the Leibniz equality or a registered setoid equality. + where :g:`eq` is the Leibniz equality or a registered setoid equality. -Then :n:`rewrite @term` finds the first subterm matching `term`\ :sub:`1` in the goal, -resulting in instances `term`:sub:`1`' and `term`:sub:`2`' and then -replaces every occurrence of `term`:subscript:`1`' by `term`:subscript:`2`'. -Hence, some of the variables :g:`x`\ :sub:`i` are solved by unification, -and some of the types :g:`A`\ :sub:`1`:g:`, ..., A`\ :sub:`n` become new -subgoals. + Then :n:`rewrite @term` finds the first subterm matching `term`\ :sub:`1` in the goal, + resulting in instances `term`:sub:`1`' and `term`:sub:`2`' and then + replaces every occurrence of `term`:subscript:`1`' by `term`:subscript:`2`'. + Hence, some of the variables :g:`x`\ :sub:`i` are solved by unification, + and some of the types :g:`A`\ :sub:`1`:g:`, ..., A`\ :sub:`n` become new + subgoals. -.. exn:: The @term provided does not end with an equation. + .. exn:: The @term provided does not end with an equation. -.. exn:: Tactic generated a subgoal identical to the original goal. This happens if @term does not occur in the goal. + .. exn:: Tactic generated a subgoal identical to the original goal. This happens if @term does not occur in the goal. -.. tacv:: rewrite -> @term + .. tacv:: rewrite -> @term - Is equivalent to :n:`rewrite @term` + Is equivalent to :n:`rewrite @term` -.. tacv:: rewrite <- @term + .. tacv:: rewrite <- @term - Uses the equality :n:`@term`:sub:`1` :n:`= @term` :sub:`2` from right to left + Uses the equality :n:`@term`:sub:`1` :n:`= @term` :sub:`2` from right to left -.. tacv:: rewrite @term in clause + .. tacv:: rewrite @term in clause - Analogous to :n:`rewrite @term` but rewriting is done following clause - (similarly to :ref:`performing computations <performingcomputations>`). For instance: + Analogous to :n:`rewrite @term` but rewriting is done following clause + (similarly to :ref:`performing computations <performingcomputations>`). For instance: + :n:`rewrite H in H`:sub:`1` will rewrite `H` in the hypothesis `H`:sub:`1` instead of the current goal. @@ -2440,136 +2440,128 @@ subgoals. + :n:`rewrite H in *` is a combination of :n:`rewrite H` and :n:`rewrite H in * |-` that succeeds if at least one of these two tactics succeeds. - Orientation :g:`->` or :g:`<-` can be inserted before the :n:`@term` to rewrite. + Orientation :g:`->` or :g:`<-` can be inserted before the :token:`term` to rewrite. -.. tacv:: rewrite @term at occurrences + .. tacv:: rewrite @term at occurrences - Rewrite only the given occurrences of :n:`@term`. Occurrences are - specified from left to right as for pattern (:tacn:`pattern`). The rewrite is - always performed using setoid rewriting, even for Leibniz’s equality, so one - has to ``Import Setoid`` to use this variant. + Rewrite only the given occurrences of :token:`term`. Occurrences are + specified from left to right as for pattern (:tacn:`pattern`). The rewrite is + always performed using setoid rewriting, even for Leibniz’s equality, so one + has to ``Import Setoid`` to use this variant. -.. tacv:: rewrite @term by tactic + .. tacv:: rewrite @term by tactic - Use tactic to completely solve the side-conditions arising from the - :tacn:`rewrite`. + Use tactic to completely solve the side-conditions arising from the + :tacn:`rewrite`. -.. tacv:: rewrite {+ @term} + .. tacv:: rewrite {+, @term} - Is equivalent to the `n` successive tactics :n:`{+ rewrite @term}`, each one - working on the first subgoal generated by the previous one. Orientation - :g:`->` or :g:`<-` can be inserted before each :n:`@term` to rewrite. One - unique clause can be added at the end after the keyword in; it will then - affect all rewrite operations. + Is equivalent to the `n` successive tactics :n:`{+; rewrite @term}`, each one + working on the first subgoal generated by the previous one. Orientation + :g:`->` or :g:`<-` can be inserted before each :token:`term` to rewrite. One + unique clause can be added at the end after the keyword in; it will then + affect all rewrite operations. - In all forms of rewrite described above, a :n:`@term` to rewrite can be - immediately prefixed by one of the following modifiers: + In all forms of rewrite described above, a :token:`term` to rewrite can be + immediately prefixed by one of the following modifiers: - + `?` : the tactic rewrite :n:`?@term` performs the rewrite of :n:`@term` as many - times as possible (perhaps zero time). This form never fails. - + `n?` : works similarly, except that it will do at most `n` rewrites. - + `!` : works as ?, except that at least one rewrite should succeed, otherwise - the tactic fails. - + `n!` (or simply `n`) : precisely `n` rewrites of :n:`@term` will be done, - leading to failure if these n rewrites are not possible. + + `?` : the tactic :n:`rewrite ?@term` performs the rewrite of :token:`term` as many + times as possible (perhaps zero time). This form never fails. + + :n:`@num?` : works similarly, except that it will do at most :token:`num` rewrites. + + `!` : works as `?`, except that at least one rewrite should succeed, otherwise + the tactic fails. + + :n:`@num!` (or simply :n:`@num`) : precisely :token:`num` rewrites of :token:`term` will be done, + leading to failure if these :token:`num` rewrites are not possible. -.. tacv:: erewrite @term - :name: erewrite + .. tacv:: erewrite @term + :name: erewrite - This tactic works as :n:`rewrite @term` but turning - unresolved bindings into existential variables, if any, instead of - failing. It has the same variants as :tacn:`rewrite` has. + This tactic works as :n:`rewrite @term` but turning + unresolved bindings into existential variables, if any, instead of + failing. It has the same variants as :tacn:`rewrite` has. -.. tacn:: replace @term with @term +.. tacn:: replace @term with @term’ :name: replace This tactic applies to any goal. It replaces all free occurrences of :n:`@term` - in the current goal with :n:`@term` and generates the equality :n:`@term = - @term` as a subgoal. This equality is automatically solved if it occurs among - the assumption, or if its symmetric form occurs. It is equivalent to - :n:`cut @term = @term; [intro H`:sub:`n` :n:`; rewrite <- H`:sub:`n` :n:`; clear H`:sub:`n`:n:`|| assumption || symmetry; try assumption]`. + in the current goal with :n:`@term’` and generates an equality :n:`@term = @term’` + as a subgoal. This equality is automatically solved if it occurs among + the assumptions, or if its symmetric form occurs. It is equivalent to + :n:`cut @term = @term’; [intro H`:sub:`n` :n:`; rewrite <- H`:sub:`n` :n:`; clear H`:sub:`n`:n:`|| assumption || symmetry; try assumption]`. -.. exn:: @terms do not have convertible types. + .. exn:: Terms do not have convertible types. -.. tacv:: replace @term with @term by tactic + .. tacv:: replace @term with @term’ by @tactic - This acts as :n:`replace @term` with :n:`@term` but applies tactic to solve the generated - subgoal :n:`@term = @term`. + This acts as :n:`replace @term with @term’` but applies :token:`tactic` to solve the generated + subgoal :n:`@term = @term’`. -.. tacv:: replace @term + .. tacv:: replace @term - Replaces :n:`@term` with :n:`@term’` using the first assumption whose type has - the form :n:`@term = @term’` or :n:`@term’ = @term`. + Replaces :n:`@term` with :n:`@term’` using the first assumption whose type has + the form :n:`@term = @term’` or :n:`@term’ = @term`. -.. tacv:: replace -> @term + .. tacv:: replace -> @term - Replaces :n:`@term` with :n:`@term’` using the first assumption whose type has - the form :n:`@term = @term’` + Replaces :n:`@term` with :n:`@term’` using the first assumption whose type has + the form :n:`@term = @term’` -.. tacv:: replace <- @term + .. tacv:: replace <- @term - Replaces :n:`@term` with :n:`@term’` using the first assumption whose type has - the form :n:`@term’ = @term` + Replaces :n:`@term` with :n:`@term’` using the first assumption whose type has + the form :n:`@term’ = @term` -.. tacv:: replace @term with @term in clause -.. tacv:: replace @term with @term in clause by tactic -.. tacv:: replace @term in clause replace -> @term in clause -.. tacv:: replace <- @term in clause + .. tacv:: replace @term {? with @term} in clause {? by @tactic} + .. tacv:: replace -> @term in clause + .. tacv:: replace <- @term in clause - Acts as before but the replacements take place inclause (see - :ref:`performingcomputations`) and not only in the conclusion of the goal. The - clause argument must not contain any type of nor value of. + Acts as before but the replacements take place in the specified clause (see + :ref:`performingcomputations`) and not only in the conclusion of the goal. The + clause argument must not contain any ``type of`` nor ``value of``. -.. tacv:: cutrewrite <- (@term = @term) - :cutrewrite: + .. tacv:: cutrewrite <- (@term = @term’) + :name: cutrewrite - This tactic is deprecated. It acts like :n:`replace @term with @term`, or, - equivalently as :n:`enough (@term = @term) as <-`. + This tactic is deprecated. It can be replaced by :n:`enough (@term = @term’) as <-`. -.. tacv:: cutrewrite -> (@term = @term) + .. tacv:: cutrewrite -> (@term = @term’) - This tactic is deprecated. It can be replaced by enough :n:`(@term = @term) as ->`. + This tactic is deprecated. It can be replaced by :n:`enough (@term = @term’) as ->`. .. tacn:: subst @ident :name: subst + This tactic applies to a goal that has :n:`@ident` in its context and (at + least) one hypothesis, say :g:`H`, of type :n:`@ident = t` or :n:`t = @ident` + with :n:`@ident` not occurring in :g:`t`. Then it replaces :n:`@ident` by + :g:`t` everywhere in the goal (in the hypotheses and in the conclusion) and + clears :n:`@ident` and :g:`H` from the context. -This tactic applies to a goal that has :n:`@ident` in its context and (at -least) one hypothesis, say :g:`H`, of type :n:`@ident = t` or :n:`t = @ident` -with :n:`@ident` not occurring in :g:`t`. Then it replaces :n:`@ident` by -:g:`t` everywhere in the goal (in the hypotheses and in the conclusion) and -clears :n:`@ident` and :g:`H` from the context. - -If :n:`@ident` is a local definition of the form :n:`@ident := t`, it is also -unfolded and cleared. - - -.. note:: - When several hypotheses have the form :n:`@ident = t` or :n:`t = @ident`, the - first one is used. - - -.. note:: - If `H` is itself dependent in the goal, it is replaced by the proof of - reflexivity of equality. + If :n:`@ident` is a local definition of the form :n:`@ident := t`, it is also + unfolded and cleared. + .. note:: + + When several hypotheses have the form :n:`@ident = t` or :n:`t = @ident`, the + first one is used. -.. tacv:: subst {+ @ident} + + If :g:`H` is itself dependent in the goal, it is replaced by the proof of + reflexivity of equality. - This is equivalent to :n:`subst @ident`:sub:`1`:n:`; ...; subst @ident`:sub:`n`. + .. tacv:: subst {+ @ident} -.. tacv:: subst + This is equivalent to :n:`subst @ident`:sub:`1`:n:`; ...; subst @ident`:sub:`n`. - This applies subst repeatedly from top to bottom to all identifiers of the - context for which an equality of the form :n:`@ident = t` or :n:`t = @ident` - or :n:`@ident := t` exists, with :n:`@ident` not occurring in `t`. + .. tacv:: subst + This applies subst repeatedly from top to bottom to all identifiers of the + context for which an equality of the form :n:`@ident = t` or :n:`t = @ident` + or :n:`@ident := t` exists, with :n:`@ident` not occurring in ``t``. .. opt:: Regular Subst Tactic This option controls the behavior of :tacn:`subst`. When it is - activated, :tacn:`subst` also deals with the following corner cases: + activated (it is by default), :tacn:`subst` also deals with the following corner cases: + A context with ordered hypotheses :n:`@ident`:sub:`1` :n:`= @ident`:sub:`2` and :n:`@ident`:sub:`1` :n:`= t`, or :n:`t′ = @ident`:sub:`1`` with `t′` not @@ -2587,41 +2579,40 @@ unfolded and cleared. unfolded which otherwise it would exceptionally unfold in configurations containing hypotheses of the form :n:`@ident = u`, or :n:`u′ = @ident` with `u′` not a variable. Finally, it preserves the initial order of - hypotheses, which without the option it may break. The option is on by + hypotheses, which without the option it may break. default. .. tacn:: stepl @term :name: stepl + This tactic is for chaining rewriting steps. It assumes a goal of the + form :n:`R @term @term` where ``R`` is a binary relation and relies on a + database of lemmas of the form :g:`forall x y z, R x y -> eq x z -> R z y` + where `eq` is typically a setoid equality. The application of :n:`stepl @term` + then replaces the goal by :n:`R @term @term` and adds a new goal stating + :n:`eq @term @term`. -This tactic is for chaining rewriting steps. It assumes a goal of the -form :n:`R @term @term` where `R` is a binary relation and relies on a -database of lemmas of the form :g:`forall x y z, R x y -> eq x z -> R z y` -where `eq` is typically a setoid equality. The application of :n:`stepl @term` -then replaces the goal by :n:`R @term @term` and adds a new goal stating -:n:`eq @term @term`. + .. cmd:: Declare Left Step @term -.. cmd:: Declare Left Step @term + Adds :n:`@term` to the database used by :tacn:`stepl`. - Adds :n:`@term` to the database used by :tacn:`stepl`. + The tactic is especially useful for parametric setoids which are not accepted + as regular setoids for :tacn:`rewrite` and :tacn:`setoid_replace` (see + :ref:`Generalizedrewriting`). -The tactic is especially useful for parametric setoids which are not accepted -as regular setoids for :tacn:`rewrite` and :tacn:`setoid_replace` (see -:ref:`Generalizedrewriting`). + .. tacv:: stepl @term by @tactic -.. tacv:: stepl @term by tactic + This applies :n:`stepl @term` then applies :token:`tactic` to the second goal. - This applies :n:`stepl @term` then applies tactic to the second goal. + .. tacv:: stepr @term stepr @term by tactic + :name: stepr -.. tacv:: stepr @term stepr @term by tactic - :name: stepr + This behaves as :tacn:`stepl` but on the right-hand-side of the binary + relation. Lemmas are expected to be of the form + :g:`forall x y z, R x y -> eq y z -> R x z`. - This behaves as :tacn:`stepl` but on the right-hand-side of the binary - relation. Lemmas are expected to be of the form :g:`forall x y z, R x y -> eq - y z -> R x z`. - - .. cmd:: Declare Right Step @term + .. cmd:: Declare Right Step @term Adds :n:`@term` to the database used by :tacn:`stepr`. @@ -2634,28 +2625,25 @@ as regular setoids for :tacn:`rewrite` and :tacn:`setoid_replace` (see with `U` providing that `U` is well-formed and that `T` and `U` are convertible. -.. exn:: Not convertible. - + .. exn:: Not convertible. -.. tacv:: change @term with @term + .. tacv:: change @term with @term’ - This replaces the occurrences of :n:`@term` by :n:`@term` in the current goal. - The term :n:`@term` and :n:`@term` must be convertible. + This replaces the occurrences of :n:`@term` by :n:`@term’` in the current goal. + The term :n:`@term` and :n:`@term’` must be convertible. -.. tacv:: change @term at {+ @num} with @term + .. tacv:: change @term at {+ @num} with @term’ - This replaces the occurrences numbered :n:`{+ @num}` of :n:`@term by @term` - in the current goal. The terms :n:`@term` and :n:`@term` must be convertible. + This replaces the occurrences numbered :n:`{+ @num}` of :n:`@term` by :n:`@term’` + in the current goal. The terms :n:`@term` and :n:`@term’` must be convertible. -.. exn:: Too few occurrences. + .. exn:: Too few occurrences. -.. tacv:: change @term in @ident -.. tacv:: change @term with @term in @ident -.. tacv:: change @term at {+ @num} with @term in @ident + .. tacv:: change @term {? {? at {+ @num}} with @term} in @ident - This applies the change tactic not to the goal but to the hypothesis :n:`@ident`. + This applies the :tacn:`change` tactic not to the goal but to the hypothesis :n:`@ident`. -See also: :ref:`Performing computations <performingcomputations>` + .. seealso:: :ref:`Performing computations <performingcomputations>` .. _performingcomputations: @@ -3434,7 +3422,7 @@ The general command to add a hint to some databases :n:`{+ @ident}` is Adds each :n:`Hint Unfold @ident`. .. cmdv:: Hint %( Transparent %| Opaque %) @qualid - :name: Hint %( Transparent %| Opaque %) + :name: Hint ( Transparent | Opaque ) This adds a transparency hint to the database, making :n:`@qualid` a transparent or opaque constant during resolution. This information is used diff --git a/doc/tools/coqrst/coqdoc/main.py b/doc/tools/coqrst/coqdoc/main.py index a004959eb..cedd60d3b 100644 --- a/doc/tools/coqrst/coqdoc/main.py +++ b/doc/tools/coqrst/coqdoc/main.py @@ -40,7 +40,7 @@ def coqdoc(coq_code, coqdoc_bin=None): os.write(fd, COQDOC_HEADER.encode("utf-8")) os.write(fd, coq_code.encode("utf-8")) os.close(fd) - return check_output([coqdoc_bin] + COQDOC_OPTIONS + [filename], timeout = 2).decode("utf-8") + return check_output([coqdoc_bin] + COQDOC_OPTIONS + [filename], timeout = 10).decode("utf-8") finally: os.remove(filename) diff --git a/doc/tools/coqrst/coqdomain.py b/doc/tools/coqrst/coqdomain.py index 606d725bf..8d6e23764 100644 --- a/doc/tools/coqrst/coqdomain.py +++ b/doc/tools/coqrst/coqdomain.py @@ -97,8 +97,10 @@ class CoqObject(ObjectDescription): raise NotImplementedError(self) option_spec = { - # One can give an explicit name to each documented object - 'name': directives.unchanged + # Explicit object naming + 'name': directives.unchanged, + # Silence warnings produced by report_undocumented_coq_objects + 'undocumented': directives.flag } def _subdomain(self): @@ -160,6 +162,24 @@ class CoqObject(ObjectDescription): self._add_index_entry(name, target) return target + def _warn_if_undocumented(self): + document = self.state.document + config = document.settings.env.config + report = config.report_undocumented_coq_objects + if report and not self.content and "undocumented" not in self.options: + # This is annoyingly convoluted, but we don't want to raise warnings + # or interrupt the generation of the current node. For more details + # see https://github.com/sphinx-doc/sphinx/issues/4976. + msg = 'No contents in directive {}'.format(self.name) + node = document.reporter.info(msg, line=self.lineno) + getLogger(__name__).info(node.astext()) + if report == "warning": + raise self.warning(msg) + + def run(self): + self._warn_if_undocumented() + return super().run() + class PlainObject(CoqObject): """A base class for objects whose signatures should be rendered literally.""" def _render_signature(self, signature, signode): @@ -1036,4 +1056,7 @@ def setup(app): app.add_stylesheet("notations.css") app.add_stylesheet("pre-text.css") + # Tell Sphinx about extra settings + app.add_config_value("report_undocumented_coq_objects", None, 'env') + return {'version': '0.1', "parallel_read_safe": True} diff --git a/engine/eConstr.ml b/engine/eConstr.ml index 2ab545612..f1530b2d1 100644 --- a/engine/eConstr.ml +++ b/engine/eConstr.ml @@ -285,7 +285,7 @@ let map sigma f c = match kind sigma c with else mkLetIn (na, b', t', k') | App (b,l) -> let b' = f b in - let l' = Array.smartmap f l in + let l' = Array.Smart.map f l in if b'==b && l'==l then c else mkApp (b', l') | Proj (p,t) -> @@ -293,23 +293,23 @@ let map sigma f c = match kind sigma c with if t' == t then c else mkProj (p, t') | Evar (e,l) -> - let l' = Array.smartmap f l in + let l' = Array.Smart.map f l in if l'==l then c else mkEvar (e, l') | Case (ci,p,b,bl) -> let b' = f b in let p' = f p in - let bl' = Array.smartmap f bl in + let bl' = Array.Smart.map f bl in if b'==b && p'==p && bl'==bl then c else mkCase (ci, p', b', bl') | Fix (ln,(lna,tl,bl)) -> - let tl' = Array.smartmap f tl in - let bl' = Array.smartmap f bl in + let tl' = Array.Smart.map f tl in + let bl' = Array.Smart.map f bl in if tl'==tl && bl'==bl then c else mkFix (ln,(lna,tl',bl')) | CoFix(ln,(lna,tl,bl)) -> - let tl' = Array.smartmap f tl in - let bl' = Array.smartmap f bl in + let tl' = Array.Smart.map f tl in + let bl' = Array.Smart.map f bl in if tl'==tl && bl'==bl then c else mkCoFix (ln,(lna,tl',bl')) @@ -339,7 +339,7 @@ let map_with_binders sigma g f l c0 = match kind sigma c0 with else mkLetIn (na, b', t', c') | App (c, al) -> let c' = f l c in - let al' = CArray.Fun1.smartmap f l al in + let al' = Array.Fun1.Smart.map f l al in if c' == c && al' == al then c0 else mkApp (c', al') | Proj (p, t) -> @@ -347,25 +347,25 @@ let map_with_binders sigma g f l c0 = match kind sigma c0 with if t' == t then c0 else mkProj (p, t') | Evar (e, al) -> - let al' = CArray.Fun1.smartmap f l al in + let al' = Array.Fun1.Smart.map f l al in if al' == al then c0 else mkEvar (e, al') | Case (ci, p, c, bl) -> let p' = f l p in let c' = f l c in - let bl' = CArray.Fun1.smartmap f l bl in + let bl' = Array.Fun1.Smart.map f l bl in if p' == p && c' == c && bl' == bl then c0 else mkCase (ci, p', c', bl') | Fix (ln, (lna, tl, bl)) -> - let tl' = CArray.Fun1.smartmap f l tl in + let tl' = Array.Fun1.Smart.map f l tl in let l' = iterate g (Array.length tl) l in - let bl' = CArray.Fun1.smartmap f l' bl in + let bl' = Array.Fun1.Smart.map f l' bl in if tl' == tl && bl' == bl then c0 else mkFix (ln,(lna,tl',bl')) | CoFix(ln,(lna,tl,bl)) -> - let tl' = CArray.Fun1.smartmap f l tl in + let tl' = Array.Fun1.Smart.map f l tl in let l' = iterate g (Array.length tl) l in - let bl' = CArray.Fun1.smartmap f l' bl in + let bl' = Array.Fun1.Smart.map f l' bl in mkCoFix (ln,(lna,tl',bl')) let iter sigma f c = match kind sigma c with @@ -391,9 +391,9 @@ let iter_with_full_binders sigma g f n c = | Prod (na,t,c) -> f n t; f (g (LocalAssum (na, t)) n) c | Lambda (na,t,c) -> f n t; f (g (LocalAssum (na, t)) n) c | LetIn (na,b,t,c) -> f n b; f n t; f (g (LocalDef (na, b, t)) n) c - | App (c,l) -> f n c; CArray.Fun1.iter f n l - | Evar (_,l) -> CArray.Fun1.iter f n l - | Case (_,p,c,bl) -> f n p; f n c; CArray.Fun1.iter f n bl + | App (c,l) -> f n c; Array.Fun1.iter f n l + | Evar (_,l) -> Array.Fun1.iter f n l + | Case (_,p,c,bl) -> f n p; f n c; Array.Fun1.iter f n bl | Proj (p,c) -> f n c | Fix (_,(lna,tl,bl)) -> Array.iter (f n) tl; diff --git a/engine/evarutil.ml b/engine/evarutil.ml index cb2d01bdf..38ceed569 100644 --- a/engine/evarutil.ml +++ b/engine/evarutil.ml @@ -214,7 +214,7 @@ let mk_new_meta () = EConstr.mkMeta(new_meta()) let non_instantiated sigma = let listev = Evd.undefined_map sigma in - Evar.Map.smartmap (fun evi -> nf_evar_info sigma evi) listev + Evar.Map.Smart.map (fun evi -> nf_evar_info sigma evi) listev (************************) (* Manipulating filters *) diff --git a/engine/evd.ml b/engine/evd.ml index 03b843655..78d5d4c8f 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -510,8 +510,8 @@ let raw_map f d = in ans in - let defn_evars = EvMap.smartmapi f d.defn_evars in - let undf_evars = EvMap.smartmapi f d.undf_evars in + let defn_evars = EvMap.Smart.mapi f d.defn_evars in + let undf_evars = EvMap.Smart.mapi f d.undf_evars in { d with defn_evars; undf_evars; } let raw_map_undefined f d = @@ -524,7 +524,7 @@ let raw_map_undefined f d = in ans in - { d with undf_evars = EvMap.smartmapi f d.undf_evars; } + { d with undf_evars = EvMap.Smart.mapi f d.undf_evars; } let is_evar = mem @@ -1040,11 +1040,11 @@ let map_metas_fvalue f evd = | Clval(id,(c,s),typ) -> Clval(id,(mk_freelisted (f c.rebus),s),typ) | x -> x in - set_metas evd (Metamap.smartmap map evd.metas) + set_metas evd (Metamap.Smart.map map evd.metas) let map_metas f evd = let map cl = map_clb f cl in - set_metas evd (Metamap.smartmap map evd.metas) + set_metas evd (Metamap.Smart.map map evd.metas) let meta_opt_fvalue evd mv = match Metamap.find mv evd.metas with @@ -1120,7 +1120,7 @@ let retract_coercible_metas evd = Cltyp (na, typ) | v -> v in - let metas = Metamap.smartmapi map evd.metas in + let metas = Metamap.Smart.mapi map evd.metas in !mc, set_metas evd metas let evar_source_of_meta mv evd = diff --git a/engine/termops.ml b/engine/termops.ml index c271d9d99..053fcc3db 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -931,7 +931,7 @@ let dependent_main noevar sigma m t = match EConstr.kind sigma m, EConstr.kind sigma t with | App (fm,lm), App (ft,lt) when Array.length lm < Array.length lt -> deprec m (mkApp (ft,Array.sub lt 0 (Array.length lm))); - CArray.Fun1.iter deprec m + Array.Fun1.iter deprec m (Array.sub lt (Array.length lm) ((Array.length lt) - (Array.length lm))) | _, Cast (c,_,_) when noevar && isMeta sigma c -> () diff --git a/interp/impargs.ml b/interp/impargs.ml index 7e4c4ef4f..2db67c299 100644 --- a/interp/impargs.ml +++ b/interp/impargs.ml @@ -538,7 +538,7 @@ let subst_implicits_decl subst (r,imps as o) = let r' = fst (subst_global subst r) in if r==r' then o else (r',imps) let subst_implicits (subst,(req,l)) = - (ImplLocal,List.smartmap (subst_implicits_decl subst) l) + (ImplLocal,List.Smart.map (subst_implicits_decl subst) l) let impls_of_context ctx = let map (decl, impl) = match impl with diff --git a/interp/notation.ml b/interp/notation.ml index e6df7b96c..192c477be 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -741,7 +741,7 @@ let subst_arguments_scope (subst,(req,r,n,scl,cls)) = match subst_scope_class subst cl with | Some cl' as ocl' when cl' != cl -> ocl' | _ -> ocl in - let cls' = List.smartmap subst_cl cls in + let cls' = List.Smart.map subst_cl cls in (ArgsScopeNoDischarge,r',n,scl,cls') let discharge_arguments_scope (_,(req,r,n,l,_)) = diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index b806dce0b..e51c69136 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -521,7 +521,7 @@ let rec subst_pat subst pat = | PatVar _ -> pat | PatCstr (((kn,i),j),cpl,n) -> let kn' = subst_mind subst kn - and cpl' = List.smartmap (subst_pat subst) cpl in + and cpl' = List.Smart.map (subst_pat subst) cpl in if kn' == kn && cpl' == cpl then pat else DAst.make ?loc:pat.CAst.loc @@ PatCstr (((kn',i),j),cpl',n) @@ -536,7 +536,7 @@ let rec subst_notation_constr subst bound raw = | NApp (r,rl) -> let r' = subst_notation_constr subst bound r - and rl' = List.smartmap (subst_notation_constr subst bound) rl in + and rl' = List.Smart.map (subst_notation_constr subst bound) rl in if r' == r && rl' == rl then raw else NApp(r',rl') @@ -566,14 +566,14 @@ let rec subst_notation_constr subst bound raw = | NLetIn (n,r1,t,r2) -> let r1' = subst_notation_constr subst bound r1 in - let t' = Option.smartmap (subst_notation_constr subst bound) t in + let t' = Option.Smart.map (subst_notation_constr subst bound) t in let r2' = subst_notation_constr subst bound r2 in if r1' == r1 && t == t' && r2' == r2 then raw else NLetIn (n,r1',t',r2') | NCases (sty,rtntypopt,rl,branches) -> - let rtntypopt' = Option.smartmap (subst_notation_constr subst bound) rtntypopt - and rl' = List.smartmap + let rtntypopt' = Option.Smart.map (subst_notation_constr subst bound) rtntypopt + and rl' = List.Smart.map (fun (a,(n,signopt) as x) -> let a' = subst_notation_constr subst bound a in let signopt' = Option.map (fun ((indkn,i),nal as z) -> @@ -581,9 +581,9 @@ let rec subst_notation_constr subst bound raw = if indkn == indkn' then z else ((indkn',i),nal)) signopt in if a' == a && signopt' == signopt then x else (a',(n,signopt'))) rl - and branches' = List.smartmap + and branches' = List.Smart.map (fun (cpl,r as branch) -> - let cpl' = List.smartmap (subst_pat subst) cpl + let cpl' = List.Smart.map (subst_pat subst) cpl and r' = subst_notation_constr subst bound r in if cpl' == cpl && r' == r then branch else (cpl',r')) @@ -594,14 +594,14 @@ let rec subst_notation_constr subst bound raw = NCases (sty,rtntypopt',rl',branches') | NLetTuple (nal,(na,po),b,c) -> - let po' = Option.smartmap (subst_notation_constr subst bound) po + let po' = Option.Smart.map (subst_notation_constr subst bound) po and b' = subst_notation_constr subst bound b and c' = subst_notation_constr subst bound c in if po' == po && b' == b && c' == c then raw else NLetTuple (nal,(na,po'),b',c') | NIf (c,(na,po),b1,b2) -> - let po' = Option.smartmap (subst_notation_constr subst bound) po + let po' = Option.Smart.map (subst_notation_constr subst bound) po and b1' = subst_notation_constr subst bound b1 and b2' = subst_notation_constr subst bound b2 and c' = subst_notation_constr subst bound c in @@ -610,12 +610,12 @@ let rec subst_notation_constr subst bound raw = | NRec (fk,idl,dll,tl,bl) -> let dll' = - Array.smartmap (List.smartmap (fun (na,oc,b as x) -> - let oc' = Option.smartmap (subst_notation_constr subst bound) oc in + Array.Smart.map (List.Smart.map (fun (na,oc,b as x) -> + let oc' = Option.Smart.map (subst_notation_constr subst bound) oc in let b' = subst_notation_constr subst bound b in if oc' == oc && b' == b then x else (na,oc',b'))) dll in - let tl' = Array.smartmap (subst_notation_constr subst bound) tl in - let bl' = Array.smartmap (subst_notation_constr subst bound) bl in + let tl' = Array.Smart.map (subst_notation_constr subst bound) tl in + let bl' = Array.Smart.map (subst_notation_constr subst bound) bl in if dll' == dll && tl' == tl && bl' == bl then raw else NRec (fk,idl,dll',tl',bl') @@ -628,7 +628,7 @@ let rec subst_notation_constr subst bound raw = if nref == ref then knd else Evar_kinds.ImplicitArg (nref, i, b) | _ -> knd in - let nsolve = Option.smartmap (Genintern.generic_substitute subst) solve in + let nsolve = Option.Smart.map (Genintern.generic_substitute subst) solve in if nsolve == solve && nknd == knd then raw else NHole (nknd, naming, nsolve) diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml index 08114abc4..435cf0a79 100644 --- a/kernel/cClosure.ml +++ b/kernel/cClosure.ml @@ -482,7 +482,7 @@ let rec lft_fconstr n ft = let lift_fconstr k f = if Int.equal k 0 then f else lft_fconstr k f let lift_fconstr_vect k v = - if Int.equal k 0 then v else CArray.Fun1.map lft_fconstr k v + if Int.equal k 0 then v else Array.Fun1.map lft_fconstr k v let clos_rel e i = match expand_rel i e with @@ -547,7 +547,7 @@ let mk_clos_vect env v = match v with | [|v0; v1; v2|] -> [|mk_clos env v0; mk_clos env v1; mk_clos env v2|] | [|v0; v1; v2; v3|] -> [|mk_clos env v0; mk_clos env v1; mk_clos env v2; mk_clos env v3|] -| v -> CArray.Fun1.map mk_clos env v +| v -> Array.Fun1.map mk_clos env v (* Translate the head constructor of t from constr to fconstr. This function is parameterized by the function to apply on the direct @@ -562,7 +562,7 @@ let mk_clos_deep clos_fun env t = term = FCast (clos_fun env a, k, clos_fun env b)} | App (f,v) -> { norm = Red; - term = FApp (clos_fun env f, CArray.Fun1.map clos_fun env v) } + term = FApp (clos_fun env f, Array.Fun1.map clos_fun env v) } | Proj (p,c) -> { norm = Red; term = FProj (p, clos_fun env c) } @@ -605,21 +605,21 @@ let rec to_constr constr_fun lfts v = Array.map (fun b -> constr_fun lfts (mk_clos env b)) ve) | FFix ((op,(lna,tys,bds)),e) -> let n = Array.length bds in - let ftys = CArray.Fun1.map mk_clos e tys in - let fbds = CArray.Fun1.map mk_clos (subs_liftn n e) bds in + let ftys = Array.Fun1.map mk_clos e tys in + let fbds = Array.Fun1.map mk_clos (subs_liftn n e) bds in let lfts' = el_liftn n lfts in - mkFix (op, (lna, CArray.Fun1.map constr_fun lfts ftys, - CArray.Fun1.map constr_fun lfts' fbds)) + mkFix (op, (lna, Array.Fun1.map constr_fun lfts ftys, + Array.Fun1.map constr_fun lfts' fbds)) | FCoFix ((op,(lna,tys,bds)),e) -> let n = Array.length bds in - let ftys = CArray.Fun1.map mk_clos e tys in - let fbds = CArray.Fun1.map mk_clos (subs_liftn n e) bds in + let ftys = Array.Fun1.map mk_clos e tys in + let fbds = Array.Fun1.map mk_clos (subs_liftn n e) bds in let lfts' = el_liftn (Array.length bds) lfts in - mkCoFix (op, (lna, CArray.Fun1.map constr_fun lfts ftys, - CArray.Fun1.map constr_fun lfts' fbds)) + mkCoFix (op, (lna, Array.Fun1.map constr_fun lfts ftys, + Array.Fun1.map constr_fun lfts' fbds)) | FApp (f,ve) -> mkApp (constr_fun lfts f, - CArray.Fun1.map constr_fun lfts ve) + Array.Fun1.map constr_fun lfts ve) | FProj (p,c) -> mkProj (p,constr_fun lfts c) @@ -1024,14 +1024,14 @@ and norm_head info tab m = | FProd(na,dom,rng) -> mkProd(na, kl info tab dom, kl info tab rng) | FCoFix((n,(na,tys,bds)),e) -> - let ftys = CArray.Fun1.map mk_clos e tys in + let ftys = Array.Fun1.map mk_clos e tys in let fbds = - CArray.Fun1.map mk_clos (subs_liftn (Array.length na) e) bds in + Array.Fun1.map mk_clos (subs_liftn (Array.length na) e) bds in mkCoFix(n,(na, CArray.map (kl info tab) ftys, CArray.map (kl info tab) fbds)) | FFix((n,(na,tys,bds)),e) -> - let ftys = CArray.Fun1.map mk_clos e tys in + let ftys = Array.Fun1.map mk_clos e tys in let fbds = - CArray.Fun1.map mk_clos (subs_liftn (Array.length na) e) bds in + Array.Fun1.map mk_clos (subs_liftn (Array.length na) e) bds in mkFix(n,(na, CArray.map (kl info tab) ftys, CArray.map (kl info tab) fbds)) | FEvar((i,args),env) -> mkEvar(i, Array.map (fun a -> kl info tab (mk_clos env a)) args) diff --git a/kernel/cClosure.mli b/kernel/cClosure.mli index e2f5a3b82..63daa4a7c 100644 --- a/kernel/cClosure.mli +++ b/kernel/cClosure.mli @@ -239,9 +239,6 @@ val lift_fconstr_vect : int -> fconstr array -> fconstr array val mk_clos : fconstr subs -> constr -> fconstr val mk_clos_vect : fconstr subs -> constr array -> fconstr array -val mk_clos_deep : - (fconstr subs -> constr -> fconstr) -> - fconstr subs -> constr -> fconstr val kni: clos_infos -> fconstr infos_tab -> fconstr -> stack -> fconstr * stack val knr: clos_infos -> fconstr infos_tab -> fconstr -> stack -> fconstr * stack diff --git a/kernel/clambda.ml b/kernel/clambda.ml index 641d424e2..0727eaeac 100644 --- a/kernel/clambda.ml +++ b/kernel/clambda.ml @@ -152,7 +152,7 @@ let rec map_lam_with_binders g f n lam = match lam with | Lrel _ | Lvar _ | Lconst _ | Lval _ | Lsort _ | Lind _ -> lam | Levar (evk, args) -> - let args' = Array.smartmap (f n) args in + let args' = Array.Smart.map (f n) args in if args == args' then lam else Levar (evk, args') | Lprod(dom,codom) -> let dom' = f n dom in @@ -167,19 +167,19 @@ let rec map_lam_with_binders g f n lam = if body == body' && def == def' then lam else Llet(id,def',body') | Lapp(fct,args) -> let fct' = f n fct in - let args' = Array.smartmap (f n) args in + let args' = Array.Smart.map (f n) args in if fct == fct' && args == args' then lam else mkLapp fct' args' | Lcase(ci,rtbl,t,a,branches) -> let const = branches.constant_branches in let nonconst = branches.nonconstant_branches in let t' = f n t in let a' = f n a in - let const' = Array.smartmap (f n) const in + let const' = Array.Smart.map (f n) const in let on_b b = let (ids,body) = b in let body' = f (g (Array.length ids) n) body in if body == body' then b else (ids,body') in - let nonconst' = Array.smartmap on_b nonconst in + let nonconst' = Array.Smart.map on_b nonconst in let branches' = if const == const' && nonconst == nonconst' then branches @@ -190,20 +190,20 @@ let rec map_lam_with_binders g f n lam = if t == t' && a == a' && branches == branches' then lam else Lcase(ci,rtbl,t',a',branches') | Lfix(init,(ids,ltypes,lbodies)) -> - let ltypes' = Array.smartmap (f n) ltypes in - let lbodies' = Array.smartmap (f (g (Array.length ids) n)) lbodies in + let ltypes' = Array.Smart.map (f n) ltypes in + let lbodies' = Array.Smart.map (f (g (Array.length ids) n)) lbodies in if ltypes == ltypes' && lbodies == lbodies' then lam else Lfix(init,(ids,ltypes',lbodies')) | Lcofix(init,(ids,ltypes,lbodies)) -> - let ltypes' = Array.smartmap (f n) ltypes in - let lbodies' = Array.smartmap (f (g (Array.length ids) n)) lbodies in + let ltypes' = Array.Smart.map (f n) ltypes in + let lbodies' = Array.Smart.map (f (g (Array.length ids) n)) lbodies in if ltypes == ltypes' && lbodies == lbodies' then lam else Lcofix(init,(ids,ltypes',lbodies')) | Lmakeblock(tag,args) -> - let args' = Array.smartmap (f n) args in + let args' = Array.Smart.map (f n) args in if args == args' then lam else Lmakeblock(tag,args') | Lprim(kn,ar,op,args) -> - let args' = Array.smartmap (f n) args in + let args' = Array.Smart.map (f n) args in if args == args' then lam else Lprim(kn,ar,op,args') | Lproj(i,kn,arg) -> let arg' = f n arg in @@ -216,7 +216,7 @@ and map_uint g f n u = match u with | UintVal _ -> u | UintDigits(args) -> - let args' = Array.smartmap (f n) args in + let args' = Array.Smart.map (f n) args in if args == args' then u else UintDigits(args') | UintDecomp(a) -> let a' = f n a in @@ -250,7 +250,7 @@ let rec lam_exsubst subst lam = let lam_subst_args subst args = if is_subs_id subst then args - else Array.smartmap (lam_exsubst subst) args + else Array.Smart.map (lam_exsubst subst) args (** Simplification of lambda expression *) @@ -316,7 +316,7 @@ and simplify_app substf f substa args = simplify_app substf f subst_id args | _ -> mkLapp (simplify substf f) (simplify_args substa args) -and simplify_args subst args = Array.smartmap (simplify subst) args +and simplify_args subst args = Array.Smart.map (simplify subst) args and reduce_lapp substf lids body substa largs = match lids, largs with diff --git a/kernel/constr.ml b/kernel/constr.ml index bc486210d..8f83d6baa 100644 --- a/kernel/constr.ml +++ b/kernel/constr.ml @@ -468,16 +468,16 @@ let iter_with_binders g f n c = match kind c with | Prod (_,t,c) -> f n t; f (g n) c | Lambda (_,t,c) -> f n t; f (g n) c | LetIn (_,b,t,c) -> f n b; f n t; f (g n) c - | App (c,l) -> f n c; CArray.Fun1.iter f n l - | Evar (_,l) -> CArray.Fun1.iter f n l - | Case (_,p,c,bl) -> f n p; f n c; CArray.Fun1.iter f n bl + | App (c,l) -> f n c; Array.Fun1.iter f n l + | Evar (_,l) -> Array.Fun1.iter f n l + | Case (_,p,c,bl) -> f n p; f n c; Array.Fun1.iter f n bl | Proj (p,c) -> f n c | Fix (_,(_,tl,bl)) -> - CArray.Fun1.iter f n tl; - CArray.Fun1.iter f (iterate g (Array.length tl) n) bl + Array.Fun1.iter f n tl; + Array.Fun1.iter f (iterate g (Array.length tl) n) bl | CoFix (_,(_,tl,bl)) -> - CArray.Fun1.iter f n tl; - CArray.Fun1.iter f (iterate g (Array.length tl) n) bl + Array.Fun1.iter f n tl; + Array.Fun1.iter f (iterate g (Array.length tl) n) bl (* [map f c] maps [f] on the immediate subterms of [c]; it is not recursive and the order with which subterms are processed is @@ -509,7 +509,7 @@ let map f c = match kind c with else mkLetIn (na, b', t', k') | App (b,l) -> let b' = f b in - let l' = Array.smartmap f l in + let l' = Array.Smart.map f l in if b'==b && l'==l then c else mkApp (b', l') | Proj (p,t) -> @@ -517,23 +517,23 @@ let map f c = match kind c with if t' == t then c else mkProj (p, t') | Evar (e,l) -> - let l' = Array.smartmap f l in + let l' = Array.Smart.map f l in if l'==l then c else mkEvar (e, l') | Case (ci,p,b,bl) -> let b' = f b in let p' = f p in - let bl' = Array.smartmap f bl in + let bl' = Array.Smart.map f bl in if b'==b && p'==p && bl'==bl then c else mkCase (ci, p', b', bl') | Fix (ln,(lna,tl,bl)) -> - let tl' = Array.smartmap f tl in - let bl' = Array.smartmap f bl in + let tl' = Array.Smart.map f tl in + let bl' = Array.Smart.map f bl in if tl'==tl && bl'==bl then c else mkFix (ln,(lna,tl',bl')) | CoFix(ln,(lna,tl,bl)) -> - let tl' = Array.smartmap f tl in - let bl' = Array.smartmap f bl in + let tl' = Array.Smart.map f tl in + let bl' = Array.Smart.map f bl in if tl'==tl && bl'==bl then c else mkCoFix (ln,(lna,tl',bl')) @@ -565,7 +565,7 @@ let fold_map f accu c = match kind c with else accu, mkLetIn (na, b', t', k') | App (b,l) -> let accu, b' = f accu b in - let accu, l' = Array.smartfoldmap f accu l in + let accu, l' = Array.Smart.fold_left_map f accu l in if b'==b && l'==l then accu, c else accu, mkApp (b', l') | Proj (p,t) -> @@ -573,23 +573,23 @@ let fold_map f accu c = match kind c with if t' == t then accu, c else accu, mkProj (p, t') | Evar (e,l) -> - let accu, l' = Array.smartfoldmap f accu l in + let accu, l' = Array.Smart.fold_left_map f accu l in if l'==l then accu, c else accu, mkEvar (e, l') | Case (ci,p,b,bl) -> let accu, b' = f accu b in let accu, p' = f accu p in - let accu, bl' = Array.smartfoldmap f accu bl in + let accu, bl' = Array.Smart.fold_left_map f accu bl in if b'==b && p'==p && bl'==bl then accu, c else accu, mkCase (ci, p', b', bl') | Fix (ln,(lna,tl,bl)) -> - let accu, tl' = Array.smartfoldmap f accu tl in - let accu, bl' = Array.smartfoldmap f accu bl in + let accu, tl' = Array.Smart.fold_left_map f accu tl in + let accu, bl' = Array.Smart.fold_left_map f accu bl in if tl'==tl && bl'==bl then accu, c else accu, mkFix (ln,(lna,tl',bl')) | CoFix(ln,(lna,tl,bl)) -> - let accu, tl' = Array.smartfoldmap f accu tl in - let accu, bl' = Array.smartfoldmap f accu bl in + let accu, tl' = Array.Smart.fold_left_map f accu tl in + let accu, bl' = Array.Smart.fold_left_map f accu bl in if tl'==tl && bl'==bl then accu, c else accu, mkCoFix (ln,(lna,tl',bl')) @@ -625,7 +625,7 @@ let map_with_binders g f l c0 = match kind c0 with else mkLetIn (na, b', t', c') | App (c, al) -> let c' = f l c in - let al' = CArray.Fun1.smartmap f l al in + let al' = Array.Fun1.Smart.map f l al in if c' == c && al' == al then c0 else mkApp (c', al') | Proj (p, t) -> @@ -633,25 +633,25 @@ let map_with_binders g f l c0 = match kind c0 with if t' == t then c0 else mkProj (p, t') | Evar (e, al) -> - let al' = CArray.Fun1.smartmap f l al in + let al' = Array.Fun1.Smart.map f l al in if al' == al then c0 else mkEvar (e, al') | Case (ci, p, c, bl) -> let p' = f l p in let c' = f l c in - let bl' = CArray.Fun1.smartmap f l bl in + let bl' = Array.Fun1.Smart.map f l bl in if p' == p && c' == c && bl' == bl then c0 else mkCase (ci, p', c', bl') | Fix (ln, (lna, tl, bl)) -> - let tl' = CArray.Fun1.smartmap f l tl in + let tl' = Array.Fun1.Smart.map f l tl in let l' = iterate g (Array.length tl) l in - let bl' = CArray.Fun1.smartmap f l' bl in + let bl' = Array.Fun1.Smart.map f l' bl in if tl' == tl && bl' == bl then c0 else mkFix (ln,(lna,tl',bl')) | CoFix(ln,(lna,tl,bl)) -> - let tl' = CArray.Fun1.smartmap f l tl in + let tl' = Array.Fun1.Smart.map f l tl in let l' = iterate g (Array.length tl) l in - let bl' = CArray.Fun1.smartmap f l' bl in + let bl' = Array.Fun1.Smart.map f l' bl in mkCoFix (ln,(lna,tl',bl')) type instance_compare_fn = GlobRef.t -> int -> diff --git a/kernel/context.ml b/kernel/context.ml index 4f3f649c1..5d4a10184 100644 --- a/kernel/context.ml +++ b/kernel/context.ml @@ -192,7 +192,7 @@ struct let equal eq l = List.equal (fun c -> Declaration.equal eq c) l (** Map all terms in a given rel-context. *) - let map f = List.smartmap (Declaration.map_constr f) + let map f = List.Smart.map (Declaration.map_constr f) (** Perform a given action on every declaration in a given rel-context. *) let iter f = List.iter (Declaration.iter_constr f) @@ -392,7 +392,7 @@ struct let equal eq l = List.equal (fun c -> Declaration.equal eq c) l (** Map all terms in a given named-context. *) - let map f = List.smartmap (Declaration.map_constr f) + let map f = List.Smart.map (Declaration.map_constr f) (** Perform a given action on every declaration in a given named-context. *) let iter f = List.iter (Declaration.iter_constr f) diff --git a/kernel/declareops.ml b/kernel/declareops.ml index 3652a1ce4..832d478b3 100644 --- a/kernel/declareops.ml +++ b/kernel/declareops.ml @@ -42,7 +42,7 @@ let map_decl_arity f g = function let hcons_template_arity ar = { template_param_levels = ar.template_param_levels; - (* List.smartmap (Option.smartmap Univ.hcons_univ_level) ar.template_param_levels; *) + (* List.Smart.map (Option.Smart.map Univ.hcons_univ_level) ar.template_param_levels; *) template_level = Univ.hcons_univ ar.template_level } (** {6 Constants } *) @@ -70,7 +70,7 @@ let is_opaque cb = match cb.const_body with let subst_rel_declaration sub = RelDecl.map_constr (subst_mps sub) -let subst_rel_context sub = List.smartmap (subst_rel_declaration sub) +let subst_rel_context sub = List.Smart.map (subst_rel_declaration sub) let subst_const_type sub arity = if is_empty_subst sub then arity @@ -94,7 +94,7 @@ 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.smartmap (subst_const_proj sub) cb.const_proj 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 else @@ -117,7 +117,7 @@ let subst_const_body sub cb = let hcons_rel_decl = RelDecl.map_name Names.Name.hcons %> RelDecl.map_value Constr.hcons %> RelDecl.map_type Constr.hcons -let hcons_rel_context l = List.smartmap hcons_rel_decl l +let hcons_rel_context l = List.Smart.map hcons_rel_decl l let hcons_const_def = function | Undef inl -> Undef inl @@ -178,7 +178,7 @@ let recarg_length p j = let (_,cstrs) = Rtree.dest_node p in Array.length (snd (Rtree.dest_node cstrs.(j-1))) -let subst_wf_paths sub p = Rtree.smartmap (subst_recarg sub) p +let subst_wf_paths sub p = Rtree.Smart.map (subst_recarg sub) p (** {7 Substitution of inductive declarations } *) @@ -198,10 +198,10 @@ let subst_mind_packet sub mbp = mind_consnrealdecls = mbp.mind_consnrealdecls; mind_consnrealargs = mbp.mind_consnrealargs; mind_typename = mbp.mind_typename; - mind_nf_lc = Array.smartmap (subst_mps sub) mbp.mind_nf_lc; + mind_nf_lc = Array.Smart.map (subst_mps sub) mbp.mind_nf_lc; mind_arity_ctxt = subst_rel_context sub mbp.mind_arity_ctxt; mind_arity = subst_ind_arity sub mbp.mind_arity; - mind_user_lc = Array.smartmap (subst_mps sub) mbp.mind_user_lc; + mind_user_lc = Array.Smart.map (subst_mps sub) mbp.mind_user_lc; mind_nrealargs = mbp.mind_nrealargs; mind_nrealdecls = mbp.mind_nrealdecls; mind_kelim = mbp.mind_kelim; @@ -211,13 +211,13 @@ let subst_mind_packet sub mbp = mind_reloc_tbl = mbp.mind_reloc_tbl } let subst_mind_record sub (id, ps, pb as r) = - let ps' = Array.smartmap (subst_constant sub) ps in - let pb' = Array.smartmap (subst_const_proj sub) pb in + let ps' = Array.Smart.map (subst_constant sub) ps in + let pb' = Array.Smart.map (subst_const_proj sub) pb in if ps' == ps && pb' == pb then r else (id, ps', pb') let subst_mind_body sub mib = - { mind_record = Option.smartmap (Option.smartmap (subst_mind_record sub)) mib.mind_record ; + { mind_record = Option.Smart.map (Option.Smart.map (subst_mind_record sub)) mib.mind_record ; mind_finite = mib.mind_finite ; mind_ntypes = mib.mind_ntypes ; mind_hyps = (match mib.mind_hyps with [] -> [] | _ -> assert false); @@ -225,7 +225,7 @@ let subst_mind_body sub mib = mind_nparams_rec = mib.mind_nparams_rec; mind_params_ctxt = Context.Rel.map (subst_mps sub) mib.mind_params_ctxt; - mind_packets = Array.smartmap (subst_mind_packet sub) mib.mind_packets ; + mind_packets = Array.Smart.map (subst_mind_packet sub) mib.mind_packets ; mind_universes = mib.mind_universes; mind_private = mib.mind_private; mind_typing_flags = mib.mind_typing_flags; @@ -263,15 +263,15 @@ let hcons_ind_arity = (** Substitution of inductive declarations *) let hcons_mind_packet oib = - let user = Array.smartmap Constr.hcons oib.mind_user_lc in - let nf = Array.smartmap Constr.hcons oib.mind_nf_lc in + let user = Array.Smart.map Constr.hcons oib.mind_user_lc in + let nf = Array.Smart.map Constr.hcons oib.mind_nf_lc in (* Special optim : merge [mind_user_lc] and [mind_nf_lc] if possible *) let nf = if Array.equal (==) user nf then user else nf in { oib with mind_typename = Names.Id.hcons oib.mind_typename; mind_arity_ctxt = hcons_rel_context oib.mind_arity_ctxt; mind_arity = hcons_ind_arity oib.mind_arity; - mind_consnames = Array.smartmap Names.Id.hcons oib.mind_consnames; + mind_consnames = Array.Smart.map Names.Id.hcons oib.mind_consnames; mind_user_lc = user; mind_nf_lc = nf } @@ -283,7 +283,7 @@ let hcons_mind_universes miu = let hcons_mind mib = { mib with - mind_packets = Array.smartmap hcons_mind_packet mib.mind_packets; + mind_packets = Array.Smart.map hcons_mind_packet mib.mind_packets; mind_params_ctxt = hcons_rel_context mib.mind_params_ctxt; mind_universes = hcons_mind_universes mib.mind_universes } @@ -331,7 +331,7 @@ and hcons_structure_body sb = let sfb' = hcons_structure_field_body sfb in if l == l' && sfb == sfb' then fb else (l', sfb') in - List.smartmap map sb + List.Smart.map map sb and hcons_module_signature ms = hcons_functorize hcons_module_type hcons_structure_body hcons_module_signature ms diff --git a/kernel/esubst.ml b/kernel/esubst.ml index 91cc64523..4b8edf63f 100644 --- a/kernel/esubst.ml +++ b/kernel/esubst.ml @@ -140,7 +140,7 @@ let rec comp mk_cl s1 s2 = | ESID _, _ -> s2 | SHIFT(k,s), _ -> subs_shft(k, comp mk_cl s s2) | _, CONS(x,s') -> - CONS(CArray.Fun1.map (fun s t -> mk_cl(s,t)) s1 x, comp mk_cl s1 s') + CONS(Array.Fun1.map (fun s t -> mk_cl(s,t)) s1 x, comp mk_cl s1 s') | CONS(x,s), SHIFT(k,s') -> let lg = Array.length x in if k == lg then comp mk_cl s s' diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml index 9c2fa0546..0027ebecf 100644 --- a/kernel/mod_subst.ml +++ b/kernel/mod_subst.ml @@ -367,7 +367,7 @@ let rec map_kn f f' c = in let p' = func p in let ct' = func ct in - let l' = Array.smartmap func l in + let l' = Array.Smart.map func l in if (ci.ci_ind==ci_ind && p'==p && l'==l && ct'==ct)then c else @@ -396,21 +396,21 @@ let rec map_kn f f' c = else mkLetIn (na, b', t', ct') | App (ct,l) -> let ct' = func ct in - let l' = Array.smartmap func l in + let l' = Array.Smart.map func l in if (ct'== ct && l'==l) then c else mkApp (ct',l') | Evar (e,l) -> - let l' = Array.smartmap func l in + let l' = Array.Smart.map func l in if (l'==l) then c else mkEvar (e,l') | Fix (ln,(lna,tl,bl)) -> - let tl' = Array.smartmap func tl in - let bl' = Array.smartmap func bl in + let tl' = Array.Smart.map func tl in + let bl' = Array.Smart.map func bl in if (bl == bl'&& tl == tl') then c else mkFix (ln,(lna,tl',bl')) | CoFix(ln,(lna,tl,bl)) -> - let tl' = Array.smartmap func tl in - let bl' = Array.smartmap func bl in + let tl' = Array.Smart.map func tl in + let bl' = Array.Smart.map func bl in if (bl == bl'&& tl == tl') then c else mkCoFix (ln,(lna,tl',bl')) | _ -> c diff --git a/kernel/modops.ml b/kernel/modops.ml index bbf160db2..203817118 100644 --- a/kernel/modops.ml +++ b/kernel/modops.ml @@ -130,10 +130,10 @@ let destr_nofunctor = function |NoFunctor a -> a |MoreFunctor _ -> error_is_a_functor () -let rec functor_smartmap fty f0 funct = match funct with +let rec functor_smart_map fty f0 funct = match funct with |MoreFunctor (mbid,ty,e) -> let ty' = fty ty in - let e' = functor_smartmap fty f0 e in + let e' = functor_smart_map fty f0 e in if ty==ty' && e==e' then funct else MoreFunctor (mbid,ty',e') |NoFunctor a -> let a' = f0 a in if a==a' then funct else NoFunctor a' @@ -197,7 +197,7 @@ let rec subst_structure sub do_delta sign = let mtb' = subst_modtype sub do_delta mtb in if mtb==mtb' then orig else (l,SFBmodtype mtb') in - List.smartmap subst_body sign + List.Smart.map subst_body sign and subst_body : 'a. _ -> _ -> (_ -> 'a -> 'a) -> _ -> 'a generic_module_body -> 'a generic_module_body = fun is_mod sub subst_impl do_delta mb -> @@ -210,7 +210,7 @@ and subst_body : 'a. _ -> _ -> (_ -> 'a -> 'a) -> _ -> 'a generic_module_body -> in let ty' = subst_signature sub do_delta ty in let me' = subst_impl sub me in - let aty' = Option.smartmap (subst_expression sub id_delta) aty in + let aty' = Option.Smart.map (subst_expression sub id_delta) aty in let delta' = do_delta mb.mod_delta sub in if mp==mp' && me==me' && ty==ty' && aty==aty' && delta'==mb.mod_delta then mb @@ -245,12 +245,12 @@ and subst_expr sub do_delta seb = match seb with if meb==meb' && wdb==wdb' then seb else MEwith(meb',wdb') and subst_expression sub do_delta = - functor_smartmap + functor_smart_map (subst_modtype sub do_delta) (subst_expr sub do_delta) and subst_signature sub do_delta = - functor_smartmap + functor_smart_map (subst_modtype sub do_delta) (subst_structure sub do_delta) @@ -595,13 +595,13 @@ and clean_field l field = match field with if mb==mb' then field else (lab,SFBmodule mb') |_ -> field -and clean_structure l = List.smartmap (clean_field l) +and clean_structure l = List.Smart.map (clean_field l) and clean_signature l = - functor_smartmap (clean_module_type l) (clean_structure l) + functor_smart_map (clean_module_type l) (clean_structure l) and clean_expression l = - functor_smartmap (clean_module_type l) (fun me -> me) + functor_smart_map (clean_module_type l) (fun me -> me) let rec collect_mbid l sign = match sign with |MoreFunctor (mbid,ty,m) -> diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml index 01ddffe3e..12cd5fe83 100644 --- a/kernel/nativelambda.ml +++ b/kernel/nativelambda.ml @@ -102,10 +102,10 @@ let rec map_lam_with_binders g f n lam = if body == body' && def == def' then lam else Llet(id,def',body') | Lapp(fct,args) -> let fct' = f n fct in - let args' = Array.smartmap (f n) args in + let args' = Array.Smart.map (f n) args in if fct == fct' && args == args' then lam else mkLapp fct' args' | Lprim(prefix,kn,op,args) -> - let args' = Array.smartmap (f n) args in + let args' = Array.Smart.map (f n) args in if args == args' then lam else Lprim(prefix,kn,op,args') | Lcase(annot,t,a,br) -> let t' = f n t in @@ -116,7 +116,7 @@ let rec map_lam_with_binders g f n lam = if Array.is_empty ids then f n body else f (g (Array.length ids) n) body in if body == body' then b else (cn,ids,body') in - let br' = Array.smartmap on_b br in + let br' = Array.Smart.map on_b br in if t == t' && a == a' && br == br' then lam else Lcase(annot,t',a',br') | Lif(t,bt,bf) -> let t' = f n t in @@ -124,17 +124,17 @@ let rec map_lam_with_binders g f n lam = let bf' = f n bf in if t == t' && bt == bt' && bf == bf' then lam else Lif(t',bt',bf') | Lfix(init,(ids,ltypes,lbodies)) -> - let ltypes' = Array.smartmap (f n) ltypes in - let lbodies' = Array.smartmap (f (g (Array.length ids) n)) lbodies in + let ltypes' = Array.Smart.map (f n) ltypes in + let lbodies' = Array.Smart.map (f (g (Array.length ids) n)) lbodies in if ltypes == ltypes' && lbodies == lbodies' then lam else Lfix(init,(ids,ltypes',lbodies')) | Lcofix(init,(ids,ltypes,lbodies)) -> - let ltypes' = Array.smartmap (f n) ltypes in - let lbodies' = Array.smartmap (f (g (Array.length ids) n)) lbodies in + let ltypes' = Array.Smart.map (f n) ltypes in + let lbodies' = Array.Smart.map (f (g (Array.length ids) n)) lbodies in if ltypes == ltypes' && lbodies == lbodies' then lam else Lcofix(init,(ids,ltypes',lbodies')) | Lmakeblock(prefix,cn,tag,args) -> - let args' = Array.smartmap (f n) args in + let args' = Array.Smart.map (f n) args in if args == args' then lam else Lmakeblock(prefix,cn,tag,args') | Luint u -> let u' = map_uint g f n u in @@ -144,7 +144,7 @@ and map_uint g f n u = match u with | UintVal _ -> u | UintDigits(prefix,c,args) -> - let args' = Array.smartmap (f n) args in + let args' = Array.Smart.map (f n) args in if args == args' then u else UintDigits(prefix,c,args') | UintDecomp(prefix,c,a) -> let a' = f n a in @@ -177,7 +177,7 @@ let rec lam_exsubst subst lam = let lam_subst_args subst args = if is_subs_id subst then args - else Array.smartmap (lam_exsubst subst) args + else Array.Smart.map (lam_exsubst subst) args (** Simplification of lambda expression *) @@ -272,7 +272,7 @@ and simplify_app substf f substa args = (* TODO | Lproj -> simplify if the argument is known or a known global *) | _ -> mkLapp (simplify substf f) (simplify_args substa args) -and simplify_args subst args = Array.smartmap (simplify subst) args +and simplify_args subst args = Array.Smart.map (simplify subst) args and reduce_lapp substf lids body substa largs = match lids, largs with diff --git a/kernel/reduction.ml b/kernel/reduction.ml index 81fbd4f5e..38106fbf6 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -84,7 +84,7 @@ let map_lift (l : lift) (v : fconstr array) = match v with | [|c0; c1|] -> [|(l, c0); (l, c1)|] | [|c0; c1; c2|] -> [|(l, c0); (l, c1); (l, c2)|] | [|c0; c1; c2; c3|] -> [|(l, c0); (l, c1); (l, c2); (l, c3)|] -| v -> CArray.Fun1.map (fun l t -> (l, t)) l v +| v -> Array.Fun1.map (fun l t -> (l, t)) l v let pure_stack lfts stk = let rec pure_rec lfts stk = diff --git a/kernel/univ.ml b/kernel/univ.ml index 8e19fa4e5..9782312ca 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -456,10 +456,10 @@ struct let super l = if is_small l then type1 else - List.smartmap (fun x -> Expr.successor x) l + List.Smart.map (fun x -> Expr.successor x) l let addn n l = - List.smartmap (fun x -> Expr.addn n x) l + List.Smart.map (fun x -> Expr.addn n x) l let rec merge_univs l1 l2 = match l1, l2 with @@ -500,7 +500,7 @@ struct let for_all = List.for_all - let smartmap = List.smartmap + let smart_map = List.Smart.map let map = List.map end @@ -853,7 +853,7 @@ struct let length a = Array.length a let subst_fn fn t = - let t' = CArray.smartmap fn t in + let t' = CArray.Smart.map fn t in if t' == t then t else of_array t' let levels x = LSet.of_array x @@ -890,11 +890,11 @@ let subst_instance_level s l = | _ -> l let subst_instance_instance s i = - Array.smartmap (fun l -> subst_instance_level s l) i + Array.Smart.map (fun l -> subst_instance_level s l) i let subst_instance_universe s u = let f x = Universe.Expr.map (fun u -> subst_instance_level s u) x in - let u' = Universe.smartmap f u in + let u' = Universe.smart_map f u in if u == u' then u else Universe.sort u' @@ -1100,7 +1100,7 @@ let subst_univs_level_level subst l = let subst_univs_level_universe subst u = let f x = Universe.Expr.map (fun u -> subst_univs_level_level subst u) x in - let u' = Universe.smartmap f u in + let u' = Universe.smart_map f u in if u == u' then u else Universe.sort u' diff --git a/lib/rtree.ml b/lib/rtree.ml index 0e371025e..e1c6a4c4d 100644 --- a/lib/rtree.ml +++ b/lib/rtree.ml @@ -94,22 +94,28 @@ let is_node t = Node _ -> true | _ -> false - let rec map f t = match t with Param(i,j) -> Param(i,j) | Node (a,sons) -> Node (f a, Array.map (map f) sons) | Rec(j,defs) -> Rec (j, Array.map (map f) defs) -let smartmap f t = match t with - Param _ -> t - | Node (a,sons) -> - let a'=f a and sons' = Array.smartmap (map f) sons in - if a'==a && sons'==sons then t - else Node (a',sons') - | Rec(j,defs) -> - let defs' = Array.smartmap (map f) defs in - if defs'==defs then t - else Rec(j,defs') +module Smart = +struct + + let map f t = match t with + Param _ -> t + | Node (a,sons) -> + let a'=f a and sons' = Array.Smart.map (map f) sons in + if a'==a && sons'==sons then t + else Node (a',sons') + | Rec(j,defs) -> + let defs' = Array.Smart.map (map f) defs in + if defs'==defs then t + else Rec(j,defs') + +end + +let smartmap = Smart.map (** Structural equality test, parametrized by an equality on elements *) diff --git a/lib/rtree.mli b/lib/rtree.mli index 8edfc3d37..5ab14f603 100644 --- a/lib/rtree.mli +++ b/lib/rtree.mli @@ -74,13 +74,22 @@ val incl : ('a -> 'a -> bool) -> ('a -> 'a -> 'a option) -> 'a -> 'a t -> 'a t - (** Iterators *) +(** See also [Smart.map] *) val map : ('a -> 'b) -> 'a t -> 'b t -(** [(smartmap f t) == t] if [(f a) ==a ] for all nodes *) val smartmap : ('a -> 'a) -> 'a t -> 'a t +(** @deprecated Same as [Smart.map] *) (** A rather simple minded pretty-printer *) val pp_tree : ('a -> Pp.t) -> 'a t -> Pp.t val eq_rtree : ('a -> 'a -> bool) -> 'a t -> 'a t -> bool (** @deprecated Same as [Rtree.equal] *) + +module Smart : +sig + + (** [(Smart.map f t) == t] if [(f a) ==a ] for all nodes *) + val map : ('a -> 'a) -> 'a t -> 'a t + +end diff --git a/lib/spawn.ml b/lib/spawn.ml index 6d2ad3787..63e9e452c 100644 --- a/lib/spawn.ml +++ b/lib/spawn.ml @@ -10,7 +10,7 @@ let proto_version = 0 let prefer_sock = Sys.os_type = "Win32" -let accept_timeout = 2.0 +let accept_timeout = 10.0 let pr_err s = Printf.eprintf "(Spawn ,%d) %s\n%!" (Unix.getpid ()) s let prerr_endline s = if !Flags.debug then begin pr_err s end else () diff --git a/library/lib.ml b/library/lib.ml index 8a54995b9..128b27e75 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -51,7 +51,7 @@ let subst_objects subst seg = if obj' == obj then node else (id, obj') in - List.smartmap subst_one seg + List.Smart.map subst_one seg (*let load_and_subst_objects i prefix subst seg = List.rev (List.fold_left (fun seg (id,obj as node) -> diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml index 8e53a044d..4c6156a38 100644 --- a/plugins/cc/ccalgo.ml +++ b/plugins/cc/ccalgo.ml @@ -457,7 +457,7 @@ let rec canonize_name sigma c = | LetIn (na,b,t,ct) -> mkLetIn (na, func b,func t,func ct) | App (ct,l) -> - mkApp (func ct,Array.smartmap func l) + mkApp (func ct,Array.Smart.map func l) | Proj(p,c) -> let p' = Projection.map (fun kn -> Constant.make1 (Constant.canonical kn)) p in diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml index 0901acc7d..9f5c1f1a1 100644 --- a/plugins/extraction/mlutil.ml +++ b/plugins/extraction/mlutil.ml @@ -541,24 +541,24 @@ let dump_unused_vars a = | MLcase (t,e,br) -> let e' = ren env e in - let br' = Array.smartmap (ren_branch env) br in + let br' = Array.Smart.map (ren_branch env) br in if e' == e && br' == br then a else MLcase (t,e',br') | MLfix (i,ids,v) -> let env' = List.init (Array.length ids) (fun _ -> ref false) @ env in - let v' = Array.smartmap (ren env') v in + let v' = Array.Smart.map (ren env') v in if v' == v then a else MLfix (i,ids,v') | MLapp (b,l) -> - let b' = ren env b and l' = List.smartmap (ren env) l in + let b' = ren env b and l' = List.Smart.map (ren env) l in if b' == b && l' == l then a else MLapp (b',l') | MLcons(t,r,l) -> - let l' = List.smartmap (ren env) l in + let l' = List.Smart.map (ren env) l in if l' == l then a else MLcons (t,r,l') | MLtuple l -> - let l' = List.smartmap (ren env) l in + let l' = List.Smart.map (ren env) l in if l' == l then a else MLtuple l' | MLmagic b -> diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index ccf109ce1..5e0d3e8ee 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -1242,7 +1242,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam if this_fix_info.idx + 1 = 0 then tclIDTAC (* Someone tries to defined a principle on a fully parametric definition declared as a fixpoint (strange but ....) *) else - observe_tac_stream (str "h_fix " ++ int (this_fix_info.idx +1) ) (Proofview.V82.of_tactic (fix (Some this_fix_info.name) (this_fix_info.idx +1))) + observe_tac_stream (str "h_fix " ++ int (this_fix_info.idx +1) ) (Proofview.V82.of_tactic (fix this_fix_info.name (this_fix_info.idx +1))) else Proofview.V82.of_tactic (Tactics.mutual_fix this_fix_info.name (this_fix_info.idx + 1) other_fix_infos 0) @@ -1657,7 +1657,7 @@ let prove_principle_for_gen (* observe_tac "reverting" *) (revert (List.rev (acc_rec_arg_id::args_ids))); (* (fun g -> observe (Printer.pr_goal (sig_it g) ++ fnl () ++ *) (* str "fix arg num" ++ int (List.length args_ids + 1) ); tclIDTAC g); *) - (* observe_tac "h_fix " *) (Proofview.V82.of_tactic (fix (Some fix_id) (List.length args_ids + 1))); + (* observe_tac "h_fix " *) (Proofview.V82.of_tactic (fix fix_id (List.length args_ids + 1))); (* (fun g -> observe (Printer.pr_goal (sig_it g) ++ fnl() ++ pr_lconstr_env (pf_env g ) (pf_unsafe_type_of g (mkVar fix_id) )); tclIDTAC g); *) h_intros (List.rev (acc_rec_arg_id::args_ids)); Proofview.V82.of_tactic (Equality.rewriteLR (mkConst eq_ref)); diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index 35c3acd41..b0c9ff8fc 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -269,12 +269,12 @@ let subst_Function (subst,finfos) = in let function_constant' = do_subst_con finfos.function_constant in let graph_ind' = do_subst_ind finfos.graph_ind in - let equation_lemma' = Option.smartmap do_subst_con finfos.equation_lemma in - let correctness_lemma' = Option.smartmap do_subst_con finfos.correctness_lemma in - let completeness_lemma' = Option.smartmap do_subst_con finfos.completeness_lemma in - let rect_lemma' = Option.smartmap do_subst_con finfos.rect_lemma in - let rec_lemma' = Option.smartmap do_subst_con finfos.rec_lemma in - let prop_lemma' = Option.smartmap do_subst_con finfos.prop_lemma in + let equation_lemma' = Option.Smart.map do_subst_con finfos.equation_lemma in + let correctness_lemma' = Option.Smart.map do_subst_con finfos.correctness_lemma in + let completeness_lemma' = Option.Smart.map do_subst_con finfos.completeness_lemma in + let rect_lemma' = Option.Smart.map do_subst_con finfos.rect_lemma in + let rec_lemma' = Option.Smart.map do_subst_con finfos.rec_lemma in + let prop_lemma' = Option.Smart.map do_subst_con finfos.prop_lemma in if function_constant' == finfos.function_constant && graph_ind' == finfos.graph_ind && equation_lemma' == finfos.equation_lemma && @@ -302,12 +302,12 @@ let classify_Function infos = Libobject.Substitute infos let discharge_Function (_,finfos) = let function_constant' = Lib.discharge_con finfos.function_constant and graph_ind' = Lib.discharge_inductive finfos.graph_ind - and equation_lemma' = Option.smartmap Lib.discharge_con finfos.equation_lemma - and correctness_lemma' = Option.smartmap Lib.discharge_con finfos.correctness_lemma - and completeness_lemma' = Option.smartmap Lib.discharge_con finfos.completeness_lemma - and rect_lemma' = Option.smartmap Lib.discharge_con finfos.rect_lemma - and rec_lemma' = Option.smartmap Lib.discharge_con finfos.rec_lemma - and prop_lemma' = Option.smartmap Lib.discharge_con finfos.prop_lemma + and equation_lemma' = Option.Smart.map Lib.discharge_con finfos.equation_lemma + and correctness_lemma' = Option.Smart.map Lib.discharge_con finfos.correctness_lemma + and completeness_lemma' = Option.Smart.map Lib.discharge_con finfos.completeness_lemma + and rect_lemma' = Option.Smart.map Lib.discharge_con finfos.rect_lemma + and rec_lemma' = Option.Smart.map Lib.discharge_con finfos.rec_lemma + and prop_lemma' = Option.Smart.map Lib.discharge_con finfos.prop_lemma in if function_constant' == finfos.function_constant && graph_ind' == finfos.graph_ind && diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 45c9eff2f..ab03f1831 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -1152,7 +1152,7 @@ let termination_proof_header is_mes input_type ids args_id relation tclTHEN (Proofview.V82.of_tactic (Tactics.generalize [mkVar id])) (Proofview.V82.of_tactic (clear [id]))) )) ; - observe_tac (str "fix") (Proofview.V82.of_tactic (fix (Some hrec) (nargs+1))); + observe_tac (str "fix") (Proofview.V82.of_tactic (fix hrec (nargs+1))); h_intros args_id; Proofview.V82.of_tactic (Simple.intro wf_rec_arg); observe_tac (str "tac") (tac wf_rec_arg hrec wf_rec_arg acc_inv) diff --git a/plugins/ltac/coretactics.ml4 b/plugins/ltac/coretactics.ml4 index 931633e1a..faa9e413b 100644 --- a/plugins/ltac/coretactics.ml4 +++ b/plugins/ltac/coretactics.ml4 @@ -273,15 +273,13 @@ END (* Fix *) TACTIC EXTEND fix - [ "fix" natural(n) ] -> [ Tactics.fix None n ] -| [ "fix" ident(id) natural(n) ] -> [ Tactics.fix (Some id) n ] + [ "fix" ident(id) natural(n) ] -> [ Tactics.fix id n ] END (* Cofix *) TACTIC EXTEND cofix - [ "cofix" ] -> [ Tactics.cofix None ] -| [ "cofix" ident(id) ] -> [ Tactics.cofix (Some id) ] + [ "cofix" ident(id) ] -> [ Tactics.cofix id ] END (* Clear *) diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml index 59ba4b7de..b9d0d2e25 100644 --- a/plugins/setoid_ring/newring.ml +++ b/plugins/setoid_ring/newring.ml @@ -40,11 +40,7 @@ let error msg = CErrors.user_err Pp.(str msg) type protect_flag = Eval|Prot|Rec -let tag_arg tag_rec map subs i c = - match map i with - Eval -> mk_clos subs c - | Prot -> mk_atom c - | Rec -> if Int.equal i (-1) then mk_clos subs c else tag_rec c +type protection = Evd.evar_map -> EConstr.t -> GlobRef.t -> (Int.t -> protect_flag) option let global_head_of_constr sigma c = let f, args = decompose_app sigma c in @@ -55,32 +51,24 @@ let global_of_constr_nofail c = try global_of_constr c with Not_found -> VarRef (Id.of_string "dummy") -let rec mk_clos_but f_map subs t = - let open Term in - match f_map (global_of_constr_nofail t) with - | Some map -> tag_arg (mk_clos_but f_map subs) map subs (-1) t - | None -> - (match Constr.kind t with - App(f,args) -> mk_clos_app_but f_map subs f args 0 - | Prod _ -> mk_clos_deep (mk_clos_but f_map) subs t - | _ -> mk_atom t) +let rec mk_clos_but f_map n t = + let (f, args) = Constr.decompose_appvect t in + match f_map (global_of_constr_nofail f) with + | Some tag -> + let map i t = tag_arg f_map n (tag i) t in + if Array.is_empty args then map (-1) f + else mk_red (FApp (map (-1) f, Array.mapi map args)) + | None -> mk_atom t -and mk_clos_app_but f_map subs f args n = - let open Constr in - if n >= Array.length args then mk_atom(mkApp(f, args)) - else - let fargs, args' = Array.chop n args in - let f' = mkApp(f,fargs) in - match f_map (global_of_constr_nofail f') with - | Some map -> - let f i t = tag_arg (mk_clos_but f_map subs) map subs i t in - mk_red (FApp (f (-1) f', Array.mapi f args')) - | None -> mk_atom (mkApp (f, args)) +and tag_arg f_map n tag c = match tag with +| Eval -> mk_clos (Esubst.subs_id n) c +| Prot -> mk_atom c +| Rec -> mk_clos_but f_map n c let interp_map l t = try Some(List.assoc_f GlobRef.equal t l) with Not_found -> None -let protect_maps = ref String.Map.empty +let protect_maps : protection String.Map.t ref = ref String.Map.empty let add_map s m = protect_maps := String.Map.add s m !protect_maps let lookup_map map = try String.Map.find map !protect_maps @@ -90,8 +78,14 @@ let lookup_map map = let protect_red map env sigma c0 = let evars ev = Evarutil.safe_evar_value sigma ev in let c = EConstr.Unsafe.to_constr c0 in - EConstr.of_constr (kl (create_clos_infos ~evars all env) (create_tab ()) - (mk_clos_but (lookup_map map sigma c0) (Esubst.subs_id 0) c));; + let tab = create_tab () in + let infos = create_clos_infos ~evars all env in + let map = lookup_map map sigma c0 in + let rec eval n c = match Constr.kind c with + | Prod (na, t, u) -> Constr.mkProd (na, eval n t, eval (n + 1) u) + | _ -> kl infos tab (mk_clos_but map n c) + in + EConstr.of_constr (eval 0 c) let protect_tac map = Tactics.reduct_option (protect_red map,DEFAULTcast) None diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml index a31022919..f929e9430 100644 --- a/plugins/ssr/ssrequality.ml +++ b/plugins/ssr/ssrequality.ml @@ -287,7 +287,10 @@ let foldtac occ rdx ft gl = (fun env c _ h -> try find_T env c h ~k:(fun env t _ _ -> t) with NoMatch ->c), (fun () -> try end_T () with NoMatch -> fake_pmatcher_end ()) | _ -> - (fun env c _ h -> try let sigma = unify_HO env sigma (EConstr.of_constr c) (EConstr.of_constr t) in EConstr.to_constr sigma (EConstr.of_constr t) + (fun env c _ h -> + try + let sigma = unify_HO env sigma (EConstr.of_constr c) (EConstr.of_constr t) in + EConstr.to_constr ~abort_on_undefined_evars:false sigma (EConstr.of_constr t) with _ -> errorstrm Pp.(str "fold pattern " ++ pr_constr_pat t ++ spc () ++ str "does not match redex " ++ pr_constr_pat c)), fake_pmatcher_end in diff --git a/plugins/ssr/ssrview.ml b/plugins/ssr/ssrview.ml index fc50b24a6..29a936381 100644 --- a/plugins/ssr/ssrview.ml +++ b/plugins/ssr/ssrview.ml @@ -260,7 +260,7 @@ Goal.enter_one ~__LOC__ begin fun g -> let p = Reductionops.nf_evar sigma p in let get_body = function Evd.Evar_defined x -> x | _ -> assert false in let evars_of_econstr sigma t = - Evd.evars_of_term (EConstr.to_constr sigma (EConstr.of_constr t)) in + Evarutil.undefined_evars_of_term sigma (EConstr.of_constr t) in let rigid_of s = List.fold_left (fun l k -> if Evd.is_defined sigma k then diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 56e582891..779508477 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -920,7 +920,7 @@ let rec subst_cases_pattern subst = DAst.map (function | PatVar _ as pat -> pat | PatCstr (((kn,i),j),cpl,n) as pat -> let kn' = subst_mind subst kn - and cpl' = List.smartmap (subst_cases_pattern subst) cpl in + and cpl' = List.Smart.map (subst_cases_pattern subst) cpl in if kn' == kn && cpl' == cpl then pat else PatCstr (((kn',i),j),cpl',n) ) @@ -940,7 +940,7 @@ let rec subst_glob_constr subst = DAst.map (function | GApp (r,rl) as raw -> let r' = subst_glob_constr subst r - and rl' = List.smartmap (subst_glob_constr subst) rl in + and rl' = List.Smart.map (subst_glob_constr subst) rl in if r' == r && rl' == rl then raw else GApp(r',rl') @@ -957,25 +957,25 @@ let rec subst_glob_constr subst = DAst.map (function | GLetIn (n,r1,t,r2) as raw -> let r1' = subst_glob_constr subst r1 in let r2' = subst_glob_constr subst r2 in - let t' = Option.smartmap (subst_glob_constr subst) t in + let t' = Option.Smart.map (subst_glob_constr subst) t in if r1' == r1 && t == t' && r2' == r2 then raw else GLetIn (n,r1',t',r2') | GCases (sty,rtno,rl,branches) as raw -> let open CAst in - let rtno' = Option.smartmap (subst_glob_constr subst) rtno - and rl' = List.smartmap (fun (a,x as y) -> + let rtno' = Option.Smart.map (subst_glob_constr subst) rtno + and rl' = List.Smart.map (fun (a,x as y) -> let a' = subst_glob_constr subst a in let (n,topt) = x in - let topt' = Option.smartmap + let topt' = Option.Smart.map (fun ({loc;v=((sp,i),y)} as t) -> let sp' = subst_mind subst sp in if sp == sp' then t else CAst.(make ?loc ((sp',i),y))) topt in if a == a' && topt == topt' then y else (a',(n,topt'))) rl - and branches' = List.smartmap + and branches' = List.Smart.map (fun ({loc;v=(idl,cpl,r)} as branch) -> let cpl' = - List.smartmap (subst_cases_pattern subst) cpl + List.Smart.map (subst_cases_pattern subst) cpl and r' = subst_glob_constr subst r in if cpl' == cpl && r' == r then branch else CAst.(make ?loc (idl,cpl',r'))) @@ -985,14 +985,14 @@ let rec subst_glob_constr subst = DAst.map (function GCases (sty,rtno',rl',branches') | GLetTuple (nal,(na,po),b,c) as raw -> - let po' = Option.smartmap (subst_glob_constr subst) po + let po' = Option.Smart.map (subst_glob_constr subst) po and b' = subst_glob_constr subst b and c' = subst_glob_constr subst c in if po' == po && b' == b && c' == c then raw else GLetTuple (nal,(na,po'),b',c') | GIf (c,(na,po),b1,b2) as raw -> - let po' = Option.smartmap (subst_glob_constr subst) po + let po' = Option.Smart.map (subst_glob_constr subst) po and b1' = subst_glob_constr subst b1 and b2' = subst_glob_constr subst b2 and c' = subst_glob_constr subst c in @@ -1000,12 +1000,12 @@ let rec subst_glob_constr subst = DAst.map (function GIf (c',(na,po'),b1',b2') | GRec (fix,ida,bl,ra1,ra2) as raw -> - let ra1' = Array.smartmap (subst_glob_constr subst) ra1 - and ra2' = Array.smartmap (subst_glob_constr subst) ra2 in - let bl' = Array.smartmap - (List.smartmap (fun (na,k,obd,ty as dcl) -> + let ra1' = Array.Smart.map (subst_glob_constr subst) ra1 + and ra2' = Array.Smart.map (subst_glob_constr subst) ra2 in + let bl' = Array.Smart.map + (List.Smart.map (fun (na,k,obd,ty as dcl) -> let ty' = subst_glob_constr subst ty in - let obd' = Option.smartmap (subst_glob_constr subst) obd in + let obd' = Option.Smart.map (subst_glob_constr subst) obd in if ty'==ty && obd'==obd then dcl else (na,k,obd',ty'))) bl in if ra1' == ra1 && ra2' == ra2 && bl'==bl then raw else @@ -1018,7 +1018,7 @@ let rec subst_glob_constr subst = DAst.map (function if nref == ref then knd else Evar_kinds.ImplicitArg (nref, i, b) | _ -> knd in - let nsolve = Option.smartmap (Hook.get f_subst_genarg subst) solve in + let nsolve = Option.Smart.map (Hook.get f_subst_genarg subst) solve in if nsolve == solve && nknd == knd then raw else GHole (nknd, naming, nsolve) diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml index 3ae04cd4f..5056c0457 100644 --- a/pretyping/glob_ops.ml +++ b/pretyping/glob_ops.ml @@ -331,19 +331,19 @@ let bound_glob_vars = (** Mapping of names in binders *) -(* spiwack: I used a smartmap-style kind of mapping here, because the +(* spiwack: I used a smart-style kind of mapping here, because the operation will be the identity almost all of the time (with any term outside of Ltac to begin with). But to be honest, there would probably be no significant penalty in doing reallocation as pattern-matching expressions are usually rather small. *) let map_inpattern_binders f ({loc;v=(id,nal)} as x) = - let r = CList.smartmap f nal in + let r = CList.Smart.map f nal in if r == nal then x else CAst.make ?loc (id,r) let map_tomatch_binders f ((c,(na,inp)) as x) : tomatch_tuple = - let r = Option.smartmap (fun p -> map_inpattern_binders f p) inp in + let r = Option.Smart.map (fun p -> map_inpattern_binders f p) inp in if r == inp then x else c,(f na, r) @@ -355,7 +355,7 @@ let rec map_case_pattern_binders f = DAst.map (function | PatCstr (c,ps,na) as x -> let rna = f na in let rps = - CList.smartmap (fun p -> map_case_pattern_binders f p) ps + CList.Smart.map (fun p -> map_case_pattern_binders f p) ps in if rna == na && rps == ps then x else PatCstr(c,rps,rna) @@ -366,13 +366,13 @@ let map_cases_branch_binders f ({CAst.loc;v=(il,cll,rhs)} as x) : cases_clause = It is intended to be a superset of the free variable of the right-hand side, if I understand correctly. But I'm not sure when or how they are used. *) - let r = List.smartmap (fun cl -> map_case_pattern_binders f cl) cll in + let r = List.Smart.map (fun cl -> map_case_pattern_binders f cl) cll in if r == cll then x else CAst.make ?loc (il,r,rhs) let map_pattern_binders f tomatch branches = - CList.smartmap (fun tm -> map_tomatch_binders f tm) tomatch, - CList.smartmap (fun br -> map_cases_branch_binders f br) branches + CList.Smart.map (fun tm -> map_tomatch_binders f tm) tomatch, + CList.Smart.map (fun br -> map_cases_branch_binders f br) branches (** /mapping of names in binders *) diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml index ccfb7f990..375ed10d0 100644 --- a/pretyping/patternops.ml +++ b/pretyping/patternops.ml @@ -293,11 +293,11 @@ let rec subst_pattern subst pat = PProj(p',c') | PApp (f,args) -> let f' = subst_pattern subst f in - let args' = Array.smartmap (subst_pattern subst) args in + let args' = Array.Smart.map (subst_pattern subst) args in if f' == f && args' == args then pat else PApp (f',args') | PSoApp (i,args) -> - let args' = List.smartmap (subst_pattern subst) args in + let args' = List.Smart.map (subst_pattern subst) args in if args' == args then pat else PSoApp (i,args') | PLambda (name,c1,c2) -> @@ -312,7 +312,7 @@ let rec subst_pattern subst pat = PProd (name,c1',c2') | PLetIn (name,c1,t,c2) -> let c1' = subst_pattern subst c1 in - let t' = Option.smartmap (subst_pattern subst) t in + let t' = Option.Smart.map (subst_pattern subst) t in let c2' = subst_pattern subst c2 in if c1' == c1 && t' == t && c2' == c2 then pat else PLetIn (name,c1',t',c2') @@ -326,7 +326,7 @@ let rec subst_pattern subst pat = PIf (c',c1',c2') | PCase (cip,typ,c,branches) -> let ind = cip.cip_ind in - let ind' = Option.smartmap (subst_ind subst) ind in + let ind' = Option.Smart.map (subst_ind subst) ind in let cip' = if ind' == ind then cip else { cip with cip_ind = ind' } in let typ' = subst_pattern subst typ in let c' = subst_pattern subst c in @@ -334,18 +334,18 @@ let rec subst_pattern subst pat = let c' = subst_pattern subst c in if c' == c then br else (i,n,c') in - let branches' = List.smartmap subst_branch branches in + let branches' = List.Smart.map subst_branch branches in if cip' == cip && typ' == typ && c' == c && branches' == branches then pat else PCase(cip', typ', c', branches') | PFix (lni,(lna,tl,bl)) -> - let tl' = Array.smartmap (subst_pattern subst) tl in - let bl' = Array.smartmap (subst_pattern subst) bl in + let tl' = Array.Smart.map (subst_pattern subst) tl in + let bl' = Array.Smart.map (subst_pattern subst) bl in if bl' == bl && tl' == tl then pat else PFix (lni,(lna,tl',bl')) | PCoFix (ln,(lna,tl,bl)) -> - let tl' = Array.smartmap (subst_pattern subst) tl in - let bl' = Array.smartmap (subst_pattern subst) bl in + let tl' = Array.Smart.map (subst_pattern subst) tl in + let bl' = Array.Smart.map (subst_pattern subst) bl in if bl' == bl && tl' == tl then pat else PCoFix (ln,(lna,tl',bl')) diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 6bf852fcd..de72f9427 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -421,7 +421,7 @@ let ltac_interp_name_env k0 lvar env sigma = let n = Context.Rel.length (rel_context env) - k0 in let ctxt,_ = List.chop n (rel_context env) in let open Context.Rel.Declaration in - let ctxt' = List.smartmap (map_name (ltac_interp_name lvar)) ctxt in + let ctxt' = List.Smart.map (map_name (ltac_interp_name lvar)) ctxt in if List.equal (fun d1 d2 -> Name.equal (get_name d1) (get_name d2)) ctxt ctxt' then env else push_rel_context sigma ctxt' (pop_rel_context n env sigma) diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml index 84aceeedd..9eb410f06 100644 --- a/pretyping/recordops.ml +++ b/pretyping/recordops.ml @@ -69,8 +69,8 @@ let subst_structure (subst,((kn,i),id,kl,projs as obj)) = let projs' = (* invariant: struc.s_PROJ is an evaluable reference. Thus we can take *) (* the first component of subst_con. *) - List.smartmap - (Option.smartmap (fun kn -> fst (subst_con_kn subst kn))) + List.Smart.map + (Option.Smart.map (fun kn -> fst (subst_con_kn subst kn))) projs in let id' = fst (subst_constructor subst id) in diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 34d7a0798..6fde86837 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -1404,7 +1404,7 @@ let plain_instance sigma s c = | Meta p -> (try lift n (Metamap.find p s) with Not_found -> u) | App (f,l) when isCast sigma f -> let (f,_,t) = destCast sigma f in - let l' = CArray.Fun1.smartmap irec n l in + let l' = Array.Fun1.Smart.map irec n l in (match EConstr.kind sigma f with | Meta p -> (* Don't flatten application nodes: this is used to extract a @@ -1413,7 +1413,7 @@ let plain_instance sigma s c = (try let g = Metamap.find p s in match EConstr.kind sigma g with | App _ -> - let l' = CArray.Fun1.smartmap lift 1 l' in + let l' = Array.Fun1.Smart.map lift 1 l' in mkLetIn (Name default_plain_instance_ident,g,t,mkApp(mkRel 1, l')) | _ -> mkApp (g,l') with Not_found -> mkApp (f,l')) diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index 11cc6c1f0..12a944d32 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -180,12 +180,12 @@ let subst_class (subst,cl) = let do_subst_con c = Mod_subst.subst_constant subst c and do_subst c = Mod_subst.subst_mps subst c and do_subst_gr gr = fst (subst_global subst gr) in - let do_subst_ctx = List.smartmap (RelDecl.map_constr do_subst) in + let do_subst_ctx = List.Smart.map (RelDecl.map_constr do_subst) in let do_subst_context (grs,ctx) = - List.smartmap (Option.smartmap do_subst_gr) grs, + List.Smart.map (Option.Smart.map do_subst_gr) grs, do_subst_ctx ctx in - let do_subst_projs projs = List.smartmap (fun (x, y, z) -> - (x, y, Option.smartmap do_subst_con z)) projs in + let do_subst_projs projs = List.Smart.map (fun (x, y, z) -> + (x, y, Option.Smart.map do_subst_con z)) projs in { cl_univs = cl.cl_univs; cl_impl = do_subst_gr cl.cl_impl; cl_context = do_subst_context cl.cl_context; @@ -223,7 +223,7 @@ let discharge_class (_,cl) = | Some (_, ((tc,_), _)) -> Some tc.cl_impl) ctx' in - List.smartmap (Option.smartmap Lib.discharge_global) grs + List.Smart.map (Option.Smart.map Lib.discharge_global) grs @ newgrs in grs', discharge_rel_context subst 1 ctx @ ctx' in let cl_impl' = Lib.discharge_global cl.cl_impl in @@ -234,12 +234,12 @@ let discharge_class (_,cl) = let usubst, cl_univs' = Lib.discharge_abstract_universe_context info cl.cl_univs in let context = discharge_context ctx (subst, usubst) cl.cl_context in let props = discharge_rel_context (subst, usubst) (succ (List.length (fst cl.cl_context))) cl.cl_props in - let discharge_proj (x, y, z) = x, y, Option.smartmap Lib.discharge_con z in + let discharge_proj (x, y, z) = x, y, Option.Smart.map Lib.discharge_con z in { cl_univs = cl_univs'; cl_impl = cl_impl'; cl_context = context; cl_props = props; - cl_projs = List.smartmap discharge_proj cl.cl_projs; + cl_projs = List.Smart.map discharge_proj cl.cl_projs; cl_strict = cl.cl_strict; cl_unique = cl.cl_unique } diff --git a/proofs/logic.ml b/proofs/logic.ml index 4934afa83..218b2671e 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -481,7 +481,7 @@ and mk_arggoals sigma goal goalacc funty allargs = let env = Goal.V82.env sigma goal in raise (RefinerError (env,sigma,CannotApply (t, harg))) in - Array.smartfoldmap foldmap (goalacc, funty, sigma) allargs + Array.Smart.fold_left_map foldmap (goalacc, funty, sigma) allargs and mk_casegoals sigma goal goalacc p c = let env = Goal.V82.env sigma goal in diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml index 6fb411938..a75711bae 100644 --- a/proofs/redexpr.ml +++ b/proofs/redexpr.ml @@ -92,9 +92,9 @@ let cache_strategy (_,str) = let subst_strategy (subs,(local,obj)) = local, - List.smartmap + List.Smart.map (fun (k,ql as entry) -> - let ql' = List.smartmap (Mod_subst.subst_evaluable_reference subs) ql in + let ql' = List.Smart.map (Mod_subst.subst_evaluable_reference subs) ql in if ql==ql' then entry else (k,ql')) obj diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml index 627ac31f5..0b0e629ab 100644 --- a/tactics/autorewrite.ml +++ b/tactics/autorewrite.ml @@ -30,7 +30,7 @@ let subst_hint subst hint = let cst' = subst_mps subst hint.rew_lemma in let typ' = subst_mps subst hint.rew_type in let pat' = subst_mps subst hint.rew_pat in - let t' = Option.smartmap (Genintern.generic_substitute subst) hint.rew_tac in + let t' = Option.Smart.map (Genintern.generic_substitute subst) hint.rew_tac in if hint.rew_lemma == cst' && hint.rew_type == typ' && hint.rew_tac == t' then hint else { hint with rew_lemma = cst'; rew_type = typ'; diff --git a/tactics/hints.ml b/tactics/hints.ml index 39034a19b..3ade5314b 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -448,7 +448,7 @@ let subst_path_atom subst p = | PathAny -> p | PathHints grs -> let gr' gr = fst (subst_global subst gr) in - let grs' = List.smartmap gr' grs in + let grs' = List.Smart.map gr' grs in if grs' == grs then p else PathHints grs' let rec subst_hints_path subst hp = @@ -654,7 +654,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.smartfilter p sdl + let remove_sdl p sdl = List.Smart.filter p sdl let remove_he st p se = let sl1' = remove_sdl p se.sentry_nopat in @@ -666,7 +666,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.smartfilter (fun (ge, sd) -> filter sd) db.hintdb_nopat in + let hintnopat = List.Smart.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 @@ -1065,8 +1065,8 @@ let subst_autohint (subst, obj) = in if gr' == gr then gr else gr' in let subst_hint (k,data as hint) = - let k' = Option.smartmap subst_key k in - let pat' = Option.smartmap (subst_pattern subst) data.pat in + let k' = Option.Smart.map subst_key k in + let pat' = Option.Smart.map (subst_pattern subst) data.pat in let subst_mps subst c = EConstr.of_constr (subst_mps subst (EConstr.Unsafe.to_constr c)) in let code' = match data.code.obj with | Res_pf (c,t,ctx) -> @@ -1104,13 +1104,13 @@ let subst_autohint (subst, obj) = let action = match obj.hint_action with | CreateDB _ -> obj.hint_action | AddTransparency (grs, b) -> - let grs' = List.smartmap (subst_evaluable_reference subst) grs in + let grs' = List.Smart.map (subst_evaluable_reference subst) grs in if grs == grs' then obj.hint_action else AddTransparency (grs', b) | AddHints hintlist -> - let hintlist' = List.smartmap subst_hint hintlist in + let hintlist' = List.Smart.map subst_hint hintlist in if hintlist' == hintlist then obj.hint_action else AddHints hintlist' | RemoveHints grs -> - let grs' = List.smartmap (subst_global_reference subst) grs in + let grs' = List.Smart.map (subst_global_reference subst) grs in if grs == grs' then obj.hint_action else RemoveHints grs' | AddCut path -> let path' = subst_hints_path subst path in diff --git a/tactics/ind_tables.ml b/tactics/ind_tables.ml index 6d0da0dfa..21520f5d2 100644 --- a/tactics/ind_tables.ml +++ b/tactics/ind_tables.ml @@ -53,7 +53,7 @@ let subst_one_scheme subst (ind,const) = (subst_ind subst ind,subst_constant subst const) let subst_scheme (subst,(kind,l)) = - (kind,Array.map (subst_one_scheme subst) l) + (kind,Array.Smart.map (subst_one_scheme subst) l) let discharge_scheme (_,(kind,l)) = Some (kind,Array.map (fun (ind,const) -> diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 01351e249..a42e4b44b 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -563,20 +563,7 @@ let mutual_fix f n rest j = Proofview.Goal.enter begin fun gl -> end end -let warning_nameless_fix = - CWarnings.create ~name:"nameless-fix" ~category:"deprecated" Pp.(fun () -> - str "fix/cofix without a name are deprecated, please use the named version.") - -let fix ido n = match ido with - | None -> - warning_nameless_fix (); - Proofview.Goal.enter begin fun gl -> - let name = Proof_global.get_current_proof_name () in - let id = new_fresh_id Id.Set.empty name gl in - mutual_fix id n [] 0 - end - | Some id -> - mutual_fix id n [] 0 +let fix id n = mutual_fix id n [] 0 let rec check_is_mutcoind env sigma cl = let b = whd_all env sigma cl in @@ -619,16 +606,7 @@ let mutual_cofix f others j = Proofview.Goal.enter begin fun gl -> end end -let cofix ido = match ido with - | None -> - warning_nameless_fix (); - Proofview.Goal.enter begin fun gl -> - let name = Proof_global.get_current_proof_name () in - let id = new_fresh_id Id.Set.empty name gl in - mutual_cofix id [] 0 - end - | Some id -> - mutual_cofix id [] 0 +let cofix id = mutual_cofix id [] 0 (**************************************************************) (* Reduction and conversion tactics *) diff --git a/tactics/tactics.mli b/tactics/tactics.mli index 46f782eaa..ddf78b1d4 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -41,9 +41,9 @@ val convert_concl_no_check : types -> cast_kind -> unit Proofview.tactic val convert_hyp_no_check : named_declaration -> unit Proofview.tactic val mutual_fix : Id.t -> int -> (Id.t * int * constr) list -> int -> unit Proofview.tactic -val fix : Id.t option -> int -> unit Proofview.tactic +val fix : Id.t -> int -> unit Proofview.tactic val mutual_cofix : Id.t -> (Id.t * constr) list -> int -> unit Proofview.tactic -val cofix : Id.t option -> unit Proofview.tactic +val cofix : Id.t -> unit Proofview.tactic val convert : constr -> constr -> unit Proofview.tactic val convert_leq : constr -> constr -> unit Proofview.tactic diff --git a/test-suite/coqchk/univ.v b/test-suite/coqchk/univ.v index 43815b61e..216338615 100644 --- a/test-suite/coqchk/univ.v +++ b/test-suite/coqchk/univ.v @@ -79,3 +79,11 @@ Module POLY_SUBTYP. Module X := F M. End POLY_SUBTYP. + +Module POLY_IND. + + Polymorphic Inductive ind@{u v | u < v} : Prop := . + + Polymorphic Definition cst@{u v | v < u} := Prop. + +End POLY_IND. diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml index 2a41a50dd..3de7fe06b 100644 --- a/vernac/auto_ind_decl.ml +++ b/vernac/auto_ind_decl.ml @@ -400,9 +400,9 @@ let do_replace_lb mode lb_scheme_key aavoid narg p q = lb_type_of_p >>= fun (lb_type_of_p,eff) -> Proofview.tclEVARMAP >>= fun sigma -> let lb_args = Array.append (Array.append - (Array.map (fun x -> x) v) - (Array.map (fun x -> do_arg sigma x 1) v)) - (Array.map (fun x -> do_arg sigma x 2) v) + v + (Array.Smart.map (fun x -> do_arg sigma x 1) v)) + (Array.Smart.map (fun x -> do_arg sigma x 2) v) in let app = if Array.is_empty lb_args then lb_type_of_p else mkApp (lb_type_of_p,lb_args) in @@ -471,9 +471,9 @@ let do_replace_bl mode bl_scheme_key (ind,u as indu) aavoid narg lft rgt = user_err err_msg in let bl_args = Array.append (Array.append - (Array.map (fun x -> x) v) - (Array.map (fun x -> do_arg sigma x 1) v)) - (Array.map (fun x -> do_arg sigma x 2) v ) + v + (Array.Smart.map (fun x -> do_arg sigma x 1) v)) + (Array.Smart.map (fun x -> do_arg sigma x 2) v ) in let app = if Array.is_empty bl_args then bl_t1 else mkApp (bl_t1,bl_args) @@ -923,7 +923,7 @@ let compute_dec_tact ind lnamesparrec nparrec = (* left *) Tacticals.New.tclTHENLIST [ simplest_left; - apply (EConstr.of_constr (mkApp(blI,Array.map(fun x->mkVar x) xargs))); + apply (EConstr.of_constr (mkApp(blI,Array.map mkVar xargs))); Auto.default_auto ] ; @@ -939,7 +939,7 @@ let compute_dec_tact ind lnamesparrec nparrec = assert_by (Name freshH3) (EConstr.of_constr (mkApp(eq,[|bb;mkApp(eqI,[|mkVar freshm;mkVar freshm|]);tt|]))) (Tacticals.New.tclTHENLIST [ - apply (EConstr.of_constr (mkApp(lbI,Array.map (fun x->mkVar x) xargs))); + apply (EConstr.of_constr (mkApp(lbI,Array.map mkVar xargs))); Auto.default_auto ]); Equality.general_rewrite_bindings_in true diff --git a/vernac/himsg.ml b/vernac/himsg.ml index 3c4fcf714..1add1f486 100644 --- a/vernac/himsg.ml +++ b/vernac/himsg.ml @@ -86,7 +86,7 @@ let j_nf_betaiotaevar env sigma j = uj_type = Reductionops.nf_betaiota env sigma j.uj_type } let jv_nf_betaiotaevar env sigma jl = - Array.map (fun j -> j_nf_betaiotaevar env sigma j) jl + Array.Smart.map (fun j -> j_nf_betaiotaevar env sigma j) jl (** Printers *) |