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;;
27 match status.gstatus with
29 | ([], _, [], _) :: _ as stack ->
30 (* backward compatibility: do-nothing-dot *)
32 | (g, t, k, tag) :: s ->
33 match filter_open g, k with
35 (([ loc ], t, loc_tl @+ k, tag) :: s)
38 (([ loc ], t, k, tag) :: s)
39 | _ -> fail (lazy "can't use \".\" here")
41 { status with gstatus = new_gstatus }
44 let branch_tac status =
46 match status.gstatus with
48 | (g, t, k, tag) :: s ->
49 match init_pos g with (* TODO *)
50 | [] | [ _ ] -> fail (lazy "too few goals to branch");
52 ([ loc ], [], [], `BranchTag) :: (loc_tl, t, k, tag) :: s
54 { status with gstatus = new_gstatus }
57 let shift_tac status =
59 match status.gstatus with
60 | (g, t, k, `BranchTag) :: (g', t', k', tag) :: s ->
62 | [] -> fail (lazy "no more goals to shift")
64 (([ loc ], t @+ filter_open g @+ k, [],`BranchTag)
65 :: (loc_tl, t', k', tag) :: s))
66 | _ -> fail (lazy "can't shift goals here")
68 { status with gstatus = new_gstatus }
71 let pos_tac i_s status =
73 match status.gstatus with
75 | ([ loc ], t, [],`BranchTag) :: (g', t', k', tag) :: s
77 let l_js = List.filter (fun (i, _) -> List.mem i i_s) ([loc] @+ g') in
78 ((l_js, t , [],`BranchTag)
79 :: (([ loc ] @+ g') @- l_js, t', k', tag) :: s)
80 | _ -> fail (lazy "can't use relative positioning here")
82 { status with gstatus = new_gstatus }
85 let wildcard_tac status =
87 match status.gstatus with
89 | ([ loc ] , t, [], `BranchTag) :: (g', t', k', tag) :: s
91 (([loc] @+ g', t, [], `BranchTag) :: ([], t', k', tag) :: s)
92 | _ -> fail (lazy "can't use wildcard here")
94 { status with gstatus = new_gstatus }
97 let merge_tac status =
99 match status.gstatus with
101 | (g, t, k,`BranchTag) :: (g', t', k', tag) :: s ->
102 ((t @+ filter_open g @+ g' @+ k, t', k', tag) :: s)
103 | _ -> fail (lazy "can't merge goals here")
105 { status with gstatus = new_gstatus }
108 let focus_tac gs status =
110 match status.gstatus with
112 | s -> assert(gs <> []);
114 let add_l acc _ _ l = if is_open l then l :: acc else acc in
115 fold ~env:add_l ~cont:add_l ~todo:add_l [] s
119 if not (List.exists (fun l -> goal_of_loc l = g) stack_locs) then
120 fail (lazy (sprintf "goal %d not found (or closed)" g)))
122 (zero_pos gs, [], [], `FocusTag) :: deep_close gs s
124 { status with gstatus = new_gstatus }
127 let unfocus_tac status =
129 match status.gstatus with
131 | ([], [], [], `FocusTag) :: s -> s
132 | _ -> fail (lazy "can't unfocus, some goals are still open")
134 { status with gstatus = new_gstatus }
137 let skip_tac status =
139 match status.gstatus with
141 | (gl, t, k, tag) :: s ->
142 let gl = List.map switch_of_loc gl in
143 if List.exists (function Open _ -> true | Closed _ -> false) gl then
144 fail (lazy "cannot skip an open goal")
148 { status with gstatus = new_gstatus }
151 let block_tac l status =
152 List.fold_left (fun status tac -> tac status) status l
155 let compare_statuses ~past ~present =
156 let _,_,past,_,_ = past.pstatus in
157 let _,_,present,_,_ = present.pstatus in
158 List.map fst (List.filter (fun (i,_) -> not (List.mem_assoc i past)) present),
159 List.map fst (List.filter (fun (i,_) -> not (List.mem_assoc i present)) past)
164 (* Exec and distribute_tac form a retraction pair:
165 1) exec (distribute_tac low_tac) (s,i) = low_tac (s,i)
166 2) tac [s]::G = G1::...::Gn::G' && G' is G with some goals closed =>
167 distribute_tac (exec tac) [s]::G = (G1@...Gn)::G'
168 3) tac G = distribute_tac (exec tac) G if
169 tac = distribute_tac lowtac
171 Note that executing an high tactic on a set of goals may be stronger
172 than executing the same tactic on those goals, but once at a time
173 (e.g. the tactic could perform a global analysis of the set of goals)
176 let exec tac low_status g =
177 let stack = [ [0,Open g], [], [], `NoTag ] in
178 let status = tac { gstatus = stack ; istatus = low_status } in
182 let distribute_tac tac status =
183 match status.gstatus with
185 | (g, t, k, tag) :: s ->
186 debug_print (lazy ("context length " ^string_of_int (List.length g)));
187 let rec aux s go gc =
191 debug_print (lazy "inner eval tactical");
193 if List.exists ((=) (goal_of_loc loc)) gc then
196 match switch_of_loc loc with
197 | Closed _ -> fail (lazy "cannot apply to a Closed goal")
200 let go', gc' = compare_statuses ~past:s ~present:sn in
201 sn, (go @- gc') @+ go', gc @+ gc'
205 let s0, go0, gc0 = status.istatus, [], [] in
206 let sn, gon, gcn = aux s0 go0 gc0 g in
207 debug_print (lazy ("opened: "
208 ^ String.concat " " (List.map string_of_int gon)));
209 debug_print (lazy ("closed: "
210 ^ String.concat " " (List.map string_of_int gcn)));
212 (zero_pos gon, t @~- gcn, k @~- gcn, tag) :: deep_close gcn s
214 { gstatus = stack; istatus = sn }
217 let exact t status goal =
218 let goalty = get_goalty status goal in
219 let status, t = disambiguate status t (Some goalty) (ctx_of goalty) in
220 instantiate status goal t
223 let exact_tac t = distribute_tac (exact t) ;;
225 let find_in_context name context =
226 let rec aux acc = function
227 | [] -> raise Not_found
228 | (hd,_) :: tl when hd = name -> acc
229 | _ :: tl -> aux (acc + 1) tl
234 let clear names status goal =
235 let goalty = get_goalty status goal in
239 try find_in_context name (ctx_of goalty)
241 fail (lazy ("hypothesis '" ^ name ^ "' not found")))
244 let n,h,metasenv,subst,o = status.pstatus in
245 let metasenv,subst,_ = NCicMetaSubst.restrict metasenv subst goal js in
246 { status with pstatus = n,h,metasenv,subst,o }
249 let clear_tac names =
250 if names = [] then id_tac else distribute_tac (clear names)
253 let generalize0_tac args =
254 if args = [] then id_tac
255 else exact_tac ("",0,Ast.Appl (Ast.Implicit :: args))
258 let select ~where:(wanted,_,where) status goal =
259 let goalty = get_goalty status goal in
261 match where with None -> NCic.Implicit `Term | Some where -> where
263 let status, newgoalty = select_term status goalty (wanted,path) in
264 let status, instance =
265 mk_meta status (ctx_of newgoalty) (`Decl newgoalty)
267 instantiate status goal instance
270 let select0_tac ~where = distribute_tac (select ~where) ;;
272 let select_tac ~where move_down_hyps =
273 let (wanted,hyps,where) = GrafiteDisambiguate.disambiguate_npattern where in
275 match where with None -> NCic.Implicit `Term | Some where -> where in
276 if not move_down_hyps then
277 select0_tac ~where:(wanted,hyps,Some path)
281 (fun path (name,path_name) -> NCic.Prod ("_",path_name,path))
285 generalize0_tac (List.map (fun (name,_) -> Ast.Ident (name,None)) hyps);
286 select0_tac ~where:(wanted,[],Some path);
287 clear_tac (List.map fst hyps) ]
291 let generalize_tac ~where =
292 block_tac [ select_tac ~where true ; generalize0_tac ???? ]
298 let n,h,metasenv,subst,o = status.pstatus in
301 (function (_,(Some tag,_,_,_)) ->
302 tag <> NCicMetaSubst.in_scope_tag &&
303 not (NCicMetaSubst.is_out_scope_tag tag)
309 (function (_,(Some tag,_,_,_)) ->
310 tag = NCicMetaSubst.in_scope_tag | _ -> assert false)
313 let metasenv = List.map (fun (i,(_,c,_,t)) -> i,(None,c,t)) in_m @ metasenv in
314 let in_m = List.map fst in_m in
315 let out_m = match out_m with [i] -> i | _ -> assert false in
316 { status with pstatus = n,h,metasenv,subst,o }, in_m, out_m
319 let change ~where ~with_what status goal =
320 let goalty = get_goalty status goal in
321 let (wanted,_,where) = GrafiteDisambiguate.disambiguate_npattern where in
323 match where with None -> NCic.Implicit `Term | Some where -> where
325 let status, newgoalty = select_term status goalty (wanted,path) in
326 let status, in_scope, out_scope = reopen status in
327 let status = List.fold_left (exact with_what) status in_scope in
329 let j,(n,cctx,bo,_) = out_scope in
330 let _ = typeof status (ctx_of goalty) (Obj.magic (n,cctx,bo)) in
332 let n,h,metasenv,subst,o = status.pstatus in
333 let subst = out_scope :: subst in
334 let status = { status with pstatus = n,h,metasenv,subst,o } in
336 let status, instance =
337 mk_meta status (ctx_of newgoalty) (`Decl newgoalty)
339 instantiate status goal instance
342 let apply t status goal = exact t status goal;;
344 let apply_tac t = distribute_tac (apply t) ;;
345 let change_tac ~where ~with_what = distribute_tac (change ~where ~with_what) ;;
347 let elim_tac ~what ~where status =
349 [ select_tac ~where true;
350 distribute_tac (fun status goal ->
351 let goalty = get_goalty status goal in
352 let goalsort = typeof status (ctx_of goalty) goalty in
355 disambiguate status what None (ctx_of goalty) in
356 let ty_what = typeof status (ctx_of what) what in
357 let NReference.Ref (uri,_),consno,lefts,rights =
358 analyse_indty status ty_what in
359 let name = NUri.name_of_uri uri ^
360 match term_of_cic_term goalsort (ctx_of goalsort) with
361 NCic.Sort NCic.Prop -> "_ind"
362 | NCic.Sort _ -> "_rect"
363 | _ -> assert false in
364 let leftno = List.length rights in
365 let rightno = List.length rights in
366 let holes=HExtlib.mk_list Ast.Implicit (leftno + 1 + consno + rightno) in
368 Ast.Appl(Ast.Ident(name,None)::holes @ [ w ])
370 exec (apply_tac ("",0,eliminator)) status goal) ]
377 ("",0,(Ast.Binder (`Lambda,
378 (Ast.Ident (name,None),None),Ast.Implicit)));
379 if name = "_" then clear_tac [name] else id_tac ]
382 let cases ~what status goal =
383 let gty = get_goalty status goal in
384 let status, what = disambiguate status what None (ctx_of gty) in
385 let ty = typeof status (ctx_of what) what in
386 let ref, consno, _, _ = analyse_indty status ty in
388 NCic.Match (ref,NCic.Implicit `Term, term_of_cic_term what (ctx_of gty),
389 HExtlib.mk_list (NCic.Implicit `Term) consno)
391 let ctx = ctx_of gty in
392 let status,t,ty = refine status ctx (mk_cic_term ctx t) (Some gty) in
393 instantiate status goal t
396 let cases_tac ~what ~where =
397 block_tac [ select_tac ~where true ; distribute_tac (cases ~what) ]
401 let name = if name = "_" then "_clearme" else name in
402 block_tac [ intro_tac name;
404 ~where:("",0,(None,[],None))
405 ~what:("",0,Ast.Ident (name,None));
406 if name = "_clearme" then clear_tac ["_clearme"] else id_tac ]