summaryrefslogtreecommitdiff
path: root/contrib/firstorder/ground.ml
blob: f46618695bcad2f191a9082081f4bd849eae65be (plain)
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
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
(************************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
(*   \VV/  **************************************************************)
(*    //   *      This file is distributed under the terms of the       *)
(*         *       GNU Lesser General Public License Version 2.1        *)
(************************************************************************)

(* $Id: ground.ml 9549 2007-01-28 23:30:12Z corbinea $ *)

open Formula
open Sequent
open Rules
open Instances
open Term
open Tacmach
open Tactics
open Tacticals
open Libnames

(*
let old_search=ref !Auto.searchtable 

(* I use this solution as a means to know whether hints have changed, 
but this prevents the GC from collecting the previous table, 
resulting in some limited space wasting*)

let update_flags ()=
  if not ( !Auto.searchtable == !old_search ) then
    begin
      old_search:=!Auto.searchtable;
      let predref=ref Names.KNpred.empty in
      let f p_a_t = 
	match p_a_t.Auto.code with
	    Auto.Unfold_nth (ConstRef kn)->
	      predref:=Names.KNpred.add kn !predref
	  | _ ->() in
      let g _ l=List.iter f l in
      let h _ hdb=Auto.Hint_db.iter g hdb in
	Util.Stringmap.iter h !Auto.searchtable;
	red_flags:=
	Closure.RedFlags.red_add_transparent 
	  Closure.betaiotazeta (Names.Idpred.full,!predref)
    end
*)

let update_flags ()=
  let predref=ref Names.Cpred.empty in
  let f coe=
    try
      let kn=destConst (Classops.get_coercion_value coe) in
	predref:=Names.Cpred.add kn !predref
    with Invalid_argument "destConst"-> () in
    List.iter f (Classops.coercions ());
    red_flags:=
    Closure.RedFlags.red_add_transparent 
      Closure.betaiotazeta 
      (Names.Idpred.full,Names.Cpred.complement !predref)

let ground_tac solver startseq gl=
  update_flags ();
  let rec toptac skipped seq gl=
    if Tacinterp.get_debug()=Tactic_debug.DebugOn 0
    then Pp.msgnl (Printer.pr_goal (sig_it gl));
    tclORELSE (axiom_tac seq.gl seq)
      begin
	try      
	  let (hd,seq1)=take_formula seq  
	  and re_add s=re_add_formula_list skipped s in
	  let continue=toptac [] 
	  and backtrack gl=toptac (hd::skipped) seq1 gl 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 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 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 gl in
    wrap (List.length (pf_hyps gl)) true (toptac []) (startseq gl) gl