]> matita.cs.unibo.it Git - helm.git/commitdiff
matitaprover
authorEnrico Tassi <enrico.tassi@inria.fr>
Sat, 22 Jul 2006 17:14:13 +0000 (17:14 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Sat, 22 Jul 2006 17:14:13 +0000 (17:14 +0000)
45 files changed:
helm/software/components/METAS/meta.helm-tptp_grafite.src [new file with mode: 0644]
helm/software/components/Makefile
helm/software/components/acic_content/.depend
helm/software/components/binaries/Makefile
helm/software/components/binaries/tptp2grafite/Makefile [deleted file]
helm/software/components/binaries/tptp2grafite/ast.ml [deleted file]
helm/software/components/binaries/tptp2grafite/lexer.mll [deleted file]
helm/software/components/binaries/tptp2grafite/main.ml [deleted file]
helm/software/components/binaries/tptp2grafite/parser.mly [deleted file]
helm/software/components/binaries/tptp2grafite/unit_equality_problems [deleted file]
helm/software/components/cic/libraryObjects.ml
helm/software/components/cic/libraryObjects.mli
helm/software/components/cic_proof_checking/cicPp.ml
helm/software/components/content_pres/.depend
helm/software/components/grafite/grafiteAst.ml
helm/software/components/grafite/grafiteAstPp.ml
helm/software/components/grafite_engine/grafiteEngine.ml
helm/software/components/grafite_engine/grafiteTypes.ml
helm/software/components/grafite_parser/grafiteDisambiguate.ml
helm/software/components/grafite_parser/grafiteParser.ml
helm/software/components/library/librarySync.ml
helm/software/components/syntax_extensions/profiling_macros.ml
helm/software/components/tactics/autoTactic.ml
helm/software/components/tactics/autoTactic.mli
helm/software/components/tactics/paramodulation/equality.ml
helm/software/components/tactics/paramodulation/equality.mli
helm/software/components/tactics/paramodulation/indexing.ml
helm/software/components/tactics/paramodulation/inference.ml
helm/software/components/tactics/paramodulation/saturation.ml
helm/software/components/tptp_grafite/.depend [new file with mode: 0644]
helm/software/components/tptp_grafite/Makefile [new file with mode: 0644]
helm/software/components/tptp_grafite/ast.ml [new file with mode: 0644]
helm/software/components/tptp_grafite/lexer.mll [new file with mode: 0644]
helm/software/components/tptp_grafite/main.ml [new file with mode: 0644]
helm/software/components/tptp_grafite/parser.mly [new file with mode: 0644]
helm/software/components/tptp_grafite/tptp2grafite.ml [new file with mode: 0644]
helm/software/components/tptp_grafite/tptp2grafite.mli [new file with mode: 0644]
helm/software/components/tptp_grafite/unit_equality_problems [new file with mode: 0644]
helm/software/configure.ac
helm/software/matita/.depend
helm/software/matita/Makefile
helm/software/matita/matitaInit.ml
helm/software/matita/matitac.ml
helm/software/matita/tests/TPTP/elenco_unsatisfiable.txt [new file with mode: 0644]
helm/software/matita/tests/TPTP/try.sh

diff --git a/helm/software/components/METAS/meta.helm-tptp_grafite.src b/helm/software/components/METAS/meta.helm-tptp_grafite.src
new file mode 100644 (file)
index 0000000..4c16756
--- /dev/null
@@ -0,0 +1,5 @@
+requires="helm-acic_content helm-grafite helm-lexicon"
+version="0.0.1"
+archive(byte)="tptp_grafite.cma"
+archive(native)="tptp_grafite.cmxa"
+linkopts=""
index 948ba8f3672ff3c45368aaca04d1f0a6315542ce..cfe1fd51715ae0a16531cf796172c52ce74e0273 100644 (file)
@@ -32,6 +32,7 @@ MODULES =                     \
        lexicon                 \
        grafite_engine          \
        grafite_parser          \
+       tptp_grafite            \
        $(NULL)
 
 METAS = $(MODULES:%=METAS/META.helm-%)
index f6399321e10908edb312decfbd18474deec07544..a0f6ba9ca740b008721a97b07f6d44efa4250c91 100644 (file)
@@ -25,6 +25,6 @@ acic2astMatcher.cmo: cicNotationUtil.cmi cicNotationPt.cmo cicNotationPp.cmi \
 acic2astMatcher.cmx: cicNotationUtil.cmx cicNotationPt.cmx cicNotationPp.cmx \
     acic2astMatcher.cmi 
 termAcicContent.cmo: cicNotationUtil.cmi cicNotationPt.cmo cicNotationPp.cmi \
-    acic2astMatcher.cmi termAcicContent.cmi 
+    acic2content.cmi acic2astMatcher.cmi termAcicContent.cmi 
 termAcicContent.cmx: cicNotationUtil.cmx cicNotationPt.cmx cicNotationPp.cmx \
-    acic2astMatcher.cmx termAcicContent.cmi 
+    acic2content.cmx acic2astMatcher.cmx termAcicContent.cmi 
index 0f79acfe41879c4ce22e61f26f75fd4096fadb5b..a2b89ee979f64b4ddd403183dfb570fb6af7cb94 100644 (file)
@@ -1,6 +1,6 @@
 H=@
 
-BINARIES=extractor  table_creator  utilities saturate tptp2grafite
+BINARIES=extractor  table_creator  utilities saturate
 
 all: $(BINARIES:%=rec@all@%) 
 opt: $(BINARIES:%=rec@opt@%)
diff --git a/helm/software/components/binaries/tptp2grafite/Makefile b/helm/software/components/binaries/tptp2grafite/Makefile
deleted file mode 100644 (file)
index 071bf8d..0000000
+++ /dev/null
@@ -1,39 +0,0 @@
-OCAMLC = OCAMLPATH=../../METAS ocamlfind ocamlc -package helm-grafite_parser
-TPTPDIR=/home/$(USER)/TPTP-v3.1.1/
-
-opt all: tptp2grafite
-       echo -n
-
-tptp2grafite: ast.ml parser.mly lexer.mll main.ml
-       $(OCAMLC) -c ast.ml
-       ocamlyacc parser.mly
-       $(OCAMLC) -c parser.mli
-       $(OCAMLC) -c parser.ml
-       ocamllex lexer.mll
-       $(OCAMLC) -c lexer.ml
-       $(OCAMLC) -c main.ml
-       $(OCAMLC) -linkpkg -o tptp2grafite ast.cmo lexer.cmo parser.cmo main.cmo
-
-clean:
-       rm -f tptp2grafite *.cmo *.cmi parser.mli parser.ml lexer.ml rm *.output
-
-test: tptp2grafite
-       cat $(TPTPDIR)/`head -n 1 unit_equality_problems` | ./tptp2grafite
-
-testall: tptp2grafite
-       for X in `cat unit_equality_problems`; do\
-               cat $(TPTPDIR)/$$X | ./tptp2grafite || echo ERROR PARSING $$X;\
-       done
-
-generate:
-       for X in `cat unit_equality_problems`; do\
-               ./tptp2grafite -tptppath $(TPTPDIR) $$X \
-               > ../../../matita/tests/TPTP/$$X.ma || echo Failed: $$X; \
-       done
-
-parse:
-       for X in `cat unit_equality_problems`; do\
-         echo "Parsing $$X"; \
-               ./tptp2grafite -tptppath $(TPTPDIR) $$X \
-               > /dev/null || echo Failed: $$X; \
-       done
diff --git a/helm/software/components/binaries/tptp2grafite/ast.ml b/helm/software/components/binaries/tptp2grafite/ast.ml
deleted file mode 100644 (file)
index b8f855d..0000000
+++ /dev/null
@@ -1,31 +0,0 @@
-type kinds_of_formulae = 
-  | Axiom | Hypothesis | Definition | Lemma | Theorem | Conjecture
-  | Lemma_conjecture | Negated_conjecture | Plain | Unknown
-
-type source = NoSource
-
-type info = NoInfo
-
-type term = 
-  | Variable of string
-  | Constant of string 
-  | Function of string * term list
-
-type atom = 
-  | Proposition of string
-  | Predicate of string * term list
-  | True
-  | False
-  | Eq of term * term
-  | NotEq of term * term
-
-type formulae = 
-  | Disjunction of formulae * formulae
-  | NegAtom of  atom
-  | Atom of atom
-  
-type ast = 
-  | Comment of string
-  | Inclusion of string * (string list)
-  | AnnotatedFormula of 
-      string * kinds_of_formulae * formulae * source * info list
diff --git a/helm/software/components/binaries/tptp2grafite/lexer.mll b/helm/software/components/binaries/tptp2grafite/lexer.mll
deleted file mode 100644 (file)
index 273d1b7..0000000
+++ /dev/null
@@ -1,57 +0,0 @@
-{ 
-  open Parser
-  exception BadToken of string 
-  
-  let incr_linenum lexbuf =
-    let pos = lexbuf.Lexing.lex_curr_p in
-    lexbuf.Lexing.lex_curr_p <- { pos with
-      Lexing.pos_lnum = pos.Lexing.pos_lnum + 1;
-      Lexing.pos_bol = pos.Lexing.pos_cnum;
-    }
-  ;;
-  
-}
-
-let dust = ' ' | '\t'
-let comment = '%' [^ '\n' ] * '\n'
-let lname = 
-  ['a'-'z'] ['a'-'z''A'-'Z''0'-'9''_']*
-let uname = 
-  ['A'-'Z'] ['a'-'z''A'-'Z''0'-'9''_']*
-let qstring = ''' [^ ''' ]+ '''
-let type_ =   
-  "axiom" | "hypothesis" | "definition" | "lemma" | "theorem" |
-  "conjecture" | "lemma_conjecture" | "negated_conjecture" |
-  "plain" | "unknown"
-
-let ieq = "="
-let peq = "equal"
-let nieq = "!="
-
-rule yylex = parse 
-   | dust { yylex lexbuf }
-   | '\n' { incr_linenum lexbuf; yylex lexbuf }
-   | comment { incr_linenum lexbuf; COMMENT (Lexing.lexeme lexbuf) }
-   | "include" { INCLUSION }
-   | type_ { TYPE (Lexing.lexeme lexbuf) }
-   | "cnf" { CNF } 
-   | "$true" { TRUE }
-   | "$false" { FALSE }
-   | "equal" { PEQ }
-   
-   | lname { LNAME (Lexing.lexeme lexbuf) }
-   | uname { UNAME (Lexing.lexeme lexbuf) }
-   | ['0' - '9']+ { NUM (int_of_string (Lexing.lexeme lexbuf)) }
-   | ',' { COMMA }
-   | '.' { DOT }
-   | '(' { LPAREN }
-   | ')' { RPAREN }
-   | '|' { IOR }
-   | '~' { NOT }
-   | '=' { IEQ }
-   | "!=" { NIEQ }
-   | qstring { QSTRING (Lexing.lexeme lexbuf) }
-   | eof { EOF } 
-   | _ { raise (BadToken (Lexing.lexeme lexbuf)) }
-
-{ (* trailer *) }
diff --git a/helm/software/components/binaries/tptp2grafite/main.ml b/helm/software/components/binaries/tptp2grafite/main.ml
deleted file mode 100644 (file)
index 980f2b4..0000000
+++ /dev/null
@@ -1,324 +0,0 @@
-module GA = GrafiteAst;;
-module LA = LexiconAst;;
-module PT = CicNotationPt;;
-module A = Ast;;
-let floc = HExtlib.dummy_floc;;
-
-let universe = "Univ" ;;
-
-let kw = [
- "and","myand"
-];;
-
-let mk_ident s =
-  PT.Ident ((try List.assoc s kw with Not_found -> s),None)
-;;
-
-let rec collect_arities_from_term = function
-  | A.Constant name -> [name,0]
-  | A.Variable name -> []
-  | A.Function (name,l) -> 
-      (name,List.length l)::List.flatten (List.map collect_arities_from_term l)
-;;
-
-let rec collect_fv_from_term = function
-  | A.Constant name -> []
-  | A.Variable name -> [name]
-  | A.Function (_,l) -> 
-      List.flatten (List.map collect_fv_from_term l)
-;;
-
-let collect_arities_from_atom a = 
-  let aux = function
-    | A.Proposition name -> assert false
-    | A.Predicate _ -> assert false
-    | 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
-  in
-  aux a
-;;
-  
-let collect_fv_from_atom a = 
-  let aux = function
-    | A.Proposition name -> assert false
-    | A.Predicate _ -> assert false
-    | 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 collect_fv_from_formulae = function
-  | A.Disjunction _ -> assert false
-  | A.NegAtom a 
-  | A.Atom a -> collect_fv_from_atom a
-;;
-
-let rec convert_term = function
-  | A.Variable x -> mk_ident x
-  | A.Constant x -> mk_ident x
-  | A.Function (name, args) -> 
-      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 mk_arrow component = function
-  | 0 -> mk_ident component
-  | n -> 
-      PT.Binder 
-        (`Forall,
-          ((mk_ident "_"),Some (mk_ident component)),
-          mk_arrow component (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 ->
-        PT.Binder 
-          (binder,
-            (mk_ident name,Some (mk_arrow universe nargs)),
-            aux tl)
-  in
-  aux arities
-;;
-
-let convert_atom universally a = 
-  let aux = function
-  | A.Proposition _ -> assert false
-  | A.Predicate (name,params) -> 
-      prerr_endline ("Predicate is unsupported: " ^ name);
-      assert false
-  | 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
-  build_ctx_for_arities universally 
-    (List.map (fun x -> (x,0)) (collect_fv_from_atom a)) (aux 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 assert_formulae_is_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"
-;;  
-
-let rec convert_formula fv no_arities context f =
-  let atom = atom_of_formula f in
-  let t = convert_atom (fv = []) atom in
-  let rec build_ctx n = function
-    | [] -> t
-    | hp::tl -> 
-        PT.Binder 
-          (`Forall,
-            (mk_ident ("H" ^ string_of_int n), 
-              Some (convert_formula [] true [] hp)), 
-            build_ctx (n+1) tl)
-  in
-  let arities = if no_arities then [] else collect_arities atom context in
-  build_ctx_for_arities true arities (build_ctx 0 context) 
-;;
-
-let check_if_atom_is_negative = function
-  | A.True | A.False | A.Proposition _ | A.Predicate _ -> assert false
-  | A.Eq _ -> false
-  | A.NotEq _ -> true
-;;
-
-let check_if_formula_is_negative = function
-  | A.Disjunction _ -> assert false
-  | 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
-  | A.Comment s -> 
-      let s = String.sub s 1 (String.length s - 1) in
-      let s = 
-        if s.[String.length s - 1] = '\n' then
-          String.sub s 0 (String.length s - 1)
-        else 
-          s
-      in
-      statements @ [GA.Comment (floc,GA.Note (floc,s))],
-      context
-  | A.Inclusion (s,_) ->
-      statements @ [
-        GA.Comment (
-          floc, GA.Note (
-            floc,"Inclusion of: " ^ s))], context
-  | A.AnnotatedFormula (name,kind,f,_,_) -> 
-      match kind with
-      | A.Axiom 
-      | A.Hypothesis ->
-          statements, f::context
-      | 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 f = 
-            PT.Binder 
-             (`Forall,
-               (mk_ident universe,Some (PT.Sort `Set)), 
-               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))))]@
-          (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.Tactical(floc, GA.Try(floc,
-              GA.Tactic (floc, GA.Assumption floc)), Some (GA.Dot(floc))));
-            GA.Executable(floc,GA.Command(floc, GA.Qed(floc)))],
-          context
-      | A.Definition 
-      | A.Lemma 
-      | A.Theorem 
-      | A.Conjecture
-      | A.Lemma_conjecture 
-      | A.Plain 
-      | A.Unknown -> assert false
-;;
-
-(* OPTIONS *)
-let tptppath = ref "./";;
-let librarymode = ref false;;
-let spec = [
-  ("-tptppath", 
-      Arg.String (fun x -> tptppath := x), 
-      "Where to find the Axioms/ and Problems/ directory");
-  ("-librarymode",
-      Arg.Set librarymode,
-      "... not supported yet")
-]
-
-(* HELPERS *)
-let resolve s = 
-  let resolved_name = 
-    if Filename.check_suffix s ".p" then
-      (assert (String.length s > 5);
-      let prefix = String.sub s 0 3 in
-      !tptppath ^ "/Problems/" ^ prefix ^ "/" ^ s)
-    else
-      !tptppath ^ "/" ^ s
-  in
-  if HExtlib.is_regular resolved_name then
-    resolved_name
-  else
-    begin
-      prerr_endline ("Unable to find " ^ s ^ " (" ^ resolved_name ^ ")");
-      exit 1
-    end
-;;
-
-(* MAIN *)
-let _ =
-  let usage = "Usage: tptp2grafite [options] file" in
-  let inputfile = ref "" in
-  Arg.parse spec (fun s -> inputfile := s) usage;
-  if !inputfile = "" then 
-    begin
-      prerr_endline usage;
-      exit 1
-    end;
-  let rec aux = function
-    | [] -> []
-    | ((A.Inclusion (file,_)) as hd) :: tl ->
-        let file = resolve file in
-        let lexbuf = Lexing.from_channel (open_in file) in
-        let statements = Parser.main Lexer.yylex lexbuf in
-        hd :: aux (statements @ tl)
-    | hd::tl -> hd :: aux tl
-  in
-  let statements = aux [A.Inclusion (!inputfile ^ ".p",[])] in
-  let grafite_ast_statements,_ = 
-    List.fold_left 
-      (fun (st, ctx) f -> 
-        let newst, ctx = convert_ast st ctx f in
-        newst, ctx)
-      ([],[]) statements 
-  in
-  let pp t = 
-    (* ZACK: setting width to 80 will trigger a bug of BoxPp.render_to_string
-     * 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 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
-      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
-    print_endline 
-      (GrafiteAstPp.pp_statement ~term_pp ~lazy_term_pp ~obj_pp t)
-  in
-  let extra_statements_start = [
-    GA.Executable(floc,GA.Command(floc,
-      GA.Set(floc,"baseuri","cic:/matita/TPTP/" ^ !inputfile)));
-    GA.Executable(floc,GA.Command(floc, GA.Include(floc,"logic/equality.ma")))]
-  in
-  List.iter pp extra_statements_start;
-  List.iter 
-   (fun (n,s) -> 
-   print_endline
-    (LexiconAstPp.pp_command 
-      (LA.Alias(floc,
-        LA.Ident_alias(n,s))) ^ "."))
-   [(*("eq","cic:/Coq/Init/Logic/eq.ind#xpointer(1/1)");
-   ("trans_eq","cic:/Coq/Init/Logic/trans_eq.con");
-   ("eq_ind_r","cic:/Coq/Init/Logic/eq_ind_r.con");
-   ("eq_ind","cic:/Coq/Init/Logic/eq_ind.con");
-   ("sym_eq","cic:/Coq/Init/Logic/sym_eq.con");
-   ("refl_equal","cic:/Coq/Init/Logic/eq.ind#xpointer(1/1/1)") *)];
-  List.iter pp grafite_ast_statements;
-  exit 0
diff --git a/helm/software/components/binaries/tptp2grafite/parser.mly b/helm/software/components/binaries/tptp2grafite/parser.mly
deleted file mode 100644 (file)
index 0557700..0000000
+++ /dev/null
@@ -1,145 +0,0 @@
-%{
-  (* header *)
-  open Ast
-  open Parsing
-  open Lexing
-  
-  let parse_error s = Printf.eprintf "%s: " s ;;
-  let rm_q s = String.sub s 1 (String.length s - 2) ;;
-  
-%}
-  %token <string> TYPE
-  %token <string> COMMENT
-  %token <int> NUM
-  %token <string> LNAME
-  %token <string> UNAME
-  %token <string> QSTRING
-  %token COMMA
-  %token INCLUSION
-  %token LPAREN
-  %token RPAREN
-  %token CNF
-  %token TRUE
-  %token FALSE
-  %token IOR
-  %token NOT
-  %token NIEQ
-  %token IEQ
-  %token PEQ
-  %token DOT
-  %token EOF
-
-  %type <Ast.ast list> main
-  %start main
-%%
-  main: 
-    | tptp_input EOF {[$1]}
-    | tptp_input main {$1::$2}
-    | error { 
-        let start_pos = rhs_start_pos 1 in
-                               let end_pos = rhs_end_pos 1 in
-                               Printf.eprintf "from line %d char %d to line %d char %d\n" 
-          start_pos.pos_lnum (start_pos.pos_cnum - start_pos.pos_bol)
-          end_pos.pos_lnum (end_pos.pos_cnum - end_pos.pos_bol);
-        exit 1
-       }
-  ;
-
-  tptp_input:
-    | annot_formula {$1}
-    | include_ {$1}
-    | comment {$1}
-  ;
-  annot_formula: 
-    | CNF LPAREN 
-            name COMMA formula_type COMMA formula formula_source_and_infos 
-          RPAREN DOT {
-            AnnotatedFormula ($3,$5,$7,fst $8,snd $8)  
-      }
-  ;
-  
-  formula_type: 
-    | TYPE {
-        match $1 with
-        | "axiom" -> Axiom 
-        | "hypothesis" -> Hypothesis
-        | "definition" -> Definition
-        | "lemma" -> Lemma
-        | "theorem" -> Theorem
-        | "conjecture" -> Conjecture
-        | "lemma_conjecture" -> Lemma_conjecture
-        | "negated_conjecture" -> Negated_conjecture
-        | "plain" -> Plain
-        | "unknown" -> Unknown
-        | _ -> assert false
-      }
-  ;
-  
-  formula:
-    | LPAREN disjunction RPAREN {$2}
-    | disjunction {$1}
-  ;
-
-  disjunction:
-    | literal {$1}
-    | literal IOR disjunction {
-        Disjunction ($1,$3)
-      } 
-  ;
-
-  literal:
-    | NOT atom { NegAtom $2 } 
-    | atom { Atom $1 } 
-  ;
-
-  atom: 
-    | atomic_word LPAREN term_list RPAREN { Predicate ($1,$3) }
-    | atomic_word { Proposition $1 } 
-    | TRUE { True } 
-    | FALSE { False }
-    | term IEQ term { Eq ($1,$3) }
-    | term NIEQ term { NotEq ($1,$3) }
-    | PEQ LPAREN term COMMA term RPAREN { Eq ($3,$5) }
-  ;
-
-  term_list:
-    | term { [$1] }
-    | term COMMA term_list { $1 :: $3 }
-  ;
-
-  term:
-    | upper_word { Variable $1 }
-    | atomic_word LPAREN term_list RPAREN { Function ($1,$3) }
-    | atomic_word { Constant $1 }
-  ;
-
-  upper_word: UNAME { $1 } ;
-  
-  atomic_word:
-    | LNAME { $1 }
-    | QSTRING { rm_q $1 }
-  ;
-  
-  formula_source_and_infos:
-        | { NoSource, [NoInfo] }
-    | COMMA { assert false }
-  ;
-    
-  include_: 
-    | INCLUSION LPAREN QSTRING selection_of_formulae RPAREN DOT {
-        let fname = rm_q $3 in 
-        Inclusion (fname,$4)
-    } 
-  ;
-  
-  selection_of_formulae: 
-    | { [] } 
-    | COMMA name selection_of_formulae { $2::$3 } 
-  ;
-  
-  comment: COMMENT {Comment $1} ;
-
-  name: NUM { string_of_int $1} | LNAME { $1 } | UNAME { $1 } ;
-%%
-  (* trailer *)
diff --git a/helm/software/components/binaries/tptp2grafite/unit_equality_problems b/helm/software/components/binaries/tptp2grafite/unit_equality_problems
deleted file mode 100644 (file)
index c394ddd..0000000
+++ /dev/null
@@ -1,860 +0,0 @@
-ALG005-1
-ALG006-1
-ALG007-1
-BOO001-1
-BOO002-1
-BOO002-2
-BOO003-2
-BOO003-4
-BOO004-2
-BOO004-4
-BOO005-2
-BOO005-4
-BOO006-2
-BOO006-4
-BOO007-2
-BOO007-4
-BOO008-2
-BOO008-4
-BOO009-2
-BOO009-4
-BOO010-2
-BOO010-4
-BOO011-2
-BOO011-4
-BOO012-2
-BOO012-4
-BOO013-2
-BOO013-4
-BOO014-2
-BOO014-4
-BOO015-2
-BOO015-4
-BOO016-2
-BOO017-2
-BOO018-4
-BOO019-1
-BOO021-1
-BOO022-1
-BOO023-1
-BOO024-1
-BOO025-1
-BOO026-1
-BOO027-1
-BOO028-1
-BOO029-1
-BOO030-1
-BOO031-1
-BOO032-1
-BOO033-1
-BOO034-1
-BOO036-1
-BOO037-2
-BOO037-3
-BOO067-1
-BOO068-1
-BOO069-1
-BOO070-1
-BOO071-1
-BOO072-1
-BOO073-1
-BOO074-1
-BOO075-1
-BOO076-1
-BOO077-1
-BOO078-1
-BOO079-1
-BOO080-1
-BOO081-1
-BOO082-1
-BOO083-1
-BOO084-1
-BOO085-1
-BOO086-1
-BOO087-1
-BOO088-1
-BOO089-1
-BOO090-1
-BOO091-1
-BOO092-1
-BOO093-1
-BOO094-1
-BOO095-1
-BOO096-1
-BOO097-1
-BOO098-1
-BOO099-1
-BOO100-1
-BOO101-1
-BOO102-1
-BOO103-1
-BOO104-1
-BOO105-1
-BOO106-1
-BOO107-1
-BOO108-1
-COL001-1
-COL001-2
-COL002-1
-COL002-4
-COL002-5
-COL003-1
-COL003-1
-COL003-1
-COL003-1
-COL003-1
-COL003-1
-COL003-1
-COL003-1
-COL003-1
-COL003-2
-COL004-1
-COL004-3
-COL005-1
-COL006-1
-COL006-5
-COL006-6
-COL006-7
-COL007-1
-COL008-1
-COL009-1
-COL010-1
-COL011-1
-COL012-1
-COL013-1
-COL014-1
-COL015-1
-COL016-1
-COL017-1
-COL018-1
-COL019-1
-COL020-1
-COL021-1
-COL022-1
-COL023-1
-COL024-1
-COL025-1
-COL026-1
-COL027-1
-COL029-1
-COL030-1
-COL031-1
-COL032-1
-COL033-1
-COL034-1
-COL035-1
-COL036-1
-COL037-1
-COL038-1
-COL039-1
-COL041-1
-COL042-1
-COL042-6
-COL042-7
-COL042-8
-COL042-9
-COL043-1
-COL043-3
-COL044-1
-COL044-6
-COL044-7
-COL044-8
-COL044-9
-COL045-1
-COL046-1
-COL047-1
-COL048-1
-COL049-1
-COL050-1
-COL051-1
-COL052-1
-COL053-1
-COL056-1
-COL057-1
-COL058-1
-COL058-2
-COL058-3
-COL059-1
-COL060-1
-COL060-2
-COL060-3
-COL061-1
-COL061-2
-COL061-3
-COL062-1
-COL062-2
-COL062-3
-COL063-1
-COL063-2
-COL063-3
-COL063-4
-COL063-5
-COL063-6
-COL064-1
-COL064-2
-COL064-3
-COL064-4
-COL064-5
-COL064-6
-COL064-7
-COL064-8
-COL064-9
-COL064-1
-COL064-1
-COL065-1
-COL066-1
-COL066-2
-COL066-3
-COL067-1
-COL068-1
-COL069-1
-COL070-1
-COL071-1
-COL073-1
-COL075-2
-COL083-1
-COL084-1
-COL085-1
-COL086-1
-COL087-1
-GRP001-2
-GRP001-4
-GRP002-2
-GRP002-3
-GRP002-4
-GRP010-4
-GRP011-4
-GRP012-4
-GRP014-1
-GRP022-2
-GRP023-2
-GRP024-5
-GRP114-1
-GRP115-1
-GRP116-1
-GRP117-1
-GRP118-1
-GRP119-1
-GRP120-1
-GRP121-1
-GRP122-1
-GRP136-1
-GRP137-1
-GRP138-1
-GRP139-1
-GRP140-1
-GRP141-1
-GRP142-1
-GRP143-1
-GRP144-1
-GRP145-1
-GRP146-1
-GRP147-1
-GRP148-1
-GRP149-1
-GRP150-1
-GRP151-1
-GRP152-1
-GRP153-1
-GRP154-1
-GRP155-1
-GRP156-1
-GRP157-1
-GRP158-1
-GRP159-1
-GRP160-1
-GRP161-1
-GRP162-1
-GRP163-1
-GRP164-1
-GRP164-2
-GRP165-1
-GRP165-2
-GRP166-1
-GRP166-2
-GRP166-3
-GRP166-4
-GRP167-1
-GRP167-2
-GRP167-3
-GRP167-4
-GRP167-5
-GRP168-1
-GRP168-2
-GRP169-1
-GRP169-2
-GRP170-1
-GRP170-2
-GRP170-3
-GRP170-4
-GRP171-1
-GRP171-2
-GRP172-1
-GRP172-2
-GRP173-1
-GRP174-1
-GRP175-1
-GRP175-2
-GRP175-3
-GRP175-4
-GRP176-1
-GRP176-2
-GRP177-1
-GRP177-2
-GRP178-1
-GRP178-2
-GRP179-1
-GRP179-2
-GRP179-3
-GRP180-1
-GRP180-2
-GRP181-1
-GRP181-2
-GRP181-3
-GRP181-4
-GRP182-1
-GRP182-2
-GRP182-3
-GRP182-4
-GRP183-1
-GRP183-2
-GRP183-3
-GRP183-4
-GRP184-1
-GRP184-2
-GRP184-3
-GRP184-4
-GRP185-1
-GRP185-2
-GRP185-3
-GRP185-4
-GRP186-1
-GRP186-2
-GRP186-3
-GRP186-4
-GRP187-1
-GRP188-1
-GRP188-2
-GRP189-1
-GRP189-2
-GRP190-1
-GRP190-2
-GRP191-1
-GRP191-2
-GRP192-1
-GRP193-1
-GRP193-2
-GRP195-1
-GRP196-1
-GRP200-1
-GRP201-1
-GRP202-1
-GRP203-1
-GRP204-1
-GRP205-1
-GRP206-1
-GRP207-1
-GRP393-2
-GRP394-3
-GRP399-1
-GRP403-1
-GRP404-1
-GRP405-1
-GRP406-1
-GRP407-1
-GRP408-1
-GRP409-1
-GRP410-1
-GRP411-1
-GRP412-1
-GRP413-1
-GRP414-1
-GRP415-1
-GRP416-1
-GRP417-1
-GRP418-1
-GRP419-1
-GRP420-1
-GRP421-1
-GRP422-1
-GRP423-1
-GRP424-1
-GRP425-1
-GRP426-1
-GRP427-1
-GRP428-1
-GRP429-1
-GRP430-1
-GRP431-1
-GRP432-1
-GRP433-1
-GRP434-1
-GRP435-1
-GRP436-1
-GRP437-1
-GRP438-1
-GRP439-1
-GRP440-1
-GRP441-1
-GRP442-1
-GRP443-1
-GRP444-1
-GRP445-1
-GRP446-1
-GRP447-1
-GRP448-1
-GRP449-1
-GRP450-1
-GRP451-1
-GRP452-1
-GRP453-1
-GRP454-1
-GRP455-1
-GRP456-1
-GRP457-1
-GRP458-1
-GRP459-1
-GRP460-1
-GRP461-1
-GRP462-1
-GRP463-1
-GRP464-1
-GRP465-1
-GRP466-1
-GRP467-1
-GRP468-1
-GRP469-1
-GRP470-1
-GRP471-1
-GRP472-1
-GRP473-1
-GRP474-1
-GRP475-1
-GRP476-1
-GRP477-1
-GRP478-1
-GRP479-1
-GRP480-1
-GRP481-1
-GRP482-1
-GRP483-1
-GRP484-1
-GRP485-1
-GRP486-1
-GRP487-1
-GRP488-1
-GRP489-1
-GRP490-1
-GRP491-1
-GRP492-1
-GRP493-1
-GRP494-1
-GRP495-1
-GRP496-1
-GRP497-1
-GRP498-1
-GRP499-1
-GRP500-1
-GRP501-1
-GRP502-1
-GRP503-1
-GRP504-1
-GRP505-1
-GRP506-1
-GRP507-1
-GRP508-1
-GRP509-1
-GRP510-1
-GRP511-1
-GRP512-1
-GRP513-1
-GRP514-1
-GRP515-1
-GRP516-1
-GRP517-1
-GRP518-1
-GRP519-1
-GRP520-1
-GRP521-1
-GRP522-1
-GRP523-1
-GRP524-1
-GRP525-1
-GRP526-1
-GRP527-1
-GRP528-1
-GRP529-1
-GRP530-1
-GRP531-1
-GRP532-1
-GRP533-1
-GRP534-1
-GRP535-1
-GRP536-1
-GRP537-1
-GRP538-1
-GRP539-1
-GRP540-1
-GRP541-1
-GRP542-1
-GRP543-1
-GRP544-1
-GRP545-1
-GRP546-1
-GRP547-1
-GRP548-1
-GRP549-1
-GRP550-1
-GRP551-1
-GRP552-1
-GRP553-1
-GRP554-1
-GRP555-1
-GRP556-1
-GRP557-1
-GRP558-1
-GRP559-1
-GRP560-1
-GRP561-1
-GRP562-1
-GRP563-1
-GRP564-1
-GRP565-1
-GRP566-1
-GRP567-1
-GRP568-1
-GRP569-1
-GRP570-1
-GRP571-1
-GRP572-1
-GRP573-1
-GRP574-1
-GRP575-1
-GRP576-1
-GRP577-1
-GRP578-1
-GRP579-1
-GRP580-1
-GRP581-1
-GRP582-1
-GRP583-1
-GRP584-1
-GRP585-1
-GRP586-1
-GRP587-1
-GRP588-1
-GRP589-1
-GRP590-1
-GRP591-1
-GRP592-1
-GRP593-1
-GRP594-1
-GRP595-1
-GRP596-1
-GRP597-1
-GRP598-1
-GRP599-1
-GRP600-1
-GRP601-1
-GRP602-1
-GRP603-1
-GRP604-1
-GRP605-1
-GRP606-1
-GRP607-1
-GRP608-1
-GRP609-1
-GRP610-1
-GRP611-1
-GRP612-1
-GRP613-1
-GRP614-1
-GRP615-1
-GRP616-1
-HWC004-1
-HWC004-2
-LAT006-1
-LAT007-1
-LAT008-1
-LAT009-1
-LAT010-1
-LAT011-1
-LAT012-1
-LAT013-1
-LAT014-1
-LAT016-1
-LAT017-1
-LAT018-1
-LAT019-1
-LAT020-1
-LAT021-1
-LAT022-1
-LAT023-1
-LAT024-1
-LAT025-1
-LAT026-1
-LAT027-1
-LAT028-1
-LAT031-1
-LAT032-1
-LAT033-1
-LAT034-1
-LAT038-1
-LAT039-1
-LAT039-2
-LAT040-1
-LAT042-1
-LAT043-1
-LAT044-1
-LAT045-1
-LAT046-1
-LAT047-1
-LAT048-1
-LAT049-1
-LAT050-1
-LAT051-1
-LAT052-1
-LAT053-1
-LAT054-1
-LAT055-2
-LAT059-1
-LAT060-1
-LAT061-1
-LAT062-1
-LAT063-1
-LAT070-1
-LAT071-1
-LAT072-1
-LAT073-1
-LAT074-1
-LAT075-1
-LAT076-1
-LAT077-1
-LAT078-1
-LAT079-1
-LAT080-1
-LAT081-1
-LAT082-1
-LAT083-1
-LAT084-1
-LAT085-1
-LAT086-1
-LAT087-1
-LAT088-1
-LAT089-1
-LAT090-1
-LAT091-1
-LAT092-1
-LAT093-1
-LAT094-1
-LAT095-1
-LAT096-1
-LAT097-1
-LAT098-1
-LAT099-1
-LAT100-1
-LAT101-1
-LAT102-1
-LAT103-1
-LAT104-1
-LAT105-1
-LAT106-1
-LAT107-1
-LAT108-1
-LAT109-1
-LAT110-1
-LAT111-1
-LAT112-1
-LAT113-1
-LAT114-1
-LAT115-1
-LAT116-1
-LAT117-1
-LAT118-1
-LAT119-1
-LAT120-1
-LAT121-1
-LAT122-1
-LAT123-1
-LAT124-1
-LAT125-1
-LAT126-1
-LAT127-1
-LAT128-1
-LAT129-1
-LAT130-1
-LAT131-1
-LAT132-1
-LAT133-1
-LAT134-1
-LAT135-1
-LAT136-1
-LAT137-1
-LAT138-1
-LAT139-1
-LAT140-1
-LAT141-1
-LAT142-1
-LAT143-1
-LAT144-1
-LAT145-1
-LAT146-1
-LAT147-1
-LAT148-1
-LAT149-1
-LAT150-1
-LAT151-1
-LAT152-1
-LAT153-1
-LAT154-1
-LAT155-1
-LAT156-1
-LAT157-1
-LAT158-1
-LAT159-1
-LAT160-1
-LAT161-1
-LAT162-1
-LAT163-1
-LAT164-1
-LAT165-1
-LAT166-1
-LAT167-1
-LAT168-1
-LAT169-1
-LAT170-1
-LAT171-1
-LAT172-1
-LAT173-1
-LAT174-1
-LAT175-1
-LAT176-1
-LAT177-1
-LCL109-2
-LCL109-6
-LCL110-2
-LCL111-2
-LCL112-2
-LCL113-2
-LCL114-2
-LCL115-2
-LCL116-2
-LCL132-1
-LCL133-1
-LCL134-1
-LCL135-1
-LCL136-1
-LCL137-1
-LCL138-1
-LCL139-1
-LCL140-1
-LCL141-1
-LCL153-1
-LCL154-1
-LCL155-1
-LCL156-1
-LCL157-1
-LCL158-1
-LCL159-1
-LCL160-1
-LCL161-1
-LCL162-1
-LCL163-1
-LCL164-1
-LCL165-1
-LCL407-1
-LCL407-2
-LCL409-1
-LCL410-1
-LDA001-1
-LDA002-1
-LDA007-3
-RNG007-4
-RNG008-3
-RNG008-4
-RNG008-7
-RNG009-5
-RNG009-7
-RNG010-5
-RNG010-6
-RNG010-7
-RNG011-5
-RNG012-6
-RNG013-6
-RNG014-6
-RNG015-6
-RNG016-6
-RNG017-6
-RNG018-6
-RNG019-6
-RNG019-7
-RNG020-6
-RNG020-7
-RNG021-6
-RNG021-7
-RNG023-6
-RNG023-7
-RNG024-6
-RNG024-7
-RNG025-4
-RNG025-5
-RNG025-6
-RNG025-7
-RNG025-8
-RNG025-9
-RNG026-6
-RNG026-7
-RNG027-5
-RNG027-7
-RNG027-8
-RNG027-9
-RNG028-5
-RNG028-7
-RNG028-8
-RNG028-9
-RNG029-5
-RNG029-6
-RNG029-7
-RNG030-6
-RNG030-7
-RNG031-6
-RNG031-7
-RNG032-6
-RNG032-7
-RNG033-6
-RNG033-7
-RNG033-8
-RNG033-9
-RNG035-7
-RNG036-7
-RNG042-2
-RNG042-3
-RNG043-1
-ROB001-1
-ROB002-1
-ROB003-1
-ROB004-1
-ROB005-1
-ROB006-1
-ROB006-2
-ROB007-1
-ROB007-2
-ROB008-1
-ROB009-1
-ROB010-1
-ROB013-1
-ROB020-1
-ROB020-2
-ROB022-1
-ROB023-1
-ROB024-1
-ROB026-1
-ROB027-1
-ROB028-1
-ROB030-1
-ROB031-1
-ROB032-1
-SYN080-1
-SYN083-1
-SYN305-1
-SYN552-1
index 7a4112ad5a67350a9110b54d1cc4516fd848a451..dc36636fe816d4629d6f9f08c4cfb1207ee1c8e5 100644 (file)
@@ -55,17 +55,23 @@ let insert_unique e extract l =
 
 let set_default what l =
   match what,l with
-    "equality",[eq_URI;sym_eq_URI;trans_eq_URI;eq_ind_URI;eq_ind_r_URI] ->
+  "equality",[eq_URI;sym_eq_URI;trans_eq_URI;eq_ind_URI;
+              eq_ind_r_URI;eq_f_URI;eq_f_sym_URI] ->
       eq_URIs_ref :=
-       insert_unique (eq_URI,sym_eq_URI,trans_eq_URI,eq_ind_URI,eq_ind_r_URI)
-        (fun x,_,_,_,_ -> x) !eq_URIs_ref
+       insert_unique
+         (eq_URI,sym_eq_URI,trans_eq_URI,eq_ind_URI,
+          eq_ind_r_URI,eq_f_URI,eq_f_sym_URI)
+        (fun x,_,_,_,_,_,_ -> x) !eq_URIs_ref
   | "true",[true_URI] ->
       true_URIs_ref := insert_unique true_URI (fun x -> x) !true_URIs_ref
   | "false",[false_URI] ->
       false_URIs_ref := insert_unique false_URI (fun x -> x) !false_URIs_ref
   | "absurd",[absurd_URI] ->
       absurd_URIs_ref := insert_unique absurd_URI (fun x -> x) !absurd_URIs_ref
-  | _,_ -> raise (NotRecognized what)
+  | _,l -> 
+      raise 
+        (NotRecognized (what^" with "^string_of_int(List.length l)^" params"))
+;;
 
 let reset_defaults () =
   eq_URIs_ref := default_eq_URIs;
@@ -76,11 +82,11 @@ let reset_defaults () =
 (**** LOOKUP FUNCTIONS ****)
 
 let eq_URI () =
- try let eq,_,_,_,_ = List.hd !eq_URIs_ref in Some eq
+ try let eq,_,_,_,_,_,_ = List.hd !eq_URIs_ref in Some eq
  with Failure "hd" -> None
 
 let is_eq_URI uri =
- List.exists (fun (eq,_,_,_,_) -> UriManager.eq eq uri) !eq_URIs_ref
+ List.exists (fun (eq,_,_,_,_,_,_) -> UriManager.eq eq uri) !eq_URIs_ref
 
 let is_eq_refl_URI uri =
   let urieq = UriManager.strip_xpointer uri in
@@ -89,39 +95,63 @@ let is_eq_refl_URI uri =
 ;;
 
 let is_eq_ind_URI uri =
- List.exists (fun (_,_,_,eq_ind,_) -> UriManager.eq eq_ind uri) !eq_URIs_ref
+ List.exists (fun (_,_,_,eq_ind,_,_,_) -> UriManager.eq eq_ind uri) !eq_URIs_ref
 
 let is_eq_ind_r_URI uri =
- List.exists (fun (_,_,_,_,eq_ind_r) -> UriManager.eq eq_ind_r uri) !eq_URIs_ref
+ List.exists (fun (_,_,_,_,eq_ind_r,_,_) -> UriManager.eq eq_ind_r uri) !eq_URIs_ref
 let is_trans_eq_URI uri = 
- List.exists (fun (_,_,trans_eq,_,_) -> UriManager.eq trans_eq uri) !eq_URIs_ref
+ List.exists (fun (_,_,trans_eq,_,_,_,_) -> UriManager.eq trans_eq uri) !eq_URIs_ref
 let is_sym_eq_URI uri =
- List.exists (fun (_,sym_eq,_,_,_) -> UriManager.eq sym_eq uri) !eq_URIs_ref
+ List.exists (fun (_,sym_eq,_,_,_,_,_) -> UriManager.eq sym_eq uri) !eq_URIs_ref
+let is_eq_f_URI uri =
+ List.exists (fun (_,_,_,_,_,eq_f,_) -> UriManager.eq eq_f uri) !eq_URIs_ref
+let is_eq_f_sym_URI uri =
+ List.exists (fun (_,_,_,_,_,_,eq_f1) -> UriManager.eq eq_f1 uri) !eq_URIs_ref
+
 
 let eq_refl_URI ~eq:uri =
   let uri = UriManager.strip_xpointer uri in
   UriManager.uri_of_string (UriManager.string_of_uri uri ^ "#xpointer(1/1/1)")
  
 let sym_eq_URI ~eq:uri =
  try
-  let _,x,_,_,_ = List.find (fun eq,_,_,_,_ -> UriManager.eq eq uri) !eq_URIs_ref in x
+  let _,x,_,_,_,_,_ = List.find (fun eq,_,_,_,_,_,_ -> UriManager.eq eq uri) !eq_URIs_ref in x
  with Not_found -> raise (NotRecognized (UriManager.string_of_uri uri))
 
 let trans_eq_URI ~eq:uri =
  try
-  let _,_,x,_,_ = List.find (fun eq,_,_,_,_ -> UriManager.eq eq uri) !eq_URIs_ref in x
+  let _,_,x,_,_,_,_ = List.find (fun eq,_,_,_,_,_,_ -> UriManager.eq eq uri) !eq_URIs_ref in x
  with Not_found -> raise (NotRecognized (UriManager.string_of_uri uri))
 
 let eq_ind_URI ~eq:uri =
  try
-  let _,_,_,x,_ = List.find (fun eq,_,_,_,_ -> UriManager.eq eq uri) !eq_URIs_ref in x
+  let _,_,_,x,_,_,_ = List.find (fun eq,_,_,_,_,_,_ -> UriManager.eq eq uri) !eq_URIs_ref in x
  with Not_found -> raise (NotRecognized (UriManager.string_of_uri uri))
 
 let eq_ind_r_URI ~eq:uri =
  try
-  let _,_,_,_,x = List.find (fun eq,_,_,_,_ -> UriManager.eq eq uri) !eq_URIs_ref in x
+  let _,_,_,_,x,_,_ = List.find (fun eq,_,_,_,_,_,_ -> UriManager.eq eq uri) !eq_URIs_ref in x
+ with Not_found -> raise (NotRecognized (UriManager.string_of_uri uri))
+
+let eq_f_URI ~eq:uri =
+ try
+  let _,_,_,_,_,x,_ = List.find (fun eq,_,_,_,_,_,_ -> UriManager.eq eq uri) !eq_URIs_ref in x
  with Not_found -> raise (NotRecognized (UriManager.string_of_uri uri))
 
+let eq_f_sym_URI ~eq:uri =
+ try
+  let _,_,_,_,_,_,x = List.find (fun eq,_,_,_,_,_,_ -> UriManager.eq eq uri) !eq_URIs_ref in x
+ with Not_found -> raise (NotRecognized (UriManager.string_of_uri uri))
+
+
+let eq_URI_of_eq_f_URI eq_f_URI = 
+  try
+  let x,_,_,_,_,_,_ = 
+    List.find (fun _,_,_,_,_,u,_ -> UriManager.eq eq_f_URI u) !eq_URIs_ref 
+  in x
+ with Not_found -> raise (NotRecognized (UriManager.string_of_uri eq_f_URI))
 let true_URI () =
  try Some (List.hd !true_URIs_ref) with Failure "hd" -> None
 let false_URI () =
index 9dfe5490229beca91fdf7a81c3535bc2e64e6c91..0cd9f2e975bb18801766fe52ac974e1c6232fedf 100644 (file)
@@ -34,6 +34,10 @@ val is_eq_ind_URI : UriManager.uri -> bool
 val is_eq_ind_r_URI : UriManager.uri -> bool
 val is_trans_eq_URI : UriManager.uri -> bool
 val is_sym_eq_URI : UriManager.uri -> bool
+val is_eq_f_URI : UriManager.uri -> bool
+val is_eq_f_sym_URI : UriManager.uri -> bool
+
+val eq_URI_of_eq_f_URI : UriManager.uri -> UriManager.uri
 
 exception NotRecognized of string;;
 
@@ -42,6 +46,8 @@ val eq_ind_URI : eq:UriManager.uri -> UriManager.uri
 val eq_ind_r_URI : eq:UriManager.uri -> UriManager.uri
 val trans_eq_URI : eq:UriManager.uri -> UriManager.uri
 val sym_eq_URI : eq:UriManager.uri -> UriManager.uri
+val eq_f_URI : eq:UriManager.uri -> UriManager.uri
+val eq_f_sym_URI : eq:UriManager.uri -> UriManager.uri
 
 
 val false_URI : unit -> UriManager.uri option
index e44c6b5881be2f47d260c66c6ed91142416ffd7a..feca7c3cfe07951bfd32d42ff29e74f0391e976f 100644 (file)
@@ -80,8 +80,10 @@ let rec pp t l =
        UriManager.string_of_uri (*UriManager.name_of_uri*) uri ^ pp_exp_named_subst exp_named_subst l
     | C.Meta (n,l1) ->
        "?" ^ (string_of_int n) ^ "[" ^ 
+(*
         String.concat " ; "
          (List.rev_map (function None -> "_" | Some t -> pp t l) l1) ^
+*)
         "]"
     | C.Sort s ->
        (match s with
index d16c75a761cd70b9bb06ddbdbf9e171cb0029079..2de502ee531e8f9cb5715f4afb030a450ded7be7 100644 (file)
@@ -1,5 +1,5 @@
 cicNotationPres.cmi: mpresentation.cmi box.cmi 
-boxPp.cmi: cicNotationPres.cmi 
+boxPp.cmi: mpresentation.cmi cicNotationPres.cmi box.cmi 
 content2pres.cmi: cicNotationPres.cmi 
 sequent2pres.cmi: cicNotationPres.cmi 
 renderingAttrs.cmo: renderingAttrs.cmi 
@@ -30,8 +30,8 @@ content2pres.cmo: termContentPres.cmi renderingAttrs.cmi mpresentation.cmi \
     cicNotationPres.cmi box.cmi content2pres.cmi 
 content2pres.cmx: termContentPres.cmx renderingAttrs.cmx mpresentation.cmx \
     cicNotationPres.cmx box.cmx content2pres.cmi 
-objPp.cmo: content2pres.cmi boxPp.cmi objPp.cmi 
-objPp.cmx: content2pres.cmx boxPp.cmx objPp.cmi 
+objPp.cmo: content2pres.cmi cicNotationPres.cmi boxPp.cmi objPp.cmi 
+objPp.cmx: content2pres.cmx cicNotationPres.cmx boxPp.cmx objPp.cmi 
 sequent2pres.cmo: termContentPres.cmi mpresentation.cmi cicNotationPres.cmi \
     box.cmi sequent2pres.cmi 
 sequent2pres.cmx: termContentPres.cmx mpresentation.cmx cicNotationPres.cmx \
index d38943da19ed732ce46f1528a16c531adcd2f46c..246df11c293144f981dec9ff84c51762c68a1f0d 100644 (file)
@@ -116,6 +116,7 @@ type 'obj command =
   | Include of loc * string
   | Set of loc * string * string
   | Drop of loc
+  | Print of loc * string
   | Qed of loc
   | Coercion of loc * UriManager.uri * bool (* add composites *)
   | Obj of loc * 'obj
index d35a8af114936570f77f4be4366d655d04bd0b2b..4a94152de956c5ea144f3af78e3ebd6d8392c37a 100644 (file)
@@ -207,6 +207,7 @@ let pp_command ~obj_pp = function
   | Include (_,path) -> "include \"" ^ path ^ "\""
   | Qed _ -> "qed"
   | Drop _ -> "drop"
+  | Print (_,s) -> "print " ^ s
   | Set (_, name, value) -> sprintf "set \"%s\" \"%s\"" name value
   | Coercion (_, uri, do_composites) -> pp_coercion uri do_composites
   | Obj (_,obj) -> obj_pp obj
index ab43c6cc18e67c0684562e4ed2a6dffeacb589bf..d99ab859311367572eb866e6f675bdb5612a3028 100644 (file)
@@ -582,6 +582,11 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status
  let status,cmd = disambiguate_command status (text,prefix_len,cmd) in
  let status,uris =
   match cmd with
+  | GrafiteAst.Print (_,"proofterm") ->
+      let _,_,p,_ = GrafiteTypes.get_current_proof status in
+      print_endline (AutoTactic.pp_proofterm p);
+      status,[]
+  | GrafiteAst.Print (_,_) -> status,[]
   | GrafiteAst.Default (loc, what, uris) as cmd ->
      LibraryObjects.set_default what uris;
      GrafiteTypes.add_moo_content [cmd] status,[]
index 0c02e1b6c38d86fdfcfb69ca51283dab32c5c677..0d59e4b469351dc7d39e2b2da2b0c5996780df82 100644 (file)
@@ -62,6 +62,7 @@ type status = {
 let get_current_proof status =
   match status.proof_status with
   | Incomplete_proof { proof = p } -> p
+  | Proof p -> p
   | _ -> raise (Statement_error "no ongoing proof")
 
 let get_proof_metasenv status =
index 76e5e6d86f13ae5257cd30e3a1e3081fecdf0eb9..04521361ddbb27215c87964a11cb697b37ca5171 100644 (file)
@@ -294,6 +294,7 @@ let disambiguate_command lexicon_status ~baseuri metasenv (text,prefix_len,cmd)=
   | GrafiteAst.Coercion _
   | GrafiteAst.Default _
   | GrafiteAst.Drop _
+  | GrafiteAst.Print _
   | GrafiteAst.Include _
   | GrafiteAst.Qed _
   | GrafiteAst.Set _ as cmd ->
index fadecd61e9e76825b355cfb2acdb541a436fd129..13ee7297eacec364ab468ce5b29209b36371c7e3 100644 (file)
@@ -467,6 +467,7 @@ EXTEND
       IDENT "set"; n = QSTRING; v = QSTRING ->
         GrafiteAst.Set (loc, n, v)
     | IDENT "drop" -> GrafiteAst.Drop loc
+    | IDENT "print"; s = IDENT -> GrafiteAst.Print (loc,s)
     | IDENT "qed" -> GrafiteAst.Qed loc
     | IDENT "variant" ; name = IDENT; SYMBOL ":"; 
       typ = term; SYMBOL <:unicode<def>> ; newname = IDENT ->
index a59294aaa73f7eb3173b1d6047809f27061fee76..338e84bbe4d2294617d050e4ab35c417efd276ad 100644 (file)
@@ -59,6 +59,12 @@ let paths_and_uris_of_obj uri =
   xmlunivgraphpath, univgraphuri
 
 let save_object_to_disk uri obj ugraph univlist =
+  let write f x =
+    if not (Helm_registry.get_opt_default 
+              Helm_registry.bool "matita.nodisk" ~default:false) 
+    then      
+      f x
+  in
   let ensure_path_exists path =
     let dir = Filename.dirname path in
     HExtlib.mkdir dir
@@ -74,11 +80,11 @@ let save_object_to_disk uri obj ugraph univlist =
       xmlunivgraphpath, univgraphuri = 
     paths_and_uris_of_obj uri 
   in
-  List.iter HExtlib.mkdir (List.map Filename.dirname [xmlpath]);
+  write (List.iter HExtlib.mkdir) (List.map Filename.dirname [xmlpath]);
   (* now write to disk *)
-  ensure_path_exists xmlpath;
-  Xml.pp ~gzip:true xml (Some xmlpath);
-  CicUniv.write_xml_of_ugraph xmlunivgraphpath ugraph univlist;
+  write ensure_path_exists xmlpath;
+  write (Xml.pp ~gzip:true xml) (Some xmlpath);
+  write (CicUniv.write_xml_of_ugraph xmlunivgraphpath ugraph) univlist;
   (* we return a list of uri,path we registered/created *)
   (uri,xmlpath) ::
   (univgraphuri,xmlunivgraphpath) ::
@@ -86,8 +92,8 @@ let save_object_to_disk uri obj ugraph univlist =
     (match bodyxml,bodyuri with
        None,_ -> []
      | Some bodyxml,Some bodyuri->
-         ensure_path_exists xmlbodypath;
-         Xml.pp ~gzip:true bodyxml (Some xmlbodypath);
+         write ensure_path_exists xmlbodypath;
+         write (Xml.pp ~gzip:true bodyxml) (Some xmlbodypath);
          [bodyuri, xmlbodypath]
      | _-> assert false) 
 
index 479e6738124461d50597c89728fe5d9835b5943e..9f5034a589dede7f45b7ec7ecbde5041882f01a8 100644 (file)
@@ -72,8 +72,11 @@ let profile_stop _ label =
   stop label extra
 ;;
 
+(*
 Quotation.add "profiler" (Quotation.ExStr banner);;
 Quotation.add "profile" (Quotation.ExStr profile_start_stop);;
 Quotation.add "start" (Quotation.ExStr profile_start);;
 Quotation.add "stop" (Quotation.ExStr profile_stop);;
 Quotation.add "show" (Quotation.ExStr profile_show);;
+*)
+
index d4dc5592c78379caa95f6d32fffd8af8d9f7b889..f063eeafb69ff99d7d49bf6b6810d6768f302e41 100644 (file)
@@ -494,3 +494,5 @@ let applyS_tac ~dbd ~term =
     | CicUnification.UnificationFailure msg
     | CicTypeChecker.TypeCheckerFailure msg ->
         raise (ProofEngineTypes.Fail msg))
+
+let pp_proofterm = Equality.pp_proofterm;;
index 1dfe0e2a94c60284fa8c262f8caf5caf8c86c4d7..354b1b7387d0b1496ded7981740d32e585af3f6b 100644 (file)
@@ -30,3 +30,5 @@ val auto_tac:
   ProofEngineTypes.tactic
 
 val applyS_tac: dbd:HMysql.dbd -> term: Cic.term -> ProofEngineTypes.tactic
+
+val pp_proofterm: Cic.term -> string
index 368a80f5d7f03b8a5242fc828110b85cd2255b3b..0b0b73e3f27c74ff0d5fefc202d904937726253c 100644 (file)
@@ -23,7 +23,7 @@
  * http://cs.unibo.it/helm/.
  *)
 
-let _profiler = <:profiler<_profiler>>;;
+(* let _profiler = <:profiler<_profiler>>;; *)
 
 (* $Id: inference.ml 6245 2006-04-05 12:07:51Z tassi $ *)
 
@@ -94,7 +94,8 @@ let string_of_equality ?env eq =
               id w (CicPp.ppterm ty)
               (CicPp.ppterm left) 
               (Utils.string_of_comparison o) (CicPp.ppterm right)
-        (String.concat ", " (List.map (fun (i,_,_) -> string_of_int i) m))
+        (*(String.concat ", " (List.map (fun (i,_,_) -> string_of_int i) m))*)
+        "..."
   | Some (_, context, _) -> 
       let names = Utils.names_of_context context in
       let w, _, (ty, left, right, o), m , id = open_equality eq in
@@ -102,7 +103,8 @@ let string_of_equality ?env eq =
               id w (CicPp.pp ty names)
               (CicPp.pp left names) (Utils.string_of_comparison o)
               (CicPp.pp right names)
-        (String.concat ", " (List.map (fun (i,_,_) -> string_of_int i) m))
+(*         (String.concat ", " (List.map (fun (i,_,_) -> string_of_int i) m)) *)
+           "..."
 ;;
 
 let compare (_,_,_,s1,_,_) (_,_,_,s2,_,_) =
@@ -326,10 +328,9 @@ let canonical t context menv =
                      (canonical context (mk_sym uri_sym ty m r p2)) 
                      (canonical context (mk_sym uri_sym ty l m p1))
              | Cic.Appl (([Cic.Const(uri_feq,ens);ty1;ty2;f;x;y;p])) ->
-                 
-                 let eq_f_sym = 
-                   Cic.Const (UriManager.uri_of_string
-                     "cic:/matita/logic/equality/eq_f1.con",[]) 
+                 let eq = LibraryObjects.eq_URI_of_eq_f_URI uri_feq in
+                 let eq_f_sym =
+                   Cic.Const (LibraryObjects.eq_f_sym_URI ~eq, [])
                  in
                  Cic.Appl (([eq_f_sym;ty1;ty2;f;x;y;p]))  
 
@@ -509,9 +510,8 @@ let contextualize uri ty left right t =
     | t -> 
 (*         let uri_sym = LibraryObjects.sym_eq_URI ~eq:uri in *)
 (*         let uri_ind = LibraryObjects.eq_ind_URI ~eq:uri in *)
-        let uri_feq = 
-          UriManager.uri_of_string "cic:/matita/logic/equality/eq_f.con"
-        in
+
+        let uri_feq = LibraryObjects.eq_f_URI ~eq:uri in
         let pred = 
 (*           let r = CicSubstitution.lift 1 (put_in_ctx ctx_d left) in *)
           let l = 
@@ -599,7 +599,7 @@ let parametrize_proof p l r ty =
       (fun (instance,p,n) m -> 
         (instance@[m],
         Cic.Lambda 
-          (Cic.Name ("x"^string_of_int n),
+          (Cic.Name ("X"^string_of_int n),
           CicSubstitution.lift (lift_no - n - 1) (ty_of_m m),
           p),
         n+1)) 
@@ -636,12 +636,14 @@ let string_of_id names id =
     | Exact t -> 
         Printf.sprintf "%d = %s: %s = %s [%s]" id
           (CicPp.pp t names) (CicPp.pp l names) (CicPp.pp r names)
-        (String.concat ", " (List.map (fun (i,_,_) -> string_of_int i) m))
+          "..."
+(*         (String.concat ", " (List.map (fun (i,_,_) -> string_of_int i) m)) *)
     | Step (_,(step,id1, (_,id2), _) ) ->
         Printf.sprintf "%6d: %s %6d %6d   %s = %s [%s]" id
           (string_of_rule step)
           id1 id2 (CicPp.pp l names) (CicPp.pp r names)
-        (String.concat ", " (List.map (fun (i,_,_) -> string_of_int i) m))
+(*         (String.concat ", " (List.map (fun (i,_,_) -> string_of_int i) m)) *)
+          "..."
   with
       Not_found -> assert false
 
@@ -1141,7 +1143,7 @@ module IntSet = Set.Make(IntOT);;
 let n_purged = ref 0;;
 
 let collect alive1 alive2 alive3 =
-  let _ = <:start<collect>> in
+(*   let _ = <:start<collect>> in *)
   let deps_of id = 
     let p,_,_ = proof_of_id id in  
     match p with
@@ -1164,14 +1166,87 @@ let collect alive1 alive2 alive3 =
   in
   n_purged := !n_purged + List.length to_purge;
   List.iter (Hashtbl.remove id_to_eq) to_purge;
-  let _ = <:stop<collect>> in ()  
+(*   let _ = <:stop<collect>> in ()   *)
 ;;
 
 let id_of e = 
   let _,_,_,_,id = open_equality e in id
 ;;
 
-let get_stats () = 
+let get_stats () = "" 
+(*
   <:show<Equality.>> ^ 
   "# of purged eq by the collector: " ^ string_of_int !n_purged ^ "\n"
+*)
+;;
+
+let rec pp_proofterm name t context = 
+  let rec skip_lambda tys ctx = function
+    | Cic.Lambda (n,s,t) -> skip_lambda (s::tys) ((Some n)::ctx) t
+    | t -> ctx,tys,t
+  in
+  let rename s name = 
+    match name with 
+    | Cic.Name s1 -> Cic.Name (s ^ s1)
+    | _ -> assert false
+  in
+  let rec skip_letin ctx = function
+    | Cic.LetIn (n,b,t) -> 
+        pp_proofterm (Some (rename "Lemma " n)) b ctx:: 
+          skip_letin ((Some n)::ctx) t
+    | t -> 
+        let ppterm t = CicPp.pp t ctx in
+        let rec pp inner = function
+          | Cic.Appl [Cic.Const (uri,[]);_;l;m;r;p1;p2] 
+              when Pcre.pmatch ~pat:"trans_eq" (UriManager.string_of_uri uri)->
+                if not inner then
+                  ("     " ^ ppterm l) :: pp true p1 @ 
+                            [ "   = " ^ ppterm m ] @ pp true p2 @ 
+                            [ "   = " ^ ppterm r ]
+                else
+                   pp true p1 @ 
+                            [ "   = " ^ ppterm m ] @ pp true p2 
+          | Cic.Appl [Cic.Const (uri,[]);_;l;m;p] 
+              when Pcre.pmatch ~pat:"sym_eq" (UriManager.string_of_uri uri)->
+                pp true p
+          | Cic.Appl [Cic.Const (uri,[]);_;_;_;_;_;p] 
+              when Pcre.pmatch ~pat:"eq_f" (UriManager.string_of_uri uri)->
+                pp true p
+          | Cic.Appl [Cic.Const (uri,[]);_;_;_;_;_;p] 
+              when Pcre.pmatch ~pat:"eq_f1" (UriManager.string_of_uri uri)->
+                pp true p
+          | Cic.Appl [Cic.MutConstruct (uri,_,_,[]);_;_;t;p] 
+              when Pcre.pmatch ~pat:"ex.ind" (UriManager.string_of_uri uri)->
+                      [ "witness " ^ ppterm t ] @ pp true p
+          | Cic.Appl (t::_) ->[ " [by " ^ ppterm t ^ "]"]
+          | t ->[ " [by " ^ ppterm t ^ "]"]
+        in
+        let rec compat = function
+          | a::b::tl -> (b ^ a) :: compat tl
+          | h::[] -> [h]
+          | [] -> []
+        in
+        let compat l = List.hd l :: compat (List.tl l) in
+        compat (pp false t) @ ["";""]
+  in      
+  let names, tys, body = skip_lambda [] context t in
+  let ppname name = (match name with Some (Cic.Name s) -> s | _ -> "") in
+  ppname name ^ ":\n" ^
+  (if context = [] then
+     let rec pp_l ctx = function
+          | (t,name)::tl -> 
+              "   " ^ ppname name ^ ": " ^ CicPp.pp t ctx ^ "\n" ^ 
+              pp_l (name::ctx) tl
+          | [] -> "\n\n"
+     in
+       pp_l [] (List.rev (List.combine tys names))
+   else "")
+    ^
+  String.concat "\n" (skip_letin names body)
 ;;
+
+let pp_proofterm t = 
+  "\n\n" ^ 
+  pp_proofterm (Some (Cic.Name "Hypothesis")) t []
+;;
+
index 019578ccc363d53d43c7c36f5af90bc9f707af4c..1a909dfc4b387c40465d5743bfc940964ba5e79c 100644 (file)
@@ -39,6 +39,8 @@ val pp_proof:
   (Cic.name option) list -> goal_proof -> proof -> Subst.substitution -> int ->
     Cic.term -> string
 
+val pp_proofterm: Cic.term -> string
+    
 val reset : unit -> unit
 
 val mk_equality :
@@ -71,7 +73,8 @@ val build_goal_proof:
   UriManager.uri -> goal_proof -> proof -> Cic.term-> int list -> 
     Cic.context -> Cic.metasenv -> 
     Cic.term * Cic.term list
-val build_proof_term : UriManager.uri -> (int * Cic.term) list -> int -> proof -> Cic.term
+val build_proof_term : 
+  UriManager.uri -> (int * Cic.term) list -> int -> proof -> Cic.term
 val refl_proof: UriManager.uri -> Cic.term -> Cic.term -> Cic.term 
 (** ensures that metavariables in equality are unique *)
 val fix_metas_goal: int -> goal -> int * goal
index a4bdef1a2a48b0121246ead95c73f21edb56183a..f3af1b482e8afb2eece8d1ce79d3e10af7812ec7 100644 (file)
@@ -23,7 +23,7 @@
  * http://cs.unibo.it/helm/.
  *)
 
-let _profiler = <:profiler<_profiler>>;;
+(* let _profiler = <:profiler<_profiler>>;; *)
 
 (* $Id$ *)
 
@@ -180,15 +180,9 @@ let get_candidates ?env mode tree term =
   let s = 
     match mode with
     | Matching -> 
-        let _ = <:start<retrieve_generalizations>> in
-        <:stop<retrieve_generalizations
         Index.retrieve_generalizations tree term
-        >>
     | Unification -> 
-        let _ = <:start<retrieve_unifiables>> in
-        <:stop<retrieve_unifiables
         Index.retrieve_unifiables tree term
-        >>
         
   in
   Index.PosEqSet.elements s
@@ -1039,4 +1033,4 @@ let rec demodulation_goal env table goal =
   | None -> do_right ()
 ;;
 
-let get_stats () = <:show<Indexing.>> ;;
+let get_stats () = "" ;;
index 408a7cdb8904771bc82a0e9f18dc2642ec66c0a1..f040241223bf3996f0972f3df4a4fcc8acbb89be 100644 (file)
@@ -23,7 +23,7 @@
  * http://cs.unibo.it/helm/.
  *)
 
-let _profiler = <:profiler<_profiler>>;;
+(* let _profiler = <:profiler<_profiler>>;; *)
 
 (* $Id$ *)
 
@@ -320,10 +320,10 @@ let equations_blacklist =
 let equations_blacklist = UriManager.UriSet.empty;;
 
 let tty_of_u u = 
-  let _ = <:start<tty_of_u>> in
+(*   let _ = <:start<tty_of_u>> in *)
   let t = CicUtil.term_of_uri u in
   let ty, _ = CicTypeChecker.type_of_aux' [] [] t CicUniv.empty_ugraph in
-  let _ = <:stop<tty_of_u>> in
+(*   let _ = <:stop<tty_of_u>> in *)
   t, ty
 ;;
 
@@ -336,7 +336,7 @@ let find_library_equalities caso_strano dbd context status maxmeta =
   let module C = Cic in
   let module S = CicSubstitution in
   let module T = CicTypeChecker in
-  let _ = <:start<equations_for_goal>> in
+(*   let _ = <:start<equations_for_goal>> in *)
   let signature = 
     if caso_strano then
       begin
@@ -364,7 +364,7 @@ let find_library_equalities caso_strano dbd context status maxmeta =
       None
   in
   let eqs = (MetadataQuery.equations_for_goal ~dbd ?signature status) in
-  let _ = <:stop<equations_for_goal>> in
+(*   let _ = <:stop<equations_for_goal>> in *)
   let candidates =
     List.fold_left
       (fun l uri ->
@@ -520,4 +520,4 @@ let find_context_hypotheses env equalities_indexes =
   res
 ;;
 
-let get_stats () = <:show<Inference.>> ;;
+let get_stats () = "" (*<:show<Inference.>>*) ;;
index c40b4a9ac238de328366c0c49fa9ec6e067dc23b..021afb5abdf0ed36f61450e6119d7fdc2230173c 100644 (file)
@@ -23,7 +23,7 @@
  * http://cs.unibo.it/helm/.
  *)
 
-let _profiler = <:profiler<_profiler>>;;
+(* let _profiler = <:profiler<_profiler>>;; *)
 
 (* $Id$ *)
 
@@ -174,9 +174,11 @@ let rec select env g passive =
                 if w < 30 then
                   hd, (tl, EqualitySet.remove hd pos_set)
                 else
+(*
                   (prerr_endline 
                     ("+++ skipping giant of size "^string_of_int w^" +++");
-                  select env g (tl@[hd],pos_set))
+*)
+                  select env g (tl@[hd],pos_set)
           | _ -> assert false
                   in
                    skip_giant pos_list pos_set)
@@ -265,8 +267,10 @@ let filter_dependent passive id =
            (eq::list, set), no)
       pos_list (([],pos_set),0)
   in
+(*
   if no_pruned > 0 then
     prerr_endline ("+++ pruning "^ string_of_int no_pruned ^" passives +++");  
+*)
   passive
 ;;
 
@@ -355,11 +359,11 @@ let infer eq_uri env current (active_list, active_table) =
       let maxm, copy_of_current = Equality.fix_metas !maxmeta current in
         maxmeta := maxm;
       let active_table =  Indexing.index active_table copy_of_current in
-      let _ = <:start<current contro active>> in
+(*       let _ = <:start<current contro active>> in *)
       let maxm, res =
         Indexing.superposition_right eq_uri !maxmeta env active_table current 
       in
-      let _ = <:stop<current contro active>> in
+(*       let _ = <:stop<current contro active>> in *)
       if Utils.debug_metas then
         ignore(List.map 
                  (function current -> 
@@ -386,9 +390,9 @@ let infer eq_uri env current (active_list, active_table) =
         maxmeta := maxm;
 *)
       let curr_table = Indexing.index Indexing.empty current in
-      let _ = <:start<active contro current>> in
+(*       let _ = <:start<active contro current>> in *)
       let pos = infer_positive curr_table ((*copy_of_current::*)active_list) in
-      let _ = <:stop<active contro current>> in
+(*       let _ = <:stop<active contro current>> in *)
       if Utils.debug_metas then 
         ignore(List.map 
                  (function current -> 
@@ -814,11 +818,13 @@ let check_if_goal_is_subsumed ((_,ctx,_) as env) table (goalproof,menv,ty) =
 (*      match Indexing.subsumption env table goal_equation with*)
        match Indexing.unification env table goal_equation with 
         | Some (subst, equality, swapped ) ->
+(*
             prerr_endline 
-              ("GOAL SUBSUMED IS: " ^ Equality.string_of_equality goal_equation ~env);
+             ("GOAL SUBSUMED IS: "^Equality.string_of_equality goal_equation ~env);
             prerr_endline 
-              ("GOAL IS SUBSUMED BY: " ^ Equality.string_of_equality equality ~env);
-            prerr_endline ("SUBST:" ^ Subst.ppsubst ~names subst);
+             ("GOAL IS SUBSUMED BY: "^Equality.string_of_equality equality ~env);
+            prerr_endline ("SUBST:"^Subst.ppsubst ~names subst);
+*)
             let (_,p,(ty,l,r,_),m,id) = Equality.open_equality equality in
             let cicmenv = Subst.apply_subst_metasenv subst (m @ menv) in
             let p =
@@ -899,8 +905,10 @@ let infer_goal_set env active goals =
     | [] -> active_goals, []
     | hd::tl ->
         let changed,selected = simplify_goal env hd active in
+(*
         if changed then
           prerr_endline ("--------------- goal semplificato");
+*)
         let (_,_,t1) = selected in
         let already_in = 
           List.exists (fun (_,_,t) -> Equality.meta_convertibility t t1) 
@@ -967,6 +975,13 @@ let pp_goals label goals context =
       (snd goals);
 ;;
 
+let print_status iterno goals active passive =
+  print_endline 
+    (Printf.sprintf "\n%d #ACTIVES: %d #PASSIVES: %d #GOALSET: %d(%d)"
+      iterno (size_of_active active) (size_of_passive passive)
+      (size_of_goal_set_a goals) (size_of_goal_set_p goals)) 
+;;
+
 (** given-clause algorithm with full reduction strategy: NEW implementation *)
 (* here goals is a set of goals in OR *)
 let given_clause 
@@ -989,17 +1004,9 @@ let given_clause
     else if Unix.gettimeofday () > max_time then
       (ParamodulationFailure "No more time to spend")
     else
-(*
-      let _ = prerr_endline "simpl goal with active" in
-      let _ = <:start<simplify goal set active>> in
-      let goals = simplify_goal_set env goals passive active in 
-      let _ = <:stop<simplify goal set active>> in
-*)
       let _ = 
-        prerr_endline 
-         (Printf.sprintf "%d #ACTIVES: %d #PASSIVES: %d #GOALSET: %d(%d)\n"
-           iterno (size_of_active active) (size_of_passive passive)
-           (size_of_goal_set_a goals) (size_of_goal_set_p goals)) 
+(*         print_status iterno goals active passive  *)
+        Printf.printf ".%!";
       in
       (* PRUNING OF PASSIVE THAT WILL NEVER BE PROCESSED *) 
       let passive =
@@ -1018,8 +1025,8 @@ let given_clause
       in
       match check_if_goals_set_is_solved env active goals with
       | Some p -> 
-          prerr_endline 
-            (Printf.sprintf "Found a proof in: %f\n" 
+          print_endline 
+            (Printf.sprintf "\nFound a proof in: %f\n" 
               (Unix.gettimeofday() -. initial_time));
           ParamodulationSuccess p
       | None -> 
@@ -1035,6 +1042,7 @@ let given_clause
               (* COLLECTION OF GARBAGED EQUALITIES *)
               if iterno mod 40 = 0 then
                 begin
+                  print_status iterno goals active passive;
                   let active = List.map Equality.id_of (fst active) in
                   let passive = List.map Equality.id_of (fst passive) in
                   let goal = ids_of_goal_set goals in
@@ -1042,24 +1050,21 @@ let given_clause
                 end;
               let current, passive = select env goals passive in
               (* SIMPLIFICATION OF CURRENT *)
+(*
               prerr_endline
                     ("Selected : " ^ 
                       Equality.string_of_equality ~env  current);
+*)
               let res = 
                 forward_simplify eq_uri env current active 
               in
               match res with
               | None -> step goals theorems passive active (iterno+1)
               | Some current ->
-(*
-                  prerr_endline 
-                    ("Selected simpl: " ^ 
-                      Equality.string_of_equality ~env  current);
-*)
                   (* GENERATION OF NEW EQUATIONS *)
-                  prerr_endline "infer";
+(*                   prerr_endline "infer"; *)
                   let new' = infer eq_uri env current active in
-                  prerr_endline "infer goal";
+(*                   prerr_endline "infer goal"; *)
 (*
       match check_if_goals_set_is_solved env active goals with
       | Some p -> 
@@ -1077,7 +1082,7 @@ let given_clause
                     infer_goal_set_with_current env current goals active 
                   in
                   (* FORWARD AND BACKWARD SIMPLIFICATION *)
-                  prerr_endline "fwd/back simpl";
+(*                   prerr_endline "fwd/back simpl"; *)
                   let rec simplify new' active passive head =
                     let new' = 
                       forward_simplify_new eq_uri env new' active 
@@ -1098,12 +1103,12 @@ let given_clause
                   let active, passive, new', head = 
                     simplify new' active passive []
                   in
-                  prerr_endline "simpl goal with new";
+(*                   prerr_endline "simpl goal with new"; *)
                   let goals = 
                     let a,b,_ = build_table new' in
-                    let _ = <:start<simplify_goal_set new>> in
+(*                     let _ = <:start<simplify_goal_set new>> in *)
                     let rc = simplify_goal_set env goals (a,b) in
-                    let _ = <:stop<simplify_goal_set new>> in
+(*                     let _ = <:stop<simplify_goal_set new>> in *)
                     rc
                   in
                   let passive = add_to_passive passive new' head in
@@ -1289,13 +1294,15 @@ let saturate
       raise (ProofEngineTypes.Fail (lazy ("NO proof found: " ^ s)))
   | ParamodulationSuccess 
     (goalproof,newproof,subsumption_id,subsumption_subst, proof_menv) ->
-      prerr_endline "OK, found a proof!";
-      prerr_endline 
+      print_endline "Proof:";
+      print_endline 
         (Equality.pp_proof names goalproof newproof subsumption_subst
           subsumption_id type_of_goal);
-      prerr_endline "ENDOFPROOFS___";
+(*       prerr_endline "ENDOFPROOFS"; *)
+(*
       prerr_endline ("max weight: " ^ 
        (string_of_int (Equality.max_weight goalproof newproof)));
+*)
       (* generation of the CIC proof *)
       let side_effects = 
         List.filter (fun i -> i <> goalno)
@@ -1308,7 +1315,7 @@ let saturate
           eq_uri goalproof initial type_of_goal side_effects
           context proof_menv
       in
-      prerr_endline ("PROOF: " ^ CicPp.pp goal_proof names);
+(*       prerr_endline ("PROOF: " ^ CicPp.pp goal_proof names); *)
       let goal_proof = Subst.apply_subst subsumption_subst goal_proof in
       let metas_still_open_in_proof = Utils.metas_of_term goal_proof in
 (*prerr_endline (CicPp.pp goal_proof names);*)
@@ -1318,7 +1325,7 @@ let saturate
         List.map (Subst.apply_subst subsumption_subst) side_effects_t
       in
       (* replacing fake mets with real ones *)
-      prerr_endline "replacing metas...";
+(*       prerr_endline "replacing metas..."; *)
       let irl=CicMkImplicit.identity_relocation_list_for_metavariable context in
       let goal_proof_menv, what, with_what,free_meta = 
         List.fold_left 
@@ -1351,7 +1358,8 @@ let saturate
           (ProofEngineHelpers.compare_metasenvs 
             ~oldmetasenv:metasenv ~newmetasenv:goal_proof_menv)
       in
-prerr_endline ("freemetas: " ^ String.concat "," (List.map string_of_int free_metas) );
+(* prerr_endline ("freemetas: " ^ String.concat "," (List.map string_of_int
+ * free_metas) ); *)
       (* check/refine/... build the new proof *)
       let replaced_goal = 
         ProofEngineReduction.replace
@@ -1376,7 +1384,7 @@ prerr_endline ("freemetas: " ^ String.concat "," (List.map string_of_int free_me
       let final_subst = 
         (goalno,(context,goal_proof,type_of_goal))::subst_side_effects
       in
-prerr_endline ("MENVreal_menv: " ^ CicMetaSubst.ppmetasenv [] real_menv);
+(* prerr_endline ("MENVreal_menv: " ^ CicMetaSubst.ppmetasenv [] real_menv); *)
       let _ = 
         try
           CicTypeChecker.type_of_aux' real_menv context goal_proof
@@ -1398,12 +1406,14 @@ prerr_endline ("MENVreal_menv: " ^ CicMetaSubst.ppmetasenv [] real_menv);
       let open_goals = 
         match free_meta with Some(Cic.Meta(m,_)) when m<>goalno ->[m] | _ ->[] 
       in
+(*
       Printf.eprintf 
         "GOALS APERTI: %s\nMETASENV PRIMA:\n%s\nMETASENV DOPO:\n%s\n" 
           (String.concat ", " (List.map string_of_int open_goals))
           (CicMetaSubst.ppmetasenv [] metasenv)
           (CicMetaSubst.ppmetasenv [] real_metasenv);
-      prerr_endline (Printf.sprintf "\nTIME NEEDED: %8.2f" time);
+*)
+      print_endline (Printf.sprintf "\nTIME NEEDED: %8.2f" time);
       proof, open_goals
 ;;
 
@@ -1736,8 +1746,10 @@ let superposition_tac ~target ~table ~subterms_only ~demod_table status =
   proof,[goalno]
 ;;
 
-let get_stats () = 
+let get_stats () = "" 
+(*
   <:show<Saturation.>> ^ Indexing.get_stats () ^ Inference.get_stats () ^
   Equality.get_stats ()
 ;;
+*)
 
diff --git a/helm/software/components/tptp_grafite/.depend b/helm/software/components/tptp_grafite/.depend
new file mode 100644 (file)
index 0000000..bc31032
--- /dev/null
@@ -0,0 +1,7 @@
+parser.cmi: ast.cmo 
+lexer.cmo: parser.cmi 
+lexer.cmx: parser.cmx 
+parser.cmo: ast.cmo parser.cmi 
+parser.cmx: ast.cmx parser.cmi 
+tptp2grafite.cmo: parser.cmi lexer.cmo ast.cmo tptp2grafite.cmi 
+tptp2grafite.cmx: parser.cmx lexer.cmx ast.cmx tptp2grafite.cmi 
diff --git a/helm/software/components/tptp_grafite/Makefile b/helm/software/components/tptp_grafite/Makefile
new file mode 100644 (file)
index 0000000..c5c6e63
--- /dev/null
@@ -0,0 +1,50 @@
+PACKAGE = tptp_grafite
+PREDICATES = 
+
+INTERFACE_FILES= parser.mli tptp2grafite.mli
+
+IMPLEMENTATION_FILES = ast.ml lexer.ml $(INTERFACE_FILES:%.mli=%.ml)
+EXTRA_OBJECTS_TO_INSTALL = 
+EXTRA_OBJECTS_TO_CLEAN =
+
+TPTPDIR=/home/$(USER)/TPTP-v3.1.1/
+
+all: tptp2grafite
+clean: clean_tests
+
+clean_tests:
+       rm -f tptp2grafite
+
+parser.mli parser.ml:parser.mly
+       ocamlyacc parser.mly
+lexer.ml:
+       ocamllex lexer.mll
+
+LOCAL_LINKOPTS = -package helm-$(PACKAGE) -linkpkg
+tptp2grafite: main.ml tptp_grafite.cma
+       @echo "  OCAMLC $<"
+       @$(OCAMLC) $(LOCAL_LINKOPTS) -o $@ $<
+
+test: tptp2grafite
+
+testall: tptp2grafite
+       for X in `cat unit_equality_problems`; do\
+               cat $(TPTPDIR)/$$X | ./tptp2grafite || echo ERROR PARSING $$X;\
+       done
+
+generate:
+       for X in `cat unit_equality_problems`; do\
+               ./tptp2grafite -tptppath $(TPTPDIR) $$X \
+               > ../../../matita/tests/TPTP/$$X.ma || echo Failed: $$X; \
+       done
+
+parse:
+       for X in `cat unit_equality_problems`; do\
+         echo "Parsing $$X"; \
+               ./tptp2grafite -tptppath $(TPTPDIR) $$X \
+               > /dev/null || echo Failed: $$X; \
+       done
+
+include ../../Makefile.defs
+include ../Makefile.common
+
diff --git a/helm/software/components/tptp_grafite/ast.ml b/helm/software/components/tptp_grafite/ast.ml
new file mode 100644 (file)
index 0000000..b8f855d
--- /dev/null
@@ -0,0 +1,31 @@
+type kinds_of_formulae = 
+  | Axiom | Hypothesis | Definition | Lemma | Theorem | Conjecture
+  | Lemma_conjecture | Negated_conjecture | Plain | Unknown
+
+type source = NoSource
+
+type info = NoInfo
+
+type term = 
+  | Variable of string
+  | Constant of string 
+  | Function of string * term list
+
+type atom = 
+  | Proposition of string
+  | Predicate of string * term list
+  | True
+  | False
+  | Eq of term * term
+  | NotEq of term * term
+
+type formulae = 
+  | Disjunction of formulae * formulae
+  | NegAtom of  atom
+  | Atom of atom
+  
+type ast = 
+  | Comment of string
+  | Inclusion of string * (string list)
+  | AnnotatedFormula of 
+      string * kinds_of_formulae * formulae * source * info list
diff --git a/helm/software/components/tptp_grafite/lexer.mll b/helm/software/components/tptp_grafite/lexer.mll
new file mode 100644 (file)
index 0000000..273d1b7
--- /dev/null
@@ -0,0 +1,57 @@
+{ 
+  open Parser
+  exception BadToken of string 
+  
+  let incr_linenum lexbuf =
+    let pos = lexbuf.Lexing.lex_curr_p in
+    lexbuf.Lexing.lex_curr_p <- { pos with
+      Lexing.pos_lnum = pos.Lexing.pos_lnum + 1;
+      Lexing.pos_bol = pos.Lexing.pos_cnum;
+    }
+  ;;
+  
+}
+
+let dust = ' ' | '\t'
+let comment = '%' [^ '\n' ] * '\n'
+let lname = 
+  ['a'-'z'] ['a'-'z''A'-'Z''0'-'9''_']*
+let uname = 
+  ['A'-'Z'] ['a'-'z''A'-'Z''0'-'9''_']*
+let qstring = ''' [^ ''' ]+ '''
+let type_ =   
+  "axiom" | "hypothesis" | "definition" | "lemma" | "theorem" |
+  "conjecture" | "lemma_conjecture" | "negated_conjecture" |
+  "plain" | "unknown"
+
+let ieq = "="
+let peq = "equal"
+let nieq = "!="
+
+rule yylex = parse 
+   | dust { yylex lexbuf }
+   | '\n' { incr_linenum lexbuf; yylex lexbuf }
+   | comment { incr_linenum lexbuf; COMMENT (Lexing.lexeme lexbuf) }
+   | "include" { INCLUSION }
+   | type_ { TYPE (Lexing.lexeme lexbuf) }
+   | "cnf" { CNF } 
+   | "$true" { TRUE }
+   | "$false" { FALSE }
+   | "equal" { PEQ }
+   
+   | lname { LNAME (Lexing.lexeme lexbuf) }
+   | uname { UNAME (Lexing.lexeme lexbuf) }
+   | ['0' - '9']+ { NUM (int_of_string (Lexing.lexeme lexbuf)) }
+   | ',' { COMMA }
+   | '.' { DOT }
+   | '(' { LPAREN }
+   | ')' { RPAREN }
+   | '|' { IOR }
+   | '~' { NOT }
+   | '=' { IEQ }
+   | "!=" { NIEQ }
+   | qstring { QSTRING (Lexing.lexeme lexbuf) }
+   | eof { EOF } 
+   | _ { raise (BadToken (Lexing.lexeme lexbuf)) }
+
+{ (* trailer *) }
diff --git a/helm/software/components/tptp_grafite/main.ml b/helm/software/components/tptp_grafite/main.ml
new file mode 100644 (file)
index 0000000..e52b77c
--- /dev/null
@@ -0,0 +1,22 @@
+(* OPTIONS *)
+let tptppath = ref "./";;
+let spec = [
+  ("-tptppath", 
+      Arg.String (fun x -> tptppath := x), 
+      "Where to find the Axioms/ and Problems/ directory")
+]
+
+(* MAIN *)
+let _ =
+  let usage = "Usage: tptp2grafite [options] file" in
+  let inputfile = ref "" in
+  Arg.parse spec (fun s -> inputfile := s) usage;
+  if !inputfile = "" then 
+    begin
+      prerr_endline usage;
+      exit 1
+    end;
+  print_endline 
+    (Tptp2grafite.tptp2grafite ~filename:!inputfile ~tptppath:!tptppath ());
+  exit 0
+
diff --git a/helm/software/components/tptp_grafite/parser.mly b/helm/software/components/tptp_grafite/parser.mly
new file mode 100644 (file)
index 0000000..0557700
--- /dev/null
@@ -0,0 +1,145 @@
+%{
+  (* header *)
+  open Ast
+  open Parsing
+  open Lexing
+  
+  let parse_error s = Printf.eprintf "%s: " s ;;
+  let rm_q s = String.sub s 1 (String.length s - 2) ;;
+  
+%}
+  %token <string> TYPE
+  %token <string> COMMENT
+  %token <int> NUM
+  %token <string> LNAME
+  %token <string> UNAME
+  %token <string> QSTRING
+  %token COMMA
+  %token INCLUSION
+  %token LPAREN
+  %token RPAREN
+  %token CNF
+  %token TRUE
+  %token FALSE
+  %token IOR
+  %token NOT
+  %token NIEQ
+  %token IEQ
+  %token PEQ
+  %token DOT
+  %token EOF
+
+  %type <Ast.ast list> main
+  %start main
+%%
+  main: 
+    | tptp_input EOF {[$1]}
+    | tptp_input main {$1::$2}
+    | error { 
+        let start_pos = rhs_start_pos 1 in
+                               let end_pos = rhs_end_pos 1 in
+                               Printf.eprintf "from line %d char %d to line %d char %d\n" 
+          start_pos.pos_lnum (start_pos.pos_cnum - start_pos.pos_bol)
+          end_pos.pos_lnum (end_pos.pos_cnum - end_pos.pos_bol);
+        exit 1
+       }
+  ;
+
+  tptp_input:
+    | annot_formula {$1}
+    | include_ {$1}
+    | comment {$1}
+  ;
+  annot_formula: 
+    | CNF LPAREN 
+            name COMMA formula_type COMMA formula formula_source_and_infos 
+          RPAREN DOT {
+            AnnotatedFormula ($3,$5,$7,fst $8,snd $8)  
+      }
+  ;
+  
+  formula_type: 
+    | TYPE {
+        match $1 with
+        | "axiom" -> Axiom 
+        | "hypothesis" -> Hypothesis
+        | "definition" -> Definition
+        | "lemma" -> Lemma
+        | "theorem" -> Theorem
+        | "conjecture" -> Conjecture
+        | "lemma_conjecture" -> Lemma_conjecture
+        | "negated_conjecture" -> Negated_conjecture
+        | "plain" -> Plain
+        | "unknown" -> Unknown
+        | _ -> assert false
+      }
+  ;
+  
+  formula:
+    | LPAREN disjunction RPAREN {$2}
+    | disjunction {$1}
+  ;
+
+  disjunction:
+    | literal {$1}
+    | literal IOR disjunction {
+        Disjunction ($1,$3)
+      } 
+  ;
+
+  literal:
+    | NOT atom { NegAtom $2 } 
+    | atom { Atom $1 } 
+  ;
+
+  atom: 
+    | atomic_word LPAREN term_list RPAREN { Predicate ($1,$3) }
+    | atomic_word { Proposition $1 } 
+    | TRUE { True } 
+    | FALSE { False }
+    | term IEQ term { Eq ($1,$3) }
+    | term NIEQ term { NotEq ($1,$3) }
+    | PEQ LPAREN term COMMA term RPAREN { Eq ($3,$5) }
+  ;
+
+  term_list:
+    | term { [$1] }
+    | term COMMA term_list { $1 :: $3 }
+  ;
+
+  term:
+    | upper_word { Variable $1 }
+    | atomic_word LPAREN term_list RPAREN { Function ($1,$3) }
+    | atomic_word { Constant $1 }
+  ;
+
+  upper_word: UNAME { $1 } ;
+  
+  atomic_word:
+    | LNAME { $1 }
+    | QSTRING { rm_q $1 }
+  ;
+  
+  formula_source_and_infos:
+        | { NoSource, [NoInfo] }
+    | COMMA { assert false }
+  ;
+    
+  include_: 
+    | INCLUSION LPAREN QSTRING selection_of_formulae RPAREN DOT {
+        let fname = rm_q $3 in 
+        Inclusion (fname,$4)
+    } 
+  ;
+  
+  selection_of_formulae: 
+    | { [] } 
+    | COMMA name selection_of_formulae { $2::$3 } 
+  ;
+  
+  comment: COMMENT {Comment $1} ;
+
+  name: NUM { string_of_int $1} | LNAME { $1 } | UNAME { $1 } ;
+%%
+  (* trailer *)
diff --git a/helm/software/components/tptp_grafite/tptp2grafite.ml b/helm/software/components/tptp_grafite/tptp2grafite.ml
new file mode 100644 (file)
index 0000000..841ac5f
--- /dev/null
@@ -0,0 +1,319 @@
+module GA = GrafiteAst;;
+module LA = LexiconAst;;
+module PT = CicNotationPt;;
+module A = Ast;;
+let floc = HExtlib.dummy_floc;;
+
+let universe = "Univ" ;;
+
+let kw = [
+ "and","myand"
+];;
+
+let mk_ident s =
+  PT.Ident ((try List.assoc s kw with Not_found -> s),None)
+;;
+
+let rec collect_arities_from_term = function
+  | A.Constant name -> [name,0]
+  | A.Variable name -> []
+  | A.Function (name,l) -> 
+      (name,List.length l)::List.flatten (List.map collect_arities_from_term l)
+;;
+
+let rec collect_fv_from_term = function
+  | A.Constant name -> []
+  | A.Variable name -> [name]
+  | A.Function (_,l) -> 
+      List.flatten (List.map collect_fv_from_term l)
+;;
+
+let collect_arities_from_atom a = 
+  let aux = function
+    | A.Proposition name -> assert false
+    | A.Predicate _ -> assert false
+    | 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
+  in
+  aux a
+;;
+  
+let collect_fv_from_atom a = 
+  let aux = function
+    | A.Proposition name -> assert false
+    | A.Predicate _ -> assert false
+    | 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 collect_fv_from_formulae = function
+  | A.Disjunction _ -> assert false
+  | A.NegAtom a 
+  | A.Atom a -> collect_fv_from_atom a
+;;
+
+let rec convert_term = function
+  | A.Variable x -> mk_ident x
+  | A.Constant x -> mk_ident x
+  | A.Function (name, args) -> 
+      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 mk_arrow component = function
+  | 0 -> mk_ident component
+  | n -> 
+      PT.Binder 
+        (`Forall,
+          ((mk_ident "_"),Some (mk_ident component)),
+          mk_arrow component (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 ->
+        PT.Binder 
+          (binder,
+            (mk_ident name,Some (mk_arrow universe nargs)),
+            aux tl)
+  in
+  aux arities
+;;
+
+let convert_atom universally a = 
+  let aux = function
+  | A.Proposition _ -> assert false
+  | A.Predicate (name,params) -> 
+      prerr_endline ("Predicate is unsupported: " ^ name);
+      assert false
+  | 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
+  build_ctx_for_arities universally 
+    (List.map (fun x -> (x,0)) (collect_fv_from_atom a)) (aux 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 assert_formulae_is_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"
+;;  
+
+let rec convert_formula fv no_arities context f =
+  let atom = atom_of_formula f in
+  let t = convert_atom (fv = []) atom in
+  let rec build_ctx n = function
+    | [] -> t
+    | hp::tl -> 
+        PT.Binder 
+          (`Forall,
+            (mk_ident ("H" ^ string_of_int n), 
+              Some (convert_formula [] true [] hp)), 
+            build_ctx (n+1) tl)
+  in
+  let arities = if no_arities then [] else collect_arities atom context in
+  build_ctx_for_arities true arities (build_ctx 0 context) 
+;;
+
+let check_if_atom_is_negative = function
+  | A.True | A.False | A.Proposition _ | A.Predicate _ -> assert false
+  | A.Eq _ -> false
+  | A.NotEq _ -> true
+;;
+
+let check_if_formula_is_negative = function
+  | A.Disjunction _ -> assert false
+  | 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
+  | A.Comment s -> 
+      let s = String.sub s 1 (String.length s - 1) in
+      let s = 
+        if s.[String.length s - 1] = '\n' then
+          String.sub s 0 (String.length s - 1)
+        else 
+          s
+      in
+      statements @ [GA.Comment (floc,GA.Note (floc,s))],
+      context
+  | A.Inclusion (s,_) ->
+      statements @ [
+        GA.Comment (
+          floc, GA.Note (
+            floc,"Inclusion of: " ^ s))], context
+  | A.AnnotatedFormula (name,kind,f,_,_) -> 
+      match kind with
+      | A.Axiom 
+      | A.Hypothesis ->
+          statements, f::context
+      | 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 f = 
+            PT.Binder 
+             (`Forall,
+               (mk_ident universe,Some (PT.Sort `Set)), 
+               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)))],
+          context
+      | A.Definition 
+      | A.Lemma 
+      | A.Theorem 
+      | A.Conjecture
+      | A.Lemma_conjecture 
+      | A.Plain 
+      | A.Unknown -> assert false
+;;
+
+(* HELPERS *)
+let resolve ~tptppath s = 
+  let resolved_name = 
+    if Filename.check_suffix s ".p" then
+      (assert (String.length s > 5);
+      let prefix = String.sub s 0 3 in
+      tptppath ^ "/Problems/" ^ prefix ^ "/" ^ s)
+    else
+      tptppath ^ "/" ^ s
+  in
+  if HExtlib.is_regular resolved_name then
+    resolved_name
+  else
+    begin
+      prerr_endline ("Unable to find " ^ s ^ " (" ^ resolved_name ^ ")");
+      exit 1
+    end
+;;
+
+(* MAIN *)
+let tptp2grafite ?raw_preamble ~tptppath ~filename () =
+  let rec aux = function
+    | [] -> []
+    | ((A.Inclusion (file,_)) as hd) :: tl ->
+        let file = resolve ~tptppath file in
+        let lexbuf = Lexing.from_channel (open_in file) in
+        let statements = Parser.main Lexer.yylex lexbuf in
+        hd :: aux (statements @ tl)
+    | hd::tl -> hd :: aux tl
+  in
+  let statements = aux [A.Inclusion (filename,[])] in
+  let grafite_ast_statements,_ = 
+    List.fold_left 
+      (fun (st, ctx) f -> 
+        let newst, ctx = convert_ast st ctx f in
+        newst, ctx)
+      ([],[]) statements 
+  in
+  let pp t = 
+    (* ZACK: setting width to 80 will trigger a bug of BoxPp.render_to_string
+     * 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 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
+      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
+  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)))]
+  in
+  let preamble = 
+    match raw_preamble with
+    | None -> 
+       pp (GA.Executable(floc,
+           GA.Command(floc,GA.Include(floc,"logic/equality.ma"))))
+    | Some s -> s buri
+  in
+  let extra_statements_end = [] in
+  let aliases = []
+   (*[("eq","cic:/Coq/Init/Logic/eq.ind#xpointer(1/1)");
+   ("trans_eq","cic:/Coq/Init/Logic/trans_eq.con");
+   ("eq_ind_r","cic:/Coq/Init/Logic/eq_ind_r.con");
+   ("eq_ind","cic:/Coq/Init/Logic/eq_ind.con");
+   ("sym_eq","cic:/Coq/Init/Logic/sym_eq.con");
+   ("refl_equal","cic:/Coq/Init/Logic/eq.ind#xpointer(1/1/1)")] *)
+  in
+  let s1 = List.map pp extra_statements_start in
+  let s2 = 
+    List.map 
+     (fun (n,s) -> 
+       LexiconAstPp.pp_command (LA.Alias(floc, LA.Ident_alias(n,s))) ^ ".")
+     aliases
+  in
+  let s3 = List.map pp grafite_ast_statements in
+  let s4 = List.map pp extra_statements_end in
+  String.concat "\n" (s1@[preamble]@s2@s3@s4)
+;;
diff --git a/helm/software/components/tptp_grafite/tptp2grafite.mli b/helm/software/components/tptp_grafite/tptp2grafite.mli
new file mode 100644 (file)
index 0000000..7dfa2d3
--- /dev/null
@@ -0,0 +1,29 @@
+(* Copyright (C) 2006, HELM Team.
+ * 
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ * 
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ * 
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA  02111-1307, USA.
+ * 
+ * For details, see the HELM World-Wide-Web page,
+ * http://helm.cs.unibo.it/
+ *)
+
+val tptp2grafite: 
+  ?raw_preamble:(string -> string) -> 
+  tptppath:string -> filename:string -> unit -> 
+    string 
diff --git a/helm/software/components/tptp_grafite/unit_equality_problems b/helm/software/components/tptp_grafite/unit_equality_problems
new file mode 100644 (file)
index 0000000..c394ddd
--- /dev/null
@@ -0,0 +1,860 @@
+ALG005-1
+ALG006-1
+ALG007-1
+BOO001-1
+BOO002-1
+BOO002-2
+BOO003-2
+BOO003-4
+BOO004-2
+BOO004-4
+BOO005-2
+BOO005-4
+BOO006-2
+BOO006-4
+BOO007-2
+BOO007-4
+BOO008-2
+BOO008-4
+BOO009-2
+BOO009-4
+BOO010-2
+BOO010-4
+BOO011-2
+BOO011-4
+BOO012-2
+BOO012-4
+BOO013-2
+BOO013-4
+BOO014-2
+BOO014-4
+BOO015-2
+BOO015-4
+BOO016-2
+BOO017-2
+BOO018-4
+BOO019-1
+BOO021-1
+BOO022-1
+BOO023-1
+BOO024-1
+BOO025-1
+BOO026-1
+BOO027-1
+BOO028-1
+BOO029-1
+BOO030-1
+BOO031-1
+BOO032-1
+BOO033-1
+BOO034-1
+BOO036-1
+BOO037-2
+BOO037-3
+BOO067-1
+BOO068-1
+BOO069-1
+BOO070-1
+BOO071-1
+BOO072-1
+BOO073-1
+BOO074-1
+BOO075-1
+BOO076-1
+BOO077-1
+BOO078-1
+BOO079-1
+BOO080-1
+BOO081-1
+BOO082-1
+BOO083-1
+BOO084-1
+BOO085-1
+BOO086-1
+BOO087-1
+BOO088-1
+BOO089-1
+BOO090-1
+BOO091-1
+BOO092-1
+BOO093-1
+BOO094-1
+BOO095-1
+BOO096-1
+BOO097-1
+BOO098-1
+BOO099-1
+BOO100-1
+BOO101-1
+BOO102-1
+BOO103-1
+BOO104-1
+BOO105-1
+BOO106-1
+BOO107-1
+BOO108-1
+COL001-1
+COL001-2
+COL002-1
+COL002-4
+COL002-5
+COL003-1
+COL003-1
+COL003-1
+COL003-1
+COL003-1
+COL003-1
+COL003-1
+COL003-1
+COL003-1
+COL003-2
+COL004-1
+COL004-3
+COL005-1
+COL006-1
+COL006-5
+COL006-6
+COL006-7
+COL007-1
+COL008-1
+COL009-1
+COL010-1
+COL011-1
+COL012-1
+COL013-1
+COL014-1
+COL015-1
+COL016-1
+COL017-1
+COL018-1
+COL019-1
+COL020-1
+COL021-1
+COL022-1
+COL023-1
+COL024-1
+COL025-1
+COL026-1
+COL027-1
+COL029-1
+COL030-1
+COL031-1
+COL032-1
+COL033-1
+COL034-1
+COL035-1
+COL036-1
+COL037-1
+COL038-1
+COL039-1
+COL041-1
+COL042-1
+COL042-6
+COL042-7
+COL042-8
+COL042-9
+COL043-1
+COL043-3
+COL044-1
+COL044-6
+COL044-7
+COL044-8
+COL044-9
+COL045-1
+COL046-1
+COL047-1
+COL048-1
+COL049-1
+COL050-1
+COL051-1
+COL052-1
+COL053-1
+COL056-1
+COL057-1
+COL058-1
+COL058-2
+COL058-3
+COL059-1
+COL060-1
+COL060-2
+COL060-3
+COL061-1
+COL061-2
+COL061-3
+COL062-1
+COL062-2
+COL062-3
+COL063-1
+COL063-2
+COL063-3
+COL063-4
+COL063-5
+COL063-6
+COL064-1
+COL064-2
+COL064-3
+COL064-4
+COL064-5
+COL064-6
+COL064-7
+COL064-8
+COL064-9
+COL064-1
+COL064-1
+COL065-1
+COL066-1
+COL066-2
+COL066-3
+COL067-1
+COL068-1
+COL069-1
+COL070-1
+COL071-1
+COL073-1
+COL075-2
+COL083-1
+COL084-1
+COL085-1
+COL086-1
+COL087-1
+GRP001-2
+GRP001-4
+GRP002-2
+GRP002-3
+GRP002-4
+GRP010-4
+GRP011-4
+GRP012-4
+GRP014-1
+GRP022-2
+GRP023-2
+GRP024-5
+GRP114-1
+GRP115-1
+GRP116-1
+GRP117-1
+GRP118-1
+GRP119-1
+GRP120-1
+GRP121-1
+GRP122-1
+GRP136-1
+GRP137-1
+GRP138-1
+GRP139-1
+GRP140-1
+GRP141-1
+GRP142-1
+GRP143-1
+GRP144-1
+GRP145-1
+GRP146-1
+GRP147-1
+GRP148-1
+GRP149-1
+GRP150-1
+GRP151-1
+GRP152-1
+GRP153-1
+GRP154-1
+GRP155-1
+GRP156-1
+GRP157-1
+GRP158-1
+GRP159-1
+GRP160-1
+GRP161-1
+GRP162-1
+GRP163-1
+GRP164-1
+GRP164-2
+GRP165-1
+GRP165-2
+GRP166-1
+GRP166-2
+GRP166-3
+GRP166-4
+GRP167-1
+GRP167-2
+GRP167-3
+GRP167-4
+GRP167-5
+GRP168-1
+GRP168-2
+GRP169-1
+GRP169-2
+GRP170-1
+GRP170-2
+GRP170-3
+GRP170-4
+GRP171-1
+GRP171-2
+GRP172-1
+GRP172-2
+GRP173-1
+GRP174-1
+GRP175-1
+GRP175-2
+GRP175-3
+GRP175-4
+GRP176-1
+GRP176-2
+GRP177-1
+GRP177-2
+GRP178-1
+GRP178-2
+GRP179-1
+GRP179-2
+GRP179-3
+GRP180-1
+GRP180-2
+GRP181-1
+GRP181-2
+GRP181-3
+GRP181-4
+GRP182-1
+GRP182-2
+GRP182-3
+GRP182-4
+GRP183-1
+GRP183-2
+GRP183-3
+GRP183-4
+GRP184-1
+GRP184-2
+GRP184-3
+GRP184-4
+GRP185-1
+GRP185-2
+GRP185-3
+GRP185-4
+GRP186-1
+GRP186-2
+GRP186-3
+GRP186-4
+GRP187-1
+GRP188-1
+GRP188-2
+GRP189-1
+GRP189-2
+GRP190-1
+GRP190-2
+GRP191-1
+GRP191-2
+GRP192-1
+GRP193-1
+GRP193-2
+GRP195-1
+GRP196-1
+GRP200-1
+GRP201-1
+GRP202-1
+GRP203-1
+GRP204-1
+GRP205-1
+GRP206-1
+GRP207-1
+GRP393-2
+GRP394-3
+GRP399-1
+GRP403-1
+GRP404-1
+GRP405-1
+GRP406-1
+GRP407-1
+GRP408-1
+GRP409-1
+GRP410-1
+GRP411-1
+GRP412-1
+GRP413-1
+GRP414-1
+GRP415-1
+GRP416-1
+GRP417-1
+GRP418-1
+GRP419-1
+GRP420-1
+GRP421-1
+GRP422-1
+GRP423-1
+GRP424-1
+GRP425-1
+GRP426-1
+GRP427-1
+GRP428-1
+GRP429-1
+GRP430-1
+GRP431-1
+GRP432-1
+GRP433-1
+GRP434-1
+GRP435-1
+GRP436-1
+GRP437-1
+GRP438-1
+GRP439-1
+GRP440-1
+GRP441-1
+GRP442-1
+GRP443-1
+GRP444-1
+GRP445-1
+GRP446-1
+GRP447-1
+GRP448-1
+GRP449-1
+GRP450-1
+GRP451-1
+GRP452-1
+GRP453-1
+GRP454-1
+GRP455-1
+GRP456-1
+GRP457-1
+GRP458-1
+GRP459-1
+GRP460-1
+GRP461-1
+GRP462-1
+GRP463-1
+GRP464-1
+GRP465-1
+GRP466-1
+GRP467-1
+GRP468-1
+GRP469-1
+GRP470-1
+GRP471-1
+GRP472-1
+GRP473-1
+GRP474-1
+GRP475-1
+GRP476-1
+GRP477-1
+GRP478-1
+GRP479-1
+GRP480-1
+GRP481-1
+GRP482-1
+GRP483-1
+GRP484-1
+GRP485-1
+GRP486-1
+GRP487-1
+GRP488-1
+GRP489-1
+GRP490-1
+GRP491-1
+GRP492-1
+GRP493-1
+GRP494-1
+GRP495-1
+GRP496-1
+GRP497-1
+GRP498-1
+GRP499-1
+GRP500-1
+GRP501-1
+GRP502-1
+GRP503-1
+GRP504-1
+GRP505-1
+GRP506-1
+GRP507-1
+GRP508-1
+GRP509-1
+GRP510-1
+GRP511-1
+GRP512-1
+GRP513-1
+GRP514-1
+GRP515-1
+GRP516-1
+GRP517-1
+GRP518-1
+GRP519-1
+GRP520-1
+GRP521-1
+GRP522-1
+GRP523-1
+GRP524-1
+GRP525-1
+GRP526-1
+GRP527-1
+GRP528-1
+GRP529-1
+GRP530-1
+GRP531-1
+GRP532-1
+GRP533-1
+GRP534-1
+GRP535-1
+GRP536-1
+GRP537-1
+GRP538-1
+GRP539-1
+GRP540-1
+GRP541-1
+GRP542-1
+GRP543-1
+GRP544-1
+GRP545-1
+GRP546-1
+GRP547-1
+GRP548-1
+GRP549-1
+GRP550-1
+GRP551-1
+GRP552-1
+GRP553-1
+GRP554-1
+GRP555-1
+GRP556-1
+GRP557-1
+GRP558-1
+GRP559-1
+GRP560-1
+GRP561-1
+GRP562-1
+GRP563-1
+GRP564-1
+GRP565-1
+GRP566-1
+GRP567-1
+GRP568-1
+GRP569-1
+GRP570-1
+GRP571-1
+GRP572-1
+GRP573-1
+GRP574-1
+GRP575-1
+GRP576-1
+GRP577-1
+GRP578-1
+GRP579-1
+GRP580-1
+GRP581-1
+GRP582-1
+GRP583-1
+GRP584-1
+GRP585-1
+GRP586-1
+GRP587-1
+GRP588-1
+GRP589-1
+GRP590-1
+GRP591-1
+GRP592-1
+GRP593-1
+GRP594-1
+GRP595-1
+GRP596-1
+GRP597-1
+GRP598-1
+GRP599-1
+GRP600-1
+GRP601-1
+GRP602-1
+GRP603-1
+GRP604-1
+GRP605-1
+GRP606-1
+GRP607-1
+GRP608-1
+GRP609-1
+GRP610-1
+GRP611-1
+GRP612-1
+GRP613-1
+GRP614-1
+GRP615-1
+GRP616-1
+HWC004-1
+HWC004-2
+LAT006-1
+LAT007-1
+LAT008-1
+LAT009-1
+LAT010-1
+LAT011-1
+LAT012-1
+LAT013-1
+LAT014-1
+LAT016-1
+LAT017-1
+LAT018-1
+LAT019-1
+LAT020-1
+LAT021-1
+LAT022-1
+LAT023-1
+LAT024-1
+LAT025-1
+LAT026-1
+LAT027-1
+LAT028-1
+LAT031-1
+LAT032-1
+LAT033-1
+LAT034-1
+LAT038-1
+LAT039-1
+LAT039-2
+LAT040-1
+LAT042-1
+LAT043-1
+LAT044-1
+LAT045-1
+LAT046-1
+LAT047-1
+LAT048-1
+LAT049-1
+LAT050-1
+LAT051-1
+LAT052-1
+LAT053-1
+LAT054-1
+LAT055-2
+LAT059-1
+LAT060-1
+LAT061-1
+LAT062-1
+LAT063-1
+LAT070-1
+LAT071-1
+LAT072-1
+LAT073-1
+LAT074-1
+LAT075-1
+LAT076-1
+LAT077-1
+LAT078-1
+LAT079-1
+LAT080-1
+LAT081-1
+LAT082-1
+LAT083-1
+LAT084-1
+LAT085-1
+LAT086-1
+LAT087-1
+LAT088-1
+LAT089-1
+LAT090-1
+LAT091-1
+LAT092-1
+LAT093-1
+LAT094-1
+LAT095-1
+LAT096-1
+LAT097-1
+LAT098-1
+LAT099-1
+LAT100-1
+LAT101-1
+LAT102-1
+LAT103-1
+LAT104-1
+LAT105-1
+LAT106-1
+LAT107-1
+LAT108-1
+LAT109-1
+LAT110-1
+LAT111-1
+LAT112-1
+LAT113-1
+LAT114-1
+LAT115-1
+LAT116-1
+LAT117-1
+LAT118-1
+LAT119-1
+LAT120-1
+LAT121-1
+LAT122-1
+LAT123-1
+LAT124-1
+LAT125-1
+LAT126-1
+LAT127-1
+LAT128-1
+LAT129-1
+LAT130-1
+LAT131-1
+LAT132-1
+LAT133-1
+LAT134-1
+LAT135-1
+LAT136-1
+LAT137-1
+LAT138-1
+LAT139-1
+LAT140-1
+LAT141-1
+LAT142-1
+LAT143-1
+LAT144-1
+LAT145-1
+LAT146-1
+LAT147-1
+LAT148-1
+LAT149-1
+LAT150-1
+LAT151-1
+LAT152-1
+LAT153-1
+LAT154-1
+LAT155-1
+LAT156-1
+LAT157-1
+LAT158-1
+LAT159-1
+LAT160-1
+LAT161-1
+LAT162-1
+LAT163-1
+LAT164-1
+LAT165-1
+LAT166-1
+LAT167-1
+LAT168-1
+LAT169-1
+LAT170-1
+LAT171-1
+LAT172-1
+LAT173-1
+LAT174-1
+LAT175-1
+LAT176-1
+LAT177-1
+LCL109-2
+LCL109-6
+LCL110-2
+LCL111-2
+LCL112-2
+LCL113-2
+LCL114-2
+LCL115-2
+LCL116-2
+LCL132-1
+LCL133-1
+LCL134-1
+LCL135-1
+LCL136-1
+LCL137-1
+LCL138-1
+LCL139-1
+LCL140-1
+LCL141-1
+LCL153-1
+LCL154-1
+LCL155-1
+LCL156-1
+LCL157-1
+LCL158-1
+LCL159-1
+LCL160-1
+LCL161-1
+LCL162-1
+LCL163-1
+LCL164-1
+LCL165-1
+LCL407-1
+LCL407-2
+LCL409-1
+LCL410-1
+LDA001-1
+LDA002-1
+LDA007-3
+RNG007-4
+RNG008-3
+RNG008-4
+RNG008-7
+RNG009-5
+RNG009-7
+RNG010-5
+RNG010-6
+RNG010-7
+RNG011-5
+RNG012-6
+RNG013-6
+RNG014-6
+RNG015-6
+RNG016-6
+RNG017-6
+RNG018-6
+RNG019-6
+RNG019-7
+RNG020-6
+RNG020-7
+RNG021-6
+RNG021-7
+RNG023-6
+RNG023-7
+RNG024-6
+RNG024-7
+RNG025-4
+RNG025-5
+RNG025-6
+RNG025-7
+RNG025-8
+RNG025-9
+RNG026-6
+RNG026-7
+RNG027-5
+RNG027-7
+RNG027-8
+RNG027-9
+RNG028-5
+RNG028-7
+RNG028-8
+RNG028-9
+RNG029-5
+RNG029-6
+RNG029-7
+RNG030-6
+RNG030-7
+RNG031-6
+RNG031-7
+RNG032-6
+RNG032-7
+RNG033-6
+RNG033-7
+RNG033-8
+RNG033-9
+RNG035-7
+RNG036-7
+RNG042-2
+RNG042-3
+RNG043-1
+ROB001-1
+ROB002-1
+ROB003-1
+ROB004-1
+ROB005-1
+ROB006-1
+ROB006-2
+ROB007-1
+ROB007-2
+ROB008-1
+ROB009-1
+ROB010-1
+ROB013-1
+ROB020-1
+ROB020-2
+ROB022-1
+ROB023-1
+ROB024-1
+ROB026-1
+ROB027-1
+ROB028-1
+ROB030-1
+ROB031-1
+ROB032-1
+SYN080-1
+SYN083-1
+SYN305-1
+SYN552-1
index d3f381e678befa66565e289191d13009cc8e2d9d..a1f233b6b7470de32200f0bf7363e69625d6b469 100644 (file)
@@ -76,6 +76,7 @@ FINDLIB_COMREQUIRES="\
 helm-cic_disambiguation \
 helm-grafite \
 helm-grafite_engine \
+helm-tptp_grafite \
 helm-grafite_parser \
 helm-hgdome \
 helm-tactics \
index b893373e12060f8ab15ef33e3f2b8b025fdc41e8..f67366bd7d031104d86dc45fc290ec5a5ffa7798 100644 (file)
@@ -14,10 +14,10 @@ matitacLib.cmo: matitamakeLib.cmi matitaMisc.cmi matitaInit.cmi \
     matitaExcPp.cmi matitaEngine.cmi buildTimeConf.cmi matitacLib.cmi 
 matitacLib.cmx: matitamakeLib.cmx matitaMisc.cmx matitaInit.cmx \
     matitaExcPp.cmx matitaEngine.cmx buildTimeConf.cmx matitacLib.cmi 
