]> matita.cs.unibo.it Git - helm.git/blob - helm/software/components/ng_tactics/nTactics.ml
generalized is half-implemented (still broken)
[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 message status = prerr_endline message; status ;;
25
26 let dot_tac status =
27   let new_gstatus = 
28     match status.gstatus with
29     | [] -> assert false
30     | ([], _, [], _) :: _ as stack ->
31         (* backward compatibility: do-nothing-dot *)
32         stack
33     | (g, t, k, tag) :: s ->
34         match filter_open g, k with
35         | loc :: loc_tl, _ -> 
36              (([ loc ], t, loc_tl @+ k, tag) :: s) 
37         | [], loc :: k ->
38             assert (is_open loc);
39             (([ loc ], t, k, tag) :: s)
40         | _ -> fail (lazy "can't use \".\" here")
41   in
42    { status with gstatus = new_gstatus }
43 ;;
44
45 let branch_tac status =
46   let new_gstatus = 
47     match status.gstatus with
48     | [] -> assert false
49     | (g, t, k, tag) :: s ->
50           match init_pos g with (* TODO *)
51           | [] | [ _ ] -> fail (lazy "too few goals to branch");
52           | loc :: loc_tl ->
53                ([ loc ], [], [], `BranchTag) :: (loc_tl, t, k, tag) :: s
54   in
55    { status with gstatus = new_gstatus }
56 ;;
57
58 let shift_tac status =
59   let new_gstatus = 
60     match status.gstatus with
61     | (g, t, k, `BranchTag) :: (g', t', k', tag) :: s ->
62           (match g' with
63           | [] -> fail (lazy "no more goals to shift")
64           | loc :: loc_tl ->
65                 (([ loc ], t @+ filter_open g @+ k, [],`BranchTag)
66                 :: (loc_tl, t', k', tag) :: s))
67      | _ -> fail (lazy "can't shift goals here")
68   in
69    { status with gstatus = new_gstatus }
70 ;;
71
72 let pos_tac i_s status =
73   let new_gstatus = 
74     match status.gstatus with
75     | [] -> assert false
76     | ([ loc ], t, [],`BranchTag) :: (g', t', k', tag) :: s
77       when is_fresh loc ->
78         let l_js = List.filter (fun (i, _) -> List.mem i i_s) ([loc] @+ g') in
79           ((l_js, t , [],`BranchTag)
80            :: (([ loc ] @+ g') @- l_js, t', k', tag) :: s)
81     | _ -> fail (lazy "can't use relative positioning here")
82   in
83    { status with gstatus = new_gstatus }
84 ;;
85
86 let wildcard_tac status =
87   let new_gstatus = 
88     match status.gstatus with
89     | [] -> assert false
90     | ([ loc ] , t, [], `BranchTag) :: (g', t', k', tag) :: s
91        when is_fresh loc ->
92             (([loc] @+ g', t, [], `BranchTag) :: ([], t', k', tag) :: s)
93     | _ -> fail (lazy "can't use wildcard here")
94   in
95    { status with gstatus = new_gstatus }
96 ;;
97
98 let merge_tac status =
99   let new_gstatus = 
100     match status.gstatus with
101     | [] -> assert false
102     | (g, t, k,`BranchTag) :: (g', t', k', tag) :: s ->
103         ((t @+ filter_open g @+ g' @+ k, t', k', tag) :: s)
104     | _ -> fail (lazy "can't merge goals here")
105   in
106    { status with gstatus = new_gstatus }
107 ;;
108       
109 let focus_tac gs status =
110   let new_gstatus = 
111     match status.gstatus with
112     | [] -> assert false
113     | s -> assert(gs <> []);
114           let stack_locs =
115             let add_l acc _ _ l = if is_open l then l :: acc else acc in
116             fold ~env:add_l ~cont:add_l ~todo:add_l [] s
117           in
118           List.iter
119             (fun g ->
120               if not (List.exists (fun l -> goal_of_loc l = g) stack_locs) then
121                 fail (lazy (sprintf "goal %d not found (or closed)" g)))
122             gs;
123           (zero_pos gs, [], [], `FocusTag) :: deep_close gs s
124   in
125    { status with gstatus = new_gstatus }
126 ;;
127
128 let unfocus_tac status =
129   let new_gstatus = 
130     match status.gstatus with
131     | [] -> assert false
132     | ([], [], [], `FocusTag) :: s -> s
133     | _ -> fail (lazy "can't unfocus, some goals are still open")
134   in
135    { status with gstatus = new_gstatus }
136 ;;
137
138 let skip_tac status =
139   let new_gstatus = 
140     match status.gstatus with
141     | [] -> assert false
142     | (gl, t, k, tag) :: s -> 
143         let gl = List.map switch_of_loc gl in
144         if List.exists (function Open _ -> true | Closed _ -> false) gl then 
145           fail (lazy "cannot skip an open goal")
146         else 
147           ([],t,k,tag) :: s
148   in
149    { status with gstatus = new_gstatus }
150 ;;
151
152 let block_tac l status =
153   List.fold_left (fun status tac -> tac status) status l
154 ;;
155
156 let compare_statuses ~past ~present =
157  let _,_,past,_,_ = past.pstatus in 
158  let _,_,present,_,_ = present.pstatus in 
159  let closed = 
160   List.map fst (List.filter (fun (i,_) -> not (List.mem_assoc i present)) past)
161  in
162  let opened = 
163    List.map fst (List.filter (fun (i,_) -> not(List.mem_assoc i past)) present)
164  in
165  opened, closed
166 ;;
167
168
169
170 (* Exec and distribute_tac form a retraction pair:
171     1) exec (distribute_tac low_tac) (s,i) = low_tac (s,i)
172     2) tac [s]::G = G1::...::Gn::G' && G' is G with some goals closed =>
173          distribute_tac (exec tac) [s]::G = (G1@...Gn)::G'
174     3) tac G = distribute_tac (exec tac) G if  
175        tac = distribute_tac lowtac
176     4) atomic_tac t === distribute_tac (exec t)
177
178    Note that executing an high tactic on a set of goals may be stronger
179    than executing the same tactic on those goals, but once at a time
180    (e.g. the tactic could perform a global analysis of the set of goals)
181 *)
182
183 let exec tac low_status g =
184   let stack = [ [0,Open g], [], [], `NoTag ] in
185   let status = tac { gstatus = stack ; istatus = low_status } in
186    status.istatus
187 ;;
188
189 let distribute_tac tac status =
190   match status.gstatus with
191   | [] -> assert false
192   | (g, t, k, tag) :: s ->
193       debug_print (lazy ("context length " ^string_of_int (List.length g)));
194       let rec aux s go gc =
195         function
196         | [] -> 
197             debug_print (lazy "no selected goals");
198             s, go, gc
199         | loc :: loc_tl ->
200             debug_print (lazy "inner eval tactical");
201             let s, go, gc =
202               if List.exists ((=) (goal_of_loc loc)) gc then
203                 s, go, gc
204               else
205                 match switch_of_loc loc with
206                 | Closed _ -> fail (lazy "cannot apply to a Closed goal")
207                 | Open n -> 
208                    let sn = tac s n in
209                    let go', gc' = compare_statuses ~past:s ~present:sn in
210                    sn, ((go @+ [n]) @- gc') @+ go', gc @+ gc'
211             in
212             aux s go gc loc_tl
213       in
214       let s0, go0, gc0 = status.istatus, [], [] in
215       let sn, gon, gcn = aux s0 go0 gc0 g in
216       debug_print (lazy ("opened: "
217         ^ String.concat " " (List.map string_of_int gon)));
218       debug_print (lazy ("closed: "
219         ^ String.concat " " (List.map string_of_int gcn)));
220       let stack =
221         (zero_pos gon, t @~- gcn, k @~- gcn, tag) :: deep_close gcn s
222       in
223        { gstatus = stack; istatus = sn }
224 ;;
225
226 let atomic_tac htac = distribute_tac (exec htac) ;;
227
228 let exact t status goal =
229  let goalty = get_goalty status goal in
230  let status, t = disambiguate status t (Some goalty) (ctx_of goalty) in
231  instantiate status goal t
232 ;;
233
234 let exact_tac t = distribute_tac (exact t) ;;
235
236 let find_in_context name context =
237   let rec aux acc = function
238     | [] -> raise Not_found
239     | (hd,_) :: tl when hd = name -> acc
240     | _ :: tl ->  aux (acc + 1) tl
241   in
242   aux 1 context
243 ;;
244
245 let clear names status goal =
246  let goalty = get_goalty status goal in
247  let js =
248    List.map 
249      (fun name -> 
250         try find_in_context name (ctx_of goalty)
251         with Not_found -> 
252           fail (lazy ("hypothesis '" ^ name ^ "' not found"))) 
253      names
254  in
255  let n,h,metasenv,subst,o = status.pstatus in
256  let metasenv,subst,_ = NCicMetaSubst.restrict metasenv subst goal js in
257   { status with pstatus = n,h,metasenv,subst,o }
258 ;;
259
260 let force f s = Lazy.force f s;;
261
262 let clear_tac names =
263  if names = [] then id_tac else distribute_tac (clear names)
264 ;;
265
266 let generalize0_tac args =
267  if args = [] then id_tac
268  else exact_tac ("",0,Ast.Appl (Ast.Implicit :: args))
269 ;;
270
271 let select0_tac ~where:(wanted,_,where) ~job  =
272  let found, postprocess = 
273    match job with
274    | `Substexpand argsno -> mk_in_scope, mk_out_scope argsno
275    | `Collect l -> (fun s t -> l := t::!l; mk_in_scope s t), mk_out_scope 1
276  in
277  distribute_tac (fun status goal ->
278    let goalty = get_goalty status goal in
279    let path = 
280      match where with None -> NCic.Implicit `Term | Some where -> where 
281    in
282    let status, newgoalty = 
283      select_term status ~found ~postprocess goalty (wanted,path) 
284    in
285    let status, instance = 
286      mk_meta status (ctx_of newgoalty) (`Decl newgoalty) 
287    in
288    instantiate status goal instance)
289 ;;
290
291 let select_tac ~where ~job move_down_hyps = 
292  let (wanted,hyps,where) = GrafiteDisambiguate.disambiguate_npattern where in
293  let path = 
294   match where with None -> NCic.Implicit `Term | Some where -> where in
295  if not move_down_hyps then
296   select0_tac ~where:(wanted,hyps,Some path) ~job
297  else
298   let path = 
299    List.fold_left
300      (fun path (name,path_name) -> NCic.Prod ("_",path_name,path))
301      path (List.rev hyps)
302   in
303    block_tac [ 
304      generalize0_tac (List.map (fun (name,_) -> Ast.Ident (name,None)) hyps);
305      select0_tac ~where:(wanted,[],Some path) ~job;
306      clear_tac (List.map fst hyps) ]
307 ;;
308
309 let generalize_tac ~where = 
310  let l = ref [] in
311  block_tac [ 
312    select_tac ~where ~job:(`Collect l) true; 
313    force (lazy (distribute_tac (fun status goal ->
314      let goalty = get_goalty status goal in
315      (* unift (ctx_of goal) t s *)
316      instantiate status goal 
317        (mk_cic_term (ctx_of goalty) (NCic.Appl [NCic.Implicit `Term ; 
318          term_of_cic_term (List.hd !l) (ctx_of goalty) ]))
319    ))) ]
320 ;;
321
322
323 let reopen status =
324  let n,h,metasenv,subst,o = status.pstatus in
325  let subst, newm = 
326    List.partition 
327     (function (_,(Some tag,_,_,_)) -> 
328             tag <> NCicMetaSubst.in_scope_tag && 
329             not (NCicMetaSubst.is_out_scope_tag tag)
330     | _ -> true)
331     subst 
332  in
333  let in_m, out_m = 
334    List.partition
335      (function (_,(Some tag,_,_,_)) -> 
336          tag = NCicMetaSubst.in_scope_tag | _ -> assert false)
337      newm
338  in
339  let metasenv = List.map (fun (i,(_,c,_,t)) -> i,(None,c,t)) in_m @ metasenv in
340  let in_m = List.map fst in_m in
341  let out_m = match out_m with [i] -> i | _ -> assert false in
342  { status with pstatus = n,h,metasenv,subst,o }, in_m, out_m 
343 ;;
344
345 let change ~where ~with_what status goal =
346  let goalty = get_goalty status goal in
347  let (wanted,_,where) = GrafiteDisambiguate.disambiguate_npattern where in
348  let path = 
349    match where with None -> NCic.Implicit `Term | Some where -> where 
350  in
351  let status, newgoalty = assert false (*
352    select_term status 1 goalty (wanted,path)*) in
353  let status, in_scope, out_scope = reopen status in
354  let status =  List.fold_left (exact with_what) status in_scope in
355
356  let j,(n,cctx,bo,_) = out_scope in
357  let _ = typeof status (ctx_of goalty) (Obj.magic (n,cctx,bo))  in
358
359  let n,h,metasenv,subst,o = status.pstatus in
360  let subst = out_scope :: subst in
361  let status = { status with pstatus = n,h,metasenv,subst,o } in
362
363  let status, instance = 
364    mk_meta status (ctx_of newgoalty) (`Decl newgoalty) 
365  in
366  instantiate status goal instance
367 ;;
368
369 let apply t status goal = exact t status goal;;
370
371 let apply_tac t = distribute_tac (apply t) ;;
372 let change_tac ~where ~with_what = distribute_tac (change ~where ~with_what) ;;
373
374 type indtyinfo = {
375         rightno: int;
376         leftno: int;
377         consno: int;
378         lefts: NCic.term list;
379         rights: NCic.term list;
380         reference: NReference.reference;
381  }
382 ;;
383
384 let analyze_indty_tac ~what indtyref = distribute_tac (fun status goal ->
385   let goalty = get_goalty status goal in
386   let status, what = disambiguate status what None (ctx_of goalty) in
387   let ty_what = typeof status (ctx_of what) what in 
388   let r,consno,lefts,rights = analyse_indty status ty_what in
389   let leftno = List.length rights in
390   let rightno = List.length rights in
391   indtyref := Some { 
392     rightno = rightno; leftno = leftno; consno = consno;
393     lefts = lefts; rights = rights; reference = r;
394   };
395   prerr_endline "FO";
396   exec id_tac status goal)
397 ;;
398
399 let elim_tac ~what ~where = 
400   let indtyinfo = ref None in
401   let sort = ref None in
402   let compute_goal_sort_tac = distribute_tac (fun status goal ->
403     let goalty = get_goalty status goal in
404     let goalsort = typeof status (ctx_of goalty) goalty in
405     prerr_endline "XXXXXXXX";
406     sort := Some goalsort;
407     exec id_tac status goal)
408   in
409   atomic_tac (block_tac [
410     analyze_indty_tac ~what indtyinfo;    
411     force (lazy (select_tac 
412       ~where ~job:(`Substexpand ((HExtlib.unopt !indtyinfo).rightno+1)) true));
413     print_tac "CIAO";
414     compute_goal_sort_tac;
415     print_tac "CIAO2";
416     force (lazy (
417      let sort = HExtlib.unopt !sort in
418      let ity = HExtlib.unopt !indtyinfo in
419      let NReference.Ref (uri, _) = ity.reference in
420      let name = NUri.name_of_uri uri ^
421       match term_of_cic_term sort (ctx_of sort) with
422        | NCic.Sort NCic.Prop -> "_ind"
423        | NCic.Sort _ -> "_rect"
424        | _ -> assert false 
425      in
426      let holes = 
427        HExtlib.mk_list Ast.Implicit (ity.leftno+1+ ity.consno + ity.rightno) in
428      let eliminator = 
429        let _,_,w = what in
430        Ast.Appl(Ast.Ident(name,None)::holes @ [ w ])
431      in
432      exact_tac ("",0,eliminator))) ]) 
433 ;;
434
435 let rewrite_tac ~dir ~what:(_,_,what) ~where =
436  let name =
437   match dir with `LeftToRight -> "eq_elim_r" | `RightToLeft -> "eq_ind"
438  in
439   block_tac
440    [ select_tac ~where ~job:(`Substexpand 2) true;
441      exact_tac
442       ("",0,
443        Ast.Appl(Ast.Ident(name,None)::HExtlib.mk_list Ast.Implicit 5 @
444         [what]))]
445 ;;
446
447 let intro_tac name =
448  block_tac
449   [ exact_tac
450     ("",0,(Ast.Binder (`Lambda,
451      (Ast.Ident (name,None),None),Ast.Implicit)));
452      if name = "_" then clear_tac [name] else id_tac ]
453 ;;
454
455 let cases ~what status goal =
456  let gty = get_goalty status goal in
457  let status, what = disambiguate status what None (ctx_of gty) in
458  let ty = typeof status (ctx_of what) what in
459  let ref, consno, _, _ = analyse_indty status ty in
460  let t =
461   NCic.Match (ref,NCic.Implicit `Term, term_of_cic_term what (ctx_of gty),
462     HExtlib.mk_list (NCic.Implicit `Term) consno)
463  in
464  let ctx = ctx_of gty in
465  let status,t,ty = refine status ctx (mk_cic_term ctx t) (Some gty) in
466  instantiate status goal t
467 ;;
468
469 let cases_tac ~what ~where = 
470   let indtyinfo = ref None in
471   atomic_tac 
472    (block_tac [
473       analyze_indty_tac ~what indtyinfo;
474       force (lazy (select_tac 
475         ~where ~job:(`Substexpand ((HExtlib.unopt !indtyinfo).rightno+1))true));
476       distribute_tac (cases ~what) ])
477 ;;
478
479 let case1_tac name =
480  let name = if name = "_" then "_clearme" else name in
481  block_tac [ intro_tac name; 
482              cases_tac 
483               ~where:("",0,(None,[],None)) 
484               ~what:("",0,Ast.Ident (name,None));
485               if name = "_clearme" then clear_tac ["_clearme"] else id_tac ]
486 ;;