--- /dev/null
+requires="helm-acic_content helm-grafite helm-lexicon"
+version="0.0.1"
+archive(byte)="tptp_grafite.cma"
+archive(native)="tptp_grafite.cmxa"
+linkopts=""
lexicon \
grafite_engine \
grafite_parser \
+ tptp_grafite \
$(NULL)
METAS = $(MODULES:%=METAS/META.helm-%)
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
H=@
-BINARIES=extractor table_creator utilities saturate tptp2grafite
+BINARIES=extractor table_creator utilities saturate
all: $(BINARIES:%=rec@all@%)
opt: $(BINARIES:%=rec@opt@%)
+++ /dev/null
-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
+++ /dev/null
-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
+++ /dev/null
-{
- 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 *) }
+++ /dev/null
-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
+++ /dev/null
-%{
- (* 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 *)
+++ /dev/null
-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
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;
(**** 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
;;
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 () =
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;;
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
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
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
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 \
| 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
| 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
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,[]
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 =
| GrafiteAst.Coercion _
| GrafiteAst.Default _
| GrafiteAst.Drop _
+ | GrafiteAst.Print _
| GrafiteAst.Include _
| GrafiteAst.Qed _
| GrafiteAst.Set _ as cmd ->
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 ->
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
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) ::
(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)
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);;
+*)
+
| CicUnification.UnificationFailure msg
| CicTypeChecker.TypeCheckerFailure msg ->
raise (ProofEngineTypes.Fail msg))
+
+let pp_proofterm = Equality.pp_proofterm;;
ProofEngineTypes.tactic
val applyS_tac: dbd:HMysql.dbd -> term: Cic.term -> ProofEngineTypes.tactic
+
+val pp_proofterm: Cic.term -> string
* http://cs.unibo.it/helm/.
*)
-let _profiler = <:profiler<_profiler>>;;
+(* let _profiler = <:profiler<_profiler>>;; *)
(* $Id: inference.ml 6245 2006-04-05 12:07:51Z tassi $ *)
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
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,_,_) =
(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]))
| 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 =
(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))
| 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
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
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 []
+;;
+
(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 :
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
* http://cs.unibo.it/helm/.
*)
-let _profiler = <:profiler<_profiler>>;;
+(* let _profiler = <:profiler<_profiler>>;; *)
(* $Id$ *)
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
| None -> do_right ()
;;
-let get_stats () = <:show<Indexing.>> ;;
+let get_stats () = "" ;;
* http://cs.unibo.it/helm/.
*)
-let _profiler = <:profiler<_profiler>>;;
+(* let _profiler = <:profiler<_profiler>>;; *)
(* $Id$ *)
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
;;
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
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 ->
res
;;
-let get_stats () = <:show<Inference.>> ;;
+let get_stats () = "" (*<:show<Inference.>>*) ;;
* http://cs.unibo.it/helm/.
*)
-let _profiler = <:profiler<_profiler>>;;
+(* let _profiler = <:profiler<_profiler>>;; *)
(* $Id$ *)
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)
(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
;;
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 ->
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 ->
(* 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 =
| [] -> 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)
(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
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 =
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 ->
(* 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
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 ->
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
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
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)
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);*)
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
(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
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
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
;;
proof,[goalno]
;;
-let get_stats () =
+let get_stats () = ""
+(*
<:show<Saturation.>> ^ Indexing.get_stats () ^ Inference.get_stats () ^
Equality.get_stats ()
;;
+*)
--- /dev/null
+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
--- /dev/null
+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
+
--- /dev/null
+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
--- /dev/null
+{
+ 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 *) }
--- /dev/null
+(* 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
+
--- /dev/null
+%{
+ (* 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 *)
--- /dev/null
+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)
+;;
--- /dev/null
+(* 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
--- /dev/null
+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
helm-cic_disambiguation \
helm-grafite \
helm-grafite_engine \
+helm-tptp_grafite \
helm-grafite_parser \
helm-hgdome \
helm-tactics \
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
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 \
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
matitaExcPp.cmo \
matitaEngine.cmo \
matitacLib.cmo \
+ matitaprover.cmo \
$(NULL)
MAINCMOS = \
matitadep.cmo \
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
$(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
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
"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",
| "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 *)
--- /dev/null
+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
#!/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
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`
projects / helm.git / commitdiff