hacks for paramodulation declarative proofs

[helm.git] / helm / software / matita / matitaScript.ml

diff --git a/helm/software/matita/matitaScript.ml b/helm/software/matita/matitaScript.ml
index c6f21c3f62dc19f74f1115013925913ad0306d29..e446b67f5503c9b00b5886ac379244643e43130a 100644 (file)
--- a/helm/software/matita/matitaScript.ml
+++ b/helm/software/matita/matitaScript.ml
@@ -548,9 +548,26 @@ let rec eval_macro include_paths (buffer : GText.buffer) guistuff lexicon_status
             Auto.revision time size depth
         in
         let proof_script = 
-          if List.exists (fun (s,_) -> s = "paramodulation") params then
-            (* use declarative output *)
-            "Not supported yet"
+          if true (* List.exists (fun (s,_) -> s = "paramodulation") params *) then
+              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
+              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:true
+                80 GrafiteAst.Declarative "" obj
           else
             if true then
               (* use cic2grafite *)