-matitac.cmo: matitamake.cmi matitadep.cmi matitaclean.cmi matitacLib.cmi \
-    gragrep.cmi 
-matitac.cmx: matitamake.cmx matitadep.cmx matitaclean.cmx matitacLib.cmx \
-    gragrep.cmx 
+matitac.cmo: matitaprover.cmo matitamake.cmi matitadep.cmi matitaclean.cmi \
+    matitacLib.cmi gragrep.cmi 
+matitac.cmx: matitaprover.cmx matitamake.cmx matitadep.cmx matitaclean.cmx \
+    matitacLib.cmx gragrep.cmx 
 matitadep.cmo: matitaInit.cmi matitadep.cmi 
 matitadep.cmx: matitaInit.cmx matitadep.cmi 
 matitaEngine.cmo: matitaEngine.cmi 
@@ -41,18 +41,20 @@ matitamakeLib.cmx: buildTimeConf.cmx matitamakeLib.cmi
 matitamake.cmo: matitamakeLib.cmi matitaInit.cmi matitamake.cmi 
 matitamake.cmx: matitamakeLib.cmx matitaInit.cmx matitamake.cmi 
 matitaMathView.cmo: matitaTypes.cmi matitaScript.cmi matitaMisc.cmi \
-    matitaGuiTypes.cmi matitaGtkMisc.cmi matitaExcPp.cmi buildTimeConf.cmi \
-    applyTransformation.cmi matitaMathView.cmi 
+    matitaGuiTypes.cmi matitaGtkMisc.cmi matitaExcPp.cmi lablGraphviz.cmi \
+    buildTimeConf.cmi applyTransformation.cmi matitaMathView.cmi 
 matitaMathView.cmx: matitaTypes.cmx matitaScript.cmx matitaMisc.cmx \
