added 'rewrite' option to the the hint macro. a cicBrowser with all library

objects that may rewrite the goal is displayed.

diff --git a/components/grafite/grafiteAst.ml b/components/grafite/grafiteAst.ml
index b8a89e1b6d885bf7293c8e5221f8d39e66eac22f..d5eb9c241259efcb7fc1ff0e24d328b92f68bad8 100644 (file)
--- a/components/grafite/grafiteAst.ml
+++ b/components/grafite/grafiteAst.ml
@@ -126,14 +126,14 @@ type presentation_style = Declarative
 
 type 'term macro = 
   (* Whelp's stuff *)
-  | WHint of loc * 'term 
+  | WHint of loc * 'term
   | WMatch of loc * 'term 
   | WInstance of loc * 'term 
   | WLocate of loc * string
   | WElim of loc * 'term
   (* real macros *)
   | Check of loc * 'term 
-  | Hint of loc
+  | Hint of loc * bool
   | AutoInteractive of loc * (string * string) list
   | Inline of loc * presentation_style * string * string 
      (* URI or base-uri, name prefix *) 

diff --git a/components/grafite/grafiteAstPp.ml b/components/grafite/grafiteAstPp.ml
index 0b448659484067634158e73c91f023b0c6c02956..14b7d180ca15ef61a41e86f969a527b2945731e1 100644 (file)
--- a/components/grafite/grafiteAstPp.ml
+++ b/components/grafite/grafiteAstPp.ml
@@ -239,7 +239,8 @@ let pp_macro ~term_pp =
   | WMatch (_, term) -> "whelp match " ^ term_pp term
   (* real macros *)
   | Check (_, term) -> Printf.sprintf "check %s" (term_pp term)
-  | Hint _ -> "hint"
+  | Hint (_, true) -> "hint rewrite"
+  | Hint (_, false) -> "hint"
   | AutoInteractive (_,params) -> "auto " ^ 
       String.concat " " 
         (List.map (fun (k,v) -> if v <> "" then k ^ "=" ^ v else k) params)

diff --git a/components/grafite_parser/grafiteParser.ml b/components/grafite_parser/grafiteParser.ml
index 24d1b3feb441b864d977807b931196e1c3ea33f5..e2108381200b82ae16626d0a61fd11bafc419ac3 100644 (file)
--- a/components/grafite_parser/grafiteParser.ml
+++ b/components/grafite_parser/grafiteParser.ml
@@ -459,7 +459,8 @@ EXTEND
         in
         let prefix = match prefix with None -> "" | Some prefix -> prefix in
         GrafiteAst.Inline (loc,style,suri,prefix)
-    | [ IDENT "hint" ] -> GrafiteAst.Hint loc
+    | [ IDENT "hint" ]; rew = OPT (IDENT "rewrite")  -> 
+         if rew = None then GrafiteAst.Hint (loc, false) else GrafiteAst.Hint (loc,true)
     | IDENT "auto"; params = auto_params ->
         GrafiteAst.AutoInteractive (loc,params)
     | [ IDENT "whelp"; "match" ] ; t = term -> 

diff --git a/matita/matitaScript.ml b/matita/matitaScript.ml
index fca45c02628132a700ef92bcf3fd913da19e40f1..a007e70237913407bf3fc42e4fdb9444679fcf4a 100644 (file)
--- a/matita/matitaScript.ml
+++ b/matita/matitaScript.ml
@@ -478,7 +478,7 @@ let rec eval_macro include_paths (buffer : GText.buffer) guistuff lexicon_status
      guistuff.mathviewer#show_uri_list ~reuse:true ~entry l;
      [], "", parsed_text_length
   (* REAL macro *)
-  | TA.Hint loc -> 
+  | TA.Hint (loc, rewrite) -> 
       let user_goal' =
        match user_goal with
           Some n -> n
@@ -486,38 +486,44 @@ let rec eval_macro include_paths (buffer : GText.buffer) guistuff lexicon_status
       in
       let proof = GrafiteTypes.get_current_proof grafite_status in
       let proof_status = proof,user_goal' in
-      let l = List.map fst (MQ.experimental_hint ~dbd proof_status) in
-      let selected = guistuff.urichooser l in
-      (match selected with
-      | [] -> [], "", parsed_text_length
-      | [uri] -> 
-          let suri = UriManager.string_of_uri uri in
-          let ast loc =
-            TA.Executable (loc, (TA.Tactic (loc,
-             Some (TA.Apply (loc, CicNotationPt.Uri (suri, None))),
-             TA.Dot loc))) in
-          let text =
-           comment parsed_text ^ "\n" ^
-            pp_eager_statement_ast (ast HExtlib.dummy_floc)
-            ~map_unicode_to_tex:(Helm_registry.get_bool
-              "matita.paste_unicode_as_tex")
-          in
-          let text_len = MatitaGtkMisc.utf8_string_length text in
-          let loc = HExtlib.floc_of_loc (0,text_len) in
-          let statement = `Ast (GrafiteParser.LSome (ast loc),text) in
-          let res,_,_parsed_text_len =
-           eval_statement include_paths buffer guistuff lexicon_status
-            grafite_status user_goal script statement
-          in
-           (* we need to replace all the parsed_text *)
-           res,"",String.length parsed_text
-      | _ -> 
-          HLog.error 
-            "The result of the urichooser should be only 1 uri, not:\n";
-          List.iter (
-            fun u -> HLog.error (UriManager.string_of_uri u ^ "\n")
-          ) selected;
-          assert false)
+      if rewrite then
+        let l = MQ.equations_for_goal ~dbd proof_status in
+        let entry = `Whelp (pp_macro (TA.WHint(loc, Cic.Implicit None)), l) in
+        guistuff.mathviewer#show_uri_list ~reuse:true ~entry l;
+        [], "", parsed_text_length
+      else
+        let l = List.map fst (MQ.experimental_hint ~dbd proof_status) in
+        let selected = guistuff.urichooser l in
+        (match selected with
+        | [] -> [], "", parsed_text_length
+        | [uri] -> 
+            let suri = UriManager.string_of_uri uri in
+            let ast loc =
+              TA.Executable (loc, (TA.Tactic (loc,
+               Some (TA.Apply (loc, CicNotationPt.Uri (suri, None))),
+               TA.Dot loc))) in
+            let text =
+             comment parsed_text ^ "\n" ^
+              pp_eager_statement_ast (ast HExtlib.dummy_floc)
+              ~map_unicode_to_tex:(Helm_registry.get_bool
+                "matita.paste_unicode_as_tex")
+            in
+            let text_len = MatitaGtkMisc.utf8_string_length text in
+            let loc = HExtlib.floc_of_loc (0,text_len) in
+            let statement = `Ast (GrafiteParser.LSome (ast loc),text) in
+            let res,_,_parsed_text_len =
+             eval_statement include_paths buffer guistuff lexicon_status
+              grafite_status user_goal script statement
+            in
+             (* we need to replace all the parsed_text *)
+             res,"",String.length parsed_text
+        | _ -> 
+            HLog.error 
+              "The result of the urichooser should be only 1 uri, not:\n";
+            List.iter (
+              fun u -> HLog.error (UriManager.string_of_uri u ^ "\n")
+            ) selected;
+            assert false)
   | TA.Check (_,term) ->
       let metasenv = GrafiteTypes.get_proof_metasenv grafite_status in
       let context =