]> matita.cs.unibo.it Git - helm.git/blob - helm/software/components/ng_tactics/nTactics.ml
Added ntry and nassumption tactics
[helm.git] / helm / software / components / ng_tactics / nTactics.ml
1 (*
2     ||M||  This file is part of HELM, an Hypertextual, Electronic        
3     ||A||  Library of Mathematics, developed at the Computer Science     
4     ||T||  Department, University of Bologna, Italy.                     
5     ||I||                                                                
6     ||T||  HELM is free software; you can redistribute it and/or         
7     ||A||  modify it under the terms of the GNU General Public License   
8     \   /  version 2 or (at your option) any later version.      
9      \ /   This software is distributed as is, NO WARRANTY.     
10       V_______________________________________________________________ *)
11
12 (* $Id: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *)
13
14 open Printf
15
16 let debug = true
17 let debug_print s = if debug then prerr_endline (Lazy.force s) else ()
18
19 open Continuationals.Stack
20 open NTacStatus
21 module Ast = CicNotationPt
22
23 let id_tac status = status ;;
24 let print_tac print_status message status = 
25   if print_status then pp_tac_status status;
26   prerr_endline message; 
27   status
28 ;;
29
30 let dot_tac status =
31   let new_gstatus = 
32     match status.gstatus with
33     | [] -> assert false
34     | ([], _, [], _) :: _ as stack ->
35         (* backward compatibility: do-nothing-dot *)
36         stack
37     | (g, t, k, tag) :: s ->
38         match filter_open g, k with
39         | loc :: loc_tl, _ -> 
40              (([ loc ], t, loc_tl @+ k, tag) :: s) 
41         | [], loc :: k ->
42             assert (is_open loc);
43             (([ loc ], t, k, tag) :: s)
44         | _ -> fail (lazy "can't use \".\" here")
45   in
46    { status with gstatus = new_gstatus }
47 ;;
48
49 let branch_tac status =
50   let new_gstatus = 
51     match status.gstatus with
52     | [] -> assert false
53     | (g, t, k, tag) :: s ->
54           match init_pos g with (* TODO *)
55           | [] | [ _ ] -> fail (lazy "too few goals to branch");
56           | loc :: loc_tl ->
57                ([ loc ], [], [], `BranchTag) :: (loc_tl, t, k, tag) :: s
58   in
59    { status with gstatus = new_gstatus }
60 ;;
61
62 let shift_tac status =
63   let new_gstatus = 
64     match status.gstatus with
65     | (g, t, k, `BranchTag) :: (g', t', k', tag) :: s ->
66           (match g' with
67           | [] -> fail (lazy "no more goals to shift")
68           | loc :: loc_tl ->
69                 (([ loc ], t @+ filter_open g @+ k, [],`BranchTag)
70                 :: (loc_tl, t', k', tag) :: s))
71      | _ -> fail (lazy "can't shift goals here")
72   in
73    { status with gstatus = new_gstatus }
74 ;;
75
76 let pos_tac i_s status =
77   let new_gstatus = 
78     match status.gstatus with
79     | [] -> assert false
80     | ([ loc ], t, [],`BranchTag) :: (g', t', k', tag) :: s
81       when is_fresh loc ->
82         let l_js = List.filter (fun (i, _) -> List.mem i i_s) ([loc] @+ g') in
83           ((l_js, t , [],`BranchTag)
84            :: (([ loc ] @+ g') @- l_js, t', k', tag) :: s)
85     | _ -> fail (lazy "can't use relative positioning here")
86   in
87    { status with gstatus = new_gstatus }
88 ;;
89
90 let wildcard_tac status =
91   let new_gstatus = 
92     match status.gstatus with
93     | [] -> assert false
94     | ([ loc ] , t, [], `BranchTag) :: (g', t', k', tag) :: s
95        when is_fresh loc ->
96             (([loc] @+ g', t, [], `BranchTag) :: ([], t', k', tag) :: s)
97     | _ -> fail (lazy "can't use wildcard here")
98   in
99    { status with gstatus = new_gstatus }
100 ;;
101
102 let merge_tac status =
103   let new_gstatus = 
104     match status.gstatus with
105     | [] -> assert false
106     | (g, t, k,`BranchTag) :: (g', t', k', tag) :: s ->
107         ((t @+ filter_open g @+ g' @+ k, t', k', tag) :: s)
108     | _ -> fail (lazy "can't merge goals here")
109   in
110    { status with gstatus = new_gstatus }
111 ;;
112       
113 let focus_tac gs status =
114   let new_gstatus = 
115     match status.gstatus with
116     | [] -> assert false
117     | s -> assert(gs <> []);
118           let stack_locs =
119             let add_l acc _ _ l = if is_open l then l :: acc else acc in
120             fold ~env:add_l ~cont:add_l ~todo:add_l [] s
121           in
122           List.iter
123             (fun g ->
124               if not (List.exists (fun l -> goal_of_loc l = g) stack_locs) then
125                 fail (lazy (sprintf "goal %d not found (or closed)" g)))
126             gs;
127           (zero_pos gs, [], [], `FocusTag) :: deep_close gs s
128   in
129    { status with gstatus = new_gstatus }
130 ;;
131
132 let unfocus_tac status =
133   let new_gstatus = 
134     match status.gstatus with
135     | [] -> assert false
136     | ([], [], [], `FocusTag) :: s -> s
137     | _ -> fail (lazy "can't unfocus, some goals are still open")
138   in
139    { status with gstatus = new_gstatus }
140 ;;
141
142 let skip_tac status =
143   let new_gstatus = 
144     match status.gstatus with
145     | [] -> assert false
146     | (gl, t, k, tag) :: s -> 
147         let gl = List.map switch_of_loc gl in
148         if List.exists (function Open _ -> true | Closed _ -> false) gl then 
149           fail (lazy "cannot skip an open goal")
150         else 
151           ([],t,k,tag) :: s
152   in
153    { status with gstatus = new_gstatus }
154 ;;
155
156 let block_tac l status =
157   List.fold_left (fun status tac -> tac status) status l
158 ;;
159
160 let compare_statuses ~past ~present =
161  let _,_,past,_,_ = past.pstatus in 
162  let _,_,present,_,_ = present.pstatus in 
163  List.map fst (List.filter (fun (i,_) -> not(List.mem_assoc i past)) present),
164  List.map fst (List.filter (fun (i,_) -> not (List.mem_assoc i present)) past)
165 ;;
166
167
168
169 (* Exec and distribute_tac form a retraction pair:
170     1) exec (distribute_tac low_tac) (s,i) = low_tac (s,i)
171     2) tac [s]::G = G1::...::Gn::G' && G' is G with some goals closed =>
172          distribute_tac (exec tac) [s]::G = (G1@...Gn)::G'
173     3) tac G = distribute_tac (exec tac) G if  
174        tac = distribute_tac lowtac
175     4) atomic_tac t === distribute_tac (exec t)
176
177    Note that executing an high tactic on a set of goals may be stronger
178    than executing the same tactic on those goals, but once at a time
179    (e.g. the tactic could perform a global analysis of the set of goals)
180 *)
181
182 let exec tac low_status g =
183   let stack = [ [0,Open g], [], [], `NoTag ] in
184   let status = tac { gstatus = stack ; istatus = low_status } in
185    status.istatus
186 ;;
187
188 let distribute_tac tac status =
189   match status.gstatus with
190   | [] -> assert false
191   | (g, t, k, tag) :: s ->
192       debug_print (lazy ("context length " ^string_of_int (List.length g)));
193       let rec aux s go gc =
194         function
195         | [] -> 
196             debug_print (lazy "no selected goals");
197             s, go, gc
198         | loc :: loc_tl ->
199             debug_print (lazy "inner eval tactical");
200             let s, go, gc =
201               if List.exists ((=) (goal_of_loc loc)) gc then
202                 s, go, gc
203               else
204                 match switch_of_loc loc with
205                 | Closed _ -> fail (lazy "cannot apply to a Closed goal")
206                 | Open n -> 
207                    let sn = tac s n in
208                    let go', gc' = compare_statuses ~past:s ~present:sn in
209                    sn, ((go @+ [n]) @- gc') @+ go', gc @+ gc'
210             in
211             aux s go gc loc_tl
212       in
213       let s0, go0, gc0 = status.istatus, [], [] in
214       let sn, gon, gcn = aux s0 go0 gc0 g in
215       debug_print (lazy ("opened: "
216         ^ String.concat " " (List.map string_of_int gon)));
217       debug_print (lazy ("closed: "
218         ^ String.concat " " (List.map string_of_int gcn)));
219       let stack =
220         (zero_pos gon, t @~- gcn, k @~- gcn, tag) :: deep_close gcn s
221       in
222        { gstatus = stack; istatus = sn }
223 ;;
224
225 let atomic_tac htac = distribute_tac (exec htac) ;;
226
227 let try_tac tac status =
228   try
229     tac status
230   with NTacStatus.Error _ ->
231     status
232 ;;
233
234 let first_tac tacl status =
235   let res = HExtlib.list_findopt
236     (fun tac _ ->
237        try Some (tac status) with
238            NTacStatus.Error _ -> None) tacl
239   in
240     match res with
241       | None -> raise (NTacStatus.Error (lazy("No tactic left")))
242       | Some x -> x
243 ;;
244
245 let exact_tac t = distribute_tac (fun status goal ->
246  let goalty = get_goalty status goal in
247  let status, t = disambiguate status t (Some goalty) (ctx_of goalty) in
248  instantiate status goal t)
249 ;;
250
251 let assumption status goal =
252   let gty = get_goalty status goal in
253   let context = ctx_of gty in
254   let (htac:NTacStatus.tactic) = 
255     first_tac (List.map
256                  (fun (name,_) -> 
257                     exact_tac ("",0,(Ast.Ident (name,None))))
258                  context)
259   in
260     exec htac status goal
261 ;;
262
263 let assumption_tac =
264   distribute_tac assumption
265 ;;
266
267 let find_in_context name context =
268   let rec aux acc = function
269     | [] -> raise Not_found
270     | (hd,_) :: tl when hd = name -> acc
271     | _ :: tl ->  aux (acc + 1) tl
272   in
273   aux 1 context
274 ;;
275
276 let clear_tac names =
277  if names = [] then id_tac
278  else
279   distribute_tac (fun status goal ->
280    let goalty = get_goalty status goal in
281    let js =
282      List.map 
283      (fun name -> 
284         try find_in_context name (ctx_of goalty)
285         with Not_found -> 
286           fail (lazy ("hypothesis '" ^ name ^ "' not found"))) 
287      names
288    in
289    let n,h,metasenv,subst,o = status.pstatus in
290    let metasenv,subst,_ = NCicMetaSubst.restrict metasenv subst goal js in
291     { status with pstatus = n,h,metasenv,subst,o })
292 ;;
293
294 let generalize0_tac args =
295  if args = [] then id_tac
296  else exact_tac ("",0,Ast.Appl (Ast.Implicit :: args))
297 ;;
298
299 let select0_tac ~where:(wanted,hyps,where) ~job  =
300  let found, postprocess = 
301    match job with
302    | `Substexpand argsno -> mk_in_scope, mk_out_scope argsno
303    | `Collect l -> (fun s t -> l := t::!l; mk_in_scope s t), mk_out_scope 1
304    | `ChangeWith f -> f,(fun s t -> s, t)
305  in
306  distribute_tac (fun status goal ->
307    let goalty = get_goalty status goal in
308    let path = 
309      match where with None -> NCic.Implicit `Term | Some where -> where 
310    in
311    let status, newgoalctx =
312       List.fold_right
313        (fun (name,d as entry) (status,ctx) ->
314          try
315           let path = List.assoc name hyps in
316            match d with
317               NCic.Decl ty ->
318                let status,ty =
319                 select_term status ~found ~postprocess (mk_cic_term ctx ty)
320                  (wanted,path) in
321                let status,ty = term_of_cic_term status ty ctx in
322                 status,(name,NCic.Decl ty)::ctx
323             | NCic.Def (bo,ty) ->
324                let status,bo =
325                 select_term status ~found ~postprocess (mk_cic_term ctx bo)
326                  (wanted,path) in
327                let status,bo = term_of_cic_term status bo ctx in
328                 status,(name,NCic.Def (bo,ty))::ctx
329          with
330           Not_found -> status, entry::ctx
331        ) (ctx_of goalty) (status,[])
332    in
333    let status, newgoalty = 
334      select_term status ~found ~postprocess goalty (wanted,path) in
335    (* WARNING: the next two lines simply change the context of newgoalty
336       from the old to the new one. Otherwise mk_meta will do that herself,
337       calling relocate that calls delift. However, newgoalty is now
338       ?[out_scope] and thus the delift would trigger the special unification
339       case, which is wrong now :-( *)
340    let status,newgoalty = term_of_cic_term status newgoalty (ctx_of goalty) in
341    let newgoalty = mk_cic_term newgoalctx newgoalty in
342
343    let status, instance = 
344      mk_meta status newgoalctx (`Decl newgoalty) 
345    in
346    instantiate status goal instance)
347 ;;
348
349 let select_tac ~where ~job move_down_hyps = 
350  let (wanted,hyps,where) = GrafiteDisambiguate.disambiguate_npattern where in
351  let path = 
352   match where with None -> NCic.Implicit `Term | Some where -> where in
353  if not move_down_hyps then
354   select0_tac ~where:(wanted,hyps,Some path) ~job
355  else
356   let path = 
357    List.fold_left
358      (fun path (name,path_name) -> NCic.Prod ("_",path_name,path))
359      path (List.rev hyps)
360   in
361    block_tac [ 
362      generalize0_tac (List.map (fun (name,_) -> Ast.Ident (name,None)) hyps);
363      select0_tac ~where:(wanted,[],Some path) ~job;
364      clear_tac (List.map fst hyps) ]
365 ;;
366
367 let generalize_tac ~where = 
368  let l = ref [] in
369  block_tac [ 
370    select_tac ~where ~job:(`Collect l) true; 
371    print_tac true "ha selezionato?";
372    (fun s -> distribute_tac (fun status goal ->
373       let goalty = get_goalty status goal in
374       let status,canon,rest =
375        match !l with
376           [] ->
377            (match where with
378                _,_,(None,_,_)  -> fail (lazy "No term to generalize")
379              | txt,txtlen,(Some what,_,_) ->
380                 let status, what =
381                  disambiguate status (txt,txtlen,what) None (ctx_of goalty)
382                 in
383                  status,what,[]
384            )
385         | he::tl -> status,he,tl in
386       let status = 
387        List.fold_left 
388          (fun s t -> unify s (ctx_of goalty) canon t) status rest in
389       let status, canon = term_of_cic_term status canon (ctx_of goalty) in
390       instantiate status goal 
391        (mk_cic_term (ctx_of goalty) (NCic.Appl [NCic.Implicit `Term ; canon ]))
392    ) s) ]
393 ;;
394
395 let reduce_tac ~reduction ~where =
396   let change status t = 
397     match reduction with
398     | `Normalize perform_delta ->
399         normalize status
400          ?delta:(if perform_delta then None else Some max_int) (ctx_of t) t
401     | `Whd perform_delta -> 
402         whd status
403          ?delta:(if perform_delta then None else Some max_int) (ctx_of t) t
404   in
405   let where = GrafiteDisambiguate.disambiguate_npattern where in
406   select0_tac ~where ~job:(`ChangeWith change)
407 ;;
408
409 let change_tac ~where ~with_what =
410   let change status t = 
411     let status, ww = disambiguate status with_what  None (ctx_of t) in
412     let status = unify status (ctx_of t) t ww in
413     status, ww
414   in
415   let where = GrafiteDisambiguate.disambiguate_npattern where in
416   select0_tac ~where ~job:(`ChangeWith change)
417 ;;
418
419 let letin_tac ~where ~what:(_,_,w) name =
420  block_tac [
421   select_tac ~where ~job:(`Substexpand 1) true;
422   exact_tac ("",0,Ast.LetIn((Ast.Ident (name,None),None),w,Ast.Implicit));
423  ]
424 ;;
425
426 let apply_tac = exact_tac;;
427
428 type indtyinfo = {
429         rightno: int;
430         leftno: int;
431         consno: int;
432         lefts: NCic.term list;
433         rights: NCic.term list;
434         reference: NReference.reference;
435  }
436 ;;
437
438 let analyze_indty_tac ~what indtyref = distribute_tac (fun status goal ->
439   let goalty = get_goalty status goal in
440   let status, what = disambiguate status what None (ctx_of goalty) in
441   let status, ty_what = typeof status (ctx_of what) what in 
442   let status, (r,consno,lefts,rights) = analyse_indty status ty_what in
443   let leftno = List.length rights in
444   let rightno = List.length rights in
445   indtyref := Some { 
446     rightno = rightno; leftno = leftno; consno = consno;
447     lefts = lefts; rights = rights; reference = r;
448   };
449   exec id_tac status goal)
450 ;;
451
452 let elim_tac ~what ~where = 
453   let indtyinfo = ref None in
454   let sort = ref None in
455   let compute_goal_sort_tac = distribute_tac (fun status goal ->
456     let goalty = get_goalty status goal in
457     let status, goalsort = typeof status (ctx_of goalty) goalty in
458     sort := Some goalsort;
459     exec id_tac status goal)
460   in
461   atomic_tac (block_tac [
462     analyze_indty_tac ~what indtyinfo;    
463     (fun s -> select_tac 
464       ~where ~job:(`Substexpand ((HExtlib.unopt !indtyinfo).rightno+1)) true s);
465     compute_goal_sort_tac;
466     (fun status ->
467      let sort = HExtlib.unopt !sort in
468      let ity = HExtlib.unopt !indtyinfo in
469      let NReference.Ref (uri, _) = ity.reference in
470      let istatus, sort = term_of_cic_term status.istatus sort (ctx_of sort) in
471      let status = { status with istatus = istatus } in
472      let name = NUri.name_of_uri uri ^
473       match sort with
474        | NCic.Sort NCic.Prop -> "_ind"
475        | NCic.Sort _ -> "_rect"
476        | _ -> assert false 
477      in
478      let holes = 
479        HExtlib.mk_list Ast.Implicit (ity.leftno+1+ ity.consno + ity.rightno) in
480      let eliminator = 
481        let _,_,w = what in
482        Ast.Appl(Ast.Ident(name,None)::holes @ [ w ])
483      in
484      exact_tac ("",0,eliminator) status) ]) 
485 ;;
486
487 let rewrite_tac ~dir ~what:(_,_,what) ~where =
488  let name =
489   match dir with `LeftToRight -> "eq_elim_r" | `RightToLeft -> "eq_ind"
490  in
491   block_tac
492    [ select_tac ~where ~job:(`Substexpand 1) true;
493      exact_tac
494       ("",0,
495        Ast.Appl(Ast.Ident(name,None)::HExtlib.mk_list Ast.Implicit 5 @
496         [what]))]
497 ;;
498
499 let intro_tac name =
500  block_tac
501   [ exact_tac
502      ("",0,(Ast.Binder (`Lambda,
503       (Ast.Ident (name,None),None),Ast.Implicit)));
504     if name = "_" then clear_tac [name] else id_tac ]
505 ;;
506
507 let cases ~what status goal =
508  let gty = get_goalty status goal in
509  let status, what = disambiguate status what None (ctx_of gty) in
510  let status, ty = typeof status (ctx_of what) what in
511  let status, (ref, consno, _, _) = analyse_indty status ty in
512  let status, what = term_of_cic_term status what (ctx_of gty) in
513  let t =
514   NCic.Match (ref,NCic.Implicit `Term, what,
515     HExtlib.mk_list (NCic.Implicit `Term) consno)
516  in
517  let ctx = ctx_of gty in
518  let status,t,ty = refine status ctx (mk_cic_term ctx t) (Some gty) in
519  instantiate status goal t
520 ;;
521
522 let cases_tac ~what ~where = 
523   let indtyinfo = ref None in
524   atomic_tac 
525    (block_tac [
526       analyze_indty_tac ~what indtyinfo;
527       (fun s -> select_tac 
528        ~where ~job:(`Substexpand ((HExtlib.unopt !indtyinfo).rightno+1))true s);
529       distribute_tac (cases ~what) ])
530 ;;
531
532 let case1_tac name =
533  let name = if name = "_" then "_clearme" else name in
534  block_tac [ intro_tac name; 
535              cases_tac 
536               ~where:("",0,(None,[],None)) 
537               ~what:("",0,Ast.Ident (name,None));
538              if name = "_clearme" then clear_tac ["_clearme"] else id_tac ]
539 ;;
540
541 let assert0_tac (hyps,concl) = distribute_tac (fun status goal ->
542  let gty = get_goalty status goal in
543  let eq status ctx t1 t2 =
544   let status,t1 = disambiguate status t1 None ctx in
545   let status,t1 = apply_subst status ctx t1 in
546   let status,t1 = term_of_cic_term status t1 ctx in
547   let t2 = mk_cic_term ctx t2 in
548   let status,t2 = apply_subst status ctx t2 in
549   let status,t2 = term_of_cic_term status t2 ctx in
550   prerr_endline ("COMPARING: " ^ NCicPp.ppterm ~subst:[] ~metasenv:[] ~context:ctx t1 ^ " vs " ^ NCicPp.ppterm ~subst:[] ~metasenv:[] ~context:ctx t2);
551   assert (t1=t2);
552   status
553  in
554  let status,gty' = term_of_cic_term status gty (ctx_of gty) in
555  let status = eq status (ctx_of gty) concl gty' in
556  let status,_ =
557   List.fold_right2
558    (fun (id1,e1) ((id2,e2) as item) (status,ctx) ->
559      assert (id1=id2 || (prerr_endline (id1 ^ " vs " ^ id2); false));
560      match e1,e2 with
561         `Decl t1, NCic.Decl t2 ->
562           let status = eq status ctx t1 t2 in
563           status,item::ctx
564       | `Def (b1,t1), NCic.Def (b2,t2) ->
565           let status = eq status ctx t1 t2 in
566           let status = eq status ctx b1 b2 in
567           status,item::ctx
568       | _ -> assert false
569    ) hyps (ctx_of gty) (status,[])
570  in
571   exec id_tac status goal)
572 ;;
573
574 let assert_tac seqs status =
575  match status.gstatus with
576   | [] -> assert false
577   | (g,_,_,_) :: s ->
578      assert (List.length g = List.length seqs);
579      (match seqs with
580          [] -> id_tac
581        | [seq] -> assert0_tac seq
582        | _ ->
583          block_tac
584           (branch_tac::
585           HExtlib.list_concat ~sep:[shift_tac]
586             (List.map (fun seq -> [assert0_tac seq]) seqs)@
587           [merge_tac])
588      ) status
589 ;;
590
591 let auto ~params:(l,_) status goal =
592   let gty = get_goalty status goal in
593   let n,h,metasenv,subst,o = status.pstatus in
594   let status,t = term_of_cic_term status gty (ctx_of gty) in
595   let status, l = 
596     List.fold_left
597       (fun (status, l) t ->
598         let status, t = disambiguate status t None (ctx_of gty) in
599         let status, ty = typeof status (ctx_of t) t in
600         let status, t =  term_of_cic_term status t (ctx_of gty) in
601         let status, ty = term_of_cic_term status ty (ctx_of ty) in
602         (status, (t,ty) :: l))
603       (status,[]) l
604   in
605   let rdb = status.estatus in
606   let pt, metasenv, subst = 
607     Paramod.nparamod rdb metasenv subst (ctx_of gty) (NCic.Rel ~-1,t) l 
608   in      
609   let status = { status with pstatus = n,h,metasenv,subst,o } in
610   instantiate status goal (NTacStatus.mk_cic_term (ctx_of gty) pt)
611 ;;
612
613 let auto_tac ~params status =
614   distribute_tac (auto ~params) status
615 ;;