diff options
Diffstat (limited to 'contrib/first-order/ground.ml4')
| -rw-r--r-- | contrib/first-order/ground.ml4 | 194 |
1 files changed, 96 insertions, 98 deletions
diff --git a/contrib/first-order/ground.ml4 b/contrib/first-order/ground.ml4 index b8f6849772..4fbc68c0c6 100644 --- a/contrib/first-order/ground.ml4 +++ b/contrib/first-order/ground.ml4 @@ -42,106 +42,104 @@ let _= declare_int_option gdopt let ground_tac solver startseq gl= - let rec toptac seq gl= + let rec toptac ctx seq gl= if Tacinterp.get_debug()=Tactic_debug.DebugOn 0 then Pp.msgnl (Proof_trees.pr_goal (sig_it gl)); - match seq.gl with - Atomic t-> - tclORELSE (axiom_tac t seq) (left_tac seq []) gl - | Complex (pat,t,l)-> - tclORELSE (axiom_tac t seq) - (match pat with - Rand-> - and_tac toptac seq - | Rforall-> - forall_tac toptac seq - | Rarrow-> - arrow_tac toptac seq - | Revaluable egr-> - evaluable_tac egr toptac seq - | _-> - if not (is_empty_left seq) && rev_left seq then - left_tac seq [] - else - right_tac seq []) gl - and right_tac seq ctx gl= - let re_add s=re_add_left_list ctx s in - match seq.gl with - Atomic _ -> left_tac seq ctx gl - | Complex (pat,_,atoms)-> - match pat with - Ror-> - tclORELSE - (or_tac toptac (re_add seq)) - (left_tac seq ctx) gl - | Rexists(i,dom,triv)-> - let cont_tac=left_tac seq ctx in - if seq.depth<=0 || not !qflag then - cont_tac gl - else - (match - Instances.give_right_instances i dom triv atoms seq - with - Some l -> tclORELSE - (exists_tac l toptac (re_add seq)) cont_tac gl - | None -> - tclORELSE cont_tac - (dummy_exists_tac dom toptac (re_add seq)) gl) - | _-> anomaly "unreachable place" - and left_tac seq ctx gl= - if is_empty_left seq then - solver gl - 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 toptac (re_add seq1) gl - | Lor ind-> - left_or_tac ind hd.id toptac (re_add seq1) gl - | Lforall (_,_,_)-> - let (lfp,seq2)=collect_forall seq in - tclORELSE - (if seq.depth<=0 || not !qflag then - tclFAIL 0 "max depth" - else - left_forall_tac lfp toptac (re_add seq)) - (left_tac seq2 (lfp@ctx)) gl - | Lexists ind -> - if !qflag then - left_exists_tac ind hd.id toptac (re_add seq1) gl - else (left_tac seq1 (hd::ctx)) gl - | Levaluable egr-> - left_evaluable_tac egr hd.id toptac (re_add seq1) gl - | LA (typ,lap)-> - tclORELSE - (ll_atom_tac typ hd.id toptac (re_add seq1)) - (match lap with - LLatom-> - right_tac seq1 (hd::ctx) - | LLfalse (ind,largs) | LLand (ind,largs) | LLor(ind,largs) -> - ll_ind_tac ind largs hd.id toptac (re_add seq1) - | LLforall p -> - tclORELSE - (if seq.depth<=0 || not !qflag then - tclFAIL 0 "max depth" - else - ll_forall_tac p hd.id toptac (re_add seq1)) - (left_tac seq1 (hd::ctx)) - | LLexists (ind,l) -> - if !qflag then - ll_ind_tac ind l hd.id toptac (re_add seq1) - else - left_tac seq1 (hd::ctx) - | LLarrow (a,b,c) -> - tclORELSE - (ll_arrow_tac a b c hd.id toptac (re_add seq1)) - (left_tac seq1 (hd::ctx)) - | LLevaluable egr-> - left_evaluable_tac egr hd.id toptac (re_add seq1)) gl in - wrap (List.length (pf_hyps gl)) true toptac (startseq gl) gl + tclORELSE (axiom_tac seq.gl seq) + begin + try + let (hd,seq1)=take_formula seq + and re_add s=re_add_formula_list ctx s in + let continue=toptac [] + and backtrack=toptac (hd::ctx) seq1 in + match hd.pat with + Right rpat-> + begin + match rpat with + Rand-> + and_tac continue seq1 + | Rforall-> + forall_tac continue seq1 + | Rarrow-> + arrow_tac continue seq1 + | Revaluable egr-> + evaluable_tac egr continue seq1 + | Ror-> + tclORELSE + (or_tac continue (re_add seq1)) + backtrack + | Rfalse->backtrack + | Rexists(i,dom,triv)-> + let (lfp,seq2)=collect_quantified seq in + tclORELSE + (if seq.depth<=0 || not !qflag then + tclFAIL 0 "max depth" + else + quantified_tac lfp continue (re_add seq)) + (toptac (lfp@ctx) seq2) + (* need special backtracking *) + end + | Left lpat-> + begin + match lpat with + Lfalse-> + left_false_tac hd.id + | Land ind-> + left_and_tac ind hd.id continue (re_add seq1) + | Lor ind-> + left_or_tac ind hd.id continue (re_add seq1) + | Lforall (_,_,_)-> + let (lfp,seq2)=collect_quantified seq in + tclORELSE + (if seq.depth<=0 || not !qflag then + tclFAIL 0 "max depth" + else + quantified_tac lfp continue (re_add seq)) + (toptac (lfp@ctx) seq2) + (* need special backtracking *) + | Lexists ind -> + if !qflag then + left_exists_tac ind hd.id continue (re_add seq1) + else backtrack + | Levaluable egr-> + left_evaluable_tac egr hd.id continue (re_add seq1) + | 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 -> + tclORELSE + (if seq.depth<=0 || not !qflag then + tclFAIL 0 "max depth" + else + ll_forall_tac p hd.id continue + (re_add seq1)) + 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 + | LLevaluable egr-> + left_evaluable_tac egr hd.id continue + (re_add seq1) + end + end + with Heap.EmptyHeap->solver + end gl in + wrap (List.length (pf_hyps gl)) true (toptac []) (startseq gl) gl let default_solver=(Tacinterp.interp <:tactic<Auto with *>>) |