diff options
| author |  coq <coq@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2005-05-25 13:13:15 +0000 |
|---|---|---|
| committer | coq <coq@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2005-05-25 13:13:15 +0000 |
| commit | 8464cd8a8df852799da9cb7a1fd94b8faf3cf9c6 (patch) | |
| tree | 5e14754072c2423caed6c298d54bfe493aedba27 | |
| parent | 6dfe936f332da0728380ae3a7f75bc87f6c4c447 (diff) | |
Added subtac contrib.
Added some debug printer in termops.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7073 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | .depend | 348 | ||||
| -rw-r--r-- | .depend.camlp4 | 1 | ||||
| -rw-r--r-- | Makefile | 21 | ||||
| -rw-r--r-- | contrib/subtac/infer.ml | 827 | ||||
| -rw-r--r-- | contrib/subtac/infer.mli | 59 | ||||
| -rw-r--r-- | contrib/subtac/natural.ml | 10 | ||||
| -rw-r--r-- | contrib/subtac/rewrite.ml | 637 | ||||
| -rw-r--r-- | contrib/subtac/rewrite.mli | 3 | ||||
| -rw-r--r-- | contrib/subtac/sast.ml | 27 | ||||
| -rw-r--r-- | contrib/subtac/scoq.ml | 58 | ||||
| -rw-r--r-- | contrib/subtac/sparser.ml4 | 336 | ||||
| -rw-r--r-- | dev/ocamldebug-coq.template | 1 | ||||
| -rw-r--r-- | pretyping/termops.ml | 33 | ||||
| -rw-r--r-- | pretyping/termops.mli | 2 |
14 files changed, 2205 insertions, 158 deletions
@@ -53,12 +53,12 @@ kernel/indtypes.cmi: kernel/univ.cmi kernel/typeops.cmi kernel/term.cmi \ kernel/declarations.cmi kernel/inductive.cmi: kernel/univ.cmi kernel/term.cmi kernel/names.cmi \ kernel/environ.cmi kernel/declarations.cmi -kernel/mod_subst.cmi: kernel/term.cmi lib/pp.cmi kernel/names.cmi -kernel/mod_typing.cmi: kernel/environ.cmi kernel/entries.cmi \ - kernel/declarations.cmi kernel/modops.cmi: lib/util.cmi kernel/univ.cmi kernel/names.cmi \ kernel/mod_subst.cmi kernel/environ.cmi kernel/entries.cmi \ kernel/declarations.cmi +kernel/mod_subst.cmi: kernel/term.cmi lib/pp.cmi kernel/names.cmi +kernel/mod_typing.cmi: kernel/environ.cmi kernel/entries.cmi \ + kernel/declarations.cmi kernel/names.cmi: lib/predicate.cmi lib/pp.cmi kernel/reduction.cmi: kernel/univ.cmi kernel/term.cmi kernel/sign.cmi \ kernel/environ.cmi @@ -82,9 +82,6 @@ kernel/vm.cmi: kernel/term.cmi kernel/names.cmi kernel/cemitcodes.cmi \ kernel/cbytecodes.cmi lib/bigint.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 lib/compat.cmo library/declare.cmi: kernel/term.cmi kernel/sign.cmi kernel/safe_typing.cmi \ library/nametab.cmi kernel/names.cmi library/libnames.cmi \ kernel/indtypes.cmi kernel/entries.cmi kernel/declarations.cmi \ @@ -115,6 +112,9 @@ library/library.cmi: lib/util.cmi lib/system.cmi lib/pp.cmi kernel/names.cmi \ library/nameops.cmi: kernel/term.cmi lib/pp.cmi kernel/names.cmi library/nametab.cmi: lib/util.cmi lib/pp.cmi kernel/names.cmi \ library/libnames.cmi +lib/rtree.cmi: lib/pp.cmi +lib/system.cmi: lib/pp.cmi +lib/util.cmi: lib/pp.cmi lib/compat.cmo parsing/ast.cmi: lib/util.cmi interp/topconstr.cmi lib/pp.cmi \ kernel/names.cmi kernel/mod_subst.cmi library/libnames.cmi \ interp/genarg.cmi lib/dyn.cmi parsing/coqast.cmi @@ -349,11 +349,11 @@ toplevel/record.cmi: toplevel/vernacexpr.cmo interp/topconstr.cmi \ toplevel/searchisos.cmi: kernel/term.cmi kernel/names.cmi \ library/libobject.cmi toplevel/toplevel.cmi: lib/pp.cmi parsing/pcoq.cmi -toplevel/vernac.cmi: toplevel/vernacexpr.cmo lib/util.cmi parsing/pcoq.cmi toplevel/vernacentries.cmi: toplevel/vernacinterp.cmi toplevel/vernacexpr.cmo \ interp/topconstr.cmi kernel/term.cmi kernel/names.cmi \ library/libnames.cmi pretyping/evd.cmi kernel/environ.cmi toplevel/vernacinterp.cmi: proofs/tacexpr.cmo +toplevel/vernac.cmi: toplevel/vernacexpr.cmo lib/util.cmi parsing/pcoq.cmi toplevel/whelp.cmi: interp/topconstr.cmi kernel/term.cmi kernel/names.cmi \ kernel/environ.cmi translate/ppconstrnew.cmi: lib/util.cmi interp/topconstr.cmi kernel/term.cmi \ @@ -374,9 +374,9 @@ contrib/cc/ccalgo.cmi: kernel/term.cmi kernel/names.cmi contrib/cc/ccproof.cmi: kernel/names.cmi contrib/cc/ccalgo.cmi contrib/correctness/past.cmi: lib/util.cmi interp/topconstr.cmi \ kernel/term.cmi kernel/names.cmi -contrib/correctness/pcic.cmi: pretyping/rawterm.cmi contrib/correctness/pcicenv.cmi: kernel/term.cmi kernel/sign.cmi \ kernel/names.cmi +contrib/correctness/pcic.cmi: pretyping/rawterm.cmi contrib/correctness/pdb.cmi: kernel/names.cmi contrib/correctness/peffect.cmi: lib/pp.cmi kernel/names.cmi contrib/correctness/penv.cmi: kernel/term.cmi kernel/names.cmi \ @@ -467,6 +467,16 @@ contrib/jprover/jall.cmi: contrib/jprover/opname.cmi \ contrib/jprover/jterm.cmi contrib/jprover/jlogic.cmi contrib/jprover/jlogic.cmi: contrib/jprover/jterm.cmi contrib/jprover/jterm.cmi: contrib/jprover/opname.cmi +contrib/old/rewrite.cmi: kernel/term.cmi kernel/sign.cmi \ + contrib/subtac/sast.cmo kernel/names.cmi library/libnames.cmi \ + contrib/subtac/infer.cmi pretyping/evd.cmi library/decl_kinds.cmo +contrib/old/sparser.cmi: lib/util.cmi interp/topconstr.cmi proofs/tacexpr.cmo \ + contrib/subtac/sast.cmo pretyping/rawterm.cmi parsing/pcoq.cmi \ + kernel/names.cmi library/libnames.cmi interp/genarg.cmi +contrib/subtac/infer.cmi: lib/util.cmi kernel/term.cmi \ + contrib/subtac/sast.cmo lib/pp.cmi contrib/subtac/natural.cmo \ + kernel/names.cmi +contrib/subtac/rewrite.cmi: contrib/subtac/sast.cmo kernel/names.cmi contrib/xml/doubleTypeInference.cmi: kernel/term.cmi kernel/names.cmi \ pretyping/evd.cmi kernel/environ.cmi contrib/xml/acic.cmo contrib/xml/xmlcommand.cmi: contrib/xml/xml.cmi kernel/term.cmi \ @@ -511,6 +521,14 @@ ide/config_lexer.cmo: lib/util.cmi ide/config_parser.cmi ide/config_lexer.cmx: lib/util.cmx ide/config_parser.cmx ide/config_parser.cmo: lib/util.cmi ide/config_parser.cmi ide/config_parser.cmx: lib/util.cmx ide/config_parser.cmi +ide/coqide.cmo: toplevel/vernacexpr.cmo lib/util.cmi ide/undo.cmi \ + lib/system.cmi ide/preferences.cmi proofs/pfedit.cmi ide/ideutils.cmi \ + ide/highlight.cmo ide/find_phrase.cmo ide/coq_commands.cmo ide/coq.cmi \ + ide/command_windows.cmi ide/blaster_window.cmo ide/coqide.cmi +ide/coqide.cmx: toplevel/vernacexpr.cmx lib/util.cmx ide/undo.cmx \ + lib/system.cmx ide/preferences.cmx proofs/pfedit.cmx ide/ideutils.cmx \ + ide/highlight.cmx ide/find_phrase.cmx ide/coq_commands.cmx ide/coq.cmx \ + ide/command_windows.cmx ide/blaster_window.cmx ide/coqide.cmi ide/coq.cmo: toplevel/vernacexpr.cmo toplevel/vernacentries.cmi \ toplevel/vernac.cmi lib/util.cmi pretyping/termops.cmi kernel/term.cmi \ proofs/tacmach.cmi tactics/tacinterp.cmi library/states.cmi \ @@ -535,14 +553,6 @@ ide/coq.cmx: toplevel/vernacexpr.cmx toplevel/vernacentries.cmx \ ide/coq.cmi ide/coq_tactics.cmo: ide/coq_tactics.cmi ide/coq_tactics.cmx: ide/coq_tactics.cmi -ide/coqide.cmo: toplevel/vernacexpr.cmo lib/util.cmi ide/undo.cmi \ - lib/system.cmi ide/preferences.cmi proofs/pfedit.cmi ide/ideutils.cmi \ - ide/highlight.cmo ide/find_phrase.cmo ide/coq_commands.cmo ide/coq.cmi \ - ide/command_windows.cmi ide/blaster_window.cmo ide/coqide.cmi -ide/coqide.cmx: toplevel/vernacexpr.cmx lib/util.cmx ide/undo.cmx \ - lib/system.cmx ide/preferences.cmx proofs/pfedit.cmx ide/ideutils.cmx \ - ide/highlight.cmx ide/find_phrase.cmx ide/coq_commands.cmx ide/coq.cmx \ - ide/command_windows.cmx ide/blaster_window.cmx ide/coqide.cmi ide/find_phrase.cmo: ide/ideutils.cmi ide/find_phrase.cmx: ide/ideutils.cmx ide/highlight.cmo: ide/ideutils.cmi @@ -723,6 +733,14 @@ kernel/inductive.cmo: lib/util.cmi kernel/univ.cmi kernel/type_errors.cmi \ kernel/inductive.cmx: lib/util.cmx kernel/univ.cmx kernel/type_errors.cmx \ kernel/term.cmx kernel/sign.cmx kernel/reduction.cmx kernel/names.cmx \ kernel/environ.cmx kernel/declarations.cmx kernel/inductive.cmi +kernel/modops.cmo: lib/util.cmi kernel/univ.cmi kernel/term.cmi lib/pp.cmi \ + kernel/names.cmi kernel/mod_subst.cmi kernel/environ.cmi \ + kernel/entries.cmi kernel/declarations.cmi kernel/cemitcodes.cmi \ + kernel/cbytegen.cmi kernel/modops.cmi +kernel/modops.cmx: lib/util.cmx kernel/univ.cmx kernel/term.cmx lib/pp.cmx \ + kernel/names.cmx kernel/mod_subst.cmx kernel/environ.cmx \ + kernel/entries.cmx kernel/declarations.cmx kernel/cemitcodes.cmx \ + kernel/cbytegen.cmx kernel/modops.cmi kernel/mod_subst.cmo: lib/util.cmi kernel/term.cmi lib/pp.cmi \ kernel/names.cmi kernel/mod_subst.cmi kernel/mod_subst.cmx: lib/util.cmx kernel/term.cmx lib/pp.cmx \ @@ -737,14 +755,6 @@ kernel/mod_typing.cmx: lib/util.cmx kernel/univ.cmx kernel/typeops.cmx \ kernel/names.cmx kernel/modops.cmx kernel/mod_subst.cmx \ kernel/environ.cmx kernel/entries.cmx kernel/declarations.cmx \ kernel/cemitcodes.cmx kernel/cbytegen.cmx kernel/mod_typing.cmi -kernel/modops.cmo: lib/util.cmi kernel/univ.cmi kernel/term.cmi lib/pp.cmi \ - kernel/names.cmi kernel/mod_subst.cmi kernel/environ.cmi \ - kernel/entries.cmi kernel/declarations.cmi kernel/cemitcodes.cmi \ - kernel/cbytegen.cmi kernel/modops.cmi -kernel/modops.cmx: lib/util.cmx kernel/univ.cmx kernel/term.cmx lib/pp.cmx \ - kernel/names.cmx kernel/mod_subst.cmx kernel/environ.cmx \ - kernel/entries.cmx kernel/declarations.cmx kernel/cemitcodes.cmx \ - kernel/cbytegen.cmx kernel/modops.cmi kernel/names.cmo: lib/util.cmi lib/predicate.cmi lib/pp.cmi lib/options.cmi \ lib/hashcons.cmi kernel/names.cmi kernel/names.cmx: lib/util.cmx lib/predicate.cmx lib/pp.cmx lib/options.cmx \ @@ -839,10 +849,10 @@ lib/edit.cmo: lib/util.cmi lib/pp.cmi lib/bstack.cmi lib/edit.cmi lib/edit.cmx: lib/util.cmx lib/pp.cmx lib/bstack.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/util.cmi lib/gmap.cmi lib/gmapl.cmi lib/gmapl.cmx: lib/util.cmx lib/gmap.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 @@ -851,24 +861,14 @@ lib/heap.cmo: lib/heap.cmi lib/heap.cmx: lib/heap.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/util.cmi lib/pp.cmi lib/rtree.cmi -lib/rtree.cmx: lib/util.cmx lib/pp.cmx lib/rtree.cmi -lib/stamps.cmo: lib/stamps.cmi -lib/stamps.cmx: lib/stamps.cmi -lib/system.cmo: lib/util.cmi lib/pp.cmi config/coq_config.cmi lib/system.cmi -lib/system.cmx: lib/util.cmx lib/pp.cmx config/coq_config.cmx lib/system.cmi -lib/tlm.cmo: lib/gset.cmi lib/gmap.cmi lib/tlm.cmi -lib/tlm.cmx: lib/gset.cmx lib/gmap.cmx lib/tlm.cmi -lib/util.cmo: lib/pp.cmi lib/compat.cmo lib/util.cmi -lib/util.cmx: lib/pp.cmx lib/compat.cmx lib/util.cmi library/declare.cmo: lib/util.cmi kernel/univ.cmi kernel/typeops.cmi \ kernel/type_errors.cmi kernel/term.cmi library/summary.cmi \ kernel/sign.cmi kernel/safe_typing.cmi kernel/reduction.cmi lib/pp.cmi \ @@ -983,6 +983,16 @@ library/states.cmx: lib/system.cmx library/summary.cmx library/library.cmx \ library/lib.cmx library/states.cmi library/summary.cmo: lib/util.cmi lib/pp.cmi lib/dyn.cmi library/summary.cmi library/summary.cmx: lib/util.cmx lib/pp.cmx lib/dyn.cmx library/summary.cmi +lib/rtree.cmo: lib/util.cmi lib/pp.cmi lib/rtree.cmi +lib/rtree.cmx: lib/util.cmx lib/pp.cmx lib/rtree.cmi +lib/stamps.cmo: lib/stamps.cmi +lib/stamps.cmx: lib/stamps.cmi +lib/system.cmo: lib/util.cmi lib/pp.cmi config/coq_config.cmi lib/system.cmi +lib/system.cmx: lib/util.cmx lib/pp.cmx config/coq_config.cmx lib/system.cmi +lib/tlm.cmo: lib/gset.cmi lib/gmap.cmi lib/tlm.cmi +lib/tlm.cmx: lib/gset.cmx lib/gmap.cmx lib/tlm.cmi +lib/util.cmo: lib/pp.cmi lib/compat.cmo lib/util.cmi +lib/util.cmx: lib/pp.cmx lib/compat.cmx lib/util.cmi parsing/argextend.cmo: toplevel/vernacexpr.cmo lib/util.cmi \ parsing/q_util.cmi parsing/q_coqast.cmo parsing/pcoq.cmi \ interp/genarg.cmi parsing/ast.cmi @@ -2345,20 +2355,6 @@ toplevel/toplevel.cmx: toplevel/vernacexpr.cmx toplevel/vernac.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: toplevel/vernacinterp.cmi toplevel/vernacexpr.cmo \ - toplevel/vernacentries.cmi lib/util.cmi proofs/tacmach.cmi \ - tactics/tacinterp.cmi lib/system.cmi library/states.cmi \ - proofs/refiner.cmi translate/ppvernacnew.cmi lib/pp.cmi proofs/pfedit.cmi \ - parsing/pcoq.cmi lib/options.cmi kernel/names.cmi library/library.cmi \ - library/lib.cmi parsing/lexer.cmi parsing/coqast.cmi \ - interp/constrintern.cmi interp/constrextern.cmi toplevel/vernac.cmi -toplevel/vernac.cmx: toplevel/vernacinterp.cmx toplevel/vernacexpr.cmx \ - toplevel/vernacentries.cmx lib/util.cmx proofs/tacmach.cmx \ - tactics/tacinterp.cmx lib/system.cmx library/states.cmx \ - proofs/refiner.cmx translate/ppvernacnew.cmx lib/pp.cmx proofs/pfedit.cmx \ - parsing/pcoq.cmx lib/options.cmx kernel/names.cmx library/library.cmx \ - library/lib.cmx parsing/lexer.cmx parsing/coqast.cmx \ - interp/constrintern.cmx interp/constrextern.cmx toplevel/vernac.cmi toplevel/vernacentries.cmo: kernel/vm.cmi toplevel/vernacinterp.cmi \ toplevel/vernacexpr.cmo kernel/vconv.cmi lib/util.cmi kernel/univ.cmi \ kernel/typeops.cmi interp/topconstr.cmi kernel/term.cmi \ @@ -2421,6 +2417,20 @@ toplevel/vernacinterp.cmx: toplevel/vernacexpr.cmx lib/util.cmx \ lib/options.cmx kernel/names.cmx library/libnames.cmx toplevel/himsg.cmx \ parsing/extend.cmx parsing/coqast.cmx parsing/ast.cmx \ toplevel/vernacinterp.cmi +toplevel/vernac.cmo: toplevel/vernacinterp.cmi toplevel/vernacexpr.cmo \ + toplevel/vernacentries.cmi lib/util.cmi proofs/tacmach.cmi \ + tactics/tacinterp.cmi lib/system.cmi library/states.cmi \ + proofs/refiner.cmi translate/ppvernacnew.cmi lib/pp.cmi proofs/pfedit.cmi \ + parsing/pcoq.cmi lib/options.cmi kernel/names.cmi library/library.cmi \ + library/lib.cmi parsing/lexer.cmi parsing/coqast.cmi \ + interp/constrintern.cmi interp/constrextern.cmi toplevel/vernac.cmi +toplevel/vernac.cmx: toplevel/vernacinterp.cmx toplevel/vernacexpr.cmx \ + toplevel/vernacentries.cmx lib/util.cmx proofs/tacmach.cmx \ + tactics/tacinterp.cmx lib/system.cmx library/states.cmx \ + proofs/refiner.cmx translate/ppvernacnew.cmx lib/pp.cmx proofs/pfedit.cmx \ + parsing/pcoq.cmx lib/options.cmx kernel/names.cmx library/library.cmx \ + library/lib.cmx parsing/lexer.cmx parsing/coqast.cmx \ + interp/constrintern.cmx interp/constrextern.cmx toplevel/vernac.cmi toplevel/whelp.cmo: toplevel/vernacinterp.cmi lib/util.cmi kernel/term.cmi \ lib/system.cmi interp/syntax_def.cmi pretyping/rawterm.cmi lib/pp.cmi \ parsing/pcoq.cmi lib/options.cmi library/nametab.cmi kernel/names.cmi \ @@ -2523,6 +2533,12 @@ contrib/cc/cctac.cmx: lib/util.cmx pretyping/termops.cmx kernel/term.cmx \ pretyping/evd.cmx parsing/egrammar.cmx kernel/declarations.cmx \ interp/coqlib.cmx toplevel/cerrors.cmx contrib/cc/ccproof.cmx \ contrib/cc/ccalgo.cmx +contrib/correctness/pcicenv.cmo: kernel/univ.cmi kernel/term.cmi \ + kernel/sign.cmi kernel/names.cmi library/global.cmi \ + contrib/correctness/pcicenv.cmi +contrib/correctness/pcicenv.cmx: kernel/univ.cmx kernel/term.cmx \ + kernel/sign.cmx kernel/names.cmx library/global.cmx \ + contrib/correctness/pcicenv.cmi contrib/correctness/pcic.cmo: toplevel/vernacexpr.cmo lib/util.cmi \ kernel/typeops.cmi interp/topconstr.cmi pretyping/termops.cmi \ kernel/term.cmi kernel/sign.cmi toplevel/record.cmi pretyping/rawterm.cmi \ @@ -2537,12 +2553,6 @@ contrib/correctness/pcic.cmx: toplevel/vernacexpr.cmx lib/util.cmx \ library/libnames.cmx kernel/indtypes.cmx library/global.cmx \ kernel/entries.cmx pretyping/detyping.cmx library/declare.cmx \ kernel/declarations.cmx contrib/correctness/pcic.cmi -contrib/correctness/pcicenv.cmo: kernel/univ.cmi kernel/term.cmi \ - kernel/sign.cmi kernel/names.cmi library/global.cmi \ - contrib/correctness/pcicenv.cmi -contrib/correctness/pcicenv.cmx: kernel/univ.cmx kernel/term.cmx \ - kernel/sign.cmx kernel/names.cmx library/global.cmx \ - contrib/correctness/pcicenv.cmi contrib/correctness/pdb.cmo: pretyping/termops.cmi kernel/term.cmi \ library/nametab.cmi kernel/names.cmi library/global.cmi \ interp/constrintern.cmi contrib/correctness/pdb.cmi @@ -3163,6 +3173,14 @@ contrib/interface/pbp.cmx: lib/util.cmx pretyping/typing.cmx \ proofs/logic.cmx library/libnames.cmx tactics/hipattern.cmx \ library/global.cmx interp/genarg.cmx pretyping/evd.cmx kernel/environ.cmx \ interp/coqlib.cmx contrib/interface/pbp.cmi +contrib/interface/showproof_ct.cmo: contrib/interface/xlate.cmi \ + contrib/interface/vtp.cmi contrib/interface/translate.cmi \ + parsing/printer.cmi lib/pp.cmi toplevel/metasyntax.cmi library/global.cmi \ + parsing/esyntax.cmi contrib/interface/ascent.cmi +contrib/interface/showproof_ct.cmx: contrib/interface/xlate.cmx \ + contrib/interface/vtp.cmx contrib/interface/translate.cmx \ + parsing/printer.cmx lib/pp.cmx toplevel/metasyntax.cmx library/global.cmx \ + parsing/esyntax.cmx contrib/interface/ascent.cmi contrib/interface/showproof.cmo: toplevel/vernacinterp.cmi lib/util.cmi \ pretyping/typing.cmi contrib/interface/translate.cmi \ pretyping/termops.cmi parsing/termast.cmi kernel/term.cmi \ @@ -3187,14 +3205,6 @@ contrib/interface/showproof.cmx: toplevel/vernacinterp.cmx lib/util.cmx \ pretyping/evd.cmx kernel/environ.cmx kernel/declarations.cmx \ parsing/coqast.cmx interp/constrintern.cmx pretyping/clenv.cmx \ contrib/interface/showproof.cmi -contrib/interface/showproof_ct.cmo: contrib/interface/xlate.cmi \ - contrib/interface/vtp.cmi contrib/interface/translate.cmi \ - parsing/printer.cmi lib/pp.cmi toplevel/metasyntax.cmi library/global.cmi \ - parsing/esyntax.cmi contrib/interface/ascent.cmi -contrib/interface/showproof_ct.cmx: contrib/interface/xlate.cmx \ - contrib/interface/vtp.cmx contrib/interface/translate.cmx \ - parsing/printer.cmx lib/pp.cmx toplevel/metasyntax.cmx library/global.cmx \ - parsing/esyntax.cmx contrib/interface/ascent.cmi contrib/interface/translate.cmo: contrib/interface/xlate.cmi \ contrib/interface/vtp.cmi toplevel/vernacinterp.cmi lib/util.cmi \ parsing/termast.cmi kernel/term.cmi proofs/tacmach.cmi kernel/sign.cmi \ @@ -3375,18 +3385,90 @@ contrib/romega/refl_omega.cmx: lib/util.cmx kernel/term.cmx \ parsing/printer.cmx lib/pp.cmx lib/options.cmx contrib/omega/omega.cmx \ kernel/names.cmx proofs/logic.cmx interp/coqlib.cmx \ contrib/romega/const_omega.cmx lib/bigint.cmx -contrib/xml/acic.cmo: kernel/term.cmi kernel/names.cmi -contrib/xml/acic.cmx: kernel/term.cmx kernel/names.cmx +contrib/subtac/infer.cmo: lib/util.cmi toplevel/toplevel.cmi kernel/term.cmi \ + contrib/subtac/scoq.cmo contrib/subtac/sast.cmo pretyping/rawterm.cmi \ + translate/ppconstrnew.cmi lib/pp.cmi contrib/subtac/natural.cmo \ + library/nametab.cmi kernel/names.cmi library/libnames.cmi \ + pretyping/inductiveops.cmi kernel/inductive.cmi library/global.cmi \ + kernel/declarations.cmi contrib/subtac/infer.cmi +contrib/subtac/infer.cmx: lib/util.cmx toplevel/toplevel.cmx kernel/term.cmx \ + contrib/subtac/scoq.cmx contrib/subtac/sast.cmx pretyping/rawterm.cmx \ + translate/ppconstrnew.cmx lib/pp.cmx contrib/subtac/natural.cmx \ + library/nametab.cmx kernel/names.cmx library/libnames.cmx \ + pretyping/inductiveops.cmx kernel/inductive.cmx library/global.cmx \ + kernel/declarations.cmx contrib/subtac/infer.cmi +contrib/subtac/junk.cmo: pretyping/tacred.cmi library/global.cmi \ + pretyping/evd.cmi +contrib/subtac/junk.cmx: pretyping/tacred.cmx library/global.cmx \ + pretyping/evd.cmx +contrib/subtac/rcevm.cmo: kernel/term.cmi pretyping/tacred.cmi \ + library/global.cmi pretyping/evd.cmi +contrib/subtac/rcevm.cmx: kernel/term.cmx pretyping/tacred.cmx \ + library/global.cmx pretyping/evd.cmx +contrib/subtac/rewrite.cmo: lib/util.cmi kernel/univ.cmi pretyping/typing.cmi \ + pretyping/termops.cmi kernel/term.cmi kernel/sign.cmi \ + contrib/subtac/scoq.cmo tactics/refine.cmi kernel/reduction.cmi \ + translate/ppconstrnew.cmi lib/pp.cmi proofs/pfedit.cmi \ + contrib/subtac/natural.cmo kernel/names.cmi library/libnames.cmi \ + contrib/subtac/infer.cmi pretyping/inductiveops.cmi kernel/inductive.cmi \ + library/global.cmi pretyping/evd.cmi kernel/environ.cmi \ + kernel/declarations.cmi library/decl_kinds.cmo interp/coqlib.cmi \ + toplevel/command.cmi contrib/subtac/rewrite.cmi +contrib/subtac/rewrite.cmx: lib/util.cmx kernel/univ.cmx pretyping/typing.cmx \ + pretyping/termops.cmx kernel/term.cmx kernel/sign.cmx \ + contrib/subtac/scoq.cmx tactics/refine.cmx kernel/reduction.cmx \ + translate/ppconstrnew.cmx lib/pp.cmx proofs/pfedit.cmx \ + contrib/subtac/natural.cmx kernel/names.cmx library/libnames.cmx \ + contrib/subtac/infer.cmx pretyping/inductiveops.cmx kernel/inductive.cmx \ + library/global.cmx pretyping/evd.cmx kernel/environ.cmx \ + kernel/declarations.cmx library/decl_kinds.cmx interp/coqlib.cmx \ + toplevel/command.cmx contrib/subtac/rewrite.cmi +contrib/subtac/sast.cmo: lib/util.cmi kernel/names.cmi +contrib/subtac/sast.cmx: lib/util.cmx kernel/names.cmx +contrib/subtac/scoq.cmo: kernel/term.cmi lib/pp.cmi \ + contrib/subtac/natural.cmo kernel/names.cmi library/libnames.cmi \ + library/global.cmi pretyping/evd.cmi interp/coqlib.cmi \ + interp/constrextern.cmi +contrib/subtac/scoq.cmx: kernel/term.cmx lib/pp.cmx \ + contrib/subtac/natural.cmx kernel/names.cmx library/libnames.cmx \ + library/global.cmx pretyping/evd.cmx interp/coqlib.cmx \ + interp/constrextern.cmx +contrib/subtac/sparser.cmo: toplevel/vernacinterp.cmi \ + toplevel/vernacentries.cmi lib/util.cmi interp/topconstr.cmi \ + kernel/term.cmi proofs/tacexpr.cmo contrib/subtac/sast.cmo \ + contrib/subtac/rewrite.cmi kernel/reduction.cmi lib/pp.cmi \ + parsing/pcoq.cmi lib/options.cmi kernel/names.cmi library/nameops.cmi \ + library/libnames.cmi interp/genarg.cmi parsing/egrammar.cmi \ + parsing/coqast.cmi toplevel/cerrors.cmi +contrib/subtac/sparser.cmx: toplevel/vernacinterp.cmx \ + toplevel/vernacentries.cmx lib/util.cmx interp/topconstr.cmx \ + kernel/term.cmx proofs/tacexpr.cmx contrib/subtac/sast.cmx \ + contrib/subtac/rewrite.cmx kernel/reduction.cmx lib/pp.cmx \ + parsing/pcoq.cmx lib/options.cmx kernel/names.cmx library/nameops.cmx \ + library/libnames.cmx interp/genarg.cmx parsing/egrammar.cmx \ + parsing/coqast.cmx toplevel/cerrors.cmx +contrib/subtac/top_printer.cmo: lib/util.cmi kernel/univ.cmi \ + pretyping/termops.cmi kernel/term.cmi parsing/tactic_printer.cmi \ + lib/system.cmi kernel/sign.cmi proofs/refiner.cmi proofs/proof_trees.cmi \ + parsing/printer.cmi parsing/pptactic.cmi lib/pp.cmi kernel/names.cmi \ + library/nameops.cmi library/libobject.cmi library/libnames.cmi \ + pretyping/evd.cmi kernel/environ.cmi kernel/declarations.cmi \ + interp/constrextern.cmi kernel/closure.cmi pretyping/clenv.cmi \ + toplevel/cerrors.cmi lib/bigint.cmi parsing/ast.cmi +contrib/subtac/top_printer.cmx: lib/util.cmx kernel/univ.cmx \ + pretyping/termops.cmx kernel/term.cmx parsing/tactic_printer.cmx \ + lib/system.cmx kernel/sign.cmx proofs/refiner.cmx proofs/proof_trees.cmx \ + parsing/printer.cmx parsing/pptactic.cmx lib/pp.cmx kernel/names.cmx \ + library/nameops.cmx library/libobject.cmx library/libnames.cmx \ + pretyping/evd.cmx kernel/environ.cmx kernel/declarations.cmx \ + interp/constrextern.cmx kernel/closure.cmx pretyping/clenv.cmx \ + toplevel/cerrors.cmx lib/bigint.cmx parsing/ast.cmx contrib/xml/acic2Xml.cmo: contrib/xml/xml.cmi lib/util.cmi kernel/term.cmi \ kernel/names.cmi contrib/xml/cic2acic.cmo contrib/xml/acic.cmo contrib/xml/acic2Xml.cmx: contrib/xml/xml.cmx lib/util.cmx kernel/term.cmx \ kernel/names.cmx contrib/xml/cic2acic.cmx contrib/xml/acic.cmx -contrib/xml/cic2Xml.cmo: contrib/xml/xml.cmi contrib/xml/unshare.cmi \ - tactics/tacinterp.cmi contrib/xml/cic2acic.cmo contrib/xml/acic2Xml.cmo \ - contrib/xml/acic.cmo -contrib/xml/cic2Xml.cmx: contrib/xml/xml.cmx contrib/xml/unshare.cmx \ - tactics/tacinterp.cmx contrib/xml/cic2acic.cmx contrib/xml/acic2Xml.cmx \ - contrib/xml/acic.cmx +contrib/xml/acic.cmo: kernel/term.cmi kernel/names.cmi +contrib/xml/acic.cmx: kernel/term.cmx kernel/names.cmx contrib/xml/cic2acic.cmo: lib/util.cmi contrib/xml/unshare.cmi \ kernel/univ.cmi pretyping/termops.cmi kernel/term.cmi \ pretyping/reductionops.cmi parsing/printer.cmi lib/pp.cmi \ @@ -3405,6 +3487,12 @@ contrib/xml/cic2acic.cmx: lib/util.cmx contrib/xml/unshare.cmx \ kernel/environ.cmx contrib/xml/doubleTypeInference.cmx \ library/dischargedhypsmap.cmx library/declare.cmx kernel/declarations.cmx \ contrib/xml/acic.cmx +contrib/xml/cic2Xml.cmo: contrib/xml/xml.cmi contrib/xml/unshare.cmi \ + tactics/tacinterp.cmi contrib/xml/cic2acic.cmo contrib/xml/acic2Xml.cmo \ + contrib/xml/acic.cmo +contrib/xml/cic2Xml.cmx: contrib/xml/xml.cmx contrib/xml/unshare.cmx \ + tactics/tacinterp.cmx contrib/xml/cic2acic.cmx contrib/xml/acic2Xml.cmx \ + contrib/xml/acic.cmx contrib/xml/doubleTypeInference.cmo: lib/util.cmi contrib/xml/unshare.cmi \ kernel/typeops.cmi pretyping/termops.cmi kernel/term.cmi \ pretyping/retyping.cmi pretyping/reductionops.cmi kernel/reduction.cmi \ @@ -3447,8 +3535,6 @@ contrib/xml/proofTree2Xml.cmx: contrib/xml/xml.cmx lib/util.cmx \ contrib/xml/cic2acic.cmx contrib/xml/acic2Xml.cmx contrib/xml/acic.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/xml.cmi toplevel/vernac.cmi \ lib/util.cmi contrib/xml/unshare.cmi kernel/term.cmi proofs/tacmach.cmi \ kernel/sign.cmi pretyping/recordops.cmi proofs/proof_trees.cmi \ @@ -3479,10 +3565,8 @@ contrib/xml/xmlentries.cmx: contrib/xml/xmlcommand.cmx \ toplevel/vernacinterp.cmx lib/util.cmx lib/pp.cmx parsing/pcoq.cmx \ interp/genarg.cmx parsing/extend.cmx parsing/egrammar.cmx \ toplevel/cerrors.cmx -ide/utils/configwin.cmo: ide/utils/configwin_types.cmo \ - ide/utils/configwin_ihm.cmo ide/utils/configwin.cmi -ide/utils/configwin.cmx: ide/utils/configwin_types.cmx \ - ide/utils/configwin_ihm.cmx ide/utils/configwin.cmi +contrib/xml/xml.cmo: contrib/xml/xml.cmi +contrib/xml/xml.cmx: contrib/xml/xml.cmi ide/utils/configwin_html_config.cmo: ide/utils/uoptions.cmi \ ide/utils/configwin_types.cmo ide/utils/configwin_messages.cmo \ ide/utils/configwin_ihm.cmo @@ -3493,6 +3577,10 @@ ide/utils/configwin_ihm.cmo: ide/utils/uoptions.cmi ide/utils/okey.cmi \ ide/utils/configwin_types.cmo ide/utils/configwin_messages.cmo ide/utils/configwin_ihm.cmx: ide/utils/uoptions.cmx ide/utils/okey.cmx \ ide/utils/configwin_types.cmx ide/utils/configwin_messages.cmx +ide/utils/configwin.cmo: ide/utils/configwin_types.cmo \ + ide/utils/configwin_ihm.cmo ide/utils/configwin.cmi +ide/utils/configwin.cmx: ide/utils/configwin_types.cmx \ + ide/utils/configwin_ihm.cmx ide/utils/configwin.cmi ide/utils/configwin_types.cmo: ide/utils/uoptions.cmi \ ide/utils/configwin_keys.cmo ide/utils/configwin_types.cmx: ide/utils/uoptions.cmx \ @@ -3553,6 +3641,8 @@ contrib/funind/tacinv.cmo: parsing/grammar.cma contrib/funind/tacinv.cmx: parsing/grammar.cma contrib/first-order/g_ground.cmo: parsing/grammar.cma contrib/first-order/g_ground.cmx: parsing/grammar.cma +contrib/subtac/sparser.cmo: parsing/grammar.cma +contrib/subtac/sparser.cmx: parsing/grammar.cma contrib/interface/debug_tac.cmo: parsing/grammar.cma contrib/interface/debug_tac.cmx: parsing/grammar.cma contrib/interface/centaur.cmo: parsing/grammar.cma @@ -3624,72 +3714,50 @@ tools/coq_makefile.cmx: tools/coq-tex.cmo: tools/coq-tex.cmx: coq_fix_code.o: kernel/byterun/coq_fix_code.c \ - /home/logical/local/lib/ocaml/caml/config.h \ - /home/logical/local/lib/ocaml/caml/compatibility.h \ - /home/logical/local/lib/ocaml/caml/misc.h \ - /home/logical/local/lib/ocaml/caml/mlvalues.h \ - /home/logical/local/lib/ocaml/caml/fail.h \ - /home/logical/local/lib/ocaml/caml/memory.h \ + /usr/lib/ocaml/caml/config.h /usr/lib/ocaml/caml/compatibility.h \ + /usr/lib/ocaml/caml/misc.h /usr/lib/ocaml/caml/mlvalues.h \ + /usr/lib/ocaml/caml/fail.h /usr/lib/ocaml/caml/memory.h \ kernel/byterun/coq_instruct.h kernel/byterun/coq_fix_code.h coq_interp.o: kernel/byterun/coq_interp.c kernel/byterun/coq_gc.h \ - /home/logical/local/lib/ocaml/caml/mlvalues.h \ - /home/logical/local/lib/ocaml/caml/compatibility.h \ - /home/logical/local/lib/ocaml/caml/config.h \ - /home/logical/local/lib/ocaml/caml/misc.h \ - /home/logical/local/lib/ocaml/caml/alloc.h \ - kernel/byterun/coq_instruct.h kernel/byterun/coq_fix_code.h \ - kernel/byterun/coq_memory.h /home/logical/local/lib/ocaml/caml/fail.h \ - /home/logical/local/lib/ocaml/caml/memory.h kernel/byterun/coq_values.h \ - kernel/byterun/coq_jumptbl.h + /usr/lib/ocaml/caml/mlvalues.h /usr/lib/ocaml/caml/compatibility.h \ + /usr/lib/ocaml/caml/config.h /usr/lib/ocaml/caml/misc.h \ + /usr/lib/ocaml/caml/alloc.h kernel/byterun/coq_instruct.h \ + kernel/byterun/coq_fix_code.h kernel/byterun/coq_memory.h \ + /usr/lib/ocaml/caml/fail.h /usr/lib/ocaml/caml/memory.h \ + kernel/byterun/coq_values.h kernel/byterun/coq_jumptbl.h coq_memory.o: kernel/byterun/coq_memory.c kernel/byterun/coq_gc.h \ - /home/logical/local/lib/ocaml/caml/mlvalues.h \ - /home/logical/local/lib/ocaml/caml/compatibility.h \ - /home/logical/local/lib/ocaml/caml/config.h \ - /home/logical/local/lib/ocaml/caml/misc.h \ - /home/logical/local/lib/ocaml/caml/alloc.h \ - kernel/byterun/coq_instruct.h kernel/byterun/coq_fix_code.h \ - kernel/byterun/coq_memory.h /home/logical/local/lib/ocaml/caml/fail.h \ - /home/logical/local/lib/ocaml/caml/memory.h + /usr/lib/ocaml/caml/mlvalues.h /usr/lib/ocaml/caml/compatibility.h \ + /usr/lib/ocaml/caml/config.h /usr/lib/ocaml/caml/misc.h \ + /usr/lib/ocaml/caml/alloc.h kernel/byterun/coq_instruct.h \ + kernel/byterun/coq_fix_code.h kernel/byterun/coq_memory.h \ + /usr/lib/ocaml/caml/fail.h /usr/lib/ocaml/caml/memory.h coq_values.o: kernel/byterun/coq_values.c kernel/byterun/coq_fix_code.h \ - /home/logical/local/lib/ocaml/caml/mlvalues.h \ - /home/logical/local/lib/ocaml/caml/compatibility.h \ - /home/logical/local/lib/ocaml/caml/config.h \ - /home/logical/local/lib/ocaml/caml/misc.h kernel/byterun/coq_instruct.h \ - kernel/byterun/coq_memory.h /home/logical/local/lib/ocaml/caml/fail.h \ - /home/logical/local/lib/ocaml/caml/memory.h kernel/byterun/coq_values.h \ - /home/logical/local/lib/ocaml/caml/alloc.h + /usr/lib/ocaml/caml/mlvalues.h /usr/lib/ocaml/caml/compatibility.h \ + /usr/lib/ocaml/caml/config.h /usr/lib/ocaml/caml/misc.h \ + kernel/byterun/coq_instruct.h kernel/byterun/coq_memory.h \ + /usr/lib/ocaml/caml/fail.h /usr/lib/ocaml/caml/memory.h \ + kernel/byterun/coq_values.h /usr/lib/ocaml/caml/alloc.h coq_fix_code.d.o: kernel/byterun/coq_fix_code.c \ - /home/logical/local/lib/ocaml/caml/config.h \ - /home/logical/local/lib/ocaml/caml/compatibility.h \ - /home/logical/local/lib/ocaml/caml/misc.h \ - /home/logical/local/lib/ocaml/caml/mlvalues.h \ - /home/logical/local/lib/ocaml/caml/fail.h \ - /home/logical/local/lib/ocaml/caml/memory.h \ + /usr/lib/ocaml/caml/config.h /usr/lib/ocaml/caml/compatibility.h \ + /usr/lib/ocaml/caml/misc.h /usr/lib/ocaml/caml/mlvalues.h \ + /usr/lib/ocaml/caml/fail.h /usr/lib/ocaml/caml/memory.h \ kernel/byterun/coq_instruct.h kernel/byterun/coq_fix_code.h coq_interp.d.o: kernel/byterun/coq_interp.c kernel/byterun/coq_gc.h \ - /home/logical/local/lib/ocaml/caml/mlvalues.h \ - /home/logical/local/lib/ocaml/caml/compatibility.h \ - /home/logical/local/lib/ocaml/caml/config.h \ - /home/logical/local/lib/ocaml/caml/misc.h \ - /home/logical/local/lib/ocaml/caml/alloc.h \ - kernel/byterun/coq_instruct.h kernel/byterun/coq_fix_code.h \ - kernel/byterun/coq_memory.h /home/logical/local/lib/ocaml/caml/fail.h \ - /home/logical/local/lib/ocaml/caml/memory.h kernel/byterun/coq_values.h \ - kernel/byterun/coq_jumptbl.h + /usr/lib/ocaml/caml/mlvalues.h /usr/lib/ocaml/caml/compatibility.h \ + /usr/lib/ocaml/caml/config.h /usr/lib/ocaml/caml/misc.h \ + /usr/lib/ocaml/caml/alloc.h kernel/byterun/coq_instruct.h \ + kernel/byterun/coq_fix_code.h kernel/byterun/coq_memory.h \ + /usr/lib/ocaml/caml/fail.h /usr/lib/ocaml/caml/memory.h \ + kernel/byterun/coq_values.h kernel/byterun/coq_jumptbl.h coq_memory.d.o: kernel/byterun/coq_memory.c kernel/byterun/coq_gc.h \ - /home/logical/local/lib/ocaml/caml/mlvalues.h \ - /home/logical/local/lib/ocaml/caml/compatibility.h \ - /home/logical/local/lib/ocaml/caml/config.h \ - /home/logical/local/lib/ocaml/caml/misc.h \ - /home/logical/local/lib/ocaml/caml/alloc.h \ - kernel/byterun/coq_instruct.h kernel/byterun/coq_fix_code.h \ - kernel/byterun/coq_memory.h /home/logical/local/lib/ocaml/caml/fail.h \ - /home/logical/local/lib/ocaml/caml/memory.h + /usr/lib/ocaml/caml/mlvalues.h /usr/lib/ocaml/caml/compatibility.h \ + /usr/lib/ocaml/caml/config.h /usr/lib/ocaml/caml/misc.h \ + /usr/lib/ocaml/caml/alloc.h kernel/byterun/coq_instruct.h \ + kernel/byterun/coq_fix_code.h kernel/byterun/coq_memory.h \ + /usr/lib/ocaml/caml/fail.h /usr/lib/ocaml/caml/memory.h coq_values.d.o: kernel/byterun/coq_values.c kernel/byterun/coq_fix_code.h \ - /home/logical/local/lib/ocaml/caml/mlvalues.h \ - /home/logical/local/lib/ocaml/caml/compatibility.h \ - /home/logical/local/lib/ocaml/caml/config.h \ - /home/logical/local/lib/ocaml/caml/misc.h kernel/byterun/coq_instruct.h \ - kernel/byterun/coq_memory.h /home/logical/local/lib/ocaml/caml/fail.h \ - /home/logical/local/lib/ocaml/caml/memory.h kernel/byterun/coq_values.h \ - /home/logical/local/lib/ocaml/caml/alloc.h + /usr/lib/ocaml/caml/mlvalues.h /usr/lib/ocaml/caml/compatibility.h \ + /usr/lib/ocaml/caml/config.h /usr/lib/ocaml/caml/misc.h \ + kernel/byterun/coq_instruct.h kernel/byterun/coq_memory.h \ + /usr/lib/ocaml/caml/fail.h /usr/lib/ocaml/caml/memory.h \ + kernel/byterun/coq_values.h /usr/lib/ocaml/caml/alloc.h diff --git a/.depend.camlp4 b/.depend.camlp4 index b29845a64..1a74b42a2 100644 --- a/.depend.camlp4 +++ b/.depend.camlp4 @@ -17,6 +17,7 @@ contrib/jprover/jprover.ml: parsing/grammar.cma contrib/cc/cctac.ml: parsing/grammar.cma contrib/funind/tacinv.ml: parsing/grammar.cma contrib/first-order/g_ground.ml: parsing/grammar.cma +contrib/subtac/sparser.ml: parsing/grammar.cma contrib/interface/debug_tac.ml: parsing/grammar.cma contrib/interface/centaur.ml: parsing/grammar.cma parsing/lexer.ml: @@ -73,7 +73,7 @@ LOCALINCLUDES=-I config -I tools -I tools/coqdoc \ -I contrib/interface -I contrib/fourier \ -I contrib/jprover -I contrib/cc \ -I contrib/funind -I contrib/first-order \ - -I contrib/field + -I contrib/field -I contrib/subtac MLINCLUDES=$(LOCALINCLUDES) -I $(MYCAMLP4LIB) @@ -293,12 +293,22 @@ FOCMO=\ CCCMO=contrib/cc/ccalgo.cmo contrib/cc/ccproof.cmo contrib/cc/cctac.cmo +SUBTACCMO=\ + contrib/subtac/natural.cmo \ + contrib/subtac/scoq.cmo \ + contrib/subtac/sast.cmo \ + contrib/subtac/infer.cmo \ + contrib/subtac/top_printer.cmo \ + contrib/subtac/rewrite.cmo \ + contrib/subtac/sparser.cmo + ML4FILES += contrib/jprover/jprover.ml4 contrib/cc/cctac.ml4 \ - contrib/funind/tacinv.ml4 contrib/first-order/g_ground.ml4 + contrib/funind/tacinv.ml4 contrib/first-order/g_ground.ml4 \ + contrib/subtac/sparser.ml4 CONTRIB=$(OMEGACMO) $(ROMEGACMO) $(RINGCMO) $(DPCMO) $(FIELDCMO) \ $(FOURIERCMO) $(EXTRACTIONCMO) $(JPROVERCMO) $(XMLCMO) \ - $(CCCMO) $(FUNINDCMO) $(FOCMO) + $(CCCMO) $(FUNINDCMO) $(FOCMO) $(SUBTACCMO) CMA=$(CLIBS) $(CAMLP4OBJS) CMXA=$(CMA:.cma=.cmxa) @@ -992,8 +1002,10 @@ JPROVERVO= CCVO=\ contrib/cc/CCSolve.vo +SUBTACVO= + CONTRIBVO = $(OMEGAVO) $(ROMEGAVO) $(RINGVO) $(FIELDVO) $(XMLVO) \ - $(FOURIERVO) $(JPROVERVO) $(CCVO) $(FUNINDVO) + $(FOURIERVO) $(JPROVERVO) $(CCVO) $(FUNINDVO) $(SUBTACVO) $(CONTRIBVO): states/initial.coq @@ -1008,6 +1020,7 @@ fourier: $(FOURIERVO) $(FOURIERCMO) jprover: $(JPROVERVO) $(JPROVERCMO) funind: $(FUNINDCMO) $(FUNINDVO) cc: $(CCVO) $(CCCMO) +subtac: $(SUBTACVO) $(SUBTACCMO) NEWINITVO=$(INITVO) NEWTHEORIESVO=$(THEORIESVO) diff --git a/contrib/subtac/infer.ml b/contrib/subtac/infer.ml new file mode 100644 index 000000000..dcca9361a --- /dev/null +++ b/contrib/subtac/infer.ml @@ -0,0 +1,827 @@ +open Natural +open Names +open Term +open Rawterm +open Util +open Sast +open Scoq +open Pp +open Ppconstrnew + +let ($) f g = fun x -> f (g x) + +let app_option f default = function Some x -> f x | None -> default + +let concat_map f l = + let rec aux accu = function + [] -> List.rev accu + | hd :: tl -> + aux (f hd @ accu) tl + in aux [] l + +let unique l = + let l' = List.sort Pervasives.compare l in + let rec aux accu = function + [] -> List.rev accu + | x :: (y :: _) as tl when x = y -> + aux accu tl + | hd :: tl -> + aux (hd :: accu) tl + in aux [] l' + +type term_pp = Pp.std_ppcmds + +type subtyping_error = + | UncoercibleInferType of loc * term_pp * term_pp + | UncoercibleInferTerm of loc * term_pp * term_pp * term_pp * term_pp + | UncoercibleRewrite of term_pp * term_pp + +type typing_error = + | NonFunctionalApp of loc * term_pp * term_pp + | NonConvertible of loc * term_pp * term_pp + | NonSigma of loc * term_pp + +exception Subtyping_error of subtyping_error +exception Typing_error of typing_error + +exception Debug_msg of string + +let typing_error e = raise (Typing_error e) +let subtyping_error e = raise (Subtyping_error e) + +type sort = Term.sorts +type sort_loc = sort located + +(* Decorated terms *) +type dterm = + DRel of nat + | DLambda of (name located * dtype_loc) * dterm_loc * dtype_loc + | DApp of dterm_loc * dterm_loc * dtype_loc + | DLetIn of (name located) * dterm_loc * dterm_loc * dtype_loc + | DLetTuple of (name located * dtype_loc * dtype_loc) list * dterm_loc * dterm_loc * dtype_loc + | DIfThenElse of dterm_loc * dterm_loc * dterm_loc * dtype_loc + | DSum of ((name located) * dterm_loc) * (dterm_loc * dtype_loc) * dtype_loc + | DCoq of constr * dtype_loc +and dterm_loc = dterm located +and dtype = + | DTApp of dtype_loc * dtype_loc * dtype_loc * sort_loc + | DTPi of (name located * dtype_loc) * dtype_loc * sort_loc + | DTSigma of (name located * dtype_loc) * dtype_loc * sort_loc + | DTSubset of (identifier located * dtype_loc) * dtype_loc * sort_loc + | DTRel of nat + | DTTerm of dterm_loc * dtype_loc * sort_loc + | DTSort of sort_loc + | DTInd of (identifier located) * dtype_loc * inductive * sort_loc + | DTCoq of types * dtype_loc * sort_loc +and dtype_loc = dtype located + +let print_name = function + Name s -> str (string_of_id s) + | Anonymous -> str "_" + +let print_name_loc (_, n) = print_name n + +let string_of_list l = + let rec aux = function + hd :: ((_ :: _) as tl) -> + hd ++ str "," ++ aux tl + | hd :: [] -> hd + | [] -> mt() + in aux l + +type context = (name * dtype_loc) list + +let print_dtype_locref : (context -> dtype_loc -> std_ppcmds) ref = + ref (fun ctx t -> mt()) + +let print_context ctx = + let cmds, _ = + List.fold_right + (fun (x, t) (acc, ctx) -> + let xpr = print_name x ++ str " : " ++ !print_dtype_locref ctx t in + (xpr :: acc), ((x, t) :: ctx)) + ctx ([], []) + in string_of_list cmds + +let type_of_rel ctx n = + try snd (List.nth ctx n) + with e -> + debug 3 (str "Error in type_of_rel, searching for index " ++ str (string_of_int n) + ++ str " in context " ++ print_context ctx ++ str ": " ++ + str (Printexc.to_string e)); + raise e + +let name_of_rel ctx n = + try fst (List.nth ctx n) + with e -> + debug 3 (str "Error in name_of_rel, searching for index " ++ str (string_of_int n) + ++ str " in context " ++ print_context ctx ++ str ": " ++ + str (Printexc.to_string e)); + raise e + +let rec sort_of_dtype ctx = function + | DTApp (_, _, _, x) + | DTPi (_, _, x) + | DTSigma (_, _, x) + | DTSubset (_, _, x) + | DTTerm (_, _, x) + | DTSort x + | DTInd (_, _, _, x) + | DTCoq (_, _, x) -> x + | DTRel i -> sort_of_dtype_loc ctx (type_of_rel ctx i) + +and sort_of_dtype_loc ctx (_, t) = sort_of_dtype ctx t + +let rec no_var n (loc, t) = + match t with + | DTApp (x, y, t, _) -> (no_var n x) && (no_var n y) + | DTPi ((_, x), y, _) -> (no_var n x) && (no_var (succ n) y) + | DTSigma ((_, x), y, _) -> (no_var n x) && (no_var (succ n) y) + | DTSubset ((_, x), y, _) -> (no_var n x) && (no_var (succ n) y) + | DTRel i when i <> n -> false + | x -> true + + +let rec lift_rec n k (loc, t) = + let t' = + match t with + | DTApp (x, y, t, s) -> DTApp (lift_rec n k x, lift_rec n k y, + lift_rec n k t, s) + | DTPi ((id, x), y, s) -> + DTPi ((id, lift_rec n k x), lift_rec n (succ k) y, s) + | DTSigma ((id, x), y, s) -> + DTSigma ((id, lift_rec n k x), lift_rec n (succ k) y, s) + | DTSubset ((id, x), y, s) -> + DTSubset ((id, lift_rec n k x), lift_rec n (succ k) y, s) + | (DTRel i) as x -> + if i < k then x else DTRel (n + i) + | DTTerm (t, tt, s) -> DTTerm (lift_term_rec n k t, lift_rec n k tt, s) + | DTCoq (c, t, s) -> DTCoq (Term.liftn n k c, lift_rec n k t, s) + | DTSort _ + | DTInd _ -> t + in loc, t' + +and lift_term_rec n k (loc, s) = + let s' = + match s with + DRel i -> + if i < k then s else DRel (n + i) + | DLambda ((nl, dt), dt', dtlam) -> + DLambda ((nl, lift_rec n k dt), lift_term_rec n (succ k) dt', + lift_rec n k dtlam) + | DApp (dte, dte', dt) -> + DApp (lift_term_rec n k dte, lift_term_rec n k dte', lift_rec n k dt) + | DLetIn (nl, dte, dte', dt) -> + DLetIn (nl, lift_term_rec n k dte, lift_term_rec n (succ k) dte', + lift_rec n k dt) + | DLetTuple (nl, dte, dte', dt) -> + DLetTuple (nl, lift_term_rec n k dte, + lift_term_rec n (List.length nl + k) dte', + lift_rec n k dt) + | DIfThenElse (db, de, de', dt) -> + DIfThenElse (lift_term_rec n k db, lift_term_rec n k de, + lift_term_rec n k de', lift_rec n k dt) + | DSum ((x, tx), (ty, dty), dt) -> + DSum ((x, lift_term_rec n k tx), + (lift_term_rec n (succ k) ty, lift_rec n (succ k) dty), + lift_rec n k dt) + | DCoq (c, t) -> DCoq (Term.liftn n k c, lift_rec n k t) + in loc, s' + +let lift n t = lift_rec n 0 t +let lift_term n t = lift_term_rec n 0 t + +let rec unlift_rec n k (loc, t) = + let t' = + match t with + | DTApp (x, y, t, s) -> DTApp (unlift_rec n k x, unlift_rec n k y, unlift_rec n k t, s) + | DTPi ((id, x), y, s) -> + DTPi ((id, unlift_rec n k x), unlift_rec n (succ k) y, s) + | DTSigma ((id, x), y, s) -> + DTSigma ((id, unlift_rec n k x), unlift_rec n (succ k) y, s) + | DTSubset ((id, x), y, s) -> + DTSubset ((id, unlift_rec n k x), unlift_rec n (succ k) y, s) + | (DTRel i) as x -> + if i < k then x else DTRel (i - n) + | DTTerm (t, tt, s) -> DTTerm (unlift_term_rec n k t, unlift_rec n k tt, s) + | DTCoq (c, t, s) -> DTCoq (c, unlift_rec n k t, s) + | DTSort _ + | DTInd _ -> t + in loc, t' + +and unlift_term_rec n k (loc, s) = + let s' = + match s with + DRel i -> + if i < k then s else DRel (i - n) + | DLambda ((nl, dt), dt', dtlam) -> + DLambda ((nl, unlift_rec n k dt), unlift_term_rec n (succ k) dt', + unlift_rec n k dtlam) + | DApp (dte, dte', dt) -> + DApp (unlift_term_rec n k dte, unlift_term_rec n k dte', unlift_rec n k dt) + | DLetIn (nl, dte, dte', dt) -> + DLetIn (nl, unlift_term_rec n k dte, unlift_term_rec n (succ k) dte', + unlift_rec n k dt) + | DLetTuple (nl, dte, dte', dt) -> + DLetTuple (nl, unlift_term_rec n k dte, + unlift_term_rec n (List.length nl + k) dte', + unlift_rec n k dt) + | DIfThenElse (db, de, de', dt) -> + DIfThenElse (unlift_term_rec n k db, unlift_term_rec n k de, + unlift_term_rec n k de', unlift_rec n k dt) + | DSum ((x, tx), (ty, dty), dt) -> + DSum ((x, unlift_term_rec n k tx), + (unlift_term_rec n k ty, unlift_rec n k dty), + unlift_rec n k dt) + | DCoq (c, t) -> DCoq (c, unlift_rec n k t) + in loc, s' + +let unlift n t = unlift_rec n 0 t + +let rec type_of_dterm ctx t = + match t with + DRel (i) -> + (try let t = type_of_rel ctx i in lift (succ i) t + with e -> debug 3 (str "Couldn't find type of rel in type_of_dterm"); + raise e) + | DLambda (_, _, dt) -> dt + | DApp (dte, dte', dt) -> dt + | DLetIn (nl, dte, dte', dt) -> dt + | DLetTuple (nl, dte, dte', dt) -> dt + | DIfThenElse (db, de, de', dt) -> dt + | DSum (_, _, dt) -> dt + | DCoq (_, dt) -> dt + +let type_of_dterm_loc ctx (_, t) = type_of_dterm ctx t + +let rec subst_term_type_rec (loc, s) t k = + let s' = + match s with + DRel i -> + if k < i then DRel (pred i) + else if k = i then + match snd (lift_rec k 0 t) with + DTRel i -> DRel i + | DTTerm (t, _, _) -> snd t + | _ -> failwith ("Substitution of a type in a term") + else (* k > i *) s + | DLambda ((ln, dt), e, t') -> + DLambda ((ln, subst_rec dt t k), subst_term_type_rec e t (succ k), + subst_rec t' t k) + | DApp (x, y, ta) -> + DApp (subst_term_type_rec x t k, subst_term_type_rec y t k, subst_rec ta t k) + | DLetIn (nl, e, e', t') -> + DLetIn (nl, subst_term_type_rec e t k, subst_term_type_rec e' t (succ k), + subst_rec t' t k) + | DLetTuple (nl, e, e', t') -> + DLetTuple (nl, subst_term_type_rec e t k, subst_term_type_rec e' t (k + List.length nl), + subst_rec t' t k) + | DIfThenElse (b, e, e', t') -> + DIfThenElse (subst_term_type_rec b t k, subst_term_type_rec e t k, + subst_term_type_rec e' t k, subst_rec t' t k) + | DSum ((nl, dt), (dt', tt'), t') -> + DSum ((nl, subst_term_type_rec dt t k), + (subst_term_type_rec dt' t (succ k), subst_rec tt' t (succ k)), + subst_rec t' t k) + | DCoq (c, dt) -> DCoq (c, subst_rec dt t k) + in loc, s' + +and subst_term_rec (loc, s) t k = + let ttype = + let dtype = type_of_dterm [] (snd t) in + (dummy_loc, (DTTerm (t, dtype, sort_of_dtype_loc [] dtype))) + in + let s' = + match s with + DRel i -> + if k < i then DRel (pred i) + else if k = i then snd (lift_term_rec k 0 t) + else (* k > i *) s + | DLambda ((ln, dt), e, t') -> + (* !!! *) + DLambda ((ln, subst_rec dt ttype k), + subst_term_rec e t (succ k), subst_rec t' ttype k) + | DApp (x, y, ta) -> + DApp (subst_term_rec x t k, subst_term_rec y t k, subst_rec ta ttype k) + | DLetIn (nl, e, e', t') -> + DLetIn (nl, subst_term_rec e t k, subst_term_rec e' t (succ k), + subst_rec t' ttype k) + | DLetTuple (nl, e, e', t') -> + DLetTuple (nl, subst_term_rec e t k, subst_term_rec e' t + (k + List.length nl), + subst_rec t' ttype k) + | DIfThenElse (b, e, e', t') -> + DIfThenElse (subst_term_rec b t k, subst_term_rec e t k, + subst_term_rec e' t k, subst_rec t' ttype k) + | DSum ((nl, dt), (dt', tt'), t') -> + DSum ((nl, subst_term_rec dt t k), + (subst_term_rec dt' t (succ k), subst_rec tt' tt' (succ k)), + subst_rec t' ttype k) + | DCoq (c, dt) -> + + DCoq (c, subst_rec dt ttype k) + in loc, s' + +and subst_rec (loc, s) (t : dtype_loc) k = + let s' = + match s with + DTPi ((id, a), b, s) -> DTPi ((id, subst_rec a t k), + subst_rec b t (succ k), s) + | DTSigma ((id, a), b, s) -> DTSigma ((id, subst_rec a t k), + subst_rec b t (succ k), s) + | DTSubset ((id, a), b, s) -> DTSubset ((id, subst_rec a t k), + subst_rec b t (succ k), s) + | DTRel i -> + if k < i then DTRel (pred i) + else if k = i then snd (lift k t) + else (* k > i *) s + | DTApp (x, y, t', s) -> DTApp (subst_rec x t k, subst_rec y t k, + subst_rec t' t k, s) + | DTTerm (x, tt, s) -> DTTerm (subst_term_type_rec x t k, subst_rec tt t k, s) + | DTCoq (c, ct, s) -> DTCoq (c, subst_rec ct t k, s) + | DTSort _ | DTInd _ -> s + in loc, s' + +let subst s t = subst_rec s t 0 +let subst_term s t = subst_term_rec s t 0 + +let rec print_dterm' ctx = function + | DRel n -> + (try + print_name (name_of_rel ctx n) ++ str ("(" ^ (string_of_int n) ^ ")") + with Failure _ -> str ("UNBOUND_REL_" ^ (string_of_int n))) + | DLambda ((namel, t), e, _) -> str "fun " ++ print_name (snd namel) ++ spc () ++ + str ":" ++ spc () ++ print_dtype' ctx (snd t) ++ spc () ++ str "=>" ++ spc () + ++ print_dterm_loc ((snd namel, t) :: ctx) e + | DApp (x, y, _) -> (print_dterm_loc ctx x) ++ spc () ++ + str "(" ++ (print_dterm_loc ctx y) ++ str ")" + | DLetIn (n, e, e', _) -> + let te = + try type_of_dterm_loc ctx e + with e -> debug 3 (str "Couldn't find type_of_dterm in print_dterm'"); + raise e + in + str "let" ++ spc () ++ print_name_loc n + ++ spc () ++ str "=" ++ spc () ++ print_dterm_loc ctx e ++ + print_dterm_loc ((snd n, te) :: ctx) e' + | DLetTuple (nl, t, e, _) -> + str "let" ++ spc () ++ str "(" ++ + string_of_list (List.rev_map (fun (n, _, _) -> print_name_loc n) nl) + ++ str ")" ++ spc () ++ str "=" ++ spc () ++ + print_dterm_loc ctx t ++ str "in" ++ spc () ++ + print_dterm_loc ((List.map (fun (x, y, z) -> (snd x, y)) nl) @ ctx) e + | DIfThenElse (b, t, t', _) -> + let ctx' = (Name (id_of_string "H"), (dummy_loc, DTRel 0)) :: ctx in + str "if" ++ spc () ++ print_dterm_loc ctx b ++ spc () ++ + str "then" ++ spc () ++ print_dterm_loc ctx' t ++ spc () ++ + str "else" ++ spc () ++ print_dterm_loc ctx' t' + | DSum ((n, t), (t', tt'), _) -> + let ctx' = + try (snd n, type_of_dterm_loc ctx t) :: ctx + with e -> debug 3 (str "Couldn't find type_of_dterm in print_dterm' (sum)"); + raise e + in + str "(" ++ print_name (snd n) ++ str ":=" + ++ print_dterm_loc ctx t ++ str "," + ++ print_dterm_loc ctx' t' ++ str ":" + ++ print_dtype_loc ctx' tt' ++ str ")" + | DCoq (cstr, t) -> pr_term cstr + +and print_dterm_loc ctx (_, x) = print_dterm' ctx x + (*debug_msg 1 (str ":" ++ print_dtype_loc ctx (type_of_dterm ctx x))*) + +and print_dtype' ctx = function + | DTApp (x, y, t, s) -> print_dtype_loc ctx x ++ spc() ++ + str "(" ++ print_dtype_loc ctx y ++ str ")" + | DTPi ((id, x), y, s) -> + str "(" ++ print_name_loc id ++ str ":" ++ print_dtype_loc ctx x ++ str ")" + ++ spc() ++ print_dtype_loc ((snd id, x) :: ctx) y + | DTSigma ((id, x), y, s) -> + str "[" ++ print_name_loc id ++ str ":" ++ print_dtype_loc ctx x ++ str "]" + ++ spc() ++ print_dtype_loc ((snd id, x) :: ctx) y + | DTSubset ((id, x), y, s) -> + str "{" ++ str (string_of_id (snd id)) ++ str ":" ++ print_dtype_loc ctx x ++ str "|" + ++ spc() ++ print_dtype_loc ((Name (snd id), x) :: ctx) y ++ str "}" + | (DTRel i) as x -> + (try print_name (name_of_rel ctx i) ++ str ("(" ^ (string_of_int i) ^ ")") + with Failure _ -> str ("_UNBOUND_REL_" ^ (string_of_int i))) + | DTTerm (t, tt, s) -> str "Term:(" ++ print_dterm_loc ctx t ++ str ")" + | DTInd (n, t, i, s) -> str (string_of_id (snd n)) + | DTCoq (c, t, s) -> + debug_msg 1 (str "Coq:(") ++ pr_term c ++ + debug_msg 1 (str ":" ++ print_dtype_loc ctx t ++ str ")") + | DTSort s -> + pr_term (mkSort (snd s)) + +and print_dtype_loc ctx (_, t) = print_dtype' ctx t + +let _ = print_dtype_locref := print_dtype_loc + +let rec reduce_term t = + match t with + | DLambda ((n, x), y, dt) -> DLambda ((n, reduce_type_loc x), reduce_term_loc y, reduce_type_loc dt) + | DApp (dte, dte', dt) -> snd (subst_term dte' dte) + | DLetIn (nl, dte, dte', dt) -> snd (subst_term dte' dte) + | DLetTuple (nl, dte, dte', dt) -> t (* TODO *) + | DIfThenElse (db, de, de', dt) -> t (* TODO *) + | DSum _ | DRel _ | DCoq _ -> t + +and reduce_term_loc (loc, t) = (loc, reduce_term t) + +and reduce_type = function + | DTApp (x, y, t, s) -> snd (subst y x) + | DTPi ((id, x), y, s) -> DTPi ((id, reduce_type_loc x), reduce_type_loc y, s) + | DTSigma ((id, x), y, s) -> DTSigma ((id, reduce_type_loc x), reduce_type_loc y, s) + | DTSubset ((id, x), y, s) -> DTSubset ((id, reduce_type_loc x), reduce_type_loc y, s) + | (DTRel i) as x -> x + | DTTerm (t, tt, s) -> DTTerm (reduce_term_loc t, reduce_type_loc tt, s) + | DTInd (n, t, i, s) as x -> x + | DTCoq (c, t, s) as x -> x + | DTSort _ as x -> x + +and reduce_type_loc (loc, t) = (loc, reduce_type t) + + +let rec type_equiv ctx u v = + trace (str "Check type equivalence: " ++ print_dtype_loc ctx u ++ str " and " ++ print_dtype_loc ctx v); + match snd u, snd v with + DTCoq (_, x, _), y -> type_equiv ctx x v + | x, DTCoq (_, y, _) -> type_equiv ctx u y + + | DTApp (_, _, t, _), _ -> type_equiv ctx t v + | _, DTApp (_, _, t, _) -> type_equiv ctx u t + + | (DTPi ((_, x), y, _), DTPi ((n', x'), y', _)) -> + type_equiv ctx x x' && type_equiv ((snd n', x') :: ctx) y y' + | (DTSigma ((_, x), y, _), DTSigma ((n', x'), y', _)) -> + type_equiv ctx x x' && type_equiv ((snd n', x') :: ctx) y y' + | (DTSubset ((_, x), y, _), DTSubset ((_, x'), y', _)) -> + type_equiv ctx x x' + | (DTRel x, DTRel y) -> x = y + | (DTInd (n, _, i, _), DTInd (n', _, i', _)) -> i == i' || i = i' + | _ -> false + +let convertible ctx u v = + type_equiv ctx (reduce_type_loc u) (reduce_type_loc v) + +let rec check_subtype ctx u v = + trace (str "Check subtype: " ++ print_dtype_loc ctx u ++ str " and " ++ print_dtype_loc ctx v); + match (snd u, snd v) with + DTCoq (_, t, _), _ -> check_subtype ctx t v + | _, DTCoq (_, t, _) -> check_subtype ctx u t + + | DTInd (_, t, _, _), _ -> check_subtype ctx t v + | _, DTInd (_, t, _, _) -> check_subtype ctx u t + + | DTApp (_, _, t, _), _ -> check_subtype ctx t v + | _, DTApp (_, _, t, _) -> check_subtype ctx u t + + | DTRel i, _ -> + let t = + try type_of_rel ctx i + with e -> + debug 3 (str "Couldn't find type_of_rel in check_subtype"); + raise e + in check_subtype ctx (lift (succ i) t) v + | _, DTRel i -> + let t = + try type_of_rel ctx i + with e -> debug 3 (str "Couldn't find type_of_rel in check_subtype"); + raise e + in + check_subtype ctx u (lift (succ i) t) + + | (DTPi ((_, x), y, _), DTPi ((n', x'), y', _)) -> + check_subtype ctx x' x && check_subtype ((snd n', x') :: ctx) y y' + + | (DTSigma ((_, x), y, _), DTSigma ((n', x'), y', _)) -> + check_subtype ctx x x' && check_subtype ((snd n', x') :: ctx) y y' + + | (DTSubset ((_, x), y, _), _) -> check_subtype ctx x v + | (_, DTSubset ((_, x), y, _)) -> check_subtype ctx u x + | (DTSort s, DTSort s') -> + (match snd s, snd s' with + Prop _, Type _ -> true + | x, y -> x = y) + | _ -> convertible ctx u v + +let rec mu ctx = function + | DTSubset ((_, x), y, _) -> mu ctx (snd x) + | DTCoq (_, x, _) -> mu ctx (snd x) + | DTInd (_, t, _, _) -> mu ctx (snd t) + | DTApp (_, _, t, _) -> mu ctx (snd t) + | DTRel i -> mu ctx (snd (type_of_rel ctx i)) + | x -> x + +exception Not_implemented of string + +let notimpl s = raise (Not_implemented s) + +let type_application ctx ((locx, x) as tx) ((locy, y) as ty) = + let narg, targ, tres, sres = + match mu ctx x with + | DTPi ((n, x), y, z) -> n, x, y, z + | x -> + typing_error (NonFunctionalApp (locx, + (print_dtype_loc ctx tx), + (print_dtype' ctx x))) + in + try + if check_subtype ctx ty targ then + let dtres = subst tres ty in + debug 1 (str "Subst of " ++ print_dtype_loc ctx ty ++ str " in " ++ + print_dtype_loc ((snd narg, targ) :: ctx) tres); + debug 1 (str "Subst in result type: " ++ print_dtype_loc ctx dtres); + dummy_loc, DTApp (tx, ty, dtres, sort_of_dtype_loc ctx dtres) + else + subtyping_error (UncoercibleInferType + (locy, print_dtype_loc ctx ty, print_dtype_loc ctx targ)) + + with e -> raise e (* Todo check exception etc.. *) + + +let rec dtype_of_types ctx c = + let dt = + match kind_of_term c with + | Rel i -> + DTRel (pred i) + | Var id -> + let ref = Nametab.locate (Libnames.make_short_qualid id) in + let t = Libnames.constr_of_global ref in + snd (dtype_of_types ctx t) + | Meta mv -> notimpl "Meta" + | Evar pex -> notimpl "Evar" + | Sort s -> DTSort (dummy_loc, s) + | Cast (c, t) -> snd (dtype_of_types ctx t) + | Prod (n, t, t') -> + let dt = dtype_of_types ctx t in + let ctx' = (n, dt) :: ctx in + let dt' = dtype_of_types ctx' t' in + DTPi (((dummy_loc, n), dt), dt', sort_of_dtype_loc ctx' dt') + | Lambda (n, t, e) -> notimpl "Lambda" + | LetIn (n, e, t, e') -> notimpl "LetIn" + | App (f, el) -> + snd (List.fold_left + (fun acc el -> + let tel = dtype_of_types ctx el in + type_application ctx acc tel) + (dtype_of_types ctx f) (Array.to_list el)) + | Const cst -> + let t = Global.lookup_constant cst in + let dt = dtype_of_types ctx t.Declarations.const_type in + DTCoq (c, dt, sort_of_dtype_loc ctx dt) + | Ind i -> + let (_, ind) = Inductive.lookup_mind_specif (Global.env ()) i in + DTInd ((dummy_loc, ind.Declarations.mind_typename), + dtype_of_types ctx ind.Declarations.mind_nf_arity, + i, (dummy_loc, ind.Declarations.mind_sort)) + (* let t = Inductiveops.type_of_inductive (Global.env ()) i in *) +(* debug "Lookup inductive"; *) + (* let dt = dtype_of_types ctx t in *) +(* DTCoq (t, dt, sort_of_dtype_loc ctx dt) *) + + | Construct con -> + let t = Inductiveops.type_of_constructor (Global.env ()) con in + let dt = dtype_of_types ctx t in + DTCoq (c, dt, sort_of_dtype_loc ctx dt) + | Case _ -> notimpl "Case" + | Fix fixpt -> notimpl "Fixpoint" + | CoFix cofixpt -> notimpl "CoFixpoint" + in dummy_loc, dt + +let rec dtype_of_constr ctx c = + let dt = + match kind_of_term c with + | Rel i -> DTRel (pred i) + | Var id -> + let ref = Nametab.locate (Libnames.make_short_qualid id) in + let t = Libnames.constr_of_global ref in + snd (dtype_of_constr ctx t) + | Meta mv -> notimpl "Meta" + | Evar pex -> notimpl "Evar" + | Sort s -> DTSort (dummy_loc, s) + | Cast (c, t) -> snd (dtype_of_constr ctx t) + | Prod (n, t, t') -> + let dt = dtype_of_constr ctx t in + let ctx' = (n, dt) :: ctx in + let dt' = dtype_of_constr ctx' t' in + DTPi (((dummy_loc, n), dt), dt', sort_of_dtype_loc ctx' dt') + | Lambda (n, t, e) -> notimpl "Lambda" + | LetIn (n, e, t, e') -> notimpl "LetIn" + | App (f, el) -> + snd (List.fold_left + (fun acc el -> + type_application ctx acc (dtype_of_constr ctx el)) + (dtype_of_constr ctx f) (Array.to_list el)) + | Const cst -> + let t = Global.lookup_constant cst in + let dt = dtype_of_constr ctx t.Declarations.const_type in + snd dt + + | Ind i -> + let (_, ind) = Inductive.lookup_mind_specif (Global.env ()) i in + DTInd ((dummy_loc, ind.Declarations.mind_typename), + dtype_of_types ctx ind.Declarations.mind_nf_arity, + i, (dummy_loc, ind.Declarations.mind_sort)) + + | Construct con -> + let t = Inductiveops.type_of_constructor (Global.env ()) con in + let dt = dtype_of_constr ctx t in + snd dt + | Case _ -> notimpl "Case" + | Fix fixpt -> notimpl "Fixpoint" + | CoFix cofixpt -> notimpl "CoFixpoint" + in dummy_loc, dt + +let list_assoc_index x l = + let rec aux i = function + (y, _) :: tl -> if x = y then i else aux (succ i) tl + | [] -> debug 2 (str "raising not_found in list_assoc_index"); + raise Not_found + in aux 0 l + +let coqref ctx (loc, r) = + let qualid = Libnames.make_short_qualid r in + try + let gr = Nametab.locate qualid in + debug 3 (str "Resolved " ++ str (string_of_id r) ++ str " globally"); + Libnames.constr_of_global gr + with Not_found -> + debug 3 (str "Error in coqref"); + Nametab.error_global_not_found_loc loc qualid + +let coqtermref ctx r = + let constr = coqref ctx r in + let dtype = dtype_of_constr ctx constr in + DCoq (constr, dtype), dtype + +let coqtyperef ctx r = + let constr = coqref ctx r in + let dtype = dtype_of_types ctx constr in + snd dtype, dtype + +let debug_loc n (loc, e) = + debug n (Toplevel.print_toplevel_error (Stdpp.Exc_located (loc, Debug_msg e))) + +let rec dtype n ctx (loc, t) = + let t' = + match t with + TApp (x, y) -> + let tx, ty = dtype n ctx x, dtype n ctx y in + snd (type_application ctx tx ty) + | TPi ((name, t), t') -> + let dt = dtype n ctx t in + let dt' = dtype (succ n) ((snd name, dt) :: ctx) t' in + DTPi ((name, dt), dt', (dummy_loc, type_0)) + | TSigma ((name, t), t') -> + let dt = dtype n ctx t in + let dt' = dtype (succ n) ((snd name, dt) :: ctx) t' in + DTSigma ((name, dt), dt', (dummy_loc, type_0)) + | TSubset ((i, t), t') -> + let dt = dtype n ctx t in + let ctx' = (Name (snd i), dt) :: ctx in + let dt' = dtype (succ n) ctx' t' in + DTSubset ((i, dt), dt', sort_of_dtype_loc ctx dt) + | TIdent (loc, i) -> + let name = Name i in + if List.mem_assoc name ctx then + let typ = List.assoc name ctx in + let index = list_assoc_index name ctx in + debug 3 (str "Resolved " ++ str (string_of_id i) ++ str " locally"); + DTRel index + else fst (coqtyperef ctx (loc, i)) + | TTerm t -> let t, tt = dterm n ctx t in DTTerm (t, tt, sort_of_dtype_loc ctx tt) + in (loc, t') + +and dterm n ctx (loc, t) = + let t', tt' = + match t with + | SIdent li -> + begin + let name = Name (snd li) in + if List.mem_assoc name ctx then + let typ = List.assoc name ctx in + let index = list_assoc_index name ctx in + let typ' = lift (succ index) typ in + debug 3 (str "Resolved " ++ str (string_of_id (snd li)) ++ str " locally"); + DRel index, typ' + else coqtermref ctx li + end + + | SLambda (((loc, name) as ln, t), e) -> + let dt = dtype n ctx t in + let name = Name name in + let ln = loc, name in + let ctx' = (name, dt) :: ctx in + let de, te = dterm (succ n) ctx' e in + let dpi = dummy_loc, DTPi ((ln, dt), te, sort_of_dtype_loc ctx' te) in + DLambda ((ln, dt), de, dpi), dpi + + | SLetIn ((loc, name) as ln, e, e') -> + let de, te = dterm n ctx e in + let de', te' = dterm (succ n) ((name, te) :: ctx) e' in + DLetIn (ln, de, de', te'), te' + + | SApp (f, e) -> + let dt, tf = dterm n ctx f in + let narg, targ, tres, sres = + match mu ctx (snd tf) with + | DTPi ((n, x), y, z) -> n, x, y, z + | x -> typing_error (NonFunctionalApp + (fst f, print_dterm_loc ctx dt, + print_dtype' ctx x)) + in + let de, te = dterm n ctx e in + (try + if check_subtype ctx te targ then + let term = (dummy_loc, DTTerm (de, te, sort_of_dtype_loc ctx te)) in + let dtres = subst tres term in + debug 1 (str "Subst of " ++ print_dtype_loc ctx term ++ str " in " ++ + print_dtype_loc ((snd narg, targ) :: ctx) tres); + debug 1 (str "Subst in result type: " ++ print_dtype_loc ctx dtres); + DApp (dt, de, dtres), dtres + else + subtyping_error + (UncoercibleInferTerm (fst e, + print_dtype_loc ctx te, + print_dtype_loc ctx targ, + print_dterm_loc ctx de, + print_dterm_loc ctx dt)) + + + with e -> raise e (* Todo check exception etc.. *)) + + | SSumDep (((loc, id), t), (t', tt')) -> + let dt, tt = dterm n ctx t in + let ctx' = (Name id, tt) :: ctx in + let tt' = dtype (succ n) ctx' tt' in + let dt', _ = dterm (succ n) ctx' t' in + let rest = dummy_loc, + DTSigma (((loc, Name id), tt), tt', sort_of_dtype_loc ctx' tt') + in + DSum (((loc, Name id), dt), (dt', tt'), rest), rest + + | SSumInf (t, t') -> + let dt, tt = dterm n ctx t in + let ctx' = (Anonymous, tt) :: ctx in + let dt', tt' = dterm (succ n) ctx' t' in + let rest = dummy_loc, + DTSigma (((dummy_loc, Anonymous), tt), tt', sort_of_dtype_loc ctx' tt') + in + DSum (((dummy_loc, Anonymous), dt), (dt', tt'), rest), rest + + | SIfThenElse (b, t, t') -> + let dn, tn = dterm n ctx b in + let ctx' = (Name (id_of_string "H"), + (dummy_loc, + DTCoq (Term.mkVar (id_of_string "H"), + (dummy_loc, DTSort (dummy_loc, mk_Set)), + (dummy_loc, type_0)))) :: ctx + in + let dt, tt = dterm (succ n) ctx' t + and dt', tt' = dterm (succ n) ctx' t' in + if convertible ctx' tt tt' then + DIfThenElse (dn, dt, dt', tt), (unlift 1 tt) + else typing_error (NonConvertible (loc, print_dtype_loc ctx' tt, + print_dtype_loc ctx' tt')) + + | SLetTuple (nl, t, t') -> + let dt, tt = dterm n ctx t in + debug 2 (str "Let tuple e type: " ++ print_dtype_loc ctx tt); + let rec aux n lctx tt l = + match snd tt, l with + DTSigma ((nl, t), t', s), nl' :: ((_ :: _) as tl) -> + aux (succ n) ((nl', t, tt) :: lctx) t' tl + | _, [nl] -> + (nl, tt, tt) :: lctx + | _, _ -> typing_error (NonSigma (fst tt, print_dtype_loc ctx tt)) + in + let ctx' = aux 0 [] tt nl in + let ctx'' = (List.map (fun (nl, t, t') -> (snd nl, t)) ctx') @ ctx in + let dt', tt' = dterm ((List.length nl) + n) ctx'' t' in + let t = DLetTuple (ctx', dt, dt', unlift (List.length nl) tt') in + debug 2 (str "Parsed let-tuple: " ++ print_dterm' ctx t); + debug 2 (str "ctx' = "); + debug 2 (str "ctx' = " ++ + let cmds, _ = + (List.fold_right + (fun (x, t, t') (acc, ctx) -> + let acc' = print_name_loc x ++ str ":" ++ + print_dtype_loc ctx t + in + let ctx' = (snd x, t) :: ctx in + (acc ++ spc () ++ acc', ctx')) + ctx' (mt (), ctx)) + in cmds); + + debug 2 (str "Parsed let-tuple in-term: " ++ print_dterm_loc ctx'' dt'); + debug 2 (str "Parsed let-tuple type: " ++ + print_dtype_loc ((List.map (fun (x, t, _) -> snd x, t) ctx') @ ctx) tt'); + t, tt' + + + in (loc, t'), tt' + +let infer ctx t = dterm 0 ctx t +let infer_type ctx t = dtype 0 ctx t + diff --git a/contrib/subtac/infer.mli b/contrib/subtac/infer.mli new file mode 100644 index 000000000..637e9edb1 --- /dev/null +++ b/contrib/subtac/infer.mli @@ -0,0 +1,59 @@ +type term_pp = Pp.std_ppcmds + +type subtyping_error = + | UncoercibleInferType of Util.loc * term_pp * term_pp + | UncoercibleInferTerm of Util.loc * term_pp * term_pp * term_pp * term_pp + | UncoercibleRewrite of term_pp * term_pp + +type typing_error = + | NonFunctionalApp of Util.loc * term_pp * term_pp + | NonConvertible of Util.loc * term_pp * term_pp + | NonSigma of Util.loc * term_pp + +exception Subtyping_error of subtyping_error +exception Typing_error of typing_error +exception Debug_msg of string + +val subtyping_error : subtyping_error -> 'a +val typing_error : typing_error -> 'a + +type sort = Term.sorts +type sort_loc = sort Util.located +type dterm = + DRel of Natural.nat + | DLambda of (Names.name Util.located * dtype_loc) * dterm_loc * dtype_loc + | DApp of dterm_loc * dterm_loc * dtype_loc + | DLetIn of Names.name Util.located * dterm_loc * dterm_loc * dtype_loc + | DLetTuple of (Names.name Util.located * dtype_loc * dtype_loc) list * + dterm_loc * dterm_loc * dtype_loc + | DIfThenElse of dterm_loc * dterm_loc * dterm_loc * dtype_loc + | DSum of (Names.name Util.located * dterm_loc) * (dterm_loc * dtype_loc) * + dtype_loc + | DCoq of Term.constr * dtype_loc +and dterm_loc = dterm Util.located +and dtype = + DTApp of dtype_loc * dtype_loc * dtype_loc * sort_loc + | DTPi of (Names.name Util.located * dtype_loc) * dtype_loc * sort_loc + | DTSigma of (Names.name Util.located * dtype_loc) * dtype_loc * sort_loc + | DTSubset of (Names.identifier Util.located * dtype_loc) * dtype_loc * + sort_loc + | DTRel of Natural.nat + | DTTerm of dterm_loc * dtype_loc * sort_loc + | DTSort of sort_loc + | DTInd of Names.identifier Util.located * dtype_loc * Names.inductive * + sort_loc + | DTCoq of Term.types * dtype_loc * sort_loc +and dtype_loc = dtype Util.located + +val print_dtype_loc : + (Names.name * dtype_loc) list -> dtype_loc -> Pp.std_ppcmds +val print_dterm_loc : + (Names.name * dtype_loc) list -> dterm_loc -> Pp.std_ppcmds + +val sort_of_dtype_loc : + (Names.name * dtype_loc) list -> dtype_loc -> sort_loc + + +val infer : + (Names.name * dtype_loc) list -> Sast.term_loc -> dterm_loc * dtype_loc +val infer_type : (Names.name * dtype_loc) list -> Sast.type_loc -> dtype_loc diff --git a/contrib/subtac/natural.ml b/contrib/subtac/natural.ml new file mode 100644 index 000000000..a76d7357b --- /dev/null +++ b/contrib/subtac/natural.ml @@ -0,0 +1,10 @@ +type nat = int + +let (+) (x : nat) (y : nat) = x + y +let (-) (x : nat) (y : nat) = + if y > x then raise (Invalid_argument "in substraction") + else x - y + +let succ (x : nat) = succ x + +let (<) (x : nat) (y : nat) = x < y diff --git a/contrib/subtac/rewrite.ml b/contrib/subtac/rewrite.ml new file mode 100644 index 000000000..b9dcb1a89 --- /dev/null +++ b/contrib/subtac/rewrite.ml @@ -0,0 +1,637 @@ +open Evd +open Libnames +open Coqlib +open Natural +open Infer +open Term +open Names +open Scoq +open Pp +open Ppconstrnew +open Util + +type recursion_info = { + arg_name: identifier; + arg_type: types; (* A *) + wf_relation: constr; (* R : A -> A -> Prop *) + wf_proof: constr; (* : well_founded R *) + f_type: types; (* f: A -> Set *) +} + +let id_of_name = function + Name id -> id + | Anonymous -> raise (Invalid_argument "id_of_name") + +let rel_to_vars ctx constr = + let rec aux acc = function + (n, _, _) :: ctx -> + aux (Term.subst1 (mkVar n) acc) ctx + | [] -> acc + in aux constr ctx + +let subst_ctx ctx c = + let rec aux ((ctx, n, c) as acc) = function + (name, None, typ) :: tl -> + aux (((id_of_name name, None, rel_to_vars ctx typ) :: ctx), + pred n, c) tl + | (name, Some term, typ) :: tl -> + let t' = Term.substnl [term] n c in + aux (ctx, n, t') tl + | [] -> acc + in + let (x, _, z) = aux ([], pred (List.length ctx), c) (List.rev ctx) in + (x, rel_to_vars x z) + +(* Anotation needed for failed generalization *) +let named_context_of_ctx ctx : Sign.named_context = + List.fold_right + (fun (name, x, t) ctx -> + let x' = match x with + Some e -> Some (rel_to_vars ctx e) + | None -> None + and t' = rel_to_vars ctx t in + (id_of_name name, x', t') :: ctx) + ctx [] + +let env_of_ctx ctx : Environ.env = + Environ.push_rel_context ctx (Global.env ()) + +let rels_of_ctx ctx = + let n = List.length ctx in + Array.init n (fun i -> mkRel (n - i)) + +type prog_info = { + mutable evm: evar_map; + rec_info: recursion_info option; +} + +let my_print_constr ctx term = + Termops.print_constr_env (env_of_ctx ctx) term + +let my_print_context ctx = + Termops.print_rel_context (env_of_ctx ctx) + +let pair_of_array a = (a.(0), a.(1)) +let make_name s = Name (id_of_string s) + +let app_opt c e = + match c with + Some constr -> constr e + | None -> e + +(* Standard ? *) +let unlift n c = + let rec aux n acc = + if n = 0 then acc + else aux (pred n) (Termops.pop acc) + in aux n c + +let evar_args ctx = + let len = List.length ctx in + Array.init len (fun i -> mkRel (succ i)) + +let if_branches c = + match kind_of_term c with + | App (c, l) -> + (match kind_of_term c with + Ind i -> + let len = Array.length l in + if len = 2 + then + let (a, b) = pair_of_array l in + Some (i, (a,b)) + else None + | _ -> None) + | _ -> None + +let disc_proj_exist ctx x = + trace (str "disc_proj_exist: " ++ my_print_constr ctx x); + match kind_of_term x with + | App (c, l) -> + (if Term.eq_constr c (Lazy.force sig_).proj1 + && Array.length l = 3 + then + (match kind_of_term l.(2) with + App (c, l) -> + (match kind_of_term c with + Construct c -> + if c = Term.destConstruct (Lazy.force sig_).intro + && Array.length l = 4 + then + Some (l.(0), l.(1), l.(2), l.(3)) + else None + | _ -> None) + | _ -> None) + else None) + | _ -> None + +let rec rewrite_type prog_info ctx ((loc, t) as lt) : Term.types * Term.types = + trace (str "rewrite_type: " ++ print_dtype_loc [] lt); + trace (str "context: " ++ my_print_context ctx); + let aux prog_info ctx x = fst (rewrite_type prog_info ctx x) in + match t with + DTPi ((name, a), b, s) -> + let ta = aux prog_info ctx a in + let ctx' = (snd name, None, ta) :: ctx in + (mkProd (snd name, ta, aux prog_info ctx' b)), mkSort (snd s) + + | DTSigma ((name, a), b, s) -> + let ta = aux prog_info ctx a in + let ctx' = (snd name, None, ta) :: ctx in + mkApp ((Lazy.force existS).typ, + [| ta; + mkLambda + (snd name, ta, aux prog_info ctx' b) |]), + mkSort (snd s) + + | DTSubset ((name, a), b, s) -> + let ta = aux prog_info ctx a in + let name = Name (snd name) in + let ctx' = (name, None, ta) :: ctx in + (mkApp ((Lazy.force sig_).typ, + [| ta; mkLambda (name, ta, aux prog_info ctx' b) |])), + mkSort (snd s) + + | DTRel i -> + let (_, term, typ) = List.nth ctx i in + let t = + (*match term with + Some t -> Term.lift (succ i) t + | None -> *)mkRel (succ i) + in t, Term.lift (succ i) typ + + | DTApp (x, y, t, _) -> + let (cx, tx), (cy, ty) = + rewrite_type prog_info ctx x, rewrite_type prog_info ctx y + in + let coercex, coqx = mutype prog_info ctx tx in + let narg, targ, tres = + match decompose_prod_n 1 coqx with + [x, y], z -> x, y, z + | _ -> assert(false) + in + debug 2 (str "Coercion for type application: " ++ + my_print_constr ctx cx ++ spc () + ++ my_print_constr ctx cy); + let coercey = coerce prog_info ctx ty targ in + let t' = Term.subst1 (app_opt coercey cy) tres in + let term = mkApp (app_opt coercex cx, [|app_opt coercey cy|]) in + debug 1 (str "Term obtained after coercion (at application): " ++ + my_print_constr ctx term); + term, t' + + | DTCoq (t, dt, _) -> + (* type should be equivalent to 'aux prog_info ctx dt' *) + t, Typing.type_of (env_of_ctx ctx) prog_info.evm t + | DTTerm (t, dt, _) -> rewrite_term prog_info ctx t + | DTSort s -> mkSort (snd s), mkSort type_0 (* false *) + | DTInd (_, t, i, s) -> + let (_, ind) = Inductive.lookup_mind_specif (Global.env ()) i in + mkInd i, ind.Declarations.mind_nf_arity + +and mutype prog_info ctx t = + match disc_subset t with + Some (u, p) -> + let f, ct = mutype prog_info ctx u in + (Some (fun x -> + app_opt f (mkApp ((Lazy.force sig_).proj1, + [| u; p; x |]))), + ct) + | None -> (None, t) + +and muterm prog_info ctx t = mutype prog_info ctx t + +and coerce' prog_info ctx x y : (Term.constr -> Term.constr) option = + let subco () = subset_coerce prog_info ctx x y in + trace (str "Coercion from " ++ (my_print_constr ctx x) ++ + str " to "++ my_print_constr ctx y); + match (kind_of_term x, kind_of_term y) with + | Sort s, Sort s' -> + (match s, s' with + Prop x, Prop y when x = y -> None + | Prop _, Type _ -> None + | Type x, Type y when x = y -> None (* false *) + | _ -> subco ()) + | Prod (name, a, b), Prod (name', a', b') -> + let c1 = coerce prog_info ctx a' a in + let bsubst = Term.subst1 (app_opt c1 (mkRel 1)) b in + let c2 = coerce prog_info ((name', None, a') :: ctx) bsubst b' in + (match c1, c2 with + None, None -> None + | _, _ -> + Some + (fun f -> + mkLambda (name', a', + app_opt c2 + (mkApp (Term.lift 1 f, + [| app_opt c1 (mkRel 1) |]))))) + + | App (c, l), App (c', l') -> + (match kind_of_term c, kind_of_term c' with + Ind i, Ind i' -> + let len = Array.length l in + let existS = Lazy.force existS and sig_ = Lazy.force sig_ in + if len = Array.length l' && len = 2 + && i = i' && i = Term.destInd existS.typ + then + begin (* Sigma types *) + debug 1 (str "In coerce sigma types"); + let (a, pb), (a', pb') = + pair_of_array l, pair_of_array l' + in + let c1 = coerce prog_info ctx a a' in + let remove_head c = + let (_, _, x) = Term.destProd c in + x + in + let b, b' = remove_head pb, remove_head pb' in + let b'subst = + match c1 with + None -> b' + | Some c1 -> Term.subst1 (c1 (mkRel 1)) b' + in + let ctx' = (make_name "x", None, a) :: ctx in + let c2 = coerce prog_info ctx' b b'subst in + match c1, c2 with + None, None -> None + | _, _ -> + Some + (fun x -> + let x, y = + app_opt c1 (mkApp (existS.proj1, + [| a; pb; x |])), + app_opt c2 (mkApp (existS.proj2, + [| a; pb'; x |])) + in + mkApp (existS.intro, [| x ; y |])) + end + else subco () + | _ -> subco ()) + | _, _ -> subco () + +and coerce prog_info ctx (x : Term.constr) (y : Term.constr) + : (Term.constr -> Term.constr) option + = + try let cstrs = Reduction.conv_leq (Global.env ()) x y in None + with Reduction.NotConvertible -> coerce' prog_info ctx x y + +and disc_subset x = + match kind_of_term x with + | App (c, l) -> + (match kind_of_term c with + Ind i -> + let len = Array.length l in + let sig_ = Lazy.force sig_ in + if len = 2 && i = Term.destInd sig_.typ + then + let (a, b) = pair_of_array l in + Some (a, b) + else None + | _ -> None) + | _ -> None + +and disc_exist ctx x = + trace (str "Disc_exist: " ++ my_print_constr ctx x); + match kind_of_term x with + | App (c, l) -> + (match kind_of_term c with + Construct c -> + if c = Term.destConstruct (Lazy.force sig_).intro + then Some (l.(0), l.(1), l.(2), l.(3)) + else None + | _ -> None) + | _ -> None + +and subset_coerce prog_info ctx x y = + match disc_subset x with + Some (u, p) -> + let c = coerce prog_info ctx u y in + let f x = + app_opt c (mkApp ((Lazy.force sig_).proj1, + [| u; p; x |])) + in Some f + | None -> + match disc_subset y with + Some (u, p) -> + let c = coerce prog_info ctx x u in + let t = id_of_string "t" in + let evarinfo x = + let cx = app_opt c x in + let pcx = mkApp (p, [| cx |]) in + let ctx', pcx' = subst_ctx ctx pcx in + cx, { + Evd.evar_concl = pcx'; + Evd.evar_hyps = ctx'; + Evd.evar_body = Evd.Evar_empty; + } + in + Some + (fun x -> + let key = mknewexist () in + let cx, evi = evarinfo x in + prog_info.evm <- Evd.add prog_info.evm key evi; + (mkApp + ((Lazy.force sig_).intro, + [| u; p; cx; + mkEvar (key, evar_args ctx) |]))) + | None -> + (try + let cstrs = Reduction.conv (Global.env ()) x y + in + ignore(Univ.merge_constraints cstrs (Global.universes ())); + Some (fun x -> + mkCast (x, y)) + with + Reduction.NotConvertible -> + subtyping_error + (UncoercibleRewrite (my_print_constr ctx x, + my_print_constr ctx y)) + | e -> raise e) + +and rewrite_term prog_info ctx (t : dterm_loc) : Term.constr * Term.types = + let rec aux ctx (loc, t) = + match t with + | DRel i -> + let (_, term, typ) = List.nth ctx i in + let t = mkRel (succ i) in + t, Term.lift (succ i) typ + + | DLambda ((name, targ), e, t) -> + let argt, argtt = rewrite_type prog_info ctx targ in + let coqe, et = + rewrite_term prog_info ((snd name, None, argt) :: ctx) e + in + let coqt = mkLambda (snd name, argt, coqe) + and t = mkProd (snd name, argt, et) in + (coqt, t) + + | DApp (f, e, t) -> + let cf, ft = rewrite_term prog_info ctx f in + let coercef, coqt = muterm prog_info ctx ft in + let narg, targ, tres = + match decompose_prod_n 1 coqt with + [x, y], z -> x, y, z + | _ -> assert(false) + in + let ce, te = rewrite_term prog_info ctx e in + debug 2 (str "Coercion for application" ++ + my_print_constr ctx cf ++ spc () + ++ my_print_constr ctx ce); + let call x = + let len = List.length ctx in + let cf = app_opt coercef cf in + match prog_info.rec_info with + Some r -> + (match kind_of_term cf with + Rel i when i = (pred len) -> + debug 3 (str "Spotted recursive call!"); + let ctx', proof = + subst_ctx ctx (mkApp (r.wf_relation, + [| x; mkRel len |])) + in + let evarinfo = + { + Evd.evar_concl = proof; + Evd.evar_hyps = ctx'; + Evd.evar_body = Evd.Evar_empty; + } + in + let key = mknewexist () in + prog_info.evm <- Evd.add prog_info.evm key evarinfo; + mkApp (cf, [| x; mkEvar(key, evar_args ctx) |]) + | _ -> mkApp (cf, [| x |])) + | None -> mkApp (cf, [| x |]) + in + let coercee = coerce prog_info ctx te targ in + let t' = Term.subst1 (app_opt coercee ce) tres in + let t = call (app_opt coercee ce) in + debug 2 (str "Term obtained after coercion (at application): " ++ + Termops.print_constr_env (env_of_ctx ctx) t); + t, t' + + | DSum ((x, t), (t', u), stype) -> + let ct, ctt = rewrite_term prog_info ctx t in + let ctxterm = (snd x, Some ct, ctt) :: ctx in + let ctxtype = (snd x, None, ctt) :: ctx in + let ct', tt' = rewrite_term prog_info ctxterm t' in + let cu, _ = rewrite_type prog_info ctxtype u in + let coercet' = coerce prog_info ctxtype tt' cu in + let lam = Term.subst1 ct (app_opt coercet' ct') in + debug 1 (str "Term obtained after coercion: " ++ + Termops.print_constr_env (env_of_ctx ctx) lam); + + let t' = + mkApp ((Lazy.force existS).typ, + [| ctt; mkLambda (snd x, ctt, cu) |]) + in + mkApp ((Lazy.force existS).intro, + [| ctt ; mkLambda (snd x, ctt, cu); + ct; lam |]), t' + + | DLetIn (x, e, e', t) -> + let ce, et' = rewrite_term prog_info ctx e in + let ce', t' = aux ((snd x, (Some ce), et') :: ctx) e' in + mkLetIn (snd x, ce, et', ce'), t' + + | DLetTuple (l, e, e', t) -> + (* let (a, b) = e in e', l = [b, a] *) + let ce, et = rewrite_term prog_info ctx e in + debug 1 (str "Let tuple, e = " ++ + my_print_constr ctx ce ++ + str "type of e: " ++ my_print_constr ctx et); + let l, ctx' = + let rec aux acc ctx = function + (x, t, t') :: tl -> + let tx, _ = rewrite_type prog_info ctx t in + let trest, _ = rewrite_type prog_info ctx t' in + let ctx' = (snd x, None, tx) :: ctx in + aux ((x, tx, trest) :: acc) ctx' tl + | [] -> (acc), ctx + in aux [] ctx (List.rev l) + in + let ce', et' = aux ctx' e' in + let et' = unlift (pred (List.length l)) + (mkLambda (Anonymous, et, et')) in + debug 1 (str "Let tuple, type of e': " ++ + my_print_constr ctx' et'); + + let ind = destInd (Lazy.force existSind) in + let ci = Inductiveops.make_default_case_info + (Global.env ()) RegularStyle ind + in + let lambda = + let rec aux acc = function + (x, t, tt) :: (_ :: _) as tl -> + let lam = mkLambda (snd x, t, acc) in + let term = + mkLambda (make_name "dummy", tt, + mkCase (ci, et', mkRel 1, [| lam |])) + in aux term tl + | (x, t, _) :: [] -> + let lam = mkLambda (snd x, t, acc) in + mkCase (ci, et', ce, [| lam |]) + | _ -> assert(false) + in + match l with + (x, t, t') :: tl -> + aux (mkLambda (snd x, t, ce')) tl + | [] -> failwith "DLetTuple with empty list!" + in + debug 1 (str "Let tuple term: " ++ my_print_constr ctx lambda); + lambda, et' + + | DIfThenElse (b, e, e', t) -> + let name = Name (id_of_string "H") in + let (cb, tb) = aux ctx b in + (match if_branches tb with + Some (ind, (t, f)) -> + let ci = Inductiveops.make_default_case_info + (Global.env ()) IfStyle ind + in + let (ce, te), (ce', te') = + aux ((name, None, t) :: ctx) e, + aux ((name, None, f) :: ctx) e' + in + let lam = mkLambda (Anonymous, tb, te) in + let true_case = + mkLambda (name, t, ce) + and false_case = + mkLambda (name, f, ce') + in + (mkCase (ci, lam, cb, [| true_case; false_case |])), + (Termops.pop te) + | None -> failwith ("Ill-typed if")) + + + | DCoq (constr, t) -> constr, + Typing.type_of (env_of_ctx ctx) prog_info.evm constr + + in aux ctx t + +let global_kind : Decl_kinds.global_kind = Decl_kinds.IsDefinition +let goal_kind = Decl_kinds.IsGlobal Decl_kinds.DefinitionBody + + +let make_fixpoint t id term = + let typ = + mkProd (Name t.arg_name, t.arg_type, + mkProd(Anonymous, + mkApp (t.wf_relation, [| mkRel 1; mkRel 2 |]), + mkApp (t.f_type, [| mkRel 2 |]))) + in + let term' = + mkLambda (Name id, typ, term) + in + let fix = mkApp (Lazy.force fix, + [| t.arg_type; t.wf_relation; t.wf_proof; + t.f_type; + mkLambda (Name t.arg_name, t.arg_type, + term') + |]) + in fix + +let subtac recursive id (s, t) = + check_required_library ["Coq";"Init";"Datatypes"]; + check_required_library ["Coq";"Init";"Specif"]; + try + let prog_info = { evm = Evd.empty; rec_info = None } in + trace (str "Begin infer_type of given spec"); + let coqtype, coqtype', coqtype'', prog_info, ctx, coqctx = + match recursive with + Some (n, t) -> + let t' = infer_type [] t in + let namen = Name n in + let coqt = infer_type [namen, t'] s in + let t'', _ = rewrite_type prog_info [] t' in + let coqt', _ = rewrite_type prog_info [namen, None, t''] coqt in + let ftype = mkLambda (namen, t'', coqt') in + let prog_info = + let rec_info = + { arg_name = n; + arg_type = t''; + wf_relation = Lazy.force lt; + wf_proof = Lazy.force lt_wf; + f_type = ftype; + } + in { prog_info with rec_info = Some rec_info } + in + let coqtype = dummy_loc, + DTPi (((dummy_loc, namen), t'), coqt, + sort_of_dtype_loc [] coqt) + in + let coqtype' = mkProd (namen, t'', coqt') in + let ctx = [(Name id, coqtype); (namen, t')] + and coqctx = + [(Name id, None, coqtype'); (namen, None, t'')] + in coqt, coqt', coqtype', prog_info, ctx, coqctx + | None -> + let coqt = infer_type [] s in + let coqt', _ = rewrite_type prog_info [] coqt in + coqt, coqt', coqt', prog_info, [], [] + in + trace (str "Rewrite of coqtype done" ++ + str "coqtype' = " ++ pr_term coqtype'); + let dterm, dtype = infer ctx t in + trace (str "Inference done" ++ spc () ++ + str "Infered term: " ++ print_dterm_loc ctx dterm ++ spc () ++ + str "Infered type: " ++ print_dtype_loc ctx dtype); + let dterm', dtype' = + fst (rewrite_term prog_info coqctx dterm), + fst (rewrite_type prog_info coqctx dtype) + in + trace (str "Rewrite done" ++ spc () ++ + str "Inferred Coq term:" ++ pr_term dterm' ++ spc () ++ + str "Inferred Coq type:" ++ pr_term dtype' ++ spc () ++ + str "Rewritten Coq type:" ++ pr_term coqtype'); + let coercespec = coerce prog_info coqctx dtype' coqtype' in + trace (str "Specs coercion successfull"); + let realt = app_opt coercespec dterm' in + trace (str "Term Specs coercion successfull" ++ + my_print_constr coqctx realt); + let realt = + match prog_info.rec_info with + Some t -> make_fixpoint t id realt + | None -> realt + in + trace (str "Term after reduction" ++ my_print_constr coqctx realt); + let evm = prog_info.evm in + (try trace (str "Original evar map: " ++ Evd.pr_evar_map evm); + with Not_found -> trace (str "Not found in pr_evar_map")); + let tac = Refine.refine (evm, realt) in + msgnl (str "Starting proof"); + Command.start_proof id goal_kind coqtype'' (fun _ _ -> ()); + msgnl (str "Started proof"); + Pfedit.by tac + with + | Typing_error e -> + msg_warning (str "Type error in Program tactic:"); + let cmds = + (match e with + | NonFunctionalApp (loc, x, mux) -> + str "non functional type app of term " ++ + x ++ str " of (mu) type " ++ mux + | NonSigma (loc, t) -> + str "Term is not of Sigma type: " ++ t + | NonConvertible (loc, x, y) -> + str "Unconvertible terms:" ++ spc () ++ + x ++ spc () ++ str "and" ++ spc () ++ y + ) + in msg_warning cmds + + | Subtyping_error e -> + msg_warning (str "(Program tactic) Subtyping error:"); + let cmds = + match e with + | UncoercibleInferType (loc, x, y) -> + str "Uncoercible terms:" ++ spc () + ++ x ++ spc () ++ str "and" ++ spc () ++ y + | UncoercibleInferTerm (loc, x, y, tx, ty) -> + str "Uncoercible terms:" ++ spc () + ++ tx ++ spc () ++ str "of" ++ spc () ++ str "type" ++ spc () ++ x + ++ str "and" ++ spc() ++ ty ++ spc () ++ str "of" ++ spc () ++ str "type" ++ spc () ++ y + | UncoercibleRewrite (x, y) -> + str "Uncoercible terms:" ++ spc () + ++ x ++ spc () ++ str "and" ++ spc () ++ y + in msg_warning cmds + + | e -> raise e diff --git a/contrib/subtac/rewrite.mli b/contrib/subtac/rewrite.mli new file mode 100644 index 000000000..3f8bfb136 --- /dev/null +++ b/contrib/subtac/rewrite.mli @@ -0,0 +1,3 @@ +val subtac : + (Names.identifier * Sast.type_loc) option -> + Names.identifier -> Sast.type_loc * Sast.term_loc -> unit diff --git a/contrib/subtac/sast.ml b/contrib/subtac/sast.ml new file mode 100644 index 000000000..a447992e0 --- /dev/null +++ b/contrib/subtac/sast.ml @@ -0,0 +1,27 @@ +open Names +open Util + +type const = CNat of int | CInt of int | CBool of bool + + + +type term = + SIdent of identifier located + | SLambda of (identifier located * type_ located) * term located + | SApp of term located * term located + | SLetIn of (name located) * (term located) * term located + | SLetTuple of (name located) list * term located * term located + | SIfThenElse of (term located) * (term located) * (term located) + | SSumInf of (term located) * (term located) + | SSumDep of (identifier located * term located) * (term located * type_ located) +and lettuple_el = (identifier located) option * term_loc * type_loc option +and term_loc = term located +and type_ = + | TApp of type_loc * type_loc + | TPi of (name located * type_loc) * type_loc + | TSigma of (name located * type_loc) * type_loc + | TSubset of (identifier located * type_loc) * type_loc + | TIdent of identifier located + | TTerm of term_loc + +and type_loc = type_ located diff --git a/contrib/subtac/scoq.ml b/contrib/subtac/scoq.ml new file mode 100644 index 000000000..67547389c --- /dev/null +++ b/contrib/subtac/scoq.ml @@ -0,0 +1,58 @@ +open Evd +open Libnames +open Coqlib +open Natural +open Term +open Names + +let init_constant dir s = gen_constant "Subtac" dir s + +let build_sig () = + { proj1 = init_constant ["Init"; "Specif"] "proj1_sig"; + proj2 = init_constant ["Init"; "Specif"] "proj2_sig"; + elim = init_constant ["Init"; "Specif"] "sig_rec"; + intro = init_constant ["Init"; "Specif"] "exist"; + typ = init_constant ["Init"; "Specif"] "sig" } + +let sig_ = lazy (build_sig ()) + +let boolind = lazy (gen_constant "subtac" ["Init"; "Datatypes"] "bool") +let sumboolind = lazy (gen_constant "subtac" ["Init"; "Specif"] "sumbool") +let natind = lazy (gen_constant "subtac" ["Init"; "Datatypes"] "nat") +let intind = lazy (gen_constant "subtac" ["ZArith"; "binint"] "Z") +let existSind = lazy (gen_constant "subtac" ["Init"; "Specif"] "sigS") + +let existS = lazy (build_sigma_set ()) + +(* orders *) +let lt = lazy (gen_constant "subtac" ["Init"; "Peano"] "lt") +let lt_wf = lazy (gen_constant "subtac" ["Arith"; "Wf_nat"] "lt_wf") + +let fix = lazy (gen_constant "subtac" ["Init"; "Wf"] "Fix") + +let extconstr = Constrextern.extern_constr true (Global.env ()) +let extsort s = Constrextern.extern_constr true (Global.env ()) (mkSort s) + +open Pp + +let mknewexist = + let exist_counter = ref 0 in + fun () -> let i = exist_counter in + incr exist_counter; + !i + + +let debug_level = ref 0 + +let debug n s = + if n >= !debug_level then + msgnl s + else () + +let debug_msg n s = + if n >= !debug_level then s + else mt () + +let trace s = + if !debug_level < 2 then msgnl s + else () diff --git a/contrib/subtac/sparser.ml4 b/contrib/subtac/sparser.ml4 new file mode 100644 index 000000000..c89208ae4 --- /dev/null +++ b/contrib/subtac/sparser.ml4 @@ -0,0 +1,336 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* + Syntax for the subtac terms and types. + Elaborated from correctness/psyntax.ml4 by Jean-Christophe Filliātre *) + +(* $Id$ *) + +(*i camlp4deps: "parsing/grammar.cma" i*) + +open Options +open Util +open Names +open Nameops +open Vernacentries +open Reduction +open Term +open Libnames +open Topconstr + +open Sast + +(* We define new entries for programs, with the use of this module + * Subtac. These entries are named Subtac.<foo> + *) + +module Gram = Pcoq.Gram +module Constr = Pcoq.Constr +module Tactic = Pcoq.Tactic + +module Subtac = + struct + let gec s = Gram.Entry.create ("Subtac."^s) + (* types *) + let subtac_spec : type_loc Gram.Entry.e = gec "subtac_spec" + let subtac_term : term_loc Gram.Entry.e = gec "subtac_term" + + (* Hack to parse "(x:=t)" as an explicit argument without conflicts with the *) + (* admissible notation "(x t)" + taken from g_constrnew.ml4 *) + let lpar_id_coloneq = + Gram.Entry.of_parser "test_lpar_id_coloneq" + (fun strm -> + Pp.msgnl (Pp.str ("Testing lpar_id_coloneq:" ^ + (snd (List.hd (Stream.npeek 1 strm))))); + + match Stream.npeek 1 strm with + | [("","(")] -> + (match Stream.npeek 2 strm with + | [_; ("IDENT",s)] -> + (match Stream.npeek 3 strm with + | [_; _; ("", ":=")] -> + Stream.junk strm; Stream.junk strm; Stream.junk strm; + Pp.msgnl (Pp.str "Success"); + Names.id_of_string s + | _ -> raise Stream.Failure) + | _ -> raise Stream.Failure) + | _ -> raise Stream.Failure) + + let id_coloneq = + Gram.Entry.of_parser "test_id_coloneq" + (fun strm -> + Pp.msgnl (Pp.str ("Testing id_coloneq:" ^ + (snd (List.hd (Stream.npeek 1 strm))))); + + (match Stream.npeek 1 strm with + | [("IDENT",s)] -> + (match Stream.npeek 2 strm with + | [_; ("", ":=")] -> + Stream.junk strm; Stream.junk strm; + Pp.msgnl (Pp.str "Success"); + Names.id_of_string s + | _ -> raise Stream.Failure) + | _ -> raise Stream.Failure)) + + (*let identifier = gec "identifier" + let name = gec "name" + let type_ident = gec "type_ident" + let term_ident = gec "term_ident" + (* binders *) + let binder = gec "binder" + let binder_opt = gec "binder_opt" + (*let binders = gec "binders"*) + (* programs *) + let term = gec "term" + let arg = gec "arg" + let name = gec "name"*) +end + +open Subtac +open Util +open Coqast + +GEXTEND Gram + GLOBAL: subtac_spec subtac_term; + + (* Types ******************************************************************) + subtac_spec: + [ + "10" LEFTA + [ t = subtac_spec; t' = subtac_spec -> loc, TApp (t, t') ] + + | [ t = subtac_spec_no_app -> t ] + ]; + + subtac_spec_no_app: + [ [ + "(" ; t = subtac_spec_lpar_open -> t + | "[" ; x = binder_opt; "]"; t = subtac_spec -> loc, TSigma (x, t) + | "{" ; x = binder; "|"; p = subtac_spec; "}"; "->"; t = subtac_spec -> + let ((locx, i), tx) = x in + loc, TPi (((locx, Name i), (loc, TSubset (x, p))), t) + | "{" ; x = binder; "|"; p = subtac_spec; "}" -> + loc, TSubset(x, p) + | t = type_ident; f = subtac_spec_tident -> f t + ] + ] + ; + + subtac_spec_no_app_loc: + [ [ x = subtac_spec_no_app -> (loc, x) ] + ]; + + subtac_spec_tident: + [ [ + "->"; t' = subtac_spec -> + fun t -> loc, TPi (((dummy_loc, Anonymous), t), t') + | -> (fun x -> x) + ] + ] + ; + + subtac_spec_lpar_open: + [ + [ s = identifier; t = subtac_spec_lpar_name -> t s + | s = subtac_spec; ")" -> s ] + ] + ; + + subtac_spec_lpar_name: + [ + [ ":" ; y = subtac_spec; ")"; t = subtac_spec -> + (fun s -> loc, TPi ((((fst s), Name (snd s)), y), t)) + | l = LIST1 subtac_spec_no_app_loc; ")" -> fun s -> + List.fold_left (fun acc x -> + (join_loc (fst acc) (fst x), TApp (acc, snd x))) + (fst s, TIdent s) l + ] + ] + ; + + binder: + [ [ s = identifier; ":"; t = subtac_spec -> let (l,s) = s in + ((loc, s), t) + | "{"; x = binder; "|"; p = subtac_spec; "}" -> + let ((l, s), t) = x in + ((l, s), (loc, TSubset (x, p))) + ] + ] + ; + + identifier: + [ [ s = IDENT -> (loc, id_of_string s) ] ] + ; + + name': + [ [ s = IDENT -> (loc, Name (id_of_string s)) + | "_" -> loc, Anonymous + ] ] + ; + + name: + [ [ n = OPT name' -> match n with Some n -> n | None -> loc, Anonymous ] ] + ; + + binder_opt: + [ [ s = name; ":"; t = subtac_spec -> (s, t) ] ] + ; + + type_ident: + [ [ s = identifier -> loc, TIdent s ] ] + ; + +(* term_ident: *) +(* [ [ s = identifier -> SIdent s ] ] *) +(* ; *) + +(* lpar_colon_id: *) +(* [ [ i = lpar_id_coloneq -> loc, i ] ] *) +(* ; *) + + subtac_term: + [ + "20" LEFTA + [ t = subtac_term; t' = subtac_term -> + let loc = join_loc (fst t) (fst t') in + loc, SApp (t, t') + ] + | "10" + [ + i = identifier -> loc, SIdent i + | "fun"; bl = LIST1 binder; "=>"; p = subtac_term -> + (List.fold_left + (fun acc (((loc, s), (loc', t)) as b) -> + (join_loc loc (fst acc), SLambda (b, acc))) p bl) + | "let"; "("; nl = LIST0 name SEP ","; ")" ; "="; t = subtac_term; + "in"; t' = subtac_term -> + loc, (SLetTuple (nl, t, t')) + | "let"; i = name; "="; t = subtac_term; "in"; t' = subtac_term -> + loc, (SLetIn (i, t, t')) + | "if"; b = subtac_term; "then"; t = subtac_term; "else"; t' = subtac_term -> + loc, SIfThenElse (b, t, t') + | "("; t = lpar_term -> t + ] + + ] + ; + + lpar_term: + [ [ + x = id_coloneq; t = subtac_term; ","; + t' = subtac_term; ":"; tt = subtac_spec; ")" -> + (loc, (SSumDep (((dummy_loc, x), t), (t', tt)))) + | t = subtac_term; f = lpar_term_term -> f t + ] + ] + ; + + lpar_term_term: + [ [ + ","; t' = subtac_term; ")" -> + (fun t -> loc, (SSumInf (t, t'))) + | ")" -> (fun x -> x) + ] ] + ; + (* + subtac_term_lpar_open_ident: + [ [ ":="; t = subtac_term; ","; t' = subtac_term; ":"; tt = subtac_spec; ")" -> + (fun x -> (loc, (SSumDep ((x, t), (t', tt))))) + | t = subtac_term; ")" -> + (fun x -> loc, SApp ((fst x, (SIdent x)), t)) + + ] + ] + ; + + + sigma_binder: + [ [ s = OPT subtac_annot_identifier; t = subtac_term; topt = OPT subtac_annot_type -> + (s, t, topt) ] ] + ; + + subtac_annot_type: + [ [ ":"; t = subtac_spec -> t ] ] + ; + + subtac_annot_identifier: + [ [ s = identifier; ":=" -> s ] ] + ; +*) +(* + ast1: + [ [ x = prog2; IDENT "or"; y = prog1 -> bool_or loc x y + | x = prog2; IDENT "and"; y = prog1 -> bool_and loc x y + | x = prog2 -> x + ] ] + ; + ast2: + [ [ IDENT "not"; x = prog3 -> bool_not loc x + | x = prog3 -> x + ] ] + ; + ast3: + [ [ x = prog4; rel = relation; y = prog4 -> bin_op rel loc x y + | x = prog4 -> x + ] ] + ; + ast4: + [ [ x = prog5; "+"; y = prog4 -> bin_op "Zplus" loc x y + | x = prog5; "-"; y = prog4 -> bin_op "Zminus" loc x y + | x = prog5 -> x + ] ] + ; + ast5: + [ [ x = prog6; "*"; y = prog5 -> bin_op "Zmult" loc x y + | x = prog6 -> x + ] ] + ; + ast6: + [ [ "-"; x = prog6 -> un_op "Zopp" loc x + | x = ast7 -> without_effect loc x + ] ] + ; + + relation: + [ [ "<" -> "Z_lt_ge_bool" + | "<=" -> "Z_le_gt_bool" + | ">" -> "Z_gt_le_bool" + | ">=" -> "Z_ge_lt_bool" + | "=" -> "Z_eq_bool" + | "<>" -> "Z_noteq_bool" ] ] + ; +*) + END +;; + + +type type_loc_argtype = (type_loc, constr_expr, Tacexpr.raw_tactic_expr) Genarg.abstract_argument_type +type term_loc_argtype = (term_loc, constr_expr, Tacexpr.raw_tactic_expr) Genarg.abstract_argument_type + +let (wit_subtac_spec : type_loc_argtype), + (globwit_subtac_spec : type_loc_argtype), + (rawwit_subtac_spec : type_loc_argtype) = + Genarg.create_arg "subtac_spec" + +let (wit_subtac_term : term_loc_argtype), + (globwit_subtac_term : term_loc_argtype), + (rawwit_subtac_term : term_loc_argtype) = + Genarg.create_arg "subtac_term" + + +VERNAC COMMAND EXTEND SubtacRec + [ "Recursive" "program" ident(id) "(" ident(recid) ":" subtac_spec(rect) ")" ":" subtac_spec(s) ":=" subtac_term(t) ] -> + [ Rewrite.subtac (Some (recid, rect)) id (s, t) ] +END + +VERNAC COMMAND EXTEND Subtac + [ "Program" ident(id) ":" subtac_spec(s) ":=" subtac_term(t) ] -> + [ Rewrite.subtac None id (s, t) ] +END diff --git a/dev/ocamldebug-coq.template b/dev/ocamldebug-coq.template index 96c53192d..30224216c 100644 --- a/dev/ocamldebug-coq.template +++ b/dev/ocamldebug-coq.template @@ -36,6 +36,7 @@ case $coqdebug in -I $COQTOP/contrib/interface -I $COQTOP/contrib/jprover \ -I $COQTOP/contrib/omega -I $COQTOP/contrib/romega \ -I $COQTOP/contrib/ring -I $COQTOP/contrib/xml \ + -I $COQTOP/contrib/subtac \ $* $args;; *) exec $OCAMLDEBUG $*;; esac diff --git a/pretyping/termops.ml b/pretyping/termops.ml index 263f4de13..0eefa2442 100644 --- a/pretyping/termops.ml +++ b/pretyping/termops.ml @@ -101,29 +101,34 @@ let pr_var_decl env (id,c,typ) = | Some c -> (* Force evaluation *) let pb = print_constr_env env c in - (str" := " ++ pb ++ cut () ) in + (str" := " ++ pb ++ cut () ) in let pt = print_constr_env env typ in let ptyp = (str" : " ++ pt) in - (pr_id id ++ hov 0 (pbody ++ ptyp)) -(* + (pr_id id ++ hov 0 (pbody ++ ptyp)) + let pr_rel_decl env (na,c,typ) = let pbody = match c with | None -> mt () | Some c -> (* Force evaluation *) - let pb = prterm_env env c in - (str":=" ++ spc () ++ pb ++ spc ()) in - let ptyp = prtype_env env typ in - match na with - | Anonymous -> hov 0 (str"<>" ++ spc () ++ pbody ++ str":" ++ spc () ++ ptyp) - | Name id -> hov 0 (pr_id id ++ spc () ++ pbody ++ str":" ++ spc () ++ ptyp) -*) + let pb = print_constr_env env c in + (str":=" ++ spc () ++ pb ++ spc ()) in + let ptyp = print_constr_env env typ in + match na with + | Anonymous -> hov 0 (str"<>" ++ spc () ++ pbody ++ str":" ++ spc () ++ ptyp) + | Name id -> hov 0 (pr_id id ++ spc () ++ pbody ++ str":" ++ spc () ++ ptyp) + let print_named_context env = hv 0 (fold_named_context (fun env d pps -> pps ++ ws 2 ++ pr_var_decl env d) env ~init:(mt ())) -(* -let pr_env env = + +let print_rel_context env = + hv 0 (fold_rel_context + (fun env d pps -> pps ++ ws 2 ++ pr_rel_decl env d) + env ~init:(mt ())) + +let print_env env = let sign_env = fold_named_context (fun env d pps -> @@ -136,8 +141,8 @@ let pr_env env = let pnat = pr_rel_decl env d in (pps ++ fnl () ++ pnat)) env ~init:(mt ()) in - (sign_env ++ db_env) -*) + (sign_env ++ db_env) + (*let current_module = ref empty_dirpath let set_module m = current_module := m*) diff --git a/pretyping/termops.mli b/pretyping/termops.mli index 0c491cb43..cd1cce1ba 100644 --- a/pretyping/termops.mli +++ b/pretyping/termops.mli @@ -30,6 +30,8 @@ val set_print_constr : (env -> constr -> std_ppcmds) -> unit val print_constr : constr -> std_ppcmds val print_constr_env : env -> constr -> std_ppcmds val print_named_context : env -> std_ppcmds +val print_rel_context : env -> std_ppcmds +val print_env : env -> std_ppcmds (* iterators on terms *) val prod_it : init:types -> (name * types) list -> types |