-    matitaGuiTypes.cmi matitaGtkMisc.cmx matitaExcPp.cmx buildTimeConf.cmx \
-    applyTransformation.cmx matitaMathView.cmi 
+    matitaGuiTypes.cmi matitaGtkMisc.cmx matitaExcPp.cmx lablGraphviz.cmx \
+    buildTimeConf.cmx applyTransformation.cmx matitaMathView.cmi 
 matitaMisc.cmo: buildTimeConf.cmi matitaMisc.cmi 
 matitaMisc.cmx: buildTimeConf.cmx matitaMisc.cmi 
 matita.cmo: matitaTypes.cmi matitaScript.cmi matitaMathView.cmi \
-    matitaInit.cmi matitaGui.cmi matitaGtkMisc.cmi lablGraphviz.cmi \
-    buildTimeConf.cmi 
+    matitaInit.cmi matitaGui.cmi matitaGtkMisc.cmi buildTimeConf.cmi 
 matita.cmx: matitaTypes.cmx matitaScript.cmx matitaMathView.cmx \
-    matitaInit.cmx matitaGui.cmx matitaGtkMisc.cmx lablGraphviz.cmx \
+    matitaInit.cmx matitaGui.cmx matitaGtkMisc.cmx buildTimeConf.cmx 
+matitaprover.cmo: matitaInit.cmi matitaExcPp.cmi matitaEngine.cmi \
+    buildTimeConf.cmi 
+matitaprover.cmx: matitaInit.cmx matitaExcPp.cmx matitaEngine.cmx \
     buildTimeConf.cmx 
 matitaScript.cmo: matitamakeLib.cmi matitaTypes.cmi matitaMisc.cmi \
     matitaGtkMisc.cmi matitaEngine.cmi buildTimeConf.cmi \
