X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaScript.ml;h=2d1c4d702f023c59b83439e69a62126d4cc83667;hb=927b0dc91ca0369dd029c43ffe9258e17908fa38;hp=69334355fc6e60b4c4163276f74e134d72f5de13;hpb=f264827750988795bd85d0eb6a7d3ecf236d224e;p=helm.git diff --git a/helm/matita/matitaScript.ml b/helm/matita/matitaScript.ml index 69334355f..2d1c4d702 100644 --- a/helm/matita/matitaScript.ml +++ b/helm/matita/matitaScript.ml @@ -1,4 +1,4 @@ -(* Copyright (C) 2005, HELM Team. +(* Copyright (C) 2004-2005, HELM Team. * * This file is part of HELM, an Hypertextual, Electronic * Library of Mathematics, developed at the Computer Science @@ -27,186 +27,271 @@ open Printf open MatitaTypes -exception Script_failure of string - -let remove_constant_from_world ~dbd ~uri = - CicEnvironment.remove_obj uri; - MetadataDb.unindex ~dbd ~uri; - let uri = UriManager.string_of_uri uri in - List.iter - (* TODO ZACK remove xml files from disk *) - (fun suffix -> Http_getter.unregister (uri ^ suffix)) - [""; ".body"; ".types"] - -let remove_inductive_def_from_world ~dbd ~uri = - remove_constant_from_world ~dbd ~uri; - let uri = UriManager.string_of_uri uri in - Http_getter.unregister uri; - List.iter - (fun suffix -> - let uri = - Pcre.replace ~pat:"\\.ind$" ~templ:(sprintf "_%s.con" suffix) uri - in - remove_constant_from_world ~dbd ~uri:(UriManager.uri_of_string uri)) - ["ind"; "rec"; "rect"] - -let is_empty = - let rex = Pcre.regexp "^\\s*$" in - fun s -> - Pcre.pmatch ~rex s - -class script ~(interpreter:MatitaTypes.interpreter) () = - let gui = MatitaGui.instance () in - let script = gui#script in - let buf = script#scriptTextView#buffer in - let dbd = MatitaMisc.dbd_instance () in - let rec undo_item = function - | None -> () - | Some item -> - (match item with - | `Tactic -> - let res = - interpreter#evalAst (TacticAst.Command (TacticAst.Undo None)) - in - assert (fst res) - | `Theorem -> - interpreter#setState `Command; - (MatitaMathView.sequents_viewer_instance ())#reset - | `Qed uri - | `Def uri -> remove_constant_from_world ~dbd ~uri - | `Inductive uri -> remove_inductive_def_from_world ~dbd ~uri) - in - object (self) - initializer - let console = (MatitaGui.instance ())#console in - let w f () = ignore (console#wrap_exn (fun () -> f ())) in - ignore (gui#script#scriptWinTopButton#connect#clicked (w self#top)); - ignore (gui#script#scriptWinBottomButton#connect#clicked (w self#bottom)); - ignore (gui#script#scriptWinForwardButton#connect#clicked - (w self#forward)); - ignore (gui#script#scriptWinBackButton#connect#clicked (w self#back)); - ignore (gui#script#scriptWinTopButton#connect#clicked (w self#top)); - ignore (gui#script#scriptWinJumpButton#connect#clicked (w self#jump)) - - val mutable items = [] - - (** {3 text buffer locking} *) - - (** text mark and tag representing locked part of a script *) - val locked_mark = - buf#create_mark ~name:"locked" ~left_gravity:true buf#start_iter - val locked_tag = buf#create_tag [`BACKGROUND "lightblue"; `EDITABLE false] - - (** lock script text view from the beginning to the given offset (in UTF-8 - * characters) *) - method private lockScript offset = - let mark = `MARK locked_mark in - buf#move_mark mark ~where:(buf#get_iter_at_char offset); - buf#remove_tag locked_tag ~start:buf#start_iter ~stop:buf#end_iter; - buf#apply_tag locked_tag ~start:buf#start_iter - ~stop:(buf#get_iter_at_mark mark) - - method win = gui#script - - method loadFrom fname = - buf#set_text (MatitaMisc.input_file fname); - gui#script#scriptWin#show (); - gui#main#showScriptMenuItem#set_active true - - method advance tactical = - let text = "\n" ^ tactical in - buf#insert ~iter:(buf#get_iter_at_mark (`NAME "locked")) text; - let res = self#_forward () in - if not (fst res) then begin - let locked_iter = buf#get_iter_at_mark (`NAME "locked") in - buf#delete ~start:locked_iter - ~stop:(locked_iter#forward_chars (String.length text)); - end; - res - - (** {3 script progress} *) - - method private jump () = - let locked_iter () = buf#get_iter_at_mark (`NAME "locked") in - let cursor_iter = buf#get_iter_at_mark (`NAME "insert") in - let rec forward_until_cursor () = - prerr_endline "forward_until_cursor"; - (* go forward until locked > cursor (or forward fails) *) - let success = - try - fst (self#_forward ~stop:cursor_iter ()) - with - | Script_failure _ | CicTextualParser2.Parse_error _ -> false - in - if success && (locked_iter ())#compare cursor_iter < 0 then - forward_until_cursor () + (** raised when one of the script margins (top or bottom) is reached *) +exception Margin + +let safe_substring s i j = + try String.sub s i j with Invalid_argument _ -> assert false + +let heading_nl_RE = Pcre.regexp "^\\s*\n\\s*" +let blanks_RE = Pcre.regexp "^\\s*$" + +let first_line s = + let s = Pcre.replace ~rex:heading_nl_RE s in + try + let nl_pos = String.index s '\n' in + String.sub s 0 nl_pos + with Not_found -> s + +let prepend_text header base = + if Pcre.pmatch ~rex:heading_nl_RE base then + sprintf "\n%s%s" header base + else + sprintf "%s\n%s" header base + + (** creates a statement AST for the Goal tactic, e.g. "goal 7" *) +let goal_ast n = + let module A = TacticAst in + let loc = CicAst.dummy_floc in + A.Tactical (loc, A.Tactic (loc, A.Goal (loc, n))) + +let eval_statement status mathviewer user_goal s = + let st = CicTextualParser2.parse_statement (Stream.of_string s) in + match st with + | TacticAst.Command (loc, _) | TacticAst.Tactical (loc, _) -> + let parsed_text_length = snd (CicAst.loc_of_floc loc) in + let parsed_text = safe_substring s 0 parsed_text_length in + let goal_changed = ref false in + let status = + match status.proof_status with + | Incomplete_proof (_, goal) when goal <> user_goal -> + goal_changed := true; + MatitaEngine.eval_ast status (goal_ast user_goal) + | _ -> status in - let rec back_until_cursor () = (* go backward until locked < cursor *) - prerr_endline "back_until_cursor"; - let res = self#back () in - if (locked_iter ())#compare cursor_iter > 0 then - back_until_cursor () + let new_status = MatitaEngine.eval_ast status st in + let new_aliases = + match st with + | TacticAst.Command (_, TacticAst.Alias _) -> + DisambiguateTypes.Environment.empty + | _ -> MatitaSync.alias_diff ~from:status new_status in - let cmp = (locked_iter ())#compare cursor_iter in - if cmp < 0 then (* locked < cursor *) - (prerr_endline "locked < cursor"; forward_until_cursor ()) - else if cmp > 0 then (* locked > cursor *) - (prerr_endline "locked > cursor"; back_until_cursor ()) - else (* cursor = locked *) - () - - method private top () = - try while true do self#back () done with Script_failure _ -> () - - method private bottom () = - try - while true do - let res = self#_forward () in - if not (fst res) then raise (Script_failure "error") - done - with Script_failure _ -> () - - method private _forward ?(stop = buf#end_iter) () = - let locked_iter = buf#get_iter_at_mark (`NAME "locked") in - let (success, hide) as res = - let text = buf#get_text ~start:locked_iter ~stop () in - if is_empty text then - raise (Script_failure "at bottom") + let new_text = + if DisambiguateTypes.Environment.is_empty new_aliases then + parsed_text else - interpreter#evalPhrase text + prepend_text (CicTextualParser2.EnvironmentP3.to_string new_aliases) + parsed_text in - if success then begin - let old_offset = locked_iter#offset in - let new_offset = old_offset + interpreter#endOffset in - self#lockScript new_offset; - items <- (interpreter#lastItem, old_offset) :: items - end; - res - - method private forward () = ignore (self#_forward ()) - - method private back () = - (* clean history backward until the first theorem, return offset before - * it and remaning history *) - let rec flush_theorem = function - | (Some `Theorem, offset) :: tl -> offset, tl - | _ :: tl -> flush_theorem tl - | [] -> assert false + let new_text = + if !goal_changed then + prepend_text + (TacticAstPp.pp_tactic (TacticAst.Goal (loc, user_goal))(* ^ "\n"*)) + new_text + else + new_text in - match items with - | [] -> raise (Script_failure "at top") - | (item, last_offset) :: tl -> - undo_item item; - let (last_offset, tl) = - (* if undoing a qed, go back before corresponding theorem *) - match item with - | Some (`Qed _) -> flush_theorem tl - | _ -> last_offset, tl + [ new_status, new_text ], parsed_text_length + | TacticAst.Macro (loc, mac) -> + let parsed_text_length = snd (CicAst.loc_of_floc loc) in + (match mac with (* TODO *) + | TacticAst.Hint _ -> + let s = MatitaMisc.get_proof_status status in + let l = List.map fst + (MetadataQuery.experimental_hint ~dbd:(MatitaDb.instance ()) s) in - items <- tl; - self#lockScript last_offset + List.iter prerr_endline l; + prerr_endline "FINITA LA HINT"; assert false + | TacticAst.Check (_,t) -> + let metasenv = MatitaMisc.get_proof_metasenv status in + let context = MatitaMisc.get_proof_context status in + let aliases = MatitaMisc.get_proof_aliases status in + let db = MatitaDb.instance () in + let (_env,_metasenv,term,_graph) = + let interps = + MatitaDisambiguator.disambiguate_term db context metasenv + aliases t + in + match interps with + | [x] -> x + | _ -> assert false + in + let ty,_ = + CicTypeChecker.type_of_aux' metasenv context term + CicUniv.empty_ugraph + in + mathviewer # show_term (`Cic (ty,metasenv) ); + [ status, "" ] , parsed_text_length + | _ -> failwith "not implemented") + +class script ~(buffer: GText.buffer) ~(init: MatitaTypes.status) + ~(mathviewer: MatitaTypes.mathViewer) () = +object (self) + initializer self#reset () + + val mutable statements = []; (** executed statements *) + val mutable history = [ init ]; + (** list of states before having executed statements. Head element of this + * list is the current state, last element is the state at the beginning of + * the script. + * Invariant: this list length is 1 + length of statements *) + + (** goal as seen by the user (i.e. metano corresponding to current tab) *) + val mutable userGoal = ~-1 + + (** text mark and tag representing locked part of a script *) + val locked_mark = + buffer#create_mark ~name:"locked" ~left_gravity:true buffer#start_iter + val locked_tag = buffer#create_tag [`BACKGROUND "lightblue"; `EDITABLE false] + + (* history can't be empty, the invariant above grant that it contains at + * least the init status *) + method status = match history with hd :: _ -> hd | _ -> assert false + + method private _advance ?statement () = + let s = match statement with Some s -> s | None -> self#getFuture in + if Pcre.pmatch ~rex:blanks_RE s then raise Margin; + MatitaLog.debug ("evaluating: " ^ first_line s ^ " ..."); + let (entries, parsed_len) = + eval_statement self#status mathviewer userGoal s in + let (new_statuses, new_statements) = List.split entries in +(* +prerr_endline "evalStatement returned"; +List.iter (fun s -> prerr_endline ("'" ^ s ^ "'")) new_statements; +*) + history <- List.rev new_statuses @ history; + statements <- List.rev new_statements @ statements; + let start = buffer#get_iter_at_mark (`MARK locked_mark) in + if statement = None then begin + let stop = start#copy#forward_chars parsed_len in + buffer#delete ~start ~stop + end; + let new_text = String.concat "" new_statements in + buffer#insert ~iter:start new_text; + self#moveMark (String.length new_text); + + method private _retract () = + match statements, history with + | last_statement :: _, cur_status :: prev_status :: _ -> + MatitaSync.time_travel ~present:cur_status ~past:prev_status; + statements <- List.tl statements; + history <- List.tl history; + self#moveMark (- (String.length last_statement)) + | _ -> raise Margin + + method advance ?statement () = + try + self#_advance ?statement () + with Margin -> () + + method retract () = try self#_retract () with Margin -> () + + method private getFuture = + buffer#get_text ~start:(buffer#get_iter_at_mark (`MARK locked_mark)) + ~stop:buffer#end_iter () + + (** @param rel_offset relative offset from current position of locked_mark *) + method private moveMark rel_offset = + let mark = `MARK locked_mark in + buffer#remove_tag locked_tag ~start:buffer#start_iter ~stop:buffer#end_iter; + let current_mark_pos = buffer#get_iter_at_mark mark in + let new_mark_pos = + match rel_offset with + | 0 -> current_mark_pos + | n when n > 0 -> current_mark_pos#forward_chars n + | n (* when n < 0 *) -> current_mark_pos#backward_chars (abs n) + in + buffer#move_mark mark ~where:new_mark_pos; + buffer#apply_tag locked_tag ~start:buffer#start_iter ~stop:new_mark_pos; + self#notify + + val mutable observers = [] + + method addObserver (o: MatitaTypes.status -> unit) = + observers <- o :: observers + + method private notify = + let status = self#status in + List.iter (fun o -> o status) observers + + method loadFrom fname = + buffer#set_text (MatitaMisc.input_file fname); + self#goto_top + + method saveTo fname = + let oc = open_out fname in + output_string oc (buffer#get_text ~start:buffer#start_iter + ~stop:buffer#end_iter ()); + close_out oc + + method private goto_top = + MatitaSync.time_travel ~present:self#status ~past:init; + statements <- []; + history <- [ init ]; + userGoal <- ~-1; + self#notify; + buffer#remove_tag locked_tag ~start:buffer#start_iter ~stop:buffer#end_iter; + buffer#move_mark (`MARK locked_mark) ~where:buffer#start_iter + + method reset () = + self#goto_top; + buffer#delete ~start:buffer#start_iter ~stop:buffer#end_iter + + method goto (pos: [`Top | `Bottom | `Cursor]) () = + match pos with + | `Top -> self#goto_top + | `Bottom -> + (try while true do self#_advance () done with Margin -> ()) + | `Cursor -> + let locked_iter () = buffer#get_iter_at_mark (`NAME "locked") in + let cursor_iter () = buffer#get_iter_at_mark `INSERT in + let rec forward_until_cursor () = (* go forward until locked > cursor *) + self#_advance (); + if (locked_iter ())#compare (cursor_iter ()) < 0 then + forward_until_cursor () + in + let rec back_until_cursor () = (* go backward until locked < cursor *) + self#_retract (); + if (locked_iter ())#compare (cursor_iter ()) > 0 then + back_until_cursor () + in + let cmp = (locked_iter ())#compare (cursor_iter ()) in + (try + if cmp < 0 then (* locked < cursor *) + forward_until_cursor () + else if cmp > 0 then (* locked > cursor *) + back_until_cursor () + else (* cursor = locked *) + () + with Margin -> ()) + + method onGoingProof () = + match self#status.proof_status with + | No_proof | Proof _ -> false + | Incomplete_proof _ -> true + | Intermediate _ -> assert false + + method proofStatus = MatitaMisc.get_proof_status self#status + method proofMetasenv = MatitaMisc.get_proof_metasenv self#status + method proofContext = MatitaMisc.get_proof_context self#status + method setGoal n = userGoal <- n + + (* debug *) + method dump () = + MatitaLog.debug "script status:"; + MatitaLog.debug ("history size: " ^ string_of_int (List.length history)); + MatitaLog.debug (sprintf "%d statements:" (List.length statements)); + List.iter MatitaLog.debug statements; + +end + +let _script = ref None + +let script ~buffer ~init ~mathviewer () = + let s = new script ~buffer ~init ~mathviewer () in + _script := Some s; + s - end +let instance () = match !_script with None -> assert false | Some s -> s -let script ~interpreter = new script ~interpreter ()