1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132
(************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) open Ltac_plugin open Formula open Sequent open Rules open Instances open Constr open Tacmach.New open Tacticals.New let update_flags ()= let predref=ref Names.Cpred.empty in let f coe= try let kn= fst (destConst (Classops.get_coercion_value coe)) in predref:=Names.Cpred.add kn !predref with DestKO -> () in List.iter f (Classops.coercions ()); red_flags:= CClosure.RedFlags.red_add_transparent CClosure.betaiotazeta (Names.Id.Pred.full,Names.Cpred.complement !predref) let ground_tac solver startseq = Proofview.Goal.enter begin fun gl -> update_flags (); let rec toptac skipped seq = Proofview.Goal.enter begin fun gl -> let () = if Tacinterp.get_debug()=Tactic_debug.DebugOn 0 then let gl = { Evd.it = Proofview.Goal.goal (Proofview.Goal.assume gl); sigma = project gl } in Feedback.msg_debug (Printer.pr_goal gl) in tclORELSE (axiom_tac seq.gl seq) begin try let (hd,seq1)=take_formula (project gl) seq and re_add s=re_add_formula_list (project gl) skipped s in let continue=toptac [] and backtrack =toptac (hd::skipped) seq1 in match hd.pat with Right rpat-> begin match rpat with Rand-> and_tac backtrack continue (re_add seq1) | Rforall-> let backtrack1= if !qflag then tclFAIL 0 (Pp.str "reversible in 1st order mode") else backtrack in forall_tac backtrack1 continue (re_add seq1) | Rarrow-> arrow_tac backtrack continue (re_add seq1) | Ror-> or_tac backtrack continue (re_add seq1) | Rfalse->backtrack | Rexists(i,dom,triv)-> let (lfp,seq2)=collect_quantified (project gl) seq in let backtrack2=toptac (lfp@skipped) seq2 in if !qflag && seq.depth>0 then quantified_tac lfp backtrack2 continue (re_add seq) else backtrack2 (* need special backtracking *) end | Left lpat-> begin match lpat with Lfalse-> left_false_tac hd.id | Land ind-> left_and_tac ind backtrack hd.id continue (re_add seq1) | Lor ind-> left_or_tac ind backtrack hd.id continue (re_add seq1) | Lforall (_,_,_)-> let (lfp,seq2)=collect_quantified (project gl) seq in let backtrack2=toptac (lfp@skipped) seq2 in if !qflag && seq.depth>0 then quantified_tac lfp backtrack2 continue (re_add seq) else backtrack2 (* need special backtracking *) | Lexists ind -> if !qflag then left_exists_tac ind backtrack hd.id continue (re_add seq1) else backtrack | LA (typ,lap)-> 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 | 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 end in let n = List.length (Proofview.Goal.hyps gl) in startseq (fun seq -> wrap n true (toptac []) seq) end