index 34bbe632896c9a955df90d32fc5f3dbacee732f5..46ad75c29d602211385858475d789c5101f1e62d 100644 (file)
@@ -16,7 +16,7 @@ OCAMLOPT = $(OCAMLFIND) opt $(OCAMLC_FLAGS)
 OCAMLDEP = $(OCAMLFIND) ocamldep $(OCAML_FLAGS)
 INSTALL_PROGRAMS= matita matitac
 INSTALL_PROGRAMS_LINKS_MATITA= cicbrowser 
-INSTALL_PROGRAMS_LINKS_MATITAC= matitadep matitamake matitaclean
+INSTALL_PROGRAMS_LINKS_MATITAC= matitadep matitamake matitaclean matitaprover
 
 MATITA_FLAGS = -noprofile
 NODB=false
@@ -52,6 +52,7 @@ CCMOS =                               \
        matitaExcPp.cmo         \
        matitaEngine.cmo        \
        matitacLib.cmo          \
+       matitaprover.cmo        \
        $(NULL)
 MAINCMOS =                     \
        matitadep.cmo           \
@@ -60,7 +61,7 @@ MAINCMOS =                    \
        gragrep.cmo             \
        $(NULL)
 PROGRAMS_BYTE = \
-       matita matitac cicbrowser matitadep matitaclean matitamake
+       matita matitac cicbrowser matitadep matitaclean matitamake matitaprover
 PROGRAMS = $(PROGRAMS_BYTE) matitatop
 PROGRAMS_OPT = $(patsubst %,%.opt,$(PROGRAMS_BYTE))
 NOINST_PROGRAMS = dump_moo gragrep
