fixed some macros, added test_abort.ma

diff --git a/helm/matita/matita.txt b/helm/matita/matita.txt
index 62f13367539deb44234e01007a56c025b7720bbb..05c28af47aaf62196e88b952518b9b0cbe6952db 100644 (file)
--- 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 df10be56336e7b55917180c1e7ad6ae2b47f6cbd..5fe955b3ea5f8124e428b0a7fd28f1815472ee26 100644 (file)
--- 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 9842ffdce7c05a13a9f933f4b6f758367daf0834..0d59d6f47fcfc9ba8b8e4031658bf382fcfe76dd 100644 (file)
--- 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 c4aafaf3c6f64390c0300878d645bae933c0ceb1..e589c5aaa8361b84978069f14514ac901df5e852 100644 (file)
--- 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 (file)
index 0000000..e589c5a
--- /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