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