From da178a880e3ace820b41d38b191d3785b82991f5 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Thu, 1 Jul 2010 17:21:14 +0200 Subject: Imported Upstream version 8.2pl2+dfsg --- .gitignore | 90 +++++++++++++++++++++++++++++++++++ Makefile | 9 ++-- Makefile.build | 9 ++-- Makefile.common | 2 +- Makefile.doc | 2 +- Makefile.stage1 | 1 - checker/mod_checking.ml | 2 +- config/Makefile.template | 3 ++ configure | 25 +++++----- contrib/dp/dp.ml | 18 +++---- contrib/extraction/common.ml | 10 +++- contrib/extraction/extract_env.ml | 17 +++---- contrib/extraction/mlutil.ml | 4 +- contrib/funind/recdef.ml | 26 ++++++---- contrib/xml/xml.ml4 | 2 +- contrib/xml/xmlcommand.ml | 10 ++-- dev/ocamldebug-coq.template | 2 +- dev/v8-syntax/check-grammar | 18 +++---- ide/undo_lablgtk_ge212.mli | 3 +- install.sh | 2 +- interp/constrextern.ml | 3 +- interp/constrintern.ml | 21 ++++---- kernel/indtypes.ml | 4 +- kernel/modops.ml | 8 ++-- lib/system.ml | 17 +++++-- lib/system.mli | 4 +- lib/util.ml | 22 ++++++++- lib/util.mli | 3 +- library/declaremods.ml | 5 +- library/goptions.ml | 9 ++-- library/lib.ml | 28 ++++++----- library/library.ml | 12 +---- library/states.ml | 5 +- man/coqdoc.1 | 2 +- parsing/g_decl_mode.ml4 | 4 +- parsing/g_intsyntax.ml | 10 ++-- parsing/g_vernac.ml4 | 4 +- parsing/lexer.ml4 | 25 ++++++---- parsing/pptactic.ml | 4 +- pretyping/cases.ml | 12 +++-- pretyping/clenv.ml | 13 ++--- pretyping/clenv.mli | 4 +- pretyping/detyping.ml | 5 +- pretyping/evarconv.ml | 30 ++++++++---- pretyping/evarutil.ml | 77 +++++++++++++++++++++++++----- pretyping/evarutil.mli | 4 +- pretyping/tacred.ml | 52 +++++++++++++------- pretyping/unification.ml | 4 +- proofs/decl_mode.ml | 5 +- proofs/decl_mode.mli | 4 +- proofs/logic.ml | 4 +- scripts/coqc.ml | 18 +++++-- scripts/coqmktop.ml | 4 +- tactics/decl_interp.ml | 4 +- tactics/decl_proof_instr.ml | 34 +++++++++---- tactics/decl_proof_instr.mli | 13 ++--- tactics/equality.ml | 23 +++++++-- tactics/hiddentac.ml | 8 ++-- tactics/inv.ml | 4 +- tactics/leminv.ml | 6 ++- tactics/refine.ml | 8 +++- tactics/tacinterp.ml | 13 +++-- tactics/tactics.ml | 48 ++++++++++++++++--- tactics/tauto.ml4 | 17 +++++-- theories/FSets/FSetDecide.v | 20 +++++++- theories/Init/Notations.v | 10 ++-- theories/Init/Tactics.v | 19 +++++++- theories/Lists/List.v | 8 ++-- theories/Numbers/Rational/BigQ/BigQ.v | 7 ++- theories/QArith/QArith_base.v | 28 ++++++----- theories/ZArith/Zbool.v | 6 +-- theories/ZArith/Zorder.v | 4 +- tools/coq_makefile.ml4 | 8 ++-- tools/coqdep.ml | 44 +++++++++++++++-- tools/coqdoc/pretty.mll | 7 ++- toplevel/metasyntax.ml | 24 ++++++---- toplevel/mltop.ml4 | 4 +- toplevel/toplevel.ml | 13 +++-- toplevel/vernacentries.ml | 10 ++-- 79 files changed, 745 insertions(+), 326 deletions(-) create mode 100644 .gitignore diff --git a/.gitignore b/.gitignore new file mode 100644 index 00000000..965adf7a --- /dev/null +++ b/.gitignore @@ -0,0 +1,90 @@ +*.glob +*.d +*.d.raw +*.vo +*.cm* +*.o +*.a +*.annot +*.log +*.aux +*.dvi +*.blg +*.bbl +*.idx +*.ilg +*.lof +*.toc +*.atoc +*.comidx +*.comind +*.tacidx +*.tacind +*.erridx +*.errind +*.ind +*.hcomind +*.htacind +*.herrind +*.hind +*.haux +*.htoc +*.v.tex +*.v.ps +*.v.pdf +*.v.html +bin +config/Makefile +config/coq_config.ml +contrib/dp/dp_zenon.ml +contrib/micromega/csdpcert +dev/ocamldebug-coq +dev/ocamlweb-doc/lex.ml +dev/ocamlweb-doc/syntax.ml +dev/ocamlweb-doc/syntax.mli +ide/config_lexer.ml +ide/config_parser.ml +ide/config_parser.mli +ide/highlight.ml +ide/index_urls.txt +ide/undo.mli +ide/utf8_convert.ml +ide/extract_index.ml +ide/find_phrase.ml +kernel/copcodes.ml +kernel/byterun/coq_jumptbl.h +scripts/tolink.ml +states/initial.coq +theories/Numbers/Natural/BigN/NMake.v +tools/coqdep_lexer.ml +tools/coqwc.ml +tools/gallina_lexer.ml +tools/coqdoc/pretty.ml +tools/coqdoc/index.ml +toplevel/mltop.byteml +toplevel/mltop.optml +doc/RecTutorial/RecTutorial.html +doc/common/version.tex +doc/faq/html +doc/RecTutorial/RecTutorial.pdf +doc/RecTutorial/RecTutorial.ps +doc/refman/Reference-Manual.html +doc/refman/Reference-Manual.sh +doc/refman/Reference-Manual.ps +doc/refman/Reference-Manual.pdf +doc/refman/coqide-queries.eps +doc/refman/coqide.eps +doc/refman/cover.html +doc/refman/euclid.ml +doc/refman/euclid.mli +doc/refman/heapsort.ml +doc/refman/heapsort.mli +doc/refman/html +doc/refman/styles.hva +doc/stdlib/Library.coqdoc.tex +doc/stdlib/Library.out +doc/stdlib/Library.pdf +doc/stdlib/Library.ps +doc/stdlib/html/ +doc/stdlib/index-list.html +kernel/byterun/dllcoqrun.so diff --git a/Makefile b/Makefile index 6854de92..6873d80c 100644 --- a/Makefile +++ b/Makefile @@ -6,7 +6,7 @@ # # GNU Lesser General Public License Version 2.1 # ####################################################################### -# $Id: Makefile 12063 2009-04-08 15:38:39Z herbelin $ +# $Id: Makefile 13182 2010-06-23 09:18:18Z notin $ # Makefile for Coq @@ -24,8 +24,6 @@ # by Emacs' next-error. ########################################################################### -export SHELL:=/bin/bash - export FIND_VCS_CLAUSE:='(' \ -name '{arch}' -o \ -name '.svn' -o \ @@ -183,9 +181,10 @@ docclean: rm -f doc/*/*.ps doc/*/*.pdf rm -rf doc/refman/html doc/stdlib/html doc/faq/html doc/tutorial/tutorial.v.html rm -f doc/stdlib/html/*.html - rm -f doc/refman/euclid.ml{,i} doc/refman/heapsort.ml{,i} + rm -f doc/refman/euclid.ml doc/refman/euclid.mli + rm -f doc/refman/heapsort.ml doc/refman/heapsort.mli rm -f doc/common/version.tex - rm -f doc/refman/*.eps doc/refman/Reference-Manual.html + rm -f doc/refman/styles.hva doc/refman/cover.html doc/refman/*.eps doc/refman/Reference-Manual.html rm -f doc/coq.tex rm -f doc/refman/styles.hva doc/refman/cover.html diff --git a/Makefile.build b/Makefile.build index 703c5884..148bb620 100644 --- a/Makefile.build +++ b/Makefile.build @@ -6,7 +6,7 @@ # # GNU Lesser General Public License Version 2.1 # ####################################################################### -# $Id: Makefile.build 12169 2009-06-06 21:43:23Z herbelin $ +# $Id: Makefile.build 12279 2009-08-14 14:54:56Z herbelin $ # Makefile for Coq @@ -447,6 +447,7 @@ install-ide-opt: install-ide-files: $(MKDIR) $(FULLIDELIB) $(INSTALLLIB) $(IDEFILES) $(FULLIDELIB) + if (test -f ide/index_urls.txt); then $(INSTALLLIB) ide/index_urls.txt $(FULLIDELIB); fi install-ide-info: $(MKDIR) $(FULLIDELIB) @@ -773,7 +774,7 @@ source-doc: dev/printers.cma: $(PRINTERSCMO) $(SHOW)'Testing $@' - $(HIDE)$(OCAMLC) $(BYTEFLAGS) gramlib.cma $(PRINTERSCMO) -o test-printer + $(HIDE)$(OCAMLC) $(BYTEFLAGS) unix.cma gramlib.cma $(PRINTERSCMO) -o test-printer @rm -f test-printer $(SHOW)'OCAMLC -a $@' $(HIDE)$(OCAMLC) $(BYTEFLAGS) $(PRINTERSCMO) -linkall -a -o $@ @@ -781,10 +782,10 @@ dev/printers.cma: $(PRINTERSCMO) parsing/grammar.cma: $(GRAMMARCMO) $(SHOW)'Testing $@' @touch test.ml4 - $(HIDE)$(OCAMLC) $(BYTEFLAGS) -pp "$(CAMLP4O) $(CAMLP4EXTENDFLAGS) $(GRAMMARCMO) -impl" -impl test.ml4 -o test-grammar + $(HIDE)$(OCAMLC) $(BYTEFLAGS) -pp "$(CAMLP4O) $(CAMLP4EXTENDFLAGS) -I $(CAMLLIB) unix.cma $(GRAMMARCMO) -impl" -impl test.ml4 -o test-grammar @rm -f test-grammar test.* $(SHOW)'OCAMLC -a $@' - $(HIDE)$(OCAMLC) $(BYTEFLAGS) $(GRAMMARCMO) -linkall -a -o $@ + $(HIDE)$(OCAMLC) $(BYTEFLAGS) unix.cma $(GRAMMARCMO) -linkall -a -o $@ # toplevel/mltop.ml4 (ifdef Byte) diff --git a/Makefile.common b/Makefile.common index d6f43cf5..4d76e9e5 100644 --- a/Makefile.common +++ b/Makefile.common @@ -435,7 +435,7 @@ MCHECKER:=\ # grammar modules with camlp4 GRAMMARNEEDEDCMO:=\ - lib/pp_control.cmo lib/pp.cmo lib/compat.cmo lib/flags.cmo \ + lib/profile.cmo lib/pp_control.cmo lib/pp.cmo lib/compat.cmo lib/flags.cmo \ lib/util.cmo lib/bigint.cmo lib/dyn.cmo lib/hashcons.cmo lib/predicate.cmo \ lib/rtree.cmo lib/option.cmo \ kernel/names.cmo kernel/univ.cmo \ diff --git a/Makefile.doc b/Makefile.doc index 795e0e5c..f481d681 100644 --- a/Makefile.doc +++ b/Makefile.doc @@ -209,7 +209,7 @@ else doc/stdlib/Library.coqdoc.tex: | $(COQDOC) $(THEORIESLIGHTVO) endif $(COQDOC) -q -boot --gallina --body-only --latex --stdout \ - -R theories Coq $(THEORIESLIGHTVO:.vo=.v) >> $@ + -R theories Coq $(THEORIESLIGHTVO:.vo=.v) > $@ doc/stdlib/Library.dvi: $(DOCCOMMON) doc/stdlib/Library.coqdoc.tex doc/stdlib/Library.tex (cd doc/stdlib;\ diff --git a/Makefile.stage1 b/Makefile.stage1 index c39a6372..a60d388f 100644 --- a/Makefile.stage1 +++ b/Makefile.stage1 @@ -6,7 +6,6 @@ # # GNU Lesser General Public License Version 2.1 # ####################################################################### -export SHELL:=/bin/bash include Makefile.build # All includes must be declared secondary, otherwise make will delete diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml index 9e7a2336..24000591 100644 --- a/checker/mod_checking.ml +++ b/checker/mod_checking.ml @@ -306,7 +306,7 @@ and check_structure_field (s,env) mp lab = function let sub = join_alias sub (map_mp mp' mp2') in let sub = add_mp mp' mp2' sub in (join s sub, register_alias mp' mp2 env) - with Not_found -> failwith "unkown aliased module") + with Not_found -> failwith "unknown aliased module") | SFBmodtype mty -> let kn = MPdot(mp, lab) in check_module_type env mty; diff --git a/config/Makefile.template b/config/Makefile.template index 6f9fac3c..4d45f1b4 100644 --- a/config/Makefile.template +++ b/config/Makefile.template @@ -49,6 +49,9 @@ CAMLP4BIN="CAMLP4BINDIRECTORY" # Ocaml version number CAMLVERSION=CAMLTAG +# Ocaml libraries +CAMLLIB="CAMLLIBDIRECTORY" + # Ocaml .h directory CAMLHLIB="CAMLLIBDIRECTORY" diff --git a/configure b/configure index 1ba4eaba..db7a55a0 100755 --- a/configure +++ b/configure @@ -1,4 +1,4 @@ -#!/bin/bash +#!/bin/sh ################################## # @@ -6,7 +6,7 @@ # ################################## -VERSION=8.2pl1 +VERSION=8.2pl2 VOMAGIC=08200 STATEMAGIC=58200 DATE=`LANG=C date +"%B %Y"` @@ -331,7 +331,7 @@ if [ "$MAKE" != "" ]; then OK="no" if [ -x ./make ]; then MAKEVERSION=`./make -v | head -1` - if [ "$MAKEVERSION" == "GNU Make 3.81" ]; then OK="yes"; fi + if [ "$MAKEVERSION" = "GNU Make 3.81" ]; then OK="yes"; fi fi if [ $OK = "no" ]; then echo "GNU Make >= 3.81 is needed" @@ -363,7 +363,7 @@ if [ "$browser_spec" = "no" ]; then fi if [ "$wwwcoq_spec" = "no" ]; then - WWWCOQ="http://www.lix.polytechnique.fr/coq/" + WWWCOQ="http://coq.inria.fr/" fi ######################################### @@ -665,17 +665,14 @@ esac if test "$with_doc" = "all" then - if test "`which latex`" = "" - then - echo "latex was not found; documentation will not be available" - with_doc=no - else - if test "`which hevea`" = "" - then + for cmd in "latex" "hevea" "pngtopnm" "pnmtops" ; do + if test ! -x "`which $cmd`" + then + echo "$cmd was not found; documentation will not be available" with_doc=no - echo "hevea was not found: documentation will not be available" + break fi - fi + done fi ########################################### @@ -1080,4 +1077,4 @@ echo echo "*Warning* To compile the system for a new architecture" echo " don't forget to do a 'make archclean' before './configure'." -# $Id: configure 12219 2009-07-01 09:58:00Z notin $ +# $Id: configure 13223 2010-06-29 18:28:35Z notin $ diff --git a/contrib/dp/dp.ml b/contrib/dp/dp.ml index 79ffaf3f..d8803847 100644 --- a/contrib/dp/dp.ml +++ b/contrib/dp/dp.ml @@ -701,7 +701,7 @@ let file_contents f = let timeout_sys_command cmd = if !debug then Format.eprintf "command line: %s@." cmd; let out = Filename.temp_file "out" "" in - let cmd = sprintf "cpulimit %d %s > %s 2>&1" !timeout cmd out in + let cmd = sprintf "why-cpulimit %d %s > %s 2>&1" !timeout cmd out in let ret = Sys.command cmd in if !debug then Format.eprintf "Output file %s:@.%s@." out (file_contents out); @@ -731,12 +731,12 @@ let why_files f = String.concat " " (!prelude_files @ [f]) let call_simplify fwhy = let cmd = - sprintf "why --no-arrays --simplify --encoding sstrat %s" (why_files fwhy) + sprintf "why --simplify %s" (why_files fwhy) in if Sys.command cmd <> 0 then error ("call to " ^ cmd ^ " failed"); let fsx = Filename.chop_suffix fwhy ".why" ^ "_why.sx" in let cmd = - sprintf "timeout %d Simplify %s > out 2>&1 && grep -q -w Valid out" + sprintf "why-cpulimit %d Simplify %s > out 2>&1 && grep -q -w Valid out" !timeout fsx in let out = Sys.command cmd in @@ -747,7 +747,7 @@ let call_simplify fwhy = r let call_ergo fwhy = - let cmd = sprintf "why --no-arrays --why %s" (why_files fwhy) in + let cmd = sprintf "why --alt-ergo %s" (why_files fwhy) in if Sys.command cmd <> 0 then error ("call to " ^ cmd ^ " failed"); let fwhy = Filename.chop_suffix fwhy ".why" ^ "_why.why" in let ftrace = Filename.temp_file "ergo_trace" "" in @@ -797,12 +797,12 @@ let call_zenon fwhy = let call_yices fwhy = let cmd = - sprintf "why --no-arrays -smtlib --encoding sstrat %s" (why_files fwhy) + sprintf "why -smtlib --encoding sstrat %s" (why_files fwhy) in if Sys.command cmd <> 0 then error ("call to " ^ cmd ^ " failed"); let fsmt = Filename.chop_suffix fwhy ".why" ^ "_why.smt" in let cmd = - sprintf "timeout %d yices -pc 0 -smt < %s > out 2>&1 && grep -q -w unsat out" + sprintf "why-cpulimit %d yices -pc 0 -smt %s > out 2>&1 && grep -q -w unsat out" !timeout fsmt in let out = Sys.command cmd in @@ -814,7 +814,7 @@ let call_yices fwhy = let call_cvcl fwhy = let cmd = - sprintf "why --no-arrays --cvcl --encoding sstrat %s" (why_files fwhy) + sprintf "why --cvcl --encoding sstrat %s" (why_files fwhy) in if Sys.command cmd <> 0 then error ("call to " ^ cmd ^ " failed"); let fcvc = Filename.chop_suffix fwhy ".why" ^ "_why.cvc" in @@ -831,7 +831,7 @@ let call_cvcl fwhy = let call_harvey fwhy = let cmd = - sprintf "why --no-arrays --harvey --encoding strat %s" (why_files fwhy) + sprintf "why --harvey --encoding strat %s" (why_files fwhy) in if Sys.command cmd <> 0 then error ("call to " ^ cmd ^ " failed"); let frv = Filename.chop_suffix fwhy ".why" ^ "_why.rv" in @@ -856,7 +856,7 @@ let call_harvey fwhy = r let call_gwhy fwhy = - let cmd = sprintf "gwhy --no-arrays %s" (why_files fwhy) in + let cmd = sprintf "gwhy %s" (why_files fwhy) in if Sys.command cmd <> 0 then ignore (Sys.command (sprintf "emacs %s" fwhy)); NoAnswer diff --git a/contrib/extraction/common.ml b/contrib/extraction/common.ml index 02173c1f..73f44e68 100644 --- a/contrib/extraction/common.ml +++ b/contrib/extraction/common.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: common.ml 11559 2008-11-07 22:03:34Z letouzey $ i*) +(*i $Id: common.ml 13200 2010-06-25 22:36:25Z letouzey $ i*) open Pp open Util @@ -21,6 +21,8 @@ open Mlutil open Modutil open Mod_subst +let string_of_id id = ascii_of_ident (Names.string_of_id id) + (*s Some pretty-print utility functions. *) let pp_par par st = if par then str "(" ++ st ++ str ")" else st @@ -73,7 +75,11 @@ let is_upper s = match s.[0] with 'A' .. 'Z' -> true | _ -> false let is_lower s = match s.[0] with 'a' .. 'z' | '_' -> true | _ -> false let lowercase_id id = id_of_string (String.uncapitalize (string_of_id id)) -let uppercase_id id = id_of_string (String.capitalize (string_of_id id)) +let uppercase_id id = + let s = string_of_id id in + assert (s<>""); + if s.[0] = '_' then id_of_string ("Coq_"^s) + else id_of_string (String.capitalize s) type kind = Term | Type | Cons | Mod diff --git a/contrib/extraction/extract_env.ml b/contrib/extraction/extract_env.ml index 49a86200..057a7b29 100644 --- a/contrib/extraction/extract_env.ml +++ b/contrib/extraction/extract_env.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: extract_env.ml 11846 2009-01-22 18:55:10Z letouzey $ i*) +(*i $Id: extract_env.ml 13201 2010-06-25 22:36:27Z letouzey $ i*) open Term open Declarations @@ -489,15 +489,12 @@ let simple_extraction r = match locate_ref [r] with | ([], [mp]) as p -> full_extr None p | [r],[] -> init false; - if is_custom r then - msgnl (str "User defined extraction:" ++ spc () ++ - str (find_custom r) ++ fnl ()) - else - let struc = optimize_struct [r] (mono_environment [r] []) in - let d = get_decl_in_structure r struc in - warning_axioms (); - print_one_decl struc (modpath_of_r r) d; - reset () + let struc = optimize_struct [r] (mono_environment [r] []) in + let d = get_decl_in_structure r struc in + warning_axioms (); + if is_custom r then msgnl (str "(** User defined extraction *)"); + print_one_decl struc (modpath_of_r r) d; + reset () | _ -> assert false diff --git a/contrib/extraction/mlutil.ml b/contrib/extraction/mlutil.ml index 79aeea33..4e2904ba 100644 --- a/contrib/extraction/mlutil.ml +++ b/contrib/extraction/mlutil.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: mlutil.ml 10329 2007-11-21 21:21:36Z letouzey $ i*) +(*i $Id: mlutil.ml 13202 2010-06-25 22:36:30Z letouzey $ i*) (*i*) open Pp @@ -578,7 +578,7 @@ let eta_red e = if m = n then [], f, a else if m < n then - snd (list_chop (n-m) ids), f, a + list_skipn m ids, f, a else (* m > n *) let a1,a2 = list_chop (m-n) a in [], MLapp (f,a1), a2 diff --git a/contrib/funind/recdef.ml b/contrib/funind/recdef.ml index 6dc0d5bf..14bf7cf8 100644 --- a/contrib/funind/recdef.ml +++ b/contrib/funind/recdef.ml @@ -8,7 +8,7 @@ (*i camlp4deps: "parsing/grammar.cma" i*) -(* $Id: recdef.ml 11671 2008-12-12 12:43:03Z herbelin $ *) +(* $Id: recdef.ml 12221 2009-07-04 21:53:12Z jforest $ *) open Term open Termops @@ -960,11 +960,6 @@ let open_new_goal (build_proof:tactic -> tactic -> unit) using_lemmas ref_ goal_ let ids' = pf_ids_of_hyps g in lid := List.rev (list_subtract ids' ids); if !lid = [] then lid := [hid]; -(* list_iter_i *) -(* (fun i v -> *) -(* msgnl (str "hyp" ++ int i ++ str " " ++ *) -(* Nameops.pr_id v ++ fnl () ++ fnl())) *) -(* !lid; *) tclIDTAC g ) g @@ -976,9 +971,22 @@ let open_new_goal (build_proof:tactic -> tactic -> unit) using_lemmas ref_ goal_ Auto.h_auto None [] (Some []) g | _ -> incr h_num; - tclTHEN - (eapply_with_bindings (mkVar (List.nth !lid !h_num), NoBindings)) - e_assumption + (observe_tac "finishing using" + ( + tclCOMPLETE( + tclFIRST[ + tclTHEN + (eapply_with_bindings (mkVar (List.nth !lid !h_num), NoBindings)) + e_assumption; + Eauto.eauto_with_bases + false + (true,5) + [delayed_force refl_equal] + [Auto.Hint_db.empty empty_transparent_state false] + ] + ) + ) + ) g) ; Command.save_named opacity; diff --git a/contrib/xml/xml.ml4 b/contrib/xml/xml.ml4 index e2d04cb7..5b217119 100644 --- a/contrib/xml/xml.ml4 +++ b/contrib/xml/xml.ml4 @@ -70,7 +70,7 @@ let pp strm fn = let ch = open_out filename in pp_ch strm ch; close_out ch ; - print_string ("\nWriting on file \"" ^ filename ^ "\" was succesful\n"); + print_string ("\nWriting on file \"" ^ filename ^ "\" was successful\n"); flush stdout | None -> pp_ch strm stdout diff --git a/contrib/xml/xmlcommand.ml b/contrib/xml/xmlcommand.ml index 1ae18661..f4719594 100644 --- a/contrib/xml/xmlcommand.ml +++ b/contrib/xml/xmlcommand.ml @@ -662,21 +662,21 @@ let _ = | Some fn -> let ch = open_out (fn ^ ".v") in Buffer.output_buffer ch theory_buffer ; + close_out ch; + (* dummy glob file *) + let ch = open_out (fn ^ ".glob") in close_out ch end ; Option.iter (fun fn -> let coqdoc = Filename.concat (Envars.coqbin ()) ("coqdoc" ^ Coq_config.exec_extension) in let options = " --html -s --body-only --no-index --latin1 --raw-comments" in - let dir = Option.get xml_library_root in let command cmd = if Sys.command cmd <> 0 then Util.anomaly ("Error executing \"" ^ cmd ^ "\"") in - command (coqdoc^options^" -d "^dir^" "^fn^".v"); - let dot = if fn.[0]='/' then "." else "" in - command ("mv "^dir^"/"^dot^"*.html "^fn^".xml "); - command ("rm "^fn^".v"); + command (coqdoc^options^" -o "^fn^".xml "^fn^".v"); + command ("rm "^fn^".v "^fn^".glob"); print_string("\nWriting on file \"" ^ fn ^ ".xml\" was successful\n")) ofn) ;; diff --git a/dev/ocamldebug-coq.template b/dev/ocamldebug-coq.template index 560d06d9..5f49561b 100644 --- a/dev/ocamldebug-coq.template +++ b/dev/ocamldebug-coq.template @@ -19,7 +19,7 @@ exec $OCAMLDEBUG \ -I $COQTOP/toplevel -I $COQTOP/dev -I $COQTOP/config \ -I $COQTOP/contrib/extraction -I $COQTOP/contrib/field \ -I $COQTOP/contrib/fourier -I $COQTOP/contrib/firstorder \ - -I $COQTOP/contrib/interface \ + -I $COQTOP/contrib/interface -I $COQTOP/contrib/cc \ -I $COQTOP/contrib/omega -I $COQTOP/contrib/romega \ -I $COQTOP/contrib/ring -I $COQTOP/contrib/xml \ -I $COQTOP/contrib/subtac -I $COQTOP/contrib/funind \ diff --git a/dev/v8-syntax/check-grammar b/dev/v8-syntax/check-grammar index 67da1bc5..194a55fe 100755 --- a/dev/v8-syntax/check-grammar +++ b/dev/v8-syntax/check-grammar @@ -1,31 +1,31 @@ -#!/bin/bash +#!/bin/sh # This scripts checks that the new grammar of Coq as defined in syntax-v8.tex # is consistent in the sense that all invoked non-terminals are defined -defined-nt() { +defined_nt() { grep "\\DEFNT{.*}" syntax-v8.tex | sed -e "s|.*DEFNT{\([^}]*\)}.*|\1|"|\ sort | sort -u } -used-nt() { +used_nt() { cat syntax-v8.tex | tr \\\\ \\n | grep "^NT{.*}" |\ sed -e "s|^NT{\([^}]*\)}.*|\1|" | egrep -v ^\#1\|non-terminal | sort -u } -used-term() { +used_term() { cat syntax-v8.tex | tr \\\\ \\n | grep "^TERM{.*}" |\ sed -e "s|^TERM{\([^}]*\)}.*|\1|" -e "s|\\$||g" | egrep -v ^\#1\|terminal | sort -u } -used-kwd() { +used_kwd() { cat syntax-v8.tex | tr \\\\ \\n | grep "^KWD{.*}" |\ sed -e "s|^KWD{\([^}]*\)}.*|\1|" -e "s|\\$||g" | egrep -v ^\#1 | sort -u } -defined-nt > def -used-nt > use -used-term > use-t -used-kwd > use-k +defined_nt > def +used_nt > use +used_term > use-t +used_kwd > use-k diff def use > df ############################### diff --git a/ide/undo_lablgtk_ge212.mli b/ide/undo_lablgtk_ge212.mli index 916a06e9..4488b5e9 100644 --- a/ide/undo_lablgtk_ge212.mli +++ b/ide/undo_lablgtk_ge212.mli @@ -10,9 +10,10 @@ (* An undoable view class *) -class undoable_view : [> Gtk.text_view] Gtk.obj -> +class undoable_view : ([> Gtk.text_view] as 'a) Gtk.obj -> object inherit GText.view + val obj : 'a Gtk.obj method undo : bool method redo : bool method clear_undo : unit diff --git a/install.sh b/install.sh index c2f8215b..277222f5 100755 --- a/install.sh +++ b/install.sh @@ -1,4 +1,4 @@ -#! /bin/bash +#! /bin/sh dest="$1" shift diff --git a/interp/constrextern.ml b/interp/constrextern.ml index f99af68e..99bcf159 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: constrextern.ml 11576 2008-11-10 19:13:15Z msozeau $ *) +(* $Id: constrextern.ml 12495 2009-11-11 12:10:44Z herbelin $ *) (*i*) open Pp @@ -363,7 +363,6 @@ let bind_env (sigma,sigmalist as fullsigma) var v = let rec match_cases_pattern metas sigma a1 a2 = match (a1,a2) with | r1, AVar id2 when List.mem id2 metas -> bind_env sigma id2 r1 | PatVar (_,Anonymous), AHole _ -> sigma - | a, AHole _ -> sigma | PatCstr (loc,(ind,_ as r1),args1,_), _ -> let nparams = (fst (Global.lookup_inductive ind)).Declarations.mind_nparams in diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 8d6a92a2..c8faf911 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: constrintern.ml 11739 2009-01-02 19:33:19Z herbelin $ *) +(* $Id: constrintern.ml 13131 2010-06-13 18:45:17Z herbelin $ *) open Pp open Util @@ -450,8 +450,8 @@ let rec simple_adjust_scopes n = function let find_remaining_constructor_scopes pl1 pl2 (ind,j as cstr) = let (mib,mip) = Inductive.lookup_mind_specif (Global.env()) ind in let npar = mib.Declarations.mind_nparams in - snd (list_chop (List.length pl1 + npar) - (simple_adjust_scopes (npar + List.length pl2) + snd (list_chop (npar + List.length pl1) + (simple_adjust_scopes (npar + List.length pl1 + List.length pl2) (find_arguments_scope (ConstructRef cstr)))) (**********************************************************************) @@ -526,6 +526,7 @@ let error_invalid_pattern_notation loc = let chop_aconstr_constructor loc (ind,k) args = let nparams = (fst (Global.lookup_inductive ind)).Declarations.mind_nparams in + if nparams > List.length args then error_invalid_pattern_notation loc; let params,args = list_chop nparams args in List.iter (function AHole _ -> () | _ -> error_invalid_pattern_notation loc) params; @@ -728,8 +729,7 @@ let locate_if_isevar loc na = function let check_hidden_implicit_parameters id (_,_,_,(indnames,_)) = if List.mem id indnames then errorlabstrm "" (strbrk "A parameter or name of an inductive type " ++ - pr_id id ++ strbrk " must not be used as a bound variable in the type \ -of its constructor.") + pr_id id ++ strbrk " is not allowed to be used as a bound variable in the type of its constructor.") let push_name_env ?(fail_anonymous=false) lvar (ids,unb,tmpsc,scopes as env) = function | Anonymous -> @@ -1060,15 +1060,17 @@ let internalise sigma globalenv env allow_patvar lvar c = | CLetTuple (loc, nal, (na,po), b, c) -> let env' = reset_tmp_scope env in let ((b',(na',_)),ids) = intern_case_item env' (b,(na,None)) in - let env'' = List.fold_left (push_name_env lvar) env ids in - let p' = Option.map (intern_type env'') po in + let p' = Option.map (fun p -> + let env'' = List.fold_left (push_name_env lvar) env ids in + intern_type env'' p) po in RLetTuple (loc, nal, (na', p'), b', intern (List.fold_left (push_name_env lvar) env nal) c) | CIf (loc, c, (na,po), b1, b2) -> let env' = reset_tmp_scope env in let ((c',(na',_)),ids) = intern_case_item env' (c,(na,None)) in - let env'' = List.fold_left (push_name_env lvar) env ids in - let p' = Option.map (intern_type env'') po in + let p' = Option.map (fun p -> + let env'' = List.fold_left (push_name_env lvar) env ids in + intern_type env'' p) po in RIf (loc, c', (na', p'), intern env b1, intern env b2) | CHole (loc, k) -> RHole (loc, match k with Some k -> k | None -> Evd.QuestionMark (Evd.Define true)) @@ -1147,6 +1149,7 @@ let internalise sigma globalenv env allow_patvar lvar c = [], None in let na = match tm', na with | RVar (_,id), None when Idset.mem id vars -> Name id + | RRef (loc, VarRef id), None -> Name id | _, None -> Anonymous | _, Some na -> na in (tm',(na,typ)), na::ids diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 06764834..941ab046 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: indtypes.ml 11784 2009-01-14 11:36:32Z herbelin $ *) +(* $Id: indtypes.ml 12616 2009-12-30 15:02:26Z herbelin $ *) open Util open Names @@ -494,7 +494,7 @@ let check_positivity_one (env, _,ntypes,_ as ienv) hyps i nargs lcnames indlc = raise (IllFormedInd LocalNotConstructor) else if not (List.for_all (noccur_between n ntypes) largs) - then raise (IllFormedInd (LocalNonPos n)); + then failwith_non_pos_list n ntypes largs; (nmr,List.rev lrec) in check_constr_rec ienv nmr [] c in diff --git a/kernel/modops.ml b/kernel/modops.ml index 949a7402..34d9e930 100644 --- a/kernel/modops.ml +++ b/kernel/modops.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: modops.ml 11923 2009-02-13 12:20:27Z soubiran $ i*) +(*i $Id: modops.ml 12234 2009-07-09 09:14:09Z soubiran $ i*) (*i*) open Util @@ -143,11 +143,13 @@ let rec subst_with_body sub = function and subst_modtype sub mtb = let typ_expr' = subst_struct_expr sub mtb.typ_expr in - if typ_expr'==mtb.typ_expr then + let sub_mtb = join_alias mtb.typ_alias sub in + if typ_expr'==mtb.typ_expr && sub_mtb==mtb.typ_alias then mtb else { mtb with - typ_expr = typ_expr'} + typ_expr = typ_expr'; + typ_alias = sub_mtb} and subst_structure sub sign = let subst_body = function diff --git a/lib/system.ml b/lib/system.ml index 65826c81..3fa32ef8 100644 --- a/lib/system.ml +++ b/lib/system.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: system.ml 11801 2009-01-18 20:11:41Z herbelin $ *) +(* $Id: system.ml 13175 2010-06-22 06:28:37Z herbelin $ *) open Pp open Util @@ -153,8 +153,12 @@ let where_in_path ?(warn=true) path filename = let find_file_in_path ?(warn=true) paths filename = if not (Filename.is_implicit filename) then - let root = Filename.dirname filename in - root, filename + if Sys.file_exists filename then + let root = Filename.dirname filename in + root, filename + else + errorlabstrm "System.find_file_in_path" + (hov 0 (str "Can't find file" ++ spc () ++ str filename)) else try where_in_path ~warn paths filename with Not_found -> @@ -224,6 +228,13 @@ let extern_intern ?(warn=true) magic suffix = in (extern_state,intern_state) +let with_magic_number_check f a = + try f a + with Bad_magic_number fname -> + errorlabstrm "with_magic_number_check" + (str"File " ++ str fname ++ strbrk" has bad magic number." ++ spc () ++ + strbrk "It is corrupted or was compiled with another version of Coq.") + (* Communication through files with another executable *) let connect writefun readfun com = diff --git a/lib/system.mli b/lib/system.mli index ba5aa408..426a00df 100644 --- a/lib/system.mli +++ b/lib/system.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: system.mli 11801 2009-01-18 20:11:41Z herbelin $ i*) +(*i $Id: system.mli 13175 2010-06-22 06:28:37Z herbelin $ i*) (*s Files and load paths. Load path entries remember the original root given by the user. For efficiency, we keep the full path (field @@ -54,6 +54,8 @@ val raw_extern_intern : int -> string -> val extern_intern : ?warn:bool -> int -> string -> (string -> 'a -> unit) * (load_path -> string -> 'a) +val with_magic_number_check : ('a -> 'b) -> 'a -> 'b + (*s Sending/receiving once with external executable *) val connect : (out_channel -> unit) -> (in_channel -> 'a) -> string -> 'a diff --git a/lib/util.ml b/lib/util.ml index dce36419..0d6e7ff2 100644 --- a/lib/util.ml +++ b/lib/util.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(* $Id: util.ml 12181 2009-06-10 20:53:09Z glondu $ *) +(* $Id: util.ml 13200 2010-06-25 22:36:25Z letouzey $ *) open Pp @@ -486,6 +486,26 @@ let lowercase_first_char_utf8 s = let j, n = next_utf8 s 0 in utf8_of_unicode (lowercase_unicode (String.sub s 0 j) n) +(* For extraction, we need to encode unicode character into ascii ones *) + +let ascii_of_ident s = + let check_ascii s = + let ok = ref true in + String.iter (fun c -> if Char.code c >= 128 then ok := false) s; + !ok + in + if check_ascii s then s else + let i = ref 0 and out = ref "" in + begin try while true do + let j, n = next_utf8 s !i in + out := + if n >= 128 + then Printf.sprintf "%s__U%04x_" !out n + else Printf.sprintf "%s%c" !out s.[!i]; + i := !i + j + done with End_of_input -> () end; + !out + (* Lists *) let list_intersect l1 l2 = diff --git a/lib/util.mli b/lib/util.mli index 5432eb98..97bda074 100644 --- a/lib/util.mli +++ b/lib/util.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(*i $Id: util.mli 11897 2009-02-09 19:28:02Z barras $ i*) +(*i $Id: util.mli 13200 2010-06-25 22:36:25Z letouzey $ i*) (*i*) open Pp @@ -94,6 +94,7 @@ val classify_unicode : int -> utf8_status val check_ident : string -> unit val check_ident_soft : string -> unit val lowercase_first_char_utf8 : string -> string +val ascii_of_ident : string -> string (*s Lists. *) diff --git a/library/declaremods.ml b/library/declaremods.ml index 93021384..cfada00c 100644 --- a/library/declaremods.ml +++ b/library/declaremods.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: declaremods.ml 12204 2009-06-22 16:06:49Z soubiran $ i*) +(*i $Id: declaremods.ml 12295 2009-08-27 11:01:49Z soubiran $ i*) open Pp open Util open Names @@ -851,8 +851,7 @@ let classify_import (_,(export,_ as obj)) = if export then Substitute obj else Dispose let subst_import (_,subst,(export,mp as obj)) = - let subst' = remove_alias subst in - let mp' = subst_mp subst' mp in + let mp' = subst_mp subst mp in if mp'==mp then obj else (export,mp') diff --git a/library/goptions.ml b/library/goptions.ml index a9b33235..8625ee52 100644 --- a/library/goptions.ml +++ b/library/goptions.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: goptions.ml 10348 2007-12-06 17:36:14Z aspiwack $ *) +(* $Id: goptions.ml 13196 2010-06-25 18:01:50Z herbelin $ *) (* This module manages customization parameters at the vernacular level *) @@ -297,10 +297,11 @@ let set_int_option_value = set_option_value (fun v -> function | (IntValue _) -> IntValue v | _ -> bad_type_error ()) -let set_bool_option_value = set_option_value - (fun v -> function +let set_bool_option_value key v = + try set_option_value (fun v -> function | (BoolValue _) -> BoolValue v - | _ -> bad_type_error ()) + | _ -> bad_type_error ()) key v + with UserError (_,s) -> Flags.if_verbose msg_warning s let set_string_option_value = set_option_value (fun v -> function | (StringValue _) -> StringValue v diff --git a/library/lib.ml b/library/lib.ml index 4a124cec..f0ec488b 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: lib.ml 12187 2009-06-13 19:36:59Z msozeau $ *) +(* $Id: lib.ml 12496 2009-11-11 13:37:57Z herbelin $ *) open Pp open Util @@ -171,9 +171,8 @@ let find_split_p p = let split_lib_gen test = let rec collect after equal = function - | hd::strict_before as before -> - if test hd then collect after (hd::equal) strict_before else after,equal,before - | [] as before -> after,equal,before + | hd::before when test hd -> collect after (hd::equal) before + | before -> after,equal,before in let rec findeq after = function | hd :: before -> @@ -194,7 +193,14 @@ let split_lib_gen test = | None -> error "no such entry" | Some r -> r -let split_lib sp = split_lib_gen (fun x -> (fst x) = sp) +let split_lib sp = split_lib_gen (fun x -> fst x = sp) + +let split_lib_at_opening sp = + split_lib_gen (function + | x,(OpenedSection _|OpenedModule _|OpenedModtype _|CompilingLibrary _) -> + x = sp + | _ -> + false) (* Adding operations. *) @@ -299,7 +305,7 @@ let end_module id = with Not_found -> error "no opened modules" in - let (after,modopening,before) = split_lib oname in + let (after,modopening,before) = split_lib_at_opening oname in lib_stk := before; add_entry (make_oname id) (ClosedModule (List.rev_append after (List.rev modopening))); let prefix = !path_prefix in @@ -344,7 +350,7 @@ let end_modtype id = with Not_found -> error "no opened module types" in - let (after,modtypeopening,before) = split_lib sp in + let (after,modtypeopening,before) = split_lib_at_opening sp in lib_stk := before; add_entry (make_oname id) (ClosedModtype (List.rev_append after (List.rev modtypeopening))); let dir = !path_prefix in @@ -407,7 +413,7 @@ let end_compilation dir = ("The current open module has name "^ (Names.string_of_dirpath m) ^ " and not " ^ (Names.string_of_dirpath m)); in - let (after,_,before) = split_lib oname in + let (after,_,before) = split_lib_at_opening oname in comp_name := None; !path_prefix,after @@ -587,7 +593,7 @@ let close_section id = with Not_found -> error "No opened section." in - let (secdecls,secopening,before) = split_lib oname in + let (secdecls,secopening,before) = split_lib_at_opening oname in lib_stk := before; let full_olddir = fst !path_prefix in pop_path_prefix (); @@ -640,7 +646,7 @@ let reset_to_gen test = let (_,_,before) = split_lib_gen test in set_lib_stk before -let reset_to sp = reset_to_gen (fun x -> (fst x) = sp) +let reset_to sp = reset_to_gen (fun x -> fst x = sp) let reset_to_state sp = let (_,eq,before) = split_lib sp in @@ -667,7 +673,7 @@ let delete_gen test = in set_lib_stk (List.rev_append (chop_at_dot after) (chop_before_dot before)) -let delete sp = delete_gen (fun x -> (fst x) = sp) +let delete sp = delete_gen (fun x -> fst x = sp) let reset_name (loc,id) = let (sp,_) = diff --git a/library/library.ml b/library/library.ml index 0e1342f0..2c6d02ae 100644 --- a/library/library.ml +++ b/library/library.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: library.ml 11897 2009-02-09 19:28:02Z barras $ *) +(* $Id: library.ml 13175 2010-06-22 06:28:37Z herbelin $ *) open Pp open Util @@ -328,14 +328,6 @@ let (in_import, out_import) = let (raw_extern_library, raw_intern_library) = System.raw_extern_intern Coq_config.vo_magic_number ".vo" -let with_magic_number_check f a = - try f a - with System.Bad_magic_number fname -> - errorlabstrm "with_magic_number_check" - (str"File " ++ str fname ++ spc () ++ str"has bad magic number." ++ - spc () ++ str"It is corrupted" ++ spc () ++ - str"or was compiled with another version of Coq.") - (************************************************************************) (*s Locate absolute or partially qualified library names in the path *) @@ -414,7 +406,7 @@ let mk_library md digest = { library_digest = digest } let intern_from_file f = - let ch = with_magic_number_check raw_intern_library f in + let ch = System.with_magic_number_check raw_intern_library f in let md = System.marshal_in ch in let digest = System.marshal_in ch in close_in ch; diff --git a/library/states.ml b/library/states.ml index c81f9614..3a4be1ca 100644 --- a/library/states.ml +++ b/library/states.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: states.ml 12080 2009-04-11 16:56:20Z herbelin $ *) +(* $Id: states.ml 13175 2010-06-22 06:28:37Z herbelin $ *) open System @@ -24,7 +24,8 @@ let (extern_state,intern_state) = extern_intern Coq_config.state_magic_number ".coq" in (fun s -> raw_extern s (freeze())), (fun s -> - unfreeze (raw_intern (Library.get_load_paths ()) s); + unfreeze + (with_magic_number_check (raw_intern (Library.get_load_paths ())) s); Library.overwrite_library_filenames s) (* Rollback. *) diff --git a/man/coqdoc.1 b/man/coqdoc.1 index 45fcafd2..e07ccdd3 100644 --- a/man/coqdoc.1 +++ b/man/coqdoc.1 @@ -75,7 +75,7 @@ Considers the file `file' respectively as a .v (or .g) file or a .tex file. .TP .BI \-\-files\-from \ file Read file names to process in file `file' as if they were given on the -command line. Useful for program sources splitted in several +command line. Useful for program sources split in several directories. .TP .B \-q, \ \-\-quiet diff --git a/parsing/g_decl_mode.ml4 b/parsing/g_decl_mode.ml4 index 61c3474d..35fc064b 100644 --- a/parsing/g_decl_mode.ml4 +++ b/parsing/g_decl_mode.ml4 @@ -9,7 +9,7 @@ (*i camlp4deps: "parsing/grammar.cma" i*) (*i camlp4use: "pa_extend.cmo q_MLast.cmo" i*) -(* $Id: g_decl_mode.ml4 10739 2008-04-01 14:45:20Z herbelin $ *) +(* $Id: g_decl_mode.ml4 12414 2009-10-25 18:50:41Z corbinea $ *) open Decl_expr @@ -220,7 +220,7 @@ GLOBAL: proof_instr; intro_step: [[ IDENT "suppose" ; h=assume_clause -> Psuppose h | IDENT "suppose" ; IDENT "it"; IDENT "is" ; c=pattern LEVEL "0" ; - po=OPT[ IDENT "with"; p=LIST1 hyp -> p ] ; + po=OPT[ "with"; p=LIST1 hyp SEP ","-> p ] ; ho=OPT[ IDENT "and" ; h=suppose_clause -> h ] -> Pcase (none_is_empty po,c,none_is_empty ho) | "let" ; v=let_vars -> Plet v diff --git a/parsing/g_intsyntax.ml b/parsing/g_intsyntax.ml index a589ccf1..64fa0b49 100644 --- a/parsing/g_intsyntax.ml +++ b/parsing/g_intsyntax.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: g_intsyntax.ml 11309 2008-08-06 10:30:35Z herbelin $ i*) +(*i $Id: g_intsyntax.ml 12509 2009-11-12 15:52:50Z letouzey $ i*) (* digit-based syntax for int31, bigN bigZ and bigQ *) @@ -92,13 +92,15 @@ let bigZ_neg = ConstructRef ((bigZ_id "t_",0),2) (*bigQ stuff*) let bigQ_module = ["Coq"; "Numbers"; "Rational"; "BigQ"; "BigQ"] -let qmake_module = ["Coq"; "Numbers"; "Rational"; "BigQ"; "QMake_base"] +let qmake_module = ["Coq"; "Numbers"; "Rational"; "BigQ"; "QMake"] let bigQ_path = make_path (bigQ_module@["BigQ"]) "t" (* big ugly hack bis *) -let bigQ_id = make_kn qmake_module +let bigQ_id id = (Obj.magic ((Names.MPdot ((Names.MPfile (make_dir bigQ_module)), + Names.mk_label "BigQ")), + [], Names.id_of_string id) : Names.kernel_name) let bigQ_scope = "bigQ_scope" -let bigQ_z = ConstructRef ((bigQ_id "q_type",0),1) +let bigQ_z = ConstructRef ((bigQ_id "t_",0),1) (*** Definition of the Non_closed exception, used in the pretty printing ***) diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index b2d67e1c..f727dfea 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -9,7 +9,7 @@ (*i camlp4deps: "parsing/grammar.cma" i*) (*i camlp4use: "pa_extend.cmo" i*) -(* $Id: g_vernac.ml4 12187 2009-06-13 19:36:59Z msozeau $ *) +(* $Id: g_vernac.ml4 13197 2010-06-25 22:36:17Z letouzey $ *) open Pp @@ -663,6 +663,8 @@ GEXTEND Gram check_command: (* TODO: rapprocher Eval et Check *) [ [ IDENT "Eval"; r = Tactic.red_expr; "in"; c = lconstr -> fun g -> VernacCheckMayEval (Some r, g, c) + | IDENT "Compute"; c = lconstr -> + fun g -> VernacCheckMayEval (Some Rawterm.CbvVm, g, c) | IDENT "Check"; c = lconstr -> fun g -> VernacCheckMayEval (None, g, c) ] ] ; diff --git a/parsing/lexer.ml4 b/parsing/lexer.ml4 index 2633386f..52b5ede7 100644 --- a/parsing/lexer.ml4 +++ b/parsing/lexer.ml4 @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: lexer.ml4 11786 2009-01-14 13:07:34Z herbelin $ i*) +(*i $Id: lexer.ml4 12891 2010-03-30 11:40:02Z herbelin $ i*) (*i camlp4use: "pr_o.cmo" i*) @@ -91,6 +91,14 @@ let error_utf8 cs = Stream.junk cs; (* consume the char to avoid read it and fail again *) err (bp, bp+1) Illegal_character +let utf8_char_size cs = function + (* Utf8 leading byte *) + | '\x00'..'\x7F' -> 1 + | '\xC0'..'\xDF' -> 2 + | '\xE0'..'\xEF' -> 3 + | '\xF0'..'\xF7' -> 4 + | _ (* '\x80'..\xBF'|'\xF8'..'\xFF' *) -> error_utf8 cs + let njunk n = Util.repeat n Stream.junk let check_utf8_trailing_byte cs c = @@ -355,14 +363,8 @@ and progress_utf8 last nj n c tt cs = with Not_found -> last -and progress_from_byte last nj tt cs = function - (* Utf8 leading byte *) - | '\x00'..'\x7F' as c -> progress_utf8 last nj 1 c tt cs - | '\xC0'..'\xDF' as c -> progress_utf8 last nj 2 c tt cs - | '\xE0'..'\xEF' as c -> progress_utf8 last nj 3 c tt cs - | '\xF0'..'\xF7' as c -> progress_utf8 last nj 4 c tt cs - | _ (* '\x80'..\xBF'|'\xF8'..'\xFF' *) -> - error_utf8 cs +and progress_from_byte last nj tt cs c = + progress_utf8 last nj (utf8_char_size cs c) c tt cs (* Must be a special token *) let process_chars bp c cs = @@ -370,7 +372,10 @@ let process_chars bp c cs = let ep = Stream.count cs in match t with | Some t -> (("", t), (bp, ep)) - | None -> err (bp, ep) Undefined_token + | None -> + let ep' = bp + utf8_char_size cs c in + njunk (ep' - ep) cs; + err (bp, ep') Undefined_token let parse_after_dollar bp = parser diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml index 3b433498..f52ebc76 100644 --- a/parsing/pptactic.ml +++ b/parsing/pptactic.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: pptactic.ml 11784 2009-01-14 11:36:32Z herbelin $ *) +(* $Id: pptactic.ml 12581 2009-12-13 15:02:33Z herbelin $ *) open Pp open Names @@ -378,7 +378,7 @@ let pr_as_ipat = function let pr_as_name = function | Anonymous -> mt () - | Name id -> str "as " ++ pr_lident (dummy_loc,id) + | Name id -> str " as " ++ pr_lident (dummy_loc,id) let pr_pose_as_style prc na c = spc() ++ prc c ++ pr_as_name na diff --git a/pretyping/cases.ml b/pretyping/cases.ml index c2d8921e..abe4fcc1 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: cases.ml 12167 2009-06-06 20:07:22Z herbelin $ *) +(* $Id: cases.ml 13112 2010-06-10 19:58:23Z herbelin $ *) open Util open Names @@ -851,7 +851,7 @@ let rec map_predicate f k ccl = function | Abstract _ :: rest -> map_predicate f (k+1) ccl rest -let noccurn_predicate = map_predicate noccurn +let noccur_predicate_between n = map_predicate (noccur_between n) let liftn_predicate n = map_predicate (liftn n) @@ -1122,13 +1122,16 @@ let build_branch current deps (realnames,dep) pb eqns const_info = (* into "Gamma; typs; curalias |- tms" *) let tomatch = lift_tomatch_stack const_info.cs_nargs pb.tomatch in + let pred_is_not_dep = + noccur_predicate_between 1 (List.length realnames + 1) pb.pred tomatch in + let typs'' = list_map2_i (fun i (na,t) deps -> let dep = match dep with | Name _ as na',k -> (if na <> Anonymous then na else na'),k | Anonymous,KnownNotDep -> - if deps = [] && noccurn_predicate 1 pb.pred tomatch then + if deps = [] && pred_is_not_dep then (Anonymous,KnownNotDep) else (force_name na,KnownDep) @@ -1801,7 +1804,8 @@ let prepare_predicate loc typing_fun evdref env tomatchs sign tycon pred = let t2 = mkExistential env ~src:(loc, CasesType) evdref2 in let arsign = extract_arity_signature env tomatchs sign in let names2 = List.rev (List.map (List.map pi1) arsign) in - let nal2,pred2 = build_initial_predicate KnownNotDep names2 t2 in + let pred2 = lift (List.length names2) t2 in + let nal2,pred2 = build_initial_predicate KnownNotDep names2 pred2 in [evdref, nal1, pred1; evdref2, nal2, pred2]) (* Some type annotation *) diff --git a/pretyping/clenv.ml b/pretyping/clenv.ml index 51952f4f..0bfef04a 100644 --- a/pretyping/clenv.ml +++ b/pretyping/clenv.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: clenv.ml 11897 2009-02-09 19:28:02Z barras $ *) +(* $Id: clenv.ml 13126 2010-06-13 11:09:51Z herbelin $ *) open Pp open Util @@ -410,8 +410,9 @@ let clenv_unify_binding_type clenv c t u = try let evd,c = w_coerce_to_type (cl_env clenv) clenv.evd c t u in TypeProcessed, { clenv with evd = evd }, c - with e when precatchable_exception e -> - TypeNotProcessed, clenv, c + with + | PretypeError (_,NotClean _) as e -> raise e + | e when precatchable_exception e -> TypeNotProcessed, clenv, c let clenv_assign_binding clenv k (sigma,c) = let k_typ = clenv_hnf_constr clenv (clenv_meta_type clenv k) in @@ -436,11 +437,11 @@ let clenv_match_args bl clenv = clenv_assign_binding clenv k sc) clenv bl +exception NoSuchBinding + let clenv_constrain_last_binding c clenv = let all_mvs = collect_metas clenv.templval.rebus in - let k = - try list_last all_mvs - with Failure _ -> anomaly "clenv_constrain_with_bindings" in + let k = try list_last all_mvs with Failure _ -> raise NoSuchBinding in clenv_assign_binding clenv k (Evd.empty,c) let clenv_constrain_dep_args hyps_only bl clenv = diff --git a/pretyping/clenv.mli b/pretyping/clenv.mli index 9b2d6e29..4c5535b3 100644 --- a/pretyping/clenv.mli +++ b/pretyping/clenv.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: clenv.mli 10856 2008-04-27 16:15:34Z herbelin $ i*) +(*i $Id: clenv.mli 13126 2010-06-13 11:09:51Z herbelin $ i*) (*i*) open Util @@ -94,6 +94,8 @@ type arg_bindings = open_constr explicit_bindings val clenv_independent : clausenv -> metavariable list val clenv_missing : clausenv -> metavariable list +(** for the purpose of inversion tactics *) +exception NoSuchBinding val clenv_constrain_last_binding : constr -> clausenv -> clausenv (* defines metas corresponding to the name of the bindings *) diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 73dc5d46..20cbba94 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: detyping.ml 11309 2008-08-06 10:30:35Z herbelin $ *) +(* $Id: detyping.ml 12887 2010-03-27 15:57:02Z herbelin $ *) open Pp open Util @@ -329,7 +329,6 @@ let detype_case computable detype detype_eqns testdep avoid data p c bl = n, aliastyp, Some typ in let constructs = Array.init (Array.length bl) (fun i -> (indsp,i+1)) in - let eqnl = detype_eqns constructs consnargsl bl in let tag = try if !Flags.raw_print then @@ -357,8 +356,10 @@ let detype_case computable detype detype_eqns testdep avoid data p c bl = RIf (dl,tomatch,(alias,pred), Option.get nondepbrs.(0),Option.get nondepbrs.(1)) else + let eqnl = detype_eqns constructs consnargsl bl in RCases (dl,tag,pred,[tomatch,(alias,aliastyp)],eqnl) | _ -> + let eqnl = detype_eqns constructs consnargsl bl in RCases (dl,tag,pred,[tomatch,(alias,aliastyp)],eqnl) let detype_sort = function diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 043a326d..18e79e85 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: evarconv.ml 12205 2009-06-22 16:10:15Z barras $ *) +(* $Id: evarconv.ml 12268 2009-08-11 09:02:16Z herbelin $ *) open Pp open Util @@ -66,6 +66,10 @@ let apprec_nohdbeta env evd c = | (Case _ | Fix _) -> applist (evar_apprec env evd [] c) | _ -> c +let position_problem l2r = function + | CONV -> None + | CUMUL -> Some l2r + (* [check_conv_record (t1,l1) (t2,l2)] tries to decompose the problem (t1 l1) = (t2 l2) into a problem @@ -177,9 +181,11 @@ let rec evar_conv_x env evd pbty term1 term2 = let term1 = apprec_nohdbeta env evd term1 in let term2 = apprec_nohdbeta env evd term2 in if is_undefined_evar evd term1 then - solve_simple_eqn evar_conv_x env evd (pbty,destEvar term1,term2) + solve_simple_eqn evar_conv_x env evd + (position_problem true pbty,destEvar term1,term2) else if is_undefined_evar evd term2 then - solve_simple_eqn evar_conv_x env evd (pbty,destEvar term2,term1) + solve_simple_eqn evar_conv_x env evd + (position_problem false pbty,destEvar term2,term1) else evar_eqappr_x env evd pbty (decompose_app term1) (decompose_app term2) @@ -193,14 +199,14 @@ and evar_eqappr_x env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) = let (deb1,rest1) = list_chop (List.length l1-List.length l2) l1 in ise_and i [(fun i -> solve_simple_eqn evar_conv_x env i - (pbty,ev2,applist(term1,deb1))); + (position_problem false pbty,ev2,applist(term1,deb1))); (fun i -> ise_list2 i (fun i -> evar_conv_x env i CONV) rest1 l2)] else let (deb2,rest2) = list_chop (List.length l2-List.length l1) l2 in ise_and i [(fun i -> solve_simple_eqn evar_conv_x env i - (pbty,ev1,applist(term2,deb2))); + (position_problem true pbty,ev1,applist(term2,deb2))); (fun i -> ise_list2 i (fun i -> evar_conv_x env i CONV) l1 rest2)] and f2 i = @@ -224,7 +230,8 @@ and evar_eqappr_x env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) = (* Preserve generality (except that CCI has no eta-conversion) *) let t2 = nf_evar (evars_of evd) (applist appr2) in let t2 = solve_pattern_eqn env l1 t2 in - solve_simple_eqn evar_conv_x env evd (pbty,ev1,t2) + solve_simple_eqn evar_conv_x env evd + (position_problem true pbty,ev1,t2) else if List.length l1 <= List.length l2 then @@ -256,7 +263,8 @@ and evar_eqappr_x env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) = (* Preserve generality (except that CCI has no eta-conversion) *) let t1 = nf_evar (evars_of evd) (applist appr1) in let t1 = solve_pattern_eqn env l2 t1 in - solve_simple_eqn evar_conv_x env evd (pbty,ev2,t1) + solve_simple_eqn evar_conv_x env evd + (position_problem false pbty,ev2,t1) else if List.length l2 <= List.length l1 then @@ -324,7 +332,8 @@ and evar_eqappr_x env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) = (* Preserve generality (except that CCI has no eta-conversion) *) let t2 = nf_evar (evars_of evd) (applist appr2) in let t2 = solve_pattern_eqn env l1 t2 in - solve_simple_eqn evar_conv_x env evd (pbty,ev1,t2) + solve_simple_eqn evar_conv_x env evd + (position_problem true pbty,ev1,t2) else (* Postpone the use of an heuristic *) add_conv_pb (pbty,env,applist appr1,applist appr2) evd, @@ -339,7 +348,8 @@ and evar_eqappr_x env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) = (* Preserve generality (except that CCI has no eta-conversion) *) let t1 = nf_evar (evars_of evd) (applist appr1) in let t1 = solve_pattern_eqn env l2 t1 in - solve_simple_eqn evar_conv_x env evd (pbty,ev2,t1) + solve_simple_eqn evar_conv_x env evd + (position_problem false pbty,ev2,t1) else (* Postpone the use of an heuristic *) add_conv_pb (pbty,env,applist appr1,applist appr2) evd, @@ -505,7 +515,7 @@ let first_order_unification env evd (ev1,l1) (term2,l2) = if is_defined_evar i ev1 then evar_conv_x env i CONV t2 (mkEvar ev1) else - solve_simple_eqn ~choose:true evar_conv_x env i (CONV,ev1,t2))] + solve_simple_eqn ~choose:true evar_conv_x env i (None,ev1,t2))] let choose_less_dependent_instance evk evd term args = let evi = Evd.find (evars_of evd) evk in diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index 994da427..fbaac79b 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: evarutil.ml 12107 2009-04-25 19:58:24Z herbelin $ *) +(* $Id: evarutil.ml 13116 2010-06-12 15:18:07Z herbelin $ *) open Util open Pp @@ -113,11 +113,27 @@ let push_dependent_evars sigma emap = (sigma',emap') (collect_evars emap' ccl)) emap (sigma,emap) +let push_duplicated_evars sigma emap c = + let rec collrec (one,(sigma,emap) as acc) c = + match kind_of_term c with + | Evar (evk,_) when not (Evd.mem sigma evk) -> + if List.mem evk one then + let sigma' = Evd.add sigma evk (Evd.find emap evk) in + let emap' = Evd.remove emap evk in + (one,(sigma',emap')) + else + (evk::one,(sigma,emap)) + | _ -> + fold_constr collrec acc c + in + snd (collrec ([],(sigma,emap)) c) + (* replaces a mapping of existentials into a mapping of metas. Problem if an evar appears in the type of another one (pops anomaly) *) let evars_to_metas sigma (emap, c) = let emap = nf_evars emap in let sigma',emap' = push_dependent_evars sigma emap in + let sigma',emap' = push_duplicated_evars sigma' emap' c in let change_exist evar = let ty = nf_betaiota emap (existential_type emap evar) in let n = new_meta() in @@ -559,6 +575,7 @@ let rec expansions_of_var env x = *) exception NotUnique +exception NotUniqueInType of types type evar_projection = | ProjectVar @@ -570,12 +587,13 @@ let rec find_projectable_vars with_evars env sigma y subst = if y = y' or expand_var env y = expand_var env y' then (idc,(y'=y,(id,ProjectVar))) else if with_evars & isEvar y' then + (* TODO: infer conditions for being of unifiable types *) let (evk,argsv as t) = destEvar y' in let evi = Evd.find sigma evk in let subst = make_projectable_subst sigma evi argsv in let l = find_projectable_vars with_evars env sigma y subst in match l with - | [id',p] -> (idc,(true,(id,ProjectEvar (t,evi,id',p)))) + | [id',p] -> (idc,(true,(id,ProjectEvar(t,evi,id',p)))) | _ -> failwith "" else failwith "" in let l = map_succeed is_projectable subst in @@ -596,6 +614,12 @@ let project_with_effects env sigma effects t subst = effects := p :: !effects; c +let rec find_solution_type evarenv = function + | (id,ProjectVar)::l -> pi3 (lookup_named id evarenv) + | [id,ProjectEvar _] -> (* bugged *) pi3 (lookup_named id evarenv) + | (id,ProjectEvar _)::l -> find_solution_type evarenv l + | [] -> assert false + (* In case the solution to a projection problem requires the instantiation of * subsidiary evars, [do_projection_effects] performs them; it * also try to instantiate the type of those subsidiary evars if their @@ -709,7 +733,7 @@ let filter_along f projs v = * such that "hyps' |- ?e : T" *) -let do_restrict_hyps_virtual evd evk filter = +let restrict_hyps evd evk filter = (* What to do with dependencies? Assume we have x:A, y:B(x), z:C(x,y) |- ?e:T(x,y,z) and restrict on y. - If y is in a non-erasable position in C(x,y) (i.e. it is not below an @@ -726,15 +750,15 @@ let do_restrict_hyps_virtual evd evk filter = let filter,_ = List.fold_right (fun oldb (l,filter) -> if oldb then List.hd filter::l,List.tl filter else (false::l,filter)) oldfilter ([],List.rev filter) in - new_evar evd env ~src:(evar_source evk evd) - ~filter:filter evi.evar_concl + (env,evar_source evk evd,filter,evi.evar_concl) let do_restrict_hyps evd evk projs = let filter = List.map filter_of_projection projs in if List.for_all (fun x -> x) filter then evd,evk else - let evd,nc = do_restrict_hyps_virtual evd evk filter in + let env,src,filter,ccl = restrict_hyps evd evk filter in + let evd,nc = new_evar evd env ~src ~filter ccl in let evd = Evd.evar_define evk nc evd in let evk',_ = destEvar nc in evd,evk' @@ -854,7 +878,9 @@ let rec invert_definition choose env evd (evk,argsv as ev) rhs = let c, p = match sols with | [] -> raise Not_found | [id,p] -> (mkVar id, p) - | (id,p)::_::_ -> if choose then (mkVar id, p) else raise NotUnique + | (id,p)::_::_ -> + if choose then (mkVar id, p) + else raise (NotUniqueInType(find_solution_type (evar_env evi) sols)) in let ty = lazy (Retyping.get_type_of env (evars_of !evdref) t) in let evd = do_projection_effects evar_define env ty !evdref p in @@ -862,14 +888,15 @@ let rec invert_definition choose env evd (evk,argsv as ev) rhs = c with | Not_found -> raise (NotInvertibleUsingOurAlgorithm t) - | NotUnique -> + | NotUniqueInType ty -> if not !progress then raise NotEnoughInformationToProgress; (* No unique projection but still restrict to where it is possible *) let ts = expansions_of_var env t in let test c = isEvar c or List.mem c ts in let filter = array_map_to_list test argsv in let args' = filter_along (fun x -> x) filter argsv in - let evd,evar = do_restrict_hyps_virtual !evdref evk filter in + let evarenv,src,filter,_ = restrict_hyps !evdref evk filter in + let evd,evar = new_evar !evdref evarenv ~src ~filter ty in let evk',_ = destEvar evar in let pb = (Reduction.CONV,env,mkEvar(evk',args'),t) in evdref := Evd.add_conv_pb pb evd; @@ -1122,6 +1149,24 @@ let solve_refl conv_algo env evd evk argsv1 argsv2 = let pb = (Reduction.CONV,env,mkEvar(evk,argsv1),mkEvar(evk,argsv2)) in Evd.add_conv_pb pb evd +(* Util *) + +let check_instance_type conv_algo env evd ev1 t2 = + let t2 = nf_evar (evars_of evd) t2 in + if has_undefined_evars evd t2 then + (* May contain larger constraints than needed: don't want to + commit to an equal solution while only subtyping is requested *) + evd + else + let typ2 = Retyping.get_type_of env (evars_of evd) (refresh_universes t2) in + if isEvar typ2 then (* Don't want to commit too early too *) evd + else + let typ1 = existential_type (evars_of evd) ev1 in + let evd,b = conv_algo env evd Reduction.CUMUL typ2 typ1 in + if b then evd else + user_err_loc (fst (evar_source (fst ev1) evd),"", + str "Unable to find a well-typed instantiation") + (* Tries to solve problem t1 = t2. * Precondition: t1 is an uninstantiated evar * Returns an optional list of evars that were instantiated, or None @@ -1136,15 +1181,23 @@ let solve_simple_eqn conv_algo ?(choose=false) env evd (pbty,(evk1,args1 as ev1) if evk1 = evk2 then solve_refl conv_algo env evd evk1 args1 args2 else - if pbty = Reduction.CONV + if pbty = None then solve_evar_evar evar_define env evd ev1 ev2 - else add_conv_pb (pbty,env,mkEvar ev1,t2) evd + else if pbty = Some true then + add_conv_pb (Reduction.CUMUL,env,mkEvar ev1,t2) evd + else + add_conv_pb (Reduction.CUMUL,env,t2,mkEvar ev1) evd | _ -> + let evd = + if pbty = Some false then + check_instance_type conv_algo env evd ev1 t2 + else + evd in let evd = evar_define ~choose env ev1 t2 evd in let evm = evars_of evd in let evi = Evd.find evm evk1 in if occur_existential evm evi.evar_concl then - let evenv = evar_env evi in + let evenv = evar_unfiltered_env evi in let evc = nf_isevar evd evi.evar_concl in match evi.evar_body with | Evar_defined body -> diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli index cb54f400..eef41da3 100644 --- a/pretyping/evarutil.mli +++ b/pretyping/evarutil.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: evarutil.mli 12053 2009-04-06 16:20:42Z msozeau $ i*) +(*i $Id: evarutil.mli 12268 2009-08-11 09:02:16Z herbelin $ i*) (*i*) open Util @@ -80,7 +80,7 @@ val solve_refl : evar_defs val solve_simple_eqn : (env -> evar_defs -> conv_pb -> constr -> constr -> evar_defs * bool) - -> ?choose:bool -> env -> evar_defs -> conv_pb * existential * constr -> + -> ?choose:bool -> env -> evar_defs -> bool option * existential * constr -> evar_defs * bool (* [check_evars env initial_sigma extended_sigma c] fails if some diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index 740b2ca8..f579afa6 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: tacred.ml 11897 2009-02-09 19:28:02Z barras $ *) +(* $Id: tacred.ml 12233 2009-07-08 22:50:56Z herbelin $ *) open Pp open Util @@ -137,20 +137,27 @@ let _ = Summary.survive_module = false; Summary.survive_section = false } -(* Check that c is an "elimination constant" +(* [compute_consteval] determines whether c is an "elimination constant" - either [xn:An]..[x1:A1](

