aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/dhyp.ml
blob: cd8a59136aa0fb606e281d6e655de0d38bad0714 (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
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
(************************************************************************)
(*  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$ *)

(* Chet's comments about this tactic :
 
 Programmable destruction of hypotheses and conclusions.

   The idea here is that we are going to store patterns.  These
   patterns look like:

   TYP=<pattern>
   SORT=<pattern>

   and from these patterns, we will be able to decide which tactic to
   execute.

   For hypotheses, we have a vector of 4 patterns:

   HYP[TYP] HYP[SORT] CONCL[TYP] CONCL[SORT]

   and for conclusions, we have 2:

   CONCL[TYP] CONCL[SORT]

   If the user doesn't supply some of these, they are just replaced
   with empties.

   The process of matching goes like this:

   We use a discrimination net to look for matches between the pattern
   for HYP[TOP] (CONCL[TOP]) and the type of the chosen hypothesis.
   Then, we use this to look for the right tactic to apply, by
   matching the rest of the slots.  Each match is tried, and if there
   is more than one, this fact is reported, and the one with the
   lowest priority is taken.  The priority is a parameter of the
   tactic input.

   The tactic input is an expression to hand to the
   tactic-interpreter, and its priority.

   For most tactics, the priority should be the number of subgoals
   generated.

   Matching is compatible with second-order matching of sopattern.

   SYNTAX:

   Hint DHyp <hyp-pattern> pri <tac-pattern>.

   and

   Hint DConcl <concl-pattern> pri <tac-pattern>.

   The bindings at the end allow us to transfer information from the
   patterns on terms into the patterns on tactics in a safe way - we
   will perform second-order normalization and conversion to an AST
   before substitution into the tactic-expression.

   WARNING: The binding mechanism is NOT intended to facilitate the
   transfer of large amounts of information from the terms to the
   tactic.  This should be done in a special-purpose tactic.

 *)

(*

Example : The tactic "if there is a hypothesis saying that the
successor of some number is smaller than zero, then invert such
hypothesis" is defined in this way:

Require DHyp.
Hint Destruct Hypothesis less_than_zero (le (S ?) O) 1
  (:tactic:<Inversion $0>).

Then, the tactic is used like this:

Goal (le (S O) O) -> False.
Intro H.
DHyp  H.
Qed.

The name "$0" refers to the matching hypothesis --in this case the
hypothesis H.

Similarly for the conclusion :

Hint Destruct Conclusion equal_zero  (? = ?) 1 (:tactic:<Reflexivity>).

Goal (plus O O)=O.
DConcl.
Qed.

The "Discardable" option clears the hypothesis after using it.

Require DHyp.
Hint Destruct  Discardable Hypothesis less_than_zero (le (S ?) O) 1
  (:tactic:<Inversion $0>).

Goal (n:nat)(le (S n) O) -> False.
Intros n H.
DHyp  H.
Qed.
-- Eduardo (9/3/97 )

*)

open Pp
open Util
open Names
open Term
open Environ
open Reduction
open Proof_type
open Rawterm
open Tacmach
open Refiner
open Tactics
open Clenv
open Tactics
open Tacticals
open Libobject
open Library
open Pattern
open Matching
open Pcoq
open Tacexpr
open Libnames

(* two patterns - one for the type, and one for the type of the type *)
type destructor_pattern = {
  d_typ: constr_pattern; 
  d_sort: constr_pattern }

let subst_destructor_pattern subst { d_typ = t; d_sort = s } =
  { d_typ = subst_pattern subst t; d_sort = subst_pattern subst s }

(* hypothesis patterns might need to do matching on the conclusion, too.
 * conclusion-patterns only need to do matching on the hypothesis *)
type located_destructor_pattern =
   (* discardable, pattern for hyp, pattern for concl *)
   (bool * destructor_pattern * destructor_pattern,
   (* pattern for concl *)
   destructor_pattern) location

let subst_located_destructor_pattern subst = function
  | HypLocation (b,d,d') -> 
      HypLocation
        (b,subst_destructor_pattern subst d, subst_destructor_pattern subst d')
  | ConclLocation d ->
      ConclLocation (subst_destructor_pattern subst d)

type destructor_data = {
  d_pat : located_destructor_pattern;
  d_pri : int;
  d_code : identifier option * glob_tactic_expr (* should be of phylum tactic *)
}

type t = (identifier,destructor_data) Nbtermdn.t
type frozen_t = (identifier,destructor_data) Nbtermdn.frozen_t

let tactab = (Nbtermdn.create () : t)

let lookup pat = Nbtermdn.lookup tactab pat

let init () = Nbtermdn.empty tactab

let freeze () = Nbtermdn.freeze tactab
let unfreeze fs = Nbtermdn.unfreeze fs tactab

let rollback f x =
  let fs = freeze() in 
  try f x with e -> (unfreeze fs; raise e)

let add (na,dd) =
  let pat = match dd.d_pat with
    | HypLocation(_,p,_) -> p.d_typ
    | ConclLocation p -> p.d_typ
  in 
  if Nbtermdn.in_dn tactab na then begin
    msgnl (str "Warning [Overriding Destructor Entry " ++ 
             str (string_of_id na) ++ str"]");
    Nbtermdn.remap tactab na (pat,dd)
  end else 
    Nbtermdn.add tactab (na,(pat,dd))

let _ = 
  Summary.declare_summary "destruct-hyp-concl"
    { Summary.freeze_function = freeze;
      Summary.unfreeze_function = unfreeze;
      Summary.init_function = init;
      Summary.survive_module = false;
      Summary.survive_section = false }

let forward_subst_tactic = 
  ref (fun _ -> failwith "subst_tactic is not installed for DHyp")

let set_extern_subst_tactic f = forward_subst_tactic := f

let cache_dd (_,(_,na,dd)) =
  try 
    add (na,dd)
  with _ -> 
    anomalylabstrm "Dhyp.add"
      (str"The code which adds destructor hints broke;" ++ spc () ++ 
	 str"this is not supposed to happen")

let classify_dd (_,(local,_,_ as o)) =
  if local then Dispose else Substitute o

let export_dd (local,_,_ as x) = if local then None else Some x

let subst_dd (_,subst,(local,na,dd)) =
  (local,na,
  { d_pat = subst_located_destructor_pattern subst dd.d_pat;
    d_pri = dd.d_pri; 
    d_code = !forward_subst_tactic subst dd.d_code })

let (inDD,outDD) =
  declare_object {(default_object "DESTRUCT-HYP-CONCL-DATA") with
                    cache_function = cache_dd;
		    open_function = (fun i o -> if i=1 then cache_dd o);
                    subst_function = subst_dd;
		    classify_function = classify_dd;
                    export_function = export_dd }

let forward_intern_tac = 
  ref (fun _ -> failwith "intern_tac is not installed for DHyp")

let set_extern_intern_tac f = forward_intern_tac := f

let catch_all_sort_pattern = PMeta(Some (id_of_string "SORT"))
let catch_all_type_pattern = PMeta(Some (id_of_string "TYPE"))
    
let add_destructor_hint local na loc pat pri code =
  let code = !forward_intern_tac code in
  let code =
    begin match loc, code with
      | HypLocation _, TacFun ([id],body) -> (id,body)
      | ConclLocation _, _ -> (None, code)
      | _ ->
	  errorlabstrm "add_destructor_hint"
          (str "The tactic should be a function of the hypothesis name") end
  in
  let (_,pat) = Constrintern.interp_constrpattern Evd.empty (Global.env()) pat
  in
  let pat = match loc with
    | HypLocation b ->
	HypLocation
	  (b,{d_typ=pat;d_sort=catch_all_sort_pattern},
	     {d_typ=catch_all_type_pattern;d_sort=catch_all_sort_pattern})
    | ConclLocation () ->
	ConclLocation({d_typ=pat;d_sort=catch_all_sort_pattern}) in
  Lib.add_anonymous_leaf
    (inDD (local,na,{ d_pat = pat; d_pri=pri; d_code=code }))

let match_dpat dp cls gls =
  match (cls,dp) with
    | ({onhyps=lo;onconcl=false},HypLocation(_,hypd,concld)) ->
        let hl = match lo with
            Some l -> l
          | None -> List.map (fun id -> (id,[],InHyp)) (pf_ids_of_hyps gls) in
        if not
          (List.for_all
            (fun (id,_,hl) ->
              let cltyp = pf_get_hyp_typ gls id in
              let cl = pf_concl gls in
              (hl=InHyp) &
              (is_matching hypd.d_typ cltyp) &
              (is_matching hypd.d_sort (pf_type_of gls cltyp)) &
              (is_matching concld.d_typ cl) &
              (is_matching concld.d_sort (pf_type_of gls cl)))
            hl)
        then error "No match"
    | ({onhyps=Some[];onconcl=true},ConclLocation concld) ->
        let cl = pf_concl gls in
        if not
          ((is_matching concld.d_typ cl) &
           (is_matching concld.d_sort (pf_type_of gls cl)))
        then error "No match"
    | _ -> error "ApplyDestructor"

let forward_interp_tactic = 
  ref (fun _ -> failwith "interp_tactic is not installed for DHyp")

let set_extern_interp f = forward_interp_tactic := f

let applyDestructor cls discard dd gls =
  match_dpat dd.d_pat cls gls;
  let cll = simple_clause_list_of cls gls in
  let tacl =
    List.map (fun cl ->
      match cl, dd.d_code with
        | Some (id,_,_), (Some x, tac) -> 
	    let arg =
              ConstrMayEval(ConstrTerm (RRef(dummy_loc,VarRef id),None)) in
            TacLetIn ([(dummy_loc, x), None, arg], tac)
        | None, (None, tac) -> tac
        | _, (Some _,_) -> error "Destructor expects an hypothesis"
        | _, (None,_) -> error "Destructor is for conclusion")
      cll in
  let discard_0 =
    List.map (fun cl ->
      match (cl,dd.d_pat) with
        | (Some (id,_,_),HypLocation(discardable,_,_)) ->
            if discard & discardable then thin [id] else tclIDTAC
        | (None,ConclLocation _) -> tclIDTAC
        | _ -> error "ApplyDestructor" ) cll in
  tclTHEN (tclMAP !forward_interp_tactic tacl) (tclTHENLIST discard_0) gls


(* [DHyp id gls]

   will take an identifier, get its type, look it up in the
   discrimination net, get the destructors stored there, and then try
   them in order of priority. *)

let destructHyp discard id gls =
  let hyptyp = pf_get_hyp_typ gls id in
  let ddl = List.map snd (lookup hyptyp) in
  let sorted_ddl = Sort.list (fun dd1 dd2 -> dd1.d_pri > dd2.d_pri) ddl in
  tclFIRST (List.map (applyDestructor (onHyp id) discard) sorted_ddl) gls

let cDHyp id gls = destructHyp true id gls
let dHyp id gls = destructHyp false id gls

let h_destructHyp b id =
  abstract_tactic (TacDestructHyp (b,(dummy_loc,id))) (destructHyp b id)

(* [DConcl gls]

   will take a goal, get its concl, look it up in the
   discrimination net, get the destructors stored there, and then try
   them in order of priority. *)

let dConcl gls =
  let ddl = List.map snd (lookup (pf_concl gls)) in
  let sorted_ddl = Sort.list (fun dd1 dd2 -> dd1.d_pri > dd2.d_pri) ddl in
  tclFIRST (List.map (applyDestructor onConcl false) sorted_ddl) gls

let h_destructConcl = abstract_tactic TacDestructConcl dConcl

let to2Lists (table : t) = Nbtermdn.to2lists table

let rec search n =
  if n=0 then error "Search has reached zero.";
  tclFIRST
    [intros;
     assumption;
     (tclTHEN  
        (Tacticals.tryAllClauses 
           (function 
              | Some (id,_,_) -> (dHyp id)
              | None    ->  dConcl ))
        (search (n-1)))]
    
let auto_tdb n = tclTRY (tclCOMPLETE (search n))
   
let search_depth_tdb = ref(5)

let depth_tdb = function
  | None -> !search_depth_tdb
  | Some n -> n

let h_auto_tdb n = abstract_tactic (TacAutoTDB n) (auto_tdb (depth_tdb n))