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
 104
 105 let eval_macro status (mathviewer:MatitaTypes.mathViewer) urichooser parsed_text mac =
 106   let module TA = TacticAst in
 107   let module TAPp = TacticAstPp in
 108   let module MQ = MetadataQuery in
 109   let module MD = MatitaDisambiguator in
 110   let module MDB = MatitaDb in
 111   let parsed_text_length = String.length parsed_text in
 112   match mac with
 113   | TA.Hint loc ->
 114       let s = MatitaMisc.get_proof_status status in
 115       let l = List.map fst (MQ.experimental_hint ~dbd:(MDB.instance ()) s) in
 116       let selected = urichooser l in
 117       (match selected with
 118       | [] -> [], parsed_text_length
 119       | [uri] ->
 120         let ast =
 121           (TA.Executable (loc,
 122             (TA.Tactical (loc,
 123                TA.Tactic (loc,
 124                  TA.Apply (loc, CicAst.Uri (uri,None)))))))
 125         in
 126         let new_status = MatitaEngine.eval_ast status ast in
 127         let extra_text =
 128           comment parsed_text ^
 129           "\n" ^ TAPp.pp_statement ast
 130         in
 131         [ new_status , extra_text ],parsed_text_length
 132       | _ -> assert false)
 133   | TA.Match (_,term) ->
 134       let dbd = MatitaDb.instance () in
 135       let metasenv = MatitaMisc.get_proof_metasenv status in
 136       let context = MatitaMisc.get_proof_context status in
 137       let aliases = MatitaMisc.get_proof_aliases status in
 138       let (_env,_metasenv,term,_graph) =
 139         let interps =
 140           MD.disambiguate_term dbd context metasenv aliases term
 141         in
 142         match interps with
 143         | [x] -> x
 144         | _ -> assert false
 145       in
 146       let results =  MetadataQuery.match_term ~dbd:dbd term in
 147       mathviewer#show_uri_list ~reuse:true ~entry:(`Whelp ("match", results))
 148         results;
 149       [], parsed_text_length
 150   | TA.Instance (_,term) ->
 151       let dbd = MatitaDb.instance () in
 152       let metasenv = MatitaMisc.get_proof_metasenv status in
 153       let context = MatitaMisc.get_proof_context status in
 154       let aliases = MatitaMisc.get_proof_aliases status in
 155       let (_env,_metasenv,term,_graph) =
 156         let interps =
 157           MD.disambiguate_term dbd context metasenv aliases term
 158         in
 159           match interps with
 160             | [x] -> x
 161             | _ -> assert false
 162       in
 163       let results = MetadataQuery.instance ~dbd term in
 164         mathviewer#show_uri_list ~reuse:true
 165           ~entry:(`Whelp ("instance", results)) results;
 166         [], parsed_text_length
 167
 168
 169   | TA.Check (_,t) ->
 170       let metasenv = MatitaMisc.get_proof_metasenv status in
 171       let context = MatitaMisc.get_proof_context status in
 172       let aliases = MatitaMisc.get_proof_aliases status in
 173       let db = MatitaDb.instance () in
 174       let (_env,_metasenv,term,_graph) =
 175         let interps =
 176           MD.disambiguate_term db context metasenv aliases t
 177         in
 178           match interps with
 179             | [x] -> x
 180             | _ -> assert false
 181       in
 182       let ty,_ =
 183         CicTypeChecker.type_of_aux' metasenv context term
 184           CicUniv.empty_ugraph
 185       in
 186       let t_and_ty = Cic.Cast (term,ty) in
 187         mathviewer # show_entry (`Cic (t_and_ty,metasenv));
 188         [], parsed_text_length
 189   | TA.Quit _ ->
 190       failwith "not implemented quit"
 191   | _ -> failwith "not implemented"
 192
 193
 194 let eval_executable status (mathviewer:MatitaTypes.mathViewer) urichooser user_goal parsed_text ex =
 195   let module TA = TacticAst in
 196   let module TAPp = TacticAstPp in
 197   let module MD = MatitaDisambiguator in
 198   let parsed_text_length = String.length parsed_text in
 199   match ex with
 200   | TA.Command (loc, _) | TA.Tactical (loc, _) ->
 201       eval_with_engine status user_goal parsed_text (TA.Executable (loc, ex))
 202   | TA.Macro (_,mac) ->
 203       eval_macro status mathviewer urichooser parsed_text mac
 204
 205 let rec eval_statement status (mathviewer:MatitaTypes.mathViewer) urichooser user_goal s =
 206   if Pcre.pmatch ~rex:only_dust_RE s then raise Margin;
 207   let st = CicTextualParser2.parse_statement (Stream.of_string s) in
 208   let text_of_loc loc =
 209     let parsed_text_length = snd (CicAst.loc_of_floc loc) in
 210     let parsed_text = safe_substring s 0 parsed_text_length in
 211     parsed_text, parsed_text_length
 212   in
 213   match st with
 214   | TacticAst.Comment (loc,_)->
 215       let parsed_text, parsed_text_length = text_of_loc loc in
 216       let remain_len = String.length s - parsed_text_length in
 217       let s = String.sub s parsed_text_length remain_len in
 218       let s,len = eval_statement status mathviewer urichooser user_goal s in
 219       (match s with
 220       | (status, text) :: tl ->
 221         ((status, parsed_text ^ text)::tl), (parsed_text_length + len)
 222       | [] -> [], 0)
 223   | TacticAst.Executable (loc, ex) ->
 224       let parsed_text, parsed_text_length = text_of_loc loc in
 225       eval_executable status mathviewer urichooser user_goal parsed_text ex
 226
 227
 228 class script ~(buffer: GText.buffer) ~(init: MatitaTypes.status)
 229               ~(mathviewer: MatitaTypes.mathViewer)
 230               ~urichooser () =
 231 object (self)
 232   initializer self#reset ()
 233
 234   val mutable statements = [];    (** executed statements *)
 235   val mutable history = [ init ];
 236     (** list of states before having executed statements. Head element of this
 237       * list is the current state, last element is the state at the beginning of
 238       * the script.
 239       * Invariant: this list length is 1 + length of statements *)
 240
 241   (** goal as seen by the user (i.e. metano corresponding to current tab) *)
 242   val mutable userGoal = ~-1
 243
 244   (** text mark and tag representing locked part of a script *)
 245   val locked_mark =
 246     buffer#create_mark ~name:"locked" ~left_gravity:true buffer#start_iter
 247   val locked_tag = buffer#create_tag [`BACKGROUND "lightblue"; `EDITABLE false]
 248
 249     (* history can't be empty, the invariant above grant that it contains at
 250      * least the init status *)
 251   method status = match history with hd :: _ -> hd | _ -> assert false
 252
 253   method private _advance ?statement () =
 254     let s = match statement with Some s -> s | None -> self#getFuture in
 255     MatitaLog.debug ("evaluating: " ^ first_line s ^ " ...");
 256     let (entries, parsed_len) =
 257       eval_statement self#status mathviewer urichooser userGoal s in
 258     let (new_statuses, new_statements) = List.split entries in
 259 (*
 260 prerr_endline "evalStatement returned";
 261 List.iter (fun s -> prerr_endline ("'" ^ s ^ "'")) new_statements;
 262 *)
 263     history <- List.rev new_statuses @ history;
 264     statements <- List.rev new_statements @ statements;
 265     let start = buffer#get_iter_at_mark (`MARK locked_mark) in
 266     if statement = None then begin
 267       let stop = start#copy#forward_chars parsed_len in
 268       buffer#delete ~start ~stop
 269     end;
 270     let new_text = String.concat "" new_statements in
 271     buffer#insert ~iter:start new_text;
 272     self#moveMark (String.length new_text);
 273
 274   method private _retract () =
 275     match statements, history with
 276     | last_statement :: _, cur_status :: prev_status :: _ ->
 277         MatitaSync.time_travel ~present:cur_status ~past:prev_status;
 278         statements <- List.tl statements;
 279         history <- List.tl history;
 280         self#moveMark (- (String.length last_statement))
 281     | _ -> raise Margin
 282
 283   method advance ?statement () =
 284     try
 285       self#_advance ?statement ()
 286     with Margin -> ()
 287
 288   method retract () = try self#_retract () with Margin -> ()
 289
 290   method private getFuture =
 291     buffer#get_text ~start:(buffer#get_iter_at_mark (`MARK locked_mark))
 292       ~stop:buffer#end_iter ()
 293
 294   (** @param rel_offset relative offset from current position of locked_mark *)
 295   method private moveMark rel_offset =
 296     let mark = `MARK locked_mark in
 297     buffer#remove_tag locked_tag ~start:buffer#start_iter ~stop:buffer#end_iter;
 298     let current_mark_pos = buffer#get_iter_at_mark mark in
 299     let new_mark_pos =
 300       match rel_offset with
 301       | 0 -> current_mark_pos
 302       | n when n > 0 -> current_mark_pos#forward_chars n
 303       | n (* when n < 0 *) -> current_mark_pos#backward_chars (abs n)
 304     in
 305     buffer#move_mark mark ~where:new_mark_pos;
 306     buffer#apply_tag locked_tag ~start:buffer#start_iter ~stop:new_mark_pos;
 307     self#notify
 308
 309   val mutable observers = []
 310
 311   method addObserver (o: MatitaTypes.status -> unit) =
 312     observers <- o :: observers
 313
 314   method private notify =
 315     let status = self#status in
 316     List.iter (fun o -> o status) observers
 317
 318   method loadFrom fname =
 319     buffer#set_text (MatitaMisc.input_file fname);
 320     self#goto_top
 321
 322   method saveTo fname =
 323     let oc = open_out fname in
 324     output_string oc (buffer#get_text ~start:buffer#start_iter
 325                         ~stop:buffer#end_iter ());
 326     close_out oc
 327
 328   method private goto_top =
 329     MatitaSync.time_travel ~present:self#status ~past:init;
 330     statements <- [];
 331     history <- [ init ];
 332     userGoal <- ~-1;
 333     self#notify;
 334     buffer#remove_tag locked_tag ~start:buffer#start_iter ~stop:buffer#end_iter;
 335     buffer#move_mark (`MARK locked_mark) ~where:buffer#start_iter
 336
 337   method reset () =
 338     self#goto_top;
 339     buffer#delete ~start:buffer#start_iter ~stop:buffer#end_iter
 340
 341   method goto (pos: [`Top | `Bottom | `Cursor]) () =
 342     match pos with
 343     | `Top -> self#goto_top
 344     | `Bottom ->
 345         (try while true do self#_advance () done with Margin -> ())
 346     | `Cursor ->
 347         let locked_iter () = buffer#get_iter_at_mark (`NAME "locked") in
 348         let cursor_iter () = buffer#get_iter_at_mark `INSERT in
 349         let rec forward_until_cursor () = (* go forward until locked > cursor *)
 350           self#_advance ();
 351           if (locked_iter ())#compare (cursor_iter ()) < 0 then
 352             forward_until_cursor ()
 353         in
 354         let rec back_until_cursor () = (* go backward until locked < cursor *)
 355           self#_retract ();
 356           if (locked_iter ())#compare (cursor_iter ()) > 0 then
 357             back_until_cursor ()
 358         in
 359         let cmp = (locked_iter ())#compare (cursor_iter ()) in
 360         (try
 361           if cmp < 0 then       (* locked < cursor *)
 362             forward_until_cursor ()
 363           else if cmp > 0 then  (* locked > cursor *)
 364             back_until_cursor ()
 365           else                  (* cursor = locked *)
 366               ()
 367         with Margin -> ())
 368
 369   method onGoingProof () =
 370     match self#status.proof_status with
 371     | No_proof | Proof _ -> false
 372     | Incomplete_proof _ -> true
 373     | Intermediate _ -> assert false
 374
 375   method proofStatus = MatitaMisc.get_proof_status self#status
 376   method proofMetasenv = MatitaMisc.get_proof_metasenv self#status
 377   method proofContext = MatitaMisc.get_proof_context self#status
 378   method setGoal n = userGoal <- n
 379
 380   (* debug *)
 381   method dump () =
 382     MatitaLog.debug "script status:";
 383     MatitaLog.debug ("history size: " ^ string_of_int (List.length history));
 384     MatitaLog.debug (sprintf "%d statements:" (List.length statements));
 385     List.iter MatitaLog.debug statements;
 386
 387 end
 388
 389 let _script = ref None
 390
 391 let script ~buffer ~init ~mathviewer ~urichooser () =
 392   let s = new script ~buffer ~init ~mathviewer ~urichooser () in
 393   _script := Some s;
 394   s
 395
 396 let instance () = match !_script with None -> assert false | Some s -> s
 397
 398