diff options
author | filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-03-05 14:11:40 +0000 |
---|---|---|
committer | filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-03-05 14:11:40 +0000 |
commit | c034197e869cdc418b225b9abf25dee63a47e237 (patch) | |
tree | 42b5c9ecc4840c00ac1d31e5caf38b432953f7da | |
parent | 9c88d6021a178cb64360bca75adbb6db030c480f (diff) |
module Explore générique et réécriture EAuto avec ce module; occur check dans clenv_merge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1425 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r-- | .depend | 206 | ||||
-rw-r--r-- | Makefile | 2 | ||||
-rw-r--r-- | dev/top_printers.ml | 1 | ||||
-rw-r--r-- | lib/explore.ml | 87 | ||||
-rw-r--r-- | lib/explore.mli | 43 | ||||
-rw-r--r-- | proofs/clenv.ml | 29 | ||||
-rw-r--r-- | tactics/eauto.ml | 238 |
7 files changed, 371 insertions, 235 deletions
@@ -29,6 +29,8 @@ kernel/typeops.cmi: kernel/environ.cmi kernel/evd.cmi kernel/inductive.cmi \ kernel/names.cmi kernel/sign.cmi kernel/term.cmi kernel/univ.cmi kernel/univ.cmi: kernel/names.cmi lib/pp.cmi lib/pp.cmi: lib/pp_control.cmi +lib/system.cmi: lib/pp.cmi +lib/util.cmi: lib/pp.cmi library/declare.cmi: kernel/cooking.cmi kernel/declarations.cmi \ kernel/environ.cmi kernel/evd.cmi kernel/inductive.cmi \ library/libobject.cmi kernel/names.cmi library/nametab.cmi \ @@ -49,8 +51,6 @@ library/library.cmi: library/lib.cmi library/libobject.cmi kernel/names.cmi \ library/nametab.cmi: library/libobject.cmi kernel/names.cmi lib/pp.cmi \ kernel/term.cmi lib/util.cmi library/summary.cmi: kernel/names.cmi -lib/system.cmi: lib/pp.cmi -lib/util.cmi: lib/pp.cmi parsing/ast.cmi: parsing/coqast.cmi lib/dyn.cmi kernel/names.cmi \ parsing/pcoq.cmi lib/pp.cmi parsing/astterm.cmi: parsing/coqast.cmi kernel/environ.cmi kernel/evd.cmi \ @@ -190,7 +190,7 @@ toplevel/fhimsg.cmi: kernel/environ.cmi kernel/names.cmi lib/pp.cmi \ toplevel/himsg.cmi: kernel/environ.cmi kernel/indtypes.cmi proofs/logic.cmi \ kernel/names.cmi lib/pp.cmi kernel/type_errors.cmi toplevel/metasyntax.cmi: parsing/coqast.cmi parsing/extend.cmi \ - kernel/names.cmi + kernel/names.cmi kernel/term.cmi toplevel/mltop.cmi: library/libobject.cmi kernel/names.cmi toplevel/protectedtoplevel.cmi: lib/pp.cmi toplevel/record.cmi: parsing/coqast.cmi kernel/names.cmi kernel/sign.cmi \ @@ -199,12 +199,12 @@ toplevel/recordobj.cmi: kernel/term.cmi toplevel/searchisos.cmi: library/libobject.cmi kernel/names.cmi \ kernel/term.cmi toplevel/toplevel.cmi: parsing/pcoq.cmi lib/pp.cmi +toplevel/vernac.cmi: parsing/coqast.cmi parsing/pcoq.cmi toplevel/vernacentries.cmi: parsing/coqast.cmi kernel/environ.cmi \ - kernel/names.cmi proofs/proof_type.cmi kernel/term.cmi \ - toplevel/vernacinterp.cmi + kernel/names.cmi library/nametab.cmi proofs/proof_type.cmi \ + kernel/term.cmi toplevel/vernacinterp.cmi toplevel/vernacinterp.cmi: parsing/coqast.cmi lib/dyn.cmi kernel/names.cmi \ - proofs/proof_type.cmi -toplevel/vernac.cmi: parsing/coqast.cmi parsing/pcoq.cmi + library/nametab.cmi proofs/proof_type.cmi contrib/extraction/close_env.cmi: kernel/names.cmi kernel/term.cmi contrib/extraction/extraction.cmi: contrib/extraction/miniml.cmi \ kernel/names.cmi kernel/term.cmi @@ -214,21 +214,21 @@ contrib/extraction/genpp.cmi: contrib/extraction/extraction.cmi \ contrib/extraction/miniml.cmi: kernel/names.cmi lib/pp.cmi kernel/term.cmi contrib/extraction/mlimport.cmi: kernel/names.cmi kernel/term.cmi contrib/extraction/ocaml.cmi: contrib/extraction/miniml.cmi -contrib/xml/xmlcommand.cmi: kernel/names.cmi +contrib/xml/xmlcommand.cmi: kernel/names.cmi library/nametab.cmi config/coq_config.cmo: config/coq_config.cmi config/coq_config.cmx: config/coq_config.cmi dev/db_printers.cmo: kernel/names.cmi lib/pp.cmi dev/db_printers.cmx: kernel/names.cmx lib/pp.cmx dev/top_printers.cmo: parsing/ast.cmi proofs/clenv.cmi kernel/environ.cmi \ - toplevel/errors.cmi kernel/evd.cmi kernel/names.cmi lib/pp.cmi \ - parsing/printer.cmi proofs/proof_trees.cmi proofs/refiner.cmi \ + toplevel/errors.cmi kernel/evd.cmi kernel/names.cmi library/nametab.cmi \ + lib/pp.cmi parsing/printer.cmi proofs/proof_trees.cmi proofs/refiner.cmi \ kernel/sign.cmi lib/system.cmi proofs/tacmach.cmi kernel/term.cmi \ - parsing/termast.cmi kernel/univ.cmi toplevel/vernacinterp.cmi + parsing/termast.cmi kernel/univ.cmi dev/top_printers.cmx: parsing/ast.cmx proofs/clenv.cmx kernel/environ.cmx \ - toplevel/errors.cmx kernel/evd.cmx kernel/names.cmx lib/pp.cmx \ - parsing/printer.cmx proofs/proof_trees.cmx proofs/refiner.cmx \ + toplevel/errors.cmx kernel/evd.cmx kernel/names.cmx library/nametab.cmx \ + lib/pp.cmx parsing/printer.cmx proofs/proof_trees.cmx proofs/refiner.cmx \ kernel/sign.cmx lib/system.cmx proofs/tacmach.cmx kernel/term.cmx \ - parsing/termast.cmx kernel/univ.cmx toplevel/vernacinterp.cmx + parsing/termast.cmx kernel/univ.cmx kernel/closure.cmo: kernel/environ.cmi kernel/esubst.cmi kernel/evd.cmi \ kernel/instantiate.cmi kernel/names.cmi lib/pp.cmi kernel/term.cmi \ kernel/univ.cmi lib/util.cmi kernel/closure.cmi @@ -333,22 +333,32 @@ lib/dyn.cmo: lib/util.cmi lib/dyn.cmi lib/dyn.cmx: lib/util.cmx lib/dyn.cmi lib/edit.cmo: lib/bstack.cmi lib/pp.cmi lib/util.cmi lib/edit.cmi lib/edit.cmx: lib/bstack.cmx lib/pp.cmx lib/util.cmx lib/edit.cmi -lib/gmapl.cmo: lib/gmap.cmi lib/util.cmi lib/gmapl.cmi -lib/gmapl.cmx: lib/gmap.cmx lib/util.cmx lib/gmapl.cmi +lib/explore.cmo: lib/explore.cmi +lib/explore.cmx: lib/explore.cmi lib/gmap.cmo: lib/gmap.cmi lib/gmap.cmx: lib/gmap.cmi +lib/gmapl.cmo: lib/gmap.cmi lib/util.cmi lib/gmapl.cmi +lib/gmapl.cmx: lib/gmap.cmx lib/util.cmx lib/gmapl.cmi lib/gset.cmo: lib/gset.cmi lib/gset.cmx: lib/gset.cmi lib/hashcons.cmo: lib/hashcons.cmi lib/hashcons.cmx: lib/hashcons.cmi lib/options.cmo: lib/util.cmi lib/options.cmi lib/options.cmx: lib/util.cmx lib/options.cmi -lib/pp_control.cmo: lib/pp_control.cmi -lib/pp_control.cmx: lib/pp_control.cmi lib/pp.cmo: lib/pp_control.cmi lib/pp.cmi lib/pp.cmx: lib/pp_control.cmx lib/pp.cmi +lib/pp_control.cmo: lib/pp_control.cmi +lib/pp_control.cmx: lib/pp_control.cmi lib/profile.cmo: lib/profile.cmi lib/profile.cmx: lib/profile.cmi +lib/stamps.cmo: lib/stamps.cmi +lib/stamps.cmx: lib/stamps.cmi +lib/system.cmo: config/coq_config.cmi lib/pp.cmi lib/util.cmi lib/system.cmi +lib/system.cmx: config/coq_config.cmx lib/pp.cmx lib/util.cmx lib/system.cmi +lib/tlm.cmo: lib/gmap.cmi lib/gset.cmi lib/tlm.cmi +lib/tlm.cmx: lib/gmap.cmx lib/gset.cmx lib/tlm.cmi +lib/util.cmo: lib/pp.cmi lib/util.cmi +lib/util.cmx: lib/pp.cmx lib/util.cmi library/declare.cmo: kernel/cooking.cmi kernel/declarations.cmi \ kernel/environ.cmi kernel/evd.cmi library/global.cmi library/impargs.cmi \ library/indrec.cmi kernel/inductive.cmi library/lib.cmi \ @@ -423,14 +433,6 @@ library/summary.cmo: lib/dyn.cmi kernel/names.cmi lib/pp.cmi lib/util.cmi \ library/summary.cmi library/summary.cmx: lib/dyn.cmx kernel/names.cmx lib/pp.cmx lib/util.cmx \ library/summary.cmi -lib/stamps.cmo: lib/stamps.cmi -lib/stamps.cmx: lib/stamps.cmi -lib/system.cmo: config/coq_config.cmi lib/pp.cmi lib/util.cmi lib/system.cmi -lib/system.cmx: config/coq_config.cmx lib/pp.cmx lib/util.cmx lib/system.cmi -lib/tlm.cmo: lib/gmap.cmi lib/gset.cmi lib/tlm.cmi -lib/tlm.cmx: lib/gmap.cmx lib/gset.cmx lib/tlm.cmi -lib/util.cmo: lib/pp.cmi lib/util.cmi -lib/util.cmx: lib/pp.cmx lib/util.cmi parsing/ast.cmo: parsing/coqast.cmi lib/dyn.cmi lib/hashcons.cmi \ kernel/names.cmi parsing/pcoq.cmi lib/pp.cmi lib/util.cmi parsing/ast.cmi parsing/ast.cmx: parsing/coqast.cmx lib/dyn.cmx lib/hashcons.cmx \ @@ -442,7 +444,8 @@ parsing/astterm.cmo: parsing/ast.cmi parsing/coqast.cmi library/declare.cmi \ pretyping/pretype_errors.cmi pretyping/pretyping.cmi \ pretyping/rawterm.cmi kernel/reduction.cmi pretyping/retyping.cmi \ kernel/sign.cmi pretyping/syntax_def.cmi kernel/term.cmi \ - pretyping/typing.cmi kernel/univ.cmi lib/util.cmi parsing/astterm.cmi + parsing/termast.cmi pretyping/typing.cmi kernel/univ.cmi lib/util.cmi \ + parsing/astterm.cmi parsing/astterm.cmx: parsing/ast.cmx parsing/coqast.cmx library/declare.cmx \ kernel/environ.cmx pretyping/evarutil.cmx kernel/evd.cmx \ library/global.cmx library/impargs.cmx kernel/names.cmx \ @@ -450,7 +453,8 @@ parsing/astterm.cmx: parsing/ast.cmx parsing/coqast.cmx library/declare.cmx \ pretyping/pretype_errors.cmx pretyping/pretyping.cmx \ pretyping/rawterm.cmx kernel/reduction.cmx pretyping/retyping.cmx \ kernel/sign.cmx pretyping/syntax_def.cmx kernel/term.cmx \ - pretyping/typing.cmx kernel/univ.cmx lib/util.cmx parsing/astterm.cmi + parsing/termast.cmx pretyping/typing.cmx kernel/univ.cmx lib/util.cmx \ + parsing/astterm.cmi parsing/coqast.cmo: lib/dyn.cmi lib/hashcons.cmi parsing/coqast.cmi parsing/coqast.cmx: lib/dyn.cmx lib/hashcons.cmx parsing/coqast.cmi parsing/coqlib.cmo: library/declare.cmi kernel/evd.cmi library/global.cmi \ @@ -837,24 +841,22 @@ tactics/auto.cmo: parsing/astterm.cmi tactics/btermdn.cmi proofs/clenv.cmi \ kernel/inductive.cmi library/lib.cmi library/libobject.cmi \ library/library.cmi proofs/logic.cmi kernel/names.cmi library/nametab.cmi \ lib/options.cmi pretyping/pattern.cmi proofs/pfedit.cmi lib/pp.cmi \ - pretyping/pretype_errors.cmi parsing/printer.cmi proofs/proof_type.cmi \ - pretyping/rawterm.cmi kernel/reduction.cmi kernel/sign.cmi \ - library/summary.cmi proofs/tacmach.cmi pretyping/tacred.cmi \ - tactics/tacticals.cmi tactics/tactics.cmi kernel/term.cmi \ - pretyping/typing.cmi lib/util.cmi toplevel/vernacinterp.cmi \ - tactics/auto.cmi + parsing/printer.cmi proofs/proof_type.cmi pretyping/rawterm.cmi \ + kernel/reduction.cmi kernel/sign.cmi library/summary.cmi \ + proofs/tacmach.cmi pretyping/tacred.cmi tactics/tacticals.cmi \ + tactics/tactics.cmi kernel/term.cmi pretyping/typing.cmi lib/util.cmi \ + toplevel/vernacinterp.cmi tactics/auto.cmi tactics/auto.cmx: parsing/astterm.cmx tactics/btermdn.cmx proofs/clenv.cmx \ parsing/coqast.cmx library/declare.cmx tactics/dhyp.cmx kernel/evd.cmx \ library/global.cmx tactics/hiddentac.cmx tactics/hipattern.cmx \ kernel/inductive.cmx library/lib.cmx library/libobject.cmx \ library/library.cmx proofs/logic.cmx kernel/names.cmx library/nametab.cmx \ lib/options.cmx pretyping/pattern.cmx proofs/pfedit.cmx lib/pp.cmx \ - pretyping/pretype_errors.cmx parsing/printer.cmx proofs/proof_type.cmx \ - pretyping/rawterm.cmx kernel/reduction.cmx kernel/sign.cmx \ - library/summary.cmx proofs/tacmach.cmx pretyping/tacred.cmx \ - tactics/tacticals.cmx tactics/tactics.cmx kernel/term.cmx \ - pretyping/typing.cmx lib/util.cmx toplevel/vernacinterp.cmx \ - tactics/auto.cmi + parsing/printer.cmx proofs/proof_type.cmx pretyping/rawterm.cmx \ + kernel/reduction.cmx kernel/sign.cmx library/summary.cmx \ + proofs/tacmach.cmx pretyping/tacred.cmx tactics/tacticals.cmx \ + tactics/tactics.cmx kernel/term.cmx pretyping/typing.cmx lib/util.cmx \ + toplevel/vernacinterp.cmx tactics/auto.cmi tactics/autorewrite.cmo: parsing/ast.cmi toplevel/command.cmi \ parsing/coqast.cmi tactics/equality.cmi tactics/hipattern.cmi \ library/lib.cmi library/libobject.cmi kernel/names.cmi lib/pp.cmi \ @@ -892,13 +894,13 @@ tactics/dhyp.cmx: parsing/ast.cmx parsing/astterm.cmx proofs/clenv.cmx \ tactics/dn.cmo: lib/tlm.cmi tactics/dn.cmi tactics/dn.cmx: lib/tlm.cmx tactics/dn.cmi tactics/eauto.cmo: tactics/auto.cmi proofs/clenv.cmi kernel/evd.cmi \ - kernel/instantiate.cmi proofs/logic.cmi kernel/names.cmi \ + lib/explore.cmi kernel/instantiate.cmi proofs/logic.cmi kernel/names.cmi \ pretyping/pattern.cmi lib/pp.cmi proofs/proof_trees.cmi \ proofs/proof_type.cmi kernel/reduction.cmi kernel/sign.cmi \ proofs/tacmach.cmi tactics/tacticals.cmi tactics/tactics.cmi \ kernel/term.cmi lib/util.cmi tactics/eauto.cmx: tactics/auto.cmx proofs/clenv.cmx kernel/evd.cmx \ - kernel/instantiate.cmx proofs/logic.cmx kernel/names.cmx \ + lib/explore.cmx kernel/instantiate.cmx proofs/logic.cmx kernel/names.cmx \ pretyping/pattern.cmx lib/pp.cmx proofs/proof_trees.cmx \ proofs/proof_type.cmx kernel/reduction.cmx kernel/sign.cmx \ proofs/tacmach.cmx tactics/tacticals.cmx tactics/tactics.cmx \ @@ -1061,10 +1063,10 @@ tactics/wcclausenv.cmx: proofs/clenv.cmx kernel/environ.cmx kernel/evd.cmx \ library/global.cmx proofs/logic.cmx kernel/names.cmx lib/pp.cmx \ proofs/proof_trees.cmx kernel/reduction.cmx kernel/sign.cmx \ proofs/tacmach.cmx kernel/term.cmx lib/util.cmx tactics/wcclausenv.cmi -tools/coqdep_lexer.cmo: config/coq_config.cmi -tools/coqdep_lexer.cmx: config/coq_config.cmx tools/coqdep.cmo: config/coq_config.cmi tools/coqdep_lexer.cmo tools/coqdep.cmx: config/coq_config.cmx tools/coqdep_lexer.cmx +tools/coqdep_lexer.cmo: config/coq_config.cmi +tools/coqdep_lexer.cmx: config/coq_config.cmx tools/gallina.cmo: tools/gallina_lexer.cmo tools/gallina.cmx: tools/gallina_lexer.cmx toplevel/class.cmo: pretyping/classops.cmi kernel/declarations.cmi \ @@ -1163,16 +1165,16 @@ toplevel/line_oriented_parser.cmo: toplevel/line_oriented_parser.cmi toplevel/line_oriented_parser.cmx: toplevel/line_oriented_parser.cmi toplevel/metasyntax.cmo: parsing/ast.cmi parsing/astterm.cmi \ parsing/coqast.cmi parsing/egrammar.cmi parsing/esyntax.cmi \ - parsing/extend.cmi library/lib.cmi library/libobject.cmi \ - library/library.cmi kernel/names.cmi parsing/pcoq.cmi lib/pp.cmi \ - library/summary.cmi parsing/termast.cmi lib/util.cmi toplevel/vernac.cmi \ - toplevel/metasyntax.cmi + parsing/extend.cmi library/global.cmi library/lib.cmi \ + library/libobject.cmi library/library.cmi kernel/names.cmi \ + parsing/pcoq.cmi lib/pp.cmi library/summary.cmi parsing/termast.cmi \ + lib/util.cmi toplevel/vernac.cmi toplevel/metasyntax.cmi toplevel/metasyntax.cmx: parsing/ast.cmx parsing/astterm.cmx \ parsing/coqast.cmx parsing/egrammar.cmx parsing/esyntax.cmx \ - parsing/extend.cmx library/lib.cmx library/libobject.cmx \ - library/library.cmx kernel/names.cmx parsing/pcoq.cmx lib/pp.cmx \ - library/summary.cmx parsing/termast.cmx lib/util.cmx toplevel/vernac.cmx \ - toplevel/metasyntax.cmi + parsing/extend.cmx library/global.cmx library/lib.cmx \ + library/libobject.cmx library/library.cmx kernel/names.cmx \ + parsing/pcoq.cmx lib/pp.cmx library/summary.cmx parsing/termast.cmx \ + lib/util.cmx toplevel/vernac.cmx toplevel/metasyntax.cmi toplevel/minicoq.cmo: kernel/declarations.cmi toplevel/fhimsg.cmi \ parsing/g_minicoq.cmi kernel/inductive.cmi kernel/names.cmi lib/pp.cmi \ kernel/safe_typing.cmi kernel/sign.cmi kernel/term.cmi \ @@ -1225,6 +1227,14 @@ toplevel/toplevel.cmx: parsing/ast.cmx toplevel/errors.cmx library/lib.cmx \ toplevel/vernac.cmx toplevel/vernacinterp.cmx toplevel/toplevel.cmi toplevel/usage.cmo: config/coq_config.cmi toplevel/usage.cmi toplevel/usage.cmx: config/coq_config.cmx toplevel/usage.cmi +toplevel/vernac.cmo: parsing/ast.cmi parsing/coqast.cmi \ + toplevel/discharge.cmi library/library.cmi lib/options.cmi \ + parsing/pcoq.cmi proofs/pfedit.cmi lib/pp.cmi library/states.cmi \ + lib/system.cmi lib/util.cmi toplevel/vernacinterp.cmi toplevel/vernac.cmi +toplevel/vernac.cmx: parsing/ast.cmx parsing/coqast.cmx \ + toplevel/discharge.cmx library/library.cmx lib/options.cmx \ + parsing/pcoq.cmx proofs/pfedit.cmx lib/pp.cmx library/states.cmx \ + lib/system.cmx lib/util.cmx toplevel/vernacinterp.cmx toplevel/vernac.cmi toplevel/vernacentries.cmo: parsing/ast.cmi parsing/astterm.cmi \ toplevel/class.cmi pretyping/classops.cmi toplevel/command.cmi \ parsing/coqast.cmi kernel/declarations.cmi library/declare.cmi \ @@ -1233,15 +1243,15 @@ toplevel/vernacentries.cmo: parsing/ast.cmi parsing/astterm.cmi \ library/impargs.cmi library/lib.cmi library/libobject.cmi \ library/library.cmi toplevel/metasyntax.cmi toplevel/mltop.cmi \ kernel/names.cmi library/nametab.cmi lib/options.cmi proofs/pfedit.cmi \ - lib/pp.cmi lib/pp_control.cmi parsing/pretty.cmi \ - pretyping/pretype_errors.cmi parsing/printer.cmi proofs/proof_trees.cmi \ - proofs/proof_type.cmi toplevel/record.cmi toplevel/recordobj.cmi \ - kernel/reduction.cmi proofs/refiner.cmi parsing/search.cmi lib/stamps.cmi \ - library/states.cmi pretyping/syntax_def.cmi lib/system.cmi \ - proofs/tacinterp.cmi proofs/tacmach.cmi pretyping/tacred.cmi \ - proofs/tactic_debug.cmi tactics/tactics.cmi kernel/term.cmi \ - parsing/termast.cmi kernel/typeops.cmi lib/util.cmi \ - toplevel/vernacinterp.cmi toplevel/vernacentries.cmi + lib/pp.cmi lib/pp_control.cmi parsing/pretty.cmi parsing/printer.cmi \ + proofs/proof_trees.cmi proofs/proof_type.cmi toplevel/record.cmi \ + toplevel/recordobj.cmi kernel/reduction.cmi proofs/refiner.cmi \ + parsing/search.cmi lib/stamps.cmi library/states.cmi \ + pretyping/syntax_def.cmi lib/system.cmi proofs/tacinterp.cmi \ + proofs/tacmach.cmi pretyping/tacred.cmi proofs/tactic_debug.cmi \ + tactics/tactics.cmi kernel/term.cmi parsing/termast.cmi \ + kernel/typeops.cmi lib/util.cmi toplevel/vernacinterp.cmi \ + toplevel/vernacentries.cmi toplevel/vernacentries.cmx: parsing/ast.cmx parsing/astterm.cmx \ toplevel/class.cmx pretyping/classops.cmx toplevel/command.cmx \ parsing/coqast.cmx kernel/declarations.cmx library/declare.cmx \ @@ -1250,33 +1260,25 @@ toplevel/vernacentries.cmx: parsing/ast.cmx parsing/astterm.cmx \ library/impargs.cmx library/lib.cmx library/libobject.cmx \ library/library.cmx toplevel/metasyntax.cmx toplevel/mltop.cmx \ kernel/names.cmx library/nametab.cmx lib/options.cmx proofs/pfedit.cmx \ - lib/pp.cmx lib/pp_control.cmx parsing/pretty.cmx \ - pretyping/pretype_errors.cmx parsing/printer.cmx proofs/proof_trees.cmx \ - proofs/proof_type.cmx toplevel/record.cmx toplevel/recordobj.cmx \ - kernel/reduction.cmx proofs/refiner.cmx parsing/search.cmx lib/stamps.cmx \ - library/states.cmx pretyping/syntax_def.cmx lib/system.cmx \ - proofs/tacinterp.cmx proofs/tacmach.cmx pretyping/tacred.cmx \ - proofs/tactic_debug.cmx tactics/tactics.cmx kernel/term.cmx \ - parsing/termast.cmx kernel/typeops.cmx lib/util.cmx \ - toplevel/vernacinterp.cmx toplevel/vernacentries.cmi + lib/pp.cmx lib/pp_control.cmx parsing/pretty.cmx parsing/printer.cmx \ + proofs/proof_trees.cmx proofs/proof_type.cmx toplevel/record.cmx \ + toplevel/recordobj.cmx kernel/reduction.cmx proofs/refiner.cmx \ + parsing/search.cmx lib/stamps.cmx library/states.cmx \ + pretyping/syntax_def.cmx lib/system.cmx proofs/tacinterp.cmx \ + proofs/tacmach.cmx pretyping/tacred.cmx proofs/tactic_debug.cmx \ + tactics/tactics.cmx kernel/term.cmx parsing/termast.cmx \ + kernel/typeops.cmx lib/util.cmx toplevel/vernacinterp.cmx \ + toplevel/vernacentries.cmi toplevel/vernacinterp.cmo: parsing/ast.cmi parsing/astterm.cmi \ toplevel/command.cmi parsing/coqast.cmi lib/dyn.cmi toplevel/himsg.cmi \ kernel/names.cmi library/nametab.cmi lib/options.cmi lib/pp.cmi \ - pretyping/pretype_errors.cmi proofs/proof_type.cmi proofs/tacinterp.cmi \ - lib/util.cmi toplevel/vernacinterp.cmi + proofs/proof_type.cmi proofs/tacinterp.cmi lib/util.cmi \ + toplevel/vernacinterp.cmi toplevel/vernacinterp.cmx: parsing/ast.cmx parsing/astterm.cmx \ toplevel/command.cmx parsing/coqast.cmx lib/dyn.cmx toplevel/himsg.cmx \ kernel/names.cmx library/nametab.cmx lib/options.cmx lib/pp.cmx \ - pretyping/pretype_errors.cmx proofs/proof_type.cmx proofs/tacinterp.cmx \ - lib/util.cmx toplevel/vernacinterp.cmi -toplevel/vernac.cmo: parsing/ast.cmi parsing/coqast.cmi \ - toplevel/discharge.cmi library/library.cmi lib/options.cmi \ - parsing/pcoq.cmi proofs/pfedit.cmi lib/pp.cmi library/states.cmi \ - lib/system.cmi lib/util.cmi toplevel/vernacinterp.cmi toplevel/vernac.cmi -toplevel/vernac.cmx: parsing/ast.cmx parsing/coqast.cmx \ - toplevel/discharge.cmx library/library.cmx lib/options.cmx \ - parsing/pcoq.cmx proofs/pfedit.cmx lib/pp.cmx library/states.cmx \ - lib/system.cmx lib/util.cmx toplevel/vernacinterp.cmx toplevel/vernac.cmi + proofs/proof_type.cmx proofs/tacinterp.cmx lib/util.cmx \ + toplevel/vernacinterp.cmi contrib/extraction/close_env.cmo: kernel/names.cmi kernel/term.cmi \ contrib/extraction/close_env.cmi contrib/extraction/close_env.cmx: kernel/names.cmx kernel/term.cmx \ @@ -1342,31 +1344,37 @@ contrib/omega/coq_omega.cmx: parsing/ast.cmx proofs/clenv.cmx \ contrib/omega/omega.cmo: lib/util.cmi contrib/omega/omega.cmx: lib/util.cmx contrib/ring/quote.cmo: library/declare.cmi library/global.cmi \ - kernel/instantiate.cmi kernel/names.cmi pretyping/pattern.cmi lib/pp.cmi \ - proofs/proof_trees.cmi proofs/proof_type.cmi proofs/tacmach.cmi \ - tactics/tactics.cmi kernel/term.cmi lib/util.cmi + kernel/instantiate.cmi kernel/names.cmi library/nametab.cmi \ + pretyping/pattern.cmi lib/pp.cmi proofs/proof_trees.cmi \ + proofs/proof_type.cmi proofs/tacmach.cmi tactics/tactics.cmi \ + kernel/term.cmi lib/util.cmi contrib/ring/quote.cmx: library/declare.cmx library/global.cmx \ - kernel/instantiate.cmx kernel/names.cmx pretyping/pattern.cmx lib/pp.cmx \ - proofs/proof_trees.cmx proofs/proof_type.cmx proofs/tacmach.cmx \ - tactics/tactics.cmx kernel/term.cmx lib/util.cmx + kernel/instantiate.cmx kernel/names.cmx library/nametab.cmx \ + pretyping/pattern.cmx lib/pp.cmx proofs/proof_trees.cmx \ + proofs/proof_type.cmx proofs/tacmach.cmx tactics/tactics.cmx \ + kernel/term.cmx lib/util.cmx contrib/ring/ring.cmo: parsing/astterm.cmi kernel/closure.cmi \ parsing/coqlib.cmi library/declare.cmi tactics/equality.cmi \ kernel/evd.cmi library/global.cmi tactics/hiddentac.cmi \ tactics/hipattern.cmi library/lib.cmi library/libobject.cmi \ - kernel/names.cmi pretyping/pattern.cmi lib/pp.cmi parsing/printer.cmi \ - proofs/proof_trees.cmi proofs/proof_type.cmi contrib/ring/quote.cmo \ - kernel/reduction.cmi library/summary.cmi proofs/tacmach.cmi \ - pretyping/tacred.cmi tactics/tactics.cmi kernel/term.cmi \ - pretyping/typing.cmi lib/util.cmi toplevel/vernacinterp.cmi + kernel/names.cmi library/nametab.cmi pretyping/pattern.cmi lib/pp.cmi \ + parsing/printer.cmi proofs/proof_trees.cmi proofs/proof_type.cmi \ + contrib/ring/quote.cmo kernel/reduction.cmi library/summary.cmi \ + proofs/tacmach.cmi pretyping/tacred.cmi tactics/tactics.cmi \ + kernel/term.cmi pretyping/typing.cmi lib/util.cmi \ + toplevel/vernacinterp.cmi contrib/ring/ring.cmx: parsing/astterm.cmx kernel/closure.cmx \ parsing/coqlib.cmx library/declare.cmx tactics/equality.cmx \ kernel/evd.cmx library/global.cmx tactics/hiddentac.cmx \ tactics/hipattern.cmx library/lib.cmx library/libobject.cmx \ - kernel/names.cmx pretyping/pattern.cmx lib/pp.cmx parsing/printer.cmx \ - proofs/proof_trees.cmx proofs/proof_type.cmx contrib/ring/quote.cmx \ - kernel/reduction.cmx library/summary.cmx proofs/tacmach.cmx \ - pretyping/tacred.cmx tactics/tactics.cmx kernel/term.cmx \ - pretyping/typing.cmx lib/util.cmx toplevel/vernacinterp.cmx + kernel/names.cmx library/nametab.cmx pretyping/pattern.cmx lib/pp.cmx \ + parsing/printer.cmx proofs/proof_trees.cmx proofs/proof_type.cmx \ + contrib/ring/quote.cmx kernel/reduction.cmx library/summary.cmx \ + proofs/tacmach.cmx pretyping/tacred.cmx tactics/tactics.cmx \ + kernel/term.cmx pretyping/typing.cmx lib/util.cmx \ + toplevel/vernacinterp.cmx +contrib/xml/xml.cmo: contrib/xml/xml.cmi +contrib/xml/xml.cmx: contrib/xml/xml.cmi contrib/xml/xmlcommand.cmo: kernel/declarations.cmi library/declare.cmi \ kernel/environ.cmi kernel/evd.cmi library/global.cmi library/lib.cmi \ library/libobject.cmi library/library.cmi kernel/names.cmi \ @@ -1385,8 +1393,6 @@ contrib/xml/xmlentries.cmo: lib/util.cmi toplevel/vernacinterp.cmi \ contrib/xml/xmlcommand.cmi contrib/xml/xmlentries.cmx: lib/util.cmx toplevel/vernacinterp.cmx \ contrib/xml/xmlcommand.cmx -contrib/xml/xml.cmo: contrib/xml/xml.cmi -contrib/xml/xml.cmx: contrib/xml/xml.cmi tactics/tauto.cmo: parsing/grammar.cma kernel/names.cmo parsing/ast.cmo parsing/g_tactic.cmo parsing/g_constr.cmo parsing/lexer.cmo: parsing/q_coqast.cmo: @@ -65,7 +65,7 @@ CONFIG=config/coq_config.cmo LIB=lib/pp_control.cmo lib/pp.cmo lib/util.cmo \ lib/hashcons.cmo lib/dyn.cmo lib/system.cmo lib/options.cmo \ lib/bstack.cmo lib/edit.cmo lib/stamps.cmo lib/gset.cmo lib/gmap.cmo \ - lib/tlm.cmo lib/bij.cmo lib/gmapl.cmo lib/profile.cmo + lib/tlm.cmo lib/bij.cmo lib/gmapl.cmo lib/profile.cmo lib/explore.cmo KERNEL=kernel/names.cmo kernel/univ.cmo kernel/esubst.cmo kernel/term.cmo \ kernel/sign.cmo kernel/declarations.cmo \ diff --git a/dev/top_printers.ml b/dev/top_printers.ml index 32840e86f..47fb4b48d 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -13,7 +13,6 @@ open Printer open Refiner open Tacmach open Term -open Vernacinterp open Clenv open Errors diff --git a/lib/explore.ml b/lib/explore.ml new file mode 100644 index 000000000..c336a4b3b --- /dev/null +++ b/lib/explore.ml @@ -0,0 +1,87 @@ + +(*i $Id$ i*) + +open Format + +(*s Definition of a search problem. *) + +module type SearchProblem = sig + type state + val branching : state -> state list + val success : state -> bool + val pp : state -> unit +end + +module Make = functor(S : SearchProblem) -> struct + + type position = int list + + let rec pp_position = function + | [] -> () + | [i] -> printf "%d" i + | i :: l -> pp_position l; printf ".%d" i + + (*s Depth first search. *) + + let rec depth_first s = + if S.success s then s else depth_first_many (S.branching s) + and depth_first_many = function + | [] -> raise Not_found + | s :: l -> try depth_first s with Not_found -> depth_first_many l + + let debug_depth_first s = + let rec explore p s = + pp_position p; S.pp s; + if S.success s then s else explore_many 1 p (S.branching s) + and explore_many i p = function + | [] -> + raise Not_found + | s :: l -> + try explore (i::p) s with Not_found -> explore_many (succ i) p l + in + explore [1] s + + (*s Breadth first search. We use functional FIFOS à la Okasaki. *) + + type 'a queue = 'a list * 'a list + + exception Empty + + let empty = [],[] + + let push x (h,t) = (x::h,t) + + let pop = function + | h, x::t -> x, (h,t) + | h, [] -> match List.rev h with x::t -> x, ([],t) | [] -> raise Empty + + let breadth_first s = + let rec explore q = + try + let (s, q') = pop q in enqueue q' (S.branching s) + with Empty -> + raise Not_found + and enqueue q = function + | [] -> explore q + | s :: l -> if S.success s then s else enqueue (push s q) l + in + enqueue empty [s] + + let debug_breadth_first s = + let rec explore q = + try + let ((p,s), q') = pop q in + enqueue 1 p q' (S.branching s) + with Empty -> + raise Not_found + and enqueue i p q = function + | [] -> + explore q + | s :: l -> + let ps = i::p in + pp_position ps; S.pp s; + if S.success s then s else enqueue (succ i) p (push (ps,s) q) l + in + enqueue 1 [] empty [s] + +end diff --git a/lib/explore.mli b/lib/explore.mli new file mode 100644 index 000000000..5f484f8e6 --- /dev/null +++ b/lib/explore.mli @@ -0,0 +1,43 @@ + +(*i $Id$ i*) + +(*s Search strategies. *) + +(*s A search problem implements the following signature [SearchProblem]. + [state] is the type of states of the search tree. + [branching] is the branching function; if [branching s] returns an + empty list, then search from [s] is aborted; successors of [s] are + recursively searched in the order they appear in the list. + [success] determines whether a given state is a success. + + [pp] is a pretty-printer for states used in debugging versions of the + search functions. *) + +module type SearchProblem = sig + + type state + + val branching : state -> state list + + val success : state -> bool + + val pp : state -> unit + +end + +(*s Functor [Make] returns some search functions given a search problem. + Search functions raise [Not_found] if no success is found. + States are always visited in the order they appear in the + output of [branching] (whatever the search method is). + Debugging versions of the search functions print the position of the + visited state together with the state it-self (using [S.pp]). *) + +module Make : functor(S : SearchProblem) -> sig + + val depth_first : S.state -> S.state + val debug_depth_first : S.state -> S.state + + val breadth_first : S.state -> S.state + val debug_breadth_first : S.state -> S.state + +end diff --git a/proofs/clenv.ml b/proofs/clenv.ml index f7ec08030..31555eaa8 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -556,18 +556,23 @@ let clenv_merge with_types = if w_defined_evar clenv.hook evn then let (metas',evars') = unify_0 [] clenv.hook rhs lhs in clenv_resrec (metas'@metas) (evars'@t) clenv - else - (try let rhs' = if occur_meta rhs then subst_meta metas rhs else rhs in - clenv_resrec metas t - (clenv_wtactic (w_Define evn rhs') clenv) - with ex when catchable_exception ex -> - (match krhs with - | IsApp (f,cl) when isConst f or isMutConstruct f -> - clenv_resrec metas evars - (clenv_wtactic - (mimick_evar f (Array.length cl) evn) - clenv) - | _ -> error "w_Unify")) + else begin + let rhs' = + if occur_meta rhs then subst_meta metas rhs else rhs + in + if occur_evar evn rhs' then error "w_Unify"; + try + clenv_resrec metas t + (clenv_wtactic (w_Define evn rhs') clenv) + with ex when catchable_exception ex -> + (match krhs with + | IsApp (f,cl) when isConst f or isMutConstruct f -> + clenv_resrec metas evars + (clenv_wtactic + (mimick_evar f (Array.length cl) evn) + clenv) + | _ -> error "w_Unify") + end | _ -> anomaly "clenv_resrec")) diff --git a/tactics/eauto.ml b/tactics/eauto.ml index f325f5a86..a48f7d3c9 100644 --- a/tactics/eauto.ml +++ b/tactics/eauto.ml @@ -119,7 +119,7 @@ let vernac_prolog = gentac ((Integer n) :: (List.map (fun com -> (Constr com)) coms)) let vernac_instantiate = - hide_tactic "Instantiate" instantiate_tac;; + hide_tactic "Instantiate" instantiate_tac let vernac_normevars = hide_atomic_tactic "NormEvars" normEvars @@ -130,8 +130,6 @@ open Auto (* A tactic similar to Auto, but using EApply, Assumption and e_give_exact *) (***************************************************************************) -(* A registered version of tactics in order to keep a trace *) - let unify_e_resolve (c,clenv) gls = let (wc,kONT) = startWalk gls in let clenv' = connect_clenv wc clenv in @@ -174,12 +172,16 @@ and e_my_find_search db_list local_db hdc concl = | Extern tacast -> Tacticals.conclPattern concl (out_some p) tacast in tac) - (*i fun gls -> pPNL (fmt_autotactic t); flush stdout; + (*i + fun gls -> pPNL (fmt_autotactic t); Format.print_flush (); try tac gls with e when Logic.catchable_exception(e) -> - (print_string "Fail\n"; flush stdout; raise e) - i*) - in List.map tac_of_hint hintl + (Format.print_string "Fail\n"; + Format.print_flush (); + raise e) + i*) + in + List.map tac_of_hint hintl and e_trivial_resolve db_list local_db gl = try @@ -188,132 +190,126 @@ and e_trivial_resolve db_list local_db gl = (List.hd (head_constr_bound gl [])) gl) with Bound | Not_found -> [] -(*** -let vernac_e_trivial - = hide_atomic_tactic "ETrivial" e_trivial_fail -****) - let e_possible_resolve db_list local_db gl = try List.map snd (e_my_find_search db_list local_db (List.hd (head_constr_bound gl [])) gl) with Bound | Not_found -> [] -(* A depth-first version with correct (?) backtracking using operations on lists - of goals *) - let assumption_tac_list id = apply_tac_list (e_give_exact_constr (mkVar id)) -exception Nogoals - let find_first_goal gls = - try first_goal gls with UserError _ -> raise Nogoals - -let rec e_search_depth n db_list local_db lg = - try - let g = find_first_goal lg in - if n = 0 then error "BOUND 2"; - let assumption_tacs = - List.map - (fun id gls -> - then_tactic_list - (assumption_tac_list id) - (e_search_depth n db_list local_db) - gls) - (pf_ids_of_hyps g) - in - let intro_tac = - apply_tac_list - (tclTHEN Tactics.intro - (fun g' -> - let hintl = make_resolve_hyp (pf_env g') (project g') - (pf_last_hyp g') in - (tactic_list_tactic - (e_search_depth n db_list - (Hint_db.add_list hintl local_db))) g')) - in - let rec_tacs = - List.map - (fun ntac lg' -> - (then_tactic_list - (apply_tac_list ntac) - (e_search_depth (n-1) db_list local_db) lg')) - (e_possible_resolve db_list local_db (pf_concl g)) - in - tclFIRSTLIST (assumption_tacs @ (intro_tac :: rec_tacs)) lg - with Nogoals -> - tclIDTAC_list lg - -(* Breadth-first search, a state is [(n,(lgls,val),hintl)] where - [n] is the depth of search before failing - [lgls,val] is a non empty list of remaining goals and the current validation - hintl is a possible hints list to be added to the local hints database (after intro) - we manipulate a FILO of possible states. -*) -type state = {depth : int; - tacres : goal list sigma * validation; - localdb : Auto.Hint_db.t} - -type state_queue = state list * state list - -let empty_queue = ([],[]) - -let push_state s (l1,l2) = (s::l1,l2) - -let decomp_states = function - [],[] -> raise Not_found - | (l1,a::l2)->(a,(l1,l2)) - | (l1,[])-> let l2 = List.rev l1 in (List.hd l2,([],List.tl l2)) - -let add_state n tacr db sl = push_state {depth=n;tacres=tacr;localdb=db} sl - -let e_search (n,p) db_list local_db gl = - let state0 = add_state n (tclIDTAC gl) local_db empty_queue in - let rec process_state stateq = - let (fstate,restq) = try decomp_states stateq - with Not_found -> error "BOUND 2" (* no more states *) - in - let (glls,v) = fstate.tacres - and n = fstate.depth - and local_db = fstate.localdb - in - let rec process_tacs tacl sq = - match tacl with - [] -> (* no more tactics for the goal *) - process_state sq (* continue with next state *) - | (b,tac)::tacrest -> - (try - let (lgls,ptl) = apply_tac_list tac glls in - let v' p = v (ptl p) in - let k = List.length (sig_it lgls) in - if k = 0 then (lgls,v') (* success *) - else let n' = if k < List.length (sig_it glls) or b then n else n-1 in - let hintl = (* possible new hint list for assumptions *) - if b then (* intro tactic *) - let g' = first_goal lgls in - make_resolve_hyp (pf_env g') (project g') (pf_last_hyp g') - else [] - in let ldb = Hint_db.add_list hintl local_db - in if n'=0 then - try - let (lgls1,ptl1) = e_search_depth p db_list ldb lgls - in let v1 p = v' (ptl1 p) in (lgls1,v1) - with e when Logic.catchable_exception e -> process_tacs tacrest sq - else let sq' = add_state n' (lgls, v') ldb sq - in process_tacs tacrest sq' - with e when Logic.catchable_exception e -> process_tacs tacrest sq) - in let g = first_goal glls in - let tac1 = List.map (fun id -> (false, e_give_exact_constr (mkVar id))) (pf_ids_of_hyps g) - and tac2 = (true,Tactics.intro) - and tac3 = List.map (fun tac -> (false,tac)) - (e_possible_resolve db_list local_db (pf_concl g)) - in process_tacs (tac1@tac2::tac3) restq - in process_state state0 + try first_goal gls with UserError _ -> assert false +(*s The following module [SearchProblem] is used to instantiate the generic + exploration functor [Explore.Make]. *) + +module SearchProblem = struct + + type state = { + depth : int; (*r depth of search before failing *) + tacres : goal list sigma * validation; + dblist : Auto.Hint_db.t list; + localdb : Auto.Hint_db.t list } + + let success s = (sig_it (fst s.tacres)) = [] + + let rec filter_tactics (glls,v) = function + | [] -> [] + | tac :: tacl -> + try + let (lgls,ptl) = apply_tac_list tac glls in + let v' p = v (ptl p) in + (lgls,v') :: filter_tactics (glls,v) tacl + with e when Logic.catchable_exception e -> + filter_tactics (glls,v) tacl + + let rec list_addn n x l = + if n = 0 then l else x :: (list_addn (pred n) x l) + + let compare s s' = + let d = s.depth - s'.depth in + let nbgoals s = List.length (sig_it (fst s.tacres)) in + if d <> 0 then d else nbgoals s - nbgoals s' + + let branching s = + if s.depth = 0 then + [] + else + let lg = fst s.tacres in + let nbgl = List.length (sig_it lg) in + assert (nbgl > 0); + let g = find_first_goal lg in + let assumption_tacs = + let l = + filter_tactics s.tacres + (List.map (fun id -> e_give_exact_constr (mkVar id)) + (pf_ids_of_hyps g)) + in + List.map (fun res -> { depth = s.depth; tacres = res; + dblist = s.dblist; + localdb = List.tl s.localdb }) l + in + let intro_tac = + List.map + (fun ((lgls,_) as res) -> + let g' = first_goal lgls in + let hintl = + make_resolve_hyp (pf_env g') (project g') (pf_last_hyp g') + in + let ldb = Hint_db.add_list hintl (List.hd s.localdb) in + { depth = s.depth; tacres = res; dblist = s.dblist; + localdb = ldb :: List.tl s.localdb }) + (filter_tactics s.tacres [Tactics.intro]) + in + let rec_tacs = + let l = + filter_tactics s.tacres + (e_possible_resolve s.dblist (List.hd s.localdb) (pf_concl g)) + in + List.map + (fun ((lgls,_) as res) -> + let nbgl' = List.length (sig_it lgls) in + if nbgl' < nbgl then + { depth = s.depth; tacres = res; + dblist = s.dblist; localdb = List.tl s.localdb } + else + { depth = pred s.depth; tacres = res; dblist = s.dblist; + localdb = + list_addn (nbgl'-nbgl) (List.hd s.localdb) s.localdb }) + l + in + List.sort compare (assumption_tacs @ intro_tac @ rec_tacs) + + let pp s = Format.printf "(depth=%d)\n" s.depth; Format.print_flush () + +end + +module Search = Explore.Make(SearchProblem) + +let make_initial_state n gl dblist localdb = + { SearchProblem.depth = n; + SearchProblem.tacres = tclIDTAC gl; + SearchProblem.dblist = dblist; + SearchProblem.localdb = [localdb] } + +let e_depth_search p db_list local_db gl = + try + let s = Search.depth_first (make_initial_state p gl db_list local_db) in + s.SearchProblem.tacres + with Not_found -> error "EAuto: depth first search failed" + +let e_breadth_search (n,_) db_list local_db gl = + try + let s = Search.breadth_first (make_initial_state n gl db_list local_db) in + s.SearchProblem.tacres + with Not_found -> error "EAuto: breadth first search failed" let e_search_auto (n,p) db_list gl = let local_db = make_local_hint_db gl in - if n = 0 then tactic_list_tactic (e_search_depth p db_list local_db) gl - else e_search (n,p) db_list local_db gl + if n = 0 then + e_depth_search p db_list local_db gl + else + e_breadth_search (n,p) db_list local_db gl let eauto np dbnames = let db_list = |