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.
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_______________________________________________________________ *)
12 (* $Id: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *)
17 let debug_print s = if debug then prerr_endline (Lazy.force s) else ()
19 open Continuationals.Stack
21 module Ast = CicNotationPt
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;
32 match status.gstatus with
34 | ([], _, [], _) :: _ as stack ->
35 (* backward compatibility: do-nothing-dot *)
37 | (g, t, k, tag) :: s ->
38 match filter_open g, k with
40 (([ loc ], t, loc_tl @+ k, tag) :: s)
43 (([ loc ], t, k, tag) :: s)
44 | _ -> fail (lazy "can't use \".\" here")
46 { status with gstatus = new_gstatus }
49 let branch_tac status =
51 match status.gstatus with
53 | (g, t, k, tag) :: s ->
54 match init_pos g with (* TODO *)
55 | [] | [ _ ] -> fail (lazy "too few goals to branch");
57 ([ loc ], [], [], `BranchTag) :: (loc_tl, t, k, tag) :: s
59 { status with gstatus = new_gstatus }
62 let shift_tac status =
64 match status.gstatus with
65 | (g, t, k, `BranchTag) :: (g', t', k', tag) :: s ->
67 | [] -> fail (lazy "no more goals to shift")
69 (([ loc ], t @+ filter_open g @+ k, [],`BranchTag)
70 :: (loc_tl, t', k', tag) :: s))
71 | _ -> fail (lazy "can't shift goals here")
73 { status with gstatus = new_gstatus }
76 let pos_tac i_s status =
78 match status.gstatus with
80 | ([ loc ], t, [],`BranchTag) :: (g', t', k', tag) :: s
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")
87 { status with gstatus = new_gstatus }
90 let wildcard_tac status =
92 match status.gstatus with
94 | ([ loc ] , t, [], `BranchTag) :: (g', t', k', tag) :: s
96 (([loc] @+ g', t, [], `BranchTag) :: ([], t', k', tag) :: s)
97 | _ -> fail (lazy "can't use wildcard here")
99 { status with gstatus = new_gstatus }
102 let merge_tac status =
104 match status.gstatus with
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")
110 { status with gstatus = new_gstatus }
113 let focus_tac gs status =
115 match status.gstatus with
117 | s -> assert(gs <> []);
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
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)))
127 (zero_pos gs, [], [], `FocusTag) :: deep_close gs s
129 { status with gstatus = new_gstatus }
132 let unfocus_tac status =
134 match status.gstatus with
136 | ([], [], [], `FocusTag) :: s -> s
137 | _ -> fail (lazy "can't unfocus, some goals are still open")
139 { status with gstatus = new_gstatus }
142 let skip_tac status =
144 match status.gstatus with
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")
153 { status with gstatus = new_gstatus }
156 let block_tac l status =
157 List.fold_left (fun status tac -> tac status) status l
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)
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)
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)
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
188 let distribute_tac tac status =
189 match status.gstatus with
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 =
196 debug_print (lazy "no selected goals");
199 debug_print (lazy "inner eval tactical");
201 if List.exists ((=) (goal_of_loc loc)) gc then
204 match switch_of_loc loc with
205 | Closed _ -> fail (lazy "cannot apply to a Closed goal")
208 let go', gc' = compare_statuses ~past:s ~present:sn in
209 sn, ((go @+ [n]) @- gc') @+ go', gc @+ gc'
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)));
220 (zero_pos gon, t @~- gcn, k @~- gcn, tag) :: deep_close gcn s
222 { gstatus = stack; istatus = sn }
225 let atomic_tac htac = distribute_tac (exec htac) ;;
227 let exact_tac t = distribute_tac (fun status goal ->
228 let goalty = get_goalty status goal in
229 let status, t = disambiguate status t (Some goalty) (ctx_of goalty) in
230 instantiate status goal t)
233 let find_in_context name context =
234 let rec aux acc = function
235 | [] -> raise Not_found
236 | (hd,_) :: tl when hd = name -> acc
237 | _ :: tl -> aux (acc + 1) tl
242 let clear_tac names =
243 if names = [] then id_tac
245 distribute_tac (fun status goal ->
246 let goalty = get_goalty status goal in
250 try find_in_context name (ctx_of goalty)
252 fail (lazy ("hypothesis '" ^ name ^ "' not found")))
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 })
260 let generalize0_tac args =
261 if args = [] then id_tac
262 else exact_tac ("",0,Ast.Appl (Ast.Implicit :: args))
265 let select0_tac ~where:(wanted,hyps,where) ~job =
266 let found, postprocess =
268 | `Substexpand argsno -> mk_in_scope, mk_out_scope argsno
269 | `Collect l -> (fun s t -> l := t::!l; mk_in_scope s t), mk_out_scope 1
270 | `ChangeWith f -> f,(fun s t -> s, t)
272 distribute_tac (fun status goal ->
273 let goalty = get_goalty status goal in
275 match where with None -> NCic.Implicit `Term | Some where -> where
277 let status, newgoalctx =
279 (fun (name,d as entry) (status,ctx) ->
281 let path = List.assoc name hyps in
285 select_term status ~found ~postprocess (mk_cic_term ctx ty)
287 let status,ty = term_of_cic_term status ty ctx in
288 status,(name,NCic.Decl ty)::ctx
289 | NCic.Def (bo,ty) ->
291 select_term status ~found ~postprocess (mk_cic_term ctx bo)
293 let status,bo = term_of_cic_term status bo ctx in
294 status,(name,NCic.Def (bo,ty))::ctx
296 Not_found -> status, entry::ctx
297 ) (ctx_of goalty) (status,[])
299 let status, newgoalty =
300 select_term status ~found ~postprocess goalty (wanted,path) in
301 (* WARNING: the next two lines simply change the context of newgoalty
302 from the old to the new one. Otherwise mk_meta will do that herself,
303 calling relocate that calls delift. However, newgoalty is now
304 ?[out_scope] and thus the delift would trigger the special unification
305 case, which is wrong now :-( *)
306 let status,newgoalty = term_of_cic_term status newgoalty (ctx_of goalty) in
307 let newgoalty = mk_cic_term newgoalctx newgoalty in
309 let status, instance =
310 mk_meta status newgoalctx (`Decl newgoalty)
312 instantiate status goal instance)
315 let select_tac ~where ~job move_down_hyps =
316 let (wanted,hyps,where) = GrafiteDisambiguate.disambiguate_npattern where in
318 match where with None -> NCic.Implicit `Term | Some where -> where in
319 if not move_down_hyps then
320 select0_tac ~where:(wanted,hyps,Some path) ~job
324 (fun path (name,path_name) -> NCic.Prod ("_",path_name,path))
328 generalize0_tac (List.map (fun (name,_) -> Ast.Ident (name,None)) hyps);
329 select0_tac ~where:(wanted,[],Some path) ~job;
330 clear_tac (List.map fst hyps) ]
333 let generalize_tac ~where =
336 select_tac ~where ~job:(`Collect l) true;
337 print_tac true "ha selezionato?";
338 (fun s -> distribute_tac (fun status goal ->
339 let goalty = get_goalty status goal in
340 let status,canon,rest =
344 _,_,(None,_,_) -> fail (lazy "No term to generalize")
345 | txt,txtlen,(Some what,_,_) ->
347 disambiguate status (txt,txtlen,what) None (ctx_of goalty)
351 | he::tl -> status,he,tl in
354 (fun s t -> unify s (ctx_of goalty) canon t) status rest in
355 let status, canon = term_of_cic_term status canon (ctx_of goalty) in
356 instantiate status goal
357 (mk_cic_term (ctx_of goalty) (NCic.Appl [NCic.Implicit `Term ; canon ]))
361 let reduce_tac ~reduction ~where =
362 let change status t =
364 | `Normalize perform_delta ->
366 ?delta:(if perform_delta then None else Some max_int) (ctx_of t) t
367 | `Whd perform_delta ->
369 ?delta:(if perform_delta then None else Some max_int) (ctx_of t) t
371 let where = GrafiteDisambiguate.disambiguate_npattern where in
372 select0_tac ~where ~job:(`ChangeWith change)
375 let change_tac ~where ~with_what =
376 let change status t =
377 let status, ww = disambiguate status with_what None (ctx_of t) in
378 let status = unify status (ctx_of t) t ww in
381 let where = GrafiteDisambiguate.disambiguate_npattern where in
382 select0_tac ~where ~job:(`ChangeWith change)
385 let letin_tac ~where ~what:(_,_,w) name =
387 select_tac ~where ~job:(`Substexpand 1) true;
388 exact_tac ("",0,Ast.LetIn((Ast.Ident (name,None),None),w,Ast.Implicit));
392 let apply_tac = exact_tac;;
398 lefts: NCic.term list;
399 rights: NCic.term list;
400 reference: NReference.reference;
404 let analyze_indty_tac ~what indtyref = distribute_tac (fun status goal ->
405 let goalty = get_goalty status goal in
406 let status, what = disambiguate status what None (ctx_of goalty) in
407 let status, ty_what = typeof status (ctx_of what) what in
408 let status, (r,consno,lefts,rights) = analyse_indty status ty_what in
409 let leftno = List.length rights in
410 let rightno = List.length rights in
412 rightno = rightno; leftno = leftno; consno = consno;
413 lefts = lefts; rights = rights; reference = r;
415 exec id_tac status goal)
418 let elim_tac ~what ~where =
419 let indtyinfo = ref None in
420 let sort = ref None in
421 let compute_goal_sort_tac = distribute_tac (fun status goal ->
422 let goalty = get_goalty status goal in
423 let status, goalsort = typeof status (ctx_of goalty) goalty in
424 sort := Some goalsort;
425 exec id_tac status goal)
427 atomic_tac (block_tac [
428 analyze_indty_tac ~what indtyinfo;
430 ~where ~job:(`Substexpand ((HExtlib.unopt !indtyinfo).rightno+1)) true s);
431 compute_goal_sort_tac;
433 let sort = HExtlib.unopt !sort in
434 let ity = HExtlib.unopt !indtyinfo in
435 let NReference.Ref (uri, _) = ity.reference in
436 let istatus, sort = term_of_cic_term status.istatus sort (ctx_of sort) in
437 let status = { status with istatus = istatus } in
438 let name = NUri.name_of_uri uri ^
440 | NCic.Sort NCic.Prop -> "_ind"
441 | NCic.Sort _ -> "_rect"
445 HExtlib.mk_list Ast.Implicit (ity.leftno+1+ ity.consno + ity.rightno) in
448 Ast.Appl(Ast.Ident(name,None)::holes @ [ w ])
450 exact_tac ("",0,eliminator) status) ])
453 let rewrite_tac ~dir ~what:(_,_,what) ~where =
455 match dir with `LeftToRight -> "eq_elim_r" | `RightToLeft -> "eq_ind"
458 [ select_tac ~where ~job:(`Substexpand 1) true;
461 Ast.Appl(Ast.Ident(name,None)::HExtlib.mk_list Ast.Implicit 5 @
468 ("",0,(Ast.Binder (`Lambda,
469 (Ast.Ident (name,None),None),Ast.Implicit)));
470 if name = "_" then clear_tac [name] else id_tac ]
473 let cases ~what status goal =
474 let gty = get_goalty status goal in
475 let status, what = disambiguate status what None (ctx_of gty) in
476 let status, ty = typeof status (ctx_of what) what in
477 let status, (ref, consno, _, _) = analyse_indty status ty in
478 let status, what = term_of_cic_term status what (ctx_of gty) in
480 NCic.Match (ref,NCic.Implicit `Term, what,
481 HExtlib.mk_list (NCic.Implicit `Term) consno)
483 let ctx = ctx_of gty in
484 let status,t,ty = refine status ctx (mk_cic_term ctx t) (Some gty) in
485 instantiate status goal t
488 let cases_tac ~what ~where =
489 let indtyinfo = ref None in
492 analyze_indty_tac ~what indtyinfo;
494 ~where ~job:(`Substexpand ((HExtlib.unopt !indtyinfo).rightno+1))true s);
495 distribute_tac (cases ~what) ])
499 let name = if name = "_" then "_clearme" else name in
500 block_tac [ intro_tac name;
502 ~where:("",0,(None,[],None))
503 ~what:("",0,Ast.Ident (name,None));
504 if name = "_clearme" then clear_tac ["_clearme"] else id_tac ]
507 let assert0_tac (hyps,concl) = distribute_tac (fun status goal ->
508 let gty = get_goalty status goal in
509 let eq status ctx t1 t2 =
510 let status,t1 = disambiguate status t1 None ctx in
511 let status,t1 = apply_subst status ctx t1 in
512 let status,t1 = term_of_cic_term status t1 ctx in
513 let t2 = mk_cic_term ctx t2 in
514 let status,t2 = apply_subst status ctx t2 in
515 let status,t2 = term_of_cic_term status t2 ctx in
516 prerr_endline ("COMPARING: " ^ NCicPp.ppterm ~subst:[] ~metasenv:[] ~context:ctx t1 ^ " vs " ^ NCicPp.ppterm ~subst:[] ~metasenv:[] ~context:ctx t2);
520 let status,gty' = term_of_cic_term status gty (ctx_of gty) in
521 let status = eq status (ctx_of gty) concl gty' in
524 (fun (id1,e1) ((id2,e2) as item) (status,ctx) ->
525 assert (id1=id2 || (prerr_endline (id1 ^ " vs " ^ id2); false));
527 `Decl t1, NCic.Decl t2 ->
528 let status = eq status ctx t1 t2 in
530 | `Def (b1,t1), NCic.Def (b2,t2) ->
531 let status = eq status ctx t1 t2 in
532 let status = eq status ctx b1 b2 in
535 ) hyps (ctx_of gty) (status,[])
537 exec id_tac status goal)
540 let assert_tac seqs status =
541 match status.gstatus with
544 assert (List.length g = List.length seqs);
547 | [seq] -> assert0_tac seq
551 HExtlib.list_concat ~sep:[shift_tac]
552 (List.map (fun seq -> [assert0_tac seq]) seqs)@