← Back to branch summary

~ubuntu-branches/ubuntu/wily/coq-doc/wily

« back to all changes in this revision

Viewing changes to contrib/interface/blast.ml

  • Committer: Bazaar Package Importer
  • Author(s): Stéphane Glondu, Stéphane Glondu, Samuel Mimram
  • Date: 2010-01-07 22:50:39 UTC
  • mfrom: (1.2.2 upstream)
  • Revision ID: james.westby@ubuntu.com-20100107225039-n3cq82589u0qt0s2
Tags: 8.2pl1-1
http://bugs.debian.org/563669
http://bugs.debian.org/543545
[ Stéphane Glondu ]
* New upstream release (Closes: #563669)
  - remove patches
* Packaging overhaul:
  - use git, advertise it in Vcs-* fields of debian/control
  - use debhelper 7 and dh with override
  - use source format 3.0 (quilt)
* debian/control:
  - set Maintainer to d-o-m, set Uploaders to Sam and myself
  - add Homepage field
  - bump Standards-Version to 3.8.3
* Register PDF documentation into doc-base
* Add debian/watch
* Update debian/copyright

[ Samuel Mimram ]
* Change coq-doc's description to mention that it provides documentation in
  pdf format, not postscript, closes: #543545.

Show diffs side-by-side

added added

removed removed

Lines of Context:
contrib/interface/blast.ml
 
1
(* Une tactique qui tente de d�montrer toute seule le but courant,
 
2
   interruptible par pcoq (si dans le fichier C:\WINDOWS\free il y a un A)
 
3
*)
 
4
open Termops;;
 
5
open Nameops;;
 
6
open Auto;;
 
7
open Clenv;;
 
8
open Command;;
 
9
open Declarations;;
 
10
open Declare;;
 
11
open Eauto;;
 
12
open Environ;;
 
13
open Equality;;
 
14
open Evd;;
 
15
open Hipattern;;
 
16
open Inductive;;
 
17
open Names;;
 
18
open Pattern;;
 
19
open Pbp;;
 
20
open Pfedit;;
 
21
open Pp;;
 
22
open Printer
 
23
open Proof_trees;;
 
24
open Proof_type;;
 
25
open Rawterm;;
 
26
open Reduction;;
 
27
open Refiner;;
 
28
open Sign;;
 
29
open String;;
 
30
open Tacmach;;
 
31
open Tacred;;
 
32
open Tacticals;;
 
33
open Tactics;;
 
34
open Term;;
 
35
open Typing;;
 
36
open Util;;
 
37
open Vernacentries;;
 
38
open Vernacinterp;;
 
39
 
 
40
 
 
41
let parse_com   = Pcoq.parse_string Pcoq.Constr.constr;;
 
42
let parse_tac  t =
 
43
    try (Pcoq.parse_string Pcoq.Tactic.tactic t)
 
44
    with _ -> (msgnl (hov 0 (str"pas pars�: " ++ str t));
 
45
               failwith "tactic")
 
46
;;
 
47
 
 
48
let is_free () =
 
49
   let st =open_in_bin ((Sys.getenv "HOME")^"/.free") in
 
50
   let c=input_char st in
 
51
   close_in st;
 
52
   c = 'A'
 
53
;;
 
54
 
 
55
(* marche pas *)
 
56
(*
 
57
let is_free () =
 
58
   msgnl (hov 0 [< 'str"Isfree========= "; 'fNL >]);
 
59
   let s = Stream.of_channel stdin in
 
60
   msgnl (hov 0 [< 'str"Isfree s "; 'fNL >]);
 
61
   try (Stream.empty s;
 
62
        msgnl (hov 0 [< 'str"Isfree empty "; 'fNL >]);
 
63
        true)
 
64
   with _ -> (msgnl (hov 0 [< 'str"Isfree not empty "; 'fNL >]);
 
65
              false)
 
66
;;
 
67
*)
 
68
let free_try tac g =
 
69
    if is_free()
 
70
    then (tac g)
 
71
    else (failwith "not free")
 
72
;;
 
73
let adrel (x,t) e =
 
74
    match x with 
 
75
      Name(xid) -> Environ.push_rel (x,None,t) e
 
76
    | Anonymous -> Environ.push_rel (x,None,t) e
 
77
(* les constantes ayant une d�finition apparaissant dans x *)
 
78
let rec def_const_in_term_rec vl x = 
 
79
     match (kind_of_term x) with
 
80
     Prod(n,t,c)->
 
81
        let vl = (adrel (n,t) vl) in def_const_in_term_rec vl c
 
82
   | Lambda(n,t,c) ->
 
83
        let vl = (adrel (n,t) vl) in def_const_in_term_rec vl c
 
84
   | App(f,args) -> def_const_in_term_rec vl f
 
85
   | Sort(Prop(Null)) -> Prop(Null)
 
86
   | Sort(c) -> c
 
87
   | Ind(ind) ->
 
88
          let (mib, mip) = Global.lookup_inductive ind in
 
89
          new_sort_in_family (inductive_sort_family mip)
 
90
   | Construct(c) ->
 
91
          def_const_in_term_rec vl (mkInd (inductive_of_constructor c))
 
92
   | Case(_,x,t,a) 
 
93
        -> def_const_in_term_rec vl x
 
94
   | Cast(x,_,t)-> def_const_in_term_rec vl t
 
95
   | Const(c)  -> def_const_in_term_rec vl (Typeops.type_of_constant vl c)
 
96
   | _ -> def_const_in_term_rec vl (type_of vl Evd.empty x)
 
97
;;
 
98
let def_const_in_term_ x =
 
99
    def_const_in_term_rec  (Global.env()) (strip_outer_cast x)
 
100
;;
 
101
(*************************************************************************
 
102
 recopi�s de refiner.ml, car print_subscript pas export�e dans refiner.mli 
 
103
 modif de print_info_script avec pr_bar
 
104
*)
 
105
 
 
106
let pr_bar () = str "|"
 
107
 
 
108
let rec print_info_script sigma osign pf =
 
109
  let {evar_hyps=sign; evar_concl=cl} = pf.goal in
 
110
  match pf.ref with
 
111
    | None -> (mt ())
 
112
    | Some(r,spfl) ->
 
113
        Tactic_printer.pr_rule r ++
 
114
           match spfl with
 
115
             | [] ->
 
116
                   (str " " ++ fnl())
 
117
             | [pf1] ->
 
118
                 if pf1.ref = None then 
 
119
                   (str " " ++ fnl())
 
120
                 else 
 
121
                   (str";" ++ brk(1,3) ++
 
122
                      print_info_script sigma sign pf1)
 
123
             | _ -> ( str";[" ++ fnl() ++
 
124
                       prlist_with_sep pr_bar
 
125
                         (print_info_script sigma sign) spfl ++
 
126
                       str"]")
 
127
 
 
128
let format_print_info_script sigma osign pf = 
 
129
  hov 0 (print_info_script sigma osign pf)
 
130
    
 
131
let print_subscript sigma sign pf = 
 
132
 (* if is_tactic_proof pf then 
 
133
    format_print_info_script sigma sign (subproof_of_proof pf)
 
134
  else *)
 
135
    format_print_info_script sigma sign pf
 
136
(****************)
 
137
 
 
138
let pp_string x =
 
139
   msgnl_with Format.str_formatter x;
 
140
   Format.flush_str_formatter ()
 
141
;;
 
142
 
 
143
(***********************************************************************
 
144
   copi� de tactics/eauto.ml
 
145
*)
 
146
 
 
147
(***************************************************************************)
 
148
(* A tactic similar to Auto, but using EApply, Assumption and e_give_exact *)
 
149
(***************************************************************************)
 
150
 
 
151
let priority l = List.map snd (List.filter (fun (pr,_) -> pr = 0) l)
 
152
 
 
153
let unify_e_resolve  (c,clenv) gls = 
 
154
  let clenv' = connect_clenv gls clenv in
 
155
  let _ = clenv_unique_resolver false clenv' gls in
 
156
    Hiddentac.h_simplest_eapply c gls
 
157
 
 
158
let rec e_trivial_fail_db db_list local_db goal =
 
159
  let tacl = 
 
160
    registered_e_assumption ::
 
161
    (tclTHEN Tactics.intro 
 
162
       (function g'->
 
163
          let d = pf_last_hyp g' in
 
164
          let hintl = make_resolve_hyp (pf_env g') (project g') d in
 
165
          (e_trivial_fail_db db_list
 
166
             (Hint_db.add_list hintl local_db) g'))) ::
 
167
    (List.map fst (e_trivial_resolve db_list local_db (pf_concl goal)) )
 
168
  in 
 
169
  tclFIRST (List.map tclCOMPLETE tacl) goal 
 
170
 
 
171
and e_my_find_search db_list local_db hdc concl = 
 
172
  let hdc = head_of_constr_reference hdc in
 
173
  let hintl =
 
174
    if occur_existential concl then 
 
175
      list_map_append (fun db -> 
 
176
        let flags = {Auto.auto_unif_flags with Unification.modulo_delta = Hint_db.transparent_state db} in
 
177
          List.map (fun x -> flags, x) (Hint_db.map_all hdc db)) (local_db::db_list)
 
178
    else 
 
179
      list_map_append (fun db -> 
 
180
        let flags = {Auto.auto_unif_flags with Unification.modulo_delta = Hint_db.transparent_state db} in
 
181
          List.map (fun x -> flags, x) (Hint_db.map_auto (hdc,concl) db)) (local_db::db_list)
 
182
  in 
 
183
  let tac_of_hint = 
 
184
    fun (st, ({pri=b; pat = p; code=t} as _patac)) -> 
 
185
      (b, 
 
186
       let tac =
 
187
         match t with
 
188
           | Res_pf (term,cl) -> unify_resolve st (term,cl)
 
189
           | ERes_pf (term,cl) -> unify_e_resolve (term,cl)
 
190
           | Give_exact (c) -> e_give_exact_constr c
 
191
           | Res_pf_THEN_trivial_fail (term,cl) ->
 
192
               tclTHEN (unify_e_resolve (term,cl)) 
 
193
                 (e_trivial_fail_db db_list local_db)
 
194
           | Unfold_nth c -> unfold_in_concl [all_occurrences,c]
 
195
           | Extern tacast -> Auto.conclPattern concl p tacast
 
196
       in 
 
197
       (free_try tac,pr_autotactic t))
 
198
       (*i
 
199
         fun gls -> pPNL (pr_autotactic t); Format.print_flush (); 
 
200
                     try tac gls
 
201
                     with e when Logic.catchable_exception(e) -> 
 
202
                            (Format.print_string "Fail\n"; 
 
203
                             Format.print_flush (); 
 
204
                             raise e)
 
205
       i*)
 
206
  in 
 
207
  List.map tac_of_hint hintl
 
208
    
 
209
and e_trivial_resolve db_list local_db gl = 
 
210
  try 
 
211
    priority 
 
212
      (e_my_find_search db_list local_db 
 
213
         (fst (head_constr_bound gl)) gl)
 
214
  with Bound | Not_found -> []
 
215
 
 
216
let e_possible_resolve db_list local_db gl =
 
217
  try List.map snd (e_my_find_search db_list local_db 
 
218
                      (fst (head_constr_bound gl)) gl)
 
219
  with Bound | Not_found -> []
 
220
 
 
221
let assumption_tac_list id = apply_tac_list (e_give_exact_constr (mkVar id))
 
222
 
 
223
let find_first_goal gls = 
 
224
  try first_goal gls with UserError _ -> assert false
 
225
 
 
226
(*s The following module [SearchProblem] is used to instantiate the generic
 
227
    exploration functor [Explore.Make]. *)
 
228
      
 
229
module MySearchProblem = struct
 
230
 
 
231
  type state = { 
 
232
    depth : int; (*r depth of search before failing *)
 
233
    tacres : goal list sigma * validation;
 
234
    last_tactic : std_ppcmds;
 
235
    dblist : Auto.hint_db list;
 
236
    localdb :  Auto.hint_db list }
 
237
                 
 
238
  let success s = (sig_it (fst s.tacres)) = []
 
239
 
 
240
  let rec filter_tactics (glls,v) = function
 
241
    | [] -> []
 
242
    | (tac,pptac) :: tacl -> 
 
243
        try 
 
244
          let (lgls,ptl) = apply_tac_list tac glls in 
 
245
          let v' p = v (ptl p) in
 
246
          ((lgls,v'),pptac) :: filter_tactics (glls,v) tacl
 
247
        with e when Logic.catchable_exception e ->
 
248
          filter_tactics (glls,v) tacl
 
249
 
 
250
  (* Ordering of states is lexicographic on depth (greatest first) then
 
251
     number of remaining goals. *)
 
252
  let compare s s' =
 
253
    let d = s'.depth - s.depth in
 
254
    let nbgoals s = List.length (sig_it (fst s.tacres)) in
 
255
    if d <> 0 then d else nbgoals s - nbgoals s'
 
256
 
 
257
  let branching s = 
 
258
    if s.depth = 0 then 
 
259
      []
 
260
    else      
 
261
      let lg = fst s.tacres in
 
262
      let nbgl = List.length (sig_it lg) in
 
263
      assert (nbgl > 0);
 
264
      let g = find_first_goal lg in
 
265
      let assumption_tacs = 
 
266
        let l = 
 
267
          filter_tactics s.tacres
 
268
            (List.map 
 
269
               (fun id -> (e_give_exact_constr (mkVar id),
 
270
                           (str "Exact" ++ spc()++ pr_id id)))
 
271
               (pf_ids_of_hyps g))
 
272
        in
 
273
        List.map (fun (res,pp) -> { depth = s.depth; tacres = res;
 
274
                                    last_tactic = pp; dblist = s.dblist;
 
275
                                    localdb = List.tl s.localdb }) l
 
276
      in
 
277
      let intro_tac = 
 
278
        List.map 
 
279
          (fun ((lgls,_) as res,pp) -> 
 
280
             let g' = first_goal lgls in 
 
281
             let hintl = 
 
282
               make_resolve_hyp (pf_env g') (project g') (pf_last_hyp g')
 
283
             in
 
284
             let ldb = Hint_db.add_list hintl (List.hd s.localdb) in
 
285
             { depth = s.depth; tacres = res; 
 
286
               last_tactic = pp; dblist = s.dblist;
 
287
               localdb = ldb :: List.tl s.localdb })
 
288
          (filter_tactics s.tacres [Tactics.intro,(str "Intro" )])
 
289
      in
 
290
      let rec_tacs = 
 
291
        let l = 
 
292
          filter_tactics s.tacres
 
293
            (e_possible_resolve s.dblist (List.hd s.localdb) (pf_concl g))
 
294
        in
 
295
        List.map 
 
296
          (fun ((lgls,_) as res, pp) -> 
 
297
             let nbgl' = List.length (sig_it lgls) in
 
298
             if nbgl' < nbgl then
 
299
               { depth = s.depth; tacres = res; last_tactic = pp;
 
300
                 dblist = s.dblist; localdb = List.tl s.localdb }
 
301
             else 
 
302
               { depth = pred s.depth; tacres = res; 
 
303
                 dblist = s.dblist; last_tactic = pp;
 
304
                 localdb = 
 
305
                   list_addn (nbgl'-nbgl) (List.hd s.localdb) s.localdb })
 
306
          l
 
307
      in
 
308
      List.sort compare (assumption_tacs @ intro_tac @ rec_tacs)
 
309
 
 
310
  let pp s = 
 
311
    msg (hov 0 (str " depth="++ int s.depth ++ spc() ++
 
312
                  s.last_tactic ++ str "\n"))
 
313
 
 
314
end
 
315
 
 
316
module MySearch = Explore.Make(MySearchProblem)
 
317
 
 
318
let make_initial_state n gl dblist localdb =
 
319
  { MySearchProblem.depth = n;
 
320
    MySearchProblem.tacres = tclIDTAC gl;
 
321
    MySearchProblem.last_tactic = (mt ());
 
322
    MySearchProblem.dblist = dblist;
 
323
    MySearchProblem.localdb = [localdb] }
 
324
 
 
325
let e_depth_search debug p db_list local_db gl =
 
326
  try
 
327
    let tac = if debug then MySearch.debug_depth_first else MySearch.depth_first in
 
328
    let s = tac (make_initial_state p gl db_list local_db) in
 
329
    s.MySearchProblem.tacres
 
330
  with Not_found -> error "EAuto: depth first search failed"
 
331
 
 
332
let e_breadth_search debug n db_list local_db gl =
 
333
  try
 
334
    let tac = 
 
335
      if debug then MySearch.debug_breadth_first else MySearch.breadth_first 
 
336
    in
 
337
    let s = tac (make_initial_state n gl db_list local_db) in
 
338
    s.MySearchProblem.tacres
 
339
  with Not_found -> error "EAuto: breadth first search failed"
 
340
 
 
341
let e_search_auto debug (n,p) db_list gl = 
 
342
  let local_db = make_local_hint_db true [] gl in 
 
343
  if n = 0 then 
 
344
    e_depth_search debug p db_list local_db gl
 
345
  else 
 
346
    e_breadth_search debug n db_list local_db gl
 
347
 
 
348
let eauto debug np dbnames = 
 
349
  let db_list =
 
350
    List.map
 
351
      (fun x -> 
 
352
         try searchtable_map x
 
353
         with Not_found -> error ("EAuto: "^x^": No such Hint database"))
 
354
      ("core"::dbnames) 
 
355
  in
 
356
  tclTRY (e_search_auto debug np db_list)
 
357
 
 
358
let full_eauto debug n gl = 
 
359
  let dbnames = current_db_names () in
 
360
  let dbnames =  list_subtract dbnames ["v62"] in
 
361
  let db_list = List.map searchtable_map dbnames in
 
362
  let _local_db = make_local_hint_db true [] gl in
 
363
  tclTRY (e_search_auto debug n db_list) gl
 
364
 
 
365
let my_full_eauto n gl = full_eauto false (n,0) gl
 
366
 
 
367
(**********************************************************************
 
368
   copi� de tactics/auto.ml on a juste modifi� search_gen
 
369
*)
 
370
 
 
371
(* local_db is a Hint database containing the hypotheses of current goal *)
 
372
(* Papageno : cette fonction a �t� pas mal simplifi�e depuis que la base
 
373
  de Hint imp�rative a �t� remplac�e par plusieurs bases fonctionnelles *)
 
374
 
 
375
let rec trivial_fail_db db_list local_db gl =
 
376
  let intro_tac = 
 
377
    tclTHEN intro 
 
378
      (fun g'->
 
379
         let hintl = make_resolve_hyp (pf_env g') (project g') (pf_last_hyp g')
 
380
         in trivial_fail_db db_list (Hint_db.add_list hintl local_db) g')
 
381
  in
 
382
  tclFIRST 
 
383
    (assumption::intro_tac::
 
384
     (List.map tclCOMPLETE 
 
385
        (trivial_resolve db_list local_db (pf_concl gl)))) gl
 
386
 
 
387
and my_find_search db_list local_db hdc concl =
 
388
  let tacl = 
 
389
    if occur_existential concl then 
 
390
      list_map_append (fun db -> 
 
391
        let flags = {Auto.auto_unif_flags with Unification.modulo_delta = Hint_db.transparent_state db} in
 
392
          List.map (fun x -> flags, x) (Hint_db.map_all hdc db)) (local_db::db_list)
 
393
    else 
 
394
      list_map_append (fun db -> 
 
395
        let flags = {Auto.auto_unif_flags with Unification.modulo_delta = Hint_db.transparent_state db} in
 
396
          List.map (fun x -> flags, x) (Hint_db.map_auto (hdc,concl) db)) (local_db::db_list)
 
397
  in
 
398
  List.map 
 
399
    (fun (st, {pri=b; pat=p; code=t} as _patac) -> 
 
400
       (b,
 
401
        match t with
 
402
          | Res_pf (term,cl)  -> unify_resolve st (term,cl)
 
403
          | ERes_pf (_,c) -> (fun gl -> error "eres_pf")
 
404
          | Give_exact c  -> exact_check c
 
405
          | Res_pf_THEN_trivial_fail (term,cl) -> 
 
406
              tclTHEN 
 
407
                (unify_resolve st (term,cl)) 
 
408
                (trivial_fail_db db_list local_db)
 
409
          | Unfold_nth c -> unfold_in_concl [all_occurrences,c]
 
410
          | Extern tacast -> conclPattern concl p tacast))
 
411
    tacl
 
412
 
 
413
and trivial_resolve db_list local_db cl = 
 
414
  try 
 
415
    let hdconstr = fst (head_constr_bound cl) in
 
416
    priority 
 
417
      (my_find_search db_list local_db (head_of_constr_reference hdconstr) cl)
 
418
  with Bound | Not_found -> 
 
419
    []
 
420
 
 
421
(**************************************************************************)
 
422
(*                       The classical Auto tactic                        *)
 
423
(**************************************************************************)
 
424
 
 
425
let possible_resolve db_list local_db cl =
 
426
  try 
 
427
    let hdconstr = fst (head_constr_bound cl) in
 
428
    List.map snd 
 
429
      (my_find_search db_list local_db (head_of_constr_reference hdconstr) cl)
 
430
  with Bound | Not_found -> 
 
431
    []
 
432
 
 
433
let decomp_unary_term c gls = 
 
434
  let typc = pf_type_of gls c in 
 
435
  let t = head_constr typc in 
 
436
  if Hipattern.is_conjunction (applist t) then 
 
437
    simplest_case c gls 
 
438
  else 
 
439
    errorlabstrm "Auto.decomp_unary_term" (str "not a unary type")
 
440
 
 
441
let decomp_empty_term c gls = 
 
442
  let typc = pf_type_of gls c in 
 
443
  let (hd,_) = decompose_app typc in 
 
444
  if Hipattern.is_empty_type hd then 
 
445
    simplest_case c gls 
 
446
  else 
 
447
    errorlabstrm "Auto.decomp_empty_term" (str "not an empty type")
 
448
 
 
449
 
 
450
(* decomp is an natural number giving an indication on decomposition 
 
451
   of conjunction in hypotheses, 0 corresponds to no decomposition *)
 
452
(* n is the max depth of search *)
 
453
(* local_db contains the local Hypotheses *)
 
454
 
 
455
let rec search_gen decomp n db_list local_db extra_sign goal =
 
456
  if n=0 then error "BOUND 2";
 
457
  let decomp_tacs = match decomp with 
 
458
    | 0 -> [] 
 
459
    | p -> 
 
460
        (tclTRY_sign decomp_empty_term extra_sign)
 
461
        ::
 
462
        (List.map 
 
463
           (fun id -> tclTHEN (decomp_unary_term (mkVar id)) 
 
464
                (tclTHEN 
 
465
                   (clear [id])
 
466
                   (free_try (search_gen decomp p db_list local_db []))))
 
467
           (pf_ids_of_hyps goal)) 
 
468
  in
 
469
  let intro_tac = 
 
470
    tclTHEN intro 
 
471
      (fun g' -> 
 
472
         let (hid,_,htyp as d) = pf_last_hyp g' in
 
473
         let hintl = 
 
474
           try 
 
475
             [make_apply_entry (pf_env g') (project g')
 
476
                (true,true,false) 
 
477
                None
 
478
                (mkVar hid,htyp)]
 
479
           with Failure _ -> [] 
 
480
         in
 
481
         (free_try
 
482
          (search_gen decomp n db_list (Hint_db.add_list hintl local_db) [d])
 
483
          g'))
 
484
  in
 
485
  let rec_tacs = 
 
486
    List.map 
 
487
      (fun ntac -> 
 
488
         tclTHEN ntac
 
489
           (free_try
 
490
            (search_gen decomp (n-1) db_list local_db empty_named_context)))
 
491
      (possible_resolve db_list local_db (pf_concl goal))
 
492
  in 
 
493
  tclFIRST (assumption::(decomp_tacs@(intro_tac::rec_tacs))) goal
 
494
 
 
495
 
 
496
let search = search_gen 0
 
497
 
 
498
let default_search_depth = ref 5
 
499
                             
 
500
let full_auto n gl = 
 
501
  let dbnames = current_db_names () in
 
502
  let dbnames = list_subtract dbnames ["v62"] in
 
503
  let db_list = List.map searchtable_map dbnames in
 
504
  let hyps = pf_hyps gl in
 
505
  tclTRY (search n db_list (make_local_hint_db false [] gl) hyps) gl
 
506
  
 
507
let default_full_auto gl = full_auto !default_search_depth gl
 
508
(************************************************************************)
 
509
 
 
510
let blast_tactic = ref (free_try default_full_auto)
 
511
;;
 
512
 
 
513
let blast_auto = (free_try default_full_auto)
 
514
(*                  (tclTHEN (free_try default_full_auto)
 
515
                          (free_try (my_full_eauto 2)))
 
516
*)
 
517
;;
 
518
let blast_simpl = (free_try (reduce (Simpl None) onConcl))
 
519
;;
 
520
let blast_induction1 = 
 
521
    (free_try (tclTHEN (tclTRY intro)
 
522
                       (tclTRY (tclLAST_HYP simplest_elim))))
 
523
;;
 
524
let blast_induction2 = 
 
525
    (free_try (tclTHEN (tclTRY (tclTHEN intro intro))
 
526
                       (tclTRY (tclLAST_HYP simplest_elim))))
 
527
;;
 
528
let blast_induction3 = 
 
529
    (free_try (tclTHEN (tclTRY (tclTHEN intro (tclTHEN intro intro)))
 
530
                       (tclTRY (tclLAST_HYP simplest_elim))))
 
531
;;
 
532
 
 
533
blast_tactic :=
 
534
  (tclORELSE (tclCOMPLETE blast_auto)
 
535
  (tclORELSE (tclCOMPLETE (tclTHEN blast_simpl blast_auto))
 
536
  (tclORELSE (tclCOMPLETE (tclTHEN blast_induction1
 
537
                          (tclTHEN blast_simpl blast_auto)))
 
538
  (tclORELSE (tclCOMPLETE (tclTHEN blast_induction2
 
539
                          (tclTHEN blast_simpl blast_auto)))
 
540
             (tclCOMPLETE (tclTHEN blast_induction3
 
541
                          (tclTHEN blast_simpl blast_auto)))))))
 
542
;;
 
543
(*
 
544
blast_tactic := (tclTHEN (free_try default_full_auto)
 
545
                         (free_try (my_full_eauto 4)))
 
546
;;
 
547
*)
 
548
 
 
549
let vire_extvar s =
 
550
   let interro = ref false in
 
551
   let interro_pos = ref 0 in
 
552
   for i=0 to (length s)-1 do
 
553
     if get s i = '?'
 
554
     then (interro := true;
 
555
           interro_pos := i)
 
556
     else if (!interro && 
 
557
              (List.mem (get s i)
 
558
                        ['0';'1';'2';'3';'4';'5';'6';'7';'8';'9']))
 
559
     then set s i ' '
 
560
     else interro:=false
 
561
   done;
 
562
   s
 
563
;;
 
564
 
 
565
let blast gls =
 
566
   let leaf g = {
 
567
      open_subgoals = 1;
 
568
      goal = g;
 
569
      ref = None } in
 
570
     try (let (sgl,v) as _res = !blast_tactic gls in
 
571
          let {it=lg} = sgl in
 
572
          if lg = [] 
 
573
          then (let pf = v (List.map leaf (sig_it sgl)) in
 
574
                let sign = (sig_it gls).evar_hyps in
 
575
                let x = print_subscript 
 
576
                     (sig_sig gls) sign pf in
 
577
                msgnl (hov 0 (str"Blast ==> " ++ x));
 
578
                let x = print_subscript 
 
579
                     (sig_sig gls) sign pf in
 
580
                let tac_string =
 
581
                pp_string  (hov 0 x ) in
 
582
    (* on remplace les ?1 ?2 ... de refine par ? *)
 
583
                parse_tac ((vire_extvar tac_string)
 
584
                           ^ ".")
 
585
          )
 
586
          else (msgnl (hov 0 (str"Blast failed to prove the goal..."));
 
587
                failwith "echec de blast"))
 
588
     with _ -> failwith "echec de blast"
 
589
;;
 
590
 
 
591
let blast_tac display_function = function 
 
592
          | (n::_) as _l -> 
 
593
                 (function g ->
 
594
                    let exp_ast = (blast g) in
 
595
                     (display_function exp_ast;
 
596
                       tclIDTAC g))
 
597
          |  _ -> failwith "expecting other arguments";;
 
598
 
 
599
let blast_tac_txt = 
 
600
  blast_tac
 
601
    (function x -> msgnl(Pptactic.pr_glob_tactic (Global.env()) (Tacinterp.glob_tactic x)));;
 
602
 
 
603
(* Obsol�te ?
 
604
overwriting_add_tactic "Blast1" blast_tac_txt;;
 
605
*)
 
606
 
 
607
(*
 
608
Grammar tactic ne_numarg_list : list :=
 
609
  ne_numarg_single [numarg($n)] ->[$n]
 
610
| ne_numarg_cons [numarg($n) ne_numarg_list($ns)] -> [ $n ($LIST $ns) ].
 
611
Grammar tactic simple_tactic : ast :=
 
612
  blast1 [ "Blast1" ne_numarg_list($ns) ] ->
 
613
         [ (Blast1 ($LIST $ns)) ].
 
614
 
 
615
 
 
616
 
 
617
PATH=/usr/local/bin:/usr/bin:$PATH
 
618
COQTOP=d:/Tools/coq-7.0-3mai
 
619
CAMLLIB=/usr/local/lib/ocaml
 
620
CAMLP4LIB=/usr/local/lib/camlp4
 
621
export CAMLLIB
 
622
export COQTOP
 
623
export CAMLP4LIB 
 
624
d:/Tools/coq-7.0-3mai/bin/coqtop.byte.exe 
 
625
Drop.
 
626
#use "/cygdrive/D/Tools/coq-7.0-3mai/dev/base_include";;
 
627
*)