@@ -139,6 +140,11 @@ matitatop: matitatop.ml $(CLIB_DEPS) $(CCMOS)
        $(H)echo "  OCAMLC $<"
        $(H)$(OCAMLC) $(CPKGS) -linkpkg -o $@ toplevellib.cma $(CCMOS) $<
 
+matitaprover: matitac
+       $(H)test -f $@ || ln -s $< $@
+matitaprover.opt: matitac.opt
+       $(H)test -f $@ || ln -s $< $@
+
 matitadep: matitac
        $(H)test -f $@ || ln -s $< $@
 matitadep.opt: matitac.opt
@@ -325,6 +331,8 @@ matitac.opt.static: $(STATIC_LINK) $(CLIBX_DEPS) $(CCMXS) $(MAINCMXS) matitac.ml
        strip $@
 matitadep.opt.static: matitac.opt.static
        $(H)test -f $@ || ln -s $< $@
+matitaprover.opt.static: matitac.opt.static
+       $(H)test -f $@ || ln -s $< $@
 matitaclean.opt.static: matitac.opt.static
        $(H)test -f $@ || ln -s $< $@
 matitamake.opt.static: matitac.opt.static
index 5866b74d8bff14c73e1d80ea9ccb58ac334453e1..a2a5b93fa316e5a41066a0d1f1d4079481425e19 100644 (file)
@@ -134,6 +134,11 @@ Options:"
       "gragrep",
         sprintf "Grafite Grep v%s
 Usage: gragrep [ -r ] PATH
