X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2FmatitaScript.ml;h=c29e15533ef1c6a71a10c06b04a46cec6f95481a;hb=a957099550619f87a58be467b9b11f2ad6501378;hp=f6610911f5ac2ebcb450bde106c46a616ef2fa0b;hpb=8e24e39aed25a2c31fb7073308ee3f0b80c206e6;p=helm.git

diff --git a/matita/matitaScript.ml b/matita/matitaScript.ml
index f6610911f..c29e15533 100644
--- a/matita/matitaScript.ml
+++ b/matita/matitaScript.ml
@@ -402,14 +402,20 @@ let cic2grafite context menv t =
       let pres_term = TermContentPres.pp_ast content_term in
       let dummy_tbl = Hashtbl.create 1 in
       let markup = CicNotationPres.render dummy_tbl pres_term in
-      let s = "(" ^ BoxPp.render_to_string List.hd width markup ^ ")" in
+      let s = "(" ^ BoxPp.render_to_string
+       ~map_unicode_to_tex:(Helm_registry.get_bool
+         "matita.paste_unicode_as_tex")
+       List.hd width markup ^ ")" in
       Pcre.substitute 
         ~pat:"\\\\forall [Ha-z][a-z0-9_]*" ~subst:(fun x -> "\n" ^ x) s
     in
     CicNotationPp.set_pp_term term_pp;
     let lazy_term_pp = fun x -> assert false in
     let obj_pp = CicNotationPp.pp_obj CicNotationPp.pp_term in
-    GrafiteAstPp.pp_statement ~term_pp ~lazy_term_pp ~obj_pp t
+    GrafiteAstPp.pp_statement
+     ~map_unicode_to_tex:(Helm_registry.get_bool
+       "matita.paste_unicode_as_tex")
+     ~term_pp ~lazy_term_pp ~obj_pp t
   in
   let script = String.concat "" (List.map pp ast) in
   prerr_endline script;
@@ -433,7 +439,9 @@ let rec eval_macro include_paths (buffer : GText.buffer) guistuff lexicon_status
     let metasenv = GrafiteTypes.get_proof_metasenv grafite_status in
     TAPp.pp_macro 
       ~term_pp:(fun x -> 
-        ApplyTransformation.txt_of_cic_term max_int metasenv [] (f x))
+        ApplyTransformation.txt_of_cic_term max_int metasenv [] (f x)
+         ~map_unicode_to_tex:(Helm_registry.get_bool
+           "matita.paste_unicode_as_tex"))
   in
   match mac with
   (* WHELP's stuff *)
@@ -470,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
@@ -478,35 +486,45 @@ 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) 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 l = List.filter (fun u -> not (LibraryObjects.in_eq_URIs u)) l 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 =
@@ -541,38 +559,73 @@ let rec eval_macro include_paths (buffer : GText.buffer) guistuff lexicon_status
           CicMetaSubst.apply_subst subst (Cic.Meta (i,irl))
         in
         let time = Unix.gettimeofday () -. timestamp in
-        let text = 
-          comment parsed_text ^ "\n" ^ 
-          cic2grafite cc menv proof_term ^ 
-          (Printf.sprintf "\n(* end auto proof: %4.2f *)" time)
+        let size, depth = Auto.size_and_depth cc menv proof_term in
+        let trailer = 
+          Printf.sprintf 
+            "\n(* end auto(%s) proof: TIME=%4.2f SIZE=%d DEPTH=%d *)"
+            Auto.revision time size depth
         in
