X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftptp_grafite%2Ftptp2grafite.ml;h=a19fa67c20d3281967d8ec77a754f84ede510a51;hb=a7237500e8a2a4237a6ae8ba4b8301f7bbcb6acb;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..a19fa67c2 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,41 @@ 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 neg pos = function
+    | A.Disjunction (a,b) ->
+        let neg, pos = atom_of_formula neg pos a in
+        atom_of_formula neg pos b 
+    | A.NegAtom a -> a::neg, pos 
+    | A.Atom (A.NotEq (a,b)) -> (A.Eq (a,b) :: neg), pos
+    | A.Atom a -> neg, a::pos
+;;
+
+let atom_of_formula f =
+  let neg, pos = atom_of_formula [] [] f in
+  neg @ pos
 ;;
   
-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 +126,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 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 assert_formulae_is_1eq_negated 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,18 +199,128 @@ 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
 ;;
 
-let convert_ast statements context = function
+let ng_generate_tactics fv ueq_case context arities =
+  [ GA.Executable(floc,GA.NTactic(floc, 
+     [GA.NIntro (floc,"Univ") ; GA.NDot(floc)])) ]
+  @      
+  (HExtlib.list_mapi
+   (fun (name,_) _-> 
+     GA.Executable(floc,GA.NTactic(floc, 
+      [GA.NIntro (floc,(try List.assoc name kw with Not_found -> name));
+       GA.NDot(floc)])))
+   arities)
+  @
+  (HExtlib.list_mapi
+   (fun _ i-> 
+     GA.Executable(floc,GA.NTactic(floc, 
+      [GA.NIntro (floc,"H"^string_of_int i);GA.NDot(floc)])))
+   context)
+  @
+(if fv <> [] then     
+  (List.flatten
+    (List.map 
+      (fun _ -> 
+        [GA.Executable(floc,GA.NTactic(floc, 
+          [GA.NApply (floc,
+            PT.Appl [mk_ident "ex_intro";PT.Implicit;PT.Implicit;
+              PT.Implicit;PT.Implicit]);GA.NBranch floc]));
+         GA.Executable(floc,GA.NTactic(floc, 
+          [GA.NPos (floc,[2])]))])
+      fv)) 
+ else [])@
+  [GA.Executable(floc,GA.NTactic(floc, [
+    if (*ueq_case*) true then
+        GA.NAuto (floc,(
+          HExtlib.list_mapi 
+            (fun _ i -> 
+               mk_ident ("H" ^ string_of_int i)) 
+            context    
+                ,[]))
+    else
+        GA.NAuto (floc,([],[
+                "depth",string_of_int 5;
+                "width",string_of_int 5;
+                "size",string_of_int 20;
+                "timeout",string_of_int 10;
+        ]))
+ ;
+  GA.NSemicolon(floc)]));
+(*
+  GA.Executable(floc,GA.NTactic(floc, Some (GA.Try(floc,
+    GA.Assumption floc)), GA.Dot(floc)))
+*)
+  ]@
+(if fv <> [] then     
+  (List.flatten
+    (List.map 
+      (fun _ -> 
+              [GA.Executable(floc,GA.NTactic(floc, [GA.NShift floc;
+               GA.NSkip floc; GA.NMerge floc]))])
+      fv)) 
+ else [])@
+    [GA.Executable(floc,GA.NTactic(floc,[GA.NTry(floc, GA.NAssumption(floc));
+					 GA.NSemicolon(floc)]))]@
+  [GA.Executable(floc,GA.NCommand(floc, GA.NQed(floc)))]
+;;
+
+let generate_tactics fv ueq_case =
+  [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.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.Tactic(floc, Some (
+    if true (*ueq_case*) then
+        GA.AutoBatch (floc,([],["paramodulation","";
+        "timeout",string_of_int !paramod_timeout]))
+    else
+        GA.AutoBatch (floc,([],[
+                "depth",string_of_int 5;
+                "width",string_of_int 5;
+                "size",string_of_int 20;
+                "timeout",string_of_int 10;
+        ]))
+  ),
+    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.Tactic(floc, None, GA.Shift floc));
+         GA.Executable(floc,GA.NonPunctuationTactical(floc, GA.Skip floc,
+         (GA.Merge floc)))])
+      fv)) 
+ else [])@
+  [GA.Executable(floc,GA.Command(floc, GA.Print(floc,"proofterm")));
+   GA.Executable(floc,GA.Command(floc, GA.Qed(floc)))]
+;;
+
+let convert_ast ng statements context = function
   | A.Comment s -> 
       let s = String.sub s 1 (String.length s - 1) in
       let s = 
