summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--.depend86
-rw-r--r--CHANGES43
-rw-r--r--INSTALL.ide2
-rw-r--r--INSTALL.win63
-rw-r--r--Makefile64
-rw-r--r--README.win27
-rw-r--r--config/Makefile.template17
-rw-r--r--config/coq_config.mli3
-rwxr-xr-xconfigure469
-rw-r--r--contrib/extraction/common.ml26
-rw-r--r--contrib/extraction/extraction.ml98
-rw-r--r--contrib/extraction/haskell.ml87
-rw-r--r--contrib/extraction/haskell.mli4
-rw-r--r--contrib/extraction/miniml.mli14
-rw-r--r--contrib/extraction/mlutil.ml73
-rw-r--r--contrib/extraction/modutil.ml18
-rw-r--r--contrib/extraction/modutil.mli4
-rw-r--r--contrib/extraction/ocaml.ml118
-rw-r--r--contrib/extraction/ocaml.mli8
-rw-r--r--contrib/extraction/scheme.ml78
-rw-r--r--contrib/extraction/scheme.mli4
-rw-r--r--contrib/extraction/table.ml18
-rw-r--r--contrib/extraction/table.mli8
-rw-r--r--contrib/funind/tacinv.ml423
-rw-r--r--contrib/funind/tacinvutils.ml53
-rw-r--r--contrib/interface/xlate.ml14
-rwxr-xr-xcontrib/omega/omega.ml10
-rw-r--r--dev/ocamldebug-v7.template6
-rw-r--r--dev/perf-analysis51
-rw-r--r--ide/coq.icobin0 -> 96774 bytes
-rw-r--r--ide/coq.ml6
-rwxr-xr-xide/coq2.icobin0 -> 1526 bytes
-rw-r--r--ide/coqide.ml448
-rw-r--r--ide/ideutils.ml22
-rw-r--r--ide/ideutils.mli5
-rw-r--r--ide/undo.ml4
-rw-r--r--ide/undo_lablgtk_ge26.mli35
-rw-r--r--ide/undo_lablgtk_lt26.mli (renamed from ide/undo.mli)2
-rw-r--r--interp/constrextern.ml49
-rw-r--r--interp/constrintern.ml8
-rw-r--r--interp/syntax_def.ml11
-rw-r--r--kernel/declarations.ml6
-rw-r--r--kernel/declarations.mli3
-rw-r--r--kernel/entries.ml3
-rw-r--r--kernel/entries.mli3
-rw-r--r--kernel/indtypes.ml34
-rw-r--r--kernel/safe_typing.ml12
-rw-r--r--kernel/safe_typing.mli4
-rw-r--r--kernel/subtyping.ml30
-rw-r--r--kernel/univ.ml10
-rw-r--r--lib/compat.ml42
-rw-r--r--lib/gmapl.ml4
-rw-r--r--lib/system.ml32
-rw-r--r--lib/system.mli6
-rw-r--r--library/declare.ml3
-rw-r--r--library/declaremods.ml12
-rw-r--r--library/global.ml4
-rw-r--r--library/global.mli4
-rw-r--r--library/lib.ml5
-rw-r--r--library/library.ml55
-rwxr-xr-xlibrary/nametab.ml6
-rwxr-xr-xlibrary/nametab.mli4
-rw-r--r--parsing/egrammar.ml9
-rw-r--r--parsing/egrammar.mli5
-rw-r--r--parsing/g_constrnew.ml46
-rw-r--r--parsing/g_ltacnew.ml420
-rw-r--r--parsing/g_tactic.ml46
-rw-r--r--parsing/g_tacticnew.ml46
-rw-r--r--parsing/pcoq.ml45
-rw-r--r--parsing/pcoq.mli5
-rw-r--r--parsing/pptactic.ml10
-rw-r--r--parsing/pptactic.mli4
-rw-r--r--parsing/prettyp.ml10
-rw-r--r--parsing/q_coqast.ml44
-rw-r--r--pretyping/cases.ml7
-rw-r--r--pretyping/coercion.ml6
-rw-r--r--pretyping/detyping.ml10
-rw-r--r--pretyping/evarconv.ml27
-rw-r--r--pretyping/pretyping.ml10
-rwxr-xr-xpretyping/recordops.ml10
-rwxr-xr-xpretyping/recordops.mli9
-rw-r--r--pretyping/tacred.ml5
-rw-r--r--proofs/logic.ml26
-rw-r--r--proofs/refiner.ml16
-rw-r--r--proofs/tacexpr.ml6
-rw-r--r--scripts/coqmktop.ml4
-rw-r--r--tactics/auto.ml10
-rw-r--r--tactics/inv.ml17
-rw-r--r--tactics/tacinterp.ml37
-rw-r--r--tactics/tactics.ml14
-rwxr-xr-xtest-suite/check4
-rw-r--r--test-suite/modules/modul.v2
-rw-r--r--test-suite/success/TestRefine.v (renamed from test-suite/tactics/TestRefine.v)17
-rw-r--r--theories/Reals/PartSum.v7
-rw-r--r--theories/Reals/RIneq.v4
-rw-r--r--theories/Reals/RiemannInt.v16
-rw-r--r--theories/ZArith/Zorder.v14
-rw-r--r--theories7/Reals/PartSum.v5
-rw-r--r--theories7/Reals/RiemannInt.v10
-rw-r--r--tools/coqdoc/coqdoc.sty4
-rw-r--r--toplevel/command.ml6
-rw-r--r--toplevel/coqinit.ml8
-rw-r--r--toplevel/coqtop.ml5
-rw-r--r--toplevel/discharge.ml6
-rw-r--r--toplevel/metasyntax.ml89
-rw-r--r--toplevel/record.ml5
-rw-r--r--translate/ppconstrnew.ml4
-rw-r--r--translate/pptacticnew.ml8
-rw-r--r--translate/ppvernacnew.ml11
109 files changed, 1602 insertions, 1248 deletions
diff --git a/.depend b/.depend
index d158d8dc..26002dd0 100644
--- a/.depend
+++ b/.depend
@@ -107,8 +107,8 @@ parsing/coqast.cmi: lib/util.cmi kernel/names.cmi library/libnames.cmi \
lib/dyn.cmi
parsing/egrammar.cmi: toplevel/vernacexpr.cmo lib/util.cmi \
interp/topconstr.cmi proofs/tacexpr.cmo pretyping/rawterm.cmi \
- interp/ppextend.cmi kernel/names.cmi interp/genarg.cmi parsing/extend.cmi \
- parsing/coqast.cmi parsing/ast.cmi
+ parsing/pptactic.cmi interp/ppextend.cmi kernel/names.cmi \
+ interp/genarg.cmi parsing/extend.cmi parsing/coqast.cmi parsing/ast.cmi
parsing/esyntax.cmi: interp/topconstr.cmi interp/symbols.cmi \
interp/ppextend.cmi lib/pp.cmi parsing/extend.cmi parsing/coqast.cmi \
parsing/ast.cmi
@@ -508,10 +508,10 @@ ide/find_phrase.cmo: ide/ideutils.cmi
ide/find_phrase.cmx: ide/ideutils.cmx
ide/highlight.cmo: ide/ideutils.cmi
ide/highlight.cmx: ide/ideutils.cmx
-ide/ideutils.cmo: ide/utf8_convert.cmo ide/preferences.cmi lib/pp_control.cmi \
- lib/options.cmi config/coq_config.cmi ide/ideutils.cmi
-ide/ideutils.cmx: ide/utf8_convert.cmx ide/preferences.cmx lib/pp_control.cmx \
- lib/options.cmx config/coq_config.cmx ide/ideutils.cmi
+ide/ideutils.cmo: ide/utf8_convert.cmo lib/system.cmi ide/preferences.cmi \
+ lib/pp_control.cmi lib/options.cmi config/coq_config.cmi ide/ideutils.cmi
+ide/ideutils.cmx: ide/utf8_convert.cmx lib/system.cmx ide/preferences.cmx \
+ lib/pp_control.cmx lib/options.cmx config/coq_config.cmx ide/ideutils.cmi
ide/preferences.cmo: lib/util.cmi lib/system.cmi ide/utils/configwin.cmi \
ide/config_lexer.cmo ide/preferences.cmi
ide/preferences.cmx: lib/util.cmx lib/system.cmx ide/utils/configwin.cmx \
@@ -703,11 +703,11 @@ kernel/sign.cmo: lib/util.cmi kernel/term.cmi kernel/names.cmi \
kernel/sign.cmx: lib/util.cmx kernel/term.cmx kernel/names.cmx \
kernel/sign.cmi
kernel/subtyping.cmo: lib/util.cmi kernel/univ.cmi kernel/term.cmi \
- kernel/reduction.cmi kernel/names.cmi kernel/modops.cmi \
+ kernel/reduction.cmi lib/pp.cmi kernel/names.cmi kernel/modops.cmi \
kernel/inductive.cmi kernel/environ.cmi kernel/declarations.cmi \
kernel/subtyping.cmi
kernel/subtyping.cmx: lib/util.cmx kernel/univ.cmx kernel/term.cmx \
- kernel/reduction.cmx kernel/names.cmx kernel/modops.cmx \
+ kernel/reduction.cmx lib/pp.cmx kernel/names.cmx kernel/modops.cmx \
kernel/inductive.cmx kernel/environ.cmx kernel/declarations.cmx \
kernel/subtyping.cmi
kernel/term.cmo: lib/util.cmi kernel/univ.cmi lib/pp.cmi kernel/names.cmi \
@@ -904,14 +904,14 @@ parsing/coqast.cmx: lib/util.cmx kernel/names.cmx library/libnames.cmx \
lib/hashcons.cmx lib/dyn.cmx parsing/coqast.cmi
parsing/egrammar.cmo: toplevel/vernacexpr.cmo lib/util.cmi \
interp/topconstr.cmi proofs/tacexpr.cmo library/summary.cmi \
- interp/ppextend.cmi lib/pp.cmi parsing/pcoq.cmi lib/options.cmi \
- kernel/names.cmi library/nameops.cmi library/libnames.cmi \
+ parsing/pptactic.cmi interp/ppextend.cmi lib/pp.cmi parsing/pcoq.cmi \
+ lib/options.cmi kernel/names.cmi library/nameops.cmi library/libnames.cmi \
parsing/lexer.cmi interp/genarg.cmi parsing/extend.cmi lib/bignat.cmi \
parsing/ast.cmi parsing/egrammar.cmi
parsing/egrammar.cmx: toplevel/vernacexpr.cmx lib/util.cmx \
interp/topconstr.cmx proofs/tacexpr.cmx library/summary.cmx \
- interp/ppextend.cmx lib/pp.cmx parsing/pcoq.cmx lib/options.cmx \
- kernel/names.cmx library/nameops.cmx library/libnames.cmx \
+ parsing/pptactic.cmx interp/ppextend.cmx lib/pp.cmx parsing/pcoq.cmx \
+ lib/options.cmx kernel/names.cmx library/nameops.cmx library/libnames.cmx \
parsing/lexer.cmx interp/genarg.cmx parsing/extend.cmx lib/bignat.cmx \
parsing/ast.cmx parsing/egrammar.cmi
parsing/esyntax.cmo: lib/util.cmi interp/topconstr.cmi interp/symbols.cmi \
@@ -1488,18 +1488,20 @@ proofs/logic.cmo: lib/util.cmi pretyping/typing.cmi kernel/typeops.cmi \
proofs/proof_type.cmi proofs/proof_trees.cmi parsing/printer.cmi \
pretyping/pretype_errors.cmi lib/pp.cmi lib/options.cmi \
library/nametab.cmi kernel/names.cmi library/nameops.cmi \
- pretyping/inductiveops.cmi kernel/inductive.cmi library/global.cmi \
- pretyping/evd.cmi pretyping/evarutil.cmi kernel/environ.cmi \
- parsing/coqast.cmi interp/constrextern.cmi proofs/logic.cmi
+ pretyping/inductiveops.cmi kernel/inductive.cmi kernel/indtypes.cmi \
+ library/global.cmi pretyping/evd.cmi pretyping/evarutil.cmi \
+ kernel/environ.cmi parsing/coqast.cmi interp/constrextern.cmi \
+ proofs/logic.cmi
proofs/logic.cmx: lib/util.cmx pretyping/typing.cmx kernel/typeops.cmx \
kernel/type_errors.cmx pretyping/termops.cmx kernel/term.cmx \
kernel/sign.cmx pretyping/retyping.cmx pretyping/reductionops.cmx \
proofs/proof_type.cmx proofs/proof_trees.cmx parsing/printer.cmx \
pretyping/pretype_errors.cmx lib/pp.cmx lib/options.cmx \
library/nametab.cmx kernel/names.cmx library/nameops.cmx \
- pretyping/inductiveops.cmx kernel/inductive.cmx library/global.cmx \
- pretyping/evd.cmx pretyping/evarutil.cmx kernel/environ.cmx \
- parsing/coqast.cmx interp/constrextern.cmx proofs/logic.cmi
+ pretyping/inductiveops.cmx kernel/inductive.cmx kernel/indtypes.cmx \
+ library/global.cmx pretyping/evd.cmx pretyping/evarutil.cmx \
+ kernel/environ.cmx parsing/coqast.cmx interp/constrextern.cmx \
+ proofs/logic.cmi
proofs/pfedit.cmo: lib/util.cmi pretyping/typing.cmi kernel/term.cmi \
proofs/tacmach.cmi proofs/tacexpr.cmo kernel/sign.cmi \
kernel/safe_typing.cmi proofs/refiner.cmi proofs/proof_type.cmi \
@@ -1597,9 +1599,10 @@ tactics/auto.cmo: toplevel/vernacexpr.cmo lib/util.cmi pretyping/typing.cmi \
pretyping/matching.cmi proofs/logic.cmi library/library.cmi \
library/libobject.cmi library/libnames.cmi library/lib.cmi \
kernel/inductive.cmi tactics/hipattern.cmi tactics/hiddentac.cmi \
- library/global.cmi pretyping/evd.cmi proofs/evar_refiner.cmi \
- tactics/dhyp.cmi kernel/declarations.cmi interp/constrintern.cmi \
- proofs/clenv.cmi tactics/btermdn.cmi tactics/auto.cmi
+ library/global.cmi interp/genarg.cmi pretyping/evd.cmi \
+ proofs/evar_refiner.cmi tactics/dhyp.cmi kernel/declarations.cmi \
+ interp/constrintern.cmi proofs/clenv.cmi tactics/btermdn.cmi \
+ tactics/auto.cmi
tactics/auto.cmx: toplevel/vernacexpr.cmx lib/util.cmx pretyping/typing.cmx \
pretyping/termops.cmx kernel/term.cmx tactics/tactics.cmx \
tactics/tacticals.cmx pretyping/tacred.cmx proofs/tacmach.cmx \
@@ -1611,9 +1614,10 @@ tactics/auto.cmx: toplevel/vernacexpr.cmx lib/util.cmx pretyping/typing.cmx \
pretyping/matching.cmx proofs/logic.cmx library/library.cmx \
library/libobject.cmx library/libnames.cmx library/lib.cmx \
kernel/inductive.cmx tactics/hipattern.cmx tactics/hiddentac.cmx \
- library/global.cmx pretyping/evd.cmx proofs/evar_refiner.cmx \
- tactics/dhyp.cmx kernel/declarations.cmx interp/constrintern.cmx \
- proofs/clenv.cmx tactics/btermdn.cmx tactics/auto.cmi
+ library/global.cmx interp/genarg.cmx pretyping/evd.cmx \
+ proofs/evar_refiner.cmx tactics/dhyp.cmx kernel/declarations.cmx \
+ interp/constrintern.cmx proofs/clenv.cmx tactics/btermdn.cmx \
+ tactics/auto.cmi
tactics/autorewrite.cmo: toplevel/vernacinterp.cmi lib/util.cmi \
kernel/term.cmi tactics/tactics.cmi tactics/tacticals.cmi \
tactics/tacinterp.cmi proofs/tacexpr.cmo library/summary.cmi \
@@ -1924,10 +1928,11 @@ tactics/tactics.cmo: lib/util.cmi pretyping/termops.cmi kernel/term.cmi \
library/nametab.cmi kernel/names.cmi library/nameops.cmi proofs/logic.cmi \
library/libnames.cmi pretyping/inductiveops.cmi kernel/inductive.cmi \
pretyping/indrec.cmi tactics/hipattern.cmi library/global.cmi \
- interp/genarg.cmi pretyping/evd.cmi proofs/evar_refiner.cmi \
- kernel/environ.cmi kernel/entries.cmi library/declare.cmi \
- kernel/declarations.cmi library/decl_kinds.cmo interp/coqlib.cmi \
- interp/constrintern.cmi proofs/clenv.cmi tactics/tactics.cmi
+ interp/genarg.cmi pretyping/evd.cmi pretyping/evarutil.cmi \
+ proofs/evar_refiner.cmi kernel/environ.cmi kernel/entries.cmi \
+ library/declare.cmi kernel/declarations.cmi library/decl_kinds.cmo \
+ interp/coqlib.cmi interp/constrintern.cmi proofs/clenv.cmi \
+ tactics/tactics.cmi
tactics/tactics.cmx: lib/util.cmx pretyping/termops.cmx kernel/term.cmx \
tactics/tacticals.cmx pretyping/tacred.cmx proofs/tacmach.cmx \
proofs/tacexpr.cmx kernel/sign.cmx proofs/refiner.cmx \
@@ -1936,10 +1941,11 @@ tactics/tactics.cmx: lib/util.cmx pretyping/termops.cmx kernel/term.cmx \
library/nametab.cmx kernel/names.cmx library/nameops.cmx proofs/logic.cmx \
library/libnames.cmx pretyping/inductiveops.cmx kernel/inductive.cmx \
pretyping/indrec.cmx tactics/hipattern.cmx library/global.cmx \
- interp/genarg.cmx pretyping/evd.cmx proofs/evar_refiner.cmx \
- kernel/environ.cmx kernel/entries.cmx library/declare.cmx \
- kernel/declarations.cmx library/decl_kinds.cmx interp/coqlib.cmx \
- interp/constrintern.cmx proofs/clenv.cmx tactics/tactics.cmi
+ interp/genarg.cmx pretyping/evd.cmx pretyping/evarutil.cmx \
+ proofs/evar_refiner.cmx kernel/environ.cmx kernel/entries.cmx \
+ library/declare.cmx kernel/declarations.cmx library/decl_kinds.cmx \
+ interp/coqlib.cmx interp/constrintern.cmx proofs/clenv.cmx \
+ tactics/tactics.cmi
tactics/tauto.cmo: lib/util.cmi interp/topconstr.cmi tactics/tactics.cmi \
tactics/tacticals.cmi tactics/tacinterp.cmi proofs/tacexpr.cmo \
proofs/refiner.cmi pretyping/rawterm.cmi proofs/proof_type.cmi \
@@ -2248,7 +2254,7 @@ toplevel/vernacinterp.cmx: toplevel/vernacexpr.cmx lib/util.cmx \
lib/options.cmx kernel/names.cmx library/libnames.cmx toplevel/himsg.cmx \
parsing/extend.cmx parsing/coqast.cmx parsing/ast.cmx \
toplevel/vernacinterp.cmi
-translate/ppconstrnew.cmo: lib/util.cmi interp/topconstr.cmi \
+translate/ppconstrnew.cmo: lib/util.cmi kernel/univ.cmi interp/topconstr.cmi \
pretyping/termops.cmi kernel/term.cmi interp/syntax_def.cmi \
interp/symbols.cmi pretyping/retyping.cmi pretyping/rawterm.cmi \
pretyping/pretyping.cmi interp/ppextend.cmi lib/pp.cmi \
@@ -2257,7 +2263,7 @@ translate/ppconstrnew.cmo: lib/util.cmi interp/topconstr.cmi \
library/global.cmi interp/genarg.cmi pretyping/evd.cmi parsing/coqast.cmi \
interp/constrintern.cmi interp/constrextern.cmi lib/bignat.cmi \
parsing/ast.cmi translate/ppconstrnew.cmi
-translate/ppconstrnew.cmx: lib/util.cmx interp/topconstr.cmx \
+translate/ppconstrnew.cmx: lib/util.cmx kernel/univ.cmx interp/topconstr.cmx \
pretyping/termops.cmx kernel/term.cmx interp/syntax_def.cmx \
interp/symbols.cmx pretyping/retyping.cmx pretyping/rawterm.cmx \
pretyping/pretyping.cmx interp/ppextend.cmx lib/pp.cmx \
@@ -2512,18 +2518,18 @@ contrib/extraction/extract_env.cmx: lib/util.cmx kernel/term.cmx \
contrib/extraction/extract_env.cmi
contrib/extraction/extraction.cmo: lib/util.cmi pretyping/termops.cmi \
kernel/term.cmi contrib/extraction/table.cmi library/summary.cmi \
- kernel/sign.cmi pretyping/retyping.cmi pretyping/reductionops.cmi \
- kernel/reduction.cmi pretyping/recordops.cmi library/nametab.cmi \
- kernel/names.cmi library/nameops.cmi contrib/extraction/mlutil.cmi \
+ pretyping/retyping.cmi pretyping/reductionops.cmi kernel/reduction.cmi \
+ pretyping/recordops.cmi library/nametab.cmi kernel/names.cmi \
+ library/nameops.cmi contrib/extraction/mlutil.cmi \
contrib/extraction/miniml.cmi library/libnames.cmi \
pretyping/inductiveops.cmi kernel/inductive.cmi pretyping/evd.cmi \
kernel/environ.cmi kernel/declarations.cmi \
contrib/extraction/extraction.cmi
contrib/extraction/extraction.cmx: lib/util.cmx pretyping/termops.cmx \
kernel/term.cmx contrib/extraction/table.cmx library/summary.cmx \
- kernel/sign.cmx pretyping/retyping.cmx pretyping/reductionops.cmx \
- kernel/reduction.cmx pretyping/recordops.cmx library/nametab.cmx \
- kernel/names.cmx library/nameops.cmx contrib/extraction/mlutil.cmx \
+ pretyping/retyping.cmx pretyping/reductionops.cmx kernel/reduction.cmx \
+ pretyping/recordops.cmx library/nametab.cmx kernel/names.cmx \
+ library/nameops.cmx contrib/extraction/mlutil.cmx \
contrib/extraction/miniml.cmi library/libnames.cmx \
pretyping/inductiveops.cmx kernel/inductive.cmx pretyping/evd.cmx \
kernel/environ.cmx kernel/declarations.cmx \
diff --git a/CHANGES b/CHANGES
index 7b0a41d0..7c7f5dc7 100644
--- a/CHANGES
+++ b/CHANGES
@@ -1,3 +1,46 @@
+Changes from V8.0pl2 to V8.0pl3
+===============================
+
+Tactics
+
+- The search depth argument of auto can be parameterised in the
+ Ltac language
+- Added entry constr_may_eval for tactic extensions (new syntax)
+
+Compilation
+
+- Coq sources made compatible with ocaml 3.09.0 and lablgtk 2.6.0.
+
+Standard library
+
+- A couple of lemmas of ZArith were renamed. This concerns names
+ containing O (the letter), which is replaced by 0 (the number).
+
+Bug fixes
+
+- Fixes a serious bug in CoqIde. The windows port should be able
+ to load large libraries (such as Reals) without producing the
+ "bad file descriptor" error.
+- Scope of Ltac variables: global Ltac macros no longer hide goal
+ hypotheses
+- Many fixes concerning extraction:
+ * fewer useless eta-expansions
+ * for Ocaml: extraction of records should be ok now. Problem with
+ type t = M.t in modules fixed.
+ * in Haskell: improved use of unsafeCoerce, fixed Extract Constant,
+ function types are now printed.
+ * important revision of the Scheme extraction:
+ see http://www.pps.jussieu.fr/~letouzey/scheme
+- Fixes a bug in the interpretation of record projections ("bad number
+ of parameters" error)
+- Fixed a bug in the omega tactic
+- Fixed a bug in the fold tactic regarding hypotheses ordering
+- Pretty-print of universes fixed
+- Added an empty level 99 in patterns syntax entry
+- "Notation" bug fixes ("only parsing" bug, printing of numerals
+ arguments of coercions, default spacing for recursive notations
+ with no terminal separator, "Tactic Notation" printer).
+
Changes from V8.0pl1 to V8.0pl2
===============================
diff --git a/INSTALL.ide b/INSTALL.ide
index d8f1208b..1c1d40c8 100644
--- a/INSTALL.ide
+++ b/INSTALL.ide
@@ -35,7 +35,7 @@ INSTALLATION
1) You need to install the OCaml stub library lablgtk2. See
http://wwwfun.kurims.kyoto-u.ac.jp/soft/olabl/lablgtk.html
- The first official release of lablftk2 is here:
+ The first official release of lablgtk2 is here:
http://wwwfun.kurims.kyoto-u.ac.jp/soft/olabl/dist/lablgtk-2.2.0.tar.gz
Note that even if its README requires ocaml > 3.07, it works ok with 3.06.
If you are in a hurry just run :
diff --git a/INSTALL.win b/INSTALL.win
deleted file mode 100644
index f2cddb8a..00000000
--- a/INSTALL.win
+++ /dev/null
@@ -1,63 +0,0 @@
-*****************************************************************
-* INSTALLATION PROCEDURE FOR THE COQ V8 SYSTEM UNDER WINDOWS OS *
-*****************************************************************
-
- The binary distribution consists in a .zip archive file. This .zip contains
-long filenames and cannot therefore be unpacked with pkunzip version 2. Use
-either Winzip (shareware) or the Windows version of unzip (freeware):
-
- http://www.winzip.com/
- http://www.winimage.com/zLibDll/
-
- Unzipping the distribution creates (among others) the following directories
-and files:
-
- coq\bin\ The command-line tools
- coq\lib\ The standard library files
- coq\emacs A Coq mode for your Emacs
- coq\man\man1 The man pages for the command-line tools
-
- There are two cases to consider :
-
-1. You unzip in the root of your drive (say C):
-===============================================
-
- Hence Coq will be installed in C:\coq
-
- You must add the C:\coq\bin path to your environment variable PATH. This is
-done by adding the following line to your AUTOEXEC.BAT:
-
- set PATH=%PATH%;C:\coq\bin
-
- You may also want to specify where Coq has to look for your configuration
-file .coqrc (not mandatory), e.g.:
-
- set HOME=C:\My_Documents\Coq
-
-2. You unzip in some other place (say D:\My_Dir):
-=================================================
-
- You must add the D:\My_Dir\coq\bin path to your environment variable PATH.
-This is done by adding the following line to AUTOEXEC.BAT:
-
- set PATH=%PATH%;D:\My_Dir\coq\bin
-
- You must also set the environment variables COQBIN and COQLIB to tell Coq
-that binaries and libraries are not in the default place. This is done by
-adding the following lines to your AUTOEXEC.BAT:
-
- set COQBIN=D:\My_Dir\coq\bin
- set COQLIB=D:\My_Dir\coq\lib
-
- You may also want to specify where Coq has to look for your configuration
-file .coqrc (not mandatory), e.g.:
-
- set HOME=C:\My_Documents\Coq
-
-PROBLEMS:
-=========
-
- If you have any trouble with this installation, please contact:
-coq-bugs@pauillac.inria.fr.
-
- The Coq Team.
diff --git a/Makefile b/Makefile
index d04bc6ca..fcd6c782 100644
--- a/Makefile
+++ b/Makefile
@@ -6,7 +6,7 @@
# # GNU Lesser General Public License Version 2.1 #
########################################################################
-# $Id: Makefile,v 1.459.2.13 2005/01/21 17:15:12 herbelin Exp $
+# $Id: Makefile,v 1.459.2.22 2006/01/11 23:18:05 barras Exp $
# Makefile for Coq
@@ -80,7 +80,7 @@ MLINCLUDES=$(LOCALINCLUDES) -I $(MYCAMLP4LIB)
BYTEFLAGS=$(MLINCLUDES) $(CAMLDEBUG)
OPTFLAGS=$(MLINCLUDES) $(CAMLTIMEPROF)
OCAMLDEP=ocamldep
-DEPFLAGS=$(LOCALINCLUDES)
+DEPFLAGS=-slash $(LOCALINCLUDES)
OCAMLC_P4O=$(OCAMLC) -pp $(CAMLP4O) $(BYTEFLAGS)
OCAMLOPT_P4O=$(OCAMLOPT) -pp $(CAMLP4O) $(OPTFLAGS)
@@ -331,7 +331,7 @@ $(COQTOPOPT): $(COQMKTOP) $(CMX) $(USERTACCMX)
$(COQTOPBYTE): $(COQMKTOP) $(CMO) $(USERTACCMO)
$(SHOW)'COQMKTOP -o $@'
- $(HIDE)$(COQMKTOP) -top $(LOCALINCLUDES) $(CAMLDEBUG) -o $@
+ $(HIDE)$(COQMKTOP) -top $(BYTEFLAGS) -o $@
$(COQTOP):
cd bin; ln -sf coqtop.$(BEST)$(EXE) coqtop$(EXE)
@@ -375,10 +375,6 @@ $(COQC): $(COQCCMO) $(COQTOPBYTE) $(BESTCOQTOP)
clean::
rm -f scripts/tolink.ml
-archclean::
- rm -f $(COQTOPBYTE) $(COQTOPOPT) $(BESTCOQTOP) $(COQC) $(COQMKTOP)
- rm -f $(COQTOP)
-
# we provide targets for each subdirectory
lib: $(LIBREP)
@@ -534,7 +530,7 @@ COQIDEVO=ide/utf8.vo
$(COQIDEVO): states/initial.coq
$(BOOTCOQTOP) -compile $*
-IDEFILES=$(COQIDEVO) ide/utf8.v ide/coq.png ide/.coqide-gtk2rc
+IDEFILES=$(COQIDEVO) ide/utf8.v ide/coq.ico ide/coq2.ico ide/.coqide-gtk2rc
coqide-binaries: coqide-$(HASCOQIDE)
coqide-no:
@@ -555,35 +551,40 @@ $(COQIDEOPT): $(COQMKTOP) $(CMX) $(USERTACCMX) ide/ide.cmxa
$(COQIDEBYTE): $(COQMKTOP) $(CMO) $(USERTACCMO) ide/ide.cma
$(SHOW)'COQMKTOP -o $@'
- $(HIDE)$(COQMKTOP) -g -ide -top $(LOCALINCLUDES) $(CAMLDEBUG) -o $@
+ $(HIDE)$(COQMKTOP) -ide -top $(BYTEFLAGS) -o $@
$(COQIDE):
cd bin; ln -sf coqide.$(HASCOQIDE)$(EXE) coqide$(EXE)
ide/%.cmo: ide/%.ml
$(SHOW)'OCAMLC $<'
- $(HIDE)$(OCAMLC) -g $(COQIDEFLAGS) $(BYTEFLAGS) -c $<
+ $(HIDE)$(OCAMLC) $(COQIDEFLAGS) $(BYTEFLAGS) -c $<
ide/%.cmi: ide/%.mli
$(SHOW)'OCAMLC $<'
- $(HIDE)$(OCAMLC) -g $(COQIDEFLAGS) $(BYTEFLAGS) -c $<
+ $(HIDE)$(OCAMLC) $(COQIDEFLAGS) $(BYTEFLAGS) -c $<
ide/%.cmx: ide/%.ml
$(SHOW)'OCAMLOPT $<'
$(HIDE)$(OCAMLOPT) $(COQIDEFLAGS) $(OPTFLAGS) -c $<
-ide/utils/%.cmo: ide/%.ml
+ide/utils/%.cmo: ide/utils/%.ml
$(SHOW)'OCAMLC $<'
- $(HIDE)$(OCAMLC) -g $(COQIDEFLAGS) $(BYTEFLAGS) -c $<
+ $(HIDE)$(OCAMLC) $(COQIDEFLAGS) $(BYTEFLAGS) -c $<
-ide/utils/%.cmi: ide/%.mli
+ide/utils/%.cmi: ide/utils/%.mli
$(SHOW)'OCAMLC $<'
- $(HIDE)$(OCAMLC) -g $(COQIDEFLAGS) $(BYTEFLAGS) -c $<
+ $(HIDE)$(OCAMLC) $(COQIDEFLAGS) $(BYTEFLAGS) -c $<
-ide/utils/%.cmx: ide/%.ml
+ide/utils/%.cmx: ide/utils/%.ml
$(SHOW)'OCAMLOPT $<'
$(HIDE)$(OCAMLOPT) $(COQIDEFLAGS) $(OPTFLAGS) -c $<
+# Special target to select between whether lablgtk >= 2.6.0 or not
+ide/undo.cmi: ide/undo.mli
+ $(SHOW)'OCAMLC $<'
+ $(HIDE)$(OCAMLC) $(COQIDEFLAGS) $(BYTEFLAGS) -pp "$(CAMLP4O) $(CAMLP4EXTENDFLAGS) $(CAMLP4COMPAT) -intf" -c -intf $<
+
clean::
rm -f ide/extract_index.ml ide/find_phrase.ml ide/highlight.ml
rm -f ide/config_lexer.ml ide/config_parser.mli ide/config_parser.ml
@@ -693,8 +694,6 @@ contrib7/interface/Centaur.vo: contrib7/interface/Centaur.v $(INTERFACE)
contrib7/interface/AddDad.vo: contrib7/interface/AddDad.v $(INTERFACE) states7/initial.coq
$(BESTCOQTOP) $(TRANSLATE) -boot -byte $(COQOPTS) -compile $*
-clean::
- rm -f bin/parser$(EXE) bin/coq-interface$(EXE) bin/coq-interface.opt$(EXE)
# install targets
install-pcoq:: install-pcoq-binaries install-pcoq-files install-pcoq-manpages
@@ -1104,9 +1103,6 @@ clean::
rm -f tools/coqwc.ml
rm -f tools/coqdoc/pretty.ml tools/coqdoc/index.ml
-archclean::
- rm -f $(TOOLS)
-
###########################################################################
# minicoq
###########################################################################
@@ -1121,22 +1117,19 @@ $(MINICOQ): $(MINICOQCMO)
$(SHOW)'OCAMLC -o $@'
$(HIDE)$(OCAMLC) $(BYTEFLAGS) -o $@ -custom $(CMA) $(MINICOQCMO) $(OSDEPLIBS)
-archclean::
- rm -f $(MINICOQ)
-
###########################################################################
# Installation
###########################################################################
-COQINSTALLPREFIX=
- # Can be changed for a local installation (to make packages).
- # You must NOT put a "/" at the end (Cygnus for win32 does not like "//").
+#COQINSTALLPREFIX=
+# Can be changed for a local installation (to make packages).
+# You must NOT put a "/" at the end (Cygnus for win32 does not like "//").
-FULLBINDIR=$(COQINSTALLPREFIX)$(BINDIR)
-FULLCOQLIB=$(COQINSTALLPREFIX)$(COQLIB)
-FULLMANDIR=$(COQINSTALLPREFIX)$(MANDIR)
-FULLEMACSLIB=$(COQINSTALLPREFIX)$(EMACSLIB)
-FULLCOQDOCDIR=$(COQINSTALLPREFIX)$(COQDOCDIR)
+FULLBINDIR=$(BINDIR:'$(OLDROOT)%='$(COQINSTALLPREFIX)%)
+FULLCOQLIB=$(COQLIB:'$(OLDROOT)%='$(COQINSTALLPREFIX)%)
+FULLMANDIR=$(MANDIR:'$(OLDROOT)%='$(COQINSTALLPREFIX)%)
+FULLEMACSLIB=$(EMACSLIB:'$(OLDROOT)%='$(COQINSTALLPREFIX)%)
+FULLCOQDOCDIR=$(COQDOCDIR:'$(OLDROOT)%='$(COQINSTALLPREFIX)%)
install-coq: install-binaries install-library install-coq-info
install-coq8: install-binaries install-library8 install-coq-info
@@ -1222,7 +1215,7 @@ install-emacs:
install-latex:
$(MKDIR) $(FULLCOQDOCDIR)
- cp tools/coqdoc/coqdoc.sty $(FULLCOQDOCDIR)
+ cp tools/coqdoc/coqdoc.sty $(FULLCOQDOCDIR)
# -$(UPDATETEX)
###########################################################################
@@ -1453,11 +1446,11 @@ ML4FILES += lib/pp.ml4 \
.ml4.cmx:
$(SHOW)'OCAMLOPT4 $<'
- $(HIDE)$(OCAMLOPT) $(OPTFLAGS) -pp "$(CAMLP4O) $(CAMLP4EXTENDFLAGS) `$(CAMLP4DEPS) $<` -impl" -c -impl $<
+ $(HIDE)$(OCAMLOPT) $(OPTFLAGS) -pp "$(CAMLP4O) $(CAMLP4EXTENDFLAGS) `$(CAMLP4DEPS) $<` $(CAMLP4COMPAT) -impl" -c -impl $<
.ml4.cmo:
$(SHOW)'OCAMLC4 $<'
- $(HIDE)$(OCAMLC) $(BYTEFLAGS) -pp "$(CAMLP4O) $(CAMLP4EXTENDFLAGS) `$(CAMLP4DEPS) $<` -impl" -c -impl $<
+ $(HIDE)$(OCAMLC) $(BYTEFLAGS) -pp "$(CAMLP4O) $(CAMLP4EXTENDFLAGS) `$(CAMLP4DEPS) $<` $(CAMLP4COMPAT) -impl" -c -impl $<
#.v.vo:
# $(BOOTCOQTOP) -compile $*
@@ -1473,6 +1466,7 @@ ML4FILES += lib/pp.ml4 \
###########################################################################
archclean::
+ -rm -f bin/*
rm -f config/*.cmx* config/*.[soa]
rm -f lib/*.cmx* lib/*.[soa]
rm -f kernel/*.cmx* kernel/*.[soa]
diff --git a/README.win b/README.win
index 4d698e93..b8cc0c17 100644
--- a/README.win
+++ b/README.win
@@ -6,7 +6,26 @@ THE COQ V8.0 SYSTEM
INSTALLATION.
=============
- See the file INSTALL.win for installation procedure.
+ The windows distribution of Coq consists of an installer that should
+ perform all installation steps. CoqIde (a GTK interface to Coq) can
+ be installed. In case the GTK runtime libraries are not installed,
+ the Coq installer can be set to make a copy of those libraries
+ within the directory of Coq.
+ However, if the files are installed but Coq does not work properly,
+ some steps can be made manually.
+ Let us assume that the installation dir was c:\coq. The following
+ environment variables must be set as:
+ set COQBIN=c:\coq\bin
+ set COQLIB=c:\coq\lib
+ On win9x systems, this is achieved by inserting the 2 lines above
+ in the autoexec.bat file of the system. On other windows systems,
+ environment variables can be configured via the System application
+ of the Control Panel. Then select the Advanced tab.
+ The .bat files in c:\coq should now launch Coq (or CoqIde).
+ The COQBIN path can also be added to the PATH. This might be a
+ bad idea if the GTK libraries of Coq's installer were installed
+ since they might conflict with already installed GTK libraries.
+
COMPILATION.
============
@@ -15,12 +34,10 @@ COMPILATION.
distribution. If you really need to recompile under Windows, here
are some indications:
- 1- Install ocaml version 3.06 or later, Visual C++ (needed
- for the -custom option of ocaml) and MASM (needed if you want
- to produce a native version).
+ 1- Install ocaml version 3.06 or later (mingw port preferably).
2- Install a complete set of Unix utilities (used by Makefiles).
- See: http://sources.redhat.com/cygwin/.
+ See: http://www.cygwin.com/.
3- Under cygwin, type successively
diff --git a/config/Makefile.template b/config/Makefile.template
index cd49db89..e75b8bd0 100644
--- a/config/Makefile.template
+++ b/config/Makefile.template
@@ -24,25 +24,26 @@ LOCAL=LOCALINSTALLATION
# LIBDIR=path where the Coq library will reside
# MANDIR=path where to install manual pages
# EMACSDIR=path where to put Coq's Emacs mode (coq.el)
-BINDIR="BINDIRDIRECTORY"
-COQLIB="COQLIBDIRECTORY"
-MANDIR="MANDIRDIRECTORY"
-EMACSLIB="EMACSLIBDIRECTORY"
+BINDIR='BINDIRDIRECTORY'
+COQLIB='COQLIBDIRECTORY'
+MANDIR='MANDIRDIRECTORY'
+EMACSLIB='EMACSLIBDIRECTORY'
EMACS=EMACSCOMMAND
# Path to Coq distribution
-COQTOP=COQTOPDIRECTORY
+COQTOP='COQTOPDIRECTORY'
VERSION=COQVERSION
# Directory containing Camlp4 binaries. Can be empty if camlp4 is in the PATH
-CAMLP4BIN=CAMLP4BINDIRECTORY
+CAMLP4BIN='CAMLP4BINDIRECTORY'
# Ocaml version number
CAMLVERSION=CAMLTAG
# Camlp4 library directory (avoid CAMLP4LIB used on Windows)
CAMLP4O=CAMLP4TOOL
-MYCAMLP4LIB=CAMLP4LIBDIRECTORY
+CAMLP4COMPAT=CAMLP4COMPATFLAGS
+MYCAMLP4LIB='CAMLP4LIBDIRECTORY'
# Objective-Caml compile command
OCAMLC=BYTECAMLC
@@ -86,7 +87,7 @@ EXE=EXECUTEEXTENSION
MKDIR=mkdir -p
# where to put the coqdoc.sty style file
-COQDOCDIR=COQDOCDIRECTORY
+COQDOCDIR='COQDOCDIRECTORY'
# command to update TeX' kpathsea database
#MKTEXLSR=MKTEXLSRCOMMAND
diff --git a/config/coq_config.mli b/config/coq_config.mli
index 1d88358a..4b780b1f 100644
--- a/config/coq_config.mli
+++ b/config/coq_config.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: coq_config.mli,v 1.9.16.1 2004/07/16 19:29:58 herbelin Exp $ i*)
+(*i $Id: coq_config.mli,v 1.9.16.2 2006/01/10 17:06:23 barras Exp $ i*)
val local : bool (* local use (no installation) *)
@@ -26,7 +26,6 @@ val osdeplibs : string (* OS dependant link options for ocamlc *)
(* val defined : string list (* options for lib/ocamlpp *) *)
val version : string (* version number of Coq *)
-val versionsi : string (* version number of Coq\_SearchIsos *)
val date : string (* release date *)
val compile_date : string (* compile date *)
diff --git a/configure b/configure
index 0891b262..193ebff4 100755
--- a/configure
+++ b/configure
@@ -6,8 +6,8 @@
#
##################################
-VERSION=8.0pl2
-DATE="Jan 2005"
+VERSION=8.0pl3
+DATE="Jan 2006"
# a local which command for sh
which () {
@@ -30,66 +30,50 @@ coq_profile_flag=
best_compiler=opt
local=false
+src_spec=no
+prefix_spec=no
bindir_spec=no
libdir_spec=no
mandir_spec=no
emacslib_spec=no
-emacs_spec=no
+#emacs_spec=no
coqdocdir_spec=no
reals_opt=no
reals=all
arch_spec=no
coqide_spec=no
-COQTOP=`pwd`
-
-
# Parse command-line arguments
while : ; do
case "$1" in
"") break;;
- -prefix|--prefix) bindir_spec=yes
- bindir=$2/bin
- libdir_spec=yes
- libdir=$2/lib/coq
- mandir_spec=yes
- mandir=$2/man
- coqdocdir_spec=yes
- coqdocdir=$2/share/texmf/tex/latex/misc
+ -prefix|--prefix) prefix_spec=yes
+ prefix="$2"
shift;;
-local|--local) local=true
- bindir_spec=yes
- bindir=$COQTOP/bin
- libdir_spec=yes
- libdir=$COQTOP
- mandir_spec=yes
- mandir=$COQTOP/man
- emacslib_spec=yes
- emacslib=$COQTOP/tools/emacs
- coqdocdir_spec=yes
- coqdocdir=$COQTOP/tools/coqdoc
reals_opt=yes
reals=all;;
- -src|--src) COQTOP=$2
+ -src|--src) src_spec=yes
+ COQTOP="$2"
shift;;
-bindir|--bindir) bindir_spec=yes
- bindir=$2
+ bindir="$2"
shift;;
-libdir|--libdir) libdir_spec=yes
- libdir=$2
+ libdir="$2"
shift;;
-mandir|--mandir) mandir_spec=yes
mandir=$2
shift;;
-emacslib|--emacslib) emacslib_spec=yes
- emacslib=$2
+ emacslib="$2"
shift;;
- -emacs |--emacs) emacs_spec=yes
- emacs=$2
- shift;;
+# -emacs |--emacs) emacs_spec=yes
+# emacs="$2"
+# shift;;
-coqdocdir|--coqdocdir) coqdocdir_spec=yes
- coqdocdir=$2
+ coqdocdir="$2"
shift;;
-arch|--arch) arch_spec=yes
arch=$2
@@ -111,6 +95,11 @@ while : ; do
shift
done
+if [ $prefix_spec = yes -a $local = true ] ; then
+ echo "Options -prefix and -local are incompatible"
+ echo "Configure script failed!"
+ exit 1
+fi
# compile date
DATEPGM=`which date`
@@ -146,125 +135,28 @@ case $arch_spec in
yes) ARCH=$arch
esac
-# bindir, libdir, mandir, etc.
-
-case $ARCH in
- win32)
- bindir_def=C:\\coq\\bin
- libdir_def=C:\\coq\\lib
- mandir_def=C:\\coq\\man
- emacslib_def=C:\\coq\\emacs;;
- *)
- bindir_def=/usr/local/bin
- libdir_def=/usr/local/lib/coq
- mandir_def=/usr/local/man
- emacslib_def=/usr/share/emacs/site-lisp
- coqdocdir_def=/usr/share/texmf/tex/latex/misc;;
-esac
-
-emacs_def=emacs
-
-case $bindir_spec in
- no) echo "Where should I install the Coq binaries [$bindir_def] ?"
- read BINDIR
-
- case $BINDIR in
- "") BINDIR=$bindir_def;;
- *) true;;
- esac;;
- yes) BINDIR=$bindir;;
-esac
-
-case $libdir_spec in
- no) echo "Where should I install the Coq library [$libdir_def] ?"
- read LIBDIR
-
- case $LIBDIR in
- "") LIBDIR=$libdir_def;;
- *) true;;
- esac;;
- yes) LIBDIR=$libdir;;
-esac
-
-case $mandir_spec in
- no) echo "Where should I install the Coq man pages [$mandir_def] ?"
- read MANDIR
-
- case $MANDIR in
- "") MANDIR=$mandir_def;;
- *) true;;
- esac;;
- yes) MANDIR=$mandir;;
-esac
-
-case $emacslib_spec in
- no) echo "Where should I install the Coq Emacs mode [$emacslib_def] ?"
- read EMACSLIB
-
- case $EMACSLIB in
- "") EMACSLIB=$emacslib_def;;
- *) true;;
- esac;;
- yes) EMACSLIB=$emacslib;;
-esac
-
-case $coqdocdir_spec in
- no) echo "Where should I install Coqdoc TeX/LaTeX files [$coqdocdir_def] ?"
- read COQDOCDIR
-
- case $COQDOCDIR in
- "") COQDOCDIR=$coqdocdir_def;;
- *) true;;
- esac;;
- yes) COQDOCDIR=$coqdocdir;;
-esac
-
-case $reals_opt in
- no) echo "Should I compile the complete theory of real analysis [Y/N, default is Y] ?"
- read reals_ans
-
- case $reals_ans in
- "N"|"n"|"No"|"NO"|"no")
- reals=basic;;
- *) reals=all;;
- esac;;
- yes) true;;
-esac
-
-# case $emacs_spec in
-# no) echo "Which Emacs command should I use to compile coq.el [$emacs_def] ?"
-# read EMACS
-
-# case $EMACS in
-# "") EMACS=$emacs_def;;
-# *) true;;
-# esac;;
-# yes) EMACS=$emacs;;
-# esac
-
-# OS dependent libraries
+# executable extension
case $ARCH in
- sun4*) OS=`uname -r`
- case $OS in
- 5*) OS="Sun Solaris $OS"
- OSDEPLIBS="-cclib -lunix -cclib -lnsl -cclib -lsocket";;
- *) OS="Sun OS $OS"
- OSDEPLIBS="-cclib -lunix"
- esac;;
- alpha) OSDEPLIBS="-cclib -lunix";;
- win32) OS="Win32"
- OSDEPLIBS="-cclib -lunix";;
- *) OSDEPLIBS="-cclib -lunix"
+ win32) EXE=".exe";;
+ *) EXE=""
esac
-# executable extension
+# strip command
case $ARCH in
- win32) EXE=".exe";;
- *) EXE=""
+ win32)
+ # true -> strip : it exists under cygwin !
+ STRIPCOMMAND="strip";;
+ *)
+ if [ "$coq_profile_flag" = "-p" ] ; then
+ STRIPCOMMAND="true"
+ else
+ STRIPCOMMAND="strip"
+ fi
esac
+#########################################
# Objective Caml programs
CAMLC=`which $bytecamlc`
@@ -293,16 +185,25 @@ CAMLBIN=`dirname "$CAMLC"`
CAMLVERSION=`"$CAMLC" -v | sed -n -e 's|.*version* *\(.*\)$|\1|p' `
case $CAMLVERSION in
- 1.*|2.*|3.00|3.01|3.02|3.03|3.03alpha|3.04|3.05beta|3.05)
+ 1.*|2.*|3.00|3.01|3.02|3.03|3.03alpha|3.04|3.05beta|3.05|3.08.0)
echo "Your version of Objective-Caml is $CAMLVERSION."
- echo "You need Objective-Caml 3.06 or later !"
+ if [ "$CAMLVERSION" = "3.08.0" ] ; then
+ echo "You need Objective-Caml 3.06 or later (to the exception of 3.08.0)!"
+ else
+ echo "You need Objective-Caml 3.06 or later!";
+ fi
+ echo "Configuration script failed!"
+ exit 1;;
+ 3.06|3.07*|3.08*)
+ echo "You have Objective-Caml $CAMLVERSION. Good!";;
+ ?*)
+ CAMLP4COMPAT="-loc loc"
+ echo "You have Objective-Caml $CAMLVERSION. Good!";;
+ *)
+ echo "I found the Objective-Caml compiler but cannot find its version number!"
+ echo "Is it installed properly ?"
echo "Configuration script failed!"
exit 1;;
- ?*) echo "You have Objective-Caml $CAMLVERSION. Good!";;
- *) echo "I found the Objective-Caml compiler but cannot find its version number!"
- echo "Is it installed properly ?"
- echo "Configuration script failed!"
- exit 1;;
esac
CAMLTAG=OCAML`echo $CAMLVERSION | sed -e "s/\([1-9]\)\.\([0-9]*\).*/\1\2/g"`
@@ -323,20 +224,28 @@ fi
# For coqmktop
-#CAMLLIB=`"$CAMLC" -v | sed -n -e 's|.*directory:* *\(.*\)$|\1|p' `
CAMLLIB=`"$CAMLC" -where`
# Camlp4 (greatly simplified since merged with ocaml)
CAMLP4BIN=${CAMLBIN}
+CAMLP4LIB=+camlp4
-#case $OS in
-# Win32)
- CAMLP4LIB=+camlp4
-# ;;
-# *)
-# CAMLP4LIB=${CAMLLIB}/camlp4
-#esac
+# OS dependent libraries
+
+case $ARCH in
+ sun4*) OS=`uname -r`
+ case $OS in
+ 5*) OS="Sun Solaris $OS"
+ OSDEPLIBS="-cclib -lunix -cclib -lnsl -cclib -lsocket";;
+ *) OS="Sun OS $OS"
+ OSDEPLIBS="-cclib -lunix"
+ esac;;
+ alpha) OSDEPLIBS="-cclib -lunix";;
+ win32) OS="Win32"
+ OSDEPLIBS="-cclib -lunix";;
+ *) OSDEPLIBS="-cclib -lunix"
+esac
# lablgtk2 and CoqIDE
@@ -349,7 +258,7 @@ if test -x "${CAMLLIB}/lablgtk2" ; then
else
echo "LablGtk2 found, no native threads: bytecode CoqIde will be available"
COQIDE=byte
- fi;
+ fi
else
echo "LablGtk2 found but too old: CoqIde will not be available"
COQIDE=no;
@@ -360,30 +269,154 @@ else
fi
fi
+if [ $COQIDE != no ] ; then
+ if grep "class view " "${CAMLLIB}/lablgtk2/gText.mli" | grep -q "\[>" ; then
+ LABLGTKGE26=yes;
+ else
+ LABLGTKGE26=no
+ fi
+fi
+
# Tell on windows if ocaml understands cygwin or windows path formats
#"$CAMLC" -o config/giveostype config/giveostype.ml
#CAMLOSTYPE=`config/giveostype`
#rm config/giveostype
-case $ARCH in
- win32)
- # true -> strip : it exists under cygwin !
- STRIPCOMMAND="strip";;
- *)
- if [ "$coq_profile_flag" = "-p" ] ; then
- STRIPCOMMAND="true"
- else
- STRIPCOMMAND="strip"
- fi
-esac
-
+######################################
# mktexlsr
+
#MKTEXLSR=`which mktexlsr`
#case $MKTEXLSR in
# "") MKTEXLSR=true;;
#esac
+###########################################
+# bindir, libdir, mandir, etc.
+
+canonical_pwd () {
+ocaml 2>&1 1>/dev/null <<EOF
+ prerr_endline(Sys.getcwd());;
+EOF
+}
+
+case $src_spec in
+ no) COQTOP=`canonical_pwd`
+esac
+
+case $ARCH in
+ win32)
+ bindir_def='C:\coq\bin'
+ libdir_def='C:\coq\lib'
+ mandir_def='C:\coq\man'
+ emacslib_def='C:\coq\emacs'
+ coqdocdir_def='C:\coq\latex';;
+ *)
+ bindir_def=/usr/local/bin
+ libdir_def=/usr/local/lib/coq
+ mandir_def=/usr/local/man
+ emacslib_def=/usr/share/emacs/site-lisp
+ coqdocdir_def=/usr/share/texmf/tex/latex/misc;;
+esac
+
+emacs_def=emacs
+
+case $bindir_spec/$prefix_spec/$local in
+ yes/*/*) BINDIR=$bindir ;;
+ */yes/*) BINDIR=$prefix/bin ;;
+ */*/true) BINDIR=$COQTOP/bin ;;
+ *) echo "Where should I install the Coq binaries [$bindir_def] ?"
+ read BINDIR
+ case $BINDIR in
+ "") BINDIR=$bindir_def;;
+ *) true;;
+ esac;;
+esac
+
+case $libdir_spec/$prefix_spec/$local in
+ yes/*/*) LIBDIR=$libdir;;
+ */yes/*)
+ case $ARCH in
+ win32) LIBDIR=$prefix ;;
+ *) LIBDIR=$prefix/lib/coq ;;
+ esac ;;
+ */*/true) LIBDIR=$COQTOP ;;
+ *) echo "Where should I install the Coq library [$libdir_def] ?"
+ read LIBDIR
+ case $LIBDIR in
+ "") LIBDIR=$libdir_def;;
+ *) true;;
+ esac;;
+esac
+
+case $mandir_spec/$prefix_spec/$local in
+ yes/*/*) MANDIR=$mandir;;
+ */yes/*) MANDIR=$prefix/man ;;
+ */*/true) MANDIR=$COQTOP/man ;;
+ *) echo "Where should I install the Coq man pages [$mandir_def] ?"
+ read MANDIR
+ case $MANDIR in
+ "") MANDIR=$mandir_def;;
+ *) true;;
+ esac;;
+esac
+
+case $emacslib_spec/$prefix_spec/$local in
+ yes/*/*) EMACSLIB=$emacslib;;
+ */yes/*)
+ case $ARCH in
+ win32) EMACSLIB=$prefix/emacs ;;
+ *) EMACSLIB=$prefix/share/emacs/site-lisp ;;
+ esac ;;
+ */*/true) EMACSLIB=$COQTOP/tools/emacs ;;
+ *) echo "Where should I install the Coq Emacs mode [$emacslib_def] ?"
+ read EMACSLIB
+ case $EMACSLIB in
+ "") EMACSLIB=$emacslib_def;;
+ *) true;;
+ esac;;
+esac
+
+case $coqdocdir_spec/$prefix_spec/$local in
+ yes/*/*) COQDOCDIR=$coqdocdir;;
+ */yes/*)
+ case $ARCH in
+ win32) COQDOCDIR=$prefix/latex ;;
+ *) COQDOCDIR=$prefix/share/emacs/site-lisp ;;
+ esac ;;
+ */*/true) COQDOCDIR=$COQTOP/tools/coqdoc ;;
+ *) echo "Where should I install Coqdoc TeX/LaTeX files [$coqdocdir_def] ?"
+ read COQDOCDIR
+ case $COQDOCDIR in
+ "") COQDOCDIR=$coqdocdir_def;;
+ *) true;;
+ esac;;
+esac
+
+case $reals_opt in
+ no) echo "Should I compile the complete theory of real analysis [Y/N, default is Y] ?"
+ read reals_ans
+
+ case $reals_ans in
+ "N"|"n"|"No"|"NO"|"no")
+ reals=basic;;
+ *) reals=all;;
+ esac;;
+ yes) true;;
+esac
+
+# case $emacs_spec in
+# no) echo "Which Emacs command should I use to compile coq.el [$emacs_def] ?"
+# read EMACS
+
+# case $EMACS in
+# "") EMACS=$emacs_def;;
+# *) true;;
+# esac;;
+# yes) EMACS=$emacs;;
+# esac
+
+###########################################
# Summary of the configuration
echo ""
@@ -416,16 +449,19 @@ echo ""
# Building the $COQTOP/config/coq_config.ml file
#####################################################
-# damned backslashes under M$Windows
-case $ARCH in
- win32)
- CAMLLIB=`echo $CAMLLIB |sed -e 's|\\\|\\\\\\\|g'`
- BINDIR=`echo $BINDIR |sed -e 's|\\\|\\\\\\\|g'`
- LIBDIR=`echo $LIBDIR |sed -e 's|\\\|\\\\\\\|g'`
- MANDIR=`echo $MANDIR |sed -e 's|\\\|\\\\\\\|g'`
- EMACSLIB=`echo $EMACSLIB |sed -e 's|\\\|\\\\\\\|g'`
- ;;
-esac
+# An escaped version of a variable
+escape_var () {
+ocaml 2>&1 1>/dev/null <<EOF
+ prerr_endline(String.escaped(Sys.getenv"$VAR"));;
+EOF
+}
+
+export COQTOP BINDIR LIBDIR CAMLLIB
+ESCCOQTOP="`VAR=COQTOP escape_var`"
+ESCBINDIR="`VAR=BINDIR escape_var`"
+ESCLIBDIR="`VAR=LIBDIR escape_var`"
+ESCCAMLLIB="`VAR=CAMLLIB escape_var`"
+ESCCAMLP4LIB="$ESCCAMLLIB"/camlp4
mlconfig_file=$COQTOP/config/coq_config.ml
rm -f $mlconfig_file
@@ -433,16 +469,15 @@ cat << END_OF_COQ_CONFIG > $mlconfig_file
(* DO NOT EDIT THIS FILE: automatically generated by ../configure *)
let local = $local
-let bindir = "$BINDIR"
-let coqlib = "$LIBDIR"
-let coqtop = "$COQTOP"
-let camllib = "$CAMLLIB"
-let camlp4lib = "$CAMLP4LIB"
+let bindir = "$ESCBINDIR"
+let coqlib = "$ESCLIBDIR"
+let coqtop = "$ESCCOQTOP"
+let camllib = "$ESCCAMLLIB"
+let camlp4lib = "$ESCCAMLP4LIB"
let best = "$best_compiler"
let arch = "$ARCH"
let osdeplibs = "$OSDEPLIBS"
let version = "$VERSION"
-let versionsi = "$VERSIONSI"
let date = "$DATE"
let compile_date = "$COMPILEDATE"
let exec_extension = "$EXE"
@@ -474,34 +509,45 @@ chmod a-w $mlconfig_file
rm -f $COQTOP/config/Makefile
-# damned backslashes under M$Windows (bis)
+# damned backslashes under M$Windows
case $ARCH in
win32)
- BINDIR=`echo $BINDIR |sed -e 's|\\\|\\\\\\\|g'`
- LIBDIR=`echo $LIBDIR |sed -e 's|\\\|\\\\\\\|g'`
- MANDIR=`echo $MANDIR |sed -e 's|\\\|\\\\\\\|g'`
- EMACSLIB=`echo $EMACSLIB |sed -e 's|\\\|\\\\\\\|g'`
+ ESCCOQTOP=`echo $COQTOP |sed -e 's|\\\|\\\\\\\|g'`
+ ESCBINDIR=`echo $BINDIR |sed -e 's|\\\|\\\\\\\|g'`
+ ESCLIBDIR=`echo $LIBDIR |sed -e 's|\\\|\\\\\\\|g'`
+ ESCMANDIR=`echo $MANDIR |sed -e 's|\\\|\\\\\\\|g'`
+ ESCEMACSLIB=`echo $EMACSLIB |sed -e 's|\\\|\\\\\\\|g'`
+ ESCCOQDOCDIR=`echo $COQDOCDIR |sed -e 's|\\\|\\\\\\\|g'`
+ ESCCAMLP4BIN=`echo $CAMLP4BIN |sed -e 's|\\\|\\\\\\\|g'`
;;
+ *)
+ ESCCOQTOP="$COQTOP"
+ ESCBINDIR="$BINDIR"
+ ESCLIBDIR="$LIBDIR"
+ ESCMANDIR="$MANDIR"
+ ESCEMACSLIB="$EMACSLIB"
+ ESCCOQDOCDIR="$COQDOCDIR"
+ ESCCAMLP4BIN="$CAMLP4BIN" ;;
esac
sed -e "s|LOCALINSTALLATION|$local|" \
- -e "s|COQTOPDIRECTORY|$COQTOP|" \
+ -e "s|COQTOPDIRECTORY|$ESCCOQTOP|" \
-e "s|COQVERSION|$VERSION|" \
- -e "s|BINDIRDIRECTORY|$BINDIR|" \
- -e "s|COQLIBDIRECTORY|$LIBDIR|" \
- -e "s|MANDIRDIRECTORY|$MANDIR|" \
- -e "s|EMACSLIBDIRECTORY|$EMACSLIB|" \
+ -e "s|BINDIRDIRECTORY|$ESCBINDIR|" \
+ -e "s|COQLIBDIRECTORY|$ESCLIBDIR|" \
+ -e "s|MANDIRDIRECTORY|$ESCMANDIR|" \
+ -e "s|EMACSLIBDIRECTORY|$ESCEMACSLIB|" \
-e "s|EMACSCOMMAND|$EMACS|" \
- -e "s|COQDOCDIRECTORY|$COQDOCDIR|" \
+ -e "s|COQDOCDIRECTORY|$ESCCOQDOCDIR|" \
-e "s|MKTEXLSRCOMMAND|$MKTEXLSR|" \
-e "s|ARCHITECTURE|$ARCH|" \
-e "s|OSDEPENDENTLIBS|$OSDEPLIBS|" \
-e "s|OSDEPENDENTP4OPTFLAGS|$OSDEPP4OPTFLAGS|" \
- -e "s|CAMLLIBDIRECTORY|$CAMLLIB|" \
-e "s|CAMLTAG|$CAMLTAG|" \
- -e "s|CAMLP4BINDIRECTORY|$CAMLP4BIN|" \
+ -e "s|CAMLP4BINDIRECTORY|$ESCCAMLP4BIN|" \
-e "s|CAMLP4LIBDIRECTORY|$CAMLP4LIB|" \
-e "s|CAMLP4TOOL|$camlp4o|" \
+ -e "s|CAMLP4COMPATFLAGS|$CAMLP4COMPAT|" \
-e "s|COQDEBUGFLAG|$coq_debug_flag|" \
-e "s|COQPROFILEFLAG|$coq_profile_flag|" \
-e "s|BESTCOMPILER|$best_compiler|" \
@@ -521,22 +567,31 @@ chmod a-w $COQTOP/config/Makefile
if test "$coq_debug_flag" = "-g" ; then
rm -f $COQTOP/dev/ocamldebug-v7
- if [ "$CAMLP4LIB" = "+camlp4" ] ; then
- CAMLP4LIBFORCAMLDEBUG=$CAMLLIB/camlp4
- else
- CAMLP4LIBFORCAMLDEBUG=$CAMLP4LIB
- fi
sed -e "s|COQTOPDIRECTORY|$COQTOP|" \
-e "s|COQLIBDIRECTORY|$LIBDIR|" \
-e "s|CAMLBINDIRECTORY|$CAMLBIN|" \
- -e "s|CAMLP4LIBDIRECTORY|$CAMLP4LIBFORCAMLDEBUG|" \
+ -e "s|CAMLP4LIBDIRECTORY|$CAMLLIB/camlp4|" \
$COQTOP/dev/ocamldebug-v7.template > $COQTOP/dev/ocamldebug-v7
chmod a-w,a+x $COQTOP/dev/ocamldebug-v7
fi
+##################################################
+# Fixing lablgtk types
+####################################################
+
+if [ "$LABLGTKGE26" = "yes" ] ; then
+ cp -f ide/undo_lablgtk_ge26.mli ide/undo.mli;
+else
+ cp -f ide/undo_lablgtk_lt26.mli ide/undo.mli
+fi
+
+##################################################
+# The end
+####################################################
+
echo "If anything in the above is wrong, please restart './configure'"
echo
echo "*Warning* To compile the system for a new architecture"
echo " don't forget to do a 'make archclean' before './configure'."
-# $Id: configure,v 1.74.2.7 2005/01/21 17:27:32 herbelin Exp $
+# $Id: configure,v 1.74.2.19 2006/01/13 11:50:07 barras Exp $
diff --git a/contrib/extraction/common.ml b/contrib/extraction/common.ml
index 53a2631e..8e441613 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,v 1.51.2.1 2004/07/16 19:30:07 herbelin Exp $ i*)
+(*i $Id: common.ml,v 1.51.2.4 2005/12/16 03:07:39 letouzey Exp $ i*)
open Pp
open Util
@@ -269,11 +269,18 @@ module StdParams = struct
(* TODO: remettre des conditions [lang () = Haskell] disant de qualifier. *)
+ let unquote s =
+ if lang () <> Scheme then s
+ else
+ let s = String.copy s in
+ for i=0 to String.length s - 1 do if s.[i] = '\'' then s.[i] <- '~' done;
+ s
+
let rec dottify = function
| [] -> assert false
- | [s] -> s
- | s::[""] -> s
- | s::l -> (dottify l)^"."^s
+ | [s] -> unquote s
+ | s::[""] -> unquote s
+ | s::l -> (dottify l)^"."^(unquote s)
let pp_global mpl r =
let ls = get_renamings r in
@@ -353,7 +360,7 @@ let preamble prm = match lang () with
| Ocaml -> Ocaml.preamble prm
| Haskell -> Haskell.preamble prm
| Scheme -> Scheme.preamble prm
- | Toplevel -> (fun _ _ -> mt ())
+ | Toplevel -> (fun _ _ _ -> mt ())
let preamble_sig prm = match lang () with
| Ocaml -> Ocaml.preamble_sig prm
@@ -374,7 +381,6 @@ let info f =
(str ("The file "^f^" has been created by extraction."))
let print_structure_to_file f prm struc =
- cons_cofix := Refset.empty;
Hashtbl.clear renamings;
mod_1st_level := Idmap.empty;
modcontents := Gset.empty;
@@ -387,9 +393,13 @@ let print_structure_to_file f prm struc =
else (create_mono_renamings struc; [])
in
let print_dummys =
- (struct_ast_search MLdummy struc,
+ (struct_ast_search ((=) MLdummy) struc,
struct_type_search Tdummy struc,
struct_type_search Tunknown struc)
+ in
+ let print_magic =
+ if lang () <> Haskell then false
+ else struct_ast_search (function MLmagic _ -> true | _ -> false) struc
in
(* print the implementation *)
let cout = option_app (fun (f,_) -> open_out f) f in
@@ -397,7 +407,7 @@ let print_structure_to_file f prm struc =
| None -> !Pp_control.std_ft
| Some cout -> Pp_control.with_output_to cout in
begin try
- msg_with ft (preamble prm used_modules print_dummys);
+ msg_with ft (preamble prm used_modules print_dummys print_magic);
msg_with ft (pp_struct struc);
option_iter close_out cout;
with e ->
diff --git a/contrib/extraction/extraction.ml b/contrib/extraction/extraction.ml
index 46bf06dd..6bfe861f 100644
--- a/contrib/extraction/extraction.ml
+++ b/contrib/extraction/extraction.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: extraction.ml,v 1.136.2.1 2004/07/16 19:30:07 herbelin Exp $ i*)
+(*i $Id: extraction.ml,v 1.136.2.4 2005/12/01 11:27:15 letouzey Exp $ i*)
(*i*)
open Util
@@ -183,15 +183,17 @@ let rec extract_type env db j c args =
| (Info, Default) ->
(* Standard case: two [extract_type] ... *)
let mld = extract_type env' (0::db) j d [] in
- if mld = Tdummy then Tdummy
+ if type_eq (mlt_env env) mld Tdummy then Tdummy
else Tarr (extract_type env db 0 t [], mld)
| (Info, TypeScheme) when j > 0 ->
(* A new type var. *)
let mld = extract_type env' (j::db) (j+1) d [] in
- if mld = Tdummy then Tdummy else Tarr (Tdummy, mld)
+ if type_eq (mlt_env env) mld Tdummy then Tdummy
+ else Tarr (Tdummy, mld)
| _ ->
let mld = extract_type env' (0::db) j d [] in
- if mld = Tdummy then Tdummy else Tarr (Tdummy, mld))
+ if type_eq (mlt_env env) mld Tdummy then Tdummy
+ else Tarr (Tdummy, mld))
| Sort _ -> Tdummy (* The two logical cases. *)
| _ when sort_of env (applist (c, args)) = InProp -> Tdummy
| Rel n ->
@@ -343,38 +345,53 @@ and extract_ind env kn = (* kn is supposed to be in long form *)
if List.length l = 1 && not (type_mem_kn kn (List.hd l))
then raise (I Singleton);
if l = [] then raise (I Standard);
+ if not mib.mind_record then raise (I Standard);
let ip = (kn, 0) in
- if is_custom (IndRef ip) then raise (I Standard);
- let projs =
- try (find_structure ip).s_PROJ
- with Not_found -> raise (I Standard);
+ let r = IndRef ip in
+ if is_custom r then raise (I Standard);
+ (* Now we're sure it's a record. *)
+ (* First, we find its field names. *)
+ let rec names_prod t = match kind_of_term t with
+ | Prod(n,_,t) -> n::(names_prod t)
+ | LetIn(_,_,_,t) -> names_prod t
+ | Cast(t,_) -> names_prod t
+ | _ -> []
in
- let n = nb_default_params env mip0.mind_nf_arity in
- let projs = try List.map out_some projs with _ -> raise (I Standard) in
- let is_true_proj kn =
- let (_,body) = Sign.decompose_lam_assum (constant_value env kn) in
- match kind_of_term body with
- | Rel _ -> false
- | Case _ -> true
- | _ -> assert false
+ let field_names =
+ list_skipn mip0.mind_nparams (names_prod mip0.mind_user_lc.(0)) in
+ assert (List.length field_names = List.length typ);
+ let projs = ref KNset.empty in
+ let mp,d,_ = repr_kn kn in
+ let rec select_fields l typs = match l,typs with
+ | [],[] -> []
+ | (Name id)::l, typ::typs ->
+ if type_eq (mlt_env env) Tdummy typ then select_fields l typs
+ else
+ let knp = make_kn mp d (label_of_id id) in
+ if not (List.mem false (type_to_sign (mlt_env env) typ)) then
+ projs := KNset.add knp !projs;
+ (ConstRef knp) :: (select_fields l typs)
+ | Anonymous::l, typ::typs ->
+ if type_eq (mlt_env env) Tdummy typ then select_fields l typs
+ else error_record r
+ | _ -> assert false
in
- let projs = List.filter is_true_proj projs in
- let rec check = function
- | [] -> [],[]
- | (typ, kn) :: l ->
- let l1,l2 = check l in
- if type_eq (mlt_env env) Tdummy typ then l1,l2
- else
- let r = ConstRef kn in
- if List.mem false (type_to_sign (mlt_env env) typ)
- then r :: l1, l2
- else r :: l1, r :: l2
- in
- add_record kn n (check (List.combine typ projs));
- raise (I Record)
+ let field_glob = select_fields field_names typ
+ in
+ (* Is this record officially declared with its projections ? *)
+ (* If so, we use this information. *)
+ begin try
+ let n = nb_default_params env mip0.mind_nf_arity in
+ List.iter
+ (option_iter
+ (fun kn -> if KNset.mem kn !projs then add_projection n kn))
+ (find_structure ip).s_PROJ
+ with Not_found -> ()
+ end;
+ Record field_glob
with (I info) -> info
in
- let i = {ind_info = ind_info; ind_nparams = npar; ind_packets = packets} in
+ let i = {ind_info = ind_info; ind_nparams = npar; ind_packets = packets} in
add_ind kn i;
internal_call := KNset.remove kn !internal_call;
i
@@ -564,7 +581,9 @@ and extract_cst_app env mle mlt kn args =
(* Different situations depending of the number of arguments: *)
if ls = 0 then put_magic_if magic2 head
else if List.mem true s then
- if la >= ls then put_magic_if (magic2 && not magic1) (MLapp (head, mla))
+ if la >= ls || not (List.mem false s)
+ then
+ put_magic_if (magic2 && not magic1) (MLapp (head, mla))
else
(* Not enough arguments. We complete via eta-expansion. *)
let ls' = ls-la in
@@ -599,7 +618,7 @@ and extract_cons_app env mle mlt (((kn,i) as ip,j) as cp) args =
let type_cons = type_recomp (types, Tglob (IndRef ip, list_tvar)) in
let type_cons = instantiation (nb_tvars, type_cons) in
(* Then, the usual variables [s], [ls], [la], ... *)
- let s = List.map ((<>) Tdummy) types in
+ let s = List.map (type_neq env Tdummy) types in
let ls = List.length s in
let la = List.length args in
assert (la <= ls + params_nb);
@@ -614,7 +633,7 @@ and extract_cons_app env mle mlt (((kn,i) as ip,j) as cp) args =
let head mla =
if mi.ind_info = Singleton then
put_magic_if magic1 (List.hd mla) (* assert (List.length mla = 1) *)
- else put_magic_if magic1 (MLcons (ConstructRef cp, mla))
+ else put_magic_if magic1 (MLcons (mi.ind_info, ConstructRef cp, mla))
in
(* Different situations depending of the number of arguments: *)
if la < params_nb then
@@ -670,10 +689,12 @@ and extract_case env mle ((kn,i) as ip,c,br) mlt =
(* The types of the arguments of the corresponding constructor. *)
let f t = type_subst_vect metas (type_expand env t) in
let l = List.map f oi.ip_types.(i) in
+ (* the corresponding signature *)
+ let s = List.map (type_neq env Tdummy) oi.ip_types.(i) in
(* Extraction of the branch (in functional form). *)
let e = extract_maybe_term env mle (type_recomp (l,mlt)) br.(i) in
(* We suppress dummy arguments according to signature. *)
- let ids,e = case_expunge (List.map ((<>) Tdummy) l) e in
+ let ids,e = case_expunge s e in
(ConstructRef (ip,i+1), List.rev ids, e)
in
if mi.ind_info = Singleton then
@@ -687,7 +708,7 @@ and extract_case env mle ((kn,i) as ip,c,br) mlt =
end
else
(* Standard case: we apply [extract_branch]. *)
- MLcase (a, Array.init br_size extract_branch)
+ MLcase (mi.ind_info, a, Array.init br_size extract_branch)
(*s Extraction of a (co)-fixpoint. *)
@@ -726,7 +747,7 @@ let extract_std_constant env kn body typ =
(* The real type [t']: without head lambdas, expanded, *)
(* and with [Tvar] translated to [Tvar'] (not instantiable). *)
let l,t' = type_decomp (type_expand env (var2var' t)) in
- let s = List.map ((<>) Tdummy) l in
+ let s = List.map (type_neq env Tdummy) l in
(* The initial ML environment. *)
let mle = List.fold_left Mlenv.push_std_type Mlenv.empty l in
(* Decomposing the top level lambdas of [body]. *)
@@ -836,7 +857,8 @@ let logical_decl = function
| Dterm (_,MLdummy,Tdummy) -> true
| Dtype (_,[],Tdummy) -> true
| Dfix (_,av,tv) ->
- (array_for_all ((=) MLdummy) av) && (array_for_all ((=) Tdummy) tv)
+ (array_for_all ((=) MLdummy) av) &&
+ (array_for_all ((=) Tdummy) tv)
| Dind (_,i) -> array_for_all (fun ip -> ip.ip_logical) i.ind_packets
| _ -> false
diff --git a/contrib/extraction/haskell.ml b/contrib/extraction/haskell.ml
index 29c8cd18..3834fe81 100644
--- a/contrib/extraction/haskell.ml
+++ b/contrib/extraction/haskell.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: haskell.ml,v 1.40.2.1 2004/07/16 19:30:08 herbelin Exp $ i*)
+(*i $Id: haskell.ml,v 1.40.2.5 2005/12/16 04:11:28 letouzey Exp $ i*)
(*s Production of Haskell syntax. *)
@@ -27,23 +27,41 @@ let keywords =
[ "case"; "class"; "data"; "default"; "deriving"; "do"; "else";
"if"; "import"; "in"; "infix"; "infixl"; "infixr"; "instance";
"let"; "module"; "newtype"; "of"; "then"; "type"; "where"; "_"; "__";
- "as"; "qualified"; "hiding" ; "unit" ]
+ "as"; "qualified"; "hiding" ; "unit" ; "unsafeCoerce" ]
Idset.empty
-let preamble prm used_modules (mldummy,tdummy,tunknown) =
+let preamble prm used_modules (mldummy,tdummy,tunknown) magic =
let pp_mp = function
| MPfile d -> pr_upper_id (List.hd (repr_dirpath d))
| _ -> assert false
in
+ (if not magic then mt ()
+ else
+ str "{-# OPTIONS_GHC -cpp -fglasgow-exts #-}\n" ++
+ str "{- For Hugs, use the option -F\"cpp -P -traditional\" -}\n\n")
+ ++
str "module " ++ pr_upper_id prm.mod_name ++ str " where" ++ fnl ()
++ fnl() ++
str "import qualified Prelude" ++ fnl() ++
prlist (fun mp -> str "import qualified " ++ pp_mp mp ++ fnl ()) used_modules
++ fnl () ++
- (if mldummy then
+ (if not magic then mt ()
+ else str "\
+#ifdef __GLASGOW_HASKELL__
+import qualified GHC.Base
+unsafeCoerce = GHC.Base.unsafeCoerce#
+#else
+-- HUGS
+import qualified IOExts
+unsafeCoerce = IOExts.unsafeCoerce
+#endif")
+ ++
+ fnl() ++ fnl()
+ ++
+ (if not mldummy then mt ()
+ else
str "__ = Prelude.error \"Logical or arity value used\""
- ++ fnl () ++ fnl()
- else mt())
+ ++ fnl () ++ fnl())
let preamble_sig prm used_modules (mldummy,tdummy,tunknown) = failwith "TODO"
@@ -61,27 +79,36 @@ module Make = functor(P : Mlpp_param) -> struct
let local_mpl = ref ([] : module_path list)
-let pp_global r = P.pp_global !local_mpl r
+let pp_global r =
+ if is_inline_custom r then str (find_custom r)
+ else P.pp_global !local_mpl r
+
let empty_env () = [], P.globals()
(*s Pretty-printing of types. [par] is a boolean indicating whether parentheses
are needed or not. *)
+let kn_sig =
+ let specif = MPfile (dirpath_of_string "Coq.Init.Specif") in
+ make_kn specif empty_dirpath (mk_label "sig")
+
let rec pp_type par vl t =
let rec pp_rec par = function
| Tmeta _ | Tvar' _ -> assert false
| Tvar i -> (try pr_id (List.nth vl (pred i)) with _ -> (str "a" ++ int i))
| Tglob (r,[]) -> pp_global r
| Tglob (r,l) ->
- pp_par par
- (pp_global r ++ spc () ++ prlist_with_sep spc (pp_type true vl) l)
+ if r = IndRef (kn_sig,0) then
+ pp_type true vl (List.hd l)
+ else
+ pp_par par
+ (pp_global r ++ spc () ++ prlist_with_sep spc (pp_type true vl) l)
| Tarr (t1,t2) ->
pp_par par
(pp_rec true t1 ++ spc () ++ str "->" ++ spc () ++ pp_rec false t2)
| Tdummy -> str "()"
| Tunknown -> str "()"
| Taxiom -> str "() -- AXIOM TO BE REALIZED\n"
- | Tcustom s -> str s
in
hov 0 (pp_rec par t)
@@ -125,16 +152,16 @@ let rec pp_expr par env args =
spc () ++ hov 0 pp_a2)))
| MLglob r ->
apply (pp_global r)
- | MLcons (r,[]) ->
+ | MLcons (_,r,[]) ->
assert (args=[]); pp_global r
- | MLcons (r,[a]) ->
+ | MLcons (_,r,[a]) ->
assert (args=[]);
pp_par par (pp_global r ++ spc () ++ pp_expr true env [] a)
- | MLcons (r,args') ->
+ | MLcons (_,r,args') ->
assert (args=[]);
pp_par par (pp_global r ++ spc () ++
prlist_with_sep spc (pp_expr true env []) args')
- | MLcase (t, pv) ->
+ | MLcase (_,t, pv) ->
apply (pp_par par'
(v 0 (str "case " ++ pp_expr false env [] t ++ str " of" ++
fnl () ++ str " " ++ pp_pat env pv)))
@@ -146,7 +173,8 @@ let rec pp_expr par env args =
pp_par par (str "Prelude.error" ++ spc () ++ qs s)
| MLdummy ->
str "__" (* An [MLdummy] may be applied, but I don't really care. *)
- | MLmagic a -> pp_expr par env args a
+ | MLmagic a ->
+ pp_apply (str "unsafeCoerce") par (pp_expr true env [] a :: args)
| MLaxiom -> pp_par par (str "Prelude.error \"AXIOM TO BE REALIZED\"")
and pp_pat env pv =
@@ -210,7 +238,7 @@ let pp_one_ind ip pl cv =
| [] -> (mt ())
| _ -> (str " " ++
prlist_with_sep
- (fun () -> (str " ")) (pp_type true (List.rev pl)) l))
+ (fun () -> (str " ")) (pp_type true pl) l))
in
str (if cv = [||] then "type " else "data ") ++
pp_global (IndRef ip) ++ str " " ++
@@ -239,6 +267,8 @@ let rec pp_ind first kn i ind =
(*s Pretty-printing of a declaration. *)
+let pp_string_parameters ids = prlist (fun id -> str id ++ str " ")
+
let pp_decl mpl =
local_mpl := mpl;
function
@@ -248,21 +278,32 @@ let pp_decl mpl =
| Dtype (r, l, t) ->
if is_inline_custom r then mt ()
else
- let l = rename_tvars keywords l in
- let l' = List.rev l in
- hov 2 (str "type " ++ pp_global r ++ spc () ++
- prlist (fun id -> pr_id id ++ str " ") l ++
- str "=" ++ spc () ++ pp_type false l' t) ++ fnl () ++ fnl ()
+ let l = rename_tvars keywords l in
+ let st =
+ try
+ let ids,s = find_type_custom r in
+ prlist (fun id -> str (id^" ")) ids ++ str "=" ++ spc () ++ str s
+ with not_found ->
+ prlist (fun id -> pr_id id ++ str " ") l ++
+ if t = Taxiom then str "= () -- AXIOM TO BE REALIZED\n"
+ else str "=" ++ spc () ++ pp_type false l t
+ in
+ hov 2 (str "type " ++ pp_global r ++ spc () ++ st) ++ fnl () ++ fnl ()
| Dfix (rv, defs,_) ->
let ppv = Array.map pp_global rv in
prlist_with_sep (fun () -> fnl () ++ fnl ())
(fun (pi,ti) -> pp_function (empty_env ()) pi ti)
(List.combine (Array.to_list ppv) (Array.to_list defs))
++ fnl () ++ fnl ()
- | Dterm (r, a, _) ->
+ | Dterm (r, a, t) ->
if is_inline_custom r then mt ()
else
- hov 0 (pp_function (empty_env ()) (pp_global r) a ++ fnl () ++ fnl ())
+ let e = pp_global r in
+ e ++ str " :: " ++ pp_type false [] t ++ fnl () ++
+ if is_custom r then
+ hov 0 (e ++ str " = " ++ str (find_custom r) ++ fnl() ++ fnl ())
+ else
+ hov 0 (pp_function (empty_env ()) e a ++ fnl () ++ fnl ())
let pp_structure_elem mpl = function
| (l,SEdecl d) -> pp_decl mpl d
diff --git a/contrib/extraction/haskell.mli b/contrib/extraction/haskell.mli
index 4da5db0c..822444bd 100644
--- a/contrib/extraction/haskell.mli
+++ b/contrib/extraction/haskell.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: haskell.mli,v 1.15.6.1 2004/07/16 19:30:08 herbelin Exp $ i*)
+(*i $Id: haskell.mli,v 1.15.6.2 2005/12/01 17:01:22 letouzey Exp $ i*)
open Pp
open Names
@@ -15,6 +15,6 @@ open Miniml
val keywords : Idset.t
val preamble :
- extraction_params -> module_path list -> bool * bool * bool -> std_ppcmds
+ extraction_params -> module_path list -> bool*bool*bool -> bool -> std_ppcmds
module Make : functor(P : Mlpp_param) -> Mlpp
diff --git a/contrib/extraction/miniml.mli b/contrib/extraction/miniml.mli
index 866ff847..7c18f9f5 100644
--- a/contrib/extraction/miniml.mli
+++ b/contrib/extraction/miniml.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: miniml.mli,v 1.46.2.1 2004/07/16 19:30:08 herbelin Exp $ i*)
+(*i $Id: miniml.mli,v 1.46.2.3 2005/12/01 16:43:58 letouzey Exp $ i*)
(*s Target language for extraction: a core ML called MiniML. *)
@@ -35,7 +35,6 @@ type ml_type =
| Tdummy
| Tunknown
| Taxiom
- | Tcustom of string
and ml_meta = { id : int; mutable contents : ml_type option }
@@ -46,7 +45,11 @@ type ml_schema = int * ml_type
(*s ML inductive types. *)
-type inductive_info = Record | Singleton | Coinductive | Standard
+type inductive_info =
+ | Singleton
+ | Coinductive
+ | Standard
+ | Record of global_reference list
(* A [ml_ind_packet] is the miniml counterpart of a [one_inductive_body].
If the inductive is logical ([ip_logical = false]), then all other fields
@@ -79,8 +82,9 @@ type ml_ast =
| MLlam of identifier * ml_ast
| MLletin of identifier * ml_ast * ml_ast
| MLglob of global_reference
- | MLcons of global_reference * ml_ast list
- | MLcase of ml_ast * (global_reference * identifier list * ml_ast) array
+ | MLcons of inductive_info * global_reference * ml_ast list
+ | MLcase of inductive_info * ml_ast *
+ (global_reference * identifier list * ml_ast) array
| MLfix of int * identifier array * ml_ast array
| MLexn of string
| MLdummy
diff --git a/contrib/extraction/mlutil.ml b/contrib/extraction/mlutil.ml
index fbe423a7..c01766b0 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,v 1.104.2.1 2004/07/16 19:30:08 herbelin Exp $ i*)
+(*i $Id: mlutil.ml,v 1.104.2.3 2005/12/01 16:28:04 letouzey Exp $ i*)
(*i*)
open Pp
@@ -117,9 +117,9 @@ let rec mgu = function
let needs_magic p = try mgu p; false with Impossible -> true
-let put_magic_if b a = if b then MLmagic a else a
+let put_magic_if b a = if b && lang () <> Scheme then MLmagic a else a
-let put_magic p a = if needs_magic p then MLmagic a else a
+let put_magic p a = if needs_magic p && lang () <> Scheme then MLmagic a else a
(*S ML type env. *)
@@ -327,11 +327,11 @@ let ast_iter_rel f =
| MLrel i -> f (i-n)
| MLlam (_,a) -> iter (n+1) a
| MLletin (_,a,b) -> iter n a; iter (n+1) b
- | MLcase (a,v) ->
+ | MLcase (_,a,v) ->
iter n a; Array.iter (fun (_,l,t) -> iter (n + (List.length l)) t) v
| MLfix (_,ids,v) -> let k = Array.length ids in Array.iter (iter (n+k)) v
| MLapp (a,l) -> iter n a; List.iter (iter n) l
- | MLcons (_,l) -> List.iter (iter n) l
+ | MLcons (_,_,l) -> List.iter (iter n) l
| MLmagic a -> iter n a
| MLglob _ | MLexn _ | MLdummy | MLaxiom -> ()
in iter 0
@@ -343,10 +343,10 @@ let ast_map_case f (c,ids,a) = (c,ids,f a)
let ast_map f = function
| MLlam (i,a) -> MLlam (i, f a)
| MLletin (i,a,b) -> MLletin (i, f a, f b)
- | MLcase (a,v) -> MLcase (f a, Array.map (ast_map_case f) v)
+ | MLcase (i,a,v) -> MLcase (i,f a, Array.map (ast_map_case f) v)
| MLfix (i,ids,v) -> MLfix (i, ids, Array.map f v)
| MLapp (a,l) -> MLapp (f a, List.map f l)
- | MLcons (c,l) -> MLcons (c, List.map f l)
+ | MLcons (i,c,l) -> MLcons (i,c, List.map f l)
| MLmagic a -> MLmagic (f a)
| MLrel _ | MLglob _ | MLexn _ | MLdummy | MLaxiom as a -> a
@@ -357,11 +357,11 @@ let ast_map_lift_case f n (c,ids,a) = (c,ids, f (n+(List.length ids)) a)
let ast_map_lift f n = function
| MLlam (i,a) -> MLlam (i, f (n+1) a)
| MLletin (i,a,b) -> MLletin (i, f n a, f (n+1) b)
- | MLcase (a,v) -> MLcase (f n a,Array.map (ast_map_lift_case f n) v)
+ | MLcase (i,a,v) -> MLcase (i,f n a,Array.map (ast_map_lift_case f n) v)
| MLfix (i,ids,v) ->
let k = Array.length ids in MLfix (i,ids,Array.map (f (k+n)) v)
| MLapp (a,l) -> MLapp (f n a, List.map (f n) l)
- | MLcons (c,l) -> MLcons (c, List.map (f n) l)
+ | MLcons (i,c,l) -> MLcons (i,c, List.map (f n) l)
| MLmagic a -> MLmagic (f n a)
| MLrel _ | MLglob _ | MLexn _ | MLdummy | MLaxiom as a -> a
@@ -372,10 +372,10 @@ let ast_iter_case f (c,ids,a) = f a
let ast_iter f = function
| MLlam (i,a) -> f a
| MLletin (i,a,b) -> f a; f b
- | MLcase (a,v) -> f a; Array.iter (ast_iter_case f) v
+ | MLcase (_,a,v) -> f a; Array.iter (ast_iter_case f) v
| MLfix (i,ids,v) -> Array.iter f v
| MLapp (a,l) -> f a; List.iter f l
- | MLcons (c,l) -> List.iter f l
+ | MLcons (_,c,l) -> List.iter f l
| MLmagic a -> f a
| MLrel _ | MLglob _ | MLexn _ | MLdummy | MLaxiom as a -> ()
@@ -411,7 +411,7 @@ let nb_occur t = nb_occur_k 1 t
let nb_occur_match =
let rec nb k = function
| MLrel i -> if i = k then 1 else 0
- | MLcase(a,v) ->
+ | MLcase(_,a,v) ->
(nb k a) +
Array.fold_left
(fun r (_,ids,a) -> max r (nb (k+(List.length ids)) a)) 0 v
@@ -420,7 +420,7 @@ let nb_occur_match =
Array.fold_left (fun r a -> r+(nb k a)) 0 v
| MLlam (_,a) -> nb (k+1) a
| MLapp (a,l) -> List.fold_left (fun r a -> r+(nb k a)) (nb k a) l
- | MLcons (_,l) -> List.fold_left (fun r a -> r+(nb k a)) 0 l
+ | MLcons (_,_,l) -> List.fold_left (fun r a -> r+(nb k a)) 0 l
| MLmagic a -> nb k a
| MLglob _ | MLexn _ | MLdummy | MLaxiom -> 0
in nb 1
@@ -616,7 +616,7 @@ let check_and_generalize (r0,l,c) =
if i'<1 then c
else if i'>nargs then MLrel (i-nargs+1)
else raise Impossible
- | MLcons(r,args) when r=r0 && (test_eta_args_lift n nargs args) ->
+ | MLcons(_,r,args) when r=r0 && (test_eta_args_lift n nargs args) ->
MLrel (n+1)
| a -> ast_map_lift genrec n a
in genrec 0 c
@@ -707,7 +707,7 @@ let rec permut_case_fun br acc =
let rec is_iota_gen = function
| MLcons _ -> true
- | MLcase(_,br)-> array_for_all (fun (_,_,t)->is_iota_gen t) br
+ | MLcase(_,_,br)-> array_for_all (fun (_,_,t)->is_iota_gen t) br
| _ -> false
let constructor_index = function
@@ -716,15 +716,15 @@ let constructor_index = function
let iota_gen br =
let rec iota k = function
- | MLcons (r,a) ->
+ | MLcons (i,r,a) ->
let (_,ids,c) = br.(constructor_index r) in
let c = List.fold_right (fun id t -> MLlam (id,t)) ids c in
let c = ast_lift k c in
MLapp (c,a)
- | MLcase(e,br') ->
+ | MLcase(i,e,br') ->
let new_br =
Array.map (fun (n,i,c)->(n,i,iota (k+(List.length i)) c)) br'
- in MLcase(e, new_br)
+ in MLcase(i,e, new_br)
| _ -> assert false
in iota 0
@@ -741,13 +741,18 @@ let rec simpl o = function
simpl o f
| MLapp (f, a) ->
simpl_app o (List.map (simpl o) a) (simpl o f)
- | MLcase (e,br) ->
+ | MLcase (i,e,br) ->
let br = Array.map (fun (n,l,t) -> (n,l,simpl o t)) br in
- simpl_case o br (simpl o e)
- | MLletin(id,c,e) when
- (id = dummy_name) || (is_atomic c) || (is_atomic e) ||
- (let n = nb_occur_match e in n = 0 || (n=1 && o.opt_lin_let)) ->
+ simpl_case o i br (simpl o e)
+ | MLletin(id,c,e) ->
+ let e = (simpl o e) in
+ if
+ (id = dummy_name) || (is_atomic c) || (is_atomic e) ||
+ (let n = nb_occur_match e in n = 0 || (n=1 && o.opt_lin_let))
+ then
simpl o (ast_subst c e)
+ else
+ MLletin(id, simpl o c, e)
| MLfix(i,ids,c) ->
let n = Array.length ids in
if ast_occurs_itvl 1 n c.(i) then
@@ -770,7 +775,7 @@ and simpl_app o a = function
| MLletin (id,e1,e2) when o.opt_let_app ->
(* Application of a letin: we push arguments inside *)
MLletin (id, e1, simpl o (MLapp (e2, List.map (ast_lift 1) a)))
- | MLcase (e,br) when o.opt_case_app ->
+ | MLcase (i,e,br) when o.opt_case_app ->
(* Application of a case: we push arguments inside *)
let br' =
Array.map
@@ -778,16 +783,16 @@ and simpl_app o a = function
let k = List.length l in
let a' = List.map (ast_lift k) a in
(n, l, simpl o (MLapp (t,a')))) br
- in simpl o (MLcase (e,br'))
+ in simpl o (MLcase (i,e,br'))
| (MLdummy | MLexn _) as e -> e
(* We just discard arguments in those cases. *)
| f -> MLapp (f,a)
-and simpl_case o br e =
+and simpl_case o i br e =
if o.opt_case_iot && (is_iota_gen e) then (* Generalized iota-redex *)
simpl o (iota_gen br e)
else
- try (* Does a term [f] exist such as each branch is [(f e)] ? *)
+ try (* Does a term [f] exist such that each branch is [(f e)] ? *)
if not o.opt_case_idr then raise Impossible;
let f = check_generalizable_case o.opt_case_idg br in
simpl o (MLapp (MLlam (anonymous,f),[e]))
@@ -801,9 +806,9 @@ and simpl_case o br e =
then
let ids,br = permut_case_fun br [] in
let n = List.length ids in
- if n <> 0 then named_lams ids (MLcase (ast_lift n e, br))
- else MLcase (e, br)
- else MLcase (e,br)
+ if n <> 0 then named_lams ids (MLcase (i,ast_lift n e, br))
+ else MLcase (i,e,br)
+ else MLcase (i,e,br)
let rec post_simpl = function
| MLletin(_,c,e) when (is_atomic (eta_red c)) ->
@@ -1006,8 +1011,8 @@ let optimize_fix a =
let rec ml_size = function
| MLapp(t,l) -> List.length l + ml_size t + ml_size_list l
| MLlam(_,t) -> 1 + ml_size t
- | MLcons(_,l) -> ml_size_list l
- | MLcase(t,pv) ->
+ | MLcons(_,_,l) -> ml_size_list l
+ | MLcase(_,t,pv) ->
1 + ml_size t + (Array.fold_right (fun (_,_,t) a -> a + ml_size t) pv 0)
| MLfix(_,_,f) -> ml_size_array f
| MLletin (_,_,t) -> ml_size t
@@ -1061,7 +1066,7 @@ let rec non_stricts add cand = function
| MLapp (t,l)->
let cand = non_stricts false cand t in
List.fold_left (non_stricts false) cand l
- | MLcons (_,l) ->
+ | MLcons (_,_,l) ->
List.fold_left (non_stricts false) cand l
| MLletin (_,t1,t2) ->
let cand = non_stricts false cand t1 in
@@ -1071,7 +1076,7 @@ let rec non_stricts add cand = function
let cand = lift n cand in
let cand = Array.fold_left (non_stricts false) cand f in
pop n cand
- | MLcase (t,v) ->
+ | MLcase (_,t,v) ->
(* The only interesting case: for a variable to be non-strict, *)
(* it is sufficient that it appears non-strict in at least one branch, *)
(* so we make an union (in fact a merge). *)
diff --git a/contrib/extraction/modutil.ml b/contrib/extraction/modutil.ml
index feb9e54e..54f0c992 100644
--- a/contrib/extraction/modutil.ml
+++ b/contrib/extraction/modutil.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: modutil.ml,v 1.7.2.1 2004/07/16 19:30:08 herbelin Exp $ i*)
+(*i $Id: modutil.ml,v 1.7.2.4 2005/12/01 17:01:22 letouzey Exp $ i*)
open Names
open Declarations
@@ -157,6 +157,10 @@ let struct_iter do_decl do_spec s =
type do_ref = global_reference -> unit
+let record_iter_references do_term = function
+ | Record l -> List.iter do_term l
+ | _ -> ()
+
let type_iter_references do_type t =
let rec iter = function
| Tglob (r,l) -> do_type r; List.iter iter l
@@ -169,8 +173,12 @@ let ast_iter_references do_term do_cons do_type a =
ast_iter iter a;
match a with
| MLglob r -> do_term r
- | MLcons (r,_) -> do_cons r
- | MLcase (_,v) as a -> Array.iter (fun (r,_,_) -> do_cons r) v
+ | MLcons (i,r,_) ->
+ if lang () = Ocaml then record_iter_references do_term i;
+ do_cons r
+ | MLcase (i,_,v) as a ->
+ if lang () = Ocaml then record_iter_references do_term i;
+ Array.iter (fun (r,_,_) -> do_cons r) v
| _ -> ()
in iter a
@@ -180,7 +188,7 @@ let ind_iter_references do_term do_cons do_type kn ind =
let packet_iter ip p =
do_type (IndRef ip); Array.iteri (fun j -> cons_iter (ip,j+1)) p.ip_types
in
- if ind.ind_info = Record then List.iter do_term (find_projections kn);
+ if lang () = Ocaml then record_iter_references do_term ind.ind_info;
Array.iteri (fun i -> packet_iter (kn,i)) ind.ind_packets
let decl_iter_references do_term do_cons do_type =
@@ -236,7 +244,7 @@ let struct_get_references_list struc =
exception Found
let rec ast_search t a =
- if t = a then raise Found else ast_iter (ast_search t) a
+ if t a then raise Found else ast_iter (ast_search t) a
let decl_ast_search t = function
| Dterm (_,a,_) -> ast_search t a
diff --git a/contrib/extraction/modutil.mli b/contrib/extraction/modutil.mli
index f73e18f7..7f8c4113 100644
--- a/contrib/extraction/modutil.mli
+++ b/contrib/extraction/modutil.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: modutil.mli,v 1.2.2.1 2004/07/16 19:30:08 herbelin Exp $ i*)
+(*i $Id: modutil.mli,v 1.2.2.2 2005/12/01 17:01:22 letouzey Exp $ i*)
open Names
open Declarations
@@ -42,7 +42,7 @@ val add_labels_mp : module_path -> label list -> module_path
(*s Functions upon ML modules. *)
-val struct_ast_search : ml_ast -> ml_structure -> bool
+val struct_ast_search : (ml_ast -> bool) -> ml_structure -> bool
val struct_type_search : ml_type -> ml_structure -> bool
type do_ref = global_reference -> unit
diff --git a/contrib/extraction/ocaml.ml b/contrib/extraction/ocaml.ml
index 707ef94f..ff9cfd21 100644
--- a/contrib/extraction/ocaml.ml
+++ b/contrib/extraction/ocaml.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: ocaml.ml,v 1.100.2.1 2004/07/16 19:30:08 herbelin Exp $ i*)
+(*i $Id: ocaml.ml,v 1.100.2.6 2005/12/01 17:01:22 letouzey Exp $ i*)
(*s Production of Ocaml syntax. *)
@@ -20,8 +20,6 @@ open Miniml
open Mlutil
open Modutil
-let cons_cofix = ref Refset.empty
-
(*s Some utility functions. *)
let pp_par par st = if par then str "(" ++ st ++ str ")" else st
@@ -68,6 +66,12 @@ let sec_space_if = function true -> spc () | false -> mt ()
let fnl2 () = fnl () ++ fnl ()
+let pp_parameters l =
+ (pp_boxed_tuple pp_tvar l ++ space_if (l<>[]))
+
+let pp_string_parameters l =
+ (pp_boxed_tuple str l ++ space_if (l<>[]))
+
(*s Generic renaming issues. *)
let rec rename_id id avoid =
@@ -126,7 +130,7 @@ let keywords =
"land"; "lor"; "lxor"; "lsl"; "lsr"; "asr" ; "unit" ; "_" ; "__" ]
Idset.empty
-let preamble _ used_modules (mldummy,tdummy,tunknown) =
+let preamble _ used_modules (mldummy,tdummy,tunknown) _ =
let pp_mp = function
| MPfile d -> pr_upper_id (List.hd (repr_dirpath d))
| _ -> assert false
@@ -167,22 +171,33 @@ let pp_global r =
let empty_env () = [], P.globals ()
+exception NoRecord
+
+let find_projections = function Record l -> l | _ -> raise NoRecord
+
(*s Pretty-printing of types. [par] is a boolean indicating whether parentheses
are needed or not. *)
+let kn_sig =
+ let specif = MPfile (dirpath_of_string "Coq.Init.Specif") in
+ make_kn specif empty_dirpath (mk_label "sig")
+
let rec pp_type par vl t =
let rec pp_rec par = function
| Tmeta _ | Tvar' _ | Taxiom -> assert false
| Tvar i -> (try pp_tvar (List.nth vl (pred i))
with _ -> (str "'a" ++ int i))
| Tglob (r,[]) -> pp_global r
- | Tglob (r,l) -> pp_tuple_light pp_rec l ++ spc () ++ pp_global r
+ | Tglob (r,l) ->
+ if r = IndRef (kn_sig,0) then
+ pp_tuple_light pp_rec l
+ else
+ pp_tuple_light pp_rec l ++ spc () ++ pp_global r
| Tarr (t1,t2) ->
pp_par par
(pp_rec true t1 ++ spc () ++ str "->" ++ spc () ++ pp_rec false t2)
| Tdummy -> str "__"
| Tunknown -> str "__"
- | Tcustom s -> str s
in
hov 0 (pp_rec par t)
@@ -193,7 +208,7 @@ let rec pp_type par vl t =
let expr_needs_par = function
| MLlam _ -> true
- | MLcase (_,[|_|]) -> false
+ | MLcase (_,_,[|_|]) -> false
| MLcase _ -> true
| _ -> false
@@ -231,30 +246,32 @@ let rec pp_expr par env args =
let record = List.hd args in
pp_apply (record ++ str "." ++ pp_global r) par (List.tl args)
with _ -> apply (pp_global r))
- | MLcons (r,[]) ->
+ | MLcons (Coinductive,r,[]) ->
assert (args=[]);
- if Refset.mem r !cons_cofix then
- pp_par par (str "lazy " ++ pp_global r)
- else pp_global r
- | MLcons (r,args') ->
- (try
- let projs = find_projections (kn_of_r r) in
- pp_record_pat (projs, List.map (pp_expr true env []) args')
- with Not_found ->
- assert (args=[]);
- let tuple = pp_tuple (pp_expr true env []) args' in
- if Refset.mem r !cons_cofix then
- pp_par par (str "lazy (" ++ pp_global r ++ spc() ++ tuple ++str ")")
- else pp_par par (pp_global r ++ spc () ++ tuple))
- | MLcase (t, pv) ->
+ pp_par par (str "lazy " ++ pp_global r)
+ | MLcons (Coinductive,r,args') ->
+ assert (args=[]);
+ let tuple = pp_tuple (pp_expr true env []) args' in
+ pp_par par (str "lazy (" ++ pp_global r ++ spc() ++ tuple ++str ")")
+ | MLcons (_,r,[]) ->
+ assert (args=[]);
+ pp_global r
+ | MLcons (Record projs, r, args') ->
+ assert (args=[]);
+ pp_record_pat (projs, List.map (pp_expr true env []) args')
+ | MLcons (_,r,args') ->
+ assert (args=[]);
+ let tuple = pp_tuple (pp_expr true env []) args' in
+ pp_par par (pp_global r ++ spc () ++ tuple)
+ | MLcase (i, t, pv) ->
let r,_,_ = pv.(0) in
- let expr = if Refset.mem r !cons_cofix then
+ let expr = if i = Coinductive then
(str "Lazy.force" ++ spc () ++ pp_expr true env [] t)
else
(pp_expr false env [] t)
in
(try
- let projs = find_projections (kn_of_r r) in
+ let projs = find_projections i in
let (_, ids, c) = pv.(0) in
let n = List.length ids in
match c with
@@ -263,17 +280,17 @@ let rec pp_expr par env args =
pp_global (List.nth projs (n-i))))
| MLapp (MLrel i, a) when i <= n ->
if List.exists (ast_occurs_itvl 1 n) a
- then raise Not_found
+ then raise NoRecord
else
let ids,env' = push_vars (List.rev ids) env in
(pp_apply
(pp_expr true env [] t ++ str "." ++
pp_global (List.nth projs (n-i)))
par ((List.map (pp_expr true env' []) a) @ args))
- | _ -> raise Not_found
- with Not_found ->
+ | _ -> raise NoRecord
+ with NoRecord ->
if Array.length pv = 1 then
- let s1,s2 = pp_one_pat env pv.(0) in
+ let s1,s2 = pp_one_pat env i pv.(0) in
apply
(hv 0
(pp_par par'
@@ -285,7 +302,7 @@ let rec pp_expr par env args =
apply
(pp_par par'
(v 0 (str "match " ++ expr ++ str " with" ++
- fnl () ++ str " | " ++ pp_pat env pv))))
+ fnl () ++ str " | " ++ pp_pat env i pv))))
| MLfix (i,ids,defs) ->
let ids',env' = push_vars (List.rev (Array.to_list ids)) env in
pp_fix par env' i (Array.of_list (List.rev ids'),defs) args
@@ -307,21 +324,21 @@ and pp_record_pat (projs, args) =
(List.combine projs args) ++
str " }"
-and pp_one_pat env (r,ids,t) =
+and pp_one_pat env i (r,ids,t) =
let ids,env' = push_vars (List.rev ids) env in
let expr = pp_expr (expr_needs_par t) env' [] t in
try
- let projs = find_projections (kn_of_r r) in
+ let projs = find_projections i in
pp_record_pat (projs, List.rev_map pr_id ids), expr
- with Not_found ->
+ with NoRecord ->
let args =
if ids = [] then (mt ())
else str " " ++ pp_boxed_tuple pr_id (List.rev ids) in
pp_global r ++ args, expr
-and pp_pat env pv =
+and pp_pat env i pv =
prvect_with_sep (fun () -> (fnl () ++ str " | "))
- (fun x -> let s1,s2 = pp_one_pat env x in
+ (fun x -> let s1,s2 = pp_one_pat env i x in
hov 2 (s1 ++ str " ->" ++ spc () ++ s2)) pv
and pp_function env f t =
@@ -331,20 +348,17 @@ and pp_function env f t =
let ktl = array_map_to_list (fun (_,l,t0) -> (List.length l,t0)) pv in
not (List.exists (fun (k,t0) -> ast_occurs (k+1) t0) ktl)
in
- let is_not_cofix pv =
- let (r,_,_) = pv.(0) in not (Refset.mem r !cons_cofix)
- in
match t' with
- | MLcase(MLrel 1,pv) when is_not_cofix pv ->
+ | MLcase(i,MLrel 1,pv) when i=Standard ->
if is_function pv then
(f ++ pr_binding (List.rev (List.tl bl)) ++
str " = function" ++ fnl () ++
- v 0 (str " | " ++ pp_pat env' pv))
+ v 0 (str " | " ++ pp_pat env' i pv))
else
(f ++ pr_binding (List.rev bl) ++
str " = match " ++
pr_id (List.hd bl) ++ str " with" ++ fnl () ++
- v 0 (str " | " ++ pp_pat env' pv))
+ v 0 (str " | " ++ pp_pat env' i pv))
| _ -> (f ++ pr_binding (List.rev bl) ++
str " =" ++ fnl () ++ str " " ++
@@ -384,12 +398,6 @@ let rec pp_Dfix init i ((rv,c,t) as fix) =
(*s Pretty-printing of inductive types declaration. *)
-let pp_parameters l =
- (pp_boxed_tuple pp_tvar l ++ space_if (l<>[]))
-
-let pp_string_parameters l =
- (pp_boxed_tuple str l ++ space_if (l<>[]))
-
let pp_one_ind prefix ip pl cv =
let pl = rename_tvars keywords pl in
let pp_constructor (r,l) =
@@ -420,9 +428,8 @@ let pp_singleton kn packet =
pp_comment (str "singleton inductive, whose constructor was " ++
pr_id packet.ip_consnames.(0)))
-let pp_record kn packet =
- let l = List.combine (find_projections kn) packet.ip_types.(0) in
- let projs = find_projections kn in
+let pp_record kn projs packet =
+ let l = List.combine projs packet.ip_types.(0) in
let pl = rename_tvars keywords packet.ip_vars in
str "type " ++ pp_parameters pl ++ pp_global (IndRef (kn,0)) ++ str " = { "++
hov 0 (prlist_with_sep (fun () -> str ";" ++ spc ())
@@ -466,13 +473,9 @@ let pp_ind co kn ind =
let pp_mind kn i =
match i.ind_info with
| Singleton -> pp_singleton kn i.ind_packets.(0)
- | Coinductive ->
- let nop _ = ()
- and add r = cons_cofix := Refset.add r !cons_cofix in
- decl_iter_references nop add nop (Dind (kn,i));
- pp_ind true kn i
- | Record -> pp_record kn i.ind_packets.(0)
- | _ -> pp_ind false kn i
+ | Coinductive -> pp_ind true kn i
+ | Record projs -> pp_record kn projs i.ind_packets.(0)
+ | Standard -> pp_ind false kn i
let pp_decl mpl =
local_mpl := mpl;
@@ -481,6 +484,7 @@ let pp_decl mpl =
| Dtype (r, l, t) ->
if is_inline_custom r then failwith "empty phrase"
else
+ let pp_r = pp_global r in
let l = rename_tvars keywords l in
let ids, def = try
let ids,s = find_type_custom r in
@@ -490,7 +494,7 @@ let pp_decl mpl =
if t = Taxiom then str "(* AXIOM TO BE REALIZED *)"
else str "=" ++ spc () ++ pp_type false l t
in
- hov 2 (str "type" ++ spc () ++ ids ++ pp_global r ++
+ hov 2 (str "type" ++ spc () ++ ids ++ pp_r ++
spc () ++ def)
| Dterm (r, a, t) ->
if is_inline_custom r then failwith "empty phrase"
diff --git a/contrib/extraction/ocaml.mli b/contrib/extraction/ocaml.mli
index 711c15da..5015a50d 100644
--- a/contrib/extraction/ocaml.mli
+++ b/contrib/extraction/ocaml.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: ocaml.mli,v 1.26.6.1 2004/07/16 19:30:08 herbelin Exp $ i*)
+(*i $Id: ocaml.mli,v 1.26.6.3 2005/12/01 17:01:22 letouzey Exp $ i*)
(*s Some utility functions to be reused in module [Haskell]. *)
@@ -15,8 +15,6 @@ open Names
open Libnames
open Miniml
-val cons_cofix : Refset.t ref
-
val pp_par : bool -> std_ppcmds -> std_ppcmds
val pp_abst : identifier list -> std_ppcmds
val pp_apply : std_ppcmds -> bool -> std_ppcmds list -> std_ppcmds
@@ -39,10 +37,10 @@ val get_db_name : int -> env -> identifier
val keywords : Idset.t
val preamble :
- extraction_params -> module_path list -> bool * bool * bool -> std_ppcmds
+ extraction_params -> module_path list -> bool*bool*bool -> bool -> std_ppcmds
val preamble_sig :
- extraction_params -> module_path list -> bool * bool * bool -> std_ppcmds
+ extraction_params -> module_path list -> bool*bool*bool -> std_ppcmds
(*s Production of Ocaml syntax. We export both a functor to be used for
extraction in the Coq toplevel and a function to extract some
diff --git a/contrib/extraction/scheme.ml b/contrib/extraction/scheme.ml
index 61045304..4a881da2 100644
--- a/contrib/extraction/scheme.ml
+++ b/contrib/extraction/scheme.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: scheme.ml,v 1.9.2.1 2004/07/16 19:30:08 herbelin Exp $ i*)
+(*i $Id: scheme.ml,v 1.9.2.5 2005/12/16 03:07:39 letouzey Exp $ i*)
(*s Production of Scheme syntax. *)
@@ -24,17 +24,30 @@ open Ocaml
let keywords =
List.fold_right (fun s -> Idset.add (id_of_string s))
- [ "define"; "let"; "lambda"; "lambdas"; "match-case";
+ [ "define"; "let"; "lambda"; "lambdas"; "match";
"apply"; "car"; "cdr";
"error"; "delay"; "force"; "_"; "__"]
Idset.empty
-let preamble _ _ (mldummy,_,_) =
+let preamble _ _ (mldummy,_,_) _ =
+ str ";; This extracted scheme code relies on some additional macros" ++
+ fnl () ++
+ str ";; available at http://www.pps.jussieu.fr/~letouzey/scheme" ++
+ fnl () ++
+ str "(load \"macros_extr.scm\")" ++
+ fnl () ++ fnl () ++
(if mldummy then
str "(define __ (lambda (_) __))"
++ fnl () ++ fnl()
else mt ())
+let pr_id id =
+ let s = string_of_id id in
+ for i = 0 to String.length s - 1 do
+ if s.[i] = '\'' then s.[i] <- '~'
+ done;
+ str s
+
let paren = pp_par true
let pp_abst st = function
@@ -43,6 +56,12 @@ let pp_abst st = function
| l -> paren
(str "lambdas " ++ paren (prlist_with_sep spc pr_id l) ++ spc () ++ st)
+let pp_apply st _ = function
+ | [] -> st
+ | [a] -> hov 2 (paren (st ++ spc () ++ a))
+ | args -> hov 2 (paren (str "@ " ++ st ++
+ (prlist (fun x -> spc () ++ x) args)))
+
(*s The pretty-printing functor. *)
module Make = functor(P : Mlpp_param) -> struct
@@ -63,7 +82,7 @@ let rec pp_expr env args =
| MLlam _ as a ->
let fl,a' = collect_lams a in
let fl,env' = push_vars fl env in
- pp_abst (pp_expr env' [] a') (List.rev fl)
+ apply (pp_abst (pp_expr env' [] a') (List.rev fl))
| MLletin (id,a1,a2) ->
let i,env' = push_vars [id] env in
apply
@@ -77,46 +96,46 @@ let rec pp_expr env args =
++ spc () ++ hov 0 (pp_expr env' [] a2)))))
| MLglob r ->
apply (pp_global r)
- | MLcons (r,args') ->
+ | MLcons (i,r,args') ->
assert (args=[]);
let st =
str "`" ++
paren (pp_global r ++
- (if args' = [] then mt () else (spc () ++ str ",")) ++
- prlist_with_sep
- (fun () -> spc () ++ str ",")
- (pp_expr env []) args')
+ (if args' = [] then mt () else spc ()) ++
+ prlist_with_sep spc (pp_cons_args env) args')
in
- if Refset.mem r !cons_cofix then
- paren (str "delay " ++ st)
- else st
- | MLcase (t, pv) ->
- let r,_,_ = pv.(0) in
- let e = if Refset.mem r !cons_cofix then
- paren (str "force" ++ spc () ++ pp_expr env [] t)
- else
- pp_expr env [] t
- in apply (v 3 (paren
- (str "match-case " ++ e ++ fnl () ++ pp_pat env pv)))
+ if i = Coinductive then paren (str "delay " ++ st) else st
+ | MLcase (i,t, pv) ->
+ let e =
+ if i <> Coinductive then pp_expr env [] t
+ else paren (str "force" ++ spc () ++ pp_expr env [] t)
+ in
+ apply (v 3 (paren (str "match " ++ e ++ fnl () ++ pp_pat env pv)))
| MLfix (i,ids,defs) ->
let ids',env' = push_vars (List.rev (Array.to_list ids)) env in
pp_fix env' i (Array.of_list (List.rev ids'),defs) args
| MLexn s ->
(* An [MLexn] may be applied, but I don't really care. *)
- paren (str "absurd")
+ paren (str "error" ++ spc () ++ qs s)
| MLdummy ->
str "__" (* An [MLdummy] may be applied, but I don't really care. *)
| MLmagic a ->
pp_expr env args a
- | MLaxiom -> paren (str "absurd ;;AXIOM TO BE REALIZED\n")
+ | MLaxiom -> paren (str "error \"AXIOM TO BE REALIZED\"")
+
+and pp_cons_args env = function
+ | MLcons (i,r,args) when i<>Coinductive ->
+ paren (pp_global r ++
+ (if args = [] then mt () else spc ()) ++
+ prlist_with_sep spc (pp_cons_args env) args)
+ | e -> str "," ++ pp_expr env [] e
and pp_one_pat env (r,ids,t) =
- let pp_arg id = str "?" ++ pr_id id in
let ids,env' = push_vars (List.rev ids) env in
let args =
if ids = [] then mt ()
- else (str " " ++ prlist_with_sep spc pp_arg (List.rev ids))
+ else (str " " ++ prlist_with_sep spc pr_id (List.rev ids))
in
(pp_global r ++ args), (pp_expr env' [] t)
@@ -133,7 +152,8 @@ and pp_fix env j (ids,bl) args =
(str "letrec " ++
(v 0 (paren
(prvect_with_sep fnl
- (fun (fi,ti) -> paren ((pr_id fi) ++ (pp_expr env [] ti)))
+ (fun (fi,ti) ->
+ paren ((pr_id fi) ++ spc () ++ (pp_expr env [] ti)))
(array_map2 (fun id b -> (id,b)) ids bl)) ++
fnl () ++
hov 2 (pp_apply (pr_id (ids.(j))) true args))))
@@ -156,8 +176,12 @@ let pp_decl _ = function
| Dterm (r, a, _) ->
if is_inline_custom r then mt ()
else
- hov 2 (paren (str "define " ++ pp_global r ++ spc () ++
- pp_expr (empty_env ()) [] a)) ++ fnl () ++ fnl ()
+ if is_custom r then
+ hov 2 (paren (str "define " ++ pp_global r ++ spc () ++
+ str (find_custom r))) ++ fnl () ++ fnl ()
+ else
+ hov 2 (paren (str "define " ++ pp_global r ++ spc () ++
+ pp_expr (empty_env ()) [] a)) ++ fnl () ++ fnl ()
let pp_structure_elem mp = function
| (l,SEdecl d) -> pp_decl mp d
diff --git a/contrib/extraction/scheme.mli b/contrib/extraction/scheme.mli
index 6e689a47..2a828fb9 100644
--- a/contrib/extraction/scheme.mli
+++ b/contrib/extraction/scheme.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: scheme.mli,v 1.6.6.1 2004/07/16 19:30:08 herbelin Exp $ i*)
+(*i $Id: scheme.mli,v 1.6.6.2 2005/12/01 17:01:22 letouzey Exp $ i*)
(*s Some utility functions to be reused in module [Haskell]. *)
@@ -17,7 +17,7 @@ open Names
val keywords : Idset.t
val preamble :
- extraction_params -> module_path list -> bool * bool * bool -> std_ppcmds
+ extraction_params -> module_path list -> bool*bool*bool -> bool -> std_ppcmds
module Make : functor(P : Mlpp_param) -> Mlpp
diff --git a/contrib/extraction/table.ml b/contrib/extraction/table.ml
index a65c51a4..9d73d13f 100644
--- a/contrib/extraction/table.ml
+++ b/contrib/extraction/table.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: table.ml,v 1.35.2.1 2004/07/16 19:30:08 herbelin Exp $ i*)
+(*i $Id: table.ml,v 1.35.2.2 2005/11/29 21:40:51 letouzey Exp $ i*)
open Names
open Term
@@ -90,17 +90,9 @@ let is_recursor = function
(*s Record tables. *)
-let records = ref (KNmap.empty : global_reference list KNmap.t)
-let init_records () = records := KNmap.empty
-
let projs = ref (Refmap.empty : int Refmap.t)
let init_projs () = projs := Refmap.empty
-
-let add_record kn n (l1,l2) =
- records := KNmap.add kn l1 !records;
- projs := List.fold_right (fun r -> Refmap.add r n) l2 !projs
-
-let find_projections kn = KNmap.find kn !records
+let add_projection n kn = projs := Refmap.add (ConstRef kn) n !projs
let is_projection r = Refmap.mem r !projs
let projection_arity r = Refmap.find r !projs
@@ -108,7 +100,7 @@ let projection_arity r = Refmap.find r !projs
let reset_tables () =
init_terms (); init_types (); init_inductives (); init_recursors ();
- init_records (); init_projs ()
+ init_projs ()
(*s Printing. *)
@@ -196,6 +188,10 @@ let error_MPfile_as_mod d =
err (str ("The whole file "^(string_of_dirpath d)^".v is used somewhere as a module.\n"^
"Extraction cannot currently deal with this situation.\n"))
+let error_record r =
+ err (str "Record " ++ Printer.pr_global r ++ str " has an anonymous field." ++ fnl () ++
+ str "To help extraction, please use an explicit name.")
+
(*S The Extraction auxiliary commands *)
(*s Extraction AutoInline *)
diff --git a/contrib/extraction/table.mli b/contrib/extraction/table.mli
index 680638e5..6160452a 100644
--- a/contrib/extraction/table.mli
+++ b/contrib/extraction/table.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: table.mli,v 1.25.2.1 2004/07/16 19:30:09 herbelin Exp $ i*)
+(*i $Id: table.mli,v 1.25.2.2 2005/11/29 21:40:51 letouzey Exp $ i*)
open Names
open Libnames
@@ -29,7 +29,7 @@ val error_scheme : unit -> 'a
val error_not_visible : global_reference -> 'a
val error_unqualified_name : string -> string -> 'a
val error_MPfile_as_mod : dir_path -> 'a
-
+val error_record : global_reference -> 'a
val check_inside_module : unit -> unit
val check_inside_section : unit -> unit
@@ -58,9 +58,7 @@ val lookup_ind : kernel_name -> ml_ind
val add_recursors : Environ.env -> kernel_name -> unit
val is_recursor : global_reference -> bool
-val add_record :
- kernel_name -> int -> global_reference list * global_reference list -> unit
-val find_projections : kernel_name -> global_reference list
+val add_projection : int -> kernel_name -> unit
val is_projection : global_reference -> bool
val projection_arity : global_reference -> int
diff --git a/contrib/funind/tacinv.ml4 b/contrib/funind/tacinv.ml4
index b358ff39..1500e1ae 100644
--- a/contrib/funind/tacinv.ml4
+++ b/contrib/funind/tacinv.ml4
@@ -157,11 +157,9 @@ let rec npatternify ltypes c =
| [] -> c
| (mv,nme,t)::ltypes' ->
let c'= substitterm 0 mv (mkRel 1) c in
-(* let _ = prconstr c' in *)
let tlift = lift (List.length ltypes') t in
let res =
npatternify ltypes' (mkLambda (newname_append nme "", tlift, c')) in
-(* let _ = prconstr res in *)
res
(* fait une application (c m1 m2...mn, où mi est une evar, on rend également
@@ -510,15 +508,15 @@ let rec proofPrinc mi lst_vars lst_eqs lst_recs:
| u ->
let varrels = List.rev (List.map fst lst_vars) in
let varnames = List.map snd lst_vars in
- let nb_vars = (List.length varnames) in
- let nb_eqs = (List.length lst_eqs) in
+ let nb_vars = List.length varnames in
+ let nb_eqs = List.length lst_eqs in
let eqrels = List.map fst lst_eqs in
(* [terms_recs]: appel rec du fixpoint, On concatène les appels recs
trouvés dans les let in et les Cases avec ceux trouves dans u (ie
mi.mimick). *)
(* TODO: il faudra gérer plusieurs pt fixes imbriqués ? *)
- let terms_recs = lst_recs @ (hdMatchSub_cpl mi.mimick mi.fonc) in
-
+ let terms_recs = lst_recs @ hdMatchSub_cpl mi.mimick mi.fonc in
+
(*c construction du terme: application successive des variables, des
egalites et des appels rec, a la variable existentielle correspondant a
l'hypothese de recurrence en cours. *)
@@ -573,7 +571,6 @@ let invfun_proof fonc def_fonc gl_abstr pis env sigma =
sigma=sigma; nmefonc=fonc; fonc=(0,0); doeqs=true; fix=false} in
let princ_proof,levar,lposeq,evararr,absc,parms = proofPrinc mi [] [] [] in
princ_proof,levar,lposeq,evararr,absc,parms
-
(* Do intros [i] times, then do rewrite on all introduced hyps which are called
like [heq_prefix], FIX: have another filter than the name. *)
let rec iterintro i =
@@ -596,12 +593,12 @@ let rec iterintro i =
(*
(fun hyp gl ->
- let _ = print_string ("nthhyp= "^ string_of_int i) in
+ let _ = prstr ("nthhyp= "^ string_of_int i) in
if isConst hyp && ((name_of_const hyp)==heq_prefix) then
- let _ = print_string "YES\n" in
+ let _ = prstr "YES\n" in
rewriteLR hyp gl
else
- let _ = print_string "NO\n" in
+ let _ = prstr "NO\n" in
tclIDTAC gl)
*)
@@ -818,9 +815,9 @@ let buildFunscheme fonc mutflist =
(* Declaration of the functional scheme. *)
let declareFunScheme f fname mutflist =
- let scheme =
- buildFunscheme (constr_of f)
- (Array.of_list (List.map constr_of (f::mutflist))) in
+ let flist = if mutflist=[] then [f] else mutflist in
+ let fcstrlist = Array.of_list (List.map constr_of flist) in
+ let scheme = buildFunscheme (constr_of f) fcstrlist in
let _ = prstr "Principe:" in
let _ = prconstr scheme in
let ce = {
diff --git a/contrib/funind/tacinvutils.ml b/contrib/funind/tacinvutils.ml
index 6e086d95..a125b9a7 100644
--- a/contrib/funind/tacinvutils.ml
+++ b/contrib/funind/tacinvutils.ml
@@ -21,7 +21,7 @@ open Reductionops
(*s printing of constr -- debugging *)
(* comment this line to see debug msgs *)
-let msg x = () ;; let prterm c = str ""
+let msg x = () ;; let prterm c = str ""
(* uncomment this to see debugging *)
let prconstr c = msg (str" " ++ prterm c ++ str"\n")
let prlistconstr lc = List.iter prconstr lc
@@ -194,52 +194,53 @@ let rec buildrefl_from_eqs eqs =
-(* list of occurrences of a term inside another, no imbricated
- occurrence are considered (ie we stop looking inside a termthat is
- an occurrence). *)
+(* list of occurrences of a term inside another *)
+(* Cofix will be wrong, not sure Fix is correct too *)
let rec hdMatchSub u t=
- if constr_head_match u t then
- u::(fold_constr (fun l cstr -> l@(hdMatchSub cstr t))
- []
- u)
- else
- fold_constr (fun l cstr -> l@(hdMatchSub cstr t))
- []
- u
+ let subres =
+ match kind_of_term u with
+ | Lambda (nm,tp,cstr) | Prod (nm,tp,cstr) -> hdMatchSub (lift 1 cstr) t
+ | Fix (_,(lna,tl,bl)) ->
+ Array.fold_left
+ (fun acc cstr -> acc @ hdMatchSub (lift (Array.length tl) cstr) t)
+ [] bl
+ | LetIn _ -> assert false
+ (* Correct? *)
+ | _ -> fold_constr (fun l cstr -> l @ hdMatchSub cstr t) [] u
+ in
+ if constr_head_match u t then u :: subres else subres
+
(* let hdMatchSub_list u lt = List.flatten (List.map (hdMatchSub u) lt) *)
let hdMatchSub_cpl u (d,f) =
- let res = ref [] in
- begin
- for i = d to f do res := (hdMatchSub u (mkRel i)) @ !res done;
- !res
- end
+ let res = ref [] in
+ begin
+ for i = d to f do res := hdMatchSub u (mkRel i) @ !res done;
+ !res
+ end
(* destApplication raises an exception if [t] is not an application *)
let exchange_hd_prod subst_hd t =
- let (hd,args)= destApplication t in mkApp (subst_hd,args)
+ let hd,args= destApplication t in mkApp (subst_hd,args)
(* substitute t by by_t in head of products inside in_u, reduces each
product found *)
let rec substit_red prof t by_t in_u =
if constr_head_match in_u (lift prof t)
then
- let _ = prNamedConstr "in_u" in_u in
- let x = whd_beta (exchange_hd_prod (lift prof by_t) in_u) in
- let _ = prNamedConstr "xx " x in
- let _ = prstr "\n\n" in
- x
+ let x = whd_beta (exchange_hd_prod (lift prof by_t) in_u) in
+ x
else
- map_constr_with_binders succ (fun i u -> substit_red i t by_t u)
- prof in_u
+ map_constr_with_binders succ (fun i u -> substit_red i t by_t u) prof in_u
(* [exchange_reli_arrayi t=(reli x y ...) tarr (d,f)] exchange each
reli by tarr.(f-i). *)
let exchange_reli_arrayi tarr (d,f) t =
let hd,args= destApplication t in
let i = destRel hd in
- whd_beta (mkApp (tarr.(f-i) ,args))
+ let res = whd_beta (mkApp (tarr.(f-i) ,args)) in
+ res
let exchange_reli_arrayi_L tarr (d,f) =
List.map (exchange_reli_arrayi tarr (d,f))
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index 50f5b947..02dc57de 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -195,6 +195,11 @@ let xlate_int_opt = function
| Some n -> CT_coerce_INT_to_INT_OPT (CT_int n)
| None -> CT_coerce_NONE_to_INT_OPT CT_none
+let xlate_int_or_var_opt_to_int_opt = function
+ | Some (ArgArg n) -> CT_coerce_INT_to_INT_OPT (CT_int n)
+ | Some (ArgVar _) -> xlate_error "int_or_var: TODO"
+ | None -> CT_coerce_NONE_to_INT_OPT CT_none
+
let tac_qualid_to_ct_ID ref =
CT_ident (Libnames.string_of_qualid (snd (qualid_of_reference ref)))
@@ -1026,12 +1031,12 @@ and xlate_tac =
(if a3 then CT_destructing else CT_coerce_NONE_to_DESTRUCTING CT_none),
(if a4 then CT_usingtdb else CT_coerce_NONE_to_USINGTDB CT_none))
| TacAutoTDB nopt -> CT_autotdb (xlate_int_opt nopt)
- | TacAuto (nopt, Some []) -> CT_auto (xlate_int_opt nopt)
+ | TacAuto (nopt, Some []) -> CT_auto (xlate_int_or_var_opt_to_int_opt nopt)
| TacAuto (nopt, None) ->
- CT_auto_with (xlate_int_opt nopt,
+ CT_auto_with (xlate_int_or_var_opt_to_int_opt nopt,
CT_coerce_STAR_to_ID_NE_LIST_OR_STAR CT_star)
| TacAuto (nopt, Some (id1::idl)) ->
- CT_auto_with(xlate_int_opt nopt,
+ CT_auto_with(xlate_int_or_var_opt_to_int_opt nopt,
CT_coerce_ID_NE_LIST_to_ID_NE_LIST_OR_STAR(
CT_id_ne_list(CT_ident id1, List.map (fun x -> CT_ident x) idl)))
|TacExtend(_, ("autorewritev7"|"autorewritev8"), l::t) ->
@@ -1141,7 +1146,8 @@ and xlate_tac =
| TacClearBody([]) -> assert false
| TacClearBody(a::l) ->
CT_clear_body (CT_id_ne_list (xlate_hyp a, List.map xlate_hyp l))
- | TacDAuto (a, b) -> CT_dauto(xlate_int_opt a, xlate_int_opt b)
+ | TacDAuto (a, b) ->
+ CT_dauto(xlate_int_or_var_opt_to_int_opt a, xlate_int_opt b)
| TacNewDestruct(a,b,(c,_)) ->
CT_new_destruct
(xlate_int_or_constr a, xlate_using b,
diff --git a/contrib/omega/omega.ml b/contrib/omega/omega.ml
index f2eeb5fe..f0eb1e78 100755
--- a/contrib/omega/omega.ml
+++ b/contrib/omega/omega.ml
@@ -13,7 +13,7 @@
(* *)
(**************************************************************************)
-(* $Id: omega.ml,v 1.7.2.1 2004/07/16 19:30:13 herbelin Exp $ *)
+(* $Id: omega.ml,v 1.7.2.2 2005/02/17 18:25:20 herbelin Exp $ *)
open Util
open Hashtbl
@@ -520,9 +520,11 @@ let rec depend relie_on accu = function
depend (e1.id::e2.id::relie_on) (act::accu) l
else
depend relie_on accu l
- | STATE (e,_,_,_,_) ->
- if List.mem e.id relie_on then depend relie_on (act::accu) l
- else depend relie_on accu l
+ | STATE (e,_,o,_,_) ->
+ if List.mem e.id relie_on then
+ depend (o.id::relie_on) (act::accu) l
+ else
+ depend relie_on accu l
| HYP e ->
if List.mem e.id relie_on then depend relie_on (act::accu) l
else depend relie_on accu l
diff --git a/dev/ocamldebug-v7.template b/dev/ocamldebug-v7.template
index 96c53192..1dd625c8 100644
--- a/dev/ocamldebug-v7.template
+++ b/dev/ocamldebug-v7.template
@@ -2,10 +2,10 @@
# wrap around ocamldebug for Coq
-export COQTOP=COQTOPDIRECTORY
-export COQLIB=COQLIBDIRECTORY
+export COQTOP='COQTOPDIRECTORY'
+export COQLIB='COQLIBDIRECTORY'
export COQTH=$COQLIB/theories
-CAMLBIN=CAMLBINDIRECTORY
+CAMLBIN='CAMLBINDIRECTORY'
OCAMLDEBUG=$CAMLBIN/ocamldebug
export CAMLP4LIB=`$CAMLBIN/camlp4 -where`
diff --git a/dev/perf-analysis b/dev/perf-analysis
new file mode 100644
index 00000000..4295a573
--- /dev/null
+++ b/dev/perf-analysis
@@ -0,0 +1,51 @@
+Performance analysis for V8-0-bugfix branch
+-------------------------------------------
+
+ Dec 27, 2005: contrib Karatsuba added (~ 24s)
+
+Dec 1-14, 2005: benchmarking server down
+
+Nov 29 and Dec 16, 2005: size increase
+ due to new record flag in inductive for extraction
+
+ Oct 6, 2005: contribs IPC and Tait added (~ 22s and ~ 24s)
+
+ Aug 1, 2005: contrib Kildall added (~ 64s)
+
+Jul 26-Aug 2, 2005: bench down
+
+Jul 14-15, 2005: 4 contribs failed including CoRN
+
+ Jul 7, 2005: adding contrib Fermat4: but not compabible and remove on Jul 8
+
+ Jun 17, 2005: contrib Goodstein extended and moved to CantorOrdinals (~ 28s)
+
+Jun 4, 2005: significant time reduction
+ (e.g. Nijmegen/LinAlg: -15%, Nijmegen/QArith: stable; Nijmegen/CoRN: -1%)
+ only changes are the removal of an assert checking location and
+ the pre-definition of level 200 (could it be just a parsing improvement??)
+
+ May 19, 2005: contrib Goodstein and prfx (~ 9s) added
+
+Apr 30, 2005: evaluation order of atomic tactics changed
+ (e.g. Nijmegen/CoRN: stable, Nijmegen/QArith: -2%, Nijmegen/LinAlg: +20%)
+
+Mar 20, 2005: fixed Logic.with_check bug
+ improved whole V8-0-bugfix bench by 4 %
+ (e.g. Nijmegen/CoRN: - 7.5 %, Nijmegen/QARITH: - 1.5 %)
+
+Mar 7-10, 2005: unexplained time reduction
+ (on Mar 7, changed Ppconstrnew univ printer only)
+ (note also a server upgrade around Mar 10)
+
+Feb 17, 2005: fixed omega bug #922 (wrong STATE dependency):
+ improved whole V8-0-bugfix bench by 2 %
+ (e.g. Nijmegen/CoRN: - 6.5 %, Nijmegen/QARITH: - 3 %)
+
+Feb 2, 2005: fixed ltac var interpretation order
+
+ Jan 13, 2005: contrib SumOfTwoSquare added (~ 37s)
+
+Dec 20-29, 2004: reduced whole V8-0-bugfix due to Berkeley/Godel failure
+
+Nov 27 - Dec 10, 2004: strong instability
diff --git a/ide/coq.ico b/ide/coq.ico
new file mode 100644
index 00000000..390065bc
--- /dev/null
+++ b/ide/coq.ico
Binary files differ
diff --git a/ide/coq.ml b/ide/coq.ml
index e582f2d9..31f9829b 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: coq.ml,v 1.38.2.1 2004/07/16 19:30:20 herbelin Exp $ *)
+(* $Id: coq.ml,v 1.38.2.2 2005/11/16 17:22:38 barras Exp $ *)
open Vernac
open Vernacexpr
@@ -95,10 +95,10 @@ let is_in_coq_path f =
let _ = Library.locate_qualified_library
(Libnames.make_qualid Names.empty_dirpath
(Names.id_of_string base)) in
- prerr_endline (f ^ "is in coq path");
+ prerr_endline (f ^ " is in coq path");
true
with _ ->
- prerr_endline (f ^ "is NOT in coq path");
+ prerr_endline (f ^ " is NOT in coq path");
false
let is_in_proof_mode () =
diff --git a/ide/coq2.ico b/ide/coq2.ico
new file mode 100755
index 00000000..36964902
--- /dev/null
+++ b/ide/coq2.ico
Binary files differ
diff --git a/ide/coqide.ml b/ide/coqide.ml
index 08994010..a8179fb9 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: coqide.ml,v 1.99.2.3 2004/10/15 14:50:12 coq Exp $ *)
+(* $Id: coqide.ml,v 1.99.2.6 2006/01/06 13:22:36 barras Exp $ *)
open Preferences
open Vernacexpr
@@ -247,50 +247,43 @@ let break () =
prerr_endline " ignored (not computing)"
end
-let full_do_if_not_computing text f x =
- ignore
- (Thread.create
- (async
- (fun () ->
- if Mutex.try_lock coq_computing
- then
- begin
- prerr_endline ("Launching thread " ^ text);
- let w = Blaster_window.blaster_window () in
- if not (Mutex.try_lock w#lock) then begin
- break ();
- let lck = Mutex.create () in
- Mutex.lock lck;
- prerr_endline "Waiting on blaster...";
- Condition.wait w#blaster_killed lck;
- prerr_endline "Waiting on blaster ok";
- Mutex.unlock lck
- end else Mutex.unlock w#lock;
- let idle =
- Glib.Timeout.add ~ms:300
- ~callback:(fun () -> !pulse ();true) in
- begin
- prerr_endline "Getting lock";
- try
- f x;
- Glib.Timeout.remove idle;
- prerr_endline "Releasing lock";
- Mutex.unlock coq_computing;
- with e ->
- Glib.Timeout.remove idle;
- prerr_endline "Releasing lock (on error)";
- Mutex.unlock coq_computing;
- raise e
- end
- end
- else
- prerr_endline
- "Discarded order (computations are ongoing)"))
- ())
-
let do_if_not_computing text f x =
- ignore (full_do_if_not_computing text f x)
-
+ let threaded_task () =
+ if Mutex.try_lock coq_computing
+ then
+ begin
+ prerr_endline ("Launching thread " ^ text);
+ let w = Blaster_window.blaster_window () in
+ if not (Mutex.try_lock w#lock) then begin
+ break ();
+ let lck = Mutex.create () in
+ Mutex.lock lck;
+ prerr_endline "Waiting on blaster...";
+ Condition.wait w#blaster_killed lck;
+ prerr_endline "Waiting on blaster ok";
+ Mutex.unlock lck
+ end else Mutex.unlock w#lock;
+ let idle =
+ Glib.Timeout.add ~ms:300
+ ~callback:(fun () -> async !pulse ();true) in
+ begin
+ prerr_endline "Getting lock";
+ try
+ f x;
+ Glib.Timeout.remove idle;
+ prerr_endline "Releasing lock";
+ Mutex.unlock coq_computing;
+ with e ->
+ Glib.Timeout.remove idle;
+ prerr_endline "Releasing lock (on error)";
+ Mutex.unlock coq_computing;
+ raise e
+ end
+ end
+ else
+ prerr_endline
+ "Discarded order (computations are ongoing)" in
+ ignore (Thread.create threaded_task ())
let add_input_view tv =
Vector.append input_views tv
@@ -948,27 +941,9 @@ object(self)
end
method send_to_coq verbosely replace phrase show_output show_error localize =
- try
- full_goal_done <- false;
- prerr_endline "Send_to_coq starting now";
- if replace then begin
- let r,info =
-(* full_do_if_not_computing "coq eval and replace" *)
- Coq.interp_and_replace ("Info " ^ phrase)
- in
- let msg = read_stdout () in
- self#insert_message (if show_output then msg else "");
-
- Some r
-
- end else begin
- let r = Some (Coq.interp verbosely phrase) in
- let msg = read_stdout () in
- self#insert_message (if show_output then msg else "");
- r
- end
- with e ->
- (if show_error then
+ let display_output msg =
+ self#insert_message (if show_output then msg else "") in
+ let display_error e =
let (s,loc) = Coq.process_exn e in
assert (Glib.Utf8.validate s);
self#set_message s;
@@ -986,8 +961,23 @@ object(self)
input_buffer#apply_tag_by_name "error"
~start:starti
~stop:stopi;
- input_buffer#place_cursor starti;
- ));
+ input_buffer#place_cursor starti) in
+ try
+ full_goal_done <- false;
+ prerr_endline "Send_to_coq starting now";
+ if replace then begin
+ let r,info = Coq.interp_and_replace ("info " ^ phrase) in
+ let msg = read_stdout () in
+ sync display_output msg;
+ Some r
+ end else begin
+ let r = Coq.interp verbosely phrase in
+ let msg = read_stdout () in
+ sync display_output msg;
+ Some r
+ end
+ with e ->
+ if show_error then sync display_error e;
None
method find_phrase_starting_at (start:GText.iter) =
@@ -1068,149 +1058,148 @@ object(self)
method process_next_phrase verbosely display_goals do_highlight =
- begin
- try
- self#clear_message;
- prerr_endline "process_next_phrase starting now";
- if do_highlight then begin
- !push_info "Coq is computing";
- input_view#set_editable false;
- end;
- begin match (self#find_phrase_starting_at self#get_start_of_input)
- with
- | None ->
+ let get_next_phrase () =
+ self#clear_message;
+ prerr_endline "process_next_phrase starting now";
+ if do_highlight then begin
+ !push_info "Coq is computing";
+ input_view#set_editable false;
+ end;
+ match self#find_phrase_starting_at self#get_start_of_input with
+ | None ->
if do_highlight then begin
input_view#set_editable true;
!pop_info ();
- end; false
+ end;
+ None
| Some(start,stop) ->
prerr_endline "process_next_phrase : to_process highlight";
- let b = input_buffer in
if do_highlight then begin
input_buffer#apply_tag_by_name ~start ~stop "to_process";
prerr_endline "process_next_phrase : to_process applied";
end;
prerr_endline "process_next_phrase : getting phrase";
- let phrase = start#get_slice ~stop in
- let r =
- match self#send_to_coq verbosely false phrase true true true with
- | Some ast ->
- begin
- b#move_mark ~where:stop (`NAME "start_of_input");
- b#apply_tag_by_name "processed" ~start ~stop;
- if (self#get_insert#compare) stop <= 0 then
- begin
- b#place_cursor stop;
- self#recenter_insert
- end;
- let start_of_phrase_mark = `MARK (b#create_mark start) in
- let end_of_phrase_mark = `MARK (b#create_mark stop) in
- push_phrase
- start_of_phrase_mark
- end_of_phrase_mark ast;
- if display_goals then self#show_goals;
- true
- end
- | None -> false
- in
- if do_highlight then begin
- b#remove_tag_by_name ~start ~stop "to_process" ;
- input_view#set_editable true;
- !pop_info ();
- end;
- r;
- end
- with e -> raise e
+ Some((start,stop),start#get_slice ~stop) in
+ let remove_tag (start,stop) =
+ if do_highlight then begin
+ input_buffer#remove_tag_by_name ~start ~stop "to_process" ;
+ input_view#set_editable true;
+ !pop_info ();
+ end in
+ let mark_processed (start,stop) ast =
+ let b = input_buffer in
+ b#move_mark ~where:stop (`NAME "start_of_input");
+ b#apply_tag_by_name "processed" ~start ~stop;
+ if (self#get_insert#compare) stop <= 0 then
+ begin
+ b#place_cursor stop;
+ self#recenter_insert
+ end;
+ let start_of_phrase_mark = `MARK (b#create_mark start) in
+ let end_of_phrase_mark = `MARK (b#create_mark stop) in
+ push_phrase
+ start_of_phrase_mark
+ end_of_phrase_mark ast;
+ if display_goals then self#show_goals;
+ remove_tag (start,stop) in
+ begin
+ match sync get_next_phrase () with
+ | None -> false
+ | Some (loc,phrase) ->
+ (match self#send_to_coq verbosely false phrase true true true with
+ | Some ast -> sync (mark_processed loc) ast; true
+ | None -> sync remove_tag loc; false)
end
method insert_this_phrase_on_success
show_output show_msg localize coqphrase insertphrase =
- match self#send_to_coq false false coqphrase show_output show_msg localize with
- | Some ast ->
- begin
- let stop = self#get_start_of_input in
- if stop#starts_line then
- input_buffer#insert ~iter:stop insertphrase
- else input_buffer#insert ~iter:stop ("\n"^insertphrase);
- let start = self#get_start_of_input in
- input_buffer#move_mark ~where:stop (`NAME "start_of_input");
- input_buffer#apply_tag_by_name "processed" ~start ~stop;
- if (self#get_insert#compare) stop <= 0 then
- input_buffer#place_cursor stop;
- let start_of_phrase_mark = `MARK (input_buffer#create_mark start)
- in
- let end_of_phrase_mark = `MARK (input_buffer#create_mark stop) in
- push_phrase start_of_phrase_mark end_of_phrase_mark ast;
- self#show_goals;
- (*Auto insert save on success...
- try (match Coq.get_current_goals () with
- | [] ->
+ let mark_processed ast =
+ let stop = self#get_start_of_input in
+ if stop#starts_line then
+ input_buffer#insert ~iter:stop insertphrase
+ else input_buffer#insert ~iter:stop ("\n"^insertphrase);
+ let start = self#get_start_of_input in
+ input_buffer#move_mark ~where:stop (`NAME "start_of_input");
+ input_buffer#apply_tag_by_name "processed" ~start ~stop;
+ if (self#get_insert#compare) stop <= 0 then
+ input_buffer#place_cursor stop;
+ let start_of_phrase_mark = `MARK (input_buffer#create_mark start) in
+ let end_of_phrase_mark = `MARK (input_buffer#create_mark stop) in
+ push_phrase start_of_phrase_mark end_of_phrase_mark ast;
+ self#show_goals;
+ (*Auto insert save on success...
+ try (match Coq.get_current_goals () with
+ | [] ->
(match self#send_to_coq "Save.\n" true true true with
| Some ast ->
- begin
- let stop = self#get_start_of_input in
- if stop#starts_line then
- input_buffer#insert ~iter:stop "Save.\n"
- else input_buffer#insert ~iter:stop "\nSave.\n";
- let start = self#get_start_of_input in
- input_buffer#move_mark ~where:stop (`NAME "start_of_input");
- input_buffer#apply_tag_by_name "processed" ~start ~stop;
- if (self#get_insert#compare) stop <= 0 then
- input_buffer#place_cursor stop;
- let start_of_phrase_mark = `MARK (input_buffer#create_mark start)
- in
- let end_of_phrase_mark = `MARK (input_buffer#create_mark stop) in
- push_phrase start_of_phrase_mark end_of_phrase_mark ast
- end
+ begin
+ let stop = self#get_start_of_input in
+ if stop#starts_line then
+ input_buffer#insert ~iter:stop "Save.\n"
+ else input_buffer#insert ~iter:stop "\nSave.\n";
+ let start = self#get_start_of_input in
+ input_buffer#move_mark ~where:stop (`NAME "start_of_input");
+ input_buffer#apply_tag_by_name "processed" ~start ~stop;
+ if (self#get_insert#compare) stop <= 0 then
+ input_buffer#place_cursor stop;
+ let start_of_phrase_mark =
+ `MARK (input_buffer#create_mark start) in
+ let end_of_phrase_mark =
+ `MARK (input_buffer#create_mark stop) in
+ push_phrase start_of_phrase_mark end_of_phrase_mark ast
+ end
| None -> ())
- | _ -> ())
- with _ -> ()*)
- true
- end
- | None -> self#insert_message ("Unsuccessfully tried: "^coqphrase);
+ | _ -> ())
+ with _ -> ()*) in
+ match self#send_to_coq false false coqphrase show_output show_msg localize with
+ | Some ast -> sync mark_processed ast; true
+ | None ->
+ sync
+ (fun _ -> self#insert_message ("Unsuccessfully tried: "^coqphrase))
+ ();
false
method process_until_iter_or_error stop =
let stop' = `OFFSET stop#offset in
let start = self#get_start_of_input#copy in
let start' = `OFFSET start#offset in
- input_buffer#apply_tag_by_name
- ~start
- ~stop
- "to_process";
- input_view#set_editable false;
+ sync (fun _ ->
+ input_buffer#apply_tag_by_name ~start ~stop "to_process";
+ input_view#set_editable false) ();
!push_info "Coq is computing";
- process_pending ();
+(* process_pending ();*)
(try
while ((stop#compare self#get_start_of_input>=0)
&& (self#process_next_phrase false false false))
do Util.check_for_interrupt () done
with Sys.Break ->
prerr_endline "Interrupted during process_until_iter_or_error");
- self#show_goals;
- (* Start and stop might be invalid if an eol was added at eof *)
- let start = input_buffer#get_iter start' in
- let stop = input_buffer#get_iter stop' in
- input_buffer#remove_tag_by_name ~start ~stop "to_process" ;
- input_view#set_editable true;
+ sync (fun _ ->
+ self#show_goals;
+ (* Start and stop might be invalid if an eol was added at eof *)
+ let start = input_buffer#get_iter start' in
+ let stop = input_buffer#get_iter stop' in
+ input_buffer#remove_tag_by_name ~start ~stop "to_process" ;
+ input_view#set_editable true) ();
!pop_info()
method process_until_end_or_error =
self#process_until_iter_or_error input_buffer#end_iter
method reset_initial =
- Stack.iter
- (function inf ->
- let start = input_buffer#get_iter_at_mark inf.start in
- let stop = input_buffer#get_iter_at_mark inf.stop in
- input_buffer#move_mark ~where:start (`NAME "start_of_input");
- input_buffer#remove_tag_by_name "processed" ~start ~stop;
- input_buffer#delete_mark inf.start;
- input_buffer#delete_mark inf.stop;
- )
- processed_stack;
- Stack.clear processed_stack;
- self#clear_message;
+ sync (fun _ ->
+ Stack.iter
+ (function inf ->
+ let start = input_buffer#get_iter_at_mark inf.start in
+ let stop = input_buffer#get_iter_at_mark inf.stop in
+ input_buffer#move_mark ~where:start (`NAME "start_of_input");
+ input_buffer#remove_tag_by_name "processed" ~start ~stop;
+ input_buffer#delete_mark inf.start;
+ input_buffer#delete_mark inf.stop;
+ )
+ processed_stack;
+ Stack.clear processed_stack;
+ self#clear_message) ();
Coq.reset_initial ()
@@ -1260,19 +1249,21 @@ object(self)
(match undos with
| None -> synchro ()
| Some n -> try Pfedit.undo n with _ -> synchro ());
- let start = if is_empty () then input_buffer#start_iter
- else input_buffer#get_iter_at_mark (top ()).stop
- in
- prerr_endline "Removing (long) processed tag...";
- input_buffer#remove_tag_by_name
- ~start
- ~stop:self#get_start_of_input
- "processed";
- prerr_endline "Moving (long) start_of_input...";
- input_buffer#move_mark ~where:start (`NAME "start_of_input");
- self#show_goals;
- clear_stdout ();
- self#clear_message;
+ sync (fun _ ->
+ let start = if is_empty () then input_buffer#start_iter
+ else input_buffer#get_iter_at_mark (top ()).stop
+ in
+ prerr_endline "Removing (long) processed tag...";
+ input_buffer#remove_tag_by_name
+ ~start
+ ~stop:self#get_start_of_input
+ "processed";
+ prerr_endline "Moving (long) start_of_input...";
+ input_buffer#move_mark ~where:start (`NAME "start_of_input");
+ self#show_goals;
+ clear_stdout ();
+ self#clear_message)
+ ();
with _ ->
!push_info "WARNING: undo failed badly -> Coq might be in an inconsistent state.
Please restart and report NOW.";
@@ -1315,7 +1306,7 @@ Please restart and report NOW.";
begin match last_command with
| {ast=_, (VernacSolve _ | VernacTime (VernacSolve _))} ->
begin
- try Pfedit.undo 1; ignore (pop ()); update_input ()
+ try Pfedit.undo 1; ignore (pop ()); sync update_input ()
with _ -> self#backtrack_to_no_lock start
end
| {ast=_,t;reset_info=Reset (id, {contents=true})} ->
@@ -1326,7 +1317,7 @@ Please restart and report NOW.";
| VernacEndSegment _
-> reset_to_mod id
| _ -> reset_to id);
- update_input ()
+ sync update_input ()
| { ast = _, ( VernacStartTheoremProof _
| VernacGoal _
| VernacDeclareTacticDefinition _
@@ -1340,10 +1331,10 @@ Please restart and report NOW.";
prerr_endline "WARNING : found a closed environment";
raise e
end);
- update_input ()
+ sync update_input ()
| { ast = (_, a) } when is_state_preserving a ->
ignore (pop ());
- update_input ()
+ sync update_input ()
| _ ->
self#backtrack_to_no_lock start
end;
@@ -1356,7 +1347,6 @@ Please restart and report NOW.";
method blaster () =
-
ignore (Thread.create
(fun () ->
prerr_endline "Blaster called";
@@ -1375,14 +1365,14 @@ Please restart and report NOW.";
("Goal "^gnb)
s
(fun () -> try_interptac t')
- (fun () -> self#insert_command t'' t'')
+ (sync(fun () -> self#insert_command t'' t''))
in
let set_current_goal (s,t) =
c#set
"Goal 1"
s
(fun () -> try_interptac ("progress "^t))
- (fun () -> self#insert_command t t)
+ (sync(fun () -> self#insert_command t t))
in
begin match current_gls with
| [] -> ()
@@ -1405,11 +1395,11 @@ Please restart and report NOW.";
())
method insert_command cp ip =
- self#clear_message;
+ async(fun _ -> self#clear_message)();
ignore (self#insert_this_phrase_on_success true false false cp ip)
method tactic_wizard l =
- self#clear_message;
+ async(fun _ -> self#clear_message)();
ignore
(List.exists
(fun p ->
@@ -1742,11 +1732,11 @@ let main files =
~width:!current.window_width ~height:!current.window_height
~title:"CoqIde" ()
in
-(*
- let icon_image = Filename.concat lib_ide "coq.ico" in
- let icon = GdkPixbuf.from_file icon_image in
- w#set_icon (Some icon);
-*)
+ (try
+ let icon_image = lib_ide_file "coq2.ico" in
+ let icon = GdkPixbuf.from_file icon_image in
+ w#set_icon (Some icon)
+ with _ -> ());
let vbox = GPack.vbox ~homogeneous:false ~packing:w#add () in
@@ -2064,21 +2054,21 @@ let main files =
ignore (get_current_view()).view#clear_undo));
ignore(edit_f#add_separator ());
ignore(edit_f#add_item "Cut" ~key:GdkKeysyms._X ~callback:
- (do_if_not_computing "cut"
+ (do_if_not_computing "cut" (sync
(fun () -> GtkSignal.emit_unit
(get_current_view()).view#as_view
- GtkText.View.S.cut_clipboard)));
+ GtkText.View.S.cut_clipboard))));
ignore(edit_f#add_item "Copy" ~key:GdkKeysyms._C ~callback:
(fun () -> GtkSignal.emit_unit
(get_current_view()).view#as_view
GtkText.View.S.copy_clipboard));
ignore(edit_f#add_item "Paste" ~key:GdkKeysyms._V ~callback:
- (do_if_not_computing "paste"
+ (do_if_not_computing "paste" (sync
(fun () ->
try GtkSignal.emit_unit
(get_current_view()).view#as_view
GtkText.View.S.paste_clipboard
- with _ -> prerr_endline "EMIT PASTE FAILED")));
+ with _ -> prerr_endline "EMIT PASTE FAILED"))));
ignore (edit_f#add_separator ());
@@ -2322,12 +2312,12 @@ let main files =
*)
ignore(edit_f#add_item "Complete Word" ~key:GdkKeysyms._slash ~callback:
- (do_if_not_computing "complete word"
+ (do_if_not_computing "complete word" (sync
(fun () ->
ignore (
let av = out_some ((get_current_view()).analyzed_view) in
av#complete_at_offset (av#get_insert)#offset
- ))));
+ )))));
ignore(edit_f#add_separator ());
(* external editor *)
@@ -2352,7 +2342,7 @@ let main files =
(GMain.Timeout.add ~ms:!current.global_auto_revert_delay
~callback:
(fun () ->
- do_if_not_computing "revert" (fun () -> revert_f ()) ();
+ do_if_not_computing "revert" (sync revert_f) ();
true))
in reset_revert_timer (); (* to enable statup preferences timer *)
@@ -2375,7 +2365,7 @@ let main files =
(GMain.Timeout.add ~ms:!current.auto_save_delay
~callback:
(fun () ->
- do_if_not_computing "autosave" (fun () -> auto_save_f ()) ();
+ do_if_not_computing "autosave" (sync auto_save_f) ();
true))
in reset_auto_save_timer (); (* to enable statup preferences timer *)
@@ -2444,20 +2434,6 @@ let main files =
~key:GdkKeysyms._Up
~callback:(do_or_activate (fun a -> a#undo_last_step))
`GO_UP;
-(*
- add_to_menu_toolbar
- "_Forward to"
- ~tooltip:"Forward to"
- ~key:GdkKeysyms._Right
- ~callback:(do_or_activate (fun a -> a#process_until_insert_or_error))
- `GOTO_LAST;
- add_to_menu_toolbar
- "_Backward to"
- ~tooltip:"Backward to"
- ~key:GdkKeysyms._Left
- ~callback:(do_or_activate (fun a-> a#backtrack_to_insert))
- `GOTO_FIRST;
-*)
add_to_menu_toolbar
"_Go to"
~tooltip:"Go to cursor"
@@ -2581,9 +2557,9 @@ let main files =
in
ignore (factory#add_item menu_text
~callback:
- (do_if_not_computing "simple template"
+ (do_if_not_computing "simple template" (sync
(fun () -> let {view = view } = get_current_view () in
- ignore (view#buffer#insert_interactive text))))
+ ignore (view#buffer#insert_interactive text)))))
in
List.iter
(fun l ->
@@ -2616,7 +2592,7 @@ let main files =
in
let add_complex_template (menu_text, text, offset, len, key) =
(* Templates/Lemma *)
- let callback = do_if_not_computing "complex template"
+ let callback = do_if_not_computing "complex template" (sync
(fun () ->
let {view = view } = get_current_view () in
if view#buffer#insert_interactive text then begin
@@ -2625,7 +2601,7 @@ let main files =
view#buffer#move_mark `INSERT iter;
ignore (iter#nocopy#backward_chars len);
view#buffer#move_mark `SEL_BOUND iter;
- end)
+ end))
in
ignore (templates_factory#add_item menu_text ~callback ?key)
in
@@ -2695,9 +2671,9 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S);
in
ignore (factory#add_item menu_text
~callback:
- (do_if_not_computing "simple template"
+ (do_if_not_computing "simple template" (sync
(fun () -> let {view = view } = get_current_view () in
- ignore (view#buffer#insert_interactive text))))
+ ignore (view#buffer#insert_interactive text)))))
in
*)
ignore (templates_factory#add_separator ());
@@ -2897,7 +2873,7 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S);
let detach_menu = configuration_factory#add_item
"Detach _Script Window"
~callback:
- (do_if_not_computing "detach script window"
+ (do_if_not_computing "detach script window" (sync
(fun () ->
let nb = notebook () in
if nb#misc#toplevel#get_oid=w#coerce#get_oid then
@@ -2910,7 +2886,7 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S);
nw#add_accel_group accel_group;
nb#misc#reparent nw#coerce
end
- ))
+ )))
in
let detach_current_view =
configuration_factory#add_item
@@ -3208,7 +3184,7 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S);
let _ = tv2#event#connect#motion_notify
~callback:
(fun e ->
- (do_if_not_computing "motion notify"
+ (do_if_not_computing "motion notify" (sync
(fun e ->
let win = match tv2#get_window `WIDGET with
| None -> assert false
@@ -3231,7 +3207,7 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S);
it#as_iter))
tags;
false)) e;
- false)
+ false))
in
change_font :=
(fun fd ->
@@ -3243,7 +3219,7 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S);
);
let about (b:GText.buffer) =
(try
- let image = Filename.concat lib_ide "coq.png" in
+ let image = lib_ide_file "coq.ico" in
let startup_image = GdkPixbuf.from_file image in
b#insert_pixbuf ~iter:b#start_iter
~pixbuf:startup_image;
@@ -3291,7 +3267,7 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S);
(*
ignore (faq_m#connect#activate
~callback:(fun () ->
- load (Filename.concat lib_ide "FAQ")));
+ load (lib_ide_file "FAQ")));
*)
resize_window := (fun () ->
@@ -3360,7 +3336,7 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S);
let start () =
let files = Coq.init () in
ignore_break ();
- GtkMain.Rc.add_default_file (Filename.concat lib_ide ".coqide-gtk2rc");
+ GtkMain.Rc.add_default_file (lib_ide_file ".coqide-gtk2rc");
(try
GtkMain.Rc.add_default_file (Filename.concat System.home ".coqide-gtk2rc");
with Not_found -> ());
diff --git a/ide/ideutils.ml b/ide/ideutils.ml
index 8ec0e9e4..dc3bcf71 100644
--- a/ide/ideutils.ml
+++ b/ide/ideutils.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: ideutils.ml,v 1.30.2.1 2004/07/16 19:30:20 herbelin Exp $ *)
+(* $Id: ideutils.ml,v 1.30.2.4 2006/01/06 15:40:37 barras Exp $ *)
open Preferences
@@ -32,7 +32,12 @@ let prerr_endline s =
let prerr_string s =
if !debug then (prerr_string s;flush stderr)
-let lib_ide = Filename.concat Coq_config.coqlib "ide"
+let lib_ide_file f =
+ let coqlib =
+ if !Options.boot then Coq_config.coqtop
+ else
+ System.getenv_else "COQLIB" Coq_config.coqlib in
+ Filename.concat (Filename.concat coqlib "ide") f
let get_insert input_buffer = input_buffer#get_iter_at_mark `INSERT
@@ -210,10 +215,15 @@ let find_tag_stop (tag :GText.tag) (it:GText.iter) =
let find_tag_limits (tag :GText.tag) (it:GText.iter) =
(find_tag_start tag it , find_tag_stop tag it)
-(* explanations ?? *)
+(* explanations: Win32 threads won't work if events are produced
+ in a thread different from the thread of the Gtk loop. In this
+ case we must use GtkThread.async to push a callback in the
+ main thread. Beware that the synchronus version may produce
+ deadlocks. *)
let async =
- if Sys.os_type <> "Unix" then GtkThread.async else
- (fun x -> x)
+ if Sys.os_type = "Win32" then GtkThread.async else (fun x -> x)
+let sync =
+ if Sys.os_type = "Win32" then GtkThread.sync else (fun x -> x)
let stock_to_widget ?(size=`DIALOG) s =
let img = GMisc.image ()
@@ -254,7 +264,7 @@ let browse f url =
let url_for_keyword =
let ht = Hashtbl.create 97 in
begin try
- let cin = open_in (Filename.concat lib_ide "index_urls.txt") in
+ let cin = open_in (lib_ide_file "index_urls.txt") in
try while true do
let s = input_line cin in
try
diff --git a/ide/ideutils.mli b/ide/ideutils.mli
index d91faff4..cbdaefb9 100644
--- a/ide/ideutils.mli
+++ b/ide/ideutils.mli
@@ -6,9 +6,10 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: ideutils.mli,v 1.6.2.2 2005/01/21 17:21:33 herbelin Exp $ i*)
+(*i $Id: ideutils.mli,v 1.6.2.4 2005/11/25 17:18:28 barras Exp $ i*)
val async : ('a -> unit) -> 'a -> unit
+val sync : ('a -> 'b) -> 'a -> 'b
val browse : (string -> unit) -> string -> unit
val browse_keyword : (string -> unit) -> string -> unit
val byte_offset_to_char_offset : string -> int -> int
@@ -24,7 +25,7 @@ val get_insert : < get_iter_at_mark : [> `INSERT] -> 'a; .. > -> 'a
val is_char_start : char -> bool
-val lib_ide : string
+val lib_ide_file : string -> string
val my_stat : string -> Unix.stats option
val prerr_endline : string -> unit
diff --git a/ide/undo.ml b/ide/undo.ml
index 54449515..6f740667 100644
--- a/ide/undo.ml
+++ b/ide/undo.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: undo.ml,v 1.8.2.1 2004/07/16 19:30:21 herbelin Exp $ *)
+(* $Id: undo.ml,v 1.8.2.2 2005/11/16 17:22:39 barras Exp $ *)
open GText
open Ideutils
@@ -18,7 +18,7 @@ let neg act = match act with
| Insert (s,i,l) -> Delete (s,i,l)
| Delete (s,i,l) -> Insert (s,i,l)
-class undoable_view (tv:Gtk.text_view Gtk.obj) =
+class undoable_view (tv:[>Gtk.text_view] Gtk.obj) =
let undo_lock = ref true in
object(self)
inherit GText.view tv as super
diff --git a/ide/undo_lablgtk_ge26.mli b/ide/undo_lablgtk_ge26.mli
new file mode 100644
index 00000000..d81d08d5
--- /dev/null
+++ b/ide/undo_lablgtk_ge26.mli
@@ -0,0 +1,35 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+(*i $Id: undo_lablgtk_ge26.mli,v 1.1.2.1 2005/11/18 16:37:28 herbelin Exp $ i*)
+
+(* An undoable view class *)
+
+class undoable_view : [> Gtk.text_view] Gtk.obj ->
+object
+ inherit GText.view
+ method undo : bool
+ method redo : bool
+ method clear_undo : unit
+end
+
+val undoable_view :
+ ?buffer:GText.buffer ->
+ ?editable:bool ->
+ ?cursor_visible:bool ->
+ ?justification:GtkEnums.justification ->
+ ?wrap_mode:GtkEnums.wrap_mode ->
+ ?border_width:int ->
+ ?width:int ->
+ ?height:int ->
+ ?packing:(GObj.widget -> unit) ->
+ ?show:bool ->
+ unit ->
+ undoable_view
+
+
diff --git a/ide/undo.mli b/ide/undo_lablgtk_lt26.mli
index 11613fdb..9c2176b0 100644
--- a/ide/undo.mli
+++ b/ide/undo_lablgtk_lt26.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: undo.mli,v 1.4.2.2 2005/01/21 17:21:33 herbelin Exp $ i*)
+(*i $Id: undo_lablgtk_lt26.mli,v 1.1.2.1 2005/11/18 16:37:28 herbelin Exp $ i*)
(* An undoable view class *)
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 6692dca5..25167865 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: constrextern.ml,v 1.85.2.2 2004/07/16 19:30:22 herbelin Exp $ *)
+(* $Id: constrextern.ml,v 1.85.2.7 2006/01/05 12:00:35 herbelin Exp $ *)
(*i*)
open Pp
@@ -1333,7 +1333,8 @@ and extern_symbol_pattern (tmp_scope,scopes as allscopes) vars t = function
subst in
insert_pat_delimiters (make_pat_notation loc ntn l) key)
| SynDefRule kn ->
- CPatAtom (loc,Some (Qualid (loc, shortest_qualid_of_syndef kn)))
+ let qid = shortest_qualid_of_syndef vars kn in
+ CPatAtom (loc,Some (Qualid (loc, qid)))
with
No_match -> extern_symbol_pattern allscopes vars t rules
@@ -1494,21 +1495,38 @@ let rec share_fix_binders n rbl ty def =
| _ -> List.rev rbl, ty, def
(**********************************************************************)
+(* mapping rawterms to numerals (in presence of coercions, choose the *)
+(* one with no delimiter if possible) *)
+
+let extern_possible_numeral scopes r =
+ try
+ let (sc,n) = uninterp_numeral r in
+ match Symbols.availability_of_numeral sc (make_current_scopes scopes) with
+ | None -> None
+ | Some key -> Some (insert_delimiters (CNumeral(loc_of_rawconstr r,n)) key)
+ with No_match ->
+ None
+
+let extern_optimal_numeral scopes r r' =
+ let c = extern_possible_numeral scopes r in
+ let c' = if r==r' then None else extern_possible_numeral scopes r' in
+ match c,c' with
+ | Some n, (Some (CDelimiters _) | None) | _, Some n -> n
+ | _ -> raise No_match
+
+(**********************************************************************)
(* mapping rawterms to constr_expr *)
let rec extern inctx scopes vars r =
+ let r' = remove_coercions inctx r in
try
if !Options.raw_print or !print_no_symbol then raise No_match;
- extern_numeral (Rawterm.loc_of_rawconstr r)
- scopes (Symbols.uninterp_numeral r)
+ extern_optimal_numeral scopes r r'
with No_match ->
-
- let r = remove_coercions inctx r in
-
try
if !Options.raw_print or !print_no_symbol then raise No_match;
- extern_symbol scopes vars r (Symbols.uninterp_notations r)
- with No_match -> match r with
+ extern_symbol scopes vars r' (Symbols.uninterp_notations r')
+ with No_match -> match r' with
| RRef (loc,ref) ->
extern_global loc (implicits_of_global_out ref)
(extern_reference loc vars ref)
@@ -1605,13 +1623,15 @@ let rec extern inctx scopes vars r =
| RLetTuple (loc,nal,(na,typopt),tm,b) ->
CLetTuple (loc,nal,
- (Some na,option_app (extern_type scopes (add_vname vars na)) typopt),
+ (option_app (fun _ -> na) typopt,
+ option_app (extern_type scopes (add_vname vars na)) typopt),
sub_extern false scopes vars tm,
extern false scopes (List.fold_left add_vname vars nal) b)
| RIf (loc,c,(na,typopt),b1,b2) ->
CIf (loc,sub_extern false scopes vars c,
- (Some na,option_app (extern_type scopes (add_vname vars na)) typopt),
+ (option_app (fun _ -> na) typopt,
+ option_app (extern_type scopes (add_vname vars na)) typopt),
sub_extern false scopes vars b1, sub_extern false scopes vars b2)
| RRec (loc,fk,idv,blv,tyv,bv) ->
@@ -1709,11 +1729,6 @@ and extern_eqn inctx scopes vars (loc,ids,pl,c) =
(loc,List.map (extern_cases_pattern_in_scope scopes vars) pl,
extern inctx scopes vars c)
-and extern_numeral loc scopes (sc,n) =
- match Symbols.availability_of_numeral sc (make_current_scopes scopes) with
- | None -> raise No_match
- | Some key -> insert_delimiters (CNumeral (loc,n)) key
-
and extern_symbol (tmp_scope,scopes as allscopes) vars t = function
| [] -> raise No_match
| (keyrule,pat,n as rule)::rules ->
@@ -1745,7 +1760,7 @@ and extern_symbol (tmp_scope,scopes as allscopes) vars t = function
subst in
insert_delimiters (make_notation loc ntn l) key)
| SynDefRule kn ->
- CRef (Qualid (loc, shortest_qualid_of_syndef kn)) in
+ CRef (Qualid (loc, shortest_qualid_of_syndef vars kn)) in
if args = [] then e
else
(* TODO: compute scopt for the extra args, in case, head is a ref *)
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 222ea23b..bacdb387 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: constrintern.ml,v 1.58.2.6 2004/11/22 14:21:23 herbelin Exp $ *)
+(* $Id: constrintern.ml,v 1.58.2.7 2005/11/19 10:34:35 herbelin Exp $ *)
open Pp
open Util
@@ -621,10 +621,10 @@ let merge_impargs l args =
let check_projection isproj nargs r =
match (r,isproj) with
- | RRef (loc, ref), Some nth ->
+ | RRef (loc, ref), Some _ ->
(try
- let n = Recordops.find_projection_nparams ref in
- if nargs < nth then
+ let n = Recordops.find_projection_nparams ref + 1 in
+ if nargs < n then
user_err_loc (loc,"",str "Projection has not enough parameters");
with Not_found ->
user_err_loc
diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml
index ef887d88..ceda2b47 100644
--- a/interp/syntax_def.ml
+++ b/interp/syntax_def.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: syntax_def.ml,v 1.6.2.1 2004/07/16 19:30:23 herbelin Exp $ *)
+(* $Id: syntax_def.ml,v 1.6.2.2 2006/01/03 20:33:31 herbelin Exp $ *)
open Util
open Pp
@@ -39,10 +39,15 @@ let load_syntax_constant i ((sp,kn),(local,c,onlyparse)) =
add_syntax_constant kn c;
Nametab.push_syntactic_definition (Nametab.Until i) sp kn;
if not onlyparse then
+ (* Declare it to be used as (long) name *)
Symbols.declare_uninterpretation (Symbols.SynDefRule kn) ([],c)
-let open_syntax_constant i ((sp,kn),c) =
- Nametab.push_syntactic_definition (Nametab.Exactly i) sp kn
+let open_syntax_constant i ((sp,kn),(_,c,onlyparse)) =
+ Nametab.push_syntactic_definition (Nametab.Exactly i) sp kn;
+ if not onlyparse then
+ (* Redeclare it to be used as (short) name in case an other (distfix)
+ notation was declared inbetween *)
+ Symbols.declare_uninterpretation (Symbols.SynDefRule kn) ([],c)
let cache_syntax_constant d =
load_syntax_constant 1 d
diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index 8943b0b5..ac2c52cc 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: declarations.ml,v 1.31.2.1 2004/07/16 19:30:24 herbelin Exp $ i*)
+(*i $Id: declarations.ml,v 1.31.2.2 2005/11/29 21:40:51 letouzey Exp $ i*)
(*i*)
open Util
@@ -104,6 +104,7 @@ type one_inductive_body = {
}
type mutual_inductive_body = {
+ mind_record : bool;
mind_finite : bool;
mind_ntypes : int;
mind_hyps : section_context;
@@ -139,7 +140,8 @@ let subst_mind_packet sub mbp =
}
let subst_mind sub mib =
- { mind_finite = mib.mind_finite ;
+ { mind_record = mib.mind_record ;
+ mind_finite = mib.mind_finite ;
mind_ntypes = mib.mind_ntypes ;
mind_hyps = (assert (mib.mind_hyps=[]); []) ;
mind_packets = array_smartmap (subst_mind_packet sub) mib.mind_packets ;
diff --git a/kernel/declarations.mli b/kernel/declarations.mli
index c670fe9a..6cff3936 100644
--- a/kernel/declarations.mli
+++ b/kernel/declarations.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: declarations.mli,v 1.33.2.2 2005/01/21 16:41:49 herbelin Exp $ i*)
+(*i $Id: declarations.mli,v 1.33.2.3 2005/11/29 21:40:51 letouzey Exp $ i*)
(*i*)
open Names
@@ -77,6 +77,7 @@ type one_inductive_body = {
}
type mutual_inductive_body = {
+ mind_record : bool;
mind_finite : bool;
mind_ntypes : int;
mind_hyps : section_context;
diff --git a/kernel/entries.ml b/kernel/entries.ml
index d833499e..a3d3d336 100644
--- a/kernel/entries.ml
+++ b/kernel/entries.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: entries.ml,v 1.3.8.1 2004/07/16 19:30:25 herbelin Exp $ i*)
+(*i $Id: entries.ml,v 1.3.8.2 2005/11/29 21:40:51 letouzey Exp $ i*)
(*i*)
open Names
@@ -49,6 +49,7 @@ type one_inductive_entry = {
mind_entry_lc : constr list }
type mutual_inductive_entry = {
+ mind_entry_record : bool;
mind_entry_finite : bool;
mind_entry_inds : one_inductive_entry list }
diff --git a/kernel/entries.mli b/kernel/entries.mli
index edade51a..e9bc420e 100644
--- a/kernel/entries.mli
+++ b/kernel/entries.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: entries.mli,v 1.3.8.1 2004/07/16 19:30:25 herbelin Exp $ i*)
+(*i $Id: entries.mli,v 1.3.8.2 2005/11/29 21:40:51 letouzey Exp $ i*)
(*i*)
open Names
@@ -49,6 +49,7 @@ type one_inductive_entry = {
mind_entry_lc : constr list }
type mutual_inductive_entry = {
+ mind_entry_record : bool;
mind_entry_finite : bool;
mind_entry_inds : one_inductive_entry list }
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 88f837aa..0b1d49f5 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: indtypes.ml,v 1.59.2.1 2004/07/16 19:30:25 herbelin Exp $ *)
+(* $Id: indtypes.ml,v 1.59.2.4 2005/12/30 15:58:59 barras Exp $ *)
open Util
open Names
@@ -20,10 +20,14 @@ open Reduction
open Typeops
open Entries
-(* [check_constructors_names id s cl] checks that all the constructors names
- appearing in [l] are not present in the set [s], and returns the new set
- of names. The name [id] is the name of the current inductive type, used
- when reporting the error. *)
+(* Same as noccur_between but may perform reductions.
+ Could be refined more... *)
+let weaker_noccur_between env x nvars t =
+ if noccur_between x nvars t then Some t
+ else
+ let t' = whd_betadeltaiota env t in
+ if noccur_between x nvars t then Some t'
+ else None
(************************************************************************)
(* Various well-formedness check for inductive declarations *)
@@ -46,6 +50,11 @@ type inductive_error =
exception InductiveError of inductive_error
+(* [check_constructors_names id s cl] checks that all the constructors names
+ appearing in [l] are not present in the set [s], and returns the new set
+ of names. The name [id] is the name of the current inductive type, used
+ when reporting the error. *)
+
let check_constructors_names id =
let rec check idset = function
| [] -> idset
@@ -337,9 +346,10 @@ let check_positivity_one (env, _,ntypes,_ as ienv) hyps i indlc =
match kind_of_term x with
| Prod (na,b,d) ->
assert (largs = []);
- if not (noccur_between n ntypes b) then
- raise (IllFormedInd (LocalNonPos n));
- check_pos (ienv_push_var ienv (na, b, mk_norec)) d
+ (match weaker_noccur_between env n ntypes b with
+ None -> raise (IllFormedInd (LocalNonPos n));
+ | Some b ->
+ check_pos (ienv_push_var ienv (na, b, mk_norec)) d)
| Rel k ->
let (ra,rarg) =
try List.nth ra_env (k-1)
@@ -481,7 +491,7 @@ let allowed_sorts env issmall isunit = function
then logical_sorts else impredicative_sorts
else logical_sorts
-let build_inductive env env_ar finite inds recargs cst =
+let build_inductive env env_ar record finite inds recargs cst =
let ntypes = Array.length inds in
(* Compute the set of used section variables *)
let ids =
@@ -527,7 +537,8 @@ let build_inductive env env_ar finite inds recargs cst =
} in
let packets = array_map2 build_one_packet inds recargs in
(* Build the mutual inductive *)
- { mind_ntypes = ntypes;
+ { mind_record = record;
+ mind_ntypes = ntypes;
mind_finite = finite;
mind_hyps = hyps;
mind_packets = packets;
@@ -544,5 +555,6 @@ let check_inductive env mie =
(* Then check positivity conditions *)
let recargs = check_positivity env_arities inds in
(* Build the inductive packets *)
- build_inductive env env_arities mie.mind_entry_finite inds recargs cst
+ build_inductive env env_arities mie.mind_entry_record mie.mind_entry_finite
+ inds recargs cst
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 4f180599..0f8c0d54 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: safe_typing.ml,v 1.76.2.1 2004/07/16 19:30:26 herbelin Exp $ *)
+(* $Id: safe_typing.ml,v 1.76.2.2 2005/11/23 14:46:08 barras Exp $ *)
open Util
open Names
@@ -427,11 +427,13 @@ type compiled_library =
(* We check that only initial state Require's were performed before
[start_library] was called *)
+let is_empty senv =
+ senv.revsign = [] &&
+ senv.modinfo.msid = initial_msid &&
+ senv.modinfo.variant = NONE
+
let start_library dir senv =
- if not (senv.revsign = [] &&
- senv.modinfo.msid = initial_msid &&
- senv.modinfo.variant = NONE)
- then
+ if not (is_empty senv) then
anomaly "Safe_typing.start_library: environment should be empty";
let dir_path,l =
match (repr_dirpath dir) with
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index 84b98984..b973fcde 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: safe_typing.mli,v 1.33.2.1 2004/07/16 19:30:26 herbelin Exp $ i*)
+(*i $Id: safe_typing.mli,v 1.33.2.2 2005/11/23 14:46:08 barras Exp $ i*)
(*i*)
open Names
@@ -29,6 +29,8 @@ val env_of_safe_env : safe_environment -> Environ.env
val empty_environment : safe_environment
+val is_empty : safe_environment -> bool
+
(* Adding and removing local declarations (Local or Variables) *)
val push_named_assum :
identifier * types -> safe_environment ->
diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
index 825ae8fa..835226fb 100644
--- a/kernel/subtyping.ml
+++ b/kernel/subtyping.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: subtyping.ml,v 1.11.2.1 2004/07/16 19:30:26 herbelin Exp $ i*)
+(*i $Id: subtyping.ml,v 1.11.2.2 2005/11/29 21:40:52 letouzey Exp $ i*)
(*i*)
open Util
@@ -132,6 +132,34 @@ let check_inductive cst env msid1 l info1 mib2 spec2 =
in
if kn1 <> kn2 then error ()
end;
+ (* we check that records and their field names are preserved. *)
+ (* To stay compatible, we don't fail but only issue a warning. *)
+ if mib1.mind_record <> mib2.mind_record then begin
+ let sid = string_of_id mib1.mind_packets.(0).mind_typename in
+ Pp.warning
+ (sid^": record is implemented as an inductive type or conversely.\n"^
+ "Beware that extraction cannot handle this situation.\n")
+ end;
+ if mib1.mind_record then begin
+ let rec names_prod_letin t = match kind_of_term t with
+ | Prod(n,_,t) -> n::(names_prod_letin t)
+ | LetIn(n,_,_,t) -> n::(names_prod_letin t)
+ | Cast(t,_) -> names_prod_letin t
+ | _ -> []
+ in
+ assert (Array.length mib1.mind_packets = 1);
+ assert (Array.length mib2.mind_packets = 1);
+ assert (Array.length mib1.mind_packets.(0).mind_user_lc = 1);
+ assert (Array.length mib2.mind_packets.(0).mind_user_lc = 1);
+ let fields1 = names_prod_letin mib1.mind_packets.(0).mind_user_lc.(0)
+ and fields2 = names_prod_letin mib2.mind_packets.(0).mind_user_lc.(0) in
+ if fields1 <> fields2 then
+ let sid = string_of_id mib1.mind_packets.(0).mind_typename in
+ Pp.warning
+ (sid^": record has different field names in its signature and "^
+ "implemantation.\n"^
+ "Beware that extraction cannot handle this situation.\n");
+ end;
(* we first check simple things *)
let cst =
array_fold_left2 check_packet cst mib1.mind_packets mib2.mind_packets
diff --git a/kernel/univ.ml b/kernel/univ.ml
index d46609c8..5e9fbd81 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: univ.ml,v 1.17.10.1 2004/07/16 19:30:28 herbelin Exp $ *)
+(* $Id: univ.ml,v 1.17.10.3 2005/09/08 12:27:46 herbelin Exp $ *)
(* Universes are stratified by a partial ordering $\ge$.
Let $\~{}$ be the associated equivalence. We also have a strict ordering
@@ -57,7 +57,7 @@ let pr_uni = function
| Max (gel,gtl) ->
str "max(" ++
prlist_with_sep pr_coma pr_uni_level gel ++
- if gel <> [] & gtl <> [] then pr_coma () else mt () ++
+ (if gel <> [] & gtl <> [] then pr_coma () else mt ()) ++
prlist_with_sep pr_coma
(fun x -> str "(" ++ pr_uni_level x ++ str ")+1") gtl ++
str ")"
@@ -69,9 +69,8 @@ let super = function
| Variable u ->
Max ([],[u])
| Max _ ->
- anomaly ("Cannot take the successor of a non variable universes:\n"^
- "you are probably typing a type already known to be the type\n"^
- "of a user-provided term; if you really need this, please report")
+ anomaly ("Cannot take the successor of a non variable universes\n"^
+ "(maybe a bugged tactic)")
(* returns the least upper bound of universes u and v. If they are not
constrained, then a new universe is created.
@@ -412,6 +411,7 @@ let pr_arc = function
pr_uni_level u ++ str " " ++
v 0
(prlist_with_sep pr_spc (fun v -> str "> " ++ pr_uni_level v) gt ++
+ (if ge <> [] & gt <> [] then spc () else mt ()) ++
prlist_with_sep pr_spc (fun v -> str ">= " ++ pr_uni_level v) ge) ++
fnl ()
| Equiv (u,v) ->
diff --git a/lib/compat.ml4 b/lib/compat.ml4
index 0947f5fb..7ea3ff66 100644
--- a/lib/compat.ml4
+++ b/lib/compat.ml4
@@ -20,7 +20,9 @@ let unloc (b,e) =
let loc = (b.Lexing.pos_cnum,e.Lexing.pos_cnum) in
(* Ensure that we unpack a char location that was encoded as a line-col
location by make_loc *)
+(* Gram.Entry.parse may send bad loc in 3.08, see caml-bugs #2954
assert (dummy_loc = (b,e) or make_loc loc = (b,e));
+*)
loc
end
else
diff --git a/lib/gmapl.ml b/lib/gmapl.ml
index dcb2eb94..5eb4e110 100644
--- a/lib/gmapl.ml
+++ b/lib/gmapl.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: gmapl.ml,v 1.2.16.1 2004/07/16 19:30:29 herbelin Exp $ *)
+(* $Id: gmapl.ml,v 1.2.16.2 2006/01/03 20:31:16 herbelin Exp $ *)
open Util
@@ -21,7 +21,7 @@ let fold = Gmap.fold
let add x y m =
try
let l = Gmap.find x m in
- Gmap.add x (if List.mem y l then l else y::l) m
+ Gmap.add x (y::list_except y l) m
with Not_found ->
Gmap.add x [y] m
diff --git a/lib/system.ml b/lib/system.ml
index fd782fe6..9bbcc308 100644
--- a/lib/system.ml
+++ b/lib/system.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: system.ml,v 1.31.8.1 2004/07/16 19:30:31 herbelin Exp $ *)
+(* $Id: system.ml,v 1.31.8.3 2006/01/10 17:06:23 barras Exp $ *)
open Pp
open Util
@@ -22,6 +22,8 @@ let safe_getenv_def var def =
flush Pervasives.stdout;
def
+let getenv_else s dft = try Sys.getenv s with Not_found -> dft
+
let home = (safe_getenv_def "HOME" ".")
let safe_getenv n = safe_getenv_def n ("$"^n)
@@ -60,6 +62,34 @@ let glob s = expand_macros true s 0
type physical_path = string
type load_path = physical_path list
+(* Hints to partially detects if two paths refer to the same repertory *)
+let rec remove_path_dot p =
+ let curdir = Filename.concat Filename.current_dir_name "" in (* Unix: "./" *)
+ let n = String.length curdir in
+ if String.length p > n && String.sub p 0 n = curdir then
+ remove_path_dot (String.sub p n (String.length p - n))
+ else
+ p
+
+let strip_path p =
+ let cwd = Filename.concat (Sys.getcwd ()) "" in (* Unix: "`pwd`/" *)
+ let n = String.length cwd in
+ if String.length p > n && String.sub p 0 n = cwd then
+ remove_path_dot (String.sub p n (String.length p - n))
+ else
+ remove_path_dot p
+
+let canonical_path_name p =
+ let current = Sys.getcwd () in
+ try
+ Sys.chdir p;
+ let p' = Sys.getcwd () in
+ Sys.chdir current;
+ p'
+ with Sys_error _ ->
+ (* We give up to find a canonical name and just simplify it... *)
+ strip_path p
+
(* All subdirectories, recursively *)
let exists_dir dir =
diff --git a/lib/system.mli b/lib/system.mli
index 86d78b52..dc172b70 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,v 1.17.16.1 2004/07/16 19:30:31 herbelin Exp $ i*)
+(*i $Id: system.mli,v 1.17.16.3 2006/01/10 17:06:23 barras Exp $ 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
@@ -16,6 +16,8 @@
type physical_path = string
type load_path = physical_path list
+val canonical_path_name : string -> physical_path
+
val all_subdirs : unix_path:string -> (physical_path * string list) list
val is_in_path : load_path -> string -> bool
val where_in_path : load_path -> string -> physical_path * string
@@ -24,7 +26,7 @@ val make_suffix : string -> string -> string
val file_readable_p : string -> bool
val glob : string -> string
-
+val getenv_else : string -> string -> string
val home : string
val exists_dir : string -> bool
diff --git a/library/declare.ml b/library/declare.ml
index 8b9dfeda..cfa8890a 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: declare.ml,v 1.128.2.1 2004/07/16 19:30:34 herbelin Exp $ *)
+(* $Id: declare.ml,v 1.128.2.2 2005/11/29 21:40:52 letouzey Exp $ *)
open Pp
open Util
@@ -271,6 +271,7 @@ let dummy_one_inductive_entry mie = {
(* Hack to reduce the size of .vo: we keep only what load/open needs *)
let dummy_inductive_entry m = {
+ mind_entry_record = false;
mind_entry_finite = true;
mind_entry_inds = List.map dummy_one_inductive_entry m.mind_entry_inds }
diff --git a/library/declaremods.ml b/library/declaremods.ml
index b968a432..2e8fb0a7 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,v 1.18.2.1 2004/07/16 19:30:35 herbelin Exp $ i*)
+(*i $Id: declaremods.ml,v 1.18.2.2 2005/12/30 11:08:56 herbelin Exp $ i*)
open Pp
open Util
@@ -502,17 +502,17 @@ let end_module id =
let dir = fst oldprefix in
let msid = msid_of_prefix oldprefix in
- let substobjs = try
+ let substobjs, keep, special = try
match res_o with
| None ->
- empty_subst, mbids, msid, substitute
+ (empty_subst, mbids, msid, substitute), keep, special
| Some (MTEident ln) ->
- abstract_substobjs mbids (KNmap.find ln (!modtypetab))
+ abstract_substobjs mbids (KNmap.find ln (!modtypetab)), [], []
| Some (MTEsig (msid,_)) ->
todo "Anonymous signatures not supported";
- empty_subst, mbids, msid, []
+ (empty_subst, mbids, msid, []), keep, special
| Some (MTEwith _ as mty) ->
- abstract_substobjs mbids (get_modtype_substobjs mty)
+ abstract_substobjs mbids (get_modtype_substobjs mty), [], []
| Some (MTEfunsig _) ->
anomaly "Funsig cannot be here..."
with
diff --git a/library/global.ml b/library/global.ml
index bfa9335c..8694d7af 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: global.ml,v 1.43.2.1 2004/07/16 19:30:35 herbelin Exp $ *)
+(* $Id: global.ml,v 1.43.2.2 2005/11/23 14:46:17 barras Exp $ *)
open Util
open Names
@@ -25,6 +25,8 @@ let safe_env () = !global_env
let env () = env_of_safe_env !global_env
+let env_is_empty () = is_empty !global_env
+
let _ =
declare_summary "Global environment"
{ freeze_function = (fun () -> !global_env);
diff --git a/library/global.mli b/library/global.mli
index 1da5965c..007986d1 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: global.mli,v 1.40.2.1 2004/07/16 19:30:35 herbelin Exp $ i*)
+(*i $Id: global.mli,v 1.40.2.2 2005/11/23 14:46:17 barras Exp $ i*)
(*i*)
open Names
@@ -32,6 +32,8 @@ val env : unit -> Environ.env
val universes : unit -> universes
val named_context : unit -> Sign.named_context
+val env_is_empty : unit -> bool
+
(*s Extending env with variables and local definitions *)
val push_named_assum : (identifier * types) -> Univ.constraints
val push_named_def : (identifier * constr * types option) -> Univ.constraints
diff --git a/library/lib.ml b/library/lib.ml
index a9f864ef..c46634f4 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: lib.ml,v 1.63.2.3 2004/11/22 14:21:23 herbelin Exp $ *)
+(* $Id: lib.ml,v 1.63.2.4 2005/11/04 09:02:38 herbelin Exp $ *)
open Pp
open Util
@@ -555,8 +555,7 @@ let library_part ref =
let dir,_ = repr_path sp in
match ref with
| VarRef id ->
- anomaly "TODO";
- extract_dirpath_prefix (sections_depth ()) (cwd ())
+ anomaly "library_part not supported on local variables"
| _ ->
if is_dirpath_prefix_of dir (cwd ()) then
(* Not yet (fully) discharged *)
diff --git a/library/library.ml b/library/library.ml
index cbc8874a..aaed4545 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: library.ml,v 1.79.2.2 2004/11/17 14:01:26 herbelin Exp $ *)
+(* $Id: library.ml,v 1.79.2.5 2006/01/10 17:06:23 barras Exp $ *)
open Pp
open Util
@@ -29,53 +29,26 @@ let load_path = ref ([],[] : System.physical_path list * logical_path list)
let get_load_path () = fst !load_path
-(* Hints to partially detects if two paths refer to the same repertory *)
-let rec remove_path_dot p =
- let curdir = Filename.concat Filename.current_dir_name "" in (* Unix: "./" *)
- let n = String.length curdir in
- if String.length p > n && String.sub p 0 n = curdir then
- remove_path_dot (String.sub p n (String.length p - n))
- else
- p
-
-let strip_path p =
- let cwd = Filename.concat (Sys.getcwd ()) "" in (* Unix: "`pwd`/" *)
- let n = String.length cwd in
- if String.length p > n && String.sub p 0 n = cwd then
- remove_path_dot (String.sub p n (String.length p - n))
- else
- remove_path_dot p
-
-let canonical_path_name p =
- let current = Sys.getcwd () in
- try
- Sys.chdir p;
- let p' = Sys.getcwd () in
- Sys.chdir current;
- p'
- with Sys_error _ ->
- (* We give up to find a canonical name and just simplify it... *)
- strip_path p
-
let find_logical_path phys_dir =
- let phys_dir = canonical_path_name phys_dir in
+ let phys_dir = System.canonical_path_name phys_dir in
match list_filter2 (fun p d -> p = phys_dir) !load_path with
| _,[dir] -> dir
| _,[] -> Nameops.default_root_prefix
| _,l -> anomaly ("Two logical paths are associated to "^phys_dir)
let remove_path dir =
+ let dir = System.canonical_path_name dir in
load_path := list_filter2 (fun p d -> p <> dir) !load_path
let add_load_path_entry (phys_path,coq_path) =
- let phys_path = canonical_path_name phys_path in
+ let phys_path = System.canonical_path_name phys_path in
match list_filter2 (fun p d -> p = phys_path) !load_path with
| _,[dir] ->
if coq_path <> dir
(* If this is not the default -I . to coqtop *)
&& not
- (phys_path = canonical_path_name Filename.current_dir_name
+ (phys_path = System.canonical_path_name Filename.current_dir_name
&& coq_path = Nameops.default_root_prefix)
then
begin
@@ -290,8 +263,8 @@ let (in_import, out_import) =
(************************************************************************)
(*s Loading from disk to cache (preparation phase) *)
-let vo_magic_number7 = 07992 (* V8.0 final old syntax *)
-let vo_magic_number8 = 08002 (* V8.0 final new syntax *)
+let vo_magic_number7 = 07993 (* V8.0pl3 final old syntax *)
+let vo_magic_number8 = 08003 (* V8.0pl3 final new syntax *)
let (raw_extern_library7, raw_intern_library7) =
System.raw_extern_intern vo_magic_number7 ".vo"
@@ -453,13 +426,8 @@ let rec_intern_by_filename_only id f =
m.library_name
let locate_qualified_library qid =
- (* Look if loaded in current environment *)
- try
- let dir = Nametab.full_name_module qid in
- (LibLoaded, dir, library_full_filename dir)
- with Not_found ->
- (* Look if in loadpath *)
try
+ (* Search library in loadpath *)
let dir, base = repr_qualid qid in
let loadpath =
if repr_dirpath dir = [] then get_load_path ()
@@ -470,7 +438,12 @@ let locate_qualified_library qid =
if loadpath = [] then raise LibUnmappedDir;
let name = (string_of_id base)^".vo" in
let path, file = System.where_in_path loadpath name in
- (LibInPath, extend_dirpath (find_logical_path path) base, file)
+ let dir = extend_dirpath (find_logical_path path) base in
+ (* Look if loaded *)
+ try
+ (LibLoaded, dir, library_full_filename dir)
+ with Not_found ->
+ (LibInPath, dir, file)
with Not_found -> raise LibNotFound
let rec_intern_qualified_library (loc,qid) =
diff --git a/library/nametab.ml b/library/nametab.ml
index f009d867..4bd0cb3f 100755
--- a/library/nametab.ml
+++ b/library/nametab.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: nametab.ml,v 1.48.2.1 2004/07/16 19:30:36 herbelin Exp $ *)
+(* $Id: nametab.ml,v 1.48.2.2 2005/11/21 09:16:27 herbelin Exp $ *)
open Util
open Pp
@@ -472,9 +472,9 @@ let shortest_qualid_of_global ctx ref =
let sp = Globrevtab.find (TrueGlobal ref) !the_globrevtab in
SpTab.shortest_qualid ctx sp !the_ccitab
-let shortest_qualid_of_syndef kn =
+let shortest_qualid_of_syndef ctx kn =
let sp = sp_of_syntactic_definition kn in
- SpTab.shortest_qualid Idset.empty sp !the_ccitab
+ SpTab.shortest_qualid ctx sp !the_ccitab
let shortest_qualid_of_module mp =
let dir = MPmap.find mp !the_modrevtab in
diff --git a/library/nametab.mli b/library/nametab.mli
index 08a9d1bb..4cea1d40 100755
--- a/library/nametab.mli
+++ b/library/nametab.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: nametab.mli,v 1.43.2.2 2005/01/21 16:41:51 herbelin Exp $ i*)
+(*i $Id: nametab.mli,v 1.43.2.3 2005/11/21 09:16:27 herbelin Exp $ i*)
(*i*)
open Util
@@ -144,7 +144,7 @@ val full_name_module : qualid -> dir_path
val sp_of_syntactic_definition : kernel_name -> section_path
val shortest_qualid_of_global : Idset.t -> global_reference -> qualid
-val shortest_qualid_of_syndef : kernel_name -> qualid
+val shortest_qualid_of_syndef : Idset.t -> kernel_name -> qualid
val shortest_qualid_of_tactic : ltac_constant -> qualid
val dir_of_mp : module_path -> dir_path
diff --git a/parsing/egrammar.ml b/parsing/egrammar.ml
index 7a151c1a..09889d40 100644
--- a/parsing/egrammar.ml
+++ b/parsing/egrammar.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: egrammar.ml,v 1.48.2.3 2004/11/26 19:37:59 herbelin Exp $ *)
+(* $Id: egrammar.ml,v 1.48.2.4 2005/12/23 22:16:46 herbelin Exp $ *)
open Pp
open Util
@@ -30,12 +30,13 @@ type all_grammar_command =
| TacticGrammar of
(string * (string * grammar_production list) *
(Names.dir_path * Tacexpr.raw_tactic_expr))
- list
+ list * (string * Genarg.argument_type list *
+ (string * Pptactic.grammar_terminals)) list
let subst_all_grammar_command subst = function
| Notation _ -> anomaly "Notation not in GRAMMAR summary"
| Grammar gc -> Grammar (subst_grammar_command subst gc)
- | TacticGrammar g -> TacticGrammar g (* TODO ... *)
+ | TacticGrammar (g,p) -> TacticGrammar (g,p) (* TODO ... *)
let (grammar_state : all_grammar_command list ref) = ref []
@@ -419,7 +420,7 @@ let extend_grammar gram =
(match gram with
| Notation (_,a) -> extend_constr_notation a
| Grammar g -> extend_grammar_rules g
- | TacticGrammar l -> add_tactic_entries l);
+ | TacticGrammar (l,_) -> add_tactic_entries l);
grammar_state := gram :: !grammar_state
let reset_extend_grammars_v8 () =
diff --git a/parsing/egrammar.mli b/parsing/egrammar.mli
index 0009b4b6..ade91453 100644
--- a/parsing/egrammar.mli
+++ b/parsing/egrammar.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: egrammar.mli,v 1.14.2.5 2004/11/27 09:25:44 herbelin Exp $ i*)
+(*i $Id: egrammar.mli,v 1.14.2.6 2005/12/23 22:16:46 herbelin Exp $ i*)
(*i*)
open Util
@@ -28,7 +28,8 @@ type all_grammar_command =
| TacticGrammar of
(string * (string * grammar_production list) *
(Names.dir_path * Tacexpr.raw_tactic_expr))
- list
+ list * (string * Genarg.argument_type list *
+ (string * Pptactic.grammar_terminals)) list
val extend_grammar : all_grammar_command -> unit
diff --git a/parsing/g_constrnew.ml4 b/parsing/g_constrnew.ml4
index adc26532..fe579e98 100644
--- a/parsing/g_constrnew.ml4
+++ b/parsing/g_constrnew.ml4
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: g_constrnew.ml4,v 1.41.2.2 2004/11/17 12:48:35 herbelin Exp $ *)
+(* $Id: g_constrnew.ml4,v 1.41.2.4 2005/09/21 14:47:33 herbelin Exp $ *)
open Pcoq
open Constr
@@ -285,7 +285,9 @@ GEXTEND Gram
[ [ pl = LIST1 pattern SEP ","; "=>"; rhs = lconstr -> (loc,pl,rhs) ] ]
;
pattern:
- [ "10" LEFTA
+ [ "200" RIGHTA [ ]
+ | "99" RIGHTA [ ]
+ | "10" LEFTA
[ p = pattern ; lp = LIST1 (pattern LEVEL "0") ->
(match p with
| CPatAtom (_, Some r) -> CPatCstr (loc, r, lp)
diff --git a/parsing/g_ltacnew.ml4 b/parsing/g_ltacnew.ml4
index 9c8d1675..7492ac8c 100644
--- a/parsing/g_ltacnew.ml4
+++ b/parsing/g_ltacnew.ml4
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: g_ltacnew.ml4,v 1.22.2.2 2004/07/16 19:30:38 herbelin Exp $ *)
+(* $Id: g_ltacnew.ml4,v 1.22.2.3 2005/06/21 15:31:12 herbelin Exp $ *)
open Pp
open Util
@@ -43,7 +43,7 @@ let tactic_expr = Gram.Entry.create "tactic:tactic_expr"
if not !Options.v7 then
GEXTEND Gram
- GLOBAL: tactic Vernac_.command tactic_expr tactic_arg;
+ GLOBAL: tactic Vernac_.command tactic_expr tactic_arg constr_may_eval;
tactic_expr:
[ "5" LEFTA
@@ -108,14 +108,20 @@ GEXTEND Gram
| c = Constr.constr -> ConstrMayEval (ConstrTerm c) ] ]
;
may_eval_arg:
+ [ [ c = constr_eval -> ConstrMayEval c
+ | IDENT "fresh"; s = OPT STRING -> TacFreshId s ] ]
+ ;
+ constr_eval:
[ [ IDENT "eval"; rtc = red_expr; "in"; c = Constr.constr ->
- ConstrMayEval (ConstrEval (rtc,c))
+ ConstrEval (rtc,c)
| IDENT "context"; id = identref; "["; c = Constr.lconstr; "]" ->
- ConstrMayEval (ConstrContext (id,c))
+ ConstrContext (id,c)
| IDENT "type"; IDENT "of"; c = Constr.constr ->
- ConstrMayEval (ConstrTypeOf c)
- | IDENT "fresh"; s = OPT STRING ->
- TacFreshId s ] ]
+ ConstrTypeOf c ] ]
+ ;
+ constr_may_eval: (* For extensions *)
+ [ [ c = constr_eval -> c
+ | c = Constr.constr -> ConstrTerm c ] ]
;
tactic_atom:
[ [ id = METAIDENT -> MetaIdArg (loc,id)
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index a1559572..fd64defc 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: g_tactic.ml4,v 1.83.2.4 2005/01/15 14:56:53 herbelin Exp $ *)
+(* $Id: g_tactic.ml4,v 1.83.2.5 2005/05/15 12:47:04 herbelin Exp $ *)
open Pp
open Ast
@@ -306,14 +306,14 @@ GEXTEND Gram
(* Automation tactic *)
| IDENT "Trivial"; db = hintbases -> TacTrivial db
- | IDENT "Auto"; n = OPT natural; db = hintbases -> TacAuto (n, db)
+ | IDENT "Auto"; n = OPT int_or_var; db = hintbases -> TacAuto (n, db)
| IDENT "AutoTDB"; n = OPT natural -> TacAutoTDB n
| IDENT "CDHyp"; id = identref -> TacDestructHyp (true,id)
| IDENT "DHyp"; id = identref -> TacDestructHyp (false,id)
| IDENT "DConcl" -> TacDestructConcl
| IDENT "SuperAuto"; l = autoargs -> TacSuperAuto l
- | IDENT "Auto"; n = OPT natural; IDENT "Decomp"; p = OPT natural ->
+ | IDENT "Auto"; n = OPT int_or_var; IDENT "Decomp"; p = OPT natural ->
TacDAuto (n, p)
(* Context management *)
diff --git a/parsing/g_tacticnew.ml4 b/parsing/g_tacticnew.ml4
index 643be98d..5ffd2fd7 100644
--- a/parsing/g_tacticnew.ml4
+++ b/parsing/g_tacticnew.ml4
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: g_tacticnew.ml4,v 1.35.2.6 2005/01/15 14:56:53 herbelin Exp $ *)
+(* $Id: g_tacticnew.ml4,v 1.35.2.7 2005/05/15 12:47:05 herbelin Exp $ *)
open Pp
open Ast
@@ -340,7 +340,7 @@ GEXTEND Gram
(* Automation tactic *)
| IDENT "trivial"; db = hintbases -> TacTrivial db
- | IDENT "auto"; n = OPT natural; db = hintbases -> TacAuto (n, db)
+ | IDENT "auto"; n = OPT int_or_var; db = hintbases -> TacAuto (n, db)
(* Obsolete since V8.0
| IDENT "autotdb"; n = OPT natural -> TacAutoTDB n
@@ -349,7 +349,7 @@ GEXTEND Gram
| IDENT "dconcl" -> TacDestructConcl
| IDENT "superauto"; l = autoargs -> TacSuperAuto l
*)
- | IDENT "auto"; n = OPT natural; IDENT "decomp"; p = OPT natural ->
+ | IDENT "auto"; n = OPT int_or_var; IDENT "decomp"; p = OPT natural ->
TacDAuto (n, p)
(* Context management *)
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4
index b5ab2387..a8922536 100644
--- a/parsing/pcoq.ml4
+++ b/parsing/pcoq.ml4
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: pcoq.ml4,v 1.80.2.3 2005/01/15 14:56:53 herbelin Exp $ i*)
+(*i $Id: pcoq.ml4,v 1.80.2.4 2005/06/21 15:31:12 herbelin Exp $ i*)
open Pp
open Util
@@ -379,7 +379,8 @@ module Tactic =
make_gen_entry utactic rawwit_constr_with_bindings "constr_with_bindings"
let bindings =
make_gen_entry utactic rawwit_bindings "bindings"
- let constrarg = make_gen_entry utactic rawwit_constr_may_eval "constrarg"
+(*v7*) let constrarg = make_gen_entry utactic rawwit_constr_may_eval "constrarg"
+(*v8*) let constr_may_eval = make_gen_entry utactic rawwit_constr_may_eval "constr_may_eval"
let quantified_hypothesis =
make_gen_entry utactic rawwit_quant_hyp "quantified_hypothesis"
let int_or_var = make_gen_entry utactic rawwit_int_or_var "int_or_var"
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 361137f4..15a2c2cc 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: pcoq.mli,v 1.63.2.2 2005/01/15 14:56:53 herbelin Exp $ i*)
+(*i $Id: pcoq.mli,v 1.63.2.3 2005/06/21 15:31:12 herbelin Exp $ i*)
open Util
open Names
@@ -160,7 +160,8 @@ module Tactic :
val castedopenconstr : open_constr_expr Gram.Entry.e
val constr_with_bindings : constr_expr with_bindings Gram.Entry.e
val bindings : constr_expr bindings Gram.Entry.e
- val constrarg : (constr_expr,reference) may_eval Gram.Entry.e
+(*v7*) val constrarg : (constr_expr,reference) may_eval Gram.Entry.e
+(*v8*) val constr_may_eval : (constr_expr,reference) may_eval Gram.Entry.e
val quantified_hypothesis : quantified_hypothesis Gram.Entry.e
val int_or_var : int or_var Gram.Entry.e
val red_expr : raw_red_expr Gram.Entry.e
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml
index 1d7a9428..4103ea00 100644
--- a/parsing/pptactic.ml
+++ b/parsing/pptactic.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: pptactic.ml,v 1.54.2.3 2005/01/15 14:56:53 herbelin Exp $ *)
+(* $Id: pptactic.ml,v 1.54.2.5 2005/12/23 22:16:46 herbelin Exp $ *)
open Pp
open Names
@@ -42,6 +42,8 @@ let declare_extra_tactic_pprule for_v8 s (tags,prods) =
Hashtbl.add prtac_tab_v7 (s,tags) prods;
if for_v8 then Hashtbl.add prtac_tab (s,tags) prods
+let exists_extra_tactic_pprule s tags = Hashtbl.mem prtac_tab_v7 (s,tags)
+
type 'a raw_extra_genarg_printer =
(constr_expr -> std_ppcmds) -> (raw_tactic_expr -> std_ppcmds) ->
'a -> std_ppcmds
@@ -536,7 +538,8 @@ and pr_atom1 = function
| TacTrivial (Some []) as x -> pr_atom0 x
| TacTrivial db -> hov 0 (str "Trivial" ++ pr_hintbases db)
| TacAuto (None,Some []) as x -> pr_atom0 x
- | TacAuto (n,db) -> hov 0 (str "Auto" ++ pr_opt int n ++ pr_hintbases db)
+ | TacAuto (n,db) ->
+ hov 0 (str "Auto" ++ pr_opt (pr_or_var int) n ++ pr_hintbases db)
| TacAutoTDB None as x -> pr_atom0 x
| TacAutoTDB (Some n) -> hov 0 (str "AutoTDB" ++ spc () ++ int n)
| TacDestructHyp (true,(_,id)) -> hov 0 (str "CDHyp" ++ spc () ++ pr_id id)
@@ -546,7 +549,8 @@ and pr_atom1 = function
hov 1 (str "SuperAuto" ++ pr_opt int n ++ pr_autoarg_adding l ++
pr_autoarg_destructing b1 ++ pr_autoarg_usingTDB b2)
| TacDAuto (n,p) ->
- hov 1 (str "Auto" ++ pr_opt int n ++ str "Decomp" ++ pr_opt int p)
+ hov 1 (str "Auto" ++ pr_opt (pr_or_var int) n ++ str "Decomp" ++
+ pr_opt int p)
(* Context management *)
| TacClear l ->
diff --git a/parsing/pptactic.mli b/parsing/pptactic.mli
index b9cf7401..5c3035ba 100644
--- a/parsing/pptactic.mli
+++ b/parsing/pptactic.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: pptactic.mli,v 1.9.2.2 2005/01/21 17:19:37 herbelin Exp $ i*)
+(*i $Id: pptactic.mli,v 1.9.2.3 2005/12/23 22:16:46 herbelin Exp $ i*)
open Pp
open Genarg
@@ -46,6 +46,8 @@ type grammar_terminals = string option list
val declare_extra_tactic_pprule : bool -> string ->
argument_type list * (string * grammar_terminals) -> unit
+val exists_extra_tactic_pprule : string -> argument_type list -> bool
+
val pr_match_pattern : ('a -> std_ppcmds) -> 'a match_pattern -> std_ppcmds
val pr_match_rule : bool -> ('a -> std_ppcmds) -> ('b -> std_ppcmds) ->
diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml
index 169eff94..1505745c 100644
--- a/parsing/prettyp.ml
+++ b/parsing/prettyp.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: prettyp.ml,v 1.50.2.1 2004/07/16 19:30:40 herbelin Exp $ *)
+(* $Id: prettyp.ml,v 1.50.2.2 2005/11/21 09:16:28 herbelin Exp $ *)
open Pp
open Util
@@ -180,8 +180,10 @@ let print_located_qualid ref =
let (loc,qid) = qualid_of_reference ref in
let module N = Nametab in
let expand = function
- | TrueGlobal ref -> Term ref, N.shortest_qualid_of_global Idset.empty ref
- | SyntacticDef kn -> Syntactic kn, N.shortest_qualid_of_syndef kn in
+ | TrueGlobal ref ->
+ Term ref, N.shortest_qualid_of_global Idset.empty ref
+ | SyntacticDef kn ->
+ Syntactic kn, N.shortest_qualid_of_syndef Idset.empty kn in
match List.map expand (N.extended_locate_all qid) with
| [] ->
let (dir,id) = repr_qualid qid in
@@ -329,7 +331,7 @@ let print_constant_with_infos sp =
let print_inductive sp = (print_mutual sp)
let print_syntactic_def sep kn =
- let qid = Nametab.shortest_qualid_of_syndef kn in
+ let qid = Nametab.shortest_qualid_of_syndef Idset.empty kn in
let c = Syntax_def.search_syntactic_definition dummy_loc kn in
(str (if !Options.v7 then "Syntactic Definition " else "Notation ")
++ pr_qualid qid ++ str sep ++
diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4
index a278e3d5..e8e1830a 100644
--- a/parsing/q_coqast.ml4
+++ b/parsing/q_coqast.ml4
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: q_coqast.ml4,v 1.47.2.5 2005/01/15 14:56:54 herbelin Exp $ *)
+(* $Id: q_coqast.ml4,v 1.47.2.6 2005/05/15 12:47:05 herbelin Exp $ *)
open Util
open Names
@@ -454,7 +454,7 @@ let rec mlexpr_of_atomic_tactic = function
(* Automation tactics *)
| Tacexpr.TacAuto (n,l) ->
- let n = mlexpr_of_option mlexpr_of_int n in
+ let n = mlexpr_of_option (mlexpr_of_or_var mlexpr_of_int) n in
let l = mlexpr_of_option (mlexpr_of_list mlexpr_of_string) l in
<:expr< Tacexpr.TacAuto $n$ $l$ >>
(*
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 378eee30..4aff508f 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: cases.ml,v 1.111.2.4 2004/12/09 20:07:01 herbelin Exp $ *)
+(* $Id: cases.ml,v 1.111.2.5 2005/04/29 16:31:03 herbelin Exp $ *)
open Util
open Names
@@ -171,10 +171,7 @@ let pred_case_ml env sigma isrec (IndType (indf,realargs)) (i,ft) =
open Pp
let mssg_may_need_inversion () =
- str "This pattern-matching is not exhaustive."
-
-let mssg_this_case_cannot_occur () =
- "This pattern-matching is not exhaustive."
+ str "Found a matching with no clauses on a term unknown to have an empty inductive type"
(* Utils *)
let make_anonymous_patvars =
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index f214388f..be78eb2c 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -5,7 +5,7 @@
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: coercion.ml,v 1.38.6.1 2004/07/16 19:30:44 herbelin Exp $ *)
+(* $Id: coercion.ml,v 1.38.6.2 2005/11/29 21:40:52 letouzey Exp $ *)
open Util
open Names
@@ -60,10 +60,6 @@ let inh_pattern_coerce_to loc pat ind1 ind2 =
(* appliquer le chemin de coercions p à hj *)
let apply_coercion env p hj typ_cl =
- if !compter then begin
- nbpathc := !nbpathc +1;
- nbcoer := !nbcoer + (List.length p)
- end;
try
fst (List.fold_left
(fun (ja,typ_cl) i ->
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 41f63ace..040a185e 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: detyping.ml,v 1.75.2.4 2004/07/16 19:30:44 herbelin Exp $ *)
+(* $Id: detyping.ml,v 1.75.2.5 2005/09/06 14:30:41 herbelin Exp $ *)
open Pp
open Util
@@ -446,7 +446,7 @@ and detype_eqn tenv avoid env constr construct_nargs branch =
let make_pat x avoid env b ids =
if force_wildcard () & noccurn 1 b then
PatVar (dummy_loc,Anonymous),avoid,(add_name Anonymous env),ids
- else
+ else
let id = next_name_away_with_default "x" x avoid in
PatVar (dummy_loc,Name id),id::avoid,(add_name (Name id) env),id::ids
in
@@ -487,6 +487,6 @@ and detype_binder tenv bk avoid env na ty c =
concrete_name (fst tenv) avoid env na c in
let r = detype tenv avoid' (add_name na' env) c in
match bk with
- | BProd -> RProd (dummy_loc, na',detype tenv [] env ty, r)
- | BLambda -> RLambda (dummy_loc, na',detype tenv [] env ty, r)
- | BLetIn -> RLetIn (dummy_loc, na',detype tenv [] env ty, r)
+ | BProd -> RProd (dummy_loc, na',detype tenv avoid env ty, r)
+ | BLambda -> RLambda (dummy_loc, na',detype tenv avoid env ty, r)
+ | BLetIn -> RLetIn (dummy_loc, na',detype tenv avoid env ty, r)
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 0ee95a0f..2264f82b 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: evarconv.ml,v 1.44.6.2 2004/11/26 23:51:39 herbelin Exp $ *)
+(* $Id: evarconv.ml,v 1.44.6.3 2005/11/29 21:40:52 letouzey Exp $ *)
open Util
open Names
@@ -380,21 +380,16 @@ and conv_record env isevars (c,bs,(params,params1),(us,us2),(ts,ts1),c1) =
(new_isevar isevars env dloc (substl ks b)) :: ks)
[] bs
in
- if (list_for_all2eq
- (fun u1 u -> evar_conv_x env isevars CONV u1 (substl ks u))
- us2 us)
- &
- (list_for_all2eq
- (fun x1 x -> evar_conv_x env isevars CONV x1 (substl ks x))
- params1 params)
- & (list_for_all2eq (evar_conv_x env isevars CONV) ts ts1)
- & (evar_conv_x env isevars CONV c1 (applist (c,(List.rev ks))))
- then
- (*TR*) (if !compter then (nbstruc:=!nbstruc+1;
- nbimplstruc:=!nbimplstruc+(List.length ks);true)
- else true)
- else false
-
+ (list_for_all2eq
+ (fun u1 u -> evar_conv_x env isevars CONV u1 (substl ks u))
+ us2 us)
+ &
+ (list_for_all2eq
+ (fun x1 x -> evar_conv_x env isevars CONV x1 (substl ks x))
+ params1 params)
+ & (list_for_all2eq (evar_conv_x env isevars CONV) ts ts1)
+ & (evar_conv_x env isevars CONV c1 (applist (c,(List.rev ks))))
+
let the_conv_x env isevars t1 t2 = evar_conv_x env isevars CONV t1 t2
let the_conv_x_leq env isevars t1 t2 = evar_conv_x env isevars CUMUL t1 t2
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 36df9c8a..bb0e74bb 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: pretyping.ml,v 1.123.2.3 2004/07/16 19:30:45 herbelin Exp $ *)
+(* $Id: pretyping.ml,v 1.123.2.5 2005/11/29 21:40:52 letouzey Exp $ *)
open Pp
open Util
@@ -162,13 +162,13 @@ let strip_meta id = (* For Grammar v7 compatibility *)
let pretype_id loc env (lvar,unbndltacvars) id =
let id = strip_meta id in (* May happen in tactics defined by Grammar *)
try
- List.assoc id lvar
- with Not_found ->
- try
let (n,typ) = lookup_rel_id id (rel_context env) in
{ uj_val = mkRel n; uj_type = type_app (lift n) typ }
with Not_found ->
try
+ List.assoc id lvar
+ with Not_found ->
+ try
let (_,_,typ) = lookup_named id env in
{ uj_val = mkVar id; uj_type = typ }
with Not_found ->
@@ -238,7 +238,6 @@ let rec pretype tycon env isevars lvar = function
anomaly "Found a pattern variable in a rawterm to type"
| RHole (loc,k) ->
- if !compter then nbimpl:=!nbimpl+1;
(match tycon with
| Some ty ->
{ uj_val = new_isevar isevars env (loc,k) ty; uj_type = ty }
@@ -892,7 +891,6 @@ let rec pretype tycon env isevars lvar = function
(* [pretype_type valcon env isevars lvar c] coerces [c] into a type *)
and pretype_type valcon env isevars lvar = function
| RHole loc ->
- if !compter then nbimpl:=!nbimpl+1;
(match valcon with
| Some v ->
let s =
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index f34d5624..3e73cfee 100755
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: recordops.ml,v 1.26.2.1 2004/07/16 19:30:46 herbelin Exp $ *)
+(* $Id: recordops.ml,v 1.26.2.2 2005/11/29 21:40:52 letouzey Exp $ *)
open Util
open Pp
@@ -20,14 +20,6 @@ open Libobject
open Library
open Classops
-let nbimpl = ref 0
-let nbpathc = ref 0
-let nbcoer = ref 0
-let nbstruc = ref 0
-let nbimplstruc = ref 0
-
-let compter = ref false
-
(*s Une structure S est un type inductif non récursif à un seul
constructeur (de nom par défaut Build_S) *)
diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli
index 66c1f34d..a458b7b3 100755
--- a/pretyping/recordops.mli
+++ b/pretyping/recordops.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: recordops.mli,v 1.15.2.1 2004/07/16 19:30:46 herbelin Exp $ i*)
+(*i $Id: recordops.mli,v 1.15.2.2 2005/11/29 21:40:52 letouzey Exp $ i*)
(*i*)
open Names
@@ -18,13 +18,6 @@ open Libobject
open Library
(*i*)
-val nbimpl : int ref
-val nbpathc : int ref
-val nbcoer : int ref
-val nbstruc : int ref
-val nbimplstruc : int ref
-val compter : bool ref
-
type struc_typ = {
s_CONST : identifier;
s_PARAM : int;
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index f225e79f..e8bde1f3 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: tacred.ml,v 1.75.2.6 2004/12/29 10:17:10 herbelin Exp $ *)
+(* $Id: tacred.ml,v 1.75.2.7 2005/11/02 13:18:43 herbelin Exp $ *)
open Pp
open Util
@@ -204,13 +204,14 @@ let invert_name labs l na0 env sigma ref = function
match refi with
| None -> None
| Some ref ->
- match reference_opt_value sigma env ref with
+ try match reference_opt_value sigma env ref with
| None -> None
| Some c ->
let labs',ccl = decompose_lam c in
let _, l' = whd_betalet_stack ccl in
let labs' = List.map snd labs' in
if labs' = labs & l = l' then Some ref else None
+ with Not_found (* Undefined ref *) -> None
else Some ref
| Anonymous -> None (* Actually, should not occur *)
diff --git a/proofs/logic.ml b/proofs/logic.ml
index 3cc44a0f..cefeb8ae 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: logic.ml,v 1.80.2.1 2004/07/16 19:30:49 herbelin Exp $ *)
+(* $Id: logic.ml,v 1.80.2.5 2005/12/17 21:15:52 herbelin Exp $ *)
open Pp
open Util
@@ -54,7 +54,8 @@ open Pretype_errors
let catchable_exception = function
| Util.UserError _ | TypeError _ | RefinerError _
| Stdpp.Exc_located(_,(Util.UserError _ | TypeError _ | RefinerError _ |
- Nametab.GlobalizationError _ | PretypeError (_,VarNotFound _))) -> true
+ Nametab.GlobalizationError _ | PretypeError (_,VarNotFound _) |
+ Indtypes.InductiveError (Indtypes.NotAllowedCaseAnalysis _ ))) -> true
| _ -> false
let error_cannot_unify (m,n) =
@@ -67,16 +68,9 @@ let check = ref false
let without_check tac gl =
let c = !check in
check := false;
- let r = tac gl in
- check := c;
- r
+ try let r = tac gl in check := c; r with e -> check := c; raise e
-let with_check tac gl =
- let c = !check in
- check := true;
- let r = tac gl in
- check := c;
- r
+let with_check = Options.with_option check
(************************************************************************)
(************************************************************************)
@@ -405,9 +399,13 @@ let convert_hyp sign sigma (id,b,bt as d) =
apply_to_hyp sign id
(fun sign (_,c,ct) _ ->
let env = Global.env_of_context sign in
- if !check && not (is_conv env sigma bt ct) &&
- not (option_compare (is_conv env sigma) b c) then
- error "convert-hyp rule passed non-converting term";
+ if !check && not (is_conv env sigma bt ct) then
+ (* Just a warning in V8.0bugfix for compatibility *)
+ msgnl (str "Compatibility warning: Hazardeous change of the type of " ++ pr_id id ++
+ str " (not well-typed in current signature)");
+ if !check && not (option_compare (is_conv env sigma) b c) then
+ msgnl (str "Compatibility warning: Hazardeous change of the body of " ++ pr_id id ++
+ str " (not well-typed in current signature)");
add_named_decl d sign)
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index 55f11d52..785e6dd4 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: refiner.ml,v 1.67.2.1 2004/07/16 19:30:49 herbelin Exp $ *)
+(* $Id: refiner.ml,v 1.67.2.3 2005/11/04 08:59:30 herbelin Exp $ *)
open Pp
open Util
@@ -188,12 +188,8 @@ let lookup_tactic s =
(* refiner r is a tactic applying the rule r *)
-let bad_subproof () =
- anomalylabstrm "Refiner.refiner" (str"Bad subproof in validation.")
-
let check_subproof_connection gl spfl =
- if not (list_for_all2eq (fun g pf -> g=pf.goal) gl spfl)
- then (bad_subproof (); false) else true
+ list_for_all2eq (fun g pf -> g=pf.goal) gl spfl
let abstract_tactic_expr te tacfun gls =
let (sgl_sigma,v) = tacfun gls in
@@ -778,9 +774,13 @@ let extract_pftreestate pts =
(str"Cannot extract from a proof-tree in which we have descended;" ++
spc () ++ str"Please ascend to the root");
let pfterm,subgoals = extract_open_pftreestate pts in
- if subgoals <> [] then
+ let exl = Evd.non_instantiated pts.tpfsigma in
+ if subgoals <> [] or exl <> [] then
errorlabstrm "extract_proof"
- (str "Attempt to save an incomplete proof");
+ (if subgoals <> [] then
+ str "Attempt to save an incomplete proof"
+ else
+ str "Attempt to save a proof with existential variables still non-instantiated");
let env = Global.env_of_context pts.tpf.goal.evar_hyps in
strong whd_betaiotaevar env pts.tpfsigma pfterm
(***
diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml
index 60a0a937..cd8d34db 100644
--- a/proofs/tacexpr.ml
+++ b/proofs/tacexpr.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: tacexpr.ml,v 1.33.2.2 2005/01/21 17:14:09 herbelin Exp $ i*)
+(*i $Id: tacexpr.ml,v 1.33.2.3 2005/05/15 12:47:04 herbelin Exp $ i*)
open Names
open Topconstr
@@ -146,12 +146,12 @@ type ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_atomic_tactic_expr =
(* Automation tactics *)
| TacTrivial of string list option
- | TacAuto of int option * string list option
+ | TacAuto of int or_var option * string list option
| TacAutoTDB of int option
| TacDestructHyp of (bool * identifier located)
| TacDestructConcl
| TacSuperAuto of (int option * reference list * bool * bool)
- | TacDAuto of int option * int option
+ | TacDAuto of int or_var option * int option
(* Context management *)
| TacClear of 'id list
diff --git a/scripts/coqmktop.ml b/scripts/coqmktop.ml
index 78306877..ccb06769 100644
--- a/scripts/coqmktop.ml
+++ b/scripts/coqmktop.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: coqmktop.ml,v 1.28.2.1 2004/07/16 19:30:50 herbelin Exp $ *)
+(* $Id: coqmktop.ml,v 1.28.2.2 2005/11/04 08:20:57 herbelin Exp $ *)
(* coqmktop is a script to link Coq, analogous to ocamlmktop.
The command line contains options specific to coqmktop, options for the
@@ -189,7 +189,7 @@ let parse_args () =
coqide := true; parse (op,fl) rem
| "-v8" :: rem -> parse (op,fl) rem
| "-echo" :: rem -> echo := true ; parse (op,fl) rem
- | ("-cclib"|"-ccopt"|"-I"|"-o" as o) :: rem' ->
+ | ("-cclib"|"-ccopt"|"-I"|"-o"|"-w" as o) :: rem' ->
begin
match rem' with
| a :: rem -> parse (a::o::op,fl) rem
diff --git a/tactics/auto.ml b/tactics/auto.ml
index b530178e..d7130f35 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: auto.ml,v 1.63.2.2 2004/12/06 11:25:21 herbelin Exp $ *)
+(* $Id: auto.ml,v 1.63.2.3 2005/05/15 12:47:04 herbelin Exp $ *)
open Pp
open Util
@@ -812,7 +812,10 @@ let gen_auto n dbnames =
| None -> full_auto n
| Some l -> auto n l
-let h_auto n l = Refiner.abstract_tactic (TacAuto (n,l)) (gen_auto n l)
+let inj_or_var = option_app (fun n -> Genarg.ArgArg n)
+
+let h_auto n l =
+ Refiner.abstract_tactic (TacAuto (inj_or_var n,l)) (gen_auto n l)
(**************************************************************************)
(* The "destructing Auto" from Eduardo *)
@@ -839,7 +842,8 @@ let dauto = function
| Some n, Some p -> dautomatic p n
| None, Some p -> dautomatic p !default_search_depth
-let h_dauto (n,p) = Refiner.abstract_tactic (TacDAuto (n,p)) (dauto (n,p))
+let h_dauto (n,p) =
+ Refiner.abstract_tactic (TacDAuto (inj_or_var n,p)) (dauto (n,p))
(***************************************)
(*** A new formulation of Auto *********)
diff --git a/tactics/inv.ml b/tactics/inv.ml
index 54ce467c..e4bab195 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: inv.ml,v 1.53.2.1 2004/07/16 19:30:53 herbelin Exp $ *)
+(* $Id: inv.ml,v 1.53.2.3 2005/09/08 12:28:00 herbelin Exp $ *)
open Pp
open Util
@@ -135,9 +135,8 @@ let make_inv_predicate env sigma indf realargs id status concl =
else
make_iterated_tuple env' sigma (ai,ati) (xi,ti)
in
- let type_type_rhs = get_sort_of env sigma (type_of env sigma rhs) in
let sort = get_sort_of env sigma concl in
- let eq_term = find_eq_pattern type_type_rhs sort in
+ let eq_term = Coqlib.build_coq_eq () in
let eqn = applist (eq_term ,[eqnty;lhs;rhs]) in
build_concl ((Anonymous,lift n eqn)::eqns) (n+1) restlist
in
@@ -191,12 +190,14 @@ let make_inv_predicate env sigma indf realargs id status concl =
and introduces generalized hypotheis.
Precondition: t=(mkVar id) *)
-let rec dependent_hyps id idlist sign =
+let rec dependent_hyps id idlist gl =
let rec dep_rec =function
| [] -> []
- | (id1,_,id1ty as d1)::l ->
- if occur_var (Global.env()) id id1ty
- then d1 :: dep_rec l
+ | (id1,_,_)::l ->
+ (* Update the type of id1: it may have been subject to rewriting *)
+ let d = pf_get_hyp gl id1 in
+ if occur_var_in_decl (Global.env()) id d
+ then d :: dep_rec l
else dep_rec l
in
dep_rec idlist
@@ -281,7 +282,7 @@ Nota: with Inversion_clear, only four useless hypotheses
*)
let generalizeRewriteIntros tac depids id gls =
- let dids = dependent_hyps id depids (pf_env gls) in
+ let dids = dependent_hyps id depids gls in
(tclTHENSEQ
[bring_hyps dids; tac;
(* may actually fail to replace if dependent in a previous eq *)
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 4f8e7d7c..245b5a5b 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: tacinterp.ml,v 1.84.2.8 2005/01/15 14:56:54 herbelin Exp $ *)
+(* $Id: tacinterp.ml,v 1.84.2.11 2005/11/04 09:01:27 herbelin Exp $ *)
open Constrintern
open Closure
@@ -440,20 +440,18 @@ let intern_constr_reference strict ist = function
let loc,qid = qualid_of_reference r in
RRef (loc,locate_reference qid), if strict then None else Some (CRef r)
-let intern_reference strict ist = function
- | Ident (loc,id) when is_atomic id -> Tacexp (lookup_atomic id)
- | r ->
- (try Reference (intern_tac_ref ist r)
+let intern_reference strict ist r =
+ (try Reference (intern_tac_ref ist r)
+ with Not_found ->
+ (try
+ ConstrMayEval (ConstrTerm (intern_constr_reference strict ist r))
with Not_found ->
- (try
- ConstrMayEval (ConstrTerm (intern_constr_reference strict ist r))
- with Not_found ->
- (match r with
- | Ident (loc,id) when not strict ->
- IntroPattern (IntroIdentifier id)
- | _ ->
- let (loc,qid) = qualid_of_reference r in
- error_global_not_found_loc loc qid)))
+ (match r with
+ | Ident (loc,id) when is_atomic id -> Tacexp (lookup_atomic id)
+ | Ident (loc,id) when not strict -> IntroPattern (IntroIdentifier id)
+ | _ ->
+ let (loc,qid) = qualid_of_reference r in
+ error_global_not_found_loc loc qid)))
let rec intern_intro_pattern lf ist = function
| IntroOrAndPattern l ->
@@ -668,12 +666,12 @@ let rec intern_atomic lf ist x =
(* Automation tactics *)
| TacTrivial l -> TacTrivial l
- | TacAuto (n,l) -> TacAuto (n,l)
+ | TacAuto (n,l) -> TacAuto (option_app (intern_int_or_var ist) n,l)
| TacAutoTDB n -> TacAutoTDB n
| TacDestructHyp (b,id) -> TacDestructHyp(b,intern_hyp ist id)
| TacDestructConcl -> TacDestructConcl
| TacSuperAuto (n,l,b1,b2) -> TacSuperAuto (n,l,b1,b2)
- | TacDAuto (n,p) -> TacDAuto (n,p)
+ | TacDAuto (n,p) -> TacDAuto (option_app (intern_int_or_var ist) n,p)
(* Derived basic tactics *)
| TacSimpleInduction (h,ids) ->
@@ -1558,8 +1556,7 @@ and interp_match_context ist g lr lmr =
| e when is_match_catchable e ->
apply_match_context ist env goal (nrs+1) (List.tl lex) tl))
| _ ->
- errorlabstrm "Tacinterp.apply_match_context" (str
- "No matching clauses for match goal")
+ errorlabstrm "Tacinterp.apply_match_context"
(v 0 (str "No matching clauses for match goal" ++
(if ist.debug=DebugOff then
fnl() ++ str "(use \"Debug On\" for more info)"
@@ -1744,12 +1741,12 @@ and interp_atomic ist gl = function
(* Automation tactics *)
| TacTrivial l -> Auto.h_trivial l
- | TacAuto (n, l) -> Auto.h_auto n l
+ | TacAuto (n, l) -> Auto.h_auto (option_app (interp_int_or_var ist) n) l
| TacAutoTDB n -> Dhyp.h_auto_tdb n
| TacDestructHyp (b,id) -> Dhyp.h_destructHyp b (interp_hyp ist gl id)
| TacDestructConcl -> Dhyp.h_destructConcl
| TacSuperAuto (n,l,b1,b2) -> Auto.h_superauto n l b1 b2
- | TacDAuto (n,p) -> Auto.h_dauto (n,p)
+ | TacDAuto (n,p) -> Auto.h_dauto (option_app (interp_int_or_var ist) n,p)
(* Derived basic tactics *)
| TacSimpleInduction (h,ids) ->
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index b6eaf015..2ba09e52 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: tactics.ml,v 1.162.2.4 2004/12/04 10:26:46 herbelin Exp $ *)
+(* $Id: tactics.ml,v 1.162.2.7 2005/07/13 16:18:57 herbelin Exp $ *)
open Pp
open Util
@@ -220,8 +220,16 @@ let pattern_option l = reduct_option (pattern_occs l)
(* A function which reduces accordingly to a reduction expression,
as the command Eval does. *)
+let needs_check = function
+ (* Expansion is not necessarily well-typed: e.g. expansion of t into x is
+ not well-typed in [H:(P t); x:=t |- G] because x is defined after H *)
+ | Fold _ -> true
+ | _ -> false
+
let reduce redexp cl goal =
- redin_combinator (reduction_of_redexp redexp) cl goal
+ (if needs_check redexp then with_check else (fun x -> x))
+ (redin_combinator (reduction_of_redexp redexp) cl)
+ goal
(* Unfolding occurrences of a constant *)
@@ -741,7 +749,7 @@ let letin_tac with_eq name c occs gl =
if not (mem_named_context x (pf_hyps gl)) then x else
error ("The variable "^(string_of_id x)^" is already declared") in
let (depdecls,lastlhyp,ccl)= letin_abstract id c occs gl in
- let t = pf_type_of gl c in
+ let t = Evarutil.refresh_universes (pf_type_of gl c) in
let newcl = mkNamedLetIn id c t ccl in
tclTHENLIST
[ convert_concl_no_check newcl;
diff --git a/test-suite/check b/test-suite/check
index 378c8e5d..fdc7b2d6 100755
--- a/test-suite/check
+++ b/test-suite/check
@@ -84,7 +84,8 @@ test_output() {
nbtestsok=`expr $nbtestsok + 1`
else
echo "Error! (unexpected output)"
- fi
+ fi
+ rm $tmpoutput
done
}
@@ -106,6 +107,7 @@ test_parser() {
echo "Ok"
nbtestsok=`expr $nbtestsok + 1`
fi
+ rm $tmpoutput
done
fi
}
diff --git a/test-suite/modules/modul.v b/test-suite/modules/modul.v
index 5612ea75..84942da1 100644
--- a/test-suite/modules/modul.v
+++ b/test-suite/modules/modul.v
@@ -33,7 +33,7 @@ Save.
Check (O#O).
Locate rel.
-Locate M.
+Locate Library M.
Module N:=Top.M.
diff --git a/test-suite/tactics/TestRefine.v b/test-suite/success/TestRefine.v
index f752c5bc..ee3d7e3f 100644
--- a/test-suite/tactics/TestRefine.v
+++ b/test-suite/success/TestRefine.v
@@ -182,22 +182,9 @@ Refine (well_founded_induction
(fib (pred (pred x0)) ?))
end
end).
-(*********
-Refine (well_founded_induction
- nat
- lt ?
- [_:nat]nat
- [x0:nat][fib:(x:nat)(lt x x0)->nat]
- Cases x0 of
- O => (S O)
- | (S O) => (S O)
- | (S (S p)) => (plus (fib (pred x0) ?)
- (fib (pred (pred x0)) ?))
- end).
-***********)
Exact lt_wf.
-Auto.
-Apply lt_trans with m:=(pred x0); Auto.
+Auto with arith.
+Apply lt_trans with m:=(pred x0); Auto with arith.
Save.
diff --git a/theories/Reals/PartSum.v b/theories/Reals/PartSum.v
index 13070bde..6087d3f2 100644
--- a/theories/Reals/PartSum.v
+++ b/theories/Reals/PartSum.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: PartSum.v,v 1.11.2.1 2004/07/16 19:31:11 herbelin Exp $ i*)
+(*i $Id: PartSum.v,v 1.11.2.2 2005/07/13 22:28:30 herbelin Exp $ i*)
Require Import Rbase.
Require Import Rfunctions.
@@ -489,8 +489,7 @@ elim s; intro.
left; apply a.
right; apply b.
cut (Un_growing (fun n:nat => sum_f_R0 An n)).
-intro; set (l1 := sum_f_R0 An N).
-fold l1 in r.
+intro; set (l1 := sum_f_R0 An N) in r.
unfold Un_cv in H; cut (0 < l1 - l).
intro; elim (H _ H2); intros.
set (N0 := max x N); cut (N0 >= x)%nat.
@@ -600,4 +599,4 @@ apply Rle_trans with (sum_f_R0 An n0 + Rabs (fn (S n0) x)).
do 2 rewrite <- (Rplus_comm (Rabs (fn (S n0) x))).
apply Rplus_le_compat_l; apply Hrecn0.
apply Rplus_le_compat_l; apply H1.
-Qed. \ No newline at end of file
+Qed.
diff --git a/theories/Reals/RIneq.v b/theories/Reals/RIneq.v
index a23f53ff..5da14193 100644
--- a/theories/Reals/RIneq.v
+++ b/theories/Reals/RIneq.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: RIneq.v,v 1.23.2.1 2004/07/16 19:31:11 herbelin Exp $ i*)
+(*i $Id: RIneq.v,v 1.23.2.2 2005/03/29 15:35:13 herbelin Exp $ i*)
(***************************************************************************)
(** Basic lemmas for the classical reals numbers *)
@@ -1382,7 +1382,7 @@ Qed.
(**********)
Lemma lt_IZR : forall n m:Z, IZR n < IZR m -> (n < m)%Z.
-intros z1 z2 H; apply Zlt_O_minus_lt.
+intros z1 z2 H; apply Zlt_0_minus_lt.
apply lt_O_IZR.
rewrite <- Z_R_minus.
exact (Rgt_minus (IZR z2) (IZR z1) H).
diff --git a/theories/Reals/RiemannInt.v b/theories/Reals/RiemannInt.v
index 51323ac4..ce33afdb 100644
--- a/theories/Reals/RiemannInt.v
+++ b/theories/Reals/RiemannInt.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: RiemannInt.v,v 1.18.2.1 2004/07/16 19:31:13 herbelin Exp $ i*)
+(*i $Id: RiemannInt.v,v 1.18.2.2 2005/07/13 23:18:52 herbelin Exp $ i*)
Require Import Rfunctions.
Require Import SeqSeries.
@@ -1593,13 +1593,12 @@ Lemma RiemannInt_P17 :
intro f; intros; unfold RiemannInt in |- *;
case (RiemannInt_exists pr1 RinvN RinvN_cv);
case (RiemannInt_exists pr2 RinvN RinvN_cv); intros;
- set (phi1 := phi_sequence RinvN pr1);
+ set (phi1 := phi_sequence RinvN pr1) in u0;
set (phi2 := fun N:nat => mkStepFun (StepFun_P32 (phi1 N)));
apply Rle_cv_lim with
(fun N:nat => Rabs (RiemannInt_SF (phi1 N)))
(fun N:nat => RiemannInt_SF (phi2 N)).
intro; unfold phi2 in |- *; apply StepFun_P34; assumption.
-fold phi1 in u0;
apply (continuity_seq Rabs (fun N:nat => RiemannInt_SF (phi1 N)) x0);
try assumption.
apply Rcontinuity_abs.
@@ -2372,10 +2371,11 @@ unfold R_dist in |- *; unfold Rminus in |- *; rewrite Ropp_0;
left; apply (cond_pos (RinvN n)).
exists N0; intros; elim (H1 n); elim (H2 n); elim (H3 n); clear H1 H2 H3;
intros; unfold R_dist in |- *; unfold Rminus in |- *;
- rewrite Ropp_0; rewrite Rplus_0_r; set (phi1 := phi_sequence RinvN pr1 n);
- fold phi1 in H8; set (phi2 := phi_sequence RinvN pr2 n);
- fold phi2 in H3; set (phi3 := phi_sequence RinvN pr3 n);
- fold phi2 in H1; assert (H10 : IsStepFun phi3 a b).
+ rewrite Ropp_0; rewrite Rplus_0_r;
+ set (phi1 := phi_sequence RinvN pr1 n) in H8 |- *;
+ set (phi2 := phi_sequence RinvN pr2 n) in H3 |- *;
+ set (phi3 := phi_sequence RinvN pr3 n) in H1 |- *;
+ assert (H10 : IsStepFun phi3 a b).
apply StepFun_P44 with c.
apply (pre phi3).
split; assumption.
@@ -2442,7 +2442,7 @@ rewrite <- (Rabs_Ropp (f x - phi3 x)); rewrite Ropp_minus_distr;
replace (phi3 x + -1 * phi2 x) with (phi3 x - f x + (f x - phi2 x));
[ apply Rabs_triang | ring ].
apply Rplus_le_compat.
-fold phi3 in H1; apply H1.
+apply H1.
elim H14; intros; split.
replace (Rmin a c) with a.
apply Rle_trans with b; try assumption.
diff --git a/theories/ZArith/Zorder.v b/theories/ZArith/Zorder.v
index 55d4d958..27eb02cd 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,v 1.6.2.1 2004/07/16 19:31:22 herbelin Exp $ i*)
+(*i $Id: Zorder.v,v 1.6.2.3 2005/03/29 15:35:12 herbelin Exp $ i*)
(** Binary Integers (Pierre Crégut (CNET, Lannion, France) *)
@@ -849,12 +849,15 @@ intros p H1; unfold Zgt in |- *; pattern 0 at 2 in |- *;
intros p H; discriminate H.
Qed.
-Lemma Zmult_lt_O_compat : forall n m:Z, 0 < n -> 0 < m -> 0 < n * m.
+Lemma Zmult_lt_0_compat : forall n m:Z, 0 < n -> 0 < m -> 0 < n * m.
intros a b apos bpos.
apply Zgt_lt.
apply Zmult_gt_0_compat; try apply Zlt_gt; assumption.
Qed.
+(* For compatibility *)
+Notation Zmult_lt_O_compat := Zmult_lt_0_compat (only parsing).
+
Lemma Zmult_gt_0_le_0_compat : forall n m:Z, n > 0 -> 0 <= m -> 0 <= m * n.
Proof.
intros x y H1 H2; apply Zmult_le_0_compat; trivial.
@@ -958,8 +961,11 @@ intros n m H; apply Zplus_lt_reg_l with (p := m); rewrite Zplus_minus;
assumption.
Qed.
-Lemma Zlt_O_minus_lt : forall n m:Z, 0 < n - m -> m < n.
+Lemma Zlt_0_minus_lt : forall n m:Z, 0 < n - m -> m < n.
Proof.
intros n m H; apply Zplus_lt_reg_l with (p := - m); rewrite Zplus_opp_l;
rewrite Zplus_comm; exact H.
-Qed. \ No newline at end of file
+Qed.
+
+(* For compatibility *)
+Notation Zlt_O_minus_lt := Zlt_0_minus_lt (only parsing).
diff --git a/theories7/Reals/PartSum.v b/theories7/Reals/PartSum.v
index ee5fa498..4d28bec8 100644
--- a/theories7/Reals/PartSum.v
+++ b/theories7/Reals/PartSum.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: PartSum.v,v 1.1.2.1 2004/07/16 19:31:33 herbelin Exp $ i*)
+(*i $Id: PartSum.v,v 1.1.2.2 2005/07/13 23:19:16 herbelin Exp $ i*)
Require Rbase.
Require Rfunctions.
@@ -385,8 +385,7 @@ Elim s; Intro.
Left; Apply a.
Right; Apply b.
Cut (Un_growing [n:nat](sum_f_R0 An n)).
-Intro; Pose l1 := (sum_f_R0 An N).
-Fold l1 in r.
+Intro; LetTac l1 := (sum_f_R0 An N) in r.
Unfold Un_cv in H; Cut ``0<l1-l``.
Intro; Elim (H ? H2); Intros.
Pose N0 := (max x N); Cut (ge N0 x).
diff --git a/theories7/Reals/RiemannInt.v b/theories7/Reals/RiemannInt.v
index c9301b56..cc537c6d 100644
--- a/theories7/Reals/RiemannInt.v
+++ b/theories7/Reals/RiemannInt.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: RiemannInt.v,v 1.1.2.1 2004/07/16 19:31:34 herbelin Exp $ i*)
+(*i $Id: RiemannInt.v,v 1.1.2.2 2005/07/13 23:19:16 herbelin Exp $ i*)
Require Rfunctions.
Require SeqSeries.
@@ -710,9 +710,9 @@ Apply r_Rmult_mult with ``2``; [Unfold Rdiv; Do 2 Rewrite -> (Rmult_sym ``2``);
Qed.
Lemma RiemannInt_P17 : (f:R->R;a,b:R;pr1:(Riemann_integrable f a b);pr2:(Riemann_integrable [x:R](Rabsolu (f x)) a b)) ``a<=b`` -> ``(Rabsolu (RiemannInt pr1))<=(RiemannInt pr2)``.
-Intro f; Intros; Unfold RiemannInt; Case (RiemannInt_exists 1!f 2!a 3!b pr1 5!RinvN RinvN_cv); Case (RiemannInt_exists 1!([x0:R](Rabsolu (f x0))) 2!a 3!b pr2 5!RinvN RinvN_cv); Intros; Pose phi1 := (phi_sequence RinvN pr1); Pose phi2 := [N:nat](mkStepFun (StepFun_P32 (phi1 N))); Apply Rle_cv_lim with [N:nat](Rabsolu (RiemannInt_SF (phi1 N))) [N:nat](RiemannInt_SF (phi2 N)).
+Intro f; Intros; Unfold RiemannInt; Case (RiemannInt_exists 1!f 2!a 3!b pr1 5!RinvN RinvN_cv); Case (RiemannInt_exists 1!([x0:R](Rabsolu (f x0))) 2!a 3!b pr2 5!RinvN RinvN_cv); Intros; LetTac phi1 := (phi_sequence RinvN pr1) in u0; Pose phi2 := [N:nat](mkStepFun (StepFun_P32 (phi1 N))); Apply Rle_cv_lim with [N:nat](Rabsolu (RiemannInt_SF (phi1 N))) [N:nat](RiemannInt_SF (phi2 N)).
Intro; Unfold phi2; Apply StepFun_P34; Assumption.
-Fold phi1 in u0; Apply (continuity_seq Rabsolu [N:nat](RiemannInt_SF (phi1 N)) x0); Try Assumption.
+Apply (continuity_seq Rabsolu [N:nat](RiemannInt_SF (phi1 N)) x0); Try Assumption.
Apply continuity_Rabsolu.
Pose phi3 := (phi_sequence RinvN pr2); Assert H0 : (EXT psi3:nat->(StepFun a b) | (n:nat) ((t:R)``(Rmin a b) <= t``/\``t <= (Rmax a b)``->``(Rabsolu ((Rabsolu (f t))-((phi3 n) t)))<= (psi3 n t)``)/\``(Rabsolu (RiemannInt_SF (psi3 n))) < (RinvN n)``).
Split with [n:nat](projT1 ? ? (phi_sequence_prop RinvN pr2 n)); Intro; Apply (projT2 ? ? (phi_sequence_prop RinvN pr2 n)).
@@ -1139,7 +1139,7 @@ Elim (H ? H4); Clear H; Intros N0 H; Assert H5 : (n:nat)(ge n N0)->``(RinvN n)<e
Intros; Replace (pos (RinvN n)) with ``(R_dist (mkposreal (/((INR n)+1)) (RinvN_pos n)) 0)``.
Apply H; Assumption.
Unfold R_dist; Unfold Rminus; Rewrite Ropp_O; Rewrite Rplus_Or; Apply Rabsolu_right; Apply Rle_sym1; Left; Apply (cond_pos (RinvN n)).
-Exists N0; Intros; Elim (H1 n); Elim (H2 n); Elim (H3 n); Clear H1 H2 H3; Intros; Unfold R_dist; Unfold Rminus; Rewrite Ropp_O; Rewrite Rplus_Or; Pose phi1 := (phi_sequence RinvN pr1 n); Fold phi1 in H8; Pose phi2 := (phi_sequence RinvN pr2 n); Fold phi2 in H3; Pose phi3 := (phi_sequence RinvN pr3 n); Fold phi2 in H1; Assert H10 : (IsStepFun phi3 a b).
+Exists N0; Intros; Elim (H1 n); Elim (H2 n); Elim (H3 n); Clear H1 H2 H3; Intros; Unfold R_dist; Unfold Rminus; Rewrite Ropp_O; Rewrite Rplus_Or; LetTac phi1 := (phi_sequence RinvN pr1 n) in H8 Goal; LetTac phi2 := (phi_sequence RinvN pr2 n) in H3 Goal; LetTac phi3 := (phi_sequence RinvN pr3 n) in H1 Goal; Assert H10 : (IsStepFun phi3 a b).
Apply StepFun_P44 with c.
Apply (pre phi3).
Split; Assumption.
@@ -1171,7 +1171,7 @@ Apply Rle_compatibility; Apply StepFun_P37; Try Assumption.
Intros; Simpl; Rewrite Rmult_1l; Apply Rle_trans with ``(Rabsolu ((f x)-(phi3 x)))+(Rabsolu ((f x)-(phi2 x)))``.
Rewrite <- (Rabsolu_Ropp ``(f x)-(phi3 x)``); Rewrite Ropp_distr2; Replace ``(phi3 x)+ -1*(phi2 x)`` with ``((phi3 x)-(f x))+((f x)-(phi2 x))``; [Apply Rabsolu_triang | Ring].
Apply Rplus_le.
-Fold phi3 in H1; Apply H1.
+Apply H1.
Elim H14; Intros; Split.
Replace (Rmin a c) with a.
Apply Rle_trans with b; Try Assumption.
diff --git a/tools/coqdoc/coqdoc.sty b/tools/coqdoc/coqdoc.sty
index 7f7aa9aa..68b9ab26 100644
--- a/tools/coqdoc/coqdoc.sty
+++ b/tools/coqdoc/coqdoc.sty
@@ -16,8 +16,8 @@
\pagestyle{fancyplain}
%BEGIN LATEX
-\plainheadrulewidth 0.4pt
-\plainfootrulewidth 0pt
+\renewcommand{\plainheadrulewidth}{0.4pt}
+\renewcommand{\plainfootrulewidth}{0pt}
\lhead[\coqdocleftpageheader]{\leftmark}
\rhead[\leftmark]{\coqdocrightpageheader}
\cfoot{}
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 3da1c838..10d6a620 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: command.ml,v 1.116.2.3 2004/12/31 12:01:16 herbelin Exp $ *)
+(* $Id: command.ml,v 1.116.2.4 2005/11/29 21:40:53 letouzey Exp $ *)
open Pp
open Util
@@ -372,7 +372,9 @@ let interp_mutual lparams lnamearconstrs finite =
(List.rev arityl) lnamearconstrs
in
States.unfreeze fs;
- notations, { mind_entry_finite = finite; mind_entry_inds = mispecvec }
+ notations, { mind_entry_record = false;
+ mind_entry_finite = finite;
+ mind_entry_inds = mispecvec }
with e -> States.unfreeze fs; raise e
let declare_mutual_with_eliminations isrecord mie =
diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml
index 4a4f7828..4ba8f6c2 100644
--- a/toplevel/coqinit.ml
+++ b/toplevel/coqinit.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: coqinit.ml,v 1.30.2.1 2004/07/16 19:31:47 herbelin Exp $ *)
+(* $Id: coqinit.ml,v 1.30.2.4 2006/01/11 23:18:06 barras Exp $ *)
open Pp
open System
@@ -68,16 +68,15 @@ let hm2 s =
let n = String.length s in
if n > 1 && s.[0] = '.' && s.[1] = '/' then String.sub s 2 (n-2) else s
-let getenv_else s dft = try Sys.getenv s with Not_found -> dft
-
(* Initializes the LoadPath according to COQLIB and Coq_config *)
let init_load_path () =
(* developper specific directories to open *)
let dev = if Coq_config.local then [ "dev" ] else [] in
let coqlib =
- if Coq_config.local || !Options.boot then Coq_config.coqtop
+ if !Options.boot then Coq_config.coqtop
(* variable COQLIB overrides the default library *)
else getenv_else "COQLIB" Coq_config.coqlib in
+ let coqlib = canonical_path_name coqlib in
(* first user-contrib *)
let user_contrib = coqlib/"user-contrib" in
if Sys.file_exists user_contrib then
@@ -90,6 +89,7 @@ let init_load_path () =
(if !Options.v7 then "states7" else "states") :: dev @ vdirs in
List.iter (fun s -> coq_add_rec_path (coqlib/s)) dirs;
let camlp4 = getenv_else "CAMLP4LIB" Coq_config.camlp4lib in
+ let camlp4 = canonical_path_name camlp4 in
add_ml_include camlp4;
(* then current directory *)
Mltop.add_path "." Nameops.default_root_prefix;
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 83d240a1..af787460 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: coqtop.ml,v 1.72.2.4 2004/09/03 15:05:23 herbelin Exp $ *)
+(* $Id: coqtop.ml,v 1.72.2.5 2005/11/23 14:46:09 barras Exp $ *)
open Pp
open Util
@@ -295,7 +295,8 @@ let init is_ide =
init_load_path ();
inputstate ();
engage ();
- if not !batch_mode then Declaremods.start_library !toplevel_name;
+ if not !batch_mode && Global.env_is_empty() then
+ Declaremods.start_library !toplevel_name;
init_library_roots ();
load_vernac_obj ();
require ();
diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml
index 688885b1..281ff1b6 100644
--- a/toplevel/discharge.ml
+++ b/toplevel/discharge.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: discharge.ml,v 1.81.2.1 2004/07/16 19:31:48 herbelin Exp $ *)
+(* $Id: discharge.ml,v 1.81.2.2 2005/11/29 21:40:53 letouzey Exp $ *)
open Pp
open Util
@@ -118,6 +118,7 @@ let abstract_inductive sec_sp ids_to_abs hyps inds =
let process_inductive sec_sp osecsp nsecsp oldenv (ids_to_discard,modlist) mib =
assert (Array.length mib.mind_packets > 0);
+ let record = mib.mind_record in
let finite = mib.mind_finite in
let inds =
array_map_to_list
@@ -153,7 +154,8 @@ let process_inductive sec_sp osecsp nsecsp oldenv (ids_to_discard,modlist) mib =
in
let indmodifs,cstrmodifs =
List.split (list_tabulate lmodif_one_mind mib.mind_ntypes) in
- ({ mind_entry_finite = finite;
+ ({ mind_entry_record = record;
+ mind_entry_finite = finite;
mind_entry_inds = inds' },
indmodifs,
List.flatten cstrmodifs,
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index ca64cda0..4c554209 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: metasyntax.ml,v 1.105.2.6 2004/11/22 12:41:38 herbelin Exp $ *)
+(* $Id: metasyntax.ml,v 1.105.2.12 2006/01/04 20:31:16 herbelin Exp $ *)
open Pp
open Util
@@ -154,12 +154,11 @@ let rec make_tags = function
let declare_pprule = function
(* Pretty-printing rules only for Grammar (Tactic Notation) *)
- | Egrammar.TacticGrammar gl ->
- let f (s,(s',l),tac) =
- let pp = (make_tags l, (s',List.map make_terminal_status l)) in
- Pptactic.declare_extra_tactic_pprule true s pp;
- Pptactic.declare_extra_tactic_pprule false s pp in
- List.iter f gl
+ | Egrammar.TacticGrammar (_,pp) ->
+ let f (s,t,p) =
+ Pptactic.declare_extra_tactic_pprule true s (t,p);
+ Pptactic.declare_extra_tactic_pprule false s (t,p) in
+ List.iter f pp
| _ -> ()
let cache_grammar (_,a) =
@@ -199,12 +198,24 @@ let add_grammar_obj univ entryl =
(* Tactic notations *)
-let locate_tactic_body dir (s,p,e) = (s,p,(dir,e))
+let rec tactic_notation_key = function
+ | VTerm id :: _ -> id
+ | _ :: l -> tactic_notation_key l
+ | [] -> "terminal_free_notation"
+
+let rec next_key_away key t =
+ if Pptactic.exists_extra_tactic_pprule key t then next_key_away (key^"'") t
+ else key
+
+let locate_tactic_body dir (s,(s',prods as x),e) =
+ let tags = make_tags prods in
+ let s = if s="" then next_key_away (tactic_notation_key prods) tags else s in
+ (s,x,(dir,e)),(s,tags,(s',List.map make_terminal_status prods))
let add_tactic_grammar g =
let dir = Lib.cwd () in
- let g = List.map (locate_tactic_body dir) g in
- Lib.add_anonymous_leaf (inGrammar (Egrammar.TacticGrammar g))
+ let pa,pp = List.split (List.map (locate_tactic_body dir) g) in
+ Lib.add_anonymous_leaf (inGrammar (Egrammar.TacticGrammar (pa,pp)))
(* Printing grammar entries *)
@@ -598,8 +609,12 @@ let make_hunks etyps symbols from =
| SProdList (m,sl) :: prods ->
let i = list_index m vars in
let _,prec = precedence_of_entry_type from (List.nth typs (i-1)) in
- (* We add NonTerminal for simulation but remove it afterwards *)
- let _,sl' = list_sep_last (make NoBreak (sl@[NonTerminal m])) in
+ let sl' =
+ (* If no separator: add a break *)
+ if sl = [] then add_break 1 []
+ (* We add NonTerminal for simulation but remove it afterwards *)
+ else snd (list_sep_last (make NoBreak (sl@[NonTerminal m])))
+ in
UnpListMetaVar (i,prec,sl') :: make CanBreak prods
| [] -> []
@@ -813,6 +828,10 @@ let pr_level ntn (from,args) =
str "at level " ++ int from ++ spc () ++ str "with arguments" ++ spc() ++
prlist_with_sep pr_coma (pr_arg_level from) args
+(* In v8: prec = Some prec8 is for both parsing and printing *)
+(* In v7 and translator:
+ prec is for parsing (None if V8Notation),
+ prec8 for v8 printing (v7 printing is via ast) *)
let cache_syntax_extension (_,(_,((prec,prec8),ntn,gr,se))) =
try
let oldprec, oldprec8 = Symbols.level_of_notation ntn in
@@ -869,7 +888,7 @@ let (inSyntaxExtension, outSyntaxExtension) =
classify_function = classify_syntax_definition;
export_function = export_syntax_definition}
-let interp_modifiers =
+let interp_modifiers modl =
let onlyparsing = ref false in
let rec interp assoc level etyps format = function
| [] ->
@@ -898,10 +917,9 @@ let interp_modifiers =
onlyparsing := true;
interp assoc level etyps format l
| SetFormat s :: l ->
- if format <> None then error "A format is given more than once"
- onlyparsing := true;
+ if format <> None then error "A format is given more than once";
interp assoc level etyps (Some s) l
- in interp None None [] None
+ in interp None None [] None modl
let merge_modifiers a n l =
(match a with None -> [] | Some a -> [SetAssoc a]) @
@@ -1037,22 +1055,30 @@ let compute_syntax_data forv7 (df,modifiers) =
((onlyparse,recvars,vars,
ntn_for_interp,notation),prec,ppdata,(Lib.library_dp(),df))
+(* Uninterpreted (reserved) notations *)
let add_syntax_extension local mv mv8 =
+ (* from v7:
+ if mv8 <> None: tells the translator how to print in v8
+ if mv <> None: tells how to parse and, how to print in v7
+ mv = None = mv8 does not occur
+ from v8 (mv8 is always None and mv is always Some)
+ mv tells how to parse and print in v8
+ *)
let data8 = option_app (compute_syntax_data false) mv8 in
let data = option_app (compute_syntax_data !Options.v7) mv in
let prec,gram_rule = match data with
- | None -> None, None
+ | None -> None, None (* Case of V8Notation from v7 *)
| Some ((_,_,_,_,notation),prec,(n,typs,symbols,_),_) ->
Some prec, Some (make_grammar_rule n typs symbols notation None) in
match data, data8 with
| None, None -> (* Nothing to do: V8Notation while not translating *) ()
| _, Some d | Some d, None ->
- let ((_,_,_,_,ntn),ppprec,ppdata,_) = d in
+ let ((_,_,_,_,ntn),ppprec,ppdata,_) = d in (* tells how to print *)
let ntn' = match data with Some ((_,_,_,_,ntn),_,_,_) -> ntn | _ -> ntn in
let pp_rule = make_pp_rule ppdata in
Lib.add_anonymous_leaf
(inSyntaxExtension (local,((prec,ppprec),ntn',gram_rule,pp_rule)))
-
+
(**********************************************************************)
(* Distfix, Infix, Symbols *)
@@ -1147,7 +1173,7 @@ let contract_notation ntn =
else ntn in
aux ntn 0
-let add_notation_in_scope local df c mods omodv8 scope toks =
+let add_notation_in_scope local df c mods omodv8 scope =
let ((onlyparse,recs,vars,intnot,notation),prec,(n,typs,symbols,_ as ppdata),df')=
compute_syntax_data !Options.v7 (df,mods) in
(* Declare the parsing and printing rules if not already done *)
@@ -1260,7 +1286,7 @@ let add_notation_interpretation df names c sc =
add_notation_interpretation_core false symbs for_oldpp df a sc onlyparse
false gram_data
-let add_notation_in_scope_v8only local df c mv8 scope toks =
+let add_notation_in_scope_v8only local df c mv8 scope =
let (_,recs,vars,intnot,notation),prec,ppdata,df' = compute_syntax_data false (df,mv8) in
let pp_rule = make_pp_rule ppdata in
Lib.add_anonymous_leaf
@@ -1277,7 +1303,7 @@ let add_notation_v8only local c (df,modifiers) sc =
match toks with
| [String x] when (modifiers = [] or modifiers = [SetOnlyParsing]) ->
(* This is a ident to be declared as a rule *)
- add_notation_in_scope_v8only local df c (SetLevel 0::modifiers) sc toks
+ add_notation_in_scope_v8only local df c (SetLevel 0::modifiers) sc
| _ ->
let (assoc,lev,typs,onlyparse,fmt) = interp_modifiers modifiers in
match lev with
@@ -1299,12 +1325,16 @@ let add_notation_v8only local c (df,modifiers) sc =
if List.for_all (function SetAssoc _ -> false | _ -> true)
modifiers
then SetAssoc Gramext.NonA :: modifiers else modifiers in
- add_notation_in_scope_v8only local df c mods sc toks
+ add_notation_in_scope_v8only local df c mods sc
let is_quoted_ident x =
let x' = unquote_notation_token x in
x <> x' & try Lexer.check_ident x'; true with _ -> false
+(* v7: dfmod=None; mv8=Some: add only v8 printing rule *)
+(* dfmod=Some: add v7 parsing rule; mv8=Some: add v8 printing rule *)
+(* dfmod=Some; mv8=None: same v7-parsing and v8-printing rules *)
+(* v8: dfmod=Some; mv8=None: same v8 parsing and printing rules *)
let add_notation local c dfmod mv8 sc =
match dfmod with
| None -> add_notation_v8only local c (out_some mv8) sc
@@ -1313,7 +1343,7 @@ let add_notation local c dfmod mv8 sc =
match toks with
| [String x] when (modifiers = [] or modifiers = [SetOnlyParsing]) ->
(* This is a ident to be declared as a rule *)
- add_notation_in_scope local df c (SetLevel 0::modifiers) mv8 sc toks
+ add_notation_in_scope local df c (SetLevel 0::modifiers) mv8 sc
| _ ->
let (assoc,lev,typs,onlyparse,fmt) = interp_modifiers modifiers in
match lev with
@@ -1335,11 +1365,11 @@ let add_notation local c dfmod mv8 sc =
add_notation_interpretation_core local symbs for_old df a
sc onlyparse false gram_data
else
- add_notation_in_scope local df c modifiers mv8 sc toks
+ add_notation_in_scope local df c modifiers mv8 sc
| Some n ->
(* Declare both syntax and interpretation *)
let assoc = match assoc with None -> Some Gramext.NonA | a -> a in
- add_notation_in_scope local df c modifiers mv8 sc toks
+ add_notation_in_scope local df c modifiers mv8 sc
(* TODO add boxes information in the expression *)
@@ -1371,7 +1401,6 @@ let add_distfix local assoc n df r sc =
let a = mkAppC (mkRefC r, vars) in
let assoc = match assoc with None -> Gramext.LeftA | Some a -> a in
add_notation_in_scope local df a [SetAssoc assoc;SetLevel n] None sc
- (split_notation_string df)
let make_infix_data n assoc modl mv8 =
(* Infix defaults to LEFTA in V7 (cf doc) *)
@@ -1404,7 +1433,7 @@ let add_infix local (inf,modl) pr mv8 sc =
else
if n8 = None then error "Needs a level" else
let mv8 = match a8 with None -> SetAssoc Gramext.NonA :: mv8 |_ -> mv8 in
- add_notation_in_scope_v8only local df a mv8 sc toks
+ add_notation_in_scope_v8only local df a mv8 sc
else begin
let (assoc,n,onlyparse,fmt) = interp_infix_modifiers modl in
(* check the precedence *)
@@ -1435,10 +1464,10 @@ let add_infix local (inf,modl) pr mv8 sc =
onlyparse false gram_data
else
let mv,mv8 = make_infix_data n assoc modl mv8 in
- add_notation_in_scope local df a mv mv8 sc toks
+ add_notation_in_scope local df a mv mv8 sc
else
let mv,mv8 = make_infix_data n assoc modl mv8 in
- add_notation_in_scope local df a mv mv8 sc toks
+ add_notation_in_scope local df a mv mv8 sc
end
let standardise_locatable_notation ntn =
diff --git a/toplevel/record.ml b/toplevel/record.ml
index f703c067..3a10c7e5 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: record.ml,v 1.52.2.1 2004/07/16 19:31:49 herbelin Exp $ *)
+(* $Id: record.ml,v 1.52.2.2 2005/11/29 21:40:53 letouzey Exp $ *)
open Pp
open Util
@@ -226,7 +226,8 @@ let definition_structure ((is_coe,(_,idstruc)),ps,cfs,idbuild,s) =
mind_entry_consnames = [idbuild];
mind_entry_lc = [type_constructor] } in
let mie =
- { mind_entry_finite = true;
+ { mind_entry_record = true;
+ mind_entry_finite = true;
mind_entry_inds = [mie_ind] } in
let sp = declare_mutual_with_eliminations true mie in
let rsp = (sp,0) in (* This is ind path of idstruc *)
diff --git a/translate/ppconstrnew.ml b/translate/ppconstrnew.ml
index f75f767d..381ac2c3 100644
--- a/translate/ppconstrnew.ml
+++ b/translate/ppconstrnew.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: ppconstrnew.ml,v 1.62.2.4 2004/12/29 10:17:11 herbelin Exp $ *)
+(* $Id: ppconstrnew.ml,v 1.62.2.6 2005/03/08 10:13:45 herbelin Exp $ *)
(*i*)
open Ast
@@ -118,7 +118,7 @@ let pr_optc pr = function
| None -> mt ()
| Some x -> pr_sep_com spc pr x
-let pr_universe u = str "<univ>"
+let pr_universe = Univ.pr_uni
let pr_sort = function
| RProp Term.Null -> str "Prop"
diff --git a/translate/pptacticnew.ml b/translate/pptacticnew.ml
index 80298c3e..7da30c4e 100644
--- a/translate/pptacticnew.ml
+++ b/translate/pptacticnew.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: pptacticnew.ml,v 1.57.2.2 2004/07/16 19:31:52 herbelin Exp $ *)
+(* $Id: pptacticnew.ml,v 1.57.2.3 2005/05/15 12:47:03 herbelin Exp $ *)
open Pp
open Names
@@ -587,7 +587,8 @@ and pr_atom1 env = function
| TacTrivial (Some []) as x -> pr_atom0 env x
| TacTrivial db -> hov 0 (str "trivial" ++ pr_hintbases db)
| TacAuto (None,Some []) as x -> pr_atom0 env x
- | TacAuto (n,db) -> hov 0 (str "auto" ++ pr_opt int n ++ pr_hintbases db)
+ | TacAuto (n,db) ->
+ hov 0 (str "auto" ++ pr_opt (pr_or_var int) n ++ pr_hintbases db)
(* | TacAutoTDB None as x -> pr_atom0 env x
| TacAutoTDB (Some n) -> hov 0 (str "autotdb" ++ spc () ++ int n)
| TacDestructHyp (true,id) ->
@@ -599,7 +600,8 @@ and pr_atom1 env = function
hov 1 (str "superauto" ++ pr_opt int n ++ pr_autoarg_adding l ++
pr_autoarg_destructing b1 ++ pr_autoarg_usingTDB b2)*)
| TacDAuto (n,p) ->
- hov 1 (str "auto" ++ pr_opt int n ++ str "decomp" ++ pr_opt int p)
+ hov 1 (str "auto" ++ pr_opt (pr_or_var int) n ++ str "decomp" ++
+ pr_opt int p)
(* Context management *)
| TacClear l ->
diff --git a/translate/ppvernacnew.ml b/translate/ppvernacnew.ml
index bfcbee43..2e921c4e 100644
--- a/translate/ppvernacnew.ml
+++ b/translate/ppvernacnew.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: ppvernacnew.ml,v 1.95.2.3 2004/10/12 10:10:29 herbelin Exp $ *)
+(* $Id: ppvernacnew.ml,v 1.95.2.4 2005/12/23 22:16:56 herbelin Exp $ *)
open Pp
open Names
@@ -48,9 +48,12 @@ let pr_module r =
Ident (loc,id_of_string s)
| Qualid (loc,qid) ->
Qualid (loc,make_qualid (fst (repr_qualid qid)) (id_of_string s)) in
- let (_,dir,_) =
+ let dir =
try
- Library.locate_qualified_library (snd (qualid_of_reference r))
+ Nametab.full_name_module (snd (qualid_of_reference r))
+ with _ ->
+ try
+ pi2 (Library.locate_qualified_library (snd (qualid_of_reference r)))
with _ ->
errorlabstrm "" (str"Translator cannot find " ++ Libnames.pr_reference r)
in
@@ -1032,7 +1035,7 @@ let rec pr_vernac = function
| PrintImplicit qid -> str"Print Implicit" ++ spc() ++ pr_reference qid
in pr_printable p
| VernacSearch (sea,sea_r) -> pr_search sea sea_r pr_pattern
- | VernacLocate loc ->
+ | VernacLocate loc ->
let pr_locate =function
| LocateTerm qid -> pr_reference qid
| LocateFile f -> str"File" ++ spc() ++ qsnew f