+Options:"
+          BuildTimeConf.version;
+      "matitaprover",
+        sprintf "Matita's prover v%s
+Usage: matitaprover [ -tptppath ] FILE.p
 Options:"
           BuildTimeConf.version;
       "matita",
index 05add3ce4e14903836925ca089256da640076f8e..ced922a231b2644d42ed5fa3dc8d818bf80b9bb4 100644 (file)
@@ -31,6 +31,7 @@ let main () =
   | "matitadep"   | "matitadep.opt"   -> Matitadep.main ()
   | "matitaclean" | "matitaclean.opt" -> Matitaclean.main ()
   | "matitamake"  | "matitamake.opt"  -> Matitamake.main ()
+  | "matitaprover"  | "matitaprover.opt"  -> Matitaprover.main ()
   | _ ->
 (*
       let _ = Paramodulation.Saturation.init () in  *)
diff --git a/helm/software/matita/tests/TPTP/elenco_unsatisfiable.txt b/helm/software/matita/tests/TPTP/elenco_unsatisfiable.txt
new file mode 100644 (file)
index 0000000..e70ebb5
--- /dev/null
@@ -0,0 +1,698 @@
+ALG005-1.p
+ALG006-1.p
+ALG007-1.p
+BOO001-1.p
+BOO002-1.p
+BOO002-2.p
+BOO003-2.p
+BOO003-4.p
+BOO004-2.p
+BOO004-4.p
+BOO005-2.p
+BOO005-4.p
+BOO006-2.p
+BOO006-4.p
+BOO007-2.p
+BOO007-4.p
+BOO008-2.p
+BOO008-4.p
+BOO009-2.p
+BOO009-4.p
+BOO010-2.p
+BOO010-4.p
+BOO011-2.p
+BOO011-4.p
+BOO012-2.p
+BOO012-4.p
+BOO013-2.p
+BOO013-4.p
+BOO014-2.p
+BOO014-4.p
+BOO015-2.p
+BOO015-4.p
+BOO016-2.p
+BOO017-2.p
+BOO018-4.p
+BOO021-1.p
+BOO022-1.p
+BOO023-1.p
+BOO024-1.p
+BOO025-1.p
+BOO026-1.p
+BOO028-1.p
+BOO029-1.p
+BOO031-1.p
+BOO034-1.p
+BOO067-1.p
+BOO068-1.p
+BOO069-1.p
+BOO070-1.p
+BOO071-1.p
+BOO072-1.p
+BOO073-1.p
+BOO074-1.p
+BOO075-1.p
+BOO076-1.p
+COL001-1.p
+COL001-2.p
+COL002-1.p
+COL002-4.p
+COL002-5.p
+COL003-1.p
+COL004-1.p
+COL004-3.p
+COL006-1.p
+COL006-5.p
+COL006-6.p
+COL006-7.p
+COL007-1.p
+COL008-1.p
+COL009-1.p
+COL010-1.p
+COL011-1.p
+COL012-1.p
+COL013-1.p
+COL014-1.p
+COL015-1.p
+COL016-1.p
+COL017-1.p
+COL018-1.p
+COL019-1.p
+COL020-1.p
+COL021-1.p
+COL022-1.p
+COL023-1.p
+COL024-1.p
+COL025-1.p
+COL026-1.p
+COL027-1.p
+COL029-1.p
+COL030-1.p
+COL031-1.p
+COL032-1.p
+COL033-1.p
+COL034-1.p
+COL035-1.p
+COL036-1.p
+COL037-1.p
+COL038-1.p
+COL039-1.p
+COL041-1.p
+COL042-1.p
+COL042-6.p
+COL042-7.p
+COL042-8.p
+COL042-9.p
+COL043-1.p
+COL043-3.p
+COL044-1.p
+COL044-6.p
+COL044-7.p
+COL044-8.p
+COL044-9.p
+COL045-1.p
+COL046-1.p
+COL048-1.p
+COL049-1.p
+COL050-1.p
+COL051-1.p
+COL052-1.p
+COL053-1.p
+COL056-1.p
+COL057-1.p
+COL058-1.p
+COL058-2.p
+COL058-3.p
+COL059-1.p
+COL060-1.p
+COL060-2.p
+COL060-3.p
+COL061-1.p
+COL061-2.p
+COL061-3.p
+COL062-1.p
+COL062-2.p
+COL062-3.p
+COL063-1.p
+COL063-2.p
+COL063-3.p
+COL063-4.p
+COL063-5.p
+COL063-6.p
+COL064-1.p
+COL064-2.p
+COL064-3.p
+COL064-4.p
+COL064-5.p
+COL064-6.p
+COL064-7.p
+COL064-8.p
+COL064-9.p
+COL065-1.p
+COL066-1.p
+COL066-2.p
+COL066-3.p
+COL070-1.p
+COL075-2.p
+COL083-1.p
+COL084-1.p
+COL085-1.p
+COL086-1.p
+GRP001-2.p
+GRP001-4.p
+GRP002-2.p
+GRP002-3.p
+GRP002-4.p
+GRP010-4.p
+GRP011-4.p
+GRP012-4.p
+GRP014-1.p
+GRP022-2.p
+GRP023-2.p
+GRP024-5.p
+GRP114-1.p
+GRP115-1.p
+GRP116-1.p
+GRP117-1.p
+GRP118-1.p
+GRP119-1.p
+GRP120-1.p
+GRP121-1.p
+GRP122-1.p
+GRP136-1.p
+GRP137-1.p
+GRP138-1.p
+GRP139-1.p
+GRP140-1.p
+GRP141-1.p
+GRP142-1.p
+GRP143-1.p
+GRP144-1.p
+GRP145-1.p
+GRP146-1.p
+GRP147-1.p
+GRP148-1.p
+GRP149-1.p
+GRP150-1.p
+GRP151-1.p
+GRP152-1.p
+GRP153-1.p
+GRP154-1.p
+GRP155-1.p
+GRP156-1.p
+GRP157-1.p
+GRP158-1.p
+GRP159-1.p
+GRP160-1.p
+GRP161-1.p
+GRP162-1.p
+GRP163-1.p
+GRP164-1.p
+GRP164-2.p
+GRP165-1.p
+GRP165-2.p
+GRP166-1.p
+GRP166-2.p
+GRP166-3.p
+GRP166-4.p
+GRP167-1.p
+GRP167-2.p
+GRP167-3.p
+GRP167-4.p
+GRP167-5.p
+GRP168-1.p
+GRP168-2.p
+GRP169-1.p
+GRP169-2.p
+GRP170-1.p
+GRP170-2.p
+GRP170-3.p
+GRP170-4.p
+GRP171-1.p
+GRP171-2.p
+GRP172-1.p
+GRP172-2.p
+GRP173-1.p
+GRP174-1.p
+GRP175-1.p
+GRP175-2.p
+GRP175-3.p
+GRP175-4.p
+GRP176-1.p
+GRP176-2.p
+GRP177-2.p
+GRP178-1.p
+GRP178-2.p
+GRP179-1.p
+GRP179-2.p
+GRP179-3.p
+GRP180-1.p
+GRP180-2.p
+GRP181-1.p
+GRP181-2.p
+GRP181-3.p
+GRP181-4.p
+GRP182-1.p
+GRP182-2.p
+GRP182-3.p
+GRP182-4.p
+GRP183-1.p
+GRP183-2.p
+GRP183-3.p
+GRP183-4.p
+GRP184-1.p
+GRP184-2.p
+GRP184-3.p
+GRP184-4.p
+GRP185-1.p
+GRP185-2.p
+GRP185-3.p
+GRP185-4.p
+GRP186-1.p
+GRP186-2.p
+GRP186-3.p
+GRP186-4.p
+GRP187-1.p
+GRP188-1.p
+GRP188-2.p
+GRP189-1.p
+GRP189-2.p
+GRP190-1.p
+GRP190-2.p
+GRP191-1.p
+GRP191-2.p
+GRP192-1.p
+GRP193-1.p
+GRP193-2.p
+GRP195-1.p
+GRP196-1.p
+GRP200-1.p
+GRP201-1.p
+GRP202-1.p
+GRP203-1.p
+GRP205-1.p
+GRP206-1.p
+GRP403-1.p
+GRP404-1.p
+GRP405-1.p
+GRP406-1.p
+GRP407-1.p
+GRP408-1.p
+GRP409-1.p
+GRP410-1.p
+GRP411-1.p
+GRP412-1.p
+GRP413-1.p
+GRP414-1.p
+GRP415-1.p
+GRP416-1.p
+GRP417-1.p
+GRP418-1.p
+GRP419-1.p
+GRP420-1.p
+GRP421-1.p
+GRP422-1.p
+GRP423-1.p
+GRP424-1.p
+GRP425-1.p
+GRP426-1.p
+GRP427-1.p
+GRP428-1.p
+GRP429-1.p
+GRP430-1.p
+GRP431-1.p
+GRP432-1.p
+GRP433-1.p
+GRP434-1.p
+GRP435-1.p
+GRP436-1.p
+GRP437-1.p
+GRP438-1.p
+GRP439-1.p
+GRP440-1.p
+GRP441-1.p
+GRP442-1.p
+GRP443-1.p
+GRP444-1.p
+GRP445-1.p
+GRP446-1.p
+GRP447-1.p
+GRP448-1.p
+GRP449-1.p
+GRP450-1.p
+GRP451-1.p
+GRP452-1.p
+GRP453-1.p
+GRP454-1.p
+GRP455-1.p
+GRP456-1.p
+GRP457-1.p
+GRP458-1.p
+GRP459-1.p
+GRP460-1.p
+GRP461-1.p
+GRP462-1.p
+GRP463-1.p
+GRP464-1.p
+GRP465-1.p
+GRP466-1.p
+GRP467-1.p
+GRP468-1.p
+GRP469-1.p
+GRP470-1.p
+GRP471-1.p
+GRP472-1.p
+GRP473-1.p
+GRP474-1.p
+GRP475-1.p
+GRP476-1.p
+GRP477-1.p
+GRP478-1.p
+GRP479-1.p
+GRP480-1.p
+GRP481-1.p
+GRP482-1.p
+GRP483-1.p
+GRP484-1.p
+GRP485-1.p
+GRP486-1.p
+GRP487-1.p
+GRP488-1.p
+GRP489-1.p
+GRP490-1.p
+GRP491-1.p
+GRP492-1.p
+GRP493-1.p
+GRP494-1.p
+GRP495-1.p
+GRP496-1.p
+GRP497-1.p
+GRP498-1.p
+GRP499-1.p
+GRP500-1.p
+GRP501-1.p
+GRP502-1.p
+GRP503-1.p
+GRP504-1.p
+GRP505-1.p
+GRP506-1.p
+GRP507-1.p
+GRP508-1.p
+GRP509-1.p
+GRP510-1.p
+GRP511-1.p
+GRP512-1.p
+GRP513-1.p
+GRP514-1.p
+GRP515-1.p
+GRP516-1.p
+GRP517-1.p
+GRP518-1.p
+GRP519-1.p
+GRP520-1.p
+GRP521-1.p
+GRP522-1.p
+GRP523-1.p
+GRP524-1.p
+GRP525-1.p
+GRP526-1.p
+GRP527-1.p
+GRP528-1.p
+GRP529-1.p
+GRP530-1.p
+GRP531-1.p
+GRP532-1.p
+GRP533-1.p
+GRP534-1.p
+GRP535-1.p
+GRP536-1.p
+GRP537-1.p
+GRP538-1.p
+GRP539-1.p
+GRP540-1.p
+GRP541-1.p
+GRP542-1.p
+GRP543-1.p
+GRP544-1.p
+GRP545-1.p
+GRP546-1.p
+GRP547-1.p
+GRP548-1.p
+GRP549-1.p
+GRP550-1.p
+GRP551-1.p
+GRP552-1.p
+GRP553-1.p
+GRP554-1.p
+GRP555-1.p
+GRP556-1.p
+GRP557-1.p
+GRP558-1.p
+GRP559-1.p
+GRP560-1.p
+GRP561-1.p
+GRP562-1.p
+GRP563-1.p
+GRP564-1.p
+GRP565-1.p
+GRP566-1.p
+GRP567-1.p
+GRP568-1.p
+GRP569-1.p
+GRP570-1.p
+GRP571-1.p
+GRP572-1.p
+GRP573-1.p
+GRP574-1.p
+GRP575-1.p
+GRP576-1.p
+GRP577-1.p
+GRP578-1.p
+GRP579-1.p
+GRP580-1.p
+GRP581-1.p
+GRP582-1.p
+GRP583-1.p
+GRP584-1.p
+GRP585-1.p
+GRP586-1.p
+GRP587-1.p
+GRP588-1.p
+GRP589-1.p
+GRP590-1.p
+GRP591-1.p
+GRP592-1.p
+GRP593-1.p
+GRP594-1.p
+GRP595-1.p
+GRP596-1.p
+GRP597-1.p
+GRP598-1.p
+GRP599-1.p
+GRP600-1.p
+GRP601-1.p
+GRP602-1.p
+GRP603-1.p
+GRP604-1.p
+GRP605-1.p
+GRP606-1.p
+GRP607-1.p
+GRP608-1.p
+GRP609-1.p
+GRP610-1.p
+GRP611-1.p
+GRP612-1.p
+GRP613-1.p
+GRP614-1.p
+GRP615-1.p
+GRP616-1.p
+LAT006-1.p
+LAT007-1.p
+LAT008-1.p
+LAT009-1.p
+LAT010-1.p
+LAT011-1.p
+LAT012-1.p
+LAT013-1.p
+LAT014-1.p
+LAT017-1.p
+LAT018-1.p
+LAT019-1.p
+LAT020-1.p
+LAT021-1.p
+LAT022-1.p
+LAT023-1.p
+LAT026-1.p
+LAT027-1.p
+LAT028-1.p
+LAT031-1.p
+LAT032-1.p
+LAT033-1.p
+LAT034-1.p
+LAT038-1.p
+LAT039-1.p
+LAT039-2.p
+LAT040-1.p
+LAT042-1.p
+LAT043-1.p
+LAT044-1.p
+LAT045-1.p
+LAT070-1.p
+LAT072-1.p
+LAT074-1.p
+LAT075-1.p
+LAT076-1.p
+LAT077-1.p
+LAT078-1.p
+LAT079-1.p
+LAT080-1.p
+LAT081-1.p
+LAT082-1.p
+LAT083-1.p
+LAT084-1.p
+LAT085-1.p
+LAT086-1.p
+LAT087-1.p
+LAT088-1.p
+LAT089-1.p
+LAT090-1.p
+LAT091-1.p
+LAT092-1.p
+LAT093-1.p
+LAT094-1.p
+LAT095-1.p
+LAT096-1.p
+LAT097-1.p
+LAT138-1.p
+LAT139-1.p
+LAT140-1.p
+LAT141-1.p
+LAT142-1.p
+LAT143-1.p
+LAT144-1.p
+LAT145-1.p
+LAT146-1.p
+LAT147-1.p
+LAT148-1.p
+LAT149-1.p
+LAT150-1.p
+LAT151-1.p
+LAT152-1.p
+LAT153-1.p
+LAT154-1.p
+LAT155-1.p
+LAT156-1.p
+LAT157-1.p
+LAT158-1.p
+LAT159-1.p
+LAT160-1.p
+LAT161-1.p
+LAT162-1.p
+LAT163-1.p
+LAT164-1.p
+LAT165-1.p
+LAT166-1.p
+LAT167-1.p
+LAT168-1.p
+LAT169-1.p
+LAT170-1.p
+LAT171-1.p
+LAT172-1.p
+LAT173-1.p
+LAT174-1.p
+LAT175-1.p
+LAT176-1.p
+LAT177-1.p
+LCL109-2.p
+LCL109-6.p
+LCL110-2.p
+LCL111-2.p
+LCL112-2.p
+LCL113-2.p
+LCL114-2.p
+LCL115-2.p
+LCL116-2.p
+LCL132-1.p
+LCL133-1.p
+LCL134-1.p
+LCL135-1.p
+LCL138-1.p
+LCL139-1.p
+LCL140-1.p
+LCL141-1.p
+LCL153-1.p
+LCL154-1.p
+LCL155-1.p
+LCL156-1.p
+LCL157-1.p
+LCL158-1.p
+LCL159-1.p
+LCL160-1.p
+LCL161-1.p
+LCL162-1.p
+LCL163-1.p
+LCL164-1.p
+LDA001-1.p
+LDA002-1.p
+LDA007-3.p
+RNG007-4.p
+RNG008-3.p
+RNG008-4.p
+RNG008-7.p
+RNG009-5.p
+RNG009-7.p
+RNG011-5.p
+RNG012-6.p
+RNG013-6.p
+RNG014-6.p
+RNG015-6.p
+RNG016-6.p
+RNG017-6.p
+RNG018-6.p
+RNG019-6.p
+RNG019-7.p
+RNG020-6.p
+RNG020-7.p
+RNG021-6.p
+RNG021-7.p
+RNG023-6.p
+RNG023-7.p
+RNG024-6.p
+RNG024-7.p
+RNG025-4.p
+RNG025-5.p
+RNG025-6.p
+RNG025-7.p
+RNG026-6.p
+RNG026-7.p
+RNG027-5.p
+RNG027-7.p
+RNG027-8.p
+RNG027-9.p
+RNG028-5.p
+RNG028-7.p
+RNG028-8.p
+RNG028-9.p
+RNG029-5.p
+RNG029-6.p
+RNG029-7.p
+RNG035-7.p
+ROB001-1.p
+ROB002-1.p
+ROB003-1.p
+ROB004-1.p
+ROB005-1.p
+ROB006-1.p
+ROB006-2.p
+ROB008-1.p
+ROB009-1.p
+ROB010-1.p
+ROB013-1.p
+ROB022-1.p
+ROB023-1.p
+ROB026-1.p
+ROB030-1.p
+ROB031-1.p
+ROB032-1.p
+SYN080-1.p
+SYN083-1.p
index fdf8031b3a36ec7bb31fa1acce2bf2a02ee80607..bd5b982fb432e59dd904021c7aedfad63472e7d7 100755 (executable)
@@ -1,10 +1,18 @@
 #!/bin/sh
 
