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