aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--.depend223
-rw-r--r--.depend.coq8
-rw-r--r--COPYRIGHT7
-rw-r--r--Makefile40
-rwxr-xr-xconfigure9
-rw-r--r--contrib/interface/COPYRIGHT4
-rw-r--r--contrib/interface/centaur.ml4357
-rw-r--r--contrib/interface/name_to_ast.mli4
-rw-r--r--contrib/interface/parse.ml25
-rw-r--r--contrib/interface/translate.ml3
-rw-r--r--contrib/interface/translate.mli1
-rw-r--r--contrib/interface/vtp.ml1563
-rw-r--r--contrib/interface/vtp.mli27
-rw-r--r--contrib/interface/xlate.ml6
-rw-r--r--contrib/interface/xlate.mli1
-rw-r--r--lib/pp.ml41
-rw-r--r--lib/pp.mli1
-rw-r--r--library/lib.ml53
-rw-r--r--library/lib.mli4
-rw-r--r--parsing/ppconstr.ml26
-rw-r--r--parsing/ppconstr.mli10
-rw-r--r--parsing/prettyp.ml194
-rw-r--r--parsing/prettyp.mli21
-rw-r--r--parsing/printer.ml41
-rw-r--r--parsing/printer.mli10
-rw-r--r--toplevel/vernacentries.ml10
-rw-r--r--toplevel/vernacentries.mli5
27 files changed, 1533 insertions, 1121 deletions
diff --git a/.depend b/.depend
index b16a0e1c4..287e706e5 100644
--- a/.depend
+++ b/.depend
@@ -145,10 +145,11 @@ parsing/ppvernac.cmi: toplevel/vernacexpr.cmo lib/util.cmi \
interp/ppextend.cmi parsing/ppconstr.cmi lib/pp.cmi parsing/pcoq.cmi \
library/nametab.cmi kernel/names.cmi library/nameops.cmi \
library/libnames.cmi interp/genarg.cmi
-parsing/prettyp.cmi: lib/util.cmi pretyping/termops.cmi kernel/term.cmi \
- kernel/sign.cmi kernel/safe_typing.cmi pretyping/reductionops.cmi \
- lib/pp.cmi library/nametab.cmi kernel/names.cmi library/libnames.cmi \
- library/lib.cmi library/impargs.cmi kernel/environ.cmi \
+parsing/prettyp.cmi: lib/util.cmi interp/topconstr.cmi pretyping/termops.cmi \
+ kernel/term.cmi kernel/sign.cmi kernel/safe_typing.cmi \
+ pretyping/reductionops.cmi lib/pp.cmi library/nametab.cmi \
+ kernel/names.cmi library/libobject.cmi library/libnames.cmi \
+ library/lib.cmi library/impargs.cmi pretyping/evd.cmi kernel/environ.cmi \
pretyping/classops.cmi
parsing/printer.cmi: pretyping/termops.cmi kernel/term.cmi kernel/sign.cmi \
pretyping/rawterm.cmi proofs/proof_type.cmi lib/pp.cmi \
@@ -368,8 +369,9 @@ toplevel/searchisos.cmi: kernel/term.cmi kernel/names.cmi \
library/libobject.cmi
toplevel/toplevel.cmi: lib/pp.cmi parsing/pcoq.cmi
toplevel/vernacentries.cmi: toplevel/vernacinterp.cmi toplevel/vernacexpr.cmo \
- lib/util.cmi interp/topconstr.cmi kernel/term.cmi kernel/names.cmi \
- library/libnames.cmi pretyping/evd.cmi kernel/environ.cmi
+ lib/util.cmi interp/topconstr.cmi kernel/term.cmi \
+ pretyping/reductionops.cmi kernel/names.cmi library/libnames.cmi \
+ pretyping/evd.cmi kernel/environ.cmi
toplevel/vernacinterp.cmi: proofs/tacexpr.cmo
toplevel/vernac.cmi: toplevel/vernacexpr.cmo lib/util.cmi parsing/pcoq.cmi
toplevel/whelp.cmi: interp/topconstr.cmi kernel/term.cmi kernel/names.cmi \
@@ -466,8 +468,8 @@ contrib/interface/dad.cmi: interp/topconstr.cmi proofs/tacmach.cmi \
proofs/tacexpr.cmo proofs/proof_type.cmi
contrib/interface/debug_tac.cmi: proofs/tacmach.cmi proofs/tacexpr.cmo \
proofs/proof_type.cmi pretyping/evd.cmi
-contrib/interface/name_to_ast.cmi: toplevel/vernacexpr.cmo \
- library/libnames.cmi
+contrib/interface/name_to_ast.cmi: toplevel/vernacexpr.cmo kernel/names.cmi \
+ library/libobject.cmi library/libnames.cmi
contrib/interface/pbp.cmi: proofs/tacexpr.cmo proofs/proof_type.cmi \
kernel/names.cmi
contrib/interface/showproof.cmi: toplevel/vernacinterp.cmi lib/util.cmi \
@@ -479,7 +481,7 @@ contrib/interface/showproof.cmi: toplevel/vernacinterp.cmi lib/util.cmi \
pretyping/clenv.cmi contrib/interface/ascent.cmi
contrib/interface/translate.cmi: kernel/term.cmi proofs/proof_type.cmi \
pretyping/evd.cmi kernel/environ.cmi contrib/interface/ascent.cmi
-contrib/interface/vtp.cmi: contrib/interface/ascent.cmi
+contrib/interface/vtp.cmi: lib/pp.cmi contrib/interface/ascent.cmi
contrib/interface/xlate.cmi: toplevel/vernacexpr.cmo interp/topconstr.cmi \
proofs/tacexpr.cmo kernel/names.cmi contrib/interface/ascent.cmi
contrib/jprover/jall.cmi: contrib/jprover/opname.cmi \
@@ -1176,19 +1178,19 @@ parsing/pcoq.cmx: lib/util.cmx interp/topconstr.cmx proofs/tacexpr.cmx \
kernel/names.cmx library/libnames.cmx parsing/lexer.cmx interp/genarg.cmx \
parsing/extend.cmx library/decl_kinds.cmx parsing/pcoq.cmi
parsing/ppconstr.cmo: lib/util.cmi kernel/univ.cmi interp/topconstr.cmi \
- pretyping/termops.cmi kernel/term.cmi pretyping/rawterm.cmi \
- interp/ppextend.cmi lib/pp.cmi pretyping/pattern.cmi lib/options.cmi \
- interp/notation.cmi library/nametab.cmi kernel/names.cmi \
- library/nameops.cmi library/libnames.cmi interp/genarg.cmi \
- pretyping/evd.cmi interp/constrextern.cmi lib/bigint.cmi \
- parsing/ppconstr.cmi
+ pretyping/termops.cmi kernel/term.cmi proofs/tacexpr.cmo \
+ pretyping/rawterm.cmi interp/ppextend.cmi lib/pp.cmi \
+ pretyping/pattern.cmi lib/options.cmi interp/notation.cmi \
+ library/nametab.cmi kernel/names.cmi library/nameops.cmi \
+ library/libnames.cmi interp/genarg.cmi pretyping/evd.cmi \
+ interp/constrextern.cmi lib/bigint.cmi parsing/ppconstr.cmi
parsing/ppconstr.cmx: lib/util.cmx kernel/univ.cmx interp/topconstr.cmx \
- pretyping/termops.cmx kernel/term.cmx pretyping/rawterm.cmx \
- interp/ppextend.cmx lib/pp.cmx pretyping/pattern.cmx lib/options.cmx \
- interp/notation.cmx library/nametab.cmx kernel/names.cmx \
- library/nameops.cmx library/libnames.cmx interp/genarg.cmx \
- pretyping/evd.cmx interp/constrextern.cmx lib/bigint.cmx \
- parsing/ppconstr.cmi
+ pretyping/termops.cmx kernel/term.cmx proofs/tacexpr.cmx \
+ pretyping/rawterm.cmx interp/ppextend.cmx lib/pp.cmx \
+ pretyping/pattern.cmx lib/options.cmx interp/notation.cmx \
+ library/nametab.cmx kernel/names.cmx library/nameops.cmx \
+ library/libnames.cmx interp/genarg.cmx pretyping/evd.cmx \
+ interp/constrextern.cmx lib/bigint.cmx parsing/ppconstr.cmi
parsing/ppdecl_proof.cmo: lib/util.cmi kernel/term.cmi parsing/printer.cmi \
parsing/pptactic.cmi parsing/ppconstr.cmi lib/pp.cmi kernel/names.cmi \
library/nameops.cmi kernel/environ.cmi proofs/decl_expr.cmi \
@@ -1229,26 +1231,28 @@ parsing/ppvernac.cmx: toplevel/vernacexpr.cmx lib/util.cmx \
library/impargs.cmx library/goptions.cmx library/global.cmx \
interp/genarg.cmx parsing/extend.cmx parsing/egrammar.cmx \
library/declaremods.cmx library/decl_kinds.cmx parsing/ppvernac.cmi
-parsing/prettyp.cmo: lib/util.cmi pretyping/termops.cmi kernel/term.cmi \
- interp/syntax_def.cmi kernel/sign.cmi kernel/safe_typing.cmi \
- pretyping/reductionops.cmi kernel/reduction.cmi pretyping/recordops.cmi \
- parsing/printmod.cmi parsing/printer.cmi lib/pp.cmi interp/notation.cmi \
- library/nametab.cmi kernel/names.cmi library/nameops.cmi \
- library/libobject.cmi library/libnames.cmi library/lib.cmi \
- pretyping/inductiveops.cmi kernel/inductive.cmi library/impargs.cmi \
- library/global.cmi pretyping/evd.cmi kernel/environ.cmi \
- library/declare.cmi kernel/declarations.cmi kernel/conv_oracle.cmi \
- interp/constrextern.cmi pretyping/classops.cmi parsing/prettyp.cmi
-parsing/prettyp.cmx: lib/util.cmx pretyping/termops.cmx kernel/term.cmx \
- interp/syntax_def.cmx kernel/sign.cmx kernel/safe_typing.cmx \
- pretyping/reductionops.cmx kernel/reduction.cmx pretyping/recordops.cmx \
- parsing/printmod.cmx parsing/printer.cmx lib/pp.cmx interp/notation.cmx \
- library/nametab.cmx kernel/names.cmx library/nameops.cmx \
- library/libobject.cmx library/libnames.cmx library/lib.cmx \
- pretyping/inductiveops.cmx kernel/inductive.cmx library/impargs.cmx \
- library/global.cmx pretyping/evd.cmx kernel/environ.cmx \
- library/declare.cmx kernel/declarations.cmx kernel/conv_oracle.cmx \
- interp/constrextern.cmx pretyping/classops.cmx parsing/prettyp.cmi
+parsing/prettyp.cmo: lib/util.cmi interp/topconstr.cmi pretyping/termops.cmi \
+ kernel/term.cmi interp/syntax_def.cmi kernel/sign.cmi \
+ kernel/safe_typing.cmi pretyping/reductionops.cmi kernel/reduction.cmi \
+ pretyping/recordops.cmi parsing/printmod.cmi parsing/printer.cmi \
+ lib/pp.cmi interp/notation.cmi library/nametab.cmi kernel/names.cmi \
+ library/nameops.cmi library/libobject.cmi library/libnames.cmi \
+ library/lib.cmi pretyping/inductiveops.cmi kernel/inductive.cmi \
+ library/impargs.cmi library/global.cmi pretyping/evd.cmi \
+ kernel/environ.cmi library/declare.cmi kernel/declarations.cmi \
+ kernel/conv_oracle.cmi interp/constrextern.cmi pretyping/classops.cmi \
+ parsing/prettyp.cmi
+parsing/prettyp.cmx: lib/util.cmx interp/topconstr.cmx pretyping/termops.cmx \
+ kernel/term.cmx interp/syntax_def.cmx kernel/sign.cmx \
+ kernel/safe_typing.cmx pretyping/reductionops.cmx kernel/reduction.cmx \
+ pretyping/recordops.cmx parsing/printmod.cmx parsing/printer.cmx \
+ lib/pp.cmx interp/notation.cmx library/nametab.cmx kernel/names.cmx \
+ library/nameops.cmx library/libobject.cmx library/libnames.cmx \
+ library/lib.cmx pretyping/inductiveops.cmx kernel/inductive.cmx \
+ library/impargs.cmx library/global.cmx pretyping/evd.cmx \
+ kernel/environ.cmx library/declare.cmx kernel/declarations.cmx \
+ kernel/conv_oracle.cmx interp/constrextern.cmx pretyping/classops.cmx \
+ parsing/prettyp.cmi
parsing/printer.cmo: lib/util.cmi pretyping/termops.cmi kernel/term.cmi \
kernel/sign.cmi proofs/refiner.cmi proofs/proof_type.cmi \
parsing/ppconstr.cmi lib/pp.cmi proofs/pfedit.cmi lib/options.cmi \
@@ -2255,12 +2259,13 @@ toplevel/command.cmo: toplevel/vernacexpr.cmo lib/util.cmi kernel/typeops.cmi \
library/nametab.cmi kernel/names.cmi library/nameops.cmi \
toplevel/metasyntax.cmi proofs/logic.cmi library/library.cmi \
library/libobject.cmi library/libnames.cmi library/lib.cmi \
- kernel/inductive.cmi kernel/indtypes.cmi pretyping/indrec.cmi \
- library/impargs.cmi library/global.cmi pretyping/evd.cmi \
- pretyping/evarutil.cmi pretyping/evarconv.cmi kernel/environ.cmi \
- kernel/entries.cmi library/declare.cmi kernel/declarations.cmi \
- library/decl_kinds.cmo interp/constrintern.cmi interp/constrextern.cmi \
- toplevel/class.cmi toplevel/command.cmi
+ pretyping/inductiveops.cmi kernel/inductive.cmi kernel/indtypes.cmi \
+ pretyping/indrec.cmi library/impargs.cmi library/global.cmi \
+ pretyping/evd.cmi pretyping/evarutil.cmi pretyping/evarconv.cmi \
+ kernel/environ.cmi kernel/entries.cmi library/declare.cmi \
+ kernel/declarations.cmi library/decl_kinds.cmo interp/coqlib.cmi \
+ interp/constrintern.cmi interp/constrextern.cmi toplevel/class.cmi \
+ toplevel/command.cmi
toplevel/command.cmx: toplevel/vernacexpr.cmx lib/util.cmx kernel/typeops.cmx \
interp/topconstr.cmx pretyping/termops.cmx kernel/term.cmx \
proofs/tacmach.cmx interp/syntax_def.cmx library/states.cmx \
@@ -2271,12 +2276,13 @@ toplevel/command.cmx: toplevel/vernacexpr.cmx lib/util.cmx kernel/typeops.cmx \
library/nametab.cmx kernel/names.cmx library/nameops.cmx \
toplevel/metasyntax.cmx proofs/logic.cmx library/library.cmx \
library/libobject.cmx library/libnames.cmx library/lib.cmx \
- kernel/inductive.cmx kernel/indtypes.cmx pretyping/indrec.cmx \
- library/impargs.cmx library/global.cmx pretyping/evd.cmx \
- pretyping/evarutil.cmx pretyping/evarconv.cmx kernel/environ.cmx \
- kernel/entries.cmx library/declare.cmx kernel/declarations.cmx \
- library/decl_kinds.cmx interp/constrintern.cmx interp/constrextern.cmx \
- toplevel/class.cmx toplevel/command.cmi
+ pretyping/inductiveops.cmx kernel/inductive.cmx kernel/indtypes.cmx \
+ pretyping/indrec.cmx library/impargs.cmx library/global.cmx \
+ pretyping/evd.cmx pretyping/evarutil.cmx pretyping/evarconv.cmx \
+ kernel/environ.cmx kernel/entries.cmx library/declare.cmx \
+ kernel/declarations.cmx library/decl_kinds.cmx interp/coqlib.cmx \
+ interp/constrintern.cmx interp/constrextern.cmx toplevel/class.cmx \
+ toplevel/command.cmi
toplevel/coqinit.cmo: toplevel/vernac.cmi toplevel/toplevel.cmi \
lib/system.cmi lib/pp.cmi lib/options.cmi kernel/names.cmi \
library/nameops.cmi toplevel/mltop.cmi config/coq_config.cmi \
@@ -3252,8 +3258,9 @@ contrib/interface/centaur.cmo: contrib/interface/xlate.cmi \
contrib/interface/showproof.cmi parsing/search.cmi proofs/refiner.cmi \
kernel/reduction.cmi pretyping/rawterm.cmi toplevel/protectedtoplevel.cmi \
proofs/proof_type.cmi proofs/proof_trees.cmi parsing/printer.cmi \
- pretyping/pretyping.cmi parsing/pptactic.cmi lib/pp.cmi proofs/pfedit.cmi \
- parsing/pcoq.cmi contrib/interface/pbp.cmi library/nametab.cmi \
+ pretyping/pretyping.cmi parsing/prettyp.cmi parsing/pptactic.cmi \
+ parsing/ppconstr.cmi lib/pp.cmi proofs/pfedit.cmi parsing/pcoq.cmi \
+ contrib/interface/pbp.cmi lib/options.cmi library/nametab.cmi \
kernel/names.cmi library/nameops.cmi contrib/interface/name_to_ast.cmi \
pretyping/matching.cmi toplevel/line_oriented_parser.cmi \
library/library.cmi library/libobject.cmi library/libnames.cmi \
@@ -3272,8 +3279,9 @@ contrib/interface/centaur.cmx: contrib/interface/xlate.cmx \
contrib/interface/showproof.cmx parsing/search.cmx proofs/refiner.cmx \
kernel/reduction.cmx pretyping/rawterm.cmx toplevel/protectedtoplevel.cmx \
proofs/proof_type.cmx proofs/proof_trees.cmx parsing/printer.cmx \
- pretyping/pretyping.cmx parsing/pptactic.cmx lib/pp.cmx proofs/pfedit.cmx \
- parsing/pcoq.cmx contrib/interface/pbp.cmx library/nametab.cmx \
+ pretyping/pretyping.cmx parsing/prettyp.cmx parsing/pptactic.cmx \
+ parsing/ppconstr.cmx lib/pp.cmx proofs/pfedit.cmx parsing/pcoq.cmx \
+ contrib/interface/pbp.cmx lib/options.cmx library/nametab.cmx \
kernel/names.cmx library/nameops.cmx contrib/interface/name_to_ast.cmx \
pretyping/matching.cmx toplevel/line_oriented_parser.cmx \
library/library.cmx library/libobject.cmx library/libnames.cmx \
@@ -3417,9 +3425,9 @@ contrib/interface/translate.cmx: contrib/interface/xlate.cmx \
library/libobject.cmx pretyping/evd.cmx pretyping/evarutil.cmx \
kernel/environ.cmx interp/constrextern.cmx contrib/interface/ascent.cmi \
contrib/interface/translate.cmi
-contrib/interface/vtp.cmo: contrib/interface/ascent.cmi \
+contrib/interface/vtp.cmo: lib/pp.cmi contrib/interface/ascent.cmi \
contrib/interface/vtp.cmi
-contrib/interface/vtp.cmx: contrib/interface/ascent.cmi \
+contrib/interface/vtp.cmx: lib/pp.cmx contrib/interface/ascent.cmi \
contrib/interface/vtp.cmi
contrib/interface/xlate.cmo: toplevel/vernacexpr.cmo lib/util.cmi \
interp/topconstr.cmi kernel/term.cmi proofs/tacexpr.cmo \
@@ -3706,21 +3714,23 @@ contrib/subtac/g_subtac.cmx: toplevel/vernacinterp.cmx \
contrib/subtac/subtac_cases.cmo: lib/util.cmi kernel/typeops.cmi \
kernel/type_errors.cmi pretyping/termops.cmi kernel/term.cmi \
contrib/subtac/subtac_utils.cmi kernel/sign.cmi pretyping/retyping.cmi \
- pretyping/reductionops.cmi pretyping/rawterm.cmi \
- pretyping/pretype_errors.cmi lib/pp.cmi kernel/names.cmi \
- library/nameops.cmi pretyping/inductiveops.cmi kernel/inductive.cmi \
- library/global.cmi pretyping/evd.cmi pretyping/evarutil.cmi \
- pretyping/evarconv.cmi kernel/environ.cmi kernel/declarations.cmi \
- pretyping/coercion.cmi kernel/closure.cmi contrib/subtac/subtac_cases.cmi
+ pretyping/reductionops.cmi pretyping/rawterm.cmi parsing/printer.cmi \
+ pretyping/pretype_errors.cmi parsing/prettyp.cmi lib/pp.cmi \
+ kernel/names.cmi library/nameops.cmi pretyping/inductiveops.cmi \
+ kernel/inductive.cmi library/global.cmi pretyping/evd.cmi \
+ pretyping/evarutil.cmi pretyping/evarconv.cmi kernel/environ.cmi \
+ kernel/declarations.cmi pretyping/coercion.cmi kernel/closure.cmi \
+ contrib/subtac/subtac_cases.cmi
contrib/subtac/subtac_cases.cmx: lib/util.cmx kernel/typeops.cmx \
kernel/type_errors.cmx pretyping/termops.cmx kernel/term.cmx \
contrib/subtac/subtac_utils.cmx kernel/sign.cmx pretyping/retyping.cmx \
- pretyping/reductionops.cmx pretyping/rawterm.cmx \
- pretyping/pretype_errors.cmx lib/pp.cmx kernel/names.cmx \
- library/nameops.cmx pretyping/inductiveops.cmx kernel/inductive.cmx \
- library/global.cmx pretyping/evd.cmx pretyping/evarutil.cmx \
- pretyping/evarconv.cmx kernel/environ.cmx kernel/declarations.cmx \
- pretyping/coercion.cmx kernel/closure.cmx contrib/subtac/subtac_cases.cmi
+ pretyping/reductionops.cmx pretyping/rawterm.cmx parsing/printer.cmx \
+ pretyping/pretype_errors.cmx parsing/prettyp.cmx lib/pp.cmx \
+ kernel/names.cmx library/nameops.cmx pretyping/inductiveops.cmx \
+ kernel/inductive.cmx library/global.cmx pretyping/evd.cmx \
+ pretyping/evarutil.cmx pretyping/evarconv.cmx kernel/environ.cmx \
+ kernel/declarations.cmx pretyping/coercion.cmx kernel/closure.cmx \
+ contrib/subtac/subtac_cases.cmi
contrib/subtac/subtac_coercion.cmo: lib/util.cmi kernel/typeops.cmi \
pretyping/termops.cmi kernel/term.cmi contrib/subtac/subtac_utils.cmi \
contrib/subtac/subtac_errors.cmi pretyping/retyping.cmi \
@@ -3809,8 +3819,9 @@ contrib/subtac/subtac_interp_fixpoint.cmx: lib/util.cmx kernel/typeops.cmx \
contrib/subtac/subtac_interp_fixpoint.cmi
contrib/subtac/subtac.cmo: toplevel/vernacexpr.cmo lib/util.cmi \
kernel/typeops.cmi kernel/type_errors.cmi pretyping/termops.cmi \
- kernel/term.cmi contrib/subtac/subtac_utils.cmi \
- contrib/subtac/subtac_pretyping.cmi contrib/subtac/subtac_errors.cmi \
+ kernel/term.cmi tactics/tacinterp.cmi proofs/tacexpr.cmo \
+ contrib/subtac/subtac_utils.cmi contrib/subtac/subtac_pretyping.cmi \
+ contrib/subtac/subtac_obligations.cmi contrib/subtac/subtac_errors.cmi \
contrib/subtac/subtac_command.cmi contrib/subtac/subtac_coercion.cmi \
kernel/sign.cmi pretyping/reductionops.cmi pretyping/recordops.cmi \
pretyping/rawterm.cmi parsing/printer.cmi pretyping/pretype_errors.cmi \
@@ -3824,8 +3835,9 @@ contrib/subtac/subtac.cmo: toplevel/vernacexpr.cmo lib/util.cmi \
toplevel/cerrors.cmi contrib/subtac/subtac.cmi
contrib/subtac/subtac.cmx: toplevel/vernacexpr.cmx lib/util.cmx \
kernel/typeops.cmx kernel/type_errors.cmx pretyping/termops.cmx \
- kernel/term.cmx contrib/subtac/subtac_utils.cmx \
- contrib/subtac/subtac_pretyping.cmx contrib/subtac/subtac_errors.cmx \
+ kernel/term.cmx tactics/tacinterp.cmx proofs/tacexpr.cmx \
+ contrib/subtac/subtac_utils.cmx contrib/subtac/subtac_pretyping.cmx \
+ contrib/subtac/subtac_obligations.cmx contrib/subtac/subtac_errors.cmx \
contrib/subtac/subtac_command.cmx contrib/subtac/subtac_coercion.cmx \
kernel/sign.cmx pretyping/reductionops.cmx pretyping/recordops.cmx \
pretyping/rawterm.cmx parsing/printer.cmx pretyping/pretype_errors.cmx \
@@ -4180,38 +4192,39 @@ tools/coq_makefile.cmx:
tools/coq-tex.cmo:
tools/coq-tex.cmx:
coq_fix_code.o: kernel/byterun/coq_fix_code.c \
- /usr/local/lib/ocaml/caml/config.h \
- /usr/local/lib/ocaml/caml/compatibility.h \
- /usr/local/lib/ocaml/caml/misc.h /usr/local/lib/ocaml/caml/config.h \
- /usr/local/lib/ocaml/caml/mlvalues.h /usr/local/lib/ocaml/caml/misc.h \
- /usr/local/lib/ocaml/caml/fail.h /usr/local/lib/ocaml/caml/mlvalues.h \
- /usr/local/lib/ocaml/caml/memory.h kernel/byterun/coq_instruct.h \
+ /usr/lib/ocaml/3.09.2/caml/config.h \
+ /usr/lib/ocaml/3.09.2/caml/compatibility.h \
+ /usr/lib/ocaml/3.09.2/caml/misc.h /usr/lib/ocaml/3.09.2/caml/config.h \
+ /usr/lib/ocaml/3.09.2/caml/mlvalues.h /usr/lib/ocaml/3.09.2/caml/misc.h \
+ /usr/lib/ocaml/3.09.2/caml/fail.h /usr/lib/ocaml/3.09.2/caml/mlvalues.h \
+ /usr/lib/ocaml/3.09.2/caml/memory.h kernel/byterun/coq_instruct.h \
kernel/byterun/coq_fix_code.h
coq_interp.o: kernel/byterun/coq_interp.c kernel/byterun/coq_gc.h \
- /usr/local/lib/ocaml/caml/mlvalues.h \
- /usr/local/lib/ocaml/caml/compatibility.h \
- /usr/local/lib/ocaml/caml/config.h /usr/local/lib/ocaml/caml/misc.h \
- /usr/local/lib/ocaml/caml/alloc.h /usr/local/lib/ocaml/caml/mlvalues.h \
- kernel/byterun/coq_instruct.h kernel/byterun/coq_fix_code.h \
- kernel/byterun/coq_memory.h /usr/local/lib/ocaml/caml/config.h \
- /usr/local/lib/ocaml/caml/fail.h /usr/local/lib/ocaml/caml/misc.h \
- /usr/local/lib/ocaml/caml/memory.h kernel/byterun/coq_values.h \
- kernel/byterun/coq_jumptbl.h
+ /usr/lib/ocaml/3.09.2/caml/mlvalues.h \
+ /usr/lib/ocaml/3.09.2/caml/compatibility.h \
+ /usr/lib/ocaml/3.09.2/caml/config.h /usr/lib/ocaml/3.09.2/caml/misc.h \
+ /usr/lib/ocaml/3.09.2/caml/alloc.h \
+ /usr/lib/ocaml/3.09.2/caml/mlvalues.h kernel/byterun/coq_instruct.h \
+ kernel/byterun/coq_fix_code.h kernel/byterun/coq_memory.h \
+ /usr/lib/ocaml/3.09.2/caml/config.h /usr/lib/ocaml/3.09.2/caml/fail.h \
+ /usr/lib/ocaml/3.09.2/caml/misc.h /usr/lib/ocaml/3.09.2/caml/memory.h \
+ kernel/byterun/coq_values.h kernel/byterun/coq_jumptbl.h
coq_memory.o: kernel/byterun/coq_memory.c kernel/byterun/coq_gc.h \
- /usr/local/lib/ocaml/caml/mlvalues.h \
- /usr/local/lib/ocaml/caml/compatibility.h \
- /usr/local/lib/ocaml/caml/config.h /usr/local/lib/ocaml/caml/misc.h \
- /usr/local/lib/ocaml/caml/alloc.h /usr/local/lib/ocaml/caml/mlvalues.h \
- kernel/byterun/coq_instruct.h kernel/byterun/coq_fix_code.h \
- kernel/byterun/coq_memory.h /usr/local/lib/ocaml/caml/config.h \
- /usr/local/lib/ocaml/caml/fail.h /usr/local/lib/ocaml/caml/misc.h \
- /usr/local/lib/ocaml/caml/memory.h kernel/byterun/coq_interp.h
+ /usr/lib/ocaml/3.09.2/caml/mlvalues.h \
+ /usr/lib/ocaml/3.09.2/caml/compatibility.h \
+ /usr/lib/ocaml/3.09.2/caml/config.h /usr/lib/ocaml/3.09.2/caml/misc.h \
+ /usr/lib/ocaml/3.09.2/caml/alloc.h \
+ /usr/lib/ocaml/3.09.2/caml/mlvalues.h kernel/byterun/coq_instruct.h \
+ kernel/byterun/coq_fix_code.h kernel/byterun/coq_memory.h \
+ /usr/lib/ocaml/3.09.2/caml/config.h /usr/lib/ocaml/3.09.2/caml/fail.h \
+ /usr/lib/ocaml/3.09.2/caml/misc.h /usr/lib/ocaml/3.09.2/caml/memory.h \
+ kernel/byterun/coq_interp.h
coq_values.o: kernel/byterun/coq_values.c kernel/byterun/coq_fix_code.h \
- /usr/local/lib/ocaml/caml/mlvalues.h \
- /usr/local/lib/ocaml/caml/compatibility.h \
- /usr/local/lib/ocaml/caml/config.h /usr/local/lib/ocaml/caml/misc.h \
+ /usr/lib/ocaml/3.09.2/caml/mlvalues.h \
+ /usr/lib/ocaml/3.09.2/caml/compatibility.h \
+ /usr/lib/ocaml/3.09.2/caml/config.h /usr/lib/ocaml/3.09.2/caml/misc.h \
kernel/byterun/coq_instruct.h kernel/byterun/coq_memory.h \
- /usr/local/lib/ocaml/caml/config.h /usr/local/lib/ocaml/caml/fail.h \
- /usr/local/lib/ocaml/caml/mlvalues.h /usr/local/lib/ocaml/caml/misc.h \
- /usr/local/lib/ocaml/caml/memory.h kernel/byterun/coq_values.h \
- /usr/local/lib/ocaml/caml/alloc.h
+ /usr/lib/ocaml/3.09.2/caml/config.h /usr/lib/ocaml/3.09.2/caml/fail.h \
+ /usr/lib/ocaml/3.09.2/caml/mlvalues.h /usr/lib/ocaml/3.09.2/caml/misc.h \
+ /usr/lib/ocaml/3.09.2/caml/memory.h kernel/byterun/coq_values.h \
+ /usr/lib/ocaml/3.09.2/caml/alloc.h
diff --git a/.depend.coq b/.depend.coq
index 702465857..3e8941e9d 100644
--- a/.depend.coq
+++ b/.depend.coq
@@ -32,6 +32,7 @@ theories/Reals/RIneq.vo: theories/Reals/RIneq.v theories/Reals/Raxioms.vo theori
theories/Reals/DiscrR.vo: theories/Reals/DiscrR.v theories/Reals/RIneq.vo contrib/omega/Omega.vo
theories/Reals/Rbase.vo: theories/Reals/Rbase.v theories/Reals/Rdefinitions.vo theories/Reals/Raxioms.vo theories/Reals/RIneq.vo theories/Reals/DiscrR.vo
theories/Reals/LegacyRfield.vo: theories/Reals/LegacyRfield.v theories/Reals/Raxioms.vo contrib/field/LegacyField.vo
+theories/Reals/Rpow_def.vo: theories/Reals/Rpow_def.v theories/Reals/Rdefinitions.vo
theories/Reals/R_Ifp.vo: theories/Reals/R_Ifp.v theories/Reals/Rbase.vo contrib/omega/Omega.vo
theories/Reals/Rbasic_fun.vo: theories/Reals/Rbasic_fun.v theories/Reals/Rbase.vo theories/Reals/R_Ifp.vo contrib/fourier/Fourier.vo
theories/Reals/R_sqr.vo: theories/Reals/R_sqr.v theories/Reals/Rbase.vo theories/Reals/Rbasic_fun.vo
@@ -279,6 +280,7 @@ theories/Reals/RIneq.vo: theories/Reals/RIneq.v theories/Reals/Raxioms.vo theori
theories/Reals/DiscrR.vo: theories/Reals/DiscrR.v theories/Reals/RIneq.vo contrib/omega/Omega.vo
theories/Reals/Rbase.vo: theories/Reals/Rbase.v theories/Reals/Rdefinitions.vo theories/Reals/Raxioms.vo theories/Reals/RIneq.vo theories/Reals/DiscrR.vo
theories/Reals/LegacyRfield.vo: theories/Reals/LegacyRfield.v theories/Reals/Raxioms.vo contrib/field/LegacyField.vo
+theories/Reals/Rpow_def.vo: theories/Reals/Rpow_def.v theories/Reals/Rdefinitions.vo
theories/Reals/R_Ifp.vo: theories/Reals/R_Ifp.v theories/Reals/Rbase.vo contrib/omega/Omega.vo
theories/Reals/Rbasic_fun.vo: theories/Reals/Rbasic_fun.v theories/Reals/Rbase.vo theories/Reals/R_Ifp.vo contrib/fourier/Fourier.vo
theories/Reals/R_sqr.vo: theories/Reals/R_sqr.v theories/Reals/Rbase.vo theories/Reals/Rbasic_fun.vo
@@ -359,8 +361,10 @@ contrib/field/LegacyField_Tactic.vo: contrib/field/LegacyField_Tactic.v theories
contrib/field/LegacyField.vo: contrib/field/LegacyField.v contrib/field/LegacyField_Compl.vo contrib/field/LegacyField_Theory.vo contrib/field/LegacyField_Tactic.vo
contrib/fourier/Fourier_util.vo: contrib/fourier/Fourier_util.v theories/Reals/Rbase.vo
contrib/fourier/Fourier.vo: contrib/fourier/Fourier.v contrib/ring/quote.cmo contrib/ring/ring.cmo contrib/fourier/fourier.cmo contrib/fourier/fourierR.cmo contrib/field/field.cmo contrib/fourier/Fourier_util.vo contrib/field/LegacyField.vo theories/Reals/DiscrR.vo
-contrib/subtac/FixSub.vo: contrib/subtac/FixSub.v theories/Init/Wf.vo theories/Arith/Wf_nat.vo theories/Arith/Lt.vo
-contrib/subtac/Utils.vo: contrib/subtac/Utils.v
+contrib/subtac/Utils.vo: contrib/subtac/Utils.v theories/Logic/ProofIrrelevance.vo
+contrib/subtac/FixSub.vo: contrib/subtac/FixSub.v theories/Init/Wf.vo contrib/subtac/Utils.vo theories/Arith/Wf_nat.vo theories/Arith/Lt.vo
+contrib/subtac/Subtac.vo: contrib/subtac/Subtac.v contrib/subtac/Utils.vo contrib/subtac/FixSub.vo
+contrib/subtac/FunctionalExtensionality.vo: contrib/subtac/FunctionalExtensionality.v contrib/subtac/Utils.vo contrib/subtac/FixSub.vo
contrib/rtauto/Bintree.vo: contrib/rtauto/Bintree.v theories/Lists/List.vo theories/NArith/BinPos.vo
contrib/rtauto/Rtauto.vo: contrib/rtauto/Rtauto.v theories/Lists/List.vo contrib/rtauto/Bintree.vo theories/Bool/Bool.vo theories/NArith/BinPos.vo
contrib/recdef/Recdef.vo: contrib/recdef/Recdef.v theories/Arith/Compare_dec.vo theories/Arith/Wf_nat.vo
diff --git a/COPYRIGHT b/COPYRIGHT
index ac7d87dfa..2cbb6fbce 100644
--- a/COPYRIGHT
+++ b/COPYRIGHT
@@ -5,6 +5,13 @@ University Paris Sud.
Copyright 1999-2004 The Coq development team,
INRIA-CNRS, University Paris Sud, All rights reserved.
+This version contains modifications by Lionel Elie Mamane
+<lionel@mamane.lu> done while under employment of the Radboud
+University Nijmegen. However, no copyright-assignment-to-employer
+agreement was signed, and copyright of articles and books written on
+work time rest with the employee. By analogy, it is Lionel's opinion
+that copyright on these changes rests with him.
+
This product includes also software developed by
Yves Bertot, Lemme, INRIA Sophia-Antipolis (contrib/interface,
parsing/search.ml)
diff --git a/Makefile b/Makefile
index e7bdfdde4..bf642dd7f 100644
--- a/Makefile
+++ b/Makefile
@@ -620,7 +620,11 @@ beforedepend:: ide/utf8_convert.ml
COQIDEVO=ide/utf8.vo
-$(COQIDEVO): states/initial.coq
+ifdef NO_RECOMPILE_LIB
+ $(COQIDEVO): | states/initial.coq
+else
+ $(COQIDEVO): states/initial.coq
+endif
$(BOOTCOQTOP) -compile $*
IDEFILES=$(COQIDEVO) ide/utf8.v ide/coq.png ide/.coqide-gtk2rc
@@ -961,7 +965,7 @@ REALSBASEVO=\
theories/Reals/Rdefinitions.vo \
theories/Reals/Raxioms.vo theories/Reals/RIneq.vo \
theories/Reals/DiscrR.vo theories/Reals/Rbase.vo \
- theories/Reals/LegacyRfield.vo
+ theories/Reals/LegacyRfield.vo theories/Reals/Rpow_def.vo
REALS_basic=
@@ -1086,7 +1090,11 @@ CONTRIBVO = $(OMEGAVO) $(ROMEGAVO) $(RINGVO) $(FIELDVO) $(XMLVO) \
$(FOURIERVO) $(JPROVERVO) $(CCVO) $(FUNINDVO) $(SUBTACVO) \
$(RTAUTOVO) $(RECDEFVO) $(NEWRINGVO)
-$(CONTRIBVO): states/initial.coq
+ifdef NO_RECOMPILE_LIB
+ $(CONTRIBVO): | states/initial.coq
+else
+ $(CONTRIBVO): states/initial.coq
+endif
contrib: $(CONTRIBVO) $(CONTRIBCMO)
omega: $(OMEGAVO) $(OMEGACMO) $(ROMEGAVO) $(ROMEGACMO)
@@ -1114,10 +1122,18 @@ SYNTAXPP=syntax/PPConstr.v syntax/PPCases.v
states/initial.coq: states/MakeInitial.v $(INITVO)
$(BOOTCOQTOP) -batch -notop -silent -nois -load-vernac-source states/MakeInitial.v -outputstate states/initial.coq
-theories/Init/%.vo: $(BESTCOQTOP) theories/Init/%.v
+ifdef NO_RECOMPILE_LIB
+ theories/Init/%.vo: theories/Init/%.v | $(BESTCOQTOP)
+else
+ theories/Init/%.vo: $(BESTCOQTOP) theories/Init/%.v
+endif
$(BOOTCOQTOP) -nois -compile theories/Init/$*
-theories/%.vo: theories/%.v states/initial.coq
+ifdef NO_RECOMPILE_LIB
+ theories/%.vo: theories/%.v | states/initial.coq
+else
+ theories/%.vo: theories/%.v states/initial.coq
+endif
$(BOOTCOQTOP) -compile theories/$*
contrib/%.vo: contrib/%.v
@@ -1595,14 +1611,22 @@ parsing/lexer.cmo: parsing/lexer.ml4
.PHONY: revision
revision:
-ifeq ($(CHECKEDOUT),1)
+ifeq ($(CHECKEDOUT),svn)
- /bin/rm -f revision
- if test -x `which svn`; then \
- export LANG=C; \
+ if test -x "`which svn`"; then \
+ LANG=C; export LANG; \
svn info . | sed -ne '/URL/s/.*\/\([^\/]\{1,\}\)/\1/p' > revision; \
svn info . | sed -ne '/Revision/s/Revision: \([0-9]\{1,\}\)/\1/p'>> revision; \
fi
endif
+ifeq ($(CHECKEDOUT),gnuarch)
+ - /bin/rm -f revision
+ if test -x "`which tla`"; then \
+ LANG=C; export LANG; \
+ tla tree-version > revision ; \
+ tla tree-revision | sed -ne 's|.*--||p' >> revision ; \
+ fi
+endif
archclean::
/bin/rm -f revision
diff --git a/configure b/configure
index 9b2bdb1bc..e059f4d30 100755
--- a/configure
+++ b/configure
@@ -260,10 +260,13 @@ case $ARCH in
fi
esac
-# Is the source tree checked out from svn ?
+# Is the source tree checked out from a recognised
+# version control system ?
if test -e .svn/entries ; then
- checkedout=1
-else
+ checkedout=svn
+elif [ -d '{arch}' ]; then
+ checkedout=gnuarch
+else
checkedout=0
fi
diff --git a/contrib/interface/COPYRIGHT b/contrib/interface/COPYRIGHT
index 2fb11c6bc..ff567a546 100644
--- a/contrib/interface/COPYRIGHT
+++ b/contrib/interface/COPYRIGHT
@@ -3,6 +3,7 @@
(* Coq support for the Pcoq Graphical Interface of Coq *)
(* *)
(* Copyright (C) 1999-2004 INRIA Sophia-Antipolis (Lemme team) *)
+(* Copyright (C) 2006 Lionel Elie Mamane *)
(* *)
(*****************************************************************************)
@@ -10,6 +11,9 @@ The current directory contrib/interface implements Coq support for the
Pcoq Graphical Interface of Coq. It has been developed by Yves Bertot
with contributions from Loïc Pottier and Laurence Rideau.
+Modifications by Lionel Elie Mamane <lionel@mamane.lu> for
+generalising the protocol to suit other Coq interfaces.
+
The Pcoq Graphical Interface (see http://www-sop.inria.fr/lemme/pcoq)
is developed by the Lemme team at INRIA Sophia-Antipolis (see
http://www-sop.inria.fr/lemme)
diff --git a/contrib/interface/centaur.ml4 b/contrib/interface/centaur.ml4
index 730e055b4..30c96f939 100644
--- a/contrib/interface/centaur.ml4
+++ b/contrib/interface/centaur.ml4
@@ -1,11 +1,23 @@
(*i camlp4deps: "parsing/grammar.cma" i*)
+(*
+ * This file has been modified by Lionel Elie Mamane <lionel@mamane.lu>
+ * to implement the following features
+ * - Terms (optionally) as pretty-printed string and not trees
+ * - (Optionally) give most commands their usual Coq semantics
+ * - Add the backtracking information to the status message.
+ * in the following time period
+ * - May-November 2006
+ *)
+
(*Toplevel loop for the communication between Coq and Centaur *)
open Names;;
open Nameops;;
open Util;;
open Term;;
open Pp;;
+open Ppconstr;;
+open Prettyp;;
open Libnames;;
open Libobject;;
open Library;;
@@ -43,6 +55,7 @@ open Showproof;;
open Showproof_ct;;
open Tacexpr;;
open Vernacexpr;;
+open Printer;;
let pcoq_started = ref None;;
@@ -51,6 +64,11 @@ let if_pcoq f a =
let text_proof_flag = ref "en";;
+let pcoq_history = ref true;;
+
+let assert_pcoq_history f a =
+ if !pcoq_history then f a else error "Pcoq-style history tracking deactivated";;
+
let current_proof_name () =
try
string_of_id (get_current_proof_name ())
@@ -85,6 +103,29 @@ let kill_proof_node index =
History.border_length (current_proof_name());;
+type vtp_tree =
+ | P_rl of ct_RULE_LIST
+ | P_r of ct_RULE
+ | P_s_int of ct_SIGNED_INT_LIST
+ | P_pl of ct_PREMISES_LIST
+ | P_cl of ct_COMMAND_LIST
+ | P_t of ct_TACTIC_COM
+ | P_text of ct_TEXT
+ | P_ids of ct_ID_LIST;;
+
+let print_tree t =
+ (match t with
+ | P_rl x -> fRULE_LIST x
+ | P_r x -> fRULE x
+ | P_s_int x -> fSIGNED_INT_LIST x
+ | P_pl x -> fPREMISES_LIST x
+ | P_cl x -> fCOMMAND_LIST x
+ | P_t x -> fTACTIC_COM x
+ | P_text x -> fTEXT x
+ | P_ids x -> fID_LIST x)
+ ++ (str "e\nblabla\n");;
+
+
(*Message functions, the text of these messages is recognized by the protocols *)
(*of CtCoq *)
let ctf_header message_name request_id =
@@ -97,14 +138,20 @@ let ctf_acknowledge_command request_id command_count opt_exn =
let g_count =
List.length
(fst (frontier (proof_of_pftreestate (get_pftreestate ())))) in
- g_count, (min g_count !current_goal_index)
+ g_count, !current_goal_index
else
- (0, 0) in
+ (0, 0)
+ and statnum = Lib.current_command_label ()
+ and dpth = let d = Pfedit.current_proof_depth() in if d >= 0 then d else 0
+ and pending = CT_id_list (List.map xlate_ident (Pfedit.get_all_proof_names())) in
(ctf_header "acknowledge" request_id ++
int command_count ++ fnl() ++
int goal_count ++ fnl () ++
int goal_index ++ fnl () ++
str (current_proof_name()) ++ fnl() ++
+ int statnum ++ fnl() ++
+ print_tree (P_ids pending) ++
+ int dpth ++ fnl() ++
(match opt_exn with
Some e -> Cerrors.explain_exn e
| None -> mt ()) ++ fnl() ++ str "E-n-d---M-e-s-s-a-g-e" ++ fnl ());;
@@ -126,6 +173,8 @@ let ctf_PathGoalMessage () =
let ctf_GoalReqIdMessage = ctf_header "single_goal_state";;
+let ctf_GoalsReqIdMessage = ctf_header "goals_state";;
+
let ctf_NewStateMessage = ctf_header "fresh_state";;
let ctf_SavedMessage () = fnl () ++ str "message" ++ fnl () ++
@@ -153,39 +202,16 @@ let ctf_ResetIdentMessage request_id s =
ctf_header "reset_ident" request_id ++ str s ++ fnl () ++
str "E-n-d---M-e-s-s-a-g-e" ++ fnl();;
-type vtp_tree =
- | P_rl of ct_RULE_LIST
- | P_r of ct_RULE
- | P_s_int of ct_SIGNED_INT_LIST
- | P_pl of ct_PREMISES_LIST
- | P_cl of ct_COMMAND_LIST
- | P_t of ct_TACTIC_COM
- | P_text of ct_TEXT
- | P_ids of ct_ID_LIST;;
-
-let print_tree t =
- (match t with
- | P_rl x -> fRULE_LIST x
- | P_r x -> fRULE x
- | P_s_int x -> fSIGNED_INT_LIST x
- | P_pl x -> fPREMISES_LIST x
- | P_cl x -> fCOMMAND_LIST x
- | P_t x -> fTACTIC_COM x
- | P_text x -> fTEXT x
- | P_ids x -> fID_LIST x);
- print_string "e\nblabla\n";;
-
-
let break_happened = ref false;;
let output_results stream vtp_tree =
let _ = Sys.signal Sys.sigint
(Sys.Signal_handle(fun i -> (break_happened := true;()))) in
- msg stream;
- match vtp_tree with
- Some t -> print_tree t
- | None -> ();;
+ msg (stream ++
+ (match vtp_tree with
+ Some t -> print_tree t
+ | None -> mt()));;
let output_results_nl stream =
let _ = Sys.signal Sys.sigint
@@ -221,20 +247,18 @@ let print_past_goal index =
let show_nth n =
try
- let pf = proof_of_pftreestate (get_pftreestate()) in
- if (!text_proof_flag<>"off") then
- (if n=0
- then output_results (ctf_TextMessage !global_request_id)
- (Some (P_text (show_proof !text_proof_flag [])))
- else
- let path = History.get_nth_open_path (current_proof_name()) n in
- output_results (ctf_TextMessage !global_request_id)
- (Some (P_text (show_proof !text_proof_flag path))))
- else
- output_results (ctf_GoalReqIdMessage !global_request_id)
- (let goal = List.nth (fst (frontier pf))
- (n - 1) in
- (Some (P_r (translate_goal goal))))
+ output_results (ctf_GoalReqIdMessage !global_request_id
+ ++ pr_nth_open_subgoal n)
+ None
+ with
+ | Invalid_argument s ->
+ error "No focused proof (No proof-editing in progress)";;
+
+let show_subgoals () =
+ try
+ output_results (ctf_GoalReqIdMessage !global_request_id
+ ++ pr_open_subgoals ())
+ None
with
| Invalid_argument s ->
error "No focused proof (No proof-editing in progress)";;
@@ -275,39 +299,24 @@ let ctf_EmptyGoalMessage id =
fnl () ++ str "Empty Goal is a no-op. Fun oh fun." ++ fnl ();;
-let print_check judg =
- let {uj_val=value; uj_type=typ} = judg in
- let value_ct_ast =
- (try translate_constr false (Global.env()) value
- with UserError(f,str) ->
- raise(UserError(f,Printer.pr_lconstr value ++
- fnl () ++ str ))) in
- let type_ct_ast =
- (try translate_constr false (Global.env()) typ
- with UserError(f,str) ->
- raise(UserError(f, Printer.pr_lconstr value ++ fnl() ++ str))) in
- ((ctf_SearchResults !global_request_id),
- (Some (P_pl
- (CT_premises_list
- [CT_coerce_TYPED_FORMULA_to_PREMISE
- (CT_typed_formula(value_ct_ast,type_ct_ast)
- )]))));;
-
-let ct_print_eval ast red_fun env judg =
-((if refining() then traverse_to []);
-let {uj_val=value; uj_type=typ} = judg in
-let nvalue = red_fun value
-(* // Attention , ici il faut peut être utiliser des environnemenst locaux *)
-and ntyp = nf_betaiota typ in
-(ctf_SearchResults !global_request_id,
- Some (P_pl
- (CT_premises_list
- [CT_eval_result
- (xlate_formula ast,
- translate_constr false env nvalue,
- translate_constr false env ntyp)]))));;
-
-
+let print_check env judg =
+ ((ctf_SearchResults !global_request_id) ++
+ print_judgment env judg,
+ None);;
+
+let ct_print_eval red_fun env evmap ast judg =
+ (if refining() then traverse_to []);
+ let {uj_val=value; uj_type=typ} = judg in
+ let nvalue = (red_fun env evmap) value
+ (* // Attention , ici il faut peut être utiliser des environnemenst locaux *)
+ and ntyp = nf_betaiota typ in
+ print_tree
+ (P_pl
+ (CT_premises_list
+ [CT_eval_result
+ (xlate_formula ast,
+ translate_constr false env nvalue,
+ translate_constr false env ntyp)]));;
let pbp_tac_pcoq =
pbp_tac (function (x:raw_tactic_expr) ->
@@ -330,6 +339,7 @@ let dad_tac_pcoq =
</cpa> *)
let search_output_results () =
+ (* LEM: See comments for pcoq_search *)
output_results
(ctf_SearchResults !global_request_id)
(Some (P_pl (CT_premises_list
@@ -491,19 +501,19 @@ VERNAC COMMAND EXTEND OutputGoal
END
VERNAC COMMAND EXTEND OutputGoal
- [ "Goal" "Cmd" natural(n) "with" tactic(tac) ] -> [ simulate_solve n tac ]
+ [ "Goal" "Cmd" natural(n) "with" tactic(tac) ] -> [ assert_pcoq_history (simulate_solve n) tac ]
END
VERNAC COMMAND EXTEND KillProofAfter
-| [ "Kill" "Proof" "after" natural(n) ] -> [ kill_node_verbose n ]
+| [ "Kill" "Proof" "after" natural(n) ] -> [ assert_pcoq_history kill_node_verbose n ]
END
VERNAC COMMAND EXTEND KillProofAt
-| [ "Kill" "Proof" "at" natural(n) ] -> [ kill_node_verbose n ]
+| [ "Kill" "Proof" "at" natural(n) ] -> [ assert_pcoq_history kill_node_verbose n ]
END
VERNAC COMMAND EXTEND KillSubProof
- [ "Kill" "SubProof" natural(n) ] -> [ logical_kill n ]
+ [ "Kill" "SubProof" natural(n) ] -> [ assert_pcoq_history logical_kill n ]
END
VERNAC COMMAND EXTEND PcoqReset
@@ -515,18 +525,17 @@ VERNAC COMMAND EXTEND PcoqResetInitial
END
let start_proof_hook () =
- History.start_proof (current_proof_name());
+ if !pcoq_history then History.start_proof (current_proof_name());
current_goal_index := 1
let solve_hook n =
- let name = current_proof_name () in
- let old_n_count = History.border_length name in
- let pf = proof_of_pftreestate (get_pftreestate ()) in
- let n_goals = (List.length (fst (frontier pf))) + 1 - old_n_count in
- begin
- current_goal_index := n;
- History.push_command name n n_goals
- end
+ current_goal_index := n;
+ if !pcoq_history then
+ let name = current_proof_name () in
+ let old_n_count = History.border_length name in
+ let pf = proof_of_pftreestate (get_pftreestate ()) in
+ let n_goals = (List.length (fst (frontier pf))) + 1 - old_n_count in
+ History.push_command name n n_goals
let abort_hook s = output_results_nl (ctf_AbortedMessage !global_request_id s)
@@ -535,6 +544,12 @@ let interp_search_about_item = function
| SearchString s -> GlobSearchString s
let pcoq_search s l =
+ (* LEM: I don't understand why this is done in this way (redoing the
+ * match on s here) instead of making the code in
+ * parsing/search.ml call the right function instead of
+ * "plain_display". Investigates this later.
+ * TODO
+ *)
ctv_SEARCH_LIST:=[];
begin match s with
| SearchAbout sl ->
@@ -581,27 +596,25 @@ let hyp_search_pattern c l =
(Some
(P_pl (CT_premises_list (List.rev !ctv_SEARCH_LIST))));;
let pcoq_print_name ref =
- let results = xlate_vernac_list (name_to_ast ref) in
output_results
- (fnl () ++ str "message" ++ fnl () ++ str "PRINT_VALUE" ++ fnl ())
- (Some (P_cl results))
+ (fnl () ++ str "message" ++ fnl () ++ str "PRINT_VALUE" ++ fnl () ++ print_name ref )
+ None
-let pcoq_print_check j =
- let a,b = print_check j in output_results a b
+let pcoq_print_check env j =
+ let a,b = print_check env j in output_results a b
-let pcoq_print_eval redfun env c j =
- let strm, vtp = ct_print_eval c redfun env j in
- output_results strm vtp;;
+let pcoq_print_eval redfun env evmap c j =
+ output_results
+ (ctf_SearchResults !global_request_id
+ ++ Prettyp.print_eval redfun env evmap c j)
+ None;;
open Vernacentries
let pcoq_show_goal = function
| Some n -> show_nth n
- | None ->
- if !pcoq_started = Some true (* = debug *) then
- msg (Printer.pr_open_subgoals ())
- else errorlabstrm "show_goal"
- (str "Show must be followed by an integer in Centaur mode");;
+ | None -> show_subgoals ()
+;;
let pcoq_hook = {
start_proof = start_proof_hook;
@@ -614,6 +627,127 @@ let pcoq_hook = {
show_goal = pcoq_show_goal
}
+let pcoq_term_pr = {
+ pr_constr_expr = (fun c -> str "pcoq_constr_expr\n" ++ (default_term_pr.pr_constr_expr c));
+ (* In future translate_constr false (Global.env())
+ * Except with right bool/env which I'll get :)
+ *)
+ pr_lconstr_expr = (fun c -> fFORMULA (xlate_formula c) ++ str "(pcoq_lconstr_expr of " ++ (default_term_pr.pr_lconstr_expr c) ++ str ")");
+ pr_pattern_expr = (fun c -> str "pcoq_pattern_expr\n" ++ (default_term_pr.pr_pattern_expr c));
+ pr_lpattern_expr = (fun c -> str "pcoq_constr_expr\n" ++ (default_term_pr.pr_lpattern_expr c))
+}
+
+let start_pcoq_trees () =
+ set_term_pr pcoq_term_pr
+
+(* BEGIN functions for object_pr *)
+
+(* These functions in general mirror what name_to_ast does in a subcase,
+ and then print the corresponding object as a PCoq tree. *)
+
+let object_to_ast_template object_to_ast_list sp =
+ let l = object_to_ast_list sp in
+ VernacList (List.map (fun x -> (dummy_loc, x)) l)
+
+let pcoq_print_object_template object_to_ast_list sp =
+ let results = xlate_vernac_list (object_to_ast_template object_to_ast_list sp) in
+ print_tree (P_cl results)
+
+(* This function mirror what print_check does *)
+
+let pcoq_print_typed_value_in_env env (value, typ) =
+ let value_ct_ast =
+ (try translate_constr false (Global.env()) value
+ with UserError(f,str) ->
+ raise(UserError(f,Printer.pr_lconstr value ++
+ fnl () ++ str ))) in
+ let type_ct_ast =
+ (try translate_constr false (Global.env()) typ
+ with UserError(f,str) ->
+ raise(UserError(f, Printer.pr_lconstr value ++ fnl() ++ str))) in
+ print_tree
+ (P_pl
+ (CT_premises_list
+ [CT_coerce_TYPED_FORMULA_to_PREMISE
+ (CT_typed_formula(value_ct_ast,type_ct_ast)
+ )]))
+;;
+
+(* This function mirrors what show_nth does *)
+
+let pcoq_pr_subgoal n gl =
+ try
+ print_tree
+ (if (!text_proof_flag<>"off") then
+ (* This is a horrendeous hack; it ignores the "gl" argument
+ and just takes the currently focused proof. This will bite
+ us back one day.
+ TODO: Fix this.
+ *)
+ (
+ if not !pcoq_history then error "Text mode requires Pcoq history tracking.";
+ if n=0
+ then (P_text (show_proof !text_proof_flag []))
+ else
+ let path = History.get_nth_open_path (current_proof_name()) n in
+ (P_text (show_proof !text_proof_flag path)))
+ else
+ (let goal = List.nth gl (n - 1) in
+ (P_r (translate_goal goal))))
+ with
+ | Invalid_argument _
+ | Failure "nth"
+ | Not_found -> error "No such goal";;
+
+let pcoq_pr_subgoals close_cmd evar gl =
+ (*LEM: TODO: we should check for evar emptiness or not, and do something *)
+ try
+ print_tree
+ (if (!text_proof_flag<>"off") then
+ raise (Anomaly ("centaur.ml4:pcoq_pr_subgoals", str "Text mode show all subgoals not implemented"))
+ else
+ (P_rl (translate_goals gl)))
+ with
+ | Invalid_argument _
+ | Failure "nth"
+ | Not_found -> error "No such goal";;
+
+
+(* END functions for object_pr *)
+
+let pcoq_object_pr = {
+ print_inductive = pcoq_print_object_template inductive_to_ast_list;
+ (* TODO: Check what that with_infos means, and adapt accordingly *)
+ print_constant_with_infos = pcoq_print_object_template constant_to_ast_list;
+ print_section_variable = pcoq_print_object_template variable_to_ast_list;
+ print_syntactic_def = pcoq_print_object_template (fun x -> errorlabstrm "print"
+ (str "printing of syntax definitions not implemented in PCoq syntax"));
+ (* TODO: These are placeholders only; write them *)
+ print_module = (fun x y -> str "pcoq_print_module not implemented");
+ print_modtype = (fun x -> str "pcoq_print_modtype not implemented");
+ print_named_decl = (fun x -> str "pcoq_print_named_decl not implemented");
+ (* TODO: Find out what the first argument x (a bool) is about and react accordingly *)
+ print_leaf_entry = (fun x -> pcoq_print_object_template leaf_entry_to_ast_list);
+ print_library_entry = (fun x y -> Some (str "pcoq_print_library_entry not implemented"));
+ print_context = (fun x y z -> str "pcoq_print_context not implemented");
+ print_typed_value_in_env = pcoq_print_typed_value_in_env;
+ Prettyp.print_eval = ct_print_eval;
+};;
+
+let pcoq_printer_pr = {
+ pr_subgoals = pcoq_pr_subgoals;
+ pr_subgoal = pcoq_pr_subgoal;
+ pr_goal = (fun x -> str "pcoq_pr_goal not implemented");
+};;
+
+
+let start_pcoq_objects () =
+ set_object_pr pcoq_object_pr;
+ set_printer_pr pcoq_printer_pr
+
+let start_default_objects () =
+ set_object_pr default_object_pr;
+ set_printer_pr default_printer_pr
TACTIC EXTEND pbp
| [ "pbp" ident_opt(idopt) natural_list(nl) ] ->
@@ -635,7 +769,6 @@ let start_pcoq_mode debug =
(* <\cpa>
start_dad();
</cpa> *)
- declare_in_coq();
(* The following ones are added to enable rich comments in pcoq *)
(* TODO ...
add_tactic "Image" (fun _ -> tclIDTAC);
@@ -649,6 +782,8 @@ let start_pcoq_mode debug =
List.iter (fun (a,b) -> overwriting_vinterp_add a b) non_debug_changes;
*)
set_pcoq_hook pcoq_hook;
+ start_pcoq_objects();
+ Options.print_emacs := false; Pp.make_pp_nonemacs();
end;;
@@ -681,3 +816,19 @@ END
VERNAC COMMAND EXTEND StartPcoqDebug
| [ "Start" "Pcoq" "Debug" "Mode" ] -> [ start_pcoq_debug () ]
END
+
+VERNAC COMMAND EXTEND StartPcoqTerms
+| [ "Start" "Pcoq" "Trees" ] -> [ start_pcoq_trees () ]
+END
+
+VERNAC COMMAND EXTEND StartPcoqObjects
+| [ "Start" "Pcoq" "Objects" ] -> [ start_pcoq_objects () ]
+END
+
+VERNAC COMMAND EXTEND StartDefaultObjects
+| [ "Start" "Default" "Objects" ] -> [ start_default_objects () ]
+END
+
+VERNAC COMMAND EXTEND StopPcoqHistory
+| [ "Stop" "Pcoq" "History" ] -> [ pcoq_history := false ]
+END
diff --git a/contrib/interface/name_to_ast.mli b/contrib/interface/name_to_ast.mli
index b8c2d7dc7..f9e83b5e1 100644
--- a/contrib/interface/name_to_ast.mli
+++ b/contrib/interface/name_to_ast.mli
@@ -1 +1,5 @@
val name_to_ast : Libnames.reference -> Vernacexpr.vernac_expr;;
+val inductive_to_ast_list : Names.mutual_inductive -> Vernacexpr.vernac_expr list;;
+val constant_to_ast_list : Names.constant -> Vernacexpr.vernac_expr list;;
+val variable_to_ast_list : Names.variable -> Vernacexpr.vernac_expr list;;
+val leaf_entry_to_ast_list : (Libnames.section_path * Names.mutual_inductive) * Libobject.obj -> Vernacexpr.vernac_expr list;;
diff --git a/contrib/interface/parse.ml b/contrib/interface/parse.ml
index 0278a16cd..b551b143c 100644
--- a/contrib/interface/parse.ml
+++ b/contrib/interface/parse.ml
@@ -21,18 +21,19 @@ type parsed_tree =
| P_i of ct_INT;;
let print_parse_results n msg =
- print_string "message\nparsed\n";
- print_int n;
- print_string "\n";
- (match msg with
- | P_cl x -> fCOMMAND_LIST x
- | P_c x -> fCOMMAND x
- | P_t x -> fTACTIC_COM x
- | P_f x -> fFORMULA x
- | P_id x -> fID x
- | P_s x -> fSTRING x
- | P_i x -> fINT x);
- print_string "e\nblabla\n";
+ Pp.msg
+ ( str "message\nparsed\n" ++
+ int n ++
+ str "\n" ++
+ (match msg with
+ | P_cl x -> fCOMMAND_LIST x
+ | P_c x -> fCOMMAND x
+ | P_t x -> fTACTIC_COM x
+ | P_f x -> fFORMULA x
+ | P_id x -> fID x
+ | P_s x -> fSTRING x
+ | P_i x -> fINT x) ++
+ str "e\nblabla\n");
flush stdout;;
let ctf_SyntaxErrorMessage reqid pps =
diff --git a/contrib/interface/translate.ml b/contrib/interface/translate.ml
index 6e4782be0..559860b2f 100644
--- a/contrib/interface/translate.ml
+++ b/contrib/interface/translate.ml
@@ -75,3 +75,6 @@ let translate_path l =
(*translates a path and a goal into a centaur-tree --> RULE *)
let translate_goal (g:goal) =
CT_rule(translate_sign (evar_env g), translate_constr true (evar_env g) g.evar_concl);;
+
+let translate_goals (gl: goal list) =
+ CT_rule_list (List.map translate_goal gl);;
diff --git a/contrib/interface/translate.mli b/contrib/interface/translate.mli
index 65d8331b2..34841fc4b 100644
--- a/contrib/interface/translate.mli
+++ b/contrib/interface/translate.mli
@@ -5,6 +5,7 @@ open Environ;;
open Term;;
val translate_goal : goal -> ct_RULE;;
+val translate_goals : goal list -> ct_RULE_LIST;;
(* The boolean argument indicates whether names from the environment should *)
(* be avoided (same interpretation as for prterm_env and ast_of_constr) *)
val translate_constr : bool -> env -> constr -> ct_FORMULA;;
diff --git a/contrib/interface/vtp.ml b/contrib/interface/vtp.ml
index 166a0cbf6..f55eee07d 100644
--- a/contrib/interface/vtp.ml
+++ b/contrib/interface/vtp.ml
@@ -1,103 +1,108 @@
open Ascent;;
+open Pp;;
+
+(* LEM: This is actually generated automatically *)
let fNODE s n =
- print_string "n\n";
- print_string ("vernac$" ^ s);
- print_string "\n";
- print_int n;
- print_string "\n";;
+ (str "n\n") ++
+ (str ("vernac$" ^ s)) ++
+ (str "\n") ++
+ (int n) ++
+ (str "\n");;
let fATOM s1 =
- print_string "a\n";
- print_string ("vernac$" ^ s1);
- print_string "\n";;
+ (str "a\n") ++
+ (str ("vernac$" ^ s1)) ++
+ (str "\n");;
-let f_atom_string = print_string;;
-let f_atom_int = print_int;;
+let f_atom_string = str;;
+let f_atom_int = int;;
let rec fAST = function
| CT_coerce_ID_OR_INT_to_AST x -> fID_OR_INT x
| CT_coerce_ID_OR_STRING_to_AST x -> fID_OR_STRING x
| CT_coerce_SINGLE_OPTION_VALUE_to_AST x -> fSINGLE_OPTION_VALUE x
| CT_astnode(x1, x2) ->
- fID x1;
- fAST_LIST x2;
+ fID x1 ++
+ fAST_LIST x2 ++
fNODE "astnode" 2
| CT_astpath(x1) ->
- fID_LIST x1;
+ fID_LIST x1 ++
fNODE "astpath" 1
| CT_astslam(x1, x2) ->
- fID_OPT x1;
- fAST x2;
+ fID_OPT x1 ++
+ fAST x2 ++
fNODE "astslam" 2
and fAST_LIST = function
| CT_ast_list l ->
- (List.iter fAST l);
+ (List.fold_left (++) (mt()) (List.map fAST l)) ++
fNODE "ast_list" (List.length l)
and fBINARY = function
-| CT_binary x -> fATOM "binary";
- (f_atom_int x);
- print_string "\n"and fBINDER = function
+| CT_binary x -> fATOM "binary" ++
+ (f_atom_int x) ++
+ str "\n"
+and fBINDER = function
| CT_coerce_DEF_to_BINDER x -> fDEF x
| CT_binder(x1, x2) ->
- fID_OPT_NE_LIST x1;
- fFORMULA x2;
+ fID_OPT_NE_LIST x1 ++
+ fFORMULA x2 ++
fNODE "binder" 2
| CT_binder_coercion(x1, x2) ->
- fID_OPT_NE_LIST x1;
- fFORMULA x2;
+ fID_OPT_NE_LIST x1 ++
+ fFORMULA x2 ++
fNODE "binder_coercion" 2
and fBINDER_LIST = function
| CT_binder_list l ->
- (List.iter fBINDER l);
+ (List.fold_left (++) (mt()) (List.map fBINDER l)) ++
fNODE "binder_list" (List.length l)
and fBINDER_NE_LIST = function
| CT_binder_ne_list(x,l) ->
- fBINDER x;
- (List.iter fBINDER l);
+ fBINDER x ++
+ (List.fold_left (++) (mt()) (List.map fBINDER l)) ++
fNODE "binder_ne_list" (1 + (List.length l))
and fBINDING = function
| CT_binding(x1, x2) ->
- fID_OR_INT x1;
- fFORMULA x2;
+ fID_OR_INT x1 ++
+ fFORMULA x2 ++
fNODE "binding" 2
and fBINDING_LIST = function
| CT_binding_list l ->
- (List.iter fBINDING l);
+ (List.fold_left (++) (mt()) (List.map fBINDING l)) ++
fNODE "binding_list" (List.length l)
and fBOOL = function
| CT_false -> fNODE "false" 0
| CT_true -> fNODE "true" 0
and fCASE = function
-| CT_case x -> fATOM "case";
- (f_atom_string x);
- print_string "\n"and fCLAUSE = function
+| CT_case x -> fATOM "case" ++
+ (f_atom_string x) ++
+ str "\n"
+and fCLAUSE = function
| CT_clause(x1, x2) ->
- fHYP_LOCATION_LIST_OR_STAR x1;
- fSTAR_OPT x2;
+ fHYP_LOCATION_LIST_OR_STAR x1 ++
+ fSTAR_OPT x2 ++
fNODE "clause" 2
and fCOERCION_OPT = function
| CT_coerce_NONE_to_COERCION_OPT x -> fNONE x
| CT_coercion_atm -> fNODE "coercion_atm" 0
and fCOFIXTAC = function
| CT_cofixtac(x1, x2) ->
- fID x1;
- fFORMULA x2;
+ fID x1 ++
+ fFORMULA x2 ++
fNODE "cofixtac" 2
and fCOFIX_REC = function
| CT_cofix_rec(x1, x2, x3, x4) ->
- fID x1;
- fBINDER_LIST x2;
- fFORMULA x3;
- fFORMULA x4;
+ fID x1 ++
+ fBINDER_LIST x2 ++
+ fFORMULA x3 ++
+ fFORMULA x4 ++
fNODE "cofix_rec" 4
and fCOFIX_REC_LIST = function
| CT_cofix_rec_list(x,l) ->
- fCOFIX_REC x;
- (List.iter fCOFIX_REC l);
+ fCOFIX_REC x ++
+ (List.fold_left (++) (mt()) (List.map fCOFIX_REC l)) ++
fNODE "cofix_rec_list" (1 + (List.length l))
and fCOFIX_TAC_LIST = function
| CT_cofix_tac_list l ->
- (List.iter fCOFIXTAC l);
+ (List.fold_left (++) (mt()) (List.map fCOFIXTAC l)) ++
fNODE "cofix_tac_list" (List.length l)
and fCOMMAND = function
| CT_coerce_COMMAND_LIST_to_COMMAND x -> fCOMMAND_LIST x
@@ -105,479 +110,479 @@ and fCOMMAND = function
| CT_coerce_SECTION_BEGIN_to_COMMAND x -> fSECTION_BEGIN x
| CT_coerce_THEOREM_GOAL_to_COMMAND x -> fTHEOREM_GOAL x
| CT_abort(x1) ->
- fID_OPT_OR_ALL x1;
+ fID_OPT_OR_ALL x1 ++
fNODE "abort" 1
| CT_abstraction(x1, x2, x3) ->
- fID x1;
- fFORMULA x2;
- fINT_LIST x3;
+ fID x1 ++
+ fFORMULA x2 ++
+ fINT_LIST x3 ++
fNODE "abstraction" 3
| CT_add_field(x1, x2, x3, x4) ->
- fFORMULA x1;
- fFORMULA x2;
- fFORMULA x3;
- fFORMULA_OPT x4;
+ fFORMULA x1 ++
+ fFORMULA x2 ++
+ fFORMULA x3 ++
+ fFORMULA_OPT x4 ++
fNODE "add_field" 4
| CT_add_natural_feature(x1, x2) ->
- fNATURAL_FEATURE x1;
- fID x2;
+ fNATURAL_FEATURE x1 ++
+ fID x2 ++
fNODE "add_natural_feature" 2
| CT_addpath(x1, x2) ->
- fSTRING x1;
- fID_OPT x2;
+ fSTRING x1 ++
+ fID_OPT x2 ++
fNODE "addpath" 2
| CT_arguments_scope(x1, x2) ->
- fID x1;
- fID_OPT_LIST x2;
+ fID x1 ++
+ fID_OPT_LIST x2 ++
fNODE "arguments_scope" 2
| CT_bind_scope(x1, x2) ->
- fID x1;
- fID_NE_LIST x2;
+ fID x1 ++
+ fID_NE_LIST x2 ++
fNODE "bind_scope" 2
| CT_cd(x1) ->
- fSTRING_OPT x1;
+ fSTRING_OPT x1 ++
fNODE "cd" 1
| CT_check(x1) ->
- fFORMULA x1;
+ fFORMULA x1 ++
fNODE "check" 1
| CT_class(x1) ->
- fID x1;
+ fID x1 ++
fNODE "class" 1
| CT_close_scope(x1) ->
- fID x1;
+ fID x1 ++
fNODE "close_scope" 1
| CT_coercion(x1, x2, x3, x4, x5) ->
- fLOCAL_OPT x1;
- fIDENTITY_OPT x2;
- fID x3;
- fID x4;
- fID x5;
+ fLOCAL_OPT x1 ++
+ fIDENTITY_OPT x2 ++
+ fID x3 ++
+ fID x4 ++
+ fID x5 ++
fNODE "coercion" 5
| CT_cofix_decl(x1) ->
- fCOFIX_REC_LIST x1;
+ fCOFIX_REC_LIST x1 ++
fNODE "cofix_decl" 1
| CT_compile_module(x1, x2, x3) ->
- fVERBOSE_OPT x1;
- fID x2;
- fSTRING_OPT x3;
+ fVERBOSE_OPT x1 ++
+ fID x2 ++
+ fSTRING_OPT x3 ++
fNODE "compile_module" 3
| CT_declare_module(x1, x2, x3, x4) ->
- fID x1;
- fMODULE_BINDER_LIST x2;
- fMODULE_TYPE_CHECK x3;
- fMODULE_EXPR x4;
+ fID x1 ++
+ fMODULE_BINDER_LIST x2 ++
+ fMODULE_TYPE_CHECK x3 ++
+ fMODULE_EXPR x4 ++
fNODE "declare_module" 4
| CT_define_notation(x1, x2, x3, x4) ->
- fSTRING x1;
- fFORMULA x2;
- fMODIFIER_LIST x3;
- fID_OPT x4;
+ fSTRING x1 ++
+ fFORMULA x2 ++
+ fMODIFIER_LIST x3 ++
+ fID_OPT x4 ++
fNODE "define_notation" 4
| CT_definition(x1, x2, x3, x4, x5) ->
- fDEFN x1;
- fID x2;
- fBINDER_LIST x3;
- fDEF_BODY x4;
- fFORMULA_OPT x5;
+ fDEFN x1 ++
+ fID x2 ++
+ fBINDER_LIST x3 ++
+ fDEF_BODY x4 ++
+ fFORMULA_OPT x5 ++
fNODE "definition" 5
| CT_delim_scope(x1, x2) ->
- fID x1;
- fID x2;
+ fID x1 ++
+ fID x2 ++
fNODE "delim_scope" 2
| CT_delpath(x1) ->
- fSTRING x1;
+ fSTRING x1 ++
fNODE "delpath" 1
| CT_derive_depinversion(x1, x2, x3, x4) ->
- fINV_TYPE x1;
- fID x2;
- fFORMULA x3;
- fSORT_TYPE x4;
+ fINV_TYPE x1 ++
+ fID x2 ++
+ fFORMULA x3 ++
+ fSORT_TYPE x4 ++
fNODE "derive_depinversion" 4
| CT_derive_inversion(x1, x2, x3, x4) ->
- fINV_TYPE x1;
- fINT_OPT x2;
- fID x3;
- fID x4;
+ fINV_TYPE x1 ++
+ fINT_OPT x2 ++
+ fID x3 ++
+ fID x4 ++
fNODE "derive_inversion" 4
| CT_derive_inversion_with(x1, x2, x3, x4) ->
- fINV_TYPE x1;
- fID x2;
- fFORMULA x3;
- fSORT_TYPE x4;
+ fINV_TYPE x1 ++
+ fID x2 ++
+ fFORMULA x3 ++
+ fSORT_TYPE x4 ++
fNODE "derive_inversion_with" 4
| CT_explain_proof(x1) ->
- fINT_LIST x1;
+ fINT_LIST x1 ++
fNODE "explain_proof" 1
| CT_explain_prooftree(x1) ->
- fINT_LIST x1;
+ fINT_LIST x1 ++
fNODE "explain_prooftree" 1
| CT_export_id(x1) ->
- fID_NE_LIST x1;
+ fID_NE_LIST x1 ++
fNODE "export_id" 1
| CT_extract_to_file(x1, x2) ->
- fSTRING x1;
- fID_NE_LIST x2;
+ fSTRING x1 ++
+ fID_NE_LIST x2 ++
fNODE "extract_to_file" 2
| CT_extraction(x1) ->
- fID_OPT x1;
+ fID_OPT x1 ++
fNODE "extraction" 1
| CT_fix_decl(x1) ->
- fFIX_REC_LIST x1;
+ fFIX_REC_LIST x1 ++
fNODE "fix_decl" 1
| CT_focus(x1) ->
- fINT_OPT x1;
+ fINT_OPT x1 ++
fNODE "focus" 1
| CT_go(x1) ->
- fINT_OR_LOCN x1;
+ fINT_OR_LOCN x1 ++
fNODE "go" 1
| CT_guarded -> fNODE "guarded" 0
| CT_hint_destruct(x1, x2, x3, x4, x5, x6) ->
- fID x1;
- fINT x2;
- fDESTRUCT_LOCATION x3;
- fFORMULA x4;
- fTACTIC_COM x5;
- fID_LIST x6;
+ fID x1 ++
+ fINT x2 ++
+ fDESTRUCT_LOCATION x3 ++
+ fFORMULA x4 ++
+ fTACTIC_COM x5 ++
+ fID_LIST x6 ++
fNODE "hint_destruct" 6
| CT_hint_extern(x1, x2, x3, x4) ->
- fINT x1;
- fFORMULA x2;
- fTACTIC_COM x3;
- fID_LIST x4;
+ fINT x1 ++
+ fFORMULA x2 ++
+ fTACTIC_COM x3 ++
+ fID_LIST x4 ++
fNODE "hint_extern" 4
| CT_hintrewrite(x1, x2, x3, x4) ->
- fORIENTATION x1;
- fFORMULA_NE_LIST x2;
- fID x3;
- fTACTIC_COM x4;
+ fORIENTATION x1 ++
+ fFORMULA_NE_LIST x2 ++
+ fID x3 ++
+ fTACTIC_COM x4 ++
fNODE "hintrewrite" 4
| CT_hints(x1, x2, x3) ->
- fID x1;
- fID_NE_LIST x2;
- fID_LIST x3;
+ fID x1 ++
+ fID_NE_LIST x2 ++
+ fID_LIST x3 ++
fNODE "hints" 3
| CT_hints_immediate(x1, x2) ->
- fFORMULA_NE_LIST x1;
- fID_LIST x2;
+ fFORMULA_NE_LIST x1 ++
+ fID_LIST x2 ++
fNODE "hints_immediate" 2
| CT_hints_resolve(x1, x2) ->
- fFORMULA_NE_LIST x1;
- fID_LIST x2;
+ fFORMULA_NE_LIST x1 ++
+ fID_LIST x2 ++
fNODE "hints_resolve" 2
| CT_hyp_search_pattern(x1, x2) ->
- fFORMULA x1;
- fIN_OR_OUT_MODULES x2;
+ fFORMULA x1 ++
+ fIN_OR_OUT_MODULES x2 ++
fNODE "hyp_search_pattern" 2
| CT_implicits(x1, x2) ->
- fID x1;
- fID_LIST_OPT x2;
+ fID x1 ++
+ fID_LIST_OPT x2 ++
fNODE "implicits" 2
| CT_import_id(x1) ->
- fID_NE_LIST x1;
+ fID_NE_LIST x1 ++
fNODE "import_id" 1
| CT_ind_scheme(x1) ->
- fSCHEME_SPEC_LIST x1;
+ fSCHEME_SPEC_LIST x1 ++
fNODE "ind_scheme" 1
| CT_infix(x1, x2, x3, x4) ->
- fSTRING x1;
- fID x2;
- fMODIFIER_LIST x3;
- fID_OPT x4;
+ fSTRING x1 ++
+ fID x2 ++
+ fMODIFIER_LIST x3 ++
+ fID_OPT x4 ++
fNODE "infix" 4
| CT_inline(x1) ->
- fID_NE_LIST x1;
+ fID_NE_LIST x1 ++
fNODE "inline" 1
| CT_inspect(x1) ->
- fINT x1;
+ fINT x1 ++
fNODE "inspect" 1
| CT_kill_node(x1) ->
- fINT x1;
+ fINT x1 ++
fNODE "kill_node" 1
| CT_load(x1, x2) ->
- fVERBOSE_OPT x1;
- fID_OR_STRING x2;
+ fVERBOSE_OPT x1 ++
+ fID_OR_STRING x2 ++
fNODE "load" 2
| CT_local_close_scope(x1) ->
- fID x1;
+ fID x1 ++
fNODE "local_close_scope" 1
| CT_local_define_notation(x1, x2, x3, x4) ->
- fSTRING x1;
- fFORMULA x2;
- fMODIFIER_LIST x3;
- fID_OPT x4;
+ fSTRING x1 ++
+ fFORMULA x2 ++
+ fMODIFIER_LIST x3 ++
+ fID_OPT x4 ++
fNODE "local_define_notation" 4
| CT_local_hint_destruct(x1, x2, x3, x4, x5, x6) ->
- fID x1;
- fINT x2;
- fDESTRUCT_LOCATION x3;
- fFORMULA x4;
- fTACTIC_COM x5;
- fID_LIST x6;
+ fID x1 ++
+ fINT x2 ++
+ fDESTRUCT_LOCATION x3 ++
+ fFORMULA x4 ++
+ fTACTIC_COM x5 ++
+ fID_LIST x6 ++
fNODE "local_hint_destruct" 6
| CT_local_hint_extern(x1, x2, x3, x4) ->
- fINT x1;
- fFORMULA x2;
- fTACTIC_COM x3;
- fID_LIST x4;
+ fINT x1 ++
+ fFORMULA x2 ++
+ fTACTIC_COM x3 ++
+ fID_LIST x4 ++
fNODE "local_hint_extern" 4
| CT_local_hints(x1, x2, x3) ->
- fID x1;
- fID_NE_LIST x2;
- fID_LIST x3;
+ fID x1 ++
+ fID_NE_LIST x2 ++
+ fID_LIST x3 ++
fNODE "local_hints" 3
| CT_local_hints_immediate(x1, x2) ->
- fFORMULA_NE_LIST x1;
- fID_LIST x2;
+ fFORMULA_NE_LIST x1 ++
+ fID_LIST x2 ++
fNODE "local_hints_immediate" 2
| CT_local_hints_resolve(x1, x2) ->
- fFORMULA_NE_LIST x1;
- fID_LIST x2;
+ fFORMULA_NE_LIST x1 ++
+ fID_LIST x2 ++
fNODE "local_hints_resolve" 2
| CT_local_infix(x1, x2, x3, x4) ->
- fSTRING x1;
- fID x2;
- fMODIFIER_LIST x3;
- fID_OPT x4;
+ fSTRING x1 ++
+ fID x2 ++
+ fMODIFIER_LIST x3 ++
+ fID_OPT x4 ++
fNODE "local_infix" 4
| CT_local_open_scope(x1) ->
- fID x1;
+ fID x1 ++
fNODE "local_open_scope" 1
| CT_local_reserve_notation(x1, x2) ->
- fSTRING x1;
- fMODIFIER_LIST x2;
+ fSTRING x1 ++
+ fMODIFIER_LIST x2 ++
fNODE "local_reserve_notation" 2
| CT_locate(x1) ->
- fID x1;
+ fID x1 ++
fNODE "locate" 1
| CT_locate_file(x1) ->
- fSTRING x1;
+ fSTRING x1 ++
fNODE "locate_file" 1
| CT_locate_lib(x1) ->
- fID x1;
+ fID x1 ++
fNODE "locate_lib" 1
| CT_locate_notation(x1) ->
- fSTRING x1;
+ fSTRING x1 ++
fNODE "locate_notation" 1
| CT_mind_decl(x1, x2) ->
- fCO_IND x1;
- fIND_SPEC_LIST x2;
+ fCO_IND x1 ++
+ fIND_SPEC_LIST x2 ++
fNODE "mind_decl" 2
| CT_ml_add_path(x1) ->
- fSTRING x1;
+ fSTRING x1 ++
fNODE "ml_add_path" 1
| CT_ml_declare_modules(x1) ->
- fSTRING_NE_LIST x1;
+ fSTRING_NE_LIST x1 ++
fNODE "ml_declare_modules" 1
| CT_ml_print_modules -> fNODE "ml_print_modules" 0
| CT_ml_print_path -> fNODE "ml_print_path" 0
| CT_module(x1, x2, x3, x4) ->
- fID x1;
- fMODULE_BINDER_LIST x2;
- fMODULE_TYPE_CHECK x3;
- fMODULE_EXPR x4;
+ fID x1 ++
+ fMODULE_BINDER_LIST x2 ++
+ fMODULE_TYPE_CHECK x3 ++
+ fMODULE_EXPR x4 ++
fNODE "module" 4
| CT_module_type_decl(x1, x2, x3) ->
- fID x1;
- fMODULE_BINDER_LIST x2;
- fMODULE_TYPE_OPT x3;
+ fID x1 ++
+ fMODULE_BINDER_LIST x2 ++
+ fMODULE_TYPE_OPT x3 ++
fNODE "module_type_decl" 3
| CT_no_inline(x1) ->
- fID_NE_LIST x1;
+ fID_NE_LIST x1 ++
fNODE "no_inline" 1
| CT_omega_flag(x1, x2) ->
- fOMEGA_MODE x1;
- fOMEGA_FEATURE x2;
+ fOMEGA_MODE x1 ++
+ fOMEGA_FEATURE x2 ++
fNODE "omega_flag" 2
| CT_opaque(x1) ->
- fID_NE_LIST x1;
+ fID_NE_LIST x1 ++
fNODE "opaque" 1
| CT_open_scope(x1) ->
- fID x1;
+ fID x1 ++
fNODE "open_scope" 1
| CT_print -> fNODE "print" 0
| CT_print_about(x1) ->
- fID x1;
+ fID x1 ++
fNODE "print_about" 1
| CT_print_all -> fNODE "print_all" 0
| CT_print_classes -> fNODE "print_classes" 0
| CT_print_ltac id ->
- fID id;
+ fID id ++
fNODE "print_ltac" 1
| CT_print_coercions -> fNODE "print_coercions" 0
| CT_print_grammar(x1) ->
- fGRAMMAR x1;
+ fGRAMMAR x1 ++
fNODE "print_grammar" 1
| CT_print_graph -> fNODE "print_graph" 0
| CT_print_hint(x1) ->
- fID_OPT x1;
+ fID_OPT x1 ++
fNODE "print_hint" 1
| CT_print_hintdb(x1) ->
- fID_OR_STAR x1;
+ fID_OR_STAR x1 ++
fNODE "print_hintdb" 1
| CT_print_rewrite_hintdb(x1) ->
- fID x1;
+ fID x1 ++
fNODE "print_rewrite_hintdb" 1
| CT_print_id(x1) ->
- fID x1;
+ fID x1 ++
fNODE "print_id" 1
| CT_print_implicit(x1) ->
- fID x1;
+ fID x1 ++
fNODE "print_implicit" 1
| CT_print_loadpath -> fNODE "print_loadpath" 0
| CT_print_module(x1) ->
- fID x1;
+ fID x1 ++
fNODE "print_module" 1
| CT_print_module_type(x1) ->
- fID x1;
+ fID x1 ++
fNODE "print_module_type" 1
| CT_print_modules -> fNODE "print_modules" 0
| CT_print_natural(x1) ->
- fID x1;
+ fID x1 ++
fNODE "print_natural" 1
| CT_print_natural_feature(x1) ->
- fNATURAL_FEATURE x1;
+ fNATURAL_FEATURE x1 ++
fNODE "print_natural_feature" 1
| CT_print_opaqueid(x1) ->
- fID x1;
+ fID x1 ++
fNODE "print_opaqueid" 1
| CT_print_path(x1, x2) ->
- fID x1;
- fID x2;
+ fID x1 ++
+ fID x2 ++
fNODE "print_path" 2
| CT_print_proof(x1) ->
- fID x1;
+ fID x1 ++
fNODE "print_proof" 1
| CT_print_scope(x1) ->
- fID x1;
+ fID x1 ++
fNODE "print_scope" 1
| CT_print_setoids -> fNODE "print_setoids" 0
| CT_print_scopes -> fNODE "print_scopes" 0
| CT_print_section(x1) ->
- fID x1;
+ fID x1 ++
fNODE "print_section" 1
| CT_print_states -> fNODE "print_states" 0
| CT_print_tables -> fNODE "print_tables" 0
| CT_print_universes(x1) ->
- fSTRING_OPT x1;
+ fSTRING_OPT x1 ++
fNODE "print_universes" 1
| CT_print_visibility(x1) ->
- fID_OPT x1;
+ fID_OPT x1 ++
fNODE "print_visibility" 1
| CT_proof(x1) ->
- fFORMULA x1;
+ fFORMULA x1 ++
fNODE "proof" 1
| CT_proof_no_op -> fNODE "proof_no_op" 0
| CT_proof_with(x1) ->
- fTACTIC_COM x1;
+ fTACTIC_COM x1 ++
fNODE "proof_with" 1
| CT_pwd -> fNODE "pwd" 0
| CT_quit -> fNODE "quit" 0
| CT_read_module(x1) ->
- fID x1;
+ fID x1 ++
fNODE "read_module" 1
| CT_rec_ml_add_path(x1) ->
- fSTRING x1;
+ fSTRING x1 ++
fNODE "rec_ml_add_path" 1
| CT_recaddpath(x1, x2) ->
- fSTRING x1;
- fID_OPT x2;
+ fSTRING x1 ++
+ fID_OPT x2 ++
fNODE "recaddpath" 2
| CT_record(x1, x2, x3, x4, x5, x6) ->
- fCOERCION_OPT x1;
- fID x2;
- fBINDER_LIST x3;
- fFORMULA x4;
- fID_OPT x5;
- fRECCONSTR_LIST x6;
+ fCOERCION_OPT x1 ++
+ fID x2 ++
+ fBINDER_LIST x3 ++
+ fFORMULA x4 ++
+ fID_OPT x5 ++
+ fRECCONSTR_LIST x6 ++
fNODE "record" 6
| CT_remove_natural_feature(x1, x2) ->
- fNATURAL_FEATURE x1;
- fID x2;
+ fNATURAL_FEATURE x1 ++
+ fID x2 ++
fNODE "remove_natural_feature" 2
| CT_require(x1, x2, x3) ->
- fIMPEXP x1;
- fSPEC_OPT x2;
- fID_NE_LIST_OR_STRING x3;
+ fIMPEXP x1 ++
+ fSPEC_OPT x2 ++
+ fID_NE_LIST_OR_STRING x3 ++
fNODE "require" 3
| CT_reserve(x1, x2) ->
- fID_NE_LIST x1;
- fFORMULA x2;
+ fID_NE_LIST x1 ++
+ fFORMULA x2 ++
fNODE "reserve" 2
| CT_reserve_notation(x1, x2) ->
- fSTRING x1;
- fMODIFIER_LIST x2;
+ fSTRING x1 ++
+ fMODIFIER_LIST x2 ++
fNODE "reserve_notation" 2
| CT_reset(x1) ->
- fID x1;
+ fID x1 ++
fNODE "reset" 1
| CT_reset_section(x1) ->
- fID x1;
+ fID x1 ++
fNODE "reset_section" 1
| CT_restart -> fNODE "restart" 0
| CT_restore_state(x1) ->
- fID x1;
+ fID x1 ++
fNODE "restore_state" 1
| CT_resume(x1) ->
- fID_OPT x1;
+ fID_OPT x1 ++
fNODE "resume" 1
| CT_save(x1, x2) ->
- fTHM_OPT x1;
- fID_OPT x2;
+ fTHM_OPT x1 ++
+ fID_OPT x2 ++
fNODE "save" 2
| CT_scomments(x1) ->
- fSCOMMENT_CONTENT_LIST x1;
+ fSCOMMENT_CONTENT_LIST x1 ++
fNODE "scomments" 1
| CT_search(x1, x2) ->
- fID x1;
- fIN_OR_OUT_MODULES x2;
+ fID x1 ++
+ fIN_OR_OUT_MODULES x2 ++
fNODE "search" 2
| CT_search_about(x1, x2) ->
- fID_OR_STRING_NE_LIST x1;
- fIN_OR_OUT_MODULES x2;
+ fID_OR_STRING_NE_LIST x1 ++
+ fIN_OR_OUT_MODULES x2 ++
fNODE "search_about" 2
| CT_search_pattern(x1, x2) ->
- fFORMULA x1;
- fIN_OR_OUT_MODULES x2;
+ fFORMULA x1 ++
+ fIN_OR_OUT_MODULES x2 ++
fNODE "search_pattern" 2
| CT_search_rewrite(x1, x2) ->
- fFORMULA x1;
- fIN_OR_OUT_MODULES x2;
+ fFORMULA x1 ++
+ fIN_OR_OUT_MODULES x2 ++
fNODE "search_rewrite" 2
| CT_section_end(x1) ->
- fID x1;
+ fID x1 ++
fNODE "section_end" 1
| CT_section_struct(x1, x2, x3) ->
- fSECTION_BEGIN x1;
- fSECTION_BODY x2;
- fCOMMAND x3;
+ fSECTION_BEGIN x1 ++
+ fSECTION_BODY x2 ++
+ fCOMMAND x3 ++
fNODE "section_struct" 3
| CT_set_natural(x1) ->
- fID x1;
+ fID x1 ++
fNODE "set_natural" 1
| CT_set_natural_default -> fNODE "set_natural_default" 0
| CT_set_option(x1) ->
- fTABLE x1;
+ fTABLE x1 ++
fNODE "set_option" 1
| CT_set_option_value(x1, x2) ->
- fTABLE x1;
- fSINGLE_OPTION_VALUE x2;
+ fTABLE x1 ++
+ fSINGLE_OPTION_VALUE x2 ++
fNODE "set_option_value" 2
| CT_set_option_value2(x1, x2) ->
- fTABLE x1;
- fID_OR_STRING_NE_LIST x2;
+ fTABLE x1 ++
+ fID_OR_STRING_NE_LIST x2 ++
fNODE "set_option_value2" 2
| CT_sethyp(x1) ->
- fINT x1;
+ fINT x1 ++
fNODE "sethyp" 1
| CT_setundo(x1) ->
- fINT x1;
+ fINT x1 ++
fNODE "setundo" 1
| CT_show_existentials -> fNODE "show_existentials" 0
| CT_show_goal(x1) ->
- fINT_OPT x1;
+ fINT_OPT x1 ++
fNODE "show_goal" 1
| CT_show_implicit(x1) ->
- fINT x1;
+ fINT x1 ++
fNODE "show_implicit" 1
| CT_show_intro -> fNODE "show_intro" 0
| CT_show_intros -> fNODE "show_intros" 0
@@ -587,97 +592,98 @@ and fCOMMAND = function
| CT_show_script -> fNODE "show_script" 0
| CT_show_tree -> fNODE "show_tree" 0
| CT_solve(x1, x2, x3) ->
- fINT x1;
- fTACTIC_COM x2;
- fDOTDOT_OPT x3;
+ fINT x1 ++
+ fTACTIC_COM x2 ++
+ fDOTDOT_OPT x3 ++
fNODE "solve" 3
| CT_suspend -> fNODE "suspend" 0
| CT_syntax_macro(x1, x2, x3) ->
- fID x1;
- fFORMULA x2;
- fINT_OPT x3;
+ fID x1 ++
+ fFORMULA x2 ++
+ fINT_OPT x3 ++
fNODE "syntax_macro" 3
| CT_tactic_definition(x1) ->
- fTAC_DEF_NE_LIST x1;
+ fTAC_DEF_NE_LIST x1 ++
fNODE "tactic_definition" 1
| CT_test_natural_feature(x1, x2) ->
- fNATURAL_FEATURE x1;
- fID x2;
+ fNATURAL_FEATURE x1 ++
+ fID x2 ++
fNODE "test_natural_feature" 2
| CT_theorem_struct(x1, x2) ->
- fTHEOREM_GOAL x1;
- fPROOF_SCRIPT x2;
+ fTHEOREM_GOAL x1 ++
+ fPROOF_SCRIPT x2 ++
fNODE "theorem_struct" 2
| CT_time(x1) ->
- fCOMMAND x1;
+ fCOMMAND x1 ++
fNODE "time" 1
| CT_transparent(x1) ->
- fID_NE_LIST x1;
+ fID_NE_LIST x1 ++
fNODE "transparent" 1
| CT_undo(x1) ->
- fINT_OPT x1;
+ fINT_OPT x1 ++
fNODE "undo" 1
| CT_unfocus -> fNODE "unfocus" 0
| CT_unset_option(x1) ->
- fTABLE x1;
+ fTABLE x1 ++
fNODE "unset_option" 1
| CT_unsethyp -> fNODE "unsethyp" 0
| CT_unsetundo -> fNODE "unsetundo" 0
| CT_user_vernac(x1, x2) ->
- fID x1;
- fVARG_LIST x2;
+ fID x1 ++
+ fVARG_LIST x2 ++
fNODE "user_vernac" 2
| CT_variable(x1, x2) ->
- fVAR x1;
- fBINDER_NE_LIST x2;
+ fVAR x1 ++
+ fBINDER_NE_LIST x2 ++
fNODE "variable" 2
| CT_write_module(x1, x2) ->
- fID x1;
- fSTRING_OPT x2;
+ fID x1 ++
+ fSTRING_OPT x2 ++
fNODE "write_module" 2
and fCOMMAND_LIST = function
| CT_command_list(x,l) ->
- fCOMMAND x;
- (List.iter fCOMMAND l);
+ fCOMMAND x ++
+ (List.fold_left (++) (mt()) (List.map fCOMMAND l)) ++
fNODE "command_list" (1 + (List.length l))
and fCOMMENT = function
-| CT_comment x -> fATOM "comment";
- (f_atom_string x);
- print_string "\n"and fCOMMENT_S = function
+| CT_comment x -> fATOM "comment" ++
+ (f_atom_string x) ++
+ str "\n"
+and fCOMMENT_S = function
| CT_comment_s l ->
- (List.iter fCOMMENT l);
+ (List.fold_left (++) (mt()) (List.map fCOMMENT l)) ++
fNODE "comment_s" (List.length l)
and fCONSTR = function
| CT_constr(x1, x2) ->
- fID x1;
- fFORMULA x2;
+ fID x1 ++
+ fFORMULA x2 ++
fNODE "constr" 2
| CT_constr_coercion(x1, x2) ->
- fID x1;
- fFORMULA x2;
+ fID x1 ++
+ fFORMULA x2 ++
fNODE "constr_coercion" 2
and fCONSTR_LIST = function
| CT_constr_list l ->
- (List.iter fCONSTR l);
+ (List.fold_left (++) (mt()) (List.map fCONSTR l)) ++
fNODE "constr_list" (List.length l)
and fCONTEXT_HYP_LIST = function
| CT_context_hyp_list l ->
- (List.iter fPREMISE_PATTERN l);
+ (List.fold_left (++) (mt()) (List.map fPREMISE_PATTERN l)) ++
fNODE "context_hyp_list" (List.length l)
and fCONTEXT_PATTERN = function
| CT_coerce_FORMULA_to_CONTEXT_PATTERN x -> fFORMULA x
| CT_context(x1, x2) ->
- fID_OPT x1;
- fFORMULA x2;
+ fID_OPT x1 ++
+ fFORMULA x2 ++
fNODE "context" 2
and fCONTEXT_RULE = function
| CT_context_rule(x1, x2, x3) ->
- fCONTEXT_HYP_LIST x1;
- fCONTEXT_PATTERN x2;
- fTACTIC_COM x3;
+ fCONTEXT_HYP_LIST x1 ++
+ fCONTEXT_PATTERN x2 ++
+ fTACTIC_COM x3 ++
fNODE "context_rule" 3
| CT_def_context_rule(x1) ->
- fTACTIC_COM x1;
+ fTACTIC_COM x1 ++
fNODE "def_context_rule" 1
and fCONVERSION_FLAG = function
| CT_beta -> fNODE "beta" 0
@@ -687,49 +693,52 @@ and fCONVERSION_FLAG = function
| CT_zeta -> fNODE "zeta" 0
and fCONVERSION_FLAG_LIST = function
| CT_conversion_flag_list l ->
- (List.iter fCONVERSION_FLAG l);
+ (List.fold_left (++) (mt()) (List.map fCONVERSION_FLAG l)) ++
fNODE "conversion_flag_list" (List.length l)
and fCONV_SET = function
| CT_unf l ->
- (List.iter fID l);
+ (List.fold_left (++) (mt()) (List.map fID l)) ++
fNODE "unf" (List.length l)
| CT_unfbut l ->
- (List.iter fID l);
+ (List.fold_left (++) (mt()) (List.map fID l)) ++
fNODE "unfbut" (List.length l)
and fCO_IND = function
-| CT_co_ind x -> fATOM "co_ind";
- (f_atom_string x);
- print_string "\n"and fDECL_NOTATION_OPT = function
+| CT_co_ind x -> fATOM "co_ind" ++
+ (f_atom_string x) ++
+ str "\n"
+and fDECL_NOTATION_OPT = function
| CT_coerce_NONE_to_DECL_NOTATION_OPT x -> fNONE x
| CT_decl_notation(x1, x2, x3) ->
- fSTRING x1;
- fFORMULA x2;
- fID_OPT x3;
+ fSTRING x1 ++
+ fFORMULA x2 ++
+ fID_OPT x3 ++
fNODE "decl_notation" 3
and fDEF = function
| CT_def(x1, x2) ->
- fID_OPT x1;
- fFORMULA x2;
+ fID_OPT x1 ++
+ fFORMULA x2 ++
fNODE "def" 2
and fDEFN = function
-| CT_defn x -> fATOM "defn";
- (f_atom_string x);
- print_string "\n"and fDEFN_OR_THM = function
+| CT_defn x -> fATOM "defn" ++
+ (f_atom_string x) ++
+ str "\n"
+and fDEFN_OR_THM = function
| CT_coerce_DEFN_to_DEFN_OR_THM x -> fDEFN x
| CT_coerce_THM_to_DEFN_OR_THM x -> fTHM x
and fDEF_BODY = function
| CT_coerce_CONTEXT_PATTERN_to_DEF_BODY x -> fCONTEXT_PATTERN x
| CT_coerce_EVAL_CMD_to_DEF_BODY x -> fEVAL_CMD x
| CT_type_of(x1) ->
- fFORMULA x1;
+ fFORMULA x1 ++
fNODE "type_of" 1
and fDEF_BODY_OPT = function
| CT_coerce_DEF_BODY_to_DEF_BODY_OPT x -> fDEF_BODY x
| CT_coerce_FORMULA_OPT_to_DEF_BODY_OPT x -> fFORMULA_OPT x
and fDEP = function
-| CT_dep x -> fATOM "dep";
- (f_atom_string x);
- print_string "\n"and fDESTRUCTING = function
+| CT_dep x -> fATOM "dep" ++
+ (f_atom_string x) ++
+ str "\n"
+and fDESTRUCTING = function
| CT_coerce_NONE_to_DESTRUCTING x -> fNONE x
| CT_destructing -> fNODE "destructing" 0
and fDESTRUCT_LOCATION = function
@@ -741,54 +750,54 @@ and fDOTDOT_OPT = function
| CT_dotdot -> fNODE "dotdot" 0
and fEQN = function
| CT_eqn(x1, x2) ->
- fMATCH_PATTERN_NE_LIST x1;
- fFORMULA x2;
+ fMATCH_PATTERN_NE_LIST x1 ++
+ fFORMULA x2 ++
fNODE "eqn" 2
and fEQN_LIST = function
| CT_eqn_list l ->
- (List.iter fEQN l);
+ (List.fold_left (++) (mt()) (List.map fEQN l)) ++
fNODE "eqn_list" (List.length l)
and fEVAL_CMD = function
| CT_eval(x1, x2, x3) ->
- fINT_OPT x1;
- fRED_COM x2;
- fFORMULA x3;
+ fINT_OPT x1 ++
+ fRED_COM x2 ++
+ fFORMULA x3 ++
fNODE "eval" 3
and fFIXTAC = function
| CT_fixtac(x1, x2, x3) ->
- fID x1;
- fINT x2;
- fFORMULA x3;
+ fID x1 ++
+ fINT x2 ++
+ fFORMULA x3 ++
fNODE "fixtac" 3
and fFIX_BINDER = function
| CT_coerce_FIX_REC_to_FIX_BINDER x -> fFIX_REC x
| CT_fix_binder(x1, x2, x3, x4) ->
- fID x1;
- fINT x2;
- fFORMULA x3;
- fFORMULA x4;
+ fID x1 ++
+ fINT x2 ++
+ fFORMULA x3 ++
+ fFORMULA x4 ++
fNODE "fix_binder" 4
and fFIX_BINDER_LIST = function
| CT_fix_binder_list(x,l) ->
- fFIX_BINDER x;
- (List.iter fFIX_BINDER l);
+ fFIX_BINDER x ++
+ (List.fold_left (++) (mt()) (List.map fFIX_BINDER l)) ++
fNODE "fix_binder_list" (1 + (List.length l))
and fFIX_REC = function
| CT_fix_rec(x1, x2, x3, x4, x5) ->
- fID x1;
- fBINDER_NE_LIST x2;
- fID_OPT x3;
- fFORMULA x4;
- fFORMULA x5;
+ fID x1 ++
+ fBINDER_NE_LIST x2 ++
+ fID_OPT x3 ++
+ fFORMULA x4 ++
+ fFORMULA x5 ++
fNODE "fix_rec" 5
and fFIX_REC_LIST = function
| CT_fix_rec_list(x,l) ->
- fFIX_REC x;
- (List.iter fFIX_REC l);
+ fFIX_REC x ++
+ (List.fold_left (++) (mt()) (List.map fFIX_REC l)) ++
fNODE "fix_rec_list" (1 + (List.length l))
and fFIX_TAC_LIST = function
| CT_fix_tac_list l ->
- (List.iter fFIXTAC l);
+ (List.fold_left (++) (mt()) (List.map fFIXTAC l)) ++
fNODE "fix_tac_list" (List.length l)
and fFORMULA = function
| CT_coerce_BINARY_to_FORMULA x -> fBINARY x
@@ -797,90 +806,90 @@ and fFORMULA = function
| CT_coerce_SORT_TYPE_to_FORMULA x -> fSORT_TYPE x
| CT_coerce_TYPED_FORMULA_to_FORMULA x -> fTYPED_FORMULA x
| CT_appc(x1, x2) ->
- fFORMULA x1;
- fFORMULA_NE_LIST x2;
+ fFORMULA x1 ++
+ fFORMULA_NE_LIST x2 ++
fNODE "appc" 2
| CT_arrowc(x1, x2) ->
- fFORMULA x1;
- fFORMULA x2;
+ fFORMULA x1 ++
+ fFORMULA x2 ++
fNODE "arrowc" 2
| CT_bang(x1) ->
- fFORMULA x1;
+ fFORMULA x1 ++
fNODE "bang" 1
| CT_cases(x1, x2, x3) ->
- fMATCHED_FORMULA_NE_LIST x1;
- fFORMULA_OPT x2;
- fEQN_LIST x3;
+ fMATCHED_FORMULA_NE_LIST x1 ++
+ fFORMULA_OPT x2 ++
+ fEQN_LIST x3 ++
fNODE "cases" 3
| CT_cofixc(x1, x2) ->
- fID x1;
- fCOFIX_REC_LIST x2;
+ fID x1 ++
+ fCOFIX_REC_LIST x2 ++
fNODE "cofixc" 2
| CT_elimc(x1, x2, x3, x4) ->
- fCASE x1;
- fFORMULA_OPT x2;
- fFORMULA x3;
- fFORMULA_LIST x4;
+ fCASE x1 ++
+ fFORMULA_OPT x2 ++
+ fFORMULA x3 ++
+ fFORMULA_LIST x4 ++
fNODE "elimc" 4
| CT_existvarc -> fNODE "existvarc" 0
| CT_fixc(x1, x2) ->
- fID x1;
- fFIX_BINDER_LIST x2;
+ fID x1 ++
+ fFIX_BINDER_LIST x2 ++
fNODE "fixc" 2
| CT_if(x1, x2, x3, x4) ->
- fFORMULA x1;
- fRETURN_INFO x2;
- fFORMULA x3;
- fFORMULA x4;
+ fFORMULA x1 ++
+ fRETURN_INFO x2 ++
+ fFORMULA x3 ++
+ fFORMULA x4 ++
fNODE "if" 4
| CT_inductive_let(x1, x2, x3, x4) ->
- fFORMULA_OPT x1;
- fID_OPT_NE_LIST x2;
- fFORMULA x3;
- fFORMULA x4;
+ fFORMULA_OPT x1 ++
+ fID_OPT_NE_LIST x2 ++
+ fFORMULA x3 ++
+ fFORMULA x4 ++
fNODE "inductive_let" 4
| CT_labelled_arg(x1, x2) ->
- fID x1;
- fFORMULA x2;
+ fID x1 ++
+ fFORMULA x2 ++
fNODE "labelled_arg" 2
| CT_lambdac(x1, x2) ->
- fBINDER_NE_LIST x1;
- fFORMULA x2;
+ fBINDER_NE_LIST x1 ++
+ fFORMULA x2 ++
fNODE "lambdac" 2
| CT_let_tuple(x1, x2, x3, x4) ->
- fID_OPT_NE_LIST x1;
- fRETURN_INFO x2;
- fFORMULA x3;
- fFORMULA x4;
+ fID_OPT_NE_LIST x1 ++
+ fRETURN_INFO x2 ++
+ fFORMULA x3 ++
+ fFORMULA x4 ++
fNODE "let_tuple" 4
| CT_letin(x1, x2) ->
- fDEF x1;
- fFORMULA x2;
+ fDEF x1 ++
+ fFORMULA x2 ++
fNODE "letin" 2
| CT_notation(x1, x2) ->
- fSTRING x1;
- fFORMULA_LIST x2;
+ fSTRING x1 ++
+ fFORMULA_LIST x2 ++
fNODE "notation" 2
| CT_num_encapsulator(x1, x2) ->
- fNUM_TYPE x1;
- fFORMULA x2;
+ fNUM_TYPE x1 ++
+ fFORMULA x2 ++
fNODE "num_encapsulator" 2
| CT_prodc(x1, x2) ->
- fBINDER_NE_LIST x1;
- fFORMULA x2;
+ fBINDER_NE_LIST x1 ++
+ fFORMULA x2 ++
fNODE "prodc" 2
| CT_proj(x1, x2) ->
- fFORMULA x1;
- fFORMULA_NE_LIST x2;
+ fFORMULA x1 ++
+ fFORMULA_NE_LIST x2 ++
fNODE "proj" 2
and fFORMULA_LIST = function
| CT_formula_list l ->
- (List.iter fFORMULA l);
+ (List.fold_left (++) (mt()) (List.map fFORMULA l)) ++
fNODE "formula_list" (List.length l)
and fFORMULA_NE_LIST = function
| CT_formula_ne_list(x,l) ->
- fFORMULA x;
- (List.iter fFORMULA l);
+ fFORMULA x ++
+ (List.fold_left (++) (mt()) (List.map fFORMULA l)) ++
fNODE "formula_ne_list" (1 + (List.length l))
and fFORMULA_OPT = function
| CT_coerce_FORMULA_to_FORMULA_OPT x -> fFORMULA x
@@ -893,44 +902,46 @@ and fGRAMMAR = function
and fHYP_LOCATION = function
| CT_coerce_UNFOLD_to_HYP_LOCATION x -> fUNFOLD x
| CT_intype(x1, x2) ->
- fID x1;
- fINT_LIST x2;
+ fID x1 ++
+ fINT_LIST x2 ++
fNODE "intype" 2
| CT_invalue(x1, x2) ->
- fID x1;
- fINT_LIST x2;
+ fID x1 ++
+ fINT_LIST x2 ++
fNODE "invalue" 2
and fHYP_LOCATION_LIST_OR_STAR = function
| CT_coerce_STAR_to_HYP_LOCATION_LIST_OR_STAR x -> fSTAR x
| CT_hyp_location_list l ->
- (List.iter fHYP_LOCATION l);
+ (List.fold_left (++) (mt()) (List.map fHYP_LOCATION l)) ++
fNODE "hyp_location_list" (List.length l)
and fID = function
-| CT_ident x -> fATOM "ident";
- (f_atom_string x);
- print_string "\n"| CT_metac(x1) ->
- fINT x1;
+| CT_ident x -> fATOM "ident" ++
+ (f_atom_string x) ++
+ str "\n"
+| CT_metac(x1) ->
+ fINT x1 ++
fNODE "metac" 1
-| CT_metaid x -> fATOM "metaid";
- (f_atom_string x);
- print_string "\n"and fIDENTITY_OPT = function
+| CT_metaid x -> fATOM "metaid" ++
+ (f_atom_string x) ++
+ str "\n"
+and fIDENTITY_OPT = function
| CT_coerce_NONE_to_IDENTITY_OPT x -> fNONE x
| CT_identity -> fNODE "identity" 0
and fID_LIST = function
| CT_id_list l ->
- (List.iter fID l);
+ (List.fold_left (++) (mt()) (List.map fID l)) ++
fNODE "id_list" (List.length l)
and fID_LIST_LIST = function
| CT_id_list_list l ->
- (List.iter fID_LIST l);
+ (List.fold_left (++) (mt()) (List.map fID_LIST l)) ++
fNODE "id_list_list" (List.length l)
and fID_LIST_OPT = function
| CT_coerce_ID_LIST_to_ID_LIST_OPT x -> fID_LIST x
| CT_coerce_NONE_to_ID_LIST_OPT x -> fNONE x
and fID_NE_LIST = function
| CT_id_ne_list(x,l) ->
- fID x;
- (List.iter fID l);
+ fID x ++
+ (List.fold_left (++) (mt()) (List.map fID l)) ++
fNODE "id_ne_list" (1 + (List.length l))
and fID_NE_LIST_OR_STAR = function
| CT_coerce_ID_NE_LIST_to_ID_NE_LIST_OR_STAR x -> fID_NE_LIST x
@@ -943,12 +954,12 @@ and fID_OPT = function
| CT_coerce_NONE_to_ID_OPT x -> fNONE x
and fID_OPT_LIST = function
| CT_id_opt_list l ->
- (List.iter fID_OPT l);
+ (List.fold_left (++) (mt()) (List.map fID_OPT l)) ++
fNODE "id_opt_list" (List.length l)
and fID_OPT_NE_LIST = function
| CT_id_opt_ne_list(x,l) ->
- fID_OPT x;
- (List.iter fID_OPT l);
+ fID_OPT x ++
+ (List.fold_left (++) (mt()) (List.map fID_OPT l)) ++
fNODE "id_opt_ne_list" (1 + (List.length l))
and fID_OPT_OR_ALL = function
| CT_coerce_ID_OPT_to_ID_OPT_OR_ALL x -> fID_OPT x
@@ -968,8 +979,8 @@ and fID_OR_STRING = function
| CT_coerce_STRING_to_ID_OR_STRING x -> fSTRING x
and fID_OR_STRING_NE_LIST = function
| CT_id_or_string_ne_list(x,l) ->
- fID_OR_STRING x;
- (List.iter fID_OR_STRING l);
+ fID_OR_STRING x ++
+ (List.fold_left (++) (mt()) (List.map fID_OR_STRING l)) ++
fNODE "id_or_string_ne_list" (1 + (List.length l))
and fIMPEXP = function
| CT_coerce_NONE_to_IMPEXP x -> fNONE x
@@ -977,40 +988,41 @@ and fIMPEXP = function
| CT_import -> fNODE "import" 0
and fIND_SPEC = function
| CT_ind_spec(x1, x2, x3, x4, x5) ->
- fID x1;
- fBINDER_LIST x2;
- fFORMULA x3;
- fCONSTR_LIST x4;
- fDECL_NOTATION_OPT x5;
+ fID x1 ++
+ fBINDER_LIST x2 ++
+ fFORMULA x3 ++
+ fCONSTR_LIST x4 ++
+ fDECL_NOTATION_OPT x5 ++
fNODE "ind_spec" 5
and fIND_SPEC_LIST = function
| CT_ind_spec_list l ->
- (List.iter fIND_SPEC l);
+ (List.fold_left (++) (mt()) (List.map fIND_SPEC l)) ++
fNODE "ind_spec_list" (List.length l)
and fINT = function
-| CT_int x -> fATOM "int";
- (f_atom_int x);
- print_string "\n"and fINTRO_PATT = function
+| CT_int x -> fATOM "int" ++
+ (f_atom_int x) ++
+ str "\n"
+and fINTRO_PATT = function
| CT_coerce_ID_to_INTRO_PATT x -> fID x
| CT_disj_pattern(x,l) ->
- fINTRO_PATT_LIST x;
- (List.iter fINTRO_PATT_LIST l);
+ fINTRO_PATT_LIST x ++
+ (List.fold_left (++) (mt()) (List.map fINTRO_PATT_LIST l)) ++
fNODE "disj_pattern" (1 + (List.length l))
and fINTRO_PATT_LIST = function
| CT_intro_patt_list l ->
- (List.iter fINTRO_PATT l);
+ (List.fold_left (++) (mt()) (List.map fINTRO_PATT l)) ++
fNODE "intro_patt_list" (List.length l)
and fINTRO_PATT_OPT = function
| CT_coerce_ID_OPT_to_INTRO_PATT_OPT x -> fID_OPT x
| CT_coerce_INTRO_PATT_to_INTRO_PATT_OPT x -> fINTRO_PATT x
and fINT_LIST = function
| CT_int_list l ->
- (List.iter fINT l);
+ (List.fold_left (++) (mt()) (List.map fINT l)) ++
fNODE "int_list" (List.length l)
and fINT_NE_LIST = function
| CT_int_ne_list(x,l) ->
- fINT x;
- (List.iter fINT l);
+ fINT x ++
+ (List.fold_left (++) (mt()) (List.map fINT l)) ++
fNODE "int_ne_list" (1 + (List.length l))
and fINT_OPT = function
| CT_coerce_INT_to_INT_OPT x -> fINT x
@@ -1028,21 +1040,21 @@ and fINV_TYPE = function
and fIN_OR_OUT_MODULES = function
| CT_coerce_NONE_to_IN_OR_OUT_MODULES x -> fNONE x
| CT_in_modules(x1) ->
- fID_NE_LIST x1;
+ fID_NE_LIST x1 ++
fNODE "in_modules" 1
| CT_out_modules(x1) ->
- fID_NE_LIST x1;
+ fID_NE_LIST x1 ++
fNODE "out_modules" 1
and fLET_CLAUSE = function
| CT_let_clause(x1, x2, x3) ->
- fID x1;
- fTACTIC_OPT x2;
- fLET_VALUE x3;
+ fID x1 ++
+ fTACTIC_OPT x2 ++
+ fLET_VALUE x3 ++
fNODE "let_clause" 3
and fLET_CLAUSES = function
| CT_let_clauses(x,l) ->
- fLET_CLAUSE x;
- (List.iter fLET_CLAUSE l);
+ fLET_CLAUSE x ++
+ (List.fold_left (++) (mt()) (List.map fLET_CLAUSE l)) ++
fNODE "let_clauses" (1 + (List.length l))
and fLET_VALUE = function
| CT_coerce_DEF_BODY_to_LET_VALUE x -> fDEF_BODY x
@@ -1051,120 +1063,121 @@ and fLOCAL_OPT = function
| CT_coerce_NONE_to_LOCAL_OPT x -> fNONE x
| CT_local -> fNODE "local" 0
and fLOCN = function
-| CT_locn x -> fATOM "locn";
- (f_atom_string x);
- print_string "\n"and fMATCHED_FORMULA = function
+| CT_locn x -> fATOM "locn" ++
+ (f_atom_string x) ++
+ str "\n"
+and fMATCHED_FORMULA = function
| CT_coerce_FORMULA_to_MATCHED_FORMULA x -> fFORMULA x
| CT_formula_as(x1, x2) ->
- fFORMULA x1;
- fID_OPT x2;
+ fFORMULA x1 ++
+ fID_OPT x2 ++
fNODE "formula_as" 2
| CT_formula_as_in(x1, x2, x3) ->
- fFORMULA x1;
- fID_OPT x2;
- fFORMULA x3;
+ fFORMULA x1 ++
+ fID_OPT x2 ++
+ fFORMULA x3 ++
fNODE "formula_as_in" 3
| CT_formula_in(x1, x2) ->
- fFORMULA x1;
- fFORMULA x2;
+ fFORMULA x1 ++
+ fFORMULA x2 ++
fNODE "formula_in" 2
and fMATCHED_FORMULA_NE_LIST = function
| CT_matched_formula_ne_list(x,l) ->
- fMATCHED_FORMULA x;
- (List.iter fMATCHED_FORMULA l);
+ fMATCHED_FORMULA x ++
+ (List.fold_left (++) (mt()) (List.map fMATCHED_FORMULA l)) ++
fNODE "matched_formula_ne_list" (1 + (List.length l))
and fMATCH_PATTERN = function
| CT_coerce_ID_OPT_to_MATCH_PATTERN x -> fID_OPT x
| CT_coerce_NUM_to_MATCH_PATTERN x -> fNUM x
| CT_pattern_app(x1, x2) ->
- fMATCH_PATTERN x1;
- fMATCH_PATTERN_NE_LIST x2;
+ fMATCH_PATTERN x1 ++
+ fMATCH_PATTERN_NE_LIST x2 ++
fNODE "pattern_app" 2
| CT_pattern_as(x1, x2) ->
- fMATCH_PATTERN x1;
- fID_OPT x2;
+ fMATCH_PATTERN x1 ++
+ fID_OPT x2 ++
fNODE "pattern_as" 2
| CT_pattern_delimitors(x1, x2) ->
- fNUM_TYPE x1;
- fMATCH_PATTERN x2;
+ fNUM_TYPE x1 ++
+ fMATCH_PATTERN x2 ++
fNODE "pattern_delimitors" 2
| CT_pattern_notation(x1, x2) ->
- fSTRING x1;
- fMATCH_PATTERN_LIST x2;
+ fSTRING x1 ++
+ fMATCH_PATTERN_LIST x2 ++
fNODE "pattern_notation" 2
and fMATCH_PATTERN_LIST = function
| CT_match_pattern_list l ->
- (List.iter fMATCH_PATTERN l);
+ (List.fold_left (++) (mt()) (List.map fMATCH_PATTERN l)) ++
fNODE "match_pattern_list" (List.length l)
and fMATCH_PATTERN_NE_LIST = function
| CT_match_pattern_ne_list(x,l) ->
- fMATCH_PATTERN x;
- (List.iter fMATCH_PATTERN l);
+ fMATCH_PATTERN x ++
+ (List.fold_left (++) (mt()) (List.map fMATCH_PATTERN l)) ++
fNODE "match_pattern_ne_list" (1 + (List.length l))
and fMATCH_TAC_RULE = function
| CT_match_tac_rule(x1, x2) ->
- fCONTEXT_PATTERN x1;
- fLET_VALUE x2;
+ fCONTEXT_PATTERN x1 ++
+ fLET_VALUE x2 ++
fNODE "match_tac_rule" 2
and fMATCH_TAC_RULES = function
| CT_match_tac_rules(x,l) ->
- fMATCH_TAC_RULE x;
- (List.iter fMATCH_TAC_RULE l);
+ fMATCH_TAC_RULE x ++
+ (List.fold_left (++) (mt()) (List.map fMATCH_TAC_RULE l)) ++
fNODE "match_tac_rules" (1 + (List.length l))
and fMODIFIER = function
| CT_entry_type(x1, x2) ->
- fID x1;
- fID x2;
+ fID x1 ++
+ fID x2 ++
fNODE "entry_type" 2
| CT_format(x1) ->
- fSTRING x1;
+ fSTRING x1 ++
fNODE "format" 1
| CT_lefta -> fNODE "lefta" 0
| CT_nona -> fNODE "nona" 0
| CT_only_parsing -> fNODE "only_parsing" 0
| CT_righta -> fNODE "righta" 0
| CT_set_item_level(x1, x2) ->
- fID_NE_LIST x1;
- fINT_OR_NEXT x2;
+ fID_NE_LIST x1 ++
+ fINT_OR_NEXT x2 ++
fNODE "set_item_level" 2
| CT_set_level(x1) ->
- fINT x1;
+ fINT x1 ++
fNODE "set_level" 1
and fMODIFIER_LIST = function
| CT_modifier_list l ->
- (List.iter fMODIFIER l);
+ (List.fold_left (++) (mt()) (List.map fMODIFIER l)) ++
fNODE "modifier_list" (List.length l)
and fMODULE_BINDER = function
| CT_module_binder(x1, x2) ->
- fID_NE_LIST x1;
- fMODULE_TYPE x2;
+ fID_NE_LIST x1 ++
+ fMODULE_TYPE x2 ++
fNODE "module_binder" 2
and fMODULE_BINDER_LIST = function
| CT_module_binder_list l ->
- (List.iter fMODULE_BINDER l);
+ (List.fold_left (++) (mt()) (List.map fMODULE_BINDER l)) ++
fNODE "module_binder_list" (List.length l)
and fMODULE_EXPR = function
| CT_coerce_ID_OPT_to_MODULE_EXPR x -> fID_OPT x
| CT_module_app(x1, x2) ->
- fMODULE_EXPR x1;
- fMODULE_EXPR x2;
+ fMODULE_EXPR x1 ++
+ fMODULE_EXPR x2 ++
fNODE "module_app" 2
and fMODULE_TYPE = function
| CT_coerce_ID_to_MODULE_TYPE x -> fID x
| CT_module_type_with_def(x1, x2, x3) ->
- fMODULE_TYPE x1;
- fID_LIST x2;
- fFORMULA x3;
+ fMODULE_TYPE x1 ++
+ fID_LIST x2 ++
+ fFORMULA x3 ++
fNODE "module_type_with_def" 3
| CT_module_type_with_mod(x1, x2, x3) ->
- fMODULE_TYPE x1;
- fID_LIST x2;
- fID x3;
+ fMODULE_TYPE x1 ++
+ fID_LIST x2 ++
+ fID x3 ++
fNODE "module_type_with_mod" 3
and fMODULE_TYPE_CHECK = function
| CT_coerce_MODULE_TYPE_OPT_to_MODULE_TYPE_CHECK x -> fMODULE_TYPE_OPT x
| CT_only_check(x1) ->
- fMODULE_TYPE x1;
+ fMODULE_TYPE x1 ++
fNODE "only_check" 1
and fMODULE_TYPE_OPT = function
| CT_coerce_ID_OPT_to_MODULE_TYPE_OPT x -> fID_OPT x
@@ -1176,12 +1189,14 @@ and fNATURAL_FEATURE = function
and fNONE = function
| CT_none -> fNODE "none" 0
and fNUM = function
-| CT_int_encapsulator x -> fATOM "int_encapsulator";
- (f_atom_string x);
- print_string "\n"and fNUM_TYPE = function
-| CT_num_type x -> fATOM "num_type";
- (f_atom_string x);
- print_string "\n"and fOMEGA_FEATURE = function
+| CT_int_encapsulator x -> fATOM "int_encapsulator" ++
+ (f_atom_string x) ++
+ str "\n"
+and fNUM_TYPE = function
+| CT_num_type x -> fATOM "num_type" ++
+ (f_atom_string x) ++
+ str "\n"
+and fOMEGA_FEATURE = function
| CT_coerce_STRING_to_OMEGA_FEATURE x -> fSTRING x
| CT_flag_action -> fNODE "flag_action" 0
| CT_flag_system -> fNODE "flag_system" 0
@@ -1195,13 +1210,13 @@ and fORIENTATION = function
| CT_rl -> fNODE "rl" 0
and fPATTERN = function
| CT_pattern_occ(x1, x2) ->
- fINT_LIST x1;
- fFORMULA x2;
+ fINT_LIST x1 ++
+ fFORMULA x2 ++
fNODE "pattern_occ" 2
and fPATTERN_NE_LIST = function
| CT_pattern_ne_list(x,l) ->
- fPATTERN x;
- (List.iter fPATTERN l);
+ fPATTERN x ++
+ (List.fold_left (++) (mt()) (List.map fPATTERN l)) ++
fNODE "pattern_ne_list" (1 + (List.length l))
and fPATTERN_OPT = function
| CT_coerce_NONE_to_PATTERN_OPT x -> fNONE x
@@ -1209,146 +1224,147 @@ and fPATTERN_OPT = function
and fPREMISE = function
| CT_coerce_TYPED_FORMULA_to_PREMISE x -> fTYPED_FORMULA x
| CT_eval_result(x1, x2, x3) ->
- fFORMULA x1;
- fFORMULA x2;
- fFORMULA x3;
+ fFORMULA x1 ++
+ fFORMULA x2 ++
+ fFORMULA x3 ++
fNODE "eval_result" 3
| CT_premise(x1, x2) ->
- fID x1;
- fFORMULA x2;
+ fID x1 ++
+ fFORMULA x2 ++
fNODE "premise" 2
and fPREMISES_LIST = function
| CT_premises_list l ->
- (List.iter fPREMISE l);
+ (List.fold_left (++) (mt()) (List.map fPREMISE l)) ++
fNODE "premises_list" (List.length l)
and fPREMISE_PATTERN = function
| CT_premise_pattern(x1, x2) ->
- fID_OPT x1;
- fCONTEXT_PATTERN x2;
+ fID_OPT x1 ++
+ fCONTEXT_PATTERN x2 ++
fNODE "premise_pattern" 2
and fPROOF_SCRIPT = function
| CT_proof_script l ->
- (List.iter fCOMMAND l);
+ (List.fold_left (++) (mt()) (List.map fCOMMAND l)) ++
fNODE "proof_script" (List.length l)
and fRECCONSTR = function
| CT_defrecconstr(x1, x2, x3) ->
- fID_OPT x1;
- fFORMULA x2;
- fFORMULA_OPT x3;
+ fID_OPT x1 ++
+ fFORMULA x2 ++
+ fFORMULA_OPT x3 ++
fNODE "defrecconstr" 3
| CT_defrecconstr_coercion(x1, x2, x3) ->
- fID_OPT x1;
- fFORMULA x2;
- fFORMULA_OPT x3;
+ fID_OPT x1 ++
+ fFORMULA x2 ++
+ fFORMULA_OPT x3 ++
fNODE "defrecconstr_coercion" 3
| CT_recconstr(x1, x2) ->
- fID_OPT x1;
- fFORMULA x2;
+ fID_OPT x1 ++
+ fFORMULA x2 ++
fNODE "recconstr" 2
| CT_recconstr_coercion(x1, x2) ->
- fID_OPT x1;
- fFORMULA x2;
+ fID_OPT x1 ++
+ fFORMULA x2 ++
fNODE "recconstr_coercion" 2
and fRECCONSTR_LIST = function
| CT_recconstr_list l ->
- (List.iter fRECCONSTR l);
+ (List.fold_left (++) (mt()) (List.map fRECCONSTR l)) ++
fNODE "recconstr_list" (List.length l)
and fREC_TACTIC_FUN = function
| CT_rec_tactic_fun(x1, x2, x3) ->
- fID x1;
- fID_OPT_NE_LIST x2;
- fTACTIC_COM x3;
+ fID x1 ++
+ fID_OPT_NE_LIST x2 ++
+ fTACTIC_COM x3 ++
fNODE "rec_tactic_fun" 3
and fREC_TACTIC_FUN_LIST = function
| CT_rec_tactic_fun_list(x,l) ->
- fREC_TACTIC_FUN x;
- (List.iter fREC_TACTIC_FUN l);
+ fREC_TACTIC_FUN x ++
+ (List.fold_left (++) (mt()) (List.map fREC_TACTIC_FUN l)) ++
fNODE "rec_tactic_fun_list" (1 + (List.length l))
and fRED_COM = function
| CT_cbv(x1, x2) ->
- fCONVERSION_FLAG_LIST x1;
- fCONV_SET x2;
+ fCONVERSION_FLAG_LIST x1 ++
+ fCONV_SET x2 ++
fNODE "cbv" 2
| CT_fold(x1) ->
- fFORMULA_LIST x1;
+ fFORMULA_LIST x1 ++
fNODE "fold" 1
| CT_hnf -> fNODE "hnf" 0
| CT_lazy(x1, x2) ->
- fCONVERSION_FLAG_LIST x1;
- fCONV_SET x2;
+ fCONVERSION_FLAG_LIST x1 ++
+ fCONV_SET x2 ++
fNODE "lazy" 2
| CT_pattern(x1) ->
- fPATTERN_NE_LIST x1;
+ fPATTERN_NE_LIST x1 ++
fNODE "pattern" 1
| CT_red -> fNODE "red" 0
| CT_cbvvm -> fNODE "vm_compute" 0
| CT_simpl(x1) ->
- fPATTERN_OPT x1;
+ fPATTERN_OPT x1 ++
fNODE "simpl" 1
| CT_unfold(x1) ->
- fUNFOLD_NE_LIST x1;
+ fUNFOLD_NE_LIST x1 ++
fNODE "unfold" 1
and fRETURN_INFO = function
| CT_coerce_NONE_to_RETURN_INFO x -> fNONE x
| CT_as_and_return(x1, x2) ->
- fID_OPT x1;
- fFORMULA x2;
+ fID_OPT x1 ++
+ fFORMULA x2 ++
fNODE "as_and_return" 2
| CT_return(x1) ->
- fFORMULA x1;
+ fFORMULA x1 ++
fNODE "return" 1
and fRULE = function
| CT_rule(x1, x2) ->
- fPREMISES_LIST x1;
- fFORMULA x2;
+ fPREMISES_LIST x1 ++
+ fFORMULA x2 ++
fNODE "rule" 2
and fRULE_LIST = function
| CT_rule_list l ->
- (List.iter fRULE l);
+ (List.fold_left (++) (mt()) (List.map fRULE l)) ++
fNODE "rule_list" (List.length l)
and fSCHEME_SPEC = function
| CT_scheme_spec(x1, x2, x3, x4) ->
- fID x1;
- fDEP x2;
- fFORMULA x3;
- fSORT_TYPE x4;
+ fID x1 ++
+ fDEP x2 ++
+ fFORMULA x3 ++
+ fSORT_TYPE x4 ++
fNODE "scheme_spec" 4
and fSCHEME_SPEC_LIST = function
| CT_scheme_spec_list(x,l) ->
- fSCHEME_SPEC x;
- (List.iter fSCHEME_SPEC l);
+ fSCHEME_SPEC x ++
+ (List.fold_left (++) (mt()) (List.map fSCHEME_SPEC l)) ++
fNODE "scheme_spec_list" (1 + (List.length l))
and fSCOMMENT_CONTENT = function
| CT_coerce_FORMULA_to_SCOMMENT_CONTENT x -> fFORMULA x
| CT_coerce_ID_OR_STRING_to_SCOMMENT_CONTENT x -> fID_OR_STRING x
and fSCOMMENT_CONTENT_LIST = function
| CT_scomment_content_list l ->
- (List.iter fSCOMMENT_CONTENT l);
+ (List.fold_left (++) (mt()) (List.map fSCOMMENT_CONTENT l)) ++
fNODE "scomment_content_list" (List.length l)
and fSECTION_BEGIN = function
| CT_section(x1) ->
- fID x1;
+ fID x1 ++
fNODE "section" 1
and fSECTION_BODY = function
| CT_section_body l ->
- (List.iter fCOMMAND l);
+ (List.fold_left (++) (mt()) (List.map fCOMMAND l)) ++
fNODE "section_body" (List.length l)
and fSIGNED_INT = function
| CT_coerce_INT_to_SIGNED_INT x -> fINT x
| CT_minus(x1) ->
- fINT x1;
+ fINT x1 ++
fNODE "minus" 1
and fSIGNED_INT_LIST = function
| CT_signed_int_list l ->
- (List.iter fSIGNED_INT l);
+ (List.fold_left (++) (mt()) (List.map fSIGNED_INT l)) ++
fNODE "signed_int_list" (List.length l)
and fSINGLE_OPTION_VALUE = function
| CT_coerce_INT_to_SINGLE_OPTION_VALUE x -> fINT x
| CT_coerce_STRING_to_SINGLE_OPTION_VALUE x -> fSTRING x
and fSORT_TYPE = function
-| CT_sortc x -> fATOM "sortc";
- (f_atom_string x);
- print_string "\n"and fSPEC_LIST = function
+| CT_sortc x -> fATOM "sortc" ++
+ (f_atom_string x) ++
+ str "\n"
+and fSPEC_LIST = function
| CT_coerce_BINDING_LIST_to_SPEC_LIST x -> fBINDING_LIST x
| CT_coerce_FORMULA_LIST_to_SPEC_LIST x -> fFORMULA_LIST x
and fSPEC_OPT = function
@@ -1360,12 +1376,13 @@ and fSTAR_OPT = function
| CT_coerce_NONE_to_STAR_OPT x -> fNONE x
| CT_coerce_STAR_to_STAR_OPT x -> fSTAR x
and fSTRING = function
-| CT_string x -> fATOM "string";
- (f_atom_string x);
- print_string "\n"and fSTRING_NE_LIST = function
+| CT_string x -> fATOM "string" ++
+ (f_atom_string x) ++
+ str "\n"
+and fSTRING_NE_LIST = function
| CT_string_ne_list(x,l) ->
- fSTRING x;
- (List.iter fSTRING l);
+ fSTRING x ++
+ (List.fold_left (++) (mt()) (List.map fSTRING l)) ++
fNODE "string_ne_list" (1 + (List.length l))
and fSTRING_OPT = function
| CT_coerce_NONE_to_STRING_OPT x -> fNONE x
@@ -1373,8 +1390,8 @@ and fSTRING_OPT = function
and fTABLE = function
| CT_coerce_ID_to_TABLE x -> fID x
| CT_table(x1, x2) ->
- fID x1;
- fID x2;
+ fID x1 ++
+ fID x2 ++
fNODE "table" 2
and fTACTIC_ARG = function
| CT_coerce_EVAL_CMD_to_TACTIC_ARG x -> fEVAL_CMD x
@@ -1384,429 +1401,429 @@ and fTACTIC_ARG = function
| CT_void -> fNODE "void" 0
and fTACTIC_ARG_LIST = function
| CT_tactic_arg_list(x,l) ->
- fTACTIC_ARG x;
- (List.iter fTACTIC_ARG l);
+ fTACTIC_ARG x ++
+ (List.fold_left (++) (mt()) (List.map fTACTIC_ARG l)) ++
fNODE "tactic_arg_list" (1 + (List.length l))
and fTACTIC_COM = function
| CT_abstract(x1, x2) ->
- fID_OPT x1;
- fTACTIC_COM x2;
+ fID_OPT x1 ++
+ fTACTIC_COM x2 ++
fNODE "abstract" 2
| CT_absurd(x1) ->
- fFORMULA x1;
+ fFORMULA x1 ++
fNODE "absurd" 1
| CT_any_constructor(x1) ->
- fTACTIC_OPT x1;
+ fTACTIC_OPT x1 ++
fNODE "any_constructor" 1
| CT_apply(x1, x2) ->
- fFORMULA x1;
- fSPEC_LIST x2;
+ fFORMULA x1 ++
+ fSPEC_LIST x2 ++
fNODE "apply" 2
| CT_assert(x1, x2) ->
- fID_OPT x1;
- fFORMULA x2;
+ fID_OPT x1 ++
+ fFORMULA x2 ++
fNODE "assert" 2
| CT_assumption -> fNODE "assumption" 0
| CT_auto(x1) ->
- fINT_OPT x1;
+ fINT_OPT x1 ++
fNODE "auto" 1
| CT_auto_with(x1, x2) ->
- fINT_OPT x1;
- fID_NE_LIST_OR_STAR x2;
+ fINT_OPT x1 ++
+ fID_NE_LIST_OR_STAR x2 ++
fNODE "auto_with" 2
| CT_autorewrite(x1, x2) ->
- fID_NE_LIST x1;
- fTACTIC_OPT x2;
+ fID_NE_LIST x1 ++
+ fTACTIC_OPT x2 ++
fNODE "autorewrite" 2
| CT_autotdb(x1) ->
- fINT_OPT x1;
+ fINT_OPT x1 ++
fNODE "autotdb" 1
| CT_case_type(x1) ->
- fFORMULA x1;
+ fFORMULA x1 ++
fNODE "case_type" 1
| CT_casetac(x1, x2) ->
- fFORMULA x1;
- fSPEC_LIST x2;
+ fFORMULA x1 ++
+ fSPEC_LIST x2 ++
fNODE "casetac" 2
| CT_cdhyp(x1) ->
- fID x1;
+ fID x1 ++
fNODE "cdhyp" 1
| CT_change(x1, x2) ->
- fFORMULA x1;
- fCLAUSE x2;
+ fFORMULA x1 ++
+ fCLAUSE x2 ++
fNODE "change" 2
| CT_change_local(x1, x2, x3) ->
- fPATTERN x1;
- fFORMULA x2;
- fCLAUSE x3;
+ fPATTERN x1 ++
+ fFORMULA x2 ++
+ fCLAUSE x3 ++
fNODE "change_local" 3
| CT_clear(x1) ->
- fID_NE_LIST x1;
+ fID_NE_LIST x1 ++
fNODE "clear" 1
| CT_clear_body(x1) ->
- fID_NE_LIST x1;
+ fID_NE_LIST x1 ++
fNODE "clear_body" 1
| CT_cofixtactic(x1, x2) ->
- fID_OPT x1;
- fCOFIX_TAC_LIST x2;
+ fID_OPT x1 ++
+ fCOFIX_TAC_LIST x2 ++
fNODE "cofixtactic" 2
| CT_condrewrite_lr(x1, x2, x3, x4) ->
- fTACTIC_COM x1;
- fFORMULA x2;
- fSPEC_LIST x3;
- fID_OPT x4;
+ fTACTIC_COM x1 ++
+ fFORMULA x2 ++
+ fSPEC_LIST x3 ++
+ fID_OPT x4 ++
fNODE "condrewrite_lr" 4
| CT_condrewrite_rl(x1, x2, x3, x4) ->
- fTACTIC_COM x1;
- fFORMULA x2;
- fSPEC_LIST x3;
- fID_OPT x4;
+ fTACTIC_COM x1 ++
+ fFORMULA x2 ++
+ fSPEC_LIST x3 ++
+ fID_OPT x4 ++
fNODE "condrewrite_rl" 4
| CT_constructor(x1, x2) ->
- fINT x1;
- fSPEC_LIST x2;
+ fINT x1 ++
+ fSPEC_LIST x2 ++
fNODE "constructor" 2
| CT_contradiction -> fNODE "contradiction" 0
| CT_contradiction_thm(x1, x2) ->
- fFORMULA x1;
- fSPEC_LIST x2;
+ fFORMULA x1 ++
+ fSPEC_LIST x2 ++
fNODE "contradiction_thm" 2
| CT_cut(x1) ->
- fFORMULA x1;
+ fFORMULA x1 ++
fNODE "cut" 1
| CT_cutrewrite_lr(x1, x2) ->
- fFORMULA x1;
- fID_OPT x2;
+ fFORMULA x1 ++
+ fID_OPT x2 ++
fNODE "cutrewrite_lr" 2
| CT_cutrewrite_rl(x1, x2) ->
- fFORMULA x1;
- fID_OPT x2;
+ fFORMULA x1 ++
+ fID_OPT x2 ++
fNODE "cutrewrite_rl" 2
| CT_dauto(x1, x2) ->
- fINT_OPT x1;
- fINT_OPT x2;
+ fINT_OPT x1 ++
+ fINT_OPT x2 ++
fNODE "dauto" 2
| CT_dconcl -> fNODE "dconcl" 0
| CT_decompose_list(x1, x2) ->
- fID_NE_LIST x1;
- fFORMULA x2;
+ fID_NE_LIST x1 ++
+ fFORMULA x2 ++
fNODE "decompose_list" 2
| CT_decompose_record(x1) ->
- fFORMULA x1;
+ fFORMULA x1 ++
fNODE "decompose_record" 1
| CT_decompose_sum(x1) ->
- fFORMULA x1;
+ fFORMULA x1 ++
fNODE "decompose_sum" 1
| CT_depinversion(x1, x2, x3, x4) ->
- fINV_TYPE x1;
- fID_OR_INT x2;
- fINTRO_PATT_OPT x3;
- fFORMULA_OPT x4;
+ fINV_TYPE x1 ++
+ fID_OR_INT x2 ++
+ fINTRO_PATT_OPT x3 ++
+ fFORMULA_OPT x4 ++
fNODE "depinversion" 4
| CT_deprewrite_lr(x1) ->
- fID x1;
+ fID x1 ++
fNODE "deprewrite_lr" 1
| CT_deprewrite_rl(x1) ->
- fID x1;
+ fID x1 ++
fNODE "deprewrite_rl" 1
| CT_destruct(x1) ->
- fID_OR_INT x1;
+ fID_OR_INT x1 ++
fNODE "destruct" 1
| CT_dhyp(x1) ->
- fID x1;
+ fID x1 ++
fNODE "dhyp" 1
| CT_discriminate_eq(x1) ->
- fID_OR_INT_OPT x1;
+ fID_OR_INT_OPT x1 ++
fNODE "discriminate_eq" 1
| CT_do(x1, x2) ->
- fID_OR_INT x1;
- fTACTIC_COM x2;
+ fID_OR_INT x1 ++
+ fTACTIC_COM x2 ++
fNODE "do" 2
| CT_eapply(x1, x2) ->
- fFORMULA x1;
- fSPEC_LIST x2;
+ fFORMULA x1 ++
+ fSPEC_LIST x2 ++
fNODE "eapply" 2
| CT_eauto(x1, x2) ->
- fID_OR_INT_OPT x1;
- fID_OR_INT_OPT x2;
+ fID_OR_INT_OPT x1 ++
+ fID_OR_INT_OPT x2 ++
fNODE "eauto" 2
| CT_eauto_with(x1, x2, x3) ->
- fID_OR_INT_OPT x1;
- fID_OR_INT_OPT x2;
- fID_NE_LIST_OR_STAR x3;
+ fID_OR_INT_OPT x1 ++
+ fID_OR_INT_OPT x2 ++
+ fID_NE_LIST_OR_STAR x3 ++
fNODE "eauto_with" 3
| CT_elim(x1, x2, x3) ->
- fFORMULA x1;
- fSPEC_LIST x2;
- fUSING x3;
+ fFORMULA x1 ++
+ fSPEC_LIST x2 ++
+ fUSING x3 ++
fNODE "elim" 3
| CT_elim_type(x1) ->
- fFORMULA x1;
+ fFORMULA x1 ++
fNODE "elim_type" 1
| CT_exact(x1) ->
- fFORMULA x1;
+ fFORMULA x1 ++
fNODE "exact" 1
| CT_exact_no_check(x1) ->
- fFORMULA x1;
+ fFORMULA x1 ++
fNODE "exact_no_check" 1
| CT_vm_cast_no_check(x1) ->
fFORMULA x1;
fNODE "vm_cast_no_check" 1
| CT_exists(x1) ->
- fSPEC_LIST x1;
+ fSPEC_LIST x1 ++
fNODE "exists" 1
| CT_fail(x1, x2) ->
- fID_OR_INT x1;
- fSTRING_OPT x2;
+ fID_OR_INT x1 ++
+ fSTRING_OPT x2 ++
fNODE "fail" 2
| CT_first(x,l) ->
- fTACTIC_COM x;
- (List.iter fTACTIC_COM l);
+ fTACTIC_COM x ++
+ (List.fold_left (++) (mt()) (List.map fTACTIC_COM l)) ++
fNODE "first" (1 + (List.length l))
| CT_firstorder(x1) ->
- fTACTIC_OPT x1;
+ fTACTIC_OPT x1 ++
fNODE "firstorder" 1
| CT_firstorder_using(x1, x2) ->
- fTACTIC_OPT x1;
- fID_NE_LIST x2;
+ fTACTIC_OPT x1 ++
+ fID_NE_LIST x2 ++
fNODE "firstorder_using" 2
| CT_firstorder_with(x1, x2) ->
- fTACTIC_OPT x1;
- fID_NE_LIST x2;
+ fTACTIC_OPT x1 ++
+ fID_NE_LIST x2 ++
fNODE "firstorder_with" 2
| CT_fixtactic(x1, x2, x3) ->
- fID_OPT x1;
- fINT x2;
- fFIX_TAC_LIST x3;
+ fID_OPT x1 ++
+ fINT x2 ++
+ fFIX_TAC_LIST x3 ++
fNODE "fixtactic" 3
| CT_formula_marker(x1) ->
- fFORMULA x1;
+ fFORMULA x1 ++
fNODE "formula_marker" 1
| CT_fresh(x1) ->
- fSTRING_OPT x1;
+ fSTRING_OPT x1 ++
fNODE "fresh" 1
| CT_generalize(x1) ->
- fFORMULA_NE_LIST x1;
+ fFORMULA_NE_LIST x1 ++
fNODE "generalize" 1
| CT_generalize_dependent(x1) ->
- fFORMULA x1;
+ fFORMULA x1 ++
fNODE "generalize_dependent" 1
| CT_idtac(x1) ->
- fSTRING_OPT x1;
+ fSTRING_OPT x1 ++
fNODE "idtac" 1
| CT_induction(x1) ->
- fID_OR_INT x1;
+ fID_OR_INT x1 ++
fNODE "induction" 1
| CT_info(x1) ->
- fTACTIC_COM x1;
+ fTACTIC_COM x1 ++
fNODE "info" 1
| CT_injection_eq(x1) ->
- fID_OR_INT_OPT x1;
+ fID_OR_INT_OPT x1 ++
fNODE "injection_eq" 1
| CT_instantiate(x1, x2, x3) ->
- fINT x1;
- fFORMULA x2;
- fCLAUSE x3;
+ fINT x1 ++
+ fFORMULA x2 ++
+ fCLAUSE x3 ++
fNODE "instantiate" 3
| CT_intro(x1) ->
- fID_OPT x1;
+ fID_OPT x1 ++
fNODE "intro" 1
| CT_intro_after(x1, x2) ->
- fID_OPT x1;
- fID x2;
+ fID_OPT x1 ++
+ fID x2 ++
fNODE "intro_after" 2
| CT_intros(x1) ->
- fINTRO_PATT_LIST x1;
+ fINTRO_PATT_LIST x1 ++
fNODE "intros" 1
| CT_intros_until(x1) ->
- fID_OR_INT x1;
+ fID_OR_INT x1 ++
fNODE "intros_until" 1
| CT_inversion(x1, x2, x3, x4) ->
- fINV_TYPE x1;
- fID_OR_INT x2;
- fINTRO_PATT_OPT x3;
- fID_LIST x4;
+ fINV_TYPE x1 ++
+ fID_OR_INT x2 ++
+ fINTRO_PATT_OPT x3 ++
+ fID_LIST x4 ++
fNODE "inversion" 4
| CT_left(x1) ->
- fSPEC_LIST x1;
+ fSPEC_LIST x1 ++
fNODE "left" 1
| CT_let_ltac(x1, x2) ->
- fLET_CLAUSES x1;
- fLET_VALUE x2;
+ fLET_CLAUSES x1 ++
+ fLET_VALUE x2 ++
fNODE "let_ltac" 2
| CT_lettac(x1, x2, x3) ->
- fID_OPT x1;
- fFORMULA x2;
- fCLAUSE x3;
+ fID_OPT x1 ++
+ fFORMULA x2 ++
+ fCLAUSE x3 ++
fNODE "lettac" 3
| CT_match_context(x,l) ->
- fCONTEXT_RULE x;
- (List.iter fCONTEXT_RULE l);
+ fCONTEXT_RULE x ++
+ (List.fold_left (++) (mt()) (List.map fCONTEXT_RULE l)) ++
fNODE "match_context" (1 + (List.length l))
| CT_match_context_reverse(x,l) ->
- fCONTEXT_RULE x;
- (List.iter fCONTEXT_RULE l);
+ fCONTEXT_RULE x ++
+ (List.fold_left (++) (mt()) (List.map fCONTEXT_RULE l)) ++
fNODE "match_context_reverse" (1 + (List.length l))
| CT_match_tac(x1, x2) ->
- fTACTIC_COM x1;
- fMATCH_TAC_RULES x2;
+ fTACTIC_COM x1 ++
+ fMATCH_TAC_RULES x2 ++
fNODE "match_tac" 2
| CT_move_after(x1, x2) ->
- fID x1;
- fID x2;
+ fID x1 ++
+ fID x2 ++
fNODE "move_after" 2
| CT_new_destruct(x1, x2, x3) ->
- (List.iter fFORMULA_OR_INT x1); (* Julien F. Est-ce correct? *)
- fUSING x2;
- fINTRO_PATT_OPT x3;
+ (List.fold_left (++) (mt()) (List.map fFORMULA_OR_INT x1)) ++ (* Julien F. Est-ce correct? *)
+ fUSING x2 ++
+ fINTRO_PATT_OPT x3 ++
fNODE "new_destruct" 3
| CT_new_induction(x1, x2, x3) ->
- (List.iter fFORMULA_OR_INT x1); (* Pierre C. Est-ce correct? *)
- fUSING x2;
- fINTRO_PATT_OPT x3;
+ (List.fold_left (++) (mt()) (List.map fFORMULA_OR_INT x1)) ++ (* Pierre C. Est-ce correct? *)
+ fUSING x2 ++
+ fINTRO_PATT_OPT x3 ++
fNODE "new_induction" 3
| CT_omega -> fNODE "omega" 0
| CT_orelse(x1, x2) ->
- fTACTIC_COM x1;
- fTACTIC_COM x2;
+ fTACTIC_COM x1 ++
+ fTACTIC_COM x2 ++
fNODE "orelse" 2
| CT_parallel(x,l) ->
- fTACTIC_COM x;
- (List.iter fTACTIC_COM l);
+ fTACTIC_COM x ++
+ (List.fold_left (++) (mt()) (List.map fTACTIC_COM l)) ++
fNODE "parallel" (1 + (List.length l))
| CT_pose(x1, x2) ->
- fID_OPT x1;
- fFORMULA x2;
+ fID_OPT x1 ++
+ fFORMULA x2 ++
fNODE "pose" 2
| CT_progress(x1) ->
- fTACTIC_COM x1;
+ fTACTIC_COM x1 ++
fNODE "progress" 1
| CT_prolog(x1, x2) ->
- fFORMULA_LIST x1;
- fINT x2;
+ fFORMULA_LIST x1 ++
+ fINT x2 ++
fNODE "prolog" 2
| CT_rec_tactic_in(x1, x2) ->
- fREC_TACTIC_FUN_LIST x1;
- fTACTIC_COM x2;
+ fREC_TACTIC_FUN_LIST x1 ++
+ fTACTIC_COM x2 ++
fNODE "rec_tactic_in" 2
| CT_reduce(x1, x2) ->
- fRED_COM x1;
- fCLAUSE x2;
+ fRED_COM x1 ++
+ fCLAUSE x2 ++
fNODE "reduce" 2
| CT_refine(x1) ->
- fFORMULA x1;
+ fFORMULA x1 ++
fNODE "refine" 1
| CT_reflexivity -> fNODE "reflexivity" 0
| CT_rename(x1, x2) ->
- fID x1;
- fID x2;
+ fID x1 ++
+ fID x2 ++
fNODE "rename" 2
| CT_repeat(x1) ->
- fTACTIC_COM x1;
+ fTACTIC_COM x1 ++
fNODE "repeat" 1
| CT_replace_with(x1, x2,x3,x4) ->
- fFORMULA x1;
- fFORMULA x2;
- fCLAUSE x3;
- fTACTIC_OPT x4;
+ fFORMULA x1 ++
+ fFORMULA x2 ++
+ fCLAUSE x3 ++
+ fTACTIC_OPT x4 ++
fNODE "replace_with" 4
| CT_rewrite_lr(x1, x2, x3) ->
- fFORMULA x1;
- fSPEC_LIST x2;
- fCLAUSE x3;
+ fFORMULA x1 ++
+ fSPEC_LIST x2 ++
+ fCLAUSE x3 ++
fNODE "rewrite_lr" 3
| CT_rewrite_rl(x1, x2, x3) ->
- fFORMULA x1;
- fSPEC_LIST x2;
- fCLAUSE x3;
+ fFORMULA x1 ++
+ fSPEC_LIST x2 ++
+ fCLAUSE x3 ++
fNODE "rewrite_rl" 3
| CT_right(x1) ->
- fSPEC_LIST x1;
+ fSPEC_LIST x1 ++
fNODE "right" 1
| CT_ring(x1) ->
- fFORMULA_LIST x1;
+ fFORMULA_LIST x1 ++
fNODE "ring" 1
| CT_simple_user_tac(x1, x2) ->
- fID x1;
- fTACTIC_ARG_LIST x2;
+ fID x1 ++
+ fTACTIC_ARG_LIST x2 ++
fNODE "simple_user_tac" 2
| CT_simplify_eq(x1) ->
- fID_OR_INT_OPT x1;
+ fID_OR_INT_OPT x1 ++
fNODE "simplify_eq" 1
| CT_specialize(x1, x2, x3) ->
- fINT_OPT x1;
- fFORMULA x2;
- fSPEC_LIST x3;
+ fINT_OPT x1 ++
+ fFORMULA x2 ++
+ fSPEC_LIST x3 ++
fNODE "specialize" 3
| CT_split(x1) ->
- fSPEC_LIST x1;
+ fSPEC_LIST x1 ++
fNODE "split" 1
| CT_subst(x1) ->
- fID_LIST x1;
+ fID_LIST x1 ++
fNODE "subst" 1
| CT_superauto(x1, x2, x3, x4) ->
- fINT_OPT x1;
- fID_LIST x2;
- fDESTRUCTING x3;
- fUSINGTDB x4;
+ fINT_OPT x1 ++
+ fID_LIST x2 ++
+ fDESTRUCTING x3 ++
+ fUSINGTDB x4 ++
fNODE "superauto" 4
| CT_symmetry(x1) ->
- fCLAUSE x1;
+ fCLAUSE x1 ++
fNODE "symmetry" 1
| CT_tac_double(x1, x2) ->
- fID_OR_INT x1;
- fID_OR_INT x2;
+ fID_OR_INT x1 ++
+ fID_OR_INT x2 ++
fNODE "tac_double" 2
| CT_tacsolve(x,l) ->
- fTACTIC_COM x;
- (List.iter fTACTIC_COM l);
+ fTACTIC_COM x ++
+ (List.fold_left (++) (mt()) (List.map fTACTIC_COM l)) ++
fNODE "tacsolve" (1 + (List.length l))
| CT_tactic_fun(x1, x2) ->
- fID_OPT_NE_LIST x1;
- fTACTIC_COM x2;
+ fID_OPT_NE_LIST x1 ++
+ fTACTIC_COM x2 ++
fNODE "tactic_fun" 2
| CT_then(x,l) ->
- fTACTIC_COM x;
- (List.iter fTACTIC_COM l);
+ fTACTIC_COM x ++
+ (List.fold_left (++) (mt()) (List.map fTACTIC_COM l)) ++
fNODE "then" (1 + (List.length l))
| CT_transitivity(x1) ->
- fFORMULA x1;
+ fFORMULA x1 ++
fNODE "transitivity" 1
| CT_trivial -> fNODE "trivial" 0
| CT_trivial_with(x1) ->
- fID_NE_LIST_OR_STAR x1;
+ fID_NE_LIST_OR_STAR x1 ++
fNODE "trivial_with" 1
| CT_truecut(x1, x2) ->
- fID_OPT x1;
- fFORMULA x2;
+ fID_OPT x1 ++
+ fFORMULA x2 ++
fNODE "truecut" 2
| CT_try(x1) ->
- fTACTIC_COM x1;
+ fTACTIC_COM x1 ++
fNODE "try" 1
| CT_use(x1) ->
- fFORMULA x1;
+ fFORMULA x1 ++
fNODE "use" 1
| CT_use_inversion(x1, x2, x3) ->
- fID_OR_INT x1;
- fFORMULA x2;
- fID_LIST x3;
+ fID_OR_INT x1 ++
+ fFORMULA x2 ++
+ fID_LIST x3 ++
fNODE "use_inversion" 3
| CT_user_tac(x1, x2) ->
- fID x1;
- fTARG_LIST x2;
+ fID x1 ++
+ fTARG_LIST x2 ++
fNODE "user_tac" 2
and fTACTIC_OPT = function
| CT_coerce_NONE_to_TACTIC_OPT x -> fNONE x
| CT_coerce_TACTIC_COM_to_TACTIC_OPT x -> fTACTIC_COM x
and fTAC_DEF = function
| CT_tac_def(x1, x2) ->
- fID x1;
- fTACTIC_COM x2;
+ fID x1 ++
+ fTACTIC_COM x2 ++
fNODE "tac_def" 2
and fTAC_DEF_NE_LIST = function
| CT_tac_def_ne_list(x,l) ->
- fTAC_DEF x;
- (List.iter fTAC_DEF l);
+ fTAC_DEF x ++
+ (List.fold_left (++) (mt()) (List.map fTAC_DEF l)) ++
fNODE "tac_def_ne_list" (1 + (List.length l))
and fTARG = function
| CT_coerce_BINDING_to_TARG x -> fBINDING x
@@ -1824,81 +1841,83 @@ and fTARG = function
| CT_coerce_UNFOLD_NE_LIST_to_TARG x -> fUNFOLD_NE_LIST x
and fTARG_LIST = function
| CT_targ_list l ->
- (List.iter fTARG l);
+ (List.fold_left (++) (mt()) (List.map fTARG l)) ++
fNODE "targ_list" (List.length l)
and fTERM_CHANGE = function
| CT_check_term(x1) ->
- fFORMULA x1;
+ fFORMULA x1 ++
fNODE "check_term" 1
| CT_inst_term(x1, x2) ->
- fID x1;
- fFORMULA x2;
+ fID x1 ++
+ fFORMULA x2 ++
fNODE "inst_term" 2
and fTEXT = function
| CT_coerce_ID_to_TEXT x -> fID x
| CT_text_formula(x1) ->
- fFORMULA x1;
+ fFORMULA x1 ++
fNODE "text_formula" 1
| CT_text_h l ->
- (List.iter fTEXT l);
+ (List.fold_left (++) (mt()) (List.map fTEXT l)) ++
fNODE "text_h" (List.length l)
| CT_text_hv l ->
- (List.iter fTEXT l);
+ (List.fold_left (++) (mt()) (List.map fTEXT l)) ++
fNODE "text_hv" (List.length l)
| CT_text_op l ->
- (List.iter fTEXT l);
+ (List.fold_left (++) (mt()) (List.map fTEXT l)) ++
fNODE "text_op" (List.length l)
| CT_text_path(x1) ->
- fSIGNED_INT_LIST x1;
+ fSIGNED_INT_LIST x1 ++
fNODE "text_path" 1
| CT_text_v l ->
- (List.iter fTEXT l);
+ (List.fold_left (++) (mt()) (List.map fTEXT l)) ++
fNODE "text_v" (List.length l)
and fTHEOREM_GOAL = function
| CT_goal(x1) ->
- fFORMULA x1;
+ fFORMULA x1 ++
fNODE "goal" 1
| CT_theorem_goal(x1, x2, x3, x4) ->
- fDEFN_OR_THM x1;
- fID x2;
- fBINDER_LIST x3;
- fFORMULA x4;
+ fDEFN_OR_THM x1 ++
+ fID x2 ++
+ fBINDER_LIST x3 ++
+ fFORMULA x4 ++
fNODE "theorem_goal" 4
and fTHM = function
-| CT_thm x -> fATOM "thm";
- (f_atom_string x);
- print_string "\n"and fTHM_OPT = function
+| CT_thm x -> fATOM "thm" ++
+ (f_atom_string x) ++
+ str "\n"
+and fTHM_OPT = function
| CT_coerce_NONE_to_THM_OPT x -> fNONE x
| CT_coerce_THM_to_THM_OPT x -> fTHM x
and fTYPED_FORMULA = function
| CT_typed_formula(x1, x2) ->
- fFORMULA x1;
- fFORMULA x2;
+ fFORMULA x1 ++
+ fFORMULA x2 ++
fNODE "typed_formula" 2
and fUNFOLD = function
| CT_coerce_ID_to_UNFOLD x -> fID x
| CT_unfold_occ(x1, x2) ->
- fID x1;
- fINT_NE_LIST x2;
+ fID x1 ++
+ fINT_NE_LIST x2 ++
fNODE "unfold_occ" 2
and fUNFOLD_NE_LIST = function
| CT_unfold_ne_list(x,l) ->
- fUNFOLD x;
- (List.iter fUNFOLD l);
+ fUNFOLD x ++
+ (List.fold_left (++) (mt()) (List.map fUNFOLD l)) ++
fNODE "unfold_ne_list" (1 + (List.length l))
and fUSING = function
| CT_coerce_NONE_to_USING x -> fNONE x
| CT_using(x1, x2) ->
- fFORMULA x1;
- fSPEC_LIST x2;
+ fFORMULA x1 ++
+ fSPEC_LIST x2 ++
fNODE "using" 2
and fUSINGTDB = function
| CT_coerce_NONE_to_USINGTDB x -> fNONE x
| CT_usingtdb -> fNODE "usingtdb" 0
and fVAR = function
-| CT_var x -> fATOM "var";
- (f_atom_string x);
- print_string "\n"and fVARG = function
+| CT_var x -> fATOM "var" ++
+ (f_atom_string x) ++
+ str "\n"
+and fVARG = function
| CT_coerce_AST_to_VARG x -> fAST x
| CT_coerce_AST_LIST_to_VARG x -> fAST_LIST x
| CT_coerce_BINDER_to_VARG x -> fBINDER x
@@ -1916,7 +1935,7 @@ and fVAR = function
| CT_coerce_VARG_LIST_to_VARG x -> fVARG_LIST x
and fVARG_LIST = function
| CT_varg_list l ->
- (List.iter fVARG l);
+ (List.fold_left (++) (mt()) (List.map fVARG l)) ++
fNODE "varg_list" (List.length l)
and fVERBOSE_OPT = function
| CT_coerce_NONE_to_VERBOSE_OPT x -> fNONE x
diff --git a/contrib/interface/vtp.mli b/contrib/interface/vtp.mli
index fe30b317a..d7bd8db53 100644
--- a/contrib/interface/vtp.mli
+++ b/contrib/interface/vtp.mli
@@ -1,15 +1,16 @@
open Ascent;;
+open Pp;;
-val fCOMMAND_LIST : ct_COMMAND_LIST -> unit;;
-val fCOMMAND : ct_COMMAND -> unit;;
-val fTACTIC_COM : ct_TACTIC_COM -> unit;;
-val fFORMULA : ct_FORMULA -> unit;;
-val fID : ct_ID -> unit;;
-val fSTRING : ct_STRING -> unit;;
-val fINT : ct_INT -> unit;;
-val fRULE_LIST : ct_RULE_LIST -> unit;;
-val fRULE : ct_RULE -> unit;;
-val fSIGNED_INT_LIST : ct_SIGNED_INT_LIST -> unit;;
-val fPREMISES_LIST : ct_PREMISES_LIST -> unit;;
-val fID_LIST : ct_ID_LIST -> unit;;
-val fTEXT : ct_TEXT -> unit;; \ No newline at end of file
+val fCOMMAND_LIST : ct_COMMAND_LIST -> std_ppcmds;;
+val fCOMMAND : ct_COMMAND -> std_ppcmds;;
+val fTACTIC_COM : ct_TACTIC_COM -> std_ppcmds;;
+val fFORMULA : ct_FORMULA -> std_ppcmds;;
+val fID : ct_ID -> std_ppcmds;;
+val fSTRING : ct_STRING -> std_ppcmds;;
+val fINT : ct_INT -> std_ppcmds;;
+val fRULE_LIST : ct_RULE_LIST -> std_ppcmds;;
+val fRULE : ct_RULE -> std_ppcmds;;
+val fSIGNED_INT_LIST : ct_SIGNED_INT_LIST -> std_ppcmds;;
+val fPREMISES_LIST : ct_PREMISES_LIST -> std_ppcmds;;
+val fID_LIST : ct_ID_LIST -> std_ppcmds;;
+val fTEXT : ct_TEXT -> std_ppcmds;;
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index 601952292..522419030 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -15,12 +15,6 @@ open Libnames;;
open Goptions;;
-let in_coq_ref = ref false;;
-
-let declare_in_coq () = in_coq_ref:=true;;
-
-let in_coq () = !in_coq_ref;;
-
(* // Verify whether this is dead code, as of coq version 7 *)
(* The following three sentences have been added to cope with a change
of strategy from the Coq team in the way rules construct ast's. The
diff --git a/contrib/interface/xlate.mli b/contrib/interface/xlate.mli
index bedb4ac82..2e2b95fe7 100644
--- a/contrib/interface/xlate.mli
+++ b/contrib/interface/xlate.mli
@@ -6,4 +6,3 @@ val xlate_formula : Topconstr.constr_expr -> ct_FORMULA;;
val xlate_ident : Names.identifier -> ct_ID;;
val xlate_vernac_list : Vernacexpr.vernac_expr -> ct_COMMAND_LIST;;
-val declare_in_coq : (unit -> unit);;
diff --git a/lib/pp.ml4 b/lib/pp.ml4
index 324499337..d4e6eb722 100644
--- a/lib/pp.ml4
+++ b/lib/pp.ml4
@@ -17,6 +17,7 @@ open Pp_control
[Pp] -> [Options] *)
let print_emacs = ref false
let make_pp_emacs() = print_emacs:=true
+let make_pp_nonemacs() = print_emacs:=false
(* The different kinds of blocks are:
\begin{description}
diff --git a/lib/pp.mli b/lib/pp.mli
index d4248cc7f..7b9d7d663 100644
--- a/lib/pp.mli
+++ b/lib/pp.mli
@@ -16,6 +16,7 @@ open Pp_control
chars inserted at some places). This function should called once in
module [Options], that's all. *)
val make_pp_emacs:unit -> unit
+val make_pp_nonemacs:unit -> unit
(* Pretty-printers. *)
diff --git a/library/lib.ml b/library/lib.ml
index 4c822114e..c51dc79a7 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -22,9 +22,11 @@ type node =
| Leaf of obj
| CompilingLibrary of object_prefix
| OpenedModule of bool option * object_prefix * Summary.frozen
+ | ClosedModule of library_segment
| OpenedModtype of object_prefix * Summary.frozen
+ | ClosedModtype of library_segment
| OpenedSection of object_prefix * Summary.frozen
- | ClosedSection
+ | ClosedSection of library_segment
| FrozenState of Summary.frozen
and library_entry = object_name * node
@@ -60,7 +62,11 @@ let classify_segment seg =
clean ((id,o')::substl, keepl, anticipl) stk
| Anticipate o' ->
clean (substl, keepl, o'::anticipl) stk)
- | (oname,ClosedSection) :: stk -> clean acc stk
+ | (_,ClosedSection _) :: stk -> clean acc stk
+ (* LEM; TODO: Understand what this does and see if what I do is the
+ correct thing for ClosedMod(ule|type) *)
+ | (_,ClosedModule _) :: stk -> clean acc stk
+ | (_,ClosedModtype _) :: stk -> clean acc stk
| (_,OpenedSection _) :: _ -> error "there are still opened sections"
| (_,OpenedModule _) :: _ -> error "there are still opened modules"
| (_,OpenedModtype _) :: _ -> error "there are still opened module types"
@@ -152,16 +158,28 @@ let find_split_p p =
let split_lib_gen test =
let rec collect after equal = function
- | hd::before ->
- if test hd then collect after (hd::equal) before else after,equal,hd::before
- | [] -> after,equal,[]
+ | hd::strict_before as before ->
+ if test hd then collect after (hd::equal) strict_before else after,equal,before
+ | [] as before -> after,equal,before
in
let rec findeq after = function
| hd :: before ->
- if test hd then collect after [hd] before else findeq (hd::after) before
- | [] -> error "no such entry"
- in
- findeq [] !lib_stk
+ if test hd
+ then Some (collect after [hd] before)
+ else (match hd with
+ | (sp,ClosedModule seg)
+ | (sp,ClosedModtype seg)
+ | (sp,ClosedSection seg) ->
+ (match findeq after seg with
+ | None -> findeq (hd::after) before
+ | Some (sub_after,sub_equal,sub_before) ->
+ Some (sub_after, sub_equal, (List.append sub_before before)))
+ | _ -> findeq (hd::after) before)
+ | [] -> None
+ in
+ match findeq [] !lib_stk with
+ | None -> error "no such entry"
+ | Some r -> r
let split_lib sp = split_lib_gen (fun x -> (fst x) = sp)
@@ -251,9 +269,15 @@ let end_module id =
with Not_found ->
error "no opened modules"
in
- let (after,_,before) = split_lib oname in
+ let (after,modopening,before) = split_lib oname in
lib_stk := before;
+ add_entry (make_oname id) (ClosedModule (List.rev_append after (List.rev modopening)));
let prefix = !path_prefix in
+ (* LEM: This module business seems more complicated than sections;
+ shouldn't a backtrack into a closed module also do something
+ with global.ml, given that closing a module does?
+ TODO
+ *)
recalc_path_prefix ();
(* add_frozen_state must be called after processing the module,
because we cannot recache interactive modules *)
@@ -285,8 +309,9 @@ let end_modtype id =
with Not_found ->
error "no opened module types"
in
- let (after,_,before) = split_lib sp in
+ let (after,modtypeopening,before) = split_lib sp in
lib_stk := before;
+ add_entry (make_oname id) (ClosedModtype (List.rev_append after (List.rev modtypeopening)));
let dir = !path_prefix in
recalc_path_prefix ();
(* add_frozen_state must be called after processing the module type.
@@ -496,11 +521,11 @@ let close_section id =
with Not_found ->
error "no opened section"
in
- let (secdecls,_,before) = split_lib oname in
+ let (secdecls,secopening,before) = split_lib oname in
lib_stk := before;
let full_olddir = fst !path_prefix in
pop_path_prefix ();
- add_entry (make_oname id) ClosedSection;
+ add_entry (make_oname id) (ClosedSection (List.rev_append secdecls (List.rev secopening)));
if !Options.xml_export then !xml_close_section id;
let newdecls = List.map discharge_item secdecls in
Summary.section_unfreeze_summaries fs;
@@ -550,7 +575,7 @@ let reset_name (loc,id) =
let is_mod_node = function
| OpenedModule _ | OpenedModtype _ | OpenedSection _
- | ClosedSection -> true
+ | ClosedModule _ | ClosedModtype _ | ClosedSection _ -> true
| Leaf o -> let t = object_tag o in t = "MODULE" || t = "MODULE TYPE"
| _ -> false
diff --git a/library/lib.mli b/library/lib.mli
index 9f5a3f78a..f13ff82ae 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -25,9 +25,11 @@ type node =
| Leaf of obj
| CompilingLibrary of object_prefix
| OpenedModule of bool option * object_prefix * Summary.frozen
+ | ClosedModule of library_segment
| OpenedModtype of object_prefix * Summary.frozen
+ | ClosedModtype of library_segment
| OpenedSection of object_prefix * Summary.frozen
- | ClosedSection
+ | ClosedSection of library_segment
| FrozenState of Summary.frozen
and library_segment = (object_name * node) list
diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml
index e1f375d0a..901866523 100644
--- a/parsing/ppconstr.ml
+++ b/parsing/ppconstr.ml
@@ -619,10 +619,28 @@ let rec strip_context n iscast t =
LocalRawDef (na,b) :: bl', c
| _ -> anomaly "strip_context"
-let pr_constr_expr c = pr lsimple c
-let pr_lconstr_expr c = pr ltop c
-let pr_pattern_expr c = pr lsimple c
-let pr_lpattern_expr c = pr ltop c
+type term_pr = {
+ pr_constr_expr : constr_expr -> std_ppcmds;
+ pr_lconstr_expr : constr_expr -> std_ppcmds;
+ pr_pattern_expr : Tacexpr.pattern_expr -> std_ppcmds;
+ pr_lpattern_expr : Tacexpr.pattern_expr -> std_ppcmds
+}
+
+let default_term_pr = {
+ pr_constr_expr = pr lsimple;
+ pr_lconstr_expr = pr ltop;
+ pr_pattern_expr = pr lsimple;
+ pr_lpattern_expr = pr ltop
+}
+
+let term_pr = ref default_term_pr
+
+let set_term_pr = (:=) term_pr
+
+let pr_constr_expr c = !term_pr.pr_constr_expr c
+let pr_lconstr_expr c = !term_pr.pr_lconstr_expr c
+let pr_pattern_expr c = !term_pr.pr_pattern_expr c
+let pr_lpattern_expr c = !term_pr.pr_lpattern_expr c
let pr_cases_pattern_expr = pr_patt ltop
diff --git a/parsing/ppconstr.mli b/parsing/ppconstr.mli
index 1cafe2800..f351144dc 100644
--- a/parsing/ppconstr.mli
+++ b/parsing/ppconstr.mli
@@ -70,3 +70,13 @@ val pr_lpattern_expr : Tacexpr.pattern_expr -> std_ppcmds
val pr_constr_expr : constr_expr -> std_ppcmds
val pr_lconstr_expr : constr_expr -> std_ppcmds
val pr_cases_pattern_expr : cases_pattern_expr -> std_ppcmds
+
+type term_pr = {
+ pr_constr_expr : constr_expr -> std_ppcmds;
+ pr_lconstr_expr : constr_expr -> std_ppcmds;
+ pr_pattern_expr : Tacexpr.pattern_expr -> std_ppcmds;
+ pr_lpattern_expr : Tacexpr.pattern_expr -> std_ppcmds
+}
+
+val set_term_pr : term_pr -> unit
+val default_term_pr : term_pr
diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml
index 7f8c6a776..64f6de12d 100644
--- a/parsing/prettyp.ml
+++ b/parsing/prettyp.ml
@@ -6,6 +6,10 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
+(* Changed by (and thus parts copyright ©) by Lionel Elie Mamane <lionel@mamane.lu>
+ * on May-June 2006 for implementation of abstraction of pretty-printing of objects.
+ *)
+
(* $Id$ *)
open Pp
@@ -29,6 +33,24 @@ open Libnames
open Nametab
open Recordops
+type object_pr = {
+ print_inductive : mutual_inductive -> std_ppcmds;
+ print_constant_with_infos : constant -> std_ppcmds;
+ print_section_variable : variable -> std_ppcmds;
+ print_syntactic_def : kernel_name -> std_ppcmds;
+ print_module : bool -> Names.module_path -> std_ppcmds;
+ print_modtype : kernel_name -> std_ppcmds;
+ print_named_decl : identifier * constr option * types -> std_ppcmds;
+ print_leaf_entry : bool -> Libnames.object_name * Libobject.obj -> Pp.std_ppcmds;
+ print_library_entry : bool -> (object_name * Lib.node) -> std_ppcmds option;
+ print_context : bool -> int option -> Lib.library_segment -> std_ppcmds;
+ print_typed_value_in_env : Environ.env -> Term.constr * Term.types -> Pp.std_ppcmds;
+ print_eval : Reductionops.reduction_function -> env -> Evd.evar_map -> Topconstr.constr_expr -> unsafe_judgment -> std_ppcmds;
+}
+
+let gallina_print_module = print_module
+let gallina_print_modtype = print_modtype
+
(*********************)
(** Basic printing *)
@@ -223,21 +245,12 @@ let print_located_qualid ref =
(******************************************)
(**** Printing declarations and judgments *)
+(**** Gallina layer *****)
-let print_typed_value_in_env env (trm,typ) =
+let gallina_print_typed_value_in_env env (trm,typ) =
(pr_lconstr_env env trm ++ fnl () ++
str " : " ++ pr_ltype_env env typ ++ fnl ())
-let print_typed_value x = print_typed_value_in_env (Global.env ()) x
-
-let print_judgment env {uj_val=trm;uj_type=typ} =
- print_typed_value_in_env env (trm, typ)
-
-let print_safe_judgment env j =
- let trm = Safe_typing.j_val j in
- let typ = Safe_typing.j_type j in
- print_typed_value_in_env env (trm, typ)
-
(* To be improved; the type should be used to provide the types in the
abstractions. This should be done recursively inside pr_lconstr, so that
the pretty-print of a proposition (P:(nat->nat)->Prop)(P [u]u)
@@ -255,7 +268,7 @@ let print_named_def name body typ =
let print_named_assum name typ =
(str "*** [" ++ str name ++ str " : " ++ pr_ltype typ ++ str "]" ++ fnl ())
-let print_named_decl (id,c,typ) =
+let gallina_print_named_decl (id,c,typ) =
let s = string_of_id id in
match c with
| Some body -> print_named_def s body typ
@@ -309,7 +322,7 @@ let pr_mutual_inductive finite indl =
prlist_with_sep (fun () -> fnl () ++ str" with ")
print_one_inductive indl)
-let print_inductive sp =
+let gallina_print_inductive sp =
let (mib,mip) = Global.lookup_inductive (sp,0) in
let mipv = mib.mind_packets in
let names = list_tabulate (fun x -> (sp,x)) (Array.length mipv) in
@@ -317,9 +330,9 @@ let print_inductive sp =
print_inductive_implicit_args sp mipv ++
print_inductive_argument_scopes sp mipv
-let print_section_variable sp =
+let gallina_print_section_variable sp =
let d = get_variable sp in
- print_named_decl d ++
+ gallina_print_named_decl d ++
print_name_infos (VarRef sp)
let print_body = function
@@ -348,70 +361,131 @@ let print_constant with_values sep sp =
(if with_values then print_typed_body (val_0,typ) else pr_ltype typ) ++
fnl ())
-let print_constant_with_infos sp =
+let gallina_print_constant_with_infos sp =
print_constant true " = " sp ++ print_name_infos (ConstRef sp)
-let print_syntactic_def sep kn =
- let qid = Nametab.shortest_qualid_of_syndef Idset.empty kn in
- let c = Syntax_def.search_syntactic_definition dummy_loc kn in
+let gallina_print_syntactic_def kn =
+ let sep = " := "
+ and qid = Nametab.shortest_qualid_of_syndef Idset.empty kn
+ and c = Syntax_def.search_syntactic_definition dummy_loc kn in
str "Notation " ++ pr_qualid qid ++ str sep ++
Constrextern.without_symbols pr_lrawconstr c ++ fnl ()
-let print_leaf_entry with_values sep ((sp,kn as oname),lobj) =
- let tag = object_tag lobj in
- match (oname,tag) with
- | (_,"VARIABLE") ->
- (* Outside sections, VARIABLES still exist but only with universes
- constraints *)
- (try Some(print_section_variable (basename sp)) with Not_found -> None)
- | (_,"CONSTANT") ->
- Some (print_constant with_values sep (constant_of_kn kn))
- | (_,"INDUCTIVE") ->
- Some (print_inductive kn)
- | (_,"MODULE") ->
- let (mp,_,l) = repr_kn kn in
- Some (print_module with_values (MPdot (mp,l)))
- | (_,"MODULE TYPE") ->
- Some (print_modtype kn)
- | (_,("AUTOHINT"|"GRAMMAR"|"SYNTAXCONSTANT"|"PPSYNTAX"|"TOKEN"|"CLASS"|
- "COERCION"|"REQUIRE"|"END-SECTION"|"STRUCTURE")) -> None
- (* To deal with forgotten cases... *)
- | (_,s) -> None
-(*
- | (_,s) ->
- (str(string_of_path sp) ++ str" : " ++
- str"Unrecognized object " ++ str s ++ fnl ())
-*)
-
-let rec print_library_entry with_values ent =
- let sep = if with_values then " = " else " : " in
+
+let gallina_print_leaf_entry with_values ((sp,kn as oname),lobj) =
+ let sep = if with_values then " = " else " : "
+ and tag = object_tag lobj in
+ match (oname,tag) with
+ | (_,"VARIABLE") ->
+ (* Outside sections, VARIABLES still exist but only with universes
+ constraints *)
+ (try Some(gallina_print_section_variable (basename sp)) with Not_found -> None)
+ | (_,"CONSTANT") ->
+ Some (print_constant with_values sep (constant_of_kn kn))
+ | (_,"INDUCTIVE") ->
+ Some (gallina_print_inductive kn)
+ | (_,"MODULE") ->
+ let (mp,_,l) = repr_kn kn in
+ Some (print_module with_values (MPdot (mp,l)))
+ | (_,"MODULE TYPE") ->
+ Some (print_modtype kn)
+ | (_,("AUTOHINT"|"GRAMMAR"|"SYNTAXCONSTANT"|"PPSYNTAX"|"TOKEN"|"CLASS"|
+ "COERCION"|"REQUIRE"|"END-SECTION"|"STRUCTURE")) -> None
+ (* To deal with forgotten cases... *)
+ | (_,s) -> None
+
+let gallina_print_library_entry with_values ent =
let pr_name (sp,_) = pr_id (basename sp) in
match ent with
| (oname,Lib.Leaf lobj) ->
- print_leaf_entry with_values sep (oname,lobj)
+ gallina_print_leaf_entry with_values (oname,lobj)
| (oname,Lib.OpenedSection (dir,_)) ->
Some (str " >>>>>>> Section " ++ pr_name oname)
- | (oname,Lib.ClosedSection) ->
+ | (oname,Lib.ClosedSection _) ->
Some (str " >>>>>>> Closed Section " ++ pr_name oname)
| (_,Lib.CompilingLibrary (dir,_)) ->
Some (str " >>>>>>> Library " ++ pr_dirpath dir)
| (oname,Lib.OpenedModule _) ->
Some (str " >>>>>>> Module " ++ pr_name oname)
+ | (oname,Lib.ClosedModule _) ->
+ Some (str " >>>>>>> Closed Module " ++ pr_name oname)
| (oname,Lib.OpenedModtype _) ->
Some (str " >>>>>>> Module Type " ++ pr_name oname)
+ | (oname,Lib.ClosedModtype _) ->
+ Some (str " >>>>>>> Closed Module Type " ++ pr_name oname)
| (_,Lib.FrozenState _) ->
None
-
-let print_context with_values =
+
+let gallina_print_leaf_entry with_values c =
+ match gallina_print_leaf_entry with_values c with
+ | None -> mt ()
+ | Some pp -> pp ++ fnl()
+
+let gallina_print_context with_values =
let rec prec n = function
| h::rest when n = None or out_some n > 0 ->
- (match print_library_entry with_values h with
+ (match gallina_print_library_entry with_values h with
| None -> prec n rest
| Some pp -> prec (option_map ((+) (-1)) n) rest ++ pp ++ fnl ())
| _ -> mt ()
in
prec
+let gallina_print_eval red_fun env evmap _ {uj_val=trm;uj_type=typ} =
+ let ntrm = red_fun env evmap trm in
+ (str " = " ++ gallina_print_typed_value_in_env env (ntrm,typ))
+
+(******************************************)
+(**** Printing abstraction layer *)
+
+let default_object_pr = {
+ print_inductive = gallina_print_inductive;
+ print_constant_with_infos = gallina_print_constant_with_infos;
+ print_section_variable = gallina_print_section_variable;
+ print_syntactic_def = gallina_print_syntactic_def;
+ print_module = gallina_print_module;
+ print_modtype = gallina_print_modtype;
+ print_named_decl = gallina_print_named_decl;
+ print_leaf_entry = gallina_print_leaf_entry;
+ print_library_entry = gallina_print_library_entry;
+ print_context = gallina_print_context;
+ print_typed_value_in_env = gallina_print_typed_value_in_env;
+ print_eval = gallina_print_eval;
+}
+
+let object_pr = ref default_object_pr
+let set_object_pr = (:=) object_pr
+
+let print_inductive x = !object_pr.print_inductive x
+let print_constant_with_infos c = !object_pr.print_constant_with_infos c
+let print_section_variable c = !object_pr.print_section_variable c
+let print_syntactic_def x = !object_pr.print_syntactic_def x
+let print_module x = !object_pr.print_module x
+let print_modtype x = !object_pr.print_modtype x
+let print_named_decl x = !object_pr.print_named_decl x
+let print_leaf_entry x = !object_pr.print_leaf_entry x
+let print_library_entry x = !object_pr.print_library_entry x
+let print_context x = !object_pr.print_context x
+let print_typed_value_in_env x = !object_pr.print_typed_value_in_env x
+let print_eval x = !object_pr.print_eval x
+
+(******************************************)
+(**** Printing declarations and judgments *)
+(**** Abstract layer *****)
+
+let print_typed_value x = print_typed_value_in_env (Global.env ()) x
+
+let print_judgment env {uj_val=trm;uj_type=typ} =
+ print_typed_value_in_env env (trm, typ)
+
+let print_safe_judgment env j =
+ let trm = Safe_typing.j_val j in
+ let typ = Safe_typing.j_type j in
+ print_typed_value_in_env env (trm, typ)
+
+(*********************)
+(* *)
+
let print_full_context () =
print_context true None (Lib.contents_after None)
@@ -485,8 +559,9 @@ let read_sec_context r =
let rec get_cxt in_cxt = function
| (_,Lib.OpenedSection ((dir',_),_) as hd)::rest ->
if dir = dir' then (hd::in_cxt) else get_cxt (hd::in_cxt) rest
- | (_,Lib.ClosedSection)::rest ->
+ | (_,Lib.ClosedSection _)::rest ->
error "Cannot print the contents of a closed section"
+ (* LEM: Actually, we could if we wanted to. *)
| [] -> []
| hd::rest -> get_cxt (hd::in_cxt) rest
in
@@ -499,17 +574,13 @@ let print_sec_context sec =
let print_sec_context_typ sec =
print_context false None (read_sec_context sec)
-let print_eval red_fun env {uj_val=trm;uj_type=typ} =
- let ntrm = red_fun env Evd.empty trm in
- (str " = " ++ print_judgment env {uj_val = ntrm; uj_type = typ})
-
let print_name ref =
match locate_any_name ref with
| Term (ConstRef sp) -> print_constant_with_infos sp
| Term (IndRef (sp,_)) -> print_inductive sp
| Term (ConstructRef ((sp,_),_)) -> print_inductive sp
| Term (VarRef sp) -> print_section_variable sp
- | Syntactic kn -> print_syntactic_def " := " kn
+ | Syntactic kn -> print_syntactic_def kn
| Dir (DirModule(dirpath,(mp,_))) -> print_module (printable_body dirpath) mp
| Dir _ -> mt ()
| ModuleType (_,kn) -> print_modtype kn
@@ -530,9 +601,7 @@ let print_name ref =
| Lib.Leaf obj -> (oname,obj)
| _ -> raise Not_found
in
- match print_leaf_entry true " = " (oname,lobj) with
- | None -> mt ()
- | Some pp -> pp ++ fnl()
+ print_leaf_entry true (oname,lobj)
with Not_found ->
errorlabstrm
"print_name" (pr_qualid qid ++ spc () ++ str "not a defined object")
@@ -561,7 +630,7 @@ let print_about ref =
| Term ref ->
print_ref false ref ++ print_name_infos ref ++ print_opacity ref
| Syntactic kn ->
- print_syntactic_def " := " kn
+ print_syntactic_def kn
| Dir _ | ModuleType _ | Undefined _ ->
mt () end
++
@@ -642,3 +711,4 @@ let print_canonical_projections () =
(canonical_projections ())
(*************************************************************************)
+
diff --git a/parsing/prettyp.mli b/parsing/prettyp.mli
index 84d7a5665..df16e3526 100644
--- a/parsing/prettyp.mli
+++ b/parsing/prettyp.mli
@@ -36,11 +36,10 @@ val print_sec_context_typ : reference -> std_ppcmds
val print_judgment : env -> unsafe_judgment -> std_ppcmds
val print_safe_judgment : env -> Safe_typing.judgment -> std_ppcmds
val print_eval :
- reduction_function -> env -> unsafe_judgment -> std_ppcmds
+ reduction_function -> env -> Evd.evar_map -> Topconstr.constr_expr -> unsafe_judgment -> std_ppcmds
(* This function is exported for the graphical user-interface pcoq *)
val build_inductive : mutual_inductive -> int ->
global_reference * rel_context * types * identifier array * types array
-val print_inductive : mutual_inductive -> std_ppcmds
val print_name : reference -> std_ppcmds
val print_opaque_name : reference -> std_ppcmds
val print_about : reference -> std_ppcmds
@@ -63,3 +62,21 @@ val inspect : int -> std_ppcmds
(* Locate *)
val print_located_qualid : reference -> std_ppcmds
+
+type object_pr = {
+ print_inductive : mutual_inductive -> std_ppcmds;
+ print_constant_with_infos : constant -> std_ppcmds;
+ print_section_variable : variable -> std_ppcmds;
+ print_syntactic_def : kernel_name -> std_ppcmds;
+ print_module : bool -> Names.module_path -> std_ppcmds;
+ print_modtype : kernel_name -> std_ppcmds;
+ print_named_decl : identifier * constr option * types -> std_ppcmds;
+ print_leaf_entry : bool -> Libnames.object_name * Libobject.obj -> Pp.std_ppcmds;
+ print_library_entry : bool -> (object_name * Lib.node) -> std_ppcmds option;
+ print_context : bool -> int option -> Lib.library_segment -> std_ppcmds;
+ print_typed_value_in_env : Environ.env -> Term.constr * Term.types -> Pp.std_ppcmds;
+ print_eval : reduction_function -> env -> Evd.evar_map -> Topconstr.constr_expr -> unsafe_judgment -> std_ppcmds
+}
+
+val set_object_pr : object_pr -> unit
+val default_object_pr : object_pr
diff --git a/parsing/printer.ml b/parsing/printer.ml
index deaf796ad..f777a37ed 100644
--- a/parsing/printer.ml
+++ b/parsing/printer.ml
@@ -254,7 +254,7 @@ let pr_subgoal_metas metas env=
hv 0 (prlist_with_sep mt pr_one metas)
(* display complete goal *)
-let pr_goal g =
+let default_pr_goal g =
let env = evar_env g in
let preamb,penv,pc =
if g.evar_extra = None then
@@ -297,12 +297,12 @@ let rec pr_evars_int i = function
str (string_of_existential ev) ++ str " : " ++ pegl)) ++
fnl () ++ pei
-let pr_subgoal n =
+let default_pr_subgoal n =
let rec prrec p = function
| [] -> error "No such goal"
| g::rest ->
if p = 1 then
- let pg = pr_goal g in
+ let pg = default_pr_goal g in
v 0 (str "subgoal " ++ int n ++ str " is:" ++ cut () ++ pg)
else
prrec (p-1) rest
@@ -310,7 +310,7 @@ let pr_subgoal n =
prrec n
(* Print open subgoals. Checks for uninstantiated existential variables *)
-let pr_subgoals close_cmd sigma = function
+let default_pr_subgoals close_cmd sigma = function
| [] ->
begin
match close_cmd with
@@ -327,7 +327,7 @@ let pr_subgoals close_cmd sigma = function
str "variables :" ++fnl () ++ (hov 0 pei))
end
| [g] ->
- let pg = pr_goal g in
+ let pg = default_pr_goal g in
v 0 (str ("1 "^"subgoal") ++cut () ++ pg)
| g1::rest ->
let rec pr_rec n = function
@@ -337,11 +337,39 @@ let pr_subgoals close_cmd sigma = function
let prest = pr_rec (n+1) rest in
(cut () ++ pc ++ prest)
in
- let pg1 = pr_goal g1 in
+ let pg1 = default_pr_goal g1 in
let prest = pr_rec 2 rest in
v 0 (int(List.length rest+1) ++ str" subgoals" ++ cut ()
++ pg1 ++ prest ++ fnl ())
+
+(**********************************************************************)
+(* Abstraction layer *)
+
+
+type printer_pr = {
+ pr_subgoals : string option -> evar_map -> goal list -> std_ppcmds;
+ pr_subgoal : int -> goal list -> std_ppcmds;
+ pr_goal : goal -> std_ppcmds;
+}
+
+let default_printer_pr = {
+ pr_subgoals = default_pr_subgoals;
+ pr_subgoal = default_pr_subgoal;
+ pr_goal = default_pr_goal;
+}
+
+let printer_pr = ref default_printer_pr
+
+let set_printer_pr = (:=) printer_pr
+
+let pr_subgoals x = !printer_pr.pr_subgoals x
+let pr_subgoal x = !printer_pr.pr_subgoal x
+let pr_goal x = !printer_pr.pr_goal x
+
+(* End abstraction layer *)
+(**********************************************************************)
+
let pr_subgoals_of_pfts pfts =
let close_cmd = Decl_mode.get_end_command pfts in
let gls = fst (Refiner.frontier (proof_of_pftreestate pfts)) in
@@ -360,6 +388,7 @@ let pr_open_subgoals () =
if List.length gls < 2 then
pr_subgoal n gls
else
+ (* LEM TODO: this way of saying how many subgoals has to be abstracted out*)
v 0 (int(List.length gls) ++ str" subgoals" ++ cut () ++
pr_subgoal n gls)
diff --git a/parsing/printer.mli b/parsing/printer.mli
index 580eec8dc..00cf4984d 100644
--- a/parsing/printer.mli
+++ b/parsing/printer.mli
@@ -107,3 +107,13 @@ val emacs_str : string -> string -> string
(* Backwards compatibility *)
val prterm : constr -> std_ppcmds (* = pr_lconstr *)
+
+type printer_pr = {
+ pr_subgoals : string option -> evar_map -> goal list -> std_ppcmds;
+ pr_subgoal : int -> goal list -> std_ppcmds;
+ pr_goal : goal -> std_ppcmds;
+};;
+
+val set_printer_pr : printer_pr -> unit
+
+val default_printer_pr : printer_pr
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 4c24f3505..9d8bbcc00 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -44,8 +44,8 @@ type pcoq_hook = {
abort : string -> unit;
search : searchable -> dir_path list * bool -> unit;
print_name : reference -> unit;
- print_check : Environ.unsafe_judgment -> unit;
- print_eval : (constr -> constr) -> Environ.env -> constr_expr ->
+ print_check : Environ.env -> Environ.unsafe_judgment -> unit;
+ print_eval : Reductionops.reduction_function -> Environ.env -> Evd.evar_map -> constr_expr ->
Environ.unsafe_judgment -> unit;
show_goal : int option -> unit
}
@@ -888,13 +888,13 @@ let vernac_check_may_eval redexp glopt rc =
let j = Typeops.typing env c in
match redexp with
| None ->
- if !pcoq <> None then (out_some !pcoq).print_check j
+ if !pcoq <> None then (out_some !pcoq).print_check env j
else msg (print_judgment env j)
| Some r ->
let redfun = fst (reduction_of_red_expr (interp_redexp env evmap r)) in
if !pcoq <> None
- then (out_some !pcoq).print_eval (redfun env evmap) env rc j
- else msg (print_eval redfun env j)
+ then (out_some !pcoq).print_eval redfun env evmap rc j
+ else msg (print_eval redfun env evmap rc j)
(* The same but avoiding the current goal context if any *)
let vernac_global_check c =
diff --git a/toplevel/vernacentries.mli b/toplevel/vernacentries.mli
index e4e61c554..65464d4e2 100644
--- a/toplevel/vernacentries.mli
+++ b/toplevel/vernacentries.mli
@@ -39,8 +39,9 @@ type pcoq_hook = {
abort : string -> unit;
search : searchable -> dir_path list * bool -> unit;
print_name : Libnames.reference -> unit;
- print_check : Environ.unsafe_judgment -> unit;
- print_eval : (constr -> constr) -> Environ.env -> constr_expr -> Environ.unsafe_judgment -> unit;
+ print_check : Environ.env -> Environ.unsafe_judgment -> unit;
+ print_eval : Reductionops.reduction_function -> Environ.env -> Evd.evar_map -> constr_expr ->
+ Environ.unsafe_judgment -> unit;
show_goal : int option -> unit
}
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-13 09:29:39 +0000