]> matita.cs.unibo.it Git - helm.git/commitdiff
hacks for paramodulation declarative proofs
authorEnrico Tassi <enrico.tassi@inria.fr>
Fri, 1 Jun 2007 07:35:59 +0000 (07:35 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Fri, 1 Jun 2007 07:35:59 +0000 (07:35 +0000)
components/acic_content/acic2content.ml
components/acic_procedural/acic2Procedural.ml
components/acic_procedural/acic2Procedural.mli
components/content_pres/content2pres.ml
components/content_pres/content2pres.mli
matita/applyTransformation.ml
matita/applyTransformation.mli
matita/matitaScript.ml

index 1b8c287fabef5f77c261974cc9d84c07a4703635..eddee38b1a51ed2c985df789006c574ae21604e0 100644 (file)
@@ -479,7 +479,8 @@ and acic2content seed ?name ~ids_to_inner_sorts ~ids_to_inner_types t =
             }
           in
           generate_intros_let_tac seed id n s true proof'' name ~ids_to_inner_types
-        else raise Not_a_proof 
+        else 
+          raise Not_a_proof 
     | C.ALetIn (id,n,s,t) ->
         let sort = Hashtbl.find ids_to_inner_sorts id in
         if sort = `Prop then
@@ -500,7 +501,8 @@ and acic2content seed ?name ~ids_to_inner_sorts ~ids_to_inner_types t =
             }
           in
           generate_intros_let_tac seed id n s false proof'' name ~ids_to_inner_types
-        else raise Not_a_proof 
+        else 
+          raise Not_a_proof
     | C.AAppl (id,li) ->
         (try coercion 
            seed li ~ids_to_inner_types ~ids_to_inner_sorts
index 23b934d51d35fc151f0833f2e518838c820a59ac..f39aa18bd96ee3a162baa10fa6da07ca3b6f8805 100644 (file)
@@ -56,7 +56,6 @@ type status = {
    clears_note: string;
    case: int list;
    skip_thm_and_qed : bool;
-   skip_initial_lambdas : bool;
 }
 
 (* helpers ******************************************************************)
@@ -376,12 +375,7 @@ and proc_proof st t =
          (Pp.ppterm (H.cic it)) (Pp.ppterm (H.cic et))) 
          | None          -> None, "\nNo types"
       in
-      let context, clears = 
-        if st.skip_initial_lambdas then
-          st.context, []
-        else
-          Cn.get_clears st.context (H.cic t) xtypes 
-      in
+      let context, clears = Cn.get_clears st.context (H.cic t) xtypes in
       let note = Pp.ppcontext st.context ^ note in
       {st with context = context; clears = clears; clears_note = note; }
    in
@@ -429,13 +423,6 @@ let proc_obj st = function
       let ast = proc_proof st v in
       let steps, nodes = T.count_steps 0 ast, T.count_nodes 0 ast in
       let text = Printf.sprintf "tactics: %u\nnodes: %u" steps nodes in
-      let ast = 
-        if st.skip_initial_lambdas then 
-          match ast with
-            | T.Intros _::tl -> tl
-            | ast -> ast
-        else ast
-      in
       if st.skip_thm_and_qed then ast
       else T.Theorem (Some s, t, "") :: ast @ [T.Qed text]
    | _                                                               ->
@@ -444,7 +431,7 @@ let proc_obj st = function
 (* interface functions ******************************************************)
 
 let acic2procedural ~ids_to_inner_sorts ~ids_to_inner_types ?depth
-?(skip_thm_and_qed=false) ?(skip_initial_lambdas=false) prefix aobj = 
+?(skip_thm_and_qed=false) prefix aobj = 
    let st = {
       sorts       = ids_to_inner_sorts;
       types       = ids_to_inner_types;
@@ -457,7 +444,6 @@ let acic2procedural ~ids_to_inner_sorts ~ids_to_inner_types ?depth
       clears_note = "";
       case        = [];
       skip_thm_and_qed = skip_thm_and_qed;
-      skip_initial_lambdas = skip_initial_lambdas;
    } in
    HLog.debug "Procedural: level 2 transformation";
    let steps = proc_obj st aobj in
index 35092fb16099d1279263bf181b5b969b460b994e..08e49a3439acf78e6ba72f5164fef3427b5e72e7 100644 (file)
@@ -26,7 +26,7 @@
 val acic2procedural:
    ids_to_inner_sorts:(Cic.id, Cic2acic.sort_kind) Hashtbl.t ->
    ids_to_inner_types:(Cic.id, Cic2acic.anntypes) Hashtbl.t -> 
-   ?depth:int -> ?skip_thm_and_qed:bool -> ?skip_initial_lambdas:bool ->
+   ?depth:int -> ?skip_thm_and_qed:bool ->
      string -> Cic.annobj ->
       (Cic.annterm, Cic.annterm,
        Cic.annterm GrafiteAst.reduction, Cic.annterm CicNotationPt.obj, string)
index e377706b7ddb69b49650306eb5a71180b0d9d6e6..b9c46917c236c32006f0759a1b4fbc7b8c7c7dfa 100644 (file)
@@ -134,8 +134,9 @@ let rec justification term2pres p =
   else (B.b_kw "by"),
     Some (B.b_toggle [B.b_kw "proof";proof2pres true term2pres p])
      
-and proof2pres is_top_down term2pres p =
-  let rec proof2pres is_top_down p omit_dot =
+and proof2pres ?skip_initial_lambdas is_top_down term2pres p =
+  let rec proof2pres ?(skip_initial_lambdas_internal=false) is_top_down p omit_dot =
+    prerr_endline p.Con.proof_conclude.Con.conclude_method;
     let indent = 
       let is_decl e = 
         (match e with 
@@ -150,16 +151,19 @@ and proof2pres is_top_down term2pres p =
        | Some t -> Some (term2pres t)) in
     let body =
         let presconclude = 
-          conclude2pres is_top_down p.Con.proof_conclude indent omit_conclusion
+          conclude2pres ~skip_initial_lambdas_internal is_top_down p.Con.proof_conclude indent omit_conclusion
            omit_dot in
         let presacontext = 
           acontext2pres
            (p.Con.proof_conclude.Con.conclude_method = "BU_Conversion")
-           p.Con.proof_apply_context presconclude indent
+            p.Con.proof_apply_context
+            presconclude indent
            (p.Con.proof_conclude.Con.conclude_method = "BU_Conversion")
         in
-         context2pres p.Con.proof_context presacontext
-  in
+        context2pres 
+          (if skip_initial_lambdas_internal then [] else p.Con.proof_context)
+          presacontext
+    in
     match p.Con.proof_name with
       None -> body
     | Some name ->
@@ -256,7 +260,7 @@ and proof2pres is_top_down term2pres p =
            [B.H([Some "helm","xref","ace_"^p.Con.proof_id],[hd]);
             continuation])) ac continuation 
 
-  and conclude2pres is_top_down conclude indent omit_conclusion omit_dot =
+  and conclude2pres ?skip_initial_lambdas_internal is_top_down conclude indent omit_conclusion omit_dot =
     let tconclude_body = 
       match conclude.Con.conclude_conclusion with
         Some t (*when not omit_conclusion or
@@ -274,7 +278,8 @@ and proof2pres is_top_down term2pres p =
            (* false ind is in charge to add the conclusion *)
            falseind conclude
           else  
-            let conclude_body = conclude_aux conclude in
+            let conclude_body = 
+              conclude_aux ?skip_initial_lambdas_internal conclude in
             let ann_concl = 
               if  conclude.Con.conclude_method = "Intros+LetTac"
                || conclude.Con.conclude_method = "ByInduction"
@@ -286,7 +291,7 @@ and proof2pres is_top_down term2pres p =
                ((if not is_top_down || omit_dot then [make_concl "we proved" concl; B.Text([],if not is_top_down then "(previous)" else "")] else [B.Text([],"done")]) @ if not omit_dot then [B.Text([],".")] else [])
             in
              B.V ([], [conclude_body; ann_concl])
-      | _ -> conclude_aux conclude
+      | _ -> conclude_aux ?skip_initial_lambdas_internal conclude
     in
      if indent then 
        B.indent (B.H ([Some "helm", "xref", conclude.Con.conclude_id],
@@ -294,7 +299,7 @@ and proof2pres is_top_down term2pres p =
      else 
        B.H ([Some "helm", "xref", conclude.Con.conclude_id],[tconclude_body])
 
-  and conclude_aux conclude =
+  and conclude_aux ?skip_initial_lambdas_internal conclude =
     if conclude.Con.conclude_method = "TD_Conversion" then
       let expected = 
         (match conclude.Con.conclude_conclusion with 
@@ -333,7 +338,7 @@ and proof2pres is_top_down term2pres p =
        )
     else if conclude.Con.conclude_method = "Intros+LetTac" then
       (match conclude.Con.conclude_args with
-         [Con.ArgProof p] -> proof2pres true p false
+         [Con.ArgProof p] -> proof2pres ?skip_initial_lambdas_internal true p false
        | _ -> assert false)
 (* OLD CODE 
       let conclusion = 
@@ -385,14 +390,19 @@ and proof2pres is_top_down term2pres p =
 *) B.V([], [justif1 ; B.H([],[B.b_kw "we proved (" ; term2 ; B.b_kw "=" ; term1; B.b_kw ") (previous)."]); B.b_kw "by _"])
     else if conclude.Con.conclude_method = "Eq_chain" then
       let justification p =
-       let j1,j2 = justification term2pres p in
+        if skip_initial_lambdas <> None (* cheating *) then
+          [B.b_kw "by _"]
+        else
+          let j1,j2 = justification term2pres p in
          j1 :: B.b_space :: (match j2 with Some j -> [j] | None -> [])
       in
       let rec aux args =
        match args with
          | [] -> []
          | (Con.ArgProof p)::(Con.Term t)::tl -> 
-             B.HOV(RenderingAttrs.indent_attributes `BoxML,([B.b_kw "=";B.b_space;term2pres t;B.b_space]@justification p))::(aux tl)
+             B.HOV(RenderingAttrs.indent_attributes `BoxML,([B.b_kw
+              "=";B.b_space;term2pres t;B.b_space]@justification p@
+              (if tl <> [] then [B.Text ([],".")] else [])))::(aux tl)
          | _ -> assert false 
       in
       let hd = 
@@ -400,7 +410,7 @@ and proof2pres is_top_down term2pres p =
          | Con.Term t -> t 
          | _ -> assert false 
       in
-      B.HOV([],[term2pres hd; (* B.b_space; *)
+      B.HOV([],[B.Text ([],"conclude");B.b_space;term2pres hd; (* B.b_space; *)
              B.V ([],aux (List.tl conclude.Con.conclude_args))])
     else if conclude.Con.conclude_method = "Apply" then
       let pres_args = 
@@ -682,7 +692,7 @@ and proof2pres is_top_down term2pres p =
          | _ -> assert false
 
     in
-    proof2pres is_top_down p false
+    proof2pres ?skip_initial_lambdas_internal:skip_initial_lambdas is_top_down p false
 
 exception ToDo
 
@@ -798,16 +808,24 @@ let joint_def2pres term2pres def =
   | `Inductive ind -> inductive2pres term2pres ind
   | _ -> assert false (* ZACK or raise ToDo? *)
 
-let content2pres term2pres (id,params,metasenv,obj) =
+let content2pres 
+  ?skip_initial_lambdas ?(skip_thm_and_qed=false) term2pres 
+  (id,params,metasenv,obj) 
+=
   match obj with
   | `Def (Content.Const, thesis, `Proof p) ->
       let name = get_name p.Content.proof_name in
