]> matita.cs.unibo.it Git - helm.git/blob - helm/matita/matitaScript.ml
removed debug prerr_endline
[helm.git] / helm / matita / matitaScript.ml
1 (* Copyright (C) 2004-2005, HELM Team.
2  * 
3  * This file is part of HELM, an Hypertextual, Electronic
4  * Library of Mathematics, developed at the Computer Science
5  * Department, University of Bologna, Italy.
6  * 
7  * HELM is free software; you can redistribute it and/or
8  * modify it under the terms of the GNU General Public License
9  * as published by the Free Software Foundation; either version 2
10  * of the License, or (at your option) any later version.
11  * 
12  * HELM is distributed in the hope that it will be useful,
13  * but WITHOUT ANY WARRANTY; without even the implied warranty of
14  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
15  * GNU General Public License for more details.
16  *
17  * You should have received a copy of the GNU General Public License
18  * along with HELM; if not, write to the Free Software
19  * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
20  * MA  02111-1307, USA.
21  * 
22  * For details, see the HELM World-Wide-Web page,
23  * http://helm.cs.unibo.it/
24  *)
25
26 open Printf
27
28 open MatitaTypes
29
30   (** raised when one of the script margins (top or bottom) is reached *)
31 exception Margin
32
33 let safe_substring s i j =
34   try String.sub s i j with Invalid_argument _ -> assert false
35
36 let heading_nl_RE = Pcre.regexp "^\\s*\n\\s*"
37 let only_dust_RE = Pcre.regexp "^(\\s|\n|%%[^\n]*\n)*$"
38 let multiline_RE = Pcre.regexp "^\n[^\n]+$"
39 let newline_RE = Pcre.regexp "\n"
40  
41 let comment str =
42   if Pcre.pmatch ~rex:multiline_RE str then
43     "\n(** " ^ (Pcre.replace ~rex:newline_RE str) ^ " **)"
44   else
45     "\n(**\n" ^ str ^ "\n**)"
46                      
47 let first_line s =
48   let s = Pcre.replace ~rex:heading_nl_RE s in
49   try
50     let nl_pos = String.index s '\n' in
51     String.sub s 0 nl_pos
52   with Not_found -> s
53
54 let prepend_text header base =
55   if Pcre.pmatch ~rex:heading_nl_RE base then
56     sprintf "\n%s%s" header base
57   else
58     sprintf "%s\n%s" header base
59
60   (** creates a statement AST for the Goal tactic, e.g. "goal 7" *)
61 let goal_ast n =
62   let module A = TacticAst in
63   let loc = CicAst.dummy_floc in
64   A.Executable (loc, A.Tactical (loc, A.Tactic (loc, A.Goal (loc, n))))
65
66 let eval_with_engine status user_goal parsed_text st =
67   let module TA = TacticAst in
68   let module TAPp = TacticAstPp in
69   let parsed_text_length = String.length parsed_text in
70   let loc, ex = 
71     match st with TA.Executable (loc,ex) -> loc, ex | _ -> assert false 
72   in
73   let goal_changed = ref false in
74   let status =
75     match status.proof_status with
76       | Incomplete_proof (_, goal) when goal <> user_goal ->
77           goal_changed := true;
78           MatitaEngine.eval_ast status (goal_ast user_goal)
79       | _ -> status
80   in
81   let new_status = MatitaEngine.eval_ast status st in
82   let new_aliases =
83     match ex with
84       | TA.Command (_, TA.Alias _) ->
85           DisambiguateTypes.Environment.empty
86       | _ -> MatitaSync.alias_diff ~from:status new_status
87   in
88   let new_text =
89     if DisambiguateTypes.Environment.is_empty new_aliases then
90       parsed_text
91     else
92       prepend_text (CicTextualParser2.EnvironmentP3.to_string new_aliases)
93         parsed_text
94   in
95   let new_text =
96     if !goal_changed then
97       prepend_text
98         (TAPp.pp_tactic (TA.Goal (loc, user_goal))(* ^ "\n"*))
99         new_text
100     else
101       new_text
102   in
103     [ new_status, new_text ], parsed_text_length, None
104
105 let disambiguate term status =
106   let module MD = MatitaDisambiguator in
107   let dbd = MatitaDb.instance () in
108   let metasenv = MatitaMisc.get_proof_metasenv status in
109   let context = MatitaMisc.get_proof_context status in
110   let aliases = MatitaMisc.get_proof_aliases status in
111   let interps = MD.disambiguate_term dbd context metasenv aliases term in
112   match interps with 
113   | [_,_,x,_] -> x
114   | _ -> assert false
115  
116 let eval_macro status (mathviewer:MatitaTypes.mathViewer) urichooser parsed_text
117 script mac =
118   let module TA = TacticAst in
119   let module TAPp = TacticAstPp in
120   let module MQ = MetadataQuery in
121   let module MDB = MatitaDb in
122   let module CTC = CicTypeChecker in
123   let module CU = CicUniv in
124   (* no idea why ocaml wants this *)
125   let advance ?statement () = script#advance ?statement () in
126   let parsed_text_length = String.length parsed_text in
127   let dbd = MatitaDb.instance () in
128   match mac with
129   (* WHELP's stuff *)
130   | TA.WMatch (loc, term) -> 
131       let term = disambiguate term status in
132       let l =  MQ.match_term ~dbd term in
133       let entry = `Whelp (TAPp.pp_macro_cic (TA.WMatch (loc, term)), l) in
134       mathviewer#show_uri_list ~reuse:true ~entry l;
135       [], parsed_text_length, None
136   | TA.WInstance (loc, term) ->
137       let term = disambiguate term status in
138       let l = MQ.instance ~dbd term in
139       let entry = `Whelp (TAPp.pp_macro_cic (TA.WInstance (loc, term)), l) in
140       mathviewer#show_uri_list ~reuse:true ~entry l;
141       [], parsed_text_length, None
142   | TA.WLocate (loc, s) -> 
143       let l = MQ.locate ~dbd s in
144       let entry = `Whelp (TAPp.pp_macro_cic (TA.WLocate (loc, s)), l) in
145       mathviewer#show_uri_list ~reuse:true ~entry l;
146       [], parsed_text_length, None  
147   | TA.WElim (loc, term) ->
148       let term = disambiguate term status in
149       let uri =
150         match term with
151         | Cic.MutInd (uri,n,_) -> UriManager.string_of_uriref (uri,[n])
152         | _ -> failwith "Not a MutInd"
153       in
154       let l = MQ.elim ~dbd uri in
155       let entry = `Whelp (TAPp.pp_macro_cic (TA.WElim (loc, term)), l) in
156       mathviewer#show_uri_list ~reuse:true ~entry l;
157       [], parsed_text_length, None  
158   | TA.WHint (loc, term) ->
159       let term = disambiguate term status in
160       let s = ((None,[0,[],term], Cic.Meta (0,[]) ,term),0) in
161       let l = List.map fst (MQ.experimental_hint ~dbd s) in
162       let entry = `Whelp (TAPp.pp_macro_cic (TA.WHint (loc, term)), l) in
163       mathviewer#show_uri_list ~reuse:true ~entry l;
164       [], parsed_text_length, None  
165   (* REAL macro *)
166   | TA.Hint loc -> 
167       let s = MatitaMisc.get_proof_status status in
168       let l = List.map fst (MQ.experimental_hint ~dbd s) in
169       let selected = urichooser l in
170       (match selected with
171       | [] -> [], parsed_text_length, None
172       | [uri] -> 
173         let ast = 
174           (TA.Executable (loc,
175             (TA.Tactical (loc, 
176                TA.Tactic (loc,
177                  TA.Apply (loc, CicAst.Uri (uri,None))))))) 
178         in
179         let new_status = MatitaEngine.eval_ast status ast in
180         let extra_text = 
181           comment parsed_text ^ 
182           "\n" ^ TAPp.pp_statement ast
183         in
184         [ new_status , extra_text ], parsed_text_length, None
185       | _ -> assert false)
186   | TA.Check (_,term) ->
187       let metasenv = MatitaMisc.get_proof_metasenv status in
188       let context = MatitaMisc.get_proof_context status in
189       let aliases = MatitaMisc.get_proof_aliases status in
190       let interps = 
191         MatitaDisambiguator.disambiguate_term 
192           dbd context metasenv aliases term 
193       in
194       let _, metasenv , term, ugraph =
195         match interps with 
196         | [x] -> x
197         | _ -> assert false
198       in
199       let ty,_ = CTC.type_of_aux' metasenv context term ugraph in
200       let t_and_ty = Cic.Cast (term,ty) in
201       mathviewer#show_entry (`Cic (t_and_ty,metasenv));
202       [], parsed_text_length, None
203   | TA.Abort _ -> 
204       let rec go_back () =
205         let status = script#status.proof_status in
206         match status with
207         | No_proof -> ()
208         | _ -> script#retract ();go_back()
209       in
210       [], parsed_text_length, Some go_back
211   | TA.Redo (_, Some i) ->  [], parsed_text_length, 
212       Some (fun () -> for j = 1 to i do advance () done)
213   | TA.Redo (_, None) ->   [], parsed_text_length, 
214       Some (fun () -> advance ())
215   | TA.Undo (_, Some i) ->  [], parsed_text_length, 
216       Some (fun () -> for j = 1 to i do script#retract () done)
217   | TA.Undo (_, None) -> [], parsed_text_length, 
218       Some (fun () -> script#retract ())
219   (* TODO *)
220   | TA.Quit _ -> failwith "not implemented"
221   | TA.Print (_,kind) -> failwith "not implemented"
222   | TA.Search_pat (_, search_kind, str) -> failwith "not implemented"
223   | TA.Search_term (_, search_kind, term) -> failwith "not implemented"
224
225                                 
226 let eval_executable status (mathviewer:MatitaTypes.mathViewer) urichooser
227 user_goal parsed_text script ex =
228   let module TA = TacticAst in
229   let module TAPp = TacticAstPp in
230   let module MD = MatitaDisambiguator in
231   let parsed_text_length = String.length parsed_text in
232   match ex with
233   | TA.Command (loc, _) | TA.Tactical (loc, _) ->
234       eval_with_engine status user_goal parsed_text (TA.Executable (loc, ex))
235   | TA.Macro (_,mac) ->
236       eval_macro status mathviewer urichooser parsed_text script mac
237
238 let rec eval_statement status (mathviewer:MatitaTypes.mathViewer) urichooser
239 user_goal script s =
240   if Pcre.pmatch ~rex:only_dust_RE s then raise Margin;
241   let st = CicTextualParser2.parse_statement (Stream.of_string s) in
242   let text_of_loc loc =
243     let parsed_text_length = snd (CicAst.loc_of_floc loc) in
244     let parsed_text = safe_substring s 0 parsed_text_length in
245     parsed_text, parsed_text_length
246   in
247   match st with
248   | TacticAst.Comment (loc,_)-> 
249       let parsed_text, parsed_text_length = text_of_loc loc in
250       let remain_len = String.length s - parsed_text_length in
251       let s = String.sub s parsed_text_length remain_len in
252       let s,len, act = 
253         eval_statement status mathviewer urichooser user_goal script s 
254       in
255       (match s with
256       | (status, text) :: tl ->
257         ((status, parsed_text ^ text)::tl), (parsed_text_length + len), act
258       | [] -> [], 0, None)
259   | TacticAst.Executable (loc, ex) ->
260       let parsed_text, parsed_text_length = text_of_loc loc in
261       eval_executable 
262         status mathviewer urichooser user_goal parsed_text script ex
263   
264
265 class script ~(buffer: GText.buffer) ~(init: MatitaTypes.status) 
266               ~(mathviewer: MatitaTypes.mathViewer) 
267               ~urichooser () =
268 object (self)
269   initializer self#reset ()
270
271   val mutable statements = [];    (** executed statements *)
272   val mutable history = [ init ];
273     (** list of states before having executed statements. Head element of this
274       * list is the current state, last element is the state at the beginning of
275       * the script.
276       * Invariant: this list length is 1 + length of statements *)
277
278   (** goal as seen by the user (i.e. metano corresponding to current tab) *)
279   val mutable userGoal = ~-1
280
281   (** text mark and tag representing locked part of a script *)
282   val locked_mark =
283     buffer#create_mark ~name:"locked" ~left_gravity:true buffer#start_iter
284   val locked_tag = buffer#create_tag [`BACKGROUND "lightblue"; `EDITABLE false]
285
286     (* history can't be empty, the invariant above grant that it contains at
287      * least the init status *)
288   method status = match history with hd :: _ -> hd | _ -> assert false
289
290   method private _advance ?statement () =
291     let s = match statement with Some s -> s | None -> self#getFuture in
292     MatitaLog.debug ("evaluating: " ^ first_line s ^ " ...");
293     let (entries, parsed_len, post_advance_action) = 
294       eval_statement self#status mathviewer urichooser userGoal self s in
295     let (new_statuses, new_statements) = List.split entries in
296 (*
297 prerr_endline "evalStatement returned";
298 List.iter (fun s -> prerr_endline ("'" ^ s ^ "'")) new_statements;
299 *)
300     history <- List.rev new_statuses @ history;
301     statements <- List.rev new_statements @ statements;
302     let start = buffer#get_iter_at_mark (`MARK locked_mark) in
303     if statement = None then begin
304       let stop = start#copy#forward_chars parsed_len in
305       buffer#delete ~start ~stop
306     end;
307     let new_text = String.concat "" new_statements in
308     buffer#insert ~iter:start new_text;
309     self#moveMark (String.length new_text);
310     match post_advance_action with 
311       | Some f -> f () 
312       | _ -> ()
313
314   method private _retract () =
315     match statements, history with
316     | last_statement :: _, cur_status :: prev_status :: _ ->
317         MatitaSync.time_travel ~present:cur_status ~past:prev_status;
318         statements <- List.tl statements;
319         history <- List.tl history;
320         self#moveMark (- (String.length last_statement));
321     | _ -> raise Margin
322
323   method advance ?statement () =
324     try
325       self#_advance ?statement ()
326     with Margin -> ()
327
328   method retract () = try self#_retract () with Margin -> ()
329
330   method private getFuture =
331     buffer#get_text ~start:(buffer#get_iter_at_mark (`MARK locked_mark))
332       ~stop:buffer#end_iter ()
333
334   (** @param rel_offset relative offset from current position of locked_mark *)
335   method private moveMark rel_offset =
336     let mark = `MARK locked_mark in
337     let old_insert = buffer#get_iter_at_mark `INSERT in
338     buffer#remove_tag locked_tag ~start:buffer#start_iter ~stop:buffer#end_iter;
339     let current_mark_pos = buffer#get_iter_at_mark mark in
340     let new_mark_pos =
341       match rel_offset with
342       | 0 -> current_mark_pos
343       | n when n > 0 -> current_mark_pos#forward_chars n
344       | n (* when n < 0 *) -> current_mark_pos#backward_chars (abs n)
345     in
346     buffer#move_mark mark ~where:new_mark_pos;
347     buffer#apply_tag locked_tag ~start:buffer#start_iter ~stop:new_mark_pos;
348     buffer#move_mark `INSERT old_insert;
349     self#notify
350
351   val mutable observers = []
352
353   method addObserver (o: MatitaTypes.status -> unit) =
354     observers <- o :: observers
355
356   method private notify =
357     let status = self#status in
358     List.iter (fun o -> o status) observers
359
360   method loadFrom fname =
361     buffer#set_text (MatitaMisc.input_file fname);
362     self#goto_top
363
364   method saveTo fname =
365     let oc = open_out fname in
366     output_string oc (buffer#get_text ~start:buffer#start_iter
367                         ~stop:buffer#end_iter ());
368     close_out oc
369
370   method private goto_top =
371     MatitaSync.time_travel ~present:self#status ~past:init;
372     statements <- [];
373     history <- [ init ];
374     userGoal <- ~-1;
375     self#notify;
376     buffer#remove_tag locked_tag ~start:buffer#start_iter ~stop:buffer#end_iter;
377     buffer#move_mark (`MARK locked_mark) ~where:buffer#start_iter
378
379   method reset () =
380     self#goto_top;
381     buffer#delete ~start:buffer#start_iter ~stop:buffer#end_iter
382
383   method goto (pos: [`Top | `Bottom | `Cursor]) () =
384     match pos with
385     | `Top -> self#goto_top
386     | `Bottom ->
387         (try while true do self#_advance () done with Margin -> ())
388     | `Cursor ->
389         let locked_iter () = buffer#get_iter_at_mark (`NAME "locked") in
390         let cursor_iter () = buffer#get_iter_at_mark `INSERT in
391         let rec forward_until_cursor () = (* go forward until locked > cursor *)
392           self#_advance ();
393           if (locked_iter ())#compare (cursor_iter ()) < 0 then
394             forward_until_cursor ()
395         in
396         let rec back_until_cursor () = (* go backward until locked < cursor *)
397           self#_retract ();
398           if (locked_iter ())#compare (cursor_iter ()) > 0 then
399             back_until_cursor ()
400         in
401         let cmp = (locked_iter ())#compare (cursor_iter ()) in
402         (try
403           if cmp < 0 then       (* locked < cursor *)
404             forward_until_cursor ()
405           else if cmp > 0 then  (* locked > cursor *)
406             back_until_cursor ()
407           else                  (* cursor = locked *)
408               ()
409         with Margin -> ())
410
411   method onGoingProof () =
412     match self#status.proof_status with
413     | No_proof | Proof _ -> false
414     | Incomplete_proof _ -> true
415     | Intermediate _ -> assert false
416
417   method proofStatus = MatitaMisc.get_proof_status self#status
418   method proofMetasenv = MatitaMisc.get_proof_metasenv self#status
419   method proofContext = MatitaMisc.get_proof_context self#status
420   method setGoal n = userGoal <- n
421
422   (* debug *)
423   method dump () =
424     MatitaLog.debug "script status:";
425     MatitaLog.debug ("history size: " ^ string_of_int (List.length history));
426     MatitaLog.debug (sprintf "%d statements:" (List.length statements));
427     List.iter MatitaLog.debug statements;
428
429 end
430
431 let _script = ref None
432
433 let script ~buffer ~init ~mathviewer ~urichooser () =
434   let s = new script ~buffer ~init ~mathviewer ~urichooser () in
435   _script := Some s;
436   s
437
438 let instance () = match !_script with None -> assert false | Some s -> s
439
440