From 594103c3c448e4699d6b6195d39d6adbdef953af Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 30 Jul 2007 12:00:31 +0000 Subject: [PATCH] added 'rewrite' option to the the hint macro. a cicBrowser with all library objects that may rewrite the goal is displayed. --- components/grafite/grafiteAst.ml | 4 +- components/grafite/grafiteAstPp.ml | 3 +- components/grafite_parser/grafiteParser.ml | 3 +- matita/matitaScript.ml | 72 ++++++++++++---------- 4 files changed, 45 insertions(+), 37 deletions(-) diff --git a/components/grafite/grafiteAst.ml b/components/grafite/grafiteAst.ml index b8a89e1b6..d5eb9c241 100644 --- 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 0b4486594..14b7d180c 100644 --- 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 24d1b3feb..e21083812 100644 --- 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 fca45c026..a007e7023 100644 --- 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 = -- 2.39.2