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'
183 3) tac G = distribute_tac (exec tac) G if
184 tac = distribute_tac lowtac
186 Note that executing an high tactic on a set of goals may be stronger
187 than executing the same tactic on those goals, but once at a time
188 (e.g. the tactic could perform a global analysis of the set of goals)
191 let exec tac (low_status,g) =
192 let stack = [ [0,Open g], [], [], `NoTag ] in
193 let _,_,old_metasenv,_,_ = low_status.pstatus in
194 let status = tac { gstatus = stack ; istatus = low_status } in
195 let _,_,metasenv,_,_ = status.istatus.pstatus in
196 let open_goals, closed_goals =
197 compare_menv ~past:old_metasenv ~present:metasenv
199 status.istatus, open_goals, closed_goals
202 let distribute_tac tac status =
203 match status.gstatus with
205 | (g, t, k, tag) :: s ->
206 debug_print (lazy ("context length " ^string_of_int (List.length g)));
207 let rec aux s go gc =
211 debug_print (lazy "inner eval tactical");
213 if List.exists ((=) (goal_of_loc loc)) gc then
216 match switch_of_loc loc with
217 | Closed _ -> fail (lazy "cannot apply to a Closed goal")
219 let s, go', gc' = tac (s,n) in
220 s, (go @- gc') @+ go', gc @+ gc'
224 let s0, go0, gc0 = status.istatus, [], [] in
225 let sn, gon, gcn = aux s0 go0 gc0 g in
226 debug_print (lazy ("opened: "
227 ^ String.concat " " (List.map string_of_int gon)));
228 debug_print (lazy ("closed: "
229 ^ String.concat " " (List.map string_of_int gcn)));
231 (zero_pos gon, t @~- gcn, k @~- gcn, tag) :: deep_close gcn s
233 { gstatus = stack; istatus = sn }
238 type cic_term = NCic.conjecture
239 type ast_term = string * int * CicNotationPt.term
240 type position = Ctx of NCic.context | Term of cic_term
242 let relocate (name,ctx,t as term) context =
243 if ctx = context then term else assert false
246 let disambiguate (status : lowtac_status) (t : ast_term)
247 (ty : cic_term option) (where : position) =
248 let uri,height,metasenv,subst,obj = status.pstatus in
249 let context = match where with Ctx c -> c | Term (_,c,_) -> c in
252 | None -> None | Some ty -> let _,_,x = relocate ty context in Some x
254 let metasenv, subst, lexicon_status, t =
255 GrafiteDisambiguate.disambiguate_nterm expty
256 status.lstatus context metasenv subst t
258 let new_pstatus = uri,height,metasenv,subst,obj in
259 { lstatus = lexicon_status; pstatus = new_pstatus }, (None, context, t)
262 let get_goal (status : lowtac_status) (g : int) =
263 let _,_,metasenv,_,_ = status.pstatus in
264 List.assoc g metasenv
267 let return ~orig status =
268 let _,_,past,_,_ = orig.pstatus in
269 let _,_,present,_,_ = status.pstatus in
270 let open_goals, closed_goals = compare_menv ~past ~present in
271 status, open_goals, closed_goals
274 let instantiate status i t =
275 let name,height,metasenv,subst,obj = status.pstatus in
276 let _, context, ty = List.assoc i metasenv in
277 let _,_,t = relocate t context in
278 let m = NCic.Meta (i,(0,NCic.Irl (List.length context))) in
279 let db = NCicUnifHint.db () in (* XXX fixme *)
280 let metasenv, subst = NCicUnification.unify db metasenv subst context m t in
281 { status with pstatus = (name,height,metasenv,subst,obj) }
284 let apply t (status as orig, goal) =
285 let goalty = get_goal status goal in
286 let status, t = disambiguate status t (Some goalty) (Term goalty) in
287 let status = instantiate status goal t in
292 let apply t (status,goal) =
293 let uri,height,(metasenv as old_metasenv), subst,obj = status.pstatus in
294 let name,context,gty = List.assoc goal metasenv in
295 let metasenv, subst, lexicon_status, t =
296 GrafiteDisambiguate.disambiguate_nterm (Some gty)
297 status.lstatus context metasenv subst t
299 let subst, metasenv =
300 (goal, (name, context, t, gty)):: subst,
301 List.filter(fun (x,_) -> x <> goal) metasenv
303 let open_goals, closed_goals =
304 compare_menv ~past:old_metasenv ~present:metasenv in
305 let new_pstatus = uri,height,metasenv,subst,obj in
307 prerr_endline ("termine disambiguato: " ^
308 NCicPp.ppterm ~context ~metasenv ~subst t);
309 prerr_endline ("menv:" ^ NCicPp.ppmetasenv ~subst metasenv);
310 prerr_endline ("subst:" ^ NCicPp.ppsubst subst ~metasenv);
311 prerr_endline "fine napply";
313 { lstatus = lexicon_status; pstatus = new_pstatus }, open_goals, closed_goals
316 let apply_tac t = distribute_tac (apply t) ;;