diff options
Diffstat (limited to 'contrib/first-order')
| -rw-r--r-- | contrib/first-order/formula.ml | 132 | ||||
| -rw-r--r-- | contrib/first-order/formula.mli | 4 | ||||
| -rw-r--r-- | contrib/first-order/ground.ml | 95 | ||||
| -rw-r--r-- | contrib/first-order/instances.ml | 20 | ||||
| -rw-r--r-- | contrib/first-order/instances.mli | 5 | ||||
| -rw-r--r-- | contrib/first-order/rules.ml | 142 | ||||
| -rw-r--r-- | contrib/first-order/rules.mli | 20 | ||||
| -rw-r--r-- | contrib/first-order/sequent.ml | 38 |
8 files changed, 249 insertions, 207 deletions
diff --git a/contrib/first-order/formula.ml b/contrib/first-order/formula.ml index bce1ef24e..7901e0d40 100644 --- a/contrib/first-order/formula.ml +++ b/contrib/first-order/formula.ml @@ -79,13 +79,14 @@ let match_with_evaluable gl t= type kind_of_formula= Arrow of constr*constr | False of inductive*constr list - | And of inductive*constr list - | Or of inductive*constr list + | And of inductive*constr list*bool + | Or of inductive*constr list*bool | Exists of inductive*constr list | Forall of constr*constr | Atom of constr let rec kind_of_formula gl term = + let normalize t=nf_betadeltaiota (pf_env gl) (Refiner.sig_sig gl) t in let cciterm=whd_betaiotazeta term in match match_with_imp_term cciterm with Some (a,b)-> Arrow(a,(pop b)) @@ -94,16 +95,23 @@ let rec kind_of_formula gl term = Some (_,a,b)-> Forall(a,b) |_-> match match_with_nodep_ind cciterm with - Some (i,l)-> + Some (i,l,n)-> let ind=destInd i in + let has_realargs=(n>0) in let (mib,mip) = Global.lookup_inductive ind in - if Inductiveops.mis_is_recursive (ind,mib,mip) then + let is_trivial= + let is_constant c = + nb_prod c = mip.mind_nparams in + array_exists is_constant mip.mind_nf_lc in + if Inductiveops.mis_is_recursive (ind,mib,mip) || + (has_realargs && not is_trivial) + then Atom cciterm else (match Array.length mip.mind_consnames with 0->False(ind,l) - | 1->And(ind,l) - | _->Or(ind,l)) + | 1->And(ind,l,is_trivial) + | _->Or(ind,l,is_trivial)) | _ -> match match_with_sigma_type cciterm with Some (i,l)-> Exists((destInd i),l) @@ -114,9 +122,7 @@ let rec kind_of_formula gl term = (pf_env gl) (Refiner.sig_sig gl) t in kind_of_formula gl nt - | None ->Atom (nf_betadeltaiota - (pf_env gl) - (Refiner.sig_sig gl) cciterm) + | None ->Atom (normalize cciterm) type atoms = {positive:constr list;negative:constr list} @@ -128,14 +134,22 @@ let build_atoms gl metagen polarity cciterm = let trivial =ref false and positive=ref [] and negative=ref [] in - let pfenv=lazy (pf_env gl) in - let rec build_rec env polarity cciterm = + let normalize t=nf_betadeltaiota (pf_env gl) (Refiner.sig_sig gl) t in + let rec build_rec env polarity cciterm= match kind_of_formula gl cciterm with False(_,_)->if not polarity then trivial:=true | Arrow (a,b)-> build_rec env (not polarity) a; build_rec env polarity b - | And(i,l) | Or(i,l)-> + | And(i,l,b) | Or(i,l,b)-> + if b then + begin + let unsigned=normalize (substnl env 0 cciterm) in + if polarity then + positive:= unsigned :: !positive + else + negative:= unsigned :: !negative + end; let v = ind_hyps 0 i l in let g i _ (_,_,t) = build_rec env polarity (lift i t) in @@ -165,8 +179,7 @@ let build_atoms gl metagen polarity cciterm = (!trivial, {positive= !positive; negative= !negative}) - - + type right_pattern = Rarrow | Rand @@ -198,52 +211,59 @@ type t={id:global_reference; atoms:atoms} let build_formula side nam typ gl metagen= - try - let m=meta_succ(metagen false) in - let trivial,atoms= - if !qflag then - build_atoms gl metagen side typ - else no_atoms in - let pattern= - if side then - let pat= - match kind_of_formula gl typ with - False(_,_) -> Rfalse - | Atom a -> raise (Is_atom a) - | And(_,_) -> Rand - | Or(_,_) -> Ror - | Exists (i,l) -> - let (_,_,d)=list_last (ind_hyps 0 i l).(0) in - Rexists(m,d,trivial) - | Forall (_,a) -> Rforall - | Arrow (a,b) -> Rarrow in - Right pat - else - let pat= - match kind_of_formula gl typ with - False(i,_) -> Lfalse - | Atom a -> raise (Is_atom a) - | And(i,_) -> Land i - | Or(i,_) -> Lor i - | Exists (ind,_) -> Lexists ind - | Forall (d,_) -> - Lforall(m,d,trivial) - | Arrow (a,b) -> - let nfa=nf_betadeltaiota (pf_env gl) (Refiner.sig_sig gl) a in - LA (nfa, + let normalize t=nf_betadeltaiota (pf_env gl) (Refiner.sig_sig gl) t in + try + let m=meta_succ(metagen false) in + let trivial,atoms= + if !qflag then + build_atoms gl metagen side typ + else no_atoms in + let pattern= + if side then + let pat= + match kind_of_formula gl typ with + False(_,_) -> Rfalse + | Atom a -> raise (Is_atom a) + | And(_,_,_) -> Rand + | Or(_,_,_) -> Ror + | Exists (i,l) -> + let (_,_,d)=list_last (ind_hyps 0 i l).(0) in + Rexists(m,d,trivial) + | Forall (_,a) -> Rforall + | Arrow (a,b) -> Rarrow in + Right pat + else + let pat= + match kind_of_formula gl typ with + False(i,_) -> Lfalse + | Atom a -> raise (Is_atom a) + | And(i,_,b) -> + if b then + let nftyp=normalize typ in raise (Is_atom nftyp) + else Land i + | Or(i,_,b) -> + if b then + let nftyp=normalize typ in raise (Is_atom nftyp) + else Lor i + | Exists (ind,_) -> Lexists ind + | Forall (d,_) -> + Lforall(m,d,trivial) + | Arrow (a,b) -> + let nfa=normalize a in + LA (nfa, match kind_of_formula gl a with False(i,l)-> LLfalse(i,l) | Atom t-> LLatom - | And(i,l)-> LLand(i,l) - | Or(i,l)-> LLor(i,l) + | And(i,l,_)-> LLand(i,l) + | Or(i,l,_)-> LLor(i,l) | Arrow(a,c)-> LLarrow(a,c,b) | Exists(i,l)->LLexists(i,l) | Forall(_,_)->LLforall a) in - Left pat - in - Left {id=nam; - constr=nf_betadeltaiota (pf_env gl) (Refiner.sig_sig gl) typ; - pat=pattern; - atoms=atoms} - with Is_atom a-> Right a (* already in nf *) + Left pat + in + Left {id=nam; + constr=normalize typ; + pat=pattern; + atoms=atoms} + with Is_atom a-> Right a (* already in nf *) diff --git a/contrib/first-order/formula.mli b/contrib/first-order/formula.mli index cbf3dc152..35ae80f59 100644 --- a/contrib/first-order/formula.mli +++ b/contrib/first-order/formula.mli @@ -30,7 +30,7 @@ val ind_hyps : int -> inductive -> constr list -> Sign.rel_context array val match_with_evaluable : Proof_type.goal Tacmach.sigma -> constr -> (evaluable_global_reference * constr) option - +(* type kind_of_formula = Arrow of constr*constr | False of inductive*constr list @@ -42,7 +42,7 @@ type kind_of_formula = val kind_of_formula : Proof_type.goal Tacmach.sigma -> constr -> kind_of_formula - +*) type atoms = {positive:constr list;negative:constr list} val dummy_id: global_reference diff --git a/contrib/first-order/ground.ml b/contrib/first-order/ground.ml index cc63b4afc..7571da2de 100644 --- a/contrib/first-order/ground.ml +++ b/contrib/first-order/ground.ml @@ -27,30 +27,32 @@ let ground_tac solver startseq gl= let (hd,seq1)=take_formula seq and re_add s=re_add_formula_list skipped s in let continue=toptac [] - and backtrack=toptac (hd::skipped) seq1 in + and backtrack gl=toptac (hd::skipped) seq1 gl in match hd.pat with Right rpat-> begin match rpat with Rand-> - and_tac continue (re_add seq1) + and_tac backtrack continue (re_add seq1) | Rforall-> - forall_tac continue (re_add seq1) + let backtrack1= + if !qflag then + tclFAIL 0 "reversible in 1st order mode" + else + backtrack in + forall_tac backtrack continue (re_add seq1) | Rarrow-> arrow_tac continue (re_add seq1) | Ror-> - tclORELSE - (or_tac continue (re_add seq1)) - backtrack + or_tac backtrack continue (re_add seq1) | Rfalse->backtrack | Rexists(i,dom,triv)-> let (lfp,seq2)=collect_quantified seq in let backtrack2=toptac (lfp@skipped) seq2 in - tclORELSE - (if seq.depth<=0 || not !qflag then - tclFAIL 0 "max depth" - else - quantified_tac lfp continue (re_add seq1)) + if !qflag && seq.depth>0 then + quantified_tac lfp backtrack2 + continue (re_add seq) + else backtrack2 (* need special backtracking *) end | Left lpat-> @@ -59,53 +61,50 @@ let ground_tac solver startseq gl= Lfalse-> left_false_tac hd.id | Land ind-> - left_and_tac ind hd.id continue (re_add seq1) + left_and_tac ind backtrack + hd.id continue (re_add seq1) | Lor ind-> - left_or_tac ind hd.id continue (re_add seq1) + left_or_tac ind backtrack + hd.id continue (re_add seq1) | Lforall (_,_,_)-> let (lfp,seq2)=collect_quantified seq in let backtrack2=toptac (lfp@skipped) seq2 in - tclORELSE - (if seq.depth<=0 || not !qflag then - tclFAIL 0 "max depth" - else - quantified_tac lfp continue (re_add seq)) + if !qflag && seq.depth>0 then + quantified_tac lfp backtrack2 + continue (re_add seq) + else backtrack2 (* need special backtracking *) - | Lexists ind -> - if !qflag then + | Lexists ind -> + if !qflag then left_exists_tac ind hd.id continue (re_add seq1) else backtrack | LA (typ,lap)-> - tclORELSE - (ll_atom_tac typ hd.id continue (re_add seq1)) - begin - match lap with - LLatom -> backtrack - | LLand (ind,largs) | LLor(ind,largs) - | LLfalse (ind,largs)-> - (ll_ind_tac ind largs hd.id continue - (re_add seq1)) - | LLforall p -> - if seq.depth<=0 || not !qflag then - backtrack - else - tclORELSE - (ll_forall_tac p hd.id continue - (re_add seq1)) + let la_tac= + begin + match lap with + LLatom -> backtrack + | LLand (ind,largs) | LLor(ind,largs) + | LLfalse (ind,largs)-> + (ll_ind_tac ind largs backtrack + hd.id continue (re_add seq1)) + | LLforall p -> + if seq.depth>0 && !qflag then + (ll_forall_tac p backtrack + hd.id continue (re_add seq1)) + else backtrack + | LLexists (ind,l) -> + if !qflag then + ll_ind_tac ind l backtrack + hd.id continue (re_add seq1) + else backtrack - | LLexists (ind,l) -> - if !qflag then - ll_ind_tac ind l hd.id continue - (re_add seq1) - else - backtrack - | LLarrow (a,b,c) -> - tclORELSE - (ll_arrow_tac a b c hd.id continue - (re_add seq1)) - backtrack - end + | LLarrow (a,b,c) -> + (ll_arrow_tac a b c backtrack + hd.id continue (re_add seq1)) + end in + ll_atom_tac typ la_tac hd.id continue (re_add seq1) end with Heap.EmptyHeap->solver end gl in wrap (List.length (pf_hyps gl)) true (toptac []) (startseq gl) gl + diff --git a/contrib/first-order/instances.ml b/contrib/first-order/instances.ml index f8076b72c..4e57bd3ca 100644 --- a/contrib/first-order/instances.ml +++ b/contrib/first-order/instances.ml @@ -31,7 +31,7 @@ let compare_instance inst1 inst2= Phantom(d1),Phantom(d2)-> (OrderedConstr.compare d1 d2) | Real((m1,c1),n1),Real((m2,c2),n2)-> - ((-) =? (-) ==? OrderedConstr.compare) m1 m2 n1 n2 c1 c2 + ((-) =? (-) ==? OrderedConstr.compare) m2 m1 n1 n2 c1 c2 | Phantom(_),Real((m,_),_)-> if m=0 then -1 else 1 | Real((m,_),_),Phantom(_)-> if m=0 then 1 else -1 @@ -132,7 +132,7 @@ let mk_open_instance id gl m t= (* tactics *) -let left_instance_tac (inst,id) tacrec seq= +let left_instance_tac (inst,id) continue seq= match inst with Phantom dom-> if lookup (id,None) seq then @@ -145,7 +145,7 @@ let left_instance_tac (inst,id) tacrec seq= [mkApp(constr_of_reference id, [|mkVar (Tacmach.pf_nth_hyp_id gls 1)|])] gls); introf; - tclSOLVE [wrap 1 false tacrec + tclSOLVE [wrap 1 false continue (deepen (record (id,None) seq))]]; tclTRY assumption] | Real((m,t) as c,_)-> @@ -167,9 +167,9 @@ let left_instance_tac (inst,id) tacrec seq= [special_generalize; introf; tclSOLVE - [wrap 1 false tacrec (deepen (record (id,Some c) seq))]] + [wrap 1 false continue (deepen (record (id,Some c) seq))]] -let right_instance_tac inst tacrec seq= +let right_instance_tac inst continue seq= match inst with Phantom dom -> tclTHENS (cut dom) @@ -178,11 +178,11 @@ let right_instance_tac inst tacrec seq= (fun gls-> split (Rawterm.ImplicitBindings [mkVar (Tacmach.pf_nth_hyp_id gls 1)]) gls); - tclSOLVE [wrap 0 false tacrec (deepen seq)]]; + tclSOLVE [wrap 0 false continue (deepen seq)]]; tclTRY assumption] | Real ((0,t),_) -> (tclTHEN (split (Rawterm.ImplicitBindings [t])) - (tclSOLVE [wrap 0 true tacrec (deepen seq)])) + (tclSOLVE [wrap 0 true continue (deepen seq)])) | Real ((m,t),_) -> tclFAIL 0 "not implemented ... yet" @@ -192,8 +192,10 @@ let instance_tac inst= else left_instance_tac inst -let quantified_tac lf tacrec seq gl= +let quantified_tac lf backtrack continue seq gl= let insts=give_instances lf seq in - tclFIRST (List.map (fun inst->instance_tac inst tacrec seq) insts) gl + tclORELSE + (tclFIRST (List.map (fun inst->instance_tac inst continue seq) insts)) + backtrack gl diff --git a/contrib/first-order/instances.mli b/contrib/first-order/instances.mli index ed85308cd..b4f745918 100644 --- a/contrib/first-order/instances.mli +++ b/contrib/first-order/instances.mli @@ -16,7 +16,10 @@ open Rules val collect_quantified : Sequent.t -> Formula.t list * Sequent.t -val quantified_tac : Formula.t list -> seqtac +val give_instances : Formula.t list -> Sequent.t -> + (Unify.instance * global_reference) list + +val quantified_tac : Formula.t list -> seqtac with_backtracking diff --git a/contrib/first-order/rules.ml b/contrib/first-order/rules.ml index be91c9ec5..12593de70 100644 --- a/contrib/first-order/rules.ml +++ b/contrib/first-order/rules.ml @@ -24,7 +24,9 @@ type seqtac= (Sequent.t -> tactic) -> Sequent.t -> tactic type lseqtac= global_reference -> seqtac -let wrap n b tacrec seq gls= +type 'a with_backtracking = tactic -> 'a + +let wrap n b continue seq gls= check_for_interrupt (); let nc=pf_hyps gls in let env=pf_env gls in @@ -41,7 +43,7 @@ let wrap n b tacrec seq gls= let seq1=aux n nc [] in let seq2=if b then add_formula true dummy_id (pf_concl gls) seq1 gls else seq1 in - tacrec seq2 gls + continue seq2 gls let id_of_global=function VarRef id->id @@ -58,47 +60,53 @@ let axiom_tac t seq= try exact_no_check (constr_of_reference (find_left t seq)) with Not_found->tclFAIL 0 "No axiom link" -let ll_atom_tac a id tacrec seq= - try - tclTHENLIST - [generalize [mkApp(constr_of_reference id, - [|constr_of_reference (find_left a seq)|])]; - clear_global id; - introf; - wrap 1 false tacrec seq] - with Not_found->tclFAIL 0 "No link" +let ll_atom_tac a backtrack id continue seq= + tclIFTHENELSE + (try + tclTHENLIST + [generalize [mkApp(constr_of_reference id, + [|constr_of_reference (find_left a seq)|])]; + clear_global id; + introf] + with Not_found->tclFAIL 0 "No link") + (wrap 1 false continue seq) backtrack (* right connectives rules *) -let and_tac tacrec seq= - tclTHEN simplest_split (wrap 0 true tacrec seq) +let and_tac backtrack continue seq= + tclIFTHENELSE simplest_split (wrap 0 true continue seq) backtrack -let or_tac tacrec seq= - any_constructor (Some (tclSOLVE [wrap 0 true tacrec seq])) +let or_tac backtrack continue seq= + tclORELSE + (any_constructor (Some (tclSOLVE [wrap 0 true continue seq]))) + backtrack -let arrow_tac tacrec seq= - tclTHEN introf (wrap 1 true tacrec seq) +let arrow_tac continue seq= + tclTHEN introf (wrap 1 true continue seq) (* left connectives rules *) -let left_and_tac ind id tacrec seq= - let n=(construct_nhyps ind).(0) in - tclTHENLIST +let left_and_tac ind backtrack id continue seq= + let n=(construct_nhyps ind).(0) in + tclIFTHENELSE + (tclTHENLIST [simplest_elim (constr_of_reference id); clear_global id; - tclDO n introf; - wrap n false tacrec seq] + tclDO n introf]) + (wrap n false continue seq) + backtrack -let left_or_tac ind id tacrec seq= +let left_or_tac ind backtrack id continue seq= let v=construct_nhyps ind in let f n= tclTHENLIST [clear_global id; tclDO n introf; - wrap n false tacrec seq] in - tclTHENSV + wrap n false continue seq] in + tclIFTHENSVELSE (simplest_elim (constr_of_reference id)) (Array.map f v) + backtrack let left_false_tac id= simplest_elim (constr_of_reference id) @@ -107,8 +115,7 @@ let left_false_tac id= (* We use this function for false, and, or, exists *) -let ll_ind_tac ind largs id tacrec seq gl= - (try +let ll_ind_tac ind largs backtrack id continue seq gl= let rcs=ind_hyps 0 ind largs in let vargs=Array.of_list largs in (* construire le terme H->B, le generaliser etc *) @@ -122,56 +129,65 @@ let ll_ind_tac ind largs id tacrec seq gl= Sign.it_mkLambda_or_LetIn head rc in let lp=Array.length rcs in let newhyps=list_tabulate myterm lp in - tclTHENLIST - [generalize newhyps; - clear_global id; - tclDO lp introf; - wrap lp false tacrec seq] - with Invalid_argument _ ->tclFAIL 0 "") gl - -let ll_arrow_tac a b c id tacrec seq= + tclIFTHENELSE + (tclTHENLIST + [generalize newhyps; + clear_global id; + tclDO lp introf]) + (wrap lp false continue seq) backtrack gl + +let ll_arrow_tac a b c backtrack id continue seq= let cc=mkProd(Anonymous,a,(lift 1 b)) in let d=mkLambda (Anonymous,b, mkApp ((constr_of_reference id), [|mkLambda (Anonymous,(lift 1 a),(mkRel 2))|])) in - tclTHENS (cut c) - [tclTHENLIST - [introf; - clear_global id; - wrap 1 false tacrec seq]; - tclTHENS (cut cc) - [exact_no_check (constr_of_reference id); - tclTHENLIST - [generalize [d]; - introf; + tclORELSE + (tclTHENS (cut c) + [tclTHENLIST + [introf; clear_global id; - tclSOLVE [wrap 1 true tacrec seq]]]] + wrap 1 false continue seq]; + tclTHENS (cut cc) + [exact_no_check (constr_of_reference id); + tclTHENLIST + [generalize [d]; + introf; + clear_global id; + tclSOLVE [wrap 1 true continue seq]]]]) + backtrack (* quantifier rules (easy side) *) -let forall_tac tacrec seq= - tclTHEN introf (wrap 0 true tacrec seq) +let forall_tac backtrack continue seq= + tclORELSE + (tclTHEN introf (wrap 0 true continue seq)) + (if !qflag then + tclFAIL 0 "reversible in 1st order mode" + else + backtrack) -let left_exists_tac ind id tacrec seq= +let left_exists_tac ind id continue seq= let n=(construct_nhyps ind).(0) in tclTHENLIST [simplest_elim (constr_of_reference id); clear_global id; tclDO n introf; - (wrap (n-1) false tacrec seq)] - -let ll_forall_tac prod id tacrec seq= - tclTHENS (cut prod) - [tclTHENLIST - [introf; - (fun gls-> - let id0=pf_nth_hyp_id gls 1 in - let term=mkApp((constr_of_reference id),[|mkVar(id0)|]) in - tclTHEN (generalize [term]) (clear [id0]) gls); - clear_global id; - introf; - tclSOLVE [wrap 1 false tacrec (deepen seq)]]; - tclSOLVE [wrap 0 true tacrec (deepen seq)]] + (wrap (n-1) false continue seq)] + +let ll_forall_tac prod backtrack id continue seq= + tclORELSE + (tclTHENS (cut prod) + [tclTHENLIST + [introf; + (fun gls-> + let id0=pf_nth_hyp_id gls 1 in + let term=mkApp((constr_of_reference id),[|mkVar(id0)|]) in + tclTHEN (generalize [term]) (clear [id0]) gls); + clear_global id; + introf; + tclSOLVE [wrap 1 false continue (deepen seq)]]; + tclSOLVE [wrap 0 true continue (deepen seq)]]) + backtrack (* rules for instantiation with unification moved to instances.ml *) diff --git a/contrib/first-order/rules.mli b/contrib/first-order/rules.mli index afccfcd1b..c5c15fdd5 100644 --- a/contrib/first-order/rules.mli +++ b/contrib/first-order/rules.mli @@ -17,6 +17,8 @@ type seqtac= (Sequent.t -> tactic) -> Sequent.t -> tactic type lseqtac= global_reference -> seqtac +type 'a with_backtracking = tactic -> 'a + val wrap : int -> bool -> seqtac val id_of_global: global_reference -> identifier @@ -25,28 +27,28 @@ val clear_global: global_reference -> tactic val axiom_tac : constr -> Sequent.t -> tactic -val ll_atom_tac : constr -> lseqtac +val ll_atom_tac : constr -> lseqtac with_backtracking -val and_tac : seqtac +val and_tac : seqtac with_backtracking -val or_tac : seqtac +val or_tac : seqtac with_backtracking val arrow_tac : seqtac -val left_and_tac : inductive -> lseqtac +val left_and_tac : inductive -> lseqtac with_backtracking -val left_or_tac : inductive -> lseqtac +val left_or_tac : inductive -> lseqtac with_backtracking val left_false_tac : global_reference -> tactic -val ll_ind_tac : inductive -> constr list -> lseqtac +val ll_ind_tac : inductive -> constr list -> lseqtac with_backtracking -val ll_arrow_tac : constr -> constr -> constr -> lseqtac +val ll_arrow_tac : constr -> constr -> constr -> lseqtac with_backtracking -val forall_tac : seqtac +val forall_tac : seqtac with_backtracking val left_exists_tac : inductive -> lseqtac -val ll_forall_tac : types -> lseqtac +val ll_forall_tac : types -> lseqtac with_backtracking val normalize_evaluables : tactic diff --git a/contrib/first-order/sequent.ml b/contrib/first-order/sequent.ml index 4c18090b9..4d074f67f 100644 --- a/contrib/first-order/sequent.ml +++ b/contrib/first-order/sequent.ml @@ -26,29 +26,29 @@ let priority = (* pure heuristics, <=0 for non reversible *) Right rf-> begin match rf with - Rarrow -> 100 - | Rand -> 40 - | Ror -> -15 - | Rfalse -> -50 (* dead end for sure *) - | Rforall -> 100 - | Rexists (_,_,_) -> -30 + Rarrow -> 100 + | Rand -> 40 + | Ror -> -15 + | Rfalse -> -50 + | Rforall -> 100 + | Rexists (_,_,_) -> -29 end | Left lf -> match lf with - Lfalse -> 1000 (* yipee ! *) - | Land _ -> 90 - | Lor _ -> 40 - | Lforall (_,_,_) -> -30 (* must stay at lowest priority *) - | Lexists _ -> 60 + Lfalse -> 999 + | Land _ -> 90 + | Lor _ -> 40 + | Lforall (_,_,_) -> -30 + | Lexists _ -> 60 | LA(_,lap) -> match lap with - LLatom -> 0 - | LLfalse (_,_) -> 100 - | LLand (_,_) -> 80 - | LLor (_,_) -> 70 - | LLforall _ -> -20 - | LLexists (_,_) -> 50 - | LLarrow (_,_,_) -> -10 + LLatom -> 0 + | LLfalse (_,_) -> 100 + | LLand (_,_) -> 80 + | LLor (_,_) -> 70 + | LLforall _ -> -20 + | LLexists (_,_) -> 50 + | LLarrow (_,_,_) -> -10 let left_reversible lpat=(priority lpat)>0 @@ -186,7 +186,7 @@ let lookup item seq= | Some ((m2,t2) as c2)->id=id2 && m2>m && more_general c2 c in History.exists p seq.history -let add_formula side nam t seq gl= +let rec add_formula side nam t seq gl= match build_formula side nam t gl seq.cnt with Left f-> if side then |