X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaScript.ml;h=af38ff8c2c86589f306cfcdcebb2cf644f12a7ff;hb=7aa0e7901b71a660c6d6f55d96a38a3a9d1d3c7d;hp=0d59d6f47fcfc9ba8b8e4031658bf382fcfe76dd;hpb=6b8da04f526b3484dc92f61a23a8e61e63422c13;p=helm.git diff --git a/helm/matita/matitaScript.ml b/helm/matita/matitaScript.ml index 0d59d6f47..af38ff8c2 100644 --- a/helm/matita/matitaScript.ml +++ b/helm/matita/matitaScript.ml @@ -24,9 +24,11 @@ *) open Printf - open MatitaTypes +let debug = true +let debug_print = if debug then prerr_endline else ignore + (** raised when one of the script margins (top or bottom) is reached *) exception Margin @@ -75,16 +77,35 @@ let eval_with_engine status user_goal parsed_text st = match status.proof_status with | Incomplete_proof (_, goal) when goal <> user_goal -> goal_changed := true; - MatitaEngine.eval_ast status (goal_ast user_goal) + MatitaEngine.eval_ast + ~do_heavy_checks:true status (goal_ast user_goal) | _ -> status in - let new_status = MatitaEngine.eval_ast status st in + let new_status = MatitaEngine.eval_ast ~do_heavy_checks:true status st in let new_aliases = match ex with - | TA.Command (_, TA.Alias _) -> - DisambiguateTypes.Environment.empty + | TA.Command (_, TA.Alias _) + | TA.Command (_, TA.Include _) -> DisambiguateTypes.Environment.empty | _ -> MatitaSync.alias_diff ~from:status new_status in + (* we remove the defined object since we consider them "automathic aliases" *) + let new_aliases = + let module DTE = DisambiguateTypes.Environment in + let module UM = UriManager in + DTE.fold ( + fun k ((v,_) as value) acc -> + let b = + try + let v = UM.strip_xpointer (UM.uri_of_string v) in + List.exists (fun (s,_) -> s = v) new_status.objects + with UM.IllFormedUri _ -> false + in + if b then + acc + else + DTE.add k value acc + ) new_aliases DTE.empty + in let new_text = if DisambiguateTypes.Environment.is_empty new_aliases then parsed_text @@ -100,7 +121,7 @@ let eval_with_engine status user_goal parsed_text st = else new_text in - [ new_status, new_text ], parsed_text_length, None + [ new_status, new_text ], parsed_text_length let disambiguate term status = let module MD = MatitaDisambiguator in @@ -113,8 +134,9 @@ let disambiguate term status = | [_,_,x,_] -> x | _ -> assert false -let eval_macro status (mathviewer:MatitaTypes.mathViewer) urichooser parsed_text -script mac = +let eval_macro status (mathviewer:MatitaTypes.mathViewer) urichooser + parsed_text script mac += let module TA = TacticAst in let module TAPp = TacticAstPp in let module MQ = MetadataQuery in @@ -132,57 +154,63 @@ script mac = let l = MQ.match_term ~dbd term in let entry = `Whelp (TAPp.pp_macro_cic (TA.WMatch (loc, term)), l) in mathviewer#show_uri_list ~reuse:true ~entry l; - [], parsed_text_length, None + [], parsed_text_length | TA.WInstance (loc, term) -> let term = disambiguate term status in let l = MQ.instance ~dbd term in let entry = `Whelp (TAPp.pp_macro_cic (TA.WInstance (loc, term)), l) in mathviewer#show_uri_list ~reuse:true ~entry l; - [], parsed_text_length, None + [], parsed_text_length | TA.WLocate (loc, s) -> let l = MQ.locate ~dbd s in let entry = `Whelp (TAPp.pp_macro_cic (TA.WLocate (loc, s)), l) in mathviewer#show_uri_list ~reuse:true ~entry l; - [], parsed_text_length, None + [], parsed_text_length | TA.WElim (loc, term) -> let term = disambiguate term status in let uri = match term with - | Cic.MutInd (uri,n,_) -> UriManager.string_of_uriref (uri,[n]) + | Cic.MutInd (uri,n,_) -> UriManager.uri_of_uriref uri n None | _ -> failwith "Not a MutInd" in let l = MQ.elim ~dbd uri in let entry = `Whelp (TAPp.pp_macro_cic (TA.WElim (loc, term)), l) in mathviewer#show_uri_list ~reuse:true ~entry l; - [], parsed_text_length, None + [], parsed_text_length | TA.WHint (loc, term) -> let term = disambiguate term status in let s = ((None,[0,[],term], Cic.Meta (0,[]) ,term),0) in let l = List.map fst (MQ.experimental_hint ~dbd s) in let entry = `Whelp (TAPp.pp_macro_cic (TA.WHint (loc, term)), l) in mathviewer#show_uri_list ~reuse:true ~entry l; - [], parsed_text_length, None + [], parsed_text_length (* REAL macro *) | TA.Hint loc -> let s = MatitaMisc.get_proof_status status in let l = List.map fst (MQ.experimental_hint ~dbd s) in let selected = urichooser l in (match selected with - | [] -> [], parsed_text_length, None + | [] -> [], parsed_text_length | [uri] -> let ast = - (TA.Executable (loc, - (TA.Tactical (loc, - TA.Tactic (loc, - TA.Apply (loc, CicAst.Uri (uri,None))))))) + TA.Executable (loc, + (TA.Tactical (loc, + TA.Tactic (loc, + TA.Apply (loc, CicAst.Uri (UriManager.string_of_uri uri,None)))))) in let new_status = MatitaEngine.eval_ast status ast in let extra_text = comment parsed_text ^ "\n" ^ TAPp.pp_statement ast in - [ new_status , extra_text ], parsed_text_length, None - | _ -> assert false) + [ new_status , extra_text ], parsed_text_length + | _ -> + MatitaLog.error + "The result of the urichooser should be only 1 uri, not:\n"; + List.iter ( + fun u -> MatitaLog.error (UriManager.string_of_uri u ^ "\n") + ) selected; + assert false) | TA.Check (_,term) -> let metasenv = MatitaMisc.get_proof_metasenv status in let context = MatitaMisc.get_proof_context status in @@ -199,8 +227,8 @@ script mac = let ty,_ = CTC.type_of_aux' metasenv context term ugraph in let t_and_ty = Cic.Cast (term,ty) in mathviewer#show_entry (`Cic (t_and_ty,metasenv)); - [], parsed_text_length, None - | TA.Abort _ -> + [], parsed_text_length +(* | TA.Abort _ -> let rec go_back () = let status = script#status.proof_status in match status with @@ -215,7 +243,7 @@ script mac = | TA.Undo (_, Some i) -> [], parsed_text_length, Some (fun () -> for j = 1 to i do script#retract () done) | TA.Undo (_, None) -> [], parsed_text_length, - Some (fun () -> script#retract ()) + Some (fun () -> script#retract ()) *) (* TODO *) | TA.Quit _ -> failwith "not implemented" | TA.Print (_,kind) -> failwith "not implemented" @@ -224,19 +252,37 @@ script mac = let eval_executable status (mathviewer:MatitaTypes.mathViewer) urichooser -user_goal parsed_text script ex = +ask_confirmation user_goal parsed_text script ex = let module TA = TacticAst in let module TAPp = TacticAstPp in let module MD = MatitaDisambiguator in + let module ML = MatitacleanLib in let parsed_text_length = String.length parsed_text in match ex with | TA.Command (loc, _) | TA.Tactical (loc, _) -> - eval_with_engine status user_goal parsed_text (TA.Executable (loc, ex)) + (try + (match ML.baseuri_of_baseuri_decl (TA.Executable (loc,ex)) with + | None -> () + | Some u -> + if not (MatitacleanLib.is_empty u) then + match + ask_confirmation + ~title:"Baseuri redefinition" + ~message:( + "Baseuri " ^ u ^ " already exists.\n" ^ + "Do you want to redefine the corresponding "^ + "part of the library?") + with + | `YES -> MatitacleanLib.clean_baseuris [u] + | `NO -> () + | `CANCEL -> raise MatitaTypes.Cancel); + eval_with_engine status user_goal parsed_text (TA.Executable (loc, ex)) + with MatitaTypes.Cancel -> [], 0) | TA.Macro (_,mac) -> eval_macro status mathviewer urichooser parsed_text script mac let rec eval_statement status (mathviewer:MatitaTypes.mathViewer) urichooser -user_goal script s = +ask_confirmation user_goal script s = if Pcre.pmatch ~rex:only_dust_RE s then raise Margin; let st = CicTextualParser2.parse_statement (Stream.of_string s) in let text_of_loc loc = @@ -249,24 +295,47 @@ user_goal script s = let parsed_text, parsed_text_length = text_of_loc loc in let remain_len = String.length s - parsed_text_length in let s = String.sub s parsed_text_length remain_len in - let s,len, act = - eval_statement status mathviewer urichooser user_goal script s + let s,len = + eval_statement status + mathviewer urichooser ask_confirmation user_goal script s in (match s with | (status, text) :: tl -> - ((status, parsed_text ^ text)::tl), (parsed_text_length + len), act - | [] -> [], 0, None) + ((status, parsed_text ^ text)::tl), (parsed_text_length + len) + | [] -> [], 0) | TacticAst.Executable (loc, ex) -> let parsed_text, parsed_text_length = text_of_loc loc in eval_executable - status mathviewer urichooser user_goal parsed_text script ex + status mathviewer urichooser ask_confirmation + user_goal parsed_text script ex +let fresh_script_id = + let i = ref 0 in + fun () -> incr i; !i class script ~(buffer: GText.buffer) ~(init: MatitaTypes.status) ~(mathviewer: MatitaTypes.mathViewer) + ~set_star + ~ask_confirmation ~urichooser () = object (self) - initializer self#reset () + val mutable filename = None + val scriptId = fresh_script_id () + method private getFilename = + match filename with Some f -> f | _ -> assert false + method private ppFilename = + match filename with Some f -> f | None -> sprintf ".unnamed%d.ma" scriptId + + initializer + ignore(GMain.Timeout.add ~ms:300000 + ~callback:(fun _ -> self#_saveToBackuptFile ();true)); + ignore(buffer#connect#modified_changed + (fun _ -> if buffer#modified then + set_star self#ppFilename true + else + set_star self#ppFilename false)); + self#reset (); + self#template () val mutable statements = []; (** executed statements *) val mutable history = [ init ]; @@ -277,6 +346,7 @@ object (self) (** goal as seen by the user (i.e. metano corresponding to current tab) *) val mutable userGoal = ~-1 + val mutable lock_mark_pos = 0 (** text mark and tag representing locked part of a script *) val locked_mark = @@ -290,8 +360,10 @@ object (self) method private _advance ?statement () = let s = match statement with Some s -> s | None -> self#getFuture in MatitaLog.debug ("evaluating: " ^ first_line s ^ " ..."); - let (entries, parsed_len, post_advance_action) = - eval_statement self#status mathviewer urichooser userGoal self s in + let (entries, parsed_len) = + eval_statement self#status + mathviewer urichooser ask_confirmation userGoal self s + in let (new_statuses, new_statements) = List.split entries in (* prerr_endline "evalStatement returned"; @@ -300,16 +372,17 @@ 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); - match post_advance_action with - | Some f -> f () - | _ -> () + if new_text <> String.sub s 0 parsed_len then + begin +(* prerr_endline ("new:" ^ new_text); *) +(* prerr_endline ("s:" ^ String.sub s 0 parsed_len); *) + let stop = start#copy#forward_chars parsed_len in + buffer#delete ~start ~stop; + buffer#insert ~iter:start new_text; +(* prerr_endline "AUTOMATICALLY MODIFIED!!!!!" *) + end; + self#moveMark (String.length new_text) method private _retract () = match statements, history with @@ -322,15 +395,25 @@ List.iter (fun s -> prerr_endline ("'" ^ s ^ "'")) new_statements; method advance ?statement () = try - self#_advance ?statement () - with Margin -> () + self#_advance ?statement (); + self#notify + with + | Margin -> self#notify + | exc -> self#notify; raise exc - method retract () = try self#_retract () with Margin -> () + method retract () = + try + self#_retract (); + self#notify + with + | Margin -> self#notify + | exc -> self#notify; raise exc 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 @@ -345,8 +428,19 @@ List.iter (fun s -> prerr_endline ("'" ^ s ^ "'")) new_statements; in buffer#move_mark mark ~where:new_mark_pos; buffer#apply_tag locked_tag ~start:buffer#start_iter ~stop:new_mark_pos; + lock_mark_pos <- new_mark_pos#offset; buffer#move_mark `INSERT old_insert; - self#notify + begin + match self#status.proof_status with + Incomplete_proof (_,goal) -> self#setGoal goal + | _ -> () + end ; + while Glib.Main.pending () do ignore(Glib.Main.iteration false); done + + method clean_dirty_lock = + let lock_mark_iter = buffer#get_iter (`OFFSET lock_mark_pos) in + buffer#remove_tag locked_tag ~start:buffer#start_iter ~stop:buffer#end_iter; + buffer#apply_tag locked_tag ~start:buffer#start_iter ~stop:lock_mark_iter val mutable observers = [] @@ -357,34 +451,69 @@ List.iter (fun s -> prerr_endline ("'" ^ s ^ "'")) new_statements; 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 + method loadFromFile () = + buffer#set_text (MatitaMisc.input_file self#getFilename); + self#goto_top; + buffer#set_modified false + + method assignFileName file = + filename <- Some file; + + method saveToFile () = + let oc = open_out self#getFilename in output_string oc (buffer#get_text ~start:buffer#start_iter ~stop:buffer#end_iter ()); - close_out oc - + close_out oc; + buffer#set_modified false + + method private _saveToBackuptFile () = + if buffer#modified then + begin + let f = self#ppFilename ^ "~" in + let oc = open_out f in + output_string oc (buffer#get_text ~start:buffer#start_iter + ~stop:buffer#end_iter ()); + close_out oc; + MatitaLog.debug ("backup " ^ f ^ " saved") + end + 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 + buffer#delete ~start:buffer#start_iter ~stop:buffer#end_iter; + self#notify; + buffer#set_modified false + + method template () = + let template = MatitaMisc.input_file BuildTimeConf.script_template in + buffer#insert ~iter:(buffer#get_iter `START) template; + filename <- None; + buffer#set_modified false; + set_star self#ppFilename false method goto (pos: [`Top | `Bottom | `Cursor]) () = match pos with - | `Top -> self#goto_top + | `Top -> self#goto_top; self#notify | `Bottom -> - (try while true do self#_advance () done with Margin -> ()) + (try + let getpos _ = buffer#get_iter_at_mark (`MARK locked_mark) in + let rec dowhile pos = + self#_advance (); + if pos#compare (getpos ()) < 0 then + dowhile (getpos ()) + in + dowhile (getpos ()); + self#notify + with + | Margin -> self#notify + | exc -> self#notify; raise exc) | `Cursor -> let locked_iter () = buffer#get_iter_at_mark (`NAME "locked") in let cursor_iter () = buffer#get_iter_at_mark `INSERT in @@ -401,13 +530,15 @@ List.iter (fun s -> prerr_endline ("'" ^ s ^ "'")) new_statements; let cmp = (locked_iter ())#compare (cursor_iter ()) in (try if cmp < 0 then (* locked < cursor *) - forward_until_cursor () + (forward_until_cursor (); self#notify) else if cmp > 0 then (* locked > cursor *) - back_until_cursor () + (back_until_cursor (); self#notify) else (* cursor = locked *) () - with Margin -> ()) - + with + | Margin -> self#notify + | exc -> self#notify; raise exc) + method onGoingProof () = match self#status.proof_status with | No_proof | Proof _ -> false @@ -419,19 +550,45 @@ List.iter (fun s -> prerr_endline ("'" ^ s ^ "'")) new_statements; method proofContext = MatitaMisc.get_proof_context self#status method setGoal n = userGoal <- n + method eos = + let s = self#getFuture in + let rec is_there_and_executable s = + if Pcre.pmatch ~rex:only_dust_RE s then raise Margin; + let st = CicTextualParser2.parse_statement (Stream.of_string s) in + match st with + | TacticAst.Comment (loc,_)-> + let parsed_text_length = snd (CicAst.loc_of_floc loc) in + let remain_len = String.length s - parsed_text_length in + let next = String.sub s parsed_text_length remain_len in + is_there_and_executable next + | TacticAst.Executable (loc, ex) -> false + in + try + is_there_and_executable s + with + | CicTextualParser2.Parse_error _ -> false + | Margin -> true + + + (* 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; + MatitaLog.debug ("Current file name: " ^ + (match filename with None -> "[ no name ]" | Some f -> f)); end let _script = ref None -let script ~buffer ~init ~mathviewer ~urichooser () = - let s = new script ~buffer ~init ~mathviewer ~urichooser () in +let script ~buffer ~init ~mathviewer ~urichooser ~ask_confirmation ~set_star () += + let s = new script + ~buffer ~init ~mathviewer ~ask_confirmation ~urichooser ~set_star () + in _script := Some s; s