aboutsummaryrefslogtreecommitdiffhomepage
path: root/contrib/interface/pbp.ml
blob: 01747aa58f9d56d2e0521c0f302e9931ef23c785 (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
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
(* A proof by pointing algorithm. *)
open Util;;
open Names;;
open Term;;
open Tactics;;
open Tacticals;;
open Hipattern;;
open Pattern;;
open Matching;;
open Reduction;;
open Rawterm;;
open Environ;;

open Proof_trees;;
open Proof_type;;
open Tacmach;;
open Tacexpr;;
open Typing;;
open Pp;;
open Libnames;;
open Genarg;;
open Topconstr;;
open Termops;;

let zz = Util.dummy_loc;;

let hyp_radix = id_of_string "H";;

let next_global_ident = next_global_ident_away true

(* get_hyp_by_name : goal sigma -> string -> constr,
   looks up for an hypothesis (or a global constant), from its name *)
let get_hyp_by_name g name =
  let evd = project g in
  let env = pf_env g in
  try (let judgment = 
         Pretyping.Default.understand_judgment 
          evd env (RVar(zz, name)) in
       ("hyp",judgment.uj_type))
(* je sais, c'est pas beau, mais je ne sais pas trop me servir de look_up...
   Loïc *)
  with _ -> (let c = Nametab.global (Ident (zz,name)) in
             ("cste",type_of (Global.env()) Evd.empty (constr_of_global c)))
;;

type pbp_atom =
  | PbpTryAssumption of identifier option
  | PbpTryClear of identifier list
  | PbpGeneralize of identifier * identifier list
  | PbpLApply of identifier (* = CutAndApply *)
  | PbpIntros of intro_pattern_expr located list
  | PbpSplit
  (* Existential *)
  | PbpExists of identifier
  (* Or *)
  | PbpLeft
  | PbpRight
  (* Head *)
  | PbpApply of identifier
  | PbpElim of identifier * identifier list;;

(* Invariant: In PbpThens ([a1;...;an],[t1;...;tp]), all tactics
   [a1]..[an-1] are atomic (or try of an atomic) tactic and produce
   exactly one goal, and [an] produces exactly p subgoals

   In [PbpThen [a1;..an]], all tactics are (try of) atomic tactics and
   produces exactly one subgoal, except the last one which may complete the
   goal

   Convention: [PbpThen []] is Idtac and [PbpThen t] is a coercion
   from atomic to composed tactic
*)

type pbp_sequence =
  | PbpThens of pbp_atom list * pbp_sequence list
  | PbpThen of pbp_atom list

(* This flattens sequences of tactics producing just one subgoal *)
let chain_tactics tl1 = function
  | PbpThens (tl2, tl3) -> PbpThens (tl1@tl2, tl3)
  | PbpThen tl2 -> PbpThen (tl1@tl2)

type pbp_rule = (identifier list *
                    identifier list *
                    bool *
                    identifier option *
                    (types, constr) kind_of_term *
                    int list *
                    (identifier list ->
                     identifier list ->
                     bool ->
                       identifier option -> (types, constr) kind_of_term -> int list -> pbp_sequence)) ->
                    pbp_sequence option;;


let make_named_intro id = PbpIntros [zz,IntroIdentifier id];;

let make_clears str_list = PbpThen [PbpTryClear str_list]

let add_clear_names_if_necessary tactic clear_names =
    match clear_names with
      [] -> tactic
    | l -> chain_tactics [PbpTryClear l] tactic;;

let make_final_cmd f optname clear_names constr path =
    add_clear_names_if_necessary (f optname constr path) clear_names;;

let (rem_cast:pbp_rule) = function
    (a,c,cf,o, Cast(f,_,_), p, func) ->
      Some(func a c cf o (kind_of_term f) p)
  | _ -> None;;

let (forall_intro: pbp_rule) = function
  (avoid,
   clear_names,
   clear_flag,
   None,
   Prod(Name x, _, body),
   (2::path),
   f) ->
     let x' = next_global_ident x avoid in
      Some(chain_tactics [make_named_intro x']
	      (f (x'::avoid)
		clear_names clear_flag None (kind_of_term body) path))
| _ -> None;;

let (imply_intro2: pbp_rule) = function
  avoid, clear_names,
  clear_flag, None, Prod(Anonymous, _, body), 2::path, f ->
   let h' = next_global_ident hyp_radix avoid in
     Some(chain_tactics [make_named_intro h']
          (f (h'::avoid) clear_names clear_flag None (kind_of_term body) path))
  | _ -> None;;

      
(*
let (imply_intro1: pbp_rule) = function
  avoid, clear_names,
  clear_flag, None, Prod(Anonymous, prem, body), 1::path, f ->
   let h' = next_global_ident hyp_radix avoid in
   let str_h' = h' in
     Some(chain_tactics [make_named_intro str_h']
            (f (h'::avoid) clear_names clear_flag (Some str_h') 
		(kind_of_term prem) path))
  | _ -> None;;
*)

let make_var id = CRef (Ident(zz, id))

let make_app f l = CApp (zz,(None,f),List.map (fun x -> (x,None)) l)

let make_pbp_pattern x =
  make_app (make_var (id_of_string "PBP_META"))
     [make_var (id_of_string ("Value_for_" ^ (string_of_id x)))]

let rec make_then = function
  | [] -> TacId []
  | [t] -> t
  | t1::t2::l -> make_then (TacThen (t1,[||],t2,[||])::l)

let make_pbp_atomic_tactic = function
  | PbpTryAssumption None -> TacTry (TacAtom (zz, TacAssumption))
  | PbpTryAssumption (Some a) ->
      TacTry (TacAtom (zz, TacExact (make_var a)))
  | PbpExists x -> 
      TacAtom (zz, TacSplit (false,true,ImplicitBindings [make_pbp_pattern x]))
  | PbpGeneralize (h,args) ->
      let l = List.map make_pbp_pattern args in
      TacAtom (zz, TacGeneralize [((true,[]),make_app (make_var h) l),Anonymous])
  | PbpLeft -> TacAtom (zz, TacLeft (false,NoBindings))
  | PbpRight -> TacAtom (zz, TacRight (false,NoBindings))
  | PbpIntros l -> TacAtom (zz, TacIntroPattern l)
  | PbpLApply h -> TacAtom (zz, TacLApply (make_var h))
  | PbpApply h -> TacAtom (zz, TacApply (true,false,[make_var h,NoBindings],None))
  | PbpElim (hyp_name, names) ->
      let bind = List.map (fun s ->(zz,NamedHyp s,make_pbp_pattern s)) names in
      TacAtom
	(zz, TacElim (false,(make_var hyp_name,ExplicitBindings bind),None))
  | PbpTryClear l -> 
      TacTry (TacAtom (zz, TacClear (false,List.map (fun s -> AI (zz,s)) l)))
  | PbpSplit -> TacAtom (zz, TacSplit (false,false,NoBindings));;

let rec make_pbp_tactic = function
  | PbpThen tl -> make_then (List.map make_pbp_atomic_tactic tl)
  | PbpThens (l,tl) ->
      TacThens
        (make_then (List.map make_pbp_atomic_tactic l),
	 List.map make_pbp_tactic tl)

let (forall_elim: pbp_rule) = function
  avoid, clear_names, clear_flag, 
  Some h, Prod(Name x, _, body), 2::path, f ->
  let h' = next_global_ident hyp_radix avoid in
  let clear_names' = if clear_flag then h::clear_names else clear_names in
    Some
     (chain_tactics [PbpGeneralize (h,[x]); make_named_intro h']
        (f (h'::avoid) clear_names' true (Some h') (kind_of_term body) path))
  | _ -> None;;


let (imply_elim1: pbp_rule) = function
  avoid, clear_names, clear_flag,
  Some h, Prod(Anonymous, prem, body), 1::path, f ->
  let clear_names' = if clear_flag then h::clear_names else clear_names in
  let h' = next_global_ident hyp_radix avoid in
  let _str_h' = (string_of_id h') in
  Some(PbpThens
	  ([PbpLApply h],
	   [chain_tactics [make_named_intro h'] (make_clears (h::clear_names));
	    f avoid clear_names' false None (kind_of_term prem) path]))
  | _ -> None;;


let (imply_elim2: pbp_rule) = function
  avoid, clear_names, clear_flag,
  Some h, Prod(Anonymous, prem, body), 2::path, f ->
  let clear_names' = if clear_flag then h::clear_names else clear_names in
  let h' = next_global_ident hyp_radix avoid in
  Some(PbpThens
	 ([PbpLApply h],
          [chain_tactics [make_named_intro h']
              (f (h'::avoid) clear_names' false (Some h') 
		      (kind_of_term body) path);
           make_clears clear_names]))
  | _ -> None;;

let reference dir s = Coqlib.gen_reference "Pbp" ("Init"::dir) s

let constant dir s =  Coqlib.gen_constant "Pbp" ("Init"::dir) s

let andconstr: unit -> constr = Coqlib.build_coq_and;;
let prodconstr () = constant ["Datatypes"] "prod";;
let exconstr = Coqlib.build_coq_ex;;
let sigconstr () = constant ["Specif"] "sig";;
let sigTconstr () = (Coqlib.build_sigma_type()).Coqlib.typ;;
let orconstr = Coqlib.build_coq_or;;
let sumboolconstr = Coqlib.build_coq_sumbool;;
let sumconstr() = constant ["Datatypes"] "sum";;
let notconstr = Coqlib.build_coq_not;;
let notTconstr () = constant ["Logic_Type"] "notT";;

let is_matching_local a b = is_matching (pattern_of_constr a) b;;

let rec (or_and_tree_to_intro_pattern: identifier list -> 
	   constr -> int list -> 
	     intro_pattern_expr * identifier list * identifier *constr
	     * int list * int * int) =
fun avoid c path -> match kind_of_term c, path with
  | (App(oper, [|c1; c2|]), 2::a::path)
    when ((is_matching_local (andconstr()) oper) or
	  (is_matching_local (prodconstr()) oper)) & (a = 1 or a = 2) ->
      let id2 = next_global_ident hyp_radix avoid in
      let cont_expr = if a = 1 then c1 else c2 in
      let cont_patt, avoid_names, id, c, path, rank, total_branches = 
	or_and_tree_to_intro_pattern (id2::avoid) cont_expr path in
      let patt_list = 
	if a = 1 then
	  [zz,cont_patt; zz,IntroIdentifier id2]
	else
	  [zz,IntroIdentifier id2; zz,cont_patt] in
      	(IntroOrAndPattern[patt_list], avoid_names, id, c, path, rank, 
	 total_branches)
  | (App(oper, [|c1; c2|]), 2::3::path)
    when ((is_matching_local (exconstr()) oper) or
	  (is_matching_local (sigconstr()) oper)) ->
      (match (kind_of_term c2) with 
	   Lambda (Name x, _, body) ->
	     let id1 = next_global_ident x avoid in
	     let cont_patt, avoid_names, id, c, path, rank, total_branches =
	       or_and_tree_to_intro_pattern (id1::avoid) body path in
	     (IntroOrAndPattern[[zz,IntroIdentifier id1; zz,cont_patt]],
	      avoid_names, id, c, path, rank, total_branches)
	 | _ -> assert false)
  | (App(oper, [|c1; c2|]), 2::a::path)
      when ((is_matching_local (orconstr ()) oper) or
            (is_matching_local (sumboolconstr ()) oper) or
	    (is_matching_local (sumconstr ()) oper)) & (a = 1 or a = 2) ->
      let id2 = next_global_ident hyp_radix avoid in
      let cont_expr = if a = 1 then c1 else c2 in
      let cont_patt, avoid_names, id, c, path, rank, total_branches =
 	or_and_tree_to_intro_pattern (id2::avoid) cont_expr path in
      let new_rank = if a = 1 then rank else rank+1 in
      let patt_list =
	if a = 1 then
	  [[zz,cont_patt];[zz,IntroIdentifier id2]]
	else
	  [[zz,IntroIdentifier id2];[zz,cont_patt]] in
	(IntroOrAndPattern patt_list, 
	 avoid_names, id, c, path, new_rank, total_branches+1)
  | (_, path) -> let id = next_global_ident hyp_radix avoid in
      (IntroIdentifier id, (id::avoid), id, c, path, 1, 1);;

let auxiliary_goals clear_names clear_flag this_name n_aux others =
  let clear_cmd = 
    make_clears (if clear_flag then (this_name ::clear_names) else clear_names) in
  let rec clear_list = function
      0 -> others
    | n -> clear_cmd::(clear_list (n - 1)) in
  clear_list n_aux;;


let (imply_intro3: pbp_rule) = function
    avoid, clear_names, clear_flag, None, Prod(Anonymous, prem, body),
    1::path, f ->
      let intro_patt, avoid_names, id, c, p, rank, total_branches =
	or_and_tree_to_intro_pattern avoid prem path in
	if total_branches = 1 then
	  Some(chain_tactics [PbpIntros [zz,intro_patt]]
		 (f avoid_names clear_names clear_flag (Some id)
		    (kind_of_term c) path))
	else
	  Some
	    (PbpThens
	       ([PbpIntros [zz,intro_patt]],
	    	auxiliary_goals clear_names clear_flag id
		  (rank - 1)
		  ((f avoid_names clear_names clear_flag (Some id)
		      (kind_of_term c) path)::
		     auxiliary_goals clear_names clear_flag id 
		     (total_branches - rank) [])))
  | _ -> None;;
		 


let (and_intro: pbp_rule) = function
    avoid, clear_names, clear_flag,
    None, App(and_oper, [|c1; c2|]), 2::a::path, f 
      ->
      if ((is_matching_local (andconstr()) and_oper) or
          (is_matching_local (prodconstr ()) and_oper)) & (a = 1 or a = 2) then
      	let cont_term = if a = 1 then c1 else c2 in
      	let cont_cmd = f avoid clear_names false None 
			 (kind_of_term cont_term) path in
      	let clear_cmd = make_clears clear_names in
      	let cmds =
            (if a = 1 
	    then [cont_cmd;clear_cmd] 
	    else [clear_cmd;cont_cmd]) in
      	Some (PbpThens ([PbpSplit],cmds))
      else None
  | _ -> None;;

let exists_from_lambda avoid clear_names clear_flag c2 path f =
  match kind_of_term c2 with
    Lambda(Name x, _, body) -> 
      Some (PbpThens ([PbpExists x],
		      [f avoid clear_names false None (kind_of_term body) path]))
  | _ -> None;;


let (ex_intro: pbp_rule) = function
    avoid, clear_names, clear_flag, None,
    App(oper, [| c1; c2|]), 2::3::path, f
      when (is_matching_local (exconstr ()) oper)
 	or (is_matching_local (sigconstr ()) oper) ->
	  exists_from_lambda avoid clear_names clear_flag c2 path f
  | _ -> None;;

let (exT_intro : pbp_rule) = function
    avoid, clear_names, clear_flag, None,
    App(oper, [| c1; c2|]), 2::2::2::path, f
      when (is_matching_local (sigTconstr ()) oper) ->
	exists_from_lambda avoid clear_names clear_flag c2 path f
  | _ -> None;;

let (or_intro: pbp_rule) = function
    avoid, clear_names, clear_flag, None,
    App(or_oper, [|c1; c2 |]), 2::a::path, f ->
      if ((is_matching_local (orconstr ()) or_oper) or
        (is_matching_local (sumboolconstr ()) or_oper) or 
	(is_matching_local (sumconstr ()) or_oper))
	  & (a = 1 or a = 2) then
	let cont_term = if a = 1 then c1 else c2 in
	let fst_cmd = if a = 1 then PbpLeft else PbpRight in
	let cont_cmd = f avoid clear_names false None 
			 (kind_of_term cont_term) path in
	Some(chain_tactics [fst_cmd] cont_cmd)
      else
	None
  | _ -> None;;
	
let dummy_id = id_of_string "Dummy";;

let (not_intro: pbp_rule) = function
    avoid, clear_names, clear_flag, None,
    App(not_oper, [|c1|]), 2::1::path, f ->
      if(is_matching_local (notconstr ()) not_oper) or 
	(is_matching_local (notTconstr ()) not_oper) then
	let h' = next_global_ident hyp_radix avoid in
	Some(chain_tactics [make_named_intro h']
	       (f (h'::avoid) clear_names false (Some h') 
		  (kind_of_term c1) path))
      else
 	None
  | _ -> None;;




let elim_with_bindings hyp_name names =
  PbpElim (hyp_name, names);;

(* This function is used to follow down a path, while staying on the spine of
   successive products (universal quantifications or implications).
   Arguments are the current observed constr object and the path that remains
   to be followed, and an integer indicating how many products have already been
   crossed.
   Result is:
     - a list of string indicating the names of universally quantified variables.
     - a list of integers indicating the positions of the successive 
       universally quantified variables.
     - an integer indicating the number of non-dependent products.
     - the last constr object encountered during the walk down, and
     - the remaining path.

   For instance the following session should happen:
  let tt = raw_constr_of_com (Evd.mt_evd())(gLOB(initial_sign()))
     (parse_com "(P:nat->Prop)(x:nat)(P x)->(P x)") in
     down_prods (tt, [2;2;2], 0)
  ---> ["P","x"],[0;1], 1, <<(P x)>>, []
*)


let rec down_prods: (types, constr) kind_of_term * (int list) * int -> 
           identifier list * (int list) * int * (types, constr) kind_of_term *
  (int list) = 
   function
     Prod(Name x, _, body), 2::path, k ->
	let res_sl, res_il, res_i, res_cstr, res_p 
	    = down_prods (kind_of_term body, path, k+1) in
	x::res_sl, (k::res_il), res_i, res_cstr, res_p
   | Prod(Anonymous, _, body), 2::path, k ->
        let res_sl, res_il, res_i, res_cstr, res_p 
	    = down_prods (kind_of_term body, path, k+1) in
	res_sl, res_il, res_i+1, res_cstr, res_p
   | cstr, path, _ -> [], [], 0, cstr, path;;

exception Pbp_internal of int list;;

(* This function should be usable to check that a type can be used by the
   Apply command.  Basically, c is supposed to be the head of some
   type, where l gives the ranks of all universally quantified variables.
   It check that these universally quantified variables occur in the head.

   The knowledge I have on constr structures is incomplete.
*)
let (check_apply: (types, constr) kind_of_term -> (int list) -> bool) = 
   function c -> function l ->
   let rec delete n = function
     | [] -> []
     | p::tl -> if n = p then tl else p::(delete n tl) in
   let rec check_rec l = function
   | App(f, array) ->
       Array.fold_left (fun l c -> check_rec l (kind_of_term c))
	 (check_rec l (kind_of_term f)) array
   | Const _ -> l
   | Ind _ -> l
   | Construct _ -> l
   | Var _ -> l
   | Rel p ->
       let result = delete p l in
       if result = [] then
	 raise (Pbp_internal [])
       else
	 result
   | _ -> raise (Pbp_internal l) in
   try 
     (check_rec l c) = []
   with Pbp_internal l -> l = [];;

let (mk_db_indices: int list -> int -> int list) =
  function int_list -> function nprems ->
   let total = (List.length int_list) + nprems  in
   let rec mk_db_aux = function
     [] -> []
   | a::l -> (total - a)::(mk_db_aux l) in
   mk_db_aux int_list;;
     

(* This proof-by-pointing rule is quite complicated, as it attempts to foresee
   usages of head tactics.  A first operation is to follow the path as far
   as possible while staying on the spine of products (function down_prods)
   and then to check whether the next step will be an elim step.  If the 
   answer is true, then the built command takes advantage of the power of
   head tactics.  *)

let (head_tactic_patt: pbp_rule) = function
    avoid, clear_names, clear_flag, Some h, cstr, path, f ->
    (match down_prods (cstr, path, 0) with
    | (str_list, _, nprems, App(oper,[|c1; c2|]), b::a::path)
      when (((is_matching_local (exconstr ()) oper) (* or
	      (is_matching_local (sigconstr ()) oper) *))  && a = 3) ->
		   (match (kind_of_term c2) with
		     Lambda(Name x, _,body) ->
		       Some(PbpThens
		    		 ([elim_with_bindings h str_list],
				   let x' = next_global_ident x avoid in
				   let cont_body =
				     Prod(Name x', c1,
					    mkProd(Anonymous, body, 
						   mkVar(dummy_id))) in
				   let cont_tac 
				       = f avoid (h::clear_names) false None
				       cont_body (2::1::path) in
				   cont_tac::(auxiliary_goals
						       clear_names clear_flag
						       h nprems [])))
		     | _ -> None)
    | (str_list, _, nprems, 
       App(oper,[|c1|]), 2::1::path) 
      	when
 	  (is_matching_local (notconstr ()) oper) or
 	  (is_matching_local (notTconstr ()) oper) ->
	 Some(chain_tactics [elim_with_bindings h str_list]
		 (f avoid clear_names false None (kind_of_term c1) path))
    | (str_list, _, nprems, 
       App(oper, [|c1; c2|]), 2::a::path) 
      when ((is_matching_local (andconstr()) oper) or
	    (is_matching_local (prodconstr()) oper)) & (a = 1 or a = 2) ->
	let h1 = next_global_ident hyp_radix avoid in
	let h2 = next_global_ident hyp_radix (h1::avoid) in
	Some(PbpThens
                  ([elim_with_bindings h str_list],
		    let cont_body = 
		      if a = 1 then c1 else c2 in
		    let cont_tac = 
		      f (h2::h1::avoid) (h::clear_names) 
                        false (Some (if 1 = a then h1 else h2))
                        (kind_of_term cont_body) path in
		      (chain_tactics 
			 [make_named_intro h1; make_named_intro h2]
			 cont_tac)::
	       (auxiliary_goals clear_names clear_flag h nprems [])))
    | (str_list, _, nprems, App(oper,[|c1; c2|]), 2::a::path)
      when ((is_matching_local (sigTconstr()) oper)) & a = 2 ->
		   (match (kind_of_term c2),path with
		     Lambda(Name x, _,body), (2::path) ->
		       Some(PbpThens
		    		 ([elim_with_bindings h str_list],
				   let x' = next_global_ident x avoid in
				   let cont_body =
				     Prod(Name x', c1,
					    mkProd(Anonymous, body, 
						   mkVar(dummy_id))) in
				   let cont_tac 
				       = f avoid (h::clear_names) false None
				       cont_body (2::1::path) in
				   cont_tac::(auxiliary_goals
						       clear_names clear_flag
						       h nprems [])))
		     | _ -> None)
    | (str_list, _, nprems, App(oper,[|c1; c2|]), 2::a::path)
	when ((is_matching_local (orconstr ()) oper) or
              (is_matching_local (sumboolconstr ()) oper) or
	      (is_matching_local (sumconstr ()) oper)) &
                (a = 1 or a = 2) ->
	  Some(PbpThens
		    ([elim_with_bindings h str_list],
		      let cont_body =
			if a = 1 then c1 else c2 in
                      (* h' is the name for the new intro *)
		      let h' = next_global_ident hyp_radix avoid in
		      let cont_tac =
                        chain_tactics 
			  [make_named_intro h']
			  (f 
			     (* h' should not be used again *)
			     (h'::avoid)
			     (* the disjunct itself can be discarded *)
			     (h::clear_names) false (Some h')
                             (kind_of_term cont_body) path) in
		      let snd_tac = 
			chain_tactics
			   [make_named_intro h']
			   (make_clears (h::clear_names)) in
		      let tacs1 = 
			if a = 1 then
			  [cont_tac; snd_tac]
		      	else
			  [snd_tac; cont_tac] in
		      tacs1@(auxiliary_goals (h::clear_names)
				   false dummy_id nprems [])))
    | (str_list, int_list, nprems, c, []) 
        when  (check_apply c (mk_db_indices int_list nprems)) &
              (match c with Prod(_,_,_) -> false
              |  _ -> true) &
              (List.length int_list) + nprems > 0 ->
          Some(add_clear_names_if_necessary (PbpThen [PbpApply h]) clear_names)
    | _ -> None)
  | _ -> None;;
      

let pbp_rules = ref [rem_cast;head_tactic_patt;forall_intro;imply_intro2;
                      forall_elim; imply_intro3; imply_elim1; imply_elim2;
		      and_intro; or_intro; not_intro; ex_intro; exT_intro];;


let try_trace = ref true;;

let traced_try (f1:tactic) g =
    try (try_trace := true; tclPROGRESS f1 g)
    with e when Logic.catchable_exception e ->
      (try_trace := false; tclIDTAC g);;

let traced_try_entry = function
     [Tacexp t] ->
           traced_try (Tacinterp.interp t)
  |  _ -> failwith "traced_try_entry received wrong arguments";;


(* When the recursive descent along the path is over, one includes the
   command requested by the point-and-shoot strategy.  Default is
   Try Assumption--Try Exact.  *)


let default_ast optname constr path = PbpThen [PbpTryAssumption optname]

(* This is the main proof by pointing function. *)
(* avoid: les noms a ne pas utiliser *)
(* final_cmd: la fonction appelee par defaut *)
(* opt_name: eventuellement le nom de l'hypothese sur laquelle on agit *)

let rec pbpt final_cmd avoid clear_names clear_flag opt_name constr path =
  let rec try_all_rules rl =
      match rl with 
         f::tl ->
           (match f (avoid, clear_names, clear_flag,
                     opt_name, constr, path, pbpt final_cmd) with
              Some(ast) -> ast
            | None -> try_all_rules tl)
      |	 [] -> make_final_cmd final_cmd opt_name clear_names constr path
  in try_all_rules (!pbp_rules);;

(* these are the optimisation functions. *)
(* This function takes care of flattening successive then commands. *)


(* Invariant: in [flatten_sequence t], occurrences of [PbpThenCont(l,t)] enjoy
    that t is some [PbpAtom t] *)

(* This optimization function takes care of compacting successive Intro commands
   together. *)

let rec group_intros names = function
    [] -> (match names with
        [] -> []
      | l -> [PbpIntros l])
  | (PbpIntros ids)::others -> group_intros (names@ids) others
  | t1::others ->
      (match names with
	  [] -> t1::(group_intros [] others)
	| l -> (PbpIntros l)::t1::(group_intros [] others))

let rec optim2 = function
  | PbpThens (tl1,tl2) -> PbpThens (group_intros [] tl1, List.map optim2 tl2)
  | PbpThen tl -> PbpThen (group_intros [] tl)


let rec cleanup_clears str_list = function
    [] -> []
  | x::tail ->
      if List.mem x str_list then cleanup_clears str_list tail
      else x::(cleanup_clears str_list tail);;

(* This function takes care of compacting instanciations of universal
   quantifications. *)

let rec optim3_aux str_list = function
    (PbpGeneralize (h,l1))::
    (PbpIntros [zz,IntroIdentifier s])::(PbpGeneralize (h',l2))::others
      when s=h' ->
      optim3_aux (s::str_list) (PbpGeneralize (h,l1@l2)::others)
  | (PbpTryClear names)::other ->
      (match cleanup_clears str_list names with
	  [] -> other
	| l -> (PbpTryClear l)::other)
  | a::l -> a::(optim3_aux str_list l) 
  | [] -> [];;

let rec optim3 str_list = function
    PbpThens (tl1, tl2) ->
      PbpThens (optim3_aux str_list tl1, List.map (optim3 str_list) tl2)
  | PbpThen tl -> PbpThen (optim3_aux str_list tl)

let optim x = make_pbp_tactic (optim3 [] (optim2 x));;

(* TODO
add_tactic "Traced_Try" traced_try_entry;;
*)

let rec tactic_args_to_ints = function
    [] -> []
  | (Integer n)::l -> n::(tactic_args_to_ints l)
  | _ -> failwith "expecting only numbers";;

(*
let pbp_tac display_function = function 
            (Identifier a)::l -> 
                 (function g ->
                    let str = (string_of_id a) in
		    let (ou,tstr) = (get_hyp_by_name g str) in
		    let exp_ast =
		      pbpt default_ast
		        (match ou with
			       "hyp" ->(pf_ids_of_hyps g)
			       |_ -> (a::(pf_ids_of_hyps g)))
                        []
			false
			(Some str)
			(kind_of_term tstr)
                        (tactic_args_to_ints l) in
                    (display_function (optim exp_ast);
                        tclIDTAC g))
          | ((Integer n)::_) as l -> 
                 (function g ->
                    let exp_ast =
                       (pbpt default_ast (pf_ids_of_hyps g) [] false
                          None (kind_of_term (pf_concl g))
			  (tactic_args_to_ints l)) in
                     (display_function (optim exp_ast);
                       tclIDTAC g))
          | [] -> (function g ->
                     (display_function (default_ast None (pf_concl g) []);
                      tclIDTAC g))
          |  _ -> failwith "expecting other arguments";;


*)
let pbp_tac display_function idopt nl =
  match idopt with
    | Some str ->
        (function g ->
	  let (ou,tstr) = (get_hyp_by_name g str) in
	  let exp_ast =
	    pbpt default_ast
	      (match ou with
		  "hyp" ->(pf_ids_of_hyps g)
		|_ -> (str::(pf_ids_of_hyps g)))
              []
	      false
	      (Some str)
	      (kind_of_term tstr)
              nl in
              (display_function (optim exp_ast); tclIDTAC g))
    | None ->
	if nl <> [] then
          (function g ->
            let exp_ast =
              (pbpt default_ast (pf_ids_of_hyps g) [] false
		None (kind_of_term (pf_concl g)) nl) in
            (display_function (optim exp_ast); tclIDTAC g))
	else
          (function g ->
            (display_function
	       (make_pbp_tactic (default_ast None (pf_concl g) []));
            tclIDTAC g));;