Case (Rel i) of f1..fk end g1 ..gp) + either [yn:Tn]..[y1:T1](match yi with f1..fk end g1 ..gp) - or [xn:An]..[x1:A1](Fix(f|t) (Rel i1) ..(Rel ip)) - with i1..ip distinct variables not occuring in t + or [yn:Tn]..[y1:T1](Fix(f|t) yi1..yip) + with yi1..yip distinct variables among the yi, not occurring in t - In the second case, keep relevenant information ([i1,Ai1;..;ip,Aip],n) - in order to compute an equivalent of Fix(f|t)[xi<-ai] as + In the second case, [check_fix_reversibility [T1;...;Tn] args fix] + checks that [args] is a subset of disjoint variables in y1..yn (a necessary + condition for reversibility). It also returns the relevant + information ([i1,Ti1;..;ip,Tip],n) in order to compute an + equivalent of Fix(f|t) such that - [yip:Bip]..[yi1:Bi1](F bn..b1) - == [yip:Bip]..[yi1:Bi1](Fix(f|t)[xi<-ai] (Rel p)..(Rel 1)) + g := [xp:Tip']..[x1:Ti1'](f a1..an) + == [xp:Tip']..[x1:Ti1'](Fix(f|t) yi1..yip) - with bj=aj if j<>ik and bj=(Rel c) and Bic=Aic[xn..xic-1 <- an..aic-1] + with a_k:=y_k if k<>i_j, a_k:=args_k otherwise, and + Tij':=Tij[x1..xi(j-1) <- a1..ai(j-1)] + + Note that the types Tk, when no i_j=k, must not be dependent on + the xp..x1. *) let check_fix_reversibility labs args ((lv,i),(_,tys,bds)) = @@ -172,8 +179,14 @@ let check_fix_reversibility labs args ((lv,i),(_,tys,bds)) = | _ -> raise Elimconst) args in - if not (list_distinct (List.map fst li)) then + let reversible_rels = List.map fst li in + if not (list_distinct reversible_rels) then raise Elimconst; + list_iter_i (fun i t_i -> + if not (List.mem_assoc (i+1) li) then + let fvs = List.map ((+) (i+1)) (Intset.elements (free_rels t_i)) in + if list_intersect fvs reversible_rels <> [] then raise Elimconst) + labs; let k = lv.(i) in if k < nargs then (* Such an optimisation would need eta-expansion @@ -294,19 +307,22 @@ let rev_firstn_liftn fn ln = (* If f is bound to EliminationFix (n',infos), then n' is the minimal number of args for starting the reduction and infos is (nbfix,[(yi1,Ti1);...;(yip,Tip)],n) indicating that f converts - to some [y1:T1,...,yn:Tn](Fix(..) yip .. yi1) where we can remark that - yij = Rel(n+1-j) + to some [y1:T1,...,yn:Tn](Fix(..) yip .. yi1) where the y_{i_j} consist in a + disjoint subset of the yi, i.e. 1 <= ij <= n and the ij are disjoint (in + particular, p <= n). + + f is applied to largs := arg1 .. argn and we need for recursive + calls to build the function - f is applied to largs and we need for recursive calls to build the function g := [xp:Tip',...,x1:Ti1'](f a1 ... an) s.t. (g u1 ... up) reduces to (Fix(..) u1 ... up) This is made possible by setting - a_k:=z_j if k=i_j - a_k:=y_k otherwise + a_k:=x_j if k=i_j for some j + a_k:=arg_k otherwise - The type Tij' is Tij[yn..yi(j-1)..y1 <- ai(j-1)..a1] + The type Tij' is Tij[yi(j-1)..y1 <- ai(j-1)..a1] *) let x = Name (id_of_string "x") @@ -328,7 +344,7 @@ let make_elim_fun (names,(nbfix,lv,n)) largs = | Some (minargs,ref) -> let body = applistc (mkEvalRef ref) la in let g = - list_fold_left_i (fun q (* j from comment is n+1-q *) c (ij,tij) -> + list_fold_left_i (fun q (* j = n+1-q *) c (ij,tij) -> let subst = List.map (lift (-q)) (list_firstn (n-ij) la) in let tij' = substl (List.rev subst) tij in mkLambda (x,tij',c)) 1 body (List.rev lv) diff --git a/pretyping/unification.ml b/pretyping/unification.ml index bfd601e2..c92f1fc6 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: unification.ml 12163 2009-06-06 17:36:47Z herbelin $ *) +(* $Id: unification.ml 12268 2009-08-11 09:02:16Z herbelin $ *) open Pp open Util @@ -517,7 +517,7 @@ let order_metas metas = (* Solve an equation ?n[x1=u1..xn=un] = t where ?n is an evar *) let solve_simple_evar_eqn env evd ev rhs = - let evd,b = solve_simple_eqn Evarconv.evar_conv_x env evd (CONV,ev,rhs) in + let evd,b = solve_simple_eqn Evarconv.evar_conv_x env evd (None,ev,rhs) in if not b then error_cannot_unify env (evars_of evd) (mkEvar ev,rhs); let (evd,b) = Evarconv.consider_remaining_unif_problems env evd in if not b then error "Cannot solve unification constraints"; diff --git a/proofs/decl_mode.ml b/proofs/decl_mode.ml index f8fc4e87..134a4d8b 100644 --- a/proofs/decl_mode.ml +++ b/proofs/decl_mode.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: decl_mode.ml 10739 2008-04-01 14:45:20Z herbelin $ i*) +(*i $Id: decl_mode.ml 12422 2009-10-27 08:42:49Z corbinea $ i*) open Names open Term @@ -45,7 +45,7 @@ type split_tree= | Split_patt of Idset.t * inductive * (bool array * (Idset.t * split_tree) option) array | Close_patt of split_tree - | End_patt of (identifier * int) + | End_patt of (identifier * (int * int)) type elim_kind = EK_dep of split_tree @@ -124,3 +124,4 @@ let get_last env = try let (id,_,_) = List.hd (Environ.named_context env) in id with Invalid_argument _ -> error "no previous statement to use" + diff --git a/proofs/decl_mode.mli b/proofs/decl_mode.mli index 77bee313..bcfd6a96 100644 --- a/proofs/decl_mode.mli +++ b/proofs/decl_mode.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: decl_mode.mli 10739 2008-04-01 14:45:20Z herbelin $ *) +(* $Id: decl_mode.mli 12422 2009-10-27 08:42:49Z corbinea $ *) open Names open Term @@ -33,7 +33,7 @@ type split_tree= | Split_patt of Idset.t * inductive * (bool array * (Idset.t * split_tree) option) array | Close_patt of split_tree - | End_patt of (identifier * int) + | End_patt of (identifier * (int * int)) type elim_kind = EK_dep of split_tree diff --git a/proofs/logic.ml b/proofs/logic.ml index caf6f56b..c019d45f 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: logic.ml 12168 2009-06-06 21:34:37Z herbelin $ *) +(* $Id: logic.ml 12240 2009-07-15 09:52:52Z herbelin $ *) open Pp open Util @@ -438,7 +438,7 @@ and mk_casegoals sigma goal goalacc p c = let (acc'',pt) = mk_hdgoals sigma goal acc' p in let pj = {uj_val=p; uj_type=pt} in let indspec = - try find_mrectype env sigma ct + try find_mrectype env sigma (nf_evar sigma ct) with Not_found -> anomaly "mk_casegoals" in let (lbrty,conclty) = type_case_branches_with_names env indspec pj c in diff --git a/scripts/coqc.ml b/scripts/coqc.ml index 784e2d51..69357b2f 100644 --- a/scripts/coqc.ml +++ b/scripts/coqc.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: coqc.ml 11749 2009-01-05 14:01:04Z notin $ *) +(* $Id: coqc.ml 12911 2010-04-09 10:08:37Z herbelin $ *) (* Afin de rendre Coq plus portable, ce programme Caml remplace le script coqc. @@ -126,8 +126,8 @@ let parse_args () = parse (cfiles,args) rem | ("-?"|"-h"|"-H"|"-help"|"--help") :: _ -> usage () - | ("-I"|"-include"|"-outputstate" - |"-inputstate"|"-is"|"-load-vernac-source"|"-l"|"-load-vernac-object" + | ("-outputstate"|"-inputstate"|"-is" + |"-load-vernac-source"|"-l"|"-load-vernac-object" |"-load-ml-source"|"-require"|"-load-ml-object"|"-user" |"-init-file" | "-dump-glob" | "-coqlib" as o) :: rem -> begin @@ -135,7 +135,17 @@ let parse_args () = | s :: rem' -> parse (cfiles,s::o::args) rem' | [] -> usage () end - | "-R" as o :: s :: t :: rem -> parse (cfiles,t::s::o::args) rem + | ("-I"|"-include" as o) :: rem -> + begin + match rem with + | s :: "-as" :: t :: rem' -> parse (cfiles,t::"-as"::s::o::args) rem' + | s :: "-as" :: [] -> usage () + | s :: rem' -> parse (cfiles,s::o::args) rem' + | [] -> usage () + end + | "-R" :: s :: "-as" :: t :: rem -> parse (cfiles,t::"-as"::s::"-R"::args) rem + | "-R" :: s :: "-as" :: [] -> usage () + | "-R" :: s :: t :: rem -> parse (cfiles,t::s::"-R"::args) rem | ("-notactics"|"-debug"|"-nolib" |"-debugVM"|"-alltransp"|"-VMno" diff --git a/scripts/coqmktop.ml b/scripts/coqmktop.ml index 9a7d30b1..ee8ef1d9 100644 --- a/scripts/coqmktop.ml +++ b/scripts/coqmktop.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: coqmktop.ml 11784 2009-01-14 11:36:32Z herbelin $ *) +(* $Id: coqmktop.ml 12874 2010-03-19 23:15:52Z herbelin $ *) (* coqmktop is a script to link Coq, analogous to ocamlmktop. The command line contains options specific to coqmktop, options for the @@ -277,7 +277,7 @@ let main () = (*file for dynlink *) let dynlink= if not (!opt || !top) then - [(print_int 2; tmp_dynlink())] + [tmp_dynlink()] else [] in diff --git a/tactics/decl_interp.ml b/tactics/decl_interp.ml index c99884c0..62824670 100644 --- a/tactics/decl_interp.ml +++ b/tactics/decl_interp.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: decl_interp.ml 11576 2008-11-10 19:13:15Z msozeau $ i*) +(*i $Id: decl_interp.ml 12422 2009-10-27 08:42:49Z corbinea $ i*) open Util open Names @@ -334,7 +334,7 @@ let interp_cases info sigma env params (pat:cases_pattern_expr) hyps = if List.length params <> expected then errorlabstrm "suppose it is" (str "Wrong number of extra arguments: " ++ - (if expected = 0 then str "none" else int expected) ++ + (if expected = 0 then str "none" else int expected) ++ spc () ++ str "expected.") in let app_ind = let rind = RRef (dummy_loc,Libnames.IndRef pinfo.per_ind) in diff --git a/tactics/decl_proof_instr.ml b/tactics/decl_proof_instr.ml index 62a8ddfc..67d1d41a 100644 --- a/tactics/decl_proof_instr.ml +++ b/tactics/decl_proof_instr.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: decl_proof_instr.ml 12135 2009-05-20 14:49:23Z herbelin $ *) +(* $Id: decl_proof_instr.ml 12422 2009-10-27 08:42:49Z corbinea $ *) open Util open Pp @@ -1161,7 +1161,7 @@ let case_tac params pat_info hyps gls0 = let clause = build_dep_clause params pat_info per_info hyps gls0 in let ninfo1 = {pm_stack=Suppose_case::info.pm_stack} in let nek = - register_dep_subcase (id,List.length hyps) (pf_env gls0) per_info + register_dep_subcase (id,(List.length params,List.length hyps)) (pf_env gls0) per_info pat_info.pat_pat ek in let ninfo2 = {pm_stack=Per(et,per_info,nek,id::old_clauses)::rest} in tclTHENS (assert_postpone id clause) @@ -1227,6 +1227,7 @@ let hrec_for fix_id per_info gls obj_id = let hd2 = applist (mkVar fix_id,args@[obj]) in compose_lam rc (whd_beta gls.sigma hd2) + let rec execute_cases fix_name per_info tacnext args objs nhrec tree gls = match tree, objs with Close_patt t,_ -> @@ -1235,16 +1236,19 @@ let rec execute_cases fix_name per_info tacnext args objs nhrec tree gls = | Skip_patt (_,t),skipped::next_objs -> let args0 = push_arg skipped args in execute_cases fix_name per_info tacnext args0 next_objs nhrec t gls - | End_patt (id,nhyps),[] -> + | End_patt (id,(nparams,nhyps)),[] -> begin match List.assoc id args with [None,br_args] -> - let metas = - list_tabulate (fun n -> mkMeta (succ n)) nhyps in + let all_metas = + list_tabulate (fun n -> mkMeta (succ n)) (nparams + nhyps) in + let param_metas,hyp_metas = list_chop nparams all_metas in tclTHEN (tclDO nhrec introf) (tacnext - (applist (mkVar id,List.rev_append br_args metas))) gls + (applist (mkVar id, + List.append param_metas + (List.rev_append br_args hyp_metas)))) gls | _ -> anomaly "wrong stack size" end | Split_patt (ids,ind,br), casee::next_objs -> @@ -1318,7 +1322,19 @@ let rec execute_cases fix_name per_info tacnext args objs nhrec tree gls = | End_patt (_,_) , _ :: _ -> anomaly "execute_cases : End of branch with garbage left" - +let understand_my_constr c gls = + let env = pf_env gls in + let nc = names_of_rel_context env in + let rawc = Detyping.detype false [] nc c in + let rec frob = function REvar _ -> RHole (dummy_loc,QuestionMark Expand) | rc -> map_rawconstr frob rc in + Pretyping.Default.understand_tcc (sig_sig gls) env ~expected_type:(pf_concl gls) (frob rawc) + +let set_refine,my_refine = +let refine = ref (fun (_:open_constr) -> (assert false : tactic) ) in +((fun tac -> refine:= tac), +(fun c gls -> + let oc = understand_my_constr c gls in + !refine oc gls)) (* end focus/claim *) @@ -1361,7 +1377,7 @@ let end_tac et2 gls = | ET_Case_analysis,EK_dep tree -> execute_cases Anonymous pi (fun c -> tclTHENLIST - [refine c; + [my_refine c; clear clauses; justification assumption]) (initial_instance_stack clauses) [pi.per_casee] 0 tree @@ -1382,7 +1398,7 @@ let end_tac et2 gls = (fun c -> tclTHENLIST [clear [fix_id]; - refine c; + my_refine c; clear clauses; justification assumption]) (initial_instance_stack clauses) diff --git a/tactics/decl_proof_instr.mli b/tactics/decl_proof_instr.mli index 877c8047..5f4a0485 100644 --- a/tactics/decl_proof_instr.mli +++ b/tactics/decl_proof_instr.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: decl_proof_instr.mli 11481 2008-10-20 19:23:51Z herbelin $ *) +(* $Id: decl_proof_instr.mli 12422 2009-10-27 08:42:49Z corbinea $ *) open Refiner open Names @@ -42,20 +42,20 @@ val execute_cases : Term.constr list -> int -> Decl_mode.split_tree -> Proof_type.tactic val tree_of_pats : - identifier * int -> (Rawterm.cases_pattern*recpath) list list -> + identifier * (int * int) -> (Rawterm.cases_pattern*recpath) list list -> split_tree val add_branch : - identifier * int -> (Rawterm.cases_pattern*recpath) list list -> + identifier * (int * int) -> (Rawterm.cases_pattern*recpath) list list -> split_tree -> split_tree val append_branch : - identifier * int -> int -> (Rawterm.cases_pattern*recpath) list list -> + identifier *(int * int) -> int -> (Rawterm.cases_pattern*recpath) list list -> (Names.Idset.t * Decl_mode.split_tree) option -> (Names.Idset.t * Decl_mode.split_tree) option val append_tree : - identifier * int -> int -> (Rawterm.cases_pattern*recpath) list list -> + identifier * (int * int) -> int -> (Rawterm.cases_pattern*recpath) list list -> split_tree -> split_tree val build_dep_clause : Term.types Decl_expr.statement list -> @@ -65,7 +65,7 @@ val build_dep_clause : Term.types Decl_expr.statement list -> Decl_expr.hyp list -> Proof_type.goal Tacmach.sigma -> Term.types val register_dep_subcase : - Names.identifier * int -> + Names.identifier * (int * int) -> Environ.env -> Decl_mode.per_info -> Rawterm.cases_pattern -> Decl_mode.elim_kind -> Decl_mode.elim_kind @@ -115,3 +115,4 @@ val init_tree: (Names.Idset.t * Decl_mode.split_tree) option) -> Decl_mode.split_tree +val set_refine : (Evd.open_constr -> Proof_type.tactic) -> unit diff --git a/tactics/equality.ml b/tactics/equality.ml index 58a00419..bf199379 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: equality.ml 12053 2009-04-06 16:20:42Z msozeau $ *) +(* $Id: equality.ml 12886 2010-03-27 14:22:00Z herbelin $ *) open Pp open Util @@ -688,6 +688,16 @@ let minimal_free_rels env sigma (c,cty) = else (cty',rels') +(* Like the above, but recurse over all the rels found until there are + no more rels to be found *) +let minimal_free_rels_rec env sigma = + let rec minimalrec_free_rels_rec prev_rels (c,cty) = + let (cty,direct_rels) = minimal_free_rels env sigma (c,cty) in + let combined_rels = Intset.union prev_rels direct_rels in + let folder rels i = snd (minimalrec_free_rels_rec rels (c, type_of env sigma (mkRel i))) + in (cty, List.fold_left folder combined_rels (Intset.elements (Intset.diff direct_rels prev_rels))) + in minimalrec_free_rels_rec Intset.empty + (* [sig_clausal_form siglen ty] Will explode [siglen] [sigS,sigT ]'s on [ty] (depending on the @@ -706,7 +716,7 @@ let minimal_free_rels env sigma (c,cty) = WARNING: No checking is done to make sure that the sigS(or sigT)'s are actually there. - - Only homogenious pairs are built i.e. pairs where all the + - Only homogeneous pairs are built i.e. pairs where all the dependencies are of the same sort [sig_clausal_form] proceed as follows: the default tuple is @@ -747,7 +757,12 @@ let sig_clausal_form env sigma sort_of_ty siglen ty dflt = Evd.existential_opt_value (Evd.evars_of !evdref) (destEvar ev) with - | Some w -> applist(exist_term,[a;p_i_minus_1;w;tuple_tail]) + | Some w -> + let w_type = type_of env sigma w in + if Evarconv.e_conv env evdref w_type a then + applist(exist_term,[a;p_i_minus_1;w;tuple_tail]) + else + error "Cannot solve a unification problem." | None -> anomaly "Not enough components to build the dependent tuple" in let scf = sigrec_clausal_form siglen ty in @@ -812,7 +827,7 @@ let sig_clausal_form env sigma sort_of_ty siglen ty dflt = *) let make_iterated_tuple env sigma dflt (z,zty) = - let (zty,rels) = minimal_free_rels env sigma (z,zty) in + let (zty,rels) = minimal_free_rels_rec env sigma (z,zty) in let sort_of_zty = get_sort_of env sigma zty in let sorted_rels = Sort.list (<) (Intset.elements rels) in let (tuple,tuplety) = diff --git a/tactics/hiddentac.ml b/tactics/hiddentac.ml index 8e517453..4ab40acb 100644 --- a/tactics/hiddentac.ml +++ b/tactics/hiddentac.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: hiddentac.ml 12102 2009-04-24 10:48:11Z herbelin $ *) +(* $Id: hiddentac.ml 13124 2010-06-13 11:09:38Z herbelin $ *) open Term open Proof_type @@ -83,10 +83,10 @@ let h_simple_induction_destruct isrec h = let h_simple_induction = h_simple_induction_destruct true let h_simple_destruct = h_simple_induction_destruct false -let h_induction_destruct isrec ev l = +let h_induction_destruct ev isrec l = abstract_tactic (TacInductionDestruct (isrec,ev,List.map (fun (c,e,idl,cl) -> List.map inj_ia c,Option.map inj_open_wb e,idl,cl) l)) - (induction_destruct ev isrec l) + (induction_destruct isrec ev l) let h_new_induction ev c e idl cl = h_induction_destruct ev true [c,e,idl,cl] let h_new_destruct ev c e idl cl = h_induction_destruct ev false [c,e,idl,cl] @@ -105,7 +105,7 @@ let h_revert l = abstract_tactic (TacRevert l) (revert l) (* Constructors *) let h_left ev l = abstract_tactic (TacLeft (ev,l)) (left_with_ebindings ev l) -let h_right ev l = abstract_tactic (TacLeft (ev,l)) (right_with_ebindings ev l) +let h_right ev l = abstract_tactic (TacRight (ev,l)) (right_with_ebindings ev l) let h_split ev l = abstract_tactic (TacSplit (ev,false,l)) (split_with_ebindings ev l) (* Moved to tacinterp because of dependencies in Tacinterp.interp let h_any_constructor t = diff --git a/tactics/inv.ml b/tactics/inv.ml index 977b602e..af204e77 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: inv.ml 11784 2009-01-14 11:36:32Z herbelin $ *) +(* $Id: inv.ml 12410 2009-10-24 17:23:39Z herbelin $ *) open Pp open Util @@ -291,7 +291,7 @@ let generalizeRewriteIntros tac depids id gls = let rec tclMAP_i n tacfun = function | [] -> tclDO n (tacfun None) | a::l -> - if n=0 then error "Too much names." + if n=0 then error "Too many names." else tclTHEN (tacfun (Some a)) (tclMAP_i (n-1) tacfun l) let remember_first_eq id x = if !x = no_move then x := MoveAfter id diff --git a/tactics/leminv.ml b/tactics/leminv.ml index e798f59a..4cbfa6c2 100644 --- a/tactics/leminv.ml +++ b/tactics/leminv.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: leminv.ml 11897 2009-02-09 19:28:02Z barras $ *) +(* $Id: leminv.ml 13126 2010-06-13 11:09:51Z herbelin $ *) open Pp open Util @@ -291,11 +291,15 @@ let add_inversion_lemma_exn na com comsort bool tac = (* ================================= *) let lemInv id c gls = + ignore (pf_get_hyp gls id); (* ensure id exists *) try let clause = mk_clenv_type_of gls c in let clause = clenv_constrain_last_binding (mkVar id) clause in Clenvtac.res_pf clause ~allow_K:true gls with + | NoSuchBinding -> + errorlabstrm "" + (hov 0 (pr_constr c ++ spc () ++ str "does not refer to an inversion lemma.")) | UserError (a,b) -> errorlabstrm "LemInv" (str "Cannot refine current goal with the lemma " ++ diff --git a/tactics/refine.ml b/tactics/refine.ml index 322d25e5..ff3f0887 100644 --- a/tactics/refine.ml +++ b/tactics/refine.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: refine.ml 12187 2009-06-13 19:36:59Z msozeau $ *) +(* $Id: refine.ml 13129 2010-06-13 14:23:55Z herbelin $ *) (* JCF -- 6 janvier 1998 EXPERIMENTAL *) @@ -108,6 +108,8 @@ let replace_by_meta env sigma = function | _ -> invalid_arg "Tcc.replace_by_meta (TO DO)" *) in + if occur_meta ty then + error "Unable to manage a dependent metavariable of higher-order type."; mkCast (m,DEFAULTcast, ty),[n,ty],[Some th] exception NoMeta @@ -189,6 +191,8 @@ let rec compute_metamap env sigma c = match kind_of_term c with end | Case (ci,p,cc,v) -> + if occur_meta p then + error "Unable to manage a metavariable in the return clause of a match."; (* bof... *) let nbr = Array.length v in let v = Array.append [|p;cc|] v in @@ -380,3 +384,5 @@ let refine (evd,c) gl = complicated to update meta types when passing through a binder *) let th = compute_metamap (pf_env gl) evd c in tclTHEN (Refiner.tclEVARS evd) (tcc_aux [] th) gl + +let _ = Decl_proof_instr.set_refine refine (* dirty trick to solve circular dependency *) diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 71b50b66..5c891c58 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: tacinterp.ml 12187 2009-06-13 19:36:59Z msozeau $ *) +(* $Id: tacinterp.ml 13130 2010-06-13 18:45:09Z herbelin $ *) open Constrintern open Closure @@ -1096,7 +1096,9 @@ let apply_one_mhyp_context ist env gl lmatch (hypname,patv,pat) lhyps = match_next_pattern find_next') with | PatternMatchingFailure -> apply_one_mhyp_context_rec tl in - match_next_pattern (fun () -> match_pat lmatch hyp pat) () + match_next_pattern (fun () -> + let hyp = if b<>None then refresh_universes_strict hyp else hyp in + match_pat lmatch hyp pat) () | Some patv -> match b with | Some body -> @@ -1112,7 +1114,9 @@ let apply_one_mhyp_context ist env gl lmatch (hypname,patv,pat) lhyps = | PatternMatchingFailure -> match_next_pattern_in_body next_in_body' () in match_next_pattern_in_typ - (fun () -> match_pat lmeta hyp pat) () + (fun () -> + let hyp = refresh_universes_strict hyp in + match_pat lmeta hyp pat) () with PatternMatchingFailure -> apply_one_mhyp_context_rec tl in match_next_pattern_in_body @@ -2872,7 +2876,8 @@ let add_tacdef isrec tacl = (***************************************************************************) (* Other entry points *) -let glob_tactic x = intern_tactic (make_empty_glob_sign ()) x +let glob_tactic x = + Flags.with_option strict_check (intern_tactic (make_empty_glob_sign ())) x let glob_tactic_env l env x = Flags.with_option strict_check diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 0a8b5d01..0a4c0fbe 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: tactics.ml 12187 2009-06-13 19:36:59Z msozeau $ *) +(* $Id: tactics.ml 12956 2010-04-20 08:49:15Z herbelin $ *) open Pp open Util @@ -249,14 +249,51 @@ let change_option occl t = function Some id -> change_in_hyp occl t id | None -> change_in_concl occl t -let change occl c cls = +let out_arg = function + | ArgVar _ -> anomaly "Unevaluated or_var variable" + | ArgArg x -> x + +let adjust_clause occl cls = + (* warn as much as possible on loss of occurrence information *) (match cls, occl with ({onhyps=(Some(_::_::_)|None)} |{onhyps=Some(_::_);concl_occs=((false,_)|(true,_::_))}), Some _ -> error "No occurrences expected when changing several hypotheses." | _ -> ()); - onClauses (change_option occl c) cls + (* get at clause from cls if only goal or one hyp specified *) + let occl,cls = match occl with + | None -> None,cls + | Some (occs,c) -> + if cls.onhyps=Some[] && occs=all_occurrences then + Some (on_snd (List.map out_arg) cls.concl_occs,c), + {cls with concl_occs=all_occurrences_expr} + else + match cls.onhyps with + | Some[(occs',id),l] when + cls.concl_occs=no_occurrences_expr && occs=all_occurrences -> + Some (on_snd (List.map out_arg) occs',c), + {cls with onhyps=Some[(all_occurrences_expr,id),l]} + | _ -> + occl,cls in + (* check if cls has still specified occs *) + if cls.onhyps <> None && + List.exists (fun ((occs,_),_) -> occs <> all_occurrences_expr) + (Option.get cls.onhyps) + || cls.concl_occs <> all_occurrences_expr && + cls.concl_occs <> no_occurrences_expr + then + Flags.if_verbose Pp.msg_warning + (if cls.onhyps=Some[] then + str "Trailing \"at\" modifier not taken into account." + else + str "\"at\" modifier in clause \"in\" not taken into account."); + (* Anticipate on onClauses which removes concl if not at all occs *) + if cls.concl_occs=no_occurrences_expr then cls + else {cls with concl_occs=all_occurrences_expr} + +let change occl c cls = + onClauses (change_option occl c) (adjust_clause occl cls) (* Pour usage interne (le niveau User est pris en compte par reduce) *) let red_in_concl = reduct_in_concl (red_product,DEFAULTcast) @@ -1397,10 +1434,6 @@ let quantify lconstr = the left of each x1, ...). *) -let out_arg = function - | ArgVar _ -> anomaly "Unevaluated or_var variable" - | ArgArg x -> x - let occurrences_of_hyp id cls = let rec hyp_occ = function [] -> None @@ -2546,6 +2579,7 @@ let induction_tac_felim with_evars indvars scheme gl = let apply_induction_in_context isrec hyp0 indsign indvars names induct_tac gl = let env = pf_env gl in let statlists,lhyp0,indhyps,deps = cook_sign hyp0 indvars env in + let deps = List.map (fun (id,c,t)-> (id,c,refresh_universes_strict t)) deps in let tmpcl = it_mkNamedProd_or_LetIn (pf_concl gl) deps in let names = compute_induction_names (Array.length indsign) names in let dephyps = List.map (fun (id,_,_) -> id) deps in diff --git a/tactics/tauto.ml4 b/tactics/tauto.ml4 index 1729695d..d3e7da6a 100644 --- a/tactics/tauto.ml4 +++ b/tactics/tauto.ml4 @@ -8,7 +8,7 @@ (*i camlp4deps: "parsing/grammar.cma" i*) -(*i $Id: tauto.ml4 11739 2009-01-02 19:33:19Z herbelin $ i*) +(*i $Id: tauto.ml4 12955 2010-04-20 08:10:14Z herbelin $ i*) open Term open Hipattern @@ -20,6 +20,7 @@ open Tacticals open Tacinterp open Tactics open Util +open Genarg let assoc_var s ist = match List.assoc (Names.id_of_string s) ist.lfun with @@ -97,18 +98,21 @@ let is_conj ist = let flatten_contravariant_conj ist = let typ = assoc_var "X1" ist in let c = assoc_var "X2" ist in + let hyp = assoc_var "id" ist in match match_with_conjunction ~strict:strict_in_contravariant_hyp typ with | Some (_,args) -> let i = List.length args in if not binary_mode || i = 2 then let newtyp = valueIn (VConstr (List.fold_right mkArrow args c)) in + let hyp = valueIn (VConstr hyp) in let intros = iter_tac (List.map (fun _ -> <:tactic< intro >>) args) <:tactic< idtac >> in <:tactic< let newtyp := $newtyp in - assert newtyp by ($intros; apply id; split; assumption); - clear id + let hyp := $hyp in + assert newtyp by ($intros; apply hyp; split; assumption); + clear hyp >> else <:tactic> @@ -129,16 +133,19 @@ let is_disj ist = let flatten_contravariant_disj ist = let typ = assoc_var "X1" ist in let c = assoc_var "X2" ist in + let hyp = assoc_var "id" ist in match match_with_disjunction ~strict:strict_in_contravariant_hyp typ with | Some (_,args) -> let i = List.length args in if not binary_mode || i = 2 then + let hyp = valueIn (VConstr hyp) in iter_tac (list_map_i (fun i arg -> let typ = valueIn (VConstr (mkArrow arg c)) in <:tactic< let typ := $typ in - assert typ by (intro; apply id; constructor $i; assumption) - >>) 1 args) <:tactic< clear id >> + let hyp := $hyp in + assert typ by (intro; apply hyp; constructor $i; assumption) + >>) 1 args) <:tactic< let hyp := $hyp in clear hyp >> else <:tactic> | _ -> diff --git a/theories/FSets/FSetDecide.v b/theories/FSets/FSetDecide.v index 06b4e028..f84d8f58 100644 --- a/theories/FSets/FSetDecide.v +++ b/theories/FSets/FSetDecide.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(* $Id: FSetDecide.v 11699 2008-12-18 11:49:08Z letouzey $ *) +(* $Id: FSetDecide.v 13199 2010-06-25 22:36:22Z letouzey $ *) (**************************************************************) (* FSetDecide.v *) @@ -346,6 +346,19 @@ the above form: (** ** Generic Tactics We begin by defining a few generic, useful tactics. *) + (** remove logical hypothesis inter-dependencies (fix #2136). *) + + Ltac no_logical_interdep := + match goal with + | H : ?P |- _ => + match type of P with + | Prop => + match goal with H' : context [ H ] |- _ => clear dependent H' end + | _ => fail + end; no_logical_interdep + | _ => idtac + end. + (** [if t then t1 else t2] executes [t] and, if it does not fail, then [t1] will be applied to all subgoals produced. If [t] fails, then [t2] is executed. *) @@ -405,7 +418,7 @@ the above form: propositions of interest. *) Inductive FSet_elt_Prop : Prop -> Prop := - | eq_Prop : forall (S : Set) (x y : S), + | eq_Prop : forall (S : Type) (x y : S), FSet_elt_Prop (x = y) | eq_elt_prop : forall x y, FSet_elt_Prop (E.eq x y) @@ -660,6 +673,9 @@ the above form: Ltac fsetdec := (** We first unfold any occurrences of [iff]. *) unfold iff in *; + (** We remove dependencies to logical hypothesis. This way, + later "clear" will work nicely (see bug #2136) *) + no_logical_interdep; (** We fold occurrences of [not] because it is better for [intros] to leave us with a goal of [~ P] than a goal of [False]. *) diff --git a/theories/Init/Notations.v b/theories/Init/Notations.v index 3dc6385d..5f18edcd 100644 --- a/theories/Init/Notations.v +++ b/theories/Init/Notations.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Notations.v 11073 2008-06-08 20:24:51Z herbelin $ i*) +(*i $Id: Notations.v 12271 2009-08-11 10:29:45Z herbelin $ i*) (** These are the notations whose level and associativity are imposed by Coq *) @@ -68,13 +68,13 @@ Reserved Notation "{ x }" (at level 0, x at level 99). (** Notations for sigma-types or subsets *) Reserved Notation "{ x | P }" (at level 0, x at level 99). -Reserved Notation "{ x | P & Q }" (at level 0, x at level 99). +Reserved Notation "{ x | P & Q }" (at level 0, x at level 99). Reserved Notation "{ x : A | P }" (at level 0, x at level 99). -Reserved Notation "{ x : A | P & Q }" (at level 0, x at level 99). +Reserved Notation "{ x : A | P & Q }" (at level 0, x at level 99). -Reserved Notation "{ x : A & P }" (at level 0, x at level 99). -Reserved Notation "{ x : A & P & Q }" (at level 0, x at level 99). +Reserved Notation "{ x : A & P }" (at level 0, x at level 99). +Reserved Notation "{ x : A & P & Q }" (at level 0, x at level 99). Delimit Scope type_scope with type. Delimit Scope core_scope with core. diff --git a/theories/Init/Tactics.v b/theories/Init/Tactics.v index 2d7e2159..48b4568d 100644 --- a/theories/Init/Tactics.v +++ b/theories/Init/Tactics.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Tactics.v 11741 2009-01-03 14:34:39Z herbelin $ i*) +(*i $Id: Tactics.v 13198 2010-06-25 22:36:20Z letouzey $ i*) Require Import Notations. Require Import Logic. @@ -174,3 +174,20 @@ Tactic Notation "now" tactic(t) := t; easy. (** A tactic to document or check what is proved at some point of a script *) Ltac now_show c := change c. + +(** Clear an hypothesis and its dependencies *) + +Tactic Notation "clear" "dependent" hyp(h) := + let rec depclear h := + clear h || + match goal with + | H : context [ h ] |- _ => depclear H; depclear h + end || + fail "hypothesis to clear is used in the conclusion (maybe indirectly)" + in depclear h. + +(** Revert an hypothesis and its dependencies : + this is actually generalize dependent... *) + +Tactic Notation "revert" "dependent" hyp(h) := + generalize dependent h. diff --git a/theories/Lists/List.v b/theories/Lists/List.v index a72283d9..c015854e 100644 --- a/theories/Lists/List.v +++ b/theories/Lists/List.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: List.v 10999 2008-05-27 15:55:22Z letouzey $ i*) +(*i $Id: List.v 12446 2009-10-29 21:43:06Z glondu $ i*) Require Import Le Gt Minus Min Bool. @@ -1081,11 +1081,11 @@ Section Map. (** [flat_map] *) - Fixpoint flat_map (f:A -> list B) (l:list A) {struct l} : - list B := + Definition flat_map (f:A -> list B) := + fix flat_map (l:list A) {struct l} : list B := match l with | nil => nil - | cons x t => (f x)++(flat_map f t) + | cons x t => (f x)++(flat_map t) end. Lemma in_flat_map : forall (f:A->list B)(l:list A)(y:B), diff --git a/theories/Numbers/Rational/BigQ/BigQ.v b/theories/Numbers/Rational/BigQ/BigQ.v index 21f2513f..f01cbbc5 100644 --- a/theories/Numbers/Rational/BigQ/BigQ.v +++ b/theories/Numbers/Rational/BigQ/BigQ.v @@ -8,7 +8,7 @@ (* Benjamin Gregoire, Laurent Thery, INRIA, 2007 *) (************************************************************************) -(*i $Id: BigQ.v 11208 2008-07-04 16:57:46Z letouzey $ i*) +(*i $Id: BigQ.v 12509 2009-11-12 15:52:50Z letouzey $ i*) Require Import Field Qfield BigN BigZ QSig QMake. @@ -44,6 +44,11 @@ Delimit Scope bigQ_scope with bigQ. Bind Scope bigQ_scope with bigQ. Bind Scope bigQ_scope with BigQ.t. +(* Allow nice printing of rational numerals, either as (Qz 1234) + or as (Qq 1234 5678) *) +Arguments Scope BigQ.Qz [bigZ_scope]. +Arguments Scope BigQ.Qq [bigZ_scope bigN_scope]. + Infix "+" := BigQ.add : bigQ_scope. Infix "-" := BigQ.sub : bigQ_scope. Notation "- x" := (BigQ.opp x) : bigQ_scope. diff --git a/theories/QArith/QArith_base.v b/theories/QArith/QArith_base.v index 78cf2892..0b6d1cfe 100644 --- a/theories/QArith/QArith_base.v +++ b/theories/QArith/QArith_base.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: QArith_base.v 11301 2008-08-04 19:41:18Z herbelin $ i*) +(*i $Id: QArith_base.v 13215 2010-06-29 09:31:45Z letouzey $ i*) Require Export ZArith. Require Export ZArithRing. @@ -157,16 +157,15 @@ Qed. (** We now consider [Q] seen as a setoid. *) -Definition Q_Setoid : Setoid_Theory Q Qeq. -Proof. - split; red; unfold Qeq in |- *; auto; apply Qeq_trans. -Qed. +Add Relation Q Qeq + reflexivity proved by Qeq_refl + symmetry proved by Qeq_sym + transitivity proved by Qeq_trans +as Q_Setoid. -Add Setoid Q Qeq Q_Setoid as Qsetoid. - -Hint Resolve (Seq_refl Q Qeq Q_Setoid): qarith. -Hint Resolve (Seq_sym Q Qeq Q_Setoid): qarith. -Hint Resolve (Seq_trans Q Qeq Q_Setoid): qarith. +Hint Resolve Qeq_refl : qarith. +Hint Resolve Qeq_sym : qarith. +Hint Resolve Qeq_trans : qarith. Theorem Qnot_eq_sym : forall x y, ~x == y -> ~y == x. Proof. @@ -633,8 +632,15 @@ Proof. unfold Qle, Qlt, Qeq; intros; apply Zle_lt_or_eq; auto. Qed. +(** These hints were meant to be added to the qarith database, + but a typo prevented that. This will be fixed in 8.3. + Concerning 8.2, for maximal compatibility , we + leave them in a separate database, in order to preserve + the strength of both [auto with qarith] and [auto with *]. + (see bug #2346). *) + Hint Resolve Qle_not_lt Qlt_not_le Qnot_le_lt Qnot_lt_le - Qlt_le_weak Qlt_not_eq Qle_antisym Qle_refl: qartih. + Qlt_le_weak Qlt_not_eq Qle_antisym Qle_refl: qarith_extra. (** Some decidability results about orders. *) diff --git a/theories/ZArith/Zbool.v b/theories/ZArith/Zbool.v index 71befa4a..34771897 100644 --- a/theories/ZArith/Zbool.v +++ b/theories/ZArith/Zbool.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: Zbool.v 11208 2008-07-04 16:57:46Z letouzey $ *) +(* $Id: Zbool.v 12271 2009-08-11 10:29:45Z herbelin $ *) Require Import BinInt. Require Import Zeven. @@ -18,9 +18,9 @@ Require Import Sumbool. Unset Boxed Definitions. Open Local Scope Z_scope. -(** * Boolean operations from decidabilty of order *) +(** * Boolean operations from decidability of order *) (** The decidability of equality and order relations over - type [Z] give some boolean functions with the adequate specification. *) + type [Z] gives some boolean functions with the adequate specification. *) Definition Z_lt_ge_bool (x y:Z) := bool_of_sumbool (Z_lt_ge_dec x y). Definition Z_ge_lt_bool (x y:Z) := bool_of_sumbool (Z_ge_lt_dec x y). diff --git a/theories/ZArith/Zorder.v b/theories/ZArith/Zorder.v index 425aa83b..73808f92 100644 --- a/theories/ZArith/Zorder.v +++ b/theories/ZArith/Zorder.v @@ -5,7 +5,7 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Zorder.v 10291 2007-11-06 02:18:53Z letouzey $ i*) +(*i $Id: Zorder.v 12888 2010-03-28 19:35:03Z herbelin $ i*) (** Binary Integers (Pierre Crégut (CNET, Lannion, France) *) @@ -1025,3 +1025,5 @@ Qed. (** For compatibility *) Notation Zlt_O_minus_lt := Zlt_0_minus_lt (only parsing). +Notation Zle_gt_succ := Zlt_gt_succ (only parsing). +Notation Zle_succ_gt := Zlt_succ_gt (only parsing). diff --git a/tools/coq_makefile.ml4 b/tools/coq_makefile.ml4 index eb3a19fa..3ca1e7d3 100644 --- a/tools/coq_makefile.ml4 +++ b/tools/coq_makefile.ml4 @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: coq_makefile.ml4 12176 2009-06-09 09:44:40Z notin $ *) +(* $Id: coq_makefile.ml4 12470 2009-11-05 15:50:20Z notin $ *) (* créer un Makefile pour un développement Coq automatiquement *) @@ -163,7 +163,7 @@ let install_include_by_root var files (_,inc_r) = let ldir = List.assoc "." (List.map (fun (p,l,_) -> (p,l)) inc_r) in let pdir = physical_dir_of_logical_dir ldir in printf "\t(for i in $(%s); do \\\n" var; - printf "\t install -D $$i $(COQLIB)/user-contrib/%s/$$i; \\\n" pdir; + printf "\t install -d `dirname $(COQLIB)/user-contrib/%s/$$i`; \\\n\t install $$i $(COQLIB)/user-contrib/%s/$$i; \\\n" pdir pdir; printf "\t done)\n" with Not_found -> (* Files in the scope of a -R option (assuming they are disjoint) *) @@ -172,12 +172,12 @@ let install_include_by_root var files (_,inc_r) = begin let pdir' = physical_dir_of_logical_dir ldir in printf "\t(cd %s; for i in $(%s%d); do \\\n" pdir var i; - printf "\t install -D $$i $(COQLIB)/user-contrib/%s/$$i; \\\n" pdir'; + printf "\t install -d `dirname $(COQLIB)/user-contrib/%s/$$i`; \\\n\t install $$i $(COQLIB)/user-contrib/%s/$$i; \\\n" pdir' pdir'; printf "\t done)\n" end) inc_r; (* Files not in the scope of a -R option *) printf "\t(for i in $(%s0); do \\\n" var; - printf "\t install -D $$i $(COQLIB)/user-contrib/$(INSTALLDEFAULTROOT)/$$i; \\\n"; + printf "\t install -d `dirname $(COQLIB)/user-contrib/$(INSTALLDEFAULTROOT)/$$i`; \\\n\t install $$i $(COQLIB)/user-contrib/$(INSTALLDEFAULTROOT)/$$i; \\\n"; printf "\t done)\n" let install (vfiles,mlfiles,_,sds) inc = diff --git a/tools/coqdep.ml b/tools/coqdep.ml index 4febe9d1..91a7e6d0 100644 --- a/tools/coqdep.ml +++ b/tools/coqdep.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: coqdep.ml 11749 2009-01-05 14:01:04Z notin $ *) +(* $Id: coqdep.ml 12916 2010-04-10 15:18:17Z herbelin $ *) open Printf open Coqdep_lexer @@ -60,7 +60,9 @@ let safe_hash_add clq q (k,v) = (k1,l1)::cltl when k=k1 -> (k1,v::l1)::cltl | cl::cltl -> cl::add_clash cltl | [] -> [(k,[v;v2])] in - clq := add_clash !clq + clq := add_clash !clq; + (* overwrite previous bindings, as coqc does *) + Hashtbl.add q k v with Not_found -> Hashtbl.add q k v (* Files found in the loadpaths *) @@ -167,6 +169,37 @@ let cut_prefix p s = let ls = String.length s in if ls >= lp && String.sub s 0 lp = p then String.sub s lp (ls - lp) else s +(* 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 = ' ' or c = '#' or c = ':' (* separators and comments *) + or c = '%' (* pattern *) + or c = '?' or c = '[' or c = ']' or c = '*' (* expansion in filenames *) + or 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' + let canonize f = let f' = absolute_dir (Filename.dirname f) // Filename.basename f in match List.filter (fun (_,full) -> f' = full) !vAccu with @@ -423,6 +456,11 @@ let add_coqlib_known phys_dir log_dir f = Hashtbl.add coqlibKnown [basename] (); Hashtbl.add coqlibKnown name () +let rec suffixes = function + | [] -> assert false + | [name] -> [[name]] + | dir::suffix as l -> l::suffixes suffix + let add_known phys_dir log_dir f = if (Filename.check_suffix f ".ml" || Filename.check_suffix f ".mli" || Filename.check_suffix f ".ml4") then let basename = make_ml_module_name f in @@ -431,7 +469,7 @@ let add_known phys_dir log_dir f = let basename = Filename.chop_suffix f ".v" in let name = log_dir@[basename] in let file = phys_dir//basename in - let paths = [name;[basename]] in + let paths = suffixes name in List.iter (fun n -> safe_hash_add clash_v vKnown (n,file)) paths diff --git a/tools/coqdoc/pretty.mll b/tools/coqdoc/pretty.mll index c4a1a76f..b29e0734 100644 --- a/tools/coqdoc/pretty.mll +++ b/tools/coqdoc/pretty.mll @@ -7,7 +7,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: pretty.mll 12187 2009-06-13 19:36:59Z msozeau $ i*) +(*i $Id: pretty.mll 12908 2010-04-09 08:54:04Z herbelin $ i*) (*s Utility functions for the scanners *) @@ -126,7 +126,7 @@ Str.regexp "[ \t]*(\\*\\*[ \t]+printing[ \t]+\\([^ \t]+\\)" let printing_token_re = Str.regexp - "[ \t]*\\(\\(%\\([^%]*\\)%\\)\\|\\(\\$[^$]*\\$\\)\\)?[ \t]*\\(#\\(\\([^#]\\|&#\\)*\\)#\\)?" + "[ \t]*\\(\\(%\\([^%]*\\)%\\)\\|\\(\\$[^$]*\\$\\)\\)?[ \t]*\\(#\\(\\(&#\\|[^#]\\)*\\)#\\)?" let add_printing_token toks pps = try @@ -731,6 +731,9 @@ and body = parse | token_no_brackets { let s = lexeme lexbuf in symbol lexbuf s; body lexbuf } + | ".." + { Output.char '.'; Output.char '.'; + body lexbuf } | _ { let c = lexeme_char lexbuf 0 in Output.char c; body lexbuf } diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml index 6a75b99c..821a73f7 100644 --- a/toplevel/metasyntax.ml +++ b/toplevel/metasyntax.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: metasyntax.ml 11786 2009-01-14 13:07:34Z herbelin $ *) +(* $Id: metasyntax.ml 12882 2010-03-23 22:34:38Z herbelin $ *) open Pp open Util @@ -266,16 +266,18 @@ let split_notation_string str = (* Interpret notations with a recursive component *) -let rec find_pattern xl = function - | Break n as x :: l, Break n' :: l' when n=n' -> - find_pattern (x::xl) (l,l') +let out_nt = function NonTerminal x -> x | _ -> assert false + +let rec find_pattern nt xl = function + | Break n as x :: l, Break n' :: l' when n=n' -> + find_pattern nt (x::xl) (l,l') | Terminal s as x :: l, Terminal s' :: l' when s = s' -> - find_pattern (x::xl) (l,l') - | [NonTerminal x], NonTerminal x' :: l' -> - (x,x',xl),l' - | [NonTerminal _], Terminal s :: _ | Terminal s :: _, _ -> + find_pattern nt (x::xl) (l,l') + | [], NonTerminal x' :: l' -> + (out_nt nt,x',List.rev xl),l' + | [], Terminal s :: _ | Terminal s :: _, _ -> error ("The token "^s^" occurs on one side of \"..\" but not on the other side.") - | [NonTerminal _], Break s :: _ | Break s :: _, _ -> + | [], Break s :: _ | Break s :: _, _ -> error ("A break occurs on one side of \"..\" but not on the other side.") | ((SProdList _ | NonTerminal _) :: _ | []), _ -> error ("The special symbol \"..\" must occur in a configuration of the form\n\"x symbs .. symbs y\".") @@ -283,7 +285,8 @@ let rec find_pattern xl = function let rec interp_list_parser hd = function | [] -> [], [], List.rev hd | NonTerminal id :: tl when id = ldots_var -> - let ((x,y,sl),tl') = find_pattern [] (hd,tl) in + let hd = List.rev hd in + let ((x,y,sl),tl') = find_pattern (List.hd hd) [] (List.tl hd,tl) in let yl,xl,tl'' = interp_list_parser [] tl' in (* We remember each pair of variable denoting a recursive part to *) (* remove the second copy of it afterwards *) @@ -299,6 +302,7 @@ let rec interp_list_parser hd = function yl, xl, List.rev_append hd tl' | SProdList _ :: _ -> anomaly "Unexpected SProdList in interp_list_parser" + (* Find non-terminal tokens of notation *) let unquote_notation_token s = diff --git a/toplevel/mltop.ml4 b/toplevel/mltop.ml4 index 176f336b..b54700d3 100644 --- a/toplevel/mltop.ml4 +++ b/toplevel/mltop.ml4 @@ -11,7 +11,7 @@ * camlp4deps will not work for this file unless Makefile system enhanced. *) -(* $Id: mltop.ml4 11801 2009-01-18 20:11:41Z herbelin $ *) +(* $Id: mltop.ml4 12341 2009-09-17 16:03:19Z glondu $ *) open Util open Pp @@ -109,7 +109,7 @@ let dir_ml_load s = * in this file, the Makefile dependency logic needs to be updated. *) let warn = Flags.is_verbose() in - let _,gname = where_in_path ~warn !coq_mlpath_copy s in + let _,gname = find_file_in_path ~warn !coq_mlpath_copy s in try Dynlink.loadfile gname; with | Dynlink.Error a -> diff --git a/toplevel/toplevel.ml b/toplevel/toplevel.ml index a1acd1d6..9d64f983 100644 --- a/toplevel/toplevel.ml +++ b/toplevel/toplevel.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: toplevel.ml 11784 2009-01-14 11:36:32Z herbelin $ *) +(* $Id: toplevel.ml 12891 2010-03-30 11:40:02Z herbelin $ *) open Pp open Util @@ -163,11 +163,10 @@ let print_location_in_file s inlibrary fname loc = try let (line, bol) = line_of_pos 1 0 0 in close_in ic; - hov 0 - (errstrm ++ str"File " ++ str ("\""^fname^"\"") ++ str"," ++ spc() ++ - hov 0 (str"line " ++ int line ++ str"," ++ spc() ++ - str"characters " ++ - Cerrors.print_loc (make_loc (bp-bol,ep-bol))) ++ str":") ++ + hov 0 (* No line break so as to follow emacs error message format *) + (errstrm ++ str"File " ++ str ("\""^fname^"\"") ++ + str", line " ++ int line ++ str", characters " ++ + Cerrors.print_loc (make_loc (bp-bol,ep-bol))) ++ str":" ++ fnl () with e -> (close_in ic; @@ -316,7 +315,7 @@ let parse_to_dot = let rec discard_to_dot () = try Gram.Entry.parse parse_to_dot top_buffer.tokens - with Stdpp.Exc_located(_,Token.Error _) -> + with Stdpp.Exc_located(_,(Token.Error _|Lexer.Error _)) -> discard_to_dot() diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 6a0acb52..385afbec 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: vernacentries.ml 12187 2009-06-13 19:36:59Z msozeau $ i*) +(*i $Id: vernacentries.ml 12343 2009-09-17 17:02:03Z glondu $ i*) (* Concrete syntax of the mathematical vernacular MV V2.6 *) @@ -234,12 +234,8 @@ let dump_universes s = (* "Locate" commands *) let locate_file f = - try - let _,file = System.where_in_path ~warn:false (Library.get_load_paths ()) f in - msgnl (str file) - with Not_found -> - msgnl (hov 0 (str"Can't find file" ++ spc () ++ str f ++ spc () ++ - str"on loadpath")) + let _,file = System.find_file_in_path ~warn:false (Library.get_load_paths ()) f in + msgnl (str file) let msg_found_library = function | Library.LibLoaded, fulldir, file -> -- cgit v1.2.3