diff options
| author | corbinea | 2003-02-24 17:12:57 +0000 |
|---|---|---|
| committer | corbinea | 2003-02-24 17:12:57 +0000 |
| commit | b496630ec937dbf2d823d76c53cf6ab81b1544a9 (patch) | |
| tree | 958784db6939aef7b8a137a910abd42778fdd4ac | |
| parent | 3ae01fb7081658f9c2efaa24f4a7f69925dd6e95 (diff) | |
Bringing Linear back to life (Still somewhat buggy).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3699 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | .depend | 210 | ||||
| -rw-r--r-- | .depend.camlp4 | 2 | ||||
| -rw-r--r-- | Makefile | 19 | ||||
| -rwxr-xr-x | contrib/linear/ccidpc.ml4 | 371 | ||||
| -rwxr-xr-x | contrib/linear/dpc.ml4 | 64 | ||||
| -rw-r--r-- | contrib/linear/dpctypes.ml | 60 | ||||
| -rwxr-xr-x | contrib/linear/dpctypes.mli | 59 | ||||
| -rwxr-xr-x | contrib/linear/general.ml | 41 | ||||
| -rwxr-xr-x | contrib/linear/general.mli | 16 | ||||
| -rwxr-xr-x | contrib/linear/graph.ml | 70 | ||||
| -rwxr-xr-x | contrib/linear/graph.mli | 12 | ||||
| -rwxr-xr-x | contrib/linear/kwc.ml | 233 | ||||
| -rwxr-xr-x | contrib/linear/lk_proofs.ml | 730 | ||||
| -rwxr-xr-x | contrib/linear/prove.ml | 80 | ||||
| -rwxr-xr-x | contrib/linear/prove.mli | 19 | ||||
| -rwxr-xr-x | contrib/linear/subst.ml | 150 | ||||
| -rwxr-xr-x | contrib/linear/subst.mli | 21 | ||||
| -rwxr-xr-x | contrib/linear/unif.ml | 311 | ||||
| -rwxr-xr-x | contrib/linear/unif.mli | 27 |
19 files changed, 2421 insertions, 74 deletions
@@ -40,10 +40,10 @@ kernel/indtypes.cmi: kernel/declarations.cmi kernel/entries.cmi \ kernel/univ.cmi kernel/inductive.cmi: kernel/declarations.cmi kernel/environ.cmi \ kernel/names.cmi kernel/term.cmi kernel/univ.cmi -kernel/mod_typing.cmi: kernel/declarations.cmi kernel/entries.cmi \ - kernel/environ.cmi kernel/modops.cmi: kernel/declarations.cmi kernel/entries.cmi \ kernel/environ.cmi kernel/names.cmi kernel/univ.cmi lib/util.cmi +kernel/mod_typing.cmi: kernel/declarations.cmi kernel/entries.cmi \ + kernel/environ.cmi kernel/names.cmi: lib/pp.cmi lib/predicate.cmi kernel/reduction.cmi: kernel/environ.cmi kernel/sign.cmi kernel/term.cmi \ kernel/univ.cmi @@ -63,9 +63,6 @@ kernel/typeops.cmi: kernel/entries.cmi kernel/environ.cmi kernel/names.cmi \ kernel/univ.cmi: kernel/names.cmi lib/pp.cmi lib/bignat.cmi: lib/pp.cmi lib/pp.cmi: lib/pp_control.cmi -lib/rtree.cmi: lib/pp.cmi -lib/system.cmi: lib/pp.cmi -lib/util.cmi: lib/pp.cmi library/declare.cmi: kernel/cooking.cmi library/decl_kinds.cmo \ kernel/declarations.cmi library/dischargedhypsmap.cmi kernel/entries.cmi \ kernel/indtypes.cmi library/libnames.cmi library/libobject.cmi \ @@ -94,7 +91,9 @@ library/library.cmi: library/libnames.cmi library/libobject.cmi \ library/nameops.cmi: kernel/names.cmi lib/pp.cmi library/nametab.cmi: library/libnames.cmi kernel/names.cmi lib/pp.cmi \ kernel/sign.cmi lib/util.cmi -library/summary.cmi: library/libnames.cmi kernel/names.cmi +lib/rtree.cmi: lib/pp.cmi +lib/system.cmi: lib/pp.cmi +lib/util.cmi: lib/pp.cmi parsing/ast.cmi: parsing/coqast.cmi lib/dyn.cmi interp/genarg.cmi \ library/libnames.cmi kernel/names.cmi lib/pp.cmi interp/topconstr.cmi \ lib/util.cmi @@ -308,11 +307,11 @@ toplevel/recordobj.cmi: library/libnames.cmi proofs/tacexpr.cmo toplevel/searchisos.cmi: library/libobject.cmi kernel/names.cmi \ kernel/term.cmi toplevel/toplevel.cmi: parsing/pcoq.cmi lib/pp.cmi -toplevel/vernac.cmi: parsing/pcoq.cmi lib/util.cmi toplevel/vernacexpr.cmo toplevel/vernacentries.cmi: kernel/environ.cmi pretyping/evd.cmi \ library/libnames.cmi kernel/names.cmi kernel/term.cmi \ interp/topconstr.cmi toplevel/vernacexpr.cmo toplevel/vernacinterp.cmi toplevel/vernacinterp.cmi: proofs/tacexpr.cmo +toplevel/vernac.cmi: parsing/pcoq.cmi lib/util.cmi toplevel/vernacexpr.cmo translate/ppconstrnew.cmi: parsing/coqast.cmi kernel/environ.cmi \ parsing/extend.cmi library/libnames.cmi kernel/names.cmi parsing/pcoq.cmi \ lib/pp.cmi pretyping/rawterm.cmi proofs/tacexpr.cmo kernel/term.cmi \ @@ -329,11 +328,11 @@ contrib/cc/ccalgo.cmi: kernel/names.cmi kernel/term.cmi contrib/cc/ccproof.cmi: contrib/cc/ccalgo.cmi kernel/names.cmi contrib/correctness/past.cmi: kernel/names.cmi contrib/correctness/ptype.cmi \ kernel/term.cmi interp/topconstr.cmi lib/util.cmi -contrib/correctness/pcic.cmi: contrib/correctness/past.cmi \ - pretyping/rawterm.cmi contrib/correctness/pcicenv.cmi: kernel/names.cmi \ contrib/correctness/penv.cmi contrib/correctness/prename.cmi \ kernel/sign.cmi kernel/term.cmi +contrib/correctness/pcic.cmi: contrib/correctness/past.cmi \ + pretyping/rawterm.cmi contrib/correctness/pdb.cmi: kernel/names.cmi contrib/correctness/past.cmi \ contrib/correctness/ptype.cmi contrib/correctness/peffect.cmi: kernel/names.cmi lib/pp.cmi @@ -420,6 +419,11 @@ 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/linear/dpctypes.cmi: kernel/names.cmi kernel/term.cmi +contrib/linear/prove.cmi: contrib/linear/dpctypes.cmi +contrib/linear/subst.cmi: contrib/linear/dpctypes.cmi kernel/names.cmi +contrib/linear/unif.cmi: contrib/linear/dpctypes.cmi \ + contrib/linear/general.cmi contrib/xml/doubleTypeInference.cmi: contrib/xml/acic.cmo kernel/environ.cmi \ pretyping/evd.cmi kernel/term.cmi contrib/xml/xmlcommand.cmi: library/libnames.cmi @@ -443,6 +447,12 @@ dev/top_printers.cmx: parsing/ast.cmx toplevel/cerrors.cmx proofs/clenv.cmx \ pretyping/termops.cmx kernel/univ.cmx doc/parse.cmo: parsing/ast.cmi doc/parse.cmx: parsing/ast.cmx +ide/coqide.cmo: ide/coq.cmi ide/find_phrase.cmo ide/highlight.cmo \ + ide/ideutils.cmo proofs/pfedit.cmi lib/pp_control.cmi ide/preferences.cmo \ + lib/util.cmi toplevel/vernacexpr.cmo +ide/coqide.cmx: ide/coq.cmx ide/find_phrase.cmx ide/highlight.cmx \ + ide/ideutils.cmx proofs/pfedit.cmx lib/pp_control.cmx ide/preferences.cmx \ + lib/util.cmx toplevel/vernacexpr.cmx ide/coq.cmo: toplevel/cerrors.cmi config/coq_config.cmi toplevel/coqtop.cmi \ kernel/environ.cmi pretyping/evarutil.cmi pretyping/evd.cmi \ tactics/hipattern.cmi ide/ideutils.cmo library/lib.cmi kernel/names.cmi \ @@ -459,12 +469,6 @@ ide/coq.cmx: toplevel/cerrors.cmx config/coq_config.cmx toplevel/coqtop.cmx \ proofs/refiner.cmx library/states.cmx proofs/tacmach.cmx kernel/term.cmx \ lib/util.cmx toplevel/vernac.cmx toplevel/vernacentries.cmx \ toplevel/vernacexpr.cmx ide/coq.cmi -ide/coqide.cmo: ide/coq.cmi ide/find_phrase.cmo ide/highlight.cmo \ - ide/ideutils.cmo proofs/pfedit.cmi lib/pp_control.cmi lib/util.cmi \ - toplevel/vernacexpr.cmo -ide/coqide.cmx: ide/coq.cmx ide/find_phrase.cmx ide/highlight.cmx \ - ide/ideutils.cmx proofs/pfedit.cmx lib/pp_control.cmx lib/util.cmx \ - toplevel/vernacexpr.cmx ide/find_phrase.cmo: ide/ideutils.cmo ide/find_phrase.cmx: ide/ideutils.cmx ide/highlight.cmo: ide/ideutils.cmo @@ -595,6 +599,12 @@ kernel/inductive.cmo: kernel/declarations.cmi kernel/environ.cmi \ kernel/inductive.cmx: kernel/declarations.cmx kernel/environ.cmx \ kernel/names.cmx kernel/reduction.cmx kernel/sign.cmx kernel/term.cmx \ kernel/type_errors.cmx kernel/univ.cmx lib/util.cmx kernel/inductive.cmi +kernel/modops.cmo: kernel/declarations.cmi kernel/entries.cmi \ + kernel/environ.cmi kernel/names.cmi lib/pp.cmi kernel/term.cmi \ + kernel/univ.cmi lib/util.cmi kernel/modops.cmi +kernel/modops.cmx: kernel/declarations.cmx kernel/entries.cmx \ + kernel/environ.cmx kernel/names.cmx lib/pp.cmx kernel/term.cmx \ + kernel/univ.cmx lib/util.cmx kernel/modops.cmi kernel/mod_typing.cmo: kernel/declarations.cmi kernel/entries.cmi \ kernel/environ.cmi kernel/modops.cmi kernel/names.cmi \ kernel/reduction.cmi kernel/subtyping.cmi kernel/term_typing.cmi \ @@ -603,12 +613,6 @@ kernel/mod_typing.cmx: kernel/declarations.cmx kernel/entries.cmx \ kernel/environ.cmx kernel/modops.cmx kernel/names.cmx \ kernel/reduction.cmx kernel/subtyping.cmx kernel/term_typing.cmx \ kernel/typeops.cmx kernel/univ.cmx lib/util.cmx kernel/mod_typing.cmi -kernel/modops.cmo: kernel/declarations.cmi kernel/entries.cmi \ - kernel/environ.cmi kernel/names.cmi lib/pp.cmi kernel/term.cmi \ - kernel/univ.cmi lib/util.cmi kernel/modops.cmi -kernel/modops.cmx: kernel/declarations.cmx kernel/entries.cmx \ - kernel/environ.cmx kernel/names.cmx lib/pp.cmx kernel/term.cmx \ - kernel/univ.cmx lib/util.cmx kernel/modops.cmi kernel/names.cmo: lib/hashcons.cmi lib/pp.cmi lib/predicate.cmi lib/util.cmi \ kernel/names.cmi kernel/names.cmx: lib/hashcons.cmx lib/pp.cmx lib/predicate.cmx lib/util.cmx \ @@ -691,34 +695,24 @@ lib/edit.cmo: lib/bstack.cmi lib/pp.cmi lib/util.cmi lib/edit.cmi lib/edit.cmx: lib/bstack.cmx lib/pp.cmx lib/util.cmx lib/edit.cmi lib/explore.cmo: lib/explore.cmi lib/explore.cmx: lib/explore.cmi -lib/gmap.cmo: lib/gmap.cmi -lib/gmap.cmx: lib/gmap.cmi lib/gmapl.cmo: lib/gmap.cmi lib/util.cmi lib/gmapl.cmi lib/gmapl.cmx: lib/gmap.cmx lib/util.cmx lib/gmapl.cmi +lib/gmap.cmo: lib/gmap.cmi +lib/gmap.cmx: lib/gmap.cmi lib/gset.cmo: lib/gset.cmi lib/gset.cmx: lib/gset.cmi lib/hashcons.cmo: lib/hashcons.cmi lib/hashcons.cmx: lib/hashcons.cmi lib/options.cmo: lib/util.cmi lib/options.cmi lib/options.cmx: lib/util.cmx lib/options.cmi -lib/pp.cmo: lib/pp_control.cmi lib/pp.cmi -lib/pp.cmx: lib/pp_control.cmx lib/pp.cmi lib/pp_control.cmo: lib/pp_control.cmi lib/pp_control.cmx: lib/pp_control.cmi +lib/pp.cmo: lib/pp_control.cmi lib/pp.cmi +lib/pp.cmx: lib/pp_control.cmx lib/pp.cmi lib/predicate.cmo: lib/predicate.cmi lib/predicate.cmx: lib/predicate.cmi lib/profile.cmo: lib/profile.cmi lib/profile.cmx: lib/profile.cmi -lib/rtree.cmo: lib/pp.cmi lib/util.cmi lib/rtree.cmi -lib/rtree.cmx: lib/pp.cmx lib/util.cmx lib/rtree.cmi -lib/stamps.cmo: lib/stamps.cmi -lib/stamps.cmx: lib/stamps.cmi -lib/system.cmo: config/coq_config.cmi lib/pp.cmi lib/util.cmi lib/system.cmi -lib/system.cmx: config/coq_config.cmx lib/pp.cmx lib/util.cmx lib/system.cmi -lib/tlm.cmo: lib/gmap.cmi lib/gset.cmi lib/tlm.cmi -lib/tlm.cmx: lib/gmap.cmx lib/gset.cmx lib/tlm.cmi -lib/util.cmo: lib/pp.cmi lib/util.cmi -lib/util.cmx: lib/pp.cmx lib/util.cmi library/declare.cmo: library/decl_kinds.cmo kernel/declarations.cmi \ library/dischargedhypsmap.cmi kernel/entries.cmi kernel/environ.cmi \ library/global.cmi library/impargs.cmi kernel/indtypes.cmi \ @@ -823,6 +817,16 @@ library/states.cmx: library/lib.cmx library/library.cmx library/summary.cmx \ lib/system.cmx library/states.cmi library/summary.cmo: lib/dyn.cmi lib/pp.cmi lib/util.cmi library/summary.cmi library/summary.cmx: lib/dyn.cmx lib/pp.cmx lib/util.cmx library/summary.cmi +lib/rtree.cmo: lib/pp.cmi lib/util.cmi lib/rtree.cmi +lib/rtree.cmx: lib/pp.cmx lib/util.cmx lib/rtree.cmi +lib/stamps.cmo: lib/stamps.cmi +lib/stamps.cmx: lib/stamps.cmi +lib/system.cmo: config/coq_config.cmi lib/pp.cmi lib/util.cmi lib/system.cmi +lib/system.cmx: config/coq_config.cmx lib/pp.cmx lib/util.cmx lib/system.cmi +lib/tlm.cmo: lib/gmap.cmi lib/gset.cmi lib/tlm.cmi +lib/tlm.cmx: lib/gmap.cmx lib/gset.cmx lib/tlm.cmi +lib/util.cmo: lib/pp.cmi lib/util.cmi +lib/util.cmx: lib/pp.cmx lib/util.cmi parsing/argextend.cmo: parsing/ast.cmi interp/genarg.cmi parsing/pcoq.cmi \ parsing/q_coqast.cmo parsing/q_util.cmi lib/util.cmi \ toplevel/vernacexpr.cmo @@ -1831,10 +1835,10 @@ tactics/wcclausenv.cmx: proofs/clenv.cmx kernel/environ.cmx \ pretyping/reductionops.cmx proofs/refiner.cmx kernel/sign.cmx \ proofs/tacmach.cmx kernel/term.cmx pretyping/termops.cmx lib/util.cmx \ tactics/wcclausenv.cmi -tools/coq_vo2xml.cmo: config/coq_config.cmi toplevel/usage.cmi -tools/coq_vo2xml.cmx: config/coq_config.cmx toplevel/usage.cmx tools/coqdep.cmo: config/coq_config.cmi tools/coqdep_lexer.cmo tools/coqdep.cmx: config/coq_config.cmx tools/coqdep_lexer.cmx +tools/coq_vo2xml.cmo: config/coq_config.cmi toplevel/usage.cmi +tools/coq_vo2xml.cmx: config/coq_config.cmx toplevel/usage.cmx tools/gallina.cmo: tools/gallina_lexer.cmo tools/gallina.cmx: tools/gallina_lexer.cmx toplevel/cerrors.cmo: parsing/ast.cmi pretyping/cases.cmi toplevel/himsg.cmi \ @@ -2037,16 +2041,6 @@ toplevel/toplevel.cmx: toplevel/cerrors.cmx library/lib.cmx \ toplevel/vernac.cmx toplevel/vernacexpr.cmx toplevel/toplevel.cmi toplevel/usage.cmo: config/coq_config.cmi toplevel/usage.cmi toplevel/usage.cmx: config/coq_config.cmx toplevel/usage.cmi -toplevel/vernac.cmo: parsing/coqast.cmi parsing/lexer.cmi library/lib.cmi \ - library/library.cmi kernel/names.cmi lib/options.cmi parsing/pcoq.cmi \ - proofs/pfedit.cmi lib/pp.cmi translate/ppvernacnew.cmi library/states.cmi \ - lib/system.cmi lib/util.cmi toplevel/vernacentries.cmi \ - toplevel/vernacexpr.cmo toplevel/vernacinterp.cmi toplevel/vernac.cmi -toplevel/vernac.cmx: parsing/coqast.cmx parsing/lexer.cmx library/lib.cmx \ - library/library.cmx kernel/names.cmx lib/options.cmx parsing/pcoq.cmx \ - proofs/pfedit.cmx lib/pp.cmx translate/ppvernacnew.cmx library/states.cmx \ - lib/system.cmx lib/util.cmx toplevel/vernacentries.cmx \ - toplevel/vernacexpr.cmx toplevel/vernacinterp.cmx toplevel/vernac.cmi toplevel/vernacentries.cmo: tactics/auto.cmi toplevel/class.cmi \ pretyping/classops.cmi toplevel/command.cmi interp/constrextern.cmi \ interp/constrintern.cmi library/decl_kinds.cmo library/declaremods.cmi \ @@ -2107,6 +2101,16 @@ toplevel/vernacinterp.cmx: parsing/ast.cmx parsing/coqast.cmx \ kernel/names.cmx lib/options.cmx lib/pp.cmx proofs/proof_type.cmx \ proofs/tacexpr.cmx tactics/tacinterp.cmx lib/util.cmx \ toplevel/vernacexpr.cmx toplevel/vernacinterp.cmi +toplevel/vernac.cmo: parsing/coqast.cmi parsing/lexer.cmi library/lib.cmi \ + library/library.cmi kernel/names.cmi lib/options.cmi parsing/pcoq.cmi \ + proofs/pfedit.cmi lib/pp.cmi translate/ppvernacnew.cmi library/states.cmi \ + lib/system.cmi lib/util.cmi toplevel/vernacentries.cmi \ + toplevel/vernacexpr.cmo toplevel/vernacinterp.cmi toplevel/vernac.cmi +toplevel/vernac.cmx: parsing/coqast.cmx parsing/lexer.cmx library/lib.cmx \ + library/library.cmx kernel/names.cmx lib/options.cmx parsing/pcoq.cmx \ + proofs/pfedit.cmx lib/pp.cmx translate/ppvernacnew.cmx library/states.cmx \ + lib/system.cmx lib/util.cmx toplevel/vernacentries.cmx \ + toplevel/vernacexpr.cmx toplevel/vernacinterp.cmx toplevel/vernac.cmi translate/ppconstrnew.cmo: parsing/ast.cmi lib/bignat.cmi \ interp/constrextern.cmi interp/constrintern.cmi parsing/coqast.cmi \ lib/dyn.cmi parsing/esyntax.cmi pretyping/evd.cmi interp/genarg.cmi \ @@ -2169,6 +2173,18 @@ contrib/cc/cctac.cmx: contrib/cc/ccalgo.cmx contrib/cc/ccproof.cmx \ lib/pp.cmx parsing/pptactic.cmx proofs/proof_type.cmx proofs/refiner.cmx \ tactics/tacinterp.cmx proofs/tacmach.cmx tactics/tacticals.cmx \ tactics/tactics.cmx kernel/term.cmx lib/util.cmx +contrib/correctness/pcicenv.cmo: library/global.cmi kernel/names.cmi \ + contrib/correctness/past.cmi contrib/correctness/penv.cmi \ + contrib/correctness/pmisc.cmi contrib/correctness/pmonad.cmi \ + contrib/correctness/prename.cmi contrib/correctness/ptype.cmi \ + contrib/correctness/putil.cmi kernel/sign.cmi kernel/term.cmi \ + kernel/univ.cmi contrib/correctness/pcicenv.cmi +contrib/correctness/pcicenv.cmx: library/global.cmx kernel/names.cmx \ + contrib/correctness/past.cmi contrib/correctness/penv.cmx \ + contrib/correctness/pmisc.cmx contrib/correctness/pmonad.cmx \ + contrib/correctness/prename.cmx contrib/correctness/ptype.cmi \ + contrib/correctness/putil.cmx kernel/sign.cmx kernel/term.cmx \ + kernel/univ.cmx contrib/correctness/pcicenv.cmi contrib/correctness/pcic.cmo: kernel/declarations.cmi library/declare.cmi \ pretyping/detyping.cmi kernel/entries.cmi library/global.cmi \ kernel/indtypes.cmi library/libnames.cmi library/nameops.cmi \ @@ -2185,18 +2201,6 @@ contrib/correctness/pcic.cmx: kernel/declarations.cmx library/declare.cmx \ kernel/sign.cmx kernel/term.cmx pretyping/termops.cmx \ interp/topconstr.cmx kernel/typeops.cmx lib/util.cmx \ toplevel/vernacexpr.cmx contrib/correctness/pcic.cmi -contrib/correctness/pcicenv.cmo: library/global.cmi kernel/names.cmi \ - contrib/correctness/past.cmi contrib/correctness/penv.cmi \ - contrib/correctness/pmisc.cmi contrib/correctness/pmonad.cmi \ - contrib/correctness/prename.cmi contrib/correctness/ptype.cmi \ - contrib/correctness/putil.cmi kernel/sign.cmi kernel/term.cmi \ - kernel/univ.cmi contrib/correctness/pcicenv.cmi -contrib/correctness/pcicenv.cmx: library/global.cmx kernel/names.cmx \ - contrib/correctness/past.cmi contrib/correctness/penv.cmx \ - contrib/correctness/pmisc.cmx contrib/correctness/pmonad.cmx \ - contrib/correctness/prename.cmx contrib/correctness/ptype.cmi \ - contrib/correctness/putil.cmx kernel/sign.cmx kernel/term.cmx \ - kernel/univ.cmx contrib/correctness/pcicenv.cmi contrib/correctness/pdb.cmo: library/declare.cmi library/global.cmi \ kernel/names.cmi library/nametab.cmi contrib/correctness/past.cmi \ contrib/correctness/peffect.cmi contrib/correctness/penv.cmi \ @@ -2737,6 +2741,14 @@ contrib/interface/pbp.cmx: interp/coqlib.cmx kernel/environ.cmx \ tactics/tacinterp.cmx proofs/tacmach.cmx tactics/tacticals.cmx \ tactics/tactics.cmx kernel/term.cmx interp/topconstr.cmx \ pretyping/typing.cmx lib/util.cmx contrib/interface/pbp.cmi +contrib/interface/showproof_ct.cmo: contrib/interface/ascent.cmi \ + parsing/esyntax.cmi library/global.cmi toplevel/metasyntax.cmi lib/pp.cmi \ + parsing/printer.cmi contrib/interface/translate.cmi \ + contrib/interface/vtp.cmi contrib/interface/xlate.cmi +contrib/interface/showproof_ct.cmx: contrib/interface/ascent.cmi \ + parsing/esyntax.cmx library/global.cmx toplevel/metasyntax.cmx lib/pp.cmx \ + parsing/printer.cmx contrib/interface/translate.cmx \ + contrib/interface/vtp.cmx contrib/interface/xlate.cmx contrib/interface/showproof.cmo: proofs/clenv.cmi interp/constrintern.cmi \ parsing/coqast.cmi kernel/declarations.cmi kernel/environ.cmi \ pretyping/evd.cmi interp/genarg.cmi library/global.cmi \ @@ -2761,14 +2773,6 @@ contrib/interface/showproof.cmx: proofs/clenv.cmx interp/constrintern.cmx \ pretyping/termops.cmx contrib/interface/translate.cmx \ pretyping/typing.cmx lib/util.cmx toplevel/vernacinterp.cmx \ contrib/interface/showproof.cmi -contrib/interface/showproof_ct.cmo: contrib/interface/ascent.cmi \ - parsing/esyntax.cmi library/global.cmi toplevel/metasyntax.cmi lib/pp.cmi \ - parsing/printer.cmi contrib/interface/translate.cmi \ - contrib/interface/vtp.cmi contrib/interface/xlate.cmi -contrib/interface/showproof_ct.cmx: contrib/interface/ascent.cmi \ - parsing/esyntax.cmx library/global.cmx toplevel/metasyntax.cmx lib/pp.cmx \ - parsing/printer.cmx contrib/interface/translate.cmx \ - contrib/interface/vtp.cmx contrib/interface/xlate.cmx contrib/interface/translate.cmo: contrib/interface/ascent.cmi parsing/ast.cmi \ interp/constrextern.cmi contrib/interface/ctast.cmo kernel/environ.cmi \ pretyping/evarutil.cmi pretyping/evd.cmi library/libobject.cmi \ @@ -2839,6 +2843,66 @@ 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/linear/ccidpc.cmo: proofs/clenv.cmi contrib/linear/dpctypes.cmi \ + kernel/environ.cmi proofs/evar_refiner.cmi library/global.cmi \ + toplevel/himsg.cmi tactics/hipattern.cmi library/libnames.cmi \ + library/nameops.cmi kernel/names.cmi library/nametab.cmi lib/pp.cmi \ + parsing/printer.cmi pretyping/rawterm.cmi pretyping/reductionops.cmi \ + kernel/sign.cmi tactics/tacinterp.cmi proofs/tacmach.cmi \ + tactics/tacticals.cmi tactics/tactics.cmi kernel/term.cmi \ + pretyping/termops.cmi lib/util.cmi +contrib/linear/ccidpc.cmx: proofs/clenv.cmx contrib/linear/dpctypes.cmx \ + kernel/environ.cmx proofs/evar_refiner.cmx library/global.cmx \ + toplevel/himsg.cmx tactics/hipattern.cmx library/libnames.cmx \ + library/nameops.cmx kernel/names.cmx library/nametab.cmx lib/pp.cmx \ + parsing/printer.cmx pretyping/rawterm.cmx pretyping/reductionops.cmx \ + kernel/sign.cmx tactics/tacinterp.cmx proofs/tacmach.cmx \ + tactics/tacticals.cmx tactics/tactics.cmx kernel/term.cmx \ + pretyping/termops.cmx lib/util.cmx +contrib/linear/dpc.cmo: contrib/linear/ccidpc.cmo toplevel/cerrors.cmi \ + parsing/egrammar.cmi interp/genarg.cmi parsing/pcoq.cmi lib/pp.cmi \ + parsing/pptactic.cmi proofs/proof_trees.cmi contrib/linear/prove.cmi \ + proofs/refiner.cmi tactics/tacinterp.cmi proofs/tacmach.cmi \ + tactics/tacticals.cmi tactics/tactics.cmi lib/util.cmi +contrib/linear/dpc.cmx: contrib/linear/ccidpc.cmx toplevel/cerrors.cmx \ + parsing/egrammar.cmx interp/genarg.cmx parsing/pcoq.cmx lib/pp.cmx \ + parsing/pptactic.cmx proofs/proof_trees.cmx contrib/linear/prove.cmx \ + proofs/refiner.cmx tactics/tacinterp.cmx proofs/tacmach.cmx \ + tactics/tacticals.cmx tactics/tactics.cmx lib/util.cmx +contrib/linear/dpctypes.cmo: kernel/names.cmi kernel/term.cmi \ + contrib/linear/dpctypes.cmi +contrib/linear/dpctypes.cmx: kernel/names.cmx kernel/term.cmx \ + contrib/linear/dpctypes.cmi +contrib/linear/general.cmo: contrib/linear/general.cmi +contrib/linear/general.cmx: contrib/linear/general.cmi +contrib/linear/graph.cmo: contrib/linear/graph.cmi +contrib/linear/graph.cmx: contrib/linear/graph.cmi +contrib/linear/kwc.cmo: contrib/linear/dpctypes.cmi \ + contrib/linear/general.cmi contrib/linear/graph.cmi kernel/names.cmi \ + contrib/linear/subst.cmi contrib/linear/unif.cmi lib/util.cmi +contrib/linear/kwc.cmx: contrib/linear/dpctypes.cmx \ + contrib/linear/general.cmx contrib/linear/graph.cmx kernel/names.cmx \ + contrib/linear/subst.cmx contrib/linear/unif.cmx lib/util.cmx +contrib/linear/lk_proofs.cmo: contrib/linear/dpctypes.cmi \ + contrib/linear/general.cmi kernel/names.cmi contrib/linear/subst.cmi \ + contrib/linear/unif.cmi +contrib/linear/lk_proofs.cmx: contrib/linear/dpctypes.cmx \ + contrib/linear/general.cmx kernel/names.cmx contrib/linear/subst.cmx \ + contrib/linear/unif.cmx +contrib/linear/prove.cmo: contrib/linear/dpctypes.cmi contrib/linear/kwc.cmo \ + contrib/linear/lk_proofs.cmo contrib/linear/prove.cmi +contrib/linear/prove.cmx: contrib/linear/dpctypes.cmx contrib/linear/kwc.cmx \ + contrib/linear/lk_proofs.cmx contrib/linear/prove.cmi +contrib/linear/subst.cmo: contrib/linear/dpctypes.cmi \ + contrib/linear/general.cmi kernel/names.cmi contrib/linear/subst.cmi +contrib/linear/subst.cmx: contrib/linear/dpctypes.cmx \ + contrib/linear/general.cmx kernel/names.cmx contrib/linear/subst.cmi +contrib/linear/unif.cmo: contrib/linear/dpctypes.cmi \ + contrib/linear/general.cmi library/nameops.cmi contrib/linear/subst.cmi \ + contrib/linear/unif.cmi +contrib/linear/unif.cmx: contrib/linear/dpctypes.cmx \ + contrib/linear/general.cmx library/nameops.cmx contrib/linear/subst.cmx \ + contrib/linear/unif.cmi contrib/omega/coq_omega.cmo: parsing/ast.cmi proofs/clenv.cmi \ kernel/closure.cmi tactics/contradiction.cmi interp/coqlib.cmi \ kernel/declarations.cmi library/declare.cmi kernel/environ.cmi \ @@ -2941,12 +3005,12 @@ contrib/romega/refl_omega.cmx: parsing/ast.cmx tactics/auto.cmx \ proofs/proof_type.cmx kernel/reduction.cmx kernel/sign.cmx \ proofs/tacmach.cmx tactics/tacticals.cmx tactics/tactics.cmx \ kernel/term.cmx lib/util.cmx -contrib/xml/acic.cmo: kernel/names.cmi kernel/term.cmi -contrib/xml/acic.cmx: kernel/names.cmx kernel/term.cmx contrib/xml/acic2Xml.cmo: contrib/xml/acic.cmo contrib/xml/cic2acic.cmo \ kernel/names.cmi kernel/term.cmi lib/util.cmi contrib/xml/xml.cmi contrib/xml/acic2Xml.cmx: contrib/xml/acic.cmx contrib/xml/cic2acic.cmx \ kernel/names.cmx kernel/term.cmx lib/util.cmx contrib/xml/xml.cmx +contrib/xml/acic.cmo: kernel/names.cmi kernel/term.cmi +contrib/xml/acic.cmx: kernel/names.cmx kernel/term.cmx contrib/xml/cic2acic.cmo: contrib/xml/acic.cmo library/declare.cmi \ library/dischargedhypsmap.cmi contrib/xml/doubleTypeInference.cmi \ kernel/environ.cmi pretyping/evarutil.cmi pretyping/evd.cmi \ @@ -3001,8 +3065,6 @@ contrib/xml/proofTree2Xml.cmx: contrib/xml/acic.cmx contrib/xml/acic2Xml.cmx \ contrib/xml/xml.cmx contrib/xml/unshare.cmo: contrib/xml/unshare.cmi contrib/xml/unshare.cmx: contrib/xml/unshare.cmi -contrib/xml/xml.cmo: contrib/xml/xml.cmi -contrib/xml/xml.cmx: contrib/xml/xml.cmi contrib/xml/xmlcommand.cmo: contrib/xml/acic.cmo contrib/xml/acic2Xml.cmo \ contrib/xml/cic2acic.cmo library/decl_kinds.cmo kernel/declarations.cmi \ library/declare.cmi kernel/environ.cmi pretyping/evd.cmi \ @@ -3029,6 +3091,8 @@ contrib/xml/xmlentries.cmx: toplevel/cerrors.cmx parsing/egrammar.cmx \ parsing/extend.cmx interp/genarg.cmx parsing/pcoq.cmx lib/pp.cmx \ parsing/pptactic.cmx tactics/tacinterp.cmx lib/util.cmx \ toplevel/vernacinterp.cmx contrib/xml/xmlcommand.cmx +contrib/xml/xml.cmo: contrib/xml/xml.cmi +contrib/xml/xml.cmx: contrib/xml/xml.cmi tactics/tauto.cmo: parsing/grammar.cma tactics/tauto.cmx: parsing/grammar.cma tactics/newtauto.cmo: parsing/grammar.cma @@ -3067,6 +3131,10 @@ contrib/jprover/jprover.cmo: parsing/grammar.cma contrib/jprover/jprover.cmx: parsing/grammar.cma contrib/cc/cctac.cmo: parsing/grammar.cma contrib/cc/cctac.cmx: parsing/grammar.cma +contrib/linear/ccidpc.cmo: parsing/grammar.cma +contrib/linear/ccidpc.cmx: parsing/grammar.cma +contrib/linear/dpc.cmo: parsing/grammar.cma +contrib/linear/dpc.cmx: parsing/grammar.cma parsing/lexer.cmo: parsing/lexer.cmx: parsing/q_util.cmo: diff --git a/.depend.camlp4 b/.depend.camlp4 index c8dddc1328..9fc97cdd1d 100644 --- a/.depend.camlp4 +++ b/.depend.camlp4 @@ -17,6 +17,8 @@ contrib/extraction/g_extraction.ml: parsing/grammar.cma contrib/xml/xmlentries.ml: parsing/grammar.cma contrib/jprover/jprover.ml: parsing/grammar.cma contrib/cc/cctac.ml: parsing/grammar.cma +contrib/linear/ccidpc.ml: parsing/grammar.cma +contrib/linear/dpc.ml: parsing/grammar.cma parsing/lexer.ml: parsing/q_util.ml: parsing/q_coqast.ml: @@ -44,7 +44,7 @@ LOCALINCLUDES=-I config -I tools -I scripts -I lib -I kernel -I library \ -I contrib/ring -I contrib/xml \ -I contrib/extraction -I contrib/correctness \ -I contrib/interface -I contrib/fourier \ - -I contrib/jprover -I contrib/cc + -I contrib/jprover -I contrib/cc -I contrib/linear MLINCLUDES=$(LOCALINCLUDES) -I $(MYCAMLP4LIB) @@ -347,11 +347,24 @@ JPROVERCMO=\ CCCMO=contrib/cc/ccalgo.cmo contrib/cc/ccproof.cmo contrib/cc/cctac.cmo -ML4FILES += contrib/jprover/jprover.ml4 contrib/cc/cctac.ml4 +LINEARCMO=\ + contrib/linear/dpctypes.cmo \ + contrib/linear/general.cmo \ + contrib/linear/graph.cmo \ + contrib/linear/subst.cmo \ + contrib/linear/unif.cmo \ + contrib/linear/lk_proofs.cmo \ + contrib/linear/ccidpc.cmo \ + contrib/linear/kwc.cmo \ + contrib/linear/prove.cmo \ + contrib/linear/dpc.cmo + +ML4FILES += contrib/jprover/jprover.ml4 contrib/cc/cctac.ml4 \ + contrib/linear/ccidpc.ml4 contrib/linear/dpc.ml4 CONTRIB=$(OMEGACMO) $(ROMEGACMO) $(RINGCMO) $(FIELDCMO) \ $(FOURIERCMO) $(EXTRACTIONCMO) $(JPROVERCMO) $(XMLCMO) \ - $(CORRECTNESSCMO) $(CCCMO) $(USERCMO) + $(CORRECTNESSCMO) $(CCCMO) $(LINEARCMO) $(USERCMO) CMA=$(CLIBS) $(CAMLP4OBJS) CMXA=$(CMA:.cma=.cmxa) diff --git a/contrib/linear/ccidpc.ml4 b/contrib/linear/ccidpc.ml4 new file mode 100755 index 0000000000..1e3ec39e48 --- /dev/null +++ b/contrib/linear/ccidpc.ml4 @@ -0,0 +1,371 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) + +(*i camlp4deps: "parsing/grammar.cma" i*) + +(*i $Id$ i*) + +open Dpctypes + +open Names +open Nameops +open Pp +open Term +open Termops +open Environ +open Himsg +open Tacmach +open Reductionops +open Clenv +open Tactics +open Hipattern +open Tacticals +open Tactics +open Util +open Sign +open Tacinterp + +(* +let mmk = make_module_marker ["#Prelude.obj"] + +let and_pattern = put_pat mmk "(and ? ?)" +let or_pattern = put_pat mmk "(or ? ?)" +let not_pattern = put_pat mmk "(not ?)" +let exist_pattern = put_pat mmk "(ex ? ?)" + +let and_head = put_pat mmk "and" +let or_head = put_pat mmk "or" +let not_head = put_pat mmk "not" +let exist_head = put_pat mmk "ex" + +*) + +let op2bool=function Some _->true |None->false + +let match_with_imp_term t = + match kind_of_term t with + Prod (_,a,b)-> + if not (dependent (mkRel 1) b) then + Some (a,b) else None + | _-> None + +let is_imp_term t=op2bool (match_with_imp_term t) + +let match_with_forall_term t = + match kind_of_term (whd_betaiota t) with + Prod (x,a,b)-> + if dependent (mkRel 1) b then Some (x,a,b) else None + | _ -> None + +let is_forall_term t=op2bool (match_with_forall_term t) + +let constr_of_string s () = + Libnames.constr_of_reference (Nametab.locate (Libnames.qualid_of_string s)) + +let id_ex=constr_of_string "Coq.Init.Logic.ex" + +let match_with_exist_term t= + match kind_of_term t with + App(t,v)-> + if t=id_ex () && (Array.length v)=2 then + match kind_of_term v.(1) with + Lambda(na,a,b)->Some(na,a,b) + |_->assert false + else None + | _->None + +let is_exist_term t=op2bool (match_with_exist_term t) + +let id_not=constr_of_string "Coq.Init.Logic.not" + +let id_false=constr_of_string "Coq.Init.Logic.False" + +let match_with_not_term t= + match kind_of_term t with + App(t,v)-> + if t=id_not () && (Array.length v)=1 then + Some v.(0) + else None + | Prod(_,a,b)-> + if b=id_false () then + Some a + else None + | _->None + + +let is_not_term t=op2bool (match_with_not_term t) + +let ctr = ref 0 + +let gen_ident id = make_ident (atompart_of_id id) (incr ctr;Some !ctr) + +let gen_name a na = + let (Name id) = (named_hd Environ.empty_env a na) + in gen_ident id + +let dpc_of_cci_term lid = + let rec tradrec cciterm = + let (hd,args) = whd_betaiota_stack cciterm in + let dpcargs = List.map tradrec args + in (match kind_of_term hd with + Var id -> if dpcargs=[] then VAR id + else if List.mem id lid + then failwith "dpc_of_cci_term (not first order)" + else APP (VAR id :: dpcargs) + + | (Const _ | Ind _ | Construct _) as t + -> if dpcargs=[] then GLOB (CN hd) + else APP (GLOB (CN hd) :: dpcargs) + + | _ -> errorlabstrm "dpc_of_cci_term" + (str "Not a first order formula")) + in tradrec + + +let cci_of_dpc_term tradsign sign = + let rec tradrec = function + VAR id -> + (try let (_,t,_)=lookup_named id tradsign in + match t with + Some t'-> t' + |None ->Term.mkVar id + with Not_found->Term.mkVar id) + | GLOB (ID id) -> Term.mkVar id + | GLOB (CN t) -> t + | APP (t::dpcargs) -> + let t' = tradrec t in + Term.applist(t', List.map tradrec dpcargs) + in tradrec + + +let dpc_of_cci_fmla gls cciterm = + let rec tradrec lid cciterm = + match match_with_conjunction cciterm with + Some (_,[a;b])->Conj(tradrec lid a,tradrec lid b) + |_-> + (match match_with_disjunction cciterm with + Some (_,[a;b])->Disj(tradrec lid a,tradrec lid b) + |_-> + (match match_with_not_term cciterm with + Some a->Neg(tradrec lid a) + |_-> + (match match_with_imp_term cciterm with + Some (a,b)->Imp (tradrec lid a,tradrec lid (pop b)) + |_-> + (match match_with_forall_term cciterm with + Some ((na,a,b) as trp)-> + let id = gen_name a na in + let f=mkApp(mkLambda trp,[|mkVar id|]) in + ForAll(id,tradrec (id::lid) f) + |_-> + (match match_with_exist_term cciterm with + Some ((na,a,b)as trp)-> + let id = gen_name a na in + let f=mkApp(mkLambda trp,[|mkVar id|]) in + Exists(id,tradrec (id::lid) f) + |_-> + let (hd,args) = whd_betaiota_stack cciterm in + let dpcargs = List.map (dpc_of_cci_term lid) args + in (match kind_of_term hd with + Var id -> if List.mem id lid + then errorlabstrm "dpc_of_cci_fmla" + (str "Quantification over a predicate") + else Atom((ID id,0),dpcargs) + | Ind _ | Construct _ | Const _ + -> Atom( (CN hd,0) , dpcargs) + | _ -> errorlabstrm "dpc_of_cci_flma" + ((Printer.prterm_env + (Global.env_of_context (pf_hyps gls)) hd) ++ + (spc ()) ++ + (str "is not an atomic predicate")))))))) + in tradrec [] (whd_betaiota cciterm) + +let rec index x=function + []-> raise Not_found + | y::q-> if x=y then 0 else 1+(index x q) + + +let rec alpha_term bl1 bl2 p_0 p_1 = + match p_0,p_1 with + ((VAR id1), (VAR id2)) -> + if not (List.mem id1 bl1) then + id1=id2 + else + index id1 bl1 = index id2 bl2 + | ((GLOB t1), (GLOB t2)) -> t1=t2 + | ((APP al1), (APP al2)) -> + List.for_all2 (alpha_term bl1 bl2) al1 al2 + | (_, _) -> false + + +let forAllI gls=if is_forall_term (pf_concl gls) then + intro gls else tclFAIL 0 gls + +let forAllE id t gls = + let rgl=pf_whd_betadeltaiota gls (pf_type_of gls (mkVar id)) in + if is_forall_term rgl then + generalize [mkApp (mkVar id,[|t|])] gls else tclFAIL 0 gls + +let existE id gls = + let (_,_,t)=lookup_named id (pf_hyps gls) in + if is_exist_term t then + ((tclTHEN (simplest_elim (mkVar id)) + (tclDO 2 (dImp None)))) gls + else tclFAIL 0 gls + +let negE id gls = + let (_,_,t)=lookup_named id (pf_hyps gls) in + if is_not_term t then + (simplest_elim (mkVar id)) gls + else tclFAIL 0 gls + +(*t exist_intro_head = put_pat mmk "ex_intro"*) + +let existI t gls = + let (wc,kONT) = Evar_refiner.startWalk gls in + let clause = mk_clenv_hnf_constr_type_of wc (pf_concl gls) in + let clause' = clenv_constrain_missing_args [t] clause + in res_pf kONT clause' gls + + +let rec alpha_fmla bl1 bl2 p_0 p_1 = + match p_0,p_1 with + ((Atom((cn1,_),al1)), (Atom((cn2,_),al2))) -> + cn1=cn2 & List.for_all2 (alpha_term bl1 bl2) al1 al2 + | ((Conj(a1,b1)),(Conj(a2,b2))) -> + alpha_fmla bl1 bl2 a1 a2 & alpha_fmla bl1 bl2 b1 b2 + + | ((Disj(a1,b1)),(Disj(a2,b2))) -> + alpha_fmla bl1 bl2 a1 a2 & alpha_fmla bl1 bl2 b1 b2 + + | ((Imp(a1,b1)),(Imp(a2,b2))) -> + alpha_fmla bl1 bl2 a1 a2 & alpha_fmla bl1 bl2 b1 b2 + + | ((Neg(a1)), (Neg(a2))) -> alpha_fmla bl1 bl2 a1 a2 + + | ((ForAll(x1,a1)), (ForAll(x2,a2))) -> + alpha_fmla (x1::bl1) (x2::bl2) a1 a2 + + | ((Exists(x1,a1)), (Exists(x2,a2))) -> + alpha_fmla (x1::bl1) (x2::bl2) a1 a2 + + | (_, _) -> false + +let alpha_eq (kspine,m) (jspine,n) = alpha_fmla kspine jspine m n + +let first_pred p = + let rec firstrec = function + [] -> error "first_pred" + | h::t -> if p h then h else firstrec t + in firstrec + + +let find_fmla_left (kspine,f) (jspine,gl) = + let ids = pf_ids_of_hyps gl + and sign= pf_hyps gl in + first_pred + (fun id -> + let (_,_,t)=lookup_named id sign in + ( try alpha_eq (kspine,f) + (jspine,dpc_of_cci_fmla gl t) + with _ -> false) + ) ids + + +let onNthClause tac n gls = + let cls = nth_clause n gls + in onClause tac cls gls + + +let elimTypeFalse gls = + (elim_type (pf_global gls (id_of_string "False"))) gls + + +let rec tradpf kspine jspine dpcpf gls = + match dpcpf with + + Proof2(_,_,Axiom2 f) -> + let id = find_fmla_left (kspine,f) (jspine,gls) + in exact_no_check (mkVar id) gls + + | Proof2(_,_,LWeakening2(_,pf)) -> trad kspine jspine pf gls + + | Proof2(_,_,RWeakening2(_,pf)) -> + ( (tclTHEN (elimTypeFalse) (tradpf kspine jspine pf)) ) gls + + | Proof2(_,_,RConj2(f1,pf1,f2,pf2)) -> + ((tclTHENS (dAnd None) ([trad kspine jspine pf1; + trad kspine jspine pf2]))) gls + + | Proof2(_,_,LConj2(f1,f2,pf)) -> + let id = find_fmla_left (kspine,Conj(f1,f2)) (jspine,gls) + in ((tclTHEN (dAnd (Some id)) ((trad kspine jspine pf)))) gls + + | Proof2(_,_,LDisj2(f1,pf1,f2,pf2)) -> + let id = find_fmla_left (kspine,Disj(f1,f2)) (jspine,gls) + in (match pf1 with + Proof2(_,[],_) -> ((tclTHENS (orE id) + ([ ((tclTHEN (elimTypeFalse) (trad kspine jspine pf1))); + trad kspine jspine pf2]))) gls + | _ -> ((tclTHENS (orE id) + ([ trad kspine jspine pf1; + ((tclTHEN (elimTypeFalse) (trad kspine jspine pf2)))]))) gls + ) + + | Proof2(_,_,RImp2(f1,f2,pf)) -> + ((tclTHEN (dImp None) ((trad kspine jspine pf)))) gls + + | Proof2(_,_,LImp2(f1,pf1,f2,pf2)) -> + let id = find_fmla_left (kspine,Imp(f1,f2)) (jspine,gls) + in ((tclTHENS (dImp (Some id)) + ([trad kspine jspine pf2; + trad kspine jspine pf1]))) gls + + | Proof2(_,_,RForAll2(kid,f,pf)) -> + ((tclTHEN forAllI + ((onLastHyp (fun jid -> + trad (kid::kspine) (jid::jspine) pf))))) gls + + | Proof2(_,_,LForAll2(kid,kterm,f,pf)) -> + let jterm = cci_of_dpc_term (pf_hyps gls) (kspine,jspine) kterm in + let id = find_fmla_left (kspine,ForAll(kid,f)) (jspine,gls) + in ((tclTHEN (forAllE id jterm) + (trad kspine jspine pf))) gls + + | Proof2(_,_,LExists2(kid,f,pf)) -> + let id = find_fmla_left (kspine,Exists(kid,f)) (jspine,gls) + in ((tclTHEN (existE id) + ((onNthClause (fun (Some jid) -> + trad (kid::kspine) (jid::jspine) pf) + (-2))))) gls + + | Proof2(_,_,RExists2(kid,kterm,f,pf)) -> + let jterm = cci_of_dpc_term (pf_hyps gls) (kspine,jspine) kterm + in ((tclTHEN (existI jterm) (tradpf kspine jspine pf))) gls + + | Proof2(_,_,RDisj2(f1,f2,Proof2(_,_,RWeakening2(f3,pf)))) -> + if alpha_eq (kspine,f1) (kspine,f3) then + ((tclTHEN (right Rawterm.NoBindings) (tradpf kspine jspine pf))) gls + else if alpha_eq (kspine,f2) (kspine,f3) then + ((tclTHEN (left Rawterm.NoBindings) (tradpf kspine jspine pf))) gls + else error "Not Intuitionistic, eh?" + + | Proof2(_,_,RNeg2(f,pf)) -> + ((tclTHEN ((tclTHEN (red_in_concl) (Tactics.intro))) (tradpf kspine jspine pf))) gls + + | Proof2(_,_,LNeg2(f,pf)) -> + let id = find_fmla_left (kspine,Neg(f)) (jspine,gls) + in ((tclTHEN (negE id) (tradpf kspine jspine pf))) gls + + | _ -> error "tradpf : Not an intuitionistic proof !" + +and trad kspine jspine dpcpf gls = + tradpf kspine jspine dpcpf gls + + +(* $Id$ *) diff --git a/contrib/linear/dpc.ml4 b/contrib/linear/dpc.ml4 new file mode 100755 index 0000000000..ba7bc884d4 --- /dev/null +++ b/contrib/linear/dpc.ml4 @@ -0,0 +1,64 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) + +(*i camlp4deps: "parsing/grammar.cma" i*) + +(*i $Id$ i*) + +open Pp +open Util + +open Proof_trees +open Tacmach +open Tactics +open Tacinterp +open Tacticals +open Prove +open Ccidpc + +let rec intros_forall gls = + let t = pf_concl gls + in if is_forall_term t + then ((tclTHEN forAllI (intros_forall))) gls + else tclIDTAC gls + +let dPC_nq gls = + let f = dpc_of_cci_fmla gls (pf_concl gls) in + try let pf = prove_f f in + tradpf [] [] pf gls + with Not_provable_in_DPC s -> errorlabstrm "dpc__DPC_nq" + (str "Not provable in Direct Predicate Calculus") + + | No_intuitionnistic_proof n -> errorlabstrm "dpc__DPC_nq" + ((str "Found ") ++ + (str (string_of_int n)) ++ + (str " classical proof(s) but no intuitionnistic one !")) + + +let dPC = + ((tclTHEN (intros_forall) (dPC_nq))) + + +let dPC_l lcom = + (tclTHEN (intros_forall) + (tclTHEN (generalize lcom) (dPC))) + +(* +let dPC_tac = hide_atomic_tactic "DPC" dPC + +let dPC_l_tac = hide_tactic "DPC_l" + (fun lcom -> dPC_l lcom) +*) + +TACTIC EXTEND Linear +[ "Linear" ]->[(dPC)] +|[ "Linear" "with" ne_constr_list(l) ] -> [(dPC_l l)] +END + + + diff --git a/contrib/linear/dpctypes.ml b/contrib/linear/dpctypes.ml new file mode 100644 index 0000000000..b21bd67e4a --- /dev/null +++ b/contrib/linear/dpctypes.ml @@ -0,0 +1,60 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) + +(*i $Id$ *) + + +open Names +open Term + +type constname = + ID of identifier + | SK of identifier + | CN of constr + + +type atom_id = constname * int + +type term = VAR of identifier + | GLOB of constname + | APP of term list + +type formula = Atom of atom_id * (term list) + | Neg of formula + | Imp of formula * formula + | Conj of formula * formula + | Disj of formula * formula + | ForAll of identifier * formula + | Exists of identifier * formula + +type sequent = Seq of formula list + +type sfla = Po of formula + | No of formula + +exception Impossible_case + +type lkproof2 = Proof2 of (formula list) * (formula list) * rule2 + and rule2 = + Axiom2 of formula + | RWeakening2 of formula * lkproof2 + | LWeakening2 of formula * lkproof2 + | RNeg2 of formula * lkproof2 + | LNeg2 of formula * lkproof2 + | RConj2 of formula * lkproof2 * formula * lkproof2 + | LConj2 of formula * formula * lkproof2 + | RDisj2 of formula * formula * lkproof2 + | LDisj2 of formula * lkproof2 * formula * lkproof2 + | RImp2 of formula * formula * lkproof2 + | LImp2 of formula * lkproof2 * formula * lkproof2 + | RForAll2 of identifier * formula * lkproof2 + | LForAll2 of identifier * term * formula * lkproof2 + | RExists2 of identifier * term * formula * lkproof2 + | LExists2 of identifier * formula * lkproof2 + + diff --git a/contrib/linear/dpctypes.mli b/contrib/linear/dpctypes.mli new file mode 100755 index 0000000000..7115cf5199 --- /dev/null +++ b/contrib/linear/dpctypes.mli @@ -0,0 +1,59 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) + +(*i $Id$ *) + +open Names +open Term + +type constname = + ID of identifier + | SK of identifier + | CN of constr + + +type atom_id = constname * int + +type term = VAR of identifier + | GLOB of constname + | APP of term list + +type formula = Atom of atom_id * (term list) + | Neg of formula + | Imp of formula * formula + | Conj of formula * formula + | Disj of formula * formula + | ForAll of identifier * formula + | Exists of identifier * formula + +type sequent = Seq of formula list + +type sfla = Po of formula + | No of formula + +exception Impossible_case + +type lkproof2 = Proof2 of (formula list) * (formula list) * rule2 + and rule2 = + Axiom2 of formula + | RWeakening2 of formula * lkproof2 + | LWeakening2 of formula * lkproof2 + | RNeg2 of formula * lkproof2 + | LNeg2 of formula * lkproof2 + | RConj2 of formula * lkproof2 * formula * lkproof2 + | LConj2 of formula * formula * lkproof2 + | RDisj2 of formula * formula * lkproof2 + | LDisj2 of formula * lkproof2 * formula * lkproof2 + | RImp2 of formula * formula * lkproof2 + | LImp2 of formula * lkproof2 * formula * lkproof2 + | RForAll2 of identifier * formula * lkproof2 + | LForAll2 of identifier * term * formula * lkproof2 + | RExists2 of identifier * term * formula * lkproof2 + | LExists2 of identifier * formula * lkproof2 + +(* $Id$ *) diff --git a/contrib/linear/general.ml b/contrib/linear/general.ml new file mode 100755 index 0000000000..5b998c5afa --- /dev/null +++ b/contrib/linear/general.ml @@ -0,0 +1,41 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) + +(*i $Id$ *) + +let substract l1 l2= + let rec sub_aux=function + []->[] + | x::q->if List.mem x l2 then sub_aux q else x::(sub_aux q) + in sub_aux l1 + +let rec union l1=function + []->l1 + | x::q-> if List.mem x l1 then union l1 q else x::(union l1 q) + +(*** glue : make the concatenation of the lists of a lists list *****) + +let rec glue = function + (l::ll) -> union l (glue ll) + | [] -> [] + +(*** disjoint l1 l2 : returns true if the lists l1 and l2 are disjoint ******) + +let disjoint l1 l2 = + let rec disjoint_rec = function + (a::ll1) -> if List.mem a l2 then false else disjoint_rec ll1 + | [] -> true + in disjoint_rec l1 + +(*** such_that : 'a list -> ('a -> bool) -> 'a list *******) + +let such_that l p = + let rec such_rec = function + a::ll -> if (p a) then a::(such_rec ll) else such_rec ll + | [] -> [] + in such_rec l diff --git a/contrib/linear/general.mli b/contrib/linear/general.mli new file mode 100755 index 0000000000..8acf596613 --- /dev/null +++ b/contrib/linear/general.mli @@ -0,0 +1,16 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) + +(*i $Id$ i*) + +val substract : 'a list -> 'a list -> 'a list +val union : 'a list -> 'a list -> 'a list +val glue : 'a list list -> 'a list +val disjoint : 'a list -> 'a list -> bool +val such_that : 'a list -> ('a -> bool) -> 'a list + diff --git a/contrib/linear/graph.ml b/contrib/linear/graph.ml new file mode 100755 index 0000000000..94ddcbd97d --- /dev/null +++ b/contrib/linear/graph.ml @@ -0,0 +1,70 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) + +(*i $Id$ i*) + +(* Given a DIRECTED graph G represented by a list of + (x , [neighbours of x]) + then (have_cycle G) returns true if G has a nontrivial cycle. + Remark : G is not necessarly connected. *******) + +type mark = NotMarked | OnThePath | AlreadyVisited;; + +let df_cycle v marks g = + let rec df_cycle_rec x = + (List.assoc x marks) := OnThePath; + let nx = List.assoc x g + in let nb_marks = + List.fold_left (fun s x -> if !(List.assoc x marks)=OnThePath + then s+1 else s) 0 nx + in if nb_marks>0 + then true + else let isc = List.fold_left (fun r y -> if r then true + else if !(List.assoc y marks)=AlreadyVisited + then false + else (df_cycle_rec y)) false nx + in if isc then true + else ((List.assoc x marks) := AlreadyVisited; false) + and df_init ls = match ls with + (s::lls) -> if (!(List.assoc s marks)=NotMarked) + & ((List.length (List.assoc s g))>0) + then (if df_cycle_rec s + then true + else df_init lls) + else df_init lls + | [] -> false + in df_init v;; + +let have_cycle g = + let v = List.map (fun (x,_) -> x) g + in let marks = List.map (fun x -> (x,ref NotMarked)) v + in if List.length g<2 + then false + else let x0 = fst (List.hd g) + in df_cycle v marks g;; + +(* Examples... + + have_cycle [(1,[2;3]); (2,[3]); (3,[])];; (false) + + have_cycle [(1,[2;3]); (2,[1;3]); (3,[1;2])];; (true) + + have_cycle [(1 , [6]); + (2 , [3;4;5]); + (3 , [2;5]); + (4 , [2]); + (5 , [2;3]); + (6 , [1])];; (true) + + have_cycle [(2,[3]); (4,[]); (1,[4]); (3,[])];; (false) + + have_cycle [(3,[1;2]); (4,[]); (2,[4]); (1,[4])];; (false) + +*) + + diff --git a/contrib/linear/graph.mli b/contrib/linear/graph.mli new file mode 100755 index 0000000000..63ae558e54 --- /dev/null +++ b/contrib/linear/graph.mli @@ -0,0 +1,12 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) + +(*i $Id$ i*) + +val have_cycle : ('a * 'a list) list -> bool;; + diff --git a/contrib/linear/kwc.ml b/contrib/linear/kwc.ml new file mode 100755 index 0000000000..13a9b85400 --- /dev/null +++ b/contrib/linear/kwc.ml @@ -0,0 +1,233 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) + +(*i $Id$ i*) + +open Util +open Names + +open General +open Dpctypes +open Subst +open Unif +open Graph + +(* Herbrand form *************) + +let h_fun v ex f = + let lt = List.map (fun x -> VAR(x)) ex + in subst v (APP (GLOB (SK v)::lt)) f + +let free_her fv f = + let rec fh_rec f = function + v::ll -> let f0 = subst v (APP [GLOB (SK v)]) f + in fh_rec f0 ll + | [] -> f + in fh_rec f fv + +let herbrand f = + let rec h_rec ex sign f = match f with + ForAll(v,f1) -> if sign then (h_rec ex sign (h_fun v ex f1)) + else (h_rec (v::ex) sign f1) + | Exists(v,f1) -> if sign then (h_rec (v::ex) sign f1) + else (h_rec ex sign (h_fun v ex f1)) + | Neg(f1) -> let (e,h) = (h_rec ex ((not (sign))) f1) + in (e , Neg h) + | Atom(s,lt) -> (ex,Atom(s,lt)) + | Imp(f1,f2) -> (let (ex1,h1) = (h_rec ex ((not (sign))) f1) + and (ex2,h2) = (h_rec ex sign f2) + in (union ex1 ex2,Imp(h1,h2))) + | Conj(f1,f2) -> (let (ex1,h1) = (h_rec ex sign f1) + and (ex2,h2) = (h_rec ex sign f2) + in (union ex1 ex2,Conj(h1,h2))) + | Disj(f1,f2) -> (let (ex1,h1) = (h_rec ex sign f1) + and (ex2,h2) = (h_rec ex sign f2) + in (union ex1 ex2,Disj(h1,h2))) + in let (ex,f0) = h_rec [] true f + in let fv = free_var_formula f + in (ex,free_her fv f0) + +let separate f = + let n = ref 0 + in let rec sep_rec f = match f with + Atom((s,0),lt) -> n := !n+1; + Atom((s,!n),lt) + | Atom((s,_),_) -> anomaly "separate" + | Neg(f1) -> Neg(sep_rec f1) + | ForAll(s,f1) -> ForAll(s,sep_rec f1) + | Exists(s,f1) -> Exists(s,sep_rec f1) + | Imp(f1,f2)-> Imp(sep_rec f1,sep_rec f2) + | Conj(f1,f2) -> Conj(sep_rec f1,sep_rec f2) + | Disj(f1,f2) -> Disj(sep_rec f1,sep_rec f2) + in sep_rec f + +(* Searching for paths... *********) + +let lit_conj f = + let rec lc_rec sign = function + Atom(_,_) as a -> if sign then ([a],[],[]) else ([],[a],[]) + | Neg(f1) -> lc_rec ((not (sign))) f1 + | Conj(f1,f2) -> let (p1,n1,c1) = lc_rec sign f1 + and (p2,n2,c2) = lc_rec sign f2 + in let c = if sign then [((f1,f2),(p1@n1,p2@n2))] + else [] + in (p1@p2,n1@n2,c@c1@c2) + | Disj(f1,f2) -> let (p1,n1,c1) = lc_rec sign f1 + and (p2,n2,c2) = lc_rec sign f2 + in let c = if sign then [] + else [((f1,f2),(p1@n1,p2@n2))] + in (p1@p2,n1@n2,c@c1@c2) + | Imp(f1,f2) -> let (p1,n1,c1) = lc_rec ((not (sign))) f1 + and (p2,n2,c2) = lc_rec sign f2 + in let c = if sign then [] + else [((f1,f2),(p1@n1,p2@n2))] + in (p1@p2,n1@n2,c@c1@c2) + | _ -> raise Impossible_case + in lc_rec true f + + +(* Finding all matches ********) + +let mb p q = + let rec mb_rec = function + (_,(lf1,lf2))::ll -> ((not(( ((List.mem p lf1) & (List.mem q lf2)) + or ((List.mem q lf1) & (List.mem p lf2))))) ) + & (mb_rec ll) + | [] -> true + in mb_rec + + +let all_matches pos neg lcj = + let rec all_matches_p (x,y) = function + ((Atom (x_0,x_1)) as q::neg1) -> + let lm = try [((Atom (x,y)),q,unif_atoms (x,y) (x_0,x_1))] + with Not_unifiable -> [] + in if mb (Atom (x,y)) q lcj then lm@(all_matches_p (x,y) neg1) + else (all_matches_p (x,y) neg1) + | _ -> [] + and all_matches_rec = function + ((Atom (x_0,x_1))::pos1) -> (all_matches_p (x_0,x_1) neg)@(all_matches_rec pos1) + | _ -> [] + in all_matches_rec pos + +(* combine_path P L : returns the least path containing all the matches + in P and L. If no such path exists, it raises + CP_error *********) + +exception CP_error + +let rec lit_unicity = function + (p::ll) -> if List.mem p ll then false else lit_unicity ll + | [] -> true + +let combine_path (m1,u1) (m2,u2) = + let lm = union m1 m2 + in let llt = List.map (fun (p,q,_) -> [p;q]) lm + in let lt = List.flatten llt + in if lit_unicity lt + then let u = try up u1 u2 with Up_error -> raise CP_error + in (lm , u) + else raise CP_error + +(* lit_in_matches : formula list -> (match list) -> bool *****) + +let lit_in_matches lF ml = + let rec lim_rec = function + ((p,q,_)::mmll) -> if (List.mem p lF) or (List.mem q lF) + then true + else lim_rec mmll + | [] -> false + in lim_rec ml + +(* 16.III.94 *********) +(* Simple Depth First Search (p.138) *******) +(* NB : path = match list * unifier ********) + +let rec matches_pos p = function + ((p1,q,u) as m::mM) -> if p=p1 + then [([m] , u)]@(matches_pos p mM) + else matches_pos p mM + | [] -> [] + +let rec matches_neg q = function + ((p,q1,u) as m::mM) -> if q=q1 + then [([m] , u)]@(matches_neg q mM) + else matches_neg q mM + | [] -> [] + +let uncovered (ml,_) lcj = + let rec uncov_rec = function + (((f1,f2),(lf1,lf2))::llccjj) -> + let sat1 = lit_in_matches lf1 ml + in let sat2 = lit_in_matches lf2 ml + in if sat1 & ((not (sat2))) + then (f2,lf2)::(uncov_rec llccjj) + else if sat2 & ((not (sat1))) + then (f1,lf1)::(uncov_rec llccjj) + else (uncov_rec llccjj) + | [] -> [] + in uncov_rec lcj + +let paths pos neg m lcj = + let rec paths_rec = function + ((_,_,u) as m_0::mM) -> (extend ([m_0],u))@(paths_rec mM) + | [] -> [] + and extension p (f1,lf1) = + let lm = glue (List.map (fun x -> if List.mem x pos + then matches_pos x m + else matches_neg x m) lf1) + in let rec ext_rec = function + (l::ll) ->( try (combine_path p l)::(ext_rec ll) + with CP_error -> ext_rec ll + ) + | [] -> [] + in ext_rec lm + and extend p = + let uc = uncovered p lcj + in if uc = [] + then [p] + else glue (List.map (fun x -> (glue (List.map extend (extension p x)))) uc) + in paths_rec m + +(* Dealing with cycles... ******) + +let conj_graph lm lc lt = + let rec nb_of_x = function + (p::lpp) -> (try let q = List.assoc p lm in q::(nb_of_x lpp) + with Not_found -> nb_of_x lpp) + | [] -> [] + and nb_rec x = function + ((l1,l2)::lcc) -> + if List.mem x l1 + then (nb_of_x l2)@(nb_rec x lcc) + else if List.mem x l2 + then (nb_of_x l1)@(nb_rec x lcc) + else nb_rec x lcc + | [] -> [] + and conj_graph_rec = function + (p::ll) -> (p,nb_rec p lc)::(conj_graph_rec ll) + | [] -> [] + in conj_graph_rec lt + +let is_cyclic_path lcj (lmu,u) = + let lm = List.flatten (List.map (fun (p,q,_) -> [(p,q);(q,p)]) lmu) + in let lc = List.map (fun (_,pl) -> pl) lcj + in let lt = List.map (fun (p,_) -> p) lm + in let g = conj_graph lm lc lt + in have_cycle g + +let good_paths lcj lp = + let rec good_paths_rec = function + (p::pp) -> if is_cyclic_path lcj p + then good_paths_rec pp + else p::(good_paths_rec pp) + | [] -> [] + in good_paths_rec lp + + + diff --git a/contrib/linear/lk_proofs.ml b/contrib/linear/lk_proofs.ml new file mode 100755 index 0000000000..e4ee298072 --- /dev/null +++ b/contrib/linear/lk_proofs.ml @@ -0,0 +1,730 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) + +(*i $Id$ i*) + +open Names + +open General +open Dpctypes +open Subst +open Unif + +let proj = function + (Po x) -> x + | (No x) -> x + + +let all_lit_sfla f = + all_lit (proj f) + +let sat p t = + let f = proj t + in let lt = all_lit f + in let rec sat_rec = function + ((p,q,_)::lm) -> if (List.mem p lt) or (List.mem q lt) + then true + else sat_rec lm + | [] -> false + in sat_rec (fst p) + +let decomp s p = + let rec decomp_rec = function + (t1::llTT) -> + let (ns,disj,at,nat,conj,rneg,lneg) = decomp_rec llTT + in if (not ((sat p t1))) + then (t1::ns,disj,at,nat,conj,rneg,lneg) + else (match t1 with + Po(Atom(_)) -> (ns,disj,t1::at,nat,conj,rneg,lneg) + | No(Atom(_)) -> (ns,disj,at,t1::nat,conj,rneg,lneg) + | Po(Neg(_)) -> (ns,disj,at,nat,conj,t1::rneg,lneg) + | No(Neg(_)) -> (ns,disj,at,nat,conj,rneg,t1::lneg) + | Po(Conj(_,_)) -> (ns,disj,at,nat,t1::conj,rneg,lneg) + | No(Disj(_,_)) -> (ns,disj,at,nat,t1::conj,rneg,lneg) + | No(Imp(_,_)) -> (ns,disj,at,nat,t1::conj,rneg,lneg) + | Po(Disj(_,_)) -> (ns,t1::disj,at,nat,conj,rneg,lneg) + | Po(Imp(_,_)) -> (ns,t1::disj,at,nat,conj,rneg,lneg) + | No(Conj(_,_)) -> (ns,t1::disj,at,nat,conj,rneg,lneg) + | _ -> failwith "decomp_rec : quantified formula !" + ) + | [] -> ([],[],[],[],[],[],[]) + in decomp_rec s + +let rec apply_weakening ((Proof2(sq1,sq2,_)) as pr) = function + (t::llTT) -> (match t with + (Po(f)) -> apply_weakening (Proof2(sq1,f::sq2,RWeakening2(f,pr))) llTT + | (No(f)) -> apply_weakening (Proof2(f::sq1,sq2,LWeakening2(f,pr))) llTT + ) + | [] -> pr + +let one_disj_comp = function + Po(Disj(f1,f2)) -> (Po(f1),Po(f2)) + | No(Conj(f1,f2)) -> (No(f1),No(f2)) + | Po(Imp(f1,f2)) -> (No(f1),Po(f2)) + | _ -> failwith "Not a disjunction in one_disj_comp !" + + +let apply_one_disj ((Proof2(sq1,sq2,r)) as lk) d = + (match d with + Po(Disj(f1,f2)) -> + let sq2' = substract sq2 [f1;f2] + in (Proof2(sq1,Disj(f1,f2)::sq2',RDisj2(f1,f2,lk))) + | No(Conj(f1,f2)) -> + let sq1' = substract sq1 [f1;f2] + in (Proof2(Conj(f1,f2)::sq1',sq2,LConj2(f1,f2,lk))) + | Po(Imp(f1,f2)) -> + let sq1' = substract sq1 [f1] + and sq2' = substract sq2 [f2] + in (Proof2(sq1',Imp(f1,f2)::sq2',RImp2(f1,f2,lk))) + | _ -> failwith "Not a disjunction in apply_one_disj !" + ) + +let rec apply_disj lk = function + (d::ld) -> let lk1 = apply_disj lk ld + in apply_one_disj lk1 d + | [] -> lk + +let find_axiom (at,nat) p = + let rec find_axiom_rec = function + ((a,b,_)::lm) -> if (List.mem (Po a) at) & (List.mem (No b) nat) + then (a,b) + else find_axiom_rec lm + | [] -> raise Not_found + in find_axiom_rec (fst p) + +let sep_at at llt (lmu,_) = + let lm = List.map (fun (p,q,_) -> (p,q)) lmu + in let rec sep_at_rec = function + ((Po a)::ll) -> let (l1,l2) = sep_at_rec ll + in if (try let b = List.assoc a lm in List.mem b llt + with Not_found -> false) + then ((Po a)::l1,l2) + else (l1,(Po a)::l2) + | [] -> ([],[]) + in sep_at_rec at + +let sep_nat nat llt (lmu,_) = + let lm = List.map (fun (p,q,_) -> (q,p)) lmu + in let rec sep_nat_rec = function + ((No a)::ll) -> let (l1,l2) = sep_nat_rec ll + in if (try let b = List.assoc a lm in List.mem b llt + with Not_found -> false) + then ((No a)::l1,l2) + else (l1,(No a)::l2) + | [] -> ([],[]) + in sep_nat_rec nat + +let sep_neg neg llt (lmu,_) = + let lm = glue (List.map (fun (p,q,_) -> [(p,q);(q,p)]) lmu) + in let rec connect = function + p::pp -> if (try let q = List.assoc p lm in List.mem q llt + with Not_found -> false) + then true + else connect pp + | [] -> false + in let rec sep_neg_rec = function + (g::ll) -> let (l1,l2) = sep_neg_rec ll + in let lit = all_lit_sfla g + in if connect lit then (g::l1,l2) + else (l1,g::l2) + | [] -> ([],[]) + in sep_neg_rec neg + +(*** connect_graph : tree list -> path -> (tree,tree list,tree list) list + etant donnee une liste de conjonctions et un path, + rend le graphe des connections des formules conjonctives + sous la forme d'une liste de + (conjonction C, conjonctions reliees a C par la gauche, + conjonctions reliees a C par la droite) **********) + +let connect_graph conj (lmu,_) = + let lm = glue (List.map (fun (p,q,_) -> [(p,q);(q,p)]) lmu) + in let fun_lit = function + Po(Conj(f1,f2)) -> (all_lit f1,all_lit f2) + | No(Disj(f1,f2)) -> (all_lit f1,all_lit f2) + | No(Imp(f1,f2)) -> (all_lit f1,all_lit f2) + | _ -> failwith "Not a conjunction in connect_graph !" + in let lt = List.map (fun x -> (x,fun_lit x)) conj + in let in_which b = let rec in_which_rec = function + ((c,(l1,l2))::ll) -> if (List.mem b l1) or (List.mem b l2) + then c else in_which_rec ll + | [] -> raise Not_found + in in_which_rec lt + in let rec fun_nb c = function + (a::ll) -> let lnb = fun_nb c ll + in (try let b = List.assoc a lm + in let c1 = in_which b + in if c1=c then lnb else c1::lnb + with Not_found -> lnb) + | [] -> [] + in let fun_cg c = let (l1,l2) = List.assoc c lt + in (fun_nb c l1,fun_nb c l2) + in List.map (fun x -> let (l1,l2) = fun_cg x in (x,l1,l2)) conj + +let cut_path (lm,u) lt = + let rec cut_path_rec = function + ((p,q,_) as m::llmm) -> let (llmm1,llmm2) = cut_path_rec llmm + in if (List.mem p lt) or (List.mem q lt) + then (m::llmm1,llmm2) + else (llmm1,m::llmm2) + | [] -> ([],[]) + in let (lm1,lm2) = cut_path_rec lm + in ((lm1,u),(lm2,u)) + +(*** sep_path : (at,nat,conj) -> path -> tree,(sequent,path),(sequent,path) + etant donnes (at,nat,conj) et p, fait la separation en deux couples + (sequent,path) correspondant aux deux membres d'une conjonction + et rend egalement la conjonction en question ********) + +let sep_path (at,nat,conj,rneg,lneg) p = + let g = connect_graph conj p + in let rec find_all_X0 = function + ((x,l1,l2) as gd::ll) -> if disjoint l1 l2 then + gd::(find_all_X0 ll) + else find_all_X0 ll + | [] -> [] + in let all_X0 = find_all_X0 g + in let rec find_X0 = function + [x] -> x + | ((Po(Conj _),_,_) as c::_) -> c (** on recherche d'abord A/\B **) + | _::ll -> find_X0 ll + in let (x0,l1,l2) = if all_X0=[] then + failwith "Can't find X0 in sep_path ! (impossible case)" + else find_X0 all_X0 + in let (g,d) = (match x0 with + Po(Conj(f1,f2)) -> (Po(f1),Po(f2)) + | No(Disj(f1,f2)) -> (No(f1),No(f2)) + | No(Imp(f1,f2)) -> (Po(f1),No(f2)) + | _ -> failwith "Not a conjunction in sep_path !") + in let s1 = g::l1 + in let s2 = d::(substract conj (x0::l1)) + in let litS1 = glue (List.map (fun x -> all_lit_sfla x) s1) + in let (at1,at2) = sep_at at litS1 p + and (nat1,nat2) = sep_nat nat litS1 p + in let neg = lneg @ (List.map (fun (Po (Neg f)) -> (No f)) rneg) + in let (neg1,neg2) = sep_neg neg litS1 p + in let lit_at1 = List.map proj at1 + and lit_nat1 = List.map proj nat1 + and lit_neg1 = List.map proj neg1 + in let (p1,p2) = cut_path p (lit_at1@lit_nat1@lit_neg1@litS1) + in let sq1 = s1 @ at1 @ nat1 @ neg1 + in let sq2 = s2 @ at2 @ nat2 @ neg2 + in (x0,(sq1,p1),(sq2,p2)) + +let conj_case x0 ((Proof2(sq11,sq12,rl1)) as pr1) + ((Proof2(sq21,sq22,rl2)) as pr2) = + (match x0 with + Po(Conj(f1,f2)) -> + let sq2 = (substract sq12 [f1])@(substract sq22 [f2]) + in (Proof2(sq11@sq21,Conj(f1,f2)::sq2, + RConj2(f1,pr1,f2,pr2))) + | No(Disj(f1,f2)) -> + let sq1 = (substract sq11 [f1])@(substract sq21 [f2]) + in (Proof2(Disj(f1,f2)::sq1,sq12@sq22, + LDisj2(f1,pr1,f2,pr2))) + | No(Imp(f1,f2)) -> + let sq1 = sq11@(substract sq21 [f2]) + and sq2 = (substract sq12 [f1])@sq22 + in (Proof2(Imp(f1,f2)::sq1,sq2,LImp2(f1,pr1,f2,pr2))) + | _ -> failwith "Not a conjunction in conj_case !" + ) + +let rec rneg_case pr = function + ((Po(Neg f))::lng) -> + let ((Proof2(sq1,sq2,_)) as pr1) = rneg_case pr lng + in let sq1' = substract sq1 [f] + and sq2' = (Neg f)::sq2 + in (Proof2(sq1',sq2',RNeg2(f,pr1))) + | [] -> pr + +let lneg_case ((Proof2(sq1,sq2,_)) as pr) (No(Neg f)) = + let sq1' = (Neg f)::sq1 + and sq2' = substract sq2 [f] + in (Proof2(sq1',sq2',LNeg2(f,pr))) + +let find_lneg lneg = + let rec is_negneg = function + t::ll -> (match t with + No(Neg(Neg(f))) -> t + | _ -> is_negneg ll + ) + | [] -> raise Not_found + in try is_negneg lneg + with Not_found -> List.hd lneg + +let rec proof_of_path sT p = + let (ns,disj,at,nat,conj,rneg,lneg) = decomp sT p + in let sT1 = substract sT ns + in let pr1 = if disj=[] + then cases (at,nat,conj,rneg,lneg) p + else disj_case disj sT1 p + in apply_weakening pr1 ns +and disj_case disj sT1 p = + let rec disj_case_rec s = function + d::ld -> let (a,b) = one_disj_comp d + in let nsatA = (not ((sat p a))) + and nsatB = (not ((sat p b))) + in let s1 = substract s [d] + in let s2 = if nsatA then b::s1 + else if nsatB then a::s1 + else a::(b::s1) + in let pr = disj_case_rec s2 ld + in let pr1 = if nsatA then apply_weakening pr [a] + else if nsatB then apply_weakening pr [b] + else pr + in apply_one_disj pr1 d + | [] -> proof_of_path s p + in disj_case_rec sT1 disj +and cases (at,nat,conj,rneg,lneg) p = + try let (a,b) = find_axiom (at,nat) p + in let pr = (Proof2([b],[a],Axiom2(a))) + in let wk = (substract at [(Po a)]) + @(substract nat [(No b)]) + @conj@rneg@lneg + in apply_weakening pr wk + with Not_found -> + if conj<>[] then + let (x0,(s1,p1),(s2,p2)) = sep_path (at,nat,conj,rneg,lneg) p + in let pr1 = proof_of_path s1 p1 + in let pr2 = proof_of_path s2 p2 + in let pr = conj_case x0 pr1 pr2 + in rneg_case pr rneg + else + if rneg<>[] then + let s = at@nat@lneg@(List.map (fun (Po (Neg f)) -> (No f)) rneg) + in let pr = proof_of_path s p + in rneg_case pr rneg + else + let (No (Neg f)) as g = find_lneg lneg + in let s = at@nat@(substract lneg [g])@[Po f] + in let pr = proof_of_path s p + in lneg_case pr g + + +(* pi_formula : separated formula -> formula + pi_proof : separated proof -> proof *******) + +let rec pi_formula = function + Atom((s,_),lt) -> Atom((s,0),lt) + | Neg(f) -> Neg(pi_formula f) + | Imp(f1,f2) -> Imp(pi_formula f1,pi_formula f2) + | Conj(f1,f2) -> Conj(pi_formula f1,pi_formula f2) + | Disj(f1,f2) -> Disj(pi_formula f1,pi_formula f2) + | ForAll(s,f) -> ForAll(s,pi_formula f) + | Exists(s,f) -> Exists(s,pi_formula f) + +let rec pi_proof (Proof2(sq1,sq2,rule)) = + let sq1' = List.map pi_formula sq1 + and sq2' = List.map pi_formula sq2 + in let rule1 = match rule with + Axiom2(f) -> Axiom2(pi_formula f) + | RWeakening2(f,p) -> RWeakening2(pi_formula f,pi_proof p) + | LWeakening2(f,p) -> LWeakening2(pi_formula f,pi_proof p) + | RNeg2(f,p) -> RNeg2(pi_formula f,pi_proof p) + | LNeg2(f,p) -> LNeg2(pi_formula f,pi_proof p) + | RConj2(f1,p1,f2,p2) + -> RConj2(pi_formula f1,pi_proof p1,pi_formula f2,pi_proof p2) + | LDisj2(f1,p1,f2,p2) + -> LDisj2(pi_formula f1,pi_proof p1,pi_formula f2,pi_proof p2) + | LImp2(f1,p1,f2,p2) + -> LImp2(pi_formula f1,pi_proof p1,pi_formula f2,pi_proof p2) + | LConj2(f1,f2,p) -> LConj2(pi_formula f1,pi_formula f2,pi_proof p) + | RDisj2(f1,f2,p) -> RDisj2(pi_formula f1,pi_formula f2,pi_proof p) + | RImp2(f1,f2,p) -> RImp2(pi_formula f1,pi_formula f2,pi_proof p) + | RForAll2(s,f,p) -> RForAll2(s,pi_formula f,pi_proof p) + | LExists2(s,f,p) -> LExists2(s,pi_formula f,pi_proof p) + | LForAll2(s,t,f,p) -> LForAll2(s,t,pi_formula f,pi_proof p) + | RExists2(s,t,f,p) -> RExists2(s,t,pi_formula f,pi_proof p) + in (Proof2(sq1',sq2',rule1)) + +(*** Introduction of quantifiers in proof ******) + +type quantifier = Universal of identifier * formula * bool + | Existential of identifier * formula * bool + + +let her v ex = + let lt = List.map (fun x-> VAR(x)) ex + in (v,APP (GLOB (SK v)::lt)) + +(*** quant_var returns all the quantifiers of a formula *****) + +let quant_var f = + let rec qv_rec sign = function + ForAll(v,f) -> let qt = qv_rec sign f in + if sign then (Universal(v,f,true))::qt + else (Existential(v,f,false))::qt + | Exists(v,f) -> let qt = qv_rec sign f in + if sign then (Existential(v,f,true))::qt + else (Universal(v,f,false))::qt + | Atom(_) -> [] + | Neg(f) -> qv_rec ((not (sign))) f + | Imp(f1,f2) -> let qt1 = qv_rec ((not (sign))) f1 + and qt2 = qv_rec sign f2 + in qt1@qt2 + | Conj(f1,f2) -> let qt1 = qv_rec sign f1 + and qt2 = qv_rec sign f2 + in qt1@qt2 + | Disj(f1,f2) -> let qt1 = qv_rec sign f1 + and qt2 = qv_rec sign f2 + in qt1@qt2 + in qv_rec true f + +(*** replace the skolem functions by their corresponding variables ****) + +let rec unher_term lv = function + | APP (GLOB (SK v)::_) -> VAR v + | APP lt -> APP (unher_list_term lv lt) + | x -> x +and unher_list_term lv lt = + List.map (unher_term lv) lt + +let rec unher_unif lv = function + ((x,t)::ll) -> (x,unher_term lv t)::(unher_unif lv ll) + | [] -> [] + +let rec unher_formula lv = function + Atom(s,lt) -> Atom(s,unher_list_term lv lt) + | Neg(f) -> Neg(unher_formula lv f) + | Imp(f1,f2) -> Imp(unher_formula lv f1,unher_formula lv f2) + | Conj(f1,f2) -> Conj(unher_formula lv f1,unher_formula lv f2) + | Disj(f1,f2) -> Disj(unher_formula lv f1,unher_formula lv f2) + | ForAll(s,f) -> ForAll(s,unher_formula lv f) + | Exists(s,f) -> Exists(s,unher_formula lv f) + +let rec unher_sequent lv = function + (f::ll) -> (unher_formula lv f)::(unher_sequent lv ll) + | [] -> [] + +let rec unher_proof lv (Proof2(sq1,sq2,rule)) = + let sq1' = unher_sequent lv sq1 + and sq2' = unher_sequent lv sq2 + in let rule1 = match rule with + Axiom2(f) -> Axiom2(unher_formula lv f) + | RWeakening2(f,p) -> RWeakening2(unher_formula lv f,unher_proof lv p) + | LWeakening2(f,p) -> LWeakening2(unher_formula lv f,unher_proof lv p) + | RNeg2(f,p) -> RNeg2(unher_formula lv f,unher_proof lv p) + | LNeg2(f,p) -> LNeg2(unher_formula lv f,unher_proof lv p) + | RConj2(f1,p1,f2,p2) -> RConj2(unher_formula lv f1,unher_proof lv p1, + unher_formula lv f2,unher_proof lv p2) + | LDisj2(f1,p1,f2,p2) -> LDisj2(unher_formula lv f1,unher_proof lv p1, + unher_formula lv f2,unher_proof lv p2) + | LImp2(f1,p1,f2,p2) -> LImp2(unher_formula lv f1,unher_proof lv p1, + unher_formula lv f2,unher_proof lv p2) + | LConj2(f1,f2,p) -> LConj2(unher_formula lv f1,unher_formula lv f2, + unher_proof lv p) + | RDisj2(f1,f2,p) -> RDisj2(unher_formula lv f1,unher_formula lv f2, + unher_proof lv p) + | RImp2(f1,f2,p) -> RImp2(unher_formula lv f1,unher_formula lv f2, + unher_proof lv p) + | RForAll2(s,f,p) -> RForAll2(s,unher_formula lv f,unher_proof lv p) + | LExists2(s,f,p) -> LExists2(s,unher_formula lv f,unher_proof lv p) + | LForAll2(s,t,f,p) -> LForAll2(s,t,unher_formula lv f,unher_proof lv p) + | RExists2(s,t,f,p) -> RExists2(s,t,unher_formula lv f,unher_proof lv p) + in (Proof2(sq1',sq2',rule1)) + +(*** subst_f_qt : quantifier_list -> formula -> formula *****) + +let subst_f_qt sqt f = + let rec sub_rec f0 = function + q::ll -> let f1 = sub_rec f0 ll in + (match q with + Universal(id,f_0,t) -> let f' = if t then ForAll(id,f_0) + else Exists(id,f_0) + in subst_f_f f_0 f' f1 + | Existential(id,f_0,t) -> let f' = if t then Exists(id,f_0) + else ForAll(id,f_0) + in subst_f_f f_0 f' f1 + ) + | [] -> f0 + in sub_rec f sqt + + +let quant_in id f = + let rec qi = function + Atom(_) -> false + | Neg(f1) -> qi f1 + | Conj(f1,f2) -> (qi f1) or (qi f2) + | Disj(f1,f2) -> (qi f1) or (qi f2) + | Imp(f1,f2) -> (qi f1) or (qi f2) + | ForAll(id',f1) -> if id=id' then true else qi f1 + | Exists(id',f1) -> if id=id' then true else qi f1 + in qi f + + +let weak_quant f = + let rec wq_rec = function + ((Universal(id,_,_)) as q)::ll -> if quant_in id f then q::(wq_rec ll) + else wq_rec ll + | ((Existential(id,_,_)) as q)::ll -> if quant_in id f then q::(wq_rec ll) + else wq_rec ll + | [] -> [] + in wq_rec + + +let proof_quant (Proof2(sq1,sq2,_)) sqt = + let sq = List.map (subst_f_qt sqt)(sq1@sq2) + in + let id_in_sq id = + List.fold_left (fun r f -> if r then true else (id_in_formula id f)) false sq + in + let rec pq_rec = function + ((Universal(id,_,_)) as q)::ll -> if id_in_sq id then q::(pq_rec ll) + else pq_rec ll + | ((Existential(id,_,_)) as q)::ll -> if id_in_sq id then q::(pq_rec ll) + else pq_rec ll + | [] -> [] + in pq_rec sqt + + +let find_quant pog sq1' sq2' = + let appear = function + (Universal(id,f,t)) + -> let qf = if t then ForAll(id,f) else Exists(id,f) + in (List.mem qf sq1') or (List.mem qf sq2') + | (Existential(id,f,t)) + -> let qf = if t then Exists(id,f) else ForAll(id,f) + in (List.mem qf sq1') or (List.mem qf sq2') + in + let rec find_rec = function + (q,r)::l -> if !r=0 then if appear q then q + else find_rec l + else find_rec l + | [] -> raise Not_found + in find_rec pog + + +(*** make_pog : make partial order graph + make_pog : quantifier list -> (quantifier * quantifier) list + -> (quantifier * int ref) list *******) + +let make_pog qt cst = + let pog0 = List.map (fun x -> (x,ref 0)) qt + in + let rec make_rec = function + (q,q')::l -> if (List.mem q qt) & (List.mem q' qt) then + let r = List.assoc q' pog0 in r := !r + 1 + else () ; + make_rec l + | [] -> pog0 + in + make_rec cst + + +let update_pog cst pog lq = + let remove_one q0 = + let rec rm_rec = function + (q,r)::ll -> if q=q0 + then rm_rec ll + else if List.mem (q0,q) cst + then begin r := !r - 1; (q,r)::(rm_rec ll) end + else (q,r)::(rm_rec ll) + | [] -> [] + in rm_rec + in + let rec remove_all pog0 = function + q::ll -> let pog1 = remove_one q pog0 in + remove_all pog1 ll + | [] -> pog0 + in + remove_all pog lq + + +(*** sort_pog : pog -> quantifier list *****) + +let sort_pog cst pog = + let pog' = List.map (fun (x,r) -> (x,ref (!r))) pog + in + let decrease_one x = + let rec dec_rec = function + (q,q')::ll -> if (q=x) & (List.mem_assoc q' pog') + then begin + let r = List.assoc q' pog' in + r := !r - 1; dec_rec ll + end + else dec_rec ll + | [] -> () + in dec_rec cst + in + let rec decrease = function + x::ll -> decrease_one x; decrease ll + | [] -> () + in + let rec find_min = function + (x,r)::ll -> if !r=0 + then begin r := -1; x::(find_min ll) end + else find_min ll + | [] -> [] + in + let rec loop od = + let m = find_min pog' in + if m=[] then od + else begin decrease m; loop (od@m) end + in loop [] + + +(*** quant_proof : cst -> pog -> lkproof2 -> lkproof2 ********) + +let rec quant_proof cst pog ((Proof2(sq1,sq2,rule)) as pr) = + if pog=[] then pr + else + let sqt = sort_pog cst pog in + let sq1' = List.map (subst_f_qt sqt) sq1 + and sq2' = List.map (subst_f_qt sqt) sq2 + in + let rule' = match rule with + LWeakening2(f,p) -> let f' = subst_f_qt sqt f in + let wq = weak_quant f' sqt in + LWeakening2(f',quant_proof cst (update_pog cst pog wq) p) + | RWeakening2(f,p) -> let f' = subst_f_qt sqt f in + let wq = weak_quant f' sqt in + RWeakening2(f',quant_proof cst (update_pog cst pog wq) p) + | _ -> (try + let q1 = find_quant pog sq1' sq2' in + let pr' = quant_proof cst (update_pog cst pog [q1]) pr in + (match q1 with + Universal(id,f,t) -> if t then RForAll2(id,f,pr') + else LExists2(id,f,pr') + | Existential(id,f,t) -> if t then RExists2(id,VAR id,f,pr') + else LForAll2(id,VAR id,f,pr') ) + with Not_found -> + (match rule with + Axiom2(f) -> Axiom2(f) + | RNeg2(f,p) -> RNeg2(subst_f_qt sqt f,quant_proof cst pog p) + | LNeg2(f,p) -> LNeg2(subst_f_qt sqt f,quant_proof cst pog p) + | RConj2(f1,p1,f2,p2) + -> let sqt1 = proof_quant p1 sqt in + let pog1 = make_pog sqt1 cst in + let pog2 = make_pog (substract sqt sqt1) cst in + RConj2(subst_f_qt sqt f1,quant_proof cst pog1 p1, + subst_f_qt sqt f2,quant_proof cst pog2 p2) + | LConj2(f1,f2,p) -> LConj2(subst_f_qt sqt f1,subst_f_qt sqt f2, + quant_proof cst pog p) + | RDisj2(f1,f2,p) -> RDisj2(subst_f_qt sqt f1,subst_f_qt sqt f2, + quant_proof cst pog p) + | LDisj2(f1,p1,f2,p2) + -> let sqt1 = proof_quant p1 sqt in + let pog1 = make_pog sqt1 cst in + let pog2 = make_pog (substract sqt sqt1) cst in + LDisj2(subst_f_qt sqt f1,quant_proof cst pog1 p1, + subst_f_qt sqt f2,quant_proof cst pog2 p2) + | RImp2(f1,f2,p) -> RImp2(subst_f_qt sqt f1,subst_f_qt sqt f2, + quant_proof cst pog p) + | LImp2(f1,p1,f2,p2) + -> let sqt1 = proof_quant p1 sqt in + let pog1 = make_pog sqt1 cst in + let pog2 = make_pog (substract sqt sqt1) cst in + LImp2(subst_f_qt sqt f1,quant_proof cst pog1 p1, + subst_f_qt sqt f2,quant_proof cst pog2 p2) + | _ -> raise Impossible_case + )) + in (Proof2(sq1',sq2',rule')) + + +(*** apply_unif_f : unifier -> formula -> formula *****) + +let apply_unif_f u = + let rec auf_rec = function + Atom(n,lt) -> Atom(n,List.map (apply_unif u) lt) + | Neg(f) -> Neg(auf_rec f) + | Conj(f1,f2) -> Conj(auf_rec f1,auf_rec f2) + | Disj(f1,f2) -> Disj(auf_rec f1,auf_rec f2) + | Imp(f1,f2) -> Imp(auf_rec f1,auf_rec f2) + | ForAll(id,f) -> ForAll(id,auf_rec f) + | Exists(id,f) -> Exists(id,auf_rec f) + in auf_rec + + +(*** witness_proof : quantifier list -> unifier -> lkproof2 -> lkproof2 ****) + +let witness_proof u0 pr = + let rec wit_rec u (Proof2(sq1,sq2,rule)) = + let sq1' = List.map (apply_unif_f u) sq1 + and sq2' = List.map (apply_unif_f u) sq2 in + let rule' = match rule with + Axiom2(f) -> Axiom2(apply_unif_f u f) + | RWeakening2(f,p) -> RWeakening2(apply_unif_f u f,wit_rec u p) + | LWeakening2(f,p) -> LWeakening2(apply_unif_f u f,wit_rec u p) + | RNeg2(f,p) -> RNeg2(apply_unif_f u f,wit_rec u p) + | LNeg2(f,p) -> LNeg2(apply_unif_f u f,wit_rec u p) + | RConj2(f1,p1,f2,p2) -> RConj2(apply_unif_f u f1,wit_rec u p1, + apply_unif_f u f2,wit_rec u p2) + | LConj2(f1,f2,p) -> LConj2(apply_unif_f u f1,apply_unif_f u f2, + wit_rec u p) + | RDisj2(f1,f2,p) -> RDisj2(apply_unif_f u f1,apply_unif_f u f2, + wit_rec u p) + | LDisj2(f1,p1,f2,p2) -> LDisj2(apply_unif_f u f1,wit_rec u p1, + apply_unif_f u f2,wit_rec u p2) + | RImp2(f1,f2,p) -> RImp2(apply_unif_f u f1,apply_unif_f u f2, + wit_rec u p) + | LImp2(f1,p1,f2,p2) -> LImp2(apply_unif_f u f1,wit_rec u p1, + apply_unif_f u f2,wit_rec u p2) + | RForAll2(id,f,p) -> RForAll2(id,apply_unif_f u f,wit_rec u p) + | LForAll2(id,_,f,p) -> let f' = apply_unif_f u f in + let t = assoc_unif (VAR id) u0 in + LForAll2(id,t,f',wit_rec ((VAR id,t)::u) p) + | RExists2(id,_,f,p) -> let f' = apply_unif_f u f in + let t = assoc_unif (VAR id) u0 in + RExists2(id,t,f',wit_rec ((VAR id,t)::u) p) + | LExists2(id,f,p) -> LExists2(id,apply_unif_f u f,wit_rec u p) + in (Proof2(sq1',sq2',rule')) + in wit_rec [] pr + + +(*** make constraints on quantifiers ******) +(*** make_constraints : + quantifier list -> unifier -> (quantifier * quantifier) list ***) + +let in_witness id t = + let vt = all_var_term t + in List.mem id vt + + +let before u = fun + p_0 p_1 -> match p_0,p_1 with ((Universal(id,f,_)), (Universal(id',f',_))) + -> if id=id' then false + else quant_in id' f + | ((Universal(id,f,_)), (Existential(id',f',_))) + -> (quant_in id' f) or (in_witness id (assoc_unif (VAR id') u)) + | ((Existential(id,f,_)), (Universal(id',f',_))) + -> quant_in id' f + | ((Existential(id,f,_)), (Existential(id',f',_))) + -> if id=id' then false + else (quant_in id' f) or (in_witness id (assoc_unif (VAR id') u)) + + +let make_constraints qt u = + let rec goods = function + (a,b)::ll -> if before u a b + then (a,b)::(goods ll) + else goods ll + | [] -> [] + in + let all = glue (List.map (fun a -> (List.map (fun b -> (a,b)) qt)) qt) + in + goods all + + + +(*** Introduce all the quantifiers in a proof (one after each other, + using apply_ex and apply_un) ********) + +let int_quant f u pr = + let qt = quant_var f + in let un_qt = such_that qt (function (Universal _) -> true | _ -> false) + and fr_var = free_var_formula f + in let un_var = List.map (fun (Universal(id,_,_)) -> id) un_qt + in let sk_var = un_var @ fr_var + in let u0 = unher_unif sk_var u + in let pr0 = pi_proof pr + in let pr1 = unher_proof sk_var pr0 + in let cst = make_constraints qt u0 + in let pog = make_pog qt cst + in let qpr = quant_proof cst pog pr1 + in witness_proof u0 qpr + diff --git a/contrib/linear/prove.ml b/contrib/linear/prove.ml new file mode 100755 index 0000000000..35c3f3427b --- /dev/null +++ b/contrib/linear/prove.ml @@ -0,0 +1,80 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) + +(*i $Id$ i*) + +open Dpctypes;; +open Kwc;; +open Lk_proofs;; + +exception Not_provable_in_DPC of string +;; +exception No_intuitionnistic_proof of int +;; + +(* is_int_proof : lkproof2 -> bool *******) + +let rec is_int_proof (Proof2(sq1,sq2,rule)) = + if (List.length sq2)>1 then false + else match rule with + Axiom2(_) -> true + | RWeakening2(_,p) -> is_int_proof p + | LWeakening2(_,p) -> is_int_proof p + | RNeg2(_,p) -> is_int_proof p + | LNeg2(_,p) -> is_int_proof p + | RConj2(_,p1,_,p2) -> (is_int_proof p1) & (is_int_proof p2) + | LConj2(_,_,p) -> is_int_proof p + | RDisj2(f1,f2,Proof2(_,_,RWeakening2(f3,p))) -> + if (f3=f1) or (f3=f2) then is_int_proof p + else false + | RDisj2(_,_,_) -> false + | LDisj2(_,p1,_,p2) -> (is_int_proof p1) & (is_int_proof p2) + | RImp2(_,_,p) -> is_int_proof p + | LImp2(_,p1,_,p2) -> (is_int_proof p1) & (is_int_proof p2) + | RForAll2(_,_,p) -> is_int_proof p + | LForAll2(_,_,_,p) -> is_int_proof p + | RExists2(_,_,_,p) -> is_int_proof p + | LExists2(_,_,p) -> is_int_proof p +;; + +(* find_int_proof : f -> f1 -> path list -> lkproof2 *****) + +let find_int_proof f f1 all_v_paths = + let rec find_rec = function + p::ll -> let pr0 = proof_of_path [Po(f1)] p in + if is_int_proof pr0 + then int_quant f (snd p) pr0 + else find_rec ll + | [] -> raise Not_found + in find_rec all_v_paths +;; + +(* prove_f : formula -> lk_proof2 + prove : string -> lk_proof2 *******) + +let prove_f f = + let f0 = separate f + in let (ex,f1) = herbrand f0 + in let (pos,neg,lcj) = lit_conj f1 + in let cj = List.map (fun (c,_) -> c) lcj + in let m = all_matches pos neg lcj + in if m = [] + then raise (Not_provable_in_DPC "(No match)") + + else let all_paths = paths pos neg m lcj + in if all_paths = [] + then raise (Not_provable_in_DPC "(No path)") + + else let all_valid_paths = good_paths lcj all_paths + in if all_valid_paths = [] + then raise (Not_provable_in_DPC "(No valid path)") + + else try find_int_proof f f1 all_valid_paths + with Not_found -> let n = List.length all_valid_paths + in raise (No_intuitionnistic_proof n) +;; diff --git a/contrib/linear/prove.mli b/contrib/linear/prove.mli new file mode 100755 index 0000000000..67381b438a --- /dev/null +++ b/contrib/linear/prove.mli @@ -0,0 +1,19 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) + +(*i $Id$ i*) + +open Dpctypes;; + +exception Not_provable_in_DPC of string +;; +exception No_intuitionnistic_proof of int +;; + +val prove_f : formula -> lkproof2;; + diff --git a/contrib/linear/subst.ml b/contrib/linear/subst.ml new file mode 100755 index 0000000000..8e16565d7a --- /dev/null +++ b/contrib/linear/subst.ml @@ -0,0 +1,150 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) + +(*i $Id$ i*) + +open General +open Names +open Dpctypes + +(* subst_term : identifier -> term -> term -> term + subst_list_term : identifier -> term -> term list -> term list *****) + +let rec subst_term v t = function + VAR(s) -> if s=v then t else (VAR s) + | GLOB _ as x -> x + | APP(lt) -> APP(subst_list_term v t lt) +and subst_list_term v t = function + t1::l1 -> (subst_term v t t1)::(subst_list_term v t l1) +| [] -> [] + +(* subst : identifier -> term -> formula -> formula *) + +let subst v t = + let rec subst_rec f = match f with + Atom(s,lt) -> Atom(s,subst_list_term v t lt) + | Neg(f1) -> Neg(subst_rec f1) + | Imp(f1,f2) -> Imp(subst_rec f1,subst_rec f2) + | Conj(f1,f2) -> Conj(subst_rec f1, subst_rec f2) + | Disj(f1,f2) -> Disj(subst_rec f1, subst_rec f2) + | ForAll(s,f1) -> ForAll(s,subst_rec f1) + | Exists(s,f1) -> Exists(s, subst_rec f1) + in subst_rec + +(* all_lit : formula -> formula list *) + +let rec all_lit = function + Atom((x_0,x_1)) -> [Atom((x_0,x_1))] + | Neg(f) -> all_lit f + | Conj(f1,f2) -> (all_lit f1)@(all_lit f2) + | Disj(f1,f2) -> (all_lit f1)@(all_lit f2) + | Imp(f1,f2) -> (all_lit f1)@(all_lit f2) + | _ -> raise Impossible_case + +(* occurs : formula -> formula -> bool *) + +let occurs s = + let rec occurs_rec f = if s=f then true else match f with + Neg(f1) -> (occurs_rec f1) + | ForAll(s,f1) -> (occurs_rec f1) + | Exists(s,f1) -> (occurs_rec f1) + | Imp(f1,f2) -> (occurs_rec f1) or (occurs_rec f2) + | Conj(f1,f2) -> (occurs_rec f1) or (occurs_rec f2) + | Disj(f1,f2) -> (occurs_rec f1) or (occurs_rec f2) + | _ -> false + in occurs_rec + +(* subst_f_f : formula -> formula -> formula -> formula *) + +let rec subst_f_f fa fb f = + if f=fa + then fb + else match f with + Atom(_,_) as a -> a + | Neg(f1) -> Neg(subst_f_f fa fb f1) + | Conj(f1,f2) -> Conj(subst_f_f fa fb f1,subst_f_f fa fb f2) + | Disj(f1,f2) -> Disj(subst_f_f fa fb f1,subst_f_f fa fb f2) + | Imp(f1,f2) -> Imp(subst_f_f fa fb f1,subst_f_f fa fb f2) + | ForAll(s,f1) -> ForAll(s,subst_f_f fa fb f1) + | Exists(s,f1) -> Exists(s,subst_f_f fa fb f1) + +(* subst_proof2 : identifier -> term -> lkproof2 -> lkproof2 *) + +let rec subst_proof2 v t (Proof2(sq1,sq2,rule)) = + let sq1' = List.map (subst v t) sq1 + and sq2' = List.map (subst v t) sq2 + in let rule1 = match rule with + Axiom2(f) -> Axiom2(subst v t f) + | RWeakening2(f,p) -> RWeakening2(subst v t f,subst_proof2 v t p) + | LWeakening2(f,p) -> LWeakening2(subst v t f,subst_proof2 v t p) + | RNeg2(f,p) -> RNeg2(subst v t f,subst_proof2 v t p) + | LNeg2(f,p) -> LNeg2(subst v t f,subst_proof2 v t p) + | RConj2(f1,p1,f2,p2) -> RConj2(subst v t f1,subst_proof2 v t p1, + subst v t f2,subst_proof2 v t p2) + | LDisj2(f1,p1,f2,p2) -> LDisj2(subst v t f1,subst_proof2 v t p1, + subst v t f2,subst_proof2 v t p2) + | LImp2(f1,p1,f2,p2) -> LImp2(subst v t f1,subst_proof2 v t p1, + subst v t f2,subst_proof2 v t p2) + | LConj2(f1,f2,p) -> LConj2(subst v t f1,subst v t f2, + subst_proof2 v t p) + | RDisj2(f1,f2,p) -> RDisj2(subst v t f1,subst v t f2, + subst_proof2 v t p) + | RImp2(f1,f2,p) -> RImp2(subst v t f1,subst v t f2, + subst_proof2 v t p) + | RForAll2(s,f,p) -> RForAll2(s,subst v t f,subst_proof2 v t p) + | LExists2(s,f,p) -> LExists2(s,subst v t f,subst_proof2 v t p) + | LForAll2(s,t1,f,p) -> LForAll2(s,subst_term v t t1, + subst v t f,subst_proof2 v t p) + | RExists2(s,t1,f,p) -> RExists2(s,subst_term v t t1, + subst v t f,subst_proof2 v t p) + in (Proof2(sq1',sq2',rule1)) + +(* All the free variables of a formula... ******) + +let rec all_var_term = function + VAR s -> [s] + | GLOB _ -> [] + | APP lt -> all_var_list_term lt +and all_var_list_term = function + t::ll -> union (all_var_term t) (all_var_list_term ll) + | [] -> [] + +(* free_var_formula : formula -> identifier list ******) + +let rec free_var_formula = function + Atom(s,lt) -> all_var_list_term lt + | Neg(f) -> free_var_formula f + | Imp(f1,f2) -> union (free_var_formula f1) (free_var_formula f2) + | Conj(f1,f2) -> union (free_var_formula f1) (free_var_formula f2) + | Disj(f1,f2) -> union (free_var_formula f1) (free_var_formula f2) + | ForAll(s,f) -> substract (free_var_formula f) [s] + | Exists(s,f) -> substract (free_var_formula f) [s] + +(*** id_in_term : identifier -> term -> bool + id_in_list : identifier -> term list -> bool ****) + +let rec id_in_term id = function + VAR id' -> id=id' + | GLOB _ -> false + | APP lt -> id_in_list id lt +and id_in_list id = + List.fold_left (fun r t -> if r then true else id_in_term id t) false + + +(*** id_in_formula : identifier -> formula -> bool ****) + +let rec id_in_formula id = function + Atom(_,lt) -> id_in_list id lt + | Neg(f) -> id_in_formula id f + | Conj(f1,f2) -> (id_in_formula id f1) or (id_in_formula id f2) + | Disj(f1,f2) -> (id_in_formula id f1) or (id_in_formula id f2) + | Imp(f1,f2) -> (id_in_formula id f1) or (id_in_formula id f2) + | ForAll(id',f) -> (id=id') or (id_in_formula id f) + | Exists(id',f) -> (id=id') or (id_in_formula id f) + + diff --git a/contrib/linear/subst.mli b/contrib/linear/subst.mli new file mode 100755 index 0000000000..907d4d4192 --- /dev/null +++ b/contrib/linear/subst.mli @@ -0,0 +1,21 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) + +(*i $Id$ i*) + +open Dpctypes +open Names + +val subst_term : identifier -> term -> term -> term +val subst : identifier -> term -> formula -> formula +val all_lit : formula -> formula list +val subst_f_f : formula -> formula -> formula -> formula +val all_var_term : term -> identifier list +val free_var_formula : formula -> identifier list +val id_in_formula : identifier -> formula -> bool + diff --git a/contrib/linear/unif.ml b/contrib/linear/unif.ml new file mode 100755 index 0000000000..8cf2b0b7d4 --- /dev/null +++ b/contrib/linear/unif.ml @@ -0,0 +1,311 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) + +(*i $Id$ i*) + + (* UNIFICATION : Martelli & Montanari's algorithm *) + (* ---------------------------------------------- *) + +(* Terms are of the type : + * type term = Var of identifier + * | Glob of constname + * | App of term list + * + * Unification of two atomic formulae : + * unif_atoms : atom_id * term list -> atom_id * term list + * -> (term*term) list + * + * Unification of two terms : + * unif_terms : term -> term -> (term*term) list + * + *) + +open Nameops +open General +open Dpctypes +open Subst + +exception Not_unifiable +exception Up_error + +let rec vars_of_list l = match l with + t::ll -> let vll = vars_of_list ll + in let vt = vars_of_term t + in union vt vll + | [] -> [] +and vars_of_term t = match t with + VAR x -> [VAR(x)] + | GLOB _ -> [] + | APP lt -> vars_of_list lt + +let rec nb_occ_term x t = match t with + VAR y -> if x=VAR(y) then 1 else 0 + | APP lt -> nb_occ_list x lt + | _ -> 0 +and nb_occ_list x l = match l with + t::ll -> (nb_occ_term x t)+(nb_occ_list x ll) + | [] -> 0 + +let cpt = ref 0 + +let w_atom = "-" + +let new_id () = + cpt := !cpt+1; + make_ident w_atom (Some !cpt) + +let rec initU l1 l2 = match (l1,l2) with + ((a1::ll1),(a2::ll2)) -> let w = new_id() + in let equ = ([VAR w],[a1; a2]) + in equ::(initU ll1 ll2) + | ([],[]) -> [] + | _ -> raise Impossible_case + +let initT l1 l2 = + let lt =l1@l2 + in List.map (fun x -> ([x],[])) (vars_of_list lt) + +let rec cF (t1,t2) = match t1 with + VAR(x1) -> + (match t2 with + VAR _ -> ([t1] , [([t1; t2],[])]) + | _ -> ([] , [([t1],[t2])]) + ) + | GLOB _ -> (match t2 with + GLOB _ -> if t1=t2 then ([t1] , []) else raise Not_unifiable + | VAR _ -> ([] , [([t2],[t1])]) + | _ -> raise Not_unifiable) + | APP lt1 -> + (match t2 with + VAR _ -> ([] , [([t2],[t1])]) + | GLOB _ -> raise Not_unifiable + | APP lt2 -> + if (List.length lt1)=(List.length lt2) + then let lcf = List.map cF (List.combine lt1 lt2) + in let lc = List.map (function ([x],_) -> x + | ([],e) -> List.hd (fst (List.hd e)) + | _ -> failwith "Imp.CF") lcf + in let llf = List.map (fun (_,x) -> x) lcf + in ([APP lc] , glue llf) + else raise Not_unifiable + ) + +let assocT x t = + let rec assocT_rec = function + ((lv , _) as equ::tT) -> if List.mem x lv then equ + else assocT_rec tT + | [] -> raise Not_found + in assocT_rec t + +let rec sub_elem_list x = function + (a::l) -> if a=x then l else a::(sub_elem_list x l) + | [] -> [] + +let newUT1 x1 x2 u t = + let (lv1,lt1) as equ1 = assocT x1 t + in let (lv2,lt2) as equ2 = assocT x2 t + in let nT = sub_elem_list equ1 (sub_elem_list equ2 t) + in if equ1=equ2 + then (u , t) + else if lt1=[] or lt2=[] + then (u , (lv1@lv2 , lt1@lt2)::nT) + else let t1 = List.hd lt1 and t2 = List.hd lt2 + in let (c,f) = cF (t1,t2) + in (f@u , (lv1@lv2 , c)::nT) + +let newUT2 x1 t1 u t = + let (lv1,lt1) as equ1 = assocT x1 t + in let nT = sub_elem_list equ1 t + in match lt1 with + [t2] -> let (c,f) = cF (t1,t2) + in (f@u , (lv1 , c)::nT) + | [] -> (u , (lv1 , [t1])::nT) + | _ -> failwith "Imp.newUT2" + +let newUT3 w t1 t2 u t = + let (c,f) = cF (t1,t2) + in match t1 with + VAR(_) as x1 -> let (lv1,lt1) as equ1 = assocT x1 t + in let nT = sub_elem_list equ1 t + in let tT = (w::lv1,lt1)::nT + in (match t2 with + VAR(_) as x2 -> (([x1;x2],[])::u , tT) + | _ -> (([x1],[t2])::u , tT) + ) + | _ -> (match t2 with + VAR(_) as x2 -> let (lv2,lt2) as equ2 = assocT x2 t + in let nT = sub_elem_list equ2 t + in let tT = (w::lv2,lt2)::nT + in (([x2],[t1])::u , tT) + | _ -> let (c,f) = cF (t1,t2) + in (f@u , ([w],c)::t) + ) + + (* mm : Compute the derivation of (U,T) until U=[] ***********) + +let rec mm u t = match u with + ((v,s)::uU) -> + (match s with + [] -> (match v with + [x1;x2] -> let (nU,nT) = newUT1 x1 x2 uU t + in mm nU nT + | _ -> failwith "Imp.cas 1" + ) + | [t1] -> (match v with + [x1] -> let (nU,nT) = newUT2 x1 t1 uU t + in mm nU nT + | _ -> failwith "Imp.cas 2" + ) + | [t1;t2] -> (match v with + [x1] -> let (nU,nT) = newUT3 x1 t1 t2 uU t + in mm nU nT + | _ -> failwith "Imp.cas 3" + ) + | _ -> raise Impossible_case + ) + | [] -> t + + +let nb_occ_list_list lv ltt = + let rec nb_occ_ll_rec = function + (v::lv1) -> (nb_occ_list v ltt)+(nb_occ_ll_rec lv1) + | [] -> 0 + in nb_occ_ll_rec lv + +let rec gro_aux = function + (VAR x)::ll -> if (atompart_of_id x) = w_atom then gro_aux ll + else (VAR x)::(gro_aux ll) + | h::ll -> h::(gro_aux ll) + | [] -> [] + +let rec gro_aux_T = function + ((lv,lt)::tT) -> + let lv0 = gro_aux lv + in (match lv0 with + [] -> gro_aux_T tT + | _ -> (lv0,lt)::(gro_aux_T tT) + ) + | [] -> [] + +(* From now on, the equations of T are associated with the number of + occurences of their variables in the right equations *********) + +let rec find_null = function + ((r,(_,_)) as equ::tT) -> if !r=0 then equ else find_null tT + | [] -> raise Not_unifiable + +let rec recompute t1 t = match t1 with + ((r,(lv,lt))::tT) -> let n = nb_occ_list_list lv [t] + in (ref (!r-n),(lv,lt))::(recompute tT t) + | [] -> [] + +let rec sorted_Tc t sT = + if t=[] then sT else + let (_,(lv,lt)) as equ = find_null t + in let t1 = sub_elem_list equ t + in match lt with + [] -> sorted_Tc t1 (equ::sT) + | [t_0] -> sorted_Tc (recompute t1 t_0) (equ::sT) + | _ -> raise Impossible_case + +let rec apply_subst s = function + VAR(_) as v -> if List.mem_assoc v s then List.assoc v s + else v + | GLOB _ as x -> x + | APP lt -> APP (List.map (apply_subst s) lt) + +let rec unif_from_sTc un = function + ((_,(lv,lt))::tT) -> + (match lt with + [] -> let x1 = List.hd lv and lv1 = List.tl lv + in let u0 = List.map (fun x->(x,x1)) lv1 + in unif_from_sTc (un@u0) tT + | [t] -> let t0 = apply_subst un t + in let u0 = List.map (fun x->(x,t0)) lv + in unif_from_sTc (un@u0) tT + | _ -> raise Impossible_case + ) + | [] -> un + +let unif_from_T t0 = + let t = gro_aux_T t0 + in let llt = List.map (fun (_,x) -> x) t + in let ltt = glue llt + in let rec comp_nb t1 = match t1 with + ((lv,lt)::tT1) -> (ref (nb_occ_list_list lv ltt),(lv,lt)):: + (comp_nb tT1) + | _ -> [] + in let tc = comp_nb t + in let sTc = sorted_Tc tc [] + in unif_from_sTc [] sTc + +(* unif_atoms : atom -> atom -> unifier ******) + +let unif_atoms (p1,l1) (p2,l2) = + if (fst p1)<>(fst p2) or (List.length l1)<>(List.length l2) + then raise Not_unifiable + else cpt := 0; + let t = mm (initU l1 l2) (initT l1 l2) + in unif_from_T t + +(* unif_terms : term -> term -> unifier *******) + +let unif_terms t1 t2 = + cpt := 0; + let l1 = [t1] and l2 =[t2] + in let t = mm (initU l1 l2) (initT l1 l2) + in unif_from_T t + +(* assoc_unif : unifier -> variable -> term ******) + +let assoc_unif v u = + try List.assoc v u + with Not_found -> v + +(* apply_unif : unifier -> term -> term ******) + +let apply_unif u t = + let rec au_rec = function + VAR _ as v -> assoc_unif v u + | GLOB _ as x -> x + | APP lt -> APP (List.map au_rec lt) + in au_rec t + +(* appear_var_term : variable -> term -> bool ********) + +let appear_var_term v t = + let rec avt_rec = function + VAR _ as v1 -> v1=v + | GLOB _ -> false + | APP lt -> List.fold_left (fun x t1 -> x or (avt_rec t1)) false lt + in avt_rec t + +(* up u1 u2 : returns the least unifier greater than u1 and u2 + If no such unifier exists, it raises Up_error *******) + +let rec up u1 u2 = match u2 with + (((VAR s1) as y1,t1) as eq::uu2) -> + if List.mem_assoc y1 u1 + then let m1 = List.assoc y1 u1 + in let t1' = apply_unif u1 t1 + in let u0 = try unif_terms m1 t1' + with Not_unifiable -> raise Up_error + in let u1' = List.map (fun (x,t) -> (x,apply_unif u0 t)) u1 + in up (u1'@u0) uu2 + else let t1' = apply_unif u1 t1 + in if t1' = y1 + then u1 + else if appear_var_term y1 t1' + then raise Up_error + else let u1' = + List.map (fun (x,t) -> (x,subst_term s1 t1' t)) u1 + in up ((y1,t1')::u1') uu2 + | [] -> u1 + | _ -> failwith "unif__up: impossible case" + +(* $Id$ *) diff --git a/contrib/linear/unif.mli b/contrib/linear/unif.mli new file mode 100755 index 0000000000..61a29ee8be --- /dev/null +++ b/contrib/linear/unif.mli @@ -0,0 +1,27 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) + +(*i $Id$ i*) + +open General +open Dpctypes + +exception Not_unifiable + +val unif_atoms : atom_id * term list -> atom_id * term list + -> (term * term) list +val unif_terms : term -> term -> (term * term) list + +val assoc_unif : 'a -> ('a * 'a) list -> 'a +val apply_unif : (term * term) list -> term -> term +val appear_var_term : term -> term -> bool + +exception Up_error + +val up : (term * term) list -> (term * term) list -> (term * term) list + |