+prover=y
+
 MATITAC=../../matitac.opt
 #MATITAC=../../matitac
+MATITAPROVER=../../matitaprover.opt
+TPTPPATH=/home/tassi/helm/trunk/TPTP-v3.1.1/
 
 if [ -z "$1" ]; then
-  TODO=Unsatisfiable/[A-Z]*.ma
+  if [ $prover = 'y' ]; then
+    TODO=`cat elenco_unsatisfiable.txt`          
+  else
+    TODO=Unsatisfiable/[A-Z]*.ma
+  fi
 else
   TODO=`cat $1`
 fi
@@ -15,8 +23,17 @@ i=1
 for X in $TODO; do
   echo -n "$X ... "
   LOGNAME=logs/log.`basename $X`
-  $MATITAC -nodb $X > $LOGNAME 2>&1
-  RATING=`grep "Rating" $X | sed 's/v.*//' | sed 's/(\*//'`
+  if [ $prover = 'y' ]; then
+    $MATITAPROVER -tptppath $TPTPPATH $X > $LOGNAME 2>&1
+  else
+    $MATITAC -nodb $X > $LOGNAME 2>&1
+  fi
+  if [ $prover = 'y' ]; then
+    BASE=`echo $X | cut -c 1-3`          
+    RATING=`grep "Rating" $TPTPPATH/Problems/$BASE/$X | sed 's/v.*//' | sed 's/%//'`     
+  else
+    RATING=`grep "Rating" $X | sed 's/v.*//' | sed 's/(\*//'`
+  fi
   if [ `grep "Found a proof" $LOGNAME | wc -l` -gt 0 ]; then
     TIME=`grep "TIME NEEDED" $LOGNAME`
     MAXWEIGHT=`grep "max weight:" $LOGNAME`