diff options
| author |  corbinea <corbinea@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-10-16 15:44:47 +0000 |
|---|---|---|
| committer | corbinea <corbinea@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-10-16 15:44:47 +0000 |
| commit | 8b5f6f835be01b2b0510cdbea939050d2c2583c6 (patch) | |
| tree | dca1d522a0845397fa13344ec771cadd1b27caba | |
| parent | 5f116846807c7cc6c5b58b13158f26505e558f2c (diff) | |
Ground update + Linear removal
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4654 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | .depend | 67 | ||||
| -rw-r--r-- | .depend.camlp4 | 2 | ||||
| -rw-r--r-- | Makefile | 19 | ||||
| -rwxr-xr-x | contrib/linear/ccidpc.ml4 | 379 | ||||
| -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 | 745 | ||||
| -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, 3 insertions, 2372 deletions
@@ -452,11 +452,6 @@ 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 @@ -3135,64 +3130,6 @@ 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 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 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 lib/options.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 lib/options.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 kernel/environ.cmi tactics/equality.cmi \ @@ -3439,10 +3376,6 @@ 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 contrib/funind/tacinv.cmo: parsing/grammar.cma contrib/funind/tacinv.cmx: parsing/grammar.cma contrib/first-order/g_ground.cmo: parsing/grammar.cma diff --git a/.depend.camlp4 b/.depend.camlp4 index 13318ae60..ee4e34156 100644 --- a/.depend.camlp4 +++ b/.depend.camlp4 @@ -16,8 +16,6 @@ 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 contrib/funind/tacinv.ml: parsing/grammar.cma contrib/first-order/g_ground.ml: parsing/grammar.cma parsing/lexer.ml: @@ -61,7 +61,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/linear \ + -I contrib/jprover -I contrib/cc \ -I contrib/funind -I contrib/first-order MLINCLUDES=$(LOCALINCLUDES) -I $(MYCAMLP4LIB) @@ -301,25 +301,12 @@ FOCMO=\ CCCMO=contrib/cc/ccalgo.cmo contrib/cc/ccproof.cmo contrib/cc/cctac.cmo -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/funind/tacinv.ml4 \ - contrib/first-order/g_ground.ml4 + contrib/funind/tacinv.ml4 contrib/first-order/g_ground.ml4 CONTRIB=$(OMEGACMO) $(ROMEGACMO) $(RINGCMO) $(FIELDCMO) \ $(FOURIERCMO) $(EXTRACTIONCMO) $(JPROVERCMO) $(XMLCMO) \ - $(CORRECTNESSCMO) $(CCCMO) $(LINEARCMO) $(FUNINDCMO) $(FOCMO) + $(CORRECTNESSCMO) $(CCCMO) $(FUNINDCMO) $(FOCMO) CMA=$(CLIBS) $(CAMLP4OBJS) CMXA=$(CMA:.cma=.cmxa) diff --git a/contrib/linear/ccidpc.ml4 b/contrib/linear/ccidpc.ml4 deleted file mode 100755 index a9b3e50ee..000000000 --- a/contrib/linear/ccidpc.ml4 +++ /dev/null @@ -1,379 +0,0 @@ -(***********************************************************************) -(* 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 "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) - |_->raise Impossible_case - else None - | _->None - -let is_exist_term t=op2bool (match_with_exist_term t) - -let id_not=constr_of_string "Logic.not" - -let id_false=constr_of_string "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 = - match (named_hd Environ.empty_env a na) with - (Name id)->gen_ident id - | Anonymous->raise Impossible_case - -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) - | _-> raise Impossible_case - in tradrec - - -let dpc_of_cci_fmla gls cciterm = - let rec tradrec lid cciterm = - match match_with_exist_term cciterm with - Some ((na,a,b)as trp)-> - let id = gen_name a na in - let f=whd_beta (mkApp ((mkLambda trp),[|mkVar id|])) in - Exists(id,tradrec (id::lid) f) - |_-> - (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=whd_beta (mkApp ((mkLambda trp),[|mkVar id|])) in - ForAll(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 id gls=if is_forall_term (pf_concl gls) then - intro_using id gls else tclFAIL 0 "goal is not universally quantified" 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 - tclTHEN (generalize [mkApp (mkVar id,[|t|])]) intro gls - else tclFAIL 0 "hypothesis is not universally quantified" gls - -let existE id id2 gls = - let (_,_,t)=lookup_named id (pf_hyps gls) in - if is_exist_term t then - ((tclTHEN (simplest_elim (mkVar id)) - (tclTHEN (intro_using id2) (dImp None)))) gls - else tclFAIL 0 "hypothesis is not existentially quantified" 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 "hypothesis is not negated" gls - -(*t exist_intro_head = put_pat mmk "ex_intro"*) - -let existI t gls = - if is_exist_term (pf_concl gls) then - split (Rawterm.ImplicitBindings [t]) gls - else tclFAIL 0 "goal is not existentially quantified" 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 sign= pf_hyps gl in - let (id,_,_)=first_pred - (fun (id,_,t) -> - ( try - alpha_eq (kspine,f) - (jspine,dpc_of_cci_fmla gl t) - with _ -> false) - ) sign in id - - -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_check (mkVar id)*)assumption 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 kid) - ((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 kid) - ((onNthClause (function (Some jid) -> - trad (kid::kspine) (jid::jspine) pf - | None-> raise Impossible_case) - (-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 - - - diff --git a/contrib/linear/dpc.ml4 b/contrib/linear/dpc.ml4 deleted file mode 100755 index d30cf9ae1..000000000 --- a/contrib/linear/dpc.ml4 +++ /dev/null @@ -1,64 +0,0 @@ -(***********************************************************************) -(* 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 intro (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 deleted file mode 100644 index b21bd67e4..000000000 --- a/contrib/linear/dpctypes.ml +++ /dev/null @@ -1,60 +0,0 @@ -(***********************************************************************) -(* 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 deleted file mode 100755 index 7115cf519..000000000 --- a/contrib/linear/dpctypes.mli +++ /dev/null @@ -1,59 +0,0 @@ -(***********************************************************************) -(* 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 deleted file mode 100755 index 5b998c5af..000000000 --- a/contrib/linear/general.ml +++ /dev/null @@ -1,41 +0,0 @@ -(***********************************************************************) -(* 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 deleted file mode 100755 index 8acf59661..000000000 --- a/contrib/linear/general.mli +++ /dev/null @@ -1,16 +0,0 @@ -(***********************************************************************) -(* 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 deleted file mode 100755 index 94ddcbd97..000000000 --- a/contrib/linear/graph.ml +++ /dev/null @@ -1,70 +0,0 @@ -(***********************************************************************) -(* 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 deleted file mode 100755 index 63ae558e5..000000000 --- a/contrib/linear/graph.mli +++ /dev/null @@ -1,12 +0,0 @@ -(***********************************************************************) -(* 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 deleted file mode 100755 index 13a9b8540..000000000 --- a/contrib/linear/kwc.ml +++ /dev/null @@ -1,233 +0,0 @@ -(***********************************************************************) -(* 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 deleted file mode 100755 index 5ca3338c5..000000000 --- a/contrib/linear/lk_proofs.ml +++ /dev/null @@ -1,745 +0,0 @@ -(***********************************************************************) -(* 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) - | [] -> ([],[]) - | _->raise Impossible_case - 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) - | [] -> ([],[]) - | _->raise Impossible_case - 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 - | _->raise Impossible_case - 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 (function - (Po (Neg f)) -> (No f) - | _->raise Impossible_case) 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 - | _->raise Impossible_case - - -let lneg_case ((Proof2(sq1,sq2,_)) as pr) =function - (No(Neg f))-> - let sq1' = (Neg f)::sq1 - and sq2' = substract sq2 [f] - in (Proof2(sq1',sq2',LNeg2(f,pr))) - | _->raise Impossible_case - -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 (function - (Po (Neg f)) -> (No f) - | _->raise Impossible_case) rneg) - in let pr = proof_of_path s p - in rneg_case pr rneg - else - match find_lneg lneg with - (No (Neg f)) as g -> - let s = at@nat@(substract lneg [g])@[Po f] in - let pr = proof_of_path s p in - lneg_case pr g - |_->raise Impossible_case - - -(* 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 (function - (Universal(id,_,_)) -> id - | _ ->raise Impossible_case) 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 deleted file mode 100755 index 35c3f3427..000000000 --- a/contrib/linear/prove.ml +++ /dev/null @@ -1,80 +0,0 @@ -(***********************************************************************) -(* 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 deleted file mode 100755 index 67381b438..000000000 --- a/contrib/linear/prove.mli +++ /dev/null @@ -1,19 +0,0 @@ -(***********************************************************************) -(* 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 deleted file mode 100755 index 8e16565d7..000000000 --- a/contrib/linear/subst.ml +++ /dev/null @@ -1,150 +0,0 @@ -(***********************************************************************) -(* 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 deleted file mode 100755 index 907d4d419..000000000 --- a/contrib/linear/subst.mli +++ /dev/null @@ -1,21 +0,0 @@ -(***********************************************************************) -(* 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 deleted file mode 100755 index 8cf2b0b7d..000000000 --- a/contrib/linear/unif.ml +++ /dev/null @@ -1,311 +0,0 @@ -(***********************************************************************) -(* 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 deleted file mode 100755 index 61a29ee8b..000000000 --- a/contrib/linear/unif.mli +++ /dev/null @@ -1,27 +0,0 @@ -(***********************************************************************) -(* 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 - |