diff options
Diffstat (limited to 'contrib')
| -rw-r--r-- | contrib/first-order/engine.ml4 | 105 | ||||
| -rw-r--r-- | contrib/first-order/formula.ml | 213 | ||||
| -rw-r--r-- | contrib/first-order/formula.mli | 69 | ||||
| -rw-r--r-- | contrib/first-order/rules.ml | 186 | ||||
| -rw-r--r-- | contrib/first-order/rules.mli | 51 | ||||
| -rw-r--r-- | contrib/first-order/sequent.ml | 97 | ||||
| -rw-r--r-- | contrib/first-order/sequent.mli | 44 | ||||
| -rw-r--r-- | contrib/first-order/unify.ml | 131 | ||||
| -rw-r--r-- | contrib/first-order/unify.mli | 13 |
9 files changed, 909 insertions, 0 deletions
diff --git a/contrib/first-order/engine.ml4 b/contrib/first-order/engine.ml4 new file mode 100644 index 0000000000..8b85316a90 --- /dev/null +++ b/contrib/first-order/engine.ml4 @@ -0,0 +1,105 @@ +(***********************************************************************) +(* 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*) + +(* $Id$ *) + +open Formula +open Sequent +open Rules +open Term +open Tacmach +open Tactics +open Tacticals +open Util + +let mytac ninst solver gl= + let metagen=newcnt () in + let rec toptac ninst seq gl= + match seq.gl with + Atomic t-> + tclORELSE (axiom_tac t seq) (left_tac ninst seq []) gl + | Complex (pat,l)-> + match pat with + Rand->and_tac seq (toptac ninst) metagen gl + | Rforall->forall_tac seq (toptac ninst) metagen gl + | Rarrow->arrow_tac seq (toptac ninst) metagen gl + | _-> + if not (is_empty_left seq) && rev_left seq then + left_tac ninst seq [] gl + else + right_tac ninst seq pat l [] gl + and right_tac ninst seq pat atoms ctx gl= + let re_add s=re_add_left_list ctx s in + match pat with + Ror-> + tclORELSE + (or_tac (re_add seq) (toptac ninst) metagen) + (left_tac ninst seq ctx) gl + | Rexists(i,dom)-> + tclORELSE + (if ninst=0 then tclFAIL 0 "max depth" else + exists_tac i dom atoms (re_add seq) (toptac (ninst-1)) metagen) + (left_tac ninst seq ctx) gl + | _-> anomaly "unreachable place" + and left_tac ninst seq ctx gl= + if is_empty_left seq then + solver gl (* put solver here *) + else + let (hd,seq1)=take_left seq in + let re_add s=re_add_left_list ctx s in + match hd.pat with + Lfalse->left_false_tac hd.id gl + | Land ind->left_and_tac ind hd.id seq1 (toptac ninst) metagen gl + | Lor ind->left_or_tac ind hd.id seq1 (toptac ninst) metagen gl + | Lforall (i,dom)-> + tclORELSE + (if ninst=0 then tclFAIL 0 "max depth" else + left_forall_tac i dom hd.atoms hd.id (re_add seq) + (toptac (ninst-1)) metagen) + (left_tac ninst seq1 (hd::ctx)) gl + | Lexists ->left_exists_tac hd.id seq1 (toptac ninst) metagen gl + | LAatom a-> + let pat,atoms= + match seq1.gl with + Atomic t->assert false + | Complex (pat,atoms)->pat,atoms in + tclORELSE + (ll_atom_tac a hd.id (re_add seq1) (toptac ninst) metagen) + (right_tac ninst seq1 pat atoms (hd::ctx)) gl + | LAfalse->ll_false_tac hd.id seq1 (toptac ninst) metagen gl + | LAand (ind,largs) | LAor(ind,largs) -> + ll_ind_tac ind largs hd.id seq1 (toptac ninst) metagen gl + | LAforall p -> + tclORELSE + (if ninst=0 then tclFAIL 0 "max depth" else + ll_forall_tac p hd.id (re_add seq1) + (toptac (ninst-1)) metagen) + (left_tac ninst seq1 (hd::ctx)) gl + | LAexists (ind,a,p,_) -> + ll_ind_tac ind [a;p] hd.id seq1 (toptac ninst) metagen gl + | LAarrow (a,b,c) -> + tclORELSE + (ll_arrow_tac a b c hd.id (re_add seq1) + (toptac ninst) metagen) + (left_tac ninst seq1 (hd::ctx)) gl in + wrap (List.length (pf_hyps gl)) true empty_seq (toptac ninst) metagen gl + +let default_solver=Tacinterp.interp <:tactic<Auto with *>> + +let default_depth=5 + +TACTIC EXTEND Ground + [ "Ground" ] -> [ mytac default_depth default_solver] +| [ "Ground" integer(n)] -> [ mytac n default_solver] +| [ "Ground" tactic(t)] -> [ mytac default_depth (snd t)] +| [ "Ground" integer(n) tactic(t)] -> [ mytac n (snd t)] +END + + diff --git a/contrib/first-order/formula.ml b/contrib/first-order/formula.ml new file mode 100644 index 0000000000..aee1c01d07 --- /dev/null +++ b/contrib/first-order/formula.ml @@ -0,0 +1,213 @@ +(***********************************************************************) +(* 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 *) +(***********************************************************************) + +(* $Id$ *) + +open Hipattern +open Names +open Term +open Termops +open Reductionops +open Tacmach +open Util +open Declarations + +type ('a,'b)sum=Left of 'a|Right of 'b + +type kind_of_formula= + Arrow of constr*constr + |And of inductive*constr list + |Or of inductive*constr list + |Exists of inductive*constr*constr*constr + |Forall of constr*constr + |Atom of constr + |False + +type counter = bool -> int + +let newcnt ()= + let cnt=ref (-1) in + fun b->if b then incr cnt;!cnt + +let constant path str ()=Coqlib.gen_constant "User" ["Init";path] str + +let op2bool=function Some _->true |None->false + +let id_ex=constant "Logic" "ex" +let id_sig=constant "Specif" "sig" +let id_sigT=constant "Specif" "sigT" +let id_sigS=constant "Specif" "sigS" +let id_not=constant "Logic" "not" + +let is_ex t = + t=(id_ex ()) || + t=(id_sig ()) || + t=(id_sigT ()) || + t=(id_sigS ()) + +let match_with_exist_term t= + match kind_of_term t with + App(t,v)-> + if t=id_ex () && (Array.length v)=2 then + let p=v.(1) in + match kind_of_term p with + Lambda(na,a,b)->Some(t,a,b,p) + | _ ->Some(t,v.(0),mkApp(p,[|mkRel 1|]),p) + else None + | _->None + +let match_with_not_term t= + match match_with_nottype t with + | None -> + (match kind_of_term t with + App (no,b) when no=id_not ()->Some (no,b.(0)) + | _->None) + | o -> o + +let rec nb_prod_after n c= + match kind_of_term c with + | Prod (_,_,b) ->if n>0 then nb_prod_after (n-1) b else + 1+(nb_prod_after 0 b) + | _ -> 0 + +let nhyps mip = + let constr_types = mip.mind_nf_lc in + let nhyps = nb_prod_after mip.mind_nparams in + Array.map nhyps constr_types + +let construct_nhyps ind= nhyps (snd (Global.lookup_inductive ind)) + +(* builds the array of arrays of constructor hyps for (ind Vargs)*) +let ind_hyps ind largs= + let (mib,mip) = Global.lookup_inductive ind in + if Inductiveops.mis_is_recursive (ind,mib,mip) then + failwith "no_recursion" else + let n=mip.mind_nparams in + if n<>(List.length largs) then anomaly "params ?" else + let p=nhyps mip in + let lp=Array.length p in + let types= mip.mind_nf_lc in + let myhyps i= + let t1=Term.prod_applist types.(i) largs in + fst (Sign.decompose_prod_n_assum p.(i) t1) in + Array.init lp myhyps + +let kind_of_formula cciterm = + match match_with_imp_term cciterm with + Some (a,b)-> Arrow(a,(pop b)) + |_-> + match match_with_forall_term cciterm with + Some (_,a,b)-> Forall(a,b) + |_-> + match match_with_exist_term cciterm with + Some (i,a,b,p)-> Exists((destInd i),a,b,p) + |_-> + match match_with_nodep_ind cciterm with + None -> Atom cciterm + | Some (i,l)-> + let ind=destInd i in + let (mib,mip) = Global.lookup_inductive ind in + if Inductiveops.mis_is_recursive (ind,mib,mip) then + Atom cciterm + else + match Array.length mip.mind_consnames with + 0->False + | 1->And(ind,l) + | _->Or(ind,l) + +let build_atoms metagen= + let rec build_rec env polarity cciterm = + match kind_of_formula cciterm with + False->[] + | Arrow (a,b)-> + (build_rec env (not polarity) a)@ + (build_rec env polarity b) + | And(i,l) | Or(i,l)-> + let v = ind_hyps i l in + Array.fold_right + (fun l accu-> + List.fold_right + (fun (_,_,t) accu0-> + (build_rec env polarity t)@accu0) l accu) v [] + | Forall(_,b)|Exists(_,_,b,_)-> + let var=mkMeta (metagen true) in + build_rec (var::env) polarity b + | Atom t-> + [polarity,(substnl env 0 cciterm)] + in build_rec [] + +type right_pattern = + Rand + | Ror + | Rforall + | Rexists of int*constr + | Rarrow + +type right_formula = + Complex of right_pattern*((bool*constr) list) + | Atomic of constr + +type left_pattern= + Lfalse + | Land of inductive + | Lor of inductive + | Lforall of int*constr + | Lexists + | LAatom of constr + | LAfalse + | LAand of inductive*constr list + | LAor of inductive*constr list + | LAforall of constr + | LAexists of inductive*constr*constr*constr + | LAarrow of constr*constr*constr + +type left_formula={id:identifier; + pat:left_pattern; + atoms:(bool*constr) list} + +exception Is_atom of constr + +let build_left_entry nam typ metagen= + try + let pattern= + match kind_of_formula typ with + False -> Lfalse + | Atom a -> raise (Is_atom a) + | And(i,_) -> Land i + | Or(i,_) -> Lor i + | Exists (_,_,_,_) -> Lexists + | Forall (d,_) -> let m=1+(metagen false) in Lforall(m,d) + | Arrow (a,b) -> + (match kind_of_formula a with + False-> LAfalse + | Atom a-> LAatom a + | And(i,l)-> LAand(i,l) + | Or(i,l)-> LAor(i,l) + | Arrow(a,c)-> LAarrow(a,c,b) + | Exists(i,a,_,p)->LAexists(i,a,p,b) + | Forall(_,_)->LAforall a) in + let l=build_atoms metagen false typ in + Left {id=nam;pat=pattern;atoms=l} + with Is_atom a-> Right a + +let build_right_entry typ metagen= + try + let pattern= + match kind_of_formula typ with + False -> raise (Is_atom typ) + | Atom a -> raise (Is_atom a) + | And(_,_) -> Rand + | Or(_,_) -> Ror + | Exists (_,d,_,_) -> + let m=1+(metagen false) in Rexists(m,d) + | Forall (_,a) -> Rforall + | Arrow (a,b) -> Rarrow in + let l=build_atoms metagen true typ in + Complex(pattern,l) + with Is_atom a-> Atomic a + diff --git a/contrib/first-order/formula.mli b/contrib/first-order/formula.mli new file mode 100644 index 0000000000..bb6dc030aa --- /dev/null +++ b/contrib/first-order/formula.mli @@ -0,0 +1,69 @@ +(***********************************************************************) +(* 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 *) +(***********************************************************************) + +(* $Id$ *) + +open Term +open Names + +type ('a,'b) sum = Left of 'a | Right of 'b + +type kind_of_formula= + Arrow of constr*constr + |And of inductive*constr list + |Or of inductive*constr list + |Exists of inductive*constr*constr*constr + |Forall of constr*constr + |Atom of constr + |False + +type counter = bool -> int + +val newcnt : unit -> counter + +val construct_nhyps : inductive -> int array + +val ind_hyps : inductive -> constr list -> Sign.rel_context array + +val kind_of_formula : constr -> kind_of_formula + +type right_pattern = + Rand + | Ror + | Rforall + | Rexists of int*constr + | Rarrow + +type right_formula = + Complex of right_pattern*((bool*constr) list) + | Atomic of constr + +type left_pattern= + Lfalse + | Land of inductive + | Lor of inductive + | Lforall of int*constr + | Lexists + | LAatom of constr + | LAfalse + | LAand of inductive*constr list + | LAor of inductive*constr list + | LAforall of constr + | LAexists of inductive*constr*constr*constr + | LAarrow of constr*constr*constr + +type left_formula={id:identifier; + pat:left_pattern; + atoms:(bool*constr) list} + +val build_left_entry : + identifier -> types -> counter -> (left_formula,types) sum + +val build_right_entry : types -> counter -> right_formula + + diff --git a/contrib/first-order/rules.ml b/contrib/first-order/rules.ml new file mode 100644 index 0000000000..5e2e0a72d6 --- /dev/null +++ b/contrib/first-order/rules.ml @@ -0,0 +1,186 @@ +(***********************************************************************) +(* 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 *) +(***********************************************************************) + +(* $Id$ *) + +open Util +open Names +open Term +open Tacmach +open Tactics +open Tacticals +open Termops +open Reductionops +open Declarations +open Formula +open Sequent +open Unify + +type hptac= Sequent.t -> (Sequent.t -> tactic) -> counter -> tactic + +type lhptac= identifier -> hptac + +let wrap n b seq tacrec metagen gls= + let nc=pf_hyps gls in + let rec aux i nc= + if i<=0 then seq else + match nc with + []->anomaly "Not the expected number of hyps" + | (id,_,typ)::q-> (add_left (id,typ) (aux (i-1) q) metagen) in + let seq1= + if b then + (change_right (pf_concl gls) (aux n nc) metagen) + else + (aux n nc) in + tacrec seq1 gls + +let axiom_tac t seq= + try exact_no_check (mkVar (find_left t seq)) + with Not_found->tclFAIL 0 "No axiom link" + +let and_tac seq tacrec metagen= + tclTHEN simplest_split (wrap 0 true seq tacrec metagen) + +let left_and_tac ind id seq tacrec metagen= + let n=(construct_nhyps ind).(0) in + tclTHENLIST + [simplest_elim (mkVar id); + clear [id]; + tclDO n intro; + wrap n false seq tacrec metagen] + +let or_tac seq tacrec metagen= + any_constructor (Some (tclSOLVE [wrap 0 true seq tacrec metagen])) + +let left_or_tac ind id seq tacrec metagen= + let v=construct_nhyps ind in + let f n= + tclTHENLIST + [clear [id]; + tclDO n intro; + wrap n false seq tacrec metagen] in + tclTHENSV + (simplest_elim (mkVar id)) + (Array.map f v) + +let forall_tac seq tacrec metagen= + tclTHEN intro (wrap 0 true seq tacrec metagen) + +let left_forall_tac i dom atoms id seq tacrec metagen= + let insts=find_instances i atoms seq in + if insts=[] then + tclTHENS (cut dom) + [tclTHENLIST + [intro; + (fun gls->generalize + [mkApp(mkVar id,[|mkVar (Tacmach.pf_nth_hyp_id gls 1)|])] gls); + intro; + tclSOLVE [wrap 1 false seq tacrec metagen]] + ;tclIDTAC] + else + let tac t= + tclTHENLIST + [generalize [mkApp(mkVar id,[|t|])]; + intro; + tclSOLVE [wrap 1 false seq tacrec metagen]] in + tclFIRST (List.map tac insts) + +let arrow_tac seq tacrec metagen= + tclTHEN intro (wrap 1 true seq tacrec metagen) + +let exists_tac i dom atoms seq tacrec metagen= + let insts=find_instances i atoms seq in + if insts=[] then + tclTHENS (cut dom) + [tclTHENLIST + [intro; + (fun gls-> + split (Rawterm.ImplicitBindings + [mkVar (Tacmach.pf_nth_hyp_id gls 1)]) gls); + tclSOLVE [wrap 0 false seq tacrec metagen]] + ;tclIDTAC] + else + let tac t= + tclTHEN (split (Rawterm.ImplicitBindings [t])) + (tclSOLVE [wrap 0 true seq tacrec metagen]) in + tclFIRST (List.map tac insts) + +let left_exists_tac id seq tacrec metagen= + tclTHENLIST + [simplest_elim (mkVar id); + clear [id]; + tclDO 2 intro; + (wrap 1 false seq tacrec metagen)] + +let ll_arrow_tac a b c id seq tacrec metagen= + let cc=mkProd(Anonymous,a,(lift 1 b)) in + let d=mkLambda (Anonymous,b, + mkApp ((mkVar id), + [|mkLambda (Anonymous,(lift 1 a),(mkRel 2))|])) in + tclTHENS (cut c) + [tclTHENLIST + [intro; + clear [id]; + wrap 1 false seq tacrec metagen]; + tclTHENS (cut cc) + [exact_no_check (mkVar id); + tclTHENLIST + [generalize [d]; + intro; + clear [id]; + tclSOLVE [wrap 1 true seq tacrec metagen]]]] + +let ll_atom_tac a id seq tacrec metagen= + try + tclTHENLIST + [generalize [mkApp(mkVar id,[|mkVar (find_left a seq)|])]; + clear [id]; + intro; + wrap 1 false seq tacrec metagen] + with Not_found->tclFAIL 0 "No link" + +let ll_false_tac id seq tacrec metagen= + tclTHEN (clear [id]) (wrap 0 false seq tacrec metagen) + +let left_false_tac id= + simplest_elim (mkVar id) + +(*We use this function for and, or, exists*) + +let ll_ind_tac ind largs id seq tacrec metagen gl= + (try + let rcs=ind_hyps ind largs in + let vargs=Array.of_list largs in + (* construire le terme H->B, le generaliser etc *) + let myterm i= + let rc=rcs.(i) in + let p=List.length rc in + let cstr=mkApp ((mkConstruct (ind,(i+1))),vargs) in + let vars=Array.init p (fun j->mkRel (p-j)) in + let capply=mkApp ((lift p cstr),vars) in + let head=mkApp ((lift p (mkVar id)),[|capply|]) in + Sign.it_mkLambda_or_LetIn head rc in + let lp=Array.length rcs in + let newhyps=List.map myterm (interval 0 (lp-1)) in + tclTHENLIST + [generalize newhyps; + clear [id]; + tclDO lp intro; + wrap lp false seq tacrec metagen] + with Invalid_argument _ ->tclFAIL 0 "") gl + +let ll_forall_tac prod id seq tacrec metagen= + tclTHENS (cut prod) + [tclTHENLIST + [(fun gls->generalize + [mkApp(mkVar id,[|mkVar (Tacmach.pf_nth_hyp_id gls 1)|])] gls); + clear [id]; + intro; + tclSOLVE [wrap 1 false seq tacrec metagen]]; + tclSOLVE [wrap 0 true seq tacrec metagen]] + diff --git a/contrib/first-order/rules.mli b/contrib/first-order/rules.mli new file mode 100644 index 0000000000..98dc01bbed --- /dev/null +++ b/contrib/first-order/rules.mli @@ -0,0 +1,51 @@ +(***********************************************************************) +(* 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 *) +(***********************************************************************) + +(* $Id$ *) + +open Term +open Tacmach +open Names + +type hptac= Sequent.t -> (Sequent.t -> tactic) -> Formula.counter -> tactic + +type lhptac= identifier -> hptac + +val wrap : int -> bool -> hptac + +val axiom_tac : constr -> Sequent.t -> tactic + +val and_tac : hptac + +val left_and_tac : inductive -> lhptac + +val or_tac : hptac + +val left_or_tac : inductive -> lhptac + +val forall_tac : hptac + +val left_forall_tac : int -> types -> (bool * constr) list -> lhptac + +val arrow_tac : hptac + +val exists_tac : int -> types -> (bool * constr) list -> hptac + +val left_exists_tac : lhptac + +val ll_arrow_tac : constr -> constr -> constr -> lhptac + +val ll_atom_tac : constr -> lhptac + +val ll_false_tac : lhptac + +val left_false_tac : identifier -> tactic + +val ll_ind_tac : inductive -> constr list -> lhptac + +val ll_forall_tac : types -> lhptac diff --git a/contrib/first-order/sequent.ml b/contrib/first-order/sequent.ml new file mode 100644 index 0000000000..84e3f18ed4 --- /dev/null +++ b/contrib/first-order/sequent.ml @@ -0,0 +1,97 @@ +(***********************************************************************) +(* 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 *) +(***********************************************************************) + +(* $Id$ *) + +open Term +open Util +open Formula +open Tacmach +open Names + +let priority=function (* pure heuristics, <=0 for non reversible *) + Lfalse ->1000 + | Land _ -> 90 + | Lor _ -> 40 + | Lforall (_,_) -> -20 + | Lexists -> 60 + | LAatom _ -> 0 + | LAfalse -> 100 + | LAand (_,_) -> 80 + | LAor (_,_) -> 70 + | LAforall _ -> -30 + | LAexists (_,_,_,_) -> 50 + | LAarrow (_,_,_) -> -10 + + +let right_atomic=function + Atomic _->true + | Complex (_,_) ->false + +let right_reversible= + function + Rarrow | Rand | Rforall->true + | _ ->false + +let left_reversible lpat=(priority lpat)>0 + +module OrderedFormula= +struct + type t=left_formula + let compare e1 e2=(priority e1.pat) - (priority e2.pat) +end + +module OrderedConstr= +struct + type t=constr + let compare=Pervasives.compare +end + +module CM=Map.Make(OrderedConstr) + +module HP=Heap.Functional(OrderedFormula) + +type t= + {hyps:HP.t;hatoms:identifier CM.t;gl:right_formula} + +let add_left (nam,t) seq metagen= + match build_left_entry nam t metagen with + Left f->{seq with hyps=HP.add f seq.hyps} + | Right t->{seq with hatoms=CM.add t nam seq.hatoms} + +let re_add_left_list lf seq= + {seq with hyps=List.fold_right HP.add lf seq.hyps} + +let change_right t seq metagen= + {seq with gl=build_right_entry t metagen} + +let find_left t seq=CM.find t seq.hatoms + +let atomic_right seq= right_atomic seq.gl + +let rev_left seq= + try + let lpat=(HP.maximum seq.hyps).pat in + left_reversible lpat + with Heap.EmptyHeap -> false + +let is_empty_left seq= + seq.hyps=HP.empty + +let take_left seq= + let hd=HP.maximum seq.hyps + and hp=HP.remove seq.hyps in + hd,{seq with hyps=hp} + +let take_right seq=seq.gl + +let empty_seq= + {hyps=HP.empty; + hatoms=CM.empty; + gl=Atomic (mkMeta 1)} + diff --git a/contrib/first-order/sequent.mli b/contrib/first-order/sequent.mli new file mode 100644 index 0000000000..8b72b3f210 --- /dev/null +++ b/contrib/first-order/sequent.mli @@ -0,0 +1,44 @@ +(***********************************************************************) +(* 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 *) +(***********************************************************************) + +(* $Id$ *) + +open Term +open Util +open Formula +open Tacmach +open Names + +val right_reversible : right_pattern -> bool + +val left_reversible : left_pattern -> bool + +module CM: Map.S with type key=constr + +module HP: Heap.S with type elt=left_formula + +type t = {hyps:HP.t;hatoms: identifier CM.t;gl:right_formula} + +val add_left : identifier * constr -> t -> counter -> t + +val re_add_left_list : left_formula list -> t -> t + +val change_right : constr -> t -> counter -> t + +val find_left : constr -> t -> identifier + +val rev_left : t -> bool + +val is_empty_left : t -> bool + +val take_left : t -> left_formula * t + +val take_right : t -> right_formula + +val empty_seq : t + diff --git a/contrib/first-order/unify.ml b/contrib/first-order/unify.ml new file mode 100644 index 0000000000..9d6bb39d31 --- /dev/null +++ b/contrib/first-order/unify.ml @@ -0,0 +1,131 @@ +(***********************************************************************) +(* 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 Formula +open Sequent +open Tacmach +open Term +open Termops +open Reductionops + +exception UFAIL of constr*constr + +let unif t1 t2= (* Martelli-Montanari style *) + let bige=Queue.create () + and sigma=ref [] in + let bind i t= + sigma:=(i,t):: + (List.map (function (n,tn)->(n,subst_meta [i,t] tn)) !sigma) in + let rec head_reduce t= + (* forbids non-sigma-normal meta in head position*) + match kind_of_term t with + Meta i-> + (try + head_reduce (List.assoc i !sigma) + with Not_found->t) + | _->t in + Queue.add (t1,t2) bige; + try while true do + let t1,t2=Queue.take bige in + let nt1=head_reduce (whd_betaiotazeta t1) + and nt2=head_reduce (whd_betaiotazeta t2) in + match (kind_of_term nt1),(kind_of_term nt2) with + Meta i,Meta j-> + if i<>j then + if i<j then bind j nt1 + else bind i nt2 + | Meta i,_ -> + let t=subst_meta !sigma nt2 in + if Intset.is_empty (free_rels t) && + not (occur_term (mkMeta i) t) then + bind i t else raise (UFAIL(nt1,nt2)) + | _,Meta i -> + let t=subst_meta !sigma nt1 in + if Intset.is_empty (free_rels t) && + not (occur_term (mkMeta i) t) then + bind i t else raise (UFAIL(nt1,nt2)) + | Cast(_,_),_->Queue.add (strip_outer_cast nt1,nt2) bige + | _,Cast(_,_)->Queue.add (nt1,strip_outer_cast nt2) bige + | (Prod(_,a,b),Prod(_,c,d))|(Lambda(_,a,b),Lambda(_,c,d))-> + Queue.add (a,c) bige;Queue.add (pop b,pop d) bige + | Case (_,pa,ca,va),Case (_,pb,cb,vb)-> + Queue.add (pa,pb) bige; + Queue.add (ca,cb) bige; + let l=Array.length va in + if l<>(Array.length vb) then + raise (UFAIL (nt1,nt2)) + else + for i=0 to l-1 do + Queue.add (va.(i),vb.(i)) bige + done + | App(ha,va),App(hb,vb)-> + Queue.add (ha,hb) bige; + let l=Array.length va in + if l<>(Array.length vb) then + raise (UFAIL (nt1,nt2)) + else + for i=0 to l-1 do + Queue.add (va.(i),vb.(i)) bige + done + | _->if not (eq_constr nt1 nt2) then raise (UFAIL (nt1,nt2)) + done; + assert false + (* this place is unreachable but needed for the sake of typing *) + with Queue.Empty-> !sigma + +(* collect tries finds ground instantiations for Meta i*) +let is_ground t=(Clenv.collect_metas t)=[] + +let collect i l= + try + let t=List.assoc i l in + if is_ground t then Some t else None + with Not_found->None + +let unif_atoms_for_meta i (b1,t1) (b2,t2)= + if b1=b2 then None else + try + collect i (unif t1 t2) + with UFAIL(_,_) ->None + +module OrderedConstr= +struct + type t=constr + let compare=Pervasives.compare +end + +module CS=Set.Make(OrderedConstr) + +let match_atom_list i atom l= + let f atom2 accu= + match unif_atoms_for_meta i atom atom2 with + None-> accu + | Some t-> CS.add t accu in + List.fold_right f l CS.empty + +let match_lists i l1 l2= + let f atom accu= + CS.union (match_atom_list i atom l2) accu in + List.fold_right f l1 CS.empty + +let find_instances i l seq= + let match_hyp f accu= + CS.union (match_lists i l f.atoms) accu in + let match_atom t nam accu= + CS.union (match_atom_list i (false,t) l) accu in + let s1= + match seq.gl with + Atomic t->(match_atom_list i (true,t) l) + | Complex(_,l1)->(match_lists i l l1) in + let s2=CM.fold match_atom seq.hatoms s1 in + let s3=HP.fold match_hyp seq.hyps s2 in + CS.fold (fun x l->x::l) s3 [] + diff --git a/contrib/first-order/unify.mli b/contrib/first-order/unify.mli new file mode 100644 index 0000000000..04d7951014 --- /dev/null +++ b/contrib/first-order/unify.mli @@ -0,0 +1,13 @@ +(***********************************************************************) +(* 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 *) +(***********************************************************************) + +(* $Id$ *) + +open Term + +val find_instances : int -> (bool * constr) list -> Sequent.t -> constr list |