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 mathviewer 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       let parsed_text_length = snd (CicAst.loc_of_floc loc) in
  97       (match mac with (* TODO *)
  98        | TacticAst.Hint _ ->
  99           let s = MatitaMisc.get_proof_status status in
 100           let l = List.map fst
 101             (MetadataQuery.experimental_hint ~dbd:(MatitaDb.instance ()) s)
 102           in
 103           List.iter prerr_endline l;
 104           prerr_endline "FINITA LA HINT"; assert false
 105         | TacticAst.Check (_,t) ->
 106             let metasenv = MatitaMisc.get_proof_metasenv status in
 107             let context = MatitaMisc.get_proof_context status in
 108             let aliases = MatitaMisc.get_proof_aliases status in
 109             let db = MatitaDb.instance () in
 110             let (_env,_metasenv,term,_graph) =
 111               let interps =
 112                 MatitaDisambiguator.disambiguate_term db context metasenv
 113                   aliases t
 114               in
 115               match interps with
 116               | [x] -> x
 117               | _ -> assert false
 118             in
 119             let ty,_ =
 120               CicTypeChecker.type_of_aux' metasenv context term
 121                 CicUniv.empty_ugraph
 122             in
 123             mathviewer # show_term (`Cic (ty,metasenv) );
 124             [ status, "" ] , parsed_text_length
 125        | _ -> failwith "not implemented")
 126
 127 class script ~(buffer: GText.buffer) ~(init: MatitaTypes.status)
 128               ~(mathviewer: MatitaTypes.mathViewer) () =
 129 object (self)
 130   initializer self#reset ()
 131
 132   val mutable statements = [];    (** executed statements *)
 133   val mutable history = [ init ];
 134     (** list of states before having executed statements. Head element of this
 135       * list is the current state, last element is the state at the beginning of
 136       * the script.
 137       * Invariant: this list length is 1 + length of statements *)
 138
 139   (** goal as seen by the user (i.e. metano corresponding to current tab) *)
 140   val mutable userGoal = ~-1
 141
 142   (** text mark and tag representing locked part of a script *)
 143   val locked_mark =
 144     buffer#create_mark ~name:"locked" ~left_gravity:true buffer#start_iter
 145   val locked_tag = buffer#create_tag [`BACKGROUND "lightblue"; `EDITABLE false]
 146
 147     (* history can't be empty, the invariant above grant that it contains at
 148      * least the init status *)
 149   method status = match history with hd :: _ -> hd | _ -> assert false
 150
 151   method private _advance ?statement () =
 152     let s = match statement with Some s -> s | None -> self#getFuture in
 153     if Pcre.pmatch ~rex:blanks_RE s then raise Margin;
 154     MatitaLog.debug ("evaluating: " ^ first_line s ^ " ...");
 155     let (entries, parsed_len) =
 156       eval_statement self#status mathviewer userGoal s in
 157     let (new_statuses, new_statements) = List.split entries in
 158 (*
 159 prerr_endline "evalStatement returned";
 160 List.iter (fun s -> prerr_endline ("'" ^ s ^ "'")) new_statements;
 161 *)
 162     history <- List.rev new_statuses @ history;
 163     statements <- List.rev new_statements @ statements;
 164     let start = buffer#get_iter_at_mark (`MARK locked_mark) in
 165     if statement = None then begin
 166       let stop = start#copy#forward_chars parsed_len in
 167       buffer#delete ~start ~stop
 168     end;
 169     let new_text = String.concat "" new_statements in
 170     buffer#insert ~iter:start new_text;
 171     self#moveMark (String.length new_text);
 172
 173   method private _retract () =
 174     match statements, history with
 175     | last_statement :: _, cur_status :: prev_status :: _ ->
 176         MatitaSync.time_travel ~present:cur_status ~past:prev_status;
 177         statements <- List.tl statements;
 178         history <- List.tl history;
 179         self#moveMark (- (String.length last_statement))
 180     | _ -> raise Margin
 181
 182   method advance ?statement () =
 183     try
 184       self#_advance ?statement ()
 185     with Margin -> ()
 186
 187   method retract () = try self#_retract () with Margin -> ()
 188
 189   method private getFuture =
 190     buffer#get_text ~start:(buffer#get_iter_at_mark (`MARK locked_mark))
 191       ~stop:buffer#end_iter ()
 192
 193   (** @param rel_offset relative offset from current position of locked_mark *)
 194   method private moveMark rel_offset =
 195     let mark = `MARK locked_mark in
 196     buffer#remove_tag locked_tag ~start:buffer#start_iter ~stop:buffer#end_iter;
 197     let current_mark_pos = buffer#get_iter_at_mark mark in
 198     let new_mark_pos =
 199       match rel_offset with
 200       | 0 -> current_mark_pos
 201       | n when n > 0 -> current_mark_pos#forward_chars n
 202       | n (* when n < 0 *) -> current_mark_pos#backward_chars (abs n)
 203     in
 204     buffer#move_mark mark ~where:new_mark_pos;
 205     buffer#apply_tag locked_tag ~start:buffer#start_iter ~stop:new_mark_pos;
 206     self#notify
 207
 208   val mutable observers = []
 209
 210   method addObserver (o: MatitaTypes.status -> unit) =
 211     observers <- o :: observers
 212
 213   method private notify =
 214     let status = self#status in
 215     List.iter (fun o -> o status) observers
 216
 217   method loadFrom fname =
 218     buffer#set_text (MatitaMisc.input_file fname);
 219     self#goto_top
 220
 221   method saveTo fname =
 222     let oc = open_out fname in
 223     output_string oc (buffer#get_text ~start:buffer#start_iter
 224                         ~stop:buffer#end_iter ());
 225     close_out oc
 226
 227   method private goto_top =
 228     MatitaSync.time_travel ~present:self#status ~past:init;
 229     statements <- [];
 230     history <- [ init ];
 231     userGoal <- ~-1;
 232     self#notify;
 233     buffer#remove_tag locked_tag ~start:buffer#start_iter ~stop:buffer#end_iter;
 234     buffer#move_mark (`MARK locked_mark) ~where:buffer#start_iter
 235
 236   method reset () =
 237     self#goto_top;
 238     buffer#delete ~start:buffer#start_iter ~stop:buffer#end_iter
 239
 240   method goto (pos: [`Top | `Bottom | `Cursor]) () =
 241     match pos with
 242     | `Top -> self#goto_top
 243     | `Bottom ->
 244         (try while true do self#_advance () done with Margin -> ())
 245     | `Cursor ->
 246         let locked_iter () = buffer#get_iter_at_mark (`NAME "locked") in
 247         let cursor_iter () = buffer#get_iter_at_mark `INSERT in
 248         let rec forward_until_cursor () = (* go forward until locked > cursor *)
 249           self#_advance ();
 250           if (locked_iter ())#compare (cursor_iter ()) < 0 then
 251             forward_until_cursor ()
 252         in
 253         let rec back_until_cursor () = (* go backward until locked < cursor *)
 254           self#_retract ();
 255           if (locked_iter ())#compare (cursor_iter ()) > 0 then
 256             back_until_cursor ()
 257         in
 258         let cmp = (locked_iter ())#compare (cursor_iter ()) in
 259         (try
 260           if cmp < 0 then       (* locked < cursor *)
 261             forward_until_cursor ()
 262           else if cmp > 0 then  (* locked > cursor *)
 263             back_until_cursor ()
 264           else                  (* cursor = locked *)
 265               ()
 266         with Margin -> ())
 267
 268   method onGoingProof () =
 269     match self#status.proof_status with
 270     | No_proof | Proof _ -> false
 271     | Incomplete_proof _ -> true
 272     | Intermediate _ -> assert false
 273
 274   method proofStatus = MatitaMisc.get_proof_status self#status
 275   method proofMetasenv = MatitaMisc.get_proof_metasenv self#status
 276   method proofContext = MatitaMisc.get_proof_context self#status
 277   method setGoal n = userGoal <- n
 278
 279   (* debug *)
 280   method dump () =
 281     MatitaLog.debug "script status:";
 282     MatitaLog.debug ("history size: " ^ string_of_int (List.length history));
 283     MatitaLog.debug (sprintf "%d statements:" (List.length statements));
 284     List.iter MatitaLog.debug statements;
 285
 286 end
 287
 288 let _script = ref None
 289
 290 let script ~buffer ~init ~mathviewer () =
 291   let s = new script ~buffer ~init ~mathviewer () in
 292   _script := Some s;
 293   s
 294
 295 let instance () = match !_script with None -> assert false | Some s -> s
 296
 297