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 exception Error of string lazy_t
20 let fail msg = raise (Error msg)
22 type lowtac_status = {
24 lstatus : LexiconEngine.status
27 type lowtactic = lowtac_status * int -> lowtac_status * int list * int list
30 gstatus : Continuationals.Stack.t;
31 istatus : lowtac_status;
34 type tactic = tac_status -> tac_status
36 type tactic_term = CicNotationPt.term Disambiguate.disambiguator_input
38 let pp_tac_status status =
39 prerr_endline (NCicPp.ppobj status.istatus.pstatus)
42 open Continuationals.Stack
46 match status.gstatus with
48 | ([], _, [], _) :: _ as stack ->
49 (* backward compatibility: do-nothing-dot *)
51 | (g, t, k, tag) :: s ->
52 match filter_open g, k with
54 (([ loc ], t, loc_tl @+ k, tag) :: s)
57 (([ loc ], t, k, tag) :: s)
58 | _ -> fail (lazy "can't use \".\" here")
60 { status with gstatus = new_gstatus }
63 let branch_tac status =
65 match status.gstatus with
67 | (g, t, k, tag) :: s ->
68 match init_pos g with (* TODO *)
69 | [] | [ _ ] -> fail (lazy "too few goals to branch");
71 ([ loc ], [], [], `BranchTag) :: (loc_tl, t, k, tag) :: s
73 { status with gstatus = new_gstatus }
76 let shift_tac status =
78 match status.gstatus with
79 | (g, t, k, `BranchTag) :: (g', t', k', tag) :: s ->
81 | [] -> fail (lazy "no more goals to shift")
83 (([ loc ], t @+ filter_open g @+ k, [],`BranchTag)
84 :: (loc_tl, t', k', tag) :: s))
85 | _ -> fail (lazy "can't shift goals here")
87 { status with gstatus = new_gstatus }
90 let pos_tac i_s status =
92 match status.gstatus with
94 | ([ loc ], t, [],`BranchTag) :: (g', t', k', tag) :: s
96 let l_js = List.filter (fun (i, _) -> List.mem i i_s) ([loc] @+ g') in
97 ((l_js, t , [],`BranchTag)
98 :: (([ loc ] @+ g') @- l_js, t', k', tag) :: s)
99 | _ -> fail (lazy "can't use relative positioning here")
101 { status with gstatus = new_gstatus }
104 let wildcard_tac status =
106 match status.gstatus with
108 | ([ loc ] , t, [], `BranchTag) :: (g', t', k', tag) :: s
110 (([loc] @+ g', t, [], `BranchTag) :: ([], t', k', tag) :: s)
111 | _ -> fail (lazy "can't use wildcard here")
113 { status with gstatus = new_gstatus }
116 let merge_tac status =
118 match status.gstatus with
120 | (g, t, k,`BranchTag) :: (g', t', k', tag) :: s ->
121 ((t @+ filter_open g @+ g' @+ k, t', k', tag) :: s)
122 | _ -> fail (lazy "can't merge goals here")
124 { status with gstatus = new_gstatus }
127 let focus_tac gs status =
129 match status.gstatus with
131 | s -> assert(gs <> []);
133 let add_l acc _ _ l = if is_open l then l :: acc else acc in
134 fold ~env:add_l ~cont:add_l ~todo:add_l [] s
138 if not (List.exists (fun l -> goal_of_loc l = g) stack_locs) then
139 fail (lazy (sprintf "goal %d not found (or closed)" g)))
141 (zero_pos gs, [], [], `FocusTag) :: deep_close gs s
143 { status with gstatus = new_gstatus }
146 let unfocus_tac status =
148 match status.gstatus with
150 | ([], [], [], `FocusTag) :: s -> s
151 | _ -> fail (lazy "can't unfocus, some goals are still open")
153 { status with gstatus = new_gstatus }
156 let skip_tac status =
158 match status.gstatus with
160 | (gl, t, k, tag) :: s ->
161 let gl = List.map switch_of_loc gl in
162 if List.exists (function Open _ -> true | Closed _ -> false) gl then
163 fail (lazy "cannot skip an open goal")
167 { status with gstatus = new_gstatus }
170 let block_tac l status =
171 List.fold_left (fun status tac -> tac status) status l
174 let compare_menv ~past ~present =
175 List.map fst (List.filter (fun (i,_) -> not (List.mem_assoc i past)) present),
176 List.map fst (List.filter (fun (i,_) -> not (List.mem_assoc i present)) past)
179 (* Exec and distribute_tac form a retraction pair:
180 1) exec (distribute_tac low_tac) (s,i) = low_tac (s,i)
181 2) tac [s]::G = G1::...::Gn::G' && G' is G with some goals closed =>
182 distribute_tac (exec tac) [s]::G = (G1@...Gn)::G'
184 Note that executing an high tactic on a set of goals may be stronger
185 than executing the same tactic on those goals, but once at a time
186 (e.g. the tactic could perform a global analysis of the set of goals)
189 let exec tac (low_status,g) =
190 let stack = [ [0,Open g], [], [], `NoTag ] in
191 let _,_,old_metasenv,_,_ = low_status.pstatus in
192 let status = tac { gstatus = stack ; istatus = low_status } in
193 let _,_,metasenv,_,_ = status.istatus.pstatus in
194 let open_goals, closed_goals =
195 compare_menv ~past:old_metasenv ~present:metasenv
197 status.istatus, open_goals, closed_goals
200 let distribute_tac tac status =
201 match status.gstatus with
203 | (g, t, k, tag) :: s ->
204 debug_print (lazy ("context length " ^string_of_int (List.length g)));
205 let rec aux s go gc =
209 debug_print (lazy "inner eval tactical");
211 if List.exists ((=) (goal_of_loc loc)) gc then
214 match switch_of_loc loc with
215 | Closed _ -> fail (lazy "cannot apply to a Closed goal")
217 let s, go', gc' = tac (s,n) in
218 s, (go @- gc') @+ go', gc @+ gc'
222 let s0, go0, gc0 = status.istatus, [], [] in
223 let sn, gon, gcn = aux s0 go0 gc0 g in
224 debug_print (lazy ("opened: "
225 ^ String.concat " " (List.map string_of_int gon)));
226 debug_print (lazy ("closed: "
227 ^ String.concat " " (List.map string_of_int gcn)));
229 (zero_pos gon, t @~- gcn, k @~- gcn, tag) :: deep_close gcn s
231 { gstatus = stack; istatus = sn }
235 type cic_term = NCic.conjecture
236 type ast_term = CicNotationPt.term
237 type position = Ctx of NCic.context | Term of cic_term
239 let relocate (name,ctx,t as term) context =
240 if ctx = context then term else assert false
243 let disambiguate (status : lowtac_status) (t : ast_term)
244 (ty : cic_term option) (where : position) =
245 let uri,height,metasenv,subst,obj = status.pstatus in
246 let context = match where with Ctx c -> c | Term (_,c,_) -> c in
249 | None -> None | Some ty -> let _,_,x = relocate ty context in Some x
251 let metasenv, subst, lexicon_status, t =
252 GrafiteDisambiguate.disambiguate_nterm expty
253 status.lstatus context metasenv subst t
255 let new_pstatus = uri,height,metasenv,subst,obj in
256 { lstatus = lexicon_status; pstatus = new_pstatus }, (None, context, t)
259 let get_goal (status : low_status) (g : int) =
260 let _,_,metasenv,_,_ = status.pstatus in
261 List.assoc goal metasenv
264 let return ~orig status =
265 let _,_,past,_,_ = orig.pstatus in
266 let _,_,present,_,_ = status.pstatus in
267 let open_goals, closed_goals = compare_menv ~past ~present in
268 status, open_goals, closed_goals
271 let apply t (status as orig,goal) =
272 let goal = get_goal status goal in
273 let status, t = disambiguate status t goal (Term goal) in
274 let subst, metasenv =
275 (goal, (name, context, t, gty)):: subst,
276 List.filter(fun (x,_) -> x <> goal) metasenv
284 let apply t (status,goal) =
285 let uri,height,(metasenv as old_metasenv), subst,obj = status.pstatus in
286 let name,context,gty = List.assoc goal metasenv in
287 let metasenv, subst, lexicon_status, t =
288 GrafiteDisambiguate.disambiguate_nterm (Some gty)
289 status.lstatus context metasenv subst t
291 let subst, metasenv =
292 (goal, (name, context, t, gty)):: subst,
293 List.filter(fun (x,_) -> x <> goal) metasenv
295 let open_goals, closed_goals =
296 compare_menv ~past:old_metasenv ~present:metasenv in
297 let new_pstatus = uri,height,metasenv,subst,obj in
299 prerr_endline ("termine disambiguato: " ^
300 NCicPp.ppterm ~context ~metasenv ~subst t);
301 prerr_endline ("menv:" ^ NCicPp.ppmetasenv ~subst metasenv);
302 prerr_endline ("subst:" ^ NCicPp.ppsubst subst ~metasenv);
303 prerr_endline "fine napply";
305 { lstatus = lexicon_status; pstatus = new_pstatus }, open_goals, closed_goals
308 let apply_tac t = distribute_tac (apply t) ;;