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

diff --git a/matita/matitaScript.ml b/matita/matitaScript.ml
index f6610911f..844d2f01e 100644
--- a/matita/matitaScript.ml
+++ b/matita/matitaScript.ml
@@ -541,38 +541,69 @@ 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 
-        in
-        let ty,_ = 
-          CicTypeChecker.type_of_aux' menv [] proof_term CicUniv.empty_ugraph
-        in
-        let obj = 
-          Cic.Constant ("",Some proof_term, ty, [], [`Flavour `Lemma])
+        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:false 
+                ~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:false 
+                    ~skip_thm_and_qed:true
+                    ~skip_initial_lambdas:how_many_lambdas
+                    80 (GrafiteAst.Procedural None) "" obj)) 
         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:false style suri prefix 
+       in
        [], str, String.length parsed_text
                                 
 and eval_executable include_paths (buffer : GText.buffer) guistuff