From: Enrico Tassi Date: Sat, 22 Jul 2006 17:14:13 +0000 (+0000) Subject: matitaprover X-Git-Tag: 0.4.95@7852~1164 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=894b08ca7d14aa7e31c35f3acb3903a1c3472a27;p=helm.git matitaprover --- diff --git a/components/METAS/meta.helm-tptp_grafite.src b/components/METAS/meta.helm-tptp_grafite.src new file mode 100644 index 000000000..4c1675626 --- /dev/null +++ b/components/METAS/meta.helm-tptp_grafite.src @@ -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="" diff --git a/components/Makefile b/components/Makefile index 948ba8f36..cfe1fd517 100644 --- a/components/Makefile +++ b/components/Makefile @@ -32,6 +32,7 @@ MODULES = \ lexicon \ grafite_engine \ grafite_parser \ + tptp_grafite \ $(NULL) METAS = $(MODULES:%=METAS/META.helm-%) diff --git a/components/acic_content/.depend b/components/acic_content/.depend index f6399321e..a0f6ba9ca 100644 --- a/components/acic_content/.depend +++ b/components/acic_content/.depend @@ -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 diff --git a/components/binaries/Makefile b/components/binaries/Makefile index 0f79acfe4..a2b89ee97 100644 --- a/components/binaries/Makefile +++ b/components/binaries/Makefile @@ -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/components/binaries/tptp2grafite/Makefile b/components/binaries/tptp2grafite/Makefile deleted file mode 100644 index 071bf8ddb..000000000 --- a/components/binaries/tptp2grafite/Makefile +++ /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/components/binaries/tptp2grafite/ast.ml b/components/binaries/tptp2grafite/ast.ml deleted file mode 100644 index b8f855dd1..000000000 --- a/components/binaries/tptp2grafite/ast.ml +++ /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/components/binaries/tptp2grafite/lexer.mll b/components/binaries/tptp2grafite/lexer.mll deleted file mode 100644 index 273d1b79b..000000000 --- a/components/binaries/tptp2grafite/lexer.mll +++ /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/components/binaries/tptp2grafite/main.ml b/components/binaries/tptp2grafite/main.ml deleted file mode 100644 index 980f2b456..000000000 --- a/components/binaries/tptp2grafite/main.ml +++ /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/components/binaries/tptp2grafite/parser.mly b/components/binaries/tptp2grafite/parser.mly deleted file mode 100644 index 05577000c..000000000 --- a/components/binaries/tptp2grafite/parser.mly +++ /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 TYPE - %token COMMENT - %token NUM - %token LNAME - %token UNAME - %token 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 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/components/binaries/tptp2grafite/unit_equality_problems b/components/binaries/tptp2grafite/unit_equality_problems deleted file mode 100644 index c394ddd95..000000000 --- a/components/binaries/tptp2grafite/unit_equality_problems +++ /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 diff --git a/components/cic/libraryObjects.ml b/components/cic/libraryObjects.ml index 7a4112ad5..dc36636fe 100644 --- a/components/cic/libraryObjects.ml +++ b/components/cic/libraryObjects.ml @@ -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 () = diff --git a/components/cic/libraryObjects.mli b/components/cic/libraryObjects.mli index 9dfe54902..0cd9f2e97 100644 --- a/components/cic/libraryObjects.mli +++ b/components/cic/libraryObjects.mli @@ -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 diff --git a/components/cic_proof_checking/cicPp.ml b/components/cic_proof_checking/cicPp.ml index e44c6b588..feca7c3cf 100644 --- a/components/cic_proof_checking/cicPp.ml +++ b/components/cic_proof_checking/cicPp.ml @@ -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 diff --git a/components/content_pres/.depend b/components/content_pres/.depend index d16c75a76..2de502ee5 100644 --- a/components/content_pres/.depend +++ b/components/content_pres/.depend @@ -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 \ diff --git a/components/grafite/grafiteAst.ml b/components/grafite/grafiteAst.ml index d38943da1..246df11c2 100644 --- a/components/grafite/grafiteAst.ml +++ b/components/grafite/grafiteAst.ml @@ -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 diff --git a/components/grafite/grafiteAstPp.ml b/components/grafite/grafiteAstPp.ml index d35a8af11..4a94152de 100644 --- a/components/grafite/grafiteAstPp.ml +++ b/components/grafite/grafiteAstPp.ml @@ -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 diff --git a/components/grafite_engine/grafiteEngine.ml b/components/grafite_engine/grafiteEngine.ml index ab43c6cc1..d99ab8593 100644 --- a/components/grafite_engine/grafiteEngine.ml +++ b/components/grafite_engine/grafiteEngine.ml @@ -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,[] diff --git a/components/grafite_engine/grafiteTypes.ml b/components/grafite_engine/grafiteTypes.ml index 0c02e1b6c..0d59e4b46 100644 --- a/components/grafite_engine/grafiteTypes.ml +++ b/components/grafite_engine/grafiteTypes.ml @@ -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 = diff --git a/components/grafite_parser/grafiteDisambiguate.ml b/components/grafite_parser/grafiteDisambiguate.ml index 76e5e6d86..04521361d 100644 --- a/components/grafite_parser/grafiteDisambiguate.ml +++ b/components/grafite_parser/grafiteDisambiguate.ml @@ -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 -> diff --git a/components/grafite_parser/grafiteParser.ml b/components/grafite_parser/grafiteParser.ml index fadecd61e..13ee7297e 100644 --- a/components/grafite_parser/grafiteParser.ml +++ b/components/grafite_parser/grafiteParser.ml @@ -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> ; newname = IDENT -> diff --git a/components/library/librarySync.ml b/components/library/librarySync.ml index a59294aaa..338e84bbe 100644 --- a/components/library/librarySync.ml +++ b/components/library/librarySync.ml @@ -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) diff --git a/components/syntax_extensions/profiling_macros.ml b/components/syntax_extensions/profiling_macros.ml index 479e67381..9f5034a58 100644 --- a/components/syntax_extensions/profiling_macros.ml +++ b/components/syntax_extensions/profiling_macros.ml @@ -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);; +*) + diff --git a/components/tactics/autoTactic.ml b/components/tactics/autoTactic.ml index d4dc5592c..f063eeafb 100644 --- a/components/tactics/autoTactic.ml +++ b/components/tactics/autoTactic.ml @@ -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;; diff --git a/components/tactics/autoTactic.mli b/components/tactics/autoTactic.mli index 1dfe0e2a9..354b1b738 100644 --- a/components/tactics/autoTactic.mli +++ b/components/tactics/autoTactic.mli @@ -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 diff --git a/components/tactics/paramodulation/equality.ml b/components/tactics/paramodulation/equality.ml index 368a80f5d..0b0b73e3f 100644 --- a/components/tactics/paramodulation/equality.ml +++ b/components/tactics/paramodulation/equality.ml @@ -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> in +(* let _ = <:start> 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> in () +(* let _ = <:stop> in () *) ;; let id_of e = let _,_,_,_,id = open_equality e in id ;; -let get_stats () = +let get_stats () = "" +(* <:show> ^ "# 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 [] +;; + diff --git a/components/tactics/paramodulation/equality.mli b/components/tactics/paramodulation/equality.mli index 019578ccc..1a909dfc4 100644 --- a/components/tactics/paramodulation/equality.mli +++ b/components/tactics/paramodulation/equality.mli @@ -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 diff --git a/components/tactics/paramodulation/indexing.ml b/components/tactics/paramodulation/indexing.ml index a4bdef1a2..f3af1b482 100644 --- a/components/tactics/paramodulation/indexing.ml +++ b/components/tactics/paramodulation/indexing.ml @@ -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> in - <:stop> | Unification -> - let _ = <:start> in - <:stop> in Index.PosEqSet.elements s @@ -1039,4 +1033,4 @@ let rec demodulation_goal env table goal = | None -> do_right () ;; -let get_stats () = <:show> ;; +let get_stats () = "" ;; diff --git a/components/tactics/paramodulation/inference.ml b/components/tactics/paramodulation/inference.ml index 408a7cdb8..f04024122 100644 --- a/components/tactics/paramodulation/inference.ml +++ b/components/tactics/paramodulation/inference.ml @@ -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> in +(* let _ = <:start> in *) let t = CicUtil.term_of_uri u in let ty, _ = CicTypeChecker.type_of_aux' [] [] t CicUniv.empty_ugraph in - let _ = <:stop> in +(* let _ = <:stop> 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> in +(* let _ = <:start> 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> in +(* let _ = <:stop> 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> ;; +let get_stats () = "" (*<:show>*) ;; diff --git a/components/tactics/paramodulation/saturation.ml b/components/tactics/paramodulation/saturation.ml index c40b4a9ac..021afb5ab 100644 --- a/components/tactics/paramodulation/saturation.ml +++ b/components/tactics/paramodulation/saturation.ml @@ -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> in +(* let _ = <:start> in *) let maxm, res = Indexing.superposition_right eq_uri !maxmeta env active_table current in - let _ = <:stop> in +(* let _ = <:stop> 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> in +(* let _ = <:start> in *) let pos = infer_positive curr_table ((*copy_of_current::*)active_list) in - let _ = <:stop> in +(* let _ = <:stop> 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> in - let goals = simplify_goal_set env goals passive active in - let _ = <:stop> 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> in +(* let _ = <:start> in *) let rc = simplify_goal_set env goals (a,b) in - let _ = <:stop> in +(* let _ = <:stop> 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> ^ Indexing.get_stats () ^ Inference.get_stats () ^ Equality.get_stats () ;; +*) diff --git a/components/tptp_grafite/.depend b/components/tptp_grafite/.depend new file mode 100644 index 000000000..bc310327f --- /dev/null +++ b/components/tptp_grafite/.depend @@ -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/components/tptp_grafite/Makefile b/components/tptp_grafite/Makefile new file mode 100644 index 000000000..c5c6e6346 --- /dev/null +++ b/components/tptp_grafite/Makefile @@ -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/components/tptp_grafite/ast.ml b/components/tptp_grafite/ast.ml new file mode 100644 index 000000000..b8f855dd1 --- /dev/null +++ b/components/tptp_grafite/ast.ml @@ -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/components/tptp_grafite/lexer.mll b/components/tptp_grafite/lexer.mll new file mode 100644 index 000000000..273d1b79b --- /dev/null +++ b/components/tptp_grafite/lexer.mll @@ -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/components/tptp_grafite/main.ml b/components/tptp_grafite/main.ml new file mode 100644 index 000000000..e52b77c43 --- /dev/null +++ b/components/tptp_grafite/main.ml @@ -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/components/tptp_grafite/parser.mly b/components/tptp_grafite/parser.mly new file mode 100644 index 000000000..05577000c --- /dev/null +++ b/components/tptp_grafite/parser.mly @@ -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 TYPE + %token COMMENT + %token NUM + %token LNAME + %token UNAME + %token 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 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/components/tptp_grafite/tptp2grafite.ml b/components/tptp_grafite/tptp2grafite.ml new file mode 100644 index 000000000..841ac5f5c --- /dev/null +++ b/components/tptp_grafite/tptp2grafite.ml @@ -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/components/tptp_grafite/tptp2grafite.mli b/components/tptp_grafite/tptp2grafite.mli new file mode 100644 index 000000000..7dfa2d3d0 --- /dev/null +++ b/components/tptp_grafite/tptp2grafite.mli @@ -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/components/tptp_grafite/unit_equality_problems b/components/tptp_grafite/unit_equality_problems new file mode 100644 index 000000000..c394ddd95 --- /dev/null +++ b/components/tptp_grafite/unit_equality_problems @@ -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 diff --git a/configure.ac b/configure.ac index d3f381e67..a1f233b6b 100644 --- a/configure.ac +++ b/configure.ac @@ -76,6 +76,7 @@ FINDLIB_COMREQUIRES="\ helm-cic_disambiguation \ helm-grafite \ helm-grafite_engine \ +helm-tptp_grafite \ helm-grafite_parser \ helm-hgdome \ helm-tactics \ diff --git a/matita/.depend b/matita/.depend index b893373e1..f67366bd7 100644 --- a/matita/.depend +++ b/matita/.depend @@ -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 \ diff --git a/matita/Makefile b/matita/Makefile index 34bbe6328..46ad75c29 100644 --- a/matita/Makefile +++ b/matita/Makefile @@ -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 diff --git a/matita/matitaInit.ml b/matita/matitaInit.ml index 5866b74d8..a2a5b93fa 100644 --- a/matita/matitaInit.ml +++ b/matita/matitaInit.ml @@ -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", diff --git a/matita/matitac.ml b/matita/matitac.ml index 05add3ce4..ced922a23 100644 --- a/matita/matitac.ml +++ b/matita/matitac.ml @@ -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/matita/tests/TPTP/elenco_unsatisfiable.txt b/matita/tests/TPTP/elenco_unsatisfiable.txt new file mode 100644 index 000000000..e70ebb599 --- /dev/null +++ b/matita/tests/TPTP/elenco_unsatisfiable.txt @@ -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 diff --git a/matita/tests/TPTP/try.sh b/matita/tests/TPTP/try.sh index fdf8031b3..bd5b982fb 100755 --- a/matita/tests/TPTP/try.sh +++ b/matita/tests/TPTP/try.sh @@ -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`