+      let proof = proof2pres true term2pres ?skip_initial_lambdas p in
+      if skip_thm_and_qed then
+        proof
+      else
       B.b_v
         [Some "helm","xref","id"]
-        ([ B.b_h [] (B.b_kw ("theorem " ^ name) :: params2pres params @ [B.b_kw ":"]);
+        ([ B.b_h [] (B.b_kw ("theorem " ^ name) :: 
+          params2pres params @ [B.b_kw ":"]);
            B.indent (term2pres thesis) ; B.b_kw "." ] @
          metasenv2pres term2pres metasenv @
-         [proof2pres true term2pres p ; B.b_kw "qed."])
+         [proof ; B.b_kw "qed."])
   | `Def (_, ty, `Definition body) ->
       let name = get_name body.Content.def_name in
       B.b_v
@@ -834,8 +852,10 @@ let content2pres term2pres (id,params,metasenv,obj) =
         :: List.map (joint_def2pres term2pres) joint.Content.joint_defs)
   | _ -> raise ToDo
 
-let content2pres ~ids_to_inner_sorts =
-  content2pres
+let content2pres 
+  ?skip_initial_lambdas ?skip_thm_and_qed ~ids_to_inner_sorts 
+=
+  content2pres ?skip_initial_lambdas ?skip_thm_and_qed
     (fun ?(prec=90) annterm ->
       let ast, ids_to_uris =
         TermAcicContent.ast_of_acic ids_to_inner_sorts annterm
index 793c31a4fdcb462450777f23dabb987b923a4641..6dd0fd8aacb3960a2915df99f8ed15b685fbc452 100644 (file)
@@ -33,6 +33,7 @@
 (**************************************************************************)
 
 val content2pres:
+  ?skip_initial_lambdas:bool -> ?skip_thm_and_qed:bool ->
   ids_to_inner_sorts:(Cic.id, Cic2acic.sort_kind) Hashtbl.t ->
   Cic.annterm Content.cobj ->
     CicNotationPres.boxml_markup
index 0b8bbd1bceeddda0750c8209d9f0e0c10e8303e0..3cfaff52637177e736ff14ea6a8a99ac84f94ae5 100644 (file)
@@ -150,7 +150,7 @@ let term2pres ?map_unicode_to_tex n ids_to_inner_sorts annterm =
    let bobj =
       CicNotationPres.box_of_mpres (
          CicNotationPres.render ~prec:90 ids_to_uris 
-           (TermContentPres.pp_ast ast)
+            (TermContentPres.pp_ast ast)
       )
    in
    let render = function _::x::_ -> x | _ -> assert false in
@@ -166,34 +166,39 @@ let txt_of_cic_object
         let aobj,_,_,ids_to_inner_sorts,ids_to_inner_types,_,_ =
             Cic2acic.acic_object_of_cic_object obj
         in
-       aobj, ids_to_inner_sorts, ids_to_inner_types
+        aobj, ids_to_inner_sorts, ids_to_inner_types
      with e -> 
         let msg = "txt_of_cic_object: " ^ Printexc.to_string e in
-       failwith msg
+        failwith msg
   in
   match style with
      | G.Declarative      ->
         let aobj, ids_to_inner_sorts, ids_to_inner_types = get_aobj obj in
-       let cobj = Acic2content.annobj2content ids_to_inner_sorts ids_to_inner_types aobj in
-        let bobj = Content2pres.content2pres ids_to_inner_sorts cobj in
+        let cobj = 
+          Acic2content.annobj2content 
+            ids_to_inner_sorts ids_to_inner_types aobj 
+        in
+        let bobj = 
+          Content2pres.content2pres 
+            ?skip_initial_lambdas ?skip_thm_and_qed ~ids_to_inner_sorts cobj 
+        in
         remove_closed_substs ("\n\n" ^
-          BoxPp.render_to_string ?map_unicode_to_tex
+           BoxPp.render_to_string ?map_unicode_to_tex
             (function _::x::_ -> x | _ -> assert false) n
             (CicNotationPres.mpres_of_box bobj)
-       )
+        )
      | G.Procedural depth ->
         let obj = ProceduralOptimizer.optimize_obj obj in
