From 6b8da04f526b3484dc92f61a23a8e61e63422c13 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 18 May 2005 14:34:40 +0000 Subject: [PATCH] fixed some macros, added test_abort.ma --- helm/matita/matita.txt | 13 +++--- helm/matita/matitaMathView.ml | 23 ++++++---- helm/matita/matitaScript.ml | 77 +++++++++++++++++++++++---------- helm/matita/tests/test3.ma | 8 ++++ helm/matita/tests/test_abort.ma | 16 +++++++ 5 files changed, 100 insertions(+), 37 deletions(-) create mode 100644 helm/matita/tests/test_abort.ma diff --git a/helm/matita/matita.txt b/helm/matita/matita.txt index 62f133675..05c28af47 100644 --- a/helm/matita/matita.txt +++ b/helm/matita/matita.txt @@ -9,14 +9,15 @@ TODO - menu contestuale (tasto dx) nel sequent viewer -> - controllo per script modificato o meno prima di uscire -> - riattaccare hbugs (brrr...) -> Zack -- spostare il codice di creazione delle tabelle da - MatitaDb, al momento quelle create da matita possono - andare out of sync con quelle create dai file .sql -- commenti exeguibili (forse devono essere una lista e non - un singolo executable e forse devono contenere anche Note - e non solo Executable DONE +- history deve aggiornare anche la whelp bar -> Gares +- commenti exeguibili (forse devono essere una lista e non + un singolo executable e forse devono contenere anche Note + e non solo Executable) -> Gares +- spostare il codice di creazione delle tabelle da + MatitaDb, al momento quelle create da matita possono + andare out of sync con quelle create dai file .sql -> Gares - tree update in background -> Gares - update del getter in background -> Zack - agganciare href_callback del sequent_viewer -> Zack diff --git a/helm/matita/matitaMathView.ml b/helm/matita/matitaMathView.ml index df10be563..5fe955b3e 100644 --- a/helm/matita/matitaMathView.ml +++ b/helm/matita/matitaMathView.ml @@ -307,6 +307,15 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) combo#set_active (aux 0 queries); win#queryInputText#set_text input in + let set_whelp_query txt = + let query, arg = + try + let q = Pcre.extract ~rex:whelp_query_RE txt in + q.(1), q.(2) + with Invalid_argument _ -> failwith "Malformed Whelp query" + in + activate_combo_query arg query + in let toplevel = win#toplevel in let mathView = sequentViewer ~packing:win#scrolledBrowser#add () in let fail msg = @@ -449,7 +458,9 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) | `Cic (term, metasenv) -> self#_loadTermCic term metasenv | `Dir dir -> self#_loadDir dir | `Uri uri -> self#_loadUriManagerUri (UriManager.uri_of_string uri) - | `Whelp (query, results) -> self#_loadList results); + | `Whelp (query, results) -> + set_whelp_query query; + self#_loadList results); self#setEntry entry end with @@ -556,13 +567,9 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) let is_whelp txt = Pcre.pmatch ~rex:whelp_RE txt in if is_whelp txt then begin - let q = Pcre.extract ~rex:whelp_query_RE txt in - let query, arg = - try - q.(1), q.(2) - with Invalid_argument _ -> failwith "Malformed Whelp query" - in - activate_combo_query arg query; + set_whelp_query txt; + + (MatitaScript.instance ())#advance ~statement:(txt^".") () end else diff --git a/helm/matita/matitaScript.ml b/helm/matita/matitaScript.ml index 9842ffdce..0d59d6f47 100644 --- a/helm/matita/matitaScript.ml +++ b/helm/matita/matitaScript.ml @@ -100,7 +100,7 @@ let eval_with_engine status user_goal parsed_text st = else new_text in - [ new_status, new_text ], parsed_text_length + [ new_status, new_text ], parsed_text_length, None let disambiguate term status = let module MD = MatitaDisambiguator in @@ -113,13 +113,16 @@ let disambiguate term status = | [_,_,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 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 @@ -129,18 +132,18 @@ let eval_macro status (mathviewer:MatitaTypes.mathViewer) urichooser parsed_text 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 + [], parsed_text_length, None | 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 + [], parsed_text_length, None | 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 + [], parsed_text_length, None | TA.WElim (loc, term) -> let term = disambiguate term status in let uri = @@ -151,21 +154,21 @@ let eval_macro status (mathviewer:MatitaTypes.mathViewer) urichooser parsed_text 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 + [], parsed_text_length, None | 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 + [], parsed_text_length, None (* 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 + | [] -> [], parsed_text_length, None | [uri] -> let ast = (TA.Executable (loc, @@ -178,7 +181,7 @@ let eval_macro status (mathviewer:MatitaTypes.mathViewer) urichooser parsed_text comment parsed_text ^ "\n" ^ TAPp.pp_statement ast in - [ new_status , extra_text ],parsed_text_length + [ new_status , extra_text ], parsed_text_length, None | _ -> assert false) | TA.Check (_,term) -> let metasenv = MatitaMisc.get_proof_metasenv status in @@ -196,13 +199,32 @@ let eval_macro status (mathviewer:MatitaTypes.mathViewer) urichooser parsed_text 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.Quit _ -> - failwith "not implemented quit" - | _ -> failwith "not implemented" + [], parsed_text_length, None + | TA.Abort _ -> + let rec go_back () = + let status = script#status.proof_status in + match status with + | No_proof -> () + | _ -> script#retract ();go_back() + in + [], 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 @@ -211,9 +233,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 = @@ -226,14 +249,17 @@ 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, act = + 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) + ((status, parsed_text ^ text)::tl), (parsed_text_length + len), act + | [] -> [], 0, None) | 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) @@ -264,8 +290,8 @@ 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) = - eval_statement self#status mathviewer urichooser userGoal s in + let (entries, parsed_len, post_advance_action) = + eval_statement self#status mathviewer urichooser userGoal self s in let (new_statuses, new_statements) = List.split entries in (* prerr_endline "evalStatement returned"; @@ -281,6 +307,9 @@ List.iter (fun s -> prerr_endline ("'" ^ s ^ "'")) new_statements; 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 () + | _ -> () method private _retract () = match statements, history with @@ -288,7 +317,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 () = @@ -305,6 +334,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 = @@ -315,6 +345,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 = [] diff --git a/helm/matita/tests/test3.ma b/helm/matita/tests/test3.ma index c4aafaf3c..e589c5aaa 100644 --- a/helm/matita/tests/test3.ma +++ b/helm/matita/tests/test3.ma @@ -5,4 +5,12 @@ goal 5. exact nat. intro. reflexivity. +qed. +alias num (instance 0) = "natural number". +alias symbol "times" (instance 0) = "natural times". + +theorem b:\forall p:nat. p * 0=0. +intro. +auto. +abort. qed. \ No newline at end of file diff --git a/helm/matita/tests/test_abort.ma b/helm/matita/tests/test_abort.ma new file mode 100644 index 000000000..e589c5aaa --- /dev/null +++ b/helm/matita/tests/test_abort.ma @@ -0,0 +1,16 @@ +alias symbol "eq" (instance 0) = "leibnitz's equality". +theorem a:\forall x.x=x. +alias id "nat" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)". +goal 5. +exact nat. +intro. +reflexivity. +qed. +alias num (instance 0) = "natural number". +alias symbol "times" (instance 0) = "natural times". + +theorem b:\forall p:nat. p * 0=0. +intro. +auto. +abort. +qed. \ No newline at end of file -- 2.39.2