From d14df293d2696f00a8de137bea9fe3a89e0bdeb0 Mon Sep 17 00:00:00 2001 From: letouzey Date: Wed, 19 Dec 2001 11:42:11 +0000 Subject: reparation du make depend et du .depend git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2334 85f007b7-540e-0410-9357-904b9bb8a0f7 --- .depend | 113 ++-- .depend.camlp4 | 7 + Makefile | 74 +-- contrib/interface/dad.ml | 358 ------------- contrib/interface/dad.ml4 | 358 +++++++++++++ contrib/interface/line_parser.ml | 235 --------- contrib/interface/line_parser.ml4 | 235 +++++++++ contrib/xml/xml.ml | 80 --- contrib/xml/xml.ml4 | 80 +++ contrib/xml/xmlcommand.ml | 1037 ------------------------------------- contrib/xml/xmlcommand.ml4 | 1037 +++++++++++++++++++++++++++++++++++++ lib/pp.ml | 222 -------- lib/pp.ml4 | 222 ++++++++ tools/coq-tex.ml | 274 ---------- tools/coq-tex.ml4 | 274 ++++++++++ tools/coq_makefile.ml | 430 --------------- tools/coq_makefile.ml4 | 430 +++++++++++++++ 17 files changed, 2746 insertions(+), 2720 deletions(-) delete mode 100644 contrib/interface/dad.ml create mode 100644 contrib/interface/dad.ml4 delete mode 100755 contrib/interface/line_parser.ml create mode 100755 contrib/interface/line_parser.ml4 delete mode 100644 contrib/xml/xml.ml create mode 100644 contrib/xml/xml.ml4 delete mode 100644 contrib/xml/xmlcommand.ml create mode 100644 contrib/xml/xmlcommand.ml4 delete mode 100644 lib/pp.ml create mode 100644 lib/pp.ml4 delete mode 100644 tools/coq-tex.ml create mode 100644 tools/coq-tex.ml4 delete mode 100644 tools/coq_makefile.ml create mode 100644 tools/coq_makefile.ml4 diff --git a/.depend b/.depend index 90fbac0d03..c92f200882 100644 --- a/.depend +++ b/.depend @@ -25,6 +25,8 @@ kernel/typeops.cmi: kernel/environ.cmi kernel/names.cmi kernel/sign.cmi \ kernel/term.cmi kernel/univ.cmi kernel/univ.cmi: kernel/names.cmi lib/pp.cmi lib/pp.cmi: lib/pp_control.cmi +lib/system.cmi: lib/pp.cmi +lib/util.cmi: lib/pp.cmi library/declare.cmi: kernel/cooking.cmi kernel/declarations.cmi \ kernel/environ.cmi kernel/indtypes.cmi library/libobject.cmi \ library/library.cmi kernel/names.cmi library/nametab.cmi \ @@ -45,8 +47,6 @@ library/nameops.cmi: kernel/environ.cmi kernel/names.cmi lib/pp.cmi \ library/nametab.cmi: kernel/environ.cmi kernel/names.cmi lib/pp.cmi \ lib/util.cmi library/summary.cmi: kernel/names.cmi -lib/system.cmi: lib/pp.cmi -lib/util.cmi: lib/pp.cmi parsing/ast.cmi: parsing/coqast.cmi lib/dyn.cmi kernel/names.cmi \ parsing/pcoq.cmi lib/pp.cmi parsing/astterm.cmi: parsing/coqast.cmi kernel/environ.cmi pretyping/evd.cmi \ @@ -225,18 +225,18 @@ toplevel/recordobj.cmi: library/nametab.cmi toplevel/searchisos.cmi: library/libobject.cmi kernel/names.cmi \ kernel/term.cmi toplevel/toplevel.cmi: parsing/pcoq.cmi lib/pp.cmi +toplevel/vernac.cmi: parsing/coqast.cmi parsing/pcoq.cmi toplevel/vernacentries.cmi: kernel/environ.cmi pretyping/evd.cmi \ kernel/names.cmi kernel/term.cmi toplevel/vernacinterp.cmi toplevel/vernacinterp.cmi: parsing/coqast.cmi lib/dyn.cmi kernel/names.cmi \ library/nametab.cmi proofs/proof_type.cmi -toplevel/vernac.cmi: parsing/coqast.cmi parsing/pcoq.cmi contrib/correctness/past.cmi: parsing/coqast.cmi kernel/names.cmi \ contrib/correctness/ptype.cmi kernel/term.cmi +contrib/correctness/pcic.cmi: contrib/correctness/past.cmi \ + pretyping/rawterm.cmi contrib/correctness/pcicenv.cmi: kernel/names.cmi \ contrib/correctness/penv.cmi contrib/correctness/prename.cmi \ kernel/sign.cmi kernel/term.cmi -contrib/correctness/pcic.cmi: contrib/correctness/past.cmi \ - pretyping/rawterm.cmi contrib/correctness/pdb.cmi: kernel/names.cmi contrib/correctness/past.cmi \ contrib/correctness/ptype.cmi contrib/correctness/peffect.cmi: kernel/names.cmi lib/pp.cmi @@ -427,24 +427,32 @@ lib/edit.cmo: lib/bstack.cmi lib/pp.cmi lib/util.cmi lib/edit.cmi lib/edit.cmx: lib/bstack.cmx lib/pp.cmx lib/util.cmx lib/edit.cmi lib/explore.cmo: lib/explore.cmi lib/explore.cmx: lib/explore.cmi -lib/gmapl.cmo: lib/gmap.cmi lib/util.cmi lib/gmapl.cmi -lib/gmapl.cmx: lib/gmap.cmx lib/util.cmx lib/gmapl.cmi lib/gmap.cmo: lib/gmap.cmi lib/gmap.cmx: lib/gmap.cmi +lib/gmapl.cmo: lib/gmap.cmi lib/util.cmi lib/gmapl.cmi +lib/gmapl.cmx: lib/gmap.cmx lib/util.cmx lib/gmapl.cmi lib/gset.cmo: lib/gset.cmi lib/gset.cmx: lib/gset.cmi lib/hashcons.cmo: lib/hashcons.cmi lib/hashcons.cmx: lib/hashcons.cmi lib/options.cmo: lib/util.cmi lib/options.cmi lib/options.cmx: lib/util.cmx lib/options.cmi -lib/pp_control.cmo: lib/pp_control.cmi -lib/pp_control.cmx: lib/pp_control.cmi lib/pp.cmo: lib/pp_control.cmi lib/pp.cmi lib/pp.cmx: lib/pp_control.cmx lib/pp.cmi +lib/pp_control.cmo: lib/pp_control.cmi +lib/pp_control.cmx: lib/pp_control.cmi lib/predicate.cmo: lib/predicate.cmi lib/predicate.cmx: lib/predicate.cmi lib/profile.cmo: lib/profile.cmi lib/profile.cmx: lib/profile.cmi +lib/stamps.cmo: lib/stamps.cmi +lib/stamps.cmx: lib/stamps.cmi +lib/system.cmo: config/coq_config.cmi lib/pp.cmi lib/util.cmi lib/system.cmi +lib/system.cmx: config/coq_config.cmx lib/pp.cmx lib/util.cmx lib/system.cmi +lib/tlm.cmo: lib/gmap.cmi lib/gset.cmi lib/tlm.cmi +lib/tlm.cmx: lib/gmap.cmx lib/gset.cmx lib/tlm.cmi +lib/util.cmo: lib/pp.cmi lib/util.cmi +lib/util.cmx: lib/pp.cmx lib/util.cmi library/declare.cmo: kernel/declarations.cmi kernel/environ.cmi \ library/global.cmi library/impargs.cmi kernel/indtypes.cmi \ kernel/inductive.cmi library/lib.cmi library/libobject.cmi \ @@ -521,14 +529,6 @@ library/summary.cmo: lib/dyn.cmi kernel/names.cmi lib/pp.cmi lib/util.cmi \ library/summary.cmi library/summary.cmx: lib/dyn.cmx kernel/names.cmx lib/pp.cmx lib/util.cmx \ library/summary.cmi -lib/stamps.cmo: lib/stamps.cmi -lib/stamps.cmx: lib/stamps.cmi -lib/system.cmo: config/coq_config.cmi lib/pp.cmi lib/util.cmi lib/system.cmi -lib/system.cmx: config/coq_config.cmx lib/pp.cmx lib/util.cmx lib/system.cmi -lib/tlm.cmo: lib/gmap.cmi lib/gset.cmi lib/tlm.cmi -lib/tlm.cmx: lib/gmap.cmx lib/gset.cmx lib/tlm.cmi -lib/util.cmo: lib/pp.cmi lib/util.cmi -lib/util.cmx: lib/pp.cmx lib/util.cmi parsing/ast.cmo: parsing/coqast.cmi lib/dyn.cmi kernel/names.cmi \ parsing/pcoq.cmi lib/pp.cmi lib/util.cmi parsing/ast.cmi parsing/ast.cmx: parsing/coqast.cmx lib/dyn.cmx kernel/names.cmx \ @@ -1345,12 +1345,12 @@ tactics/wcclausenv.cmx: proofs/clenv.cmx kernel/environ.cmx \ proofs/proof_trees.cmx pretyping/reductionops.cmx kernel/sign.cmx \ proofs/tacmach.cmx kernel/term.cmx pretyping/termops.cmx lib/util.cmx \ tactics/wcclausenv.cmi -tools/coqdep_lexer.cmo: config/coq_config.cmi -tools/coqdep_lexer.cmx: config/coq_config.cmx -tools/coqdep.cmo: config/coq_config.cmi tools/coqdep_lexer.cmo -tools/coqdep.cmx: config/coq_config.cmx tools/coqdep_lexer.cmx tools/coq_vo2xml.cmo: config/coq_config.cmi toplevel/usage.cmi tools/coq_vo2xml.cmx: config/coq_config.cmx toplevel/usage.cmx +tools/coqdep.cmo: config/coq_config.cmi tools/coqdep_lexer.cmo +tools/coqdep.cmx: config/coq_config.cmx tools/coqdep_lexer.cmx +tools/coqdep_lexer.cmo: config/coq_config.cmi +tools/coqdep_lexer.cmx: config/coq_config.cmx tools/gallina.cmo: tools/gallina_lexer.cmo tools/gallina.cmx: tools/gallina_lexer.cmx toplevel/class.cmo: pretyping/classops.cmi kernel/declarations.cmi \ @@ -1531,6 +1531,16 @@ toplevel/toplevel.cmx: parsing/ast.cmx toplevel/errors.cmx library/lib.cmx \ toplevel/vernac.cmx toplevel/vernacinterp.cmx toplevel/toplevel.cmi toplevel/usage.cmo: config/coq_config.cmi toplevel/usage.cmi toplevel/usage.cmx: config/coq_config.cmx toplevel/usage.cmi +toplevel/vernac.cmo: parsing/ast.cmi parsing/coqast.cmi library/lib.cmi \ + library/library.cmi library/nameops.cmi kernel/names.cmi lib/options.cmi \ + parsing/pcoq.cmi lib/pp.cmi library/states.cmi lib/system.cmi \ + pretyping/termops.cmi lib/util.cmi toplevel/vernacinterp.cmi \ + toplevel/vernac.cmi +toplevel/vernac.cmx: parsing/ast.cmx parsing/coqast.cmx library/lib.cmx \ + library/library.cmx library/nameops.cmx kernel/names.cmx lib/options.cmx \ + parsing/pcoq.cmx lib/pp.cmx library/states.cmx lib/system.cmx \ + pretyping/termops.cmx lib/util.cmx toplevel/vernacinterp.cmx \ + toplevel/vernac.cmi toplevel/vernacentries.cmo: parsing/ast.cmi parsing/astterm.cmi \ toplevel/class.cmi pretyping/classops.cmi toplevel/command.cmi \ parsing/coqast.cmi kernel/declarations.cmi library/declare.cmi \ @@ -1575,28 +1585,6 @@ toplevel/vernacinterp.cmx: parsing/ast.cmx parsing/astterm.cmx \ kernel/names.cmx library/nametab.cmx lib/options.cmx lib/pp.cmx \ proofs/proof_type.cmx proofs/tacinterp.cmx lib/util.cmx \ toplevel/vernacinterp.cmi -toplevel/vernac.cmo: parsing/ast.cmi parsing/coqast.cmi library/lib.cmi \ - library/library.cmi library/nameops.cmi kernel/names.cmi lib/options.cmi \ - parsing/pcoq.cmi lib/pp.cmi library/states.cmi lib/system.cmi \ - pretyping/termops.cmi lib/util.cmi toplevel/vernacinterp.cmi \ - toplevel/vernac.cmi -toplevel/vernac.cmx: parsing/ast.cmx parsing/coqast.cmx library/lib.cmx \ - library/library.cmx library/nameops.cmx kernel/names.cmx lib/options.cmx \ - parsing/pcoq.cmx lib/pp.cmx library/states.cmx lib/system.cmx \ - pretyping/termops.cmx lib/util.cmx toplevel/vernacinterp.cmx \ - toplevel/vernac.cmi -contrib/correctness/pcicenv.cmo: library/global.cmi kernel/names.cmi \ - contrib/correctness/past.cmi contrib/correctness/penv.cmi \ - contrib/correctness/pmisc.cmi contrib/correctness/pmonad.cmi \ - contrib/correctness/prename.cmi contrib/correctness/ptype.cmi \ - contrib/correctness/putil.cmi kernel/sign.cmi kernel/term.cmi \ - kernel/univ.cmi contrib/correctness/pcicenv.cmi -contrib/correctness/pcicenv.cmx: library/global.cmx kernel/names.cmx \ - contrib/correctness/past.cmi contrib/correctness/penv.cmx \ - contrib/correctness/pmisc.cmx contrib/correctness/pmonad.cmx \ - contrib/correctness/prename.cmx contrib/correctness/ptype.cmi \ - contrib/correctness/putil.cmx kernel/sign.cmx kernel/term.cmx \ - kernel/univ.cmx contrib/correctness/pcicenv.cmi contrib/correctness/pcic.cmo: parsing/ast.cmi kernel/declarations.cmi \ library/declare.cmi pretyping/detyping.cmi kernel/indtypes.cmi \ kernel/names.cmi library/nametab.cmi contrib/correctness/past.cmi \ @@ -1609,6 +1597,18 @@ contrib/correctness/pcic.cmx: parsing/ast.cmx kernel/declarations.cmx \ contrib/correctness/pmisc.cmx pretyping/rawterm.cmx toplevel/record.cmx \ kernel/sign.cmx kernel/term.cmx pretyping/termops.cmx kernel/typeops.cmx \ lib/util.cmx contrib/correctness/pcic.cmi +contrib/correctness/pcicenv.cmo: library/global.cmi kernel/names.cmi \ + contrib/correctness/past.cmi contrib/correctness/penv.cmi \ + contrib/correctness/pmisc.cmi contrib/correctness/pmonad.cmi \ + contrib/correctness/prename.cmi contrib/correctness/ptype.cmi \ + contrib/correctness/putil.cmi kernel/sign.cmi kernel/term.cmi \ + kernel/univ.cmi contrib/correctness/pcicenv.cmi +contrib/correctness/pcicenv.cmx: library/global.cmx kernel/names.cmx \ + contrib/correctness/past.cmi contrib/correctness/penv.cmx \ + contrib/correctness/pmisc.cmx contrib/correctness/pmonad.cmx \ + contrib/correctness/prename.cmx contrib/correctness/ptype.cmi \ + contrib/correctness/putil.cmx kernel/sign.cmx kernel/term.cmx \ + kernel/univ.cmx contrib/correctness/pcicenv.cmi contrib/correctness/pdb.cmo: library/declare.cmi library/global.cmi \ kernel/names.cmi library/nametab.cmi contrib/correctness/past.cmi \ contrib/correctness/peffect.cmi contrib/correctness/penv.cmi \ @@ -2081,14 +2081,6 @@ contrib/interface/pbp.cmx: parsing/astterm.cmx parsing/coqlib.cmx \ kernel/reduction.cmx proofs/tacinterp.cmx proofs/tacmach.cmx \ tactics/tacticals.cmx tactics/tactics.cmx kernel/term.cmx \ pretyping/typing.cmx lib/util.cmx contrib/interface/pbp.cmi -contrib/interface/showproof_ct.cmo: contrib/interface/ascent.cmi \ - parsing/esyntax.cmi library/global.cmi toplevel/metasyntax.cmi lib/pp.cmi \ - parsing/printer.cmi contrib/interface/translate.cmi \ - contrib/interface/vtp.cmi contrib/interface/xlate.cmi -contrib/interface/showproof_ct.cmx: contrib/interface/ascent.cmi \ - parsing/esyntax.cmx library/global.cmx toplevel/metasyntax.cmx lib/pp.cmx \ - parsing/printer.cmx contrib/interface/translate.cmx \ - contrib/interface/vtp.cmx contrib/interface/xlate.cmx contrib/interface/showproof.cmo: parsing/ast.cmi parsing/astterm.cmi \ proofs/clenv.cmi parsing/coqast.cmi kernel/declarations.cmi \ kernel/environ.cmi pretyping/evd.cmi library/global.cmi \ @@ -2109,6 +2101,14 @@ contrib/interface/showproof.cmx: parsing/ast.cmx parsing/astterm.cmx \ kernel/term.cmx parsing/termast.cmx pretyping/termops.cmx \ contrib/interface/translate.cmx pretyping/typing.cmx lib/util.cmx \ toplevel/vernacinterp.cmx contrib/interface/showproof.cmi +contrib/interface/showproof_ct.cmo: contrib/interface/ascent.cmi \ + parsing/esyntax.cmi library/global.cmi toplevel/metasyntax.cmi lib/pp.cmi \ + parsing/printer.cmi contrib/interface/translate.cmi \ + contrib/interface/vtp.cmi contrib/interface/xlate.cmi +contrib/interface/showproof_ct.cmx: contrib/interface/ascent.cmi \ + parsing/esyntax.cmx library/global.cmx toplevel/metasyntax.cmx lib/pp.cmx \ + parsing/printer.cmx contrib/interface/translate.cmx \ + contrib/interface/vtp.cmx contrib/interface/xlate.cmx contrib/interface/translate.cmo: contrib/interface/ascent.cmi parsing/ast.cmi \ contrib/interface/ctast.cmo kernel/environ.cmi pretyping/evarutil.cmi \ pretyping/evd.cmi library/libobject.cmi library/library.cmi \ @@ -2205,6 +2205,8 @@ contrib/romega/refl_omega.cmx: parsing/ast.cmx tactics/auto.cmx \ parsing/printer.cmx proofs/proof_type.cmx kernel/reduction.cmx \ kernel/sign.cmx proofs/tacmach.cmx tactics/tacticals.cmx \ tactics/tactics.cmx kernel/term.cmx lib/util.cmx +contrib/xml/xml.cmo: contrib/xml/xml.cmi +contrib/xml/xml.cmx: contrib/xml/xml.cmi contrib/xml/xmlcommand.cmo: kernel/declarations.cmi library/declare.cmi \ kernel/environ.cmi pretyping/evd.cmi library/global.cmi library/lib.cmi \ library/libobject.cmi library/library.cmi library/nameops.cmi \ @@ -2225,8 +2227,6 @@ contrib/xml/xmlentries.cmo: lib/util.cmi toplevel/vernacinterp.cmi \ contrib/xml/xmlcommand.cmi contrib/xml/xmlentries.cmx: lib/util.cmx toplevel/vernacinterp.cmx \ contrib/xml/xmlcommand.cmx -contrib/xml/xml.cmo: contrib/xml/xml.cmi -contrib/xml/xml.cmx: contrib/xml/xml.cmi tactics/tauto.cmo: parsing/grammar.cma kernel/names.cmo parsing/ast.cmo parsing/g_tactic.cmo parsing/g_ltac.cmo parsing/g_constr.cmo contrib/correctness/psyntax.cmo: parsing/grammar.cma contrib/field/field.cmo: parsing/grammar.cma kernel/names.cmo parsing/ast.cmo parsing/g_tactic.cmo parsing/g_ltac.cmo parsing/g_constr.cmo @@ -2244,3 +2244,10 @@ parsing/g_tactic.cmo: parsing/grammar.cma parsing/g_ltac.cmo: parsing/grammar.cma parsing/extend.cmo: parsing/grammar.cma toplevel/mltop.cmo: +lib/pp.cmo: +contrib/xml/xml.cmo: +contrib/xml/xmlcommand.cmo: +contrib/interface/dad.cmo: +contrib/interface/line_parser.cmo: +tools/coq_makefile.cmo: +tools/coq-tex.cmo: diff --git a/.depend.camlp4 b/.depend.camlp4 index ac3ad8320d..6064e6a838 100644 --- a/.depend.camlp4 +++ b/.depend.camlp4 @@ -15,3 +15,10 @@ parsing/g_tactic.ml: parsing/grammar.cma parsing/g_ltac.ml: parsing/grammar.cma parsing/extend.ml: parsing/grammar.cma toplevel/mltop.ml: +lib/pp.ml: +contrib/xml/xml.ml: +contrib/xml/xmlcommand.ml: +contrib/interface/dad.ml: +contrib/interface/line_parser.ml: +tools/coq_makefile.ml: +tools/coq-tex.ml: diff --git a/Makefile b/Makefile index b9b99fceb4..8771465bf8 100644 --- a/Makefile +++ b/Makefile @@ -761,13 +761,7 @@ ML4FILES += toplevel/mltop.ml4 clean:: rm -f toplevel/mltop.byteml toplevel/mltop.optml -# files compiled with camlp4 because of streams syntax - -lib/pp.cmo: lib/pp.ml - $(OCAMLC) -pp camlp4o $(BYTEFLAGS) -c $< - -lib/pp.cmx: lib/pp.ml - $(OCAMLOPT) -pp camlp4o $(OPTFLAGS) -c $< +# files compiled with -rectypes kernel/term.cmo: kernel/term.ml $(OCAMLC) -rectypes $(BYTEFLAGS) -c $< @@ -781,41 +775,59 @@ library/nametab.cmo: library/nametab.ml library/nametab.cmx: library/nametab.ml $(OCAMLOPT) -rectypes $(OPTFLAGS) -c $< -contrib/xml/xml.cmo: contrib/xml/xml.ml - $(OCAMLC) -pp camlp4o $(BYTEFLAGS) -c $< +# files compiled with camlp4 because of streams syntax + +#lib/pp.cmo: lib/pp.ml +# $(OCAMLC) $(BYTEFLAGS) -c $< + +#lib/pp.cmx: lib/pp.ml +# $(OCAMLOPT_P4O) -c $< + +#contrib/xml/xml.cmo: contrib/xml/xml.ml4 +# $(OCAMLC_P4O) -c $< + +#contrib/xml/xml.cmx: contrib/xml/xml.ml4 +# $(OCAMLOPT_P4O) -c $< + +#contrib/xml/xmlcommand.cmo: contrib/xml/xmlcommand.ml4 +# $(OCAMLC_P4O) -c $< + +#contrib/xml/xmlcommand.cmx: contrib/xml/xmlcommand.ml4 +# $(OCAMLOPT_P4O) -c $< -contrib/xml/xml.cmx: contrib/xml/xml.ml - $(OCAMLOPT) -pp camlp4o $(OPTFLAGS) -c $< +#contrib/interface/dad.cmo: contrib/interface/dad.ml4 +# $(OCAMLC_P4O) -c $< -contrib/xml/xmlcommand.cmo: contrib/xml/xmlcommand.ml - $(OCAMLC) -pp camlp4o $(BYTEFLAGS) -c $< +#contrib/interface/dad.cmx: contrib/interface/dad.ml4 +# $(OCAMLOPT_P4O) -c $< -contrib/xml/xmlcommand.cmx: contrib/xml/xmlcommand.ml - $(OCAMLOPT) -pp camlp4o $(OPTFLAGS) -c $< +#contrib/interface/line_parser.cmo: contrib/interface/line_parser.ml4 +# $(OCAMLC_P4O) -c $< -contrib/interface/dad.cmo: contrib/interface/dad.ml - $(OCAMLC) -pp camlp4o $(BYTEFLAGS) -c $< +#contrib/interface/line_parser.cmx: contrib/interface/line_parser.ml4 +# $(OCAMLOPT_P4O) -c $< -contrib/interface/dad.cmx: contrib/interface/dad.ml - $(OCAMLOPT) -pp camlp4o $(OPTFLAGS) -c $< +#tools/coq_makefile.cmo: tools/coq_makefile.ml4 +# $(OCAMLC_P4O) -c $< -contrib/interface/line_parser.cmo: contrib/interface/line_parser.ml - $(OCAMLC) -pp camlp4o $(BYTEFLAGS) -c $< +#tools/coq_makefile.cmx: tools/coq_makefile.ml4 +# $(OCAMLOPT_P4O) -c $< -contrib/interface/line_parser.cmx: contrib/interface/line_parser.ml - $(OCAMLOPT) -pp camlp4o $(OPTFLAGS) -c $< +#tools/coq-tex.cmo: tools/coq-tex.ml4 +# $(OCAMLC_P4O) -c $< -tools/coq_makefile.cmo: tools/coq_makefile.ml - $(OCAMLC) -pp camlp4o $(BYTEFLAGS) -c $< +#tools/coq-tex.cmx: tools/coq-tex.ml4 +# $(OCAMLOPT_P4O) -c $< -tools/coq_makefile.cmx: tools/coq_makefile.ml - $(OCAMLOPT) -pp camlp4o $(OPTFLAGS) -c $< +ML4FILES += lib/pp.ml4 \ + contrib/xml/xml.ml4 \ + contrib/xml/xmlcommand.ml4 \ + contrib/interface/dad.ml4 \ + contrib/interface/line_parser.ml4 \ + tools/coq_makefile.ml4 \ + tools/coq-tex.ml4 -tools/coq-tex.cmo: tools/coq-tex.ml - $(OCAMLC) -pp camlp4o $(BYTEFLAGS) -c $< -tools/coq-tex.cmx: tools/coq-tex.ml - $(OCAMLOPT) -pp camlp4o $(OPTFLAGS) -c $< ########################################################################### # Default rules diff --git a/contrib/interface/dad.ml b/contrib/interface/dad.ml deleted file mode 100644 index ce38174044..0000000000 --- a/contrib/interface/dad.ml +++ /dev/null @@ -1,358 +0,0 @@ -(* This file contains an ml version of drag-and-drop. *) - -(* #use "/net/home/bertot/experiments/pcoq/src/dad/dad.ml" *) - -open Names;; -open Term;; -open Rawterm;; -open Util;; -open Environ;; -open Tactics;; -open Tacticals;; -open Pattern;; -open Reduction;; -open Ctast;; -open Termast;; -open Astterm;; -open Vernacinterp;; -open Nametab - -open Proof_type;; -open Proof_trees;; -open Tacmach;; -open Typing;; -open Pp;; - -open Paths;; - -(* In a first approximation, drag-and-drop rules are like in CtCoq - 1/ a pattern, - 2,3/ Two paths: start and end positions, - 4/ the degree: the number of steps the algorithm should go up from the - longest common prefix, - 5/ the tail path: the suffix of the longest common prefix of length the - degree, - 6/ the command pattern, where meta variables are represented by objects - of the form Node(_,"META"; [Num(_,i)]) -*) - - -type dad_rule = Ctast.t * int list * int list * int * int list * Ctast.t;; - -(* This value will be used systematically when constructing objects of - type Ctast.t, the value is stupid and meaningless, but it is needed - to construct well-typed terms. *) - -let zz = (0,0);; - -(* This function receives a length n, a path p, and a term and returns a - couple whose first component is the subterm designated by the prefix - of p of length n, and the second component is the rest of the path *) - -let rec get_subterm (depth:int) (path: int list) (constr:constr) = - match depth, path, kind_of_term constr with - 0, l, c -> (constr,l) - | n, 2::a::tl, App(func,arr) -> - get_subterm (n - 2) tl arr.(a-1) - | _,l,_ -> failwith (int_list_to_string - "wrong path or wrong form of term" - l);; - -(* This function maps a substitution on an abstract syntax tree. The - first argument, an object of type env, is necessary to - transform constr terms into abstract syntax trees. The second argument is - the substitution, a list of pairs linking an integer and a constr term. *) -let map_subst (env :env) - (subst:(int * Term.constr) list) = - let rec map_subst_aux = function - Node(_, "META", [Num(_, i)]) -> - let constr = List.assoc i subst in - Ctast.ast_to_ct (ast_of_constr false env constr) - | Node(loc, s, l) -> Node(loc, s, List.map map_subst_aux l) - | ast -> ast in - map_subst_aux;; - - -(* This function is really the one that is important. *) -let rec find_cmd (l:(string * dad_rule) list) env constr p p1 p2 = - match l with - [] -> failwith "nothing happens" - | (name, (pat, p_f, p_l, deg, p_r, cmd))::tl -> - let length = List.length p in - try - if deg > length then - failwith "internal" - else - let term_to_match, p_r = - try - get_subterm (length - deg) p constr - with - Failure s -> failwith "internal" in - let _, constr_pat = - interp_constrpattern Evd.empty (Global.env()) - (ct_to_ast pat) in - let subst = matches constr_pat term_to_match in - if (is_prefix p_f (p_r@p1)) & (is_prefix p_l (p_r@p2)) then - map_subst env subst cmd - else - failwith "internal" - with - Failure "internal" -> find_cmd tl env constr p p1 p2 - | PatternMatchingFailure -> find_cmd tl env constr p p1 p2;; - - -let dad_rule_list = ref ([]: (string * dad_rule) list);; - - -(* \\ This function is also used in pbp. *) -let rec tactic_args_to_ints = function - [] -> [] - | (Integer n)::l -> n::(tactic_args_to_ints l) - | _ -> failwith "expecting only numbers";; - -(* We assume that the two lists of integers for the tactic are simply - given in one list, separated by a dummy tactic. *) -let rec part_tac_args l = function - [] -> l,[] - | (Tacexp a)::tl -> l, (tactic_args_to_ints tl) - | (Integer n)::tl -> part_tac_args (n::l) tl - | _ -> failwith "expecting only numbers and the word \"to\"";; - - -(* The dad_tac tactic takes a display_function as argument. This makes - it possible to use it in pcoq, but also in other contexts, just by - changing the output routine. *) -let dad_tac display_function = function - l -> let p1, p2 = part_tac_args [] l in - (function g -> - let (p_a, p1prime, p2prime) = decompose_path (List.rev p1,p2) in - (display_function - (find_cmd (!dad_rule_list) (pf_env g) - (pf_concl g) p_a p1prime p2prime)); - tclIDTAC g);; - -(* Now we enter dad rule list management. *) - -let add_dad_rule name patt p1 p2 depth pr command = - dad_rule_list := (name, - (patt, p1, p2, depth, pr, command))::!dad_rule_list;; - -let rec remove_if_exists name = function - [] -> false, [] - | ((a,b) as rule1)::tl -> if a = name then - let result1, l = (remove_if_exists name tl) in - true, l - else - let result1, l = remove_if_exists name tl in - result1, (rule1::l);; - -let remove_dad_rule name = - let result1, result2 = remove_if_exists name !dad_rule_list in - if result1 then - failwith("No such name among the drag and drop rules " ^ name) - else - dad_rule_list := result2;; - -let dad_rule_names () = - List.map (function (s,_) -> s) !dad_rule_list;; - -(* this function is inspired from matches_core in pattern.ml *) -let constrain ((n : int),(pat : constr_pattern)) sigma = - if List.mem_assoc n sigma then - if pat = (List.assoc n sigma) then sigma - else failwith "internal" - else - (n,pat)::sigma - -(* This function is inspired from matches_core in pattern.ml *) -let more_general_pat pat1 pat2 = - let rec match_rec sigma p1 p2 = - match p1, p2 with - | PMeta (Some n), m -> constrain (n,m) sigma - - | PMeta None, m -> sigma - - | PRef (VarRef sp1), PRef(VarRef sp2) when sp1 = sp2 -> sigma - - | PVar v1, PVar v2 when v1 = v2 -> sigma - - | PRef ref1, PRef ref2 when ref1 = ref2 -> sigma - - | PRel n1, PRel n2 when n1 = n2 -> sigma - - | PSort (RProp c1), PSort (RProp c2) when c1 = c2 -> sigma - - | PSort (RType _), PSort (RType _) -> sigma - - | PApp (c1,arg1), PApp (c2,arg2) -> - (try array_fold_left2 match_rec (match_rec sigma c1 c2) arg1 arg2 - with Invalid_argument _ -> failwith "internal") - | _ -> failwith "unexpected case in more_general_pat" in - try let _ = match_rec [] pat1 pat2 in true - with Failure "internal" -> false;; - -let more_general r1 r2 = - match r1,r2 with - (_,(patt1,p11,p12,_,_,_)), - (_,(patt2,p21,p22,_,_,_)) -> - (more_general_pat patt1 patt2) & - (is_prefix p11 p21) & (is_prefix p12 p22);; - -let not_less_general r1 r2 = - not (match r1,r2 with - (_,(patt1,p11,p12,_,_,_)), - (_,(patt2,p21,p22,_,_,_)) -> - (more_general_pat patt1 patt2) & - (is_prefix p21 p11) & (is_prefix p22 p12));; - -let rec add_in_list_sorting rule1 = function - [] -> [rule1] - | (b::tl) as this_list -> - if more_general rule1 b then - b::(add_in_list_sorting rule1 tl) - else if not_less_general rule1 b then - let tl2 = add_in_list_sorting_aux rule1 tl in - (match tl2 with - [] -> rule1::this_list - | _ -> b::tl2) - else - rule1::this_list -and add_in_list_sorting_aux rule1 = function - [] -> [] - | b::tl -> - if more_general rule1 b then - b::(add_in_list_sorting rule1 tl) - else - let tl2 = add_in_list_sorting_aux rule1 tl in - (match tl2 with - [] -> [] - | _ -> rule1::tl2);; - -let rec sort_list = function - [] -> [] - | a::l -> add_in_list_sorting a (sort_list l);; - -let mk_dad_meta n = Node(zz,"META",[Num(zz, n)]);; -let mk_rewrite1 ast = - Node(zz,"TACTICLIST", - [Node(zz,"RewriteLR", - [Node(zz, "COMMAND", ast);Node(zz,"BINDINGS",[])])]);; - -let mk_rewrite2 ast = - Node(zz,"TACTICLIST", - [Node(zz,"RewriteRL", - [Node(zz, "COMMAND", ast);Node(zz,"BINDINGS",[])])]);; - - - -let start_dad () = -vinterp_add "AddDadRule" - (function - | [VARG_STRING name; VARG_CONSTR pat; VARG_NUMBERLIST p1; - VARG_NUMBERLIST p2; VARG_TACTIC com] -> - (function () -> - let pr = match decompose_path (p1, p2) with pr, _, _ -> pr in - (add_dad_rule name (Ctast.ast_to_ct pat) p1 p2 (List.length pr) pr (Ctast.ast_to_ct com))) - | _ -> errorlabstrm "AddDadRule1" - [< str "AddDadRule2">]); -add_dad_rule "distributivity-inv" -(Node(zz,"APPLIST",[Nvar(zz,"mult");Node(zz,"APPLIST",[Nvar(zz,"plus");Node(zz,"META",[Num(zz,4)]);Node(zz,"META",[Num(zz,3)])]);Node(zz,"META",[Num(zz,2)])])) -[2; 2] -[2; 1] -1 -[2] -(mk_rewrite1 ([Node(zz, "APPLIST", [Nvar(zz, "mult_plus_distr");(mk_dad_meta 4) ;(mk_dad_meta 3) ;(mk_dad_meta 2) ])])); - -add_dad_rule "distributivity1-r" -(Node(zz,"APPLIST",[Nvar(zz,"plus");Node(zz,"APPLIST",[Nvar(zz,"mult");Node(zz,"META",[Num(zz,4)]);Node(zz,"META",[Num(zz,2)])]);Node(zz,"APPLIST",[Nvar(zz,"mult");Node(zz,"META",[Num(zz,3)]);Node(zz,"META",[Num(zz,2)])])])) -[2; 2; 2; 2] -[] -0 -[] -(mk_rewrite2 ([Node(zz, "APPLIST", [Nvar(zz, "mult_plus_distr");(mk_dad_meta 4) ;(mk_dad_meta 3) ;(mk_dad_meta 2) ])])); - -add_dad_rule "distributivity1-l" -(Node(zz,"APPLIST",[Nvar(zz,"plus");Node(zz,"APPLIST",[Nvar(zz,"mult");Node(zz,"META",[Num(zz,4)]);Node(zz,"META",[Num(zz,2)])]);Node(zz,"APPLIST",[Nvar(zz,"mult");Node(zz,"META",[Num(zz,3)]);Node(zz,"META",[Num(zz,2)])])])) -[2; 1; 2; 2] -[] -0 -[] -(mk_rewrite2 ([Node(zz, "APPLIST", [Nvar(zz, "mult_plus_distr");(mk_dad_meta 4) ;(mk_dad_meta 3) ;(mk_dad_meta 2) ])])); - -add_dad_rule "associativity" -(Node(zz,"APPLIST",[Nvar(zz,"plus");Node(zz,"APPLIST",[Nvar(zz,"plus");Node(zz,"META",[Num(zz,4)]);Node(zz,"META",[Num(zz,3)])]);Node(zz,"META",[Num(zz,2)])])) -[2; 1] -[] -0 -[] -(mk_rewrite1 ([Node(zz, "APPLIST", [Nvar(zz, "plus_assoc_r");(mk_dad_meta 4) ;(mk_dad_meta 3) ;(mk_dad_meta 2) ])])); - -add_dad_rule "minus-identity-lr" -(Node(zz,"APPLIST",[Nvar(zz,"minus");Node(zz,"META",[Num(zz,2)]);Node(zz,"META",[Num(zz,2)])])) -[2; 1] -[2; 2] -1 -[2] -(mk_rewrite2 ([Node(zz, "APPLIST", [Nvar(zz, "minus_n_n");(mk_dad_meta 2) ])])); - -add_dad_rule "minus-identity-rl" -(Node(zz,"APPLIST",[Nvar(zz,"minus");Node(zz,"META",[Num(zz,2)]);Node(zz,"META",[Num(zz,2)])])) -[2; 2] -[2; 1] -1 -[2] -(mk_rewrite2 ([Node(zz, "APPLIST", [Nvar(zz, "minus_n_n");(mk_dad_meta 2) ])])); - -add_dad_rule "plus-sym-rl" -(Node(zz,"APPLIST",[Nvar(zz,"plus");Node(zz,"META",[Num(zz,3)]);Node(zz,"META",[Num(zz,2)])])) -[2; 2] -[2; 1] -1 -[2] -(mk_rewrite1 ([Node(zz, "APPLIST", [Nvar(zz, "plus_sym");(mk_dad_meta 3) ;(mk_dad_meta 2) ])])); - -add_dad_rule "plus-sym-lr" -(Node(zz,"APPLIST",[Nvar(zz,"plus");Node(zz,"META",[Num(zz,3)]);Node(zz,"META",[Num(zz,2)])])) -[2; 1] -[2; 2] -1 -[2] -(mk_rewrite1 ([Node(zz, "APPLIST", [Nvar(zz, "plus_sym");(mk_dad_meta 3) ;(mk_dad_meta 2) ])])); - -add_dad_rule "absorb-0-r-rl" -(Node(zz,"APPLIST",[Nvar(zz,"plus");Node(zz,"META",[Num(zz,2)]);Nvar(zz,"O")])) -[2; 2] -[1] -0 -[] -(mk_rewrite2 ([Node(zz, "APPLIST", [Nvar(zz, "plus_n_O");(mk_dad_meta 2) ])])); - -add_dad_rule "absorb-0-r-lr" -(Node(zz,"APPLIST",[Nvar(zz,"plus");Node(zz,"META",[Num(zz,2)]);Nvar(zz,"O")])) -[1] -[2; 2] -0 -[] -(mk_rewrite2 ([Node(zz, "APPLIST", [Nvar(zz, "plus_n_O");(mk_dad_meta 2) ])])); - -add_dad_rule "plus-permute-lr" -(Node(zz,"APPLIST",[Nvar(zz,"plus");Node(zz,"META",[Num(zz,4)]);Node(zz,"APPLIST",[Nvar(zz,"plus");Node(zz,"META",[Num(zz,3)]);Node(zz,"META",[Num(zz,2)])])])) -[2; 1] -[2; 2; 2; 1] -1 -[2] -(mk_rewrite1 ([Node(zz, "APPLIST", [Nvar(zz, "plus_permute");(mk_dad_meta 4) ;(mk_dad_meta 3) ;(mk_dad_meta 2) ])])); - -add_dad_rule "plus-permute-rl" -(Node(zz,"APPLIST",[Nvar(zz,"plus");Node(zz,"META",[Num(zz,4)]);Node(zz,"APPLIST",[Nvar(zz,"plus");Node(zz,"META",[Num(zz,3)]);Node(zz,"META",[Num(zz,2)])])])) -[2; 2; 2; 1] -[2; 1] -1 -[2] -(mk_rewrite1 ([Node(zz, "APPLIST", [Nvar(zz, "plus_permute");(mk_dad_meta 4) ;(mk_dad_meta 3) ;(mk_dad_meta 2) ])]));; - -vinterp_add "StartDad" - (function - | [] -> - (function () -> start_dad()) - | _ -> errorlabstrm "StartDad" [< >]);; diff --git a/contrib/interface/dad.ml4 b/contrib/interface/dad.ml4 new file mode 100644 index 0000000000..ce38174044 --- /dev/null +++ b/contrib/interface/dad.ml4 @@ -0,0 +1,358 @@ +(* This file contains an ml version of drag-and-drop. *) + +(* #use "/net/home/bertot/experiments/pcoq/src/dad/dad.ml" *) + +open Names;; +open Term;; +open Rawterm;; +open Util;; +open Environ;; +open Tactics;; +open Tacticals;; +open Pattern;; +open Reduction;; +open Ctast;; +open Termast;; +open Astterm;; +open Vernacinterp;; +open Nametab + +open Proof_type;; +open Proof_trees;; +open Tacmach;; +open Typing;; +open Pp;; + +open Paths;; + +(* In a first approximation, drag-and-drop rules are like in CtCoq + 1/ a pattern, + 2,3/ Two paths: start and end positions, + 4/ the degree: the number of steps the algorithm should go up from the + longest common prefix, + 5/ the tail path: the suffix of the longest common prefix of length the + degree, + 6/ the command pattern, where meta variables are represented by objects + of the form Node(_,"META"; [Num(_,i)]) +*) + + +type dad_rule = Ctast.t * int list * int list * int * int list * Ctast.t;; + +(* This value will be used systematically when constructing objects of + type Ctast.t, the value is stupid and meaningless, but it is needed + to construct well-typed terms. *) + +let zz = (0,0);; + +(* This function receives a length n, a path p, and a term and returns a + couple whose first component is the subterm designated by the prefix + of p of length n, and the second component is the rest of the path *) + +let rec get_subterm (depth:int) (path: int list) (constr:constr) = + match depth, path, kind_of_term constr with + 0, l, c -> (constr,l) + | n, 2::a::tl, App(func,arr) -> + get_subterm (n - 2) tl arr.(a-1) + | _,l,_ -> failwith (int_list_to_string + "wrong path or wrong form of term" + l);; + +(* This function maps a substitution on an abstract syntax tree. The + first argument, an object of type env, is necessary to + transform constr terms into abstract syntax trees. The second argument is + the substitution, a list of pairs linking an integer and a constr term. *) +let map_subst (env :env) + (subst:(int * Term.constr) list) = + let rec map_subst_aux = function + Node(_, "META", [Num(_, i)]) -> + let constr = List.assoc i subst in + Ctast.ast_to_ct (ast_of_constr false env constr) + | Node(loc, s, l) -> Node(loc, s, List.map map_subst_aux l) + | ast -> ast in + map_subst_aux;; + + +(* This function is really the one that is important. *) +let rec find_cmd (l:(string * dad_rule) list) env constr p p1 p2 = + match l with + [] -> failwith "nothing happens" + | (name, (pat, p_f, p_l, deg, p_r, cmd))::tl -> + let length = List.length p in + try + if deg > length then + failwith "internal" + else + let term_to_match, p_r = + try + get_subterm (length - deg) p constr + with + Failure s -> failwith "internal" in + let _, constr_pat = + interp_constrpattern Evd.empty (Global.env()) + (ct_to_ast pat) in + let subst = matches constr_pat term_to_match in + if (is_prefix p_f (p_r@p1)) & (is_prefix p_l (p_r@p2)) then + map_subst env subst cmd + else + failwith "internal" + with + Failure "internal" -> find_cmd tl env constr p p1 p2 + | PatternMatchingFailure -> find_cmd tl env constr p p1 p2;; + + +let dad_rule_list = ref ([]: (string * dad_rule) list);; + + +(* \\ This function is also used in pbp. *) +let rec tactic_args_to_ints = function + [] -> [] + | (Integer n)::l -> n::(tactic_args_to_ints l) + | _ -> failwith "expecting only numbers";; + +(* We assume that the two lists of integers for the tactic are simply + given in one list, separated by a dummy tactic. *) +let rec part_tac_args l = function + [] -> l,[] + | (Tacexp a)::tl -> l, (tactic_args_to_ints tl) + | (Integer n)::tl -> part_tac_args (n::l) tl + | _ -> failwith "expecting only numbers and the word \"to\"";; + + +(* The dad_tac tactic takes a display_function as argument. This makes + it possible to use it in pcoq, but also in other contexts, just by + changing the output routine. *) +let dad_tac display_function = function + l -> let p1, p2 = part_tac_args [] l in + (function g -> + let (p_a, p1prime, p2prime) = decompose_path (List.rev p1,p2) in + (display_function + (find_cmd (!dad_rule_list) (pf_env g) + (pf_concl g) p_a p1prime p2prime)); + tclIDTAC g);; + +(* Now we enter dad rule list management. *) + +let add_dad_rule name patt p1 p2 depth pr command = + dad_rule_list := (name, + (patt, p1, p2, depth, pr, command))::!dad_rule_list;; + +let rec remove_if_exists name = function + [] -> false, [] + | ((a,b) as rule1)::tl -> if a = name then + let result1, l = (remove_if_exists name tl) in + true, l + else + let result1, l = remove_if_exists name tl in + result1, (rule1::l);; + +let remove_dad_rule name = + let result1, result2 = remove_if_exists name !dad_rule_list in + if result1 then + failwith("No such name among the drag and drop rules " ^ name) + else + dad_rule_list := result2;; + +let dad_rule_names () = + List.map (function (s,_) -> s) !dad_rule_list;; + +(* this function is inspired from matches_core in pattern.ml *) +let constrain ((n : int),(pat : constr_pattern)) sigma = + if List.mem_assoc n sigma then + if pat = (List.assoc n sigma) then sigma + else failwith "internal" + else + (n,pat)::sigma + +(* This function is inspired from matches_core in pattern.ml *) +let more_general_pat pat1 pat2 = + let rec match_rec sigma p1 p2 = + match p1, p2 with + | PMeta (Some n), m -> constrain (n,m) sigma + + | PMeta None, m -> sigma + + | PRef (VarRef sp1), PRef(VarRef sp2) when sp1 = sp2 -> sigma + + | PVar v1, PVar v2 when v1 = v2 -> sigma + + | PRef ref1, PRef ref2 when ref1 = ref2 -> sigma + + | PRel n1, PRel n2 when n1 = n2 -> sigma + + | PSort (RProp c1), PSort (RProp c2) when c1 = c2 -> sigma + + | PSort (RType _), PSort (RType _) -> sigma + + | PApp (c1,arg1), PApp (c2,arg2) -> + (try array_fold_left2 match_rec (match_rec sigma c1 c2) arg1 arg2 + with Invalid_argument _ -> failwith "internal") + | _ -> failwith "unexpected case in more_general_pat" in + try let _ = match_rec [] pat1 pat2 in true + with Failure "internal" -> false;; + +let more_general r1 r2 = + match r1,r2 with + (_,(patt1,p11,p12,_,_,_)), + (_,(patt2,p21,p22,_,_,_)) -> + (more_general_pat patt1 patt2) & + (is_prefix p11 p21) & (is_prefix p12 p22);; + +let not_less_general r1 r2 = + not (match r1,r2 with + (_,(patt1,p11,p12,_,_,_)), + (_,(patt2,p21,p22,_,_,_)) -> + (more_general_pat patt1 patt2) & + (is_prefix p21 p11) & (is_prefix p22 p12));; + +let rec add_in_list_sorting rule1 = function + [] -> [rule1] + | (b::tl) as this_list -> + if more_general rule1 b then + b::(add_in_list_sorting rule1 tl) + else if not_less_general rule1 b then + let tl2 = add_in_list_sorting_aux rule1 tl in + (match tl2 with + [] -> rule1::this_list + | _ -> b::tl2) + else + rule1::this_list +and add_in_list_sorting_aux rule1 = function + [] -> [] + | b::tl -> + if more_general rule1 b then + b::(add_in_list_sorting rule1 tl) + else + let tl2 = add_in_list_sorting_aux rule1 tl in + (match tl2 with + [] -> [] + | _ -> rule1::tl2);; + +let rec sort_list = function + [] -> [] + | a::l -> add_in_list_sorting a (sort_list l);; + +let mk_dad_meta n = Node(zz,"META",[Num(zz, n)]);; +let mk_rewrite1 ast = + Node(zz,"TACTICLIST", + [Node(zz,"RewriteLR", + [Node(zz, "COMMAND", ast);Node(zz,"BINDINGS",[])])]);; + +let mk_rewrite2 ast = + Node(zz,"TACTICLIST", + [Node(zz,"RewriteRL", + [Node(zz, "COMMAND", ast);Node(zz,"BINDINGS",[])])]);; + + + +let start_dad () = +vinterp_add "AddDadRule" + (function + | [VARG_STRING name; VARG_CONSTR pat; VARG_NUMBERLIST p1; + VARG_NUMBERLIST p2; VARG_TACTIC com] -> + (function () -> + let pr = match decompose_path (p1, p2) with pr, _, _ -> pr in + (add_dad_rule name (Ctast.ast_to_ct pat) p1 p2 (List.length pr) pr (Ctast.ast_to_ct com))) + | _ -> errorlabstrm "AddDadRule1" + [< str "AddDadRule2">]); +add_dad_rule "distributivity-inv" +(Node(zz,"APPLIST",[Nvar(zz,"mult");Node(zz,"APPLIST",[Nvar(zz,"plus");Node(zz,"META",[Num(zz,4)]);Node(zz,"META",[Num(zz,3)])]);Node(zz,"META",[Num(zz,2)])])) +[2; 2] +[2; 1] +1 +[2] +(mk_rewrite1 ([Node(zz, "APPLIST", [Nvar(zz, "mult_plus_distr");(mk_dad_meta 4) ;(mk_dad_meta 3) ;(mk_dad_meta 2) ])])); + +add_dad_rule "distributivity1-r" +(Node(zz,"APPLIST",[Nvar(zz,"plus");Node(zz,"APPLIST",[Nvar(zz,"mult");Node(zz,"META",[Num(zz,4)]);Node(zz,"META",[Num(zz,2)])]);Node(zz,"APPLIST",[Nvar(zz,"mult");Node(zz,"META",[Num(zz,3)]);Node(zz,"META",[Num(zz,2)])])])) +[2; 2; 2; 2] +[] +0 +[] +(mk_rewrite2 ([Node(zz, "APPLIST", [Nvar(zz, "mult_plus_distr");(mk_dad_meta 4) ;(mk_dad_meta 3) ;(mk_dad_meta 2) ])])); + +add_dad_rule "distributivity1-l" +(Node(zz,"APPLIST",[Nvar(zz,"plus");Node(zz,"APPLIST",[Nvar(zz,"mult");Node(zz,"META",[Num(zz,4)]);Node(zz,"META",[Num(zz,2)])]);Node(zz,"APPLIST",[Nvar(zz,"mult");Node(zz,"META",[Num(zz,3)]);Node(zz,"META",[Num(zz,2)])])])) +[2; 1; 2; 2] +[] +0 +[] +(mk_rewrite2 ([Node(zz, "APPLIST", [Nvar(zz, "mult_plus_distr");(mk_dad_meta 4) ;(mk_dad_meta 3) ;(mk_dad_meta 2) ])])); + +add_dad_rule "associativity" +(Node(zz,"APPLIST",[Nvar(zz,"plus");Node(zz,"APPLIST",[Nvar(zz,"plus");Node(zz,"META",[Num(zz,4)]);Node(zz,"META",[Num(zz,3)])]);Node(zz,"META",[Num(zz,2)])])) +[2; 1] +[] +0 +[] +(mk_rewrite1 ([Node(zz, "APPLIST", [Nvar(zz, "plus_assoc_r");(mk_dad_meta 4) ;(mk_dad_meta 3) ;(mk_dad_meta 2) ])])); + +add_dad_rule "minus-identity-lr" +(Node(zz,"APPLIST",[Nvar(zz,"minus");Node(zz,"META",[Num(zz,2)]);Node(zz,"META",[Num(zz,2)])])) +[2; 1] +[2; 2] +1 +[2] +(mk_rewrite2 ([Node(zz, "APPLIST", [Nvar(zz, "minus_n_n");(mk_dad_meta 2) ])])); + +add_dad_rule "minus-identity-rl" +(Node(zz,"APPLIST",[Nvar(zz,"minus");Node(zz,"META",[Num(zz,2)]);Node(zz,"META",[Num(zz,2)])])) +[2; 2] +[2; 1] +1 +[2] +(mk_rewrite2 ([Node(zz, "APPLIST", [Nvar(zz, "minus_n_n");(mk_dad_meta 2) ])])); + +add_dad_rule "plus-sym-rl" +(Node(zz,"APPLIST",[Nvar(zz,"plus");Node(zz,"META",[Num(zz,3)]);Node(zz,"META",[Num(zz,2)])])) +[2; 2] +[2; 1] +1 +[2] +(mk_rewrite1 ([Node(zz, "APPLIST", [Nvar(zz, "plus_sym");(mk_dad_meta 3) ;(mk_dad_meta 2) ])])); + +add_dad_rule "plus-sym-lr" +(Node(zz,"APPLIST",[Nvar(zz,"plus");Node(zz,"META",[Num(zz,3)]);Node(zz,"META",[Num(zz,2)])])) +[2; 1] +[2; 2] +1 +[2] +(mk_rewrite1 ([Node(zz, "APPLIST", [Nvar(zz, "plus_sym");(mk_dad_meta 3) ;(mk_dad_meta 2) ])])); + +add_dad_rule "absorb-0-r-rl" +(Node(zz,"APPLIST",[Nvar(zz,"plus");Node(zz,"META",[Num(zz,2)]);Nvar(zz,"O")])) +[2; 2] +[1] +0 +[] +(mk_rewrite2 ([Node(zz, "APPLIST", [Nvar(zz, "plus_n_O");(mk_dad_meta 2) ])])); + +add_dad_rule "absorb-0-r-lr" +(Node(zz,"APPLIST",[Nvar(zz,"plus");Node(zz,"META",[Num(zz,2)]);Nvar(zz,"O")])) +[1] +[2; 2] +0 +[] +(mk_rewrite2 ([Node(zz, "APPLIST", [Nvar(zz, "plus_n_O");(mk_dad_meta 2) ])])); + +add_dad_rule "plus-permute-lr" +(Node(zz,"APPLIST",[Nvar(zz,"plus");Node(zz,"META",[Num(zz,4)]);Node(zz,"APPLIST",[Nvar(zz,"plus");Node(zz,"META",[Num(zz,3)]);Node(zz,"META",[Num(zz,2)])])])) +[2; 1] +[2; 2; 2; 1] +1 +[2] +(mk_rewrite1 ([Node(zz, "APPLIST", [Nvar(zz, "plus_permute");(mk_dad_meta 4) ;(mk_dad_meta 3) ;(mk_dad_meta 2) ])])); + +add_dad_rule "plus-permute-rl" +(Node(zz,"APPLIST",[Nvar(zz,"plus");Node(zz,"META",[Num(zz,4)]);Node(zz,"APPLIST",[Nvar(zz,"plus");Node(zz,"META",[Num(zz,3)]);Node(zz,"META",[Num(zz,2)])])])) +[2; 2; 2; 1] +[2; 1] +1 +[2] +(mk_rewrite1 ([Node(zz, "APPLIST", [Nvar(zz, "plus_permute");(mk_dad_meta 4) ;(mk_dad_meta 3) ;(mk_dad_meta 2) ])]));; + +vinterp_add "StartDad" + (function + | [] -> + (function () -> start_dad()) + | _ -> errorlabstrm "StartDad" [< >]);; diff --git a/contrib/interface/line_parser.ml b/contrib/interface/line_parser.ml deleted file mode 100755 index 91eda0eed0..0000000000 --- a/contrib/interface/line_parser.ml +++ /dev/null @@ -1,235 +0,0 @@ -(* line-oriented Syntactic analyser for a Coq parser *) -(* This parser expects a very small number of commands, each given on a complete -line. Some of these commands are then followed by a text fragment terminated -by a precise keyword, which is also expected to appear alone on a line. *) - -(* The main parsing loop procedure is "parser_loop", given at the end of this -file. It read lines one by one and checks whether they can be parsed using -a very simple parser. This very simple parser uses a lexer, which is also given -in this file. - -The lexical analyser: - There are only 5 sorts of tokens *) -type simple_tokens = Tspace | Tid of string | Tint of int | Tstring of string | - Tlbracket | Trbracket;; - -(* When recognizing identifiers or strings, the lexical analyser accumulates - the characters in a buffer, using the command add_in_buff. To recuperate - the characters, one can use get_buff (this code was inspired by the - code in src/meta/lexer.ml of Coq revision 6.1) *) -let add_in_buff,get_buff = - let buff = ref (String.create 80) in - (fun i x -> - let len = String.length !buff in - if i >= len then (buff := !buff ^ (String.create len);()); - String.set !buff i x; - succ i), - (fun len -> String.sub !buff 0 len);; - -(* Identifiers are [a-zA-Z_][a-zA-Z0-9_]*. When arriving here the first - character has already been recognized. *) -let rec ident len = parser - [<''_' | 'a'..'z' | 'A'..'Z' | '0'..'9' as c; s >] -> - ident (add_in_buff len c) s -| [< >] -> let str = get_buff len in Tid(str);; - -(* While recognizing integers, one constructs directly the integer value. - The ascii code of '0' is important for this. *) -let code0 = Char.code '0';; - -let get_digit c = Char.code c - code0;; - -(* Integers are [0-9]* - The variable intval is the integer value of the text that has already - been recognized. As for identifiers, the first character has already been - recognized. *) - -let rec parse_int intval = parser - [< ''0'..'9' as c ; i=parse_int (10 * intval + get_digit c)>] -> i -| [< >] -> Tint intval;; - -(* The string lexer is borrowed from the string parser of Coq V6.1 - This may be a problem if convention have changed in Coq, - However this parser is only used to recognize file names which should - not contain too many special characters *) - -let rec spec_char = parser - [< ''n' >] -> '\n' -| [< ''t' >] -> '\t' -| [< ''b' >] -> '\008' -| [< ''r' >] -> '\013' -| [< ''0'..'9' as c; v= (spec1 (get_digit c)) >] -> - Char.chr v -| [< 'x >] -> x - -and spec1 v = parser - [< ''0'..'9' as c; s >] -> spec1 (10*v+(get_digit c)) s -| [< >] -> v -;; - -(* This is the actual string lexical analyser. Strings are - QUOT([^QUOT\\]|\\[0-9]*|\\[^0-9])QUOT (the word QUOT is used - to represents double quotation characters, that cannot be used - freely, even inside comments. *) - -let rec string len = parser - [< ''"' >] -> len -| [<''\\' ; - len = (parser [< ''\n' >] -> len - | [< c=spec_char >] -> add_in_buff len c); - s >] -> string len s -| [< 'x; s >] -> string (add_in_buff len x) s;; - -(* The lexical analyser repeats the recognized given by next_token: - spaces and tabulations are ignored, identifiers, integers, - strings, opening and closing square brackets. Lexical errors are - ignored ! *) -let rec next_token = parser count - [< '' ' | '\t'; tok = next_token >] -> tok -| [< ''_' | 'a'..'z' | 'A'..'Z' as c;i = (ident (add_in_buff 0 c))>] -> i -| [< ''0'..'9' as c ; i = (parse_int (get_digit c))>] -> i -| [< ''"' ; len = (string 0) >] -> Tstring (get_buff len) -| [< ''[' >] -> Tlbracket -| [< '']' >] -> Trbracket -| [< '_ ; x = next_token >] -> x;; - -(* A very simple lexical analyser to recognize a integer value behind - blank characters *) - -let rec next_int = parser count - [< '' ' | '\t'; v = next_int >] -> v -| [< ''0'..'9' as c; i = (parse_int (get_digit c))>] -> - (match i with - Tint n -> n - | _ -> failwith "unexpected branch in next_int");; - -(* This is the actual lexical analyser, implemented as a function on a stream. - It will be used with the Stream.from primitive to construct a function - of type char Stream.t -> simple_token option Stream.t *) -let token_stream cs _ = - try let tok = next_token cs in - Some tok - with Stream.Failure -> None;; - -(* Two of the actions of the parser request that one reads the rest of - the input up to a specific string stop_string. This is done - with a function that transform the input_channel into a pair of - char Stream.t, reading from the input_channel all the lines to - the stop_string first. *) - - -let rec gather_strings stop_string input_channel = - let buff = input_line input_channel in - if buff = stop_string then - [] - else - (buff::(gather_strings stop_string input_channel));; - - -(* the result of this function is supposed to be used in a Stream.from - construction. *) - -let line_list_to_stream string_list = - let count = ref 0 in - let buff = ref "" in - let reserve = ref string_list in - let current_length = ref 0 in - (fun i -> if (i - !count) >= !current_length then - begin - count := !count + !current_length + 1; - match !reserve with - | [] -> None - | s1::rest -> - begin - buff := s1; - current_length := String.length !buff; - reserve := rest; - Some '\n' - end - end - else - Some(String.get !buff (i - !count)));; - - -(* In older revisions of this file you would find a function that - does line oriented breakdown of the input channel without resorting to - a list of lines. However, the need for the list of line appeared when - we wanted to have a channel and a list of strings describing the same - data, one for regular parsing and the other for error recovery. *) - -let channel_to_stream_and_string_list stop_string input_channel = - let string_list = gather_strings stop_string input_channel in - (line_list_to_stream string_list, string_list);; - -let flush_until_end_of_stream char_stream = - Stream.iter (function _ -> ()) char_stream;; - -(* There are only 5 kinds of lines recognized by our little parser. - Unrecognized lines are ignored. *) -type parser_request = - | PRINT_VERSION - | PARSE_STRING of string - (* parse_string [] then text and && END--OF--DATA *) - | QUIET_PARSE_STRING - (* quiet_parse_string then text and && END--OF--DATA *) - | PARSE_FILE of string - (* parse_file *) - | ADD_PATH of string - (* add_path *) - | LOAD_SYNTAX of string - (* load_syntax_file *) - | GARBAGE -;; - -(* The procedure parser_loop should never terminate while the input_channel is - not closed. This procedure receives the functions called for each sentence - as arguments. Thus the code is completely independent from the Coq sources. *) -let parser_loop functions input_channel = - let print_version_action, - parse_string_action, - quiet_parse_string_action, - parse_file_action, - add_path_action, - load_syntax_action = functions in - let rec parser_loop_rec input_channel = - (let line = input_line input_channel in - let reqid, parser_request = - try - (match Stream.from (token_stream (Stream.of_string line)) with - parser - | [< 'Tid "print_version" >] -> - 0, PRINT_VERSION - | [< 'Tid "parse_string" ; 'Tint reqid ; 'Tlbracket ; - 'Tid phylum ; 'Trbracket >] - -> reqid,PARSE_STRING phylum - | [< 'Tid "quiet_parse_string" >] -> - 0,QUIET_PARSE_STRING - | [< 'Tid "parse_file" ; 'Tint reqid ; 'Tstring fname >] -> - reqid, PARSE_FILE fname - | [< 'Tid "add_path"; 'Tint reqid ; 'Tstring directory >] - -> reqid, ADD_PATH directory - | [< 'Tid "load_syntax_file"; 'Tint reqid; 'Tid module_name >] -> - reqid, LOAD_SYNTAX module_name - | [< 'Tid "quit_parser" >] -> raise End_of_file - | [< >] -> 0, GARBAGE) - with - Stream.Failure | Stream.Error _ -> 0,GARBAGE in - match parser_request with - PRINT_VERSION -> print_version_action () - | PARSE_STRING phylum -> - let regular_stream, string_list = - channel_to_stream_and_string_list "&& END--OF--DATA" input_channel in - parse_string_action reqid phylum (Stream.from regular_stream) - string_list;() - | QUIET_PARSE_STRING -> - let regular_stream, string_list = - channel_to_stream_and_string_list "&& END--OF--DATA" input_channel in - quiet_parse_string_action - (Stream.from regular_stream);() - | PARSE_FILE file_name -> - parse_file_action reqid file_name - | ADD_PATH path -> add_path_action reqid path - | LOAD_SYNTAX syn -> load_syntax_action reqid syn - | GARBAGE -> ()); - parser_loop_rec input_channel in - parser_loop_rec input_channel;; diff --git a/contrib/interface/line_parser.ml4 b/contrib/interface/line_parser.ml4 new file mode 100755 index 0000000000..91eda0eed0 --- /dev/null +++ b/contrib/interface/line_parser.ml4 @@ -0,0 +1,235 @@ +(* line-oriented Syntactic analyser for a Coq parser *) +(* This parser expects a very small number of commands, each given on a complete +line. Some of these commands are then followed by a text fragment terminated +by a precise keyword, which is also expected to appear alone on a line. *) + +(* The main parsing loop procedure is "parser_loop", given at the end of this +file. It read lines one by one and checks whether they can be parsed using +a very simple parser. This very simple parser uses a lexer, which is also given +in this file. + +The lexical analyser: + There are only 5 sorts of tokens *) +type simple_tokens = Tspace | Tid of string | Tint of int | Tstring of string | + Tlbracket | Trbracket;; + +(* When recognizing identifiers or strings, the lexical analyser accumulates + the characters in a buffer, using the command add_in_buff. To recuperate + the characters, one can use get_buff (this code was inspired by the + code in src/meta/lexer.ml of Coq revision 6.1) *) +let add_in_buff,get_buff = + let buff = ref (String.create 80) in + (fun i x -> + let len = String.length !buff in + if i >= len then (buff := !buff ^ (String.create len);()); + String.set !buff i x; + succ i), + (fun len -> String.sub !buff 0 len);; + +(* Identifiers are [a-zA-Z_][a-zA-Z0-9_]*. When arriving here the first + character has already been recognized. *) +let rec ident len = parser + [<''_' | 'a'..'z' | 'A'..'Z' | '0'..'9' as c; s >] -> + ident (add_in_buff len c) s +| [< >] -> let str = get_buff len in Tid(str);; + +(* While recognizing integers, one constructs directly the integer value. + The ascii code of '0' is important for this. *) +let code0 = Char.code '0';; + +let get_digit c = Char.code c - code0;; + +(* Integers are [0-9]* + The variable intval is the integer value of the text that has already + been recognized. As for identifiers, the first character has already been + recognized. *) + +let rec parse_int intval = parser + [< ''0'..'9' as c ; i=parse_int (10 * intval + get_digit c)>] -> i +| [< >] -> Tint intval;; + +(* The string lexer is borrowed from the string parser of Coq V6.1 + This may be a problem if convention have changed in Coq, + However this parser is only used to recognize file names which should + not contain too many special characters *) + +let rec spec_char = parser + [< ''n' >] -> '\n' +| [< ''t' >] -> '\t' +| [< ''b' >] -> '\008' +| [< ''r' >] -> '\013' +| [< ''0'..'9' as c; v= (spec1 (get_digit c)) >] -> + Char.chr v +| [< 'x >] -> x + +and spec1 v = parser + [< ''0'..'9' as c; s >] -> spec1 (10*v+(get_digit c)) s +| [< >] -> v +;; + +(* This is the actual string lexical analyser. Strings are + QUOT([^QUOT\\]|\\[0-9]*|\\[^0-9])QUOT (the word QUOT is used + to represents double quotation characters, that cannot be used + freely, even inside comments. *) + +let rec string len = parser + [< ''"' >] -> len +| [<''\\' ; + len = (parser [< ''\n' >] -> len + | [< c=spec_char >] -> add_in_buff len c); + s >] -> string len s +| [< 'x; s >] -> string (add_in_buff len x) s;; + +(* The lexical analyser repeats the recognized given by next_token: + spaces and tabulations are ignored, identifiers, integers, + strings, opening and closing square brackets. Lexical errors are + ignored ! *) +let rec next_token = parser count + [< '' ' | '\t'; tok = next_token >] -> tok +| [< ''_' | 'a'..'z' | 'A'..'Z' as c;i = (ident (add_in_buff 0 c))>] -> i +| [< ''0'..'9' as c ; i = (parse_int (get_digit c))>] -> i +| [< ''"' ; len = (string 0) >] -> Tstring (get_buff len) +| [< ''[' >] -> Tlbracket +| [< '']' >] -> Trbracket +| [< '_ ; x = next_token >] -> x;; + +(* A very simple lexical analyser to recognize a integer value behind + blank characters *) + +let rec next_int = parser count + [< '' ' | '\t'; v = next_int >] -> v +| [< ''0'..'9' as c; i = (parse_int (get_digit c))>] -> + (match i with + Tint n -> n + | _ -> failwith "unexpected branch in next_int");; + +(* This is the actual lexical analyser, implemented as a function on a stream. + It will be used with the Stream.from primitive to construct a function + of type char Stream.t -> simple_token option Stream.t *) +let token_stream cs _ = + try let tok = next_token cs in + Some tok + with Stream.Failure -> None;; + +(* Two of the actions of the parser request that one reads the rest of + the input up to a specific string stop_string. This is done + with a function that transform the input_channel into a pair of + char Stream.t, reading from the input_channel all the lines to + the stop_string first. *) + + +let rec gather_strings stop_string input_channel = + let buff = input_line input_channel in + if buff = stop_string then + [] + else + (buff::(gather_strings stop_string input_channel));; + + +(* the result of this function is supposed to be used in a Stream.from + construction. *) + +let line_list_to_stream string_list = + let count = ref 0 in + let buff = ref "" in + let reserve = ref string_list in + let current_length = ref 0 in + (fun i -> if (i - !count) >= !current_length then + begin + count := !count + !current_length + 1; + match !reserve with + | [] -> None + | s1::rest -> + begin + buff := s1; + current_length := String.length !buff; + reserve := rest; + Some '\n' + end + end + else + Some(String.get !buff (i - !count)));; + + +(* In older revisions of this file you would find a function that + does line oriented breakdown of the input channel without resorting to + a list of lines. However, the need for the list of line appeared when + we wanted to have a channel and a list of strings describing the same + data, one for regular parsing and the other for error recovery. *) + +let channel_to_stream_and_string_list stop_string input_channel = + let string_list = gather_strings stop_string input_channel in + (line_list_to_stream string_list, string_list);; + +let flush_until_end_of_stream char_stream = + Stream.iter (function _ -> ()) char_stream;; + +(* There are only 5 kinds of lines recognized by our little parser. + Unrecognized lines are ignored. *) +type parser_request = + | PRINT_VERSION + | PARSE_STRING of string + (* parse_string [] then text and && END--OF--DATA *) + | QUIET_PARSE_STRING + (* quiet_parse_string then text and && END--OF--DATA *) + | PARSE_FILE of string + (* parse_file *) + | ADD_PATH of string + (* add_path *) + | LOAD_SYNTAX of string + (* load_syntax_file *) + | GARBAGE +;; + +(* The procedure parser_loop should never terminate while the input_channel is + not closed. This procedure receives the functions called for each sentence + as arguments. Thus the code is completely independent from the Coq sources. *) +let parser_loop functions input_channel = + let print_version_action, + parse_string_action, + quiet_parse_string_action, + parse_file_action, + add_path_action, + load_syntax_action = functions in + let rec parser_loop_rec input_channel = + (let line = input_line input_channel in + let reqid, parser_request = + try + (match Stream.from (token_stream (Stream.of_string line)) with + parser + | [< 'Tid "print_version" >] -> + 0, PRINT_VERSION + | [< 'Tid "parse_string" ; 'Tint reqid ; 'Tlbracket ; + 'Tid phylum ; 'Trbracket >] + -> reqid,PARSE_STRING phylum + | [< 'Tid "quiet_parse_string" >] -> + 0,QUIET_PARSE_STRING + | [< 'Tid "parse_file" ; 'Tint reqid ; 'Tstring fname >] -> + reqid, PARSE_FILE fname + | [< 'Tid "add_path"; 'Tint reqid ; 'Tstring directory >] + -> reqid, ADD_PATH directory + | [< 'Tid "load_syntax_file"; 'Tint reqid; 'Tid module_name >] -> + reqid, LOAD_SYNTAX module_name + | [< 'Tid "quit_parser" >] -> raise End_of_file + | [< >] -> 0, GARBAGE) + with + Stream.Failure | Stream.Error _ -> 0,GARBAGE in + match parser_request with + PRINT_VERSION -> print_version_action () + | PARSE_STRING phylum -> + let regular_stream, string_list = + channel_to_stream_and_string_list "&& END--OF--DATA" input_channel in + parse_string_action reqid phylum (Stream.from regular_stream) + string_list;() + | QUIET_PARSE_STRING -> + let regular_stream, string_list = + channel_to_stream_and_string_list "&& END--OF--DATA" input_channel in + quiet_parse_string_action + (Stream.from regular_stream);() + | PARSE_FILE file_name -> + parse_file_action reqid file_name + | ADD_PATH path -> add_path_action reqid path + | LOAD_SYNTAX syn -> load_syntax_action reqid syn + | GARBAGE -> ()); + parser_loop_rec input_channel in + parser_loop_rec input_channel;; diff --git a/contrib/xml/xml.ml b/contrib/xml/xml.ml deleted file mode 100644 index 60e16ab19b..0000000000 --- a/contrib/xml/xml.ml +++ /dev/null @@ -1,80 +0,0 @@ -(***********************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* *) -(* 18/10/2000 *) -(* *) -(* This module defines a pretty-printer and the stream of commands to the pp *) -(* *) -(******************************************************************************) - - -(* the type token for XML cdata, empty elements and not-empty elements *) -(* Usage: *) -(* Str cdata *) -(* Empty (element_name, [attrname1, value1 ; ... ; attrnamen, valuen] *) -(* NEmpty (element_name, [attrname1, value2 ; ... ; attrnamen, valuen], *) -(* content *) -type token = Str of string - | Empty of string * (string * string) list - | NEmpty of string * (string * string) list * token Stream.t -;; - -(* currified versions of the constructors make the code more readable *) -let xml_empty name attrs = [< 'Empty(name,attrs) >] -let xml_nempty name attrs content = [< 'NEmpty(name,attrs,content) >] -let xml_cdata str = [< 'Str str >] - -(* Usage: *) -(* pp tokens None pretty prints the output on stdout *) -(* pp tokens (Some filename) pretty prints the output on the file filename *) -let pp strm fn = - let channel = ref stdout in - let rec pp_r m = - parser - [< 'Str a ; s >] -> - print_spaces m ; - fprint_string (a ^ "\n") ; - pp_r m s - | [< 'Empty(n,l) ; s >] -> - print_spaces m ; - fprint_string ("<" ^ n) ; - List.iter (function (n,v) -> fprint_string (" " ^ n ^ "=\"" ^ v ^ "\"")) l; - fprint_string "/>\n" ; - pp_r m s - | [< 'NEmpty(n,l,c) ; s >] -> - print_spaces m ; - fprint_string ("<" ^ n) ; - List.iter (function (n,v) -> fprint_string (" " ^ n ^ "=\"" ^ v ^ "\"")) l; - fprint_string ">\n" ; - pp_r (m+1) c ; - print_spaces m ; - fprint_string ("\n") ; - pp_r m s - | [< >] -> () - and print_spaces m = - for i = 1 to m do fprint_string " " done - and fprint_string str = - output_string !channel str - in - match fn with - Some filename -> - let filename = filename ^ ".xml" in - channel := open_out filename ; - pp_r 0 strm ; - close_out !channel ; - print_string ("\nWriting on file \"" ^ filename ^ "\" was succesfull\n"); - flush stdout - | None -> - pp_r 0 strm -;; diff --git a/contrib/xml/xml.ml4 b/contrib/xml/xml.ml4 new file mode 100644 index 0000000000..60e16ab19b --- /dev/null +++ b/contrib/xml/xml.ml4 @@ -0,0 +1,80 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* *) +(* 18/10/2000 *) +(* *) +(* This module defines a pretty-printer and the stream of commands to the pp *) +(* *) +(******************************************************************************) + + +(* the type token for XML cdata, empty elements and not-empty elements *) +(* Usage: *) +(* Str cdata *) +(* Empty (element_name, [attrname1, value1 ; ... ; attrnamen, valuen] *) +(* NEmpty (element_name, [attrname1, value2 ; ... ; attrnamen, valuen], *) +(* content *) +type token = Str of string + | Empty of string * (string * string) list + | NEmpty of string * (string * string) list * token Stream.t +;; + +(* currified versions of the constructors make the code more readable *) +let xml_empty name attrs = [< 'Empty(name,attrs) >] +let xml_nempty name attrs content = [< 'NEmpty(name,attrs,content) >] +let xml_cdata str = [< 'Str str >] + +(* Usage: *) +(* pp tokens None pretty prints the output on stdout *) +(* pp tokens (Some filename) pretty prints the output on the file filename *) +let pp strm fn = + let channel = ref stdout in + let rec pp_r m = + parser + [< 'Str a ; s >] -> + print_spaces m ; + fprint_string (a ^ "\n") ; + pp_r m s + | [< 'Empty(n,l) ; s >] -> + print_spaces m ; + fprint_string ("<" ^ n) ; + List.iter (function (n,v) -> fprint_string (" " ^ n ^ "=\"" ^ v ^ "\"")) l; + fprint_string "/>\n" ; + pp_r m s + | [< 'NEmpty(n,l,c) ; s >] -> + print_spaces m ; + fprint_string ("<" ^ n) ; + List.iter (function (n,v) -> fprint_string (" " ^ n ^ "=\"" ^ v ^ "\"")) l; + fprint_string ">\n" ; + pp_r (m+1) c ; + print_spaces m ; + fprint_string ("\n") ; + pp_r m s + | [< >] -> () + and print_spaces m = + for i = 1 to m do fprint_string " " done + and fprint_string str = + output_string !channel str + in + match fn with + Some filename -> + let filename = filename ^ ".xml" in + channel := open_out filename ; + pp_r 0 strm ; + close_out !channel ; + print_string ("\nWriting on file \"" ^ filename ^ "\" was succesfull\n"); + flush stdout + | None -> + pp_r 0 strm +;; diff --git a/contrib/xml/xmlcommand.ml b/contrib/xml/xmlcommand.ml deleted file mode 100644 index 7b6303130b..0000000000 --- a/contrib/xml/xmlcommand.ml +++ /dev/null @@ -1,1037 +0,0 @@ -(***********************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* *) -(* 06/12/2000 *) -(* *) -(******************************************************************************) - - -(* CONFIGURATION PARAMETERS *) - -let dtdname = "http://www.cs.unibo.it/helm/dtd/cic.dtd";; -let typesdtdname = "http://www.cs.unibo.it/helm/dtd/cictypes.dtd";; -let verbose = ref false;; (* always set to true during a "Print XML All" *) - -(* UTILITY FUNCTIONS *) - -let print_if_verbose s = if !verbose then print_string s;; - -type tag = - Constant - | Inductive - | Variable -;; - -(* Next exception is used only inside print_object and tag_of_string_tag *) -exception Uninteresting;; - -let tag_of_string_tag = - function - "CONSTANT" - | "PARAMETER" -> Constant - | "INDUCTIVE" -> Inductive - | "VARIABLE" -> Variable - | _ -> raise Uninteresting -;; - -let ext_of_tag = - function - Constant -> "con" - | Inductive -> "ind" - | Variable -> "var" -;; - -(* Internally, for Coq V7, params of inductive types are associated *) -(* not to the whole block of mutual inductive (as it was in V6) but to *) -(* each member of the block; but externally, all params are required *) -(* to be the same; the following function checks that the parameters *) -(* of each inductive of a same block are all the same, then returns *) -(* this number; it fails otherwise *) -let extract_nparams pack = - let module D = Declarations in - let module U = Util in - let module S = Sign in - - let {D.mind_nparams=nparams0} = pack.(0) in - let arity0 = pack.(0).D.mind_user_arity in - let params0, _ = S.decompose_prod_n_assum nparams0 arity0 in - for i = 1 to Array.length pack - 1 do - let {D.mind_nparams=nparamsi} = pack.(i) in - let arityi = pack.(i).D.mind_user_arity in - let paramsi, _ = S.decompose_prod_n_assum nparamsi arityi in - if params0 <> paramsi then U.error "Cannot convert a block of inductive definitions with parameters specific to each inductive to a block of mutual inductive definitions with parameters global to the whole block" - done; - nparams0 - -(* could_have_namesakes sp = true iff o is an object that could be cooked and *) -(* than that could exists in cooked form with the same name in a super *) -(* section of the actual section *) -let could_have_namesakes o sp = (* namesake = omonimo in italian *) - let module D = Declare in - let tag = Libobject.object_tag o in - print_if_verbose ("Object tag: " ^ tag ^ "\n") ; - match tag with - "CONSTANT" -> - (match D.constant_strength sp with - | D.DischargeAt _ -> false (* a local definition *) - | D.NotDeclare -> false (* not a definition *) - | D.NeverDischarge -> true (* a non-local one *) - ) - | "PARAMETER" (* axioms and *) - | "INDUCTIVE" -> true (* mutual inductive types are never local *) - | "VARIABLE" -> false (* variables are local, so no namesakes *) - | _ -> false (* uninteresting thing that won't be printed*) -;; - - -(* uri_of_path sp is a broken (wrong) uri pointing to the object whose *) -(* section path is sp *) -let uri_of_path sp tag = - let module N = Names in - let module No = Nameops in - let ext_of_sp sp = ext_of_tag tag in - let dir0 = No.extend_dirpath (No.dirpath sp) (No.basename sp) in - let dir = List.map N.string_of_id (List.rev (N.repr_dirpath dir0)) in - "cic:/" ^ (String.concat "/" dir) ^ "." ^ (ext_of_sp sp) -;; - -let string_of_sort = - let module T = Term in - function - T.Prop(T.Pos) -> "Set" - | T.Prop(T.Null) -> "Prop" - | T.Type(_) -> "Type" -;; - -let string_of_name = - let module N = Names in - function - N.Name id -> N.string_of_id id - | _ -> Util.anomaly "this should not happen" -;; - -(* A SIMPLE DATA STRUCTURE AND SOME FUNCTIONS TO MANAGE THE CURRENT *) -(* ENVIRONMENT (= [l1, ..., ln] WHERE li IS THE LIST OF VARIABLES *) -(* DECLARED IN THE i-th SUPER-SECTION OF THE CURRENT SECTION *) - -(*CSC: commento sbagliato ed obsoleto *) -(* list of variables availables in the actual section *) -let pvars = ref ([[]] : string list list);; -let cumenv = ref Environ.empty_env;; - -let string_of_vars_list = - let add_prefix n s = string_of_int n ^ ": " ^ s in - let rec aux = - function - [n,v] -> (n,v) - | (n,v)::tl -> - let (k,s) = aux tl in - if k = n then (k, v ^ " " ^ s) else (n, v ^ " " ^ add_prefix k s) - | [] -> assert false - in - function - [] -> "" - | vl -> let (k,s) = aux vl in add_prefix k s -;; - -(* -let string_of_pvars pvars hyps = - let rec aux = - function - [] -> (0, "") - | he::tl -> - let (n,s) = aux tl in - (n + 1, - string_of_int n ^ ": " ^ (String.concat " ") (List.rev he) ^ - match s with "" -> "" | _ -> " " ^ s - ) - in - snd (aux (List.rev pvars)) -;; -*) - -let string_of_pvars pvars hyps = - let find_depth pvars v = - let rec aux n = - function - [] -> assert false -(* (-1,"?") For Print XML *) -(* -print_string "\nPVARS:" ; -List.iter (List.iter print_string) pvars ; -print_string "\nHYPS:" ; -List.iter print_string hyps ; -print_string "\n" ; -flush stdout ; -assert false -*) - | l::_ when List.mem v l -> (n,v) - | _::tl -> aux (n+1) tl - in - aux 0 pvars - in - string_of_vars_list (List.map (find_depth pvars) (List.rev hyps)) -;; - -type variables_type = - Definition of string * Term.constr * Term.types - | Assumption of string * Term.constr -;; - -let add_to_pvars x = - let module E = Environ in - let v = - match x with - Definition (v, bod, typ) -> - cumenv := - E.push_named_decl (Names.id_of_string v, Some bod, typ) !cumenv ; - v - | Assumption (v, typ) -> - cumenv := - E.push_named_decl (Names.id_of_string v, None, typ) !cumenv ; - v - in - match !pvars with - [] -> assert false - | (he::tl) -> pvars := (v::he)::tl -;; - -let get_depth_of_var v = - let rec aux n = - function - [] -> None - | (he::tl) -> if List.mem v he then Some n else aux (n + 1) tl - in - aux 0 !pvars -;; - -(* FUNCTIONS TO CREATE IDENTIFIERS *) - -(* seed to create the next identifier *) -let next_id_cic = ref 0;; -let next_id_types = ref 0;; - -(* reset_ids () reset the identifier seed to 0 *) -let reset_ids () = - next_id_cic := 0 ; - next_id_types := 0 -;; - -(* get_next_id () returns fresh identifier *) -let get_next_id = - function - `T -> - let res = - "t" ^ string_of_int !next_id_types - in - incr next_id_types ; - res - | `I -> - let res = - "i" ^ string_of_int !next_id_cic - in - incr next_id_cic ; - res -;; - -type innersort = - InnerProp of Term.constr (* the constr is the type of the term *) - | InnerSet - | InnerType -;; - -(* FUNCTION TO PRINT A SINGLE TERM OF CIC *) -(* print_term t l where t is a term of Cic returns a stream of XML tokens *) -(* suitable to be printed via the pretty printer Xml.pp. l is the list of *) -(* bound names *) -let print_term inner_types l env csr = - let module N = Names in - let module E = Environ in - let module T = Term in - let module X = Xml in - let module R = Retyping in - let rec names_to_ids = - function - [] -> [] - | (N.Name id)::l -> id::(names_to_ids l) - | _ -> names_to_ids l - in - - let inner_type_display env term = - let type_of_term = - Reduction.nf_betaiota (R.get_type_of env (Evd.empty) term) - in - match R.get_sort_family_of env (Evd.empty) type_of_term with - T.InProp -> InnerProp type_of_term - | T.InSet -> InnerSet - | T.InType -> InnerType - in - -(*WHICH FORCE FUNCTION DEPENDS ON THE ORDERING YOU WANT - let rec force = - parser - [< 'he ; tl >] -> let tl = (force tl) in [< 'he ; tl >] - | [< >] -> [<>] - in -*) - let force x = x in - - let rec term_display idradix in_lambda l env cstr = - let next_id = get_next_id idradix in - let add_sort_attribute do_output_type l' = - let xmlinnertype = inner_type_display env cstr in - match xmlinnertype with - InnerProp type_of_term -> - if do_output_type & idradix = `I then - begin - let pp_cmds = term_display `T false l env type_of_term in - inner_types := (next_id, pp_cmds)::!inner_types ; - end ; - ("sort","Prop")::l' - | InnerSet -> ("sort","Set")::l' - | InnerType -> ("sort","Type")::l' - in - let add_type_attribute l' = - ("type", string_of_sort (R.get_sort_of env (Evd.empty) cstr))::l' - in - (* kind_of_term helps doing pattern matching hiding the lower level of *) - (* coq coding of terms (the one of the logical framework) *) - match T.kind_of_term cstr with - T.Rel n -> - let id = - match List.nth l (n - 1) with - N.Name id -> id - | N.Anonymous -> Nameops.make_ident "_" None - in - X.xml_empty "REL" - (add_sort_attribute false - ["value",(string_of_int n) ; - "binder",(N.string_of_id id) ; - "id", next_id]) - | T.Var id -> - let depth = - match get_depth_of_var (N.string_of_id id) with - None -> "?" (* when printing via Show XML Proof or Print XML id *) - (* no infos about variables uri are known *) -(*V7 posso usare nametab, forse*) - | Some n -> string_of_int n - in - X.xml_empty "VAR" - (add_sort_attribute false - ["relUri",depth ^ "," ^ (N.string_of_id id) ; - "id", next_id]) - | T.Meta n -> - X.xml_empty "META" - (add_sort_attribute false ["no",(string_of_int n) ; "id", next_id]) - | T.Sort s -> - X.xml_empty "SORT" ["value",(string_of_sort s) ; "id", next_id] - | T.Cast (t1,t2) -> - X.xml_nempty "CAST" (add_sort_attribute false ["id", next_id]) -(force - [< X.xml_nempty "term" [] (term_display idradix false l env t1) ; - X.xml_nempty "type" [] (term_display idradix false l env t2) - >] -) - | T.LetIn (nid,s,t,d)-> - let nid' = Nameops.next_name_away nid (names_to_ids l) in - X.xml_nempty "LETIN" (add_sort_attribute true ["id", next_id]) -(force - [< X.xml_nempty "term" [] (term_display idradix false l env s) ; - X.xml_nempty "letintarget" ["binder",(N.string_of_id nid')] - (term_display idradix false - ((N.Name nid')::l) - (E.push_rel (N.Name nid', Some s, t) env) - d - ) - >] -) - | T.Prod (N.Name _ as nid, t1, t2) -> - let nid' = Nameops.next_name_away nid (names_to_ids l) in - X.xml_nempty "PROD" (add_type_attribute ["id", next_id]) -(force - [< X.xml_nempty "source" [] (term_display idradix false l env t1) ; - X.xml_nempty "target" - (if idradix = `T && - T.noccurn 1 t2 - then [] - else ["binder",(N.string_of_id nid')]) - (term_display idradix false - ((N.Name nid')::l) - (E.push_rel (N.Name nid', None, t1) env) - t2 - ) - >] -) - | T.Prod (N.Anonymous as nid, t1, t2) -> - X.xml_nempty "PROD" (add_type_attribute ["id", next_id]) -(force - [< X.xml_nempty "source" [] (term_display idradix false l env t1) ; - X.xml_nempty "target" [] - (term_display idradix false - (nid::l) - (E.push_rel (nid, None, t1) env) - t2 - ) - >] -) - | T.Lambda (N.Name _ as nid, t1, t2) -> - let nid' = Nameops.next_name_away nid (names_to_ids l) in - X.xml_nempty "LAMBDA" (add_sort_attribute (not in_lambda) ["id",next_id]) -(force - [< X.xml_nempty "source" [] (term_display idradix false l env t1) ; - X.xml_nempty "target" ["binder",(N.string_of_id nid')] - (term_display idradix true - ((N.Name nid')::l) - (E.push_rel (N.Name nid', None, t1) env) - t2 - ) - >] -) - | T.Lambda (N.Anonymous as nid, t1, t2) -> - X.xml_nempty "LAMBDA" (add_sort_attribute (not in_lambda) ["id", next_id]) -(force - [< X.xml_nempty "source" [] (term_display idradix false l env t1) ; - X.xml_nempty "target" [] - (term_display idradix true - (nid::l) - (E.push_rel (nid, None, t1) env) - t2 - ) - >] -) - | T.App (h,t) -> - X.xml_nempty "APPLY" (add_sort_attribute true ["id", next_id]) -(force - [< (term_display idradix false l env h) ; - (Array.fold_right - (fun x i -> [< (term_display idradix false l env x); i >]) t [<>]) - >] -) - | T.Const sp -> - X.xml_empty "CONST" - (add_sort_attribute false - ["uri",(uri_of_path sp Constant) ; "id", next_id]) - | T.Ind (sp,i) -> - X.xml_empty "MUTIND" - ["uri",(uri_of_path sp Inductive) ; - "noType",(string_of_int i) ; - "id", next_id] - | T.Construct ((sp,i),j) -> - X.xml_empty "MUTCONSTRUCT" - (add_sort_attribute false - ["uri",(uri_of_path sp Inductive) ; - "noType",(string_of_int i) ; - "noConstr",(string_of_int j) ; - "id", next_id]) - | T.Case ({T.ci_ind=(sp,i)},ty,term,a) -> - let (uri, typeno) = (uri_of_path sp Inductive),i in - X.xml_nempty "MUTCASE" - (add_sort_attribute true - ["uriType",uri ; "noType",(string_of_int typeno) ; "id",next_id]) -(force - [< X.xml_nempty "patternsType" [] - [< (term_display idradix false l env ty) >] ; - X.xml_nempty "inductiveTerm" [] - [< (term_display idradix false l env term)>]; - Array.fold_right - (fun x i -> - [< X.xml_nempty "pattern" [] - [] ; i>] - ) a [<>] - >] -) - | T.Fix ((ai,i),((f,t,b) as rec_decl)) -> - X.xml_nempty "FIX" - (add_sort_attribute true ["noFun", (string_of_int i) ; "id",next_id]) -(force - [< Array.fold_right - (fun (fi,ti,bi,ai) i -> - [< X.xml_nempty "FixFunction" - ["name", (string_of_name fi); "recIndex", (string_of_int ai)] - [< X.xml_nempty "type" [] - [< term_display idradix false l env ti >] ; - X.xml_nempty "body" [] [< - term_display idradix false - ((Array.to_list f)@l) - (E.push_rec_types rec_decl env) - bi - >] - >] ; - i - >] - ) - (Array.mapi (fun j x -> (x,t.(j),b.(j),ai.(j)) ) f ) - [<>] - >] -) - | T.CoFix (i,((f,t,b) as rec_decl)) -> - X.xml_nempty "COFIX" - (add_sort_attribute true ["noFun", (string_of_int i) ; "id",next_id]) -(force - [< Array.fold_right - (fun (fi,ti,bi) i -> - [< X.xml_nempty "CofixFunction" ["name", (string_of_name fi)] - [< X.xml_nempty "type" [] - [< term_display idradix false l env ti >] ; - X.xml_nempty "body" [] [< - term_display idradix false - ((Array.to_list f)@l) - (E.push_rec_types rec_decl env) - bi - >] - >] ; - i - >] - ) - (Array.mapi (fun j x -> (x,t.(j),b.(j)) ) f ) [<>] - >] -) - | T.Evar _ -> - Util.anomaly "Evar node in a term!!!" - in - (*CSC: ad l vanno andrebbero aggiunti i nomi da non *) - (*CSC: mascherare (costanti? variabili?) *) - term_display `I false l env csr -;; - -(* FUNCTIONS TO PRINT A SINGLE OBJECT OF COQ *) - -(* print_current_proof term type id conjectures *) -(* where term is the term of the proof in progress p *) -(* and type is the type of p *) -(* and id is the identifier (name) of p *) -(* and conjectures is the list of conjectures (cic terms) *) -(* returns a stream of XML tokens suitable to be pretty printed via Xml.pp *) -let print_current_proof c typ id mv inner_types = - let module X = Xml in - let env = (Safe_typing.env_of_safe_env (Global.safe_env ())) in - [< X.xml_cdata "\n" ; - X.xml_cdata ("\n\n") ; - X.xml_nempty "CurrentProof" ["name",id ; "id", get_next_id `I] - [< List.fold_right - (fun (j,t) i -> - [< X.xml_nempty "Conjecture" ["no",(string_of_int j)] - [< print_term inner_types [] env t >] ; i >]) - mv [<>] ; - X.xml_nempty "body" [] [< print_term inner_types [] env c >] ; - X.xml_nempty "type" [] [< print_term inner_types [] env typ >] - >] - >] -;; - -(* print_axiom id type params *) -(* where type is the type of an axiom a *) -(* and id is the identifier (name) of a *) -(* and params is the list of formal params for a *) -(* returns a stream of XML tokens suitable to be pretty printed via Xml.pp *) -let print_axiom id typ fv hyps env inner_types = - let module X = Xml in - let module N = Names in - [< X.xml_cdata "\n" ; - X.xml_cdata ("\n\n") ; - X.xml_nempty "Axiom" - ["name",(N.string_of_id id) ; - "id", get_next_id `I ; - "params",(string_of_pvars fv hyps)] - [< X.xml_nempty "type" [] (print_term inner_types [] env typ) >] - >] -;; - -(* print_definition id term type params hyps *) -(* where id is the identifier (name) of a definition d *) -(* and term is the term (body) of d *) -(* and type is the type of d *) -(* and params is the list of formal params for d *) -(* returns a stream of XML tokens suitable to be pretty printed via Xml.pp *) -let print_definition id c typ fv hyps env inner_types = - let module X = Xml in - let module N = Names in - [< X.xml_cdata "\n" ; - X.xml_cdata ("\n\n") ; - X.xml_nempty "Definition" - ["name",(N.string_of_id id) ; - "id", get_next_id `I ; - "params",(string_of_pvars fv hyps)] - [< X.xml_nempty "body" [] (print_term inner_types [] env c) ; - X.xml_nempty "type" [] (print_term inner_types [] env typ) >] - >] -;; - -(* print_variable id type *) -(* where id is the identifier (name) of a variable v *) -(* and type is the type of v *) -(* returns a stream of XML tokens suitable to be pretty printed via Xml.pp *) -let print_variable id body typ env inner_types = - let module X = Xml in - let module N = Names in - [< X.xml_cdata "\n" ; - X.xml_cdata ("\n\n") ; - X.xml_nempty "Variable" ["name",(N.string_of_id id); "id", get_next_id `I] - [< (match body with - None -> [<>] - | Some body -> - X.xml_nempty "body" [] (print_term inner_types [] env body) - ) ; - X.xml_nempty "type" [] (print_term inner_types [] env typ) - >] - >] -;; - -(* print_mutual_inductive_packet p *) -(* where p is a mutual inductive packet (an inductive definition in a block *) -(* of mutual inductive definitions) *) -(* returns a stream of XML tokens suitable to be pretty printed via Xml.pp *) -(* Used only by print_mutual_inductive *) -let print_mutual_inductive_packet inner_types names env finite p = - let module D = Declarations in - let module N = Names in - let module T = Term in - let module X = Xml in - let {D.mind_consnames=consnames ; - D.mind_typename=typename ; - D.mind_nf_lc=lc ; - D.mind_nf_arity=arity} = p - in - [< X.xml_nempty "InductiveType" - ["name",(N.string_of_id typename) ; - "inductive",(string_of_bool finite) - ] - [< - X.xml_nempty "arity" [] - (print_term inner_types [] env (T.body_of_type arity)) ; - (Array.fold_right - (fun (name,lc) i -> - [< X.xml_nempty "Constructor" ["name",(N.string_of_id name)] - (print_term inner_types names env lc) ; - i - >]) - (Array.mapi (fun j x -> (x,T.body_of_type lc.(j)) ) consnames ) - [<>] - ) - >] - >] -;; - -(* print_mutual_inductive packs params nparams *) -(* where packs is the list of inductive definitions in the block of *) -(* mutual inductive definitions b *) -(* and params is the list of formal params for b *) -(* and nparams is the number of "parameters" in the arity of the *) -(* mutual inductive types *) -(* returns a stream of XML tokens suitable to be pretty printed via Xml.pp *) -let print_mutual_inductive finite packs fv hyps env inner_types = - let module D = Declarations in - let module E = Environ in - let module X = Xml in - let module N = Names in - let nparams = extract_nparams packs in - let names = - List.map - (fun p -> let {D.mind_typename=typename} = p in N.Name(typename)) - (Array.to_list packs) - in - let env = - List.fold_right - (fun {D.mind_typename=typename ; D.mind_nf_arity=arity} env -> - E.push_rel (N.Name typename, None, arity) env) - (Array.to_list packs) - env - in - [< X.xml_cdata "\n" ; - X.xml_cdata ("\n\n") ; - X.xml_nempty "InductiveDefinition" - ["noParams",string_of_int nparams ; - "id",get_next_id `I ; - "params",(string_of_pvars fv hyps)] - [< (Array.fold_right - (fun x i -> - [< print_mutual_inductive_packet - inner_types names env finite x ; i >] - ) packs [< >] - ) - >] - >] -;; - -let string_list_of_named_context_list = - List.map - (function (n,_,_) -> Names.string_of_id n) -;; - -let types_filename_of_filename = - function - Some f -> Some (f ^ ".types") - | None -> None -;; - -let pp_cmds_of_inner_types inner_types target_uri = - let module X = Xml in - let rec stream_of_list = - function - [] -> [<>] - | he::tl -> [< he ; stream_of_list tl >] - in - [< X.xml_cdata "\n" ; - X.xml_cdata ("\n\n"); - X.xml_nempty "InnerTypes" ["of",target_uri] - (stream_of_list - (List.map - (function - (id,type_pp_cmds) -> X.xml_nempty "TYPE" ["of",id] type_pp_cmds) - (List.rev inner_types) - )) - >] -;; - -(* print id dest *) -(* where sp is the qualified identifier (section path) of a *) -(* definition/theorem, variable or inductive definition *) -(* and dest is either None (for stdout) or (Some filename) *) -(* pretty prints via Xml.pp the object whose identifier is id on dest *) -(* Note: it is printed only (and directly) the most cooked available *) -(* form of the definition (all the parameters are *) -(* lambda-abstracted, but the object can still refer to variables) *) -let print qid fn = - let module D = Declarations in - let module G = Global in - let module N = Names in - let module Nt = Nametab in - let module T = Term in - let module X = Xml in - let (_,id) = Nt.repr_qualid qid in - let glob_ref = Nametab.locate qid in - let env = (Safe_typing.env_of_safe_env (G.safe_env ())) in - reset_ids () ; - let inner_types = ref [] in - let sp,tag,pp_cmds = - match glob_ref with - Nt.VarRef id -> - let sp = Declare.find_section_variable id in - let (_,body,typ) = G.lookup_named id in - sp,Variable,print_variable id body (T.body_of_type typ) env inner_types - | Nt.ConstRef sp -> - let {D.const_body=val0 ; D.const_type = typ ; D.const_hyps = hyps} = - G.lookup_constant sp in - let hyps = string_list_of_named_context_list hyps in - let typ = T.body_of_type typ in - sp,Constant, - begin - match val0 with - None -> print_axiom id typ [] hyps env inner_types - | Some c -> print_definition id c typ [] hyps env inner_types - end - | Nt.IndRef (sp,_) -> - let {D.mind_packets=packs ; - D.mind_hyps=hyps; - D.mind_finite=finite} = G.lookup_mind sp in - let hyps = string_list_of_named_context_list hyps in - sp,Inductive, - print_mutual_inductive finite packs [] hyps env inner_types - | Nt.ConstructRef _ -> - Util.anomaly ("print: this should not happen") - in - Xml.pp pp_cmds fn ; - Xml.pp (pp_cmds_of_inner_types !inner_types (uri_of_path sp tag)) - (types_filename_of_filename fn) -;; - -(* show dest *) -(* where dest is either None (for stdout) or (Some filename) *) -(* pretty prints via Xml.pp the proof in progress on dest *) -let show fn = - let pftst = Pfedit.get_pftreestate () in - let str = Names.string_of_id (Pfedit.get_current_proof_name ()) in - let pf = Tacmach.proof_of_pftreestate pftst in - let typ = (Proof_trees.goal_of_proof pf).Evd.evar_concl in - let val0,mv = Tacmach.extract_open_pftreestate pftst in - reset_ids () ; - let inner_types = ref [] in - Xml.pp - (print_current_proof val0 typ str mv inner_types) - fn ; - Xml.pp (pp_cmds_of_inner_types !inner_types ("?" ^ str ^ "?")) - (types_filename_of_filename fn) -;; - -(* FUNCTIONS TO PRINT AN ENTIRE SECTION OF COQ *) - -(* list of (name, uncooked sp, most cooked sp, uncooked leaf object, *) -(* list of possible variables, directory name) *) -(* used to collect informations on the uncooked and most cooked forms *) -(* of objects that could be cooked (have namesakes) *) -let printed = ref [];; - -(* makes a filename from a directory name, a section path and an extension *) -let mkfilename dn sp ext = - let dir_list_of_dirpath s = - let rec aux n = - try - let pos = String.index_from s n '/' in - let head = String.sub s n (pos - n) in - head::(aux (pos + 1)) - with - Not_found -> [String.sub s n (String.length s - n)] - in - aux 0 - in - let rec join_dirs cwd = - function - [] -> assert false - | [he] -> "/" ^ he - | he::tail -> - let newcwd = cwd ^ "/" ^ he in - (try - Unix.mkdir newcwd 0o775 - with _ -> () (* Let's ignore the errors on mkdir *) - ) ; - "/" ^ he ^ join_dirs newcwd tail - in - let module L = Library in - let module S = System in - let module N = Names in - let module No = Nameops in - match dn with - None -> None - | Some basedir -> - let dir0 = No.extend_dirpath (No.dirpath sp) (No.basename sp) in - let dir = List.map N.string_of_id (List.rev (N.repr_dirpath dir0)) in - Some (basedir ^ join_dirs basedir dir ^ "." ^ ext) -;; - -(* print_object leaf_object id section_path directory_name formal_vars *) -(* where leaf_object is a leaf object *) -(* and id is the identifier (name) of the definition/theorem *) -(* or of the inductive definition o *) -(* and section_path is the section path of o *) -(* and directory_name is the base directory in which putting the print *) -(* and formal_vars is the list of parameters (variables) of o *) -(* pretty prints via Xml.pp the object o in the right directory deduced *) -(* from directory_name and section_path *) -(* Note: it is printed only the uncooked available form of the object plus *) -(* the list of parameters of the object deduced from it's most cooked *) -(* form *) -let print_object lobj id sp dn fv env = - let module D = Declarations in - let module E = Environ in - let module G = Global in - let module N = Names in - let module T = Term in - let module X = Xml in - let strtag = Libobject.object_tag lobj in - try - let tag = tag_of_string_tag strtag in - reset_ids () ; - let inner_types = ref [] in - let pp_cmds = - match strtag with - "CONSTANT" (* = Definition, Theorem *) - | "PARAMETER" (* = Axiom *) -> - let {D.const_body=val0 ; D.const_type = typ ; D.const_hyps = hyps} = - G.lookup_constant sp - in - let hyps = string_list_of_named_context_list hyps in - let typ = T.body_of_type typ in - begin - match val0 with - None -> print_axiom id typ fv hyps env inner_types - | Some c -> print_definition id c typ fv hyps env inner_types - end - | "INDUCTIVE" -> - let - {D.mind_packets=packs ; - D.mind_hyps = hyps; - D.mind_finite = finite - } = G.lookup_mind sp - in - let hyps = string_list_of_named_context_list hyps in - print_mutual_inductive finite packs fv hyps env inner_types - | "VARIABLE" -> - let (_,(_,varentry,_)) = Declare.out_variable lobj in - begin - match varentry with - Declare.SectionLocalDef (body,optt) -> - let typ = match optt with - | None -> Retyping.get_type_of env Evd.empty body - | Some t -> t in - add_to_pvars (Definition (N.string_of_id id, body, typ)) ; - print_variable id (Some body) typ env inner_types - | Declare.SectionLocalAssum typ -> - add_to_pvars (Assumption (N.string_of_id id, typ)) ; - print_variable id None (T.body_of_type typ) env inner_types - end - | "CLASS" - | "COERCION" - | _ -> raise Uninteresting - and fileext () = ext_of_tag tag in - let fn = (mkfilename dn sp (fileext ())) in - Xml.pp pp_cmds fn ; - Xml.pp (pp_cmds_of_inner_types !inner_types (uri_of_path sp tag)) - (types_filename_of_filename fn) - with - Uninteresting -> () -;; - -(* print_library_segment state bprintleaf directory_name *) -(* where state is a list of (section-path, node) *) -(* and bprintleaf is true iff the leaf objects should be printed *) -(* and directory_name is the name of the base directory in which to print *) -(* the files *) -(* print via print_node all the nodes (leafs excluded if bprintleaf is false) *)(* in state *) -let rec print_library_segment state bprintleaf dn = - List.iter - (function (sp, node) -> - print_if_verbose ("Print_library_segment: " ^ Names.string_of_path sp ^ "\n") ; - print_node node (Nameops.basename sp) sp bprintleaf dn ; - print_if_verbose "\n" - ) (List.rev state) -(* print_node node id section_path bprintleaf directory_name *) -(* prints a single node (and all it's subnodes via print_library_segment *) -and print_node n id sp bprintleaf dn = - let module L = Lib in - match n with - L.Leaf o -> - print_if_verbose "LEAF\n" ; - if bprintleaf then - begin - if not (List.mem id !printed) then - (* this is an uncooked term or a local (with no namesakes) term *) - begin -try - if could_have_namesakes o sp then - begin - (* this is an uncooked term *) - print_if_verbose ("OK, stampo solo questa volta " ^ Names.string_of_id id ^ "\n") ; - print_object o id sp dn !pvars !cumenv ; - printed := id::!printed - end - else - begin - (* this is a local term *) - print_if_verbose ("OK, stampo " ^ Names.string_of_id id ^ "\n") ; - print_object o id sp dn !pvars !cumenv - end -with _ -> print_if_verbose ("EXCEPTION RAISED!!!\n"); - end - else - begin - (* update the least cooked sp *) - print_if_verbose ("Suppongo gia' stampato " ^ Names.string_of_id id ^ "\n") - end - end - | L.OpenedSection (dir,_) -> - let id = snd (Nameops.split_dirpath dir) in - print_if_verbose ("OpenDir " ^ Names.string_of_id id ^ "\n") - | L.ClosedSection (_,dir,state) -> - let id = snd (Nameops.split_dirpath dir) in - print_if_verbose("ClosedDir " ^ Names.string_of_id id ^ "\n") ; - if bprintleaf then - begin - (* open a new scope *) - pvars := []::!pvars ; - print_library_segment state bprintleaf dn ; - (* close the scope *) - match !pvars with - [] -> assert false - | he::tl -> pvars := tl - end ; - print_if_verbose "/ClosedDir\n" - | L.Module s -> - print_if_verbose ("Module " ^ (Names.string_of_dirpath s) ^ "\n") - | L.FrozenState _ -> - print_if_verbose ("FrozenState\n") -;; - -(* print_closed_section module_name node directory_name *) -(* where module_name is the name of a module *) -(* and node is the library segment of the module *) -(* and directory_name is the base directory in which to put the xml files *) -(* prints all the leaf objects of the tree rooted in node using *) -(* print_library_segment on all its sons *) -let print_closed_section s ls dn = - let module L = Lib in - printed := [] ; - pvars := [[]] ; - cumenv := Safe_typing.env_of_safe_env (Global.safe_env ()) ; - print_if_verbose ("Module " ^ s ^ ":\n") ; - print_library_segment ls true dn ; - print_if_verbose "\n/Module\n" ; -;; - -(* printModule identifier directory_name *) -(* where identifier is the name of a module (section) d *) -(* and directory_name is the directory in which to root all the xml files *) -(* prints all the xml files and directories corresponding to the subsections *) -(* and terms of the module d *) -(* Note: the terms are printed in their uncooked form plus the informations *) -(* on the parameters of their most cooked form *) -let printModule qid dn = - let module L = Library in - let module N = Nametab in - let module X = Xml in - - let (_,dir_path,_) = L.locate_qualified_library qid in - - let str = N.string_of_qualid qid in - let ls = L.module_segment (Some dir_path) in - print_if_verbose ("MODULE_BEGIN " ^ str ^ " " ^ - (L.module_full_filename dir_path) ^ "\n") ; - print_closed_section str (List.rev ls) dn ; - print_if_verbose ("MODULE_END " ^ str ^ " " ^ - (L.module_full_filename dir_path) ^ "\n") -;; - -(* printSection identifier directory_name *) -(* where identifier is the name of a closed section d *) -(* and directory_name is the directory in which to root all the xml files *) -(* prints all the xml files and directories corresponding to the subsections *) -(* and terms of the closed section d *) -(* Note: the terms are printed in their uncooked form plus the informations *) -(* on the parameters of their most cooked form *) -let printSection id dn = - let module L = Library in - let module N = Names in - let module No = Nameops in - let module X = Xml in - let sp = Lib.make_path id in - let ls = - let rec find_closed_section = - function - [] -> raise Not_found - | (_,Lib.ClosedSection (_,dir,ls))::_ when snd (No.split_dirpath dir) = id - -> ls - | _::t -> find_closed_section t - in - print_string ("Searching " ^ Names.string_of_path sp ^ "\n") ; - find_closed_section (Lib.contents_after None) - in - let str = N.string_of_id id in - print_if_verbose ("SECTION_BEGIN " ^ str ^ " " ^ N.string_of_path sp ^ "\n"); - print_closed_section str ls dn ; - print_if_verbose ("SECTION_END " ^ str ^ " " ^ N.string_of_path sp ^ "\n") -;; - -(* print All () prints what is the structure of the current environment of *) -(* Coq. No terms are printed. Useful only for debugging *) -let printAll () = - let state = Library.module_segment None in - let oldverbose = !verbose in - verbose := true ; - print_library_segment state false None ; -(* - let ml = Library.loaded_modules () in - List.iter (function i -> printModule (Names.id_of_string i) None) ml ; -*) - verbose := oldverbose -;; diff --git a/contrib/xml/xmlcommand.ml4 b/contrib/xml/xmlcommand.ml4 new file mode 100644 index 0000000000..7b6303130b --- /dev/null +++ b/contrib/xml/xmlcommand.ml4 @@ -0,0 +1,1037 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* *) +(* 06/12/2000 *) +(* *) +(******************************************************************************) + + +(* CONFIGURATION PARAMETERS *) + +let dtdname = "http://www.cs.unibo.it/helm/dtd/cic.dtd";; +let typesdtdname = "http://www.cs.unibo.it/helm/dtd/cictypes.dtd";; +let verbose = ref false;; (* always set to true during a "Print XML All" *) + +(* UTILITY FUNCTIONS *) + +let print_if_verbose s = if !verbose then print_string s;; + +type tag = + Constant + | Inductive + | Variable +;; + +(* Next exception is used only inside print_object and tag_of_string_tag *) +exception Uninteresting;; + +let tag_of_string_tag = + function + "CONSTANT" + | "PARAMETER" -> Constant + | "INDUCTIVE" -> Inductive + | "VARIABLE" -> Variable + | _ -> raise Uninteresting +;; + +let ext_of_tag = + function + Constant -> "con" + | Inductive -> "ind" + | Variable -> "var" +;; + +(* Internally, for Coq V7, params of inductive types are associated *) +(* not to the whole block of mutual inductive (as it was in V6) but to *) +(* each member of the block; but externally, all params are required *) +(* to be the same; the following function checks that the parameters *) +(* of each inductive of a same block are all the same, then returns *) +(* this number; it fails otherwise *) +let extract_nparams pack = + let module D = Declarations in + let module U = Util in + let module S = Sign in + + let {D.mind_nparams=nparams0} = pack.(0) in + let arity0 = pack.(0).D.mind_user_arity in + let params0, _ = S.decompose_prod_n_assum nparams0 arity0 in + for i = 1 to Array.length pack - 1 do + let {D.mind_nparams=nparamsi} = pack.(i) in + let arityi = pack.(i).D.mind_user_arity in + let paramsi, _ = S.decompose_prod_n_assum nparamsi arityi in + if params0 <> paramsi then U.error "Cannot convert a block of inductive definitions with parameters specific to each inductive to a block of mutual inductive definitions with parameters global to the whole block" + done; + nparams0 + +(* could_have_namesakes sp = true iff o is an object that could be cooked and *) +(* than that could exists in cooked form with the same name in a super *) +(* section of the actual section *) +let could_have_namesakes o sp = (* namesake = omonimo in italian *) + let module D = Declare in + let tag = Libobject.object_tag o in + print_if_verbose ("Object tag: " ^ tag ^ "\n") ; + match tag with + "CONSTANT" -> + (match D.constant_strength sp with + | D.DischargeAt _ -> false (* a local definition *) + | D.NotDeclare -> false (* not a definition *) + | D.NeverDischarge -> true (* a non-local one *) + ) + | "PARAMETER" (* axioms and *) + | "INDUCTIVE" -> true (* mutual inductive types are never local *) + | "VARIABLE" -> false (* variables are local, so no namesakes *) + | _ -> false (* uninteresting thing that won't be printed*) +;; + + +(* uri_of_path sp is a broken (wrong) uri pointing to the object whose *) +(* section path is sp *) +let uri_of_path sp tag = + let module N = Names in + let module No = Nameops in + let ext_of_sp sp = ext_of_tag tag in + let dir0 = No.extend_dirpath (No.dirpath sp) (No.basename sp) in + let dir = List.map N.string_of_id (List.rev (N.repr_dirpath dir0)) in + "cic:/" ^ (String.concat "/" dir) ^ "." ^ (ext_of_sp sp) +;; + +let string_of_sort = + let module T = Term in + function + T.Prop(T.Pos) -> "Set" + | T.Prop(T.Null) -> "Prop" + | T.Type(_) -> "Type" +;; + +let string_of_name = + let module N = Names in + function + N.Name id -> N.string_of_id id + | _ -> Util.anomaly "this should not happen" +;; + +(* A SIMPLE DATA STRUCTURE AND SOME FUNCTIONS TO MANAGE THE CURRENT *) +(* ENVIRONMENT (= [l1, ..., ln] WHERE li IS THE LIST OF VARIABLES *) +(* DECLARED IN THE i-th SUPER-SECTION OF THE CURRENT SECTION *) + +(*CSC: commento sbagliato ed obsoleto *) +(* list of variables availables in the actual section *) +let pvars = ref ([[]] : string list list);; +let cumenv = ref Environ.empty_env;; + +let string_of_vars_list = + let add_prefix n s = string_of_int n ^ ": " ^ s in + let rec aux = + function + [n,v] -> (n,v) + | (n,v)::tl -> + let (k,s) = aux tl in + if k = n then (k, v ^ " " ^ s) else (n, v ^ " " ^ add_prefix k s) + | [] -> assert false + in + function + [] -> "" + | vl -> let (k,s) = aux vl in add_prefix k s +;; + +(* +let string_of_pvars pvars hyps = + let rec aux = + function + [] -> (0, "") + | he::tl -> + let (n,s) = aux tl in + (n + 1, + string_of_int n ^ ": " ^ (String.concat " ") (List.rev he) ^ + match s with "" -> "" | _ -> " " ^ s + ) + in + snd (aux (List.rev pvars)) +;; +*) + +let string_of_pvars pvars hyps = + let find_depth pvars v = + let rec aux n = + function + [] -> assert false +(* (-1,"?") For Print XML *) +(* +print_string "\nPVARS:" ; +List.iter (List.iter print_string) pvars ; +print_string "\nHYPS:" ; +List.iter print_string hyps ; +print_string "\n" ; +flush stdout ; +assert false +*) + | l::_ when List.mem v l -> (n,v) + | _::tl -> aux (n+1) tl + in + aux 0 pvars + in + string_of_vars_list (List.map (find_depth pvars) (List.rev hyps)) +;; + +type variables_type = + Definition of string * Term.constr * Term.types + | Assumption of string * Term.constr +;; + +let add_to_pvars x = + let module E = Environ in + let v = + match x with + Definition (v, bod, typ) -> + cumenv := + E.push_named_decl (Names.id_of_string v, Some bod, typ) !cumenv ; + v + | Assumption (v, typ) -> + cumenv := + E.push_named_decl (Names.id_of_string v, None, typ) !cumenv ; + v + in + match !pvars with + [] -> assert false + | (he::tl) -> pvars := (v::he)::tl +;; + +let get_depth_of_var v = + let rec aux n = + function + [] -> None + | (he::tl) -> if List.mem v he then Some n else aux (n + 1) tl + in + aux 0 !pvars +;; + +(* FUNCTIONS TO CREATE IDENTIFIERS *) + +(* seed to create the next identifier *) +let next_id_cic = ref 0;; +let next_id_types = ref 0;; + +(* reset_ids () reset the identifier seed to 0 *) +let reset_ids () = + next_id_cic := 0 ; + next_id_types := 0 +;; + +(* get_next_id () returns fresh identifier *) +let get_next_id = + function + `T -> + let res = + "t" ^ string_of_int !next_id_types + in + incr next_id_types ; + res + | `I -> + let res = + "i" ^ string_of_int !next_id_cic + in + incr next_id_cic ; + res +;; + +type innersort = + InnerProp of Term.constr (* the constr is the type of the term *) + | InnerSet + | InnerType +;; + +(* FUNCTION TO PRINT A SINGLE TERM OF CIC *) +(* print_term t l where t is a term of Cic returns a stream of XML tokens *) +(* suitable to be printed via the pretty printer Xml.pp. l is the list of *) +(* bound names *) +let print_term inner_types l env csr = + let module N = Names in + let module E = Environ in + let module T = Term in + let module X = Xml in + let module R = Retyping in + let rec names_to_ids = + function + [] -> [] + | (N.Name id)::l -> id::(names_to_ids l) + | _ -> names_to_ids l + in + + let inner_type_display env term = + let type_of_term = + Reduction.nf_betaiota (R.get_type_of env (Evd.empty) term) + in + match R.get_sort_family_of env (Evd.empty) type_of_term with + T.InProp -> InnerProp type_of_term + | T.InSet -> InnerSet + | T.InType -> InnerType + in + +(*WHICH FORCE FUNCTION DEPENDS ON THE ORDERING YOU WANT + let rec force = + parser + [< 'he ; tl >] -> let tl = (force tl) in [< 'he ; tl >] + | [< >] -> [<>] + in +*) + let force x = x in + + let rec term_display idradix in_lambda l env cstr = + let next_id = get_next_id idradix in + let add_sort_attribute do_output_type l' = + let xmlinnertype = inner_type_display env cstr in + match xmlinnertype with + InnerProp type_of_term -> + if do_output_type & idradix = `I then + begin + let pp_cmds = term_display `T false l env type_of_term in + inner_types := (next_id, pp_cmds)::!inner_types ; + end ; + ("sort","Prop")::l' + | InnerSet -> ("sort","Set")::l' + | InnerType -> ("sort","Type")::l' + in + let add_type_attribute l' = + ("type", string_of_sort (R.get_sort_of env (Evd.empty) cstr))::l' + in + (* kind_of_term helps doing pattern matching hiding the lower level of *) + (* coq coding of terms (the one of the logical framework) *) + match T.kind_of_term cstr with + T.Rel n -> + let id = + match List.nth l (n - 1) with + N.Name id -> id + | N.Anonymous -> Nameops.make_ident "_" None + in + X.xml_empty "REL" + (add_sort_attribute false + ["value",(string_of_int n) ; + "binder",(N.string_of_id id) ; + "id", next_id]) + | T.Var id -> + let depth = + match get_depth_of_var (N.string_of_id id) with + None -> "?" (* when printing via Show XML Proof or Print XML id *) + (* no infos about variables uri are known *) +(*V7 posso usare nametab, forse*) + | Some n -> string_of_int n + in + X.xml_empty "VAR" + (add_sort_attribute false + ["relUri",depth ^ "," ^ (N.string_of_id id) ; + "id", next_id]) + | T.Meta n -> + X.xml_empty "META" + (add_sort_attribute false ["no",(string_of_int n) ; "id", next_id]) + | T.Sort s -> + X.xml_empty "SORT" ["value",(string_of_sort s) ; "id", next_id] + | T.Cast (t1,t2) -> + X.xml_nempty "CAST" (add_sort_attribute false ["id", next_id]) +(force + [< X.xml_nempty "term" [] (term_display idradix false l env t1) ; + X.xml_nempty "type" [] (term_display idradix false l env t2) + >] +) + | T.LetIn (nid,s,t,d)-> + let nid' = Nameops.next_name_away nid (names_to_ids l) in + X.xml_nempty "LETIN" (add_sort_attribute true ["id", next_id]) +(force + [< X.xml_nempty "term" [] (term_display idradix false l env s) ; + X.xml_nempty "letintarget" ["binder",(N.string_of_id nid')] + (term_display idradix false + ((N.Name nid')::l) + (E.push_rel (N.Name nid', Some s, t) env) + d + ) + >] +) + | T.Prod (N.Name _ as nid, t1, t2) -> + let nid' = Nameops.next_name_away nid (names_to_ids l) in + X.xml_nempty "PROD" (add_type_attribute ["id", next_id]) +(force + [< X.xml_nempty "source" [] (term_display idradix false l env t1) ; + X.xml_nempty "target" + (if idradix = `T && + T.noccurn 1 t2 + then [] + else ["binder",(N.string_of_id nid')]) + (term_display idradix false + ((N.Name nid')::l) + (E.push_rel (N.Name nid', None, t1) env) + t2 + ) + >] +) + | T.Prod (N.Anonymous as nid, t1, t2) -> + X.xml_nempty "PROD" (add_type_attribute ["id", next_id]) +(force + [< X.xml_nempty "source" [] (term_display idradix false l env t1) ; + X.xml_nempty "target" [] + (term_display idradix false + (nid::l) + (E.push_rel (nid, None, t1) env) + t2 + ) + >] +) + | T.Lambda (N.Name _ as nid, t1, t2) -> + let nid' = Nameops.next_name_away nid (names_to_ids l) in + X.xml_nempty "LAMBDA" (add_sort_attribute (not in_lambda) ["id",next_id]) +(force + [< X.xml_nempty "source" [] (term_display idradix false l env t1) ; + X.xml_nempty "target" ["binder",(N.string_of_id nid')] + (term_display idradix true + ((N.Name nid')::l) + (E.push_rel (N.Name nid', None, t1) env) + t2 + ) + >] +) + | T.Lambda (N.Anonymous as nid, t1, t2) -> + X.xml_nempty "LAMBDA" (add_sort_attribute (not in_lambda) ["id", next_id]) +(force + [< X.xml_nempty "source" [] (term_display idradix false l env t1) ; + X.xml_nempty "target" [] + (term_display idradix true + (nid::l) + (E.push_rel (nid, None, t1) env) + t2 + ) + >] +) + | T.App (h,t) -> + X.xml_nempty "APPLY" (add_sort_attribute true ["id", next_id]) +(force + [< (term_display idradix false l env h) ; + (Array.fold_right + (fun x i -> [< (term_display idradix false l env x); i >]) t [<>]) + >] +) + | T.Const sp -> + X.xml_empty "CONST" + (add_sort_attribute false + ["uri",(uri_of_path sp Constant) ; "id", next_id]) + | T.Ind (sp,i) -> + X.xml_empty "MUTIND" + ["uri",(uri_of_path sp Inductive) ; + "noType",(string_of_int i) ; + "id", next_id] + | T.Construct ((sp,i),j) -> + X.xml_empty "MUTCONSTRUCT" + (add_sort_attribute false + ["uri",(uri_of_path sp Inductive) ; + "noType",(string_of_int i) ; + "noConstr",(string_of_int j) ; + "id", next_id]) + | T.Case ({T.ci_ind=(sp,i)},ty,term,a) -> + let (uri, typeno) = (uri_of_path sp Inductive),i in + X.xml_nempty "MUTCASE" + (add_sort_attribute true + ["uriType",uri ; "noType",(string_of_int typeno) ; "id",next_id]) +(force + [< X.xml_nempty "patternsType" [] + [< (term_display idradix false l env ty) >] ; + X.xml_nempty "inductiveTerm" [] + [< (term_display idradix false l env term)>]; + Array.fold_right + (fun x i -> + [< X.xml_nempty "pattern" [] + [] ; i>] + ) a [<>] + >] +) + | T.Fix ((ai,i),((f,t,b) as rec_decl)) -> + X.xml_nempty "FIX" + (add_sort_attribute true ["noFun", (string_of_int i) ; "id",next_id]) +(force + [< Array.fold_right + (fun (fi,ti,bi,ai) i -> + [< X.xml_nempty "FixFunction" + ["name", (string_of_name fi); "recIndex", (string_of_int ai)] + [< X.xml_nempty "type" [] + [< term_display idradix false l env ti >] ; + X.xml_nempty "body" [] [< + term_display idradix false + ((Array.to_list f)@l) + (E.push_rec_types rec_decl env) + bi + >] + >] ; + i + >] + ) + (Array.mapi (fun j x -> (x,t.(j),b.(j),ai.(j)) ) f ) + [<>] + >] +) + | T.CoFix (i,((f,t,b) as rec_decl)) -> + X.xml_nempty "COFIX" + (add_sort_attribute true ["noFun", (string_of_int i) ; "id",next_id]) +(force + [< Array.fold_right + (fun (fi,ti,bi) i -> + [< X.xml_nempty "CofixFunction" ["name", (string_of_name fi)] + [< X.xml_nempty "type" [] + [< term_display idradix false l env ti >] ; + X.xml_nempty "body" [] [< + term_display idradix false + ((Array.to_list f)@l) + (E.push_rec_types rec_decl env) + bi + >] + >] ; + i + >] + ) + (Array.mapi (fun j x -> (x,t.(j),b.(j)) ) f ) [<>] + >] +) + | T.Evar _ -> + Util.anomaly "Evar node in a term!!!" + in + (*CSC: ad l vanno andrebbero aggiunti i nomi da non *) + (*CSC: mascherare (costanti? variabili?) *) + term_display `I false l env csr +;; + +(* FUNCTIONS TO PRINT A SINGLE OBJECT OF COQ *) + +(* print_current_proof term type id conjectures *) +(* where term is the term of the proof in progress p *) +(* and type is the type of p *) +(* and id is the identifier (name) of p *) +(* and conjectures is the list of conjectures (cic terms) *) +(* returns a stream of XML tokens suitable to be pretty printed via Xml.pp *) +let print_current_proof c typ id mv inner_types = + let module X = Xml in + let env = (Safe_typing.env_of_safe_env (Global.safe_env ())) in + [< X.xml_cdata "\n" ; + X.xml_cdata ("\n\n") ; + X.xml_nempty "CurrentProof" ["name",id ; "id", get_next_id `I] + [< List.fold_right + (fun (j,t) i -> + [< X.xml_nempty "Conjecture" ["no",(string_of_int j)] + [< print_term inner_types [] env t >] ; i >]) + mv [<>] ; + X.xml_nempty "body" [] [< print_term inner_types [] env c >] ; + X.xml_nempty "type" [] [< print_term inner_types [] env typ >] + >] + >] +;; + +(* print_axiom id type params *) +(* where type is the type of an axiom a *) +(* and id is the identifier (name) of a *) +(* and params is the list of formal params for a *) +(* returns a stream of XML tokens suitable to be pretty printed via Xml.pp *) +let print_axiom id typ fv hyps env inner_types = + let module X = Xml in + let module N = Names in + [< X.xml_cdata "\n" ; + X.xml_cdata ("\n\n") ; + X.xml_nempty "Axiom" + ["name",(N.string_of_id id) ; + "id", get_next_id `I ; + "params",(string_of_pvars fv hyps)] + [< X.xml_nempty "type" [] (print_term inner_types [] env typ) >] + >] +;; + +(* print_definition id term type params hyps *) +(* where id is the identifier (name) of a definition d *) +(* and term is the term (body) of d *) +(* and type is the type of d *) +(* and params is the list of formal params for d *) +(* returns a stream of XML tokens suitable to be pretty printed via Xml.pp *) +let print_definition id c typ fv hyps env inner_types = + let module X = Xml in + let module N = Names in + [< X.xml_cdata "\n" ; + X.xml_cdata ("\n\n") ; + X.xml_nempty "Definition" + ["name",(N.string_of_id id) ; + "id", get_next_id `I ; + "params",(string_of_pvars fv hyps)] + [< X.xml_nempty "body" [] (print_term inner_types [] env c) ; + X.xml_nempty "type" [] (print_term inner_types [] env typ) >] + >] +;; + +(* print_variable id type *) +(* where id is the identifier (name) of a variable v *) +(* and type is the type of v *) +(* returns a stream of XML tokens suitable to be pretty printed via Xml.pp *) +let print_variable id body typ env inner_types = + let module X = Xml in + let module N = Names in + [< X.xml_cdata "\n" ; + X.xml_cdata ("\n\n") ; + X.xml_nempty "Variable" ["name",(N.string_of_id id); "id", get_next_id `I] + [< (match body with + None -> [<>] + | Some body -> + X.xml_nempty "body" [] (print_term inner_types [] env body) + ) ; + X.xml_nempty "type" [] (print_term inner_types [] env typ) + >] + >] +;; + +(* print_mutual_inductive_packet p *) +(* where p is a mutual inductive packet (an inductive definition in a block *) +(* of mutual inductive definitions) *) +(* returns a stream of XML tokens suitable to be pretty printed via Xml.pp *) +(* Used only by print_mutual_inductive *) +let print_mutual_inductive_packet inner_types names env finite p = + let module D = Declarations in + let module N = Names in + let module T = Term in + let module X = Xml in + let {D.mind_consnames=consnames ; + D.mind_typename=typename ; + D.mind_nf_lc=lc ; + D.mind_nf_arity=arity} = p + in + [< X.xml_nempty "InductiveType" + ["name",(N.string_of_id typename) ; + "inductive",(string_of_bool finite) + ] + [< + X.xml_nempty "arity" [] + (print_term inner_types [] env (T.body_of_type arity)) ; + (Array.fold_right + (fun (name,lc) i -> + [< X.xml_nempty "Constructor" ["name",(N.string_of_id name)] + (print_term inner_types names env lc) ; + i + >]) + (Array.mapi (fun j x -> (x,T.body_of_type lc.(j)) ) consnames ) + [<>] + ) + >] + >] +;; + +(* print_mutual_inductive packs params nparams *) +(* where packs is the list of inductive definitions in the block of *) +(* mutual inductive definitions b *) +(* and params is the list of formal params for b *) +(* and nparams is the number of "parameters" in the arity of the *) +(* mutual inductive types *) +(* returns a stream of XML tokens suitable to be pretty printed via Xml.pp *) +let print_mutual_inductive finite packs fv hyps env inner_types = + let module D = Declarations in + let module E = Environ in + let module X = Xml in + let module N = Names in + let nparams = extract_nparams packs in + let names = + List.map + (fun p -> let {D.mind_typename=typename} = p in N.Name(typename)) + (Array.to_list packs) + in + let env = + List.fold_right + (fun {D.mind_typename=typename ; D.mind_nf_arity=arity} env -> + E.push_rel (N.Name typename, None, arity) env) + (Array.to_list packs) + env + in + [< X.xml_cdata "\n" ; + X.xml_cdata ("\n\n") ; + X.xml_nempty "InductiveDefinition" + ["noParams",string_of_int nparams ; + "id",get_next_id `I ; + "params",(string_of_pvars fv hyps)] + [< (Array.fold_right + (fun x i -> + [< print_mutual_inductive_packet + inner_types names env finite x ; i >] + ) packs [< >] + ) + >] + >] +;; + +let string_list_of_named_context_list = + List.map + (function (n,_,_) -> Names.string_of_id n) +;; + +let types_filename_of_filename = + function + Some f -> Some (f ^ ".types") + | None -> None +;; + +let pp_cmds_of_inner_types inner_types target_uri = + let module X = Xml in + let rec stream_of_list = + function + [] -> [<>] + | he::tl -> [< he ; stream_of_list tl >] + in + [< X.xml_cdata "\n" ; + X.xml_cdata ("\n\n"); + X.xml_nempty "InnerTypes" ["of",target_uri] + (stream_of_list + (List.map + (function + (id,type_pp_cmds) -> X.xml_nempty "TYPE" ["of",id] type_pp_cmds) + (List.rev inner_types) + )) + >] +;; + +(* print id dest *) +(* where sp is the qualified identifier (section path) of a *) +(* definition/theorem, variable or inductive definition *) +(* and dest is either None (for stdout) or (Some filename) *) +(* pretty prints via Xml.pp the object whose identifier is id on dest *) +(* Note: it is printed only (and directly) the most cooked available *) +(* form of the definition (all the parameters are *) +(* lambda-abstracted, but the object can still refer to variables) *) +let print qid fn = + let module D = Declarations in + let module G = Global in + let module N = Names in + let module Nt = Nametab in + let module T = Term in + let module X = Xml in + let (_,id) = Nt.repr_qualid qid in + let glob_ref = Nametab.locate qid in + let env = (Safe_typing.env_of_safe_env (G.safe_env ())) in + reset_ids () ; + let inner_types = ref [] in + let sp,tag,pp_cmds = + match glob_ref with + Nt.VarRef id -> + let sp = Declare.find_section_variable id in + let (_,body,typ) = G.lookup_named id in + sp,Variable,print_variable id body (T.body_of_type typ) env inner_types + | Nt.ConstRef sp -> + let {D.const_body=val0 ; D.const_type = typ ; D.const_hyps = hyps} = + G.lookup_constant sp in + let hyps = string_list_of_named_context_list hyps in + let typ = T.body_of_type typ in + sp,Constant, + begin + match val0 with + None -> print_axiom id typ [] hyps env inner_types + | Some c -> print_definition id c typ [] hyps env inner_types + end + | Nt.IndRef (sp,_) -> + let {D.mind_packets=packs ; + D.mind_hyps=hyps; + D.mind_finite=finite} = G.lookup_mind sp in + let hyps = string_list_of_named_context_list hyps in + sp,Inductive, + print_mutual_inductive finite packs [] hyps env inner_types + | Nt.ConstructRef _ -> + Util.anomaly ("print: this should not happen") + in + Xml.pp pp_cmds fn ; + Xml.pp (pp_cmds_of_inner_types !inner_types (uri_of_path sp tag)) + (types_filename_of_filename fn) +;; + +(* show dest *) +(* where dest is either None (for stdout) or (Some filename) *) +(* pretty prints via Xml.pp the proof in progress on dest *) +let show fn = + let pftst = Pfedit.get_pftreestate () in + let str = Names.string_of_id (Pfedit.get_current_proof_name ()) in + let pf = Tacmach.proof_of_pftreestate pftst in + let typ = (Proof_trees.goal_of_proof pf).Evd.evar_concl in + let val0,mv = Tacmach.extract_open_pftreestate pftst in + reset_ids () ; + let inner_types = ref [] in + Xml.pp + (print_current_proof val0 typ str mv inner_types) + fn ; + Xml.pp (pp_cmds_of_inner_types !inner_types ("?" ^ str ^ "?")) + (types_filename_of_filename fn) +;; + +(* FUNCTIONS TO PRINT AN ENTIRE SECTION OF COQ *) + +(* list of (name, uncooked sp, most cooked sp, uncooked leaf object, *) +(* list of possible variables, directory name) *) +(* used to collect informations on the uncooked and most cooked forms *) +(* of objects that could be cooked (have namesakes) *) +let printed = ref [];; + +(* makes a filename from a directory name, a section path and an extension *) +let mkfilename dn sp ext = + let dir_list_of_dirpath s = + let rec aux n = + try + let pos = String.index_from s n '/' in + let head = String.sub s n (pos - n) in + head::(aux (pos + 1)) + with + Not_found -> [String.sub s n (String.length s - n)] + in + aux 0 + in + let rec join_dirs cwd = + function + [] -> assert false + | [he] -> "/" ^ he + | he::tail -> + let newcwd = cwd ^ "/" ^ he in + (try + Unix.mkdir newcwd 0o775 + with _ -> () (* Let's ignore the errors on mkdir *) + ) ; + "/" ^ he ^ join_dirs newcwd tail + in + let module L = Library in + let module S = System in + let module N = Names in + let module No = Nameops in + match dn with + None -> None + | Some basedir -> + let dir0 = No.extend_dirpath (No.dirpath sp) (No.basename sp) in + let dir = List.map N.string_of_id (List.rev (N.repr_dirpath dir0)) in + Some (basedir ^ join_dirs basedir dir ^ "." ^ ext) +;; + +(* print_object leaf_object id section_path directory_name formal_vars *) +(* where leaf_object is a leaf object *) +(* and id is the identifier (name) of the definition/theorem *) +(* or of the inductive definition o *) +(* and section_path is the section path of o *) +(* and directory_name is the base directory in which putting the print *) +(* and formal_vars is the list of parameters (variables) of o *) +(* pretty prints via Xml.pp the object o in the right directory deduced *) +(* from directory_name and section_path *) +(* Note: it is printed only the uncooked available form of the object plus *) +(* the list of parameters of the object deduced from it's most cooked *) +(* form *) +let print_object lobj id sp dn fv env = + let module D = Declarations in + let module E = Environ in + let module G = Global in + let module N = Names in + let module T = Term in + let module X = Xml in + let strtag = Libobject.object_tag lobj in + try + let tag = tag_of_string_tag strtag in + reset_ids () ; + let inner_types = ref [] in + let pp_cmds = + match strtag with + "CONSTANT" (* = Definition, Theorem *) + | "PARAMETER" (* = Axiom *) -> + let {D.const_body=val0 ; D.const_type = typ ; D.const_hyps = hyps} = + G.lookup_constant sp + in + let hyps = string_list_of_named_context_list hyps in + let typ = T.body_of_type typ in + begin + match val0 with + None -> print_axiom id typ fv hyps env inner_types + | Some c -> print_definition id c typ fv hyps env inner_types + end + | "INDUCTIVE" -> + let + {D.mind_packets=packs ; + D.mind_hyps = hyps; + D.mind_finite = finite + } = G.lookup_mind sp + in + let hyps = string_list_of_named_context_list hyps in + print_mutual_inductive finite packs fv hyps env inner_types + | "VARIABLE" -> + let (_,(_,varentry,_)) = Declare.out_variable lobj in + begin + match varentry with + Declare.SectionLocalDef (body,optt) -> + let typ = match optt with + | None -> Retyping.get_type_of env Evd.empty body + | Some t -> t in + add_to_pvars (Definition (N.string_of_id id, body, typ)) ; + print_variable id (Some body) typ env inner_types + | Declare.SectionLocalAssum typ -> + add_to_pvars (Assumption (N.string_of_id id, typ)) ; + print_variable id None (T.body_of_type typ) env inner_types + end + | "CLASS" + | "COERCION" + | _ -> raise Uninteresting + and fileext () = ext_of_tag tag in + let fn = (mkfilename dn sp (fileext ())) in + Xml.pp pp_cmds fn ; + Xml.pp (pp_cmds_of_inner_types !inner_types (uri_of_path sp tag)) + (types_filename_of_filename fn) + with + Uninteresting -> () +;; + +(* print_library_segment state bprintleaf directory_name *) +(* where state is a list of (section-path, node) *) +(* and bprintleaf is true iff the leaf objects should be printed *) +(* and directory_name is the name of the base directory in which to print *) +(* the files *) +(* print via print_node all the nodes (leafs excluded if bprintleaf is false) *)(* in state *) +let rec print_library_segment state bprintleaf dn = + List.iter + (function (sp, node) -> + print_if_verbose ("Print_library_segment: " ^ Names.string_of_path sp ^ "\n") ; + print_node node (Nameops.basename sp) sp bprintleaf dn ; + print_if_verbose "\n" + ) (List.rev state) +(* print_node node id section_path bprintleaf directory_name *) +(* prints a single node (and all it's subnodes via print_library_segment *) +and print_node n id sp bprintleaf dn = + let module L = Lib in + match n with + L.Leaf o -> + print_if_verbose "LEAF\n" ; + if bprintleaf then + begin + if not (List.mem id !printed) then + (* this is an uncooked term or a local (with no namesakes) term *) + begin +try + if could_have_namesakes o sp then + begin + (* this is an uncooked term *) + print_if_verbose ("OK, stampo solo questa volta " ^ Names.string_of_id id ^ "\n") ; + print_object o id sp dn !pvars !cumenv ; + printed := id::!printed + end + else + begin + (* this is a local term *) + print_if_verbose ("OK, stampo " ^ Names.string_of_id id ^ "\n") ; + print_object o id sp dn !pvars !cumenv + end +with _ -> print_if_verbose ("EXCEPTION RAISED!!!\n"); + end + else + begin + (* update the least cooked sp *) + print_if_verbose ("Suppongo gia' stampato " ^ Names.string_of_id id ^ "\n") + end + end + | L.OpenedSection (dir,_) -> + let id = snd (Nameops.split_dirpath dir) in + print_if_verbose ("OpenDir " ^ Names.string_of_id id ^ "\n") + | L.ClosedSection (_,dir,state) -> + let id = snd (Nameops.split_dirpath dir) in + print_if_verbose("ClosedDir " ^ Names.string_of_id id ^ "\n") ; + if bprintleaf then + begin + (* open a new scope *) + pvars := []::!pvars ; + print_library_segment state bprintleaf dn ; + (* close the scope *) + match !pvars with + [] -> assert false + | he::tl -> pvars := tl + end ; + print_if_verbose "/ClosedDir\n" + | L.Module s -> + print_if_verbose ("Module " ^ (Names.string_of_dirpath s) ^ "\n") + | L.FrozenState _ -> + print_if_verbose ("FrozenState\n") +;; + +(* print_closed_section module_name node directory_name *) +(* where module_name is the name of a module *) +(* and node is the library segment of the module *) +(* and directory_name is the base directory in which to put the xml files *) +(* prints all the leaf objects of the tree rooted in node using *) +(* print_library_segment on all its sons *) +let print_closed_section s ls dn = + let module L = Lib in + printed := [] ; + pvars := [[]] ; + cumenv := Safe_typing.env_of_safe_env (Global.safe_env ()) ; + print_if_verbose ("Module " ^ s ^ ":\n") ; + print_library_segment ls true dn ; + print_if_verbose "\n/Module\n" ; +;; + +(* printModule identifier directory_name *) +(* where identifier is the name of a module (section) d *) +(* and directory_name is the directory in which to root all the xml files *) +(* prints all the xml files and directories corresponding to the subsections *) +(* and terms of the module d *) +(* Note: the terms are printed in their uncooked form plus the informations *) +(* on the parameters of their most cooked form *) +let printModule qid dn = + let module L = Library in + let module N = Nametab in + let module X = Xml in + + let (_,dir_path,_) = L.locate_qualified_library qid in + + let str = N.string_of_qualid qid in + let ls = L.module_segment (Some dir_path) in + print_if_verbose ("MODULE_BEGIN " ^ str ^ " " ^ + (L.module_full_filename dir_path) ^ "\n") ; + print_closed_section str (List.rev ls) dn ; + print_if_verbose ("MODULE_END " ^ str ^ " " ^ + (L.module_full_filename dir_path) ^ "\n") +;; + +(* printSection identifier directory_name *) +(* where identifier is the name of a closed section d *) +(* and directory_name is the directory in which to root all the xml files *) +(* prints all the xml files and directories corresponding to the subsections *) +(* and terms of the closed section d *) +(* Note: the terms are printed in their uncooked form plus the informations *) +(* on the parameters of their most cooked form *) +let printSection id dn = + let module L = Library in + let module N = Names in + let module No = Nameops in + let module X = Xml in + let sp = Lib.make_path id in + let ls = + let rec find_closed_section = + function + [] -> raise Not_found + | (_,Lib.ClosedSection (_,dir,ls))::_ when snd (No.split_dirpath dir) = id + -> ls + | _::t -> find_closed_section t + in + print_string ("Searching " ^ Names.string_of_path sp ^ "\n") ; + find_closed_section (Lib.contents_after None) + in + let str = N.string_of_id id in + print_if_verbose ("SECTION_BEGIN " ^ str ^ " " ^ N.string_of_path sp ^ "\n"); + print_closed_section str ls dn ; + print_if_verbose ("SECTION_END " ^ str ^ " " ^ N.string_of_path sp ^ "\n") +;; + +(* print All () prints what is the structure of the current environment of *) +(* Coq. No terms are printed. Useful only for debugging *) +let printAll () = + let state = Library.module_segment None in + let oldverbose = !verbose in + verbose := true ; + print_library_segment state false None ; +(* + let ml = Library.loaded_modules () in + List.iter (function i -> printModule (Names.id_of_string i) None) ml ; +*) + verbose := oldverbose +;; diff --git a/lib/pp.ml b/lib/pp.ml deleted file mode 100644 index 2d4c76d916..0000000000 --- a/lib/pp.ml +++ /dev/null @@ -1,222 +0,0 @@ -(***********************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* nc := 0 (* ascii char *) - | '\128'..'\191' -> nc := 0 (* cannot start with a continuation byte *) - | '\192'..'\223' -> nc := 1 (* expect 1 continuation byte *) - | '\224'..'\239' -> nc := 2 (* expect 2 continuation bytes *) - | '\240'..'\247' -> nc := 3 (* expect 3 continuation bytes *) - | '\248'..'\251' -> nc := 4 (* expect 4 continuation bytes *) - | '\252'..'\253' -> nc := 5 (* expect 5 continuation bytes *) - | '\254'..'\255' -> nc := 0 (* invalid byte *) - end ; - incr p ; - while !p < len && !nc > 0 do - match s.[!p] with - | '\128'..'\191' (* next continuation byte *) -> incr p ; decr nc - | _ (* not a continuation byte *) -> nc := 0 - done ; - incr cnt - done ; - !cnt - -(* formatting commands *) -let str s = [< 'Ppcmd_print (utf8_length s,s) >] -let stras (i,s) = [< 'Ppcmd_print (i,s) >] -let brk (a,b) = [< 'Ppcmd_print_break (a,b) >] -let tbrk (a,b) = [< 'Ppcmd_print_tbreak (a,b) >] -let tab () = [< 'Ppcmd_set_tab >] -let fnl () = [< 'Ppcmd_force_newline >] -let pifb () = [< 'Ppcmd_print_if_broken >] -let ws n = [< 'Ppcmd_white_space n >] - -(* derived commands *) -let spc () = [< 'Ppcmd_print_break (1,0) >] -let cut () = [< 'Ppcmd_print_break (0,0) >] -let align () = [< 'Ppcmd_print_break (0,0) >] -let int n = str (string_of_int n) -let real r = str (string_of_float r) -let bool b = str (string_of_bool b) -let qstring s = str ("\""^(String.escaped s)^"\"") -let qs = qstring -let mt () = [< >] - -(* boxing commands *) -let h n s = [< 'Ppcmd_box(Pp_hbox n,s) >] -let v n s = [< 'Ppcmd_box(Pp_vbox n,s) >] -let hv n s = [< 'Ppcmd_box(Pp_hvbox n,s) >] -let hov n s = [< 'Ppcmd_box(Pp_hovbox n,s) >] -let t s = [< 'Ppcmd_box(Pp_tbox,s) >] - -(* Opening and closing of boxes *) -let hb n = [< 'Ppcmd_open_box(Pp_hbox n) >] -let vb n = [< 'Ppcmd_open_box(Pp_vbox n) >] -let hvb n = [< 'Ppcmd_open_box(Pp_hvbox n) >] -let hovb n = [< 'Ppcmd_open_box(Pp_hovbox n) >] -let tb () = [< 'Ppcmd_open_box Pp_tbox >] -let close () = [< 'Ppcmd_close_box >] -let tclose () = [< 'Ppcmd_close_tbox >] - -let (++) = Stream.iapp - -(* pretty printing functions *) -let pp_dirs ft = - let maxbox = (get_gp ft).max_depth in - let pp_open_box = function - | Pp_hbox n -> Format.pp_open_hbox ft () - | Pp_vbox n -> Format.pp_open_vbox ft n - | Pp_hvbox n -> Format.pp_open_hvbox ft n - | Pp_hovbox n -> Format.pp_open_hovbox ft n - | Pp_tbox -> Format.pp_open_tbox ft () - in - let rec pp_cmd = function - | Ppcmd_print(n,s) -> Format.pp_print_as ft n s - | Ppcmd_box(bty,ss) -> (* Prevent evaluation of the stream! *) - pp_open_box bty ; - if not (Format.over_max_boxes ()) then Stream.iter pp_cmd ss; - Format.pp_close_box ft () - | Ppcmd_open_box bty -> pp_open_box bty - | Ppcmd_close_box -> Format.pp_close_box ft () - | Ppcmd_close_tbox -> Format.pp_close_tbox ft () - | Ppcmd_white_space n -> Format.pp_print_break ft n 0 - | Ppcmd_print_break(m,n) -> Format.pp_print_break ft m n - | Ppcmd_set_tab -> Format.pp_set_tab ft () - | Ppcmd_print_tbreak(m,n) -> Format.pp_print_tbreak ft m n - | Ppcmd_force_newline -> Format.pp_force_newline ft () - | Ppcmd_print_if_broken -> Format.pp_print_if_newline ft () - in - let pp_dir = function - | Ppdir_ppcmds cmdstream -> Stream.iter pp_cmd cmdstream - | Ppdir_print_newline -> Format.pp_print_newline ft () - | Ppdir_print_flush -> Format.pp_print_flush ft () - in - fun dirstream -> - try - Stream.iter pp_dir dirstream - with - | e -> Format.pp_print_flush ft () ; raise e - - -(* pretty print on stdout and stderr *) - -let pp_std_dirs = pp_dirs std_ft -let pp_err_dirs = pp_dirs err_ft - -let ppcmds x = Ppdir_ppcmds x - -(* pretty printing functions WITHOUT FLUSH *) -let pp_with ft strm = - pp_dirs ft [< 'Ppdir_ppcmds strm >] - -let ppnl_with ft strm = - pp_dirs ft [< 'Ppdir_ppcmds [< strm ; 'Ppcmd_force_newline >] >] - -let warning_with ft string = - ppnl_with ft [< str "Warning: " ; str string >] - -let warn_with ft pps = - ppnl_with ft [< str "Warning: " ; pps >] - -let pp_flush_with ft = - Format.pp_print_flush ft - - -(* pretty printing functions WITH FLUSH *) -let msg_with ft strm = - pp_dirs ft [< 'Ppdir_ppcmds strm ; 'Ppdir_print_flush >] - -let msgnl_with ft strm = - pp_dirs ft [< 'Ppdir_ppcmds strm ; 'Ppdir_print_newline >] - -let msg_warning_with ft strm= - pp_dirs ft [< 'Ppdir_ppcmds [< str "Warning: "; strm>]; - 'Ppdir_print_newline >] - - -(* pretty printing functions WITHOUT FLUSH *) -let pp = pp_with std_ft -let ppnl = ppnl_with std_ft -let pperr = pp_with err_ft -let pperrnl = ppnl_with err_ft -let message s = ppnl (str s) -let warning = warning_with std_ft -let warn = warn_with std_ft -let pp_flush = Format.pp_print_flush std_ft -let flush_all() = flush stderr; flush stdout; pp_flush() - -(* pretty printing functions WITH FLUSH *) -let msg = msg_with std_ft -let msgnl = msgnl_with std_ft -let msgerr = msg_with err_ft -let msgerrnl = msgnl_with err_ft -let msg_warning = msg_warning_with std_ft diff --git a/lib/pp.ml4 b/lib/pp.ml4 new file mode 100644 index 0000000000..2d4c76d916 --- /dev/null +++ b/lib/pp.ml4 @@ -0,0 +1,222 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* nc := 0 (* ascii char *) + | '\128'..'\191' -> nc := 0 (* cannot start with a continuation byte *) + | '\192'..'\223' -> nc := 1 (* expect 1 continuation byte *) + | '\224'..'\239' -> nc := 2 (* expect 2 continuation bytes *) + | '\240'..'\247' -> nc := 3 (* expect 3 continuation bytes *) + | '\248'..'\251' -> nc := 4 (* expect 4 continuation bytes *) + | '\252'..'\253' -> nc := 5 (* expect 5 continuation bytes *) + | '\254'..'\255' -> nc := 0 (* invalid byte *) + end ; + incr p ; + while !p < len && !nc > 0 do + match s.[!p] with + | '\128'..'\191' (* next continuation byte *) -> incr p ; decr nc + | _ (* not a continuation byte *) -> nc := 0 + done ; + incr cnt + done ; + !cnt + +(* formatting commands *) +let str s = [< 'Ppcmd_print (utf8_length s,s) >] +let stras (i,s) = [< 'Ppcmd_print (i,s) >] +let brk (a,b) = [< 'Ppcmd_print_break (a,b) >] +let tbrk (a,b) = [< 'Ppcmd_print_tbreak (a,b) >] +let tab () = [< 'Ppcmd_set_tab >] +let fnl () = [< 'Ppcmd_force_newline >] +let pifb () = [< 'Ppcmd_print_if_broken >] +let ws n = [< 'Ppcmd_white_space n >] + +(* derived commands *) +let spc () = [< 'Ppcmd_print_break (1,0) >] +let cut () = [< 'Ppcmd_print_break (0,0) >] +let align () = [< 'Ppcmd_print_break (0,0) >] +let int n = str (string_of_int n) +let real r = str (string_of_float r) +let bool b = str (string_of_bool b) +let qstring s = str ("\""^(String.escaped s)^"\"") +let qs = qstring +let mt () = [< >] + +(* boxing commands *) +let h n s = [< 'Ppcmd_box(Pp_hbox n,s) >] +let v n s = [< 'Ppcmd_box(Pp_vbox n,s) >] +let hv n s = [< 'Ppcmd_box(Pp_hvbox n,s) >] +let hov n s = [< 'Ppcmd_box(Pp_hovbox n,s) >] +let t s = [< 'Ppcmd_box(Pp_tbox,s) >] + +(* Opening and closing of boxes *) +let hb n = [< 'Ppcmd_open_box(Pp_hbox n) >] +let vb n = [< 'Ppcmd_open_box(Pp_vbox n) >] +let hvb n = [< 'Ppcmd_open_box(Pp_hvbox n) >] +let hovb n = [< 'Ppcmd_open_box(Pp_hovbox n) >] +let tb () = [< 'Ppcmd_open_box Pp_tbox >] +let close () = [< 'Ppcmd_close_box >] +let tclose () = [< 'Ppcmd_close_tbox >] + +let (++) = Stream.iapp + +(* pretty printing functions *) +let pp_dirs ft = + let maxbox = (get_gp ft).max_depth in + let pp_open_box = function + | Pp_hbox n -> Format.pp_open_hbox ft () + | Pp_vbox n -> Format.pp_open_vbox ft n + | Pp_hvbox n -> Format.pp_open_hvbox ft n + | Pp_hovbox n -> Format.pp_open_hovbox ft n + | Pp_tbox -> Format.pp_open_tbox ft () + in + let rec pp_cmd = function + | Ppcmd_print(n,s) -> Format.pp_print_as ft n s + | Ppcmd_box(bty,ss) -> (* Prevent evaluation of the stream! *) + pp_open_box bty ; + if not (Format.over_max_boxes ()) then Stream.iter pp_cmd ss; + Format.pp_close_box ft () + | Ppcmd_open_box bty -> pp_open_box bty + | Ppcmd_close_box -> Format.pp_close_box ft () + | Ppcmd_close_tbox -> Format.pp_close_tbox ft () + | Ppcmd_white_space n -> Format.pp_print_break ft n 0 + | Ppcmd_print_break(m,n) -> Format.pp_print_break ft m n + | Ppcmd_set_tab -> Format.pp_set_tab ft () + | Ppcmd_print_tbreak(m,n) -> Format.pp_print_tbreak ft m n + | Ppcmd_force_newline -> Format.pp_force_newline ft () + | Ppcmd_print_if_broken -> Format.pp_print_if_newline ft () + in + let pp_dir = function + | Ppdir_ppcmds cmdstream -> Stream.iter pp_cmd cmdstream + | Ppdir_print_newline -> Format.pp_print_newline ft () + | Ppdir_print_flush -> Format.pp_print_flush ft () + in + fun dirstream -> + try + Stream.iter pp_dir dirstream + with + | e -> Format.pp_print_flush ft () ; raise e + + +(* pretty print on stdout and stderr *) + +let pp_std_dirs = pp_dirs std_ft +let pp_err_dirs = pp_dirs err_ft + +let ppcmds x = Ppdir_ppcmds x + +(* pretty printing functions WITHOUT FLUSH *) +let pp_with ft strm = + pp_dirs ft [< 'Ppdir_ppcmds strm >] + +let ppnl_with ft strm = + pp_dirs ft [< 'Ppdir_ppcmds [< strm ; 'Ppcmd_force_newline >] >] + +let warning_with ft string = + ppnl_with ft [< str "Warning: " ; str string >] + +let warn_with ft pps = + ppnl_with ft [< str "Warning: " ; pps >] + +let pp_flush_with ft = + Format.pp_print_flush ft + + +(* pretty printing functions WITH FLUSH *) +let msg_with ft strm = + pp_dirs ft [< 'Ppdir_ppcmds strm ; 'Ppdir_print_flush >] + +let msgnl_with ft strm = + pp_dirs ft [< 'Ppdir_ppcmds strm ; 'Ppdir_print_newline >] + +let msg_warning_with ft strm= + pp_dirs ft [< 'Ppdir_ppcmds [< str "Warning: "; strm>]; + 'Ppdir_print_newline >] + + +(* pretty printing functions WITHOUT FLUSH *) +let pp = pp_with std_ft +let ppnl = ppnl_with std_ft +let pperr = pp_with err_ft +let pperrnl = ppnl_with err_ft +let message s = ppnl (str s) +let warning = warning_with std_ft +let warn = warn_with std_ft +let pp_flush = Format.pp_print_flush std_ft +let flush_all() = flush stderr; flush stdout; pp_flush() + +(* pretty printing functions WITH FLUSH *) +let msg = msg_with std_ft +let msgnl = msgnl_with std_ft +let msgerr = msg_with err_ft +let msgerrnl = msgnl_with err_ft +let msg_warning = msg_warning_with std_ft diff --git a/tools/coq-tex.ml b/tools/coq-tex.ml deleted file mode 100644 index 541777d6e4..0000000000 --- a/tools/coq-tex.ml +++ /dev/null @@ -1,274 +0,0 @@ -(***********************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* () - | _ -> begin - print_string "This program only runs under Unix !\n"; - flush stdout; - exit 1 - end - -let linelen = ref 72 -let output = ref "" -let output_specified = ref false -let image = ref "" -let cut_at_blanks = ref false -let verbose = ref false -let slanted = ref false -let hrule = ref false -let small = ref false - -let coq_prompt = Str.regexp "Coq < " -let any_prompt = Str.regexp "^[A-Z0-9a-z_\$']* < " - -let remove_prompt s = Str.replace_first any_prompt "" s - -(* First pass: extract the Coq phrases to evaluate from [texfile] - * and put them into the file [inputv] *) - -let begin_coq = Str.regexp "\\\\begin{coq_\(example\|example\*\|example\#\|eval\)}[ \t]*$" -let end_coq = Str.regexp "\\\\end{coq_\(example\|example\*\|example\#\|eval\)}[ \t]*$" - -let extract texfile inputv = - let chan_in = open_in texfile in - let chan_out = open_out inputv in - let rec inside () = - let s = input_line chan_in in - if Str.string_match end_coq s 0 then - outside () - else begin - output_string chan_out (s ^ "\n"); - inside () - end - and outside () = - let s = input_line chan_in in - if Str.string_match begin_coq s 0 then - inside () - else - outside () - in - try - outside () - with End_of_file -> - begin close_in chan_in; close_out chan_out end - -(* Second pass: insert the answers of Coq from [coq_output] into the - * TeX file [texfile]. The result goes in file [result]. *) - -let begin_coq_example = - Str.regexp "\\\\begin{coq_\(example\|example\*\|example\#\)}[ \t]*$" -let begin_coq_eval = Str.regexp "\\\\begin{coq_eval}[ \t]*$" -let end_coq_example = Str.regexp "\\\\end{coq_\(example\|example\*\|example\#\)}[ \t]*$" -let end_coq_eval = Str.regexp "\\\\end{coq_eval}[ \t]*$" -let dot_end_line = Str.regexp "\\.[ \t]*$" - -let has_match r s = - try let _ = Str.search_forward r s 0 in true with Not_found -> false - -let percent = Str.regexp "%" -let bang = Str.regexp "!" -let expos = Str.regexp "^" - -let tex_escaped s = - let rec trans = parser - | [< s1 = (parser - | [< ''_'|'$'|'{'|'}'|'&'|'%'|'#' as c >] -> - "\\" ^ (String.make 1 c) - | [< ''\\' >] -> "\\char'134" - | [< ''^' >] -> "\\char'136" - | [< ''~' >] -> "\\char'176" - | [< '' ' >] -> "~" - | [< ''<' >] -> "{<}" - | [< ''>' >] -> "{>}" - | [< 'c >] -> String.make 1 c); - s2 = trans >] -> s1 ^ s2 - | [< >] -> "" - in - trans (Stream.of_string s) - -let encapsule sl c_out s = - if sl then - Printf.fprintf c_out "\\texttt{\\textit{%s}}\\\\\n" (tex_escaped s) - else - Printf.fprintf c_out "\\texttt{%s}\\\\\n" (tex_escaped s) - -let print_block c_out bl = - List.iter (fun s -> if s="" then () else encapsule !slanted c_out s) bl - -let insert texfile coq_output result = - let c_tex = open_in texfile in - let c_coq = open_in coq_output in - let c_out = open_out result in - (* next_block k : this function reads the next block of Coq output - * removing the k leading prompts. - * it returns the block as a list of string) *) - let last_read = ref "" in - let next_block k = - if !last_read = "" then last_read := input_line c_coq; - (* skip k prompts *) - for i = 1 to k do - last_read := remove_prompt !last_read; - done; - (* read and return the following lines until a prompt is found *) - let rec read_lines () = - let s = input_line c_coq in - if Str.string_match any_prompt s 0 then begin - last_read := s; [] - end else - s :: (read_lines ()) - in - let first = !last_read in first :: (read_lines ()) - in - (* we are outside of a \begin{coq_...} ... \end{coq_...} block *) - let rec outside () = - let s = input_line c_tex in - if Str.string_match begin_coq_example s 0 then begin - if !small then output_string c_out "\\begin{small}\n"; - output_string c_out "\\begin{flushleft}\n"; - if !hrule then output_string c_out "\\hrulefill\\\\\n"; - inside (Str.matched_group 1 s <> "example*") - (Str.matched_group 1 s <> "example#") 0 true - end else if Str.string_match begin_coq_eval s 0 then - eval 0 - else begin - output_string c_out (s ^ "\n"); - outside () - end - (* we are inside a \begin{coq_example?} ... \end{coq_example?} block - * show_answers tells what kind of block it is - * k is the number of lines read until now *) - and inside show_answers show_questions k first_block = - let s = input_line c_tex in - if Str.string_match end_coq_example s 0 then begin - if !hrule then output_string c_out "\\hrulefill\\\\\n"; - output_string c_out "\\end{flushleft}\n"; - if !small then output_string c_out "\\end{small}\n"; - outside () - end else begin - if !verbose then Printf.printf "Coq < %s\n" s; - if (not first_block) & k=0 then output_string c_out "\\medskip\n"; - if show_questions then encapsule false c_out ("Coq < " ^ s); - if has_match dot_end_line s then begin - let bl = next_block (succ k) in - if !verbose then List.iter print_endline bl; - if show_answers then print_block c_out bl; - inside show_answers show_questions 0 false - end else - inside show_answers show_questions (succ k) first_block - end - (* we are inside a \begin{coq_eval} ... \end{coq_eval} block - * k is the number of lines read until now *) - and eval k = - let s = input_line c_tex in - if Str.string_match end_coq_eval s 0 then - outside () - else begin - if !verbose then Printf.printf "Coq < %s\n" s; - if has_match dot_end_line s then - let bl = next_block (succ k) in - if !verbose then List.iter print_endline bl; - eval 0 - else - eval (succ k) - end - in - try - let _ = next_block 0 in (* to skip the Coq banner *) - outside () - with End_of_file -> begin - close_in c_tex; - close_in c_coq; - close_out c_out - end - -(* Process of one TeX file *) - -let rm f = try Sys.remove f with _ -> () - -let one_file texfile = - let inputv = Filename.temp_file "coq_tex" ".v" in - let coq_output = Filename.temp_file "coq_tex" ".coq_output"in - let result = - if !output_specified then - !output - else if Filename.check_suffix texfile ".tex" then - (Filename.chop_suffix texfile ".tex") ^ ".v.tex" - else - texfile ^ ".v.tex" - in - try - (* 1. extract Coq phrases *) - extract texfile inputv; - (* 2. run Coq on input *) - let _ = Sys.command (Printf.sprintf "%s < %s > %s 2>&1" !image inputv - coq_output) - in - (* 3. insert Coq output into original file *) - insert texfile coq_output result; - (* 4. clean up *) - rm inputv; rm coq_output - with e -> begin - rm inputv; rm coq_output; - raise e - end - -(* Parsing of the command line, check of the Coq command and process - * of all the files in the command line, one by one *) - -let files = ref [] - -let parse_cl () = - Arg.parse - [ "-o", Arg.String (fun s -> output_specified := true; output := s), - "output-file Specifiy the resulting LaTeX file"; - "-n", Arg.Int (fun n -> linelen := n), - "line-width Set the line width"; - "-image", Arg.String (fun s -> image := s), - "coq-image Use coq-image as Coq command"; - "-w", Arg.Set cut_at_blanks, - " Try to cut lines at blanks"; - "-v", Arg.Set verbose, - " Verbose mode (show Coq answers on stdout)"; - "-sl", Arg.Set slanted, - " Coq answers in slanted font (only with LaTeX2e)"; - "-hrule", Arg.Set hrule, - " Coq parts are written between 2 horizontal lines"; - "-small", Arg.Set small, - " Coq parts are written in small font" - ] - (fun s -> files := s :: !files) - "coq-tex [options] file ..." - -let main () = - parse_cl (); - if !image = "" then begin - Printf.printf "Warning: preprocessing with default image \"coqtop\"\n"; - image := "coqtop" - end; - if Sys.command (!image ^ " -batch > /dev/null 2>&1") <> 0 then begin - Printf.printf "Error: "; - let _ = Sys.command (!image ^ " -batch") in - exit 1 - end else begin - Printf.printf "Your version of coqtop seems OK\n"; - flush stdout - end; - List.iter one_file (List.rev !files) - -let _ = Printexc.catch main () diff --git a/tools/coq-tex.ml4 b/tools/coq-tex.ml4 new file mode 100644 index 0000000000..541777d6e4 --- /dev/null +++ b/tools/coq-tex.ml4 @@ -0,0 +1,274 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* () + | _ -> begin + print_string "This program only runs under Unix !\n"; + flush stdout; + exit 1 + end + +let linelen = ref 72 +let output = ref "" +let output_specified = ref false +let image = ref "" +let cut_at_blanks = ref false +let verbose = ref false +let slanted = ref false +let hrule = ref false +let small = ref false + +let coq_prompt = Str.regexp "Coq < " +let any_prompt = Str.regexp "^[A-Z0-9a-z_\$']* < " + +let remove_prompt s = Str.replace_first any_prompt "" s + +(* First pass: extract the Coq phrases to evaluate from [texfile] + * and put them into the file [inputv] *) + +let begin_coq = Str.regexp "\\\\begin{coq_\(example\|example\*\|example\#\|eval\)}[ \t]*$" +let end_coq = Str.regexp "\\\\end{coq_\(example\|example\*\|example\#\|eval\)}[ \t]*$" + +let extract texfile inputv = + let chan_in = open_in texfile in + let chan_out = open_out inputv in + let rec inside () = + let s = input_line chan_in in + if Str.string_match end_coq s 0 then + outside () + else begin + output_string chan_out (s ^ "\n"); + inside () + end + and outside () = + let s = input_line chan_in in + if Str.string_match begin_coq s 0 then + inside () + else + outside () + in + try + outside () + with End_of_file -> + begin close_in chan_in; close_out chan_out end + +(* Second pass: insert the answers of Coq from [coq_output] into the + * TeX file [texfile]. The result goes in file [result]. *) + +let begin_coq_example = + Str.regexp "\\\\begin{coq_\(example\|example\*\|example\#\)}[ \t]*$" +let begin_coq_eval = Str.regexp "\\\\begin{coq_eval}[ \t]*$" +let end_coq_example = Str.regexp "\\\\end{coq_\(example\|example\*\|example\#\)}[ \t]*$" +let end_coq_eval = Str.regexp "\\\\end{coq_eval}[ \t]*$" +let dot_end_line = Str.regexp "\\.[ \t]*$" + +let has_match r s = + try let _ = Str.search_forward r s 0 in true with Not_found -> false + +let percent = Str.regexp "%" +let bang = Str.regexp "!" +let expos = Str.regexp "^" + +let tex_escaped s = + let rec trans = parser + | [< s1 = (parser + | [< ''_'|'$'|'{'|'}'|'&'|'%'|'#' as c >] -> + "\\" ^ (String.make 1 c) + | [< ''\\' >] -> "\\char'134" + | [< ''^' >] -> "\\char'136" + | [< ''~' >] -> "\\char'176" + | [< '' ' >] -> "~" + | [< ''<' >] -> "{<}" + | [< ''>' >] -> "{>}" + | [< 'c >] -> String.make 1 c); + s2 = trans >] -> s1 ^ s2 + | [< >] -> "" + in + trans (Stream.of_string s) + +let encapsule sl c_out s = + if sl then + Printf.fprintf c_out "\\texttt{\\textit{%s}}\\\\\n" (tex_escaped s) + else + Printf.fprintf c_out "\\texttt{%s}\\\\\n" (tex_escaped s) + +let print_block c_out bl = + List.iter (fun s -> if s="" then () else encapsule !slanted c_out s) bl + +let insert texfile coq_output result = + let c_tex = open_in texfile in + let c_coq = open_in coq_output in + let c_out = open_out result in + (* next_block k : this function reads the next block of Coq output + * removing the k leading prompts. + * it returns the block as a list of string) *) + let last_read = ref "" in + let next_block k = + if !last_read = "" then last_read := input_line c_coq; + (* skip k prompts *) + for i = 1 to k do + last_read := remove_prompt !last_read; + done; + (* read and return the following lines until a prompt is found *) + let rec read_lines () = + let s = input_line c_coq in + if Str.string_match any_prompt s 0 then begin + last_read := s; [] + end else + s :: (read_lines ()) + in + let first = !last_read in first :: (read_lines ()) + in + (* we are outside of a \begin{coq_...} ... \end{coq_...} block *) + let rec outside () = + let s = input_line c_tex in + if Str.string_match begin_coq_example s 0 then begin + if !small then output_string c_out "\\begin{small}\n"; + output_string c_out "\\begin{flushleft}\n"; + if !hrule then output_string c_out "\\hrulefill\\\\\n"; + inside (Str.matched_group 1 s <> "example*") + (Str.matched_group 1 s <> "example#") 0 true + end else if Str.string_match begin_coq_eval s 0 then + eval 0 + else begin + output_string c_out (s ^ "\n"); + outside () + end + (* we are inside a \begin{coq_example?} ... \end{coq_example?} block + * show_answers tells what kind of block it is + * k is the number of lines read until now *) + and inside show_answers show_questions k first_block = + let s = input_line c_tex in + if Str.string_match end_coq_example s 0 then begin + if !hrule then output_string c_out "\\hrulefill\\\\\n"; + output_string c_out "\\end{flushleft}\n"; + if !small then output_string c_out "\\end{small}\n"; + outside () + end else begin + if !verbose then Printf.printf "Coq < %s\n" s; + if (not first_block) & k=0 then output_string c_out "\\medskip\n"; + if show_questions then encapsule false c_out ("Coq < " ^ s); + if has_match dot_end_line s then begin + let bl = next_block (succ k) in + if !verbose then List.iter print_endline bl; + if show_answers then print_block c_out bl; + inside show_answers show_questions 0 false + end else + inside show_answers show_questions (succ k) first_block + end + (* we are inside a \begin{coq_eval} ... \end{coq_eval} block + * k is the number of lines read until now *) + and eval k = + let s = input_line c_tex in + if Str.string_match end_coq_eval s 0 then + outside () + else begin + if !verbose then Printf.printf "Coq < %s\n" s; + if has_match dot_end_line s then + let bl = next_block (succ k) in + if !verbose then List.iter print_endline bl; + eval 0 + else + eval (succ k) + end + in + try + let _ = next_block 0 in (* to skip the Coq banner *) + outside () + with End_of_file -> begin + close_in c_tex; + close_in c_coq; + close_out c_out + end + +(* Process of one TeX file *) + +let rm f = try Sys.remove f with _ -> () + +let one_file texfile = + let inputv = Filename.temp_file "coq_tex" ".v" in + let coq_output = Filename.temp_file "coq_tex" ".coq_output"in + let result = + if !output_specified then + !output + else if Filename.check_suffix texfile ".tex" then + (Filename.chop_suffix texfile ".tex") ^ ".v.tex" + else + texfile ^ ".v.tex" + in + try + (* 1. extract Coq phrases *) + extract texfile inputv; + (* 2. run Coq on input *) + let _ = Sys.command (Printf.sprintf "%s < %s > %s 2>&1" !image inputv + coq_output) + in + (* 3. insert Coq output into original file *) + insert texfile coq_output result; + (* 4. clean up *) + rm inputv; rm coq_output + with e -> begin + rm inputv; rm coq_output; + raise e + end + +(* Parsing of the command line, check of the Coq command and process + * of all the files in the command line, one by one *) + +let files = ref [] + +let parse_cl () = + Arg.parse + [ "-o", Arg.String (fun s -> output_specified := true; output := s), + "output-file Specifiy the resulting LaTeX file"; + "-n", Arg.Int (fun n -> linelen := n), + "line-width Set the line width"; + "-image", Arg.String (fun s -> image := s), + "coq-image Use coq-image as Coq command"; + "-w", Arg.Set cut_at_blanks, + " Try to cut lines at blanks"; + "-v", Arg.Set verbose, + " Verbose mode (show Coq answers on stdout)"; + "-sl", Arg.Set slanted, + " Coq answers in slanted font (only with LaTeX2e)"; + "-hrule", Arg.Set hrule, + " Coq parts are written between 2 horizontal lines"; + "-small", Arg.Set small, + " Coq parts are written in small font" + ] + (fun s -> files := s :: !files) + "coq-tex [options] file ..." + +let main () = + parse_cl (); + if !image = "" then begin + Printf.printf "Warning: preprocessing with default image \"coqtop\"\n"; + image := "coqtop" + end; + if Sys.command (!image ^ " -batch > /dev/null 2>&1") <> 0 then begin + Printf.printf "Error: "; + let _ = Sys.command (!image ^ " -batch") in + exit 1 + end else begin + Printf.printf "Your version of coqtop seems OK\n"; + flush stdout + end; + List.iter one_file (List.rev !files) + +let _ = Printexc.catch main () diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml deleted file mode 100644 index 613257c685..0000000000 --- a/tools/coq_makefile.ml +++ /dev/null @@ -1,430 +0,0 @@ -(***********************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* (ML "foo") *) - | V of string (* V file : foo.v -> (V "foo") *) - | Special of string * string * string (* file, dependencies, command *) - | Subdir of string - | Def of string * string (* X=foo -> Def ("X","foo") *) - | Include of string - | RInclude of string * string (* -R physicalpath logicalpath *) - -let output_channel = ref stdout - -let some_file = ref false -let some_vfile = ref false -let some_mlfile = ref false - -let opt = ref "-opt" - -let print x = output_string !output_channel x - -let rec print_list sep = function - | [ x ] -> print x - | x :: l -> print x; print sep; print_list sep l - | [] -> () - -let section s = - let l = String.length s in - let sep = String.make (l+5) '#' - and sep2 = String.make (l+5) ' ' in - String.set sep (l+4) '\n'; - String.set sep2 0 '#'; - String.set sep2 (l+3) '#'; - String.set sep2 (l+4) '\n'; - print sep; - print sep2; - print "# "; print s; print " #\n"; - print sep2; - print sep; - print "\n" - -let usage () = - output_string stderr "Usage summary: - -coq_makefile [subdirectory] .... [file.v] ... [file.ml] ... [-custom - command dependencies file] ... [-I dir] ... [-R physicalpath logicalpath] - ... [VARIABLE = value] ... [-opt|-byte] [-f file] [-o file] [-h] [--help] - -[file.v]: Coq file to be compiled -[file.ml]: ML file to be compiled -[subdirectory] : subdirectory that should be \"made\" -[-custom command dependencies file]: add target \"file\" with command - \"command\" and dependencies \"dependencies\" -[-I dir]: look for dependencies in \"dir\" -[-R physicalpath logicalpath]: look for dependencies resursively starting from - \"physicalpath\". The logical path associated to the physical path is - \"logicalpath\". -[VARIABLE = value]: Add the variable definition \"VARIABLE=value\" -[-byte]: compile with byte-code version of coq -[-opt]: compile with native-code version of coq -[-f file]: take the contents of file as arguments -[-o file]: output should go in file file -[-h]: print this usage summary -[--help]: equivalent to [-h]\n"; - exit 1 - -let standard sds = - print "byte:\n"; - print "\t$(MAKE) all \"OPT=\"\n\n"; - print "opt:\n"; - if !opt = "" then print "\t@echo \"WARNING: opt is disabled\"\n"; - print "\t$(MAKE) all \"OPT="; print !opt; print "\"\n\n"; - if !some_file then print "include .depend\n\n"; - print "depend:\n"; - if !some_file then begin - print "\trm .depend\n"; - print "\t$(COQDEP) -i $(COQLIBS) *.v *.ml *.mli >.depend\n"; - print "\t$(COQDEP) $(COQLIBS) -suffix .html *.v >>.depend\n"; - end; - List.iter - (fun x -> print "\t(cd "; print x; print " ; $(MAKE) depend)\n") - sds; - print "\n"; - print "xml::\n"; - List.iter - (fun x -> print "\t(cd "; print x; print " ; $(MAKE) xml)\n") - sds; - print "\n"; - print "install:\n"; - print "\tmkdir -p `$(COQC) -where`/user-contrib\n"; - if !some_vfile then print "\tcp -f *.vo `$(COQC) -where`/user-contrib\n"; - if !some_mlfile then print "\tcp -f *.cmo `$(COQC) -where`/user-contrib\n"; - List.iter - (fun x -> print "\t(cd "; print x; print " ; $(MAKE) install)\n") - sds; - print "\n"; - print "Makefile: Make\n"; - print "\tmv -f Makefile Makefile.bak\n"; - print "\t$(COQBIN)coq_makefile -f Make -o Makefile\n"; - print "\n"; - print "clean:\n"; - print "\trm -f *.cmo *.cmi *.cmx *.o *.vo *.vi *.g *~\n"; - print "\trm -f all.ps all-gal.ps $(HTMLFILES) $(GHTMLFILES)\n"; - List.iter - (fun x -> print "\t(cd "; print x; print " ; $(MAKE) clean)\n") - sds; - print "\n"; - print "archclean:\n"; - print "\trm -f *.cmx *.o\n"; - List.iter - (fun x -> print "\t(cd "; print x; print " ; $(MAKE) archclean)\n") - sds; - print "\n" - -let implicit () = - let ml_rules () = - print ".mli.cmi:\n\t$(CAMLC) $(ZDEBUG) $(ZFLAGS) $<\n\n"; - print ".ml.cmo:\n\t$(CAMLC) $(ZDEBUG) $(ZFLAGS) $<\n\n"; - print ".ml.cmx:\n\t$(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) $<\n\n"; - and v_rule () = - print ".v.vo:\n\t$(COQC) $(COQDEBUG) $(COQFLAGS) $*\n\n"; - print ".v.vi:\n\t$(COQC) -i $(COQDEBUG) $(COQFLAGS) $*\n\n"; - print ".v.g:\n\t$(GALLINA) $<\n\n"; - print ".v.tex:\n\t$(COQWEB) $< -o $@\n\n"; - print ".v.html:\n\t$(COQWEB) -html $< -o $@\n\n"; - print ".g.g.tex:\n\t$(COQWEB) $< -o $@\n\n"; - print ".g.g.html:\n\t$(COQWEB) -html $< -o $@\n\n" - and ml_suffixes = - if !some_mlfile then - [ ".mli"; ".ml"; ".cmo"; ".cmi"; ".cmx" ] - else - [] - and v_suffixes = - if !some_vfile then - [ ".v"; ".vo"; ".vi"; ".g"; ".html"; ".tex"; ".g.tex"; ".g.html" ] - else - [] - in - let suffixes = ml_suffixes @ v_suffixes in - if suffixes <> [] then begin - print ".SUFFIXES: "; print_list " " suffixes; - print "\n\n" - end; - if !some_mlfile then ml_rules (); - if !some_vfile then v_rule () - -let variables l = - let rec var_aux = function - | [] -> () - | Def(v,def) :: r -> print v; print "="; print def; print "\n"; var_aux r - | _ :: r -> var_aux r - in - section "Variables definitions."; - print "CAMLP4LIB=`camlp4 -where`\n"; -(* print "MAKE=make \"COQBIN=$(COQBIN)\" \"OPT=$(OPT)\"\n"; *) - print "COQSRC=-I $(COQTOP)/kernel -I $(COQTOP)/lib \\ - -I $(COQTOP)/library -I $(COQTOP)/parsing -I $(COQTOP)/pretyping \\ - -I $(COQTOP)/proofs -I $(COQTOP)/syntax -I $(COQTOP)/tactics \\ - -I $(COQTOP)/toplevel -I $(CAMLP4LIB)\n"; - print "ZFLAGS=$(OCAMLLIBS) $(COQSRC)\n"; - print "OPT="; if !opt = "-byte" then print "-byte"; print "\n"; - print "COQFLAGS=-q $(OPT) $(COQLIBS)\n"; - print "COQC=$(COQBIN)coqc\n"; - print "GALLINA=gallina\n"; - print "COQWEB=coqweb\n"; - print "CAMLC=ocamlc -c\n"; - print "CAMLOPTC=ocamlopt -c\n"; - print "CAMLLINK=ocamlc\n"; - print "CAMLOPTLINK=ocamlopt\n"; - print "COQDEP=$(COQBIN)coqdep -c\n"; - print "COQVO2XML=coq_vo2xml\n"; - var_aux l; - print "\n" - -let include_dirs l = - let include_aux' includeR = - let rec include_aux = function - | [] -> [] - | Include x :: r -> ("-I " ^ x) :: (include_aux r) - | RInclude (p,l) :: r when includeR -> - let l' = if l = "" then "\"\"" else l in - ("-R " ^ p ^ " " ^ l') :: (include_aux r) - | _ :: r -> include_aux r - in - include_aux - in - let i_ocaml = "-I ." :: (include_aux' false l) in - let i_coq = "-I ." :: (include_aux' true l) in - section "Libraries definition."; - print "OCAMLLIBS="; print_list "\\\n " i_ocaml; print "\n"; - print "COQLIBS="; print_list "\\\n " i_coq; print "\n\n" - -let special l = - let pr_sp (file,dependencies,com) = - print file; print ": "; print dependencies; print "\n"; - print "\t"; print com; print "\n\n" - in - let rec sp_aux = function - | [] -> [] - | Special (file,deps,com) :: r -> (file,deps,com) :: (sp_aux r) - | _ :: r -> sp_aux r - in - let sps = sp_aux l in - if sps <> [] then section "Custom targets."; - List.iter pr_sp sps - -let subdirs l = - let rec subdirs_aux = function - | [] -> [] - | Subdir x :: r -> x :: (subdirs_aux r) - | _ :: r -> subdirs_aux r - and pr_subdir s = - print s; print ":\n\tcd "; print s; print " ; $(MAKE) all\n\n" - in - let sds = subdirs_aux l in - if sds <> [] then section "Subdirectories."; - List.iter pr_subdir sds; - section "Special targets."; - print ".PHONY: "; - print_list " " - ("all" :: "opt" :: "byte" :: "archclean" :: "clean" :: "install" - :: "depend" :: "xml" :: sds); - print "\n\n"; - sds - -(* Extract gallina/html filenames (foo.v) from the list of all targets *) - -let rec other_files suff = function - | V n :: r -> - let f = (Filename.chop_suffix n ".vo") ^ suff in - f :: (other_files suff r) - | _ :: r -> - other_files suff r - | [] -> - [] - -let vfiles = other_files ".v" -let gfiles = other_files ".g" -let hfiles = other_files ".html" -let tfiles = other_files ".tex" -let vifiles = other_files ".vi" -let gtfiles l = List.map (fun f -> f ^ ".tex") (gfiles l) -let ghfiles l = List.map (fun f -> f ^ ".html") (gfiles l) -let vofiles = other_files ".vo" - -let all_target l = - let rec fnames = function - | ML n :: r -> n :: (fnames r) - | Subdir n :: r -> n :: (fnames r) - | V n :: r -> n :: (fnames r) - | Special (n,_,_) :: r -> n :: (fnames r) - | Include _ :: r -> fnames r - | RInclude _ :: r -> fnames r - | Def _ :: r -> fnames r - | [] -> [] - in - section "Definition of the \"all\" target."; - print "VFILES="; print_list "\\\n " (vfiles l); print "\n"; - print "VOFILES=$(VFILES:.v=.vo)\n"; - print "VIFILES=$(VFILES:.v=.vi)\n"; - print "GFILES=$(VFILES:.v=.g)\n"; - print "HTMLFILES=$(VFILES:.v=.html)\n"; - print "GHTMLFILES=$(VFILES:.v=.g.html)\n"; - print "\n"; - print "all: "; print_list "\\\n " (fnames l); - print "\n\n"; - if !some_vfile then begin - print "spec: $(VIFILES)\n\n"; - print "gallina: $(GFILES)\n\n"; - print "html: $(HTMLFILES)\n\n"; - print "gallinahtml: $(GHTMLFILES)\n\n"; - print "all.ps: $(VFILES)\n"; - print "\t$(COQWEB) -ps -o $@ `$(COQDEP) -sort -suffix .v $(VFILES)`\n\n"; - print "all-gal.ps: $(GFILES)\n"; - print "\t$(COQWEB) -ps -o $@ `$(COQDEP) -sort -suffix .g $(VFILES)`\n\n"; - print "xml:: .xml_time_stamp\n"; - print ".xml_time_stamp: "; print_list "\\\n " (vofiles l); - print "\n\t$(COQVO2XML) $(COQFLAGS) $(?:%.o=%)\n"; - print "\ttouch .xml_time_stamp"; - print "\n\n" - end - -let parse f = - let rec string = parser - | [< '' ' | '\n' | '\t' >] -> "" - | [< 'c; s >] -> (String.make 1 c)^(string s) - | [< >] -> "" - and string2 = parser - | [< ''"' >] -> "" - | [< 'c; s >] -> (String.make 1 c)^(string2 s) - and skip_comment = parser - | [< ''\n'; s >] -> s - | [< 'c; s >] -> skip_comment s - | [< >] -> [< >] - and args = parser - | [< '' ' | '\n' | '\t'; s >] -> args s - | [< ''#'; s >] -> args (skip_comment s) - | [< ''"'; str = string2; s >] -> ("" ^ str) :: args s - | [< 'c; str = string; s >] -> ((String.make 1 c) ^ str) :: (args s) - | [< >] -> [] - in - let c = open_in f in - let res = args (Stream.of_channel c) in - close_in c; - res - -let rec process_cmd_line = function - | [] -> - some_file := !some_file or !some_mlfile or !some_vfile; [] - | ("-h"|"--help") :: _ -> - usage () - | ("-no-opt"|"-byte") :: r -> - opt := "-byte"; process_cmd_line r - | ("-full"|"-opt") :: r -> - opt := "-opt"; process_cmd_line r - | "-custom" :: com :: dependencies :: file :: r -> - some_file := true; - Special (file,dependencies,com) :: (process_cmd_line r) - | "-I" :: d :: r -> - Include d :: (process_cmd_line r) - | "-R" :: p :: l :: r -> - RInclude (p,l) :: (process_cmd_line r) - | ("-I" | "-h" | "--help" | "-custom") :: _ -> - usage () - | "-f"::file::r -> - process_cmd_line ((parse file)@r) - | ["-f"] -> - usage () - | "-o" :: file :: r -> - output_channel := (open_out file); - (process_cmd_line r) - | v :: "=" :: def :: r -> - Def (v,def) :: (process_cmd_line r) - | f :: r -> - if Filename.check_suffix f ".v" then begin - some_vfile := true; - V (f^"o") :: (process_cmd_line r) - end else if Filename.check_suffix f ".ml" then begin - some_mlfile := true; - ML ((Filename.chop_suffix f "ml")^"cmo") :: (process_cmd_line r) - end else - Subdir f :: (process_cmd_line r) - -let banner () = - print -"############################################################################## -## The Calculus of Inductive Constructions ## -## ## -## Projet Coq ## -## ## -## INRIA ENS-CNRS ## -## Rocquencourt Lyon ## -## ## -## Coq V7 ## -## ## -## ## -############################################################################## - -" - -let warning () = - print "# WARNING\n#\n"; - print "# This Makefile has been automagically generated by coq_makefile\n"; - print "# Edit at your own risks !\n"; - print "#\n# END OF WARNING\n\n" - -let print_list l = List.iter (fun x -> print x; print " ") l - -let command_line args = - print "#\n# This Makefile was generated by the command line :\n"; - print "# coq_makefile "; - print_list args; - print "\n#\n\n" - -let directories_deps l = - let print_dep f dep = - if dep <> [] then begin print f; print ": "; print_list dep; print "\n" end - in - let rec iter ((dirs,before) as acc) = function - | [] -> - () - | (Subdir d) :: l -> - print_dep d before; iter (d :: dirs, d :: before) l - | (ML f) :: l -> - print_dep f dirs; iter (dirs, f :: before) l - | (V f) :: l -> - print_dep f dirs; iter (dirs, f :: before) l - | (Special (f,_,_)) :: l -> - print_dep f dirs; iter (dirs, f :: before) l - | _ :: l -> - iter acc l - in - iter ([],[]) l - -let do_makefile args = - let l = process_cmd_line args in - banner (); - warning (); - command_line args; - variables l; - include_dirs l; - all_target l; - special l; - let sds = subdirs l in - implicit (); - standard sds; - (* TEST directories_deps l; *) - warning (); - if not (!output_channel == stdout) then close_out !output_channel; - exit 0 - -let main () = - let args = - if Array.length Sys.argv = 1 then usage (); - List.tl (Array.to_list Sys.argv) - in - do_makefile args - -let _ = Printexc.catch main () - diff --git a/tools/coq_makefile.ml4 b/tools/coq_makefile.ml4 new file mode 100644 index 0000000000..613257c685 --- /dev/null +++ b/tools/coq_makefile.ml4 @@ -0,0 +1,430 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* (ML "foo") *) + | V of string (* V file : foo.v -> (V "foo") *) + | Special of string * string * string (* file, dependencies, command *) + | Subdir of string + | Def of string * string (* X=foo -> Def ("X","foo") *) + | Include of string + | RInclude of string * string (* -R physicalpath logicalpath *) + +let output_channel = ref stdout + +let some_file = ref false +let some_vfile = ref false +let some_mlfile = ref false + +let opt = ref "-opt" + +let print x = output_string !output_channel x + +let rec print_list sep = function + | [ x ] -> print x + | x :: l -> print x; print sep; print_list sep l + | [] -> () + +let section s = + let l = String.length s in + let sep = String.make (l+5) '#' + and sep2 = String.make (l+5) ' ' in + String.set sep (l+4) '\n'; + String.set sep2 0 '#'; + String.set sep2 (l+3) '#'; + String.set sep2 (l+4) '\n'; + print sep; + print sep2; + print "# "; print s; print " #\n"; + print sep2; + print sep; + print "\n" + +let usage () = + output_string stderr "Usage summary: + +coq_makefile [subdirectory] .... [file.v] ... [file.ml] ... [-custom + command dependencies file] ... [-I dir] ... [-R physicalpath logicalpath] + ... [VARIABLE = value] ... [-opt|-byte] [-f file] [-o file] [-h] [--help] + +[file.v]: Coq file to be compiled +[file.ml]: ML file to be compiled +[subdirectory] : subdirectory that should be \"made\" +[-custom command dependencies file]: add target \"file\" with command + \"command\" and dependencies \"dependencies\" +[-I dir]: look for dependencies in \"dir\" +[-R physicalpath logicalpath]: look for dependencies resursively starting from + \"physicalpath\". The logical path associated to the physical path is + \"logicalpath\". +[VARIABLE = value]: Add the variable definition \"VARIABLE=value\" +[-byte]: compile with byte-code version of coq +[-opt]: compile with native-code version of coq +[-f file]: take the contents of file as arguments +[-o file]: output should go in file file +[-h]: print this usage summary +[--help]: equivalent to [-h]\n"; + exit 1 + +let standard sds = + print "byte:\n"; + print "\t$(MAKE) all \"OPT=\"\n\n"; + print "opt:\n"; + if !opt = "" then print "\t@echo \"WARNING: opt is disabled\"\n"; + print "\t$(MAKE) all \"OPT="; print !opt; print "\"\n\n"; + if !some_file then print "include .depend\n\n"; + print "depend:\n"; + if !some_file then begin + print "\trm .depend\n"; + print "\t$(COQDEP) -i $(COQLIBS) *.v *.ml *.mli >.depend\n"; + print "\t$(COQDEP) $(COQLIBS) -suffix .html *.v >>.depend\n"; + end; + List.iter + (fun x -> print "\t(cd "; print x; print " ; $(MAKE) depend)\n") + sds; + print "\n"; + print "xml::\n"; + List.iter + (fun x -> print "\t(cd "; print x; print " ; $(MAKE) xml)\n") + sds; + print "\n"; + print "install:\n"; + print "\tmkdir -p `$(COQC) -where`/user-contrib\n"; + if !some_vfile then print "\tcp -f *.vo `$(COQC) -where`/user-contrib\n"; + if !some_mlfile then print "\tcp -f *.cmo `$(COQC) -where`/user-contrib\n"; + List.iter + (fun x -> print "\t(cd "; print x; print " ; $(MAKE) install)\n") + sds; + print "\n"; + print "Makefile: Make\n"; + print "\tmv -f Makefile Makefile.bak\n"; + print "\t$(COQBIN)coq_makefile -f Make -o Makefile\n"; + print "\n"; + print "clean:\n"; + print "\trm -f *.cmo *.cmi *.cmx *.o *.vo *.vi *.g *~\n"; + print "\trm -f all.ps all-gal.ps $(HTMLFILES) $(GHTMLFILES)\n"; + List.iter + (fun x -> print "\t(cd "; print x; print " ; $(MAKE) clean)\n") + sds; + print "\n"; + print "archclean:\n"; + print "\trm -f *.cmx *.o\n"; + List.iter + (fun x -> print "\t(cd "; print x; print " ; $(MAKE) archclean)\n") + sds; + print "\n" + +let implicit () = + let ml_rules () = + print ".mli.cmi:\n\t$(CAMLC) $(ZDEBUG) $(ZFLAGS) $<\n\n"; + print ".ml.cmo:\n\t$(CAMLC) $(ZDEBUG) $(ZFLAGS) $<\n\n"; + print ".ml.cmx:\n\t$(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) $<\n\n"; + and v_rule () = + print ".v.vo:\n\t$(COQC) $(COQDEBUG) $(COQFLAGS) $*\n\n"; + print ".v.vi:\n\t$(COQC) -i $(COQDEBUG) $(COQFLAGS) $*\n\n"; + print ".v.g:\n\t$(GALLINA) $<\n\n"; + print ".v.tex:\n\t$(COQWEB) $< -o $@\n\n"; + print ".v.html:\n\t$(COQWEB) -html $< -o $@\n\n"; + print ".g.g.tex:\n\t$(COQWEB) $< -o $@\n\n"; + print ".g.g.html:\n\t$(COQWEB) -html $< -o $@\n\n" + and ml_suffixes = + if !some_mlfile then + [ ".mli"; ".ml"; ".cmo"; ".cmi"; ".cmx" ] + else + [] + and v_suffixes = + if !some_vfile then + [ ".v"; ".vo"; ".vi"; ".g"; ".html"; ".tex"; ".g.tex"; ".g.html" ] + else + [] + in + let suffixes = ml_suffixes @ v_suffixes in + if suffixes <> [] then begin + print ".SUFFIXES: "; print_list " " suffixes; + print "\n\n" + end; + if !some_mlfile then ml_rules (); + if !some_vfile then v_rule () + +let variables l = + let rec var_aux = function + | [] -> () + | Def(v,def) :: r -> print v; print "="; print def; print "\n"; var_aux r + | _ :: r -> var_aux r + in + section "Variables definitions."; + print "CAMLP4LIB=`camlp4 -where`\n"; +(* print "MAKE=make \"COQBIN=$(COQBIN)\" \"OPT=$(OPT)\"\n"; *) + print "COQSRC=-I $(COQTOP)/kernel -I $(COQTOP)/lib \\ + -I $(COQTOP)/library -I $(COQTOP)/parsing -I $(COQTOP)/pretyping \\ + -I $(COQTOP)/proofs -I $(COQTOP)/syntax -I $(COQTOP)/tactics \\ + -I $(COQTOP)/toplevel -I $(CAMLP4LIB)\n"; + print "ZFLAGS=$(OCAMLLIBS) $(COQSRC)\n"; + print "OPT="; if !opt = "-byte" then print "-byte"; print "\n"; + print "COQFLAGS=-q $(OPT) $(COQLIBS)\n"; + print "COQC=$(COQBIN)coqc\n"; + print "GALLINA=gallina\n"; + print "COQWEB=coqweb\n"; + print "CAMLC=ocamlc -c\n"; + print "CAMLOPTC=ocamlopt -c\n"; + print "CAMLLINK=ocamlc\n"; + print "CAMLOPTLINK=ocamlopt\n"; + print "COQDEP=$(COQBIN)coqdep -c\n"; + print "COQVO2XML=coq_vo2xml\n"; + var_aux l; + print "\n" + +let include_dirs l = + let include_aux' includeR = + let rec include_aux = function + | [] -> [] + | Include x :: r -> ("-I " ^ x) :: (include_aux r) + | RInclude (p,l) :: r when includeR -> + let l' = if l = "" then "\"\"" else l in + ("-R " ^ p ^ " " ^ l') :: (include_aux r) + | _ :: r -> include_aux r + in + include_aux + in + let i_ocaml = "-I ." :: (include_aux' false l) in + let i_coq = "-I ." :: (include_aux' true l) in + section "Libraries definition."; + print "OCAMLLIBS="; print_list "\\\n " i_ocaml; print "\n"; + print "COQLIBS="; print_list "\\\n " i_coq; print "\n\n" + +let special l = + let pr_sp (file,dependencies,com) = + print file; print ": "; print dependencies; print "\n"; + print "\t"; print com; print "\n\n" + in + let rec sp_aux = function + | [] -> [] + | Special (file,deps,com) :: r -> (file,deps,com) :: (sp_aux r) + | _ :: r -> sp_aux r + in + let sps = sp_aux l in + if sps <> [] then section "Custom targets."; + List.iter pr_sp sps + +let subdirs l = + let rec subdirs_aux = function + | [] -> [] + | Subdir x :: r -> x :: (subdirs_aux r) + | _ :: r -> subdirs_aux r + and pr_subdir s = + print s; print ":\n\tcd "; print s; print " ; $(MAKE) all\n\n" + in + let sds = subdirs_aux l in + if sds <> [] then section "Subdirectories."; + List.iter pr_subdir sds; + section "Special targets."; + print ".PHONY: "; + print_list " " + ("all" :: "opt" :: "byte" :: "archclean" :: "clean" :: "install" + :: "depend" :: "xml" :: sds); + print "\n\n"; + sds + +(* Extract gallina/html filenames (foo.v) from the list of all targets *) + +let rec other_files suff = function + | V n :: r -> + let f = (Filename.chop_suffix n ".vo") ^ suff in + f :: (other_files suff r) + | _ :: r -> + other_files suff r + | [] -> + [] + +let vfiles = other_files ".v" +let gfiles = other_files ".g" +let hfiles = other_files ".html" +let tfiles = other_files ".tex" +let vifiles = other_files ".vi" +let gtfiles l = List.map (fun f -> f ^ ".tex") (gfiles l) +let ghfiles l = List.map (fun f -> f ^ ".html") (gfiles l) +let vofiles = other_files ".vo" + +let all_target l = + let rec fnames = function + | ML n :: r -> n :: (fnames r) + | Subdir n :: r -> n :: (fnames r) + | V n :: r -> n :: (fnames r) + | Special (n,_,_) :: r -> n :: (fnames r) + | Include _ :: r -> fnames r + | RInclude _ :: r -> fnames r + | Def _ :: r -> fnames r + | [] -> [] + in + section "Definition of the \"all\" target."; + print "VFILES="; print_list "\\\n " (vfiles l); print "\n"; + print "VOFILES=$(VFILES:.v=.vo)\n"; + print "VIFILES=$(VFILES:.v=.vi)\n"; + print "GFILES=$(VFILES:.v=.g)\n"; + print "HTMLFILES=$(VFILES:.v=.html)\n"; + print "GHTMLFILES=$(VFILES:.v=.g.html)\n"; + print "\n"; + print "all: "; print_list "\\\n " (fnames l); + print "\n\n"; + if !some_vfile then begin + print "spec: $(VIFILES)\n\n"; + print "gallina: $(GFILES)\n\n"; + print "html: $(HTMLFILES)\n\n"; + print "gallinahtml: $(GHTMLFILES)\n\n"; + print "all.ps: $(VFILES)\n"; + print "\t$(COQWEB) -ps -o $@ `$(COQDEP) -sort -suffix .v $(VFILES)`\n\n"; + print "all-gal.ps: $(GFILES)\n"; + print "\t$(COQWEB) -ps -o $@ `$(COQDEP) -sort -suffix .g $(VFILES)`\n\n"; + print "xml:: .xml_time_stamp\n"; + print ".xml_time_stamp: "; print_list "\\\n " (vofiles l); + print "\n\t$(COQVO2XML) $(COQFLAGS) $(?:%.o=%)\n"; + print "\ttouch .xml_time_stamp"; + print "\n\n" + end + +let parse f = + let rec string = parser + | [< '' ' | '\n' | '\t' >] -> "" + | [< 'c; s >] -> (String.make 1 c)^(string s) + | [< >] -> "" + and string2 = parser + | [< ''"' >] -> "" + | [< 'c; s >] -> (String.make 1 c)^(string2 s) + and skip_comment = parser + | [< ''\n'; s >] -> s + | [< 'c; s >] -> skip_comment s + | [< >] -> [< >] + and args = parser + | [< '' ' | '\n' | '\t'; s >] -> args s + | [< ''#'; s >] -> args (skip_comment s) + | [< ''"'; str = string2; s >] -> ("" ^ str) :: args s + | [< 'c; str = string; s >] -> ((String.make 1 c) ^ str) :: (args s) + | [< >] -> [] + in + let c = open_in f in + let res = args (Stream.of_channel c) in + close_in c; + res + +let rec process_cmd_line = function + | [] -> + some_file := !some_file or !some_mlfile or !some_vfile; [] + | ("-h"|"--help") :: _ -> + usage () + | ("-no-opt"|"-byte") :: r -> + opt := "-byte"; process_cmd_line r + | ("-full"|"-opt") :: r -> + opt := "-opt"; process_cmd_line r + | "-custom" :: com :: dependencies :: file :: r -> + some_file := true; + Special (file,dependencies,com) :: (process_cmd_line r) + | "-I" :: d :: r -> + Include d :: (process_cmd_line r) + | "-R" :: p :: l :: r -> + RInclude (p,l) :: (process_cmd_line r) + | ("-I" | "-h" | "--help" | "-custom") :: _ -> + usage () + | "-f"::file::r -> + process_cmd_line ((parse file)@r) + | ["-f"] -> + usage () + | "-o" :: file :: r -> + output_channel := (open_out file); + (process_cmd_line r) + | v :: "=" :: def :: r -> + Def (v,def) :: (process_cmd_line r) + | f :: r -> + if Filename.check_suffix f ".v" then begin + some_vfile := true; + V (f^"o") :: (process_cmd_line r) + end else if Filename.check_suffix f ".ml" then begin + some_mlfile := true; + ML ((Filename.chop_suffix f "ml")^"cmo") :: (process_cmd_line r) + end else + Subdir f :: (process_cmd_line r) + +let banner () = + print +"############################################################################## +## The Calculus of Inductive Constructions ## +## ## +## Projet Coq ## +## ## +## INRIA ENS-CNRS ## +## Rocquencourt Lyon ## +## ## +## Coq V7 ## +## ## +## ## +############################################################################## + +" + +let warning () = + print "# WARNING\n#\n"; + print "# This Makefile has been automagically generated by coq_makefile\n"; + print "# Edit at your own risks !\n"; + print "#\n# END OF WARNING\n\n" + +let print_list l = List.iter (fun x -> print x; print " ") l + +let command_line args = + print "#\n# This Makefile was generated by the command line :\n"; + print "# coq_makefile "; + print_list args; + print "\n#\n\n" + +let directories_deps l = + let print_dep f dep = + if dep <> [] then begin print f; print ": "; print_list dep; print "\n" end + in + let rec iter ((dirs,before) as acc) = function + | [] -> + () + | (Subdir d) :: l -> + print_dep d before; iter (d :: dirs, d :: before) l + | (ML f) :: l -> + print_dep f dirs; iter (dirs, f :: before) l + | (V f) :: l -> + print_dep f dirs; iter (dirs, f :: before) l + | (Special (f,_,_)) :: l -> + print_dep f dirs; iter (dirs, f :: before) l + | _ :: l -> + iter acc l + in + iter ([],[]) l + +let do_makefile args = + let l = process_cmd_line args in + banner (); + warning (); + command_line args; + variables l; + include_dirs l; + all_target l; + special l; + let sds = subdirs l in + implicit (); + standard sds; + (* TEST directories_deps l; *) + warning (); + if not (!output_channel == stdout) then close_out !output_channel; + exit 0 + +let main () = + let args = + if Array.length Sys.argv = 1 then usage (); + List.tl (Array.to_list Sys.argv) + in + do_makefile args + +let _ = Printexc.catch main () + -- cgit v1.2.3