X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaScript.ml;h=043fc31e43d45825f621dd485494645751b687f6;hb=ded3a0b12793fc8e463a4a3be9f62f54f734897e;hp=fed62fbb321c4e73b45a4b59b82e0e9c017386f9;hpb=de4483296d06aac3df4da10d5401b1f97c4350ab;p=helm.git diff --git a/helm/matita/matitaScript.ml b/helm/matita/matitaScript.ml index fed62fbb3..043fc31e4 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 @@ -85,6 +87,24 @@ let eval_with_engine status user_goal parsed_text st = 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 @@ -101,18 +121,72 @@ let eval_with_engine status user_goal parsed_text st = new_text in [ new_status, new_text ], parsed_text_length + +let disambiguate term status = + let module MD = MatitaDisambiguator in + let dbd = MatitaDb.instance () in + 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 interps = MD.disambiguate_term dbd context metasenv aliases term in + match interps with + | [_,_,x,_] -> x + | _ -> assert false -let eval_macro status (mathviewer:MatitaTypes.mathViewer) urichooser parsed_text 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 - let module MD = MatitaDisambiguator in let module MDB = MatitaDb in + let module CTC = CicTypeChecker in + let module CU = CicUniv in + (* no idea why ocaml wants this *) + let advance ?statement () = script#advance ?statement () in let parsed_text_length = String.length parsed_text in + let dbd = MatitaDb.instance () in match mac with + (* WHELP's stuff *) + | TA.WMatch (loc, term) -> + let term = disambiguate term status in + 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 + | 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 + | 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 + | TA.WElim (loc, term) -> + let term = disambiguate term status in + let uri = + match term with + | 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 + | 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 + (* REAL macro *) | TA.Hint loc -> let s = MatitaMisc.get_proof_status status in - let l = List.map fst (MQ.experimental_hint ~dbd:(MDB.instance ()) s) in + let l = List.map fst (MQ.experimental_hint ~dbd s) in let selected = urichooser l in (match selected with | [] -> [], parsed_text_length @@ -121,77 +195,63 @@ let eval_macro status (mathviewer:MatitaTypes.mathViewer) urichooser parsed_text (TA.Executable (loc, (TA.Tactical (loc, TA.Tactic (loc, - TA.Apply (loc, CicAst.Uri (uri,None))))))) + 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 - | _ -> assert false) - | TA.Match (_,term) -> - let dbd = MatitaDb.instance () in + [ 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 let aliases = MatitaMisc.get_proof_aliases status in - let (_env,_metasenv,term,_graph) = - let interps = - MD.disambiguate_term dbd context metasenv aliases term - in + let interps = + MatitaDisambiguator.disambiguate_term + dbd context metasenv aliases term + in + let _, metasenv , term, ugraph = match interps with | [x] -> x | _ -> assert false in - let results = MetadataQuery.match_term ~dbd:dbd term in - mathviewer#show_uri_list ~reuse:true ~entry:(`Whelp ("match", results)) - results; + 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 - | TA.Instance (_,term) -> - let dbd = MatitaDb.instance () in - 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 (_env,_metasenv,term,_graph) = - let interps = - MD.disambiguate_term dbd context metasenv aliases term - in - match interps with - | [x] -> x - | _ -> assert false +(* | TA.Abort _ -> + let rec go_back () = + let status = script#status.proof_status in + match status with + | No_proof -> () + | _ -> script#retract ();go_back() in - let results = MetadataQuery.instance ~dbd term in - mathviewer#show_uri_list ~reuse:true - ~entry:(`Whelp ("instance", results)) results; - [], parsed_text_length - - - | TA.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 = - MD.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 - let t_and_ty = Cic.Cast (term,ty) in - mathviewer # show_entry (`Cic (t_and_ty,metasenv)); - [], parsed_text_length - | TA.Quit _ -> - failwith "not implemented quit" - | _ -> failwith "not implemented" + [], parsed_text_length, Some go_back + | TA.Redo (_, Some i) -> [], parsed_text_length, + Some (fun () -> for j = 1 to i do advance () done) + | TA.Redo (_, None) -> [], parsed_text_length, + Some (fun () -> advance ()) + | 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 ()) *) + (* TODO *) + | TA.Quit _ -> failwith "not implemented" + | TA.Print (_,kind) -> failwith "not implemented" + | TA.Search_pat (_, search_kind, str) -> failwith "not implemented" + | TA.Search_term (_, search_kind, term) -> failwith "not implemented" -let eval_executable status (mathviewer:MatitaTypes.mathViewer) urichooser user_goal parsed_text ex = +let eval_executable status (mathviewer:MatitaTypes.mathViewer) urichooser +user_goal parsed_text script ex = let module TA = TacticAst in let module TAPp = TacticAstPp in let module MD = MatitaDisambiguator in @@ -200,9 +260,10 @@ let eval_executable status (mathviewer:MatitaTypes.mathViewer) urichooser user_g | TA.Command (loc, _) | TA.Tactical (loc, _) -> eval_with_engine status user_goal parsed_text (TA.Executable (loc, ex)) | TA.Macro (_,mac) -> - eval_macro status mathviewer urichooser parsed_text mac + eval_macro status mathviewer urichooser parsed_text script mac -let rec eval_statement status (mathviewer:MatitaTypes.mathViewer) urichooser user_goal s = +let rec eval_statement status (mathviewer:MatitaTypes.mathViewer) urichooser +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 = @@ -215,21 +276,36 @@ let rec eval_statement status (mathviewer:MatitaTypes.mathViewer) urichooser use 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 = eval_statement status mathviewer urichooser user_goal s in + let s,len = + eval_statement status mathviewer urichooser user_goal script s + in (match s with | (status, text) :: tl -> ((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 ex + eval_executable + status mathviewer urichooser user_goal parsed_text script ex class script ~(buffer: GText.buffer) ~(init: MatitaTypes.status) ~(mathviewer: MatitaTypes.mathViewer) + ~set_star ~urichooser () = +let std_filename = "unNamed.ma" in object (self) - initializer self#reset () + val mutable filename = std_filename + + initializer + ignore(GMain.Timeout.add ~ms:20000 + ~callback:(fun _ -> self#_saveToBackuptFile ();true)); + ignore(buffer#connect#modified_changed + (fun _ -> if buffer#modified then + set_star filename true + else + set_star filename false)); + self#reset () val mutable statements = []; (** executed statements *) val mutable history = [ init ]; @@ -241,6 +317,7 @@ object (self) (** 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 @@ -254,7 +331,7 @@ object (self) let s = match statement with Some s -> s | None -> self#getFuture in MatitaLog.debug ("evaluating: " ^ first_line s ^ " ..."); let (entries, parsed_len) = - eval_statement self#status mathviewer urichooser userGoal s in + eval_statement self#status mathviewer urichooser userGoal self s in let (new_statuses, new_statements) = List.split entries in (* prerr_endline "evalStatement returned"; @@ -263,13 +340,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); + 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 @@ -277,7 +358,7 @@ List.iter (fun s -> prerr_endline ("'" ^ s ^ "'")) new_statements; MatitaSync.time_travel ~present:cur_status ~past:prev_status; statements <- List.tl statements; history <- List.tl history; - self#moveMark (- (String.length last_statement)) + self#moveMark (- (String.length last_statement)); | _ -> raise Margin method advance ?statement () = @@ -294,6 +375,7 @@ List.iter (fun s -> prerr_endline ("'" ^ s ^ "'")) new_statements; (** @param rel_offset relative offset from current position of locked_mark *) method private moveMark rel_offset = let mark = `MARK locked_mark in + let old_insert = buffer#get_iter_at_mark `INSERT 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 = @@ -304,6 +386,7 @@ 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; + buffer#move_mark `INSERT old_insert; self#notify val mutable observers = [] @@ -315,16 +398,29 @@ 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 filename); + self#goto_top; + buffer#set_modified false + + method assignFileName file = + filename <- file; + + method saveToFile () = + let oc = open_out filename 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 () = + let f = filename ^ "~" 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 file " ^ f ^ " saved") + method private goto_top = MatitaSync.time_travel ~present:self#status ~past:init; statements <- []; @@ -383,13 +479,14 @@ List.iter (fun s -> prerr_endline ("'" ^ s ^ "'")) new_statements; 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: " ^ filename); 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 ~set_star () = + let s = new script ~buffer ~init ~mathviewer ~urichooser ~set_star () in _script := Some s; s