diff options
75 files changed, 1748 insertions, 396 deletions
@@ -12,6 +12,8 @@ S kernel/byterun B kernel/byterun S library B library +S engine +B engine S pretyping B pretyping S interp diff --git a/COMPATIBILITY b/COMPATIBILITY index eaeb2cba24..ab29903b93 100644 --- a/COMPATIBILITY +++ b/COMPATIBILITY @@ -3,7 +3,36 @@ Potential sources of incompatibilities between Coq V8.4 and V8.5 (see also file CHANGES) -Universe Polymorphism. +- options for *coq* compilation (see below for ocaml). + +** [-I foo] is now deprecated and will not add directory foo to the + coq load path (only for ocaml, see below). Just replace [-I foo] by + [-Q foo ""] in your project file and re-generate makefile. Or + perform the same operation directly in your makefile if you edit it + by hand. + +** Option -R Foo bar is the same in v8.5 than in v8.4 concerning coq + load path. + +** Option [-I foo -as bar] is unchanged but discouraged unless you + compile ocaml code. Use -Q foo bar instead. + + for more details: file CHANGES or section "Customization at launch + time" of the reference manual. + +- Command line options for ocaml Compilation of ocaml code (plugins) + +** [-I foo] is *not* deprecated to add foo to the ocaml load path. + +** [-I foo -as bar] adds foo to the ocaml load path *and* adds foo to + the coq load path with logical name bar (shortcut for -I foo -Q foo + bar). + + for more details: file CHANGES or section "Customization at launch + time" of the reference manual. + + +- Universe Polymorphism. - Refinement, unification and tactics are now aware of universes, resulting in more localized errors. Universe inconsistencies diff --git a/Makefile.build b/Makefile.build index 57c22c6588..c5b4bbfe85 100644 --- a/Makefile.build +++ b/Makefile.build @@ -501,12 +501,13 @@ test-suite: world $(ALLSTDLIB).v ################################################################## .PHONY: lib kernel byterun library proofs tactics interp parsing pretyping -.PHONY: highparsing stm toplevel hightactics +.PHONY: engine highparsing stm toplevel hightactics lib: lib/clib.cma lib/lib.cma kernel: kernel/kernel.cma byterun: $(BYTERUN) library: library/library.cma +engine: engine/engine.cma proofs: proofs/proofs.cma tactics: tactics/tactics.cma interp: interp/interp.cma @@ -597,7 +598,7 @@ theories/Numbers/Natural/BigN/NMake_gen.v: theories/Numbers/Natural/BigN/NMake_g printers: $(DEBUGPRINTERS) -tools: $(TOOLS) $(DEBUGPRINTERS) $(COQDEPBOOT) +tools: $(TOOLS) $(DEBUGPRINTERS) $(OCAMLLIBDEP) # coqdep_boot : a basic version of coqdep, with almost no dependencies. @@ -605,12 +606,9 @@ tools: $(TOOLS) $(DEBUGPRINTERS) $(COQDEPBOOT) # to avoid using implicit rules and hence .ml.d files that would need # coqdep_boot. -COQDEPBOOTSRC:= \ - tools/coqdep_lexer.mli tools/coqdep_lexer.ml \ - tools/coqdep_common.mli tools/coqdep_common.ml \ - tools/coqdep_boot.ml +OCAMLLIBDEPSRC:= tools/ocamllibdep.ml -$(COQDEPBOOT): $(COQDEPBOOTSRC) +$(OCAMLLIBDEP): $(OCAMLLIBDEPSRC) $(SHOW)'OCAMLBEST -o $@' $(HIDE)$(call bestocaml, -I tools, unix) @@ -1058,33 +1056,33 @@ endif OCAMLDEP_NG = $(OCAMLDEP) -slash -ml-synonym .ml4 -checker/%.ml.d: $(D_DEPEND_BEFORE_SRC) checker/%.ml $(D_DEPEND_AFTER_SRC) $(COQDEPBOOT) $(GENFILES) +checker/%.ml.d: $(D_DEPEND_BEFORE_SRC) checker/%.ml $(D_DEPEND_AFTER_SRC) $(GENFILES) $(SHOW)'OCAMLDEP $<' $(HIDE)$(OCAMLDEP_NG) $(LOCALCHKLIBS) "$<" $(TOTARGET) -checker/%.mli.d: $(D_DEPEND_BEFORE_SRC) checker/%.mli $(D_DEPEND_AFTER_SRC) $(COQDEPBOOT) $(GENFILES) +checker/%.mli.d: $(D_DEPEND_BEFORE_SRC) checker/%.mli $(D_DEPEND_AFTER_SRC) $(GENFILES) $(SHOW)'OCAMLDEP $<' $(HIDE)$(OCAMLDEP_NG) $(LOCALCHKLIBS) "$<" $(TOTARGET) -%.ml.d: $(D_DEPEND_BEFORE_SRC) %.ml $(D_DEPEND_AFTER_SRC) $(COQDEPBOOT) $(GENFILES) +%.ml.d: $(D_DEPEND_BEFORE_SRC) %.ml $(D_DEPEND_AFTER_SRC) $(GENFILES) $(SHOW)'OCAMLDEP $<' $(HIDE)$(OCAMLDEP_NG) $(DEPFLAGS) "$<" $(TOTARGET) -%.mli.d: $(D_DEPEND_BEFORE_SRC) %.mli $(D_DEPEND_AFTER_SRC) $(COQDEPBOOT) $(GENFILES) +%.mli.d: $(D_DEPEND_BEFORE_SRC) %.mli $(D_DEPEND_AFTER_SRC) $(GENFILES) $(SHOW)'OCAMLDEP $<' $(HIDE)$(OCAMLDEP_NG) $(DEPFLAGS) "$<" $(TOTARGET) -checker/%.mllib.d: $(D_DEPEND_BEFORE_SRC) checker/%.mllib $(D_DEPEND_AFTER_SRC) $(COQDEPBOOT) $(GENFILES) - $(SHOW)'COQDEP $<' - $(HIDE)$(COQDEPBOOT) -I checker -c "$<" $(TOTARGET) +checker/%.mllib.d: $(D_DEPEND_BEFORE_SRC) checker/%.mllib $(D_DEPEND_AFTER_SRC) $(OCAMLLIBDEP) $(GENFILES) + $(SHOW)'OCAMLLIBDEP $<' + $(HIDE)$(OCAMLLIBDEP) $(LOCALCHKLIBS) "$<" $(TOTARGET) -%.mllib.d: $(D_DEPEND_BEFORE_SRC) %.mllib $(D_DEPEND_AFTER_SRC) $(COQDEPBOOT) $(GENFILES) - $(SHOW)'COQDEP $<' - $(HIDE)$(COQDEPBOOT) -I kernel -I tools/coqdoc -c "$<" $(TOTARGET) +%.mllib.d: $(D_DEPEND_BEFORE_SRC) %.mllib $(D_DEPEND_AFTER_SRC) $(OCAMLLIBDEP) $(GENFILES) + $(SHOW)'OCAMLLIBDEP $<' + $(HIDE)$(OCAMLLIBDEP) $(DEPFLAGS) "$<" $(TOTARGET) -%.v.d: $(D_DEPEND_BEFORE_SRC) %.v $(D_DEPEND_AFTER_SRC) $(COQDEPBOOT) $(GENVFILES) +%.v.d: $(D_DEPEND_BEFORE_SRC) %.v $(D_DEPEND_AFTER_SRC) $(COQDEP) $(GENVFILES) $(SHOW)'COQDEP $<' - $(HIDE)$(COQDEPBOOT) $(DEPNATDYN) "$<" $(TOTARGET) + $(HIDE)$(COQDEP) -boot $(DEPNATDYN) "$<" $(TOTARGET) %_stubs.c.d: $(D_DEPEND_BEFORE_SRC) %_stubs.c $(D_DEPEND_AFTER_SRC) $(SHOW)'CCDEP $<' diff --git a/Makefile.common b/Makefile.common index 07df8bb157..15ac13ff17 100644 --- a/Makefile.common +++ b/Makefile.common @@ -63,7 +63,7 @@ CSDPCERT:=plugins/micromega/csdpcert$(EXE) CORESRCDIRS:=\ config lib kernel kernel/byterun library \ proofs tactics pretyping interp stm \ - toplevel parsing printing grammar intf + toplevel parsing printing grammar intf engine PLUGINS:=\ omega romega micromega quote \ @@ -87,7 +87,7 @@ CHKSRCDIRS:= checker lib config kernel parsing ########################################################################### COQDEP:=bin/coqdep$(EXE) -COQDEPBOOT:=bin/coqdep_boot$(EXE) +OCAMLLIBDEP:=bin/ocamllibdep$(EXE) COQMAKEFILE:=bin/coq_makefile$(EXE) GALLINA:=bin/gallina$(EXE) COQTEX:=bin/coq-tex$(EXE) @@ -99,7 +99,7 @@ COQWORKMGR:=bin/coqworkmgr$(EXE) TOOLS:=$(COQDEP) $(COQMAKEFILE) $(GALLINA) $(COQTEX) $(COQWC) $(COQDOC) $(COQC)\ $(COQWORKMGR) -PRIVATEBINARIES:=$(FAKEIDE) $(COQDEPBOOT) +PRIVATEBINARIES:=$(FAKEIDE) $(OCAMLLIBDEP) ########################################################################### # Documentation @@ -161,7 +161,7 @@ BYTERUN:=$(addprefix kernel/byterun/, \ # the libraries directly CORECMA:=lib/clib.cma lib/lib.cma kernel/kernel.cma library/library.cma \ - pretyping/pretyping.cma interp/interp.cma proofs/proofs.cma \ + engine/engine.cma pretyping/pretyping.cma interp/interp.cma proofs/proofs.cma \ parsing/parsing.cma printing/printing.cma tactics/tactics.cma \ stm/stm.cma toplevel/toplevel.cma parsing/highparsing.cma tactics/hightactics.cma @@ -255,7 +255,7 @@ CSDPCERTCMO:=$(addprefix plugins/micromega/, \ DEBUGPRINTERS:=dev/top_printers.cmo dev/vm_printers.cmo dev/printers.cma -COQDEPCMO:=$(COQENVCMO) tools/coqdep_lexer.cmo tools/coqdep_common.cmo tools/coqdep.cmo +COQDEPCMO:=$(COQENVCMO) lib/system.cmo tools/coqdep_lexer.cmo tools/coqdep_common.cmo tools/coqdep.cmo COQDOCCMO:=lib/clib.cma $(addprefix tools/coqdoc/, \ cdglobals.cmo alpha.cmo index.cmo tokens.cmo output.cmo cpretty.cmo main.cmo ) @@ -371,7 +371,7 @@ MANPAGES:=man/coq-tex.1 man/coqdep.1 man/gallina.1 \ OCAMLDOCDIR=dev/ocamldoc DOCMLIS=$(wildcard ./lib/*.mli ./intf/*.mli ./kernel/*.mli ./library/*.mli \ - ./pretyping/*.mli ./interp/*.mli printing/*.mli \ + ./engine/*.mli ./pretyping/*.mli ./interp/*.mli printing/*.mli \ ./parsing/*.mli ./proofs/*.mli \ ./tactics/*.mli ./stm/*.mli ./toplevel/*.mli) @@ -63,6 +63,7 @@ "library": include "parsing": include "plugins": include +"engine": include "pretyping": include "printing": include "proofs": include diff --git a/checker/check.mllib b/checker/check.mllib index 22df375623..1d8ad34682 100644 --- a/checker/check.mllib +++ b/checker/check.mllib @@ -33,6 +33,7 @@ Util Ephemeron Future CUnix + System Profile RemoteCounter diff --git a/configure.ml b/configure.ml index 9ff483603c..3cf462ebe0 100644 --- a/configure.ml +++ b/configure.ml @@ -11,11 +11,11 @@ #load "str.cma" open Printf -let coq_version = "8.5beta1" -let coq_macos_version = "8.5.91" (** "[...] should be a string comprised of +let coq_version = "trunk" +let coq_macos_version = "8.4.90" (** "[...] should be a string comprised of three non-negative, period-separed integers [...]" *) -let vo_magic = 8591 -let state_magic = 58501 +let vo_magic = 8511 +let state_magic = 58511 let distributed_exec = ["coqtop";"coqc";"coqchk";"coqdoc";"coqmktop";"coqworkmgr"; "coqdoc";"coq_makefile";"coq-tex";"gallina";"coqwc";"csdpcert";"coqdep"] diff --git a/dev/base_include b/dev/base_include index de63c557d3..e086c64cd9 100644 --- a/dev/base_include +++ b/dev/base_include @@ -8,6 +8,7 @@ #directory "toplevel";; #directory "library";; #directory "kernel";; +#directory "engine";; #directory "pretyping";; #directory "lib";; #directory "proofs";; diff --git a/dev/ocamldebug-coq.run b/dev/ocamldebug-coq.run index d4ab22ced1..b00d084edb 100644 --- a/dev/ocamldebug-coq.run +++ b/dev/ocamldebug-coq.run @@ -17,7 +17,8 @@ exec $OCAMLDEBUG \ -I $COQTOP \ -I $COQTOP/config -I $COQTOP/printing -I $COQTOP/grammar \ -I $COQTOP/lib -I $COQTOP/intf -I $COQTOP/kernel \ - -I $COQTOP/library -I $COQTOP/pretyping -I $COQTOP/parsing \ + -I $COQTOP/library -I $COQTOP/engine \ + -I $COQTOP/pretyping -I $COQTOP/parsing \ -I $COQTOP/interp -I $COQTOP/proofs -I $COQTOP/tactics -I $COQTOP/stm \ -I $COQTOP/toplevel -I $COQTOP/dev -I $COQTOP/config \ -I $COQTOP/plugins/cc -I $COQTOP/plugins/dp \ diff --git a/engine/engine.mllib b/engine/engine.mllib new file mode 100644 index 0000000000..dc7ff2a642 --- /dev/null +++ b/engine/engine.mllib @@ -0,0 +1,5 @@ +Logic_monad +Termops +Namegen +Evd +Proofview_monad diff --git a/pretyping/evd.ml b/engine/evd.ml index bf519fb7c0..bf519fb7c0 100644 --- a/pretyping/evd.ml +++ b/engine/evd.ml diff --git a/pretyping/evd.mli b/engine/evd.mli index fe785a8314..fe785a8314 100644 --- a/pretyping/evd.mli +++ b/engine/evd.mli diff --git a/proofs/logic_monad.ml b/engine/logic_monad.ml index d509670ec2..d509670ec2 100644 --- a/proofs/logic_monad.ml +++ b/engine/logic_monad.ml diff --git a/proofs/logic_monad.mli b/engine/logic_monad.mli index ab729aff71..ab729aff71 100644 --- a/proofs/logic_monad.mli +++ b/engine/logic_monad.mli diff --git a/pretyping/namegen.ml b/engine/namegen.ml index 5aca11ae61..5aca11ae61 100644 --- a/pretyping/namegen.ml +++ b/engine/namegen.ml diff --git a/pretyping/namegen.mli b/engine/namegen.mli index f66bc6d88c..f66bc6d88c 100644 --- a/pretyping/namegen.mli +++ b/engine/namegen.mli diff --git a/proofs/proofview_monad.ml b/engine/proofview_monad.ml index 6e68cd2e45..6e68cd2e45 100644 --- a/proofs/proofview_monad.ml +++ b/engine/proofview_monad.ml diff --git a/proofs/proofview_monad.mli b/engine/proofview_monad.mli index d2a2e55fb1..d2a2e55fb1 100644 --- a/proofs/proofview_monad.mli +++ b/engine/proofview_monad.mli diff --git a/pretyping/termops.ml b/engine/termops.ml index 9f04faa839..9f04faa839 100644 --- a/pretyping/termops.ml +++ b/engine/termops.ml diff --git a/pretyping/termops.mli b/engine/termops.mli index 2552c67e61..2552c67e61 100644 --- a/pretyping/termops.mli +++ b/engine/termops.mli diff --git a/grammar/tacextend.ml4 b/grammar/tacextend.ml4 index 0421ad7ce4..02e43361a2 100644 --- a/grammar/tacextend.ml4 +++ b/grammar/tacextend.ml4 @@ -75,7 +75,8 @@ let make_clause (pt,_,e) = let make_fun_clauses loc s l = check_unicity s l; - Compat.make_fun loc (List.map make_clause l) + let map c = Compat.make_fun loc [make_clause c] in + mlexpr_of_list map l let rec make_args = function | [] -> <:expr< [] >> @@ -110,14 +111,14 @@ let rec make_tags loc = function <:expr< [ $t$ :: $l$ ] >> | _::l -> make_tags loc l -let make_one_printing_rule se (pt,_,e) = +let make_one_printing_rule (pt,_,e) = let level = mlexpr_of_int 0 in (* only level 0 supported here *) let loc = MLast.loc_of_expr e in let prods = mlexpr_of_list mlexpr_terminals_of_grammar_tactic_prod_item_expr pt in - <:expr< ($se$, { Pptactic.pptac_args = $make_tags loc pt$; - pptac_prods = ($level$, $prods$) }) >> + <:expr< { Pptactic.pptac_args = $make_tags loc pt$; + pptac_prods = ($level$, $prods$) } >> -let make_printing_rule se = mlexpr_of_list (make_one_printing_rule se) +let make_printing_rule = mlexpr_of_list make_one_printing_rule let make_empty_check = function | GramNonTerminal(_, t, e, _)-> @@ -139,30 +140,20 @@ let make_empty_check = function (* Idem *) raise Exit -let rec possibly_empty_subentries loc = function - | [] -> [] - | (s,prodsl) :: l -> - let rec aux = function - | [] -> (false,<:expr< None >>) - | prods :: rest -> - try - let l = List.map make_empty_check prods in - if has_extraarg prods then - (true,<:expr< try Some $mlexpr_of_list (fun x -> x) l$ - with [ Exit -> $snd (aux rest)$ ] >>) - else - (true, <:expr< Some $mlexpr_of_list (fun x -> x) l$ >>) - with Exit -> aux rest in - let (nonempty,v) = aux prodsl in - if nonempty then (s,v) :: possibly_empty_subentries loc l - else possibly_empty_subentries loc l - -let possibly_atomic loc prods = - let l = List.map_filter (function - | GramTerminal s :: l, _, _ -> Some (s,l) - | _ -> None) prods +let rec possibly_atomic loc = function +| [] -> [] +| ((GramNonTerminal _ :: _ | []), _, _) :: rem -> + (** This is not parsed by the TACTIC EXTEND rules *) + assert false +| (GramTerminal s :: prods, _, _) :: rem -> + let entry = + try + let l = List.map make_empty_check prods in + let l = mlexpr_of_list (fun x -> x) l in + (s, <:expr< try Some $l$ with [ Exit -> None ] >>) + with Exit -> (s, <:expr< None >>) in - possibly_empty_subentries loc (List.factorize_left String.equal l) + entry :: possibly_atomic loc rem (** Special treatment of constr entries *) let is_constr_gram = function @@ -186,6 +177,7 @@ let declare_tactic loc s c cl = match cl with let vars = mlexpr_of_list (mlexpr_of_option mlexpr_of_ident) vars in let entry = mlexpr_of_string s in let se = <:expr< { Tacexpr.mltac_tactic = $entry$; Tacexpr.mltac_plugin = $plugin_name$ } >> in + let ml = <:expr< { Tacexpr.mltac_name = $se$; Tacexpr.mltac_index = 0 } >> in let name = mlexpr_of_string name in let tac = (** Special handling of tactics without arguments: such tactics do not do @@ -200,13 +192,13 @@ let declare_tactic loc s c cl = match cl with (** Arguments are not passed directly to the ML tactic in the TacML node, the ML tactic retrieves its arguments in the [ist] environment instead. This is the rôle of the [lift_constr_tac_to_ml_tac] function. *) - let body = <:expr< Tacexpr.TacFun ($vars$, Tacexpr.TacML ($dloc$, $se$, [])) >> in + let body = <:expr< Tacexpr.TacFun ($vars$, Tacexpr.TacML ($dloc$, $ml$, [])) >> in let name = <:expr< Names.Id.of_string $name$ >> in declare_str_items loc [ <:str_item< do { let obj () = Tacenv.register_ltac True False $name$ $body$ in try do { - Tacenv.register_ml_tactic $se$ $tac$; + Tacenv.register_ml_tactic $se$ [|$tac$|]; Mltop.declare_cache_obj obj $plugin_name$; } with [ e when Errors.noncritical e -> Pp.msg_warning @@ -219,7 +211,7 @@ let declare_tactic loc s c cl = match cl with TacML tactic. *) let entry = mlexpr_of_string s in let se = <:expr< { Tacexpr.mltac_tactic = $entry$; Tacexpr.mltac_plugin = $plugin_name$ } >> in - let pp = make_printing_rule se cl in + let pp = make_printing_rule cl in let gl = mlexpr_of_clause cl in let atom = mlexpr_of_list (mlexpr_of_pair mlexpr_of_string (fun x -> x)) @@ -228,9 +220,9 @@ let declare_tactic loc s c cl = match cl with declare_str_items loc [ <:str_item< do { try do { - Tacenv.register_ml_tactic $se$ $make_fun_clauses loc s cl$; + Tacenv.register_ml_tactic $se$ (Array.of_list $make_fun_clauses loc s cl$); Mltop.declare_cache_obj $obj$ $plugin_name$; - List.iter (fun (s, r) -> Pptactic.declare_ml_tactic_pprule s r) $pp$; } + Pptactic.declare_ml_tactic_pprule $se$ (Array.of_list $pp$); } with [ e when Errors.noncritical e -> Pp.msg_warning (Pp.app diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli index ff090ca844..78b88289e1 100644 --- a/intf/tacexpr.mli +++ b/intf/tacexpr.mli @@ -99,6 +99,11 @@ type ml_tactic_name = { mltac_tactic : string; } +type ml_tactic_entry = { + mltac_name : ml_tactic_name; + mltac_index : int; +} + (** Composite types *) (** In globalize tactics, we need to keep the initial [constr_expr] to recompute @@ -285,7 +290,7 @@ and 'a gen_tactic_expr = | TacFun of 'a gen_tactic_fun_ast | TacArg of 'a gen_tactic_arg located (* For ML extensions *) - | TacML of Loc.t * ml_tactic_name * 'l generic_argument list + | TacML of Loc.t * ml_tactic_entry * 'l generic_argument list (* For syntax extensions *) | TacAlias of Loc.t * KerName.t * (Id.t * 'l generic_argument) list diff --git a/lib/cMap.ml b/lib/cMap.ml index cf590d96c3..876f847365 100644 --- a/lib/cMap.ml +++ b/lib/cMap.ml @@ -12,6 +12,13 @@ sig val compare : t -> t -> int end +module type MonadS = +sig + type +'a t + val return : 'a -> 'a t + val (>>=) : 'a t -> ('a -> 'b t) -> 'b t +end + module type S = Map.S module type ExtS = @@ -30,6 +37,12 @@ sig sig val map : (key -> 'a -> key * 'b) -> 'a t -> 'b t end + module Monad(M : MonadS) : + sig + val fold : (key -> 'a -> 'b -> 'b M.t) -> 'a t -> 'b -> 'b M.t + val fold_left : (key -> 'a -> 'b -> 'b M.t) -> 'a t -> 'b -> 'b M.t + val fold_right : (key -> 'a -> 'b -> 'b M.t) -> 'a t -> 'b -> 'b M.t + end end module MapExt (M : Map.OrderedType) : @@ -47,6 +60,12 @@ sig sig val map : (M.t -> 'a -> M.t * 'b) -> 'a map -> 'b map end + module Monad(MS : MonadS) : + sig + val fold : (M.t -> 'a -> 'b -> 'b MS.t) -> 'a map -> 'b -> 'b MS.t + val fold_left : (M.t -> 'a -> 'b -> 'b MS.t) -> 'a map -> 'b -> 'b MS.t + val fold_right : (M.t -> 'a -> 'b -> 'b MS.t) -> 'a map -> 'b -> 'b MS.t + end end = struct (** This unsafe module is a way to access to the actual implementations of @@ -159,6 +178,29 @@ struct end + module Monad(M : MonadS) = + struct + + open M + + let rec fold_left f s accu = match map_prj s with + | MEmpty -> return accu + | MNode (l, k, v, r, h) -> + fold_left f l accu >>= fun accu -> + f k v accu >>= fun accu -> + fold_left f r accu + + let rec fold_right f s accu = match map_prj s with + | MEmpty -> return accu + | MNode (l, k, v, r, h) -> + fold_right f r accu >>= fun accu -> + f k v accu >>= fun accu -> + fold_right f l accu + + let fold = fold_left + + end + end module Make(M : Map.OrderedType) = diff --git a/lib/cMap.mli b/lib/cMap.mli index 23d3801e08..cd3d2f5b19 100644 --- a/lib/cMap.mli +++ b/lib/cMap.mli @@ -14,6 +14,13 @@ sig val compare : t -> t -> int end +module type MonadS = +sig + type +'a t + val return : 'a -> 'a t + val (>>=) : 'a t -> ('a -> 'b t) -> 'b t +end + module type S = Map.S module type ExtS = @@ -59,6 +66,14 @@ sig i.e.: for all (k : key) (x : 'a), compare (fst (f k x)) k = 0. *) end + module Monad(M : MonadS) : + sig + val fold : (key -> 'a -> 'b -> 'b M.t) -> 'a t -> 'b -> 'b M.t + val fold_left : (key -> 'a -> 'b -> 'b M.t) -> 'a t -> 'b -> 'b M.t + val fold_right : (key -> 'a -> 'b -> 'b M.t) -> 'a t -> 'b -> 'b M.t + end + (** Fold operators parameterized by any monad. *) + end module Make(M : Map.OrderedType) : ExtS with diff --git a/lib/hMap.ml b/lib/hMap.ml index f902eded03..8e900cd581 100644 --- a/lib/hMap.ml +++ b/lib/hMap.ml @@ -329,4 +329,18 @@ struct Int.Map.map fs s end + module Monad(M : CMap.MonadS) = + struct + module IntM = Int.Map.Monad(M) + module ExtM = Map.Monad(M) + open M + + let fold f s accu = + let ff _ m accu = ExtM.fold f m accu in + IntM.fold ff s accu + + let fold_left _ _ _ = assert false + let fold_right _ _ _ = assert false + end + end diff --git a/lib/system.ml b/lib/system.ml index 73095f9cd6..70f5904629 100644 --- a/lib/system.ml +++ b/lib/system.ml @@ -13,44 +13,85 @@ open Errors open Util open Unix -(* All subdirectories, recursively *) +(** Dealing with directories *) -let exists_dir dir = - try let _ = closedir (opendir dir) in true with Unix_error _ -> false +type unix_path = string (* path in unix-style, with '/' separator *) + +type file_kind = + | FileDir of unix_path * (* basename of path: *) string + | FileRegular of string (* basename of file *) + +(* Copy of Filename.concat but assuming paths to always be POSIX *) + +let (//) dirname filename = + let l = String.length dirname in + if l = 0 || dirname.[l-1] = '/' + then dirname ^ filename + else dirname ^ "/" ^ filename + +(* Excluding directories; We avoid directories starting with . as well + as CVS and _darcs and any subdirs given via -exclude-dir *) let skipped_dirnames = ref ["CVS"; "_darcs"] -let exclude_search_in_dirname f = skipped_dirnames := f :: !skipped_dirnames +let exclude_directory f = skipped_dirnames := f :: !skipped_dirnames let ok_dirname f = - not (String.is_empty f) && f.[0] != '.' && - not (String.List.mem f !skipped_dirnames) && - (match Unicode.ident_refutation f with None -> true | _ -> false) + not (f = "") && f.[0] != '.' && + not (List.mem f !skipped_dirnames) (*&& + (match Unicode.ident_refutation f with None -> true | _ -> false)*) + +(* Check directory can be opened *) + +let exists_dir dir = + try let _ = closedir (opendir dir) in true with Unix_error _ -> false + +let check_unix_dir warn dir = + if (Sys.os_type = "Win32" || Sys.os_type = "Cygwin") && + (String.length dir > 2 && dir.[1] = ':' || + String.contains dir '\\' || + String.contains dir ';') + then warn ("assuming " ^ dir ^ + " to be a Unix path even if looking like a Win32 path.") + +let apply_subdir f path name = + (* we avoid all files and subdirs starting by '.' (e.g. .svn) *) + (* as well as skipped files like CVS, ... *) + if name.[0] <> '.' && ok_dirname name then + let path = if path = "." then name else path//name in + match try (stat path).st_kind with Unix_error _ -> S_BLK with + | S_DIR -> f (FileDir (path,name)) + | S_REG -> f (FileRegular name) + | _ -> () + +let process_directory f path = + let dirh = opendir path in + try while true do apply_subdir f path (readdir dirh) done + with End_of_file -> closedir dirh + +let process_subdirectories f path = + let f = function FileDir (path,base) -> f path base | FileRegular _ -> () in + process_directory f path + +(** Returns the list of all recursive subdirectories of [root] in + depth-first search, with sons ordered as on the file system; + warns if [root] does not exist *) let all_subdirs ~unix_path:root = let l = ref [] in let add f rel = l := (f, rel) :: !l in - let rec traverse dir rel = - let dirh = opendir dir in - try - while true do - let f = readdir dirh in - if ok_dirname f then - let file = Filename.concat dir f in - try - begin match (stat file).st_kind with - | S_DIR -> - let newrel = rel @ [f] in - add file newrel; - traverse file newrel - | _ -> () - end - with Unix_error (e,s1,s2) -> () - done - with End_of_file -> - closedir dirh + let rec traverse path rel = + let f = function + | FileDir (path,f) -> + let newrel = rel @ [f] in + add path newrel; + traverse path newrel + | _ -> () + in process_directory f path in - if exists_dir root then traverse root []; + check_unix_dir (fun s -> msg_warning (str s)) root; + if exists_dir root then traverse root [] + else msg_warning (str ("Cannot open " ^ root)); List.rev !l let rec search paths test = diff --git a/lib/system.mli b/lib/system.mli index a3d66d577a..6ed4503266 100644 --- a/lib/system.mli +++ b/lib/system.mli @@ -8,14 +8,46 @@ (** {5 Coqtop specific system utilities} *) +(** {6 Directories} *) + +type unix_path = string (* path in unix-style, with '/' separator *) + +type file_kind = + | FileDir of unix_path * (* basename of path: *) string + | FileRegular of string (* basename of file *) + +val (//) : unix_path -> string -> unix_path + +val exists_dir : unix_path -> bool + +(** [check_unix_dir warn path] calls [warn] with an appropriate + message if [path] looks does not look like a Unix path on Windows *) + +val check_unix_dir : (string -> unit) -> unix_path -> unit + +(** [exclude_search_in_dirname path] excludes [path] when processing + directories *) + +val exclude_directory : unix_path -> unit + +(** [process_directory f path] applies [f] on contents of directory + [path]; fails with Unix_error if the latter does not exists; skips + all files or dirs starting with "." *) + +val process_directory : (file_kind -> unit) -> unix_path -> unit + +(** [process_subdirectories f path] applies [f path/file file] on each + [file] of the directory [path]; fails with Unix_error if the + latter does not exists; kips all files or dirs starting with "." *) + +val process_subdirectories : (unix_path -> string -> unit) -> unix_path -> unit + (** {6 Files and load paths} *) (** Load path entries remember the original root given by the user. For efficiency, we keep the full path (field [directory]), the root path and the path relative to the root. *) -val exclude_search_in_dirname : string -> unit - val all_subdirs : unix_path:string -> (CUnix.physical_path * string list) list val is_in_path : CUnix.load_path -> string -> bool val is_in_system_path : string -> bool @@ -24,8 +56,6 @@ val where_in_path : val where_in_path_rex : CUnix.load_path -> Str.regexp -> (CUnix.physical_path * string) list -val exists_dir : string -> bool - val find_file_in_path : ?warn:bool -> CUnix.load_path -> string -> CUnix.physical_path * string diff --git a/myocamlbuild.ml b/myocamlbuild.ml index 097a104259..73ef7e1eda 100644 --- a/myocamlbuild.ml +++ b/myocamlbuild.ml @@ -104,7 +104,7 @@ let _build = Options.build_dir let core_libs = ["lib/clib"; "lib/lib"; "kernel/kernel"; "library/library"; - "pretyping/pretyping"; "interp/interp"; "proofs/proofs"; + "engine/engine"; "pretyping/pretyping"; "interp/interp"; "proofs/proofs"; "parsing/parsing"; "printing/printing"; "tactics/tactics"; "stm/stm"; "toplevel/toplevel"; "parsing/highparsing"; "tactics/hightactics"] diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml index 01194c60d0..d9eb5d4126 100644 --- a/parsing/egramcoq.ml +++ b/parsing/egramcoq.ml @@ -258,8 +258,12 @@ type all_grammar_command = let add_ml_tactic_entry name prods = let entry = weaken_entry Tactic.simple_tactic in - let mkact loc l : raw_tactic_expr = Tacexpr.TacML (loc, name, List.map snd l) in - let rules = List.map (make_rule mkact) prods in + let mkact i loc l : raw_tactic_expr = + let open Tacexpr in + let entry = { mltac_name = name; mltac_index = i } in + TacML (loc, entry, List.map snd l) + in + let rules = List.map_i (fun i p -> make_rule (mkact i) p) 0 prods in synchronize_level_positions (); grammar_extend entry None (None ,[(None, None, List.rev rules)]); 1 diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index b1cbea51c8..5c74d74f89 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -1309,7 +1309,7 @@ let open_new_goal build_proof sigma using_lemmas ref_ goal_name (gls_type,decomp tclFIRST[ tclTHEN (Proofview.V82.of_tactic (eapply_with_bindings (mkVar (List.nth !lid !h_num), NoBindings))) - e_assumption; + (Proofview.V82.of_tactic e_assumption); Eauto.eauto_with_bases (true,5) [Evd.empty,Lazy.force refl_equal] diff --git a/plugins/setoid_ring/g_newring.ml4 b/plugins/setoid_ring/g_newring.ml4 new file mode 100644 index 0000000000..856ec0db5f --- /dev/null +++ b/plugins/setoid_ring/g_newring.ml4 @@ -0,0 +1,90 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(*i camlp4deps: "grammar/grammar.cma" i*) + +open Pp +open Util +open Libnames +open Printer +open Newring_ast +open Newring + +DECLARE PLUGIN "newring_plugin" + +TACTIC EXTEND protect_fv + [ "protect_fv" string(map) "in" ident(id) ] -> + [ Proofview.V82.tactic (protect_tac_in map id) ] +| [ "protect_fv" string(map) ] -> + [ Proofview.V82.tactic (protect_tac map) ] +END + +TACTIC EXTEND closed_term + [ "closed_term" constr(t) "[" ne_reference_list(l) "]" ] -> + [ Proofview.V82.tactic (closed_term t l) ] +END + +VERNAC ARGUMENT EXTEND ring_mod + | [ "decidable" constr(eq_test) ] -> [ Ring_kind(Computational eq_test) ] + | [ "abstract" ] -> [ Ring_kind Abstract ] + | [ "morphism" constr(morph) ] -> [ Ring_kind(Morphism morph) ] + | [ "constants" "[" tactic(cst_tac) "]" ] -> [ Const_tac(CstTac cst_tac) ] + | [ "closed" "[" ne_global_list(l) "]" ] -> [ Const_tac(Closed l) ] + | [ "preprocess" "[" tactic(pre) "]" ] -> [ Pre_tac pre ] + | [ "postprocess" "[" tactic(post) "]" ] -> [ Post_tac post ] + | [ "setoid" constr(sth) constr(ext) ] -> [ Setoid(sth,ext) ] + | [ "sign" constr(sign_spec) ] -> [ Sign_spec sign_spec ] + | [ "power" constr(pow_spec) "[" ne_global_list(l) "]" ] -> + [ Pow_spec (Closed l, pow_spec) ] + | [ "power_tac" constr(pow_spec) "[" tactic(cst_tac) "]" ] -> + [ Pow_spec (CstTac cst_tac, pow_spec) ] + | [ "div" constr(div_spec) ] -> [ Div_spec div_spec ] +END + +VERNAC COMMAND EXTEND AddSetoidRing CLASSIFIED AS SIDEFF + | [ "Add" "Ring" ident(id) ":" constr(t) ring_mods(l) ] -> + [ let (k,set,cst,pre,post,power,sign, div) = process_ring_mods l in + add_theory id (ic t) set k cst (pre,post) power sign div] + | [ "Print" "Rings" ] => [Vernac_classifier.classify_as_query] -> [ + msg_notice (strbrk "The following ring structures have been declared:"); + Spmap.iter (fun fn fi -> + msg_notice (hov 2 + (Ppconstr.pr_id (Libnames.basename fn)++spc()++ + str"with carrier "++ pr_constr fi.ring_carrier++spc()++ + str"and equivalence relation "++ pr_constr fi.ring_req)) + ) !from_name ] +END + +TACTIC EXTEND ring_lookup +| [ "ring_lookup" tactic0(f) "[" constr_list(lH) "]" ne_constr_list(lrt) ] -> + [ let (t,lr) = List.sep_last lrt in ring_lookup f lH lr t] +END + +VERNAC ARGUMENT EXTEND field_mod + | [ ring_mod(m) ] -> [ Ring_mod m ] + | [ "completeness" constr(inj) ] -> [ Inject inj ] +END + +VERNAC COMMAND EXTEND AddSetoidField CLASSIFIED AS SIDEFF +| [ "Add" "Field" ident(id) ":" constr(t) field_mods(l) ] -> + [ let (k,set,inj,cst_tac,pre,post,power,sign,div) = process_field_mods l in + add_field_theory id (ic t) set k cst_tac inj (pre,post) power sign div] +| [ "Print" "Fields" ] => [Vernac_classifier.classify_as_query] -> [ + msg_notice (strbrk "The following field structures have been declared:"); + Spmap.iter (fun fn fi -> + msg_notice (hov 2 + (Ppconstr.pr_id (Libnames.basename fn)++spc()++ + str"with carrier "++ pr_constr fi.field_carrier++spc()++ + str"and equivalence relation "++ pr_constr fi.field_req)) + ) !field_from_name ] +END + +TACTIC EXTEND field_lookup +| [ "field_lookup" tactic(f) "[" constr_list(lH) "]" ne_constr_list(lt) ] -> + [ let (t,l) = List.sep_last lt in field_lookup f lH l t ] +END diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml index 2f9e8509c2..7844a36c16 100644 --- a/plugins/setoid_ring/newring.ml4 +++ b/plugins/setoid_ring/newring.ml @@ -30,8 +30,7 @@ open Declare open Decl_kinds open Entries open Misctypes - -DECLARE PLUGIN "newring_plugin" +open Newring_ast (****************************************************************************) (* controlled reduction *) @@ -105,13 +104,6 @@ let protect_tac_in map id = Tactics.reduct_option (protect_red map,DEFAULTcast) (Some(id, Locus.InHyp));; -TACTIC EXTEND protect_fv - [ "protect_fv" string(map) "in" ident(id) ] -> - [ Proofview.V82.tactic (protect_tac_in map id) ] -| [ "protect_fv" string(map) ] -> - [ Proofview.V82.tactic (protect_tac map) ] -END;; - (****************************************************************************) let closed_term t l = @@ -120,12 +112,6 @@ let closed_term t l = if Quote.closed_under cs t then tclIDTAC else tclFAIL 0 (mt()) ;; -TACTIC EXTEND closed_term - [ "closed_term" constr(t) "[" ne_reference_list(l) "]" ] -> - [ Proofview.V82.tactic (closed_term t l) ] -END -;; - (* TACTIC EXTEND echo | [ "echo" constr(t) ] -> [ Pp.msg (Termops.print_constr t); Tacinterp.eval_tactic (TacId []) ] @@ -143,6 +129,10 @@ let closed_term_ast l = mltac_plugin = "newring_plugin"; mltac_tactic = "closed_term"; } in + let tacname = { + mltac_name = tacname; + mltac_index = 0; + } in let l = List.map (fun gr -> ArgArg(Loc.ghost,gr)) l in TacFun([Some(Id.of_string"t")], TacML(Loc.ghost,tacname, @@ -350,20 +340,6 @@ let _ = add_map "ring" (****************************************************************************) (* Ring database *) -type ring_info = - { ring_carrier : types; - ring_req : constr; - ring_setoid : constr; - ring_ext : constr; - ring_morph : constr; - ring_th : constr; - ring_cst_tac : glob_tactic_expr; - ring_pow_tac : glob_tactic_expr; - ring_lemma1 : constr; - ring_lemma2 : constr; - ring_pre_tac : glob_tactic_expr; - ring_post_tac : glob_tactic_expr } - module Cmap = Map.Make(Constr) let from_carrier = Summary.ref Cmap.empty ~name:"ring-tac-carrier-table" @@ -595,13 +571,6 @@ let dest_morph env sigma m_spec = (c,czero,cone,cadd,cmul,None,None,ceqb,phi) | _ -> error "bad morphism structure" - -type 'constr coeff_spec = - Computational of 'constr (* equality test *) - | Abstract (* coeffs = Z *) - | Morphism of 'constr (* general morphism *) - - let reflect_coeff rkind = (* We build an ill-typed terms on purpose... *) match rkind with @@ -609,10 +578,6 @@ let reflect_coeff rkind = | Computational c -> lapp coq_comp [|c|] | Morphism m -> lapp coq_morph [|m|] -type cst_tac_spec = - CstTac of raw_tactic_expr - | Closed of reference list - let interp_cst_tac env sigma rk kind (zero,one,add,mul,opp) cst_tac = match cst_tac with Some (CstTac t) -> Tacintern.glob_tactic t @@ -716,41 +681,12 @@ let add_theory name (sigma,rth) eqth morphth cst_tac (pre,post) power sign div = ring_post_tac = posttac }) in () -type 'constr ring_mod = - Ring_kind of 'constr coeff_spec - | Const_tac of cst_tac_spec - | Pre_tac of raw_tactic_expr - | Post_tac of raw_tactic_expr - | Setoid of Constrexpr.constr_expr * Constrexpr.constr_expr - | Pow_spec of cst_tac_spec * Constrexpr.constr_expr - (* Syntaxification tactic , correctness lemma *) - | Sign_spec of Constrexpr.constr_expr - | Div_spec of Constrexpr.constr_expr - - let ic_coeff_spec = function | Computational t -> Computational (ic_unsafe t) | Morphism t -> Morphism (ic_unsafe t) | Abstract -> Abstract -VERNAC ARGUMENT EXTEND ring_mod - | [ "decidable" constr(eq_test) ] -> [ Ring_kind(Computational eq_test) ] - | [ "abstract" ] -> [ Ring_kind Abstract ] - | [ "morphism" constr(morph) ] -> [ Ring_kind(Morphism morph) ] - | [ "constants" "[" tactic(cst_tac) "]" ] -> [ Const_tac(CstTac cst_tac) ] - | [ "closed" "[" ne_global_list(l) "]" ] -> [ Const_tac(Closed l) ] - | [ "preprocess" "[" tactic(pre) "]" ] -> [ Pre_tac pre ] - | [ "postprocess" "[" tactic(post) "]" ] -> [ Post_tac post ] - | [ "setoid" constr(sth) constr(ext) ] -> [ Setoid(sth,ext) ] - | [ "sign" constr(sign_spec) ] -> [ Sign_spec sign_spec ] - | [ "power" constr(pow_spec) "[" ne_global_list(l) "]" ] -> - [ Pow_spec (Closed l, pow_spec) ] - | [ "power_tac" constr(pow_spec) "[" tactic(cst_tac) "]" ] -> - [ Pow_spec (CstTac cst_tac, pow_spec) ] - | [ "div" constr(div_spec) ] -> [ Div_spec div_spec ] -END - let set_once s r v = if Option.is_empty !r then r := Some v else error (s^" cannot be set twice") @@ -775,20 +711,6 @@ let process_ring_mods l = let k = match !kind with Some k -> k | None -> Abstract in (k, !set, !cst_tac, !pre, !post, !power, !sign, !div) -VERNAC COMMAND EXTEND AddSetoidRing CLASSIFIED AS SIDEFF - | [ "Add" "Ring" ident(id) ":" constr(t) ring_mods(l) ] -> - [ let (k,set,cst,pre,post,power,sign, div) = process_ring_mods l in - add_theory id (ic t) set k cst (pre,post) power sign div] - | [ "Print" "Rings" ] => [Vernac_classifier.classify_as_query] -> [ - msg_notice (strbrk "The following ring structures have been declared:"); - Spmap.iter (fun fn fi -> - msg_notice (hov 2 - (Ppconstr.pr_id (Libnames.basename fn)++spc()++ - str"with carrier "++ pr_constr fi.ring_carrier++spc()++ - str"and equivalence relation "++ pr_constr fi.ring_req)) - ) !from_name ] -END - (*****************************************************************************) (* The tactics consist then only in a lookup in the ring database and call the appropriate ltac. *) @@ -834,13 +756,6 @@ let ring_lookup (f:glob_tactic_expr) lH rl t = with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e end -TACTIC EXTEND ring_lookup -| [ "ring_lookup" tactic0(f) "[" constr_list(lH) "]" ne_constr_list(lrt) ] -> - [ let (t,lr) = List.sep_last lrt in ring_lookup f lH lr t] -END - - - (***********************************************************************) let new_field_path = @@ -914,19 +829,6 @@ let dest_field env evd th_spec = (Some true,r,zero,one,add,mul,None,None,div,inv,req,rth) | _ -> error "bad field structure" -type field_info = - { field_carrier : types; - field_req : constr; - field_cst_tac : glob_tactic_expr; - field_pow_tac : glob_tactic_expr; - field_ok : constr; - field_simpl_eq_ok : constr; - field_simpl_ok : constr; - field_simpl_eq_in_ok : constr; - field_cond : constr; - field_pre_tac : glob_tactic_expr; - field_post_tac : glob_tactic_expr } - let field_from_carrier = Summary.ref Cmap.empty ~name:"field-tac-carrier-table" let field_from_name = Summary.ref Spmap.empty ~name:"field-tac-name-table" @@ -1073,15 +975,6 @@ let add_field_theory name (sigma,fth) eqth morphth cst_tac inj (pre,post) power field_pre_tac = pretac; field_post_tac = posttac }) in () -type 'constr field_mod = - Ring_mod of 'constr ring_mod - | Inject of Constrexpr.constr_expr - -VERNAC ARGUMENT EXTEND field_mod - | [ ring_mod(m) ] -> [ Ring_mod m ] - | [ "completeness" constr(inj) ] -> [ Inject inj ] -END - let process_field_mods l = let kind = ref None in let set = ref None in @@ -1106,21 +999,6 @@ let process_field_mods l = let k = match !kind with Some k -> k | None -> Abstract in (k, !set, !inj, !cst_tac, !pre, !post, !power, !sign, !div) -VERNAC COMMAND EXTEND AddSetoidField CLASSIFIED AS SIDEFF -| [ "Add" "Field" ident(id) ":" constr(t) field_mods(l) ] -> - [ let (k,set,inj,cst_tac,pre,post,power,sign,div) = process_field_mods l in - add_field_theory id (ic t) set k cst_tac inj (pre,post) power sign div] -| [ "Print" "Fields" ] => [Vernac_classifier.classify_as_query] -> [ - msg_notice (strbrk "The following field structures have been declared:"); - Spmap.iter (fun fn fi -> - msg_notice (hov 2 - (Ppconstr.pr_id (Libnames.basename fn)++spc()++ - str"with carrier "++ pr_constr fi.field_carrier++spc()++ - str"and equivalence relation "++ pr_constr fi.field_req)) - ) !field_from_name ] -END - - let ltac_field_structure e = let req = carg e.field_req in let cst_tac = Tacexp e.field_cst_tac in @@ -1149,9 +1027,3 @@ let field_lookup (f:glob_tactic_expr) lH rl t = Proofview.tclTHEN (Proofview.Unsafe.tclEVARS !evdref) (ltac_apply f (field@[lH;rl])) with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e end - - -TACTIC EXTEND field_lookup -| [ "field_lookup" tactic(f) "[" constr_list(lH) "]" ne_constr_list(lt) ] -> - [ let (t,l) = List.sep_last lt in field_lookup f lH l t ] -END diff --git a/plugins/setoid_ring/newring.mli b/plugins/setoid_ring/newring.mli new file mode 100644 index 0000000000..4bd3383d65 --- /dev/null +++ b/plugins/setoid_ring/newring.mli @@ -0,0 +1,78 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +open Names +open Constr +open Libnames +open Globnames +open Constrexpr +open Tacexpr +open Proof_type +open Newring_ast + +val protect_tac_in : string -> Id.t -> tactic + +val protect_tac : string -> tactic + +val closed_term : constr -> global_reference list -> tactic + +val process_ring_mods : + constr_expr ring_mod list -> + constr coeff_spec * (constr * constr) option * + cst_tac_spec option * raw_tactic_expr option * + raw_tactic_expr option * + (cst_tac_spec * constr_expr) option * + constr_expr option * constr_expr option + +val add_theory : + Id.t -> + Evd.evar_map * constr -> + (constr * constr) option -> + constr coeff_spec -> + cst_tac_spec option -> + raw_tactic_expr option * raw_tactic_expr option -> + (cst_tac_spec * constr_expr) option -> + constr_expr option -> + constr_expr option -> unit + +val ic : constr_expr -> Evd.evar_map * constr + +val from_name : ring_info Spmap.t ref + +val ring_lookup : + glob_tactic_expr -> + constr list -> + constr list -> constr -> unit Proofview.tactic + +val process_field_mods : + constr_expr field_mod list -> + constr coeff_spec * + (constr * constr) option * constr option * + cst_tac_spec option * raw_tactic_expr option * + raw_tactic_expr option * + (cst_tac_spec * constr_expr) option * + constr_expr option * constr_expr option + +val add_field_theory : + Id.t -> + Evd.evar_map * constr -> + (constr * constr) option -> + constr coeff_spec -> + cst_tac_spec option -> + constr option -> + raw_tactic_expr option * raw_tactic_expr option -> + (cst_tac_spec * constr_expr) option -> + constr_expr option -> + constr_expr option -> unit + +val field_from_name : field_info Spmap.t ref + +val field_lookup : + glob_tactic_expr -> + constr list -> + constr list -> constr -> unit Proofview.tactic diff --git a/plugins/setoid_ring/newring_ast.mli b/plugins/setoid_ring/newring_ast.mli new file mode 100644 index 0000000000..c26fcc8d1f --- /dev/null +++ b/plugins/setoid_ring/newring_ast.mli @@ -0,0 +1,63 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +open Constr +open Libnames +open Constrexpr +open Tacexpr + +type 'constr coeff_spec = + Computational of 'constr (* equality test *) + | Abstract (* coeffs = Z *) + | Morphism of 'constr (* general morphism *) + +type cst_tac_spec = + CstTac of raw_tactic_expr + | Closed of reference list + +type 'constr ring_mod = + Ring_kind of 'constr coeff_spec + | Const_tac of cst_tac_spec + | Pre_tac of raw_tactic_expr + | Post_tac of raw_tactic_expr + | Setoid of constr_expr * constr_expr + | Pow_spec of cst_tac_spec * constr_expr + (* Syntaxification tactic , correctness lemma *) + | Sign_spec of constr_expr + | Div_spec of constr_expr + +type 'constr field_mod = + Ring_mod of 'constr ring_mod + | Inject of constr_expr + +type ring_info = + { ring_carrier : types; + ring_req : constr; + ring_setoid : constr; + ring_ext : constr; + ring_morph : constr; + ring_th : constr; + ring_cst_tac : glob_tactic_expr; + ring_pow_tac : glob_tactic_expr; + ring_lemma1 : constr; + ring_lemma2 : constr; + ring_pre_tac : glob_tactic_expr; + ring_post_tac : glob_tactic_expr } + +type field_info = + { field_carrier : types; + field_req : constr; + field_cst_tac : glob_tactic_expr; + field_pow_tac : glob_tactic_expr; + field_ok : constr; + field_simpl_eq_ok : constr; + field_simpl_ok : constr; + field_simpl_eq_in_ok : constr; + field_cond : constr; + field_pre_tac : glob_tactic_expr; + field_post_tac : glob_tactic_expr } diff --git a/plugins/setoid_ring/newring_plugin.mllib b/plugins/setoid_ring/newring_plugin.mllib index a98392f1e0..7d6c495889 100644 --- a/plugins/setoid_ring/newring_plugin.mllib +++ b/plugins/setoid_ring/newring_plugin.mllib @@ -1,2 +1,3 @@ Newring Newring_plugin_mod +G_newring diff --git a/pretyping/pretyping.mllib b/pretyping/pretyping.mllib index 25d17c7c9f..436f61d7b6 100644 --- a/pretyping/pretyping.mllib +++ b/pretyping/pretyping.mllib @@ -1,7 +1,4 @@ Locusops -Termops -Namegen -Evd Reductionops Vnorm Inductiveops diff --git a/printing/pptactic.ml b/printing/pptactic.ml index f8264e5af6..a76d73006a 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -34,13 +34,14 @@ type pp_tactic = { } (* ML Extensions *) -let prtac_tab = Hashtbl.create 17 +let prtac_tab : (ml_tactic_name, pp_tactic array) Hashtbl.t = + Hashtbl.create 17 (* Tactic notations *) let prnotation_tab = Summary.ref ~name:"pptactic-notation" KNmap.empty let declare_ml_tactic_pprule key pt = - Hashtbl.add prtac_tab (key, pt.pptac_args) pt.pptac_prods + Hashtbl.add prtac_tab key pt let declare_notation_tactic_pprule kn pt = prnotation_tab := KNmap.add kn pt !prnotation_tab @@ -414,14 +415,18 @@ module Make in pr_sequence (fun x -> x) l - let pr_extend_gen pr_gen lev s l = + let pr_extend_gen pr_gen lev { mltac_name = s; mltac_index = i } l = try - let tags = List.map genarg_tag l in - let (lev',pl) = Hashtbl.find prtac_tab (s,tags) in + let pp_rules = Hashtbl.find prtac_tab s in + let pp = pp_rules.(i) in + let (lev', pl) = pp.pptac_prods in let p = pr_tacarg_using_rule pr_gen (pl,l) in if lev' > lev then surround p else p with Not_found -> - let name = str s.mltac_plugin ++ str "::" ++ str s.mltac_tactic in + let name = + str s.mltac_plugin ++ str "::" ++ str s.mltac_tactic ++ + str "@" ++ int i + in let args = match l with | [] -> mt () | _ -> spc() ++ pr_sequence pr_gen l @@ -756,7 +761,7 @@ module Make pr_reference : 'ref -> std_ppcmds; pr_name : 'nam -> std_ppcmds; pr_generic : 'lev generic_argument -> std_ppcmds; - pr_extend : int -> ml_tactic_name -> 'lev generic_argument list -> std_ppcmds; + pr_extend : int -> ml_tactic_entry -> 'lev generic_argument list -> std_ppcmds; pr_alias : int -> KerName.t -> 'lev generic_argument list -> std_ppcmds; } diff --git a/printing/pptactic.mli b/printing/pptactic.mli index fa91aefcf3..30b9483db7 100644 --- a/printing/pptactic.mli +++ b/printing/pptactic.mli @@ -48,7 +48,7 @@ type pp_tactic = { pptac_prods : int * grammar_terminals; } -val declare_ml_tactic_pprule : ml_tactic_name -> pp_tactic -> unit +val declare_ml_tactic_pprule : ml_tactic_name -> pp_tactic array -> unit val declare_notation_tactic_pprule : KerName.t -> pp_tactic -> unit (** The default pretty-printers produce {!Pp.std_ppcmds} that are diff --git a/printing/pptacticsig.mli b/printing/pptacticsig.mli index 166a6675c1..1631bda377 100644 --- a/printing/pptacticsig.mli +++ b/printing/pptacticsig.mli @@ -59,19 +59,19 @@ module type Pp = sig (constr_expr -> std_ppcmds) -> (constr_expr -> std_ppcmds) -> (tolerability -> raw_tactic_expr -> std_ppcmds) -> (constr_expr -> std_ppcmds) -> int -> - ml_tactic_name -> raw_generic_argument list -> std_ppcmds + ml_tactic_entry -> raw_generic_argument list -> std_ppcmds val pr_glob_extend: (glob_constr_and_expr -> std_ppcmds) -> (glob_constr_and_expr -> std_ppcmds) -> (tolerability -> glob_tactic_expr -> std_ppcmds) -> (glob_constr_pattern_and_expr -> std_ppcmds) -> int -> - ml_tactic_name -> glob_generic_argument list -> std_ppcmds + ml_tactic_entry -> glob_generic_argument list -> std_ppcmds val pr_extend : (Term.constr -> std_ppcmds) -> (Term.constr -> std_ppcmds) -> (tolerability -> glob_tactic_expr -> std_ppcmds) -> (constr_pattern -> std_ppcmds) -> int -> - ml_tactic_name -> typed_generic_argument list -> std_ppcmds + ml_tactic_entry -> typed_generic_argument list -> std_ppcmds val pr_ltac_constant : Nametab.ltac_constant -> std_ppcmds diff --git a/proofs/proofs.mllib b/proofs/proofs.mllib index 32bf5576fa..1bd701cb9b 100644 --- a/proofs/proofs.mllib +++ b/proofs/proofs.mllib @@ -4,8 +4,6 @@ Evar_refiner Proof_using Proof_type Proof_errors -Logic_monad -Proofview_monad Logic Proofview Proof diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index e97a42e6e4..c0fe514f08 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -184,7 +184,7 @@ let with_prods nprods poly (c, clenv) f gls = let rec e_trivial_fail_db db_list local_db goal = let tacl = - Eauto.registered_e_assumption :: + Proofview.V82.of_tactic Eauto.registered_e_assumption :: (tclTHEN (Proofview.V82.of_tactic Tactics.intro) (function g'-> let d = pf_last_hyp g' in diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4 index 3d98bc6e19..789bcd1bdd 100644 --- a/tactics/eauto.ml4 +++ b/tactics/eauto.ml4 @@ -33,27 +33,35 @@ DECLARE PLUGIN "eauto" let eauto_unif_flags = auto_flags_of_state full_transparent_state -let e_give_exact ?(flags=eauto_unif_flags) c gl = let t1 = (pf_type_of gl c) and t2 = pf_concl gl in +let e_give_exact ?(flags=eauto_unif_flags) c = + Proofview.Goal.nf_enter begin fun gl -> + let t1 = Tacmach.New.pf_type_of gl c in + let t2 = Tacmach.New.pf_concl gl in if occur_existential t1 || occur_existential t2 then - tclTHEN (Proofview.V82.of_tactic (Clenvtac.unify ~flags t1)) (exact_no_check c) gl - else Proofview.V82.of_tactic (exact_check c) gl + Tacticals.New.tclTHEN (Clenvtac.unify ~flags t1) (Proofview.V82.tactic (exact_no_check c)) + else exact_check c + end let assumption id = e_give_exact (mkVar id) -let e_assumption gl = - tclFIRST (List.map assumption (pf_ids_of_hyps gl)) gl +let e_assumption = + Proofview.Goal.enter begin fun gl -> + Tacticals.New.tclFIRST (List.map assumption (Tacmach.New.pf_ids_of_hyps gl)) + end TACTIC EXTEND eassumption -| [ "eassumption" ] -> [ Proofview.V82.tactic e_assumption ] +| [ "eassumption" ] -> [ e_assumption ] END TACTIC EXTEND eexact -| [ "eexact" constr(c) ] -> [ Proofview.V82.tactic (e_give_exact c) ] +| [ "eexact" constr(c) ] -> [ e_give_exact c ] END -let registered_e_assumption gl = - tclFIRST (List.map (fun id gl -> e_give_exact (mkVar id) gl) - (pf_ids_of_hyps gl)) gl +let registered_e_assumption = + Proofview.Goal.enter begin fun gl -> + Tacticals.New.tclFIRST (List.map (fun id -> e_give_exact (mkVar id)) + (Tacmach.New.pf_ids_of_hyps gl)) + end (************************************************************************) (* PROLOG tactic *) @@ -82,7 +90,7 @@ let one_step l gl = [Proofview.V82.of_tactic Tactics.intro] @ (List.map (fun c -> Proofview.V82.of_tactic (Tactics.Simple.eapply c)) (List.map mkVar (pf_ids_of_hyps gl))) @ (List.map (fun c -> Proofview.V82.of_tactic (Tactics.Simple.eapply c)) l) - @ (List.map assumption (pf_ids_of_hyps gl)) + @ (List.map (fun c -> Proofview.V82.of_tactic (assumption c)) (pf_ids_of_hyps gl)) let rec prolog l n gl = if n <= 0 then error "prolog - failure"; @@ -138,19 +146,21 @@ let e_exact poly flags (c,clenv) = if poly then Clenv.refresh_undefined_univs clenv else clenv, Univ.empty_level_subst in e_give_exact (* ~flags *) (Vars.subst_univs_level_constr subst c) - -let rec e_trivial_fail_db db_list local_db goal = + +let rec e_trivial_fail_db db_list local_db = + let next = Proofview.Goal.nf_enter begin fun gl -> + let d = Tacmach.New.pf_last_hyp gl in + let hintl = make_resolve_hyp (Tacmach.New.pf_env gl) (Proofview.Goal.sigma gl) d in + e_trivial_fail_db db_list (Hint_db.add_list hintl local_db) + end in + Proofview.Goal.enter begin fun gl -> let tacl = registered_e_assumption :: - (tclTHEN (Proofview.V82.of_tactic Tactics.intro) - (function g'-> - let d = pf_last_hyp g' in - let hintl = make_resolve_hyp (pf_env g') (project g') d in - (e_trivial_fail_db db_list - (Hint_db.add_list hintl local_db) g'))) :: - (List.map fst (e_trivial_resolve db_list local_db (pf_concl goal)) ) + (Tacticals.New.tclTHEN Tactics.intro next) :: + (List.map fst (e_trivial_resolve db_list local_db (Tacmach.New.pf_nf_concl gl))) in - tclFIRST (List.map tclCOMPLETE tacl) goal + Tacticals.New.tclFIRST (List.map Tacticals.New.tclCOMPLETE tacl) + end and e_my_find_search db_list local_db hdc concl = let hint_of_db = hintmap_of hdc concl in @@ -164,14 +174,14 @@ and e_my_find_search db_list local_db hdc concl = (b, let tac = match t with - | Res_pf (term,cl) -> Proofview.V82.of_tactic (unify_resolve poly st (term,cl)) - | ERes_pf (term,cl) -> unify_e_resolve poly st (term,cl) + | Res_pf (term,cl) -> unify_resolve poly st (term,cl) + | ERes_pf (term,cl) -> Proofview.V82.tactic (unify_e_resolve poly st (term,cl)) | Give_exact (c,cl) -> e_exact poly st (c,cl) | Res_pf_THEN_trivial_fail (term,cl) -> - tclTHEN (unify_e_resolve poly st (term,cl)) - (e_trivial_fail_db db_list local_db) - | Unfold_nth c -> reduce (Unfold [AllOccurrences,c]) onConcl - | Extern tacast -> Proofview.V82.of_tactic (conclPattern concl p tacast) + (Tacticals.New.tclTHEN (Proofview.V82.tactic (unify_e_resolve poly st (term,cl))) + (e_trivial_fail_db db_list local_db)) + | Unfold_nth c -> Proofview.V82.tactic (reduce (Unfold [AllOccurrences,c]) onConcl) + | Extern tacast -> conclPattern concl p tacast in (tac,lazy (pr_autotactic t))) in @@ -223,7 +233,7 @@ module SearchProblem = struct | [] -> [] | (tac,pptac) :: tacl -> try - let lgls = apply_tac_list tac glls in + let lgls = apply_tac_list (Proofview.V82.of_tactic tac) glls in (* let gl = Proof_trees.db_pr_goal (List.hd (sig_it glls)) in *) (* msg (hov 1 (pptac ++ str" gives: \n" ++ pr_goals lgls ++ str"\n")); *) (lgls,pptac) :: aux tacl @@ -272,7 +282,7 @@ module SearchProblem = struct { depth = s.depth; tacres = res; last_tactic = pp; dblist = s.dblist; localdb = ldb :: List.tl s.localdb; prev = ps }) - (filter_tactics s.tacres [Proofview.V82.of_tactic Tactics.intro,lazy (str "intro")]) + (filter_tactics s.tacres [Tactics.intro,lazy (str "intro")]) in let rec_tacs = let l = diff --git a/tactics/eauto.mli b/tactics/eauto.mli index 7073e8a2b8..b55c70fa12 100644 --- a/tactics/eauto.mli +++ b/tactics/eauto.mli @@ -21,11 +21,11 @@ val wit_auto_using : Genarg.genarg_type -val e_assumption : tactic +val e_assumption : unit Proofview.tactic -val registered_e_assumption : tactic +val registered_e_assumption : unit Proofview.tactic -val e_give_exact : ?flags:Unification.unify_flags -> constr -> tactic +val e_give_exact : ?flags:Unification.unify_flags -> constr -> unit Proofview.tactic val gen_eauto : ?debug:Tacexpr.debug -> bool * int -> open_constr list -> hint_db_name list option -> tactic diff --git a/tactics/tacenv.ml b/tactics/tacenv.ml index 84c0a99b18..53f3f5652c 100644 --- a/tactics/tacenv.ml +++ b/tactics/tacenv.ml @@ -47,7 +47,7 @@ let pr_tacname t = let tac_tab = ref MLTacMap.empty -let register_ml_tactic ?(overwrite = false) s (t : ml_tactic) = +let register_ml_tactic ?(overwrite = false) s (t : ml_tactic array) = let () = if MLTacMap.mem s !tac_tab then if overwrite then @@ -58,9 +58,11 @@ let register_ml_tactic ?(overwrite = false) s (t : ml_tactic) = in tac_tab := MLTacMap.add s t !tac_tab -let interp_ml_tactic s = +let interp_ml_tactic { mltac_name = s; mltac_index = i } = try - MLTacMap.find s !tac_tab + let tacs = MLTacMap.find s !tac_tab in + let () = if Array.length tacs <= i then raise Not_found in + tacs.(i) with Not_found -> Errors.errorlabstrm "" (str "The tactic " ++ str (pr_tacname s) ++ str " is not installed.") diff --git a/tactics/tacenv.mli b/tactics/tacenv.mli index 29677fd4ca..424bb142c7 100644 --- a/tactics/tacenv.mli +++ b/tactics/tacenv.mli @@ -48,8 +48,8 @@ type ml_tactic = typed_generic_argument list -> Geninterp.interp_sign -> unit Proofview.tactic (** Type of external tactics, used by [TacML]. *) -val register_ml_tactic : ?overwrite:bool -> ml_tactic_name -> ml_tactic -> unit +val register_ml_tactic : ?overwrite:bool -> ml_tactic_name -> ml_tactic array -> unit (** Register an external tactic. *) -val interp_ml_tactic : ml_tactic_name -> ml_tactic +val interp_ml_tactic : ml_tactic_entry -> ml_tactic (** Get the named tactic. Raises a user error if it does not exist. *) diff --git a/tactics/tauto.ml4 b/tactics/tauto.ml4 index 4b03ff249f..e6f33a47be 100644 --- a/tactics/tauto.ml4 +++ b/tactics/tauto.ml4 @@ -159,6 +159,8 @@ let flatten_contravariant_conj flags ist = let constructor i = let name = { Tacexpr.mltac_plugin = "coretactics"; mltac_tactic = "constructor" } in + (** Take care of the index: this is the second entry in constructor. *) + let name = { Tacexpr.mltac_name = name; mltac_index = 1 } in let i = in_gen (rawwit Constrarg.wit_int_or_var) (Misctypes.ArgArg i) in Tacexpr.TacML (Loc.ghost, name, [i]) diff --git a/test-suite/bugs/closed/3911.v b/test-suite/bugs/closed/3911.v new file mode 100644 index 0000000000..b289eafbf4 --- /dev/null +++ b/test-suite/bugs/closed/3911.v @@ -0,0 +1,26 @@ +(* Tested against coq ee596bc *) + +Set Nonrecursive Elimination Schemes. +Set Primitive Projections. +Set Universe Polymorphism. + +Record setoid := { base : Type }. + +Definition catdata (Obj Arr : Type) : Type := nat. + (* [nat] can be replaced by any other type, it seems, + without changing the error *) + +Record cat : Type := + { + obj : setoid; + arr : Type; + dta : catdata (base obj) arr + }. + +Definition bcwa (C:cat) (B:setoid) :Type := nat. + (* As above, nothing special about [nat] here. *) + +Record temp {C}{B} (e:bcwa C B) := + { fld : base (obj C) }. + +Print temp_rect. diff --git a/test-suite/bugs/closed/3929.v b/test-suite/bugs/closed/3929.v new file mode 100644 index 0000000000..4031dcc45e --- /dev/null +++ b/test-suite/bugs/closed/3929.v @@ -0,0 +1,12 @@ +Goal True. +evar (T:Type). +pose (Z:=nat). +let Tv:=eval cbv [T] in T in +pose (x:=Tv). +revert x. +refine (_ : let x:=Z in True). +let Zv:=eval cbv [Z] in Z in +let Tv:=eval cbv [T] in T in +constr_eq Zv Tv. +Abort. + diff --git a/test-suite/bugs/closed/3957.v b/test-suite/bugs/closed/3957.v new file mode 100644 index 0000000000..e20a6e97f0 --- /dev/null +++ b/test-suite/bugs/closed/3957.v @@ -0,0 +1,6 @@ +Ltac foo tac := tac. + +Goal True. +Proof. +foo subst. +Admitted. diff --git a/test-suite/bugs/opened/3889.v b/test-suite/bugs/opened/3889.v new file mode 100644 index 0000000000..6b287324cc --- /dev/null +++ b/test-suite/bugs/opened/3889.v @@ -0,0 +1,11 @@ +Require Import Program. + +Inductive Even : nat -> Prop := +| evenO : Even O +| evenS : forall n, Odd n -> Even (S n) +with Odd : nat -> Prop := +| oddS : forall n, Even n -> Odd (S n). +Axiom admit : forall {T}, T. +Program Fixpoint doubleE {n} (e : Even n) : Even (2 * n) := admit +with doubleO {n} (o : Odd n) : Odd (S (2 * n)) := _. +Next Obligation of doubleE. diff --git a/test-suite/bugs/opened/3890.v b/test-suite/bugs/opened/3890.v new file mode 100644 index 0000000000..f9ac9be2c8 --- /dev/null +++ b/test-suite/bugs/opened/3890.v @@ -0,0 +1,18 @@ +Class Foo. +Class Bar := b : Type. + +Instance foo : Foo := _. +(* 1 subgoals, subgoal 1 (ID 4) + + ============================ + Foo *) + +Instance bar : Bar. +exact Type. +Defined. +(* bar is defined *) + +About foo. +(* foo not a defined object. *) + +Fail Defined. diff --git a/test-suite/bugs/opened/3916.v b/test-suite/bugs/opened/3916.v new file mode 100644 index 0000000000..fd95503e6b --- /dev/null +++ b/test-suite/bugs/opened/3916.v @@ -0,0 +1,3 @@ +Require Import List. + +Fail Hint Resolve -> in_map. (* Also happens when using <- instead of -> *) diff --git a/test-suite/bugs/opened/3919.v-disabled b/test-suite/bugs/opened/3919.v-disabled new file mode 100644 index 0000000000..0d661de9c4 --- /dev/null +++ b/test-suite/bugs/opened/3919.v-disabled @@ -0,0 +1,13 @@ +Require Import MSets. +Require Import Orders. + +Declare Module Signal : OrderedType. + +Module S := MSetAVL.Make(Signal). +Module Sdec := Decide(S). +Export Sdec. + +Hint Extern 0 (Signal.eq ?x ?y) => now symmetry. + +Goal forall o s, Signal.eq o s. +Proof. fsetdec. Qed. diff --git a/test-suite/bugs/opened/3922.v b/test-suite/bugs/opened/3922.v new file mode 100644 index 0000000000..ce4f509cad --- /dev/null +++ b/test-suite/bugs/opened/3922.v @@ -0,0 +1,83 @@ +Set Universe Polymorphism. +Notation Type0 := Set. + +Definition Type1 := Eval hnf in let gt := (Set : Type@{i}) in Type@{i}. + +Notation compose := (fun g f x => g (f x)). + +Notation "g 'o' f" := (compose g f) (at level 40, left associativity) : function_scope. +Open Scope function_scope. + +Definition pointwise_paths {A} {P:A->Type} (f g:forall x:A, P x) + := forall x:A, f x = g x. + +Notation "f == g" := (pointwise_paths f g) (at level 70, no associativity) : type_scope. + +Class Contr_internal (A : Type) := BuildContr { + center : A ; + contr : (forall y : A, center = y) +}. + +Inductive trunc_index : Type := +| minus_two : trunc_index +| trunc_S : trunc_index -> trunc_index. + +Notation "n .+1" := (trunc_S n) (at level 2, left associativity, format "n .+1") : trunc_scope. +Local Open Scope trunc_scope. +Notation "-2" := minus_two (at level 0) : trunc_scope. +Notation "-1" := (-2.+1) (at level 0) : trunc_scope. + +Fixpoint IsTrunc_internal (n : trunc_index) (A : Type) : Type := + match n with + | -2 => Contr_internal A + | n'.+1 => forall (x y : A), IsTrunc_internal n' (x = y) + end. + +Class IsTrunc (n : trunc_index) (A : Type) : Type := + Trunc_is_trunc : IsTrunc_internal n A. + +Notation Contr := (IsTrunc -2). +Notation IsHProp := (IsTrunc -1). + +Monomorphic Axiom dummy_funext_type : Type0. +Monomorphic Class Funext := { dummy_funext_value : dummy_funext_type }. + +Inductive Unit : Type1 := + tt : Unit. + +Record TruncType (n : trunc_index) := BuildTruncType { + trunctype_type : Type ; + istrunc_trunctype_type : IsTrunc n trunctype_type +}. + +Arguments BuildTruncType _ _ {_}. + +Coercion trunctype_type : TruncType >-> Sortclass. + +Notation "n -Type" := (TruncType n) (at level 1) : type_scope. +Notation hProp := (-1)-Type. + +Notation BuildhProp := (BuildTruncType -1). + +Private Inductive Trunc (n : trunc_index) (A :Type) : Type := + tr : A -> Trunc n A. +Arguments tr {n A} a. + +Global Instance istrunc_truncation (n : trunc_index) (A : Type@{i}) +: IsTrunc@{j} n (Trunc@{i} n A). +Admitted. + +Definition Trunc_ind {n A} + (P : Trunc n A -> Type) {Pt : forall aa, IsTrunc n (P aa)} + : (forall a, P (tr a)) -> (forall aa, P aa) +:= (fun f aa => match aa with tr a => fun _ => f a end Pt). +Definition merely (A : Type@{i}) : hProp@{i} := BuildhProp (Trunc -1 A). +Definition cconst_factors_contr `{Funext} {X Y : Type} (f : X -> Y) + (P : Type) `{Pc : X -> Contr P} + (g : X -> P) (h : P -> Y) (p : h o g == f) +: Unit. +Proof. + assert (merely X -> IsHProp P) by admit. + refine (let g' := Trunc_ind (fun _ => P) g : merely X -> P in _); + [ assumption.. | ]. + Fail pose (g' := Trunc_ind (fun _ => P) g : merely X -> P). diff --git a/test-suite/bugs/opened/3923.v b/test-suite/bugs/opened/3923.v new file mode 100644 index 0000000000..6aa6b4932e --- /dev/null +++ b/test-suite/bugs/opened/3923.v @@ -0,0 +1,33 @@ +Module Type TRIVIAL. +Parameter t:Type. +End TRIVIAL. + +Module MkStore (Key : TRIVIAL). + +Module St : TRIVIAL. +Definition t := unit. +End St. + +End MkStore. + + + +Module Type CERTRUNTIMETYPES (B : TRIVIAL). + +Parameter cert_fieldstore : Type. +Parameter empty_fieldstore : cert_fieldstore. + +End CERTRUNTIMETYPES. + + + +Module MkCertRuntimeTypes (B : TRIVIAL) : CERTRUNTIMETYPES B. + +Module FieldStore := MkStore B. + +Definition cert_fieldstore := FieldStore.St.t. +Axiom empty_fieldstore : cert_fieldstore. + +End MkCertRuntimeTypes. + +Fail Extraction MkCertRuntimeTypes. diff --git a/test-suite/bugs/opened/3926.v b/test-suite/bugs/opened/3926.v new file mode 100644 index 0000000000..cfad763572 --- /dev/null +++ b/test-suite/bugs/opened/3926.v @@ -0,0 +1,30 @@ +Notation compose := (fun g f x => g (f x)). +Notation "g 'o' f" := (compose g f) (at level 40, left associativity) : function_scope. +Open Scope function_scope. +Inductive paths {A : Type} (a : A) : A -> Type := idpath : paths a a where "x = y" := (@paths _ x y) : type_scope. +Arguments idpath {A a} , [A] a. +Definition ap {A B:Type} (f:A -> B) {x y:A} (p:x = y) : f x = f y := match p with idpath => idpath end. +Class IsEquiv {A B : Type} (f : A -> B) := { equiv_inv : B -> A }. +Notation "f ^-1" := (@equiv_inv _ _ f _) (at level 3, format "f '^-1'") : equiv_scope. +Local Open Scope equiv_scope. +Axiom eisretr : forall {A B} (f : A -> B) `{IsEquiv A B f} x, f (f^-1 x) = x. +Generalizable Variables A B C f g. +Global Instance isequiv_compose `{IsEquiv A B f} `{IsEquiv B C g} : IsEquiv (compose g f) | 1000 + := Build_IsEquiv A C (compose g f) (compose f^-1 g^-1). +Definition isequiv_homotopic {A B} (f : A -> B) {g : A -> B} `{IsEquiv A B f} (h : forall x, f x = g x) : IsEquiv g + := Build_IsEquiv _ _ g (f ^-1). +Global Instance isequiv_inverse {A B} (f : A -> B) `{IsEquiv A B f} : IsEquiv f^-1 | 10000 + := Build_IsEquiv B A f^-1 f. +Definition cancelR_isequiv {A B C} (f : A -> B) {g : B -> C} + `{IsEquiv A B f} `{IsEquiv A C (g o f)} + : IsEquiv g. +Proof. + Unset Typeclasses Modulo Eta. + exact (isequiv_homotopic (compose (compose g f) f^-1) + (fun b => ap g (eisretr f b))) || fail "too early". + Undo. + Set Typeclasses Modulo Eta. + Set Typeclasses Dependency Order. + Set Typeclasses Debug. + Fail exact (isequiv_homotopic (compose (compose g f) f^-1) + (fun b => ap g (eisretr f b))). diff --git a/test-suite/bugs/opened/3928.v-disabled b/test-suite/bugs/opened/3928.v-disabled new file mode 100644 index 0000000000..b470eb229b --- /dev/null +++ b/test-suite/bugs/opened/3928.v-disabled @@ -0,0 +1,12 @@ +Typeclasses eauto := bfs. + +Class Foo := {}. +Class Bar := {}. + +Instance: Bar. +Instance: Foo -> Bar -> Foo -> Foo | 1. +Instance: Bar -> Foo | 100. +Instance: Foo -> Bar -> Foo -> Foo | 1. + +Set Typeclasses Debug. +Timeout 1 Check (_ : Foo). (* timeout *) diff --git a/test-suite/bugs/opened/3938.v b/test-suite/bugs/opened/3938.v new file mode 100644 index 0000000000..2d0d1930f1 --- /dev/null +++ b/test-suite/bugs/opened/3938.v @@ -0,0 +1,6 @@ +Require Import Coq.Arith.PeanoNat. +Hint Extern 1 => admit : typeclass_instances. +Goal forall a b (f : nat -> Set), Nat.eq a b -> f a = f b. + intros a b f H. + rewrite H. (* Toplevel input, characters 15-25: +Anomaly: Evar ?X11 was not declared. Please report. *) diff --git a/test-suite/bugs/opened/3946.v b/test-suite/bugs/opened/3946.v new file mode 100644 index 0000000000..e77bdbc652 --- /dev/null +++ b/test-suite/bugs/opened/3946.v @@ -0,0 +1,11 @@ +Require Import ZArith. + +Inductive foo := Foo : Z.le 0 1 -> foo. + +Definition bar (f : foo) := let (f) := f in f. + +(* Doesn't work: *) +(* Arguments bar f.*) + +(* Does work *) +Arguments bar f _. diff --git a/test-suite/bugs/opened/3948.v b/test-suite/bugs/opened/3948.v new file mode 100644 index 0000000000..e5bca6e522 --- /dev/null +++ b/test-suite/bugs/opened/3948.v @@ -0,0 +1,70 @@ +Require Import MSets. +Require Import Utf8. +Require FMaps. +Import Orders. + +Set Implicit Arguments. + +(* Conversion between the two kinds of OrderedType. *) +Module OTconvert (O : OrderedType) : OrderedType.OrderedType + with Definition t := O.t + with Definition eq := O.eq + with Definition lt := O.lt. + + Definition t := O.t. + Definition eq := O.eq. + Definition lt := O.lt. + Definition eq_refl := reflexivity. + Lemma eq_sym : forall x y : t, eq x y -> eq y x. + Admitted. + Lemma eq_trans : forall x y z : t, eq x y -> eq y z -> eq x z. + Admitted. + Lemma lt_trans : forall x y z : t, lt x y -> lt y z -> lt x z. + Admitted. + Lemma lt_not_eq : forall x y : t, lt x y -> ~ eq x y. + Admitted. + Lemma compare : forall x y : t, OrderedType.Compare lt eq x y. + Admitted. + Definition eq_dec := O.eq_dec. +End OTconvert. + +(* Dependent Maps *) +Module Type Interface (X : OrderedType). + Module Dom : MSetInterface.SetsOn(X) with Definition elt := X.t := MSetAVL.Make(X). + Definition key := X.t. + Parameter t : forall (A : Type) (dom : Dom.t), Type. + Parameter constant : forall A dom, A -> t A dom. +End Interface. + +Module DepMap (X : OrderedType) : (Interface X) with Definition key := X.t. + Module Dom := MSetAVL.Make(X). + Module XOT := OTconvert X. + Module S := FMapList.Make(XOT). + Definition key := X.t. + Definition OK {A} dom (map : S.t A) := ∀ x, S.In x map <-> Dom.In x dom. + Definition t := fun A dom => { map : S.t A | OK dom map}. + Corollary constant_OK : forall A dom v, OK dom (Dom.fold (fun x m => S.add x v m) dom (S.empty A)). + Admitted. + Definition constant (A : Type) dom (v : A) : t A dom := + exist (OK dom) (Dom.fold (fun x m => S.add x v m) dom (@S.empty A)) (constant_OK dom v). +End DepMap. + + +Declare Module Signal : OrderedType. +Module S := DepMap(Signal). +Notation "∅" := (S.constant _ false). + +Definition I2Kt {dom} (E : S.t (option bool) dom) : S.t bool dom := S.constant dom false. +Arguments I2Kt {dom} E. + +Inductive cmd := nothing. + +Definition semantics (A T₁ T₂ : Type) := forall dom, T₁ -> S.t A dom -> S.t A dom -> nat -> T₂ -> Prop. + +Inductive LBS : semantics bool cmd cmd := LBSnothing dom (E : S.t bool dom) : LBS nothing E ∅ 0 nothing. + +Theorem CBS_LBS : forall dom p (E E' : S.t _ dom) k p', LBS p (I2Kt E) (I2Kt E') k p'. +admit. +Defined. + +Print Assumptions CBS_LBS. diff --git a/test-suite/bugs/opened/3953.v b/test-suite/bugs/opened/3953.v new file mode 100644 index 0000000000..d90ae31e8f --- /dev/null +++ b/test-suite/bugs/opened/3953.v @@ -0,0 +1,4 @@ +Goal forall (a b : unit), a = b -> exists c, b = c. +intros. +eexists. +Fail subst. diff --git a/test-suite/bugs/opened/3956.v b/test-suite/bugs/opened/3956.v new file mode 100644 index 0000000000..94c0c6744c --- /dev/null +++ b/test-suite/bugs/opened/3956.v @@ -0,0 +1,141 @@ +(* -*- mode: coq; mode: visual-line -*- *) +Set Universe Polymorphism. +Set Primitive Projections. +Close Scope nat_scope. + +Record prod (A B : Type) := pair { fst : A ; snd : B }. +Arguments pair {A B} _ _. +Arguments fst {A B} _ / . +Arguments snd {A B} _ / . +Notation "x * y" := (prod x y) : type_scope. +Notation "( x , y , .. , z )" := (pair .. (pair x y) .. z) : core_scope. + +Definition Type1 := Eval hnf in let gt := (Set : Type@{i}) in Type@{i}. +Definition Type2 := Eval hnf in let gt := (Type1 : Type@{i}) in Type@{i}. + +Inductive paths {A : Type} (a : A) : A -> Type := + idpath : paths a a. +Arguments idpath {A a} , [A] a. +Notation "x = y" := (@paths _ x y) : type_scope. +Definition concat {A} {x y z : A} (p : x = y) (q : y = z) : x = z + := match p, q with idpath, idpath => idpath end. + +Definition path_prod {A B : Type} (z z' : A * B) +: (fst z = fst z') -> (snd z = snd z') -> (z = z'). +Proof. + destruct z, z'; simpl; intros [] []; reflexivity. +Defined. + +Module Type TypeM. + Parameter m : Type2. +End TypeM. + +Module ProdM (XM : TypeM) (YM : TypeM) <: TypeM. + Definition m := XM.m * YM.m. +End ProdM. + +Module Type FunctionM (XM YM : TypeM). + Parameter m : XM.m -> YM.m. +End FunctionM. + +Module IdmapM (XM : TypeM) <: FunctionM XM XM. + Definition m := (fun x => x) : XM.m -> XM.m. +End IdmapM. + +Module Type HomotopyM (XM YM : TypeM) (fM gM : FunctionM XM YM). + Parameter m : forall x, fM.m x = gM.m x. +End HomotopyM. + +Module ComposeM (XM YM ZM : TypeM) + (gM : FunctionM YM ZM) (fM : FunctionM XM YM) + <: FunctionM XM ZM. + Definition m := (fun x => gM.m (fM.m x)). +End ComposeM. + +Module Type CorecM (YM ZM : TypeM) (fM : FunctionM YM ZM) + (XM : TypeM) (gM : FunctionM XM ZM). + Parameter m : XM.m -> YM.m. + Parameter m_beta : forall x, fM.m (m x) = gM.m x. +End CorecM. + +Module Type CoindpathsM (YM ZM : TypeM) (fM : FunctionM YM ZM) + (XM : TypeM) (hM kM : FunctionM XM YM). + Module fhM := ComposeM XM YM ZM fM hM. + Module fkM := ComposeM XM YM ZM fM kM. + Declare Module mM (pM : HomotopyM XM ZM fhM fkM) + : HomotopyM XM YM hM kM. +End CoindpathsM. + +Module Type Comodality (XM : TypeM). + Parameter m : Type2. + Module mM <: TypeM. + Definition m := m. + End mM. + Parameter from : m -> XM.m. + Module fromM <: FunctionM mM XM. + Definition m := from. + End fromM. + Declare Module corecM : CorecM mM XM fromM. + Declare Module coindpathsM : CoindpathsM mM XM fromM. +End Comodality. + +Module Comodality_Theory (F : Comodality). + + Module F_functor_M (XM YM : TypeM) (fM : FunctionM XM YM) + (FXM : Comodality XM) (FYM : Comodality YM). + Module f_o_from_M <: FunctionM FXM.mM YM. + Definition m := fun x => fM.m (FXM.from x). + End f_o_from_M. + Module mM := FYM.corecM FXM.mM f_o_from_M. + Definition m := mM.m. + End F_functor_M. + + Module F_prod_cmp_M (XM YM : TypeM) + (FXM : Comodality XM) (FYM : Comodality YM). + Module PM := ProdM XM YM. + Module PFM := ProdM FXM FYM. + Module fstM <: FunctionM PM XM. + Definition m := @fst XM.m YM.m. + End fstM. + Module sndM <: FunctionM PM YM. + Definition m := @snd XM.m YM.m. + End sndM. + Module FPM := F PM. + Module FfstM := F_functor_M PM XM fstM FPM FXM. + Module FsndM := F_functor_M PM YM sndM FPM FYM. + Definition m : FPM.m -> PFM.m + := fun z => (FfstM.m z , FsndM.m z). + End F_prod_cmp_M. + + Module isequiv_F_prod_cmp_M + (XM YM : TypeM) + (FXM : Comodality XM) (FYM : Comodality YM). + (** The comparison map *) + Module cmpM := F_prod_cmp_M XM YM FXM FYM. + Module FPM := cmpM.FPM. + (** We construct an inverse to it using corecursion. *) + Module prod_from_M <: FunctionM cmpM.PFM cmpM.PM. + Definition m : cmpM.PFM.m -> cmpM.PM.m + := fun z => ( FXM.from (fst z) , FYM.from (snd z) ). + End prod_from_M. + Module cmpinvM <: FunctionM cmpM.PFM FPM + := FPM.corecM cmpM.PFM prod_from_M. + (** We prove the first homotopy *) + Module cmpinv_o_cmp_M <: FunctionM FPM FPM + := ComposeM FPM cmpM.PFM FPM cmpinvM cmpM. + Module idmap_FPM <: FunctionM FPM FPM + := IdmapM FPM. + Module cip_FPM := FPM.coindpathsM FPM cmpinv_o_cmp_M idmap_FPM. + Module cip_FPHM <: HomotopyM FPM cmpM.PM cip_FPM.fhM cip_FPM.fkM. + Definition m : forall x, cip_FPM.fhM.m@{i j} x = cip_FPM.fkM.m@{i j} x. + Proof. + intros x. + refine (concat (cmpinvM.m_beta@{i j} (cmpM.m@{i j} x)) _). + apply path_prod@{i i i}; simpl. + - exact (cmpM.FfstM.mM.m_beta@{i j} x). + - exact (cmpM.FsndM.mM.m_beta@{i j} x). + Defined. + Fail End cip_FPHM. +(* End isequiv_F_prod_cmp_M. + +End Comodality_Theory.*) diff --git a/test-suite/success/decl_mode2.v b/test-suite/success/decl_mode2.v new file mode 100644 index 0000000000..4475b5d479 --- /dev/null +++ b/test-suite/success/decl_mode2.v @@ -0,0 +1,246 @@ +Theorem this_is_trivial: True. +proof. + thus thesis. +end proof. +Qed. + +Theorem T: (True /\ True) /\ True. + split. split. +proof. (* first subgoal *) + thus thesis. +end proof. +trivial. (* second subgoal *) +proof. (* third subgoal *) + thus thesis. +end proof. +Abort. + +Theorem this_is_not_so_trivial: False. +proof. +end proof. (* here a warning is issued *) +Fail Qed. (* fails: the proof in incomplete *) +Admitted. (* Oops! *) + +Theorem T: True. +proof. +escape. +auto. +return. +Abort. + +Theorem T: let a:=false in let b:= true in ( if a then True else False -> if b then True else False). +intros a b. +proof. +assume H:(if a then True else False). +reconsider H as False. +reconsider thesis as True. +Abort. + +Theorem T: forall x, x=2 -> 2+x=4. +proof. +let x be such that H:(x=2). +have H':(2+x=2+2) by H. +Abort. + +Theorem T: forall x, x=2 -> 2+x=4. +proof. +let x be such that H:(x=2). +then (2+x=2+2). +Abort. + +Theorem T: forall x, x=2 -> x + x = x * x. +proof. +let x be such that H:(x=2). +have (4 = 4). + ~= (2 * 2). + ~= (x * x) by H. + =~ (2 + 2). + =~ H':(x + x) by H. +Abort. + +Theorem T: forall x, x + x = x * x -> x = 0 \/ x = 2. +proof. +let x be such that H:(x + x = x * x). +claim H':((x - 2) * x = 0). +thus thesis. +end claim. +Abort. + +Theorem T: forall (A B:Prop), A -> B -> A /\ B. +intros A B HA HB. +proof. +hence B. +Abort. + +Theorem T: forall (A B C:Prop), A -> B -> C -> A /\ B /\ C. +intros A B C HA HB HC. +proof. +thus B by HB. +Abort. + +Theorem T: forall (A B C:Prop), A -> B -> C -> A /\ B. +intros A B C HA HB HC. +proof. +hence C. (* fails *) +Abort. + +Theorem T: forall (A B:Prop), B -> A \/ B. +intros A B HB. +proof. +hence B. +Abort. + +Theorem T: forall (A B C D:Prop), C -> D -> (A /\ B) \/ (C /\ D). +intros A B C D HC HD. +proof. +thus C by HC. +Abort. + +Theorem T: forall (P:nat -> Prop), P 2 -> exists x,P x. +intros P HP. +proof. +take 2. +Abort. + +Theorem T: forall (P:nat -> Prop), P 2 -> exists x,P x. +intros P HP. +proof. +hence (P 2). +Abort. + +Theorem T: forall (P:nat -> Prop) (R:nat -> nat -> Prop), P 2 -> R 0 2 -> exists x, exists y, P y /\ R x y. +intros P R HP HR. +proof. +thus (P 2) by HP. +Abort. + +Theorem T: forall (A B:Prop) (P:nat -> Prop), (forall x, P x -> B) -> A -> A /\ B. +intros A B P HP HA. +proof. +suffices to have x such that HP':(P x) to show B by HP,HP'. +Abort. + +Theorem T: forall (A:Prop) (P:nat -> Prop), P 2 -> A -> A /\ (forall x, x = 2 -> P x). +intros A P HP HA. +proof. +focus on (forall x, x = 2 -> P x). +let x be such that (x = 2). +hence thesis by HP. +end focus. +Abort. + +Theorem T: forall x, x = 0 -> x + x = x * x. +proof. +let x be such that H:(x = 0). +define sqr x as (x * x). +reconsider thesis as (x + x = sqr x). +Abort. + +Theorem T: forall (P:nat -> Prop), forall x, P x -> P x. +proof. +let P:(nat -> Prop). +let x:nat. +assume HP:(P x). +Abort. + +Theorem T: forall (P:nat -> Prop), forall x, P x -> P x. +proof. +let P:(nat -> Prop). +let x. (* fails because x's type is not clear *) +let x be such that HP:(P x). (* here x's type is inferred from (P x) *) +Abort. + +Theorem T: forall (P:nat -> Prop), forall x, P x -> P x -> P x. +proof. +let P:(nat -> Prop). +let x:nat. +assume (P x). (* temporary name created *) +Abort. + +Theorem T: forall (P:nat -> Prop), forall x, P x -> P x. +proof. +let P:(nat -> Prop). +let x be such that (P x). (* temporary name created *) +Abort. + +Theorem T: forall (P:nat -> Prop) (A:Prop), (exists x, (P x /\ A)) -> A. +proof. +let P:(nat -> Prop),A:Prop be such that H:(exists x, P x /\ A). +consider x such that HP:(P x) and HA:A from H. +Abort. + +Here is an example with pairs: + +Theorem T: forall p:(nat * nat)%type, (fst p >= snd p) \/ (fst p < snd p). +proof. +let p:(nat * nat)%type. +consider x:nat,y:nat from p. +reconsider thesis as (x >= y \/ x < y). +Abort. + +Theorem T: forall P:(nat -> Prop), (forall n, P n -> P (n - 1)) -> +(exists m, P m) -> P 0. +proof. +let P:(nat -> Prop) be such that HP:(forall n, P n -> P (n - 1)). +given m such that Hm:(P m). +Abort. + +Theorem T: forall (A B C:Prop), (A -> C) -> (B -> C) -> (A \/ B) -> C. +proof. +let A:Prop,B:Prop,C:Prop be such that HAC:(A -> C) and HBC:(B -> C). +assume HAB:(A \/ B). +per cases on HAB. +suppose A. + hence thesis by HAC. +suppose HB:B. + thus thesis by HB,HBC. +end cases. +Abort. + +Section Coq. + +Hypothesis EM : forall P:Prop, P \/ ~ P. + +Theorem T: forall (A C:Prop), (A -> C) -> (~A -> C) -> C. +proof. +let A:Prop,C:Prop be such that HAC:(A -> C) and HNAC:(~A -> C). +per cases of (A \/ ~A) by EM. +suppose (~A). + hence thesis by HNAC. +suppose A. + hence thesis by HAC. +end cases. +Abort. + +Theorem T: forall (A C:Prop), (A -> C) -> (~A -> C) -> C. +proof. +let A:Prop,C:Prop be such that HAC:(A -> C) and HNAC:(~A -> C). +per cases on (EM A). +suppose (~A). +Abort. +End Coq. + +Theorem T: forall (A B:Prop) (x:bool), (if x then A else B) -> A \/ B. +proof. +let A:Prop,B:Prop,x:bool. +per cases on x. +suppose it is true. + assume A. + hence A. +suppose it is false. + assume B. + hence B. +end cases. +Abort. + +Theorem T: forall (n:nat), n + 0 = n. +proof. +let n:nat. +per induction on n. +suppose it is 0. + thus (0 + 0 = 0). +suppose it is (S m) and H:thesis for m. + then (S (m + 0) = S m). + thus =~ (S m + 0). +end induction. +Abort. diff --git a/theories/Lists/List.v b/theories/Lists/List.v index 3cba090f39..85e364c012 100644 --- a/theories/Lists/List.v +++ b/theories/Lists/List.v @@ -7,7 +7,7 @@ (************************************************************************) Require Setoid. -Require Import PeanoNat Le Gt Minus Bool. +Require Import PeanoNat Le Gt Minus Bool Lt. Set Implicit Arguments. (* Set Universe Polymorphism. *) @@ -1627,6 +1627,80 @@ Section Cutting. end end. + Lemma firstn_nil n: firstn n [] = []. + Proof. induction n; now simpl. Qed. + + Lemma firstn_cons n a l: firstn (S n) (a::l) = a :: (firstn n l). + Proof. now simpl. Qed. + + Lemma firstn_all l: firstn (length l) l = l. + Proof. induction l as [| ? ? H]; simpl; [reflexivity | now rewrite H]. Qed. + + Lemma firstn_all2 n: forall (l:list A), (length l) <= n -> firstn n l = l. + Proof. induction n as [|k iHk]. + - intro. inversion 1 as [H1|?]. + rewrite (length_zero_iff_nil l) in H1. subst. now simpl. + - destruct l as [|x xs]; simpl. + * now reflexivity. + * simpl. intro H. apply Peano.le_S_n in H. f_equal. apply iHk, H. + Qed. + + Lemma firstn_O l: firstn 0 l = []. + Proof. now simpl. Qed. + + Lemma firstn_le_length n: forall l:list A, length (firstn n l) <= n. + Proof. + induction n as [|k iHk]; simpl; [auto | destruct l as [|x xs]; simpl]. + - auto with arith. + - apply Peano.le_n_S, iHk. + Qed. + + Lemma firstn_length_le: forall l:list A, forall n:nat, + n <= length l -> length (firstn n l) = n. + Proof. induction l as [|x xs Hrec]. + - simpl. intros n H. apply le_n_0_eq in H. rewrite <- H. now simpl. + - destruct n. + * now simpl. + * simpl. intro H. apply le_S_n in H. now rewrite (Hrec n H). + Qed. + + Lemma firstn_app n: + forall l1 l2, + firstn n (l1 ++ l2) = (firstn n l1) ++ (firstn (n - length l1) l2). + Proof. induction n as [|k iHk]; intros l1 l2. + - now simpl. + - destruct l1 as [|x xs]. + * unfold firstn at 2, length. now rewrite 2!app_nil_l, <- minus_n_O. + * rewrite <- app_comm_cons. simpl. f_equal. apply iHk. + Qed. + + Lemma firstn_app_2 n: + forall l1 l2, + firstn ((length l1) + n) (l1 ++ l2) = l1 ++ firstn n l2. + Proof. induction n as [| k iHk];intros l1 l2. + - unfold firstn at 2. rewrite <- plus_n_O, app_nil_r. + rewrite firstn_app. rewrite <- minus_diag_reverse. + unfold firstn at 2. rewrite app_nil_r. apply firstn_all. + - destruct l2 as [|x xs]. + * simpl. rewrite app_nil_r. apply firstn_all2. auto with arith. + * rewrite firstn_app. assert (H0 : (length l1 + S k - length l1) = S k). + auto with arith. + rewrite H0, firstn_all2; [reflexivity | auto with arith]. + Qed. + + Lemma firstn_firstn: + forall l:list A, + forall i j : nat, + firstn i (firstn j l) = firstn (min i j) l. + Proof. induction l as [|x xs Hl]. + - intros. simpl. now rewrite ?firstn_nil. + - destruct i. + * intro. now simpl. + * destruct j. + + now simpl. + + simpl. f_equal. apply Hl. + Qed. + Fixpoint skipn (n:nat)(l:list A) : list A := match n with | 0 => l diff --git a/theories/Lists/ListSet.v b/theories/Lists/ListSet.v index 0a0bf0dea0..c8ed95cd45 100644 --- a/theories/Lists/ListSet.v +++ b/theories/Lists/ListSet.v @@ -48,7 +48,11 @@ Section first_definitions. end end. - (** If [a] belongs to [x], removes [a] from [x]. If not, does nothing *) + (** If [a] belongs to [x], removes [a] from [x]. If not, does nothing. + Invariant: any element should occur at most once in [x], see for + instance [set_add]. We hence remove here only the first occurrence + of [a] in [x]. *) + Fixpoint set_remove (a:A) (x:set) : set := match x with | nil => empty_set @@ -227,6 +231,68 @@ Section first_definitions. intros; elim (Aeq_dec a a0); intros; discriminate. Qed. + Lemma set_add_iff a b l : In a (set_add b l) <-> a = b \/ In a l. + Proof. + split. apply set_add_elim. apply set_add_intro. + Qed. + + Lemma set_add_nodup a l : NoDup l -> NoDup (set_add a l). + Proof. + induction 1 as [|x l H H' IH]; simpl. + - constructor; [ tauto | constructor ]. + - destruct (Aeq_dec a x) as [<-|Hax]; constructor; trivial. + rewrite set_add_iff. intuition. + Qed. + + Lemma set_remove_1 (a b : A) (l : set) : + In a (set_remove b l) -> In a l. + Proof. + induction l as [|x xs Hrec]. + - intros. auto. + - simpl. destruct (Aeq_dec b x). + * tauto. + * intro H. destruct H. + + rewrite H. apply in_eq. + + apply in_cons. apply Hrec. assumption. + Qed. + + Lemma set_remove_2 (a b:A) (l : set) : + NoDup l -> In a (set_remove b l) -> a <> b. + Proof. + induction l as [|x l IH]; intro ND; simpl. + - tauto. + - inversion_clear ND. + destruct (Aeq_dec b x) as [<-|Hbx]. + + congruence. + + destruct 1; subst; auto. + Qed. + + Lemma set_remove_3 (a b : A) (l : set) : + In a l -> a <> b -> In a (set_remove b l). + Proof. + induction l as [|x xs Hrec]. + - now simpl. + - simpl. destruct (Aeq_dec b x) as [<-|Hbx]; simpl; intuition. + congruence. + Qed. + + Lemma set_remove_iff (a b : A) (l : set) : + NoDup l -> (In a (set_remove b l) <-> In a l /\ a <> b). + Proof. + split; try split. + - eapply set_remove_1; eauto. + - eapply set_remove_2; eauto. + - destruct 1; apply set_remove_3; auto. + Qed. + + Lemma set_remove_nodup a l : NoDup l -> NoDup (set_remove a l). + Proof. + induction 1 as [|x l H H' IH]; simpl. + - constructor. + - destruct (Aeq_dec a x) as [<-|Hax]; trivial. + constructor; trivial. + rewrite set_remove_iff; trivial. intuition. + Qed. Lemma set_union_intro1 : forall (a:A) (x y:set), set_In a x -> set_In a (set_union x y). @@ -264,18 +330,26 @@ Section first_definitions. tauto. Qed. + Lemma set_union_iff a l l': In a (set_union l l') <-> In a l \/ In a l'. + Proof. + split. apply set_union_elim. apply set_union_intro. + Qed. + + Lemma set_union_nodup l l' : NoDup l -> NoDup l' -> NoDup (set_union l l'). + Proof. + induction 2 as [|x' l' ? ? IH]; simpl; trivial. now apply set_add_nodup. + Qed. + Lemma set_union_emptyL : forall (a:A) (x:set), set_In a (set_union empty_set x) -> set_In a x. intros a x H; case (set_union_elim _ _ _ H); auto || contradiction. Qed. - Lemma set_union_emptyR : forall (a:A) (x:set), set_In a (set_union x empty_set) -> set_In a x. intros a x H; case (set_union_elim _ _ _ H); auto || contradiction. Qed. - Lemma set_inter_intro : forall (a:A) (x y:set), set_In a x -> set_In a y -> set_In a (set_inter x y). @@ -326,6 +400,21 @@ Section first_definitions. eauto with datatypes. Qed. + Lemma set_inter_iff a l l' : In a (set_inter l l') <-> In a l /\ In a l'. + Proof. + split. + - apply set_inter_elim. + - destruct 1. now apply set_inter_intro. + Qed. + + Lemma set_inter_nodup l l' : NoDup l -> NoDup l' -> NoDup (set_inter l l'). + Proof. + induction 1 as [|x l H H' IH]; intro Hl'; simpl. + - constructor. + - destruct (set_mem x l'); auto. + constructor; auto. rewrite set_inter_iff; tauto. + Qed. + Lemma set_diff_intro : forall (a:A) (x y:set), set_In a x -> ~ set_In a y -> set_In a (set_diff x y). @@ -360,6 +449,20 @@ Section first_definitions. rewrite H; trivial. Qed. + Lemma set_diff_iff a l l' : In a (set_diff l l') <-> In a l /\ ~In a l'. + Proof. + split. + - split; [eapply set_diff_elim1 | eapply set_diff_elim2]; eauto. + - destruct 1. now apply set_diff_intro. + Qed. + + Lemma set_diff_nodup l l' : NoDup l -> NoDup l' -> NoDup (set_diff l l'). + Proof. + induction 1 as [|x l H H' IH]; intro Hl'; simpl. + - constructor. + - destruct (set_mem x l'); auto using set_add_nodup. + Qed. + Lemma set_diff_trivial : forall (a:A) (x:set), ~ set_In a (set_diff x x). red; intros a x H. apply (set_diff_elim2 _ _ _ H). diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml index 0931fd5506..b5d0d22819 100644 --- a/tools/coq_makefile.ml +++ b/tools/coq_makefile.ml @@ -447,7 +447,7 @@ let variables is_install opt (args,defs) = (* Caml executables and relative variables *) if !some_ml4file || !some_mlfile || !some_mlifile then begin print "COQSRCLIBS?=-I \"$(COQLIB)kernel\" -I \"$(COQLIB)lib\" \\ - -I \"$(COQLIB)library\" -I \"$(COQLIB)parsing\" -I \"$(COQLIB)pretyping\" \\ + -I \"$(COQLIB)library\" -I \"$(COQLIB)parsing\" -I \"$(COQLIB)engine\" -I \"$(COQLIB)pretyping\" \\ -I \"$(COQLIB)interp\" -I \"$(COQLIB)printing\" -I \"$(COQLIB)intf\" \\ -I \"$(COQLIB)proofs\" -I \"$(COQLIB)tactics\" -I \"$(COQLIB)tools\" \\ -I \"$(COQLIB)toplevel\" -I \"$(COQLIB)stm\" -I \"$(COQLIB)grammar\" \\ diff --git a/tools/coqdep.ml b/tools/coqdep.ml index 2e0cce6e53..dd5593f65f 100644 --- a/tools/coqdep.ml +++ b/tools/coqdep.ml @@ -9,6 +9,7 @@ open Printf open Coqdep_lexer open Coqdep_common +open System (** The basic parts of coqdep (i.e. the parts used by [coqdep -boot]) are now in [Coqdep_common]. The code that remains here concerns @@ -461,7 +462,7 @@ let rec parse = function | "-R" :: ([] | [_]) -> usage () | "-dumpgraph" :: f :: ll -> option_dump := Some (false, f); parse ll | "-dumpgraphbox" :: f :: ll -> option_dump := Some (true, f); parse ll - | "-exclude-dir" :: r :: ll -> norec_dirnames := r::!norec_dirnames; parse ll + | "-exclude-dir" :: r :: ll -> System.exclude_directory r; parse ll | "-exclude-dir" :: [] -> usage () | "-coqlib" :: r :: ll -> Flags.coqlib_spec := true; Flags.coqlib := r; parse ll | "-coqlib" :: [] -> usage () @@ -482,6 +483,7 @@ let coqdep () = if !option_boot then begin add_rec_dir add_known "theories" ["Coq"]; add_rec_dir add_known "plugins" ["Coq"]; + add_caml_dir "tactics"; add_rec_dir (fun _ -> add_caml_known) "theories" ["Coq"]; add_rec_dir (fun _ -> add_caml_known) "plugins" ["Coq"]; end else begin diff --git a/tools/coqdep_boot.ml b/tools/coqdep_boot.ml deleted file mode 100644 index bc3435a644..0000000000 --- a/tools/coqdep_boot.ml +++ /dev/null @@ -1,51 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -open Coqdep_common - -(** [coqdep_boot] is a stripped-down version of [coqdep], whose - behavior is the one of [coqdep -boot]. Its only dependencies - are [Coqdep_lexer], [Coqdep_common] and [Unix], and it should stay so. - If it needs someday some additional information, pass it via - options (see for instance [option_natdynlk] below). -*) - -let rec parse = function - | "-natdynlink" :: "no" :: ll -> option_natdynlk := false; parse ll - | "-c" :: ll -> option_c := true; parse ll - | "-boot" :: ll -> parse ll (* We're already in boot mode by default *) - | "-mldep" :: ocamldep :: ll -> - option_mldep := Some ocamldep; option_c := true; parse ll - | "-I" :: r :: ll -> - (* To solve conflict (e.g. same filename in kernel and checker) - we allow to state an explicit order *) - add_caml_dir r; - norec_dirs:=r::!norec_dirs; - parse ll - | f :: ll -> treat_file None f; parse ll - | [] -> () - -let coqdep_boot () = - let () = option_boot := true in - if Array.length Sys.argv < 2 then exit 1; - parse (List.tl (Array.to_list Sys.argv)); - if !option_c then begin - add_rec_dir add_known "." []; - add_rec_dir (fun _ -> add_caml_known) "." ["Coq"]; - end - else begin - add_rec_dir add_known "theories" ["Coq"]; - add_rec_dir add_known "plugins" ["Coq"]; - add_caml_dir "tactics"; - add_rec_dir (fun _ -> add_caml_known) "theories" ["Coq"]; - add_rec_dir (fun _ -> add_caml_known) "plugins" ["Coq"]; - end; - if !option_c then mL_dependencies (); - coq_dependencies () - -let _ = Printexc.catch coqdep_boot () diff --git a/tools/coqdep_common.ml b/tools/coqdep_common.ml index 2e6a15cebd..7d8199ab38 100644 --- a/tools/coqdep_common.ml +++ b/tools/coqdep_common.ml @@ -9,6 +9,7 @@ open Printf open Coqdep_lexer open Unix +open System (** [coqdep_boot] is a stripped-down version of [coqdep], whose behavior is the one of [coqdep -boot]. Its only dependencies @@ -27,26 +28,11 @@ let option_boot = ref false let option_mldep = ref None let norec_dirs = ref ([] : string list) -let norec_dirnames = ref ["CVS"; "_darcs"] let suffixe = ref ".vo" type dir = string option -(* Filename.concat but always with a '/' *) -let is_dir_sep s i = - match Sys.os_type with - | "Unix" -> s.[i] = '/' - | "Cygwin" | "Win32" -> - let c = s.[i] in c = '/' || c = '\\' || c = ':' - | _ -> assert false - -let (//) dirname filename = - let l = String.length dirname in - if l = 0 || is_dir_sep dirname (l-1) - then dirname ^ filename - else dirname ^ "/" ^ filename - (** [get_extension f l] checks whether [f] has one of the extensions listed in [l]. It returns [f] without its extension, alongside with the extension. When no extension match, [(f,"")] is returned *) @@ -165,6 +151,10 @@ let warning_clash file dir = eprintf "%s and %s; used the latter)\n" d2 d1 | _ -> assert false +let warning_cannot_open_dir dir = + eprintf "*** Warning: cannot open %s\n" dir; + flush stderr + let safe_assoc verbose file k = if verbose && List.mem_assoc k !clash_v then warning_clash file k; Hashtbl.find vKnown k @@ -463,42 +453,43 @@ let add_known recur phys_dir log_dir f = List.iter (fun f -> Hashtbl.add coqlibKnown f ()) paths | _ -> () -(* Visits all the directories under [dir], including [dir], - or just [dir] if [recur=false] *) +(* Visits all the directories under [dir], including [dir] *) -let rec add_directory recur add_file phys_dir log_dir = - let dirh = opendir phys_dir in - try - while true do - let f = readdir dirh in - (* we avoid all files and subdirs starting by '.' (e.g. .svn), - plus CVS and _darcs and any subdirs given via -exclude-dirs *) - if f.[0] <> '.' then - let phys_f = if phys_dir = "." then f else phys_dir//f in - match try (stat phys_f).st_kind with _ -> S_BLK with - | S_DIR when recur -> - if List.mem f !norec_dirnames then () - else - if List.mem phys_f !norec_dirs then () - else - add_directory recur add_file phys_f (log_dir@[f]) - | S_REG -> add_file phys_dir log_dir f - | _ -> () - done - with End_of_file -> closedir dirh +let is_not_seen_directory phys_f = + not (List.mem phys_f !norec_dirs) + +let rec add_directory add_file phys_dir log_dir = + let f = function + | FileDir (phys_f,f) -> + if is_not_seen_directory phys_f then + add_directory add_file phys_f (log_dir @ [f]) + | FileRegular f -> + add_file phys_dir log_dir f + in + System.check_unix_dir (fun s -> eprintf "*** Warning: %s\n" s) phys_dir; + if exists_dir phys_dir then + process_directory f phys_dir + else + warning_cannot_open_dir phys_dir (** -Q semantic: go in subdirs but only full logical paths are known. *) let add_dir add_file phys_dir log_dir = - try add_directory true (add_file false) phys_dir log_dir with Unix_error _ -> () + try add_directory (add_file false) phys_dir log_dir with Unix_error _ -> () (** -R semantic: go in subdirs and suffixes of logical paths are known. *) let add_rec_dir add_file phys_dir log_dir = - handle_unix_error (add_directory true (add_file true) phys_dir) log_dir + add_directory (add_file true) phys_dir log_dir + +(** -R semantic but only on immediate capitalized subdirs *) + +let add_rec_uppercase_subdirs add_file phys_dir log_dir = + process_subdirectories (fun phys_dir f -> + add_directory (add_file true) phys_dir (log_dir@[String.capitalize f])) + phys_dir (** -I semantic: do not go in subdirs. *) let add_caml_dir phys_dir = - handle_unix_error (add_directory true add_caml_known phys_dir) [] - + add_directory add_caml_known phys_dir [] let rec treat_file old_dirname old_name = let name = Filename.basename old_name diff --git a/tools/coqdep_common.mli b/tools/coqdep_common.mli index 71b96ca0ee..3ac602183f 100644 --- a/tools/coqdep_common.mli +++ b/tools/coqdep_common.mli @@ -12,10 +12,8 @@ val option_boot : bool ref val option_natdynlk : bool ref val option_mldep : string option ref val norec_dirs : string list ref -val norec_dirnames : string list ref val suffixe : string ref type dir = string option -val ( // ) : string -> string -> string val get_extension : string -> string list -> string * string val basename_noext : string -> string val mlAccu : (string * string * dir) list ref @@ -41,13 +39,12 @@ val coq_dependencies : unit -> unit val suffixes : 'a list -> 'a list list val add_known : bool -> string -> string list -> string -> unit val add_caml_known : string -> string list -> string -> unit -val add_directory : - bool -> - (string -> string list -> string -> unit) -> string -> string list -> unit val add_caml_dir : string -> unit val add_dir : (bool -> string -> string list -> string -> unit) -> string -> string list -> unit val add_rec_dir : (bool -> string -> string list -> string -> unit) -> string -> string list -> unit +val add_rec_uppercase_subdirs : + (bool -> string -> string list -> string -> unit) -> string -> string list -> unit val treat_file : dir -> string -> unit val error_cannot_parse : string -> int * int -> 'a diff --git a/tools/ocamllibdep.mll b/tools/ocamllibdep.mll new file mode 100644 index 0000000000..4e5edcf6c2 --- /dev/null +++ b/tools/ocamllibdep.mll @@ -0,0 +1,210 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +{ + exception Syntax_error of int*int + + let syntax_error lexbuf = + raise (Syntax_error (Lexing.lexeme_start lexbuf, Lexing.lexeme_end lexbuf)) +} + +let space = [' ' '\t' '\n' '\r'] +let lowercase = ['a'-'z' '\223'-'\246' '\248'-'\255'] +let uppercase = ['A'-'Z' '\192'-'\214' '\216'-'\222'] +let identchar = + ['A'-'Z' 'a'-'z' '_' '\192'-'\214' '\216'-'\246' '\248'-'\255' '\'' '0'-'9'] +let caml_up_ident = uppercase identchar* +let caml_low_ident = lowercase identchar* + +rule mllib_list = parse + | caml_up_ident { let s = String.uncapitalize (Lexing.lexeme lexbuf) + in s :: mllib_list lexbuf } + | "*predef*" { mllib_list lexbuf } + | space+ { mllib_list lexbuf } + | eof { [] } + | _ { syntax_error lexbuf } + +{ +open Printf +open Unix + +(** [coqdep_boot] is a stripped-down version of [coqdep] used to treat + with mllib files. +*) + +(* Makefile's escaping rules are awful: $ is escaped by doubling and + other special characters are escaped by backslash prefixing while + backslashes themselves must be escaped only if part of a sequence + followed by a special character (i.e. in case of ambiguity with a + use of it as escaping character). Moreover (even if not crucial) + it is apparently not possible to directly escape ';' and leading '\t'. *) + +let escape = + let s' = Buffer.create 10 in + fun s -> + Buffer.clear s'; + for i = 0 to String.length s - 1 do + let c = s.[i] in + if c = ' ' || c = '#' || c = ':' (* separators and comments *) + || c = '%' (* pattern *) + || c = '?' || c = '[' || c = ']' || c = '*' (* expansion in filenames *) + || i=0 && c = '~' && (String.length s = 1 || s.[1] = '/' || + 'A' <= s.[1] && s.[1] <= 'Z' || + 'a' <= s.[1] && s.[1] <= 'z') (* homedir expansion *) + then begin + let j = ref (i-1) in + while !j >= 0 && s.[!j] = '\\' do + Buffer.add_char s' '\\'; decr j (* escape all preceding '\' *) + done; + Buffer.add_char s' '\\'; + end; + if c = '$' then Buffer.add_char s' '$'; + Buffer.add_char s' c + done; + Buffer.contents s' + +(* Filename.concat but always with a '/' *) +let is_dir_sep s i = + match Sys.os_type with + | "Unix" -> s.[i] = '/' + | "Cygwin" | "Win32" -> + let c = s.[i] in c = '/' || c = '\\' || c = ':' + | _ -> assert false + +let (//) dirname filename = + let l = String.length dirname in + if l = 0 || is_dir_sep dirname (l-1) + then dirname ^ filename + else dirname ^ "/" ^ filename + +(** [get_extension f l] checks whether [f] has one of the extensions + listed in [l]. It returns [f] without its extension, alongside with + the extension. When no extension match, [(f,"")] is returned *) + +let rec get_extension f = function + | [] -> (f, "") + | s :: _ when Filename.check_suffix f s -> (Filename.chop_suffix f s, s) + | _ :: l -> get_extension f l + +let file_name s = function + | None -> s + | Some "." -> s + | Some d -> d // s + +type dir = string option + +(* Visits all the directories under [dir], including [dir], + or just [dir] if [recur=false] *) + +let rec add_directory add_file phys_dir = + let dirh = opendir phys_dir in + try + while true do + let f = readdir dirh in + (* we avoid all files and subdirs starting by '.' (e.g. .svn), + plus CVS and _darcs and any subdirs given via -exclude-dirs *) + if f.[0] <> '.' then + let phys_f = if phys_dir = "." then f else phys_dir//f in + match try (stat phys_f).st_kind with _ -> S_BLK with + | S_REG -> add_file phys_dir f + | _ -> () + done + with End_of_file -> closedir dirh + +let error_cannot_parse s (i,j) = + Printf.eprintf "File \"%s\", characters %i-%i: Syntax error\n" s i j; + exit 1 + +let warning_ml_clash x s suff s' suff' = + if suff = suff' then + eprintf + "*** Warning: %s%s already found in %s (discarding %s%s)\n" x suff + (match s with None -> "." | Some d -> d) + ((match s' with None -> "." | Some d -> d) // x) suff + +let mkknown () = + let h = (Hashtbl.create 19 : (string, dir * string) Hashtbl.t) in + let add x s suff = + try let s',suff' = Hashtbl.find h x in warning_ml_clash x s' suff' s suff + with Not_found -> Hashtbl.add h x (s,suff) + and search x = + try Some (fst (Hashtbl.find h x)) + with Not_found -> None + in add, search + +let add_ml_known, search_ml_known = mkknown () +let add_mlpack_known, search_mlpack_known = mkknown () + +let mllibAccu = ref ([] : (string * dir) list) + +let add_caml_known phys_dir f = + let basename,suff = get_extension f [".ml";".ml4";".mlpack"] in + match suff with + | ".ml"|".ml4" -> add_ml_known basename (Some phys_dir) suff + | ".mlpack" -> add_mlpack_known basename (Some phys_dir) suff + | _ -> () + +let add_caml_dir phys_dir = + handle_unix_error (add_directory add_caml_known) phys_dir + +let traite_fichier_modules md ext = + try + let chan = open_in (md ^ ext) in + let list = mllib_list (Lexing.from_channel chan) in + List.fold_left + (fun a_faire str -> match search_mlpack_known str with + | Some mldir -> + let file = file_name str mldir in + a_faire^" "^file + | None -> + match search_ml_known str with + | Some mldir -> + let file = file_name str mldir in + a_faire^" "^file + | None -> a_faire) "" list + with + | Sys_error _ -> "" + | Syntax_error (i,j) -> error_cannot_parse (md^ext) (i,j) + +let addQueue q v = q := v :: !q + +let rec treat_file old_name = + let name = Filename.basename old_name in + let dirname = Some (Filename.dirname old_name) in + match get_extension name [".mllib"] with + | (base,".mllib") -> addQueue mllibAccu (base,dirname) + | _ -> () + +let mllib_dependencies () = + List.iter + (fun (name,dirname) -> + let fullname = file_name name dirname in + let dep = traite_fichier_modules fullname ".mllib" in + let efullname = escape fullname in + printf "%s_MLLIB_DEPENDENCIES:=%s\n" efullname dep; + printf "%s.cma:$(addsuffix .cmo,$(%s_MLLIB_DEPENDENCIES))\n" efullname efullname; + printf "%s.cmxa %s.cmxs:$(addsuffix .cmx,$(%s_MLLIB_DEPENDENCIES))\n" efullname efullname efullname; + flush Pervasives.stdout) + (List.rev !mllibAccu) + +let rec parse = function + | "-I" :: r :: ll -> + (* To solve conflict (e.g. same filename in kernel and checker) + we allow to state an explicit order *) + add_caml_dir r; + parse ll + | f :: ll -> treat_file f; parse ll + | [] -> () + +let coqdep_boot () = + if Array.length Sys.argv < 2 then exit 1; + parse (List.tl (Array.to_list Sys.argv)); + mllib_dependencies () + +let _ = Printexc.catch coqdep_boot () +} diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml index 03074ced70..1ce3fe28da 100644 --- a/toplevel/coqinit.ml +++ b/toplevel/coqinit.ml @@ -132,7 +132,7 @@ let init_ocaml_path () = Mltop.add_ml_dir (Envars.coqlib ()); List.iter add_subdir [ [ "config" ]; [ "dev" ]; [ "lib" ]; [ "kernel" ]; [ "library" ]; - [ "pretyping" ]; [ "interp" ]; [ "parsing" ]; [ "proofs" ]; + [ "engine" ]; [ "pretyping" ]; [ "interp" ]; [ "parsing" ]; [ "proofs" ]; [ "tactics" ]; [ "toplevel" ]; [ "printing" ]; [ "intf" ]; [ "grammar" ]; [ "ide" ] ] diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 0b9bb2f2ee..22ab469dcb 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -455,7 +455,7 @@ let parse_args arglist = |"-compile-verbose" -> add_compile true (next ()) |"-dump-glob" -> Dumpglob.dump_into_file (next ()); glob_opt := true |"-feedback-glob" -> Dumpglob.feedback_glob () - |"-exclude-dir" -> exclude_search_in_dirname (next ()) + |"-exclude-dir" -> System.exclude_directory (next ()) |"-init-file" -> set_rcfile (next ()) |"-inputstate"|"-is" -> set_inputstate (next ()) |"-load-ml-object" -> Mltop.dir_ml_load (next ()) diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml index c8eff59b15..75e8369222 100644 --- a/toplevel/metasyntax.ml +++ b/toplevel/metasyntax.ml @@ -152,13 +152,15 @@ type ml_tactic_grammar_obj = { (** ML tactic notations whose use can be restricted to an identifier are added as true Ltac entries. *) let extend_atomic_tactic name entries = - let add_atomic (id, args) = match args with + let add_atomic i (id, args) = match args with | None -> () | Some args -> - let body = Tacexpr.TacML (Loc.ghost, name, args) in + let open Tacexpr in + let entry = { mltac_name = name; mltac_index = i } in + let body = TacML (Loc.ghost, entry, args) in Tacenv.register_ltac false false (Names.Id.of_string id) body in - List.iter add_atomic entries + List.iteri add_atomic entries let cache_ml_tactic_notation (_, obj) = extend_ml_tactic_grammar obj.mltacobj_name obj.mltacobj_prod diff --git a/toplevel/mltop.ml b/toplevel/mltop.ml index 357c5482fd..e7500f6ae4 100644 --- a/toplevel/mltop.ml +++ b/toplevel/mltop.ml @@ -155,7 +155,7 @@ let add_ml_dir s = | WithoutTop when has_dynlink -> keep_copy_mlpath s | _ -> () -(* For Rec Add ML Path *) +(* For Rec Add ML Path (-R) *) let add_rec_ml_dir unix_path = List.iter (fun (lp,_) -> add_ml_dir lp) (all_subdirs ~unix_path) |