diff options
| author |  huang <huang@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-03-22 13:29:25 +0000 |
|---|---|---|
| committer | huang <huang@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-03-22 13:29:25 +0000 |
| commit | c2f4625e7e0fea969da5b44a0ea543ebfdc32d87 (patch) | |
| tree | 1146a42b01a903d819af23cc2bd0710e1f67c5f0 | |
| parent | c5315c60d2a78f9f34f9963540390f543142d488 (diff) | |
An intuitionistic first-order theorem prover -- JProver.
See the "README" file for more information.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2563 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | .depend | 176 | ||||
| -rw-r--r-- | Makefile | 17 | ||||
| -rw-r--r-- | contrib/jprover/JProver.v | 14 | ||||
| -rw-r--r-- | contrib/jprover/README | 66 | ||||
| -rw-r--r-- | contrib/jprover/jLogic.mli | 40 | ||||
| -rw-r--r-- | contrib/jprover/jall.ml | 4698 | ||||
| -rw-r--r-- | contrib/jprover/jall.mli | 339 | ||||
| -rw-r--r-- | contrib/jprover/jlogic.ml | 106 | ||||
| -rw-r--r-- | contrib/jprover/jlogic.mli | 40 | ||||
| -rw-r--r-- | contrib/jprover/jprover.ml | 513 | ||||
| -rw-r--r-- | contrib/jprover/jterm.ml | 872 | ||||
| -rw-r--r-- | contrib/jprover/jterm.mli | 110 | ||||
| -rw-r--r-- | contrib/jprover/jtunify.ml | 507 | ||||
| -rw-r--r-- | contrib/jprover/jtunify.mli | 35 | ||||
| -rw-r--r-- | contrib/jprover/opname.ml | 90 | ||||
| -rw-r--r-- | contrib/jprover/opname.mli | 15 |
16 files changed, 7570 insertions, 68 deletions
@@ -25,6 +25,9 @@ kernel/typeops.cmi: kernel/environ.cmi kernel/names.cmi kernel/sign.cmi \ kernel/term.cmi kernel/univ.cmi kernel/univ.cmi: kernel/names.cmi lib/pp.cmi lib/pp.cmi: lib/pp_control.cmi +lib/rtree.cmi: lib/pp.cmi +lib/system.cmi: lib/pp.cmi +lib/util.cmi: lib/pp.cmi library/declare.cmi: kernel/cooking.cmi kernel/declarations.cmi \ kernel/environ.cmi kernel/indtypes.cmi library/libobject.cmi \ library/library.cmi kernel/names.cmi library/nametab.cmi \ @@ -45,9 +48,6 @@ library/nameops.cmi: kernel/environ.cmi kernel/names.cmi lib/pp.cmi \ library/nametab.cmi: kernel/environ.cmi kernel/names.cmi lib/pp.cmi \ lib/util.cmi library/summary.cmi: kernel/names.cmi -lib/rtree.cmi: lib/pp.cmi -lib/system.cmi: lib/pp.cmi -lib/util.cmi: lib/pp.cmi parsing/ast.cmi: parsing/coqast.cmi lib/dyn.cmi kernel/names.cmi \ parsing/pcoq.cmi lib/pp.cmi parsing/astterm.cmi: parsing/coqast.cmi kernel/environ.cmi pretyping/evd.cmi \ @@ -209,7 +209,7 @@ toplevel/class.cmi: pretyping/classops.cmi library/declare.cmi \ toplevel/command.cmi: parsing/coqast.cmi library/declare.cmi \ kernel/environ.cmi pretyping/evd.cmi kernel/indtypes.cmi \ library/library.cmi kernel/names.cmi library/nametab.cmi \ - pretyping/tacred.cmi kernel/term.cmi + kernel/safe_typing.cmi pretyping/tacred.cmi kernel/term.cmi toplevel/coqinit.cmi: kernel/names.cmi toplevel/discharge.cmi: kernel/names.cmi toplevel/fhimsg.cmi: kernel/environ.cmi kernel/names.cmi lib/pp.cmi \ @@ -226,18 +226,18 @@ toplevel/recordobj.cmi: library/nametab.cmi toplevel/searchisos.cmi: library/libobject.cmi kernel/names.cmi \ kernel/term.cmi toplevel/toplevel.cmi: parsing/pcoq.cmi lib/pp.cmi +toplevel/vernac.cmi: parsing/coqast.cmi parsing/pcoq.cmi toplevel/vernacentries.cmi: kernel/environ.cmi pretyping/evd.cmi \ kernel/names.cmi kernel/term.cmi toplevel/vernacinterp.cmi toplevel/vernacinterp.cmi: parsing/coqast.cmi lib/dyn.cmi kernel/names.cmi \ library/nametab.cmi proofs/proof_type.cmi -toplevel/vernac.cmi: parsing/coqast.cmi parsing/pcoq.cmi contrib/correctness/past.cmi: parsing/coqast.cmi kernel/names.cmi \ contrib/correctness/ptype.cmi kernel/term.cmi +contrib/correctness/pcic.cmi: contrib/correctness/past.cmi \ + pretyping/rawterm.cmi contrib/correctness/pcicenv.cmi: kernel/names.cmi \ contrib/correctness/penv.cmi contrib/correctness/prename.cmi \ kernel/sign.cmi kernel/term.cmi -contrib/correctness/pcic.cmi: contrib/correctness/past.cmi \ - pretyping/rawterm.cmi contrib/correctness/pdb.cmi: kernel/names.cmi contrib/correctness/past.cmi \ contrib/correctness/ptype.cmi contrib/correctness/peffect.cmi: kernel/names.cmi lib/pp.cmi @@ -315,6 +315,12 @@ contrib/interface/translate.cmi: contrib/interface/ascent.cmi \ contrib/interface/vtp.cmi: contrib/interface/ascent.cmi contrib/interface/xlate.cmi: contrib/interface/ascent.cmi \ contrib/interface/ctast.cmo +contrib/jprover/jLogic.cmi: contrib/jprover/jterm.cmi +contrib/jprover/jall.cmi: contrib/jprover/jlogic.cmi \ + contrib/jprover/jterm.cmi contrib/jprover/opname.cmi +contrib/jprover/jlogic.cmi: contrib/jprover/jterm.cmi +contrib/jprover/jterm.cmi: contrib/jprover/opname.cmi +contrib/jprover/test.cmi: contrib/jprover/jterm.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 @@ -426,24 +432,34 @@ lib/edit.cmo: lib/bstack.cmi lib/pp.cmi lib/util.cmi lib/edit.cmi lib/edit.cmx: lib/bstack.cmx lib/pp.cmx lib/util.cmx lib/edit.cmi lib/explore.cmo: lib/explore.cmi lib/explore.cmx: lib/explore.cmi -lib/gmapl.cmo: lib/gmap.cmi lib/util.cmi lib/gmapl.cmi -lib/gmapl.cmx: lib/gmap.cmx lib/util.cmx lib/gmapl.cmi lib/gmap.cmo: lib/gmap.cmi lib/gmap.cmx: lib/gmap.cmi +lib/gmapl.cmo: lib/gmap.cmi lib/util.cmi lib/gmapl.cmi +lib/gmapl.cmx: lib/gmap.cmx lib/util.cmx lib/gmapl.cmi lib/gset.cmo: lib/gset.cmi lib/gset.cmx: lib/gset.cmi lib/hashcons.cmo: lib/hashcons.cmi lib/hashcons.cmx: lib/hashcons.cmi lib/options.cmo: lib/util.cmi lib/options.cmi lib/options.cmx: lib/util.cmx lib/options.cmi -lib/pp_control.cmo: lib/pp_control.cmi -lib/pp_control.cmx: lib/pp_control.cmi lib/pp.cmo: lib/pp_control.cmi lib/pp.cmi lib/pp.cmx: lib/pp_control.cmx lib/pp.cmi +lib/pp_control.cmo: lib/pp_control.cmi +lib/pp_control.cmx: lib/pp_control.cmi lib/predicate.cmo: lib/predicate.cmi lib/predicate.cmx: lib/predicate.cmi lib/profile.cmo: lib/profile.cmi lib/profile.cmx: lib/profile.cmi +lib/rtree.cmo: lib/pp.cmi lib/util.cmi lib/rtree.cmi +lib/rtree.cmx: lib/pp.cmx lib/util.cmx lib/rtree.cmi +lib/stamps.cmo: lib/stamps.cmi +lib/stamps.cmx: lib/stamps.cmi +lib/system.cmo: config/coq_config.cmi lib/pp.cmi lib/util.cmi lib/system.cmi +lib/system.cmx: config/coq_config.cmx lib/pp.cmx lib/util.cmx lib/system.cmi +lib/tlm.cmo: lib/gmap.cmi lib/gset.cmi lib/tlm.cmi +lib/tlm.cmx: lib/gmap.cmx lib/gset.cmx lib/tlm.cmi +lib/util.cmo: lib/pp.cmi lib/util.cmi +lib/util.cmx: lib/pp.cmx lib/util.cmi library/declare.cmo: kernel/declarations.cmi kernel/environ.cmi \ library/global.cmi library/impargs.cmi kernel/indtypes.cmi \ kernel/inductive.cmi library/lib.cmi library/libobject.cmi \ @@ -520,16 +536,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/rtree.cmo: lib/pp.cmi lib/util.cmi lib/rtree.cmi -lib/rtree.cmx: lib/pp.cmx lib/util.cmx lib/rtree.cmi -lib/stamps.cmo: lib/stamps.cmi -lib/stamps.cmx: lib/stamps.cmi -lib/system.cmo: config/coq_config.cmi lib/pp.cmi lib/util.cmi lib/system.cmi -lib/system.cmx: config/coq_config.cmx lib/pp.cmx lib/util.cmx lib/system.cmi -lib/tlm.cmo: lib/gmap.cmi lib/gset.cmi lib/tlm.cmi -lib/tlm.cmx: lib/gmap.cmx lib/gset.cmx lib/tlm.cmi -lib/util.cmo: lib/pp.cmi lib/util.cmi -lib/util.cmx: lib/pp.cmx lib/util.cmi parsing/ast.cmo: parsing/coqast.cmi lib/dyn.cmi kernel/names.cmi \ parsing/pcoq.cmi lib/pp.cmi lib/util.cmi parsing/ast.cmi parsing/ast.cmx: parsing/coqast.cmx lib/dyn.cmx kernel/names.cmx \ @@ -1348,12 +1354,12 @@ tactics/wcclausenv.cmx: proofs/clenv.cmx kernel/environ.cmx \ proofs/proof_trees.cmx pretyping/reductionops.cmx kernel/sign.cmx \ proofs/tacmach.cmx kernel/term.cmx pretyping/termops.cmx lib/util.cmx \ tactics/wcclausenv.cmi -tools/coqdep_lexer.cmo: config/coq_config.cmi -tools/coqdep_lexer.cmx: config/coq_config.cmx -tools/coqdep.cmo: config/coq_config.cmi tools/coqdep_lexer.cmo -tools/coqdep.cmx: config/coq_config.cmx tools/coqdep_lexer.cmx tools/coq_vo2xml.cmo: config/coq_config.cmi toplevel/usage.cmi tools/coq_vo2xml.cmx: config/coq_config.cmx toplevel/usage.cmx +tools/coqdep.cmo: config/coq_config.cmi tools/coqdep_lexer.cmo +tools/coqdep.cmx: config/coq_config.cmx tools/coqdep_lexer.cmx +tools/coqdep_lexer.cmo: config/coq_config.cmi +tools/coqdep_lexer.cmx: config/coq_config.cmx tools/gallina.cmo: tools/gallina_lexer.cmo tools/gallina.cmx: tools/gallina_lexer.cmx toplevel/cerrors.cmo: parsing/ast.cmi pretyping/cases.cmi toplevel/himsg.cmi \ @@ -1534,6 +1540,16 @@ toplevel/toplevel.cmx: parsing/ast.cmx toplevel/cerrors.cmx library/lib.cmx \ toplevel/vernac.cmx toplevel/vernacinterp.cmx toplevel/toplevel.cmi toplevel/usage.cmo: config/coq_config.cmi toplevel/usage.cmi toplevel/usage.cmx: config/coq_config.cmx toplevel/usage.cmi +toplevel/vernac.cmo: parsing/ast.cmi parsing/coqast.cmi library/lib.cmi \ + library/library.cmi library/nameops.cmi kernel/names.cmi lib/options.cmi \ + parsing/pcoq.cmi lib/pp.cmi library/states.cmi lib/system.cmi \ + pretyping/termops.cmi lib/util.cmi toplevel/vernacinterp.cmi \ + toplevel/vernac.cmi +toplevel/vernac.cmx: parsing/ast.cmx parsing/coqast.cmx library/lib.cmx \ + library/library.cmx library/nameops.cmx kernel/names.cmx lib/options.cmx \ + parsing/pcoq.cmx lib/pp.cmx library/states.cmx lib/system.cmx \ + pretyping/termops.cmx lib/util.cmx toplevel/vernacinterp.cmx \ + toplevel/vernac.cmi toplevel/vernacentries.cmo: parsing/ast.cmi parsing/astterm.cmi \ toplevel/class.cmi pretyping/classops.cmi toplevel/command.cmi \ parsing/coqast.cmi kernel/declarations.cmi library/declare.cmi \ @@ -1578,28 +1594,6 @@ toplevel/vernacinterp.cmx: parsing/ast.cmx parsing/astterm.cmx \ kernel/names.cmx library/nametab.cmx lib/options.cmx lib/pp.cmx \ proofs/proof_type.cmx proofs/tacinterp.cmx lib/util.cmx \ toplevel/vernacinterp.cmi -toplevel/vernac.cmo: parsing/ast.cmi parsing/coqast.cmi library/lib.cmi \ - library/library.cmi library/nameops.cmi kernel/names.cmi lib/options.cmi \ - parsing/pcoq.cmi lib/pp.cmi library/states.cmi lib/system.cmi \ - pretyping/termops.cmi lib/util.cmi toplevel/vernacinterp.cmi \ - toplevel/vernac.cmi -toplevel/vernac.cmx: parsing/ast.cmx parsing/coqast.cmx library/lib.cmx \ - library/library.cmx library/nameops.cmx kernel/names.cmx lib/options.cmx \ - parsing/pcoq.cmx lib/pp.cmx library/states.cmx lib/system.cmx \ - pretyping/termops.cmx lib/util.cmx toplevel/vernacinterp.cmx \ - toplevel/vernac.cmi -contrib/correctness/pcicenv.cmo: library/global.cmi kernel/names.cmi \ - contrib/correctness/past.cmi contrib/correctness/penv.cmi \ - contrib/correctness/pmisc.cmi contrib/correctness/pmonad.cmi \ - contrib/correctness/prename.cmi contrib/correctness/ptype.cmi \ - contrib/correctness/putil.cmi kernel/sign.cmi kernel/term.cmi \ - kernel/univ.cmi contrib/correctness/pcicenv.cmi -contrib/correctness/pcicenv.cmx: library/global.cmx kernel/names.cmx \ - contrib/correctness/past.cmi contrib/correctness/penv.cmx \ - contrib/correctness/pmisc.cmx contrib/correctness/pmonad.cmx \ - contrib/correctness/prename.cmx contrib/correctness/ptype.cmi \ - contrib/correctness/putil.cmx kernel/sign.cmx kernel/term.cmx \ - kernel/univ.cmx contrib/correctness/pcicenv.cmi contrib/correctness/pcic.cmo: parsing/ast.cmi kernel/declarations.cmi \ library/declare.cmi pretyping/detyping.cmi library/global.cmi \ kernel/indtypes.cmi kernel/names.cmi library/nametab.cmi \ @@ -1614,6 +1608,18 @@ contrib/correctness/pcic.cmx: parsing/ast.cmx kernel/declarations.cmx \ pretyping/rawterm.cmx toplevel/record.cmx kernel/sign.cmx kernel/term.cmx \ pretyping/termops.cmx kernel/typeops.cmx lib/util.cmx \ contrib/correctness/pcic.cmi +contrib/correctness/pcicenv.cmo: library/global.cmi kernel/names.cmi \ + contrib/correctness/past.cmi contrib/correctness/penv.cmi \ + contrib/correctness/pmisc.cmi contrib/correctness/pmonad.cmi \ + contrib/correctness/prename.cmi contrib/correctness/ptype.cmi \ + contrib/correctness/putil.cmi kernel/sign.cmi kernel/term.cmi \ + kernel/univ.cmi contrib/correctness/pcicenv.cmi +contrib/correctness/pcicenv.cmx: library/global.cmx kernel/names.cmx \ + contrib/correctness/past.cmi contrib/correctness/penv.cmx \ + contrib/correctness/pmisc.cmx contrib/correctness/pmonad.cmx \ + contrib/correctness/prename.cmx contrib/correctness/ptype.cmi \ + contrib/correctness/putil.cmx kernel/sign.cmx kernel/term.cmx \ + kernel/univ.cmx contrib/correctness/pcicenv.cmi contrib/correctness/pdb.cmo: library/declare.cmi library/global.cmi \ kernel/names.cmi library/nametab.cmi contrib/correctness/past.cmi \ contrib/correctness/peffect.cmi contrib/correctness/penv.cmi \ @@ -1916,16 +1922,18 @@ contrib/extraction/table.cmx: kernel/declarations.cmx library/global.cmx \ toplevel/vernacinterp.cmx contrib/extraction/table.cmi contrib/field/field.cmo: parsing/astterm.cmi parsing/coqast.cmi \ library/declare.cmi pretyping/evd.cmi library/global.cmi library/lib.cmi \ - library/libobject.cmi kernel/names.cmi library/nametab.cmi \ - proofs/proof_type.cmi contrib/ring/quote.cmo contrib/ring/ring.cmo \ - library/summary.cmi proofs/tacinterp.cmi proofs/tacmach.cmi \ - kernel/term.cmi lib/util.cmi toplevel/vernacinterp.cmi + library/libobject.cmi kernel/names.cmi library/nametab.cmi lib/pp.cmi \ + proofs/proof_type.cmi contrib/ring/quote.cmo pretyping/reductionops.cmi \ + contrib/ring/ring.cmo library/summary.cmi proofs/tacinterp.cmi \ + proofs/tacmach.cmi kernel/term.cmi pretyping/typing.cmi lib/util.cmi \ + toplevel/vernacinterp.cmi contrib/field/field.cmx: parsing/astterm.cmx parsing/coqast.cmx \ library/declare.cmx pretyping/evd.cmx library/global.cmx library/lib.cmx \ - library/libobject.cmx kernel/names.cmx library/nametab.cmx \ - proofs/proof_type.cmx contrib/ring/quote.cmx contrib/ring/ring.cmx \ - library/summary.cmx proofs/tacinterp.cmx proofs/tacmach.cmx \ - kernel/term.cmx lib/util.cmx toplevel/vernacinterp.cmx + library/libobject.cmx kernel/names.cmx library/nametab.cmx lib/pp.cmx \ + proofs/proof_type.cmx contrib/ring/quote.cmx pretyping/reductionops.cmx \ + contrib/ring/ring.cmx library/summary.cmx proofs/tacinterp.cmx \ + proofs/tacmach.cmx kernel/term.cmx pretyping/typing.cmx lib/util.cmx \ + toplevel/vernacinterp.cmx contrib/fourier/fourierR.cmo: parsing/astterm.cmi proofs/clenv.cmi \ tactics/equality.cmi pretyping/evd.cmi contrib/fourier/fourier.cmo \ library/global.cmi kernel/names.cmi parsing/pcoq.cmi \ @@ -2090,14 +2098,6 @@ contrib/interface/pbp.cmx: parsing/astterm.cmx parsing/coqlib.cmx \ kernel/reduction.cmx proofs/tacinterp.cmx proofs/tacmach.cmx \ tactics/tacticals.cmx tactics/tactics.cmx kernel/term.cmx \ pretyping/typing.cmx lib/util.cmx contrib/interface/pbp.cmi -contrib/interface/showproof_ct.cmo: contrib/interface/ascent.cmi \ - parsing/esyntax.cmi library/global.cmi toplevel/metasyntax.cmi lib/pp.cmi \ - parsing/printer.cmi contrib/interface/translate.cmi \ - contrib/interface/vtp.cmi contrib/interface/xlate.cmi -contrib/interface/showproof_ct.cmx: contrib/interface/ascent.cmi \ - parsing/esyntax.cmx library/global.cmx toplevel/metasyntax.cmx lib/pp.cmx \ - parsing/printer.cmx contrib/interface/translate.cmx \ - contrib/interface/vtp.cmx contrib/interface/xlate.cmx contrib/interface/showproof.cmo: parsing/ast.cmi parsing/astterm.cmi \ proofs/clenv.cmi parsing/coqast.cmi kernel/declarations.cmi \ kernel/environ.cmi pretyping/evd.cmi library/global.cmi \ @@ -2118,6 +2118,14 @@ contrib/interface/showproof.cmx: parsing/ast.cmx parsing/astterm.cmx \ kernel/term.cmx parsing/termast.cmx pretyping/termops.cmx \ contrib/interface/translate.cmx pretyping/typing.cmx lib/util.cmx \ toplevel/vernacinterp.cmx contrib/interface/showproof.cmi +contrib/interface/showproof_ct.cmo: contrib/interface/ascent.cmi \ + parsing/esyntax.cmi library/global.cmi toplevel/metasyntax.cmi lib/pp.cmi \ + parsing/printer.cmi contrib/interface/translate.cmi \ + contrib/interface/vtp.cmi contrib/interface/xlate.cmi +contrib/interface/showproof_ct.cmx: contrib/interface/ascent.cmi \ + parsing/esyntax.cmx library/global.cmx toplevel/metasyntax.cmx lib/pp.cmx \ + parsing/printer.cmx contrib/interface/translate.cmx \ + contrib/interface/vtp.cmx contrib/interface/xlate.cmx contrib/interface/translate.cmo: contrib/interface/ascent.cmi parsing/ast.cmi \ contrib/interface/ctast.cmo kernel/environ.cmi pretyping/evarutil.cmi \ pretyping/evd.cmi library/libobject.cmi library/library.cmi \ @@ -2142,6 +2150,44 @@ contrib/interface/xlate.cmo: contrib/interface/ascent.cmi parsing/ast.cmi \ contrib/interface/xlate.cmx: contrib/interface/ascent.cmi parsing/ast.cmx \ contrib/interface/ctast.cmx library/nameops.cmx kernel/names.cmx \ lib/util.cmx contrib/interface/xlate.cmi +contrib/jprover/jall.cmo: contrib/jprover/jlogic.cmi \ + contrib/jprover/jterm.cmi contrib/jprover/jtunify.cmi \ + contrib/jprover/opname.cmi contrib/jprover/jall.cmi +contrib/jprover/jall.cmx: contrib/jprover/jlogic.cmx \ + contrib/jprover/jterm.cmx contrib/jprover/jtunify.cmx \ + contrib/jprover/opname.cmx contrib/jprover/jall.cmi +contrib/jprover/jlogic.cmo: contrib/jprover/jterm.cmi \ + contrib/jprover/opname.cmi contrib/jprover/jlogic.cmi +contrib/jprover/jlogic.cmx: contrib/jprover/jterm.cmx \ + contrib/jprover/opname.cmx contrib/jprover/jlogic.cmi +contrib/jprover/jprover.cmo: proofs/clenv.cmi library/global.cmi \ + tactics/hipattern.cmi contrib/jprover/jLogic.cmi contrib/jprover/jall.cmi \ + contrib/jprover/jlogic.cmi contrib/jprover/jterm.cmi kernel/names.cmi \ + pretyping/pattern.cmi lib/pp.cmi parsing/printer.cmi \ + proofs/proof_type.cmi kernel/reduction.cmi pretyping/reductionops.cmi \ + tactics/tacentries.cmi proofs/tacmach.cmi tactics/tacticals.cmi \ + tactics/tactics.cmi kernel/term.cmi pretyping/termops.cmi lib/util.cmi +contrib/jprover/jprover.cmx: proofs/clenv.cmx library/global.cmx \ + tactics/hipattern.cmx contrib/jprover/jLogic.cmi contrib/jprover/jall.cmx \ + contrib/jprover/jlogic.cmx contrib/jprover/jterm.cmx kernel/names.cmx \ + pretyping/pattern.cmx lib/pp.cmx parsing/printer.cmx \ + proofs/proof_type.cmx kernel/reduction.cmx pretyping/reductionops.cmx \ + tactics/tacentries.cmx proofs/tacmach.cmx tactics/tacticals.cmx \ + tactics/tactics.cmx kernel/term.cmx pretyping/termops.cmx lib/util.cmx +contrib/jprover/jterm.cmo: contrib/jprover/opname.cmi \ + contrib/jprover/jterm.cmi +contrib/jprover/jterm.cmx: contrib/jprover/opname.cmx \ + contrib/jprover/jterm.cmi +contrib/jprover/jtunify.cmo: contrib/jprover/jtunify.cmi +contrib/jprover/jtunify.cmx: contrib/jprover/jtunify.cmi +contrib/jprover/opname.cmo: contrib/jprover/opname.cmi +contrib/jprover/opname.cmx: contrib/jprover/opname.cmi +contrib/jprover/test.cmo: contrib/jprover/jLogic.cmi contrib/jprover/jall.cmi \ + contrib/jprover/jlogic.cmi contrib/jprover/jterm.cmi \ + contrib/jprover/opname.cmi contrib/jprover/test.cmi +contrib/jprover/test.cmx: contrib/jprover/jLogic.cmi contrib/jprover/jall.cmx \ + contrib/jprover/jlogic.cmx contrib/jprover/jterm.cmx \ + contrib/jprover/opname.cmx contrib/jprover/test.cmi contrib/omega/coq_omega.cmo: parsing/ast.cmi proofs/clenv.cmi \ kernel/closure.cmi parsing/coqlib.cmi kernel/declarations.cmi \ library/declare.cmi kernel/environ.cmi tactics/equality.cmi \ @@ -2214,6 +2260,8 @@ contrib/romega/refl_omega.cmx: parsing/ast.cmx tactics/auto.cmx \ parsing/printer.cmx proofs/proof_type.cmx kernel/reduction.cmx \ kernel/sign.cmx proofs/tacmach.cmx tactics/tacticals.cmx \ tactics/tactics.cmx kernel/term.cmx lib/util.cmx +contrib/xml/xml.cmo: contrib/xml/xml.cmi +contrib/xml/xml.cmx: contrib/xml/xml.cmi contrib/xml/xmlcommand.cmo: kernel/declarations.cmi library/declare.cmi \ kernel/environ.cmi pretyping/evd.cmi library/global.cmi library/lib.cmi \ library/libobject.cmi library/library.cmi library/nameops.cmi \ @@ -2234,8 +2282,6 @@ contrib/xml/xmlentries.cmo: lib/util.cmi toplevel/vernacinterp.cmi \ contrib/xml/xmlcommand.cmi contrib/xml/xmlentries.cmx: lib/util.cmx toplevel/vernacinterp.cmx \ contrib/xml/xmlcommand.cmx -contrib/xml/xml.cmo: contrib/xml/xml.cmi -contrib/xml/xml.cmx: contrib/xml/xml.cmi tactics/tauto.cmo: parsing/grammar.cma kernel/names.cmo parsing/ast.cmo parsing/g_tactic.cmo parsing/g_ltac.cmo parsing/g_constr.cmo tactics/tauto.cmx: parsing/grammar.cma kernel/names.cmo parsing/ast.cmo parsing/g_tactic.cmo parsing/g_ltac.cmo parsing/g_constr.cmo contrib/correctness/psyntax.cmo: parsing/grammar.cma @@ -42,7 +42,8 @@ LOCALINCLUDES=-I config -I tools -I scripts -I lib -I kernel -I library \ -I contrib/omega -I contrib/romega \ -I contrib/ring -I contrib/xml \ -I contrib/extraction -I contrib/correctness \ - -I contrib/interface -I contrib/fourier + -I contrib/interface -I contrib/fourier \ + -I contrib/jprover MLINCLUDES=$(LOCALINCLUDES) -I $(MYCAMLP4LIB) @@ -224,9 +225,15 @@ CORRECTNESSCMO=contrib/correctness/pmisc.cmo \ contrib/correctness/pwp.cmo contrib/correctness/pmlize.cmo \ contrib/correctness/ptactic.cmo contrib/correctness/psyntax.cmo +JPROVERCMO=contrib/jprover/opname.cmo \ + contrib/jprover/jterm.cmo contrib/jprover/jlogic.cmo \ + contrib/jprover/jtunify.cmo contrib/jprover/jall.cmo \ + contrib/jprover/jprover.cmo + + CONTRIB=$(OMEGACMO) $(ROMEGACMO) $(RINGCMO) $(FIELDCMO) $(XMLCMO) \ $(FOURIERCMO) \ - $(EXTRACTIONCMO) $(CORRECTNESSCMO) + $(EXTRACTIONCMO) $(CORRECTNESSCMO) $(JPROVERCMO) CMA=$(CLIBS) $(CAMLP4OBJS) CMXA=$(CMA:.cma=.cmxa) @@ -527,6 +534,8 @@ INTERFACEV0 = contrib/interface/Centaur.vo contrib/interface/vernacrc FOURIERVO = contrib/fourier/Fourier_util.vo contrib/fourier/Fourier.vo +JPROVERVO = contrib/jprover/JProver.vo + contrib/interface/Centaur.vo: contrib/interface/Centaur.v $(INTERFACE) $(BESTCOQTOP) -boot -byte $(COQINCLUDES) -compile $* @@ -535,7 +544,8 @@ contrib/interface/AddDad.vo: contrib/interface/AddDad.v $(INTERFACE) states/init CONTRIBVO = $(OMEGAVO) $(ROMEGAVO) $(RINGVO) $(FIELDVO) $(XMLVO) \ $(CORRECTNESSVO)\ - $(INTERFACEV0) $(FOURIERVO) + $(INTERFACEV0) $(FOURIERVO) \ + $(JPROVERVO) $(CONTRIBVO): states/initial.coq @@ -548,6 +558,7 @@ extraction: $(EXTRACTIONCMO) $(EXTRACTIONVO) correctness: $(CORRECTNESSCMO) $(CORRECTNESSVO) field: $(FIELDVO) $(FIELDCMO) fourier: $(FOURIERVO) $(FOURIERCMO) +jprover: $(JPROVERVO) $(JPROVERCMO) ALLVO = $(INITVO) $(THEORIESVO) $(CONTRIBVO) $(EXTRACTIONVO) diff --git a/contrib/jprover/JProver.v b/contrib/jprover/JProver.v new file mode 100644 index 000000000..5c0b0f3a1 --- /dev/null +++ b/contrib/jprover/JProver.v @@ -0,0 +1,14 @@ +Declare ML Module "opname" "jterm" "jlogic" "jtunify" "jall" "jprover". + +Grammar tactic simple_tactic: ast := + jprover0 [ "Jp" ] -> [ (Jp) ] + | jprover1 [ "Jp" pure_numarg($num)] -> [ (Jpn $num) ]. + +Syntax tactic level 0: + | jprover0 [<<(Jp)>>] -> ["Jp"] + | jprover1 [<<(Jp $num)>>] -> ["Jp " $num]. + +(* +Grammar tactic simple_tactic: ast := + jprover [ "Andl" identarg($id)] -> [ (Andl $id) ]. +*) diff --git a/contrib/jprover/README b/contrib/jprover/README new file mode 100644 index 000000000..2dfb42827 --- /dev/null +++ b/contrib/jprover/README @@ -0,0 +1,66 @@ +An intuitionistic first-order theorem prover -- JProver. + +Usage: + +Require JProver. +Jp [num]. + +Whem [num] is provided, proof is done automatically with +the multiplicity limit [num], otherwise no limit is forced +and JProver may not terminate. + +Example: + +Require JProver. +Coq < Goal (P:Prop) P->P. +1 subgoal + +============================ + (P:Prop)P->P + +Unnamed_thm < Jp 1. +Proof is built. +Subtree proved! +----------------------------------------- + +Description: +JProver is a theorem prover for first-order intuitionistic logic. +It is originally implemented by Stephan Schmitt and then integrated into +MetaPRL by Aleksey Nogin (see jall.ml). After this, Huang extracted the +necessary ML-codes from MetaPRL and then integrated it into Coq. + +Structure of this directory: +This directory contains + + README ------ this file + jall.ml ------ the main module of JProver + jtunify.ml ------ string unification procedures for jall.ml + jlogic.ml ------ interface module of jall.ml + jterm.ml + opname.ml ------ implement the infrastructure for jall.ml + jprover.ml ------ the interface of jall.ml to Coq + JProver.v ------ declaration for Coq + Makefile ------ the makefile + go ------ batch file to load JProver to Coq dynamically + + +Comments: +1. The original <jall.ml> is located in meta-prl/refiner/reflib of the +MetaPRL directory. Some parts of this file are modified by Huang. + +2. <jtunify.ml> is also located in meta-prl/refiner/reflib with no modification. + +3. <jlogic.ml> is modified from meta-prl/refiner/reflib/jlogic_sig.mlz. + +4. <jterm.ml> and <opname.ml> are modified from the standard term module +of MetaPRL in meta-prl/refiner/term_std. + +5. The Jp tactic currently cannot prove formula as + ((x:nat) (P x)) -> (EX y:nat| (P y)), which requires extra constants +in the domain when the left-All rule is applied. + + + +by Huang Guan-Shieng (Guan-Shieng.Huang@lri.fr), March 2002. + + diff --git a/contrib/jprover/jLogic.mli b/contrib/jprover/jLogic.mli new file mode 100644 index 000000000..a90797911 --- /dev/null +++ b/contrib/jprover/jLogic.mli @@ -0,0 +1,40 @@ +(* The interface to manipulate [jterms], which is + extracted and modified from Meta-Prl. *) + +type rule = + Ax | Andr | Andl | Orr | Orr1 | Orr2 | Orl | Impr | Impl | Negr | Negl + | Allr | Alll| Exr | Exl | Fail | Falsel | Truer + +module type JLogicSig = + sig + val is_all_term : Jterm.term -> bool + val dest_all : Jterm.term -> string * Jterm.term * Jterm.term + val is_exists_term : Jterm.term -> bool + val dest_exists : Jterm.term -> string * Jterm.term * Jterm.term + val is_and_term : Jterm.term -> bool + val dest_and : Jterm.term -> Jterm.term * Jterm.term + val is_or_term : Jterm.term -> bool + val dest_or : Jterm.term -> Jterm.term * Jterm.term + val is_implies_term : Jterm.term -> bool + val dest_implies : Jterm.term -> Jterm.term * Jterm.term + val is_not_term : Jterm.term -> bool + val dest_not : Jterm.term -> Jterm.term + type inf_step = rule * (string * Jterm.term) * (string * Jterm.term) + type inference = inf_step list + val empty_inf : inference + val append_inf : + inference -> (string * Jterm.term) -> (string * Jterm.term) -> rule -> inference + val print_inf : inference -> unit + end + +module JLogic : JLogicSig + +val show_loading : string -> unit + +type my_Debug = { + mutable debug_name : string; + mutable debug_description : string; + debug_value : bool; +} +val create_debug : 'a -> bool ref +val ruletable : rule -> string diff --git a/contrib/jprover/jall.ml b/contrib/jprover/jall.ml new file mode 100644 index 000000000..77674c7b8 --- /dev/null +++ b/contrib/jprover/jall.ml @@ -0,0 +1,4698 @@ +(* + * JProver first-order automated prover. See the interface file + * for more information and a list of references for JProver. + * + * ---------------------------------------------------------------- + * + * This file is part of MetaPRL, a modular, higher order + * logical framework that provides a logical programming + * environment for OCaml and other languages. + * + * See the file doc/index.html for information on Nuprl, + * OCaml, and more information about this system. + * + * Copyright (C) 2000 Stephan Schmitt + * + * This program is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * This program is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with this program; if not, write to the Free Software + * Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA. + * + * Author: Stephan Schmitt <schmitts@spmail.slu.edu> + * Modified by: Aleksey Nogin <nogin@cs.cornell.edu> + *) + +(*: All of Huang's modifications of this file are quoted or denoted + by comments followed by a colon. +:*) + +(*: +open Mp_debug + +open Refiner.Refiner +open Term +open TermType +open TermOp +open TermSubst +open TermMan +open RefineError +open Opname +:*) + +open Jterm +open Opname +open Jlogic +open Jtunify + +let ruletable = Jlogic.ruletable + +(*: +let free_var_op = make_opname ["free_variable";"Jprover"] +let jprover_op = make_opname ["string";"Jprover"] +:*) +let free_var_op = make_opname ["free_variable"; "Jprover"] +let jprover_op = make_opname ["jprover"; "string"] + +module JProver (JLogic : JLogicSig) = +struct + type polarity = I | O + + type connective = And | Or | Neg | Imp | All | Ex | At | Null + + type ptype = Alpha | Beta | Gamma | Delta | Phi | Psi | PNull + + type stype = + Alpha_1 | Alpha_2 | Beta_1 | Beta_2 | Gamma_0 | Delta_0 + | Phi_0 | Psi_0 | PNull_0 + + type pos = {name : string; + address : int list; + op : connective; + pol : polarity; + pt : ptype; + st : stype; + label : term} + + type 'pos ftree = + Empty + | NodeAt of 'pos + | NodeA of 'pos * ('pos ftree) array + + type atom = {aname : string; + aaddress : int list; + aprefix : string list; + apredicate : operator; + apol : polarity; + ast : stype; + alabel : term} + + type atom_relations = atom * atom list * atom list +(* all atoms except atom occur in [alpha_set] and [beta_set] of atom*) + +(* beta proofs *) + + type bproof = BEmpty + | RNode of string list * bproof + | CNode of (string * string) + | BNode of string * (string list * bproof) * (string list * bproof) + | AtNode of string * (string * string) + +(* Assume only constants for instantiations, not adapted to terms yet *) + type inf = rule * term * term + +(* proof tree for pretty print and permutation *) + type 'inf ptree = + PEmpty + | PNodeAx of 'inf + | PNodeA of 'inf * 'inf ptree + | PNodeB of 'inf * 'inf ptree * 'inf ptree + + module OrderedAtom = + struct + type t = atom + let compare a1 a2 = if (a1.aname) = (a2.aname) then 0 else + if (a1.aname) < (a2.aname) then -1 else 1 + end + + module AtomSet = Set.Make(OrderedAtom) + + module OrderedString = + struct + type t = string + let compare a1 a2 = if a1 = a2 then 0 else + if a1 < a2 then -1 else 1 + end + + module StringSet = Set.Make(OrderedString) + +(*i let _ = + show_loading "Loading Jall%t" i*) + + let debug_jprover = + create_debug (**) + { debug_name = "jprover"; + debug_description = "Display Jprover operations"; + debug_value = false + } + + let jprover_bug = Invalid_argument "Jprover bug (Jall module)" + +(*****************************************************************) + +(************* printing function *************************************) + +(************ printing T-string unifiers ****************************) + +(* ******* printing ********** *) + + let rec list_to_string s = + match s with + [] -> "" + | f::r -> + f^"."^(list_to_string r) + + let rec print_eqlist eqlist = + match eqlist with + [] -> + print_endline "" + | (atnames,f)::r -> + let (s,t) = f in + let ls = list_to_string s + and lt = list_to_string t in + begin + print_endline ("Atom names: "^(list_to_string atnames)); + print_endline (ls^" = "^lt); + print_eqlist r + end + + let print_equations eqlist = + begin + Format.open_box 0; + Format.force_newline (); + print_endline "Equations:"; + print_eqlist eqlist; + Format.force_newline (); + end + + let rec print_subst sigma = + match sigma with + [] -> + print_endline "" + | f::r -> + let (v,s) = f in + let ls = list_to_string s in + begin + print_endline (v^" = "^ls); + print_subst r + end + + let print_tunify sigma = + let (n,subst) = sigma in + begin + print_endline " "; + print_endline ("MaxVar = "^(string_of_int (n-1))); + print_endline " "; + print_endline "Substitution:"; + print_subst subst; + print_endline " " + end + +(*****************************************************) + +(********* printing atoms and their relations ***********************) + + let print_stype st = + match st with + Alpha_1 -> Format.print_string "Alpha_1" + | Alpha_2 -> Format.print_string "Alpha_2" + | Beta_1 -> Format.print_string "Beta_1" + | Beta_2 -> Format.print_string "Beta_2" + | Gamma_0 -> Format.print_string "Gamma_0" + | Delta_0 -> Format.print_string "Delta_0" + | Phi_0 -> Format.print_string "Phi_0" + | Psi_0 -> Format.print_string "Psi_0" + | PNull_0 -> Format.print_string "PNull_0" + + let print_pol pol = + if pol = O then + Format.print_string "O" + else + Format.print_string "I" + + let rec print_address int_list = + match int_list with + [] -> + Format.print_string "" + | hd::rest -> + begin + Format.print_int hd; + print_address rest + end + + let rec print_prefix prefix_list = + match prefix_list with + [] -> Format.print_string "" + | f::r -> + begin + Format.print_string f; + print_prefix r + end + + let print_atom at tab = + let ({aname=x; aaddress=y; aprefix=z; apredicate=p; apol=a; ast=b; alabel=label}) = at in + begin + Format.print_string ("{aname="^x^"; address="); + print_address y; + Format.print_string "; "; + Format.force_newline (); + Format.print_break (tab+1) (tab+1); + Format.print_string "prefix="; + print_prefix z; + Format.print_string "; predicate=<abstr>; "; + Format.print_break (tab+1) (tab+1); + Format.print_break (tab+1) (tab+1); + Format.print_string "pol="; + print_pol a; + Format.print_string "; stype="; + print_stype b; + Format.print_string "; arguments=[<abstr>]"; + Format.print_string "\n alabel="; + print_term stdout label; + Format.print_string "}" + end + + let rec print_atom_list set tab = + match set with + [] -> Format.print_string "" + | (f::r) -> + begin + Format.force_newline (); + Format.print_break (tab) (tab); + print_atom f tab; + print_atom_list r (tab) + end + + let rec print_atom_info atom_relation = + match atom_relation with + [] -> Format.print_string "" + | (a,b,c)::r -> + begin + Format.print_string "atom:"; + Format.force_newline (); + Format.print_break 3 3; + print_atom a 3; + Format.force_newline (); + Format.print_break 0 0; + Format.print_string "alpha_set:"; + print_atom_list b 3; + Format.force_newline (); + Format.print_break 0 0; + Format.print_string "beta_set:"; + print_atom_list c 3; + Format.force_newline (); + Format.force_newline (); + Format.print_break 0 0; + print_atom_info r + end + +(*************** print formula tree, tree ordering etc. ***********) + + let print_ptype pt = + match pt with + Alpha -> Format.print_string "Alpha" + | Beta -> Format.print_string "Beta" + | Gamma -> Format.print_string "Gamma" + | Delta -> Format.print_string "Delta" + | Phi -> Format.print_string "Phi" + | Psi -> Format.print_string "Psi" + | PNull -> Format.print_string "PNull" + + let print_op op = + match op with + At -> Format.print_string "Atom" + | Neg -> Format.print_string "Neg" + | And -> Format.print_string "And" + | Or -> Format.print_string "Or" + | Imp -> Format.print_string "Imp" + | Ex -> Format.print_string "Ex" + | All -> Format.print_string "All" + | Null -> Format.print_string "Null" + + let print_position position tab = + let ({name=x; address=y; op=z; pol=a; pt=b; st=c; label=t}) = position in + begin + Format.print_string ("{name="^x^"; address="); + print_address y; + Format.print_string "; "; + Format.force_newline (); + Format.print_break (tab+1) 0; +(* Format.print_break 0 3; *) + Format.print_string "op="; + print_op z; + Format.print_string "; pol="; + print_pol a; + Format.print_string "; ptype="; + print_ptype b; + Format.print_string "; stype="; + print_stype c; + Format.print_string ";"; + Format.force_newline (); + Format.print_break (tab+1) 0; + Format.print_string "label="; + Format.print_break 0 0; + Format.force_newline (); + Format.print_break tab 0; + print_term stdout t; + Format.print_string "}" + end + + let rec pp_ftree_list tree_list tab = + let rec pp_ftree ftree new_tab = + let dummy = String.make (new_tab-2) ' ' in + match ftree with + Empty -> Format.print_string "" + | NodeAt(position) -> + begin + Format.force_newline (); + Format.print_break new_tab 0; + print_string (dummy^"AtomNode: "); +(* Format.force_newline (); + Format.print_break 0 3; +*) + print_position position new_tab; + Format.force_newline (); + Format.print_break new_tab 0 + end + | NodeA(position,subtrees) -> + let tree_list = Array.to_list subtrees in + begin + Format.force_newline (); + Format.print_break new_tab 0; + Format.print_break 0 0; + print_string (dummy^"InnerNode: "); + print_position position new_tab; + Format.force_newline (); + Format.print_break 0 0; + pp_ftree_list tree_list (new_tab-3) + end + in + let new_tab = tab+5 in + match tree_list with + [] -> Format.print_string "" + | first::rest -> + begin + pp_ftree first new_tab; + pp_ftree_list rest tab + end + + let print_ftree ftree = + begin + Format.open_box 0; + Format.print_break 3 0; + pp_ftree_list [ftree] 0; + Format.print_flush () + end + + let rec stringlist_to_string stringlist = + match stringlist with + [] -> "." + | f::r -> + let rest_s = stringlist_to_string r in + (f^"."^rest_s) + + let rec print_stringlist slist = + match slist with + [] -> + Format.print_string "" + | f::r -> + begin + Format.print_string (f^"."); + print_stringlist r + end + + let rec pp_bproof_list tree_list tab = + let rec pp_bproof ftree new_tab = + let dummy = String.make (new_tab-2) ' ' in + match ftree with + BEmpty -> Format.print_string "" + | CNode((c1,c2)) -> + begin + Format.open_box 0; + Format.force_newline (); + Format.print_break (new_tab-10) 0; + Format.open_box 0; + Format.force_newline (); + Format.print_string (dummy^"CloseNode: connection = ("^c1^","^c2^")"); + Format.print_flush(); +(* Format.force_newline (); + Format.print_break 0 3; +*) + Format.open_box 0; + Format.print_break new_tab 0; + Format.print_flush() + end + | AtNode(posname,(c1,c2)) -> + begin + Format.open_box 0; + Format.force_newline (); + Format.print_break (new_tab-10) 0; + Format.open_box 0; + Format.force_newline (); + Format.print_string (dummy^"AtNode: pos = "^posname^" conneciton = ("^c1^","^c2^")"); + Format.print_flush(); +(* Format.force_newline (); + Format.print_break 0 3; +*) + Format.open_box 0; + Format.print_break new_tab 0; + Format.print_flush() + end + | RNode(alpha_layer,bproof) -> + let alpha_string = stringlist_to_string alpha_layer in + begin + Format.open_box 0; + Format.force_newline (); + Format.print_break new_tab 0; + Format.print_break 0 0; + Format.force_newline (); + Format.print_flush(); + Format.open_box 0; + print_string (dummy^"RootNode: "^alpha_string); + Format.print_flush(); + Format.open_box 0; + Format.print_break 0 0; + Format.print_flush(); + pp_bproof_list [bproof] (new_tab-3) + end + | BNode(posname,(alph1,bproof1),(alph2,bproof2)) -> + let alpha_string1 = stringlist_to_string alph1 + and alpha_string2 = stringlist_to_string alph2 in + begin + Format.open_box 0; + Format.force_newline (); + Format.print_break new_tab 0; + Format.print_break 0 0; + Format.force_newline (); + Format.print_flush(); + Format.open_box 0; + print_string (dummy^"BetaNode: pos = "^posname^" layer1 = "^alpha_string1^" layer2 = "^alpha_string2); + Format.print_flush(); + Format.open_box 0; + Format.print_break 0 0; + Format.print_flush(); + pp_bproof_list [bproof1;bproof2] (new_tab-3) + end + in + let new_tab = tab+5 in + match tree_list with + [] -> Format.print_string "" + | first::rest -> + begin + pp_bproof first new_tab; + pp_bproof_list rest tab + end + + let rec print_pairlist pairlist = + match pairlist with + [] -> Format.print_string "" + | (a,b)::rest -> + begin + Format.print_break 1 1; + Format.print_string ("("^a^","^b^")"); + print_pairlist rest + end + + let print_beta_proof bproof = + begin + Format.open_box 0; + Format.force_newline (); + Format.force_newline (); + Format.print_break 3 0; + pp_bproof_list [bproof] 0; + Format.force_newline (); + Format.force_newline (); + Format.force_newline (); + Format.print_flush () + end + + let rec print_treelist treelist = + match treelist with + [] -> + print_endline "END"; + | f::r -> + begin + print_ftree f; + Format.open_box 0; + print_endline ""; + print_endline ""; + print_endline "NEXT TREE"; + print_endline ""; + print_endline ""; + print_treelist r; + Format.print_flush () + end + + let rec print_set_list set_list = + match set_list with + [] -> "" + | f::r -> + (f.aname)^" "^(print_set_list r) + + let print_set set = + let set_list = AtomSet.elements set in + if set_list = [] then "empty" + else + print_set_list set_list + + let print_string_set set = + let set_list = StringSet.elements set in + print_stringlist set_list + + let rec print_list_sets list_of_sets = + match list_of_sets with + [] -> Format.print_string "" + | (pos,fset)::r -> + begin + Format.print_string (pos^": "); (* first element = node which successors depend on *) + print_stringlist (StringSet.elements fset); + Format.force_newline (); + print_list_sets r + end + + let print_ordering list_of_sets = + begin + Format.open_box 0; + print_list_sets list_of_sets; + Format.print_flush () + end + + let rec print_triplelist triplelist = + match triplelist with + [] -> Format.print_string "" + | ((a,b),i)::rest -> + begin + Format.print_break 1 1; + Format.print_string ("(("^a^","^b^"),"^(string_of_int i)^")"); + print_triplelist rest + end + + let print_pos_n pos_n = + Format.print_int pos_n + + let print_formula_info ftree ordering pos_n = + begin + print_ftree ftree; + Format.open_box 0; + Format.force_newline (); + print_ordering ordering; + Format.force_newline (); + Format.force_newline (); + Format.print_string "number of positions: "; + print_pos_n pos_n; + Format.force_newline (); + print_endline ""; + print_endline ""; + Format.print_flush () + end + +(* print sequent proof tree *) + + let pp_rule (pos,r,formula,term) tab = + let rep = ruletable r in + if List.mem rep ["Alll";"Allr";"Exl";"Exr"] then + begin + Format.open_box 0; +(* Format.force_newline (); *) + Format.print_break tab 0; + Format.print_string (pos^": "^rep^" "); + Format.print_flush (); +(* Format.print_break tab 0; + Format.force_newline (); + Format.print_break tab 0; +*) + + Format.open_box 0; + print_term stdout formula; + Format.print_flush (); + Format.open_box 0; + Format.print_string " "; + Format.print_flush (); + Format.open_box 0; + print_term stdout term; + Format.force_newline (); + Format.force_newline (); + Format.print_flush () + end + else + begin + Format.open_box 0; + Format.print_break tab 0; + Format.print_string (pos^": "^rep^" "); + Format.print_flush (); + Format.open_box 0; +(* Format.print_break tab 0; *) + Format.force_newline (); +(* Format.print_break tab 0; *) + print_term stdout formula; + Format.force_newline () + end + + let last addr = + if addr = "" + then "" + else + String.make 1 (String.get addr (String.length addr-1)) + + let rest addr = + if addr = "" + then "" + else + String.sub addr 0 ((String.length addr) - 1) + + let rec get_r_chain addr = + if addr = "" then + 0 + else + let l = last addr in + if l = "l" then + 0 + else (* l = "r" *) + let rs = rest addr in + 1 + (get_r_chain rs) + + let rec tpp seqtree tab addr = + match seqtree with + | PEmpty -> raise jprover_bug + | PNodeAx(rule) -> + let (pos,r,p,pa) = rule in + begin + pp_rule (pos,r,p,pa) tab; +(* Format.force_newline (); *) +(* let mult = get_r_chain addr in *) +(* Format.print_break 100 (tab - (3 * mult)) *) + end + | PNodeA(rule,left) -> + let (pos,r,p,pa) = rule in + begin + pp_rule (pos,r,p,pa) tab; + tpp left tab addr + end + | PNodeB(rule,left,right) -> + let (pos,r,p,pa) = rule in + let newtab = tab + 3 in + begin + pp_rule (pos,r,p,pa) tab; +(* Format.force_newline (); *) +(* Format.print_break 100 newtab; *) + (tpp left newtab (addr^"l")); + (tpp right newtab (addr^"r")) + end + + let tt seqtree = + begin + Format.open_box 0; + tpp seqtree 0 ""; + Format.force_newline (); + Format.close_box (); + Format.print_newline () + end + +(************ END printing functions *********************************) + +(************ Beta proofs and redundancy deletion **********************) + + let rec remove_dups_connections connection_list = + match connection_list with + [] -> [] + | (c1,c2)::r -> + if (List.mem (c1,c2) r) or (List.mem (c2,c1) r) then + (* only one direction variant of a connection stays *) + remove_dups_connections r + else + (c1,c2)::(remove_dups_connections r) + + let rec remove_dups_list list = + match list with + [] -> [] + | f::r -> + if List.mem f r then + remove_dups_list r + else + f::(remove_dups_list r) + + let beta_pure alpha_layer connections beta_expansions = + let (l1,l2) = List.split connections in + let test_list = l1 @ l2 @ beta_expansions in + begin +(* Format.open_box 0; + print_endline ""; + print_stringlist alpha_layer; + Format.print_flush(); + Format.open_box 0; + print_endline ""; + print_stringlist test_list; + print_endline ""; + Format.print_flush(); +*) + not (List.exists (fun x -> (List.mem x test_list)) alpha_layer) + end + + let rec apply_bproof_purity bproof = + match bproof with + BEmpty -> + raise jprover_bug + | CNode((c1,c2)) -> + bproof,[(c1,c2)],[] + | AtNode(_,(c1,c2)) -> + bproof,[(c1,c2)],[] + | RNode(alpha_layer,subproof) -> + let (opt_subproof,min_connections,beta_expansions) = + apply_bproof_purity subproof in + (RNode(alpha_layer,opt_subproof),min_connections,beta_expansions) + | BNode(pos,(alph1,subp1),(alph2,subp2)) -> + let (opt_subp1,min_conn1,beta_exp1) = apply_bproof_purity subp1 in + if beta_pure alph1 min_conn1 beta_exp1 then + begin +(* print_endline ("Left layer of "^pos); *) + (opt_subp1,min_conn1,beta_exp1) + end + else + let (opt_subp2,min_conn2,beta_exp2) = apply_bproof_purity subp2 in + if beta_pure alph2 min_conn2 beta_exp2 then + begin +(* print_endline ("Right layer of "^pos); *) + (opt_subp2,min_conn2,beta_exp2) + end + else + let min_conn = remove_dups_connections (min_conn1 @ min_conn2) + and beta_exp = remove_dups_list ([pos] @ beta_exp1 @ beta_exp2) in + (BNode(pos,(alph1,opt_subp1),(alph2,opt_subp2)),min_conn,beta_exp) + + let bproof_purity bproof = + let (opt_bproof,min_connections,_) = apply_bproof_purity bproof in + opt_bproof,min_connections + +(*********** split permutation *****************) + + let rec apply_permutation bproof rep_name direction act_blayer = + match bproof with + BEmpty | RNode(_,_) -> + raise jprover_bug + | AtNode(cx,(c1,c2)) -> + bproof,act_blayer + | CNode((c1,c2)) -> + bproof,act_blayer + | BNode(pos,(alph1,subp1),(alph2,subp2)) -> + if rep_name = pos then + let (new_blayer,replace_branch) = + if direction = "left" then + (alph1,subp1) + else (* direciton = "right" *) + (alph2,subp2) + in + (match replace_branch with + CNode((c1,c2)) -> + (AtNode(c1,(c1,c2))),new_blayer (* perform atom expansion at c1 *) + | _ -> + replace_branch,new_blayer + ) + else + let pproof1,new_blayer1 = apply_permutation subp1 rep_name direction act_blayer in + let pproof2,new_blayer2 = apply_permutation subp2 rep_name direction new_blayer1 in + (BNode(pos,(alph1,pproof1),(alph2,pproof2))),new_blayer2 + + let split_permutation pname opt_bproof = + match opt_bproof with + RNode(alayer,BNode(pos,(alph1,opt_subp1),(alph2,opt_subp2))) -> + if pos = pname then +(* if topmost beta expansion agrees with pname, then *) +(* only split the beta proof and give back the two subproofs *) + let (osubp1,min_con1) = bproof_purity opt_subp1 + and (osubp2,min_con2) = bproof_purity opt_subp2 in +(* there will be no purity reductions in the beta subproofs. We use this *) +(* predicate to collect the set of used leaf-connections in each subproof*) + ((RNode((alayer @ alph1),osubp1),min_con1), + (RNode((alayer @ alph2),osubp2),min_con2) + ) +(* we combine the branch after topmost beta expansion at pos into one root alpha layer *) +(* -- the beta expansion node pos will not be needed in this root layer *) + else + let perm_bproof1,balph1 = apply_permutation + (BNode(pos,(alph1,opt_subp1),(alph2,opt_subp2))) pname "left" [] + and perm_bproof2,balph2 = apply_permutation + (BNode(pos,(alph1,opt_subp1),(alph2,opt_subp2))) pname "right" [] in + + begin +(* print_endline " "; + print_beta_proof perm_bproof1; + print_endline" " ; + print_beta_proof perm_bproof2; + print_endline" "; +*) + let (osubp1,min_con1) = bproof_purity perm_bproof1 + and (osubp2,min_con2) = bproof_purity perm_bproof2 in + ((RNode((alayer @ balph1),osubp1),min_con1), + (RNode((alayer @ balph2),osubp2),min_con2) + ) + end +(* we combine the branch after the NEW topmost beta expansion at bpos *) +(* into one root alpha layer -- the beta expansion node bpos will not be *) +(* needed in this root layer *) + | _ -> + raise jprover_bug + +(*********** END split permutation *****************) + + let rec list_del list_el el_list = + match el_list with + [] -> + raise jprover_bug + | f::r -> + if list_el = f then + r + else + f::(list_del list_el r) + + let rec list_diff del_list check_list = + match del_list with + [] -> + [] + | f::r -> + if List.mem f check_list then + list_diff r check_list + else + f::(list_diff r check_list) + +(* let rec compute_alpha_layer ftree_list = + match ftree_list with + [] -> + [],[],[] + | f::r -> + (match f with + Empty -> + raise jprover_bug + | NodeAt(pos) -> + let pn = pos.name + and (rnode,ratom,borderings) = compute_alpha_layer r in + ((pn::rnode),(pn::ratom),borderings) + | NodeA(pos,suctrees) -> + let pn = pos.name in + if pos.pt = Beta then + let (rnode,ratom,borderings) = compute_alpha_layer r in + ((pn::rnode),(ratom),(f::borderings)) + else + let suclist = Array.to_list suctrees in + compute_alpha_layer (suclist @ r) + ) + + let rec compute_connection alpha_layer union_atoms connections = + match connections with + [] -> ("none","none") + | (c,d)::r -> + if (List.mem c union_atoms) & (List.mem d union_atoms) then + let (c1,c2) = + if List.mem c alpha_layer then + (c,d) + else + if List.mem d alpha_layer then + (d,c) (* then, d is supposed to occur in [alpha_layer] *) + else + raise (Invalid_argument "Jprover bug: connection match failure") + in + (c1,c2) + else + compute_connection alpha_layer union_atoms r + + let get_beta_suctrees btree = + match btree with + Empty | NodeAt(_) -> raise jprover_bug + | NodeA(pos,suctrees) -> + let b1tree = suctrees.(0) + and b2tree = suctrees.(1) in + (pos.name,b1tree,b2tree) + + let rec build_beta_proof alpha_layer union_atoms beta_orderings connections = + let (c1,c2) = compute_connection alpha_layer union_atoms connections in +(* [c1] is supposed to occur in the lowmost alpha layer of the branch, *) +(* i.e. [aplha_layer] *) + if (c1,c2) = ("none","none") then + (match beta_orderings with + [] -> raise jprover_bug + | btree::r -> + let (beta_pos,suctree1,suctree2) = get_beta_suctrees btree in + let (alpha_layer1, atoms1, bordering1) = compute_alpha_layer [suctree1] + and (alpha_layer2, atoms2, bordering2) = compute_alpha_layer [suctree2] in + let bproof1,beta1,closure1 = + build_beta_proof alpha_layer1 (atoms1 @ union_atoms) + (bordering1 @ r) connections + in + let bproof2,beta2,closure2 = + build_beta_proof alpha_layer2 (atoms2 @ union_atoms) + (bordering2 @ r) connections in + (BNode(beta_pos,(alpha_layer1,bproof1),(alpha_layer2,bproof2))),(1+beta1+beta2),(closure1+closure2) + ) + else + CNode((c1,c2)),0,1 + + let construct_beta_proof ftree connections = + let (root_node,root_atoms,beta_orderings) = compute_alpha_layer [ftree] + in + let beta_proof,beta_exp,closures = + build_beta_proof root_node root_atoms beta_orderings connections in + (RNode(root_node,beta_proof)),beta_exp,closures +*) + + +(* *********** New Version with direct computation from extension proof **** *) +(* follows a DIRECT step from proof histories via pr-connection orderings to opt. beta-proofs *) + + let rec compute_alpha_layer ftree_list = + match ftree_list with + [] -> + [] + | f::r -> + (match f with + Empty -> + raise jprover_bug + | NodeAt(pos) -> + let rnode = compute_alpha_layer r in + (pos.name::rnode) + | NodeA(pos,suctrees) -> + if pos.pt = Beta then + let rnode = compute_alpha_layer r in + (pos.name::rnode) + else + let suclist = Array.to_list suctrees in + compute_alpha_layer (suclist @ r) + ) + + let rec compute_beta_difference c1_context c2_context act_context = + match c1_context,c2_context with + ([],c2_context) -> + (list_diff c2_context act_context) +(* both connection partners in the same submatrix; [c1] already isolated *) + | ((fc1::rc1),[]) -> + [] (* [c2] is a reduction step, i.e. isolated before [c1] *) + | ((fc1::rc1),(fc2::rc2)) -> + if fc1 = fc2 then (* common initial beta-expansions *) + compute_beta_difference rc1 rc2 act_context + else + (list_diff c2_context act_context) + + let rec non_closed beta_proof_list = + match beta_proof_list with + [] -> + false + | bpf::rbpf -> + (match bpf with + RNode(_,_) -> raise (Invalid_argument "Jprover bug: invalid beta-proof") + | AtNode(_,_) -> raise (Invalid_argument "Jprover bug: invalid beta-proof") + | BEmpty -> true + | CNode(_) -> non_closed rbpf + | BNode(pos,(_,bp1),(_,bp2)) -> non_closed ([bp1;bp2] @ rbpf) + ) + + let rec cut_context pos context = + match context with + [] -> + raise (Invalid_argument "Jprover bug: invalid context element") + | (f,num)::r -> + if pos = f then + context + else + cut_context pos r + + let compute_tree_difference beta_proof c1_context = + match beta_proof with + RNode(_,_) -> raise (Invalid_argument "Jprover bug: invalid beta-proof") + | CNode(_) -> raise (Invalid_argument "Jprover bug: invalid beta-proof") + | AtNode(_,_) -> raise (Invalid_argument "Jprover bug: invalid beta-proof") + | BEmpty -> c1_context + | BNode(pos,_,_) -> +(* print_endline ("actual root: "^pos); *) + cut_context pos c1_context + + let print_context conn bcontext = + begin + Format.open_box 0; + Format.print_string conn; + Format.print_string ": "; + List.iter (fun x -> let (pos,num) = x in Format.print_string (pos^" "^(string_of_int num)^"")) bcontext; + print_endline " "; + Format.print_flush () + end + + let rec build_opt_beta_proof beta_proof ext_proof beta_atoms beta_layer_list act_context = + let rec add_c2_tree (c1,c2) c2_diff_context = + match c2_diff_context with + [] -> + (CNode(c1,c2),0) + | (f,num)::c2_diff_r -> + let next_beta_proof,next_exp = + add_c2_tree (c1,c2) c2_diff_r in + let (layer1,layer2) = List.assoc f beta_layer_list in + let new_bproof = + if num = 1 then + BNode(f,(layer1,next_beta_proof),(layer2,BEmpty)) + else (* num = 2*) + BNode(f,(layer1,BEmpty),(layer2,next_beta_proof)) + in + (new_bproof,(next_exp+1)) + in + let rec add_beta_expansions (c1,c2) rest_ext_proof c1_diff_context c2_diff_context new_act_context = + match c1_diff_context with + [] -> + let (n_c1,n_c2) = + if c2_diff_context = [] then (* make sure that leaf-connection is first element *) + (c1,c2) + else + (c2,c1) + in + let c2_bproof,c2_exp = add_c2_tree (n_c1,n_c2) c2_diff_context in + if c2_exp <> 0 then (* at least one open branch was generated to isloate [c2] *) + begin +(* print_endline "start with new beta-proof"; *) + let new_bproof,new_exp,new_closures,new_rest_proof = + build_opt_beta_proof c2_bproof rest_ext_proof beta_atoms beta_layer_list (act_context @ new_act_context) in + (new_bproof,(new_exp+c2_exp),(new_closures+1),new_rest_proof) + end + else + begin +(* print_endline "proceed with old beta-proof"; *) + (c2_bproof,c2_exp,1,rest_ext_proof) + end + | (f,num)::c1_diff_r -> + let (layer1,layer2) = List.assoc f beta_layer_list in + let next_beta_proof,next_exp,next_closures,next_ext_proof = + add_beta_expansions (c1,c2) rest_ext_proof c1_diff_r c2_diff_context new_act_context in + let new_bproof = + if num = 1 then + BNode(f,(layer1,next_beta_proof),(layer2,BEmpty)) + else (* num = 2*) + BNode(f,(layer1,BEmpty),(layer2,next_beta_proof)) + in + (new_bproof,(next_exp+1),next_closures,next_ext_proof) + + in + let rec insert_connection beta_proof (c1,c2) rest_ext_proof c1_diff_context c2_diff_context act_context = + begin +(* print_context c1 c1_diff_context; + print_endline ""; + print_context c2 c2_diff_context; + print_endline ""; +*) + match beta_proof with + RNode(_,_) -> raise (Invalid_argument "Jprover bug: invalid beta-proof") + | CNode(_) -> raise (Invalid_argument "Jprover bug: invalid beta-proof") + | AtNode(_,_) -> raise (Invalid_argument "Jprover bug: invalid beta-proof") + | BEmpty -> + add_beta_expansions (c1,c2) rest_ext_proof c1_diff_context c2_diff_context act_context + | BNode(pos,(layer1,sproof1),(layer2,sproof2)) -> +(* print_endline (c1^" "^c2^" "^pos); *) + (match c1_diff_context with + [] -> + raise (Invalid_argument "Jprover bug: invalid beta-proof") + | (f,num)::rest_context -> (* f = pos must hold!! *) + if num = 1 then + let (next_bproof,next_exp,next_closure,next_ext_proof) = + insert_connection sproof1 (c1,c2) rest_ext_proof rest_context c2_diff_context act_context in + (BNode(pos,(layer1,next_bproof),(layer2,sproof2)),next_exp,next_closure,next_ext_proof) + else (* num = 2 *) + let (next_bproof,next_exp,next_closure,next_ext_proof) = + insert_connection sproof2 (c1,c2) rest_ext_proof rest_context c2_diff_context act_context in + (BNode(pos,(layer1,sproof1),(layer2,next_bproof)),next_exp,next_closure,next_ext_proof) + ) + end + + in + match ext_proof with + [] -> + beta_proof,0,0,[] + | (c1,c2)::rproof -> +(* print_endline ("actual connection: "^c1^" "^c2); *) + let c1_context = List.assoc c1 beta_atoms + and c2_context = List.assoc c2 beta_atoms in + let c2_diff_context = compute_beta_difference c1_context c2_context act_context + and c1_diff_context = compute_tree_difference beta_proof c1_context in (* wrt. actual beta-proof *) + let (next_beta_proof,next_exp,next_closures,next_ext_proof) = + insert_connection beta_proof (c1,c2) rproof c1_diff_context c2_diff_context c1_diff_context in + if non_closed [next_beta_proof] then (* at least one branch was generated to isolate [c1] *) + let rest_beta_proof,rest_exp,rest_closures,rest_ext_proof = + build_opt_beta_proof next_beta_proof next_ext_proof beta_atoms beta_layer_list act_context in + rest_beta_proof,(next_exp+rest_exp),(next_closures+rest_closures),rest_ext_proof + else + next_beta_proof,next_exp,next_closures,next_ext_proof + + let rec annotate_atoms beta_context atlist treelist = + let rec annotate_tree beta_context tree atlist = + match tree with + Empty -> + (atlist,[],[]) + | NodeAt(pos) -> + if List.mem pos.name atlist then + let new_atlist = list_del pos.name atlist in + (new_atlist,[(pos.name,beta_context)],[]) + else + (atlist,[],[]) + | NodeA(pos,suctrees) -> + if pos.pt = Beta then + let s1,s2 = suctrees.(0),suctrees.(1) in + let alayer1 = compute_alpha_layer [s1] + and alayer2 = compute_alpha_layer [s2] + and new_beta_context1 = beta_context @ [(pos.name,1)] + and new_beta_context2 = beta_context @ [(pos.name,2)] in + let atlist1,annotates1,blayer_list1 = + annotate_atoms new_beta_context1 atlist [s1] in + let atlist2,annotates2,blayer_list2 = + annotate_atoms new_beta_context2 atlist1 [s2] + in + (atlist2,(annotates1 @ annotates2),((pos.name,(alayer1,alayer2))::(blayer_list1 @ blayer_list2))) + else + annotate_atoms beta_context atlist (Array.to_list suctrees) + in + match treelist with + [] -> (atlist,[],[]) + | f::r -> + let (next_atlist,f_annotates,f_beta_layers) = annotate_tree beta_context f atlist in + let (rest_atlist,rest_annotates,rest_beta_layers) = (annotate_atoms beta_context next_atlist r) + in + (rest_atlist, (f_annotates @ rest_annotates),(f_beta_layers @ rest_beta_layers)) + + let construct_opt_beta_proof ftree ext_proof = + let con1,con2 = List.split ext_proof in + let con_atoms = remove_dups_list (con1 @ con2) in + let (empty_atoms,beta_atoms,beta_layer_list) = annotate_atoms [] con_atoms [ftree] in + let root_node = compute_alpha_layer [ftree] in + let (beta_proof,beta_exp,closures,_) = + build_opt_beta_proof BEmpty ext_proof beta_atoms beta_layer_list [] in + (RNode(root_node,beta_proof)),beta_exp,closures + +(************* permutation ljmc -> lj *********************************) + +(* REAL PERMUTATION STAFF *) + + let subf1 n m subrel = List.mem ((n,m),1) subrel + let subf2 n m subrel = List.mem ((n,m),2) subrel + let tsubf n m tsubrel = List.mem (n,m) tsubrel + +(* Transforms all normal form layers in an LJ proof *) + + let rec modify prooftree (subrel,tsubrel) = + match prooftree with + PEmpty -> + raise jprover_bug + | PNodeAx((pos,inf,form,term)) -> + prooftree,pos + | PNodeA((pos,inf,form,term),left) -> + let t,qpos = modify left (subrel,tsubrel) in + if List.mem inf [Impr;Negr;Allr] then + PNodeA((pos,inf,form,term),t),pos (* layer bound *) + else if qpos = "Orl-True" then + PNodeA((pos,inf,form,term),t),qpos + else if List.mem inf [Andl;Alll;Exl] then + PNodeA((pos,inf,form,term),t),qpos (* simply propagation *) + else if inf = Exr then + if (subf1 pos qpos subrel) then + PNodeA((pos,inf,form,term),t),pos + else t,qpos + else if inf = Negl then + if (subf1 pos qpos subrel) then + PNodeA((pos,inf,form,term),t),"" (* empty string *) + else t,qpos + else (* x = Orr *) + if (subf1 pos qpos subrel) then + PNodeA((pos,Orr1,form,term),t),pos (* make Orr for LJ *) + else if (subf2 pos qpos subrel) then + PNodeA((pos,Orr2,form,term),t),pos (* make Orr for LJ *) + else t,qpos + | PNodeB((pos,inf,form,term),left,right) -> + let t,qpos = modify left (subrel,tsubrel) in + if inf = Andr then + if (or) (qpos = "Orl-True") (subf1 pos qpos subrel) then + let s,rpos = modify right (subrel,tsubrel) in (* Orl-True -> subf *) + if (or) (rpos = "Orl-True") (subf2 pos rpos subrel) then + PNodeB((pos,inf,form,term),t,s),pos + else s,rpos + else t,qpos (* not subf -> not Orl-True *) + else if inf = Impl then + if (subf1 pos qpos subrel) then + let s,rpos = modify right (subrel,tsubrel) in + PNodeB((pos,inf,form,term),t,s),"" (* empty string *) + else t,qpos + else (* x = Orl *) + let s,rpos = modify right (subrel,tsubrel) in + PNodeB((pos,inf,form,term),t,s),"Orl-True" + +(* transforms the subproof into an LJ proof between + the beta-inference rule (excluded) and + layer boundary in the branch ptree *) + + let rec rec_modify ptree (subrel,tsubrel) = + match ptree with + PEmpty -> + raise jprover_bug + | PNodeAx((pos,inf,form,term)) -> + ptree,pos + | PNodeA((pos,inf,form,term),left) -> + if List.mem inf [Impr;Negr;Allr] then + ptree,pos (* layer bound, stop transforming! *) + else + let t,qpos = rec_modify left (subrel,tsubrel) in + if List.mem inf [Andl;Alll;Exl] then + PNodeA((pos,inf,form,term),t),qpos (* simply propagation*) + else if inf = Exr then + if (subf1 pos qpos subrel) then + PNodeA((pos,inf,form,term),t),pos + else t,qpos + else if inf = Negl then + if (subf1 pos qpos subrel) then + PNodeA((pos,inf,form,term),t),"" (* empty string *) + else t,qpos + else (* x = Orr *) + if (subf1 pos qpos subrel) then + PNodeA((pos,Orr1,form,term),t),pos (* make Orr for LJ *) + else if (subf2 pos qpos subrel) then + PNodeA((pos,Orr2,form,term),t),pos (* make Orr for LJ *) + else t,qpos + | PNodeB((pos,inf,form,term),left,right) -> + let t,qpos = rec_modify left (subrel,tsubrel) in + if inf = Andr then + if (subf1 pos qpos subrel) then + let s,rpos = rec_modify right (subrel,tsubrel) in + if (subf2 pos rpos subrel) then + PNodeB((pos,inf,form,term),t,s),pos + else s,rpos + else t,qpos + else (* x = Impl since x= Orl cannot occur in the partial layer ptree *) + + if (subf1 pos qpos subrel) then + let s,rpos = rec_modify right (subrel,tsubrel) in + PNodeB((pos,inf,form,term),t,s),"" (* empty string *) + else t,qpos + + let weak_modify rule ptree (subrel,tsubrel) = (* recall rule = or_l *) + let (pos,inf,formlua,term) = rule in + if inf = Orl then + ptree,true + else + let ptreem,qpos = rec_modify ptree (subrel,tsubrel) in + if (subf1 pos qpos subrel) then (* weak_modify will always be applied on left branches *) + ptreem,true + else + ptreem,false + +(* Now, the permutation stuff .... *) + +(* Permutation schemes *) + +(* corresponds to local permutation lemma -- Lemma 3 in the paper -- *) +(* with eigenvariablen renaming and branch modification *) + +(* eigenvariablen renaming and branch modification over *) +(* the whole proofs, i.e. over layer boundaries, too *) + + +(* global variable vor eigenvariable renaming during permutations *) + + let eigen_counter = ref 1 + +(* append renamed paramater "r" to non-quantifier subformulae + of renamed quantifier formulae *) + +(*: BUG :*) +(*: + let make_new_eigenvariable term = + let op = (dest_term term).term_op in + let opn = (dest_op op).op_name in + let opnam = dest_opname opn in + match opnam with + [] -> + raise jprover_bug + | ofirst::orest -> + let ofname = List.hd orest in + let new_eigen_var = (ofname^"_r"^(string_of_int (!eigen_counter))) in + eigen_counter := !eigen_counter + 1; +(* print_endline ("New Counter :"^(string_of_int (!eigen_counter))); *) + mk_string_term jprover_op new_eigen_var +:*) + + let make_new_eigenvariable term = + let op = (dest_term term).term_op in + let opa = (dest_op op).op_params in + let oppar = dest_param opa in + match oppar with + | String ofname::_ -> + let new_eigen_var = (ofname^"_r"^(string_of_int (!eigen_counter))) in + eigen_counter := !eigen_counter + 1; + mk_string_term jprover_op new_eigen_var + | _ -> raise jprover_bug + + + let replace_subterm term oldt rept = + let v_term = var_subst term oldt "dummy_var" in + subst1 v_term "dummy_var" rept + + let rec eigen_rename old_parameter new_parameter ptree = + match ptree with + PEmpty -> + raise jprover_bug + | PNodeAx((pos,inf,form,term)) -> + let new_form = replace_subterm form old_parameter new_parameter in + PNodeAx((pos,inf,new_form,term)) + | PNodeA((pos,inf,form,term), left) -> + let new_form = replace_subterm form old_parameter new_parameter + and new_term = replace_subterm term old_parameter new_parameter in + let ren_left = eigen_rename old_parameter new_parameter left in + PNodeA((pos,inf,new_form,new_term), ren_left) + | PNodeB((pos,inf,form,term),left, right) -> + let new_form = replace_subterm form old_parameter new_parameter in + let ren_left = eigen_rename old_parameter new_parameter left in + let ren_right = eigen_rename old_parameter new_parameter right in + PNodeB((pos,inf,new_form,term), ren_left, ren_right) + + let rec update_ptree rule subtree direction tsubrel = + match subtree with + PEmpty -> + raise jprover_bug + | PNodeAx(r) -> + subtree + | PNodeA((pos,inf,formula,term), left) -> + if (pos,inf,formula,term) = rule then + left + (* don't delete rule if subformula belongs to renamed instance of quantifiers; *) + (* but this can never occur now since (renamed) formula is part of rule *) + else + let (posn,infn,formn,termn) = rule in + if (&) (List.mem infn [Exl;Allr] ) (term = termn) then + (* this can only occur if eigenvariable rule with same term as termn has been permuted; *) + (* the application of the same eigenvariable introduction on the same subformula with *) + (* different instantiated variables might occur! *) + (* termn cannot occur in terms of permuted quantifier rules due to substitution split *) + (* during reconstruciton of the ljmc proof *) + let new_term = make_new_eigenvariable term in +(* print_endline "Eigenvariable renaming!!!"; *) + eigen_rename termn new_term subtree + else + let left_del = + update_ptree rule left direction tsubrel + in + PNodeA((pos,inf,formula,term), left_del) + | PNodeB((pos,inf,formula,term), left, right) -> + if (pos,inf,formula,term) = rule then + if direction = "l" then + left + else + right (* direction = "r" *) + else + let left_del = update_ptree rule left direction tsubrel in + let right_del = update_ptree rule right direction tsubrel in + PNodeB((pos,inf,formula,term),left_del,right_del) + + let permute r1 r2 ptree la tsubrel = +(* print_endline "permute in"; *) + match ptree,la with + PNodeA(r1, PNodeA(r2,left)),la -> +(* print_endline "1-o-1"; *) + PNodeA(r2, PNodeA(r1,left)) + (* one-over-one *) + | PNodeA(r1, PNodeB(r2,left,right)),la -> +(* print_endline "1-o-2"; *) + PNodeB(r2, PNodeA(r1,left), PNodeA(r1,right)) + (* one-over-two *) + | PNodeB(r1, PNodeA(r2,left), right),"l" -> +(* print_endline "2-o-1 left"; *) + let right_u = update_ptree r2 right "l" tsubrel in + PNodeA(r2, PNodeB(r1, left, right_u)) + (* two-over-one left *) + | PNodeB(r1, left, PNodeA(r2,right)),"r" -> +(* print_endline "2-o-1 right"; *) + let left_u = update_ptree r2 left "l" tsubrel in + PNodeA(r2, PNodeB(r1, left_u, right)) + (* two-over-one right *) + | PNodeB(r1, PNodeB(r2,left2,right2), right),"l" -> +(* print_endline "2-o-2 left"; *) + let right_ul = update_ptree r2 right "l" tsubrel in + let right_ur = update_ptree r2 right "r" tsubrel in + PNodeB(r2,PNodeB(r1,left2,right_ul),PNodeB(r1,right2,right_ur)) + (* two-over-two left *) + | PNodeB(r1, left, PNodeB(r2,left2,right2)),"r" -> +(* print_endline "2-o-2 right"; *) + let left_ul = update_ptree r2 left "l" tsubrel in + let left_ur = update_ptree r2 left "r" tsubrel in + PNodeB(r2,PNodeB(r1,left_ul,left2),PNodeB(r1,left_ur, right2)) + (* two-over-two right *) + | _ -> raise jprover_bug + +(* permute layers, isolate addmissible branches *) + +(* computes if an Andr is d-generatives *) + + let layer_bound rule = + let (pos,inf,formula,term) = rule in + if List.mem inf [Impr;Negr;Allr] then + true + else + false + + let rec orl_free ptree = + match ptree with + PEmpty -> + raise jprover_bug + | PNodeAx(rule) -> + true + | PNodeA(rule,left) -> + if layer_bound rule then + true + else + orl_free left + | PNodeB(rule,left,right) -> + let (pos,inf,formula,term) = rule in + if inf = Orl then + false + else + (&) (orl_free left) (orl_free right) + + let rec dgenerative rule dglist ptree tsubrel = + let (pos,inf,formula,term) = rule in + if List.mem inf [Exr;Orr;Negl] then + true + else if inf = Andr then + if dglist = [] then + false + else + let first,rest = (List.hd dglist),(List.tl dglist) in + let (pos1,inf1,formula1,term1) = first in + if tsubf pos1 pos tsubrel then + true + else + dgenerative rule rest ptree tsubrel + else if inf = Impl then + not (orl_free ptree) + else + false + + +(* to compute a topmost addmissible pair r,o with + the address addr of r in the proof tree +*) + + let rec top_addmissible_pair ptree dglist act_r act_o act_addr tsubrel dummyt = + let rec search_pair ptree dglist act_r act_o act_addr tsubrel = + match ptree with + PEmpty -> raise jprover_bug + | PNodeAx(_) -> raise jprover_bug + | PNodeA(rule, left) -> +(* print_endline "alpha"; *) + if (dgenerative rule dglist left tsubrel) then (* r = Exr,Orr,Negl *) + let newdg = (@) [rule] dglist in + search_pair left newdg act_r rule act_addr tsubrel + else (* Impr, Allr, Notr only for test *) + search_pair left dglist act_r act_o act_addr tsubrel + | PNodeB(rule,left,right) -> +(* print_endline "beta"; *) + let (pos,inf,formula,term) = rule in + if List.mem inf [Andr;Impl] then + let bool = dgenerative rule dglist left tsubrel in + let newdg,newrule = + if bool then + ((@) [rule] dglist),rule + else + dglist,act_o + in + if orl_free left then + search_pair right newdg act_r newrule (act_addr^"r") tsubrel + else (* not orl_free *) + let left_r,left_o,left_addr = + search_pair left newdg act_r newrule (act_addr^"l") tsubrel in + if left_o = ("",Orr,dummyt,dummyt) then + top_addmissible_pair right dglist act_r act_o (act_addr^"r") tsubrel dummyt + else left_r,left_o,left_addr + else (* r = Orl *) + if orl_free left then + top_addmissible_pair right dglist rule act_o (act_addr^"r") tsubrel dummyt + else + let left_r,left_o,left_addr + = search_pair left dglist rule act_o (act_addr^"l") tsubrel in + if left_o = ("",Orr,dummyt,dummyt) then + top_addmissible_pair right dglist rule act_o (act_addr^"r") tsubrel dummyt + else + left_r,left_o,left_addr + in +(* print_endline "top_addmissible_pair in"; *) + if orl_free ptree then (* there must be a orl BELOW an layer bound *) + begin +(* print_endline "orl_free"; *) + act_r,act_o,act_addr + end + else + begin +(* print_endline "orl_full"; *) + search_pair ptree dglist act_r act_o act_addr tsubrel + end + + let next_direction addr act_addr = + String.make 1 (String.get addr (String.length act_addr)) + (* get starts with count 0*) + + let change_last addr d = + let split = (String.length addr) - 1 in + let prec,last = + (String.sub addr 0 split),(String.sub addr split 1) in + prec^d^last + + let last addr = + if addr = "" + then "" + else + String.make 1 (String.get addr (String.length addr-1)) + + let rest addr = + if addr = "" + then "" + else + String.sub addr 0 ((String.length addr) - 1) + + let rec permute_layer ptree dglist (subrel,tsubrel) = + let rec permute_branch r addr act_addr ptree dglist (subrel,tsubrel) = +(* print_endline "pbranch in"; *) + let la = last act_addr in (* no ensure uniqueness at 2-over-x *) + match ptree,la with + PNodeA(o,PNodeA(rule,left)),la -> (* one-over-one *) +(* print_endline " one-over-one "; *) + let permute_result = permute o rule ptree la tsubrel in + begin match permute_result with + PNodeA(r2,left2) -> + let pbleft = permute_branch r addr act_addr left2 dglist (subrel,tsubrel) in + PNodeA(r2,pbleft) + | _ -> raise jprover_bug + end + | PNodeA(o,PNodeB(rule,left,right)),la -> (* one-over-two *) +(* print_endline " one-over-two "; *) + if rule = r then (* left,right are or_l free *) + permute o rule ptree la tsubrel (* first termination case *) + else + let d = next_direction addr act_addr in + if d = "l" then + let permute_result = permute o rule ptree la tsubrel in + (match permute_result with + PNodeB(r2,left2,right2) -> + let pbleft = permute_branch r addr (act_addr^d) left2 dglist (subrel,tsubrel) in + let plright = permute_layer right2 dglist (subrel,tsubrel) in + PNodeB(r2,pbleft,plright) + | _ -> raise jprover_bug + ) + else (* d = "r", that is left of rule is or_l free *) + let left1,bool = weak_modify rule left (subrel,tsubrel) in + if bool then (* rule is relevant *) + let permute_result = permute o rule (PNodeA(o,PNodeB(rule,left1,right))) la tsubrel in + (match permute_result with + PNodeB(r2,left2,right2) -> + let pbright = permute_branch r addr (act_addr^d) right2 dglist (subrel,tsubrel) in + PNodeB(r2,left2,pbright) + | _ -> raise jprover_bug + ) + else (* rule is not relevant *) + PNodeA(o,left1) (* optimized termination case (1) *) + | PNodeB(o,PNodeA(rule,left),right1),"l" -> (* two-over-one, left *) +(* print_endline " two-over-one, left "; *) + let permute_result = permute o rule ptree la tsubrel in + (match permute_result with + PNodeA(r2,left2) -> + let pbleft = permute_branch r addr act_addr left2 dglist (subrel,tsubrel) in + PNodeA(r2,pbleft) + | _ -> raise jprover_bug + ) + | PNodeB(o,left1,PNodeA(rule,left)),"r" -> (* two-over-one, right *) + (* left of o is or_l free *) +(* print_endline " two-over-one, right"; *) + let leftm,bool = weak_modify o left1 (subrel,tsubrel) in + if bool then (* rule is relevant *) + let permute_result = permute o rule (PNodeB(o,leftm,PNodeA(rule,left))) la tsubrel in + (match permute_result with + PNodeA(r2,left2) -> + let pbleft = permute_branch r addr act_addr left2 dglist (subrel,tsubrel) in + PNodeA(r2,pbleft) + | _ -> raise jprover_bug + ) + else (* rule is not relevant *) + leftm (* optimized termination case (2) *) + | PNodeB(o,PNodeB(rule,left,right),right1),"l" -> (* two-over-two, left *) +(* print_endline " two-over-two, left"; *) + if rule = r then (* left,right are or_l free *) + let permute_result = permute o rule ptree la tsubrel in + (match permute_result with + PNodeB(r2,PNodeB(r3,left3,right3),PNodeB(r4,left4,right4)) -> +(* print_endline "permute 2-o-2, left ok"; *) + let leftm3,bool3 = weak_modify r3 left3 (subrel,tsubrel) in + let leftm4,bool4 = weak_modify r4 left4 (subrel,tsubrel) in + let plleft,plright = + if (&) bool3 bool4 then (* r3 and r4 are relevant *) + (permute_layer (PNodeB(r3,leftm3,right3)) dglist (subrel,tsubrel)), + (permute_layer (PNodeB(r4,leftm4,right4)) dglist (subrel,tsubrel)) + else if (&) bool3 (not bool4) then (* only r3 is relevant *) + begin +(* print_endline "two-over-two left: bool3 and not bool4"; *) + (permute_layer (PNodeB(r3,leftm3,right3)) dglist (subrel,tsubrel)), + leftm4 + end + else if (&) (not bool3) bool4 then (* only r4 is relevant *) + leftm3, + (permute_layer (PNodeB(r4,leftm4,right4)) dglist (subrel,tsubrel)) + else (* neither r3 nor r4 are relevant *) + leftm3,leftm4 + in + PNodeB(r2,plleft,plright) + | _ -> raise jprover_bug + ) + else + let d = next_direction addr act_addr in + let newadd = change_last act_addr d in + if d = "l" then + let permute_result = permute o rule ptree la tsubrel in + (match permute_result with + PNodeB(r2,left2,right2) -> + let pbleft = permute_branch r addr newadd left2 dglist (subrel,tsubrel) in + let plright = permute_layer right2 dglist (subrel,tsubrel) in + PNodeB(r2,pbleft,plright) + | _ -> raise jprover_bug + ) + else (* d = "r", that is left is or_l free *) + let left1,bool = weak_modify rule left (subrel,tsubrel) in + if bool then (* rule is relevant *) + let permute_result = + permute o rule (PNodeB(o,PNodeB(rule,left1,right),right1)) la tsubrel in + (match permute_result with + PNodeB(r2,PNodeB(r3,left3,right3),right2) -> + let pbright = permute_branch r addr newadd right2 dglist (subrel,tsubrel) in + let leftm3,bool3 = weak_modify r3 left3 (subrel,tsubrel) in + let plleft = + if bool3 (* r3 relevant *) then + permute_layer (PNodeB(r3,leftm3,right3)) dglist (subrel,tsubrel) + else (* r3 redundant *) + leftm3 + in + PNodeB(r2,plleft,pbright) (* further opt. NOT possible *) + | _ -> raise jprover_bug + ) + else (* rule is not relevant *) + permute_layer (PNodeB(o,left1,right1)) dglist (subrel,tsubrel) (* further opt. possible *) + (* combine with orl_free *) + | PNodeB(o,left1,PNodeB(rule,left,right)),"r" -> (* two-over-two, right *) +(* print_endline " two-over-two, right"; *) + let leftm1,bool = weak_modify o left1 (subrel,tsubrel) in (* left1 is or_l free *) + if bool then (* o is relevant, even after permutations *) + if rule = r then (* left, right or_l free *) + permute o rule (PNodeB(o,leftm1,PNodeB(rule,left,right))) la tsubrel + else + let d = next_direction addr act_addr in + let newadd = change_last act_addr d in + if d = "l" then + let permute_result = + permute o rule (PNodeB(o,leftm1,PNodeB(rule,left,right))) la tsubrel in + (match permute_result with + PNodeB(r2,left2,right2) -> + let pbleft = permute_branch r addr newadd left2 dglist (subrel,tsubrel) in + let plright = permute_layer right2 dglist (subrel,tsubrel) in + PNodeB(r2,pbleft,plright) + | _ -> raise jprover_bug + ) + else (* d = "r", that is left is or_l free *) + let leftm,bool = weak_modify rule left (subrel,tsubrel) in + if bool then (* rule is relevant *) + let permute_result = + permute o rule (PNodeB(o,leftm1,PNodeB(rule,left,right))) la tsubrel in + (match permute_result with + PNodeB(r2,left2,right2) -> + let pbright = permute_branch r addr newadd right2 dglist (subrel,tsubrel) in + PNodeB(r2,left2,pbright) (* left2 or_l free *) + | _ -> raise jprover_bug + ) + else (* rule is not relevant *) + PNodeB(o,leftm1,leftm) + + else + leftm1 + | _ -> raise jprover_bug + in + let rec trans_add_branch r o addr act_addr ptree dglist (subrel,tsubrel) = + match ptree with + (PEmpty| PNodeAx(_)) -> raise jprover_bug + | PNodeA(rule,left) -> + if (dgenerative rule dglist left tsubrel) then + let newdg = (@) [rule] dglist in + if rule = o then + begin +(* print_endline "one-rule is o"; *) + permute_branch r addr act_addr ptree dglist (subrel,tsubrel) + end + else + begin +(* print_endline "alpha - but not o"; *) + let tptree = trans_add_branch r o addr act_addr left newdg (subrel,tsubrel) in + permute_layer (PNodeA(rule,tptree)) dglist (subrel,tsubrel) + (* r may not longer be valid for rule *) + end + else + let tptree = trans_add_branch r o addr act_addr left dglist (subrel,tsubrel) in + PNodeA(rule,tptree) + | PNodeB(rule,left,right) -> + let d = next_direction addr act_addr in + let bool = (dgenerative rule dglist left tsubrel) in + if rule = o then + begin +(* print_endline "two-rule is o"; *) + permute_branch r addr (act_addr^d) ptree dglist (subrel,tsubrel) + end + else + begin +(* print_endline ("beta - but not o: address "^d); *) + let dbranch = + if d = "l" then + left + else (* d = "r" *) + right + in + let tptree = + if bool then + let newdg = (@) [rule] dglist in + (trans_add_branch r o addr (act_addr^d) dbranch newdg (subrel,tsubrel)) + else + (trans_add_branch r o addr (act_addr^d) dbranch dglist (subrel,tsubrel)) + in + if d = "l" then + permute_layer (PNodeB(rule,tptree,right)) dglist (subrel,tsubrel) + else (* d = "r" *) + begin +(* print_endline "prob. a redundant call"; *) + let back = permute_layer (PNodeB(rule,left,tptree)) dglist (subrel,tsubrel) in +(* print_endline "SURELY a redundant call"; *) + back + end + end + in +(* print_endline "permute_layer in"; *) + let dummyt = mk_var_term "dummy" in + let r,o,addr = + top_addmissible_pair ptree dglist ("",Orl,dummyt,dummyt) ("",Orr,dummyt,dummyt) "" tsubrel dummyt in + if r = ("",Orl,dummyt,dummyt) then + ptree + else if o = ("",Orr,dummyt,dummyt) then (* Orr is a dummy for no d-gen. rule *) + ptree + else + let (x1,x2,x3,x4) = r + and (y1,y2,y3,y4) = o in +(* print_endline ("top or_l: "^x1); + print_endline ("or_l address: "^addr); + print_endline ("top dgen-rule: "^y1); *) + trans_add_branch r o addr "" ptree dglist (subrel,tsubrel) + +(* Isolate layer and outer recursion structure *) +(* uses weaker layer boundaries: ONLY critical inferences *) + + let rec trans_layer ptree (subrel,tsubrel) = + let rec isol_layer ptree (subrel,tsubrel) = + match ptree with + PEmpty -> raise jprover_bug + | PNodeAx(inf) -> + ptree + | PNodeA((pos,rule,formula,term),left) -> + if List.mem rule [Allr;Impr;Negr] then + let tptree = trans_layer left (subrel,tsubrel) in + PNodeA((pos,rule,formula,term),tptree) + else + let tptree = isol_layer left (subrel,tsubrel) in + PNodeA((pos,rule,formula,term),tptree) + | PNodeB(rule,left,right) -> + let tptree_l = isol_layer left (subrel,tsubrel) + and tptree_r = isol_layer right (subrel,tsubrel) in + PNodeB(rule,tptree_l,tptree_r) + in + begin +(* print_endline "trans_layer in"; *) + let top_tree = isol_layer ptree (subrel,tsubrel) in + let back = permute_layer top_tree [] (subrel,tsubrel) in +(* print_endline "translauer out"; *) + back + end + +(* REAL PERMUTATION STAFF --- End *) + +(* build the proof tree from a list of inference rules *) + + let rec unclosed subtree = + match subtree with + PEmpty -> true + | PNodeAx(y) -> false + | PNodeA(y,left) -> (unclosed left) + | PNodeB(y,left,right) -> (or) (unclosed left) (unclosed right) + + let rec extend prooftree element = + match prooftree with + PEmpty -> + let (pos,rule,formula,term) = element in + if rule = Ax then + PNodeAx(element) + else + if List.mem rule [Andr; Orl; Impl] then + PNodeB(element,PEmpty,PEmpty) + else + PNodeA(element,PEmpty) + | PNodeAx(y) -> + PEmpty (* that's only for exhaustive pattern matching *) + | PNodeA(y, left) -> + PNodeA(y, (extend left element)) + | PNodeB(y, left, right) -> + if (unclosed left) then + PNodeB(y, (extend left element), right) + else + PNodeB(y, left, (extend right element)) + + let rec bptree prooftree nodelist nax= + match nodelist with + [] -> prooftree,nax + | ((_,pos),(rule,formula,term))::rest -> (* kick away the first argument *) + let newax = + if rule = Ax then + 1 + else + 0 + in + bptree (extend prooftree (pos,rule,formula,term)) rest (nax+newax) + + + let bproof nodelist = + bptree PEmpty nodelist 0 + + let rec get_successor_pos treelist = + match treelist with + [] -> [] + | f::r -> + ( + match f with + Empty -> get_successor_pos r + | NodeAt(_) -> raise jprover_bug + | NodeA(pos,_) -> + pos::(get_successor_pos r) + ) + + let rec get_formula_tree ftreelist f predflag = + match ftreelist with + [] -> raise jprover_bug + | ftree::rest_trees -> + (match ftree with + Empty -> get_formula_tree rest_trees f predflag + | NodeAt(_) -> get_formula_tree rest_trees f predflag + | NodeA(pos,suctrees) -> + if predflag = "pred" then + if pos.pt = Gamma then + let succs = get_successor_pos (Array.to_list suctrees) in + if List.mem f succs then + NodeA(pos,suctrees),succs + else + get_formula_tree ((Array.to_list suctrees) @ rest_trees) f predflag + else + get_formula_tree ((Array.to_list suctrees) @ rest_trees) f predflag + else (* predflag = "" *) + if pos = f then + NodeA(pos,suctrees),[] + else + get_formula_tree ((Array.to_list suctrees) @ rest_trees) f predflag + ) + + let rec get_formula_treelist ftree po = + match po with + [] -> [] + | f::r -> +(* a posistion in po has either stype Gamma_0,Psi_0,Phi_0 (non-atomic), or it has *) +(* ptype Alpha (or on the right), since there was a deadlock for proof reconstruction in LJ*) + if List.mem f.st [Phi_0;Psi_0] then + let (stree,_) = get_formula_tree [ftree] f "" in + stree::(get_formula_treelist ftree r) + else + if f.st = Gamma_0 then + let (predtree,succs) = get_formula_tree [ftree] f "pred" in + let new_po = list_diff r succs in + predtree::(get_formula_treelist ftree new_po) + else + if f.pt = Alpha then (* same as first case, or on the right *) + let (stree,_) = get_formula_tree [ftree] f "" in + stree::(get_formula_treelist ftree r) + else raise (Invalid_argument "Jprover bug: non-admissible open position") + + let rec build_formula_rel dir_treelist slist predname = + + let rec build_renamed_gamma_rel dtreelist predname posname d = + match dtreelist with + [] -> [],[] + | (x,ft)::rdtlist -> + let rest_rel,rest_ren = build_renamed_gamma_rel rdtlist predname posname d in + ( + match ft with + Empty -> (* may have empty successors due to purity in former reconstruction steps *) + rest_rel,rest_ren + | NodeAt(_) -> + raise jprover_bug (* gamma_0 position never is atomic *) + | NodeA(spos,suctrees) -> + if List.mem spos.name slist then +(* the gamma_0 position is really unsolved *) +(* this is only relevant for the gamma_0 positions in po *) + let new_name = (posname^"_"^spos.name) (* make new unique gamma name *) in + let new_srel_el = ((predname,new_name),d) + and new_rename_el = (spos.name,new_name) (* gamma_0 position as key first *) in + let (srel,sren) = build_formula_rel [(x,ft)] slist new_name in + ((new_srel_el::srel) @ rest_rel),((new_rename_el::sren) @ rest_ren) + else + rest_rel,rest_ren + ) + + + in + match dir_treelist with + [] -> [],[] + | (d,f)::dir_r -> + let (rest_rel,rest_renlist) = build_formula_rel dir_r slist predname in + match f with + Empty -> + print_endline "Hello, an empty subtree!!!!!!"; + rest_rel,rest_renlist + | NodeAt(pos) -> + (((predname,pos.name),d)::rest_rel),rest_renlist + | NodeA(pos,suctrees) -> + (match pos.pt with + Alpha | Beta -> + let dtreelist = + if (pos.pt = Alpha) & (pos.op = Neg) then + [(1,suctrees.(0))] + else + let st1 = suctrees.(0) + and st2 = suctrees.(1) in + [(1,st1);(2,st2)] + in + let (srel,sren) = build_formula_rel dtreelist slist pos.name in + ((((predname,pos.name),d)::srel) @ rest_rel),(sren @ rest_renlist) + | Delta -> + let st1 = suctrees.(0) in + let (srel,sren) = build_formula_rel [(1,st1)] slist pos.name in + ((((predname,pos.name),d)::srel) @ rest_rel),(sren @ rest_renlist) + | Psi| Phi -> + let succlist = Array.to_list suctrees in + let dtreelist = (List.map (fun x -> (d,x)) succlist) in + let (srel,sren) = build_formula_rel dtreelist slist predname in + (srel @ rest_rel),(sren @ rest_renlist) + | Gamma -> + let n = Array.length suctrees + and succlist = (Array.to_list suctrees) in + let dtreelist = (List.map (fun x -> (1,x)) succlist) in +(* if (nonemptys suctrees 0 n) = 1 then + let (srel,sren) = build_formula_rel dtreelist slist pos.name in + ((((predname,pos.name),d)::srel) @ rest_rel),(sren @ rest_renlist) + else (* we have more than one gamma instance, which means renaming *) +*) + let (srel,sren) = build_renamed_gamma_rel dtreelist predname pos.name d in + (srel @ rest_rel),(sren @ rest_renlist) + | PNull -> + raise jprover_bug + ) + + let rec rename_gamma ljmc_proof rename_list = + match ljmc_proof with + [] -> [] + | ((inst,pos),(rule,formula,term))::r -> + if List.mem rule [Alll;Exr] then + let new_gamma = List.assoc inst rename_list in + ((inst,new_gamma),(rule,formula,term))::(rename_gamma r rename_list) + else + ((inst,pos),(rule,formula,term))::(rename_gamma r rename_list) + + let rec compare_pair (s,sf) list = + if list = [] then + list + else + let (s_1,sf_1),restlist = (List.hd list),(List.tl list) in + if sf = s_1 then + (@) [(s,sf_1)] (compare_pair (s,sf) restlist) + else + compare_pair (s,sf) restlist + + let rec compare_pairlist list1 list2 = + if list1 = [] then + list1 + else + let (s1,sf1),restlist1 = (List.hd list1),(List.tl list1) in + (@) (compare_pair (s1,sf1) list2) (compare_pairlist restlist1 list2) + + let rec trans_rec pairlist translist = + let tlist = compare_pairlist pairlist translist in + if tlist = [] then + translist + else + (@) (trans_rec pairlist tlist) translist + + let transitive_closure subrel = + let pairlist,nlist = List.split subrel in + trans_rec pairlist pairlist + + let pt ptree subrel = + let tsubrel = transitive_closure subrel in + let transptree = trans_layer ptree (subrel,tsubrel) in + print_endline ""; + fst (modify transptree (subrel,tsubrel)) +(* let mtree = fst (modify transptree (subrel,tsubrel)) in *) +(* pretty_print mtree ax *) + + let rec make_node_list ljproof = + match ljproof with + PEmpty -> + raise jprover_bug + | PNodeAx((pos,inf,form,term)) -> + [(("",pos),(inf,form,term))] + | PNodeA((pos,inf,form,term),left) -> + let left_list = make_node_list left in + (("",pos),(inf,form,term))::left_list + | PNodeB((pos,inf,form,term),left,right) -> + let left_list = make_node_list left + and right_list = make_node_list right in + (("",pos),(inf,form,term))::(left_list @ right_list) + + let permute_ljmc ftree po slist ljmc_proof = + (* ftree/po are the formula tree / open positions of the sequent that caused deadlock and permutation *) +(* print_endline "!!!!!!!!!!!!!Permutation TO DO!!!!!!!!!"; *) + (* the open positions in po are either phi_0, psi_0, or gamma_0 positions *) + (* since proof reconstruction was a deadlock in LJ *) + let po_treelist = get_formula_treelist ftree po in + let dir_treelist = List.map (fun x -> (1,x)) po_treelist in + let (formula_rel,rename_list) = build_formula_rel dir_treelist slist "dummy" in + let renamed_ljmc_proof = rename_gamma ljmc_proof rename_list in + let (ptree,ax) = bproof renamed_ljmc_proof in + let ljproof = pt ptree formula_rel in + (* this is a direct formula relation, comprising left/right subformula *) + begin +(* print_treelist po_treelist; *) +(* print_endline ""; + print_endline ""; +*) +(* print_triplelist formula_rel; *) +(* print_endline ""; + print_endline ""; + tt ljproof; +*) +(* print_pairlist rename_list; *) +(* print_endline ""; + print_endline ""; +*) + make_node_list ljproof + end + +(************** PROOF RECONSTRUCTION without redundancy deletion ******************************) + + let rec init_unsolved treelist = + match treelist with + [] -> [] + | f::r -> + begin match f with + Empty -> [] + | NodeAt(pos) -> + (pos.name)::(init_unsolved r) + | NodeA(pos,suctrees) -> + let new_treelist = (Array.to_list suctrees) @ r in + (pos.name)::(init_unsolved new_treelist) + end + +(* only the unsolved positions will be represented --> skip additional root position *) + + let build_unsolved ftree = + match ftree with + Empty | NodeAt _ -> + raise jprover_bug + | NodeA(pos,suctrees) -> + ((pos.name),init_unsolved (Array.to_list suctrees)) + +(* + let rec collect_variables tree_list = + match tree_list with + [] -> [] + | f::r -> + begin match f with + Empty -> [] + | NodeAt(pos) -> + if pos.st = Gamma_0 then + pos.name::collect_variables r + else + collect_variables r + | NodeA(pos,suctrees) -> + let new_tree_list = (Array.to_list suctrees) @ r in + if pos.st = Gamma_0 then + pos.name::collect_variables new_tree_list + else + collect_variables new_tree_list + end + + let rec extend_sigmaQ sigmaQ vlist = + match vlist with + [] -> [] + | f::r -> + let vf = mk_var_term f in + if List.exists (fun x -> (fst x = vf)) sigmaQ then + extend_sigmaQ sigmaQ r + else +(* first and second component are var terms in meta-prl *) + [(vf,vf)] @ (extend_sigmaQ sigmaQ r) + + let build_sigmaQ sigmaQ ftree = + let vlist = collect_variables [ftree] in + sigmaQ @ (extend_sigmaQ sigmaQ vlist) +*) + +(* subformula relation subrel is assumed to be represented in pairs + (a,b) *) + + let rec delete e list = (* e must not necessarily occur in list *) + match list with + [] -> [] (* e must not necessarily occur in list *) + | first::rest -> + if e = first then + rest + else + first::(delete e rest) + + let rec key_delete fname pos_list = (* in key_delete, f is a pos name (key) but sucs is a list of positions *) + match pos_list with + [] -> [] (* the position with name f must not necessarily occur in pos_list *) + | f::r -> + if fname = f.name then + r + else + f::(key_delete fname r) + + let rec get_roots treelist = + match treelist with + [] -> [] + | f::r -> + match f with + Empty -> (get_roots r) (* Empty is posible below alpha-nodes after purity *) + | NodeAt(pos) -> pos::(get_roots r) + | NodeA(pos,trees) -> pos::(get_roots r) + + let rec comp_ps padd ftree = + match ftree with + Empty -> raise (Invalid_argument "Jprover bug: empty formula tree") + | NodeAt(pos) -> + [] + | NodeA(pos,strees) -> + match padd with + [] -> get_roots (Array.to_list strees) + | f::r -> + if r = [] then + pos::(comp_ps r (Array.get strees (f-1))) + else + comp_ps r (Array.get strees (f-1)) + +(* computes a list: first element predecessor, next elements successoes of p *) + + let tpredsucc p ftree = + let padd = p.address in + comp_ps padd ftree + +(* set an element in an array, without side effects *) + + let myset array int element = + let length = Array.length array in + let firstpart = Array.sub array 0 (int) in + let secondpart = Array.sub array (int+1) (length-(int+1)) in + (Array.append firstpart (Array.append [|element|] secondpart)) + + let rec compute_open treelist slist = + match treelist with + [] -> [] + | first::rest -> + let elements = + match first with + Empty -> [] + | NodeAt(pos) -> + if (List.mem (pos.name) slist) then + [pos] + else + [] + | NodeA(pos,suctrees) -> + if (List.mem (pos.name) slist) then + [pos] + else + compute_open (Array.to_list suctrees) slist + in + elements @ (compute_open rest slist) + + let rec select_connection pname connections slist = + match connections with + [] -> ("none","none") + | f::r -> + let partner = + if (fst f) = pname then + (snd f) + else + if (snd f) = pname then + (fst f) + else + "none" + in + if ((partner = "none") or (List.mem partner slist)) then + select_connection pname r slist + else + f + + let rec replace_element element element_set redord = + match redord with + [] -> raise jprover_bug (* element occurs in redord *) + | (f,fset)::r -> + if f = element then + (f,element_set)::r + else + (f,fset)::(replace_element element element_set r) + + let rec collect_succ_sets sucs redord = + match redord with + [] -> StringSet.empty + | (f,fset)::r -> + let new_sucs = key_delete f sucs in + if (List.length sucs) = (List.length new_sucs) then (* position with name f did not occur in sucs -- no deletion *) + (collect_succ_sets sucs r) + else + StringSet.union (StringSet.add f fset) (collect_succ_sets new_sucs r) + + let replace_ordering psucc_name sucs redord = + let new_psucc_set = collect_succ_sets sucs redord in +(* print_string_set new_psucc_set; *) + replace_element psucc_name new_psucc_set redord + + let rec update pname redord = + match redord with + [] -> [] + | (f,fset)::r -> + if pname=f then + r + else + (f,fset)::(update pname r) + +(* rule construction *) + + let rec selectQ_rec spos_var csigmaQ = + match csigmaQ with + [] -> mk_var_term spos_var (* dynamic completion of csigmaQ *) + | (var,term)::r -> + if spos_var=var then + term + else + selectQ_rec spos_var r + + let selectQ spos_name csigmaQ = + let spos_var = spos_name^"_jprover" in + selectQ_rec spos_var csigmaQ + + let apply_sigmaQ term sigmaQ = + let sigma_vars,sigma_terms = List.split sigmaQ in + (subst term sigma_vars sigma_terms) + + let build_rule pos spos csigmaQ orr_flag calculus = + let inst_label = apply_sigmaQ (pos.label) csigmaQ in + match pos.op,pos.pol with + Null,_ -> raise (Invalid_argument "Jprover: no rule") + | At,O -> Ax,(inst_label),xnil_term (* to give back a term *) + | At,I -> Ax,(inst_label),xnil_term + | And,O -> Andr,(inst_label),xnil_term + | And,I -> Andl,(inst_label),xnil_term + | Or,O -> + if calculus = "LJ" then + let or_rule = + if orr_flag = 1 then + Orr1 + else + Orr2 + in + or_rule,(inst_label),xnil_term + else + Orr,(inst_label),xnil_term + | Or,I -> Orl,(inst_label),xnil_term + | Neg,O -> Negr,(inst_label),xnil_term + | Neg,I -> Negl,(inst_label),xnil_term + | Imp,O -> Impr,(inst_label),xnil_term + | Imp,I -> Impl,(inst_label),xnil_term + | All,I -> Alll,(inst_label),(selectQ spos.name csigmaQ) (* elements of csigmaQ is (string * term) *) + | Ex,O -> Exr,(inst_label), (selectQ spos.name csigmaQ) + | All,O -> Allr,(inst_label),(mk_string_term jprover_op spos.name) (* must be a proper term *) + | Ex,I -> Exl,(inst_label),(mk_string_term jprover_op spos.name) (* must be a proper term *) + + +(* %%%%%%%%%%%%%%%%%%%% Split begin %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *) + + let rec nonemptys treearray j n = + if j = n then + 0 + else + let count = + if (Array.get treearray j) <> Empty then + 1 + else + 0 + in + count + (nonemptys treearray (j+1) n) + + let rec collect_pure ftreelist (flist,slist) = + + let rec collect_itpure ftree (flist,slist) = + match ftree with + Empty -> (* assumed that not all brother trees are Empty *) + [] + | NodeAt(pos) -> (* that may NOT longer be an inner node *) + if ((List.mem (pos.name) flist) or (List.mem (pos.name) slist)) then + [] + else + [pos] + | NodeA(pos,treearray) -> + collect_pure (Array.to_list treearray) (flist,slist) + in + match ftreelist with + [] -> [] + | f::r -> + (collect_itpure f (flist,slist)) @ (collect_pure r (flist,slist)) + + let rec update_list testlist list = + match testlist with + [] -> list + | f::r -> + let newlist = delete f list in (* f may not occur in list; then newlist=list *) + update_list r newlist + + let rec update_pairlist p pairlist = + match pairlist with + [] -> [] + | f::r -> + if ((fst f) = p) or ((snd f) = p) then + update_pairlist p r + else + f::(update_pairlist p r) + + let rec update_connections slist connections = + match slist with + [] -> connections + | f::r -> + let connew = update_pairlist f connections in + update_connections r connew + + let rec update_redord delset redord = (* delset is the set of positions to be deleted *) + match redord with + [] -> [] + | (f,fset)::r -> + if (StringSet.mem f delset) then + update_redord delset r (* delete all key elements f from redord which are in delset *) + else + let new_fset = StringSet.diff fset delset in (* no successor of f from delset should remain in fset *) + (f,new_fset)::(update_redord delset r) + + let rec get_position_names treelist = + match treelist with + [] -> [] + | deltree::rests -> + match deltree with + Empty -> get_position_names rests + | NodeAt(pos) -> + (pos.name)::get_position_names rests + | NodeA(pos,strees) -> + (pos.name)::(get_position_names ((Array.to_list strees) @ rests)) + + let rec slist_to_set slist = + match slist with + [] -> + StringSet.empty + | f::r -> + StringSet.add f (slist_to_set r) + + let rec print_purelist pr = + match pr with + [] -> + begin + print_string "."; + print_endline " "; + end + | f::r -> + print_string ((f.name)^", "); + print_purelist r + + let update_relations deltree redord connections unsolved_list = + let pure_names = get_position_names [deltree] in + begin +(* print_ftree deltree; + Format.open_box 0; + print_endline " "; + print_stringlist pure_names; + Format.force_newline (); + Format.print_flush (); +*) + let rednew = update_redord (slist_to_set pure_names) redord + and connew = update_connections pure_names connections + and unsolnew = update_list pure_names unsolved_list in + (rednew,connew,unsolnew) + end + + let rec collect_qpos ftreelist uslist = + match ftreelist with + [] -> [],[] + | ftree::rest -> + match ftree with + Empty -> + collect_qpos rest uslist + | NodeAt(pos) -> + let (rest_delta,rest_gamma) = collect_qpos rest uslist in + if (pos.st = Gamma_0) & (List.mem pos.name uslist) then + rest_delta,(pos.name::rest_gamma) + else + if (pos.st = Delta_0) & (List.mem pos.name uslist) then + (pos.name::rest_delta),rest_gamma + else + rest_delta,rest_gamma + | NodeA(pos,suctrees) -> + let (rest_delta,rest_gamma) = collect_qpos ((Array.to_list suctrees) @ rest) uslist in + if (pos.st = Gamma_0) & (List.mem pos.name uslist) then + rest_delta,(pos.name::rest_gamma) + else + if (pos.st = Delta_0) & (List.mem pos.name uslist) then + (pos.name::rest_delta),rest_gamma + else + rest_delta,rest_gamma + + let rec do_split gamma_diff sigmaQ = + match sigmaQ with + [] -> [] + | (v,term)::r -> + if (List.mem (String.sub v 0 (String.index v '_')) gamma_diff) then + do_split gamma_diff r + else + (v,term)::(do_split gamma_diff r) + +(* make a term list out of a bterm list *) + + let rec collect_subterms = function + [] -> [] + | bt::r -> + let dbt = dest_bterm bt in + (dbt.bterm)::(collect_subterms r) + + (*: Bug! :*) +(*: let rec collect_delta_terms = function + [] -> [] + | t::r -> + let dt = dest_term t in + let top = dt.term_op + and tterms = dt.term_terms in + let dop = dest_op top in + let don = dest_opname dop.op_name in + match don with + [] -> + let sub_terms = collect_subterms tterms in + collect_delta_terms (sub_terms @ r) + | op1::opr -> + if op1 = "jprover" then + match opr with + [] -> raise (Invalid_argument "Jprover: delta position missing") + | delta::_ -> + delta::(collect_delta_terms r) + else + let sub_terms = collect_subterms tterms in + collect_delta_terms (sub_terms @ r) +:*) + + let rec collect_delta_terms = function + [] -> [] + | t::r -> + let dt = dest_term t in + let top = dt.term_op + and tterms = dt.term_terms in + let dop = dest_op top in + let don = dest_opname dop.op_name in + let doa = dest_param dop.op_params in + match don with + [] -> + let sub_terms = collect_subterms tterms in + collect_delta_terms (sub_terms @ r) + | op1::opr -> + if op1 = "jprover" then + match doa with + [] -> raise (Invalid_argument "Jprover: delta position missing") + | String delta::_ -> + delta::(collect_delta_terms r) + | _ -> raise (Invalid_argument "Jprover: delta position error") + else + let sub_terms = collect_subterms tterms in + collect_delta_terms (sub_terms @ r) + + + + let rec check_delta_terms (v,term) ass_delta_diff dterms = + match ass_delta_diff with + [] -> term,[] + | (var,dname)::r -> + if List.mem dname dterms then + let new_var = + if var = "" then + v + else + var + in + let replace_term = mk_string_term jprover_op dname in + let next_term = var_subst term replace_term new_var in + let (new_term,next_diffs) = check_delta_terms (v,next_term) r dterms in + (new_term,((new_var,dname)::next_diffs)) + else + let (new_term,next_diffs) = check_delta_terms (v,term) r dterms in + (new_term,((var,dname)::next_diffs)) + + + let rec localize_sigma zw_sigma ass_delta_diff = + match zw_sigma with + [] -> [] + | (v,term)::r -> + let dterms = collect_delta_terms [term] in + let (new_term,new_ass_delta_diff) = check_delta_terms (v,term) ass_delta_diff dterms in + (v,new_term)::(localize_sigma r new_ass_delta_diff) + + let subst_split ft1 ft2 ftree uslist1 uslist2 uslist sigmaQ = + let delta,gamma = collect_qpos [ftree] uslist + and delta1,gamma1 = collect_qpos [ft1] uslist1 + and delta2,gamma2 = collect_qpos [ft2] uslist2 in + let delta_diff1 = list_diff delta delta1 + and delta_diff2 = list_diff delta delta2 + and gamma_diff1 = list_diff gamma gamma1 + and gamma_diff2 = list_diff gamma gamma2 in + let zw_sigma1 = do_split gamma_diff1 sigmaQ + and zw_sigma2 = do_split gamma_diff2 sigmaQ in + let ass_delta_diff1 = List.map (fun x -> ("",x)) delta_diff1 + and ass_delta_diff2 = List.map (fun x -> ("",x)) delta_diff2 in + let sigmaQ1 = localize_sigma zw_sigma1 ass_delta_diff1 + and sigmaQ2 = localize_sigma zw_sigma2 ass_delta_diff2 in + (sigmaQ1,sigmaQ2) + + let rec reduce_tree addr actual_node ftree beta_flag = + match addr with + [] -> (ftree,Empty,actual_node,beta_flag) + | a::radd -> + match ftree with + Empty -> + print_endline "Empty purity tree"; + raise jprover_bug + | NodeAt(_) -> + print_endline "Atom purity tree"; + raise jprover_bug + | NodeA(pos,strees) -> +(* print_endline pos.name; *) + (* the associated node occurs above f (or the empty address) and hence, is neither atom nor empty tree *) + + let nexttree = (Array.get strees (a-1)) in + if (nonemptys strees 0 (Array.length strees)) < 2 then + begin +(* print_endline "strees 1 or non-empties < 2"; *) + let (ft,dt,an,bf) = reduce_tree radd actual_node nexttree beta_flag in + let nstrees = myset strees (a-1) ft in +(* print_endline ("way back "^pos.name); *) + (NodeA(pos,nstrees),dt,an,bf) + end + else (* nonemptys >= 2 *) + begin +(* print_endline "nonempties >= 2 "; *) + let (new_act,new_bf) = + if pos.pt = Beta then + (actual_node,true) + else + ((pos.name),false) + in + let (ft,dt,an,bf) = reduce_tree radd new_act nexttree new_bf in + if an = pos.name then + let nstrees = myset strees (a-1) Empty in +(* print_endline ("way back assocnode "^pos.name); *) + (NodeA(pos,nstrees),nexttree,an,bf) + else (* has been replaced / will be replaced below / above pos *) + let nstrees = myset strees (a-1) ft in +(* print_endline ("way back "^pos.name); *) + (NodeA(pos,nstrees),dt,an,bf) + end + + let rec purity ftree redord connections unsolved_list = + + let rec purity_reduction pr ftree redord connections unsolved_list = + begin +(* Format.open_box 0; + print_endline " "; + print_purelist pr; + Format.force_newline (); + Format.print_flush (); +*) + match pr with + [] -> (ftree,redord,connections,unsolved_list) + | f::r -> +(* print_endline ("pure position "^(f.name)); *) + let (ftnew,deltree,assocn,beta_flag) = reduce_tree f.address "" ftree false + in +(* print_endline ("assoc node "^assocn); *) + if assocn = "" then + (Empty,[],[],[]) (* should not occur in the final version *) + else + let (rednew,connew,unsolnew) = update_relations deltree redord connections unsolved_list in + begin +(* Format.open_box 0; + print_endline " "; + print_pairlist connew; + Format.force_newline (); + Format.print_flush (); +*) + if beta_flag = true then + begin +(* print_endline "beta_flag true"; *) + purity ftnew rednew connew unsolnew + (* new pure positions may occur; old ones may not longer exist *) + end + else + purity_reduction r ftnew rednew connew unsolnew (* let's finish the old pure positions *) + end + end + + in + let flist,slist = List.split connections in + let pr = collect_pure [ftree] (flist,slist) in + purity_reduction pr ftree redord connections unsolved_list + + let rec betasplit addr ftree redord connections unsolved_list = + match ftree with + Empty -> + print_endline "bsplit Empty tree"; + raise jprover_bug + | NodeAt(_) -> + print_endline "bsplit Atom tree"; + raise jprover_bug (* the beta-node should actually occur! *) + | NodeA(pos,strees) -> + match addr with + [] -> (* we are at the beta node under consideration *) + let st1tree = (Array.get strees 0) + and st2tree = (Array.get strees 1) in + let (zw1red,zw1conn,zw1uslist) = update_relations st2tree redord connections unsolved_list + and (zw2red,zw2conn,zw2uslist) = update_relations st1tree redord connections unsolved_list in + ((NodeA(pos,[|st1tree;Empty|])),zw1red,zw1conn,zw1uslist), + ((NodeA(pos,[|Empty;st2tree|])),zw2red,zw2conn,zw2uslist) + | f::rest -> + let nexttree = Array.get strees (f-1) in + let (zw1ft,zw1red,zw1conn,zw1uslist),(zw2ft,zw2red,zw2conn,zw2uslist) = + betasplit rest nexttree redord connections unsolved_list in +(* let scopytrees = Array.copy strees in *) + let zw1trees = myset strees (f-1) zw1ft + and zw2trees = myset strees (f-1) zw2ft in + (NodeA(pos,zw1trees),zw1red,zw1conn,zw1uslist),(NodeA(pos,zw2trees),zw2red,zw2conn,zw2uslist) + + + + + let split addr pname ftree redord connections unsolved_list opt_bproof = + let (opt_bp1,min_con1),(opt_bp2,min_con2) = split_permutation pname opt_bproof in + begin +(* + print_endline "Beta proof 1: "; + print_endline ""; + print_beta_proof opt_bp1; + print_endline ""; + print_endline ("Beta proof 1 connections: "); + Format.open_box 0; + print_pairlist min_con1; + print_endline "."; + Format.print_flush(); + print_endline ""; + print_endline ""; + print_endline "Beta proof 2: "; + print_endline ""; + print_beta_proof opt_bp2; + print_endline ""; + print_endline ("Beta proof 2 connections: "); + Format.open_box 0; + print_pairlist min_con2; + print_endline "."; + Format.print_flush(); + print_endline ""; +*) + let (zw1ft,zw1red,zw1conn,zw1uslist),(zw2ft,zw2red,zw2conn,zw2uslist) = + betasplit addr ftree redord connections unsolved_list in +(* zw1conn and zw2conn are not longer needed when using beta proofs *) +(* print_endline "betasp_out"; *) + let ft1,red1,conn1,uslist1 = purity zw1ft zw1red min_con1 zw1uslist in +(* print_endline "purity_one_out"; *) + let ft2,red2,conn2,uslist2 = purity zw2ft zw2red min_con2 zw2uslist in +(* print_endline "purity_two_out"; *) +(* again, min_con1 = conn1 and min_con2 = conn2 should hold *) + begin +(* print_endline ""; + print_endline ""; + print_endline ("Purity 1 connections: "); + Format.open_box 0; + print_pairlist conn1; + print_endline "."; + print_endline ""; + Format.print_flush(); + print_endline ""; + print_endline ""; + print_endline ("Purity 2 connections: "); + Format.open_box 0; + print_pairlist conn2; + print_endline "."; + print_endline ""; + Format.print_flush(); + print_endline ""; + print_endline ""; +*) + (ft1,red1,conn1,uslist1,opt_bp1),(ft2,red2,conn2,uslist2,opt_bp2) + end + end + + +(* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% Splitting end %%%%%%%%%%%%%%%% *) + + +(* for wait labels we collect all solved atoms with pol=0 *) + + let rec collect_solved_O_At ftreelist slist = + match ftreelist with + [] -> + [] + | f::r -> + match f with + Empty -> (* may become possible after purity *) + collect_solved_O_At r slist + | NodeAt(pos) -> + if ((List.mem (pos.name) slist) or (pos.pol = I)) then (* recall slist is the unsolved list *) + collect_solved_O_At r slist + else + (* here, we have pos solved and pos.pol = O) *) + pos::(collect_solved_O_At r slist) + | NodeA(pos,treearray) -> + collect_solved_O_At ((Array.to_list treearray) @ r) slist + + let rec red_ord_block pname redord = + match redord with + [] -> false + | (f,fset)::r -> + if ((f = pname) or (not (StringSet.mem pname fset))) then + red_ord_block pname r + else + true (* then, we have (StringSet.mem pname fset) *) + + let rec check_wait_succ_LJ faddress ftree = + match ftree with + Empty -> raise jprover_bug + | NodeAt(pos) -> raise jprover_bug (* we have an gamma_0 position or an or-formula *) + | NodeA(pos,strees) -> + match faddress with + [] -> + if pos.op = Or then + match (strees.(0),strees.(1)) with + (Empty,Empty) -> raise (Invalid_argument "Jprover: redundancies occur") + | (Empty,_) -> (false,2) (* determines the Orr2 rule *) + | (_,Empty) -> (false,1) (* determines the Orr1 ruke *) + | (_,_) -> (true,0) (* wait-label is set *) + else + (false,0) + | f::r -> + if r = [] then + if (pos.pt = Gamma) & ((nonemptys strees 0 (Array.length strees)) > 1) then + (true,0) (* we are at a gamma position (exr) with one than one successor -- wait label in LJ*) + else + check_wait_succ_LJ r (Array.get strees (f-1)) + else + check_wait_succ_LJ r (Array.get strees (f-1)) + + let blocked f po redord ftree connections slist logic calculus opt_bproof = +(* print_endline ("Blocking check "^(f.name)); *) + if (red_ord_block (f.name) redord) then + begin +(* print_endline "wait-1 check positive"; *) + true,0 + end + else + if logic = "C" then + false,0 (* ready, in C only redord counts *) + else + let pa_O = collect_solved_O_At [ftree] slist (* solved atoms in ftree *) + and po_test = (delete f po) in + if calculus = "LJmc" then (* we provide dynamic wait labels for both sequent calculi *) +(* print_endline "wait-2 check"; *) + if (f.st = Psi_0) & (f.pt <> PNull) & + ((pa_O <> []) or (List.exists (fun x -> x.pol = O) po_test)) then + begin +(* print_endline "wait-2 positive"; *) + true,0 (* wait_2 label *) + end + else + begin +(* print_endline "wait-2 negative"; *) + false,0 + end + else (* calculus is supposed to be LJ *) + if calculus = "LJ" then + if ((f.st = Phi_0) & ((f.op=Neg) or (f.op=Imp)) & + ((pa_O <> []) or (List.exists (fun x -> x.pol = O) po_test)) + ) + (* this would cause an impl or negl rule with an non-empty succedent *) + then + if (f.op=Neg) then + true,0 + else (* (f.op=Imp) *) + (* In case of an impl rule on A => B, the wait_label must NOT be set + iff all succedent formulae depend exclusively on B. For this, we + perform a split operation and determine, if in the A-subgoal + all succedent formulae are pure, i.e.~have been deleted from treds. + Otherwise, in case of A-dependent succedent formulae, the + wait_label must be set. + *) + let ((_,min_con1),_) = split_permutation f.name opt_bproof in + let slist_fake = delete f.name slist in + let ((zw1ft,zw1red,_,zw1uslist),_) = + betasplit (f.address) ftree redord connections slist_fake in + let ft1,_,_,uslist1 = purity zw1ft zw1red min_con1 zw1uslist in +(* print_endline "wait label purity_one_out"; *) + let ft1_root = (List.hd (List.tl (tpredsucc f ft1))) in +(* print_endline ("wait-root "^(ft1_root.name)); *) + let po_fake = compute_open [ft1] uslist1 in + let po_fake_test = delete ft1_root po_fake + and pa_O_fake = collect_solved_O_At [ft1] uslist1 in +(* print_purelist (po_fake_test @ pa_O_fake); *) + if ((pa_O_fake <> []) or (List.exists (fun x -> x.pol = O) po_fake_test)) then + true,0 + else + false,0 + else + if ((f.pol=O) & ((f.st=Gamma_0) or (f.op=Or))) then + let (bool,orr_flag) = check_wait_succ_LJ f.address ftree in + (bool,orr_flag) + (* here is determined if orr1 or orr2 will be performed, provided bool=false) *) + (* orr_flag can be 1 or 2 *) + else + false,0 + else + raise (Invalid_argument "Jprover: calculus should be LJmc or LJ") + + let rec get_beta_preference list actual = + match list with + [] -> actual + | (f,int)::r -> + if f.op = Imp then + (f,int) + else +(* if f.op = Or then + get_beta_preference r (f,int) + else +*) + get_beta_preference r actual + + exception Gamma_deadlock + + let rec select_pos search_po po redord ftree connections slist logic calculus candidates + opt_bproof = + match search_po with + [] -> + (match candidates with + [] -> + if calculus = "LJ" then + raise Gamma_deadlock (* permutation may be necessary *) + else + raise (Invalid_argument "Jprover bug: overall deadlock") (* this case should not occur *) + | c::rest -> + get_beta_preference (c::rest) c + ) + | f::r -> (* there exist an open position *) + let (bool,orr_flag) = (blocked f po redord ftree connections slist logic calculus + opt_bproof) + in + if (bool = true) then + select_pos r po redord ftree connections slist logic calculus candidates opt_bproof + else + if f.pt = Beta then + (* search for non-splitting rules first *) +(* let beta_candidate = + if candidates = [] + then + [(f,orr_flag)] + else + !!!! but preserve first found candidate !!!!!!! + candidates + in + !!!!!!! this strategy is not sure the best -- back to old !!!!!!!!! +*) + select_pos r po redord ftree connections slist logic calculus + ((f,orr_flag)::candidates) opt_bproof + else + (f,orr_flag) + +(* let rec get_position_in_tree pname treelist = + match treelist with + [] -> raise jprover_bug + | f::r -> + begin match f with + Empty -> get_position_in_tree pname r + | NodeAt(pos) -> + if pos.name = pname then + pos + else + get_position_in_tree pname r + | NodeA(pos,suctrees) -> + get_position_in_tree pname ((Array.to_list suctrees) @ r) + end +*) + +(* total corresponds to tot in the thesis, + tot simulates the while-loop, solve is the rest *) + + let rec total ftree redord connections csigmaQ slist logic calculus opt_bproof = + let rec tot ftree redord connections po slist = + let rec solve ftree redord connections p po slist (pred,succs) orr_flag = + let newslist = delete (p.name) slist in + let rback = + if p.st = Gamma_0 then + begin +(* print_endline "that's the gamma rule"; *) + [((p.name,pred.name),(build_rule pred p csigmaQ orr_flag calculus))] + end + else + [] + in +(* print_endline "gamma check finish"; *) + let pnew = + if p.pt <> Beta then + succs @ (delete p po) + else + po + in + match p.pt with + Gamma -> + rback @ (tot ftree redord connections pnew newslist) + | Psi -> + if p.op = At then + let succ = List.hd succs in + rback @ (solve ftree redord connections succ pnew newslist (p,[]) orr_flag) (* solve atoms immediately *) + else + rback @ (tot ftree redord connections pnew newslist) + | Phi -> + if p.op = At then + let succ = List.hd succs in + rback @ (solve ftree redord connections succ pnew newslist (p,[]) orr_flag) (* solve atoms immediately *) + else + rback @ (tot ftree redord connections pnew newslist) + | PNull -> + let new_redord = update p.name redord in + let (c1,c2) = select_connection (p.name) connections newslist in + if (c1= "none" & c2 ="none") then + rback @ (tot ftree new_redord connections pnew newslist) + else + let (ass_pos,inst_pos) = +(* need the pol=O position ass_pos of the connection for later permutation *) +(* need the pol=I position inst_pos for NuPRL instantiation *) + if p.name = c1 then + if p.pol = O then + (c1,c2) + else + (c2,c1) + else (* p.name = c2 *) + if p.pol = O then + (c2,c1) + else + (c1,c2) + in + rback @ [(("",ass_pos),(build_rule p p csigmaQ orr_flag calculus))] + (* one possibility of recursion end *) + | Alpha -> + rback @ ((("",p.name),(build_rule p p csigmaQ orr_flag calculus))::(tot ftree redord connections pnew newslist)) + | Delta -> + let sp = List.hd succs in + rback @ ((("",p.name),(build_rule p sp csigmaQ orr_flag calculus))::(tot ftree redord connections pnew newslist)) + | Beta -> +(* print_endline "split_in"; *) + let (ft1,red1,conn1,uslist1,opt_bproof1),(ft2,red2,conn2,uslist2,opt_bproof2) = + split (p.address) (p.name) ftree redord connections newslist opt_bproof in + let (sigmaQ1,sigmaQ2) = subst_split ft1 ft2 ftree uslist1 uslist2 newslist csigmaQ in +(* print_endline "split_out"; *) + let p1 = total ft1 red1 conn1 sigmaQ1 uslist1 logic calculus opt_bproof1 in +(* print_endline "compute p1 out"; *) + let p2 = total ft2 red2 conn2 sigmaQ2 uslist2 logic calculus opt_bproof2 in +(* print_endline "compute p2 out"; *) + rback @ [(("",p.name),(build_rule p p csigmaQ orr_flag calculus))] @ p1 @ p2 (* second possibility of recursion end *) + in + begin try + let (p,orr_flag) = select_pos po po redord ftree connections slist logic + calculus [] opt_bproof + (* last argument for guiding selection strategy *) + in +(* print_endline ((p.name)^" "^(string_of_int orr_flag)); *) + let predsuccs = tpredsucc p ftree in + let pred = List.hd predsuccs + and succs = List.tl predsuccs in + let redpo = update (p.name) redord in (* deletes the entry (p,psuccset) from the redord *) + let rednew = + if (p.pt = Delta) then (* keep the tree ordering for the successor position only *) + let psucc = List.hd succs in + let ppsuccs = tpredsucc psucc ftree in + let pre = List.hd ppsuccs + and sucs = List.tl ppsuccs in + replace_ordering (psucc.name) sucs redpo (* union the succsets of psucc *) + else + redpo + in +(* print_endline "update ok"; *) + solve ftree rednew connections p po slist (pred,succs) orr_flag + with Gamma_deadlock -> + let ljmc_subproof = total ftree redord connections csigmaQ slist "J" "LJmc" opt_bproof + in + eigen_counter := 1; + permute_ljmc ftree po slist ljmc_subproof + (* the permuaiton result will be appended to the lj proof constructed so far *) + end + in + let po = compute_open [ftree] slist in + tot ftree redord connections po slist + + let reconstruct ftree redord sigmaQ ext_proof logic calculus = + let min_connections = remove_dups_connections ext_proof in + let (opt_bproof,beta_exp,closures) = construct_opt_beta_proof ftree ext_proof in +(* let connections = remove_dups_connections ext_proof in + let bproof,beta_exp,closures = construct_beta_proof ftree connections in + let (opt_bproof,min_connections) = bproof_purity bproof in +*) + if !debug_jprover then + begin + print_endline ""; + print_endline ("Beta proof with number of closures = "^(string_of_int closures)^" and number of beta expansions = "^(string_of_int beta_exp)); +(* print_endline ""; + print_endline ""; + print_beta_proof bproof; + print_endline ""; + print_endline ""; + print_endline "Optimal beta proof: "; + print_endline ""; + print_endline ""; + print_beta_proof opt_bproof; + print_endline ""; + print_endline ""; + print_endline ("Beta proof connections: "); + Format.open_box 0; + print_pairlist min_connections; + print_endline "."; + Format.print_flush(); *) + print_endline ""; + end; + let (newroot_name,unsolved_list) = build_unsolved ftree in + let redord2 = (update newroot_name redord) in (* otherwise we would have a deadlock *) + let (init_tree,init_redord,init_connections,init_unsolved_list) = + purity ftree redord2 min_connections unsolved_list in + begin +(* print_endline ""; + print_endline ""; + print_endline ("Purity connections: "); + Format.open_box 0; + print_pairlist init_connections; + print_endline "."; + print_endline ""; + Format.print_flush(); + print_endline ""; + print_endline ""; +*) +(* it should hold: min_connections = init_connections *) + total init_tree init_redord init_connections sigmaQ + init_unsolved_list logic calculus opt_bproof + end + +(* ***************** REDUCTION ORDERING -- both types **************************** *) + + exception Reflexive + + let rec transitive_irreflexive_closure addset const ordering = + match ordering with + [] -> + [] + | (pos,fset)::r -> + if (pos = const) or (StringSet.mem const fset) then +(* check reflexsivity during transitive closure wrt. addset ONLY!!! *) + if StringSet.mem pos addset then + raise Reflexive + else + (pos,(StringSet.union fset addset))::(transitive_irreflexive_closure addset const r) + else + (pos,fset)::(transitive_irreflexive_closure addset const r) + + let rec search_set var ordering = +(* print_endline var; *) + match ordering with + [] -> + raise (Invalid_argument "Jprover: element in ordering missing") + | (pos,fset)::r -> + if pos = var then + StringSet.add pos fset + else + search_set var r + + let add_sets var const ordering = + let addset = search_set var ordering in + transitive_irreflexive_closure addset const ordering + +(* ************* J ordering ********************************************** *) + + let rec add_arrowsJ (v,vlist) ordering = + match vlist with + [] -> ordering + | f::r -> + if ((String.get f 0)='c') then + let new_ordering = add_sets v f ordering in + add_arrowsJ (v,r) new_ordering + else + add_arrowsJ (v,r) ordering + + let rec add_substJ replace_vars replace_string ordering atom_rel = + match replace_vars with + [] -> ordering + | v::r -> + if (String.get v 1 = 'n') (* don't integrate new variables *) + or (List.exists (fun (x,_,_) -> (x.aname = v)) atom_rel) then (* no reduction ordering at atoms *) + (add_substJ r replace_string ordering atom_rel) + else + let next_ordering = add_arrowsJ (v,replace_string) ordering in + (add_substJ r replace_string next_ordering atom_rel) + + let build_orderingJ replace_vars replace_string ordering atom_rel = + try + add_substJ replace_vars replace_string ordering atom_rel + with Reflexive -> (* only possible in the FO case *) + raise Not_unifiable (*search for alternative string unifiers *) + + let rec build_orderingJ_list substJ ordering atom_rel = + match substJ with + [] -> ordering + | (v,vlist)::r -> + let next_ordering = build_orderingJ [v] vlist ordering atom_rel in + build_orderingJ_list r next_ordering atom_rel + +(* ************* J ordering END ********************************************** *) + +(* ************* quantifier ordering ********************************************** *) + + let rec add_arrowsQ v clist ordering = + match clist with + [] -> ordering + | f::r -> + let new_ordering = add_sets v f ordering in + add_arrowsQ v r new_ordering + + let rec print_sigmaQ sigmaQ = + match sigmaQ with + [] -> + print_endline "." + | (v,term)::r -> + begin + Format.open_box 0; + print_endline " "; + print_string (v^" = "); + print_term stdout term; + Format.force_newline (); + Format.print_flush (); + print_sigmaQ r + end + + let rec print_term_list tlist = + match tlist with + [] -> print_string "." + | t::r -> + begin + print_term stdout t; + print_string " "; + print_term_list r + end + + let rec add_sigmaQ new_elements ordering = + match new_elements with + [] -> ([],ordering) + | (v,termlist)::r -> + let dterms = collect_delta_terms termlist in + begin +(*: print_stringlist dterms; + mbreak "add_sigmaQ:1\n"; + Format.open_box 0; + print_endline " "; + print_endline "sigmaQ: "; + print_string (v^" = "); + print_term_list termlist; + Format.force_newline (); + print_stringlist dterms; + Format.force_newline (); + Format.print_flush (); + mbreak "add_sigmaQ:2\n"; +:*) + let new_ordering = add_arrowsQ v dterms ordering in +(*: print_ordering new_ordering; + mbreak "add_sigmaQ:3\n"; +:*) + let (rest_pairs,rest_ordering) = add_sigmaQ r new_ordering in + ((v,dterms)::rest_pairs),rest_ordering + end + + let build_orderingQ new_elements ordering = +(* new_elements is of type (string * term list) list, since one variable can receive more than *) +(* a single term due to substitution multiplication *) + try +(* print_endline "build orderingQ in"; *) (* apple *) + add_sigmaQ new_elements ordering; + with Reflexive -> + raise Failed (* new connection, please *) + + +(* ************* quantifier ordering END ********************************************** *) + +(* ****** Quantifier unification ************** *) + +(* For multiplication we assume always idempotent substitutions sigma, tau! *) + + let rec collect_assoc inst_vars tauQ = + match inst_vars with + [] -> [] + | f::r -> + let f_term = List.assoc f tauQ in + f_term::(collect_assoc r tauQ) + + let rec rec_apply sigmaQ tauQ tau_vars tau_terms = + match sigmaQ with + [] -> [],[] + | (v,term)::r -> + let app_term = subst term tau_vars tau_terms in + let old_free = free_vars_list term + and new_free = free_vars_list app_term in + let inst_vars = list_diff old_free new_free in + let inst_terms = collect_assoc inst_vars tauQ in + let (rest_sigma,rest_sigma_ordering) = rec_apply r tauQ tau_vars tau_terms in + if inst_terms = [] then + ((v,app_term)::rest_sigma),rest_sigma_ordering + else + let ordering_v = String.sub v 0 (String.index v '_') in + ((v,app_term)::rest_sigma),((ordering_v,inst_terms)::rest_sigma_ordering) + +(* let multiply sigmaQ tauQ = + let tau_vars,tau_terms = List.split tauQ + and sigma_vars,sigma_terms = List.split sigmaQ in + let apply_terms = rec_apply sigma_terms tau_vars tau_terms in + (List.combine sigma_vars apply_terms) @ tauQ +*) + + let multiply sigmaQ tauQ = + let (tau_vars,tau_terms) = List.split tauQ in + let (new_sigmaQ,sigma_ordering) = rec_apply sigmaQ tauQ tau_vars tau_terms in + let tau_ordering_terms = (List.map (fun x -> [x]) tau_terms) (* for extending ordering_elements *) in + let tau_ordering_vars = (List.map (fun x -> String.sub x 0 (String.index x '_')) tau_vars) in + let tau_ordering = (List.combine tau_ordering_vars tau_ordering_terms) in + ((new_sigmaQ @ tauQ), + (sigma_ordering @ tau_ordering) + ) + + let apply_2_sigmaQ term1 term2 sigmaQ = + let sigma_vars,sigma_terms = List.split sigmaQ in + (subst term1 sigma_vars sigma_terms),(subst term2 sigma_vars sigma_terms) + + let jqunify term1 term2 sigmaQ = + let app_term1,app_term2 = apply_2_sigmaQ term1 term2 sigmaQ in + try +(*: let tauQ = unify_mm app_term1 app_term2 String_set.StringSet.empty in :*) + let tauQ = unify_mm app_term1 app_term2 StringSet.empty in + let (mult,oel) = multiply sigmaQ tauQ in + (mult,oel) + with + RefineError _ -> (* any unification failure *) +(* print_endline "fo-unification fail"; *) + raise Failed (* new connection, please *) + +(* ************ T-STRING UNIFICATION ******************************** *) + + let rec combine subst (ov,oslist) = + match subst with + [] -> [],[] + | f::r -> + let (v,slist) = f in + let rest_vlist,rest_combine = (combine r (ov,oslist)) in + if (List.mem ov slist) then (* subst assumed to be idemponent *) + let com_element = com_subst slist (ov,oslist) in + (v::rest_vlist),((v,com_element)::rest_combine) + else + (rest_vlist,(f::rest_combine)) + + let compose sigma one_subst = + let (n,subst)=sigma + and (ov,oslist) = one_subst in + let (trans_vars,com) = combine subst (ov,oslist) + in +(* begin + print_endline "!!!!!!!!!test print!!!!!!!!!!"; + print_subst [one_subst]; + print_subst subst; + print_endline "!!!!!!!!! END test print!!!!!!!!!!"; +*) + if List.mem one_subst subst then + (trans_vars,(n,com)) + else +(* ov may multiply as variable in subst with DIFFERENT values *) +(* in order to avoid explicit atom instances!!! *) + (trans_vars,(n,(com @ [one_subst]))) +(* end *) + + let rec apply_element fs ft (v,slist) = + match (fs,ft) with + ([],[]) -> + ([],[]) + | ([],(ft_first::ft_rest)) -> + let new_ft_first = + if ft_first = v then + slist + else + [ft_first] + in + let (emptylist,new_ft_rest) = apply_element [] ft_rest (v,slist) in + (emptylist,(new_ft_first @ new_ft_rest)) + | ((fs_first::fs_rest),[]) -> + let new_fs_first = + if fs_first = v then + slist + else + [fs_first] + in + let (new_fs_rest,emptylist) = apply_element fs_rest [] (v,slist) in + ((new_fs_first @ new_fs_rest),emptylist) + | ((fs_first::fs_rest),(ft_first::ft_rest)) -> + let new_fs_first = + if fs_first = v then + slist + else + [fs_first] + and new_ft_first = + if ft_first = v then + slist + else + [ft_first] + in + let (new_fs_rest,new_ft_rest) = apply_element fs_rest ft_rest (v,slist) in + ((new_fs_first @ new_fs_rest),(new_ft_first @ new_ft_rest)) + + let rec shorten us ut = + match (us,ut) with + ([],_) -> (us,ut) + | (_,[]) -> (us,ut) + | ((fs::rs),(ft::rt)) -> + if fs = ft then + shorten rs rt + else + (us,ut) + + let rec apply_subst_list eq_rest (v,slist) = + + match eq_rest with + [] -> + (true,[]) + | (atomnames,(fs,ft))::r -> + let (n_fs,n_ft) = apply_element fs ft (v,slist) in + let (new_fs,new_ft) = shorten n_fs n_ft in (* delete equal first elements *) + match (new_fs,new_ft) with + [],[] -> + let (bool,new_eq_rest) = apply_subst_list r (v,slist) in + (bool,((atomnames,([],[]))::new_eq_rest)) + | [],(fft::rft) -> + if (is_const fft) then + (false,[]) + else + let (bool,new_eq_rest) = apply_subst_list r (v,slist) in + (bool,((atomnames,([],new_ft))::new_eq_rest)) + | (ffs::rfs),[] -> + if (is_const ffs) then + (false,[]) + else + let (bool,new_eq_rest) = apply_subst_list r (v,slist) in + (bool,((atomnames,(new_fs,[]))::new_eq_rest)) + | (ffs::rfs),(fft::rft) -> + if (is_const ffs) & (is_const fft) then + (false,[]) + (* different first constants cause local fail *) + else + (* at least one of firsts is a variable *) + let (bool,new_eq_rest) = apply_subst_list r (v,slist) in + (bool,((atomnames,(new_fs,new_ft))::new_eq_rest)) + + let apply_subst eq_rest (v,slist) atomnames = + if (List.mem v atomnames) then (* don't apply subst to atom variables !! *) + (true,eq_rest) + else + apply_subst_list eq_rest (v,slist) + + let all_variable_check eqlist = false (* needs some discussion with Jens! -- NOT done *) + +(* + let rec all_variable_check eqlist = + match eqlist with + [] -> true + | ((_,(fs,ft))::rest_eq) -> + if (fs <> []) & (ft <> []) then + let fs_first = List.hd fs + and ft_first = List.hd ft + in + if (is_const fs_first) or (is_const ft_first) then + false + else + all_variable_check rest_eq + else + false +*) + + let rec tunify_list eqlist init_sigma orderingQ atom_rel = + + let rec tunify atomnames fs ft rt rest_eq sigma ordering = + + let apply_r1 fs ft rt rest_eq sigma = +(* print_endline "r1"; *) + tunify_list rest_eq sigma ordering atom_rel + + in + let apply_r2 fs ft rt rest_eq sigma = +(* print_endline "r2"; *) + tunify atomnames rt fs ft rest_eq sigma ordering + + in + let apply_r3 fs ft rt rest_eq sigma = +(* print_endline "r3"; *) + let rfs = (List.tl fs) + and rft = (List.tl rt) in + tunify atomnames rfs ft rft rest_eq sigma ordering + + in + let apply_r4 fs ft rt rest_eq sigma = +(* print_endline "r4"; *) + tunify atomnames rt ft fs rest_eq sigma ordering + + in + let apply_r5 fs ft rt rest_eq sigma = +(* print_endline "r5"; *) + let v = (List.hd fs) in + let (compose_vars,new_sigma) = compose sigma (v,ft) in + let (bool,new_rest_eq) = apply_subst rest_eq (v,ft) atomnames in + if (bool=false) then + raise Not_unifiable + else + let new_ordering = build_orderingJ (v::compose_vars) ft ordering atom_rel in + tunify atomnames (List.tl fs) rt rt new_rest_eq new_sigma new_ordering + + in + let apply_r6 fs ft rt rest_eq sigma = +(* print_endline "r6"; *) + let v = (List.hd fs) in + let (_,new_sigma) = (compose sigma (v,[])) in + let (bool,new_rest_eq) = apply_subst rest_eq (v,[]) atomnames in + if (bool=false) then + raise Not_unifiable + else + (* no relation update since [] has been replaced for v *) + tunify atomnames (List.tl fs) ft rt new_rest_eq new_sigma ordering + + in + let apply_r7 fs ft rt rest_eq sigma = +(* print_endline "r7"; *) + let v = (List.hd fs) + and c1 = (List.hd rt) + and c2t =(List.tl rt) in + let (compose_vars,new_sigma) = (compose sigma (v,(ft @ [c1]))) in + let (bool,new_rest_eq) = apply_subst rest_eq (v,(ft @ [c1])) atomnames in + if bool=false then + raise Not_unifiable + else + let new_ordering = build_orderingJ (v::compose_vars) (ft @ [c1]) ordering atom_rel in + tunify atomnames (List.tl fs) [] c2t new_rest_eq new_sigma new_ordering + + + in + let apply_r8 fs ft rt rest_eq sigma = +(* print_endline "r8"; *) + tunify atomnames rt [(List.hd fs)] (List.tl fs) rest_eq sigma ordering + + in + let apply_r9 fs ft rt rest_eq sigma = +(* print_endline "r9"; *) + let v = (List.hd fs) + and (max,subst) = sigma in + let v_new = ("vnew"^(string_of_int max)) in + let (compose_vars,new_sigma) = (compose ((max+1),subst) (v,(ft @ [v_new]))) in + let (bool,new_rest_eq) = apply_subst rest_eq (v,(ft @ [v_new])) atomnames in + if (bool=false) then + raise Not_unifiable + else + let new_ordering = + build_orderingJ (v::compose_vars) (ft @ [v_new]) ordering atom_rel in + tunify atomnames rt [v_new] (List.tl fs) new_rest_eq new_sigma new_ordering + + in + let apply_r10 fs ft rt rest_eq sigma = +(* print_endline "r10"; *) + let x = List.hd rt in + tunify atomnames fs (ft @ [x]) (List.tl rt) rest_eq sigma ordering + + in + if r_1 fs ft rt then + apply_r1 fs ft rt rest_eq sigma + else if r_2 fs ft rt then + apply_r2 fs ft rt rest_eq sigma + else if r_3 fs ft rt then + apply_r3 fs ft rt rest_eq sigma + else if r_4 fs ft rt then + apply_r4 fs ft rt rest_eq sigma + else if r_5 fs ft rt then + apply_r5 fs ft rt rest_eq sigma + else if r_6 fs ft rt then + (try + apply_r6 fs ft rt rest_eq sigma + with Not_unifiable -> + if r_7 fs ft rt then (* r7 applicable if r6 was and tr6 = C2t' *) + (try + apply_r7 fs ft rt rest_eq sigma + with Not_unifiable -> + apply_r10 fs ft rt rest_eq sigma (* r10 always applicable if r6 was *) + ) + else +(* r10 could be represented only once if we would try it before r7.*) +(* but looking at the transformation rules, r10 should be tried at last in any case *) + apply_r10 fs ft rt rest_eq sigma (* r10 always applicable r6 was *) + ) + else if r_7 fs ft rt then (* not r6 and r7 possible if z <> [] *) + (try + apply_r7 fs ft rt rest_eq sigma + with Not_unifiable -> + apply_r10 fs ft rt rest_eq sigma (* r10 always applicable if r7 was *) + ) + else if r_8 fs ft rt then + (try + apply_r8 fs ft rt rest_eq sigma + with Not_unifiable -> + if r_10 fs ft rt then (* r10 applicable if r8 was and tr8 <> [] *) + apply_r10 fs ft rt rest_eq sigma + else + raise Not_unifiable (* simply back propagation *) + ) + else if r_9 fs ft rt then + (try + apply_r9 fs ft rt rest_eq sigma + with Not_unifiable -> + if r_10 fs ft rt then (* r10 applicable if r9 was and tr9 <> [] *) + apply_r10 fs ft rt rest_eq sigma + else + raise Not_unifiable (* simply back propagation *) + ) + + + else + if r_10 fs ft rt then (* not ri, i<10, and r10 possible if for instance *) + (* (s=[] and x=v1) or (z<>[] and xt=C1V1t') *) + apply_r10 fs ft rt rest_eq sigma + else (* NO rule applicable *) + raise Not_unifiable + in + match eqlist with + [] -> + init_sigma,orderingQ + | f::rest_eq -> + begin +(* Format.open_box 0; + print_equations [f]; + Format.print_flush (); +*) + let (atomnames,(fs,ft)) = f in + tunify atomnames fs [] ft rest_eq init_sigma orderingQ + end + +let rec test_apply_eq atomnames eqs eqt subst = + match subst with + [] -> (eqs,eqt) + | (f,flist)::r -> + let (first_appl_eqs,first_appl_eqt) = + if List.mem f atomnames then + (eqs,eqt) + else + (apply_element eqs eqt (f,flist)) + in + test_apply_eq atomnames first_appl_eqs first_appl_eqt r + +let rec test_apply_eqsubst eqlist subst = + match eqlist with + [] -> [] + | f::r -> + let (atomnames,(eqs,eqt)) = f in + let applied_element = test_apply_eq atomnames eqs eqt subst in + (atomnames,applied_element)::(test_apply_eqsubst r subst) + +let ttest us ut ns nt eqlist orderingQ atom_rel = + let (short_us,short_ut) = shorten us ut in (* apply intial rule R3 *) + (* to eliminate common beginning *) + let new_element = ([ns;nt],(short_us,short_ut)) in + let full_eqlist = + if List.mem new_element eqlist then + eqlist + else + new_element::eqlist + in + let (sigma,_) = tunify_list full_eqlist (1,[]) orderingQ atom_rel in + let (n,subst) = sigma in + let test_apply = test_apply_eqsubst full_eqlist subst in + begin + print_endline ""; + print_endline "Final equations:"; + print_equations full_eqlist; + print_endline ""; + print_endline "Final substitution:"; + print_tunify sigma; + print_endline ""; + print_endline "Applied equations:"; + print_equations test_apply + end + +let do_stringunify us ut ns nt equations fo_eqlist orderingQ atom_rel qmax = + let (short_us,short_ut) = shorten us ut in (* apply intial rule R3 to eliminate common beginning *) + let new_element = ([ns;nt],(short_us,short_ut)) in + let full_eqlist = + if List.mem new_element equations then + equations @ fo_eqlist + else + (new_element::equations) @ fo_eqlist + in + try +(* print_equations full_eqlist; *) +(* max-1 new variables have been used for the domain equations *) + let (new_sigma,new_ordering) = tunify_list full_eqlist (1,[]) orderingQ atom_rel in +(* sigmaQ will not be returned in eqlist *) + (new_sigma,(qmax,full_eqlist),new_ordering) + with Not_unifiable -> + raise Failed (* new connection please *) + +let rec one_equation gprefix dlist delta_0_prefixes n = + match dlist with + [] -> ([],n) + | f::r -> + let fprefix = List.assoc f delta_0_prefixes in + let (sf1,sg) = shorten fprefix gprefix + and v_new = ("vnewq"^(string_of_int n)) in + let fnew = sf1 @ [v_new] in + let (rest_equations,new_n) = one_equation gprefix r delta_0_prefixes (n+1) in + (([],(fnew,sg))::rest_equations),new_n + +let rec make_domain_equations fo_pairs (gamma_0_prefixes,delta_0_prefixes) n = + match fo_pairs with + [] -> ([],n) + | (g,dlist)::r -> + let gprefix = List.assoc g gamma_0_prefixes in + let (gequations,max) = one_equation gprefix dlist delta_0_prefixes n in + let (rest_equations,new_max) = + make_domain_equations r (gamma_0_prefixes,delta_0_prefixes) max in + (gequations @ rest_equations),new_max + +(* type of one unifier: int * ((string * string list) list) *) +(* global failure: (0,[]) *) + +let stringunify ext_atom try_one eqlist fo_pairs logic orderingQ atom_rel qprefixes = + if logic = "C" then + ((0,[]),(0,[]),orderingQ) + else + let (qmax,equations) = eqlist + and us = ext_atom.aprefix + and ut = try_one.aprefix + and ns = ext_atom.aname + and nt = try_one.aname in + if qprefixes = ([],[]) then (* prop case *) + begin +(* print_endline "This is the prop case"; *) + let (new_sigma,new_eqlist) = Jtunify.do_stringunify us ut ns nt equations + (* prop unification only *) + in + (new_sigma,new_eqlist,[]) (* assume the empty reduction ordering during proof search *) + end + else + begin +(* print_endline "This is the FO case"; *) +(* fo_eqlist encodes the domain condition on J quantifier substitutions *) +(* Again, always computed for the whole substitution sigmaQ *) + let (fo_eqlist,new_max) = make_domain_equations fo_pairs qprefixes qmax in + begin +(* Format.open_box 0; + print_string "domain equations in"; + print_equations fo_eqlist; + print_string "domain equations out"; + Format.print_flush (); +*) + do_stringunify us ut ns nt equations fo_eqlist orderingQ atom_rel new_max + end + end + +(**************************************** add multiplicity *********************************) + +let rec subst_replace subst_list t = + match subst_list with + [] -> t + | (old_t,new_t)::r -> + let inter_term = var_subst t old_t "dummy" in +(*: print_string "("; + print_term stdout old_t; + print_string " --> "; + print_term stdout new_t; + print_string ")\n"; + print_term stdout t; + print_newline (); + print_term stdout inter_term; + print_newline (); :*) + let new_term = subst1 inter_term "dummy" new_t in +(*: print_term stdout new_term; + print_newline (); + mbreak "\n+++========----- ---------..........\n"; :*) + subst_replace r new_term + +let rename_pos x m = + let pref = String.get x 0 in + (Char.escaped pref)^(string_of_int m) + +let update_position position m replace_n subst_list mult = + let ({name=x; address=y; op=z; pol=p; pt=a; st=b; label=t}) = position in + let nx = rename_pos x m in + let nsubst_list = + if b=Gamma_0 then + let vx = mk_var_term (x^"_jprover") + and vnx = mk_var_term (nx^"_jprover") in + (vx,vnx)::subst_list + else + if b=Delta_0 then + let sx = mk_string_term jprover_op x + and snx = mk_string_term jprover_op nx in + (sx,snx)::subst_list + else + subst_list + in + let nt = subst_replace nsubst_list t in + let add_array = Array.of_list y in + let _ = (add_array.(replace_n) <- mult) in + let new_add = Array.to_list add_array in + ({name=nx; address=new_add; op=z; pol=p; pt=a; st=b; label=nt},m,nsubst_list) + +let rec append_orderings list_of_lists = + match list_of_lists with + [] -> + [] + | f::r -> + f @ (append_orderings r) + +let rec union_orderings first_orderings = + match first_orderings with + [] -> + StringSet.empty + | (pos,fset)::r -> + StringSet.union (StringSet.add pos fset) (union_orderings r) + +let rec select_orderings add_orderings = + match add_orderings with + [] -> [] + | f::r -> + (List.hd f)::select_orderings r + +let combine_ordering_list add_orderings pos_name = + let first_orderings = select_orderings add_orderings in + let pos_succs = union_orderings first_orderings in + let rest_orderings = append_orderings add_orderings in + (pos_name,pos_succs)::rest_orderings + +let rec copy_and_rename_tree last_tree replace_n pos_n mult subst_list = + + let rec rename_subtrees tree_list nposition s_pos_n nsubst_list = + match tree_list with + [] -> ([||],[],s_pos_n) + | f::r -> + let (f_subtree,f_ordering,f_pos_n) = + copy_and_rename_tree f replace_n s_pos_n mult nsubst_list in + let (r_subtrees,r_ordering_list,r_pos_n) = rename_subtrees r nposition f_pos_n nsubst_list in + ((Array.append [|f_subtree|] r_subtrees),(f_ordering::r_ordering_list),r_pos_n) + + in + match last_tree with + Empty -> raise (Invalid_argument "Jprover: copy tree") + | NodeAt(position) -> (* can never be a Gamma_0 position -> no replacements *) + let (nposition,npos_n,_) = update_position position (pos_n+1) replace_n subst_list mult in + ((NodeAt(nposition)),[(nposition.name,StringSet.empty)],npos_n) + | NodeA(position, suctrees) -> + let (nposition,npos_n,nsubst_list) = update_position position (pos_n+1) replace_n subst_list mult in + let (new_suctrees, new_ordering_list, new_pos_n) = + rename_subtrees (Array.to_list suctrees) nposition npos_n nsubst_list in + let new_ordering = combine_ordering_list new_ordering_list (nposition.name) in + ((NodeA(nposition,new_suctrees)),new_ordering,new_pos_n) + +(* we construct for each pos a list orderings representing and correspondning to the array of succtrees *) + +let rec add_multiplicity ftree pos_n mult logic = + let rec parse_subtrees tree_list s_pos_n = + match tree_list with + [] -> ([||],[],s_pos_n) + | f::r -> + let (f_subtree,f_ordering,f_pos_n) = add_multiplicity f s_pos_n mult logic in + let (r_subtrees,r_ordering_list,r_pos_n) = parse_subtrees r f_pos_n in + ((Array.append [|f_subtree|] r_subtrees),(f_ordering::r_ordering_list),r_pos_n) + + in + match ftree with + Empty -> raise (Invalid_argument "Jprover: add mult") + | NodeAt(pos) -> (ftree,[(pos.name,StringSet.empty)],pos_n) + | NodeA(pos,suctrees) -> + let (new_suctrees, new_ordering_list, new_pos_n) = parse_subtrees (Array.to_list suctrees) pos_n in + if (((pos.pt = Phi) & (((pos.op <> At) & (logic="J")) or ((pos.op = All) & (logic = "C")))) + (* no explicit atom-instances *) + or ((pos.pt = Gamma) & (pos.st <> Phi_0))) then (* universal quantifiers are copied *) + (* at their Phi positions *) + let replace_n = (List.length pos.address) (* points to the following argument in the array_of_address *) + and last = (Array.length new_suctrees) - 1 in (* array first element has index 0 *) + let last_tree = new_suctrees.(last) in + let (add_tree,add_ordering,final_pos_n) = + copy_and_rename_tree last_tree replace_n new_pos_n mult [] in + let final_suctrees = Array.append new_suctrees [|add_tree|] + and add_orderings = List.append new_ordering_list [add_ordering] in + let final_ordering = combine_ordering_list add_orderings (pos.name) in + ((NodeA(pos,final_suctrees)),final_ordering,final_pos_n) + else + let final_ordering = combine_ordering_list new_ordering_list (pos.name) in + ((NodeA(pos,new_suctrees)),final_ordering,new_pos_n) + + +(************** Path checker ****************************************************) + +let rec get_sets atom atom_sets = + match atom_sets with + [] -> raise (Invalid_argument "Jprover bug: atom not found") + | f::r -> + let (a,b,c) = f in + if atom = a then f + else + get_sets atom r + +let rec get_connections a alpha tabulist = + match alpha with + [] -> [] + | f::r -> + if (a.apredicate = f.apredicate) & (a.apol <> f.apol) & (not (List.mem f tabulist)) then + (a,f)::(get_connections a r tabulist) + else + (get_connections a r tabulist) + +let rec connections atom_rel tabulist = + match atom_rel with + [] -> [] + | f::r -> + let (a,alpha,beta) = f in + (get_connections a alpha tabulist) @ (connections r (a::tabulist)) + +let check_alpha_relation atom set atom_sets = + let (a,alpha,beta) = get_sets atom atom_sets in + AtomSet.subset set alpha + +let rec extset atom_sets path closed = + match atom_sets with + [] -> AtomSet.empty + | f::r -> + let (at,alpha,beta) = f in + if (AtomSet.subset path alpha) & (AtomSet.subset closed beta) then + AtomSet.add at (extset r path closed) + else + (extset r path closed) + +let rec check_ext_list ext_list fail_set atom_sets = (* fail_set consists of one atom only *) + match ext_list with + [] -> AtomSet.empty + | f::r -> + if (check_alpha_relation f fail_set atom_sets) then + AtomSet.add f (check_ext_list r fail_set atom_sets) + else + (check_ext_list r fail_set atom_sets) + +let fail_ext_set ext_atom ext_set atom_sets = + let ext_list = AtomSet.elements ext_set + and fail_set = AtomSet.add ext_atom AtomSet.empty in + check_ext_list ext_list fail_set atom_sets + +let rec ext_partners con path ext_atom (reduction_partners,extension_partners) atom_sets = + match con with + [] -> + (reduction_partners,extension_partners) + | f::r -> + let (a,b) = f in + if List.mem ext_atom [a;b] then + let ext_partner = + if ext_atom = a then b else a + in + let (new_red_partners,new_ext_partners) = +(* force reduction steps first *) + if (AtomSet.mem ext_partner path) then + ((AtomSet.add ext_partner reduction_partners),extension_partners) + else + if (check_alpha_relation ext_partner path atom_sets) then + (reduction_partners,(AtomSet.add ext_partner extension_partners)) + else + (reduction_partners,extension_partners) + in + ext_partners r path ext_atom (new_red_partners,new_ext_partners) atom_sets + else + ext_partners r path ext_atom (reduction_partners,extension_partners) atom_sets + +exception Failed_connections + +let path_checker atom_rel atom_sets qprefixes init_ordering logic = + + let con = connections atom_rel [] in +(*: print_endline ""; + print_endline ("number of connections: "^(string_of_int (List.length con))); + mbreak "#connec\n"; +:*) + let rec provable path closed (orderingQ,reduction_ordering) eqlist (sigmaQ,sigmaJ) = + + let rec check_connections (reduction_partners,extension_partners) ext_atom = + let try_one = + if reduction_partners = AtomSet.empty then + if extension_partners = AtomSet.empty then + raise Failed_connections + else + AtomSet.choose extension_partners + else + (* force reduction steps always first!! *) + AtomSet.choose reduction_partners + in +(* print_endline ("connection partner "^(try_one.aname)); *) +(* print_endline ("partner path "^(print_set path)); +*) + (try + let (new_sigmaQ,new_ordering_elements) = jqunify (ext_atom.alabel) (try_one.alabel) sigmaQ in +(* build the orderingQ incrementally from the new added substitution tau of new_sigmaQ *) + let (relate_pairs,new_orderingQ) = build_orderingQ new_ordering_elements orderingQ in +(* we make in incremental reflexivity test during the string unification *) + let (new_sigmaJ,new_eqlist,new_red_ordering) = +(* new_red_ordering = [] in propositional case *) + stringunify ext_atom try_one eqlist relate_pairs logic new_orderingQ atom_rel qprefixes + in +(* print_endline ("make reduction ordering "^((string_of_int (List.length new_ordering)))); *) + let new_closed = AtomSet.add ext_atom closed in + let ((next_orderingQ,next_red_ordering),next_eqlist,(next_sigmaQ,next_sigmaJ),subproof) = + if AtomSet.mem try_one path then + provable path new_closed (new_orderingQ,new_red_ordering) new_eqlist (new_sigmaQ,new_sigmaJ) + (* always use old first-order ordering for recursion *) + else + let new_path = AtomSet.add ext_atom path + and extension = AtomSet.add try_one AtomSet.empty in + let ((norderingQ,nredordering),neqlist,(nsigmaQ,nsigmaJ),p1) = + provable new_path extension (new_orderingQ,new_red_ordering) new_eqlist (new_sigmaQ,new_sigmaJ) in + let ((nnorderingQ,nnredordering),nneqlist,(nnsigmaQ,nnsigmaJ),p2) = + provable path new_closed (norderingQ,nredordering) neqlist (nsigmaQ,nsigmaJ) in + ((nnorderingQ,nnredordering),nneqlist,(nnsigmaQ,nnsigmaJ),(p1 @ p2)) + (* first the extension subgoals = depth first; then other subgoals in same clause *) + in + ((next_orderingQ,next_red_ordering),next_eqlist,(next_sigmaQ,next_sigmaJ),(((ext_atom.aname),(try_one.aname))::subproof)) + with Failed -> +(* print_endline ("new connection for "^(ext_atom.aname)); *) +(* print_endline ("Failed"); *) + check_connections ((AtomSet.remove try_one reduction_partners), + (AtomSet.remove try_one extension_partners) + ) ext_atom + ) + + in + let rec check_extension extset = + if extset = AtomSet.empty then + raise Failed (* go directly to a new entry connection *) + else + let select_one = AtomSet.choose extset in +(* print_endline ("extension literal "^(select_one.aname)); *) +(* print_endline ("extension path "^(print_set path));*) + let (reduction_partners,extension_partners) = + ext_partners con path select_one (AtomSet.empty,AtomSet.empty) atom_sets in + (try + check_connections (reduction_partners,extension_partners) select_one + with Failed_connections -> +(* print_endline ("no connections for subgoal "^(select_one.aname)); *) +(* print_endline ("Failed_connections"); *) + let fail_ext_set = fail_ext_set select_one extset atom_sets in + check_extension fail_ext_set + ) + + in + let extset = extset atom_sets path closed in + if extset = AtomSet.empty then + ((orderingQ,reduction_ordering),eqlist,(sigmaQ,sigmaJ),[]) + else + check_extension extset + in + if qprefixes = ([],[]) then + begin +(* print_endline "!!!!!!!!!!! prop prover !!!!!!!!!!!!!!!!!!"; *) +(* in the propositional case, the reduction ordering will be computed AFTER proof search *) + let (_,eqlist,(_,(n,substJ)),ext_proof) = + provable AtomSet.empty AtomSet.empty ([],[]) (1,[]) ([],(1,[])) in + let orderingJ = build_orderingJ_list substJ init_ordering atom_rel in + ((init_ordering,orderingJ),eqlist,([],(n,substJ)),ext_proof) + end + else + provable AtomSet.empty AtomSet.empty (init_ordering,[]) (1,[]) ([],(1,[])) + +(*************************** prepare and init prover *******************************************************) + +let rec list_to_set list = + match list with + [] -> AtomSet.empty + | f::r -> + let rest_set = list_to_set r in + AtomSet.add f rest_set + +let rec make_atom_sets atom_rel = + match atom_rel with + [] -> [] + | f::r -> + let (a,alpha,beta) = f in + (a,(list_to_set alpha),(list_to_set beta))::(make_atom_sets r) + +let rec predecessor address_1 address_2 ftree = + match ftree with + Empty -> PNull (* should not occur since every pair of atoms have a common predecessor *) + | NodeAt(position) -> PNull (* should not occur as above *) + | NodeA(position,suctrees) -> + match address_1,address_2 with + [],_ -> raise (Invalid_argument "Jprover: predecessors left") + | _,[] -> raise (Invalid_argument "Jprover: predecessors right") + | (f1::r1),(f2::r2) -> + if f1 = f2 then + predecessor r1 r2 (suctrees.(f1-1)) + else + position.pt + +let rec compute_sets element ftree alist = + match alist with + [] -> [],[] + | first::rest -> + if first = element then + compute_sets element ftree rest (* element is neithes alpha- nor beta-related to itself*) + else + let (alpha_rest,beta_rest) = compute_sets element ftree rest in + if predecessor (element.aaddress) (first.aaddress) ftree = Beta then + (alpha_rest,(first::beta_rest)) + else + ((first::alpha_rest),beta_rest) + +let rec compute_atomlist_relations worklist ftree alist = (* last version of alist for total comparison *) + let rec compute_atom_relations element ftree alist = + let alpha_set,beta_set = compute_sets element ftree alist in + (element,alpha_set,beta_set) + in + match worklist with + [] -> [] + | first::rest -> + let first_relations = compute_atom_relations first ftree alist in + first_relations::(compute_atomlist_relations rest ftree alist) + +let atom_record position prefix = + let aname = (position.name) in + let aprefix = (List.append prefix [aname]) in (* atom position is last element in prefix *) + let aop = (dest_term position.label).term_op in + ({aname=aname; aaddress=(position.address); aprefix=aprefix; apredicate=aop; + apol=(position.pol); ast=(position.st); alabel=(position.label)}) + +let rec select_atoms_treelist treelist prefix = + let rec select_atoms ftree prefix = + match ftree with + Empty -> [],[],[] + | NodeAt(position) -> + [(atom_record position prefix)],[],[] + | NodeA(position,suctrees) -> + let treelist = Array.to_list suctrees in + let new_prefix = + let prefix_element = + if List.mem (position.st) [Psi_0;Phi_0] then + [(position.name)] + else + [] + in + (List.append prefix prefix_element) + in + let (gamma_0_element,delta_0_element) = + if position.st = Gamma_0 then + begin +(* Format.open_box 0; + print_endline "gamma_0 prefixes "; + print_string (position.name^" :"); + print_stringlist prefix; + print_endline " "; + Format.force_newline (); + Format.print_flush (); +*) + [(position.name,prefix)],[] + end + else + if position.st = Delta_0 then + begin +(* Format.open_box 0; + print_endline "delta_0 prefixes "; + print_string (position.name^" :"); + print_stringlist prefix; + print_endline " "; + Format.force_newline (); + Format.print_flush (); +*) + [],[(position.name,prefix)] + end + else + [],[] + in + let (rest_alist,rest_gamma_0_prefixes,rest_delta_0_prefixes) = + select_atoms_treelist treelist new_prefix in + (rest_alist,(rest_gamma_0_prefixes @ gamma_0_element), + (rest_delta_0_prefixes @ delta_0_element)) + + in + match treelist with + [] -> [],[],[] + | first::rest -> + let (first_alist,first_gprefixes,first_dprefixes) = select_atoms first prefix + and (rest_alist,rest_gprefixes,rest_dprefixes) = select_atoms_treelist rest prefix in + ((first_alist @ rest_alist),(first_gprefixes @ rest_gprefixes), + (first_dprefixes @ rest_dprefixes)) + +let prepare_prover ftree = + let alist,gamma_0_prefixes,delta_0_prefixes = select_atoms_treelist [ftree] [] in + let atom_rel = compute_atomlist_relations alist ftree alist in + (atom_rel,(gamma_0_prefixes,delta_0_prefixes)) + +(* ************************ Build intial formula tree and relations *********************************** *) +(* Building a formula tree and the tree ordering from the input formula, i.e. OCaml term *) + +let make_position_name stype pos_n = + let prefix = + if List.mem stype [Phi_0;Gamma_0] + then "v" + else + if List.mem stype [Psi_0;Delta_0] + then "c" + else + "a" + in + prefix^(string_of_int pos_n) + +let dual_pol pol = + if pol = O then I else O + +let check_subst_term (variable,old_term) pos_name stype = + if (List.mem stype [Gamma_0;Delta_0]) then + let new_variable = + if stype = Gamma_0 then (mk_var_term (pos_name^"_jprover")) + else + (mk_string_term jprover_op pos_name) + in + (subst1 old_term variable new_variable) (* replace variable (non-empty) in t by pos_name *) + (* pos_name is either a variable term or a constant, f.i. a string term *) + (* !!! check unification module how handling eingenvariables as constants !!! *) + else + old_term + +let rec build_ftree (variable,old_term) pol stype address pos_n = + let pos_name = make_position_name stype pos_n in + let term = check_subst_term (variable,old_term) pos_name stype in + if JLogic.is_and_term term then + let s,t = JLogic.dest_and term in + let ptype,stype_1,stype_2 = + if pol = O + then Beta,Beta_1,Beta_2 + else + Alpha,Alpha_1,Alpha_2 + in + let position = {name=pos_name; address=address; op=And; pol=pol; pt=ptype; st=stype; label=term} in + let subtree_left,ordering_left,posn_left = build_ftree ("",s) pol stype_1 (address@[1]) (pos_n+1) in + let subtree_right,ordering_right,posn_right = build_ftree ("",t) pol stype_2 (address@[2]) + (posn_left+1) in + let (succ_left,whole_left) = List.hd ordering_left + and (succ_right,whole_right) = List.hd ordering_right in + let pos_succs = + (StringSet.add succ_left (StringSet.add succ_right (StringSet.union whole_left whole_right))) + in + (NodeA(position,[|subtree_left;subtree_right|]), + ((position.name,pos_succs)::(ordering_left @ ordering_right)), + posn_right + ) + else + if JLogic.is_or_term term then + let s,t = JLogic.dest_or term in + let ptype,stype_1,stype_2 = + if pol = O + then Alpha,Alpha_1,Alpha_2 + else + Beta,Beta_1,Beta_2 + in + let position = {name=pos_name; address=address; op=Or; pol=pol; pt=ptype; st=stype; label=term} in + let subtree_left,ordering_left,posn_left = build_ftree ("",s) pol stype_1 (address@[1]) (pos_n+1) in + let subtree_right,ordering_right,posn_right = build_ftree ("",t) pol stype_2 (address@[2]) + (posn_left+1) in + let (succ_left,whole_left) = List.hd ordering_left + and (succ_right,whole_right) = List.hd ordering_right in + let pos_succs = + StringSet.add succ_left (StringSet.add succ_right (StringSet.union whole_left whole_right)) in + (NodeA(position,[|subtree_left;subtree_right|]), + ((position.name),pos_succs) :: (ordering_left @ ordering_right), + posn_right + ) + else + if JLogic.is_implies_term term then + let s,t = JLogic.dest_implies term in + let ptype_0,stype_0,ptype,stype_1,stype_2 = + if pol = O + then Psi,Psi_0,Alpha,Alpha_1,Alpha_2 + else + Phi,Phi_0,Beta,Beta_1,Beta_2 + in + let pos2_name = make_position_name stype_0 (pos_n+1) in + let sposition = {name=pos_name; address=address; op=Imp; pol=pol; pt=ptype_0; st=stype; label=term} + and position = {name=pos2_name; address=address@[1]; op=Imp; pol=pol; pt=ptype; st=stype_0; label=term} in + let subtree_left,ordering_left,posn_left = build_ftree ("",s) (dual_pol pol) stype_1 (address@[1;1]) + (pos_n+2) in + let subtree_right,ordering_right,posn_right = build_ftree ("",t) pol stype_2 (address@[1;2]) + (posn_left+1) in + let (succ_left,whole_left) = List.hd ordering_left + and (succ_right,whole_right) = List.hd ordering_right in + let pos_succs = + StringSet.add succ_left (StringSet.add succ_right (StringSet.union whole_left whole_right)) in + let pos_ordering = (position.name,pos_succs) :: (ordering_left @ ordering_right) in + (NodeA(sposition,[|NodeA(position,[|subtree_left;subtree_right|])|]), + ((sposition.name,(StringSet.add position.name pos_succs))::pos_ordering), + posn_right + ) + else + if JLogic.is_not_term term then + let s = JLogic.dest_not term in + let ptype_0,stype_0,ptype,stype_1= + if pol = O + then Psi,Psi_0,Alpha,Alpha_1 + else + Phi,Phi_0,Alpha,Alpha_1 + in + let pos2_name = make_position_name stype_0 (pos_n+1) in + let sposition = {name=pos_name; address=address; op=Neg; pol=pol; pt=ptype_0; st=stype; label=term} + and position = {name=pos2_name; address=address@[1]; op=Neg; pol=pol; pt=ptype; st=stype_0; label=term} in + let subtree_left,ordering_left,posn_left = build_ftree ("",s) (dual_pol pol) stype_1 (address@[1;1]) + (pos_n+2) in + let (succ_left,whole_left) = List.hd ordering_left in + let pos_succs = + StringSet.add succ_left whole_left in + let pos_ordering = (position.name,pos_succs) :: ordering_left in + (NodeA(sposition,[|NodeA(position,[| subtree_left|])|]), + ((sposition.name,(StringSet.add position.name pos_succs))::pos_ordering), + posn_left + ) + else + if JLogic.is_exists_term term then + let v,s,t = JLogic.dest_exists term in (* s is type of v and will be supressed here *) + let ptype,stype_1 = + if pol = O + then Gamma,Gamma_0 + else + Delta,Delta_0 + in + let position = {name=pos_name; address=address; op=Ex; pol=pol; pt=ptype; st=stype; label=term} in + let subtree_left,ordering_left,posn_left = build_ftree (v,t) pol stype_1 (address@[1]) (pos_n+1) in + let (succ_left,whole_left) = List.hd ordering_left in + let pos_succs = + StringSet.add succ_left whole_left in + (NodeA(position,[|subtree_left|]), + ((position.name,pos_succs) :: ordering_left), + posn_left + ) + else + if JLogic.is_all_term term then + let v,s,t = JLogic.dest_all term in + (* s is type of v and will be supressed here *) + let ptype_0,stype_0,ptype,stype_1= + if pol = O + then Psi,Psi_0,Delta,Delta_0 + else + Phi,Phi_0,Gamma,Gamma_0 + in + let pos2_name = make_position_name stype_0 (pos_n+1) in + let sposition = {name=pos_name; address=address; op=All; pol=pol; pt=ptype_0; st=stype; label=term} + and position = {name=pos2_name; address=address@[1]; op=All; pol=pol; pt=ptype; st=stype_0; label=term} in + let subtree_left,ordering_left,posn_left = build_ftree (v,t) pol stype_1 (address@[1;1]) + (pos_n+2) in + let (succ_left,whole_left) = List.hd ordering_left in + let pos_succs = + StringSet.add succ_left whole_left in + let pos_ordering = (position.name,pos_succs) :: ordering_left in + (NodeA(sposition,[|NodeA(position,[|subtree_left|])|]), + ((sposition.name,(StringSet.add position.name pos_succs))::pos_ordering), + posn_left + ) + else (* finally, term is atomic *) + let ptype_0,stype_0 = + if pol = O + then Psi,Psi_0 + else + Phi,Phi_0 + in + let pos2_name = make_position_name stype_0 (pos_n+1) in + let sposition = {name=pos_name; address=address; op=At; pol=pol; pt=ptype_0; st=stype; label=term} + and position = {name=pos2_name; address=address@[1]; op=At; pol=pol; pt=PNull; st=stype_0; label=term} in + (NodeA(sposition,[|NodeAt(position)|]), + [(sposition.name,(StringSet.add position.name StringSet.empty));(position.name,StringSet.empty)], + pos_n+1 + ) + +let rec construct_ftree termlist treelist orderinglist pos_n goal = + match termlist with + [] -> + let new_root = {name="w"; address=[]; op=Null; pol=O; pt=Psi; st=PNull_0; label=goal} + and treearray = Array.of_list treelist in + NodeA(new_root,treearray),(("w",(union_orderings orderinglist))::orderinglist),pos_n + | ft::rest_terms -> + let next_address = [((List.length treelist)+1)] + and next_pol,next_goal = + if rest_terms = [] then + O,ft (* construct tree for the conclusion *) + else + I,goal + in + let new_tree,new_ordering,new_pos_n = + build_ftree ("",ft) next_pol Alpha_1 next_address (pos_n+1) in + construct_ftree rest_terms (treelist @ [new_tree]) + (orderinglist @ new_ordering) new_pos_n next_goal + +(*************************** Main LOOP ************************************) +let unprovable = RefineError ("Jprover", StringError "formula is not provable") +let mult_limit_exn = RefineError ("Jprover", StringError "multiplicity limit reached") +let coq_exn = RefineError ("Jprover", StringError "interface for coq: error on ") + +let init_prover ftree = + let atom_relation,qprefixes = prepare_prover ftree in +(* print_atom_info atom_relation; *) (* apple *) + let atom_sets = make_atom_sets atom_relation in + (atom_relation,atom_sets,qprefixes) + + +let rec try_multiplicity mult_limit ftree ordering pos_n mult logic = + try + let (atom_relation,atom_sets,qprefixes) = init_prover ftree in + let ((orderingQ,red_ordering),eqlist,unifier,ext_proof) = + path_checker atom_relation atom_sets qprefixes ordering logic in + (ftree,red_ordering,eqlist,unifier,ext_proof) (* orderingQ is not needed as return value *) + with Failed -> + match mult_limit with + Some m when m == mult -> + raise mult_limit_exn + | _ -> + let new_mult = mult+1 in + begin + Format.open_box 0; + Format.force_newline (); + Format.print_string "Multiplicity Fail: "; + Format.print_string ("Try new multiplicity "^(string_of_int new_mult)); + Format.force_newline (); + Format.print_flush (); + + let (new_ftree,new_ordering,new_pos_n) = + add_multiplicity ftree pos_n new_mult logic in + if (new_ftree = ftree) then + raise unprovable + else +(* print_formula_info new_ftree new_ordering new_pos_n; *) (* apple *) + try_multiplicity mult_limit new_ftree new_ordering new_pos_n new_mult logic + end + +let prove mult_limit termlist logic = + let (ftree,ordering,pos_n) = construct_ftree termlist [] [] 0 (mk_var_term "dummy") in +(* pos_n = number of positions without new root "w" *) +(* print_formula_info ftree ordering pos_n; *) (* apple *) + try_multiplicity mult_limit ftree ordering pos_n 1 logic + +(********** first-order type theory interface *******************) + +let rec renam_free_vars termlist = + match termlist + with [] -> [],[] + | f::r -> + let var_names = free_vars_list f in + let string_terms = + List.map (fun x -> (mk_string_term free_var_op x)) var_names + in + let mapping = List.combine var_names string_terms + and new_f = subst f var_names string_terms in + let (rest_mapping,rest_renamed) = renam_free_vars r in + let unique_mapping = remove_dups_list (mapping @ rest_mapping) in + (unique_mapping,(new_f::rest_renamed)) + +let rec apply_var_subst term var_subst_list = + match var_subst_list with + [] -> term + | (v,t)::r -> + let next_term = var_subst term t v in + apply_var_subst next_term r + +let rec make_equal_list n list_object = + if n = 0 then + [] + else + list_object::(make_equal_list (n-1) list_object) + +let rec create_output rule_list input_map = + match rule_list with + [] -> JLogic.empty_inf + | f::r -> + let (pos,(rule,term1,term2)) = f in + let delta1_names = collect_delta_terms [term1] + and delta2_names = collect_delta_terms [term2] in + let unique_deltas = remove_dups_list (delta1_names @ delta2_names) in + let delta_terms = + List.map (fun x -> (mk_string_term jprover_op x)) unique_deltas in + let delta_vars = List.map (fun x -> (x^"_jprover")) unique_deltas in + let delta_map = List.combine delta_vars delta_terms in + let var_mapping = (input_map @ delta_map) in + let frees1 = free_vars_list term1 + and frees2 = free_vars_list term2 in + let unique_object = mk_var_term "v0_jprover" in + let unique_list1 = make_equal_list (List.length frees1) unique_object + and unique_list2 = make_equal_list (List.length frees2) unique_object + in + let next_term1 = subst term1 frees1 unique_list1 + and next_term2 = subst term2 frees2 unique_list2 in + let new_term1 = apply_var_subst next_term1 var_mapping + and new_term2 = apply_var_subst next_term2 var_mapping + and (a,b) = pos + in +(*: print_string (a^"+++"^b^"\n"); :*) + +(* kick away the first argument, the position *) + (JLogic.append_inf (create_output r input_map) (b,new_term1) (a,new_term2) rule) + +let rec make_test_interface rule_list input_map = + match rule_list with + [] -> [] + | f::r -> + let (pos,(rule,term1,term2)) = f in + let delta1_names = collect_delta_terms [term1] + and delta2_names = collect_delta_terms [term2] in + let unique_deltas = remove_dups_list (delta1_names @ delta2_names) in + let delta_terms = + List.map (fun x -> (mk_string_term jprover_op x)) unique_deltas in + let delta_vars = List.map (fun x -> (x^"_jprover")) unique_deltas in + let delta_map = List.combine delta_vars delta_terms in + let var_mapping = (input_map @ delta_map) in + let frees1 = free_vars_list term1 + and frees2 = free_vars_list term2 in + let unique_object = mk_var_term "v0_jprover" in + let unique_list1 = make_equal_list (List.length frees1) unique_object + and unique_list2 = make_equal_list (List.length frees2) unique_object + in + begin +(* + print_endline ""; + print_endline ""; + print_stringlist frees1; + print_endline ""; + print_stringlist frees2; + print_endline ""; + print_endline ""; +*) + let next_term1 = subst term1 frees1 unique_list1 + and next_term2 = subst term2 frees2 unique_list2 in + let new_term1 = apply_var_subst next_term1 var_mapping + and new_term2 = apply_var_subst next_term2 var_mapping + in + (pos,(rule,new_term1,new_term2))::(make_test_interface r input_map) + end + +(**************************************************************) + +(*: modified for Coq :*) + +let decomp_pos pos = + let {name=n; address=a; label=l} = pos in + (n,(a,l)) + +let rec build_formula_id ftree = + let rec build_fid_list = function + [] -> [] + | t::rest -> (build_formula_id t)@(build_fid_list rest) + in + match ftree with + Empty -> [] + | NodeAt(position) -> + [decomp_pos position] + | NodeA(position,subtrees) -> + let tree_list = Array.to_list subtrees in + (decomp_pos position)::(build_fid_list tree_list) + +let rec encode1 = function (* normal *) + [] -> "" + | i::r -> "_"^(string_of_int i)^(encode1 r) + +let rec encode2 = function (* move up *) + [i] -> "" + | i::r -> "_"^(string_of_int i)^(encode2 r) + | _ -> raise coq_exn + +let rec encode3 = function (* move down *) + [] -> "_1" + | i::r -> "_"^(string_of_int i)^(encode3 r) + +let lookup_coq str map = + try + let (il,t) = List.assoc str map in + il + with Not_found -> raise coq_exn + +let create_coq_input inf map = + let rec rec_coq_part inf = + match inf with + [] -> [] + | (rule, (s1, t1), ((s2, t2) as k))::r -> + begin + match rule with + Andl | Andr | Orl | Orr1 | Orr2 -> + (rule, (encode1 (lookup_coq s1 map), t1), k)::(rec_coq_part r) + | Impr | Impl | Negr | Negl | Ax -> + (rule, (encode2 (lookup_coq s1 map), t1), k)::(rec_coq_part r) + | Exr -> + (rule, (encode1 (lookup_coq s1 map), t1), + (encode1 (lookup_coq s2 map), t2))::(rec_coq_part r) + | Exl -> + (rule, (encode1 (lookup_coq s1 map), t1), + (encode3 (lookup_coq s1 map), t2))::(rec_coq_part r) + | Allr | Alll -> + (rule, (encode2 (lookup_coq s1 map), t1), + (* (s2, t2))::(rec_coq_part r) *) + (encode3 (lookup_coq s1 map), t2))::(rec_coq_part r) + | _ -> raise coq_exn + end + in + rec_coq_part inf + +let gen_prover mult_limit logic calculus hyps concls = + let (input_map,renamed_termlist) = renam_free_vars (hyps @ concls) in + let (ftree,red_ordering,eqlist,(sigmaQ,sigmaJ),ext_proof) = prove mult_limit renamed_termlist logic in + let sequent_proof = reconstruct ftree red_ordering sigmaQ ext_proof logic calculus in + let (ptree,count_ax) = bproof sequent_proof in + let idl = build_formula_id ftree in +(* print_ftree ftree; apple *) + (* transform types and rename constants *) + (* we can transform the eigenvariables AFTER proof reconstruction since *) + (* new delta_0 constants may have been constructed during rule permutation *) + (* from the LJmc to the LJ proof *) + create_coq_input (create_output sequent_proof input_map) idl + +(*: end of coq modification :*) + +let prover mult_limit hyps concl = gen_prover mult_limit "J" "LJ" hyps [concl] + +(************* test with propositional proof reconstruction ************) + +let rec count_axioms seq_list = + match seq_list with + [] -> 0 + | f::r -> + let (rule,_,_) = f in + if rule = Ax then + 1 + count_axioms r + else + count_axioms r + +let do_prove mult_limit termlist logic calculus = + try begin + let (input_map,renamed_termlist) = renam_free_vars termlist in + let (ftree,red_ordering,eqlist,(sigmaQ,sigmaJ),ext_proof) = prove mult_limit renamed_termlist logic in + Format.open_box 0; + Format.force_newline (); + Format.force_newline (); + Format.print_string "Extension proof ready"; + Format.force_newline (); + Format.force_newline (); + Format.print_string ("Length of Extension proof: "^((string_of_int (List.length ext_proof)))^ + " Axioms"); + Format.force_newline (); + Format.force_newline (); + print_endline "Extension proof:"; + Format.open_box 0; + print_pairlist ext_proof; (* print list of type (string * string) list *) + Format.force_newline (); + Format.force_newline (); + Format.force_newline (); + Format.print_flush (); + Format.print_flush (); + Format.open_box 0; + print_ordering red_ordering; + Format.print_flush (); + Format.open_box 0; + Format.force_newline (); +(* ----------------------------------------------- *) + Format.open_box 0; + print_tunify sigmaJ; + Format.print_flush (); + print_endline ""; + print_endline ""; + print_sigmaQ sigmaQ; + print_endline ""; + print_endline ""; + Format.open_box 0; + let (qmax,equations) = eqlist in + print_endline ("number of quantifier domains : "^(string_of_int (qmax-1))); + print_endline ""; + print_equations equations; + Format.print_flush (); + print_endline ""; + print_endline ""; + print_endline ("Length of equations : "^((string_of_int (List.length equations)))); + print_endline ""; + print_endline ""; +(* --------------------------------------------------------- *) + Format.print_string "Break ... "; + print_endline ""; + print_endline ""; + Format.print_flush (); +(*: let _ = input_char stdin in :*) + let reconstr_proof = reconstruct ftree red_ordering sigmaQ ext_proof logic calculus in + let sequent_proof = make_test_interface reconstr_proof input_map in + Format.open_box 0; + Format.force_newline (); + Format.force_newline (); + Format.print_string "Sequent proof ready"; + Format.force_newline (); + Format.force_newline (); + Format.print_flush (); + let (ptree,count_ax) = bproof sequent_proof in + Format.open_box 0; + Format.print_string ("Length of sequent proof: "^((string_of_int count_ax))^" Axioms"); + Format.force_newline (); + Format.force_newline (); + Format.force_newline (); + Format.force_newline (); + Format.print_flush (); + tt ptree; (*: print proof tree :*) + Format.print_flush (); + print_endline ""; + print_endline "" + end with exn -> begin + print_endline "Jprover got an exception:"; + print_endline (Printexc.to_string exn) + end + +let test concl logic calculus = (* calculus should be LJmc or LJ for J, and LK for C *) + do_prove None [concl] logic calculus + +(* for sequents *) + +let seqtest list_term logic calculus = + let bterms = (dest_term list_term).term_terms in + let termlist = collect_subterms bterms in + do_prove None termlist logic calculus + +(*****************************************************************) + +end (* of struct *) diff --git a/contrib/jprover/jall.mli b/contrib/jprover/jall.mli new file mode 100644 index 000000000..1811fe59c --- /dev/null +++ b/contrib/jprover/jall.mli @@ -0,0 +1,339 @@ +(* JProver provides an efficient refiner for first-order classical + and first-order intuitionistic logic. It consists of two main parts: + a proof search procedure and a proof reconstruction procedure. + + + Proof Search + ============ + + The proof search process is based on a matrix-based (connection-based) + proof procedure, i.e.~a non-normalform extension procedure. + Besides the well-known quantifier substitution (Martelli Montanari), + a special string unifiation procedure is used in order to + efficiently compute intuitionistic rule non-permutabilities. + + + Proof Reconstruction + ==================== + + The proof reconstruction process converts machine-generated matrix proofs + into cut-free Gentzen-style sequent proofs. For classcal logic "C", + Gentzen's sequent calculus "LK" is used as target calculus. + For intuitionistic logic "J", either Gentzen's single-conclusioned sequent + calculus "LJ" or Fitting's multiply-conclusioned sequent calculus "LJmc" + can be used. All sequent claculi are implemented in a set-based formulation + in order to avoid structural rules. + + The proof reconstruction procedure combines three main procedures, depending + on the selected logics and sequent calculi. It consists of: + + 1) A uniform traversal algorithm for all logics and target sequent calculi. + This procedure converts classical (intuitionistic) matrix proofs + directly into cut-free "LK" ("LJmc" or "LJ") sequent proofs. + However, the direct construction of "LJ" proofs may fail in some cases + due to proof theoretical reasons. + + 2) A complete redundancy deletion algorithm, which integrates additional + knowledge from the proof search process into the reconstruction process. + This procedure is called by the traversal algorithms in order to avoid + search and deadlocks during proof reconstruciton. + + 3) A permutation-based proof transformation for converting "LJmc" proofs + into "LJ" proofs. + This procedure is called by-need, whenever the direct reconstruction + of "LJ" proofs from matrix proofs fails. + + + + + Literature: + ========== + + JProver system description was presented at CADE 2001: + @InProceedings{inp:Schmitt+01a, + author = "Stephan Schmitt and Lori Lorigo and Christoph Kreitz and + Alexey Nogin", + title = "{{\sf JProver}}: Integrating Connection-based Theorem + Proving into Interactive Proof Assistants", + booktitle = "International Joint Conference on Automated Reasoning", + year = "2001", + editor = "R. Gore and A. Leitsch and T. Nipkow", + volume = 2083, + series = LNAI, + pages = "421--426", + publisher = SPRINGER, + language = English, + where = OWN, + } + + The implementation of JProver is based on the following publications: + + + + Slides of PRL-seminar talks: + --------------------------- + + An Efficient Refiner for First-order Intuitionistic Logic + + http://www.cs.cornell.edu/Nuprl/PRLSeminar/PRLSeminar99_00/schmitt/feb28.html + + + An Efficient Refiner for First-order Intuitionistic Logic (Part II) + + http://www.cs.cornell.edu/Nuprl/PRLSeminar/PRLSeminar99_00/schmitt/may22.html + + + + Proof search: + ------------- + + +[1] + @InProceedings{inp:OttenKreitz96b, + author = "J.~Otten and C.~Kreitz", + title = "A uniform proof procedure for classical and + non-classical logics", + booktitle = "Proceedings of the 20$^{th}$ German Annual Conference on + Artificial Intelligence", + year = "1996", + editor = "G.~G{\"o}rz and S.~H{\"o}lldobler", + number = "1137", + series = LNAI, + pages = "307--319", + publisher = SPRINGER + } + + +[2] + @Article{ar:KreitzOtten99, + author = "C.~Kreitz and J.~Otten", + title = "Connection-based theorem proving in classical and + non-classical logics", + journal = "Journal for Universal Computer Science, + Special Issue on Integration of Deductive Systems", + year = "1999", + volume = "5", + number = "3", + pages = "88--112" + } + + + + + Special string unifiation procedure: + ------------------------------------ + + +[3] + @InProceedings{inp:OttenKreitz96a, + author = "J.~Otten and C.~Kreitz", + titl = "T-string-unification: unifying prefixes in + non-classical proof methods", + booktitle = "Proceedings of the 5$^{th}$ Workshop on Theorem Proving + with Analytic Tableaux and Related Methods", + year = 1996, + editor = "U.~Moscato", + number = "1071", + series = LNAI, + pages = "244--260", + publisher = SPRINGER, + month = "May " + } + + + + Proof reconstruction: Uniform traversal algorithm + ------------------------------------------------- + + +[4] + @InProceedings{inp:SchmittKreitz96a, + author = "S.~Schmitt and C.~Kreitz", + title = "Converting non-classical matrix proofs into + sequent-style systems", + booktitle = "Proceedings of the 13$^t{}^h$ Conference on + Automated Deduction", + editor = M.~A.~McRobbie and J.~K.~Slaney", + number = "1104", + series = LNAI, + pages = "418--432", + year = "1996", + publisher = SPRINGER, + month = "July/August" + } + + +[5] + @Article{ar:KreitzSchmitt00, + author = "C.~Kreitz and S.~Schmitt", + title = "A uniform procedure for converting matrix proofs + into sequent-style systems", + journal = "Journal of Information and Computation", + year = "2000", + note = "(to appear)" + } + + +[6] + @Book{bo:Schmitt00, + author = "S.~Schmitt", + title = "Proof reconstruction in classical and non-classical logics", + year = "2000", + publisher = "Infix", + series = "Dissertationen zur K{\"u}nstlichen Intelleigenz", + number = "(to appear)", + note = "(Ph.{D}.~{T}hesis, Technische Universit{\"a}t Darmstadt, + FG Intellektik, Germany, 1999)" + } + + The traversal algorithm is presented in the Chapters 2 and 3 of my thesis. + The thesis will be made available for the Department through Christoph Kreitz, + Upson 4159, kreitz@cs.cornell.edu + + + + + Proof reconstruction: Complete redundancy deletion + -------------------------------------------------- + + +[7] + @Book{bo:Schmitt00, + author = "S.~Schmitt", + title = "Proof reconstruction in classical and non-classical logics", + year = "2000", + publisher = "Infix", + series = "Dissertationen zur K{\"u}nstlichen Intelleigenz", + note = "(Ph.{D}.~{T}hesis, Technische Universit{\"a}t Darmstadt, + FG Intellektik, Germany, 1999)" + note = "(to appear)", + + } + + The integration of proof knowledge and complete redundancy deletion is presented + in Chapter 4 of my thesis. + + +[8] + @InProceedings{inp:Schmitt00, + author = "S.~Schmitt", + title = "A tableau-like representation framework for efficient + proof reconstruction", + booktitle = "Proceedings of the International Conference on Theorem Proving + with Analytic Tableaux and Related Methods", + year = "2000", + series = LNAI, + publisher = SPRINGER, + month = "June" + note = "(to appear)", + } + + + + + Proof Reconstruction: Permutation-based poof transformations "LJ" -> "LJmc" + --------------------------------------------------------------------------- + + +[9] + @InProceedings{inp:EglySchmitt98, + author = "U.~Egly and S.~Schmitt", + title = "Intuitionistic proof transformations and their + application to constructive program synthesis", + booktitle = "Proceedings of the 4$^{th}$ International Conference + on Artificial Intelligence and Symbolic Computation", + year = "1998", + editor = "J.~Calmet and J.~Plaza", + number = "1476", + series = LNAI, + pages = "132--144", + publisher = SPRINGER, + month = "September" + } + + +[10] + @Article{ar:EglySchmitt99, + author = "U.~Egly and S.~Schmitt", + title = "On intuitionistic proof transformations, their + complexity, and application to constructive program synthesis", + journal = "Fundamenta Informaticae, + Special Issue: Symbolic Computation and Artificial Intelligence", + year = "1999", + volume = "39", + number = "1--2", + pages = "59--83" + } +*) + +(*: open Refiner.Refiner +open Refiner.Refiner.Term +open Refiner.Refiner.TermType +open Refiner.Refiner.TermSubst + +open Jlogic_sig +:*) + +open Jterm +open Opname +open Jlogic + +val ruletable : rule -> string + +module JProver(JLogic: JLogicSig) : +sig + val test : term -> string -> string -> unit + + (* Procedure call: test conclusion logic calculus + + test is applied to a first-order formula. The output is some + formatted sequent proof for test / debugging purposes. + + The arguments for test are as follows: + + logic = "C"|"J" + i.e. first-order classical logic or first-order intuitionistic logic + + calculus = "LK"|"LJ"|"LJmc" + i.e. "LK" for classical logic "C", and either Gentzen's single conclusioned + calculus "LJ" or Fittings multiply-conclusioned calculus "LJmc" for + intuitionistic logic "J". + + term = first-order formula representing the proof goal. + *) + + + + val seqtest : term -> string -> string -> unit + + (* seqtest procedure is for debugging purposes only *) + + + val gen_prover : int option -> string -> string -> term list -> term list -> JLogic.inference + + (* Procedure call: gen_prover mult_limit logic calculus hypothesis conclusion + + The arguments for gen_prover are as follows: + + mult_limit - maximal multiplicity to try, None for unlimited + + logic = same as in test + + calculus = same as in test + + hypothesis = list of first-order terms forming the antecedent of the input sequent + + conclusion = list of first-order terms forming the succedent of the input sequent + This list should contain only one element if logic = "J" and calculus = "LJ". + *) + + + val prover : int option -> term list -> term -> JLogic.inference + + (* Procedure call: gen_prover mult_limit "J" "LJ" hyps [concl] + + prover provides the first-order refiner for NuPRL, using + a single concluisoned succedent [concl] in the sequent. + The result is a sequent proof in the single-conclusioned calculus "LJ". + *) +end diff --git a/contrib/jprover/jlogic.ml b/contrib/jprover/jlogic.ml new file mode 100644 index 000000000..c074e93e6 --- /dev/null +++ b/contrib/jprover/jlogic.ml @@ -0,0 +1,106 @@ +open Opname +open Jterm + +type rule = + | Ax | Andr | Andl | Orr | Orr1 | Orr2 | Orl | Impr | Impl | Negr | Negl + | Allr | Alll| Exr | Exl | Fail | Falsel | Truer + +let ruletable = function + | Fail -> "Fail" + | Ax -> "Ax" + | Negl -> "Negl" + | Negr -> "Negr" + | Andl -> "Andl" + | Andr -> "Andr" + | Orl -> "Orl" + | Orr -> "Orr" + | Orr1 -> "Orr1" + | Orr2 -> "Orr2" + | Impl -> "Impl" + | Impr -> "Impr" + | Exl -> "Exl" + | Exr -> "Exr" + | Alll -> "Alll" + | Allr -> "Allr" + | Falsel -> "Falsel" + | Truer -> "Truer" + +module type JLogicSig = +sig + (* understanding the input *) + val is_all_term : term -> bool + val dest_all : term -> string * term * term + val is_exists_term : term -> bool + val dest_exists : term -> string * term * term + val is_and_term : term -> bool + val dest_and : term -> term * term + val is_or_term : term -> bool + val dest_or : term -> term * term + val is_implies_term : term -> bool + val dest_implies : term -> term * term + val is_not_term : term -> bool + val dest_not : term -> term + + (* processing the output *) + type inf_step = rule * (string * term) * (string * term) + type inference = inf_step list +(* type inference *) + val empty_inf : inference + val append_inf : inference -> (string * term) -> (string * term) -> rule -> inference + val print_inf : inference -> unit +end;; + +(* Copy from [term_op_std.ml]: *) + + let rec print_address int_list = + match int_list with + | [] -> + Format.print_string "" + | hd::rest -> + begin + Format.print_int hd; + print_address rest + end + +module JLogic: JLogicSig = +struct + let is_all_term = Jterm.is_all_term + let dest_all = Jterm.dest_all + let is_exists_term = Jterm.is_exists_term + let dest_exists = Jterm.dest_exists + let is_and_term = Jterm.is_and_term + let dest_and = Jterm.dest_and + let is_or_term = Jterm.is_or_term + let dest_or = Jterm.dest_or + let is_implies_term = Jterm.is_implies_term + let dest_implies = Jterm.dest_implies + let is_not_term = Jterm.is_not_term + let dest_not = Jterm.dest_not + + type inf_step = rule * (string * term) * (string * term) + type inference = inf_step list + + let empty_inf = [] + let append_inf inf t1 t2 rule = + (rule, t1, t2)::inf + + let rec print_inf inf = + match inf with + | [] -> print_string "."; Format.print_flush () + | (rule, (n1,t1), (n2,t2))::d -> + print_string (ruletable rule); + print_string (":("^n1^":"); + print_term stdout t1; + print_string (","^n2^":"); + print_term stdout t2; + print_string ")\n"; + print_inf d +end;; + +let show_loading s = print_string s +type my_Debug = { mutable debug_name: string; + mutable debug_description: string; + debug_value: bool + } + +let create_debug x = ref false diff --git a/contrib/jprover/jlogic.mli b/contrib/jprover/jlogic.mli new file mode 100644 index 000000000..a90797911 --- /dev/null +++ b/contrib/jprover/jlogic.mli @@ -0,0 +1,40 @@ +(* The interface to manipulate [jterms], which is + extracted and modified from Meta-Prl. *) + +type rule = + Ax | Andr | Andl | Orr | Orr1 | Orr2 | Orl | Impr | Impl | Negr | Negl + | Allr | Alll| Exr | Exl | Fail | Falsel | Truer + +module type JLogicSig = + sig + val is_all_term : Jterm.term -> bool + val dest_all : Jterm.term -> string * Jterm.term * Jterm.term + val is_exists_term : Jterm.term -> bool + val dest_exists : Jterm.term -> string * Jterm.term * Jterm.term + val is_and_term : Jterm.term -> bool + val dest_and : Jterm.term -> Jterm.term * Jterm.term + val is_or_term : Jterm.term -> bool + val dest_or : Jterm.term -> Jterm.term * Jterm.term + val is_implies_term : Jterm.term -> bool + val dest_implies : Jterm.term -> Jterm.term * Jterm.term + val is_not_term : Jterm.term -> bool + val dest_not : Jterm.term -> Jterm.term + type inf_step = rule * (string * Jterm.term) * (string * Jterm.term) + type inference = inf_step list + val empty_inf : inference + val append_inf : + inference -> (string * Jterm.term) -> (string * Jterm.term) -> rule -> inference + val print_inf : inference -> unit + end + +module JLogic : JLogicSig + +val show_loading : string -> unit + +type my_Debug = { + mutable debug_name : string; + mutable debug_description : string; + debug_value : bool; +} +val create_debug : 'a -> bool ref +val ruletable : rule -> string diff --git a/contrib/jprover/jprover.ml b/contrib/jprover/jprover.ml new file mode 100644 index 000000000..fd98f20e6 --- /dev/null +++ b/contrib/jprover/jprover.ml @@ -0,0 +1,513 @@ +open Jlogic + +module JA = Jall +module JT = Jterm +module T = Tactics +module TCL = Tacticals +module TM = Tacmach +module N = Names +module PT = Proof_type +module TE = Tacentries +module PA = Pattern +module HP = Hipattern +module TR = Term +module PR = Printer +module RO = Reductionops +module UT = Util + +module J=JA.JProver(JLogic) (* the JProver *) + +(*i +module NO = Nameops +module TO = Termops +module RE = Reduction +module CL = Coqlib +module ID = Inductiveops +module CV = Clenv +module RF = Refiner +i*) + +(* Interface to JProver: *) +(* type JLogic.inf_step = rule * (string * Jterm.term) * (string * Jterm.term) *) +type jp_inf_step = JLogic.inf_step +type jp_inference = JLogic.inference (* simply a list of [inf_step] *) + +(* Definitions for rebuilding proof tree from JProver: *) +(* leaf, one-branch, two-branch, two-branch, true, false *) +type jpbranch = JP0 | JP1 | JP2 | JP2' | JPT | JPF +type jptree = | JPempty (* empty tree *) + | JPAx of jp_inf_step (* Axiom node *) + | JPA of jp_inf_step * jptree + | JPB of jp_inf_step * jptree * jptree + +(* Private debugging tools: *) +(*i*) +let mbreak s = Format.print_flush (); print_string ("-break at: "^s); + Format.print_flush (); let _ = input_char stdin in () +(*i*) +let jp_error re = raise (JT.RefineError ("jprover", JT.StringError re)) + +(* print Coq constructor *) +let print_constr ct = Pp.ppnl (PR.prterm ct); Format.print_flush () + +let rec print_constr_list = function + | [] -> () + | ct::r -> print_constr ct; print_constr_list r + +let print_constr_pair op c1 c2 = + print_string (op^"("); + print_constr c1; + print_string ","; + print_constr c2; + print_string ")\n" + + +(* Parsing modules for Coq: *) +(* [is_coq_???] : testing functions *) +(* [dest_coq_???] : destructors *) + +let is_coq_true = HP.is_unit_type + +let is_coq_false = HP.is_empty_type + +(* return two subterms *) +let dest_coq_and ct = + match (HP.match_with_conjunction ct) with + | Some (hdapp,args) -> +(*i print_constr hdapp; print_constr_list args; i*) + begin + match args with + | s1::s2::[] -> +(*i print_constr_pair "and" s1 s2; i*) + (s1,s2) + | _ -> jp_error "dest_coq_and" + end + | None -> jp_error "dest_coq_and" + +let is_coq_or = HP.is_disjunction + +(* return two subterms *) +let dest_coq_or ct = + match (HP.match_with_disjunction ct) with + | Some (hdapp,args) -> +(*i print_constr hdapp; print_constr_list args; i*) + begin + match args with + | s1::s2::[] -> +(*i print_constr_pair "or" s1 s2; i*) + (s1,s2) + | _ -> jp_error "dest_coq_or" + end + | None -> jp_error "dest_coq_or" + +let is_coq_not = HP.is_nottype + +let dest_coq_not ct = + match (HP.match_with_nottype ct) with + | Some (hdapp,arg) -> +(*i print_constr hdapp; print_constr args; i*) +(*i print_string "not "; + print_constr arg; i*) + arg + | None -> jp_error "dest_coq_not" + + +let is_coq_impl ct = + match TR.kind_of_term ct with + | TR.Prod (_,_,b) -> (not (Termops.dependent (TR.mkRel 1) b)) + | _ -> false + + +let dest_coq_impl c = + match TR.kind_of_term c with + | TR.Prod (_,b,c) -> +(*i print_constr_pair "impl" b c; i*) + (b, c) + | _ -> jp_error "dest_coq_impl" + +(* provide new variables for renaming of universal variables *) +let new_counter = + let ctr = ref 0 in + fun () -> incr ctr;!ctr + +(* provide new symbol name for unknown Coq constructors *) +let new_ecounter = + let ectr = ref 0 in + fun () -> incr ectr;!ectr + +let is_coq_forall ct = + match TR.kind_of_term (RO.whd_betaiota ct) with + | TR.Prod (_,_,b) -> Termops.dependent (TR.mkRel 1) b + | _ -> false + +(* return the bounded variable (as a string) and the bounded term *) +let dest_coq_forall ct = + match TR.kind_of_term (RO.whd_betaiota ct) with + | TR.Prod (_,_,b) -> + let x ="jp_"^(string_of_int (new_counter())) in + let v = TR.mkVar (N.id_of_string x) in + let c = TR.subst1 v b in (* substitute de Bruijn variable by [v] *) +(*i print_constr_pair "forall" v c; i*) + (x, c) + | _ -> jp_error "dest_coq_forall" + + +(* Apply [ct] to [t]: *) +let sAPP ct t = + match TR.kind_of_term (RO.whd_betaiota ct) with + | TR.Prod (_,_,b) -> + let c = TR.subst1 t b in + c + | _ -> jp_error "sAPP" + + +let is_coq_exists ct = + if not (HP.is_conjunction ct) then false + else let (hdapp,args) = TR.decompose_app ct in + match args with + | _::la::[] -> + begin + try + match TR.destLambda la with + | (N.Name _,_,_) -> true + | _ -> false + with _ -> false + end + | _ -> false + +(* return the bounded variable (as a string) and the bounded term *) +let dest_coq_exists ct = + let (hdapp,args) = TR.decompose_app ct in + match args with + | _::la::[] -> + begin + try + match TR.destLambda la with + | (N.Name x,t1,t2) -> + let v = TR.mkVar x in + let t3 = TR.subst1 v t2 in +(*i print_constr_pair "exists" v t3; i*) + (N.string_of_id x, t3) + | _ -> jp_error "dest_coq_exists" + with _ -> jp_error "dest_coq_exists" + end + | _ -> jp_error "dest_coq_exists" + + +let is_coq_and ct = + if (HP.is_conjunction ct) && not (is_coq_exists ct) + && not (is_coq_true ct) then true + else false + + +(* Parsing modules: *) + +let jtbl = Hashtbl.create 53 (* associate for unknown Coq constr. *) +let rtbl = Hashtbl.create 53 (* reverse table of [jtbl] *) + +let dest_coq_symb ct = + N.string_of_id (TR.destVar ct) + +(* provide new names for unknown Coq constr. *) +(* [ct] is the unknown constr., string [s] is appended to the name encoding *) +let create_coq_name ct s = + try + Hashtbl.find jtbl ct + with Not_found -> + let t = ("jp_"^s^(string_of_int (new_ecounter()))) in + Hashtbl.add jtbl ct t; + Hashtbl.add rtbl t ct; + t + +let dest_coq_app ct = + let (hd, args) = TR.decompose_app ct in +(*i print_constr hd; + print_constr_list args; i*) + if TR.isVar hd then + (dest_coq_symb hd, args) + else (* unknown constr *) + (create_coq_name hd "P_", args) + +let rec parsing2 c = (* for function symbols, variables, constants *) + if (TR.isApp c) then (* function symbol? *) + let (f,args) = dest_coq_app c in + JT.fun_ f (List.map parsing2 args) + else if TR.isVar c then (* identifiable variable or constant *) + JT.var_ (dest_coq_symb c) + else (* unknown constr *) + JT.var_ (create_coq_name c "var_") + +(* the main parsing function *) +let rec parsing c = + let ct = Reduction.whd_betadeltaiota (Global.env ()) c in + if is_coq_true ct then + JT.true_ + else if is_coq_false ct then + JT.false_ + else if is_coq_not ct then + JT.not_ (parsing (dest_coq_not ct)) + else if is_coq_impl ct then + let (t1,t2) = dest_coq_impl ct in + JT.imp_ (parsing t1) (parsing t2) + else if is_coq_or ct then + let (t1,t2) = dest_coq_or ct in + JT.or_ (parsing t1) (parsing t2) + else if is_coq_and ct then + let (t1,t2) = dest_coq_and ct in + JT.and_ (parsing t1) (parsing t2) + else if is_coq_forall ct then + let (v,t) = dest_coq_forall ct in + JT.forall v (parsing t) + else if is_coq_exists ct then + let (v,t) = dest_coq_exists ct in + JT.exists v (parsing t) + else if TR.isApp ct then (* predicate symbol with arguments *) + let (p,args) = dest_coq_app ct in + JT.pred_ p (List.map parsing2 args) + else if TR.isVar ct then (* predicate symbol without arguments *) + let p = dest_coq_symb ct in + JT.pred_ p [] + else (* unknown predicate *) + JT.pred_ (create_coq_name ct "Q_") [] + +(*i + print_string "??";print_constr ct; + JT.const_ ("err_"^(string_of_int (new_ecounter()))) +i*) + + +(* Translate JProver terms into Coq constructors: *) +(* The idea is to retrieve it from [rtbl] if it exists indeed, otherwise + create one. *) +let rec constr_of_jterm t = + if (JT.is_var_term t) then (* a variable *) + let v = JT.dest_var t in + try + Hashtbl.find rtbl v + with Not_found -> TR.mkVar (N.id_of_string v) + else if (JT.is_fun_term t) then (* a function symbol *) + let (f,ts) = JT.dest_fun t in + let f' = try Hashtbl.find rtbl f with Not_found -> TR.mkVar (N.id_of_string f) in + TR.mkApp (f', Array.of_list (List.map constr_of_jterm ts)) + else jp_error "constr_of_jterm" + + +(* Coq tactics for Sequent Calculus LJ: *) +(* Note that for left-rule a name indicating the being applied rule + in Coq's Hints is required; for right-rule a name is also needed + if it will pass some subterm to the left-hand side. + However, all of these can be computed by the path [id] of the being + applied rule. +*) + +(* and-right *) +let dyn_andr = + T.split [] + +(* For example, the following implements the [and-left] rule: *) +let dyn_andl id = (* [id1]: left child; [id2]: right child *) + let id1 = (N.id_of_string (id^"_1")) and id2 = (N.id_of_string (id^"_2")) in + (TCL.tclTHEN (T.simplest_elim (TR.mkVar (N.id_of_string id))) (T.intros_using [id1;id2])) + +let dyn_orr1 = + T.left [] + +let dyn_orr2 = + T.right [] + +let dyn_orl id = + let id1 = (N.id_of_string (id^"_1")) and id2 = (N.id_of_string (id^"_2")) in + (TCL.tclTHENS (T.simplest_elim (TR.mkVar (N.id_of_string id))) + [T.intro_using id1; T.intro_using id2]) + +let dyn_negr id = + let id1 = id^"_1_1" in + TE.v_intro [PT.Identifier (N.id_of_string id1)] + +let dyn_negl id = + T.simplest_elim (TR.mkVar (N.id_of_string id)) + +let dyn_impr id = + let id1 = id^"_1_1" in + TE.v_intro [PT.Identifier (N.id_of_string id1)] + +let dyn_impl id gl = + let t = TM.pf_get_hyp_typ gl (N.id_of_string id) in + let (_,b) = dest_coq_impl t in + let id2 = (N.id_of_string (id^"_1_2")) in + (TCL.tclTHENL (TCL.tclTHENS (T.cut b) [T.intro_using id2;TCL.tclIDTAC]) + (T.apply_term (TR.mkVar (N.id_of_string id)) + [TR.mkMeta (Clenv.new_meta())])) gl + +let dyn_allr c = (* [c] must be an eigenvariable which replaces [v] *) + TE.v_intro [PT.Identifier (N.id_of_string c)] + +(* [id2] is the path of the instantiated term for [id]*) +let dyn_alll id id2 t gl = + let id' = N.id_of_string id in + let id2' = N.id_of_string id2 in + let ct = TM.pf_get_hyp_typ gl id' in + let ta = sAPP ct t in + TCL.tclTHENS (T.cut ta) [T.intro_using id2'; T.apply (TR.mkVar id')] gl + +let dyn_exl id id2 c = (* [c] must be an eigenvariable *) + (TCL.tclTHEN (T.simplest_elim (TR.mkVar (N.id_of_string id))) + (T.intros_using [(N.id_of_string c);(N.id_of_string id2)])) + +let dyn_exr t = + T.one_constructor 1 [(PT.Com,t)] + +let dyn_falsel = dyn_negl + +let dyn_truer = + T.one_constructor 1 [] + +(* Do the proof by the guidance of JProver. *) + +let do_one_step inf = + let (rule, (s1, t1), ((s2, t2) as k)) = inf in + begin +(*i if not (Jterm.is_xnil_term t2) then + begin + print_string "1: "; JT.print_term stdout t2; print_string "\n"; + print_string "2: "; print_constr (constr_of_jterm t2); print_string "\n"; + end; +i*) + match rule with + | Andl -> dyn_andl s1 + | Andr -> dyn_andr + | Orl -> dyn_orl s1 + | Orr1 -> dyn_orr1 + | Orr2 -> dyn_orr2 + | Impr -> dyn_impr s1 + | Impl -> dyn_impl s1 + | Negr -> dyn_negr s1 + | Negl -> dyn_negl s1 + | Allr -> dyn_allr (JT.dest_var t2) + | Alll -> dyn_alll s1 s2 (constr_of_jterm t2) + | Exr -> dyn_exr (constr_of_jterm t2) + | Exl -> dyn_exl s1 s2 (JT.dest_var t2) + | Ax -> T.assumption (*i TCL.tclIDTAC i*) + | Truer -> dyn_truer + | Falsel -> dyn_falsel s1 + | _ -> jp_error "do_one_step" + (* this is impossible *) + end +;; + +(* Parameter [tr] is the reconstucted proof tree from output of JProver. *) +let do_coq_proof tr = + let rec rec_do trs = + match trs with + | JPempty -> TCL.tclIDTAC + | JPAx h -> do_one_step h + | JPA (h, t) -> TCL.tclTHEN (do_one_step h) (rec_do t) + | JPB (h, left, right) -> TCL.tclTHENS (do_one_step h) [rec_do left; rec_do right] + in + rec_do tr + + +(* Rebuild the proof tree from the output of JProver: *) + +(* Since some universal variables are not necessarily first-order, + lazy substitution may happen. They are recorded in [rtbl]. *) +let reg_unif_subst t1 t2 = + let (v,_,_) = JT.dest_all t1 in + Hashtbl.add rtbl v (TR.mkVar (N.id_of_string (JT.dest_var t2))) + +let count_jpbranch one_inf = + let (rule, (_, t1), (_, t2)) = one_inf in + begin + match rule with + | Ax -> JP0 + | Orr1 | Orr2 | Negl | Impr | Alll | Exr | Exl -> JP1 + | Andr | Orl -> JP2 + | Negr -> if (JT.is_true_term t1) then JPT else JP1 + | Andl -> if (JT.is_false_term t1) then JPF else JP1 + | Impl -> JP2' (* reverse the sons of [Impl] since [dyn_impl] reverses them *) + | Allr -> reg_unif_subst t1 t2; JP1 + | _ -> jp_error "count_jpbranch" + end + +let replace_by r = function + (rule, a, b) -> (r, a, b) + +let rec build_jptree inf = + match inf with + | [] -> ([], JPempty) + | h::r -> + begin + match count_jpbranch h with + | JP0 -> (r,JPAx h) + | JP1 -> let (r1,left) = build_jptree r in + (r1, JPA(h, left)) + | JP2 -> let (r1,left) = build_jptree r in + let (r2,right) = build_jptree r1 in + (r2, JPB(h, left, right)) + | JP2' -> let (r1,left) = build_jptree r in (* for [Impl] *) + let (r2,right) = build_jptree r1 in + (r2, JPB(h, right, left)) + | JPT -> let (r1,left) = build_jptree r in (* right True *) + (r1, JPAx (replace_by Truer h)) + | JPF -> let (r1,left) = build_jptree r in (* left False *) + (r1, JPAx (replace_by Falsel h)) + end + + +(* The main function: *) +(* [limits] is the multiplicity limit. *) +let jp limits gls = + let concl = TM.pf_concl gls in + let ct = concl in +(*i print_constr ct; i*) + Hashtbl.clear jtbl; (* empty the hash tables *) + Hashtbl.clear rtbl; + let t = parsing ct in +(*i JT.print_term stdout t; i*) + try + let p = (J.prover limits [] t) in +(*i print_string "\n"; + JLogic.print_inf p; i*) + let (il,tr) = build_jptree p in + if (il = []) then + begin + print_string "Proof is built.\n"; + do_coq_proof tr gls + end + else UT.error "Cannot reconstruct proof tree from JProver." + with e -> print_string "JProver fails to prove this:\n"; + JT.print_error_msg e; + UT.error "JProver terminated." + +(* an unfailed generalization procedure *) +let rec unfail_gen = function + | [] -> TCL.tclIDTAC + | h::r -> + TCL.tclTHEN + (TCL.tclORELSE (T.generalize [h]) (TCL.tclIDTAC)) + (unfail_gen r) + +(* no argument, which stands for no multiplicity limit *) +let dyn_jp l gls = + assert (l = []); + let ls = List.map (fst) (List.rev (TM.pf_hyps_types gls)) in +(*i T.generalize (List.map TR.mkVar ls) gls i*) + (* generalize the context *) + TCL.tclTHEN (TCL.tclTRY T.red_in_concl) + (TCL.tclTHEN (unfail_gen (List.map TR.mkVar ls)) + (jp None)) gls + +(* one integer argument for the multiplicity *) +let dyn_jpn l gls = + match l with + | [PT.Integer n] -> + let ls = List.map (fst) (List.rev (TM.pf_hyps_types gls)) in + TCL.tclTHEN (TCL.tclTRY T.red_in_concl) + (TCL.tclTHEN (unfail_gen (List.map TR.mkVar ls)) + (jp (Some n))) gls + | _ -> jp_error "Impossible!!!" + + +let h_jp = TM.hide_tactic "Jp" dyn_jp + +let h_jpn = TM.hide_tactic "Jpn" dyn_jpn diff --git a/contrib/jprover/jterm.ml b/contrib/jprover/jterm.ml new file mode 100644 index 000000000..7fc923a56 --- /dev/null +++ b/contrib/jprover/jterm.ml @@ -0,0 +1,872 @@ +open Printf +open Opname +open List + +(* Definitions of [jterm]: *) +type param = param' + and operator = operator' + and term = term' + and bound_term = bound_term' + and param' = + | Number of int + | String of string + | Token of string + | Var of string + | ParamList of param list + and operator' = { op_name : opname; op_params : param list } + and term' = { term_op : operator; term_terms : bound_term list } + and bound_term' = { bvars : string list; bterm : term } +;; + +(* Debugging tools: *) +(*i*) +let mbreak s = Format.print_flush (); print_string ("-break at: "^s); + Format.print_flush (); let _ = input_char stdin in () +(*i*) + +type error_msg = + | TermMatchError of term * string + | StringError of string + +exception RefineError of string * error_msg + +let ref_raise = function + | RefineError(s,e) -> raise (RefineError(s,e)) + | _ -> raise (RefineError ("Jterm", StringError "unexpected error")) + +(* Printing utilities: *) + +let fprint_str ostream s = + let _ = fprintf ostream "%s." s in ostream + +let fprint_str_list ostream sl = + ignore (List.fold_left fprint_str ostream sl); + Format.print_flush () + +let fprint_opname ostream = function + { opname_token= tk; opname_name = sl } -> + fprint_str_list ostream sl + +let rec fprint_param ostream = function + | Number n -> fprintf ostream " %d " n + | String s -> fprint_str_list ostream [s] + | Token t -> fprint_str_list ostream [t] + | Var v -> fprint_str_list ostream [v] + | ParamList ps -> fprint_param_list ostream ps +and fprint_param_list ostream = function + | [] -> () + | param::r -> fprint_param ostream param; + fprint_param_list ostream r +;; + +let print_strs = fprint_str_list stdout + + +(* Interface to [Jall.ml]: *) +(* It is extracted from Meta-Prl's standard implementation. *) +(*c begin of the extraction *) + +type term_subst = (string * term) list +let mk_term op bterms = { term_op = op; term_terms = bterms } +let make_term x = x (* external [make_term : term' -> term] = "%identity" *) +let dest_term x = x (* external [dest_term : term -> term'] = "%identity" *) +let mk_op name params = + { op_name = name; op_params = params } + +let make_op x = x (* external [make_op : operator' -> operator] = "%identity" *) +let dest_op x = x (* external [dest_op : operator -> operator'] = "%identity" *) +let mk_bterm bvars term = { bvars = bvars; bterm = term } +let make_bterm x = x (* external [make_bterm : bound_term' -> bound_term] = "%identity" *) +let dest_bterm x = x (* external [dest_bterm : bound_term -> bound_term'] = "%identity" *) +let make_param x = x (* external [make_param : param' -> param] = "%identity" *) +let dest_param x = x (* external [dest_param : param -> param'] = "%identity" *) + +(* + * Operator names. + *) +let opname_of_term = function + { term_op = { op_name = name } } -> + name + +(* + * Get the subterms. + * None of the subterms should be bound. + *) +let subterms_of_term t = + List.map (fun { bterm = t } -> t) t.term_terms + +let subterm_count { term_terms = terms } = + List.length terms + +let subterm_arities { term_terms = terms } = + List.map (fun { bvars = vars } -> List.length vars) terms + +(* + * Manifest terms are injected into the "perv" module. + *) +let xperv = make_opname ["Perv"] +let sequent_opname = mk_opname "sequent" xperv + +(* + * Variables. + *) + +let var_opname = make_opname ["var"] + +(* + * See if a term is a variable. + *) +let is_var_term = function + | { term_op = { op_name = opname; op_params = [Var v] }; + term_terms = [] + } when Opname.eq opname var_opname -> true + | _ -> + false + +(* + * Destructor for a variable. + *) +let dest_var = function + | { term_op = { op_name = opname; op_params = [Var v] }; + term_terms = [] + } when Opname.eq opname var_opname -> v + | t -> + ref_raise(RefineError ("dest_var", TermMatchError (t, "not a variable"))) +(* + * Make a variable. + *) +let mk_var_term v = + { term_op = { op_name = var_opname; op_params = [Var v] }; + term_terms = [] + } + +(* + * Simple terms + *) +(* + * "Simple" terms have no parameters and no binding variables. + *) +let is_simple_term_opname name = function + | { term_op = { op_name = name'; op_params = [] }; + term_terms = bterms + } when Opname.eq name' name -> + let rec aux = function + | { bvars = []; bterm = _ }::t -> aux t + | _::t -> false + | [] -> true + in + aux bterms + | _ -> false + +let mk_any_term op terms = + let aux t = + { bvars = []; bterm = t } + in + { term_op = op; term_terms = List.map aux terms } + +let mk_simple_term name terms = + mk_any_term { op_name = name; op_params = [] } terms + +let dest_simple_term = function + | ({ term_op = { op_name = name; op_params = [] }; + term_terms = bterms + } : term) as t -> + let aux = function + | { bvars = []; bterm = t } -> + t + | _ -> + ref_raise(RefineError ("dest_simple_term", TermMatchError (t, "binding vars exist"))) + in + name, List.map aux bterms + | t -> + ref_raise(RefineError ("dest_simple_term", TermMatchError (t, "params exist"))) + +let dest_simple_term_opname name = function + | ({ term_op = { op_name = name'; op_params = [] }; + term_terms = bterms + } : term) as t -> + if Opname.eq name name' then + let aux = function + | { bvars = []; bterm = t } -> t + | _ -> ref_raise(RefineError ("dest_simple_term_opname", TermMatchError (t, "binding vars exist"))) + in + List.map aux bterms + else + ref_raise(RefineError ("dest_simple_term_opname", TermMatchError (t, "opname mismatch"))) + | t -> + ref_raise(RefineError ("dest_simple_term_opname", TermMatchError (t, "params exist"))) + +(* + * Bound terms. + *) +let mk_simple_bterm bterm = + { bvars = []; bterm = bterm } + +let dest_simple_bterm = function + | { bvars = []; bterm = bterm } -> + bterm + | _ -> + ref_raise(RefineError ("dest_simple_bterm", StringError ("bterm is not simple"))) + +(* Copy from [term_op_std.ml]: *) +(*i modified for Jprover, as a patch... i*) +let mk_string_term opname s = + { term_op = { op_name = opname; op_params = [String s] }; term_terms = [] } + +(*i let mk_string_term opname s = + let new_opname={opname_token=opname.opname_token; opname_name=(List.tl opname.opname_name)@[s]} in + { term_op = { op_name = new_opname; op_params = [String (List.hd opname.opname_name)] }; term_terms = [] } +i*) + +(* Copy from [term_subst_std.ml]: *) + +let rec free_vars_term gvars bvars = function + | { term_op = { op_name = opname; op_params = [Var v] }; term_terms = bterms } when Opname.eq opname var_opname -> + (* This is a variable *) + let gvars' = + if List.mem v bvars or List.mem v gvars then + gvars + else + v::gvars + in + free_vars_bterms gvars' bvars bterms + | { term_terms = bterms } -> + free_vars_bterms gvars bvars bterms + and free_vars_bterms gvars bvars = function + | { bvars = vars; bterm = term}::l -> + let bvars' = vars @ bvars in + let gvars' = free_vars_term gvars bvars' term in + free_vars_bterms gvars' bvars l + | [] -> + gvars + +let free_vars_list = free_vars_term [] [] + + +(* Termop: *) + +let is_no_subterms_term opname = function + | { term_op = { op_name = opname'; op_params = [] }; + term_terms = [] + } -> + Opname.eq opname' opname + | _ -> + false + +(* + * Terms with one subterm. + *) +let is_dep0_term opname = function + | { term_op = { op_name = opname'; op_params = [] }; + term_terms = [{ bvars = [] }] + } -> Opname.eq opname' opname + | _ -> false + +let mk_dep0_term opname t = + { term_op = { op_name = opname; op_params = [] }; + term_terms = [{ bvars = []; bterm = t }] + } + +let dest_dep0_term opname = function + | { term_op = { op_name = opname'; op_params = [] }; + term_terms = [{ bvars = []; bterm = t }] + } when Opname.eq opname' opname -> t + | t -> ref_raise(RefineError ("dest_dep0_term", TermMatchError (t, "not a dep0 term"))) + +(* + * Terms with two subterms. + *) +let is_dep0_dep0_term opname = function + | { term_op = { op_name = opname'; op_params = [] }; + term_terms = [{ bvars = [] }; { bvars = [] }] + } -> Opname.eq opname' opname + | _ -> false + +let mk_dep0_dep0_term opname = fun + t1 t2 -> + { term_op = { op_name = opname; op_params = [] }; + term_terms = [{ bvars = []; bterm = t1 }; + { bvars = []; bterm = t2 }] + } + +let dest_dep0_dep0_term opname = function + | { term_op = { op_name = opname'; op_params = [] }; + term_terms = [{ bvars = []; bterm = t1 }; + { bvars = []; bterm = t2 }] + } when Opname.eq opname' opname -> t1, t2 + | t -> ref_raise(RefineError ("dest_dep0_dep0_term", TermMatchError (t, "bad arity"))) + +(* + * Bound term. + *) + +let is_dep0_dep1_term opname = function + | { term_op = { op_name = opname'; op_params = [] }; + term_terms = [{ bvars = [] }; { bvars = [_] }] + } when Opname.eq opname' opname -> true + | _ -> false + +let is_dep0_dep1_any_term = function + | { term_op = { op_params = [] }; + term_terms = [{ bvars = [] }; { bvars = [_] }] + } -> true + | _ -> false + +let mk_dep0_dep1_term opname = fun + v t1 t2 -> { term_op = { op_name = opname; op_params = [] }; + term_terms = [{ bvars = []; bterm = t1 }; + { bvars = [v]; bterm = t2 }] + } + +let dest_dep0_dep1_term opname = function + | { term_op = { op_name = opname'; op_params = [] }; + term_terms = [{ bvars = []; bterm = t1 }; + { bvars = [v]; bterm = t2 }] + } when Opname.eq opname' opname -> v, t1, t2 + | t -> ref_raise(RefineError ("dest_dep0_dep1_term", TermMatchError (t, "bad arity"))) + +let rec smap f = function + | [] -> [] + | (hd::tl) as l -> + let hd' = f hd in + let tl' = smap f tl in + if (hd==hd')&&(tl==tl') then l else hd'::tl' + +let rec try_check_assoc v v' = function + | [] -> raise Not_found + | (v1,v2)::tl -> + begin match v=v1, v'=v2 with + | true, true -> true + | false, false -> try_check_assoc v v' tl + | _ -> false + end + +let rec zip_list l l1 l2 = match (l1,l2) with + | (h1::t1), (h2::t2) -> + zip_list ((h1,h2)::l) t1 t2 + | [], [] -> + l + | _ -> raise (Failure "Term.zip_list") + +let rec assoc_in_range eq y = function + | (_, y')::tl -> + (eq y y') || (assoc_in_range eq y tl) + | [] -> + false + +let rec check_assoc v v' = function + | [] -> v=v' + | (v1,v2)::tl -> + begin match v=v1, v'=v2 with + | true, true -> true + | false, false -> check_assoc v v' tl + | _ -> false + end + +let rec zip a b = match (a,b) with + | (h1::t1), (h2::t2) -> + (h1, h2) :: zip t1 t2 + | [], [] -> + [] + | + _ -> raise (Failure "Term.zip") + +let rec for_all2 f l1 l2 = + match (l1,l2) with + | h1::t1, h2::t2 -> for_all2 f t1 t2 & f h1 h2 + | [], [] -> true + | _ -> false + +let newname v i = + v ^ "_" ^ (string_of_int i) + +let rec new_var v avoid i = + let v' = newname v i in + if avoid v' + then new_var v avoid (succ i) + else v' + +let vnewname v avoid = new_var v avoid 1 + +let rev_mem a b = List.mem b a + +let rec find_index_aux v i = function + | h::t -> + if h = v then + i + else + find_index_aux v (i + 1) t + | [] -> + raise Not_found + +let find_index v l = find_index_aux v 0 l + +let rec remove_elements l1 l2 = + match l1, l2 with + | flag::ft, h::t -> + if flag then + remove_elements ft t + else + h :: remove_elements ft t + | _, l -> + l + +let rec subtract l1 l2 = + match l1 with + | h::t -> + if List.mem h l2 then + subtract t l2 + else + h :: subtract t l2 + | [] -> + [] + +let rec fv_mem fv v = + match fv with + | [] -> false + | h::t -> + List.mem v h || fv_mem t v + +let rec new_vars fv = function + | [] -> [] + | v::t -> + (* Rename the first one, then add it to free vars *) + let v' = vnewname v (fv_mem fv) in + v'::(new_vars ([v']::fv) t) + +let rec fsubtract l = function + | [] -> l + | h::t -> + fsubtract (subtract l h) t + +let add_renames_fv r l = + let rec aux = function + | [] -> l + | v::t -> [v]::(aux t) + in + aux r + +let add_renames_terms r l = + let rec aux = function + | [] -> l + | v::t -> (mk_var_term v)::(aux t) + in + aux r + +(* + * First order simultaneous substitution. + *) +let rec subst_term terms fv vars = function + | { term_op = { op_name = opname; op_params = [Var(v)] }; term_terms = [] } as t + when Opname.eq opname var_opname-> + (* Var case *) + begin + try List.nth terms (find_index v vars) with + Not_found -> + t + end + | { term_op = op; term_terms = bterms } -> + (* Other term *) + { term_op = op; term_terms = subst_bterms terms fv vars bterms } + +and subst_bterms terms fv vars bterms = + (* When subst through bterms, catch binding occurrences *) + let rec subst_bterm = function + | { bvars = []; bterm = term } -> + (* Optimize the common case *) + { bvars = []; bterm = subst_term terms fv vars term } + + | { bvars = bvars; bterm = term } -> + (* First subtract bound instances *) + let flags = List.map (function v -> List.mem v bvars) vars in + let vars' = remove_elements flags vars in + let fv' = remove_elements flags fv in + let terms' = remove_elements flags terms in + + (* If any of the binding variables are free, rename them *) + let renames = subtract bvars (fsubtract bvars fv') in + if renames <> [] then + let fv'' = (free_vars_list term)::fv' in + let renames' = new_vars fv'' renames in + { bvars = subst_bvars renames' renames bvars; + bterm = subst_term + (add_renames_terms renames' terms') + (add_renames_fv renames' fv') + (renames @ vars') + term + } + else + { bvars = bvars; + bterm = subst_term terms' fv' vars' term + } + in + List.map subst_bterm bterms + +and subst_bvars renames' renames bvars = + let subst_bvar v = + try List.nth renames' (find_index v renames) with + Not_found -> v + in + List.map subst_bvar bvars + +let subst term vars terms = + subst_term terms (List.map free_vars_list terms) vars term + +(*i bug!!! in the [term_std] module + let subst1 t var term = + let fv = free_vars_list term in + if List.mem var fv then + subst_term [term] [fv] [var] t + else + t +The following is the correct implementation +i*) + +let subst1 t var term = +if List.mem var (free_vars_list t) then + subst_term [term] [free_vars_list term] [var] t +else + t + +let apply_subst t s = + let vs,ts = List.split s in + subst t vs ts + +let rec equal_params p1 p2 = + match p1, p2 with + | Number n1, Number n2 -> + n1 = n2 + | ParamList pl1, ParamList pl2 -> + List.for_all2 equal_params pl1 pl2 + | _ -> + p1 = p2 + +let rec equal_term vars t t' = + match t, t' with + | { term_op = { op_name = opname1; op_params = [Var v] }; + term_terms = [] + }, + { term_op = { op_name = opname2; op_params = [Var v'] }; + term_terms = [] + } when Opname.eq opname1 var_opname & Opname.eq opname2 var_opname -> + check_assoc v v' vars + | { term_op = { op_name = name1; op_params = params1 }; term_terms = bterms1 }, + { term_op = { op_name = name2; op_params = params2 }; term_terms = bterms2 } -> + (Opname.eq name1 name2) + & (for_all2 equal_params params1 params2) + & (equal_bterms vars bterms1 bterms2) +and equal_bterms vars bterms1 bterms2 = + let equal_bterm = fun + { bvars = bvars1; bterm = term1 } + { bvars = bvars2; bterm = term2 } -> + equal_term (zip_list vars bvars1 bvars2) term1 term2 + in + for_all2 equal_bterm bterms1 bterms2 + + +let alpha_equal t1 t2 = + try equal_term [] t1 t2 with Failure _ -> false + +let var_subst t t' v = + let { term_op = { op_name = opname } } = t' in + let vt = mk_var_term v in + let rec subst_term = function + { term_op = { op_name = opname'; op_params = params }; + term_terms = bterms + } as t -> + (* Check if this is the same *) + if Opname.eq opname' opname & alpha_equal t t' then + vt + else + { term_op = { op_name = opname'; op_params = params }; + term_terms = List.map subst_bterm bterms + } + + and subst_bterm { bvars = vars; bterm = term } = + if List.mem v vars then + let av = vars @ (free_vars_list term) in + let v' = vnewname v (fun v -> List.mem v av) in + let rename var = if var = v then v' else var in + let term = subst1 term v (mk_var_term v') in + { bvars = smap rename vars; bterm = subst_term term } + else + { bvars = vars; bterm = subst_term term } + in + subst_term t + +let xnil_opname = mk_opname "nil" xperv +let xnil_term = mk_simple_term xnil_opname [] +let is_xnil_term = is_no_subterms_term xnil_opname + +(*c End of the extraction from Meta-Prl *) + +(* Huang's modification: *) +let all_opname = make_opname ["quantifier";"all"] +let is_all_term = is_dep0_dep1_term all_opname +let dest_all = dest_dep0_dep1_term all_opname +let mk_all_term = mk_dep0_dep1_term all_opname + +let exists_opname = make_opname ["quantifier";"exst"] +let is_exists_term = is_dep0_dep1_term exists_opname +let dest_exists = dest_dep0_dep1_term exists_opname +let mk_exists_term = mk_dep0_dep1_term exists_opname + +let or_opname = make_opname ["connective";"or"] +let is_or_term = is_dep0_dep0_term or_opname +let dest_or = dest_dep0_dep0_term or_opname +let mk_or_term = mk_dep0_dep0_term or_opname + +let and_opname = make_opname ["connective";"and"] +let is_and_term = is_dep0_dep0_term and_opname +let dest_and = dest_dep0_dep0_term and_opname +let mk_and_term = mk_dep0_dep0_term and_opname + +let cor_opname = make_opname ["connective";"cor"] +let is_cor_term = is_dep0_dep0_term cor_opname +let dest_cor = dest_dep0_dep0_term cor_opname +let mk_cor_term = mk_dep0_dep0_term cor_opname + +let cand_opname = make_opname ["connective";"cand"] +let is_cand_term = is_dep0_dep0_term cand_opname +let dest_cand = dest_dep0_dep0_term cand_opname +let mk_cand_term = mk_dep0_dep0_term cand_opname + +let implies_opname = make_opname ["connective";"=>"] +let is_implies_term = is_dep0_dep0_term implies_opname +let dest_implies = dest_dep0_dep0_term implies_opname +let mk_implies_term = mk_dep0_dep0_term implies_opname + +let iff_opname = make_opname ["connective";"iff"] +let is_iff_term = is_dep0_dep0_term iff_opname +let dest_iff = dest_dep0_dep0_term iff_opname +let mk_iff_term = mk_dep0_dep0_term iff_opname + +let not_opname = make_opname ["connective";"not"] +let is_not_term = is_dep0_term not_opname +let dest_not = dest_dep0_term not_opname +let mk_not_term = mk_dep0_term not_opname + +let var_ = mk_var_term +let fun_opname = make_opname ["function"] +let fun_ f ts = mk_any_term {op_name = fun_opname; op_params = [String f] } ts + +let is_fun_term = function + | { term_op = { op_name = opname; op_params = [String f] }} + when Opname.eq opname fun_opname -> true + | _ -> + false + +let dest_fun = function + | { term_op = { op_name = opname; op_params = [String f] }; term_terms = ts} + when Opname.eq opname fun_opname -> (f, List.map (fun { bterm = t } -> t) ts) + | t -> + ref_raise(RefineError ("dest_fun", TermMatchError (t, "not a function symbol"))) + +let const_ c = fun_ c [] +let is_const_term = function + | { term_op = { op_name = opname; op_params = [String f] }; term_terms = [] } + when Opname.eq opname fun_opname -> true + | _ -> + false + +let dest_const t = + let (n, ts) = dest_fun t in n + +let pred_opname = make_opname ["predicate"] +let pred_ p ts = mk_any_term {op_name = pred_opname; op_params = [String p] } ts + +let not_ = mk_not_term +let and_ = mk_and_term +let or_ = mk_or_term +let imp_ = mk_implies_term +let cand_ = mk_cand_term +let cor_ = mk_cor_term +let iff_ = mk_iff_term +let nil_term = {term_op={op_name=nil_opname; op_params=[]}; term_terms=[] } +let forall v t = mk_all_term v nil_term t +let exists v t= mk_exists_term v nil_term t +let rec wbin op = function + | [] -> raise (Failure "Term.wbin") + | [t] -> t + | t::r -> op t (wbin op r) + +let wand_ = wbin and_ +let wor_ = wbin or_ +let wimp_ = wbin imp_ + +(*i let true_opname = make_opname ["bool";"true"] +let is_true_term = is_no_subterms_term true_opname +let true_ = mk_simple_term true_opname [] +let false_ = not_ true_ + +let is_false_term t = + if is_not_term t then + let t1 = dest_not t in + is_true_term t1 + else + false +i*) + +let dummy_false_ = mk_simple_term (make_opname ["bool";"false"]) [] +let dummy_true_ = mk_simple_term (make_opname ["bool";"true"]) [] +let false_ = and_ (dummy_false_) (not_ dummy_false_) +let true_ = not_ (and_ (dummy_true_) (not_ dummy_true_)) + +let is_false_term t = + if (alpha_equal t false_) then true + else false + +let is_true_term t = + if (alpha_equal t true_) then true + else false + +(* Print a term [t] via the [ostream]: *) +let rec fprint_term ostream t prec = + let l_print op_prec = + if (prec > op_prec) then fprintf ostream "(" in + let r_print op_prec = + if (prec > op_prec) then fprintf ostream ")" in + if is_false_term t then (* false *) + fprint_str_list ostream ["False"] + else if is_true_term t then (* true *) + fprint_str_list ostream ["True"] + else if is_all_term t then (* for all *) + let v, t1, t2 = dest_all t in + fprint_str_list ostream ["A."^v]; + fprint_term ostream t2 4 + else if is_exists_term t then (* exists *) + let v, t1, t2 = dest_exists t in + fprint_str_list ostream ["E."^v]; + fprint_term ostream t2 4 (* implication *) + else if is_implies_term t then + let t1, t2 = dest_implies t in + l_print 0; + fprint_term ostream t1 1; + fprint_str_list ostream ["=>"]; + fprint_term ostream t2 0; + r_print 0 + else if is_and_term t then (* logical and *) + let t1, t2 = dest_and t in + l_print 3; + fprint_term ostream t1 3; + fprint_str_list ostream ["&"]; + fprint_term ostream t2 3; + r_print 3 + else if is_or_term t then (* logical or *) + let t1, t2 = dest_or t in + l_print 2; + fprint_term ostream t1 2; + fprint_str_list ostream ["|"]; + fprint_term ostream t2 2; + r_print 2 + else if is_not_term t then (* logical not *) + let t2 = dest_not t in + fprint_str_list ostream ["~"]; + fprint_term ostream t2 4 (* nil term *) + else if is_xnil_term t then + fprint_str_list ostream ["NIL"] + else match t with (* other cases *) + { term_op = { op_name = opname; op_params = opparm }; term_terms = bterms} -> + if (Opname.eq opname pred_opname) || (Opname.eq opname fun_opname) then + begin + fprint_param_list ostream opparm; + if bterms != [] then + begin + fprintf ostream "("; + fprint_bterm_list ostream prec bterms; + fprintf ostream ")"; + end + end else + begin + fprintf ostream "["; +(* fprint_opname ostream opname; + fprintf ostream ": "; *) + fprint_param_list ostream opparm; + if bterms != [] then + begin + fprintf ostream "("; + fprint_bterm_list ostream prec bterms; + fprintf ostream ")"; + end; + fprintf ostream "]" + end +and fprint_bterm_list ostream prec = function + | [] -> () + | {bvars=bv; bterm=bt}::r -> + fprint_str_list ostream bv; + fprint_term ostream bt prec; + if (r<>[]) then fprint_str_list ostream [","]; + fprint_bterm_list ostream prec r +;; + + +let print_term ostream t = + Format.print_flush (); + fprint_term ostream t 0; + Format.print_flush () + +let print_error_msg = function + | RefineError(s,e) -> print_string ("(module "^s^") "); + begin + match e with + | TermMatchError(t,s) -> print_term stdout t; print_string (s^"\n") + | StringError s -> print_string (s^"\n") + end + | ue -> print_string "Unexpected error for Jp.\n"; + raise ue + + +(* Naive implementation for [jterm] substitution, unification, etc.: *) +let substitute subst term = + apply_subst term subst + +(* A naive unification algorithm: *) +let compsubst subst1 subst2 = + (List.map (fun (v, t) -> (v, substitute subst1 t)) subst2) @ subst1 +;; + +let rec extract_terms = function + | [] -> [] + | h::r -> let {bvars=_; bterm=bt}=h in bt::extract_terms r + +(* Occurs check: *) +let occurs v t = + let rec occur_rec t = + if is_var_term t then v=dest_var t + else let { term_op = _ ; term_terms = bterms} = t in + let sons = extract_terms bterms in + List.exists occur_rec sons + in + occur_rec t + +(* The naive unification algorithm: *) +let rec unify2 (term1,term2) = + if is_var_term term1 then + if equal_term [] term1 term2 then [] + else let v1 = dest_var term1 in + if occurs v1 term2 then raise (RefineError ("unify1", StringError ("1"))) + else [v1,term2] + else if is_var_term term2 then + let v2 = dest_var term2 in + if occurs v2 term1 then raise (RefineError ("unify2", StringError ("2"))) + else [v2,term1] + else + let { term_op = { op_name = opname1; op_params = params1 }; + term_terms = bterms1 + } = term1 + in + let { term_op = { op_name = opname2; op_params = params2 }; + term_terms = bterms2 + } = term2 + in + if Opname.eq opname1 opname2 & params1 = params2 then + let sons1 = extract_terms bterms1 + and sons2 = extract_terms bterms2 in + List.fold_left2 + (fun s t1 t2 -> compsubst + (unify2 (substitute s t1, substitute s t2)) s) + [] sons1 sons2 + else raise (RefineError ("unify3", StringError ("3"))) + +let unify term1 term2 = unify2 (term1, term2) +let unify_mm term1 term2 _ = unify2 (term1, term2) diff --git a/contrib/jprover/jterm.mli b/contrib/jprover/jterm.mli new file mode 100644 index 000000000..0bc42010d --- /dev/null +++ b/contrib/jprover/jterm.mli @@ -0,0 +1,110 @@ +(* This module is modified and extracted from Meta-Prl. *) + +(* Definitions of [jterm]: *) +type param = param' +and operator = operator' +and term = term' +and bound_term = bound_term' +and param' = + | Number of int + | String of string + | Token of string + | Var of string + | ParamList of param list +and operator' = { op_name : Opname.opname; op_params : param list; } +and term' = { term_op : operator; term_terms : bound_term list; } +and bound_term' = { bvars : string list; bterm : term; } +type term_subst = (string * term) list + +type error_msg = TermMatchError of term * string | StringError of string + +exception RefineError of string * error_msg + +(* Collect free variables: *) +val free_vars_list : term -> string list + +(* Substitutions: *) +val subst_term : term list -> string list list -> string list -> term -> term +val subst : term -> string list -> term list -> term +val subst1 : term -> string -> term -> term +val var_subst : term -> term -> string -> term +val apply_subst : term -> (string * term) list -> term + +(* Unification: *) +val unify_mm : term -> term -> 'a -> (string * term) list + +val xnil_term : term' + +(* Testing functions: *) +val is_xnil_term : term' -> bool +val is_var_term : term' -> bool +val is_true_term : term' -> bool +val is_false_term : term' -> bool +val is_all_term : term' -> bool +val is_exists_term : term' -> bool +val is_or_term : term' -> bool +val is_and_term : term' -> bool +val is_cor_term : term' -> bool +val is_cand_term : term' -> bool +val is_implies_term : term' -> bool +val is_iff_term : term' -> bool +val is_not_term : term' -> bool +val is_fun_term : term -> bool +val is_const_term : term -> bool + + +(* Constructors for [jterms]: *) +val var_ : string -> term' +val fun_ : string -> term list -> term' +val const_ : string -> term' +val pred_ : string -> term list -> term' +val not_ : term -> term' +val and_ : term -> term -> term' +val or_ : term -> term -> term' +val imp_ : term -> term -> term' +val cand_ : term -> term -> term' +val cor_ : term -> term -> term' +val iff_ : term -> term -> term' +val false_ : term' +val true_ : term' +val nil_term : term' +val forall : string -> term -> term' +val exists : string -> term -> term' + + +(* Destructors for [jterm]: *) +val dest_var : term -> string +val dest_fun : term -> string * term list +val dest_const : term -> string +val dest_not : term -> term +val dest_iff : term -> term * term +val dest_implies : term -> term * term +val dest_cand : term -> term * term +val dest_cor : term -> term * term +val dest_and : term -> term * term +val dest_or : term -> term * term +val dest_exists : term -> string * term * term +val dest_all : term -> string * term * term + +(* Wide-logical connectives: *) +val wand_ : term list -> term +val wor_ : term list -> term +val wimp_ : term list -> term + +(* Printing and debugging tools: *) +val fprint_str_list : out_channel -> string list -> unit +val mbreak : string -> unit +val print_strs : string list -> unit +val print_term : out_channel -> term -> unit +val print_error_msg : exn -> unit + +(* Other exported functions for [jall.ml]: *) +val make_term : 'a -> 'a +val dest_term : 'a -> 'a +val make_op : 'a -> 'a +val dest_op : 'a -> 'a +val make_bterm : 'a -> 'a +val dest_bterm : 'a -> 'a +val dest_param : 'a -> 'a +val mk_var_term : string -> term' +val mk_string_term : Opname.opname -> string -> term' diff --git a/contrib/jprover/jtunify.ml b/contrib/jprover/jtunify.ml new file mode 100644 index 000000000..6a173e86d --- /dev/null +++ b/contrib/jprover/jtunify.ml @@ -0,0 +1,507 @@ +(* + * Unification procedures for JProver. See jall.mli for more + * information on JProver. + * + * ---------------------------------------------------------------- + * + * This file is part of MetaPRL, a modular, higher order + * logical framework that provides a logical programming + * environment for OCaml and other languages. + * + * See the file doc/index.html for information on Nuprl, + * OCaml, and more information about this system. + * + * Copyright (C) 2000 Stephan Schmitt + * + * This program is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * This program is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with this program; if not, write to the Free Software + * Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA. + * + * Author: Stephan Schmitt <schmitts@spmail.slu.edu> + * Modified by: Aleksey Nogin <nogin@cs.cornell.edu> + *) + +exception Not_unifiable +exception Failed + +let jprover_bug = Invalid_argument "Jprover bug (Jtunify module)" + +(* ************ T-STRING UNIFICATION *********************************) + + +(* ******* printing ********** *) + +let rec list_to_string s = + match s with + [] -> "" + | f::r -> + f^"."^(list_to_string r) + +let rec print_eqlist eqlist = + match eqlist with + [] -> + print_endline "" + | (atnames,f)::r -> + let (s,t) = f in + let ls = list_to_string s + and lt = list_to_string t in + begin + print_endline ("Atom names: "^(list_to_string atnames)); + print_endline (ls^" = "^lt); + print_eqlist r + end + +let print_equations eqlist = + begin + Format.open_box 0; + Format.force_newline (); + print_endline "Equations:"; + print_eqlist eqlist; + Format.force_newline (); + end + +let rec print_subst sigma = + match sigma with + [] -> + print_endline "" + | f::r -> + let (v,s) = f in + let ls = list_to_string s in + begin + print_endline (v^" = "^ls); + print_subst r + end + +let print_tunify sigma = + let (n,subst) = sigma in + begin + print_endline " "; + print_endline ("MaxVar = "^(string_of_int (n-1))); + print_endline " "; + print_endline "Substitution:"; + print_subst subst; + print_endline " " + end + + (*****************************************************) + +let is_const name = + (String.get name 0) = 'c' + +let is_var name = + (String.get name 0) = 'v' + +let r_1 s ft rt = + (s = []) && (ft = []) && (rt = []) + +let r_2 s ft rt = + (s = []) && (ft = []) && (List.length rt >= 1) + +let r_3 s ft rt = + ft=[] && (List.length s >= 1) && (List.length rt >= 1) && (List.hd s = List.hd rt) + +let r_4 s ft rt = + ft=[] + && (List.length s >= 1) + && (List.length rt >= 1) + && is_const (List.hd s) + && is_var (List.hd rt) + +let r_5 s ft rt = + rt=[] + && (List.length s >= 1) + && is_var (List.hd s) + +let r_6 s ft rt = + ft=[] + && (List.length s >= 1) + && (List.length rt >= 1) + && is_var (List.hd s) + && is_const (List.hd rt) + +let r_7 s ft rt = + List.length s >= 1 + && (List.length rt >= 2) + && is_var (List.hd s) + && is_const (List.hd rt) + && is_const (List.hd (List.tl rt)) + +let r_8 s ft rt = + ft=[] + && List.length s >= 2 + && List.length rt >= 1 + && let v = List.hd s + and v1 = List.hd rt in + (is_var v) & (is_var v1) & (v <> v1) + +let r_9 s ft rt = + (List.length s >= 2) && (List.length ft >= 1) && (List.length rt >= 1) + && let v = (List.hd s) + and v1 = (List.hd rt) in + (is_var v) & (is_var v1) & (v <> v1) + +let r_10 s ft rt = + (List.length s >= 1) && (List.length rt >= 1) + && let v = List.hd s + and x = List.hd rt in + (is_var v) && (v <> x) + && (((List.tl s) =[]) or (is_const x) or ((List.tl rt) <> [])) + +let rec com_subst slist ((ov,ovlist) as one_subst) = + match slist with + [] -> raise jprover_bug + | f::r -> + if f = ov then + (ovlist @ r) + else + f::(com_subst r one_subst) + +let rec combine subst ((ov,oslist) as one_subst) = + match subst with + [] -> [] + | ((v, slist) as f) :: r -> + let rest_combine = (combine r one_subst) in + if (List.mem ov slist) then (* subst assumed to be idemponent *) + let com_element = com_subst slist one_subst in + ((v,com_element)::rest_combine) + else + (f::rest_combine) + +let compose ((n,subst) as sigma) ((ov,oslist) as one_subst) = + let com = combine subst one_subst in +(* begin + print_endline "!!!!!!!!!test print!!!!!!!!!!"; + print_subst [one_subst]; + print_subst subst; + print_endline "!!!!!!!!! END test print!!!!!!!!!!"; +*) + if List.mem one_subst subst then + (n,com) + else +(* ov may multiply as variable in subst with DIFFERENT values *) +(* in order to avoid explicit atom instances!!! *) + (n,(com @ [one_subst])) +(* end *) + +let rec apply_element fs ft (v,slist) = + match (fs,ft) with + ([],[]) -> + ([],[]) + | ([],(ft_first::ft_rest)) -> + let new_ft_first = + if ft_first = v then + slist + else + [ft_first] + in + let (emptylist,new_ft_rest) = apply_element [] ft_rest (v,slist) in + (emptylist,(new_ft_first @ new_ft_rest)) + | ((fs_first::fs_rest),[]) -> + let new_fs_first = + if fs_first = v then + slist + else + [fs_first] + in + let (new_fs_rest,emptylist) = apply_element fs_rest [] (v,slist) in + ((new_fs_first @ new_fs_rest),emptylist) + | ((fs_first::fs_rest),(ft_first::ft_rest)) -> + let new_fs_first = + if fs_first = v then + slist + else + [fs_first] + and new_ft_first = + if ft_first = v then + slist + else + [ft_first] + in + let (new_fs_rest,new_ft_rest) = apply_element fs_rest ft_rest (v,slist) in + ((new_fs_first @ new_fs_rest),(new_ft_first @ new_ft_rest)) + +let rec shorten us ut = + match (us,ut) with + ([],_) | (_,[]) -> raise jprover_bug + | ((fs::rs),(ft::rt)) -> + if fs = ft then + shorten rs rt + else + (us,ut) + +let rec apply_subst_list eq_rest (v,slist) = + match eq_rest with + [] -> + (true,[]) + | (atomnames,(fs,ft))::r -> + let (n_fs,n_ft) = apply_element fs ft (v,slist) in + let (new_fs,new_ft) = shorten n_fs n_ft in (* delete equal first elements *) + match (new_fs,new_ft) with + [],[] -> + let (bool,new_eq_rest) = apply_subst_list r (v,slist) in + (bool,((atomnames,([],[]))::new_eq_rest)) + | [],(fft::rft) -> + if (is_const fft) then + (false,[]) + else + let (bool,new_eq_rest) = apply_subst_list r (v,slist) in + (bool,((atomnames,([],new_ft))::new_eq_rest)) + | (ffs::rfs),[] -> + if (is_const ffs) then + (false,[]) + else + let (bool,new_eq_rest) = apply_subst_list r (v,slist) in + (bool,((atomnames,(new_fs,[]))::new_eq_rest)) + | (ffs::rfs),(fft::rft) -> + if (is_const ffs) & (is_const fft) then + (false,[]) + (* different first constants cause local fail *) + else + (* at least one of firsts is a variable *) + let (bool,new_eq_rest) = apply_subst_list r (v,slist) in + (bool,((atomnames,(new_fs,new_ft))::new_eq_rest)) + +let apply_subst eq_rest (v,slist) atomnames = + if (List.mem v atomnames) then (* don't apply subst to atom variables !! *) + (true,eq_rest) + else + apply_subst_list eq_rest (v,slist) + + +(* let all_variable_check eqlist = false needs some discussion with Jens! -- NOT done *) + +(* + let rec all_variable_check eqlist = + match eqlist with + [] -> true + | ((_,(fs,ft))::rest_eq) -> + if (fs <> []) & (ft <> []) then + let fs_first = List.hd fs + and ft_first = List.hd ft + in + if (is_const fs_first) or (is_const ft_first) then + false + else + all_variable_check rest_eq + else + false +*) + +let rec tunify_list eqlist init_sigma = + let rec tunify atomnames fs ft rt rest_eq sigma = + let apply_r1 fs ft rt rest_eq sigma = + (* print_endline "r1"; *) + tunify_list rest_eq sigma + + in + let apply_r2 fs ft rt rest_eq sigma = + (* print_endline "r2"; *) + tunify atomnames rt fs ft rest_eq sigma + + in + let apply_r3 fs ft rt rest_eq sigma = + (* print_endline "r3"; *) + let rfs = (List.tl fs) + and rft = (List.tl rt) in + tunify atomnames rfs ft rft rest_eq sigma + + in + let apply_r4 fs ft rt rest_eq sigma = + (* print_endline "r4"; *) + tunify atomnames rt ft fs rest_eq sigma + + in + let apply_r5 fs ft rt rest_eq sigma = + (* print_endline "r5"; *) + let v = (List.hd fs) in + let new_sigma = compose sigma (v,ft) in + let (bool,new_rest_eq) = apply_subst rest_eq (v,ft) atomnames in + if (bool=false) then + raise Not_unifiable + else + tunify atomnames (List.tl fs) rt rt new_rest_eq new_sigma + + in + let apply_r6 fs ft rt rest_eq sigma = + (* print_endline "r6"; *) + let v = (List.hd fs) in + let new_sigma = (compose sigma (v,[])) in + let (bool,new_rest_eq) = apply_subst rest_eq (v,[]) atomnames in + if (bool=false) then + raise Not_unifiable + else + tunify atomnames (List.tl fs) ft rt new_rest_eq new_sigma + + in + let apply_r7 fs ft rt rest_eq sigma = + (* print_endline "r7"; *) + let v = (List.hd fs) + and c1 = (List.hd rt) + and c2t =(List.tl rt) in + let new_sigma = (compose sigma (v,(ft @ [c1]))) in + let (bool,new_rest_eq) = apply_subst rest_eq (v,(ft @ [c1])) atomnames in + if bool=false then + raise Not_unifiable + else + tunify atomnames (List.tl fs) [] c2t new_rest_eq new_sigma + in + let apply_r8 fs ft rt rest_eq sigma = + (* print_endline "r8"; *) + tunify atomnames rt [(List.hd fs)] (List.tl fs) rest_eq sigma + + in + let apply_r9 fs ft rt rest_eq sigma = + (* print_endline "r9"; *) + let v = (List.hd fs) + and (max,subst) = sigma in + let v_new = ("vnew"^(string_of_int max)) in + let new_sigma = (compose ((max+1),subst) (v,(ft @ [v_new]))) in + let (bool,new_rest_eq) = apply_subst rest_eq (v,(ft @ [v_new])) atomnames in + if (bool=false) then + raise Not_unifiable + else + tunify atomnames rt [v_new] (List.tl fs) new_rest_eq new_sigma + + in + let apply_r10 fs ft rt rest_eq sigma = + (* print_endline "r10"; *) + let x = List.hd rt in + tunify atomnames fs (ft @ [x]) (List.tl rt) rest_eq sigma + + in + if r_1 fs ft rt then + apply_r1 fs ft rt rest_eq sigma + else if r_2 fs ft rt then + apply_r2 fs ft rt rest_eq sigma + else if r_3 fs ft rt then + apply_r3 fs ft rt rest_eq sigma + else if r_4 fs ft rt then + apply_r4 fs ft rt rest_eq sigma + else if r_5 fs ft rt then + apply_r5 fs ft rt rest_eq sigma + else if r_6 fs ft rt then + (try + apply_r6 fs ft rt rest_eq sigma + with Not_unifiable -> + if r_7 fs ft rt then (* r7 applicable if r6 was and tr6 = C2t' *) + (try + apply_r7 fs ft rt rest_eq sigma + with Not_unifiable -> + apply_r10 fs ft rt rest_eq sigma (* r10 always applicable if r6 was *) + ) + else + (* r10 could be represented only once if we would try it before r7.*) + (* but looking at the transformation rules, r10 should be tried at last in any case *) + apply_r10 fs ft rt rest_eq sigma (* r10 always applicable r6 was *) + ) + else if r_7 fs ft rt then (* not r6 and r7 possible if z <> [] *) + (try + apply_r7 fs ft rt rest_eq sigma + with Not_unifiable -> + apply_r10 fs ft rt rest_eq sigma (* r10 always applicable if r7 was *) + ) + else if r_8 fs ft rt then + (try + apply_r8 fs ft rt rest_eq sigma + with Not_unifiable -> + if r_10 fs ft rt then (* r10 applicable if r8 was and tr8 <> [] *) + apply_r10 fs ft rt rest_eq sigma + else + raise Not_unifiable (* simply back propagation *) + ) + else if r_9 fs ft rt then + (try + apply_r9 fs ft rt rest_eq sigma + with Not_unifiable -> + if r_10 fs ft rt then (* r10 applicable if r9 was and tr9 <> [] *) + apply_r10 fs ft rt rest_eq sigma + else + raise Not_unifiable (* simply back propagation *) + ) + else if r_10 fs ft rt then (* not ri, i<10, and r10 possible if for instance *) + (* (s=[] and x=v1) or (z<>[] and xt=C1V1t') *) + apply_r10 fs ft rt rest_eq sigma + else (* NO rule applicable *) + raise Not_unifiable + in + match eqlist with + [] -> + init_sigma + | f::rest_eq -> + let (atomnames,(fs,ft)) = f in + tunify atomnames fs [] ft rest_eq init_sigma + +let rec test_apply_eq atomnames eqs eqt subst = + match subst with + [] -> (eqs,eqt) + | (f,flist)::r -> + let (first_appl_eqs,first_appl_eqt) = + if List.mem f atomnames then + (eqs,eqt) + else + (apply_element eqs eqt (f,flist)) + in + test_apply_eq atomnames first_appl_eqs first_appl_eqt r + +let rec test_apply_eqsubst eqlist subst = + match eqlist with + [] -> [] + | f::r -> + let (atomnames,(eqs,eqt)) = f in + let applied_element = test_apply_eq atomnames eqs eqt subst in + (atomnames,applied_element)::(test_apply_eqsubst r subst) + +let ttest us ut ns nt eqlist orderingQ atom_rel = + let (short_us,short_ut) = shorten us ut in (* apply intial rule R3 *) + (* to eliminate common beginning *) + let new_element = ([ns;nt],(short_us,short_ut)) in + let full_eqlist = + if List.mem new_element eqlist then + eqlist + else + new_element::eqlist + in + let sigma = tunify_list full_eqlist (1,[]) in + let (n,subst) = sigma in + let test_apply = test_apply_eqsubst full_eqlist subst in + begin + print_endline ""; + print_endline "Final equations:"; + print_equations full_eqlist; + print_endline ""; + print_endline "Final substitution:"; + print_tunify sigma; + print_endline ""; + print_endline "Applied equations:"; + print_equations test_apply + end + +let do_stringunify us ut ns nt equations = + let (short_us,short_ut) = shorten us ut in (* apply intial rule R3 to eliminate common beginning *) + let new_element = ([ns;nt],(short_us,short_ut)) in + let full_eqlist = + if List.mem new_element equations then + equations + else + new_element::equations + in +(* print_equations full_eqlist; *) + (try + let new_sigma = tunify_list full_eqlist (1,[]) in + (new_sigma,(1,full_eqlist)) + with Not_unifiable -> + raise Failed (* new connection please *) + ) + + +(* type of one unifier: int * (string * string) list *) diff --git a/contrib/jprover/jtunify.mli b/contrib/jprover/jtunify.mli new file mode 100644 index 000000000..0aabc79ee --- /dev/null +++ b/contrib/jprover/jtunify.mli @@ -0,0 +1,35 @@ +exception Not_unifiable +exception Failed + +(* Utilities *) + +val is_const : string -> bool +val is_var : string -> bool +val r_1 : 'a list -> 'b list -> 'c list -> bool +val r_2 : 'a list -> 'b list -> 'c list -> bool +val r_3 : 'a list -> 'b list -> 'a list -> bool +val r_4 : string list -> 'a list -> string list -> bool +val r_5 : string list -> 'a -> 'b list -> bool +val r_6 : string list -> 'a list -> string list -> bool +val r_7 : string list -> 'a -> string list -> bool +val r_8 : string list -> 'a list -> string list -> bool +val r_9 : string list -> 'a list -> string list -> bool +val r_10 : string list -> 'a -> string list -> bool +val com_subst : 'a list -> 'a * 'a list -> 'a list + +(* Debugging *) + +val print_equations : (string list * (string list * string list)) list -> unit + +val print_tunify : int * (string * string list) list -> unit + +(* Main function *) + +val do_stringunify : string list -> + string list -> + string -> + string -> + (string list * (string list * string list)) list -> + (int * (string * string list) list) * (* unifier *) + (int * ((string list * (string list * string list)) list)) (* applied new eqlist *) + diff --git a/contrib/jprover/opname.ml b/contrib/jprover/opname.ml new file mode 100644 index 000000000..d0aa90463 --- /dev/null +++ b/contrib/jprover/opname.ml @@ -0,0 +1,90 @@ +open Printf + +type token = string +type atom = string list + +let opname_token = String.make 4 (Char.chr 0) + +type opname = + { mutable opname_token : token; + mutable opname_name : string list + } + +let (optable : (string list, opname) Hashtbl.t) = Hashtbl.create 97 + +(* * Constructors.*) +let nil_opname = { opname_token = opname_token; opname_name = [] } + +let _ = Hashtbl.add optable [] nil_opname + +let rec mk_opname s ({ opname_token = token; opname_name = name } as opname) = + if token == opname_token then + let name = s :: name in + try Hashtbl.find optable name with + Not_found -> + let op = { opname_token = opname_token; opname_name = name } in + Hashtbl.add optable name op; + op + else + mk_opname s (normalize_opname opname) + +and make_opname = function + | [] -> + nil_opname + | h :: t -> + mk_opname h (make_opname t) + +and normalize_opname opname = + if opname.opname_token == opname_token then + (* This opname is already normalized *) + opname + else + let res = make_opname opname.opname_name + in + opname.opname_name <- res.opname_name; + opname.opname_token <- opname_token; + res + +(* * Atoms are the inner string list. *) +let intern opname = + if opname.opname_token == opname_token then + opname.opname_name + else + let name = (normalize_opname opname).opname_name in + opname.opname_token <- opname_token; + opname.opname_name <- name; + name + +let eq_inner op1 op2 = + op1.opname_name <- (normalize_opname op1).opname_name; + op1.opname_token <- opname_token; + op2.opname_name <- (normalize_opname op2).opname_name; + op2.opname_token <- opname_token; + op1.opname_name == op2.opname_name + +let eq op1 op2 = + (op1.opname_name == op2.opname_name) + or ((op1.opname_token != opname_token or op2.opname_token != opname_token) & eq_inner op1 op2) + +(* * Destructor. *) +let dst_opname = function + | { opname_name = n :: name } -> n, { opname_token = opname_token; opname_name = name } + | _ -> raise (Invalid_argument "dst_opname") + +let dest_opname { opname_name = name } = + name + +let string_of_opname op = + let rec flatten = function + | [] -> + "" + | h::t -> + let rec collect s = function + | h::t -> + collect (h ^ "!" ^ s) t + | [] -> + s + in + collect h t + in + flatten op.opname_name diff --git a/contrib/jprover/opname.mli b/contrib/jprover/opname.mli new file mode 100644 index 000000000..56bf84e22 --- /dev/null +++ b/contrib/jprover/opname.mli @@ -0,0 +1,15 @@ +(* This module is extracted from Meta-Prl. *) + +type token = string +and atom = string list +val opname_token : token +type opname = { + mutable opname_token : token; + mutable opname_name : string list; +} +val nil_opname : opname +val mk_opname : string -> opname -> opname +val make_opname : string list -> opname +val eq : opname -> opname -> bool +val dest_opname : opname -> string list +val string_of_opname : opname -> string |