-        (* alternative using FG stuff 
-        let proof_term = 
-          Auto.lambda_close ~prefix_name:"orrible_hack_" proof_term menv cc 
+        let proof_script = 
+          if List.exists (fun (s,_) -> s = "paramodulation") params then
+              let proof_term, how_many_lambdas = 
+                Auto.lambda_close ~prefix_name:"orrible_hack_" 
+                  proof_term menv cc 
+              in
+              let ty,_ = 
+                CicTypeChecker.type_of_aux'
+                  menv [] proof_term CicUniv.empty_ugraph
+              in
+              prerr_endline (CicPp.ppterm proof_term);
+              (* use declarative output *)
+              let obj =
+                (* il proof_term vive in cc, devo metterci i lambda no? *)
+                (Cic.CurrentProof ("xxx",menv,proof_term,ty,[],[]))
+              in
+               ApplyTransformation.txt_of_cic_object
+                ~map_unicode_to_tex:(Helm_registry.get_bool
+                  "matita.paste_unicode_as_tex")
+                ~skip_thm_and_qed:true
+                ~skip_initial_lambdas:how_many_lambdas
+                80 GrafiteAst.Declarative "" obj
+          else
+            if true then
+              (* use cic2grafite *)
+              cic2grafite cc menv proof_term 
+            else
+              (* alternative using FG stuff *)
+              let proof_term, how_many_lambdas = 
+                Auto.lambda_close ~prefix_name:"orrible_hack_" 
+                  proof_term menv cc 
+              in
+              let ty,_ = 
+                CicTypeChecker.type_of_aux'
+                  menv [] proof_term CicUniv.empty_ugraph
+              in
+              let obj = 
+                Cic.Constant ("",Some proof_term, ty, [], [`Flavour `Lemma])
+              in
+                Pcre.qreplace ~templ:"?" ~pat:"orrible_hack_[0-9]+"
+                 (strip_comments
+                  (ApplyTransformation.txt_of_cic_object
+                    ~map_unicode_to_tex:(Helm_registry.get_bool
+                      "matita.paste_unicode_as_tex")
+                    ~skip_thm_and_qed:true
+                    ~skip_initial_lambdas:how_many_lambdas
+                    80 (GrafiteAst.Procedural None) "" obj)) 
         in
-        let ty,_ = 
-          CicTypeChecker.type_of_aux' menv [] proof_term CicUniv.empty_ugraph
-        in
-        let obj = 
-          Cic.Constant ("",Some proof_term, ty, [], [`Flavour `Lemma])
-        in
-        let text = 
-          comment parsed_text ^ 
-          Pcre.qreplace ~templ:"?" ~pat:"orrible_hack_[0-9]+"
-           (strip_comments
-            (ApplyTransformation.txt_of_cic_object
-              ~map_unicode_to_tex:false 
-              ~skip_thm_and_qed:true
-              ~skip_initial_lambdas:true
-              80 (GrafiteAst.Procedural None) "" obj)) ^
-          "(* end auto proof *)"
-        in
-        *)
+        let text = comment parsed_text ^ "\n" ^ proof_script ^ trailer in
         [],text,parsed_text_length
       with
-        ProofEngineTypes.Fail _ -> [], comment parsed_text, parsed_text_length)
+        ProofEngineTypes.Fail _ as exn -> 
+          raise exn
+          (* [], comment parsed_text ^ "\nfail.\n", parsed_text_length *))
   | TA.Inline (_,style,suri,prefix) ->
-       let str = ApplyTransformation.txt_of_inline_macro style suri prefix in
+       let str = 
+         ApplyTransformation.txt_of_inline_macro
+          ~map_unicode_to_tex:(Helm_registry.get_bool
+            "matita.paste_unicode_as_tex")
+          style suri prefix 
+       in
        [], str, String.length parsed_text
                                 
 and eval_executable include_paths (buffer : GText.buffer) guistuff
@@ -588,7 +641,7 @@ script ex loc
      | TA.Command (_,TA.Set (_,"baseuri",u)) ->
         if  Http_getter_storage.is_read_only u then
           raise (ActionCancelled ("baseuri " ^ u ^ " is readonly"));
-        if not (Http_getter_storage.is_empty u) then
+        if not (Http_getter_storage.is_empty ~local:true u) then
          (match 
             guistuff.ask_confirmation 
               ~title:"Baseuri redefinition"