@@ -175,50 +344,23 @@ 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 
-(*
-          if fv <> [] then 
-            prerr_endline ("FREE VARIABLES: " ^ String.concat "," fv);
-*)
+          let ueq_case = is_formulae_1eq_negated f in
+          let fv = collect_fv_1stord_from_formulae f in 
+          let old_f = f in
           let f = 
             PT.Binder 
              (`Forall,
-               (mk_ident universe,Some (PT.Sort `Set)), 
+               (mk_ident universe,Some (PT.Sort (`Type (CicUniv.fresh ())))), 
                convert_formula fv false context f)
           in
           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))))] @
-          (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))])
-                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))))
-            ]@
-          (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.Merge floc)))])
-                fv)) 
-           else [])@
-            [GA.Executable(floc,GA.Command(floc, GA.Print(floc,"proofterm")));
-             GA.Executable(floc,GA.Command(floc, GA.Qed(floc)))],
+          (statements @ 
+          [ GA.Executable(floc,GA.Command(floc,
+             (*if ng then GA.NObj (floc,o) else*) GA.Obj(floc,o))); ] @
+          if ng then 
+            ng_generate_tactics fv ueq_case context
+              (let atom = atom_of_formula old_f in collect_arities atom context)
+          else generate_tactics fv ueq_case),
           context
       | A.Definition 
       | A.Lemma 
@@ -249,7 +391,9 @@ let resolve ~tptppath s =
 ;;
 
 (* MAIN *)
-let tptp2grafite ?raw_preamble ~tptppath ~filename () =
+let tptp2grafite ?(timeout=600) ?(def_depth=10) ?raw_preamble ~tptppath ~filename ~ng () =
+  paramod_timeout := timeout;
+  depth := def_depth;
   let rec aux = function
     | [] -> []
     | ((A.Inclusion (file,_)) as hd) :: tl ->
@@ -263,7 +407,7 @@ let tptp2grafite ?raw_preamble ~tptppath ~filename () =
   let grafite_ast_statements,_ = 
     List.fold_left 
       (fun (st, ctx) f -> 
-        let newst, ctx = convert_ast st ctx f in
+        let newst, ctx = convert_ast ng st ctx f in
         newst, ctx)
       ([],[]) statements 
   in
@@ -272,29 +416,33 @@ let tptp2grafite ?raw_preamble ~tptppath ~filename () =
      * which will show up using the following command line:
      * ./tptp2grafite -tptppath ~tassi/TPTP-v3.1.1 GRP170-1 *)
     let width = max_int in
-    let term_pp content_term =
+    let term_pp prec content_term =
       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 lookup_uri = fun _ -> None in
+      let markup = CicNotationPres.render ~lookup_uri ~prec pres_term 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
+       ~rex:(Pcre.regexp ~flags:[`UTF8] "∀[Ha-z][a-z0-9_]*") ~subst:(fun x -> "\n" ^ x) 
+       s
     in
-    CicNotationPp.set_pp_term term_pp;
+    CicNotationPp.set_pp_term (term_pp 90);
     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
+    Pcre.replace ~pat:"theorem" ~templ:"ntheorem" 
+     (GrafiteAstPp.pp_statement
+       ~map_unicode_to_tex:false ~term_pp:(term_pp 19) ~lazy_term_pp ~obj_pp t)
   in
   let buri = Pcre.replace ~pat:"\\.p$" ("cic:/matita/TPTP/" ^ filename) in
   let extra_statements_start = [
-    GA.Executable(floc,GA.Command(floc,
-    GA.Set(floc,"baseuri",buri)))]
+    (*GA.Executable(floc,GA.Command(floc,
+    GA.Set(floc,"baseuri",buri)))*)]
   in
   let preamble = 
     match raw_preamble with
     | None -> 
-       pp (GA.Executable(floc,
-           GA.Command(floc,GA.Include(floc,"logic/equality.ma"))))
+      pp
+       (GA.Executable(floc,
+         GA.Command(floc,GA.Include(floc,true,`OldAndNew,"logic/equality.ma"))))
     | Some s -> s buri
   in
   let extra_statements_end = [] in