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 blanks_RE = Pcre.regexp "^\\s*$"
  38
  39 let first_line s =
  40   let s = Pcre.replace ~rex:heading_nl_RE s in
  41   try
  42     let nl_pos = String.index s '\n' in
  43     String.sub s 0 nl_pos
  44   with Not_found -> s
  45
  46 let prepend_text header base =
  47   if Pcre.pmatch ~rex:heading_nl_RE base then
  48     sprintf "\n%s%s" header base
  49   else
  50     sprintf "%s\n%s" header base
  51
  52   (** creates a statement AST for the Goal tactic, e.g. "goal 7" *)
  53 let goal_ast n =
  54   let module A = TacticAst in
  55   let loc = CicAst.dummy_floc in
  56   A.Tactical (loc, A.Tactic (loc, A.Goal (loc, n)))
  57
  58 let eval_statement status user_goal s =
  59   let st = CicTextualParser2.parse_statement (Stream.of_string s) in
  60   match st with
  61   | TacticAst.Command (loc, _) | TacticAst.Tactical (loc, _) ->
  62       let parsed_text_length = snd (CicAst.loc_of_floc loc) in
  63       let parsed_text = safe_substring s 0 parsed_text_length in
  64       let goal_changed = ref false in
  65       let status =
  66         match status.proof_status with
  67         | Incomplete_proof (_, goal) when goal <> user_goal ->
  68             goal_changed := true;
  69             MatitaEngine.eval_ast status (goal_ast user_goal)
  70         | _ -> status
  71       in
  72       let new_status = MatitaEngine.eval_ast status st in
  73       let new_aliases =
  74         match st with
  75         | TacticAst.Command (_, TacticAst.Alias _) ->
  76             DisambiguateTypes.Environment.empty
  77         | _ -> MatitaSync.alias_diff ~from:status new_status
  78       in
  79       let new_text =
  80         if DisambiguateTypes.Environment.is_empty new_aliases then
  81           parsed_text
  82         else
  83           prepend_text (CicTextualParser2.EnvironmentP3.to_string new_aliases)
  84             parsed_text
  85       in
  86       let new_text =
  87         if !goal_changed then
  88           prepend_text
  89             (TacticAstPp.pp_tactic (TacticAst.Goal (loc, user_goal))(* ^ "\n"*))
  90             new_text
  91         else
  92           new_text
  93       in
  94       [ new_status, new_text ], parsed_text_length
  95   | TacticAst.Macro (loc, mac) ->
  96       (match mac with (* TODO *)
  97        | _ -> failwith "not implemented")
  98
  99 class script ~(buffer: GText.buffer) ~(init: MatitaTypes.status) () =
 100 object (self)
 101   initializer self#reset ()
 102
 103   val mutable statements = [];    (** executed statements *)
 104   val mutable history = [ init ];
 105     (** list of states before having executed statements. Head element of this
 106       * list is the current state, last element is the state at the beginning of
 107       * the script.
 108       * Invariant: this list length is 1 + length of statements *)
 109
 110   (** goal as seen by the user (i.e. metano corresponding to current tab) *)
 111   val mutable userGoal = ~-1
 112
 113   (** text mark and tag representing locked part of a script *)
 114   val locked_mark =
 115     buffer#create_mark ~name:"locked" ~left_gravity:true buffer#start_iter
 116   val locked_tag = buffer#create_tag [`BACKGROUND "lightblue"; `EDITABLE false]
 117
 118     (* history can't be empty, the invariant above grant that it contains at
 119      * least the init status *)
 120   method status = match history with hd :: _ -> hd | _ -> assert false
 121
 122   method private _advance ?statement () =
 123     let s = match statement with Some s -> s | None -> self#getFuture in
 124     if Pcre.pmatch ~rex:blanks_RE s then raise Margin;
 125     MatitaLog.debug ("evaluating: " ^ first_line s ^ " ...");
 126     let (entries, parsed_len) = eval_statement self#status userGoal s in
 127     let (new_statuses, new_statements) = List.split entries in
 128 (*
 129 prerr_endline "evalStatement returned";
 130 List.iter (fun s -> prerr_endline ("'" ^ s ^ "'")) new_statements;
 131 *)
 132     history <- List.rev new_statuses @ history;
 133     statements <- List.rev new_statements @ statements;
 134     let start = buffer#get_iter_at_mark (`MARK locked_mark) in
 135     if statement = None then begin
 136       let stop = start#copy#forward_chars parsed_len in
 137       buffer#delete ~start ~stop
 138     end;
 139     let new_text = String.concat "" new_statements in
 140     buffer#insert ~iter:start new_text;
 141     self#moveMark (String.length new_text);
 142
 143   method private _retract () =
 144     match statements, history with
 145     | last_statement :: _, cur_status :: prev_status :: _ ->
 146         MatitaSync.time_travel ~present:cur_status ~past:prev_status;
 147         statements <- List.tl statements;
 148         history <- List.tl history;
 149         self#moveMark (- (String.length last_statement))
 150     | _ -> raise Margin
 151
 152   method advance ?statement () =
 153     try
 154       self#_advance ?statement ()
 155     with Margin -> ()
 156
 157   method retract () = try self#_retract () with Margin -> ()
 158
 159   method private getFuture =
 160     buffer#get_text ~start:(buffer#get_iter_at_mark (`MARK locked_mark))
 161       ~stop:buffer#end_iter ()
 162
 163   (** @param rel_offset relative offset from current position of locked_mark *)
 164   method private moveMark rel_offset =
 165     let mark = `MARK locked_mark in
 166     buffer#remove_tag locked_tag ~start:buffer#start_iter ~stop:buffer#end_iter;
 167     let current_mark_pos = buffer#get_iter_at_mark mark in
 168     let new_mark_pos =
 169       match rel_offset with
 170       | 0 -> current_mark_pos
 171       | n when n > 0 -> current_mark_pos#forward_chars n
 172       | n (* when n < 0 *) -> current_mark_pos#backward_chars (abs n)
 173     in
 174     buffer#move_mark mark ~where:new_mark_pos;
 175     buffer#apply_tag locked_tag ~start:buffer#start_iter ~stop:new_mark_pos;
 176     self#notify
 177
 178   val mutable observers = []
 179
 180   method addObserver (o: MatitaTypes.status -> unit) =
 181     observers <- o :: observers
 182
 183   method private notify =
 184     let status = self#status in
 185     List.iter (fun o -> o status) observers
 186
 187   method loadFrom fname =
 188     buffer#set_text (MatitaMisc.input_file fname);
 189     self#goto_top
 190
 191   method saveTo fname =
 192     let oc = open_out fname in
 193     output_string oc (buffer#get_text ~start:buffer#start_iter
 194                         ~stop:buffer#end_iter ());
 195     close_out oc
 196
 197   method private goto_top =
 198     MatitaSync.time_travel ~present:self#status ~past:init;
 199     statements <- [];
 200     history <- [ init ];
 201     userGoal <- ~-1;
 202     self#notify;
 203     buffer#remove_tag locked_tag ~start:buffer#start_iter ~stop:buffer#end_iter;
 204     buffer#move_mark (`MARK locked_mark) ~where:buffer#start_iter
 205
 206   method reset () =
 207     self#goto_top;
 208     buffer#delete ~start:buffer#start_iter ~stop:buffer#end_iter
 209
 210   method goto (pos: [`Top | `Bottom | `Cursor]) () =
 211     match pos with
 212     | `Top -> self#goto_top
 213     | `Bottom ->
 214         (try while true do self#_advance () done with Margin -> ())
 215     | `Cursor ->
 216         let locked_iter () = buffer#get_iter_at_mark (`NAME "locked") in
 217         let cursor_iter () = buffer#get_iter_at_mark `INSERT in
 218         let rec forward_until_cursor () = (* go forward until locked > cursor *)
 219           self#_advance ();
 220           if (locked_iter ())#compare (cursor_iter ()) < 0 then
 221             forward_until_cursor ()
 222         in
 223         let rec back_until_cursor () = (* go backward until locked < cursor *)
 224           self#_retract ();
 225           if (locked_iter ())#compare (cursor_iter ()) > 0 then
 226             back_until_cursor ()
 227         in
 228         let cmp = (locked_iter ())#compare (cursor_iter ()) in
 229         (try
 230           if cmp < 0 then       (* locked < cursor *)
 231             forward_until_cursor ()
 232           else if cmp > 0 then  (* locked > cursor *)
 233             back_until_cursor ()
 234           else                  (* cursor = locked *)
 235               ()
 236         with Margin -> ())
 237
 238   method onGoingProof () =
 239     match self#status.proof_status with
 240     | No_proof | Proof _ -> false
 241     | Incomplete_proof _ -> true
 242     | Intermediate _ -> assert false
 243
 244   method proofStatus = MatitaMisc.get_proof_status self#status
 245   method proofMetasenv = MatitaMisc.get_proof_metasenv self#status
 246   method proofContext = MatitaMisc.get_proof_context self#status
 247   method setGoal n = userGoal <- n
 248
 249   (* debug *)
 250   method dump () =
 251     MatitaLog.debug "script status:";
 252     MatitaLog.debug ("history size: " ^ string_of_int (List.length history));
 253     MatitaLog.debug (sprintf "%d statements:" (List.length statements));
 254     List.iter MatitaLog.debug statements;
 255
 256 end
 257
 258 let _script = ref None
 259
 260 let script ~buffer ~init () =
 261   let s = new script ~buffer ~init () in
 262   _script := Some s;
 263   s
 264
 265 let instance () = match !_script with None -> assert false | Some s -> s
 266