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#stack 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#set_stack gstatus
49 let branch_tac ?(force=false) status =
51 match status#stack with
53 | (g, t, k, tag) :: s ->
54 match init_pos g with (* TODO *)
55 | [] -> fail (lazy "empty goals")
56 | [_] when (not force) -> fail (lazy "too few goals to branch")
58 ([ loc ], [], [], `BranchTag) :: (loc_tl, t, k, tag) :: s
60 status#set_stack gstatus
63 let shift_tac status =
65 match status#stack with
66 | (g, t, k, `BranchTag) :: (g', t', k', tag) :: s ->
68 | [] -> fail (lazy "no more goals to shift")
70 (([ loc ], t @+ filter_open g @+ k, [],`BranchTag)
71 :: (loc_tl, t', k', tag) :: s))
72 | _ -> fail (lazy "can't shift goals here")
74 status#set_stack gstatus
77 let pos_tac i_s status =
79 match status#stack with
81 | ([ loc ], t, [],`BranchTag) :: (g', t', k', tag) :: s
83 let l_js = List.filter (fun (i, _) -> List.mem i i_s) ([loc] @+ g') in
84 ((l_js, t , [],`BranchTag)
85 :: (([ loc ] @+ g') @- l_js, t', k', tag) :: s)
86 | _ -> fail (lazy "can't use relative positioning here")
88 status#set_stack gstatus
91 let case_tac lab status =
93 match status#stack with
95 | ([ loc ], t, [],`BranchTag) :: (g', t', k', tag) :: s
100 let _,_,metasenv,_,_ = status#obj in
101 match NCicUtils.lookup_meta (goal_of_loc curloc) metasenv with
102 attrs,_,_ when List.mem (`Name lab) attrs -> true
103 | _ -> false) ([loc] @+ g') in
104 ((l_js, t , [],`BranchTag)
105 :: (([ loc ] @+ g') @- l_js, t', k', tag) :: s)
106 | _ -> fail (lazy "can't use relative positioning here")
108 status#set_stack gstatus
111 let wildcard_tac status =
113 match status#stack with
115 | ([ loc ] , t, [], `BranchTag) :: (g', t', k', tag) :: s
117 (([loc] @+ g', t, [], `BranchTag) :: ([], t', k', tag) :: s)
118 | _ -> fail (lazy "can't use wildcard here")
120 status#set_stack gstatus
123 let merge_tac status =
125 match status#stack with
127 | (g, t, k,`BranchTag) :: (g', t', k', tag) :: s ->
128 ((t @+ filter_open g @+ g' @+ k, t', k', tag) :: s)
129 | _ -> fail (lazy "can't merge goals here")
131 status#set_stack gstatus
134 let focus_tac gs status =
136 match status#stack with
138 | s -> assert(gs <> []);
140 let add_l acc _ _ l = if is_open l then l :: acc else acc in
141 fold ~env:add_l ~cont:add_l ~todo:add_l [] s
145 if not (List.exists (fun l -> goal_of_loc l = g) stack_locs) then
146 fail (lazy (sprintf "goal %d not found (or closed)" g)))
148 (zero_pos gs, [], [], `FocusTag) :: deep_close gs s
150 status#set_stack gstatus
153 let unfocus_tac status =
155 match status#stack with
157 | (g, [], [], `FocusTag) :: s when filter_open g = [] -> s
158 | _ as s -> fail (lazy ("can't unfocus, some goals are still open:\n"^
159 Continuationals.Stack.pp s))
161 status#set_stack gstatus
164 let skip_tac status =
166 match status#stack with
168 | (gl, t, k, tag) :: s ->
169 let gl = List.map switch_of_loc gl in
170 if List.exists (function Open _ -> true | Closed _ -> false) gl then
171 fail (lazy "cannot skip an open goal")
175 status#set_stack gstatus
178 let block_tac l status =
179 List.fold_left (fun status tac -> tac status) status l
183 let compare_statuses ~past ~present =
184 let _,_,past,_,_ = past#obj in
185 let _,_,present,_,_ = present#obj in
186 List.map fst (List.filter (fun (i,_) -> not(List.mem_assoc i past)) present),
187 List.map fst (List.filter (fun (i,_) -> not (List.mem_assoc i present)) past)
192 (* Exec and distribute_tac form a retraction pair:
193 1) exec (distribute_tac low_tac) (s,i) = low_tac (s,i)
194 2) tac [s]::G = G1::...::Gn::G' && G' is G with some goals closed =>
195 distribute_tac (exec tac) [s]::G = (G1@...Gn)::G'
196 3) tac G = distribute_tac (exec tac) G if
197 tac = distribute_tac lowtac
198 4) atomic_tac t === distribute_tac (exec t)
200 Note that executing an high tactic on a set of goals may be stronger
201 than executing the same tactic on those goals, but once at a time
202 (e.g. the tactic could perform a global analysis of the set of goals)
205 let exec tac (low_status : #lowtac_status) g =
206 let stack = [ [0,Open g], [], [], `NoTag ] in
208 (new NTacStatus.status low_status#obj stack)#set_estatus low_status
210 let status = tac status in
211 (low_status#set_estatus status)#set_obj status#obj
214 let distribute_tac tac (status : #tac_status) =
215 match status#stack with
217 | (g, t, k, tag) :: s ->
218 debug_print (lazy ("context length " ^string_of_int (List.length g)));
219 let rec aux s go gc =
222 debug_print (lazy "no selected goals");
225 debug_print (lazy "inner eval tactical");
227 if List.exists ((=) (goal_of_loc loc)) gc then
230 match switch_of_loc loc with
231 | Closed _ -> fail (lazy "cannot apply to a Closed goal")
234 let go', gc' = compare_statuses ~past:s ~present:sn in
235 sn, ((go @+ [n]) @- gc') @+ go', gc @+ gc'
239 let s0 = (new NTacStatus.status status#obj ())#set_estatus status in
240 let s0, go0, gc0 = s0, [], [] in
241 let sn, gon, gcn = aux s0 go0 gc0 g in
242 debug_print (lazy ("opened: "
243 ^ String.concat " " (List.map string_of_int gon)));
244 debug_print (lazy ("closed: "
245 ^ String.concat " " (List.map string_of_int gcn)));
247 (zero_pos gon, t @~- gcn, k @~- gcn, tag) :: deep_close gcn s
249 ((status#set_stack stack)#set_obj(sn:>lowtac_status)#obj)#set_estatus sn
252 let atomic_tac htac : #tac_status as 'a -> 'a = distribute_tac (exec htac) ;;
255 let rec repeat t (status : #tac_status as 'a) : 'a =
256 try repeat t (t status)
257 with NTacStatus.Error _ -> status
259 atomic_tac (repeat t) s
263 let try_tac tac status =
267 with NTacStatus.Error _ ->
270 atomic_tac try_tac status
273 let first_tac tacl status =
276 (fun tac _ -> try Some (tac status) with NTacStatus.Error _ -> None) tacl
279 | None -> fail (lazy "No tactics left")
283 let exact_tac t : 's tactic = distribute_tac (fun status goal ->
284 instantiate_with_ast status goal t)
287 let assumption_tac status = distribute_tac (fun status goal ->
288 let gty = get_goalty status goal in
289 let context = ctx_of gty in
292 (List.map (fun (name,_) -> exact_tac ("",0,(Ast.Ident (name,None))))
295 exec htac status goal) status
298 let find_in_context name context =
299 let rec aux acc = function
300 | [] -> raise Not_found
301 | (hd,_) :: tl when hd = name -> acc
302 | _ :: tl -> aux (acc + 1) tl
307 let clear_tac names =
308 if names = [] then id_tac
310 distribute_tac (fun status goal ->
311 let goalty = get_goalty status goal in
315 try find_in_context name (ctx_of goalty)
317 fail (lazy ("hypothesis '" ^ name ^ "' not found")))
320 let n,h,metasenv,subst,o = status#obj in
321 let metasenv,subst,_,_ = NCicMetaSubst.restrict metasenv subst goal js in
322 status#set_obj (n,h,metasenv,subst,o))
325 let generalize0_tac args =
326 if args = [] then id_tac
327 else exact_tac ("",0,Ast.Appl (Ast.Implicit `JustOne :: args))
330 let select0_tac ~where:(wanted,hyps,where) ~job =
331 let found, postprocess =
333 | `Substexpand argsno -> mk_in_scope, mk_out_scope argsno
334 | `Collect l -> (fun s t -> l := t::!l; mk_in_scope s t), mk_out_scope 1
335 | `ChangeWith f -> f,(fun s t -> s, t)
337 distribute_tac (fun status goal ->
338 let goalty = get_goalty status goal in
340 match where with None -> NCic.Implicit `Term | Some where -> where
342 let status, newgoalctx =
344 (fun (name,d as entry) (status,ctx) ->
346 let path = List.assoc name hyps in
350 select_term status ~found ~postprocess (mk_cic_term ctx ty)
352 let status,ty = term_of_cic_term status ty ctx in
353 status,(name,NCic.Decl ty)::ctx
354 | NCic.Def (bo,ty) ->
356 select_term status ~found ~postprocess (mk_cic_term ctx bo)
358 let status,bo = term_of_cic_term status bo ctx in
359 status,(name,NCic.Def (bo,ty))::ctx
361 Not_found -> status, entry::ctx
362 ) (ctx_of goalty) (status,[])
364 let status, newgoalty =
365 select_term status ~found ~postprocess goalty (wanted,path) in
366 (* WARNING: the next two lines simply change the context of newgoalty
367 from the old to the new one. Otherwise mk_meta will do that herself,
368 calling relocate that calls delift. However, newgoalty is now
369 ?[out_scope] and thus the delift would trigger the special unification
370 case, which is wrong now :-( *)
371 let status,newgoalty = term_of_cic_term status newgoalty (ctx_of goalty) in
372 let newgoalty = mk_cic_term newgoalctx newgoalty in
374 let status, instance =
375 mk_meta status newgoalctx (`Decl newgoalty) `IsTerm
377 instantiate ~refine:false status goal instance)
380 let select_tac ~where ~job move_down_hyps =
381 let (wanted,hyps,where) = GrafiteDisambiguate.disambiguate_npattern where in
383 match where with None -> NCic.Implicit `Term | Some where -> where in
384 if not move_down_hyps then
385 select0_tac ~where:(wanted,hyps,Some path) ~job
389 (fun path (name,path_name) -> NCic.Prod ("_",path_name,path))
393 generalize0_tac (List.map (fun (name,_) -> Ast.Ident (name,None)) hyps);
394 select0_tac ~where:(wanted,[],Some path) ~job;
395 clear_tac (List.map fst hyps) ]
398 let generalize_tac ~where =
401 select_tac ~where ~job:(`Collect l) true;
402 (fun s -> distribute_tac (fun status goal ->
403 let goalty = get_goalty status goal in
404 let status,canon,rest =
408 _,_,(None,_,_) -> fail (lazy "No term to generalize")
409 | txt,txtlen,(Some what,_,_) ->
411 disambiguate status (ctx_of goalty) (txt,txtlen,what) None
415 | he::tl -> status,he,tl in
418 (fun s t -> unify s (ctx_of goalty) canon t) status rest in
419 let status, canon = term_of_cic_term status canon (ctx_of goalty) in
420 instantiate status goal
421 (mk_cic_term (ctx_of goalty) (NCic.Appl [NCic.Implicit `Term ; canon ]))
426 atomic_tac (block_tac [
427 exact_tac ("",0, Ast.Appl [Ast.Implicit `JustOne; Ast.Implicit `JustOne]);
429 pos_tac [3]; exact_tac t;
430 shift_tac; pos_tac [2]; skip_tac;
434 let lapply_tac (s,n,t) =
435 exact_tac (s,n, Ast.Appl [Ast.Implicit `JustOne; t])
438 let reduce_tac ~reduction ~where =
439 let change status t =
441 | `Normalize perform_delta ->
443 ?delta:(if perform_delta then None else Some max_int) (ctx_of t) t
444 | `Whd perform_delta ->
446 ?delta:(if perform_delta then None else Some max_int) (ctx_of t) t
448 let where = GrafiteDisambiguate.disambiguate_npattern where in
449 select0_tac ~where ~job:(`ChangeWith change)
452 let change_tac ~where ~with_what =
453 let change status t =
454 let status, ww = disambiguate status (ctx_of t) with_what None in
455 let status = unify status (ctx_of t) t ww in
458 let where = GrafiteDisambiguate.disambiguate_npattern where in
459 select0_tac ~where ~job:(`ChangeWith change)
462 let letin_tac ~where ~what:(_,_,w) name =
464 select_tac ~where ~job:(`Substexpand 1) true;
466 ("",0,Ast.LetIn((Ast.Ident (name,None),None),w,Ast.Implicit `JustOne));
470 let apply_tac (s,n,t) =
471 let t = Ast.Appl [t; Ast.Implicit `Vector] in
479 reference: NReference.reference;
483 let ref_of_indtyinfo iti = iti.reference;;
485 let analyze_indty_tac ~what indtyref =
486 distribute_tac (fun (status as orig_status) goal ->
487 let goalty = get_goalty status goal in
488 let status, what = disambiguate status (ctx_of goalty) what None in
489 let status, ty_what = typeof status (ctx_of what) what in
490 let status, (r,consno,lefts,rights) = analyse_indty status ty_what in
491 let leftno = List.length lefts in
492 let rightno = List.length rights in
494 rightno = rightno; leftno = leftno; consno = consno; reference = r;
496 exec id_tac orig_status goal)
499 let sort_of_goal_tac sortref = distribute_tac (fun status goal ->
500 let goalty = get_goalty status goal in
501 let status,sort = typeof status (ctx_of goalty) goalty in
502 let status, sort = fix_sorts status sort in
503 let status, sort = term_of_cic_term status sort (ctx_of goalty) in
508 let elim_tac ~what:(txt,len,what) ~where =
509 let what = txt, len, Ast.Appl [what; Ast.Implicit `Vector] in
510 let indtyinfo = ref None in
511 let sort = ref (NCic.Rel 1) in
512 atomic_tac (block_tac [
513 analyze_indty_tac ~what indtyinfo;
515 ~where ~job:(`Substexpand ((HExtlib.unopt !indtyinfo).rightno+1)) true s);
516 sort_of_goal_tac sort;
518 let ity = HExtlib.unopt !indtyinfo in
519 let NReference.Ref (uri, _) = ity.reference in
521 NUri.name_of_uri uri ^ "_" ^
522 snd (NCicElim.ast_of_sort
523 (match !sort with NCic.Sort x -> x | _ -> assert false))
527 Ast.Appl [ Ast.Ident (name,None) ; Ast.Implicit `Vector ; w ]
529 exact_tac ("",0,eliminator) status) ])
532 let rewrite_tac ~dir ~what:(_,_,what) ~where status =
533 let sortref = ref (NCic.Rel 1) in
534 let status = sort_of_goal_tac sortref status in
535 let suffix = "_" ^ snd (NCicElim.ast_of_sort
536 (match !sortref with NCic.Sort x -> x | _ -> assert false))
540 `LeftToRight -> "eq" ^ suffix ^ "_r"
541 | `RightToLeft -> "eq" ^ suffix
543 let what = Ast.Appl [what; Ast.Implicit `Vector] in
545 [ select_tac ~where ~job:(`Substexpand 2) true;
548 Ast.Appl(Ast.Ident(name,None)::HExtlib.mk_list (Ast.Implicit `JustOne) 5@
555 ("",0,(Ast.Binder (`Lambda,
556 (Ast.Ident (name,None),None),Ast.Implicit `JustOne)));
557 if name = "_" then clear_tac [name] else id_tac ]
560 let name_counter = ref 0;;
561 let intros_tac ?names_ref names s =
562 let names_ref, prefix =
563 match names_ref with | None -> ref [], "__" | Some r -> r, "H"
569 (* TODO: generate better names *)
570 let name = prefix ^ string_of_int !name_counter in
571 let s = intro_tac name s in
572 names_ref := !names_ref @ [name];
576 block_tac (List.map intro_tac names) s
579 let cases ~what status goal =
580 let gty = get_goalty status goal in
581 let status, what = disambiguate status (ctx_of gty) what None in
582 let status, ty = typeof status (ctx_of what) what in
583 let status, (ref, consno, _, _) = analyse_indty status ty in
584 let status, what = term_of_cic_term status what (ctx_of gty) in
586 NCic.Match (ref,NCic.Implicit `Term, what,
587 HExtlib.mk_list (NCic.Implicit `Term) consno)
589 instantiate status goal (mk_cic_term (ctx_of gty) t)
592 let cases_tac ~what:(txt,len,what) ~where =
593 let what = txt, len, Ast.Appl [what; Ast.Implicit `Vector] in
594 let indtyinfo = ref None in
597 analyze_indty_tac ~what indtyinfo;
599 ~where ~job:(`Substexpand ((HExtlib.unopt !indtyinfo).rightno+1))true s);
600 distribute_tac (cases ~what) ])
604 let name = if name = "_" then "_clearme" else name in
605 block_tac [ intro_tac name;
607 ~where:("",0,(None,[],None))
608 ~what:("",0,Ast.Ident (name,None));
609 if name = "_clearme" then clear_tac ["_clearme"] else id_tac ]
612 let constructor_tac ?(num=1) ~args = distribute_tac (fun status goal ->
613 if num < 1 then fail (lazy "constructor numbers begin with 1");
614 let gty = get_goalty status goal in
615 let status, (r,_,_,_) = analyse_indty status gty in
616 let ref = NReference.mk_constructor num r in
618 if args = [] then Ast.NRef ref else
619 Ast.Appl (HExtlib.list_concat ~sep:[Ast.Implicit `Vector]
620 ([Ast.NRef ref] :: List.map (fun _,_,x -> [x]) args))
622 exec (apply_tac ("",0,t)) status goal)
625 let assert0_tac (hyps,concl) = distribute_tac (fun status goal ->
626 let gty = get_goalty status goal in
627 let eq status ctx t1 t2 =
628 let status,t1 = disambiguate status ctx t1 None in
629 let status,t1 = apply_subst status ctx t1 in
630 let status,t1 = term_of_cic_term status t1 ctx in
631 let t2 = mk_cic_term ctx t2 in
632 let status,t2 = apply_subst status ctx t2 in
633 let status,t2 = term_of_cic_term status t2 ctx in
634 prerr_endline ("COMPARING: " ^ NCicPp.ppterm ~subst:[] ~metasenv:[] ~context:ctx t1 ^ " vs " ^ NCicPp.ppterm ~subst:[] ~metasenv:[] ~context:ctx t2);
638 let status,gty' = term_of_cic_term status gty (ctx_of gty) in
639 let status = eq status (ctx_of gty) concl gty' in
642 (fun (id1,e1) ((id2,e2) as item) (status,ctx) ->
643 assert (id1=id2 || (prerr_endline (id1 ^ " vs " ^ id2); false));
645 `Decl t1, NCic.Decl t2 ->
646 let status = eq status ctx t1 t2 in
648 | `Def (b1,t1), NCic.Def (b2,t2) ->
649 let status = eq status ctx t1 t2 in
650 let status = eq status ctx b1 b2 in
653 ) hyps (ctx_of gty) (status,[])
655 exec id_tac status goal)
658 let assert_tac seqs status =
659 match status#stack with
662 assert (List.length g = List.length seqs);
665 | [seq] -> assert0_tac seq
668 ((branch_tac ~force:false)::
669 HExtlib.list_concat ~sep:[shift_tac]
670 (List.map (fun seq -> [assert0_tac seq]) seqs)@
675 let inversion_tac ~what:(txt,len,what) ~where =
676 let what = txt, len, Ast.Appl [what; Ast.Implicit `Vector] in
677 let indtyinfo = ref None in
678 let sort = ref (NCic.Rel 1) in
679 atomic_tac (block_tac [
680 analyze_indty_tac ~what indtyinfo;
682 ~where ~job:(`Substexpand ((HExtlib.unopt !indtyinfo).rightno+1)) true s);
683 sort_of_goal_tac sort;
685 let ity = HExtlib.unopt !indtyinfo in
686 let NReference.Ref (uri, _) = ity.reference in
688 NUri.name_of_uri uri ^ "_inv_" ^
689 snd (NCicElim.ast_of_sort
690 (match !sort with NCic.Sort x -> x | _ -> assert false))
694 Ast.Appl [ Ast.Ident (name,None) ; Ast.Implicit `Vector ; w ]
696 exact_tac ("",0,eliminator) status) ])