-       let aobj, ids_to_inner_sorts, ids_to_inner_types = get_aobj obj in
+        let aobj, ids_to_inner_sorts, ids_to_inner_types = get_aobj obj in
         let term_pp = term2pres (n - 8) ids_to_inner_sorts in
         let lazy_term_pp = term_pp in
         let obj_pp = CicNotationPp.pp_obj term_pp in
         let aux = GrafiteAstPp.pp_statement ~term_pp ~lazy_term_pp ~obj_pp in
-       let script = 
+        let script = 
     Acic2Procedural.acic2procedural 
-          ~ids_to_inner_sorts ~ids_to_inner_types ?depth ?skip_thm_and_qed 
-       ?skip_initial_lambdas prefix aobj 
+           ~ids_to_inner_sorts ~ids_to_inner_types ?depth ?skip_thm_and_qed prefix aobj 
   in
-       String.concat "" (List.map aux script) ^ "\n\n"
+        String.concat "" (List.map aux script) ^ "\n\n"
 
 let txt_of_inline_macro style suri prefix =
    let print_exc = function
@@ -208,7 +213,7 @@ let txt_of_inline_macro style suri prefix =
                             (fst (CicEnvironment.get_obj CicUniv.empty_ugraph uri))
       with
          | e -> 
-           Printf.sprintf "\n(* ERRORE IN STAMPA DI %s\nEXCEPTION: %s *)\n" 
-           (UriManager.string_of_uri uri) (print_exc e)
+            Printf.sprintf "\n(* ERRORE IN STAMPA DI %s\nEXCEPTION: %s *)\n" 
+            (UriManager.string_of_uri uri) (print_exc e)
    in
    String.concat "" (List.map map sorted_uris)
index 63c3beedf4a22225aea0f2680464b785901eabb1..170980cb0e2f95c87c39a02d58150b7f22ec1453 100644 (file)
@@ -68,7 +68,8 @@ val txt_of_cic_sequent_conclusion:
 (* columns, rendering style, name prefix, object *)
 val txt_of_cic_object: 
   ?map_unicode_to_tex:bool -> 
-  ?skip_thm_and_qed:bool -> ?skip_initial_lambdas:bool ->  
+  ?skip_thm_and_qed:bool -> 
+  ?skip_initial_lambdas:bool -> 
     int -> GrafiteAst.presentation_style -> string ->
   Cic.obj ->
     string
index c6f21c3f62dc19f74f1115013925913ad0306d29..e446b67f5503c9b00b5886ac379244643e43130a 100644 (file)
@@ -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 *)