diff options
| author |  filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-02-27 10:18:49 +0000 |
|---|---|---|
| committer | filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-02-27 10:18:49 +0000 |
| commit | 7499754463892397bc4e9894ad514bea46f2d3ef (patch) | |
| tree | 4fcb574a82c387dcfa0b91deac72f7565906aada | |
| parent | d7df08b56841170443161ed75d5f3a0dbc69e88c (diff) | |
dp: sortie Why
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8099 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | .depend | 368 | ||||
| -rw-r--r-- | Makefile | 6 | ||||
| -rw-r--r-- | contrib/dp/dp.ml | 337 | ||||
| -rw-r--r-- | contrib/dp/dp_why.ml | 123 | ||||
| -rw-r--r-- | contrib/dp/fol.mli | 24 | ||||
| -rw-r--r-- | contrib/dp/tests.v | 4 |
6 files changed, 514 insertions, 348 deletions
@@ -54,12 +54,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/pre_env.cmi: lib/util.cmi kernel/univ.cmi kernel/term.cmi \ kernel/sign.cmi kernel/names.cmi kernel/declarations.cmi @@ -85,9 +85,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/environ.cmi kernel/entries.cmi \ @@ -118,6 +115,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/egrammar.cmi: toplevel/vernacexpr.cmo lib/util.cmi \ interp/topconstr.cmi proofs/tacexpr.cmo pretyping/rawterm.cmi \ interp/ppextend.cmi parsing/pcoq.cmi kernel/names.cmi \ @@ -347,11 +347,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 contrib/cc/ccalgo.cmi: lib/util.cmi kernel/term.cmi lib/pp.cmi \ @@ -360,9 +360,9 @@ contrib/cc/ccproof.cmi: kernel/names.cmi contrib/cc/ccalgo.cmi contrib/cc/cctac.cmi: kernel/term.cmi proofs/proof_type.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 \ @@ -382,8 +382,8 @@ contrib/correctness/ptyping.cmi: interp/topconstr.cmi kernel/term.cmi \ kernel/names.cmi contrib/correctness/putil.cmi: kernel/term.cmi lib/pp.cmi kernel/names.cmi contrib/correctness/pwp.cmi: kernel/term.cmi -contrib/dp/dp.cmi: proofs/proof_type.cmi library/libnames.cmi contrib/dp/dp_cvcl.cmi: contrib/dp/fol.cmi +contrib/dp/dp.cmi: proofs/proof_type.cmi library/libnames.cmi contrib/dp/dp_simplify.cmi: contrib/dp/fol.cmi contrib/dp/dp_sorts.cmi: contrib/dp/fol.cmi contrib/dp/dp_zenon.cmi: contrib/dp/fol.cmi @@ -427,10 +427,10 @@ contrib/first-order/unify.cmi: kernel/term.cmi contrib/funind/indfun_common.cmi: kernel/term.cmi pretyping/rawterm.cmi \ lib/pp.cmi kernel/names.cmi library/libnames.cmi contrib/funind/new_arg_principle.cmi: proofs/tacmach.cmi kernel/names.cmi -contrib/funind/rawterm_to_relation.cmi: interp/topconstr.cmi \ - pretyping/rawterm.cmi kernel/names.cmi contrib/funind/rawtermops.cmi: lib/util.cmi pretyping/rawterm.cmi \ kernel/names.cmi library/libnames.cmi +contrib/funind/rawterm_to_relation.cmi: interp/topconstr.cmi \ + pretyping/rawterm.cmi kernel/names.cmi contrib/funind/tacinvutils.cmi: lib/util.cmi pretyping/termops.cmi \ kernel/term.cmi tactics/tactics.cmi tactics/tacticals.cmi \ proofs/tacmach.cmi tactics/tacinterp.cmi tactics/refine.cmi \ @@ -511,6 +511,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 +543,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 @@ -721,6 +721,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/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/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 \ @@ -735,14 +743,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/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/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/modops.cmi kernel/names.cmo: lib/util.cmi lib/predicate.cmi lib/pp.cmi lib/hashcons.cmi \ kernel/names.cmi kernel/names.cmx: lib/util.cmx lib/predicate.cmx lib/pp.cmx lib/hashcons.cmx \ @@ -841,10 +841,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 @@ -853,26 +853,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/decl_kinds.cmo: lib/util.cmi -library/decl_kinds.cmx: lib/util.cmx 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 \ @@ -905,6 +893,8 @@ library/declaremods.cmx: lib/util.cmx library/summary.cmx \ library/libobject.cmx library/libnames.cmx library/lib.cmx \ library/global.cmx kernel/environ.cmx kernel/entries.cmx \ kernel/declarations.cmx library/declaremods.cmi +library/decl_kinds.cmo: lib/util.cmi +library/decl_kinds.cmx: lib/util.cmx library/dischargedhypsmap.cmo: lib/util.cmi kernel/term.cmi \ library/summary.cmi kernel/reduction.cmi library/nametab.cmi \ kernel/names.cmi library/libobject.cmi library/libnames.cmi \ @@ -987,6 +977,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 @@ -2059,8 +2059,6 @@ tactics/termdn.cmx: lib/util.cmx kernel/term.cmx pretyping/rawterm.cmx \ pretyping/pattern.cmx library/nametab.cmx kernel/names.cmx \ library/nameops.cmx library/libnames.cmx tactics/dn.cmx \ tactics/termdn.cmi -test-suite/zarith.cmo: test-suite/zarith.cmi -test-suite/zarith.cmx: test-suite/zarith.cmi tools/coqdep.cmo: tools/coqdep_lexer.cmo config/coq_config.cmi tools/coqdep.cmx: tools/coqdep_lexer.cmx config/coq_config.cmx tools/gallina.cmo: tools/gallina_lexer.cmo @@ -2247,16 +2245,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 lib/system.cmi library/states.cmi \ - parsing/ppvernac.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 interp/constrintern.cmi toplevel/vernac.cmi -toplevel/vernac.cmx: toplevel/vernacinterp.cmx toplevel/vernacexpr.cmx \ - toplevel/vernacentries.cmx lib/util.cmx lib/system.cmx library/states.cmx \ - parsing/ppvernac.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 interp/constrintern.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 pretyping/termops.cmi \ @@ -2317,6 +2305,16 @@ toplevel/vernacinterp.cmx: toplevel/vernacexpr.cmx lib/util.cmx \ tactics/tacinterp.cmx proofs/tacexpr.cmx proofs/proof_type.cmx lib/pp.cmx \ lib/options.cmx kernel/names.cmx library/libnames.cmx toplevel/himsg.cmx \ toplevel/vernacinterp.cmi +toplevel/vernac.cmo: toplevel/vernacinterp.cmi toplevel/vernacexpr.cmo \ + toplevel/vernacentries.cmi lib/util.cmi lib/system.cmi library/states.cmi \ + parsing/ppvernac.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 interp/constrintern.cmi toplevel/vernac.cmi +toplevel/vernac.cmx: toplevel/vernacinterp.cmx toplevel/vernacexpr.cmx \ + toplevel/vernacentries.cmx lib/util.cmx lib/system.cmx library/states.cmx \ + parsing/ppvernac.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 interp/constrintern.cmx toplevel/vernac.cmi toplevel/whelp.cmo: toplevel/vernacinterp.cmi lib/util.cmi \ pretyping/termops.cmi kernel/term.cmi proofs/tacmach.cmi lib/system.cmi \ interp/syntax_def.cmi proofs/refiner.cmi pretyping/rawterm.cmi lib/pp.cmi \ @@ -2367,6 +2365,12 @@ contrib/cc/g_congruence.cmx: lib/util.cmx tactics/tactics.cmx \ proofs/refiner.cmx parsing/pptactic.cmx lib/pp.cmx parsing/pcoq.cmx \ interp/genarg.cmx parsing/egrammar.cmx toplevel/cerrors.cmx \ contrib/cc/cctac.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 \ @@ -2381,12 +2385,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 @@ -2507,30 +2505,30 @@ contrib/correctness/pwp.cmx: lib/util.cmx pretyping/termops.cmx \ library/nametab.cmx kernel/names.cmx library/libnames.cmx \ tactics/hipattern.cmx library/global.cmx kernel/environ.cmx \ contrib/correctness/pwp.cmi +contrib/dp/dp_cvcl.cmo: contrib/dp/fol.cmi contrib/dp/dp_cvcl.cmi +contrib/dp/dp_cvcl.cmx: contrib/dp/fol.cmi contrib/dp/dp_cvcl.cmi contrib/dp/dp.cmo: lib/util.cmi pretyping/typing.cmi pretyping/termops.cmi \ kernel/term.cmi tactics/tactics.cmi tactics/tacticals.cmi \ proofs/tacmach.cmi library/summary.cmi parsing/printer.cmi lib/pp.cmi \ library/nametab.cmi kernel/names.cmi library/nameops.cmi \ library/libnames.cmi tactics/hipattern.cmi library/global.cmi \ contrib/dp/fol.cmi pretyping/evd.cmi kernel/environ.cmi \ - contrib/dp/dp_zenon.cmi contrib/dp/dp_sorts.cmi \ - contrib/dp/dp_simplify.cmi contrib/dp/dp_cvcl.cmi kernel/declarations.cmi \ - interp/coqlib.cmi contrib/dp/dp.cmi + contrib/dp/dp_why.cmo kernel/declarations.cmi interp/coqlib.cmi \ + contrib/dp/dp.cmi contrib/dp/dp.cmx: lib/util.cmx pretyping/typing.cmx pretyping/termops.cmx \ kernel/term.cmx tactics/tactics.cmx tactics/tacticals.cmx \ proofs/tacmach.cmx library/summary.cmx parsing/printer.cmx lib/pp.cmx \ library/nametab.cmx kernel/names.cmx library/nameops.cmx \ library/libnames.cmx tactics/hipattern.cmx library/global.cmx \ contrib/dp/fol.cmi pretyping/evd.cmx kernel/environ.cmx \ - contrib/dp/dp_zenon.cmx contrib/dp/dp_sorts.cmx \ - contrib/dp/dp_simplify.cmx contrib/dp/dp_cvcl.cmx kernel/declarations.cmx \ - interp/coqlib.cmx contrib/dp/dp.cmi -contrib/dp/dp_cvcl.cmo: contrib/dp/fol.cmi contrib/dp/dp_cvcl.cmi -contrib/dp/dp_cvcl.cmx: contrib/dp/fol.cmi contrib/dp/dp_cvcl.cmi + contrib/dp/dp_why.cmx kernel/declarations.cmx interp/coqlib.cmx \ + contrib/dp/dp.cmi contrib/dp/dp_simplify.cmo: contrib/dp/fol.cmi contrib/dp/dp_simplify.cmi contrib/dp/dp_simplify.cmx: contrib/dp/fol.cmi contrib/dp/dp_simplify.cmi contrib/dp/dp_sorts.cmo: contrib/dp/fol.cmi contrib/dp/dp_sorts.cmi contrib/dp/dp_sorts.cmx: contrib/dp/fol.cmi contrib/dp/dp_sorts.cmi +contrib/dp/dp_why.cmo: contrib/dp/fol.cmi +contrib/dp/dp_why.cmx: contrib/dp/fol.cmi contrib/dp/dp_zenon.cmo: lib/util.cmi contrib/dp/fol.cmi \ contrib/dp/dp_zenon.cmi contrib/dp/dp_zenon.cmx: lib/util.cmx contrib/dp/fol.cmi \ @@ -2801,24 +2799,6 @@ contrib/fourier/g_fourier.cmx: lib/util.cmx tactics/tacinterp.cmx \ proofs/tacexpr.cmx proofs/refiner.cmx parsing/pptactic.cmx lib/pp.cmx \ parsing/pcoq.cmx contrib/fourier/fourierR.cmx parsing/egrammar.cmx \ toplevel/cerrors.cmx -contrib/funind/indfun.cmo: toplevel/vernacexpr.cmo lib/util.cmi \ - interp/topconstr.cmi kernel/term.cmi proofs/tacmach.cmi \ - library/states.cmi contrib/recdef/recdef.cmo \ - contrib/funind/rawterm_to_relation.cmi pretyping/rawterm.cmi lib/pp.cmi \ - lib/options.cmi interp/notation.cmi contrib/funind/new_arg_principle.cmi \ - kernel/names.cmi library/libnames.cmi pretyping/indrec.cmi \ - contrib/funind/indfun_common.cmi library/impargs.cmi library/global.cmi \ - pretyping/evd.cmi kernel/environ.cmi library/decl_kinds.cmo \ - interp/constrintern.cmi toplevel/command.cmi -contrib/funind/indfun.cmx: toplevel/vernacexpr.cmx lib/util.cmx \ - interp/topconstr.cmx kernel/term.cmx proofs/tacmach.cmx \ - library/states.cmx contrib/recdef/recdef.cmx \ - contrib/funind/rawterm_to_relation.cmx pretyping/rawterm.cmx lib/pp.cmx \ - lib/options.cmx interp/notation.cmx contrib/funind/new_arg_principle.cmx \ - kernel/names.cmx library/libnames.cmx pretyping/indrec.cmx \ - contrib/funind/indfun_common.cmx library/impargs.cmx library/global.cmx \ - pretyping/evd.cmx kernel/environ.cmx library/decl_kinds.cmx \ - interp/constrintern.cmx toplevel/command.cmx contrib/funind/indfun_common.cmo: lib/util.cmi pretyping/termops.cmi \ kernel/term.cmi pretyping/rawterm.cmi lib/pp.cmi library/nametab.cmi \ kernel/names.cmi library/libnames.cmi library/global.cmi \ @@ -2849,6 +2829,24 @@ contrib/funind/indfun_main.cmx: toplevel/vernacinterp.cmx lib/util.cmx \ contrib/funind/indfun.cmx tactics/hiddentac.cmx library/global.cmx \ interp/genarg.cmx parsing/egrammar.cmx kernel/declarations.cmx \ toplevel/cerrors.cmx +contrib/funind/indfun.cmo: toplevel/vernacexpr.cmo lib/util.cmi \ + interp/topconstr.cmi kernel/term.cmi proofs/tacmach.cmi \ + library/states.cmi contrib/recdef/recdef.cmo \ + contrib/funind/rawterm_to_relation.cmi pretyping/rawterm.cmi lib/pp.cmi \ + lib/options.cmi interp/notation.cmi contrib/funind/new_arg_principle.cmi \ + kernel/names.cmi library/libnames.cmi pretyping/indrec.cmi \ + contrib/funind/indfun_common.cmi library/impargs.cmi library/global.cmi \ + pretyping/evd.cmi kernel/environ.cmi library/decl_kinds.cmo \ + interp/constrintern.cmi toplevel/command.cmi +contrib/funind/indfun.cmx: toplevel/vernacexpr.cmx lib/util.cmx \ + interp/topconstr.cmx kernel/term.cmx proofs/tacmach.cmx \ + library/states.cmx contrib/recdef/recdef.cmx \ + contrib/funind/rawterm_to_relation.cmx pretyping/rawterm.cmx lib/pp.cmx \ + lib/options.cmx interp/notation.cmx contrib/funind/new_arg_principle.cmx \ + kernel/names.cmx library/libnames.cmx pretyping/indrec.cmx \ + contrib/funind/indfun_common.cmx library/impargs.cmx library/global.cmx \ + pretyping/evd.cmx kernel/environ.cmx library/decl_kinds.cmx \ + interp/constrintern.cmx toplevel/command.cmx contrib/funind/invfun.cmo: lib/util.cmi kernel/term.cmi tactics/tactics.cmi \ tactics/tacticals.cmi proofs/tacmach.cmi contrib/funind/tacinvutils.cmi \ kernel/sign.cmi pretyping/rawterm.cmi lib/pp.cmi kernel/names.cmi \ @@ -2893,6 +2891,18 @@ contrib/funind/new_arg_principle.cmx: toplevel/vernacexpr.cmx \ toplevel/command.cmx kernel/closure.cmx pretyping/clenv.cmx \ toplevel/cerrors.cmx contrib/cc/cctac.cmx \ contrib/funind/new_arg_principle.cmi +contrib/funind/rawtermops.cmo: lib/util.cmi proofs/tactic_debug.cmi \ + tactics/tacinterp.cmi pretyping/rawterm.cmi parsing/printer.cmi \ + parsing/ppconstr.cmi lib/pp.cmi kernel/names.cmi library/nameops.cmi \ + library/libnames.cmi pretyping/inductiveops.cmi \ + contrib/funind/indfun_common.cmi library/global.cmi pretyping/evd.cmi \ + interp/coqlib.cmi contrib/funind/rawtermops.cmi +contrib/funind/rawtermops.cmx: lib/util.cmx proofs/tactic_debug.cmx \ + tactics/tacinterp.cmx pretyping/rawterm.cmx parsing/printer.cmx \ + parsing/ppconstr.cmx lib/pp.cmx kernel/names.cmx library/nameops.cmx \ + library/libnames.cmx pretyping/inductiveops.cmx \ + contrib/funind/indfun_common.cmx library/global.cmx pretyping/evd.cmx \ + interp/coqlib.cmx contrib/funind/rawtermops.cmi contrib/funind/rawterm_to_relation.cmo: toplevel/vernacexpr.cmo lib/util.cmi \ interp/topconstr.cmi kernel/term.cmi contrib/funind/rawtermops.cmi \ pretyping/rawterm.cmi parsing/printer.cmi parsing/ppvernac.cmi lib/pp.cmi \ @@ -2907,18 +2917,6 @@ contrib/funind/rawterm_to_relation.cmx: toplevel/vernacexpr.cmx lib/util.cmx \ contrib/funind/indfun_common.cmx library/impargs.cmx interp/coqlib.cmx \ interp/constrextern.cmx toplevel/command.cmx toplevel/cerrors.cmx \ contrib/funind/rawterm_to_relation.cmi -contrib/funind/rawtermops.cmo: lib/util.cmi proofs/tactic_debug.cmi \ - tactics/tacinterp.cmi pretyping/rawterm.cmi parsing/printer.cmi \ - parsing/ppconstr.cmi lib/pp.cmi kernel/names.cmi library/nameops.cmi \ - library/libnames.cmi pretyping/inductiveops.cmi \ - contrib/funind/indfun_common.cmi library/global.cmi pretyping/evd.cmi \ - interp/coqlib.cmi contrib/funind/rawtermops.cmi -contrib/funind/rawtermops.cmx: lib/util.cmx proofs/tactic_debug.cmx \ - tactics/tacinterp.cmx pretyping/rawterm.cmx parsing/printer.cmx \ - parsing/ppconstr.cmx lib/pp.cmx kernel/names.cmx library/nameops.cmx \ - library/libnames.cmx pretyping/inductiveops.cmx \ - contrib/funind/indfun_common.cmx library/global.cmx pretyping/evd.cmx \ - interp/coqlib.cmx contrib/funind/rawtermops.cmi contrib/funind/tacinv.cmo: toplevel/vernacinterp.cmi lib/util.cmi \ pretyping/typing.cmi pretyping/termops.cmi kernel/term.cmi \ tactics/tactics.cmi tactics/tacticals.cmi pretyping/tacred.cmi \ @@ -3115,6 +3113,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 \ + 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 \ + contrib/interface/ascent.cmi contrib/interface/showproof.cmo: toplevel/vernacinterp.cmi lib/util.cmi \ pretyping/typing.cmi contrib/interface/translate.cmi \ pretyping/termops.cmi kernel/term.cmi proofs/tacmach.cmi \ @@ -3137,14 +3143,6 @@ contrib/interface/showproof.cmx: toplevel/vernacinterp.cmx lib/util.cmx \ interp/genarg.cmx pretyping/evd.cmx kernel/environ.cmx \ kernel/declarations.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 \ - 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 \ - contrib/interface/ascent.cmi contrib/interface/translate.cmo: contrib/interface/xlate.cmi \ contrib/interface/vtp.cmi toplevel/vernacinterp.cmi lib/util.cmi \ kernel/term.cmi proofs/tacmach.cmi kernel/sign.cmi proofs/proof_type.cmi \ @@ -3491,18 +3489,12 @@ contrib/subtac/subtac_coercion.cmx: lib/util.cmx kernel/typeops.cmx \ interp/coqlib.cmx contrib/subtac/context.cmx pretyping/classops.cmx contrib/subtac/subtac_errors.cmo: lib/util.cmi parsing/printer.cmi lib/pp.cmi contrib/subtac/subtac_errors.cmx: lib/util.cmx parsing/printer.cmx lib/pp.cmx -contrib/xml/acic.cmo: kernel/term.cmi kernel/names.cmi -contrib/xml/acic.cmx: kernel/term.cmx kernel/names.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 \ @@ -3521,6 +3513,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 \ @@ -3561,8 +3559,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 \ pretyping/recordops.cmi proofs/proof_trees.cmi \ @@ -3593,10 +3589,8 @@ contrib/xml/xmlentries.cmx: contrib/xml/xmlcommand.cmx \ toplevel/vernacinterp.cmx lib/util.cmx lib/pp.cmx parsing/pcoq.cmx \ parsing/lexer.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 @@ -3607,6 +3601,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 \ @@ -3732,102 +3730,58 @@ 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/config.h \ - /home/logical/local//lib/ocaml/caml/mlvalues.h \ - /home/logical/local//lib/ocaml/caml/misc.h \ - /home/logical/local//lib/ocaml/caml/fail.h \ - /home/logical/local//lib/ocaml/caml/mlvalues.h \ - /home/logical/local//lib/ocaml/caml/memory.h \ + /usr/lib/ocaml/3.08/caml/config.h \ + /usr/lib/ocaml/3.08/caml/compatibility.h \ + /usr/lib/ocaml/3.08/caml/misc.h /usr/lib/ocaml/3.08/caml/mlvalues.h \ + /usr/lib/ocaml/3.08/caml/fail.h /usr/lib/ocaml/3.08/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 \ - /home/logical/local//lib/ocaml/caml/mlvalues.h \ - kernel/byterun/coq_instruct.h kernel/byterun/coq_fix_code.h \ - kernel/byterun/coq_memory.h \ - /home/logical/local//lib/ocaml/caml/config.h \ - /home/logical/local//lib/ocaml/caml/fail.h \ - /home/logical/local//lib/ocaml/caml/misc.h \ - /home/logical/local//lib/ocaml/caml/memory.h \ + /usr/lib/ocaml/3.08/caml/mlvalues.h \ + /usr/lib/ocaml/3.08/caml/compatibility.h \ + /usr/lib/ocaml/3.08/caml/config.h /usr/lib/ocaml/3.08/caml/misc.h \ + /usr/lib/ocaml/3.08/caml/alloc.h kernel/byterun/coq_instruct.h \ + kernel/byterun/coq_fix_code.h kernel/byterun/coq_memory.h \ + /usr/lib/ocaml/3.08/caml/fail.h /usr/lib/ocaml/3.08/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 \ - /home/logical/local//lib/ocaml/caml/mlvalues.h \ - kernel/byterun/coq_instruct.h kernel/byterun/coq_fix_code.h \ - kernel/byterun/coq_memory.h \ - /home/logical/local//lib/ocaml/caml/config.h \ - /home/logical/local//lib/ocaml/caml/fail.h \ - /home/logical/local//lib/ocaml/caml/misc.h \ - /home/logical/local//lib/ocaml/caml/memory.h + /usr/lib/ocaml/3.08/caml/mlvalues.h \ + /usr/lib/ocaml/3.08/caml/compatibility.h \ + /usr/lib/ocaml/3.08/caml/config.h /usr/lib/ocaml/3.08/caml/misc.h \ + /usr/lib/ocaml/3.08/caml/alloc.h kernel/byterun/coq_instruct.h \ + kernel/byterun/coq_fix_code.h kernel/byterun/coq_memory.h \ + /usr/lib/ocaml/3.08/caml/fail.h /usr/lib/ocaml/3.08/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 \ + /usr/lib/ocaml/3.08/caml/mlvalues.h \ + /usr/lib/ocaml/3.08/caml/compatibility.h \ + /usr/lib/ocaml/3.08/caml/config.h /usr/lib/ocaml/3.08/caml/misc.h \ kernel/byterun/coq_instruct.h kernel/byterun/coq_memory.h \ - /home/logical/local//lib/ocaml/caml/config.h \ - /home/logical/local//lib/ocaml/caml/fail.h \ - /home/logical/local//lib/ocaml/caml/mlvalues.h \ - /home/logical/local//lib/ocaml/caml/misc.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/3.08/caml/fail.h /usr/lib/ocaml/3.08/caml/memory.h \ + kernel/byterun/coq_values.h /usr/lib/ocaml/3.08/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/config.h \ - /home/logical/local//lib/ocaml/caml/mlvalues.h \ - /home/logical/local//lib/ocaml/caml/misc.h \ - /home/logical/local//lib/ocaml/caml/fail.h \ - /home/logical/local//lib/ocaml/caml/mlvalues.h \ - /home/logical/local//lib/ocaml/caml/memory.h \ + /usr/lib/ocaml/3.08/caml/config.h \ + /usr/lib/ocaml/3.08/caml/compatibility.h \ + /usr/lib/ocaml/3.08/caml/misc.h /usr/lib/ocaml/3.08/caml/mlvalues.h \ + /usr/lib/ocaml/3.08/caml/fail.h /usr/lib/ocaml/3.08/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 \ - /home/logical/local//lib/ocaml/caml/mlvalues.h \ - kernel/byterun/coq_instruct.h kernel/byterun/coq_fix_code.h \ - kernel/byterun/coq_memory.h \ - /home/logical/local//lib/ocaml/caml/config.h \ - /home/logical/local//lib/ocaml/caml/fail.h \ - /home/logical/local//lib/ocaml/caml/misc.h \ - /home/logical/local//lib/ocaml/caml/memory.h \ + /usr/lib/ocaml/3.08/caml/mlvalues.h \ + /usr/lib/ocaml/3.08/caml/compatibility.h \ + /usr/lib/ocaml/3.08/caml/config.h /usr/lib/ocaml/3.08/caml/misc.h \ + /usr/lib/ocaml/3.08/caml/alloc.h kernel/byterun/coq_instruct.h \ + kernel/byterun/coq_fix_code.h kernel/byterun/coq_memory.h \ + /usr/lib/ocaml/3.08/caml/fail.h /usr/lib/ocaml/3.08/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 \ - /home/logical/local//lib/ocaml/caml/mlvalues.h \ - kernel/byterun/coq_instruct.h kernel/byterun/coq_fix_code.h \ - kernel/byterun/coq_memory.h \ - /home/logical/local//lib/ocaml/caml/config.h \ - /home/logical/local//lib/ocaml/caml/fail.h \ - /home/logical/local//lib/ocaml/caml/misc.h \ - /home/logical/local//lib/ocaml/caml/memory.h + /usr/lib/ocaml/3.08/caml/mlvalues.h \ + /usr/lib/ocaml/3.08/caml/compatibility.h \ + /usr/lib/ocaml/3.08/caml/config.h /usr/lib/ocaml/3.08/caml/misc.h \ + /usr/lib/ocaml/3.08/caml/alloc.h kernel/byterun/coq_instruct.h \ + kernel/byterun/coq_fix_code.h kernel/byterun/coq_memory.h \ + /usr/lib/ocaml/3.08/caml/fail.h /usr/lib/ocaml/3.08/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 \ + /usr/lib/ocaml/3.08/caml/mlvalues.h \ + /usr/lib/ocaml/3.08/caml/compatibility.h \ + /usr/lib/ocaml/3.08/caml/config.h /usr/lib/ocaml/3.08/caml/misc.h \ kernel/byterun/coq_instruct.h kernel/byterun/coq_memory.h \ - /home/logical/local//lib/ocaml/caml/config.h \ - /home/logical/local//lib/ocaml/caml/fail.h \ - /home/logical/local//lib/ocaml/caml/mlvalues.h \ - /home/logical/local//lib/ocaml/caml/misc.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/3.08/caml/fail.h /usr/lib/ocaml/3.08/caml/memory.h \ + kernel/byterun/coq_values.h /usr/lib/ocaml/3.08/caml/alloc.h @@ -236,9 +236,9 @@ RINGCMO=\ NEWRINGCMO=\ contrib/setoid_ring/newring.cmo -DPCMO=\ - contrib/dp/dp_simplify.cmo contrib/dp/dp_zenon.cmo contrib/dp/dp_cvcl.cmo \ - contrib/dp/dp_sorts.cmo contrib/dp/dp.cmo contrib/dp/g_dp.cmo +DPCMO=contrib/dp/dp_why.cmo contrib/dp/dp.cmo contrib/dp/g_dp.cmo +# contrib/dp/dp_simplify.cmo contrib/dp/dp_zenon.cmo contrib/dp/dp_cvcl.cmo \ +# contrib/dp/dp_sorts.cmo FIELDCMO=\ contrib/field/field.cmo diff --git a/contrib/dp/dp.ml b/contrib/dp/dp.ml index 32b39b03d..a9d450f75 100644 --- a/contrib/dp/dp.ml +++ b/contrib/dp/dp.ml @@ -1,6 +1,15 @@ -(* Author : Nicolas Ayache and Jean-Christophe Filliātre *) -(* Goal : Tactics to call decision procedures *) +(* Authors: Nicolas Ayache and Jean-Christophe Filliātre *) +(* Tactics to call decision procedures *) +(* Works in two steps: + + - first the Coq context and the current goal are translated in + Polymorphic First-Order Logic (see fol.mli in this directory) + + - then the resulting query is passed to the Why tool that translates + it to the syntax of the selected prover (Simplify, CVC Lite, haRVey, + Zenon) +*) open Util open Pp @@ -22,7 +31,7 @@ let coq_modules = init_modules @ [logic_dir] @ arith_modules @ zarith_base_modules @ [["Coq"; "omega"; "OmegaLemmas"]] -let constant = gen_constant_in_modules "Omega" coq_modules +let constant = gen_constant_in_modules "dp" coq_modules let coq_Z = lazy (constant "Z") let coq_Zplus = lazy (constant "Zplus") @@ -89,6 +98,39 @@ let coq_rename_vars env vars = id :: newvars, Environ.push_named (id, None, t) newenv) vars ([],env) +(* extract the prenex type quantifications i.e. + type_quantifiers env (A1:Set)...(Ak:Set)t = A1...An, (env+Ai), t *) +let decomp_type_quantifiers env t = + let rec loop vars t = match kind_of_term t with + | Prod (n, a, t) when is_Set a -> + loop ((n,a) :: vars) t + | _ -> + let vars, env = coq_rename_vars env vars in + let t = substl (List.map mkVar vars) t in + List.rev vars, env, t + in + loop [] t + +(* same thing with lambda binders (for axiomatize body) *) +let decomp_type_lambdas env t = + let rec loop vars t = match kind_of_term t with + | Lambda (n, a, t) when is_Set a -> + loop ((n,a) :: vars) t + | _ -> + let vars, env = coq_rename_vars env vars in + let t = substl (List.map mkVar vars) t in + List.rev vars, env, t + in + loop [] t + +let decompose_arrows = + let rec arrows_rec l c = match kind_of_term c with + | Prod (_,t,c) when not (dependent (mkRel 1) c) -> arrows_rec (t :: l) c + | Cast (c,_,_) -> arrows_rec l c + | _ -> List.rev l, c + in + arrows_rec [] + let rec eta_expanse t vars env i = assert (i >= 0); if i = 0 then @@ -104,9 +146,14 @@ let rec eta_expanse t vars env i = | _ -> assert false +let rec skip_k_args k cl = match k, cl with + | 0, _ -> cl + | _, _ :: cl -> skip_k_args (k-1) cl + | _, [] -> raise NotFO + (* Coq global references *) -type global = Gnot_fo | Gfo of Fol.hyp +type global = Gnot_fo | Gfo of Fol.decl let globals = ref Refmap.empty let globals_stack = ref [] @@ -159,7 +206,7 @@ let injection c l = let f = Imp (Fatom (Eq (App (c, vars xl), App (c, vars yl))), f) in let foralls = List.fold_right (fun (x,t) p -> Forall (x, t, p)) in let f = foralls xl (foralls yl f) in - let ax = Assert ("injection_" ^ c, f) in + let ax = Axiom ("injection_" ^ c, f) in globals_stack := ax :: !globals_stack (* rec_names_for c [|n1;...;nk|] builds the list of constant names for @@ -184,28 +231,53 @@ let term_abstractions = Hashtbl.create 97 let new_abstraction = let r = ref 0 in fun () -> incr r; "abstraction_" ^ string_of_int !r -(* assumption : p:Z *) -let rec fol_term_of_positive env p = +(* translates a Coq term p:positive into a FOL term of type int *) +let rec fol_term_of_positive tv env p = match kind_of_term p with | Term.Construct _ when p = Lazy.force coq_xH -> Cst 1 | Term.App (f, [|a|]) when f = Lazy.force coq_xI -> - Plus (Mult (Cst 2, (fol_term_of_positive env a)), Cst 1) + Plus (Mult (Cst 2, (fol_term_of_positive tv env a)), Cst 1) | Term.App (f, [|a|]) when f = Lazy.force coq_xO -> - Mult (Cst 2, (fol_term_of_positive env a)) + Mult (Cst 2, (fol_term_of_positive tv env a)) | Var id -> Fol.App (string_of_id id, []) | _ -> - tr_term [] env p + tr_term tv [] env p + +(* translate a Coq term t:Set into a FOL type expression; + tv = list of type variables *) +and tr_type tv env t = + if t = Lazy.force coq_Z then + Tid ("int", []) + else match kind_of_term t with + | Var x when List.mem x tv -> + Tvar (string_of_id x) + | _ -> + let f, cl = decompose_app t in + begin try + let r = global_of_constr f in + match tr_global env r with + | DeclType (id, k) -> + assert (k = List.length cl); (* since t:Set *) + Tid (id, List.map (tr_type tv env) cl) + | _ -> + raise NotFO + with + | Not_found -> + raise NotFO + | NotFO -> + (* we need to abstract some part of (f cl) *) + (*TODO*) + raise NotFO + end -(* assumption: t:Set or Type *) -and tr_type env ty = - if ty = Lazy.force coq_Z then [], "INT" - else if is_Prop ty then [], "BOOLEAN" - else if is_Set ty then [], "TYPE" +(**** OLD TR_TYPE + else if is_Prop ty then [], Tid ("BOOLEAN", []) + else if is_Set ty then [], Tid ("TYPE", []) else if is_imp_term ty then begin match match_with_imp_term ty with - | Some (t1, t2) -> begin match tr_type env t1, tr_type env t2 with + | Some (t1, t2) -> begin match tr_type tv env t1, tr_type tv env t2 with | ([], t1'), (l2, t2') -> t1' :: l2, t2' | _ -> raise NotFO end @@ -215,14 +287,14 @@ and tr_type env ty = try let r = global_of_constr ty in (try begin match lookup_global r with - | DeclType id -> [], id + | DeclType (id,0) -> [], Tid (id,[]) | _ -> assert false (* assumption: t:Set *) end with Not_found -> begin match r with | IndRef i -> let id = rename_global r in - let d = DeclType id in + let d = DeclType (id,0) in add_global r (Gfo d); globals_stack := d :: !globals_stack; iter_all_constructors i @@ -230,50 +302,68 @@ and tr_type env ty = let rc = global_of_constr c in try begin match tr_global env rc with - | DeclVar (idc, [], _) -> () - | DeclVar (idc, al, _) -> injection idc al + | DeclFun (idc, [], _) -> () + | DeclFun (idc, al, _) -> injection idc al | _ -> assert false end with NotFO -> ()); - [], id + [], Tid (id,[]) | _ -> let id = rename_global r in - let d = DeclType id in + let d = DeclType (id,0) in add_global r (Gfo d); globals_stack := d :: !globals_stack; - [], id + [], Tid (id,[]) (* TODO: constant type definition *) end) with Not_found -> raise NotFO +***) -and make_term_abstraction env c = +and make_term_abstraction tv env c = let ty = Typing.type_of env Evd.empty c in - let tl,t = tr_type env ty in - try - Hashtbl.find term_abstractions c - with Not_found -> - let id = new_abstraction () in - Hashtbl.add term_abstractions c id; - globals_stack := (DeclVar (id, tl, t)) :: !globals_stack; - id - -and tr_global_type env id ty = - if is_Prop ty then - DeclPred (id, []) - else if is_Set ty then - DeclType id + let id = new_abstraction () in + match tr_decl env id ty with + | DeclFun (id,_,_,_) as d -> + begin try + Hashtbl.find term_abstractions c + with Not_found -> + Hashtbl.add term_abstractions c id; + globals_stack := d :: !globals_stack; + id + end + | _ -> + raise NotFO + +(* translate a Coq declaration id:ty in a FOL declaration, that is either + - a type declaration : DeclType (id, n) where n:int is the type arity + - a function declaration : DeclFun (id, tl, t) ; that includes constants + - a predicate declaration : DeclPred (id, tl) + - an axiom : Axiom (id, p) + *) +and tr_decl env id ty = + let tv, env, t = decomp_type_quantifiers env ty in + if is_Set t then + DeclType (id, List.length tv) + else if is_Prop t then + DeclPred (id, List.length tv, []) else - let s = Typing.type_of env Evd.empty ty in + let s = Typing.type_of env Evd.empty t in if is_Prop s then - Assert (id, tr_formula [] env ty) + Axiom (id, tr_formula tv [] env t) else - let l, t = tr_type env ty in - if is_Set s then DeclVar(id, l, t) - else if t = "BOOLEAN" then - DeclPred(id, l) - else raise NotFO + let l, t = decompose_arrows t in + let l = List.map (tr_type tv env) l in + if is_Prop t then + DeclPred(id, List.length tv, l) + else + let s = Typing.type_of env Evd.empty t in + if is_Set s then + DeclFun(id, List.length tv, l, tr_type tv env t) + else + raise NotFO +(* tr_global(r) = tr_decl(id(r),typeof(r)) + a cache mechanism *) and tr_global env r = match r with | VarRef id -> lookup_local id @@ -284,7 +374,7 @@ and tr_global env r = match r with try let ty = Global.type_of_global r in let id = rename_global r in - let d = tr_global_type env id ty in + let d = tr_decl env id ty in (* r can be already declared if it is a constructor *) if not (mem_global r) then begin add_global r (Gfo d); @@ -303,16 +393,17 @@ and axiomatize_body env r id d = match r with begin match (Global.lookup_constant c).const_body with | Some b -> let b = force b in + let tv, env, b = decomp_type_lambdas env b in let axioms = (match d with - | DeclPred (id, []) -> - let value = tr_formula [] env b in + | DeclPred (id, _, []) -> + let value = tr_formula tv [] env b in [id, And (Imp (Fatom (Pred (id, [])), value), Imp (value, Fatom (Pred (id, []))))] - | DeclVar (id, [], _) -> - let value = tr_term [] env b in + | DeclFun (id, _, [], _) -> + let value = tr_term tv [] env b in [id, Fatom (Eq (Fol.App (id, []), value))] - | DeclVar (id, l, _) | DeclPred (id, l) -> + | DeclFun (id, _, l, _) | DeclPred (id, _, l) -> let b = match kind_of_term b with (* a single recursive function *) | Fix (_, (_,_,[|b|])) -> @@ -344,19 +435,19 @@ and axiomatize_body env r id d = match r with let fol_vars = List.map fol_var vars in let vars = List.combine vars l in begin match d with - | DeclVar _ -> + | DeclFun _ -> begin match kind_of_term t with | Case (ci, _, e, br) -> - equations_for_case env id vars bv ci e br + equations_for_case env id vars tv bv ci e br | _ -> let p = Fatom (Eq (App (id, fol_vars), - tr_term bv env t)) + tr_term tv bv env t)) in [id, foralls vars p] end | DeclPred _ -> - let value = tr_formula bv env t in + let value = tr_formula tv bv env t in let p = And (Imp (Fatom (Pred (id, fol_vars)), value), Imp (value, Fatom (Pred (id, fol_vars)))) @@ -367,37 +458,28 @@ and axiomatize_body env r id d = match r with end | DeclType _ -> raise NotFO - | Assert _ -> assert false) + | Axiom _ -> assert false) in - let axioms = List.map (fun (id,ax) -> Assert (id, ax)) axioms in + let axioms = List.map (fun (id,ax) -> Axiom (id, ax)) axioms in globals_stack := axioms @ !globals_stack | None -> () (* Coq axiom *) end | IndRef i -> - (*iter_all_constructors i - (let rc = reference_of_constr c in -match tr_global c with - | DeclVar(idc, l, _) -> - (fun _ c -> List.map (fun co -> ) (liste des constructeurs ą partir de c non compris));*) - begin match d with - | DeclPred _ -> - iter_all_constructors i - (fun _ c -> - let rc = reference_of_constr c in - try - begin match tr_global env rc with - | Assert _ -> () - | _ -> assert false - end - with NotFO -> - ()); - | DeclType _ -> raise NotFO - | _ -> assert false - end + iter_all_constructors i + (fun _ c -> + let rc = reference_of_constr c in + try + begin match tr_global env rc with + | DeclFun (_, _, [], _) -> () + | DeclFun (idc, _, al, _) -> injection idc al + | _ -> () + end + with NotFO -> + ()) | _ -> () -and equations_for_case env id vars bv ci e br = match kind_of_term e with +and equations_for_case env id vars tv bv ci e br = match kind_of_term e with | Var x when List.exists (fun (y, _) -> string_of_id x = y) vars -> let eqs = ref [] in iter_all_constructors ci.ci_ind @@ -405,7 +487,7 @@ and equations_for_case env id vars bv ci e br = match kind_of_term e with try let cjr = reference_of_constr cj in begin match tr_global env cjr with - | DeclVar (idc, l, _) -> + | DeclFun (idc, _, l, _) -> let b = br.(j) in let rec_vars, b = decompose_lam b in let rec_vars, env = coq_rename_vars env rec_vars in @@ -435,7 +517,7 @@ and equations_for_case env id vars bv ci e br = match kind_of_term e with let vars = remove vars x in let p = Fatom (Eq (App (id, fol_vars), - tr_term bv env b)) + tr_term tv bv env b)) in eqs := (id ^ "_" ^ idc, foralls vars p) :: !eqs | _ -> @@ -448,22 +530,22 @@ and equations_for_case env id vars bv ci e br = match kind_of_term e with (* assumption: t:T:Set *) -and tr_term bv env t = +and tr_term tv bv env t = match kind_of_term t with | Term.App (f, [|a;b|]) when f = Lazy.force coq_Zplus -> - Plus (tr_term bv env a, tr_term bv env b) + Plus (tr_term tv bv env a, tr_term tv bv env b) | Term.App (f, [|a;b|]) when f = Lazy.force coq_Zminus -> - Moins (tr_term bv env a, tr_term bv env b) + Moins (tr_term tv bv env a, tr_term tv bv env b) | Term.App (f, [|a;b|]) when f = Lazy.force coq_Zmult -> - Mult (tr_term bv env a, tr_term bv env b) + Mult (tr_term tv bv env a, tr_term tv bv env b) | Term.App (f, [|a;b|]) when f = Lazy.force coq_Zdiv -> - Div (tr_term bv env a, tr_term bv env b) + Div (tr_term tv bv env a, tr_term tv bv env b) | Term.Construct _ when t = Lazy.force coq_Z0 -> Cst 0 | Term.App (f, [|a|]) when f = Lazy.force coq_Zpos -> - fol_term_of_positive env a + fol_term_of_positive tv env a | Term.App (f, [|a|]) when f = Lazy.force coq_Zneg -> - Moins (Cst 0, (fol_term_of_positive env a)) + Moins (Cst 0, (fol_term_of_positive tv env a)) | Term.Var id when List.mem id bv -> App (string_of_id id, []) | _ -> @@ -471,8 +553,9 @@ and tr_term bv env t = begin try let r = global_of_constr f in match tr_global env r with - | DeclVar (s, _, _) -> - Fol.App (s, List.map (tr_term bv env) cl) + | DeclFun (s, k, _, _) -> + let cl = skip_k_args k cl in + Fol.App (s, List.map (tr_term tv bv env) cl) | _ -> raise NotFO with @@ -481,34 +564,31 @@ and tr_term bv env t = | NotFO -> (* we need to abstract some part of (f cl) *) let rec abstract app = function | [] -> - Fol.App (make_term_abstraction env app, []) + Fol.App (make_term_abstraction tv env app, []) | x :: l as args -> begin try - let s = make_term_abstraction env app in - Fol.App (s, List.map (tr_term bv env) args) + let s = make_term_abstraction tv env app in + Fol.App (s, List.map (tr_term tv bv env) args) with NotFO -> abstract (applist (app, [x])) l end in let app,l = match cl with - | x :: l -> applist (f, [x]), l | _ -> raise NotFO + | x :: l -> applist (f, [x]), l | [] -> raise NotFO in abstract app l end -and quantifiers n a b bv env = +and quantifiers n a b tv bv env = let vars, env = coq_rename_vars env [n,a] in let id = match vars with [x] -> x | _ -> assert false in let b = subst1 (mkVar id) b in - let t = match tr_type env a with - | [], t -> t - | _ -> raise NotFO - in + let t = tr_type tv env a in let bv = id :: bv in id, t, bv, env, b (* assumption: f is of type Prop *) -and tr_formula bv env f = +and tr_formula tv bv env f = let c, args = decompose_app f in match kind_of_term c, args with | Var id, [] -> @@ -516,49 +596,50 @@ and tr_formula bv env f = | _, [t;a;b] when c = build_coq_eq () -> let ty = Typing.type_of env Evd.empty t in if is_Set ty then - begin match tr_type env t with - | [], _ -> - Fatom (Eq (tr_term bv env a, tr_term bv env b)) - | _ -> raise NotFO - end - else raise NotFO + let _ = tr_type tv env t in + Fatom (Eq (tr_term tv bv env a, tr_term tv bv env b)) + else + raise NotFO | _, [a;b] when c = Lazy.force coq_Zle -> - Fatom (Le (tr_term bv env a, tr_term bv env b)) + Fatom (Le (tr_term tv bv env a, tr_term tv bv env b)) | _, [a;b] when c = Lazy.force coq_Zlt -> - Fatom (Lt (tr_term bv env a, tr_term bv env b)) + Fatom (Lt (tr_term tv bv env a, tr_term tv bv env b)) | _, [a;b] when c = Lazy.force coq_Zge -> - Fatom (Ge (tr_term bv env a, tr_term bv env b)) + Fatom (Ge (tr_term tv bv env a, tr_term tv bv env b)) | _, [a;b] when c = Lazy.force coq_Zgt -> - Fatom (Gt (tr_term bv env a, tr_term bv env b)) + Fatom (Gt (tr_term tv bv env a, tr_term tv bv env b)) | _, [] when c = build_coq_False () -> False | _, [] when c = build_coq_True () -> True | _, [a] when c = build_coq_not () -> - Not (tr_formula bv env a) + Not (tr_formula tv bv env a) | _, [a;b] when c = build_coq_and () -> - And (tr_formula bv env a, tr_formula bv env b) + And (tr_formula tv bv env a, tr_formula tv bv env b) | _, [a;b] when c = build_coq_or () -> - Or (tr_formula bv env a, tr_formula bv env b) + Or (tr_formula tv bv env a, tr_formula tv bv env b) | Prod (n, a, b), _ -> if is_imp_term f then - Imp (tr_formula bv env a, tr_formula bv env b) + Imp (tr_formula tv bv env a, tr_formula tv bv env b) else - let id, t, bv, env, b = quantifiers n a b bv env in - Forall (string_of_id id, t, tr_formula bv env b) + let id, t, bv, env, b = quantifiers n a b tv bv env in + Forall (string_of_id id, t, tr_formula tv bv env b) | _, [_; a] when c = build_coq_ex () -> begin match kind_of_term a with | Lambda(n, a, b) -> - let id, t, bv, env, b = quantifiers n a b bv env in - Exists (string_of_id id, t, tr_formula bv env b) - | _ -> assert false - (* a must be a Lambda since we are in the ex case *) end + let id, t, bv, env, b = quantifiers n a b tv bv env in + Exists (string_of_id id, t, tr_formula tv bv env b) + | _ -> + (* unusual case of the shape (ex p) *) + raise NotFO (* TODO: we could eta-expanse *) + end | _ -> begin try let r = global_of_constr c in match tr_global env r with - | DeclPred (s, _) -> - Fatom (Pred (s, List.map (tr_term bv env) args)) + | DeclPred (s, k, _) -> + let args = skip_k_args k args in + Fatom (Pred (s, List.map (tr_term tv bv env) args)) | _ -> raise NotFO with Not_found -> @@ -571,7 +652,7 @@ let tr_goal gl = let tr_one_hyp (id, ty) = try let s = rename_global (VarRef id) in - let d = tr_global_type (pf_env gl) s ty in + let d = tr_decl (pf_env gl) s ty in Hashtbl.add locals id (Gfo d); d with NotFO -> @@ -583,18 +664,26 @@ let tr_goal gl = (fun h acc -> try tr_one_hyp h :: acc with NotFO -> acc) (pf_hyps_types gl) [] in - let c = tr_formula [] (pf_env gl) (pf_concl gl) in + let c = tr_formula [] [] (pf_env gl) (pf_concl gl) in let hyps = List.rev_append !globals_stack (List.rev hyps) in hyps, c type prover = Simplify | CVCLite | Harvey | Zenon +(*** let call_prover prover q = match prover with | Simplify -> Dp_simplify.call (Dp_sorts.query q) | CVCLite -> Dp_cvcl.call q | Harvey -> error "haRVey not yet interfaced" | Zenon -> Dp_zenon.call (Dp_sorts.query q) +***) +let call_prover prover q = + Dp_why.output_file "test.why" q; + ignore (Sys.command "cat test.why"); + ignore (Sys.command "why --simplify test.why"); + ignore (Sys.command "timeout 5 Simplify < test_why.sx"); + Valid let dp prover gl = let concl_type = pf_type_of gl (pf_concl gl) in @@ -625,7 +714,7 @@ let dp_hint l = if is_Prop s then try let id = rename_global r in - let d = Assert (id, tr_formula [] env ty) in + let d = Axiom (id, tr_formula [] [] env ty) in add_global r (Gfo d); globals_stack := d :: !globals_stack with NotFO -> diff --git a/contrib/dp/dp_why.ml b/contrib/dp/dp_why.ml new file mode 100644 index 000000000..d6a5e145c --- /dev/null +++ b/contrib/dp/dp_why.ml @@ -0,0 +1,123 @@ + +(* Pretty-print PFOL (see fol.mli) in Why syntax *) + +open Format +open Fol + +let rec print_list sep print fmt = function + | [] -> () + | [x] -> print fmt x + | x :: r -> print fmt x; sep fmt (); print_list sep print fmt r + +let space fmt () = fprintf fmt "@ " +let comma fmt () = fprintf fmt ",@ " + +let is_why_keyword s = false (* TODO *) + +let ident fmt s = + if is_why_keyword s then fprintf fmt "why__%s" s else fprintf fmt "%s" s + +let rec print_typ fmt = function + | Tvar x -> fprintf fmt "'%s" x + | Tid (x, []) -> fprintf fmt "%s" x + | Tid (x, [t]) -> fprintf fmt "%a %s" print_typ t x + | Tid (x, tl) -> fprintf fmt "(%a) %s" (print_list comma print_typ) tl x + +let rec print_term fmt = function + | Cst n -> + fprintf fmt "%d" n + | Plus (a, b) -> + fprintf fmt "@[(%a +@ %a)@]" print_term a print_term b + | Moins (a, b) -> + fprintf fmt "@[(%a -@ %a)@]" print_term a print_term b + | Mult (a, b) -> + fprintf fmt "@[(%a *@ %a)@]" print_term a print_term b + | Div (a, b) -> + fprintf fmt "@[(%a /@ %a)@]" print_term a print_term b + | App (id, []) -> + fprintf fmt "%a" ident id + | App (id, tl) -> + fprintf fmt "@[%a(%a)@]" ident id print_terms tl + +and print_terms fmt tl = + print_list comma print_term fmt tl + +let rec print_predicate fmt p = + let pp = print_predicate in + match p with + | True -> + fprintf fmt "true" + | False -> + fprintf fmt "false" + | Fatom (Eq (a, b)) -> + fprintf fmt "@[(%a =@ %a)@]" print_term a print_term b + | Fatom (Le (a, b)) -> + fprintf fmt "@[(%a <=@ %a)@]" print_term a print_term b + | Fatom (Lt (a, b))-> + fprintf fmt "@[(%a <@ %a)@]" print_term a print_term b + | Fatom (Ge (a, b)) -> + fprintf fmt "@[(%a >=@ %a)@]" print_term a print_term b + | Fatom (Gt (a, b)) -> + fprintf fmt "@[(%a >@ %a)@]" print_term a print_term b + | Fatom (Pred (id, [])) -> + fprintf fmt "%a" ident id + | Fatom (Pred (id, tl)) -> + fprintf fmt "@[%a(%a)@]" ident id print_terms tl + | Imp (a, b) -> + fprintf fmt "@[(%a ->@ %a)@]" pp a pp b + | And (a, b) -> + fprintf fmt "@[(%a and@ %a)@]" pp a pp b + | Or (a, b) -> + fprintf fmt "@[(%a or@ %a)@]" pp a pp b + | Not a -> + fprintf fmt "@[(not@ %a)@]" pp a + | Forall (id, t, p) -> + fprintf fmt "@[(forall %a:%a.@ %a)@]" ident id print_typ t pp p + | Exists (id, t, p) -> + fprintf fmt "@[(exists %a:%a.@ %a)@]" ident id print_typ t pp p + +let print_query fmt (decls,concl) = + let print_dtype = function + | DeclType (id, 0) -> + fprintf fmt "@[type %s@]@\n@\n" id + | DeclType (id, 1) -> + fprintf fmt "@[type 'a %s@]@\n@\n" id + | DeclType (id, n) -> + fprintf fmt "@[type ("; + for i = 1 to n do fprintf fmt "'a%d" i done; + fprintf fmt ") %s@]@\n@\n" id + | DeclFun _ | DeclPred _ | Axiom _ -> + () + in + let print_dvar_dpred = function + | DeclFun (id, _, [], t) -> + fprintf fmt "@[logic %s : -> %a@]@\n@\n" id print_typ t + | DeclFun (id, _, l, t) -> + fprintf fmt "@[logic %s : %a -> %a@]@\n@\n" + id (print_list comma print_typ) l print_typ t + | DeclPred (id, _, []) -> + fprintf fmt "@[logic %s : -> prop @]@\n@\n" id + | DeclPred (id, _, l) -> + fprintf fmt "@[logic %s : %a -> prop@]@\n@\n" + id (print_list comma print_typ) l + | DeclType _ | Axiom _ -> + () + in + let print_assert = function + | Axiom (id, f) -> + fprintf fmt "@[<hov 2>axiom %s:@ %a@]@\n@\n" id print_predicate f + | DeclType _ | DeclFun _ | DeclPred _ -> + () + in + List.iter print_dtype decls; + List.iter print_dvar_dpred decls; + List.iter print_assert decls; + fprintf fmt "@[<hov 2>goal coq__goal: %a@]" print_predicate concl + +let output_file f q = + let c = open_out f in + let fmt = formatter_of_out_channel c in + fprintf fmt "@[%a@]@." print_query q; + close_out c + + diff --git a/contrib/dp/fol.mli b/contrib/dp/fol.mli index 02c73e301..5dd46b0d1 100644 --- a/contrib/dp/fol.mli +++ b/contrib/dp/fol.mli @@ -1,10 +1,9 @@ -type typ = string -(*** - | Base of string - | Arrow of typ * typ - | Tuple of typ list -***) +(* Polymorphic First-Order Logic (that is Why's input logic) *) + +type typ = + | Tvar of string + | Tid of string * typ list type term = | Cst of int @@ -33,13 +32,14 @@ and form = | True | False -type hyp = - | Assert of string * form - | DeclVar of string * typ list * typ - | DeclPred of string * typ list - | DeclType of string +(* the integer indicates the number of type variables *) +type decl = + | DeclType of string * int + | DeclFun of string * int * typ list * typ + | DeclPred of string * int * typ list + | Axiom of string * form -type query = hyp list * form +type query = decl list * form (* prover result *) diff --git a/contrib/dp/tests.v b/contrib/dp/tests.v index d12203803..10b6f0d83 100644 --- a/contrib/dp/tests.v +++ b/contrib/dp/tests.v @@ -3,7 +3,6 @@ Reset Initial. Require Import ZArith. Require Import Classical. - (* First example with the 0 and the equality translated *) Goal 0 = 0. @@ -44,6 +43,7 @@ Qed. (* Arithmetic *) +Open Scope Z_scope. Goal 1 + 1 = 2. @@ -221,4 +221,4 @@ Goal mrf (S (S O)) = true. zenon. -*)
\ No newline at end of file +*) |