X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftptp_grafite%2Ftptp2grafite.ml;h=63dfe0285bb00cb87374c0a5b20096b95c58dbbc;hb=5649890273cf8e660bba744e84ce5fee1e5efe69;hp=841ac5f5c930948345c6037f682fd780889dba15;hpb=bc76b4d2f3c380894259b45fad52cf85ae6cee18;p=helm.git

diff --git a/helm/software/components/tptp_grafite/tptp2grafite.ml b/helm/software/components/tptp_grafite/tptp2grafite.ml
index 841ac5f5c..63dfe0285 100644
--- a/helm/software/components/tptp_grafite/tptp2grafite.ml
+++ b/helm/software/components/tptp_grafite/tptp2grafite.ml
@@ -2,9 +2,17 @@ module GA = GrafiteAst;;
 module LA = LexiconAst;;
 module PT = CicNotationPt;;
 module A = Ast;;
+
+type sort = Prop | Univ;;
+
 let floc = HExtlib.dummy_floc;;
 
+
+let paramod_timeout = ref 600;;
+let depth = ref 10;;
+
 let universe = "Univ" ;;
+let prop = "Prop";;
 
 let kw = [
  "and","myand"
@@ -15,10 +23,11 @@ let mk_ident s =
 ;;
 
 let rec collect_arities_from_term = function
-  | A.Constant name -> [name,0]
-  | A.Variable name -> []
+  | A.Constant name -> [name,(0,Univ)]
+  | A.Variable name -> [name,(0,Univ)]
   | A.Function (name,l) -> 
-      (name,List.length l)::List.flatten (List.map collect_arities_from_term l)
+      (name,(List.length l,Univ))::
+        List.flatten (List.map collect_arities_from_term l)
 ;;
 
 let rec collect_fv_from_term = function
@@ -30,32 +39,42 @@ let rec collect_fv_from_term = function
 
 let collect_arities_from_atom a = 
   let aux = function
-    | A.Proposition name -> assert false
-    | A.Predicate _ -> assert false
+    | A.Proposition name -> [name,(0,Prop)]
+    | A.Predicate (name,args) -> 
+        (name,(List.length args,Prop)) :: 
+          (List.flatten (List.map collect_arities_from_term args))
     | A.True -> []
     | A.False -> []
-    | A.Eq (t1,t2) -> collect_arities_from_term t1 @ collect_arities_from_term t2
-    | A.NotEq (t1,t2) -> collect_arities_from_term t1 @ collect_arities_from_term t2
+    | A.Eq (t1,t2) -> 
+        collect_arities_from_term t1 @ collect_arities_from_term t2
+    | A.NotEq (t1,t2) -> 
+        collect_arities_from_term t1 @ collect_arities_from_term t2
   in
-  aux a
+  HExtlib.list_uniq (List.sort compare (List.flatten (List.map aux a)))
 ;;
   
 let collect_fv_from_atom a = 
   let aux = function
-    | A.Proposition name -> assert false
-    | A.Predicate _ -> assert false
+    | A.Proposition name -> [name] 
+    | A.Predicate (name,args) -> 
+        name :: List.flatten (List.map collect_fv_from_term args)
     | A.True -> []
     | A.False -> []
     | A.Eq (t1,t2) -> collect_fv_from_term t1 @ collect_fv_from_term t2
     | A.NotEq (t1,t2) -> collect_fv_from_term t1 @ collect_fv_from_term t2
   in
-  HExtlib.list_uniq (List.sort compare (aux a))
+  let rec aux2 = function
+    | [] -> []
+    | hd::tl -> aux hd @ aux2 tl
+  in
+  HExtlib.list_uniq (List.sort compare (aux2 a))
 ;;  
 
-let collect_fv_from_formulae = function
-  | A.Disjunction _ -> assert false
+let rec collect_fv_from_formulae = function
+  | A.Disjunction (a,b) -> 
+      collect_fv_from_formulae a @ collect_fv_from_formulae b
   | A.NegAtom a 
-  | A.Atom a -> collect_fv_from_atom a
+  | A.Atom a -> collect_fv_from_atom [a]
 ;;
 
 let rec convert_term = function
@@ -65,29 +84,34 @@ let rec convert_term = function
       PT.Appl (mk_ident name :: List.map convert_term args)
 ;;
 
-let atom_of_formula = function
-    | A.Disjunction _ -> assert false
-    | A.NegAtom a -> a (* removes the negation *)
-    | A.Atom a -> a
+let rec atom_of_formula = function
+    | A.Disjunction (a,b) -> 
+        atom_of_formula a @ atom_of_formula b
+    | A.NegAtom a -> [a] (* removes the negation *)
+    | A.Atom a -> [a]
 ;;
   
-let rec mk_arrow component = function
-  | 0 -> mk_ident component
+let rec mk_arrow component tail = function
+  | 0 -> begin
+      match tail with
+      | Prop -> mk_ident prop
+      | Univ -> mk_ident universe
+      end
   | n -> 
       PT.Binder 
         (`Forall,
           ((mk_ident "_"),Some (mk_ident component)),
-          mk_arrow component (n-1))
+          mk_arrow component tail (n-1))
 ;;
 
 let build_ctx_for_arities univesally arities t = 
   let binder = if univesally then `Forall else `Exists in
   let rec aux = function
     | [] -> t
-    | (name,nargs)::tl ->
+    | (name,(nargs,sort))::tl ->
         PT.Binder 
           (binder,
-            (mk_ident name,Some (mk_arrow universe nargs)),
+            (mk_ident name,Some (mk_arrow universe sort nargs)),
             aux tl)
   in
   aux arities
@@ -95,34 +119,62 @@ let build_ctx_for_arities univesally arities t =
 
 let convert_atom universally a = 
   let aux = function
-  | A.Proposition _ -> assert false
+  | A.Proposition p -> mk_ident p
   | A.Predicate (name,params) -> 
-      prerr_endline ("Predicate is unsupported: " ^ name);
-      assert false
+      PT.Appl ((mk_ident name) :: (List.map convert_term params))
   | A.True -> mk_ident "True"
   | A.False -> mk_ident "False"
   | A.Eq (l,r)
   | A.NotEq (l,r) -> (* removes the negation *)
       PT.Appl [mk_ident "eq";mk_ident universe;convert_term l;convert_term r]
   in
+  let rec aux2 = function
+    | [] -> assert false
+    | [x] -> aux x
+    | he::tl -> 
+        if universally then 
+          PT.Binder (`Forall, (mk_ident "_", Some (aux he)), aux2 tl)
+        else
+          PT.Appl [mk_ident "And";aux he;aux2 tl]
+  in
+  let arities = collect_arities_from_atom a in
+  let fv = collect_fv_from_atom a in
   build_ctx_for_arities universally 
-    (List.map (fun x -> (x,0)) (collect_fv_from_atom a)) (aux a)
+    (List.filter 
+      (function (x,(0,Univ)) -> List.mem x fv | _-> false) 
+      arities) 
+    (aux2 a)
 ;;
 
 let collect_arities atom ctx = 
-  let atoms = atom::(List.map atom_of_formula ctx) in
-  HExtlib.list_uniq (List.sort (fun (a,_) (b,_) -> compare a b) 
-    (List.flatten (List.map collect_arities_from_atom atoms)))
+  let atoms = atom@(List.flatten (List.map atom_of_formula ctx)) in
+  collect_arities_from_atom atoms
 ;;
 
-let assert_formulae_is_1eq_negated f =
+let collect_arities_from_formulae f =
+  let rec collect_arities_from_formulae = function
+  | A.Disjunction (a,b) -> 
+      collect_arities_from_formulae a @ collect_arities_from_formulae b
+  | A.NegAtom a 
+  | A.Atom a -> collect_arities_from_atom [a]
+  in
+  HExtlib.list_uniq (List.sort compare (collect_arities_from_formulae f))
+;;
+
+let is_formulae_1eq_negated f =
   let atom = atom_of_formula f in
   match atom with
-  | A.Eq (l,r) -> failwith "Negated formula is not negated"
-  | A.NotEq (l,r) -> ()
-  | _ -> failwith "Not a unit equality formula"
+  | [A.NotEq (l,r)] -> true
+  | _ -> false
 ;;  
 
+let collect_fv_1stord_from_formulae f =
+  let arities = collect_arities_from_formulae f in
+  let fv = collect_fv_from_formulae f in
+  List.map fst 
+    (List.filter (function (x,(0,Univ)) -> List.mem x fv | _-> false) arities)
+;;
+
 let rec convert_formula fv no_arities context f =
   let atom = atom_of_formula f in
   let t = convert_atom (fv = []) atom in
@@ -140,13 +192,17 @@ let rec convert_formula fv no_arities context f =
 ;;
 
 let check_if_atom_is_negative = function
-  | A.True | A.False | A.Proposition _ | A.Predicate _ -> assert false
+  | A.True -> false
+  | A.False -> true
+  | A.Proposition _ -> false
+  | A.Predicate _ -> false
   | A.Eq _ -> false
   | A.NotEq _ -> true
 ;;
 
-let check_if_formula_is_negative = function
-  | A.Disjunction _ -> assert false
+let rec check_if_formula_is_negative = function
+  | A.Disjunction (a,b) ->
+      check_if_formula_is_negative a && check_if_formula_is_negative b
   | A.NegAtom a -> not (check_if_atom_is_negative a)
   | A.Atom a -> check_if_atom_is_negative a
 ;;
@@ -175,8 +231,8 @@ let convert_ast statements context = function
       | A.Negated_conjecture when not (check_if_formula_is_negative f) ->
           statements, f::context
       | A.Negated_conjecture ->
-          assert_formulae_is_1eq_negated f;
-          let fv = collect_fv_from_formulae f in 
+          let ueq_case = is_formulae_1eq_negated f in
+          let fv = collect_fv_1stord_from_formulae f in 
 (*
           if fv <> [] then 
             prerr_endline ("FREE VARIABLES: " ^ String.concat "," fv);
@@ -190,30 +246,35 @@ let convert_ast statements context = function
           let o = PT.Theorem (`Theorem,name,f,None) in
           statements @ [
             GA.Executable(floc,GA.Command(floc,GA.Obj(floc,o)));
-            GA.Executable(floc,GA.Tactical(floc, GA.Tactic(floc,
-            GA.Intros (floc,None,[])),Some (GA.Dot(floc))))] @
+            GA.Executable(floc,GA.Tactic(floc, Some
+             (GA.Intros (floc,(None,[]))),GA.Dot(floc)))] @
           (if fv <> [] then     
             (List.flatten
               (List.map 
                 (fun _ -> 
-                  [GA.Executable(floc,GA.Tactical(floc, GA.Tactic(floc,
-                    GA.Exists floc),Some (GA.Branch floc)));
-                   GA.Executable(floc,GA.Tactical(floc,
-                    GA.Pos (floc,[2]),None))])
+                  [GA.Executable(floc,GA.Tactic(floc, Some
+                    (GA.Exists floc),GA.Branch floc));
+                   GA.Executable(floc,GA.Tactic(floc, None,
+                    (GA.Pos (floc,[2]))))])
                 fv)) 
            else [])@
-            [GA.Executable(floc,GA.Tactical(floc, GA.Tactic(floc,
-            GA.Auto (floc,["paramodulation",""])),
-              Some (GA.Dot(floc))));
-            GA.Executable(floc,GA.Tactical(floc, GA.Try(floc,
-              GA.Tactic (floc, GA.Assumption floc)), Some (GA.Dot(floc))))
+            [GA.Executable(floc,GA.Tactic(floc, Some (
+              if ueq_case then
+                  GA.AutoBatch (floc,([],["paramodulation","";
+                  "timeout",string_of_int !paramod_timeout]))
+              else
+                  GA.AutoBatch (floc,([],["depth",string_of_int !depth]))
+            ),
+              GA.Semicolon(floc)));
+            GA.Executable(floc,GA.Tactic(floc, Some (GA.Try(floc,
+              GA.Assumption floc)), GA.Dot(floc)))
             ]@
           (if fv <> [] then     
             (List.flatten
               (List.map 
                 (fun _ -> 
-                  [GA.Executable(floc,GA.Tactical(floc, GA.Shift floc, None));
-                   GA.Executable(floc,GA.Tactical(floc, GA.Skip floc,Some
+                  [GA.Executable(floc,GA.Tactic(floc, None, GA.Shift floc));
+                   GA.Executable(floc,GA.NonPunctuationTactical(floc, GA.Skip floc,
                    (GA.Merge floc)))])
                 fv)) 
            else [])@
@@ -249,7 +310,9 @@ let resolve ~tptppath s =
 ;;
 
 (* MAIN *)
-let tptp2grafite ?raw_preamble ~tptppath ~filename () =
+let tptp2grafite ?(timeout=600) ?(def_depth=10) ?raw_preamble ~tptppath ~filename () =
+  paramod_timeout := timeout;
+  depth := def_depth;
   let rec aux = function
     | [] -> []
     | ((A.Inclusion (file,_)) as hd) :: tl ->
@@ -276,14 +339,15 @@ let tptp2grafite ?raw_preamble ~tptppath ~filename () =
       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 List.hd width markup ~map_unicode_to_tex:false 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 in
-    GrafiteAstPp.pp_statement ~term_pp ~lazy_term_pp ~obj_pp t
+    let obj_pp = CicNotationPp.pp_obj CicNotationPp.pp_term in
+    GrafiteAstPp.pp_statement
+     ~map_unicode_to_tex:false ~term_pp ~lazy_term_pp ~obj_pp t
   in
   let buri = Pcre.replace ~pat:"\\.p$" ("cic:/matita/TPTP/" ^ filename) in
   let extra_statements_start = [