diff options
| -rw-r--r-- | .depend | 190 | ||||
| -rw-r--r-- | Makefile | 12 | ||||
| -rw-r--r-- | contrib/interface/name_to_ast.ml | 2 | ||||
| -rw-r--r-- | contrib/interface/xlate.ml | 4 | ||||
| -rw-r--r-- | lib/options.ml | 6 | ||||
| -rw-r--r-- | lib/options.mli | 5 | ||||
| -rw-r--r-- | library/decl_kinds.ml | 7 | ||||
| -rw-r--r-- | parsing/g_vernac.ml4 | 18 | ||||
| -rw-r--r-- | parsing/lexer.ml4 | 69 | ||||
| -rw-r--r-- | parsing/lexer.mli | 4 | ||||
| -rw-r--r-- | scripts/coqc.ml | 2 | ||||
| -rw-r--r-- | toplevel/coqtop.ml | 3 | ||||
| -rw-r--r-- | toplevel/vernac.ml | 17 | ||||
| -rw-r--r-- | toplevel/vernacentries.ml | 2 | ||||
| -rw-r--r-- | toplevel/vernacexpr.ml | 2 | ||||
| -rw-r--r-- | translate/ppconstrnew.ml | 370 | ||||
| -rw-r--r-- | translate/ppconstrnew.mli | 41 | ||||
| -rw-r--r-- | translate/pptacticnew.ml | 595 | ||||
| -rw-r--r-- | translate/pptacticnew.mli | 33 | ||||
| -rw-r--r-- | translate/ppvernacnew.ml | 499 | ||||
| -rw-r--r-- | translate/ppvernacnew.mli | 31 |
21 files changed, 1813 insertions, 99 deletions
@@ -39,10 +39,10 @@ kernel/indtypes.cmi: kernel/declarations.cmi kernel/entries.cmi \ kernel/univ.cmi kernel/inductive.cmi: kernel/declarations.cmi kernel/environ.cmi \ kernel/names.cmi kernel/term.cmi kernel/univ.cmi -kernel/mod_typing.cmi: kernel/declarations.cmi kernel/entries.cmi \ - kernel/environ.cmi kernel/modops.cmi: kernel/declarations.cmi kernel/entries.cmi \ kernel/environ.cmi kernel/names.cmi kernel/univ.cmi lib/util.cmi +kernel/mod_typing.cmi: kernel/declarations.cmi kernel/entries.cmi \ + kernel/environ.cmi kernel/names.cmi: lib/pp.cmi lib/predicate.cmi kernel/reduction.cmi: kernel/environ.cmi kernel/sign.cmi kernel/term.cmi \ kernel/univ.cmi @@ -62,9 +62,6 @@ kernel/typeops.cmi: kernel/entries.cmi kernel/environ.cmi kernel/names.cmi \ kernel/univ.cmi: kernel/names.cmi lib/pp.cmi lib/bignat.cmi: lib/pp.cmi lib/pp.cmi: lib/pp_control.cmi -lib/rtree.cmi: lib/pp.cmi -lib/system.cmi: lib/pp.cmi -lib/util.cmi: lib/pp.cmi library/declare.cmi: kernel/cooking.cmi library/decl_kinds.cmo \ kernel/declarations.cmi library/dischargedhypsmap.cmi kernel/entries.cmi \ kernel/indtypes.cmi library/libnames.cmi library/libobject.cmi \ @@ -94,6 +91,9 @@ library/nameops.cmi: kernel/names.cmi lib/pp.cmi library/nametab.cmi: library/libnames.cmi kernel/names.cmi lib/pp.cmi \ kernel/sign.cmi lib/util.cmi library/summary.cmi: library/libnames.cmi kernel/names.cmi +lib/rtree.cmi: lib/pp.cmi +lib/system.cmi: lib/pp.cmi +lib/util.cmi: lib/pp.cmi parsing/ast.cmi: parsing/coqast.cmi lib/dyn.cmi interp/genarg.cmi \ library/libnames.cmi kernel/names.cmi lib/pp.cmi interp/topconstr.cmi \ lib/util.cmi @@ -305,20 +305,32 @@ toplevel/recordobj.cmi: library/libnames.cmi proofs/tacexpr.cmo 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/pcoq.cmi lib/util.cmi toplevel/vernacexpr.cmo toplevel/vernacentries.cmi: kernel/environ.cmi pretyping/evd.cmi \ library/libnames.cmi kernel/names.cmi kernel/term.cmi \ interp/topconstr.cmi toplevel/vernacexpr.cmo toplevel/vernacinterp.cmi toplevel/vernacinterp.cmi: proofs/tacexpr.cmo +toplevel/vernac.cmi: parsing/pcoq.cmi lib/util.cmi toplevel/vernacexpr.cmo +translate/ppconstrnew.cmi: parsing/coqast.cmi kernel/environ.cmi \ + parsing/extend.cmi library/libnames.cmi kernel/names.cmi parsing/pcoq.cmi \ + lib/pp.cmi pretyping/rawterm.cmi proofs/tacexpr.cmo kernel/term.cmi \ + interp/topconstr.cmi lib/util.cmi +translate/pptacticnew.cmi: parsing/egrammar.cmi interp/genarg.cmi lib/pp.cmi \ + proofs/proof_type.cmi proofs/tacexpr.cmo +translate/ppvernacnew.cmi: parsing/ast.cmi parsing/coqast.cmi \ + parsing/extend.cmi interp/genarg.cmi library/libnames.cmi \ + library/nameops.cmi kernel/names.cmi library/nametab.cmi parsing/pcoq.cmi \ + lib/pp.cmi parsing/ppconstr.cmi interp/ppextend.cmi parsing/pptactic.cmi \ + pretyping/rawterm.cmi interp/topconstr.cmi lib/util.cmi \ + toplevel/vernacexpr.cmo contrib/cc/ccalgo.cmi: kernel/names.cmi kernel/term.cmi contrib/cc/ccproof.cmi: contrib/cc/ccalgo.cmi kernel/names.cmi contrib/correctness/past.cmi: kernel/names.cmi contrib/correctness/ptype.cmi \ kernel/term.cmi interp/topconstr.cmi lib/util.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 @@ -428,6 +440,10 @@ dev/top_printers.cmx: parsing/ast.cmx toplevel/cerrors.cmx proofs/clenv.cmx \ pretyping/termops.cmx kernel/univ.cmx doc/parse.cmo: parsing/ast.cmi doc/parse.cmx: parsing/ast.cmx +ide/coqide.cmo: ide/coq.cmi ide/find_phrase.cmo ide/highlight.cmo \ + lib/pp_control.cmi toplevel/vernacexpr.cmo +ide/coqide.cmx: ide/coq.cmx ide/find_phrase.cmx ide/highlight.cmx \ + lib/pp_control.cmx toplevel/vernacexpr.cmx ide/coq.cmo: toplevel/cerrors.cmi toplevel/coqtop.cmi kernel/environ.cmi \ pretyping/evarutil.cmi pretyping/evd.cmi kernel/names.cmi lib/options.cmi \ parsing/pcoq.cmi proofs/pfedit.cmi lib/pp.cmi parsing/printer.cmi \ @@ -440,10 +456,6 @@ ide/coq.cmx: toplevel/cerrors.cmx toplevel/coqtop.cmx kernel/environ.cmx \ proofs/proof_trees.cmx proofs/refiner.cmx proofs/tacmach.cmx \ kernel/term.cmx lib/util.cmx toplevel/vernac.cmx toplevel/vernacexpr.cmx \ ide/coq.cmi -ide/coqide.cmo: ide/coq.cmi ide/find_phrase.cmo ide/highlight.cmo \ - lib/pp_control.cmi toplevel/vernacexpr.cmo -ide/coqide.cmx: ide/coq.cmx ide/find_phrase.cmx ide/highlight.cmx \ - lib/pp_control.cmx toplevel/vernacexpr.cmx interp/constrextern.cmo: pretyping/classops.cmi library/declare.cmi \ pretyping/detyping.cmi kernel/environ.cmi library/impargs.cmi \ kernel/inductive.cmi library/libnames.cmi library/nameops.cmi \ @@ -568,6 +580,12 @@ kernel/inductive.cmo: kernel/declarations.cmi kernel/environ.cmi \ kernel/inductive.cmx: kernel/declarations.cmx kernel/environ.cmx \ kernel/names.cmx kernel/reduction.cmx kernel/sign.cmx kernel/term.cmx \ kernel/type_errors.cmx kernel/univ.cmx lib/util.cmx kernel/inductive.cmi +kernel/modops.cmo: kernel/declarations.cmi kernel/entries.cmi \ + kernel/environ.cmi kernel/names.cmi lib/pp.cmi kernel/term.cmi \ + kernel/univ.cmi lib/util.cmi kernel/modops.cmi +kernel/modops.cmx: kernel/declarations.cmx kernel/entries.cmx \ + kernel/environ.cmx kernel/names.cmx lib/pp.cmx kernel/term.cmx \ + kernel/univ.cmx lib/util.cmx kernel/modops.cmi kernel/mod_typing.cmo: kernel/declarations.cmi kernel/entries.cmi \ kernel/environ.cmi kernel/modops.cmi kernel/names.cmi \ kernel/reduction.cmi kernel/subtyping.cmi kernel/term_typing.cmi \ @@ -576,12 +594,6 @@ kernel/mod_typing.cmx: kernel/declarations.cmx kernel/entries.cmx \ kernel/environ.cmx kernel/modops.cmx kernel/names.cmx \ kernel/reduction.cmx kernel/subtyping.cmx kernel/term_typing.cmx \ kernel/typeops.cmx kernel/univ.cmx lib/util.cmx kernel/mod_typing.cmi -kernel/modops.cmo: kernel/declarations.cmi kernel/entries.cmi \ - kernel/environ.cmi kernel/names.cmi lib/pp.cmi kernel/term.cmi \ - kernel/univ.cmi lib/util.cmi kernel/modops.cmi -kernel/modops.cmx: kernel/declarations.cmx kernel/entries.cmx \ - kernel/environ.cmx kernel/names.cmx lib/pp.cmx kernel/term.cmx \ - kernel/univ.cmx lib/util.cmx kernel/modops.cmi kernel/names.cmo: lib/hashcons.cmi lib/pp.cmi lib/predicate.cmi lib/util.cmi \ kernel/names.cmi kernel/names.cmx: lib/hashcons.cmx lib/pp.cmx lib/predicate.cmx lib/util.cmx \ @@ -664,34 +676,24 @@ 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/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/gmap.cmo: lib/gmap.cmi +lib/gmap.cmx: lib/gmap.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.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/pp.cmo: lib/pp_control.cmi lib/pp.cmi +lib/pp.cmx: lib/pp_control.cmx lib/pp.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/rtree.cmo: lib/pp.cmi lib/util.cmi lib/rtree.cmi -lib/rtree.cmx: lib/pp.cmx lib/util.cmx lib/rtree.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: library/decl_kinds.cmo kernel/declarations.cmi \ library/dischargedhypsmap.cmi kernel/entries.cmi kernel/environ.cmi \ library/global.cmi library/impargs.cmi kernel/indtypes.cmi \ @@ -796,6 +798,16 @@ library/states.cmx: library/lib.cmx library/library.cmx library/summary.cmx \ lib/system.cmx library/states.cmi library/summary.cmo: lib/dyn.cmi lib/pp.cmi lib/util.cmi library/summary.cmi library/summary.cmx: lib/dyn.cmx lib/pp.cmx lib/util.cmx library/summary.cmi +lib/rtree.cmo: lib/pp.cmi lib/util.cmi lib/rtree.cmi +lib/rtree.cmx: lib/pp.cmx lib/util.cmx lib/rtree.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/argextend.cmo: parsing/ast.cmi interp/genarg.cmi parsing/pcoq.cmi \ parsing/q_coqast.cmo parsing/q_util.cmi lib/util.cmi \ toplevel/vernacexpr.cmo @@ -938,8 +950,8 @@ parsing/g_zsyntax.cmx: parsing/ast.cmx lib/bignat.cmx parsing/coqast.cmx \ kernel/names.cmx library/nametab.cmx parsing/pcoq.cmx lib/pp.cmx \ pretyping/rawterm.cmx interp/symbols.cmx parsing/termast.cmx \ interp/topconstr.cmx lib/util.cmx parsing/g_zsyntax.cmi -parsing/lexer.cmo: parsing/lexer.cmi -parsing/lexer.cmx: parsing/lexer.cmi +parsing/lexer.cmo: lib/pp.cmi parsing/lexer.cmi +parsing/lexer.cmx: lib/pp.cmx parsing/lexer.cmi parsing/pcoq.cmo: parsing/ast.cmi parsing/coqast.cmi library/decl_kinds.cmo \ parsing/extend.cmi interp/genarg.cmi parsing/lexer.cmi \ library/libnames.cmi kernel/names.cmi lib/options.cmi lib/pp.cmi \ @@ -1806,10 +1818,10 @@ tactics/wcclausenv.cmx: proofs/clenv.cmx kernel/environ.cmx \ pretyping/reductionops.cmx proofs/refiner.cmx kernel/sign.cmx \ proofs/tacmach.cmx kernel/term.cmx pretyping/termops.cmx lib/util.cmx \ tactics/wcclausenv.cmi -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/coq_vo2xml.cmo: config/coq_config.cmi toplevel/usage.cmi +tools/coq_vo2xml.cmx: config/coq_config.cmx toplevel/usage.cmx tools/gallina.cmo: tools/gallina_lexer.cmo tools/gallina.cmx: tools/gallina_lexer.cmx toplevel/cerrors.cmo: parsing/ast.cmi pretyping/cases.cmi toplevel/himsg.cmi \ @@ -2012,16 +2024,6 @@ toplevel/toplevel.cmx: toplevel/cerrors.cmx library/lib.cmx \ toplevel/vernac.cmx toplevel/vernacexpr.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/coqast.cmi library/lib.cmi library/library.cmi \ - kernel/names.cmi lib/options.cmi parsing/pcoq.cmi proofs/pfedit.cmi \ - lib/pp.cmi library/states.cmi lib/system.cmi lib/util.cmi \ - toplevel/vernacentries.cmi toplevel/vernacexpr.cmo \ - toplevel/vernacinterp.cmi toplevel/vernac.cmi -toplevel/vernac.cmx: parsing/coqast.cmx library/lib.cmx library/library.cmx \ - kernel/names.cmx lib/options.cmx parsing/pcoq.cmx proofs/pfedit.cmx \ - lib/pp.cmx library/states.cmx lib/system.cmx lib/util.cmx \ - toplevel/vernacentries.cmx toplevel/vernacexpr.cmx \ - toplevel/vernacinterp.cmx toplevel/vernac.cmi toplevel/vernacentries.cmo: tactics/auto.cmi toplevel/class.cmi \ pretyping/classops.cmi toplevel/command.cmi interp/constrextern.cmi \ interp/constrintern.cmi library/decl_kinds.cmo library/declaremods.cmi \ @@ -2082,6 +2084,54 @@ toplevel/vernacinterp.cmx: parsing/ast.cmx parsing/coqast.cmx \ kernel/names.cmx lib/options.cmx lib/pp.cmx proofs/proof_type.cmx \ proofs/tacexpr.cmx tactics/tacinterp.cmx lib/util.cmx \ toplevel/vernacexpr.cmx toplevel/vernacinterp.cmi +toplevel/vernac.cmo: parsing/coqast.cmi parsing/lexer.cmi library/lib.cmi \ + library/library.cmi kernel/names.cmi lib/options.cmi parsing/pcoq.cmi \ + proofs/pfedit.cmi lib/pp.cmi translate/ppvernacnew.cmi library/states.cmi \ + lib/system.cmi lib/util.cmi toplevel/vernacentries.cmi \ + toplevel/vernacexpr.cmo toplevel/vernacinterp.cmi toplevel/vernac.cmi +toplevel/vernac.cmx: parsing/coqast.cmx parsing/lexer.cmx library/lib.cmx \ + library/library.cmx kernel/names.cmx lib/options.cmx parsing/pcoq.cmx \ + proofs/pfedit.cmx lib/pp.cmx translate/ppvernacnew.cmx library/states.cmx \ + lib/system.cmx lib/util.cmx toplevel/vernacentries.cmx \ + toplevel/vernacexpr.cmx toplevel/vernacinterp.cmx toplevel/vernac.cmi +translate/ppconstrnew.cmo: parsing/ast.cmi lib/bignat.cmi parsing/coqast.cmi \ + lib/dyn.cmi parsing/esyntax.cmi interp/genarg.cmi library/libnames.cmi \ + library/nameops.cmi kernel/names.cmi library/nametab.cmi lib/pp.cmi \ + interp/ppextend.cmi pretyping/rawterm.cmi interp/symbols.cmi \ + kernel/term.cmi parsing/termast.cmi interp/topconstr.cmi lib/util.cmi \ + translate/ppconstrnew.cmi +translate/ppconstrnew.cmx: parsing/ast.cmx lib/bignat.cmx parsing/coqast.cmx \ + lib/dyn.cmx parsing/esyntax.cmx interp/genarg.cmx library/libnames.cmx \ + library/nameops.cmx kernel/names.cmx library/nametab.cmx lib/pp.cmx \ + interp/ppextend.cmx pretyping/rawterm.cmx interp/symbols.cmx \ + kernel/term.cmx parsing/termast.cmx interp/topconstr.cmx lib/util.cmx \ + translate/ppconstrnew.cmi +translate/pptacticnew.cmo: kernel/closure.cmi lib/dyn.cmi \ + parsing/egrammar.cmi parsing/extend.cmi interp/genarg.cmi \ + library/libnames.cmi library/nameops.cmi kernel/names.cmi lib/pp.cmi \ + parsing/ppconstr.cmi translate/ppconstrnew.cmi parsing/printer.cmi \ + pretyping/rawterm.cmi proofs/tacexpr.cmo kernel/term.cmi \ + interp/topconstr.cmi lib/util.cmi translate/pptacticnew.cmi +translate/pptacticnew.cmx: kernel/closure.cmx lib/dyn.cmx \ + parsing/egrammar.cmx parsing/extend.cmx interp/genarg.cmx \ + library/libnames.cmx library/nameops.cmx kernel/names.cmx lib/pp.cmx \ + parsing/ppconstr.cmx translate/ppconstrnew.cmx parsing/printer.cmx \ + pretyping/rawterm.cmx proofs/tacexpr.cmx kernel/term.cmx \ + interp/topconstr.cmx lib/util.cmx translate/pptacticnew.cmi +translate/ppvernacnew.cmo: parsing/ast.cmi parsing/coqast.cmi \ + library/decl_kinds.cmo parsing/extend.cmi interp/genarg.cmi \ + library/goptions.cmi library/libnames.cmi library/nameops.cmi \ + kernel/names.cmi library/nametab.cmi parsing/pcoq.cmi lib/pp.cmi \ + translate/ppconstrnew.cmi interp/ppextend.cmi translate/pptacticnew.cmi \ + pretyping/rawterm.cmi proofs/tacexpr.cmo interp/topconstr.cmi \ + lib/util.cmi toplevel/vernacexpr.cmo translate/ppvernacnew.cmi +translate/ppvernacnew.cmx: parsing/ast.cmx parsing/coqast.cmx \ + library/decl_kinds.cmx parsing/extend.cmx interp/genarg.cmx \ + library/goptions.cmx library/libnames.cmx library/nameops.cmx \ + kernel/names.cmx library/nametab.cmx parsing/pcoq.cmx lib/pp.cmx \ + translate/ppconstrnew.cmx interp/ppextend.cmx translate/pptacticnew.cmx \ + pretyping/rawterm.cmx proofs/tacexpr.cmx interp/topconstr.cmx \ + lib/util.cmx toplevel/vernacexpr.cmx translate/ppvernacnew.cmi contrib/cc/ccalgo.cmo: kernel/names.cmi kernel/term.cmi contrib/cc/ccalgo.cmi contrib/cc/ccalgo.cmx: kernel/names.cmx kernel/term.cmx contrib/cc/ccalgo.cmi contrib/cc/ccproof.cmo: contrib/cc/ccalgo.cmi kernel/names.cmi \ @@ -2102,6 +2152,18 @@ contrib/cc/cctac.cmx: contrib/cc/ccalgo.cmx contrib/cc/ccproof.cmx \ lib/pp.cmx parsing/pptactic.cmx proofs/proof_type.cmx proofs/refiner.cmx \ tactics/tacinterp.cmx proofs/tacmach.cmx tactics/tacticals.cmx \ tactics/tactics.cmx kernel/term.cmx lib/util.cmx +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: kernel/declarations.cmi library/declare.cmi \ pretyping/detyping.cmi kernel/entries.cmi library/global.cmi \ kernel/indtypes.cmi library/libnames.cmi library/nameops.cmi \ @@ -2118,18 +2180,6 @@ contrib/correctness/pcic.cmx: kernel/declarations.cmx library/declare.cmx \ kernel/sign.cmx kernel/term.cmx pretyping/termops.cmx \ interp/topconstr.cmx kernel/typeops.cmx lib/util.cmx \ toplevel/vernacexpr.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 \ @@ -2670,6 +2720,14 @@ contrib/interface/pbp.cmx: interp/coqlib.cmx kernel/environ.cmx \ tactics/tacinterp.cmx proofs/tacmach.cmx tactics/tacticals.cmx \ tactics/tactics.cmx kernel/term.cmx interp/topconstr.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: proofs/clenv.cmi interp/constrintern.cmi \ parsing/coqast.cmi kernel/declarations.cmi kernel/environ.cmi \ pretyping/evd.cmi interp/genarg.cmi library/global.cmi \ @@ -2694,14 +2752,6 @@ contrib/interface/showproof.cmx: proofs/clenv.cmx interp/constrintern.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 \ interp/constrextern.cmi contrib/interface/ctast.cmo kernel/environ.cmi \ pretyping/evarutil.cmi pretyping/evd.cmi library/libobject.cmi \ @@ -2874,12 +2924,12 @@ contrib/romega/refl_omega.cmx: parsing/ast.cmx tactics/auto.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/acic.cmo: kernel/names.cmi kernel/term.cmi -contrib/xml/acic.cmx: kernel/names.cmx kernel/term.cmx contrib/xml/acic2Xml.cmo: contrib/xml/acic.cmo contrib/xml/cic2acic.cmo \ kernel/names.cmi kernel/term.cmi lib/util.cmi contrib/xml/xml.cmi contrib/xml/acic2Xml.cmx: contrib/xml/acic.cmx contrib/xml/cic2acic.cmx \ kernel/names.cmx kernel/term.cmx lib/util.cmx contrib/xml/xml.cmx +contrib/xml/acic.cmo: kernel/names.cmi kernel/term.cmi +contrib/xml/acic.cmx: kernel/names.cmx kernel/term.cmx contrib/xml/cic2acic.cmo: contrib/xml/acic.cmo library/declare.cmi \ library/dischargedhypsmap.cmi contrib/xml/doubleTypeInference.cmi \ kernel/environ.cmi pretyping/evarutil.cmi pretyping/evd.cmi \ @@ -2934,8 +2984,6 @@ contrib/xml/proofTree2Xml.cmx: contrib/xml/acic.cmx contrib/xml/acic2Xml.cmx \ contrib/xml/xml.cmx contrib/xml/unshare.cmo: contrib/xml/unshare.cmi contrib/xml/unshare.cmx: contrib/xml/unshare.cmi -contrib/xml/xml.cmo: contrib/xml/xml.cmi -contrib/xml/xml.cmx: contrib/xml/xml.cmi contrib/xml/xmlcommand.cmo: contrib/xml/acic.cmo contrib/xml/acic2Xml.cmo \ contrib/xml/cic2acic.cmo library/decl_kinds.cmo kernel/declarations.cmi \ library/declare.cmi kernel/environ.cmi pretyping/evd.cmi \ @@ -2962,6 +3010,8 @@ contrib/xml/xmlentries.cmx: toplevel/cerrors.cmx parsing/egrammar.cmx \ parsing/extend.cmx interp/genarg.cmx parsing/pcoq.cmx lib/pp.cmx \ parsing/pptactic.cmx tactics/tacinterp.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 tactics/tauto.cmx: parsing/grammar.cma tactics/newtauto.cmo: parsing/grammar.cma @@ -39,7 +39,7 @@ noargument: LOCALINCLUDES=-I config -I tools -I scripts -I lib -I kernel -I library \ -I proofs -I tactics -I pretyping \ - -I interp -I toplevel -I parsing -I ide \ + -I interp -I toplevel -I parsing -I ide -I translate \ -I contrib/omega -I contrib/romega \ -I contrib/ring -I contrib/xml \ -I contrib/extraction -I contrib/correctness \ @@ -121,6 +121,9 @@ PARSING=\ parsing/ppconstr.cmo parsing/printer.cmo parsing/pptactic.cmo \ parsing/printmod.cmo parsing/prettyp.cmo parsing/search.cmo +TRANSLATE=\ + translate/ppconstrnew.cmo translate/pptacticnew.cmo translate/ppvernacnew.cmo + HIGHPARSING=\ parsing/g_prim.cmo parsing/g_basevernac.cmo \ parsing/g_vernac.cmo parsing/g_proofs.cmo parsing/g_tactic.cmo \ @@ -148,7 +151,7 @@ TACTICS=\ TOPLEVEL=\ toplevel/himsg.cmo toplevel/cerrors.cmo toplevel/class.cmo \ toplevel/command.cmo toplevel/record.cmo toplevel/recordobj.cmo \ - toplevel/discharge.cmo toplevel/vernacexpr.cmo \ + toplevel/discharge.cmo toplevel/vernacexpr.cmo $(TRANSLATE) \ toplevel/vernacinterp.cmo toplevel/mltop.cmo \ parsing/pcoq.cmo parsing/egrammar.cmo toplevel/metasyntax.cmo \ toplevel/vernacentries.cmo toplevel/vernac.cmo \ @@ -226,7 +229,7 @@ PARSERREQUIRES=\ pretyping/detyping.cmo parsing/termast.cmo interp/modintern.cmo \ interp/constrextern.cmo parsing/egrammar.cmo parsing/esyntax.cmo \ toplevel/metasyntax.cmo parsing/g_prim.cmo parsing/g_basevernac.cmo \ - parsing/ppconstr.cmo parsing/printer.cmo parsing/pptactic.cmo \ + parsing/ppconstr.cmo parsing/printer.cmo parsing/pptactic.cmo $(TRANSLATE) \ pretyping/typing.cmo proofs/proof_trees.cmo \ proofs/logic.cmo proofs/refiner.cmo proofs/evar_refiner.cmo \ proofs/tacmach.cmo toplevel/himsg.cmo parsing/g_natsyntax.cmo \ @@ -354,7 +357,7 @@ CMA=$(CLIBS) $(CAMLP4OBJS) CMXA=$(CMA:.cma=.cmxa) CMO=$(CONFIG) $(LIBREP) $(KERNEL) $(LIBRARY) $(PRETYPING) \ - $(PROOFS) $(TACTICS) $(INTERP) $(PARSING) $(TOPLEVEL) \ + $(PROOFS) $(TACTICS) $(INTERP) $(PARSING) $(TRANSLATE) $(TOPLEVEL) \ $(HIGHPARSING) $(HIGHTACTICS) $(CONTRIB) CMX=$(CMO:.cmo=.cmx) @@ -468,6 +471,7 @@ pretyping: $(PRETYPING) highparsing: $(HIGHPARSING) toplevel: $(TOPLEVEL) hightactics: $(HIGHTACTICS) +translate: $(TRANSLATE) # special binaries for debugging diff --git a/contrib/interface/name_to_ast.ml b/contrib/interface/name_to_ast.ml index 039127cc5..4150a0948 100644 --- a/contrib/interface/name_to_ast.ml +++ b/contrib/interface/name_to_ast.ml @@ -159,7 +159,7 @@ let make_variable_ast name typ implicits = let make_definition_ast name c typ implicits = VernacDefinition (Global, name, DefineBody ([], None, (constr_to_ast c), Some (constr_to_ast (body_of_type typ))), - (fun _ _ -> ())) + (fun _ _ -> ()),GDefinition) ::(implicits_to_ast_list implicits);; (* This function is inspired by print_constant *) diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml index e9995e559..de4821eee 100644 --- a/contrib/interface/xlate.ml +++ b/contrib/interface/xlate.ml @@ -1468,11 +1468,11 @@ let xlate_vernac = xlate_error "TODO: VernacStartTheoremProof" | VernacSuspend -> CT_suspend | VernacResume idopt -> CT_resume (xlate_ident_opt (option_app snd idopt)) - | VernacDefinition (k,s,ProveBody (bl,typ),_) -> + | VernacDefinition (k,s,ProveBody (bl,typ),_,_) -> if bl <> [] then xlate_error "TODO: Def bindings"; CT_coerce_THEOREM_GOAL_to_COMMAND( CT_theorem_goal (CT_coerce_DEFN_to_DEFN_OR_THM (xlate_defn k), xlate_ident s,xlate_formula typ)) - | VernacDefinition (kind,s,DefineBody(bl,red_option,c,typ_opt),_) -> + | VernacDefinition (kind,s,DefineBody(bl,red_option,c,typ_opt),_,_) -> CT_definition (xlate_defn kind, xlate_ident s, xlate_binder_list bl, cvt_optional_eval_for_definition c red_option, diff --git a/lib/options.ml b/lib/options.ml index cd0de97a4..f2cc7a09d 100644 --- a/lib/options.ml +++ b/lib/options.ml @@ -26,6 +26,12 @@ let xml_export = ref false let v7 = ref true +(* Translate *) +let translate = ref false +let make_translate f = translate := f; () +let do_translate () = !translate +let translate_file = ref false + (* Silent / Verbose *) let silent = ref false let make_silent flag = silent := flag; () diff --git a/lib/options.mli b/lib/options.mli index 59617ec34..af08f689e 100644 --- a/lib/options.mli +++ b/lib/options.mli @@ -25,6 +25,11 @@ val xml_export : bool ref val v7 : bool ref +val translate : bool ref +val make_translate : bool -> unit +val do_translate : unit -> bool +val translate_file : bool ref + val make_silent : bool -> unit val is_silent : unit -> bool val is_verbose : unit -> bool diff --git a/library/decl_kinds.ml b/library/decl_kinds.ml index 566da65d6..cd7c666bb 100644 --- a/library/decl_kinds.ml +++ b/library/decl_kinds.ml @@ -18,6 +18,13 @@ type theorem_kind = | Fact | Remark +type definitionkind = + | LDefinition + | GDefinition + | LCoercion + | GCoercion + | SCanonical + type locality_flag = (*bool (* local = true; global = false *)*) | Local | Global diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index e8268e038..f4315529d 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -102,10 +102,10 @@ GEXTEND Gram | IDENT "Remark" -> Remark ] ] ; def_token: - [ [ "Definition" -> (fun _ _ -> ()), Global - | IDENT "Local" -> (fun _ _ -> ()), Local - | IDENT "SubClass" -> Class.add_subclass_hook, Global - | IDENT "Local"; IDENT "SubClass" -> Class.add_subclass_hook, Local ] ] + [ [ "Definition" -> (fun _ _ -> ()), Global, GDefinition + | IDENT "Local" -> (fun _ _ -> ()), Local, LDefinition + | IDENT "SubClass" -> Class.add_subclass_hook, Global, GCoercion + | IDENT "Local"; IDENT "SubClass" -> Class.add_subclass_hook, Local, LCoercion ] ] ; assumption_token: [ [ "Hypothesis" -> (Local, Logical) @@ -178,8 +178,8 @@ GEXTEND Gram (* Definition, Theorem, Variable, Axiom, ... *) [ [ thm = thm_token; id = base_ident; bl = binders_list; ":"; c = constr -> VernacStartTheoremProof (thm, id, (bl, c), false, (fun _ _ -> ())) - | (f,d) = def_token; id = base_ident; b = def_body -> - VernacDefinition (d, id, b, f) + | (f,d,e) = def_token; id = base_ident; b = def_body -> + VernacDefinition (d, id, b, f, e) | stre = assumption_token; bl = ne_params_list -> VernacAssumption (stre, bl) | stre = assumptions_token; bl = ne_params_list -> @@ -383,17 +383,17 @@ GEXTEND Gram VernacCanonical qid | IDENT "Canonical"; IDENT "Structure"; qid = global; d = def_body -> let s = Ast.coerce_global_to_id qid in - VernacDefinition (Global,s,d,Recordobj.add_object_hook) + VernacDefinition (Global,s,d,Recordobj.add_object_hook,SCanonical) (* Rem: LOBJECT, OBJCOERCION, LOBJCOERCION have been removed (they were unused and undocumented) *) (* Coercions *) | IDENT "Coercion"; qid = global; d = def_body -> let s = Ast.coerce_global_to_id qid in - VernacDefinition (Global,s,d,Class.add_coercion_hook) + VernacDefinition (Global,s,d,Class.add_coercion_hook,GCoercion) | IDENT "Coercion"; IDENT "Local"; qid = global; d = def_body -> let s = Ast.coerce_global_to_id qid in - VernacDefinition (Local,s,d,Class.add_coercion_hook) + VernacDefinition (Local,s,d,Class.add_coercion_hook,LCoercion) | IDENT "Identity"; IDENT "Coercion"; IDENT "Local"; f = base_ident; ":"; s = class_rawexpr; ">->"; t = class_rawexpr -> VernacIdentityCoercion (Local, f, s, t) diff --git a/parsing/lexer.ml4 b/parsing/lexer.ml4 index cb0f07111..2d84593bc 100644 --- a/parsing/lexer.ml4 +++ b/parsing/lexer.ml4 @@ -8,6 +8,7 @@ (*i $Id$ i*) +open Pp open Token (* Dictionaries: trees annotated with string options, each node being a map @@ -195,20 +196,54 @@ let rec string bp len = parser | [< _ = Stream.empty >] ep -> err (bp, ep) Unterminated_string | [< 'c; s >] -> string bp (store len c) s +let comments = ref None + +type commentar = + | InVernac + | InVernacEsc of string + | BeVernac of string + | InComment of string + +let current = ref (BeVernac "") + +let add_comment () = let reinit () = match ! current with + | InVernac -> () + | InVernacEsc s -> current := InVernacEsc "" + | BeVernac s -> current := BeVernac "" + | InComment s -> current := InComment "" in +match (!comments,!current) with + | None , InVernac -> () + | None , BeVernac s | None , InComment s | None , InVernacEsc s -> reinit (); comments := Some [str s] + | Some _ , InVernac -> () + | Some l , BeVernac s | Some l , InComment s | Some l , InVernacEsc s -> reinit (); comments := Some (str s::l) + +let add_comment_pp s = match !comments with + | None -> comments := Some [s] + | Some l -> comments := Some (s::l) + +let add_string s = match !current with + | InVernac -> () + | InVernacEsc t -> current := InVernacEsc (t^s) + | BeVernac t -> current := BeVernac (t^s) + | InComment t -> current := InComment (t^s) + let rec comment bp = parser | [< ''('; _ = (parser - | [< ''*'; _ = comment bp >] -> () - | [< >] -> ()); + | [< ''*'; s >] -> add_string "(*"; comment bp s + | [< >] -> add_string "(" ); s >] -> comment bp s | [< ''*'; _ = parser - | [< '')' >] -> () - | [< s >] -> comment bp s >] -> () + | [< '')' >] -> add_string "*)"; add_comment () + | [< s >] -> add_string "*"; comment bp s >] -> () | [< ''"'; _ = (parser bp [< _ = string bp 0 >] -> ()); s >] -> comment bp s | [< _ = Stream.empty >] ep -> err (bp, ep) Unterminated_comment - | [< '_; s >] -> comment bp s + | [< '_ as z; s >] -> + (match z with + | '\n' | '\t' -> add_comment (); add_comment_pp (fnl ()) + | _ -> add_string (String.make 1 z)); comment bp s (* Parse a special token, using the [token_tree] *) @@ -235,21 +270,28 @@ let process_chars bp c cs = (* Parse a token in a char stream *) let rec next_token = parser bp - | [< '' ' | '\n' | '\r'| '\t'; s >] -> next_token s + | [< ''\n'; s >] -> (match !current with + | BeVernac s -> current := InComment s + | InComment _ -> add_comment_pp (fnl ()) + | _ -> ()); next_token s + | [< '' ' | '\t'; s >] -> (match !current with + | BeVernac _ | InComment _ -> add_comment_pp (spc ()) + | _ -> ()); next_token s + | [< ''\r'; s >] -> next_token s | [< ''$'; len = ident (store 0 '$') >] ep -> (("METAIDENT", get_buff len), (bp,ep)) | [< ''.' as c; t = parser | [< ' ('_' | 'a'..'z' | 'A'..'Z' | '\192'..'\214' | '\216'..'\246' | '\248'..'\255' as c); - len = ident (store 0 c) >] -> ("FIELD", get_buff len) + len = ident (store 0 c) >] -> current:=BeVernac ""; ("FIELD", get_buff len) (* | [< >] -> ("", ".") >] ep -> (t, (bp,ep)) *) - | [< (t,_) = process_chars bp c >] -> t >] ep -> (t, (bp,ep)) + | [< (t,_) = process_chars bp c >] -> t >] ep -> current:=BeVernac ""; (t, (bp,ep)) | [< ' ('_' | 'a'..'z' | 'A'..'Z' | '\192'..'\214' | '\216'..'\246' | '\248'..'\255' as c); len = ident (store 0 c) >] ep -> - let id = get_buff len in + let id = get_buff len in current:=InVernac; (try ("", find_keyword id) with Not_found -> ("IDENT", id)), (bp, ep) | [< ' ('0'..'9' as c); len = number (store 0 c) >] ep -> (("INT", get_buff len), (bp, ep)) @@ -257,7 +299,14 @@ let rec next_token = parser bp (("STRING", get_buff len), (bp, ep)) | [< ' ('(' as c); t = parser - | [< ''*'; _ = comment bp; s >] -> next_token s + | [< ''*'; c; s >] -> (match !current with + | InVernac -> current := InVernacEsc "(*" + | _ -> current := InComment "(*"); + comment bp c; + (match !current with + | InVernacEsc _ -> add_comment_pp (fnl ()); current := InVernac + | _ -> ()); + next_token s | [< t = process_chars bp c >] -> t >] -> t | [< 'c; t = process_chars bp c >] -> t | [< _ = Stream.empty >] -> (("EOI", ""), (bp, bp + 1)) diff --git a/parsing/lexer.mli b/parsing/lexer.mli index 9b0e3bbd8..b722e8b0c 100644 --- a/parsing/lexer.mli +++ b/parsing/lexer.mli @@ -8,6 +8,8 @@ (*i $Id$ i*) +open Pp + type error = | Illegal_character | Unterminated_comment @@ -32,3 +34,5 @@ type frozen_t val freeze : unit -> frozen_t val unfreeze : frozen_t -> unit val init : unit -> unit + +val comments : (std_ppcmds list option) ref diff --git a/scripts/coqc.ml b/scripts/coqc.ml index 4234216fa..641a3cf6d 100644 --- a/scripts/coqc.ml +++ b/scripts/coqc.ml @@ -108,6 +108,8 @@ let parse_args () = keep := true ; parse (cfiles,args) rem | ("-verbose" | "--verbose") :: rem -> verbose := true ; parse (cfiles,args) rem + | "-translate" :: rem -> + parse (cfiles,"-ftranslate"::args) rem | "-boot" :: rem -> bindir:= Filename.concat Coq_config.coqtop "bin"; parse (cfiles, "-boot"::args) rem diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index c136507fb..267174ad2 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -164,6 +164,9 @@ let parse_args () = | "-compile-verbose" :: f :: rem -> add_compile true f; parse rem | "-compile-verbose" :: [] -> usage () + | "-translate" :: rem -> make_translate true; parse rem + | "-ftranslate" :: rem -> make_translate true; translate_file := true; parse rem + | "-unsafe" :: f :: rem -> add_unsafe f; parse rem | "-unsafe" :: [] -> usage () diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index 2f6d5c934..a0b4271f6 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -11,12 +11,14 @@ (* Parsing of vernacular. *) open Pp +open Lexer open Util open Options open System open Coqast open Vernacexpr open Vernacinterp +open Ppvernacnew (* The functions in this module may raise (unexplainable!) exceptions. Use the module Coqtoplevel, which catches these exceptions @@ -97,6 +99,10 @@ let parse_phrase (po, verbch) = let just_parsing = ref false +let pr_comments = function + | None -> mt() + | Some l -> h 0 (List.fold_left (++) (mt ()) (List.rev l)) + let rec vernac interpfun input = let (loc,com) = parse_phrase input in let rec interp = function @@ -122,7 +128,13 @@ let rec vernac interpfun input = in try - interp com + if do_translate () then + let _ = interp com in + if !translate_file then + msgnl (pr_comments !comments ++ pr_vernac com ++ sep_end) + else + msgnl (hov 4 (str"New Syntax:" ++ fnl() ++ pr_comments !comments ++ pr_vernac com ++ sep_end)); comments := None + else interp com with e -> raise (DuringCommandInterp (loc, e)) @@ -178,7 +190,10 @@ let compile verbosely f = *) let ldir,long_f_dot_v = Library.start_library f in if !dump then dump_string ("F" ^ Names.string_of_dirpath ldir ^ "\n"); + let chano = if Options.do_translate () then open_out (f^".v8") else stdout in + let _ = Format.set_formatter_out_channel chano in let _ = load_vernac verbosely long_f_dot_v in + let _ = close_out chano in if Pfedit.get_all_proof_names () <> [] then (message "Error: There are pending proofs"; exit 1); Library.save_library_to ldir (long_f_dot_v ^ "o") diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 0645a87f0..6a282d547 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -1131,7 +1131,7 @@ let interp c = match c with | VernacNotation (inf,c,pl,sc) -> vernac_notation inf c pl sc (* Gallina *) - | VernacDefinition (k,id,d,f) -> vernac_definition k id d f + | VernacDefinition (k,id,d,f,_) -> vernac_definition k id d f | VernacStartTheoremProof (k,id,t,top,f) -> vernac_start_proof k (Some id) t top f | VernacEndProof (opaq,idopt) -> vernac_end_proof opaq idopt diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml index 59e089251..53434bb8e 100644 --- a/toplevel/vernacexpr.ml +++ b/toplevel/vernacexpr.ml @@ -170,7 +170,7 @@ type vernac_expr = (* Gallina *) | VernacDefinition of definition_kind * identifier * definition_expr * - declaration_hook + declaration_hook * definitionkind | VernacStartTheoremProof of theorem_kind * identifier * (local_binder list * constr_expr) * bool * declaration_hook | VernacEndProof of opacity_flag * (identifier * theorem_kind option) option diff --git a/translate/ppconstrnew.ml b/translate/ppconstrnew.ml new file mode 100644 index 000000000..7d6899f77 --- /dev/null +++ b/translate/ppconstrnew.ml @@ -0,0 +1,370 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) + +(* $Id$ *) + +open Ast +open Util +open Pp +open Nametab +open Names +open Nameops +open Libnames +open Coqast +open Ppextend +open Topconstr +open Term + +let sep = fun _ -> spc() +let sep_p = fun _ -> str"." +let sep_v = fun _ -> str"," +let sep_pp = fun _ -> str":" +let sep_pv = fun _ -> str"; " + +let dfltpr ast = (str"#GENTERM " ++ print_ast ast);; + +let pr_global ref = pr_global_env None ref + +let global_const_name kn = + try pr_global (ConstRef kn) + with Not_found -> (str ("CONST("^(string_of_kn kn)^")")) + +let global_var_name id = + try pr_global (VarRef id) + with Not_found -> (str ("SECVAR("^(string_of_id id)^")")) + +let global_ind_name (kn,tyi) = + try pr_global (IndRef (kn,tyi)) + with Not_found -> (str ("IND("^(string_of_kn kn)^","^(string_of_int tyi)^")")) + +let global_constr_name ((kn,tyi),i) = + try pr_global (ConstructRef ((kn,tyi),i)) + with Not_found -> (str ("CONSTRUCT("^(string_of_kn kn)^","^(string_of_int tyi)^","^(string_of_int i)^")")) + +let globpr gt = match gt with + | Nvar(_,s) -> (pr_id s) + | Node(_,"EVAR", [Num (_,ev)]) -> (str ("?" ^ (string_of_int ev))) + | Node(_,"CONST",[Path(_,sl)]) -> + global_const_name (section_path sl) + | Node(_,"SECVAR",[Nvar(_,s)]) -> + global_var_name s + | Node(_,"MUTIND",[Path(_,sl); Num(_,tyi)]) -> + global_ind_name (section_path sl, tyi) + | Node(_,"MUTCONSTRUCT",[Path(_,sl); Num(_,tyi); Num(_,i)]) -> + global_constr_name ((section_path sl, tyi), i) + | Dynamic(_,d) -> + if (Dyn.tag d) = "constr" then (str"<dynamic [constr]>") + else dfltpr gt + | gt -> dfltpr gt + +let wrap_exception = function + Anomaly (s1,s2) -> + warning ("Anomaly ("^s1^")"); pp s2; + str"<PP error: non-printable term>" + | Failure _ | UserError _ | Not_found -> + str"<PP error: non-printable term>" + | s -> raise s + +let latom = 0 +let lannot = 100 +let lprod = 200 +let llambda = 200 +let lif = 200 +let lletin = 200 +let lcases = 0 +let larrow = 90 +let lcast = 0 +let lapp = 10 +let ltop = (200,E) + +let prec_less child (parent,assoc) = + match assoc with + | E -> (<=) child parent + | L -> (<) child parent + | Any | Prec _ -> false + +let env_assoc_value v env = + try List.assoc v env + with Not_found -> + anomaly ("Printing metavariable "^(string_of_id v)^" is unbound") + +open Symbols + +let rec print_hunk pr env = function + | UnpMetaVar (e,prec) -> str "TODO" (* pr prec (env_assoc_value e env) *) + | UnpTerminal s -> str s + | UnpBox (b,sub) -> ppcmd_of_box b (prlist (print_hunk pr env) sub) + | UnpCut cut -> ppcmd_of_cut cut + +let pr_notation pr s env = + let unpl, level = find_notation_printing_rule s in + prlist (print_hunk pr env) unpl, level + +let pr_delimiters key strm = + let left = "`"^key^":" and right = "`" in + let lspace = + if is_letter (left.[String.length left -1]) then str " " else mt () in + let rspace = + let c = right.[0] in + if is_letter c or is_digit c or c = '\'' then str " " else mt () in + str left ++ lspace ++ strm ++ rspace ++ str right + +open Rawterm + +let pr_opt pr = function + | None -> mt () + | Some x -> spc () ++ pr x + +let pr_universe u = str "<univ>" + +let pr_sort = function + | RProp Term.Null -> str "Prop" + | RProp Term.Pos -> str "Set" + | RType u -> str "Type" ++ pr_opt pr_universe u + +let pr_explicitation = function + | None -> mt () + | Some n -> int n ++ str "!" + +let pr_expl_args pr (a,expl) = + pr_explicitation expl ++ pr (lapp,L) a + +let pr_opt_type pr = function + | CHole _ -> mt () + | t -> cut () ++ str ":" ++ pr ltop t + +let pr_tight_coma () = str "," ++ cut () + +let pr_name = function + | Anonymous -> str"_" + | Name id -> pr_id id + +let pr_located pr (loc,x) = pr x + +let pr_let_binder pr x a = + hov 0 ( + str "let" ++ spc () ++ + pr_name x ++ spc () ++ + str "=" ++ spc () ++ + pr ltop a ++ spc () ++ + str "in") + +let pr_binder pr (nal,t) = + h 0 ( + prlist_with_sep sep (pr_located pr_name) nal ++ + pr_opt_type pr t) + +let pr_binders pr bl = + h 0 (prlist_with_sep sep (pr_binder pr) bl) + +let pr_recursive_decl pr id b t c = + pr_id id ++ + brk (1,2) ++ str ": " ++ pr ltop t ++ str ":=" ++ + brk (1,2) ++ pr ltop c + +let split_lambda = function + | CLambdaN (loc,[[na],t],c) -> (na,t,c) + | CLambdaN (loc,([na],t)::bl,c) -> (na,t,CLambdaN(loc,bl,c)) + | CLambdaN (loc,(na::nal,t)::bl,c) -> (na,t,CLambdaN(loc,(nal,t)::bl,c)) + | _ -> anomaly "ill-formed fixpoint body" + +let split_product = function + | CArrow (loc,t,c) -> ((loc,Anonymous),t,c) + | CProdN (loc,[[na],t],c) -> (na,t,c) + | CProdN (loc,([na],t)::bl,c) -> (na,t,CProdN(loc,bl,c)) + | CProdN (loc,(na::nal,t)::bl,c) -> (na,t,CProdN(loc,(nal,t)::bl,c)) + | _ -> anomaly "ill-formed fixpoint body" + +let rec split_fix n typ def = + if n = 0 then ([],typ,def) + else + let (na,_,def) = split_lambda def in + let (_,t,typ) = split_product typ in + let (bl,typ,def) = split_fix (n-1) typ def in + (([na],t)::bl,typ,def) + +let pr_fixdecl pr (id,n,t,c) = + let (bl,t,c) = split_fix (n+1) t c in + pr_recursive_decl pr id + (brk (1,2) ++ str "[" ++ pr_binders pr bl ++ str "]") t c + +let pr_cofixdecl pr (id,t,c) = + pr_recursive_decl pr id (mt ()) t c + +let pr_recursive s pr_decl id = function + | [] -> anomaly "(co)fixpoint with no definition" + | d1::dl -> + hov 0 ( + str "Fix " ++ pr_id id ++ brk (0,2) ++ str "{" ++ + (v 0 ( + (hov 0 (pr_decl d1)) ++ + (prlist (fun fix -> fnl () ++ hov 0 (str "with" ++ pr_decl fix)) + dl))) ++ + str "}") + +let pr_fix pr = pr_recursive "Fix" (pr_fixdecl pr) +let pr_cofix pr = pr_recursive "Fix" (pr_cofixdecl pr) + +let rec pr_arrow pr = function + | CArrow (_,a,b) -> pr (larrow,L) a ++ str "->" ++ pr_arrow pr b + | a -> pr (larrow,E) a + +let pr_annotation pr t = str "<" ++ pr ltop t ++ str ">" + +let pr_cases _ _ _ = str "<CASES(TODO)>" + +let rec pr inherited a = + let (strm,prec) = match a with + | CRef r -> pr_reference r, latom + | CFix (_,id,fix) -> pr_fix pr (snd id) fix, latom + | CCoFix (_,id,cofix) -> pr_cofix pr (snd id) cofix, latom + | CArrow _ -> h 0 (pr_arrow pr a), larrow + | CProdN (_,bl,a) -> + h 0 ( + str "!" ++ pr_binders pr bl ++ str "." ++ spc () ++ pr ltop a), lprod + | CLambdaN (_,bl,a) -> + hov 0 ( + str "fun" ++ spc () ++ pr_binders pr bl ++ spc () ++ str "=>" ++ spc () ++ pr ltop a), + llambda + | CLetIn (_,x,a,b) -> + h 0 (pr_let_binder pr (snd x) a ++ spc () ++ pr ltop b), lletin + | CAppExpl (_,f,l) -> + h 0 ( + str "@" ++ pr_reference f ++ + prlist (fun a -> spc () ++ pr (lapp,L) a) l), lapp + | CApp (_,a,l) -> + h 0 ( + pr (lapp,E) a ++ + prlist (fun a -> spc () ++ pr_expl_args pr a) l), lapp + | CCases (_,po,c,eqns) -> + pr_cases po c eqns, lcases + | COrderedCase (_,IfStyle,po,c,[b1;b2]) -> + (* On force les parenthèses autour d'un "if" sous-terme (même si le + parsing est lui plus tolérant) *) + hov 0 ( + pr_opt (pr_annotation pr) po ++ + hv 0 ( + str "if" ++ pr ltop c ++ spc () ++ + hov 0 (str "then" ++ brk (1,1) ++ pr ltop b1) ++ spc () ++ + hov 0 (str "else" ++ brk (1,1) ++ pr ltop b2))), lif + | COrderedCase (_,LetStyle,po,c,[CLambdaN(_,[_,_ as bd],b)]) -> + hov 0 ( + pr_opt (pr_annotation pr) po ++ + hv 0 ( + str "let" ++ brk (1,1) ++ + hov 0 (str "(" ++ pr_binder pr bd ++ str ")") ++ + str "=" ++ brk (1,1) ++ + pr ltop c ++ spc () ++ + str "in " ++ pr ltop b)), lletin + | COrderedCase (_,(MatchStyle|RegularStyle as style),po,c,bl) -> + hov 0 ( + hov 0 ( + pr_opt (pr_annotation pr) po ++ brk (0,2) ++ + hov 0 ( + str (if style=RegularStyle then "Case" else "match") ++ + brk (1,1) ++ pr ltop c ++ spc () ++ + str (if style=RegularStyle then "of" else "with") ++ + brk (1,3) ++ + hov 0 (prlist (fun b -> pr ltop b ++ fnl ()) bl)) ++ + str "end")), lcases + | COrderedCase (_,_,_,_,_) -> + anomaly "malformed if or destructuring let" + | CHole _ -> str "_", latom + | CMeta (_,p) -> str "@" ++ int p, latom + | CSort (_,s) -> pr_sort s, latom + | CCast (_,a,b) -> + hv 0 (pr (lcast,L) a ++ cut () ++ str "::" ++ pr (lcast,E) b), lcast + | CNotation (_,s,env) -> pr_notation pr s env + | CNumeral (_,p) -> Bignat.pr_bigint p, latom + | CDelimiters (_,sc,a) -> pr_delimiters sc (pr ltop a), latom + | CDynamic _ -> str "<dynamic>", latom + in + if prec_less prec inherited then strm + else str"(" ++ strm ++ str")" + +let pr_constr = pr ltop + +let pr_pattern = pr_constr +let pr_occurrences prc (nl,c) = prlist (fun n -> int n ++ spc ()) nl ++ prc c + +let pr_qualid qid = str (string_of_qualid qid) + +open Rawterm + +let pr_arg pr x = spc () ++ pr x + +let pr_red_flag pr r = + (if r.rBeta then pr_arg str "Beta" else mt ()) ++ + (if r.rIota then pr_arg str "Iota" else mt ()) ++ + (if r.rZeta then pr_arg str "Zeta" else mt ()) ++ + (if r.rConst = [] then + if r.rDelta then pr_arg str "Delta" + else mt () + else + pr_arg str "Delta" ++ (if r.rDelta then str "-" else mt ()) ++ + hov 0 (str "[" ++ prlist_with_sep spc pr r.rConst ++ str "]")) + +open Genarg + +let pr_metanum pr = function + | AN x -> pr x + | MetaNum (_,n) -> str "?" ++ int n + +let pr_metaid id = str"?" ++ pr_id id + +let pr_red_expr (pr_constr,pr_ref) = function + | Red false -> str "Red" + | Hnf -> str "Hnf" + | Simpl o -> str "Simpl" ++ pr_opt (pr_occurrences pr_constr) o + | Cbv f -> + if f = {rBeta=true;rIota=true;rZeta=true;rDelta=true;rConst=[]} then + str "Compute" + else + hov 1 (str "Cbv" ++ spc () ++ pr_red_flag pr_ref f) + | Lazy f -> + hov 1 (str "Lazy" ++ spc () ++ pr_red_flag pr_ref f) + | Unfold l -> + hov 1 (str "Unfold" ++ + prlist (fun (nl,qid) -> + prlist (pr_arg int) nl ++ spc () ++ pr_ref qid) l) + | Fold l -> hov 1 (str "Fold" ++ prlist (pr_arg pr_constr) l) + | Pattern l -> + hov 1 (str "Pattern" ++ prlist (pr_occurrences pr_constr) l) + + | Red true -> error "Shouldn't be accessible from user" + | ExtraRedExpr (s,c) -> + hov 1 (str s ++ pr_arg pr_constr c) + +let rec pr_may_eval pr = function + | ConstrEval (r,c) -> + hov 0 + (str "Eval" ++ brk (1,1) ++ pr_red_expr (pr,pr_metanum pr_reference) r ++ + spc () ++ str "in" ++ brk (1,1) ++ pr c) + | ConstrContext ((_,id),c) -> + hov 0 + (str "Inst " ++ brk (1,1) ++ pr_id id ++ spc () ++ + str "[" ++ pr c ++ str "]") + | ConstrTypeOf c -> hov 0 (str "Check " ++ brk (1,1) ++ pr c) + | ConstrTerm c -> pr c + +(**********************************************************************) +let constr_syntax_universe = "constr" +(* This is starting precedence for printing constructions or tactics *) +(* Level 9 means no parentheses except for applicative terms (at level 10) *) +let constr_initial_prec = Some (9,Ppextend.L) + +let gentermpr_fail gt = + Esyntax.genprint globpr constr_syntax_universe constr_initial_prec gt + +let gentermpr gt = + try gentermpr_fail gt + with s -> wrap_exception s + +(* [at_top] means ids of env must be avoided in bound variables *) +let gentermpr_core at_top env t = + gentermpr (Termast.ast_of_constr at_top env t) diff --git a/translate/ppconstrnew.mli b/translate/ppconstrnew.mli new file mode 100644 index 000000000..1488a9d17 --- /dev/null +++ b/translate/ppconstrnew.mli @@ -0,0 +1,41 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) + +(* $Id$ *) + +open Pp +open Environ +open Term +open Libnames +open Pcoq +open Rawterm +open Extend +open Coqast +open Topconstr +open Names +open Util + +val split_fix : int -> constr_expr -> constr_expr -> + (name located list * constr_expr) list * constr_expr * constr_expr + +val pr_global : global_reference -> std_ppcmds + +val gentermpr : Coqast.t -> std_ppcmds +val gentermpr_core : bool -> env -> constr -> std_ppcmds + +val pr_opt : ('a -> std_ppcmds) -> 'a option -> std_ppcmds +val pr_name : name -> std_ppcmds +val pr_qualid : qualid -> std_ppcmds +val pr_red_expr : + ('a -> std_ppcmds) * ('b -> std_ppcmds) -> + ('a,'b) red_expr_gen -> std_ppcmds + +val pr_sort : rawsort -> std_ppcmds +val pr_pattern : Tacexpr.pattern_expr -> std_ppcmds +val pr_constr : constr_expr -> std_ppcmds +val pr_may_eval : ('a -> std_ppcmds) -> 'a may_eval -> std_ppcmds diff --git a/translate/pptacticnew.ml b/translate/pptacticnew.ml new file mode 100644 index 000000000..1cab30aa0 --- /dev/null +++ b/translate/pptacticnew.ml @@ -0,0 +1,595 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) + +(* $Id$ *) + +open Pp +open Names +open Nameops +open Util +open Extend +open Ppconstr +open Tacexpr +open Rawterm +open Topconstr +open Genarg +open Libnames + +(* Extensions *) +let prtac_tab = Hashtbl.create 17 + +let declare_extra_tactic_pprule s f g = + Hashtbl.add prtac_tab s (f,g) + +let genarg_pprule = ref Stringmap.empty + +let declare_extra_genarg_pprule (rawwit, f) (wit, g) = + let s = match unquote wit with + | ExtraArgType s -> s + | _ -> error + "Can declare a pretty-printing rule only for extra argument types" + in + let f x = f (out_gen rawwit x) in + let g x = g (out_gen wit x) in + genarg_pprule := Stringmap.add s (f,g) !genarg_pprule + +(* [pr_rawtac] is here to cheat with ML typing system, + gen_tactic_expr is polymorphic but with some occurrences of its + instance raw_tactic_expr in it; then pr_tactic should be + polymorphic but with some calls to instance of itself, what ML does + not accept; pr_rawtac0 denotes this instance of pr_tactic on + raw_tactic_expr *) + +let pr_rawtac = + ref (fun _ -> failwith "Printer for raw tactic expr is not defined" + : raw_tactic_expr -> std_ppcmds) +let pr_rawtac0 = + ref (fun _ -> failwith "Printer for raw tactic expr is not defined" + : raw_tactic_expr -> std_ppcmds) + +let pr_arg pr x = spc () ++ pr x + +let pr_metanum pr = function + | AN x -> pr x + | MetaNum (_,n) -> str "?" ++ int n + +let pr_or_var pr = function + | ArgArg x -> pr x + | ArgVar (_,s) -> pr_id s + +let pr_or_meta pr = function + | AI x -> pr x + | _ -> failwith "pr_hyp_location: unexpected quotation meta-variable" + +let pr_casted_open_constr = pr_constr + +let pr_quantified_hypothesis = function + | AnonHyp n -> int n + | NamedHyp id -> pr_id id + +let pr_quantified_hypothesis_arg h = spc () ++ pr_quantified_hypothesis h + +let pr_binding prc = function + | NamedHyp id, c -> hov 1 (pr_id id ++ str ":=" ++ cut () ++ prc c) + | AnonHyp n, c -> hov 1 (int n ++ str ":=" ++ cut () ++ prc c) + +let pr_bindings prc = function + | ImplicitBindings l -> + brk (1,1) ++ str "with" ++ brk (1,1) ++ + prlist_with_sep spc prc l + | ExplicitBindings l -> + str"TODO" (* brk (1,1) ++ str "with" ++ brk (1,1) ++ + prlist_with_sep spc (pr_binding prc) l *) + | NoBindings -> mt () + +let pr_with_bindings prc (c,bl) = prc c ++ hv 0 (pr_bindings prc bl) + +let pr_with_names = function + | [] -> mt () + | ids -> spc () ++ str "as [" ++ + hv 0 (prlist_with_sep (fun () -> spc () ++ str "| ") + (prlist_with_sep spc pr_id) ids ++ str "]") + +let rec pr_intro_pattern = function + | IntroOrAndPattern pll -> + str "[" ++ + hv 0 (prlist_with_sep pr_bar (prlist_with_sep spc pr_intro_pattern) pll) + ++ str "]" + + | IntroWildcard -> str "_" + | IntroIdentifier id -> pr_id id + +let pr_hyp_location pr_id = function + | InHyp id -> spc () ++ pr_id id + | InHypType id -> spc () ++ str "(Type of " ++ pr_id id ++ str ")" + +let pr_clause pr_id = function + | [] -> mt () + | l -> spc () ++ hov 0 (str "in" ++ prlist (pr_hyp_location pr_id) l) + +let pr_clause_pattern pr_id = function (* To check *) + | (None, []) -> mt () + | (glopt,l) -> + str "in" ++ + prlist + (fun (id,nl) -> spc () ++ prlist_with_sep spc int nl + ++ spc () ++ pr_id id) l ++ + pr_opt (prlist_with_sep spc int) glopt + +let pr_induction_arg prc = function + | ElimOnConstr c -> prc c + | ElimOnIdent (_,id) -> pr_id id + | ElimOnAnonHyp n -> int n + +let pr_match_pattern = function + | Term a -> pr_pattern a + | Subterm (None,a) -> str "[" ++ pr_pattern a ++ str "]" + | Subterm (Some id,a) -> pr_id id ++ str "[" ++ pr_pattern a ++ str "]" + +let pr_match_hyps = function + | NoHypId mp -> str "_:" ++ pr_match_pattern mp + | Hyp ((_,id),mp) -> pr_id id ++ str ":" ++ pr_match_pattern mp + +let pr_match_rule m pr = function + | Pat ([],mp,t) when m -> + str "[" ++ pr_match_pattern mp ++ str "]" + ++ spc () ++ str "->" ++ brk (1,2) ++ pr t + | Pat (rl,mp,t) -> + str "[" ++ prlist_with_sep pr_semicolon pr_match_hyps rl ++ spc () ++ + str "|-" ++ spc () ++ pr_match_pattern mp ++ spc () ++ str "]" ++ + spc () ++ str "->" ++ brk (1,2) ++ pr t + | All t -> str "_" ++ spc () ++ str "->" ++ brk (1,2) ++ pr t + +let pr_funvar = function + | None -> spc () ++ str "()" + | Some id -> spc () ++ pr_id id + +let pr_let_clause k pr = function + | ((_,id),None,t) -> hv 0(str k ++ pr_id id ++ str " =" ++ brk (1,1) ++ pr t) + | ((_,id),Some c,t) -> str "TODO(LETCLAUSE)" + +let pr_let_clauses pr = function + | hd::tl -> + hv 0 + (pr_let_clause "let " pr hd ++ spc () ++ + prlist_with_sep spc (pr_let_clause "and " pr) tl) + | [] -> anomaly "LetIn must declare at least one binding" + +let pr_rec_clause pr ((_,id),(l,t)) = + pr_id id ++ prlist pr_funvar l ++ str "->" ++ spc () ++ pr t + +let pr_rec_clauses pr l = + prlist_with_sep (fun () -> fnl () ++ str "and ") (pr_rec_clause pr) l + +let pr_hintbases = function + | None -> spc () ++ str "with *" + | Some [] -> mt () + | Some l -> + spc () ++ str "with" ++ hv 0 (prlist (fun s -> spc () ++ str s) l) + +let pr_autoarg_adding = function + | [] -> mt () + | l -> + spc () ++ str "Adding [" ++ + hv 0 (prlist_with_sep spc pr_reference l) ++ str "]" + +let pr_autoarg_destructing = function + | true -> spc () ++ str "Destructing" + | false -> mt () + +let pr_autoarg_usingTDB = function + | true -> spc () ++ str "Using TDB" + | false -> mt () + +let rec pr_rawgen prtac x = + match Genarg.genarg_tag x with + | BoolArgType -> pr_arg str (if out_gen rawwit_bool x then "true" else "false") + | IntArgType -> pr_arg int (out_gen rawwit_int x) + | IntOrVarArgType -> pr_arg (pr_or_var pr_int) (out_gen rawwit_int_or_var x) + | StringArgType -> spc () ++ str "\"" ++ str (out_gen rawwit_string x) ++ str "\"" + | PreIdentArgType -> pr_arg str (out_gen rawwit_pre_ident x) + | IdentArgType -> pr_arg pr_id (out_gen rawwit_ident x) + | RefArgType -> pr_arg pr_reference (out_gen rawwit_ref x) + | SortArgType -> pr_arg pr_sort (out_gen rawwit_sort x) + | ConstrArgType -> pr_arg pr_constr (out_gen rawwit_constr x) + | ConstrMayEvalArgType -> + pr_arg (pr_may_eval pr_constr) (out_gen rawwit_constr_may_eval x) + | QuantHypArgType -> + pr_arg pr_quantified_hypothesis (out_gen rawwit_quant_hyp x) + | RedExprArgType -> + pr_arg (pr_red_expr (pr_constr,pr_metanum pr_reference)) (out_gen rawwit_red_expr x) + | TacticArgType -> pr_arg prtac (out_gen rawwit_tactic x) + | CastedOpenConstrArgType -> + pr_arg pr_casted_open_constr (out_gen rawwit_casted_open_constr x) + | ConstrWithBindingsArgType -> + pr_arg (pr_with_bindings pr_constr) + (out_gen rawwit_constr_with_bindings x) + | List0ArgType _ -> + hov 0 (fold_list0 (fun x a -> pr_rawgen prtac x ++ a) x (mt())) + | List1ArgType _ -> + hov 0 (fold_list1 (fun x a -> pr_rawgen prtac x ++ a) x (mt())) + | OptArgType _ -> hov 0 (fold_opt (pr_rawgen prtac) (mt()) x) + | PairArgType _ -> + hov 0 + (fold_pair + (fun a b -> pr_rawgen prtac a ++ spc () ++ pr_rawgen prtac b) + x) + | ExtraArgType s -> + try fst (Stringmap.find s !genarg_pprule) x + with Not_found -> str " [no printer for " ++ str s ++ str "] " + +let rec pr_raw_tacarg_using_rule pr_gen = function + | Egrammar.TacTerm s :: l, al -> spc () ++ str s ++ pr_raw_tacarg_using_rule pr_gen (l,al) + | Egrammar.TacNonTerm _ :: l, a :: al -> pr_gen a ++ pr_raw_tacarg_using_rule pr_gen (l,al) + | [], [] -> mt () + | _ -> failwith "Inconsistent arguments of extended tactic" + +let pr_raw_extend prt s l = + try + let (s,pl) = fst (Hashtbl.find prtac_tab s) l in + str s ++ pr_raw_tacarg_using_rule (pr_rawgen prt) (pl,l) + with Not_found -> + str "TODO(" ++ str s ++ prlist (pr_rawgen prt) l ++ str ")" + +open Closure + +let pr_evaluable_reference = function + | EvalVarRef id -> pr_id id + | EvalConstRef sp -> pr_global (Libnames.ConstRef sp) + +let pr_inductive ind = pr_global (Libnames.IndRef ind) + +let rec pr_generic prtac x = + match Genarg.genarg_tag x with + | BoolArgType -> pr_arg str (if out_gen wit_bool x then "true" else "false") + | IntArgType -> pr_arg int (out_gen wit_int x) + | IntOrVarArgType -> pr_arg (pr_or_var pr_int) (out_gen wit_int_or_var x) + | StringArgType -> spc () ++ str "\"" ++ str (out_gen wit_string x) ++ str "\"" + | PreIdentArgType -> pr_arg str (out_gen wit_pre_ident x) + | IdentArgType -> pr_arg pr_id (out_gen wit_ident x) + | RefArgType -> pr_arg pr_global (out_gen wit_ref x) + | SortArgType -> pr_arg Printer.prterm (Term.mkSort (out_gen wit_sort x)) + | ConstrArgType -> pr_arg Printer.prterm (out_gen wit_constr x) + | ConstrMayEvalArgType -> + pr_arg Printer.prterm (out_gen wit_constr_may_eval x) + | QuantHypArgType -> + pr_arg pr_quantified_hypothesis (out_gen wit_quant_hyp x) + | RedExprArgType -> + pr_arg (pr_red_expr (Printer.prterm,pr_evaluable_reference)) (out_gen wit_red_expr x) + | TacticArgType -> pr_arg prtac (out_gen wit_tactic x) + | CastedOpenConstrArgType -> + pr_arg Printer.prterm (snd (out_gen wit_casted_open_constr x)) + | ConstrWithBindingsArgType -> + pr_arg (pr_with_bindings Printer.prterm) + (out_gen wit_constr_with_bindings x) + | List0ArgType _ -> + hov 0 (fold_list0 (fun x a -> pr_generic prtac x ++ a) x (mt())) + | List1ArgType _ -> + hov 0 (fold_list1 (fun x a -> pr_generic prtac x ++ a) x (mt())) + | OptArgType _ -> hov 0 (fold_opt (pr_generic prtac) (mt()) x) + | PairArgType _ -> + hov 0 + (fold_pair + (fun a b -> pr_generic prtac a ++ spc () ++ pr_generic prtac b) + x) + | ExtraArgType s -> + try snd (Stringmap.find s !genarg_pprule) x + with Not_found -> str "[no printer for " ++ str s ++ str "]" + +let rec pr_tacarg_using_rule prt = function + | Egrammar.TacTerm s :: l, al -> spc () ++ str s ++ pr_tacarg_using_rule prt (l,al) + | Egrammar.TacNonTerm _ :: l, a :: al -> pr_generic prt a ++ pr_tacarg_using_rule prt (l,al) + | [], [] -> mt () + | _ -> failwith "Inconsistent arguments of extended tactic" + +let pr_extend prt s l = + try + let (s,pl) = snd (Hashtbl.find prtac_tab s) l in + str s ++ pr_tacarg_using_rule prt (pl,l) + with Not_found -> + str s ++ prlist (pr_generic prt) l + +let make_pr_tac (pr_constr,pr_cst,pr_ind,pr_ident,pr_extend) = + +let pr_bindings = pr_bindings pr_constr in +let pr_with_bindings = pr_with_bindings pr_constr in +let pr_eliminator cb = str "using" ++ pr_arg pr_with_bindings cb in +let pr_constrarg c = spc () ++ pr_constr c in +let pr_intarg n = spc () ++ int n in + + (* Printing tactics as arguments *) +let rec pr_atom0 = function + | TacIntroPattern [] -> str "Intros" + | TacIntroMove (None,None) -> str "Intro" + | TacAssumption -> str "Assumption" + | TacAnyConstructor None -> str "Constructor" + | TacTrivial (Some []) -> str "Trivial" + | TacAuto (None,Some []) -> str "Auto" + | TacAutoTDB None -> str "AutoTDB" + | TacDestructConcl -> str "DConcl" + | TacReflexivity -> str "Reflexivity" + | TacSymmetry -> str "Symmetry" + | t -> str "(" ++ pr_atom1 t ++ str ")" + + (* Main tactic printer *) +and pr_atom1 = function + | TacExtend (_,s,l) -> pr_extend !pr_rawtac s l + | TacAlias (s,l,_) -> pr_extend !pr_rawtac s (List.map snd l) + + (* Basic tactics *) + | TacIntroPattern [] as t -> pr_atom0 t + | TacIntroPattern (_::_ as p) -> + hov 1 (str "Intros" ++ spc () ++ prlist_with_sep spc pr_intro_pattern p) + | TacIntrosUntil h -> + hv 1 (str "Intros until" ++ pr_arg pr_quantified_hypothesis h) + | TacIntroMove (None,None) as t -> pr_atom0 t + | TacIntroMove (Some id1,None) -> str "Intro " ++ pr_id id1 + | TacIntroMove (ido1,Some (_,id2)) -> + hov 1 + (str "Intro" ++ pr_opt pr_id ido1 ++ spc () ++ str "after " ++ pr_id id2) + | TacAssumption as t -> pr_atom0 t + | TacExact c -> hov 1 (str "Exact" ++ pr_arg pr_constr c) + | TacApply cb -> hov 1 (str "Apply" ++ spc () ++ pr_with_bindings cb) + | TacElim (cb,cbo) -> + hov 1 (str "Elim" ++ pr_arg pr_with_bindings cb ++ + pr_opt pr_eliminator cbo) + | TacElimType c -> hov 1 (str "ElimType" ++ pr_arg pr_constr c) + | TacCase cb -> hov 1 (str "Case" ++ spc () ++ pr_with_bindings cb) + | TacCaseType c -> hov 1 (str "CaseType" ++ pr_arg pr_constr c) + | TacFix (ido,n) -> hov 1 (str "Fix" ++ pr_opt pr_id ido ++ pr_intarg n) + | TacMutualFix (id,n,l) -> + hov 1 (str "Cofix" ++ spc () ++ pr_id id ++ pr_intarg n ++ spc () ++ + hov 0 (str "with" ++ brk (1,1) ++ + prlist_with_sep spc + (fun (id,n,c) -> + spc () ++ pr_id id ++ pr_intarg n ++ pr_arg pr_constr c) + l)) + | TacCofix ido -> hov 1 (str "Cofix" ++ pr_opt pr_id ido) + | TacMutualCofix (id,l) -> + hov 1 (str "Cofix" ++ spc () ++ pr_id id ++ spc () ++ + hov 0 (str "with" ++ brk (1,1) ++ + prlist (fun (id,c) -> spc () ++ pr_id id ++ pr_arg pr_constr c) + l)) + | TacCut c -> hov 1 (str "Cut" ++ pr_arg pr_constr c) + | TacTrueCut (None,c) -> + hov 1 (str "Assert" ++ pr_arg pr_constr c) + | TacTrueCut (Some id,c) -> + hov 1 (str "Assert" ++ spc () ++ pr_id id ++ str ":" ++ pr_constr c) + | TacForward (false,na,c) -> + hov 1 (str "Assert" ++ pr_arg pr_name na ++ str ":=" ++ pr_constr c) + | TacForward (true,na,c) -> + hov 1 (str "Pose" ++ pr_arg pr_name na ++ str ":=" ++ pr_constr c) + | TacGeneralize l -> + hov 1 (str "Generalize" ++ spc () ++ prlist_with_sep spc pr_constr l) + | TacGeneralizeDep c -> + hov 1 (str "Generalize" ++ spc () ++ str "Dependent" ++ spc () ++ + pr_constr c) + | TacLetTac (id,c,cl) -> + hov 1 (str "LetTac" ++ spc () ++ pr_id id ++ str ":=" ++ + pr_constr c ++ pr_clause_pattern pr_ident cl) + | TacInstantiate (n,c) -> + hov 1 (str "Instantiate" ++ pr_arg int n ++ pr_arg pr_constr c) + + (* Derived basic tactics *) + | TacOldInduction h -> + hov 1 (str "Induction" ++ pr_arg pr_quantified_hypothesis h) + | TacNewInduction (h,e,ids) -> + hov 1 (str "NewInduction" ++ spc () ++ pr_induction_arg pr_constr h ++ + pr_opt pr_eliminator e ++ pr_with_names ids) + | TacOldDestruct h -> + hov 1 (str "Destruct" ++ pr_arg pr_quantified_hypothesis h) + | TacNewDestruct (h,e,ids) -> + hov 1 (str "NewDestruct" ++ spc () ++ pr_induction_arg pr_constr h ++ + pr_opt pr_eliminator e ++ pr_with_names ids) + | TacDoubleInduction (h1,h2) -> + hov 1 + (str "Double Induction" ++ + pr_arg pr_quantified_hypothesis h1 ++ + pr_arg pr_quantified_hypothesis h2) + | TacDecomposeAnd c -> + hov 1 (str "Decompose Record" ++ pr_arg pr_constr c) + | TacDecomposeOr c -> + hov 1 (str "Decompose Sum" ++ pr_arg pr_constr c) + | TacDecompose (l,c) -> + hov 1 (str "Decompose" ++ spc () ++ + hov 0 (str "[" ++ prlist_with_sep spc (pr_metanum pr_ind) l + ++ str "]")) + | TacSpecialize (n,c) -> + hov 1 (str "Specialize" ++ pr_opt int n ++ pr_with_bindings c) + | TacLApply c -> + hov 1 (str "LApply" ++ pr_constr c) + + (* Automation tactics *) + | TacTrivial (Some []) as x -> pr_atom0 x + | TacTrivial db -> hov 0 (str "Trivial" ++ pr_hintbases db) + | TacAuto (None,Some []) as x -> pr_atom0 x + | TacAuto (n,db) -> hov 0 (str "Auto" ++ pr_opt int n ++ pr_hintbases db) + | TacAutoTDB None as x -> pr_atom0 x + | TacAutoTDB (Some n) -> hov 0 (str "AutoTDB" ++ spc () ++ int n) + | TacDestructHyp (true,(_,id)) -> hov 0 (str "CDHyp" ++ spc () ++ pr_id id) + | TacDestructHyp (false,(_,id)) -> hov 0 (str "DHyp" ++ spc () ++ pr_id id) + | TacDestructConcl as x -> pr_atom0 x + | TacSuperAuto (n,l,b1,b2) -> + hov 1 (str "SuperAuto" ++ pr_opt int n ++ pr_autoarg_adding l ++ + pr_autoarg_destructing b1 ++ pr_autoarg_usingTDB b2) + | TacDAuto (n,p) -> + hov 1 (str "Auto" ++ pr_opt int n ++ str "Decomp" ++ pr_opt int p) + + (* Context management *) + | TacClear l -> + hov 1 (str "Clear" ++ spc () ++ prlist_with_sep spc (pr_metanum pr_id) l) + | TacClearBody l -> + hov 1 (str "Clear" ++ spc () ++ prlist_with_sep spc (pr_metanum pr_id) l) + | TacMove (b,(_,id1),(_,id2)) -> + (* Rem: only b = true is available for users *) + assert b; + hov 1 + (str "Move" ++ brk (1,1) ++ pr_id id1 ++ spc () ++ + str "after" ++ brk (1,1) ++ pr_id id2) + | TacRename ((_,id1),(_,id2)) -> + hov 1 + (str "Rename" ++ brk (1,1) ++ pr_id id1 ++ spc () ++ + str "into" ++ brk (1,1) ++ pr_id id2) + + (* Constructors *) + | TacLeft l -> hov 1 (str "Left" ++ pr_bindings l) + | TacRight l -> hov 1 (str "Right" ++ pr_bindings l) + | TacSplit l -> hov 1 (str "Split" ++ pr_bindings l) + | TacAnyConstructor (Some t) -> + hov 1 (str "Constructor" ++ pr_arg !pr_rawtac0 t) + | TacAnyConstructor None as t -> pr_atom0 t + | TacConstructor (n,l) -> + hov 1 (str "Constructor" ++ pr_or_meta pr_intarg n ++ pr_bindings l) + + (* Conversion *) + | TacReduce (r,h) -> + hov 1 (pr_red_expr (pr_constr,pr_cst) r ++ pr_clause pr_ident h) + | TacChange (_,c,h) -> (* A Verifier *) + hov 1 (str "Change" ++ brk (1,1) ++ pr_constr c ++ pr_clause pr_ident h) + + (* Equivalence relations *) + | (TacReflexivity | TacSymmetry) as x -> pr_atom0 x + | TacTransitivity c -> str "Transitivity" ++ pr_arg pr_constr c + +and pr_tactic_seq_body tl = + hv 0 (str "[ " ++ + prlist_with_sep (fun () -> spc () ++ str "| ") prtac tl ++ str " ]") + + (* Strictly closed atomic tactic expressions *) +and pr0 = function + | TacFirst tl -> str "First" ++ spc () ++ pr_tactic_seq_body tl + | TacSolve tl -> str "Solve" ++ spc () ++ pr_tactic_seq_body tl + | TacId -> str "Idtac" + | TacFail 0 -> str "Fail" + | TacAtom (_,t) -> pr_atom0 t + | TacArg c -> pr_tacarg c + | t -> str "(" ++ prtac t ++ str ")" + + (* Semi-closed atomic tactic expressions *) +and pr1 = function + | TacAtom (_,t) -> pr_atom1 t + | TacFail n -> str "Fail " ++ int n + | t -> pr0 t + + (* Orelse tactic expressions (printed as if parsed associating on the right + though the semantics is purely associative) *) +and pr2 = function + | TacOrelse (t1,t2) -> + hov 1 (pr1 t1 ++ str " Orelse" ++ brk (1,1) ++ pr3 t2) + | t -> pr1 t + + (* Non closed prefix tactic expressions *) +and pr3 = function + | TacTry t -> hov 1 (str "Try" ++ spc () ++ pr3 t) + | TacDo (n,t) -> hov 1 (str "Do " ++ int n ++ spc () ++ pr3 t) + | TacRepeat t -> hov 1 (str "Repeat" ++ spc () ++ pr3 t) + | TacProgress t -> hov 1 (str "Progress" ++ spc () ++ pr3 t) + | TacInfo t -> hov 1 (str "Info" ++ spc () ++ pr3 t) + | t -> pr2 t + +and pr4 = function + | t -> pr3 t + + (* THEN and THENS tactic expressions (printed as if parsed + associating on the left though the semantics is purely associative) *) +and pr5 = function + | TacThens (t,tl) -> + hov 1 (pr5 t ++ spc () ++ str "&" ++ spc () ++ pr_tactic_seq_body tl) + | TacThen (t1,t2) -> + hov 1 (pr5 t1 ++ spc () ++ str "&" ++ spc () ++ pr4 t2) + | t -> pr4 t + + (* Ltac tactic expressions *) +and pr6 = function + |(TacAtom _ + | TacThen _ + | TacThens _ + | TacFirst _ + | TacSolve _ + | TacTry _ + | TacOrelse _ + | TacDo _ + | TacRepeat _ + | TacProgress _ + | TacId + | TacFail _ + | TacInfo _) as t -> pr5 t + + | TacAbstract (t,None) -> str "Abstract " ++ pr6 t + | TacAbstract (t,Some s) -> + hov 0 + (str "Abstract " ++ pr6 t ++ spc () ++ str "using" ++ spc () ++ pr_id s) + | TacLetRecIn (l,t) -> + hv 0 + (str "let rec " ++ pr_rec_clauses prtac l ++ + spc () ++ str "in" ++ fnl () ++ prtac t) + | TacLetIn (llc,u) -> + v 0 + (hv 0 (pr_let_clauses pr_tacarg0 llc ++ spc () ++ str "in") ++ fnl () ++ prtac u) + | TacLetCut llc -> + pr_let_clauses pr_tacarg0 + (List.map (fun (id,c,t) -> ((dummy_loc,id),Some c,t)) llc) + ++ fnl () + | TacMatch (t,lrul) -> + hov 0 (str "match" ++ spc () ++ pr_may_eval Ppconstr.pr_constr t ++ spc() + ++ str "with" + ++ prlist + (fun r -> fnl () ++ str "|" ++ spc () ++ pr_match_rule true prtac r) + lrul) + | TacMatchContext (lr,lrul) -> + hov 0 ( + str (if lr then "Match Reverse Context With" else "Match Context With") + ++ prlist + (fun r -> fnl () ++ str "|" ++ spc () ++ pr_match_rule false prtac r) + lrul) + | TacFun (lvar,body) -> + hov 0 (str "fun" ++ + prlist pr_funvar lvar ++ spc () ++ str "->" ++ spc () ++ prtac body) + | TacArg c -> pr_tacarg c + +and pr_tacarg0 = function + | TacDynamic (_,t) -> str ("<dynamic ["^(Dyn.tag t)^"]>") + | MetaNumArg (_,n) -> str ("?" ^ string_of_int n ) + | MetaIdArg (_,s) -> str ("$" ^ s) + | TacVoid -> str "()" + | Reference r -> pr_reference r + | ConstrMayEval (ConstrTerm c) -> str "'" ++ pr_constr c + | ConstrMayEval c -> pr_may_eval pr_constr c + | Integer n -> int n + | (TacCall _ | Tacexp _) as t -> str "(" ++ pr_tacarg1 t ++ str ")" + +and pr_tacarg1 = function + | TacCall (_,f,l) -> + hov 0 (pr_reference f ++ spc () ++ prlist_with_sep spc pr_tacarg0 l) + | Tacexp t -> !pr_rawtac t + | t -> pr_tacarg0 t + +and pr_tacarg x = pr_tacarg1 x + +and prtac x = pr6 x + +in (prtac,pr0,pr_match_rule) + +let (pr_raw_tactic,pr_raw_tactic0,pr_match_rule) = + make_pr_tac + (Ppconstrnew.pr_constr, + pr_metanum pr_reference, + pr_reference, + pr_or_meta (fun (loc,id) -> pr_id id), + pr_raw_extend) + +let _ = pr_rawtac := pr_raw_tactic +let _ = pr_rawtac0 := pr_raw_tactic0 + +let (pr_tactic,_,_) = + make_pr_tac + (Printer.prterm, + pr_evaluable_reference, + pr_inductive, + pr_id, + pr_extend) diff --git a/translate/pptacticnew.mli b/translate/pptacticnew.mli new file mode 100644 index 000000000..152b7e630 --- /dev/null +++ b/translate/pptacticnew.mli @@ -0,0 +1,33 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) + +(* $Id$ *) + +open Pp +open Genarg +open Tacexpr +open Proof_type + +val declare_extra_genarg_pprule : + ('a raw_abstract_argument_type * ('a -> std_ppcmds)) -> + ('b closed_abstract_argument_type * ('b -> std_ppcmds)) -> unit + +val declare_extra_tactic_pprule : + string -> + (raw_generic_argument list -> + string * Egrammar.grammar_tactic_production list) + -> (closed_generic_argument list -> + string * Egrammar.grammar_tactic_production list) + -> unit + +val pr_match_rule : bool -> (raw_tactic_expr -> std_ppcmds) -> + (pattern_expr,raw_tactic_expr) match_rule -> std_ppcmds + +val pr_raw_tactic : raw_tactic_expr -> std_ppcmds + +val pr_tactic : Proof_type.tactic_expr -> std_ppcmds diff --git a/translate/ppvernacnew.ml b/translate/ppvernacnew.ml new file mode 100644 index 000000000..2996c0aec --- /dev/null +++ b/translate/ppvernacnew.ml @@ -0,0 +1,499 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) + +(* $Id$ *) + +open Pp +open Names +open Nameops +open Nametab +open Util +open Extend +open Vernacexpr +open Ppconstrnew +open Pptacticnew +open Rawterm +open Coqast +open Genarg +open Pcoq +open Ast +open Libnames +open Ppextend +open Topconstr + +let sep = fun _ -> spc() +let sep_p = fun _ -> str"." +let sep_v = fun _ -> str"," +let sep_pp = fun _ -> str":" +let sep_pv = fun _ -> str"; " + +let pr_located pr (loc,x) = pr x + +let pr_entry_prec = function + | Some Gramext.LeftA -> spc() ++ str"LEFTA" + | Some Gramext.RightA -> spc() ++ str"RIGHTA" + | Some Gramext.NonA -> spc() ++ str"NONA" + | None -> mt() + +let pr_metaid _ = str"<TODO>" +let pr_metanum _ = str"<TODO>" + +let pr_set_entry_type = function + | ETIdent -> str"ident" + | ETReference -> str"global" + | ETPattern -> str"pattern" + | ETConstr _ | ETOther (_,_) -> mt () + | ETBigint -> str"TODO" + +let pr_non_terminal = function + | NtQual (u,nt) -> str u ++ str" : " ++ str nt + | NtShort nt -> str nt + +let pr_production_item = function + | VNonTerm (loc,nt,Some p) -> pr_non_terminal nt ++ str"(" ++ pr_metaid p ++ str")" + | VNonTerm (loc,nt,None) -> pr_non_terminal nt + | VTerm s -> str s + +let pr_comment pr_c = function + | CommentConstr c -> pr_c c + | CommentString s -> str s + | CommentInt n -> int n + +let pr_in_out_modules = function + | SearchInside l -> str"inside" ++ spc() ++ prlist_with_sep sep pr_reference l + | SearchOutside [] -> str"outside" + | SearchOutside l -> str"outside" ++ spc() ++ prlist_with_sep sep pr_reference l + +let pr_search a b pr_c = match a with + | SearchHead qid -> str"Search" ++ spc() ++ pr_reference qid ++ spc() ++ pr_in_out_modules b + | SearchPattern c -> str"SearchPattern" ++ spc() ++ pr_c c ++ spc() ++ pr_in_out_modules b + | SearchRewrite c -> str"SearchRewrite" ++ spc() ++ pr_c c ++ spc() ++ pr_in_out_modules b + | SearchAbout _ -> str"TODO" + +let pr_class_rawexpr = function + | FunClass -> str"FUNCLASS" + | SortClass -> str"SORTCLASS" + | RefClass qid -> pr_reference qid + +let pr_option_ref_value = function + | QualidRefValue id -> pr_reference id + | StringRefValue s -> qs s + +let pr_printoption a b = match a with + | Goptions.PrimaryTable table -> str table ++ pr_opt (prlist_with_sep sep pr_option_ref_value) b + | Goptions.SecondaryTable (table,field) -> str table ++ spc() ++ str field ++ pr_opt (prlist_with_sep sep pr_option_ref_value) b + +let pr_set_option a b = + let pr_opt_value = function + | IntValue n -> int n + | StringValue s -> str s + | BoolValue b -> mt() + in pr_printoption a None ++ spc() ++ pr_opt_value b + +let pr_topcmd _ = str"(* <Warning> : No printer for toplevel commands *)" + +let pr_destruct_location = function + | Tacexpr.ConclLocation () -> str"Conclusion" + | Tacexpr.HypLocation b -> if b then str"Discardable Hypothesis" else str"Hypothesis" + +let pr_opt_hintbases l = match l with + | [] -> mt() + | _ as z -> str":" ++ spc() ++ prlist_with_sep sep str z + +let pr_hints db h pr_c = + let db_name = function + | [] -> (false , mt()) + | c1::c2 -> match c1 with + | None,_ -> (false , mt()) + | Some name,_ -> (true , pr_id name) + in let opth = pr_opt_hintbases db + in let pr_aux = function + | CRef qid -> pr_reference qid + | _ -> mt () + in match h with + | HintsResolve l -> let (f,dbn) = db_name l in if f then hov 1 (str"Hint" ++ spc() ++ dbn ++ spc() ++ opth ++ spc() ++ str":=" ++ spc() ++ str"Resolve" ++ spc() ++ prlist_with_sep sep pr_c (List.map (fun (_,y) -> y) l)) else hov 1 (str"Hints Resolve" ++ spc() ++ prlist_with_sep sep pr_aux (List.map (fun (_,y) -> y) l) ++ spc() ++ opth) + | HintsImmediate l -> let (f,dbn) = db_name l in if f then hov 1 (str"Hint" ++ spc() ++ dbn ++ spc() ++ opth ++ spc() ++ str":=" ++ spc() ++ str"Immediate" ++ spc() ++ prlist_with_sep sep pr_c (List.map (fun (_,y) -> y) l)) else hov 1 (str"Hints Immediate" ++ spc() ++ prlist_with_sep sep pr_aux (List.map (fun (_,y) -> y) l) ++ spc() ++ opth) + | HintsUnfold l -> let (f,dbn) = db_name l in if f then hov 1 (str"Hint" ++ spc() ++ dbn ++ spc() ++ opth ++ spc() ++ str":=" ++ spc() ++ str"Unfold" ++ spc() ++ prlist_with_sep sep pr_reference (List.map (fun (_,y) -> y) l)) else hov 1 (str"Hints Unfold" ++ spc() ++ prlist_with_sep sep pr_reference (List.map (fun (_,y) -> y) l) ++ spc() ++ opth) + | HintsConstructors (n,c) -> hov 1 (str"Hint" ++ spc() ++ pr_id n ++ spc() ++ opth ++ spc() ++ str":=" ++ spc() ++ str"Constructors" ++ spc() ++ pr_reference c) + | HintsExtern (name,n,c,tac) -> hov 1 (str"Hint" ++ spc() ++ pr_id name ++ spc() ++ opth ++ spc() ++ str":=" ++ spc() ++ str"Extern" ++ spc() ++ int n ++ spc() ++ pr_c c ++ pr_raw_tactic tac) + +let pr_with_declaration pr_c = function + | CWith_Definition (id,c) -> str"Definition" ++ spc() ++ pr_id id ++ str" := " ++ pr_c c + | CWith_Module (id,qid) -> str"Module" ++ spc() ++ pr_id id ++ str" := " ++ pr_located pr_qualid qid + +let rec pr_module_type pr_c = function + | CMTEident qid -> pr_located pr_qualid qid + | CMTEwith (mty,decl) -> pr_module_type pr_c mty ++ spc() ++ str"with" ++ spc() ++ pr_with_declaration pr_c decl + +let pr_module_vardecls pr_c (l,mty) = prlist_with_sep (fun _ -> str",") pr_id l ++ spc() ++ pr_module_type pr_c mty + +let pr_module_binders l pr_c = str"[" ++ prlist_with_sep (fun _ -> str";") (pr_module_vardecls pr_c) l ++ str"]" + +let pr_module_binders_list l pr_c = pr_module_binders l pr_c + +let rec pr_module_expr = function + | CMEident qid -> pr_located pr_qualid qid + | CMEapply (me1,me2) -> pr_module_expr me1 ++ spc() ++ pr_module_expr me2 + +let pr_opt_casted_constr pr_c = function + | CCast (loc,c,t) -> pr_c c ++ str":" ++ pr_c t + | _ as c -> pr_c c + +let pr_type_option pr_c = function + | CHole loc -> mt() + | _ as c -> str":" ++ pr_c c + +let pr_valdecls pr_c = function + | LocalRawAssum (na,c) -> prlist_with_sep (fun _ -> str",") (pr_located pr_name) na ++ spc() ++ pr_type_option pr_c c + | LocalRawDef (na,c) -> pr_located pr_name na ++ spc() ++ str":=" ++ spc() ++ pr_opt_casted_constr pr_c c + +let pr_binders pr_c l = match l with +| [] -> mt() +| _ as t -> str"(" ++ prlist_with_sep (fun _ -> str") (") (pr_valdecls pr_c) t ++ str")" + +let pr_onescheme (id,dep,ind,s) = pr_id id ++ spc() ++ str":=" ++ spc() ++ if dep then str"Induction for" else str"Minimality for" ++ spc() ++ pr_reference ind ++ spc() ++ str"Sort" ++ spc() ++ pr_sort s + +let pr_class_rawexpr = function + | FunClass -> str"FUNCLASS" + | SortClass -> str"SORTCLASS" + | RefClass qid -> pr_reference qid + +let pr_assumption_token = function + | (Decl_kinds.Local,Decl_kinds.Logical) -> str"Hypothesis" + | (Decl_kinds.Local,Decl_kinds.Definitional) -> str"Variable" + | (Decl_kinds.Global,Decl_kinds.Logical) -> str"Axiom" + | (Decl_kinds.Global,Decl_kinds.Definitional) -> str"Parameter" + +let pr_params pr_c (a,(b,c)) = pr_id b ++ spc() ++ if a then str":>" else str":" ++ spc() ++ pr_c c + +let pr_ne_params_list pr_c l = prlist_with_sep sep_pv (pr_params pr_c) l + +let pr_thm_token = function + | Decl_kinds.Theorem -> str"Theorem" + | Decl_kinds.Lemma -> str"Lemma" + | Decl_kinds.Fact -> str"Fact" + | Decl_kinds.Remark -> str"Remark" + +let pr_syntax_modifier = function + | SetItemLevel (l,n) -> prlist_with_sep (fun _ -> str",") str l ++ spc() ++ str"at level" ++ spc() ++ int n + | SetLevel n -> str"at level" ++ spc() ++ int n + | SetAssoc Gramext.LeftA -> str"left associativity" + | SetAssoc Gramext.RightA -> str"right associativity" + | SetAssoc Gramext.NonA -> str"no associativity" + | SetEntryType (x,typ) -> str x ++ spc() ++ pr_set_entry_type typ + | SetOnlyParsing -> str"only parsing" + +let pr_grammar_tactic_rule (name,(s,pil),t) = str name ++ spc() ++ str"[" ++ qs s ++ spc() ++ prlist_with_sep sep pr_production_item pil ++ str"]" ++ spc() ++ str"->" ++ spc() ++ str"[" ++ pr_raw_tactic t ++ str"]" + +let pr_box b = let pr_boxkind = function + | PpHB n -> str"h" ++ spc() ++ int n + | PpVB n -> str"v" ++ spc() ++ int n + | PpHVB n -> str"hv" ++ spc() ++ int n + | PpHOVB n -> str"hov" ++ spc() ++ int n + | PpTB -> str"t" +in str"<" ++ pr_boxkind b ++ str">" + +let pr_paren_reln_or_extern = function + | None,L -> str"L" + | None,E -> str"E" + | Some pprim,Any -> qs pprim + | Some pprim,Prec p -> qs pprim ++ spc() ++ str":" ++ spc() ++ int p + | _ -> mt() + +let rec pr_next_hunks = function + | UNP_FNL -> str"FNL" + | UNP_TAB -> str"TAB" + | RO c -> qs c + | UNP_BOX (b,ll) -> str"[" ++ pr_box b ++ prlist_with_sep sep pr_next_hunks ll ++ str"]" + | UNP_BRK (n,m) -> str"[" ++ int n ++ spc() ++ int m ++ str"]" + | UNP_TBRK (n,m) -> str"[ TBRK" ++ int n ++ spc() ++ int m ++ str"]" + | PH (e,None,_) -> print_ast e + | PH (e,Some ext,pr) -> print_ast e ++ spc() ++ str":" ++ spc() ++ pr_paren_reln_or_extern (Some ext,pr) + | UNP_SYMBOLIC _ -> mt() + +let pr_unparsing u = prlist_with_sep sep pr_next_hunks u + +let pr_astpat a = str"<<" ++ print_ast a ++ str">>" + +let pr_syntax_rule (nm,s,u) = str nm ++ spc() ++ str"[" ++ pr_astpat s ++ str"]" ++ spc() ++ str"->" ++ spc() ++ pr_unparsing u + +let pr_syntax_entry (p,rl) = str"level" ++ spc() ++ int p ++ spc() ++ str":" ++ spc() ++ prlist_with_sep (fun _ -> brk(1,1) ++ str"|") pr_syntax_rule rl + +let sep_end = str";" + +(**************************************) +(* Pretty printer for vernac commands *) +(**************************************) +let make_pr_vernac pr_constr = + +let pr_constrarg c = spc () ++ pr_constr c in +let pr_intarg n = spc () ++ int n in + +let rec pr_vernac = function + + (* Proof management *) + | VernacAbortAll -> str "Abort All" + | VernacRestart -> str"Restart" + | VernacSuspend -> str"Suspend" + | VernacUnfocus -> str"Unfocus" + | VernacGoal c -> str"Goal" ++ pr_constrarg c + | VernacAbort id -> str"Abort" ++ pr_opt (pr_located pr_id) id + | VernacResume id -> str"Resume" ++ pr_opt (pr_located pr_id) id + | VernacUndo i -> if i=1 then str"Undo" else str"Undo" ++ pr_intarg i + | VernacFocus i -> str"Focus" ++ pr_opt int i + | VernacGo g -> + let pr_goable = function + | GoTo i -> int i + | GoTop -> str"top" + | GoNext -> str"next" + | GoPrev -> str"prev" + in str"Go" ++ spc() ++ pr_goable g + | VernacShow s -> + let pr_showable = function + | ShowGoal n -> str"Show" ++ pr_opt int n + | ShowGoalImplicitly n -> str"Show Implicits" ++ pr_opt int n + | ShowProof -> str"Show Proof" + | ShowNode -> str"Show Node" + | ShowScript -> str"Show Script" + | ShowExistentials -> str"Show Existentials" + | ShowTree -> str"Show Tree" + | ShowProofNames -> str"Show Conjectures" + | ShowIntros b -> str"Show " ++ (if b then str"Intros" else str"Intro") + | ExplainProof l -> str"Explain Proof" ++ spc() ++ prlist_with_sep sep int l + | ExplainTree l -> str"Explain Proof Tree" ++ spc() ++ prlist_with_sep sep int l + in pr_showable s + | VernacCheckGuard -> str"Guarded" + | VernacDebug b -> pr_topcmd b + + (* Resetting *) + | VernacResetName id -> str"Reset" ++ spc() ++ pr_located pr_id id + | VernacResetInitial -> str"Reset Initial" + | VernacBack i -> if i=1 then str"Back" else str"Back" ++ pr_intarg i + + (* State management *) + | VernacWriteState s -> str"Write State" ++ spc () ++ qs s + | VernacRestoreState s -> str"Restore State" ++ spc() ++ qs s + + (* Control *) + | VernacList l -> hov 2 (str"[" ++ spc() ++ prlist_with_sep (fun _ -> sep_end ++ fnl() ) (pr_located pr_vernac) l ++ spc() ++ str"]") + | VernacLoad (f,s) -> str"Load" ++ if f then (spc() ++ str"Verbose" ++ spc()) else spc() ++ str s + | VernacTime v -> str"Time" ++ spc() ++ pr_vernac v + | VernacVar id -> pr_id id + + (* Syntax *) + | VernacGrammar _ -> str"(* <Warning> : Grammar is replaced by Notation *)" + | VernacTacticGrammar l -> hov 1 (str"Grammar tactic simple_tactic :=" ++ spc() ++ prlist_with_sep (fun _ -> brk(1,1) ++ str"|") pr_grammar_tactic_rule l) (***) + | VernacSyntax (u,el) -> hov 1 (str"Syntax" ++ str u ++ prlist_with_sep (fun _ -> str";") pr_syntax_entry el) (***) + | VernacOpenScope sc -> str"Open Scope" ++ spc() ++ str sc + | VernacDelimiters (sc,key) -> str"Delimits Scope" ++ spc () ++ str sc ++ spc () ++ str key + | VernacArgumentsScope (q,scl) -> let pr_opt_scope = function + | None -> str"_" + | Some sc -> str sc in + str"Arguments Scope" ++ spc() ++ pr_reference q ++ spc() ++ str"[" ++ prlist_with_sep sep pr_opt_scope scl ++ str"]" + | VernacInfix (a,p,s,q,_,sn) -> (* A Verifier *) + h 0 (str"Infix" ++ pr_entry_prec a ++ pr_intarg p ++ spc() ++ qs s ++ spc() ++ pr_reference q ++ (match sn with + | None -> mt() + | Some sc -> spc() ++ str":" ++ spc() ++ str sc)) + | VernacDistfix (a,p,s,q,sn) -> h 0 (str"Distfix" ++ pr_entry_prec a ++ pr_intarg p ++ spc() ++ qs s ++ spc() ++ pr_reference q ++ (match sn with + | None -> mt() + | Some sc -> spc() ++ str":" ++ spc() ++ str sc)) + | VernacNotation (s,c,l,opt) -> str"Notation" ++ spc() ++ qs s ++ pr_constrarg c ++ (match l with + | [] -> mt() + | _ as t -> spc() ++ str"(" ++ prlist_with_sep (fun _ -> str",") pr_syntax_modifier t ++ str")") ++ (match opt with + | None -> mt() + | Some sc -> spc() ++ str":" ++ spc() ++ str sc) (***) + | VernacSyntaxExtension (a,b) -> str"Uninterpreted Notation" ++ spc() ++ qs a ++ (match b with | [] -> mt() | _ as l -> str"(" ++ prlist_with_sep (fun _ -> str",") pr_syntax_modifier l ++ str")") + + (* Gallina *) + | VernacDefinition (d,id,b,f,e) -> (* A verifier... *) + let pr_def_token = function + | Decl_kinds.LCoercion -> str"Coercion Local" + | Decl_kinds.GCoercion -> str"Coercion" + | Decl_kinds.LDefinition -> str"Local" + | Decl_kinds.GDefinition -> str"Definition" + | Decl_kinds.SCanonical -> str"Canonical Structure" + in let pr_reduce = function + | None -> mt() + | Some r -> str"Eval" ++ spc() ++ pr_red_expr (pr_constr, fun _ -> str"TODO" (* pr_metanum pr_reference *)) r ++ spc() ++ str"in" ++ spc() + in let pr_binders_def = function + | [] -> mt () + | _ as l -> spc() ++ str"(" ++ prlist_with_sep (fun _ -> str") (") (pr_valdecls pr_constr) l ++ str")" + in let pr_valloc (l,c) = match l with + | [] -> mt () + | _ -> prlist_with_sep (fun _ -> str",") (pr_located pr_name) l ++ str":" ++ pr_constr c + in let pr_binders_def2 = function + | [] -> mt () + | _ as l -> spc() ++ str"(" ++ prlist_with_sep (fun _ -> str") (") pr_valloc l ++ str")" + in let pr_def_body = function + | DefineBody (bl,red,c,d) -> (match c with + | CLambdaN (_,bl2,a) -> (pr_binders_def bl ++ pr_binders_def2 bl2, (match d with + | None -> mt() + | Some t -> spc() ++ str":" ++ pr_constrarg t) , Some (pr_reduce red ++ pr_constr a)) + | _ -> (pr_binders_def bl , (match d with + | None -> mt() + | Some t -> spc() ++ str":" ++ pr_constrarg t) , Some (pr_reduce red ++ pr_constr c))) + | ProveBody (bl,t) -> (pr_binders_def bl , pr_constrarg t , None) + in let (binds,typ,c) = pr_def_body b + in h 0 (pr_def_token e ++ spc() ++ pr_id id ++ binds ++ typ ++ (match c with + | None -> mt() + | Some cc -> spc() ++ str":=" ++ spc() ++ cc)) + | VernacStartTheoremProof (ki,id,(bl,c),b,d) -> hov 1 (pr_thm_token ki ++ spc() ++ pr_id id ++ spc() ++ (match bl with | [] -> mt() | _ -> pr_binders pr_constr bl ++ spc()) ++ str":" ++ spc() ++ pr_constr c) + | VernacEndProof (opac,o) -> (match o with + | None -> if opac then str"Qed" else str"Defined" + | Some (id,th) -> (match th with + | None -> (if opac then str"Save" else str"Defined") ++ spc() ++ pr_id id + | Some tok -> str"Save" ++ spc() ++ pr_thm_token tok ++ spc() ++ pr_id id)) + | VernacExactProof c -> str"Proof" ++ pr_constrarg c + | VernacAssumption (stre,l) -> hov 1 (pr_assumption_token stre ++ spc() ++ pr_ne_params_list pr_constr l) + | VernacInductive (f,l) -> let pr_constructor (coe,(id,c)) = pr_id id ++ spc() ++ (if coe then str":>" else str":") ++ pr_constrarg c in + let pr_constructor_list l = match l with + | [] -> mt() + | _ -> fnl() ++ str"| " ++ prlist_with_sep (fun _ -> fnl() ++ str"| ") pr_constructor l in + let pr_simple_binder (s,t) = pr_id s ++ str":" ++ pr_constr t in + let pr_ne_simple_binders = function + | [] -> mt() + | _ as l -> str"(" ++ prlist_with_sep (fun _ -> str") (") pr_simple_binder l ++ str")" ++ spc() in + let pr_oneind (id,indpar,s,lc) = pr_id id ++ spc() ++ pr_ne_simple_binders indpar ++ str":" ++ spc() ++ pr_constr s ++ spc() ++ str":=" ++ pr_constructor_list lc + in hov 1 ((if f then str"Inductive" else str"CoInductive") ++ spc() ++ prlist_with_sep (fun _ -> brk(1,1) ++ str"with ") pr_oneind l) + | VernacFixpoint recs -> let pr_fixbinder (l,c) = prlist_with_sep (fun _ -> str",") (pr_located pr_name) l ++ str":" ++ pr_constr c in + let pr_fixbinders l = str"[" ++ prlist_with_sep (fun _ -> str";") pr_fixbinder l ++ str"]" in + let pr_onerec = function + | (id,_,CProdN(_,bl,type_),CLambdaN(_,_,def)) -> pr_id id ++ spc() ++ pr_fixbinders bl ++ spc() ++ str":" ++ spc() ++ pr_constr type_ ++ spc() ++ str":=" ++ spc() ++ pr_constr def + | _ -> mt() + in hov 1 (str"Fixpoint" ++ spc() ++ prlist_with_sep (fun _ -> brk(1,1) ++ str"with ") pr_onerec recs) + | VernacCoFixpoint corecs -> let pr_onecorec (id,c,def) = pr_id id ++ spc() ++ str":" ++ pr_constrarg c ++ spc() ++ str":=" ++ pr_constrarg def + in hov 1 (str"CoFixpoint" ++ spc() ++ prlist_with_sep (fun _ -> brk(1,1) ++ str"with ") pr_onecorec corecs) + | VernacScheme l -> hov 1 (str"Scheme" ++ spc() ++ prlist_with_sep (fun _ -> brk(1,1) ++ str"with") pr_onescheme l) + + (* Gallina extensions *) + | VernacRecord ((oc,name),ps,s,c,fs) -> let pr_simple_binder (s,t) = pr_id s ++ str":" ++ pr_constr t in + let pr_record_field = function + | (oc,AssumExpr (id,t)) -> pr_id id ++ spc() ++ if oc then str":>" else str":" ++ spc() ++ pr_constr t + | (oc,DefExpr(id,b,opt)) -> (match opt with + | Some t -> pr_id id ++ spc() ++ if oc then str":>" else str":" ++ spc() ++ pr_constr t ++ spc() ++ str":=" ++ pr_constr b + | None -> pr_id id ++ spc() ++ str":=" ++ pr_constr b) in + hov 1 (str"Record" ++ if oc then str" > " else spc() ++ pr_id name ++ spc() ++ (match ps with + | [] -> mt() + | _ as l -> str"[" ++ prlist_with_sep (fun _ -> str";") pr_simple_binder l ++ str"]") ++ spc() ++ str":" ++ spc() ++ (* pr_sort s *) str"TODO" ++ spc() ++ str":=" ++ (match c with + | None -> mt() + | Some sc -> pr_id sc) ++ spc() ++ str"{" ++ cut() ++ prlist_with_sep (fun _ -> str";" ++ brk(1,1)) pr_record_field fs ++ str"}") + | VernacBeginSection id -> h 0 (str"Section" ++ spc () ++ pr_id id) + | VernacEndSegment id -> h 0 (str"End" ++ spc() ++ pr_id id) + | VernacRequire (exp,spe,l) -> h 0 ((match exp with + | None -> str"Read Module" + | Some export -> str"Require" ++ if export then spc() ++ str"Export" else mt ()) ++ spc() ++ + (match spe with + | None -> mt() + | Some flag -> (if flag then str"Specification" else str"Implementation") ++ spc ()) ++ + prlist_with_sep sep pr_reference l) + | VernacImport (f,l) -> if f then str"Export" else str"Import" ++ spc() ++ prlist_with_sep sep pr_reference l + | VernacCanonical q -> str"Canonical Structure" ++ spc() ++ pr_reference q + | VernacCoercion (s,id,c1,c2) -> hov 1 (str"Coercion" ++ (match s with | Decl_kinds.Local -> spc() ++ str"Local" ++ spc() | Decl_kinds.Global -> spc()) ++ pr_reference id ++ spc() ++ str":" ++ spc() ++ pr_class_rawexpr c1 ++ spc() ++ str">->" ++ spc() ++ pr_class_rawexpr c2) + | VernacIdentityCoercion (s,id,c1,c2) -> hov 1 (str"Identity Coercion" ++ (match s with | Decl_kinds.Local -> spc() ++ str"Local" ++ spc() | Decl_kinds.Global -> spc()) ++ pr_id id ++ spc() ++ str":" ++ spc() ++ pr_class_rawexpr c1 ++ spc() ++ str">->" ++ spc() ++ pr_class_rawexpr c2) + + (* Modules and Module Types *) + | VernacDeclareModule (id,l,m1,m2) -> hov 1 (str"Module" ++ spc() ++ pr_id id ++ spc() ++ pr_module_binders_list l pr_constr ++ (match m1 with + | None -> mt() + | Some n1 -> str" : " ++ str"TODO" (* pr_module_type pr_constr n1 *) ) ++ (match m2 with + | None -> mt() + | Some n2 -> str" := " ++ pr_module_expr n2)) + | VernacDeclareModuleType (id,l,m) -> hov 1 (str"Module Type" ++ spc() ++ pr_id id ++ spc() ++ pr_module_binders_list l pr_constr ++ (match m with + | None -> mt() + | Some n -> str" := " ++ pr_module_type pr_constr n)) + + (* Solving *) + | VernacSolve (i,tac,_) -> pr_raw_tactic tac (* A Verifier *) + | VernacSolveExistential (i,c) -> str"Existential" ++ spc() ++ int i ++ pr_constrarg c + + (* Auxiliary file and library management *) + | VernacRequireFrom (exp,spe,f) -> h 0 (str"Require" ++ if exp then spc() ++ str"Export" ++ spc() else spc() ++ (match spe with + | None -> mt() + | Some false -> str"Implementation" ++ spc() + | Some true -> str"Specification" ++ spc ()) ++ qs f) + | VernacAddLoadPath (fl,s,d) -> hov 1 (str"Add" ++ if fl then str" Rec " else spc() ++ str"LoadPath" ++ spc() ++ qs s ++ (match d with + | None -> mt() + | Some dir -> spc() ++ str"as" ++ spc() ++ pr_dirpath dir)) + | VernacRemoveLoadPath s -> str"Remove LoadPath" ++ qs s + | VernacAddMLPath (fl,s) -> str"Add" ++ if fl then str" Rec " else spc() ++ str"ML Path" ++ qs s + | VernacDeclareMLModule l -> hov 1 (str"Declare ML Module" ++ spc() ++ prlist_with_sep sep qs l) + | VernacChdir s -> str"Cd" ++ pr_opt qs s + + (* Commands *) + | VernacDeclareTacticDefinition (_,l) -> (match l with + | [] -> mt() + | [(id,b)] -> hov 1 (str"Tactic Definition" ++ spc() ++ pr_located pr_id id ++ spc() ++ str":=" ++ spc() ++ pr_raw_tactic b) + | _ as t -> let pr_vrec_clause (id,b) = pr_located pr_id id ++ spc() ++ str":=" ++ spc() ++ pr_raw_tactic b in hov 1 (str"Recursive Tactic Definition" ++ spc() ++ prlist_with_sep (fun _ -> brk(1,1) ++ str"And") pr_vrec_clause t)) + | VernacHints (dbnames,h) -> pr_hints dbnames h pr_constr + | VernacHintDestruct (id,loc,c,i,tac) -> hov 1 (str"HintDestruct" ++ spc() ++ pr_destruct_location loc ++ spc() ++ pr_id id ++ pr_constrarg c ++ pr_intarg i ++ spc() ++ str"[" ++ pr_raw_tactic tac ++ str"]") + | VernacSyntacticDefinition (id,c,None) -> hov 1 (str"Syntactic Definition" ++ spc() ++ pr_id id ++ spc() ++ str":=" ++ pr_constrarg c) + | VernacSyntacticDefinition (id,c,Some n) -> hov 1 (str"Syntactic Definition" ++ spc() ++ pr_id id ++ spc() ++ str":=" ++ pr_constrarg c ++ spc() ++ str"|" ++ int n) + | VernacDeclareImplicits (q,None) -> hov 1 (str"Implicits" ++ spc() ++ pr_reference q) + | VernacDeclareImplicits (q,Some l) -> hov 1 (str"Implicits" ++ spc() ++ pr_reference q ++ spc() ++ str"[" ++ prlist_with_sep sep int l ++ str"]") + | VernacSetOpacity (fl,l) -> hov 1 (if fl then str"Opaque" else str"Transparent" ++ spc() ++ prlist_with_sep sep pr_reference l) + | VernacUnsetOption na -> hov 1 (str"Unset" ++ spc() ++ pr_printoption na None) + | VernacSetOption (Goptions.SecondaryTable ("Implicit","Arguments"),BoolValue true) -> str"Set Implicit Arguments" + | VernacSetOption (Goptions.SecondaryTable ("Implicit","Arguments"),BoolValue false) -> str"Unset Implicit Arguments" + | VernacSetOption (na,v) -> hov 1 (str"Set" ++ spc() ++ pr_set_option na v) + | VernacAddOption (na,l) -> hov 1 (str"Add" ++ spc() ++ pr_printoption na (Some l)) + | VernacRemoveOption (na,l) -> hov 1 (str"Remove" ++ spc() ++ pr_printoption na (Some l)) + | VernacMemOption (na,l) -> hov 1 (str"Test" ++ spc() ++ pr_printoption na (Some l)) + | VernacPrintOption na -> hov 1 (str"Test" ++ spc() ++ pr_printoption na None) + | VernacCheckMayEval (r,io,c) -> + let pr_mayeval r c = match r with + | Some r0 -> h 0 (str"Eval" ++ spc() ++ pr_red_expr (pr_constr,fun _ -> str"TODO" (*pr_metanum pr_reference *)) r0 ++ spc() ++ str"in" ++ spc () ++ pr_constr c) + | None -> h 0 (str"Check" ++ spc() ++ pr_constr c) + in pr_mayeval r c + | VernacGlobalCheck c -> hov 1 (str"Type" ++ pr_constrarg c) + | VernacPrint p -> + let pr_printable = function + | PrintFullContext -> str"Print All" + | PrintSectionContext s -> str"Print Section" ++ spc() ++ pr_reference s + | PrintGrammar (uni,ent) -> str"Print Grammar" ++ spc() ++ str uni ++ spc() ++ str ent + | PrintLoadPath -> str"Print LoadPath" + | PrintModules -> str"Print Modules" + | PrintMLLoadPath -> str"Print ML Path" + | PrintMLModules -> str"Print ML Modules" + | PrintGraph -> str"Print Graph" + | PrintClasses -> str"Print Classes" + | PrintCoercions -> str"Print Coercions" + | PrintCoercionPaths (s,t) -> str"Print Coercion Paths" ++ spc() ++ pr_class_rawexpr s ++ spc() ++ pr_class_rawexpr t + | PrintTables -> str"Print Tables" + | PrintOpaqueName qid -> str"Print Proof" ++ spc() ++ pr_reference qid + | PrintHintGoal -> str"Print Hint" + | PrintHint qid -> str"Print Hint" ++ spc() ++ pr_reference qid + | PrintHintDb -> str"Print Hint *" + | PrintHintDbName s -> str"Print HintDb" ++ spc() ++ str s + | PrintUniverses fopt -> str"Dump Universes" ++ pr_opt str fopt + | PrintName qid -> str"Print" ++ spc() ++ pr_reference qid + | PrintLocalContext -> str"Print" + | PrintModuleType qid -> str"Print Module Type" ++ spc() ++ pr_reference qid + | PrintModule qid -> str"Print Module" ++ spc() ++ pr_reference qid + | PrintInspect n -> str"Inspect" ++ spc() ++ int n + | PrintScope s -> str"Scope" ++ spc() ++ str s + in pr_printable p + | VernacSearch (sea,sea_r) -> pr_search sea sea_r pr_constr + | VernacLocate loc -> + let pr_locate =function + | LocateTerm qid -> pr_reference qid + | LocateFile f -> str"File" ++ spc() ++ qs f + | LocateLibrary qid -> str"Library" ++ spc () ++ pr_reference qid + in str"Locate" ++ spc() ++ pr_locate loc + | VernacComments l -> hov 1 (str"Comments" ++ spc() ++ prlist_with_sep sep (pr_comment pr_constr) l) + | VernacNop -> str"Proof" + + (* Toplevel control *) + | VernacToplevelControl exn -> pr_topcmd exn + + (* For extension *) + | VernacExtend (s,c) -> hov 1 (str s ++ prlist_with_sep sep pr_constrarg (List.map (Genarg.out_gen Genarg.rawwit_constr) c)) + | VernacV7only _ | VernacV8only _ -> mt () + | VernacProof _ | VernacDefineModule _ -> str"TODO" +in pr_vernac + +let pr_vernac = make_pr_vernac (Ppconstrnew.pr_constr) + diff --git a/translate/ppvernacnew.mli b/translate/ppvernacnew.mli new file mode 100644 index 000000000..0e4bde50e --- /dev/null +++ b/translate/ppvernacnew.mli @@ -0,0 +1,31 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) + +(* $Id$ *) + +open Pp +open Genarg +open Vernacexpr +open Names +open Nameops +open Nametab +open Util +open Extend +open Ppconstr +open Pptactic +open Rawterm +open Coqast +open Pcoq +open Ast +open Libnames +open Ppextend +open Topconstr + +val sep_end : std_ppcmds + +val pr_vernac : vernac_expr -> std_ppcmds |