hgdome \
registry \
hmysql \
- syntax_extensions \
+ syntax_extensions \
thread \
xmldiff \
urimanager \
ng_library \
content_pres \
lexicon \
- tptp_grafite \
grafite_parser \
ng_tactics \
grafite_engine \
+++ /dev/null
-parser.cmi: ast.cmo
-parserTHF.cmi: astTHF.cmo
-tptp2grafite.cmi:
-ast.cmo:
-ast.cmx:
-lexer.cmo: parser.cmi
-lexer.cmx: parser.cmx
-astTHF.cmo:
-astTHF.cmx:
-lexerTHF.cmo: parserTHF.cmi
-lexerTHF.cmx: parserTHF.cmx
-parser.cmo: ast.cmo parser.cmi
-parser.cmx: ast.cmx parser.cmi
-parserTHF.cmo: astTHF.cmo parserTHF.cmi
-parserTHF.cmx: astTHF.cmx parserTHF.cmi
-tptp2grafite.cmo: parser.cmi lexer.cmo ast.cmo tptp2grafite.cmi
-tptp2grafite.cmx: parser.cmx lexer.cmx ast.cmx tptp2grafite.cmi
+++ /dev/null
-parser.cmi: ast.cmx
-tptp2grafite.cmi:
-ast.cmo:
-ast.cmx:
-lexer.cmo: parser.cmi
-lexer.cmx: parser.cmx
-parser.cmo: ast.cmx parser.cmi
-parser.cmx: ast.cmx parser.cmi
-tptp2grafite.cmo: parser.cmi lexer.cmx ast.cmx tptp2grafite.cmi
-tptp2grafite.cmx: parser.cmx lexer.cmx ast.cmx tptp2grafite.cmi
+++ /dev/null
-PACKAGE = tptp_grafite
-PREDICATES =
-
-INTERFACE_FILES= parser.mli parserTHF.mli tptp2grafite.mli
-
-IMPLEMENTATION_FILES = ast.ml lexer.ml astTHF.ml lexerTHF.ml $(INTERFACE_FILES:%.mli=%.ml)
-EXTRA_OBJECTS_TO_INSTALL =
-EXTRA_OBJECTS_TO_CLEAN =
-
-TPTPDIR= /home/$(USER)/work-area/TPTP-v4.0.1/
-
-all: tptp2grafite mainTHF
-clean: clean_tests clean_generated
-
-clean_generated:
- rm -f parser.mli parser.ml parserTHF.mli parserTHF.ml
- rm -f lexer.ml lexerTHF.ml
-
-clean_tests:
- rm -f tptp2grafite
-
-lexer.cmo: parser.cmi
-lexer.cmx: parser.cmi
-lexerTHF.cmo: parserTHF.cmi
-lexerTHF.cmx: parserTHF.cmi
-
-%.mli %.ml: %.mly
- ocamlyacc $*.mly
-%.ml:%.mll
- ocamllex $*.mll
-
-LOCAL_LINKOPTS = -package helm-$(PACKAGE) -linkpkg
-tptp2grafite: main.ml tptp_grafite.cma
- @echo " OCAMLC $<"
- @$(OCAMLC) $(LOCAL_LINKOPTS) -o $@ $<
-
-mainTHF: mainTHF.ml tptp_grafite.cma
- @echo " OCAMLC $<"
- @$(OCAMLC) $(LOCAL_LINKOPTS) -o $@ $<
-
-test: tptp2grafite mainTHF
-
-testall: tptp2grafite
- for X in `cat unit_equality_problems`; do\
- cat $(TPTPDIR)/$$X | ./tptp2grafite || echo ERROR PARSING $$X;\
- done
-
-generate-%:
- for X in `cat $*`; do\
- ./tptp2grafite -tptppath $(TPTPDIR) $$X.p \
- > ../../matita/tests/TPTP/$$X.ma || echo Failed: $$X; \
- done
-
-ngenerate-%:
- for X in `cat $*`; do\
- ./tptp2grafite -ng -tptppath $(TPTPDIR) $$X.p \
- > ../../matita/contribs/ng_TPTP/$$X.ma || echo Failed: $$X; \
- done
-
-parse-%:
- for X in `cat $*`; do\
- echo "Parsing $$X"; \
- ./tptp2grafite -tptppath $(TPTPDIR) $$X.p \
- > /dev/null || echo Failed: $$X; \
- done
-
-thf:
- rm -rf THF
- mkdir THF
- for x in `cat thf_problems`; do\
- echo $$x;\
- ./mainTHF -tptppath $(TPTPDIR) $$x.p > THF/$$x.ma;\
- done
-
-include ../../Makefile.defs
-include ../Makefile.common
-
+++ /dev/null
-type kinds_of_formulae =
- | Axiom | Hypothesis | Definition | Lemma | Theorem | Conjecture
- | Lemma_conjecture | Negated_conjecture | Plain | Unknown
-
-type source = NoSource
-
-type info = NoInfo
-
-type term =
- | Variable of string
- | Constant of string
- | Function of string * term list
-
-type atom =
- | Proposition of string
- | Predicate of string * term list
- | True
- | False
- | Eq of term * term
- | NotEq of term * term
-
-type formulae =
- | Disjunction of formulae * formulae
- | NegAtom of atom
- | Atom of atom
-
-type ast =
- | Comment of string
- | Inclusion of string * (string list)
- | AnnotatedFormula of
- string * kinds_of_formulae * formulae * source * info list
+++ /dev/null
-type role =
- Axiom
-| Hypothesis
-| Definition
-| Assumption
-| Lemma
-| Theorem
-| Conjecture
-| Negated_conjecture
-| Lemma_conjecture
-| Plain
-| Fi_domain
-| Fi_functors
-| Fi_predicates
-| Type
-| Unknown
-
-
-type ast =
- | ThfFormula of string * role * CicNotationPt.term
- | ThfDefinition of string * string * CicNotationPt.term
- | ThfType of string * string * CicNotationPt.term
- | Comment of string
- | Inclusion of string * (string list)
+++ /dev/null
-ANA003-1
-ANA004-1
-ANA005-1
-CAT018-4
-COL003-10
-COL003-2
-COL003-3
-COL003-4
-COL003-5
-COL003-6
-COL003-7
-COL003-8
-COL003-9
-COL006-2
-COL006-3
-COL006-4
-COL042-2
-COL042-3
-COL042-4
-COL042-5
-COL043-2
-COL044-2
-COL044-3
-COL044-4
-COL044-5
-HWC002-1
-HWC003-1
-HWC003-2
-HWV002-1
-HWV003-1
-HWV004-1
-LAT001-1
-LAT002-1
-LAT041-1
-LCL109-4
-LCL149-1
-LCL150-1
-LCL152-1
-LCL181-3
-LCL191-3
-LCL192-3
-LCL193-3
-LCL194-3
-LCL195-3
-LCL208-3
-LCL213-3
-LCL214-3
-LCL215-3
-LCL216-3
-LCL217-3
-LCL220-3
-LCL221-3
-LCL222-3
-LCL223-3
-LCL224-3
-LCL225-3
-LCL227-3
-LCL229-3
-LCL230-3
-LCL231-3
-LCL242-3
-LCL243-3
-LCL245-3
-LCL246-3
-LCL247-3
-LCL249-3
-LCL251-3
-LCL252-3
-LCL253-3
-LCL254-3
-LCL255-3
-LCL260-3
-LCL262-3
-LCL263-3
-LCL264-3
-LCL265-3
-LCL266-3
-LCL269-3
-LCL270-3
-LCL271-3
-LCL272-3
-LCL273-3
-LCL274-3
-LCL275-3
-LCL276-3
-LCL277-3
-LCL278-3
-LCL281-3
-LCL282-3
-LCL283-3
-LCL284-3
-LCL285-3
-LCL286-3
-LCL289-3
-LCL293-3
-LCL295-3
-LCL298-3
-LCL299-3
-LCL300-3
-LCL302-3
-LCL303-3
-LCL304-3
-LCL305-3
-LCL306-3
-LCL307-3
-LCL308-3
-LCL309-3
-LCL310-3
-LCL311-3
-LCL312-3
-LCL313-3
-LCL314-3
-LCL315-3
-LCL316-3
-LCL319-3
-LCL324-3
-LCL325-3
-LCL327-3
-LCL328-3
-LCL329-3
-LCL330-3
-LCL331-3
-LCL332-3
-LCL334-3
-LCL335-3
-LCL336-3
-LCL337-3
-LCL339-3
-LCL340-3
-LCL341-3
-LCL344-3
-LCL345-3
-LCL346-3
-LCL347-3
-LCL348-3
-LCL349-3
-LCL351-3
-LCL353-3
-LDA004-1
-ROB014-1
-ROB015-2
-ROB018-1
+++ /dev/null
-ANA003-2
-LCL001-1
-LCL002-1
-LCL005-1
-LCL019-1
-LCL020-1
-LCL021-1
-LCL024-1
-LCL032-1
-LCL037-1
-LCL038-1
-LCL061-1
-LCL062-1
-LCL063-1
-LCL074-1
-LCL084-2
-LCL084-3
-LCL085-1
-LCL105-1
-LCL119-1
-LCL122-1
-LCL124-1
-LCL125-1
-LCL166-1
-LCL167-1
-LCL218-1
-LCL227-1
-LCL230-1
-LCL231-1
-LCL249-1
-LCL253-1
-LCL369-1
-LCL375-1
-LCL377-1
-LCL393-1
-LCL394-1
-LCL395-1
-LCL423-1
-LCL425-1
-NUM017-1
-PLA001-1
-PLA004-1
-PLA004-2
-PLA005-1
-PLA005-2
-PLA007-1
-PLA008-1
-PLA009-1
-PLA009-2
-PLA010-1
-PLA011-1
-PLA011-2
-PLA012-1
-PLA013-1
-PLA014-1
-PLA014-2
-PLA015-1
-PLA016-1
-PLA018-1
-PLA019-1
-PLA021-1
-PLA023-1
-PUZ039-1
-PUZ040-1
-PUZ042-1
-PUZ050-1
-RNG001-2
-RNG004-3
-SWV014-1
-SYN556-1
-SYN598-1
-SYN599-1
-SYN600-1
-SYN614-1
-SYN615-1
-SYN617-1
-SYN628-1
-SYN631-1
-SYN639-1
-SYN640-1
-SYN646-1
-SYN647-1
-SYN649-1
-SYN653-1
-SYN654-1
-SYN655-1
-SYN704-1
-SYN707-1
-SYN708-1
-SYN711-1
+++ /dev/null
-{
- open Parser
- exception BadToken of string
-
- let incr_linenum lexbuf =
- let pos = lexbuf.Lexing.lex_curr_p in
- lexbuf.Lexing.lex_curr_p <- { pos with
- Lexing.pos_lnum = pos.Lexing.pos_lnum + 1;
- Lexing.pos_bol = pos.Lexing.pos_cnum;
- }
- ;;
-
-}
-
-let dust = ' ' | '\t'
-let comment = '%' [^ '\n' ] * '\n'
-let lname =
- ['a'-'z'] ['a'-'z''A'-'Z''0'-'9''_']*
-let uname =
- ['A'-'Z'] ['a'-'z''A'-'Z''0'-'9''_']*
-let qstring = ''' [^ ''' ]+ '''
-let type_ =
- "axiom" | "hypothesis" | "definition" | "lemma" | "theorem" |
- "conjecture" | "lemma_conjecture" | "negated_conjecture" |
- "plain" | "unknown"
-
-let ieq = "="
-let peq = "equal"
-let nieq = "!="
-
-rule yylex = parse
- | dust { yylex lexbuf }
- | '\n' { incr_linenum lexbuf; yylex lexbuf }
- | comment { incr_linenum lexbuf; COMMENT (Lexing.lexeme lexbuf) }
- | "include" { INCLUSION }
- | type_ { TYPE (Lexing.lexeme lexbuf) }
- | "cnf" { CNF }
- | "$true" { TRUE }
- | "$false" { FALSE }
- | "equal" { PEQ }
-
- | lname { LNAME (Lexing.lexeme lexbuf) }
- | uname { UNAME (Lexing.lexeme lexbuf) }
- | ['0' - '9']+ { NUM (int_of_string (Lexing.lexeme lexbuf)) }
- | ',' { COMMA }
- | '.' { DOT }
- | '(' { LPAREN }
- | ')' { RPAREN }
- | '|' { IOR }
- | '~' { NOT }
- | '=' { IEQ }
- | "!=" { NIEQ }
- | qstring { QSTRING (Lexing.lexeme lexbuf) }
- | eof { EOF }
- | _ { raise (BadToken (Lexing.lexeme lexbuf)) }
-
-{ (* trailer *) }
+++ /dev/null
-{
- open ParserTHF
- 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" | "type"
-
-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) }
- | "thf" { THF }
- | "$true" { TRUE }
- | "$false" { FALSE }
- | "equal" { PEQ }
-
- | "$i" { TYPE_I }
- | "$o" { TYPE_O }
- | "$tType" { TYPE_U }
- | ">" { TO }
-
- | lname { LNAME (Lexing.lexeme lexbuf) }
- | uname { UNAME (Lexing.lexeme lexbuf) }
-
- | ['0' - '9']+ { NUM (int_of_string (Lexing.lexeme lexbuf)) }
- | ',' { COMMA }
- | '.' { DOT }
- | '(' { LPAREN }
- | ')' { RPAREN }
- | '|' { IOR }
- | '&' { IAND }
- | '~' { NOT }
- | '=' { IEQ }
- | "=>" { IMPLY }
- | "<=" { IMPLYLR }
- | "<=>" { COIMPLY }
- | "<~>" { XOR }
- | "!=" { NIEQ }
- | "!" { FORALL }
- | "?" { EXISTS }
- | "!" { FORALL }
- | "^" { LAMBDA }
- | "[" { BEGINVARLIST }
- | "]" { ENDVARLIST }
- | ":" { COLON }
- | "," { COMMA }
- | "@" { APPLY }
- | qstring { QSTRING (Lexing.lexeme lexbuf) }
- | eof { EOF }
- | _ { raise (BadToken (Lexing.lexeme lexbuf)) }
-
-{ (* trailer *) }
+++ /dev/null
-(* OPTIONS *)
-let tptppath = ref "./";;
-let ng = ref false;;
-let spec = [
- ("-ng",Arg.Set ng,"Matita ng syntax");
- ("-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 ~ng:!ng ());
- exit 0
-
+++ /dev/null
-module T = CicNotationPt
-module GA = GrafiteAst
-module A = AstTHF
-
-let floc = HExtlib.dummy_floc;;
-
-(* OPTIONS *)
-let tptppath = ref "./";;
-let ng = ref false;;
-let spec = [
- ("-ng",Arg.Set ng,"Matita ng syntax");
- ("-tptppath",
- Arg.String (fun x -> tptppath := x),
- "Where to find the Axioms/ and Problems/ directory")
-]
-
-let resolve ~tptppath s =
- if s.[0] = '/' then s else
- 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
-;;
-
-
-let find_related id =
- HExtlib.filter_map_monad
- (fun acc -> function
- | A.ThfDefinition (_,did,dbody) when did = id -> Some dbody, None
- | A.ThfType (_,did,dtype) when did = id -> Some dtype, None
- | x -> acc, Some x)
-;;
-
-(* MAIN *)
-let _ =
- let usage = "Usage: tptpTHF2grafite [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 tptppath = !tptppath in
- let statements =
- 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 = ParserTHF.main LexerTHF.yylex lexbuf in
- hd :: aux (statements @ tl)
- | hd::tl -> hd :: aux tl
- in
- aux [A.Inclusion (!inputfile,[])]
- in
- let statements =
- let rec aux = function
- | [] -> []
- | A.Comment s :: tl ->
- let s = Pcre.replace ~pat:"\n" ~templ:"" s in
- let s = Pcre.replace ~pat:"\\*\\)" ~templ:"" s in
- GA.Comment (floc,GA.Note (floc,s)) :: aux tl
- | A.Inclusion (s,_) :: tl ->
- GA.Comment (
- floc, GA.Note (
- floc,"Inclusion of: " ^ s)) :: aux tl
- | A.ThfType(name,id,ty) :: tl ->
- let body, tl = find_related id None tl in
- let what = match body with None -> `Axiom | _ -> `Definition in
- GA.Executable(floc,
- GA.NCommand(floc,
- GA.NObj(floc,
- T.Theorem(what, id,ty,body,`Regular)))) :: aux tl
- | A.ThfDefinition(name,id,body) :: tl ->
- let ty, tl = find_related id None tl in
- let ty = match ty with Some x -> x | None -> T.Implicit `JustOne in
- GA.Executable(floc,
- GA.NCommand(floc,
- GA.NObj(floc,
- T.Theorem(`Definition,
- id,ty,Some body,`Regular)))):: aux tl
- | A.ThfFormula(name,(A.Axiom|A.Hypothesis|A.Assumption),term) :: tl ->
- GA.Executable(floc,
- GA.NCommand(floc,
- GA.NObj(floc,
- T.Theorem(`Axiom, name,term,None,`Regular)))):: aux tl
- | A.ThfFormula(name,A.Conjecture,term) :: tl ->
- GA.Executable(floc,
- GA.NCommand(floc,
- GA.NObj(floc,
- T.Theorem(`Theorem, name,
- term,None,`Regular)))):: aux tl
- | A.ThfFormula _ :: tl -> assert false
- in
- aux 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 prec content_term =
- let pres_term = TermContentPres.pp_ast content_term in
- let lookup_uri = fun _ -> None in
- let markup = CicNotationPres.render ~lookup_uri ~prec pres_term in
- let s = BoxPp.render_to_string List.hd width markup ~map_unicode_to_tex:false in
- Pcre.substitute
- ~rex:(Pcre.regexp ~flags:[`UTF8] "∀[Ha-z][a-z0-9_]*") ~subst:(fun x -> "\n" ^ x)
- s
- in
- CicNotationPp.set_pp_term (term_pp 90);
- let lazy_term_pp = fun x -> assert false in
- let obj_pp = CicNotationPp.pp_obj CicNotationPp.pp_term in
- Pcre.replace ~pat:"^theorem" ~templ:"ntheorem"
- (Pcre.replace ~pat:"^axiom" ~templ:"naxiom"
- (Pcre.replace ~pat:"^definition" ~templ:"ndefinition"
- (Pcre.replace ~pat:"Type \\\\sub ([0-9]+)" ~templ:"Type[$1]"
- (GrafiteAstPp.pp_statement
- ~map_unicode_to_tex:false
- ~term_pp:(term_pp 19) ~lazy_term_pp ~obj_pp t))))
- in
- print_endline (pp (GA.Executable (floc,
- GA.Command(floc,GA.Include(floc,true,`OldAndNew,"TPTP.ma")))));
- List.iter (fun x -> print_endline (pp x)) statements;
- exit 0
-
+++ /dev/null
-%{
- (* header *)
- open Ast
- open Parsing
- open Lexing
-
- let parse_error s = Printf.eprintf "%s: " s ;;
- let rm_q s = String.sub s 1 (String.length s - 2) ;;
-
-%}
- %token <string> TYPE
- %token <string> COMMENT
- %token <int> NUM
- %token <string> LNAME
- %token <string> UNAME
- %token <string> QSTRING
- %token COMMA
- %token INCLUSION
- %token LPAREN
- %token RPAREN
- %token CNF
- %token TRUE
- %token FALSE
- %token IOR
- %token NOT
- %token NIEQ
- %token IEQ
- %token PEQ
- %token DOT
- %token EOF
-
- %type <Ast.ast list> main
- %start main
-%%
- main:
- | tptp_input EOF {[$1]}
- | tptp_input main {$1::$2}
- | error {
- let start_pos = rhs_start_pos 1 in
- let end_pos = rhs_end_pos 1 in
- Printf.eprintf "from line %d char %d to line %d char %d\n"
- start_pos.pos_lnum (start_pos.pos_cnum - start_pos.pos_bol)
- end_pos.pos_lnum (end_pos.pos_cnum - end_pos.pos_bol);
- exit 1
- }
- ;
-
- tptp_input:
- | annot_formula {$1}
- | include_ {$1}
- | comment {$1}
- ;
-
- annot_formula:
- | CNF LPAREN
- name COMMA formula_type COMMA formula formula_source_and_infos
- RPAREN DOT {
- AnnotatedFormula ($3,$5,$7,fst $8,snd $8)
- }
- ;
-
- formula_type:
- | TYPE {
- match $1 with
- | "axiom" -> Axiom
- | "hypothesis" -> Hypothesis
- | "definition" -> Definition
- | "lemma" -> Lemma
- | "theorem" -> Theorem
- | "conjecture" -> Conjecture
- | "lemma_conjecture" -> Lemma_conjecture
- | "negated_conjecture" -> Negated_conjecture
- | "plain" -> Plain
- | "unknown" -> Unknown
- | _ -> assert false
- }
- ;
-
- formula:
- | LPAREN disjunction RPAREN {$2}
- | disjunction {$1}
- ;
-
- disjunction:
- | literal {$1}
- | literal IOR disjunction {
- Disjunction ($1,$3)
- }
- ;
-
- literal:
- | NOT atom { NegAtom $2 }
- | atom { Atom $1 }
- ;
-
- atom:
- | atomic_word LPAREN term_list RPAREN { Predicate ($1,$3) }
- | atomic_word { Proposition $1 }
- | TRUE { True }
- | FALSE { False }
- | term IEQ term { Eq ($1,$3) }
- | term NIEQ term { NotEq ($1,$3) }
- | PEQ LPAREN term COMMA term RPAREN { Eq ($3,$5) }
- ;
-
- term_list:
- | term { [$1] }
- | term COMMA term_list { $1 :: $3 }
- ;
-
- term:
- | upper_word { Variable $1 }
- | atomic_word LPAREN term_list RPAREN { Function ($1,$3) }
- | atomic_word { Constant $1 }
- ;
-
- upper_word: UNAME { $1 } ;
-
- atomic_word:
- | LNAME { $1 }
- | QSTRING { rm_q $1 }
- | TYPE { (* workaround! *)
- match $1 with
- | "theorem" -> "theoremP"
- | "axiom" -> "axiomP"
- | s -> prerr_endline s;assert false }
- ;
-
- formula_source_and_infos:
- | { NoSource, [NoInfo] }
- | COMMA { assert false }
- ;
-
- include_:
- | INCLUSION LPAREN QSTRING selection_of_formulae RPAREN DOT {
- let fname = rm_q $3 in
- Inclusion (fname,$4)
- }
- ;
-
- selection_of_formulae:
- | { [] }
- | COMMA name selection_of_formulae { $2::$3 }
- ;
-
- comment: COMMENT {Comment $1} ;
-
- name: NUM { string_of_int $1} | LNAME { $1 } | UNAME { $1 } ;
-%%
- (* trailer *)
+++ /dev/null
-%{
- (* header *)
- open AstTHF
- open Parsing
- open Lexing
- module T = CicNotationPt
-
- let parse_error s = Printf.eprintf "%s: " s ;;
- let rm_q s = String.sub s 1 (String.length s - 2) ;;
-
-let reserved = [
- "in","In";
- "to","To";
- "theorem","Theorem";
-];;
-
-let unreserve k =
- try List.assoc k reserved with Not_found -> k
-;;
-
-
-%}
- %token <string> TYPE
- %token <string> COMMENT
- %token <int> NUM
- %token <string> LNAME
- %token <string> UNAME
- %token <string> QSTRING
- %token COMMA
- %token INCLUSION
- %token LPAREN
- %token RPAREN
- %token CNF
- %token TRUE
- %token FALSE
- %token NOT
- %token IAND
- %token IOR
- %token NIEQ
- %token IEQ
- %token XOR
- %token IMPLY
- %token IMPLYLR
- %token COIMPLY
- %token PEQ
- %token DOT
- %token EOF
- %token FORALL
- %token EXISTS
- %token LAMBDA
- %token COLON
- %token BEGINVARLIST
- %token ENDVARLIST
- %token APPLY
- %token TYPE_I
- %token TYPE_O
- %token TYPE_U
- %token TO
- %token THF
-
- %left IOR
- %left IAND
- %nonassoc NOT
- %right TO
- %left APPLY
-
- %type <AstTHF.ast list> main
- %start main
-%%
- main:
- | tptp_input EOF {[$1]}
- | tptp_input main {$1::$2}
- | error {
- let start_pos = rhs_start_pos 1 in
- let end_pos = rhs_end_pos 1 in
- Printf.eprintf "from line %d char %d to line %d char %d\n"
- start_pos.pos_lnum (start_pos.pos_cnum - start_pos.pos_bol)
- end_pos.pos_lnum (end_pos.pos_cnum - end_pos.pos_bol);
- exit 1
- }
- ;
-
- tptp_input:
- | annot_formula {$1}
- | include_ {$1}
- | comment {$1}
- ;
-
- formula_source_and_infos:
- | { () }
- | COMMA { assert false }
- ;
-
- annot_formula:
- | THF LPAREN name COMMA formula_type COMMA
- term formula_source_and_infos RPAREN DOT {
- match $5 with
- | Definition ->
- (match $7 with
- | T.Appl [T.Symbol("Eq",_);T.Ident(name,_);body] ->
- ThfDefinition($3,unreserve name,body)
- | _ -> prerr_endline ("near " ^ $3); assert false)
- | Type ->
- (match $7 with
- | T.Cast (T.Ident(name,_),ty) -> ThfType($3,unreserve name,ty)
- | _ -> assert false)
- | _ -> ThfFormula($3,$5,$7)
- }
- ;
-
- 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
- | "type" -> Type
- | _ -> assert false
- }
- ;
-
- quantifier :
- | FORALL {`Forall}
- | EXISTS {`Exists}
- | LAMBDA {`Lambda}
-
- vardecl :
- | UNAME { T.Ident($1,None), None }
- | UNAME COLON term { T.Ident($1,None),Some $3 }
-
- varlist :
- | vardecl { [$1] }
- | vardecl COMMA varlist { $1 :: $3 }
-
- term:
- | quantifier BEGINVARLIST varlist ENDVARLIST COLON term {
- List.fold_right (fun v t -> T.Binder($1,v,t)) $3 $6
- }
- | term APPLY term {
- match $1 with
- | T.Appl l -> T.Appl (l @ [$3])
- | x -> T.Appl ([$1; $3])
- }
- | LPAREN term COLON term RPAREN { T.Cast ($2,$4) }
- | term TO term { T.Binder (`Forall,(T.Ident("_",None),Some $1),$3) }
- | term IMPLY term { T.Binder (`Forall,(T.Ident("_",None),Some $1),$3) }
- | term IMPLYLR term { T.Binder (`Forall,(T.Ident("_",None),Some $3),$1) }
- | term COIMPLY term { T.Appl [T.Symbol("Iff",0);$1;$3] }
- | term XOR term { T.Appl [T.Symbol("Xor",0);$1;$3] }
- | term IEQ term { T.Appl [T.Symbol("Eq",0);$1;$3] }
- | term NIEQ term { T.Appl [T.Symbol("NotEq",0);$1;$3] }
- | term IAND term { T.Appl [T.Symbol("And",0);$1;$3] }
- | term IOR term { T.Appl [T.Symbol("Or",0);$1;$3] }
- | NOT term { T.Appl [T.Symbol("Not",0);$2] }
- | LPAREN term RPAREN {$2}
- | LNAME { T.Ident(unreserve $1,None) }
- | UNAME { T.Ident($1,None) }
- | TYPE_I { T.Symbol("i",0) }
- | TYPE_O { T.Symbol("o",0) }
- | TYPE_U { T.Sort (`NType "0") }
- | FALSE { T.Symbol("False",0)}
- | TRUE { T.Symbol("True",0)}
- ;
-
- include_:
- | INCLUSION LPAREN QSTRING selection_of_formulae RPAREN DOT {
- let fname = rm_q $3 in
- Inclusion (fname,$4)
- }
- ;
-
- selection_of_formulae:
- | { [] }
- | COMMA name selection_of_formulae { $2::$3 }
- ;
-
- comment: COMMENT {Comment $1} ;
-
- name: NUM { string_of_int $1} | LNAME { $1 } | UNAME { $1 } ;
-%%
- (* trailer *)
+++ /dev/null
-SWV438^1
-SWV443^1
-SWV425^2
-SWV428^2
-SWV432^2
-SWV428^1
-SWV431^2
-SWV430^1
-SWV436^3
-SWV439^1
-SWV441^1
-SWV432^1
-SWV426^4
-SWV427^2
-SWV433^1
-SWV427^1
-SWV435^3
-SWV426^3
-SWV444^1
-SWV429^1
-SWV426^2
-SWV430^2
-SWV437^1
-SWV425^1
-SWV440^1
-SWV429^2
-SWV447^1
-SWV426^1
-SWV446^1
-SWV434^3
-SWV442^1
-SWV433^2
-SWV431^1
-SWV436^4
-SWV445^1
-SWV435^4
-SWV434^4
-SYO272^5
-SYO337^5
-SYO130^5
-SYO408^1
-SYO147^5
-SYO466^1
-SYO188^5
-SYO174^5
-SYO165^5
-SYO466^2
-SYO432^1
-SYO228^5
-SYO120^5
-SYO436^1
-SYO184^5
-SYO296^5
-SYO483^6
-SYO284^5
-SYO462^1
-SYO465^1
-SYO278^5
-SYO471^2
-SYO453^5
-SYO217^5
-SYO314^5
-SYO160^5
-SYO302^5
-SYO367^5
-SYO064^4.001
-SYO048^1
-SYO065^4.003
-SYO176^5
-SYO092^5
-SYO245^5
-SYO131^5
-SYO002^1
-SYO063^4
-SYO234^5
-SYO472^4
-SYO159^5
-SYO062^4.003
-SYO424^1
-SYO304^5
-SYO155^5
-SYO468^4
-SYO455^5
-SYO425^1
-SYO457^2
-SYO050^1
-SYO201^5
-SYO112^5
-SYO454^4
-SYO071^4.001
-SYO009^1
-SYO182^5
-SYO482^6
-SYO499^1
-SYO205^5
-SYO462^2
-SYO067^4.004
-SYO193^5
-SYO311^5
-SYO455^2
-SYO049^1
-SYO163^5
-SYO401^1
-SYO455^3
-SYO473^5
-SYO146^5
-SYO305^5
-SYO471^6
-SYO451^6
-SYO241^5
-SYO462^4
-SYO042^1
-SYO448^1
-SYO012^1
-SYO275^5
-SYO026^1
-SYO395^1
-SYO021^1
-SYO065^4.001
-SYO464^2
-SYO010^1
-SYO058^4
-SYO313^5
-SYO303^5
-SYO294^5
-SYO032^1
-SYO232^5
-SYO342^5
-SYO454^2
-SYO463^1
-SYO239^5
-SYO468^3
-SYO379^5
-SYO186^5
-SYO339^5
-SYO455^6
-SYO427^1
-SYO298^5
-SYO397^1
-SYO473^6
-SYO183^5
-SYO461^6
-SYO354^5
-SYO317^5
-SYO100^5
-SYO465^2
-SYO386^5
-SYO474^5
-SYO416^1
-SYO149^5
-SYO464^4
-SYO098^5
-SYO223^5
-SYO450^1
-SYO437^1
-SYO074^4.003
-SYO451^2
-SYO472^6
-SYO462^6
-SYO224^5
-SYO081^5
-SYO085^5
-SYO316^5
-SYO127^5
-SYO072^4.001
-SYO363^5
-SYO072^4.003
-SYO469^2
-SYO216^5
-SYO212^5
-SYO450^6
-SYO373^5
-SYO400^1
-SYO461^2
-SYO290^5
-SYO210^5
-SYO252^5
-SYO221^5
-SYO046^1
-SYO415^1
-SYO069^4.002
-SYO022^1
-SYO460^6
-SYO420^1
-SYO459^6
-SYO478^6
-SYO168^5
-SYO315^5
-SYO403^1
-SYO177^5
-SYO465^5
-SYO079^5
-SYO097^5
-SYO001^1
-SYO348^5
-SYO069^4.001
-SYO454^6
-SYO467^2
-SYO164^5
-SYO497^6
-SYO262^5
-SYO452^6
-SYO464^3
-SYO019^1
-SYO450^4
-SYO291^5
-SYO070^4.003
-SYO471^1
-SYO116^5
-SYO393^1
-SYO114^5
-SYO003^1
-SYO471^4
-SYO453^2
-SYO285^5
-SYO371^5
-SYO173^5
-SYO005^1
-SYO470^3
-SYO271^5
-SYO431^1
-SYO070^4.004
-SYO144^5
-SYO326^5
-SYO269^5
-SYO204^5
-SYO466^6
-SYO004^1
-SYO101^5
-SYO102^5
-SYO484^6
-SYO438^1
-SYO451^1
-SYO074^4.001
-SYO494^6
-SYO109^5
-SYO074^4.002
-SYO067^4.002
-SYO345^5
-SYO052^2
-SYO106^5
-SYO334^5
-SYO189^5
-SYO351^5
-SYO222^5
-SYO378^5
-SYO170^5
-SYO459^4
-SYO470^6
-SYO452^1
-SYO445^1
-SYO380^5
-SYO076^5
-SYO329^5
-SYO029^1
-SYO208^5
-SYO258^5
-SYO073^4.004
-SYO479^6
-SYO467^6
-SYO467^1
-SYO248^5
-SYO207^5
-SYO306^5
-SYO199^5
-SYO444^1
-SYO015^1
-SYO381^5
-SYO051^1
-SYO470^1
-SYO064^4.002
-SYO468^5
-SYO251^5
-SYO453^4
-SYO136^5
-SYO054^2
-SYO218^5
-SYO451^4
-SYO336^5
-SYO430^1
-SYO064^4.004
-SYO171^5
-SYO071^4.002
-SYO469^3
-SYO119^5
-SYO469^5
-SYO105^5
-SYO069^4.003
-SYO061^4
-SYO073^4.003
-SYO008^1
-SYO419^1
-SYO175^5
-SYO288^5
-SYO031^1
-SYO040^1
-SYO358^5
-SYO331^5
-SYO385^5
-SYO292^5
-SYO020^1
-SYO071^4.004
-SYO471^5
-SYO068^4.020
-SYO384^5
-SYO074^4.004
-SYO418^1
-SYO157^5
-SYO247^5
-SYO423^1
-SYO067^4.001
-SYO065^4.002
-SYO023^1
-SYO135^5
-SYO410^1
-SYO362^5
-SYO459^3
-SYO198^5
-SYO140^5
-SYO254^5
-SYO452^3
-SYO280^5
-SYO192^5
-SYO094^5
-SYO088^5
-SYO153^5
-SYO376^5
-SYO346^5
-SYO399^1
-SYO043^1
-SYO377^5
-SYO454^1
-SYO255^5
-SYO489^6
-SYO325^5
-SYO066^4.004
-SYO034^1
-SYO220^5
-SYO369^5
-SYO456^6
-SYO396^1
-SYO498^6
-SYO203^5
-SYO481^6
-SYO055^2
-SYO166^5
-SYO470^5
-SYO495^6
-SYO200^5
-SYO457^1
-SYO412^1
-SYO117^5
-SYO413^1
-SYO458^4
-SYO460^1
-SYO472^5
-SYO493^6
-SYO073^4.001
-SYO405^1
-SYO191^5
-SYO382^5
-SYO268^5
-SYO287^5
-SYO389^5
-SYO394^1
-SYO141^5
-SYO457^5
-SYO454^3
-SYO219^5
-SYO213^5
-SYO426^1
-SYO062^4.004
-SYO257^5
-SYO006^1
-SYO073^4.002
-SYO025^1
-SYO142^5
-SYO129^5
-SYO229^5
-SYO087^5
-SYO250^5
-SYO320^5
-SYO473^1
-SYO267^5
-SYO392^1
-SYO122^5
-SYO450^5
-SYO417^1
-SYO319^5
-SYO463^6
-SYO321^5
-SYO356^5
-SYO167^5
-SYO274^5
-SYO469^1
-SYO467^5
-SYO113^5
-SYO035^1
-SYO488^6
-SYO347^5
-SYO256^5
-SYO107^5
-SYO099^5
-SYO045^1
-SYO458^3
-SYO041^1
-SYO007^1
-SYO039^1
-SYO143^5
-SYO472^2
-SYO068^4.001
-SYO428^1
-SYO332^5
-SYO235^5
-SYO065^4.004
-SYO452^4
-SYO490^6
-SYO295^5
-SYO178^5
-SYO464^5
-SYO162^5
-SYO349^5
-SYO324^5
-SYO447^1
-SYO069^4.004
-SYO457^3
-SYO264^5
-SYO366^5
-SYO158^5
-SYO463^5
-SYO226^5
-SYO333^5
-SYO463^3
-SYO472^3
-SYO110^5
-SYO465^3
-SYO471^3
-SYO335^5
-SYO341^5
-SYO322^5
-SYO473^4
-SYO078^5
-SYO309^5
-SYO279^5
-SYO297^5
-SYO474^3
-SYO350^5
-SYO018^1
-SYO187^5
-SYO340^5
-SYO103^5
-SYO353^5
-SYO123^5
-SYO240^5
-SYO458^6
-SYO475^6
-SYO456^1
-SYO054^1
-SYO086^5
-SYO231^5
-SYO154^5
-SYO391^5
-SYO451^5
-SYO080^5
-SYO312^5
-SYO491^6
-SYO462^3
-SYO249^5
-SYO474^2
-SYO460^5
-SYO033^1
-SYO476^6
-SYO458^5
-SYO487^6
-SYO059^4
-SYO172^5
-SYO028^1
-SYO180^5
-SYO121^5
-SYO206^5
-SYO352^5
-SYO024^1
-SYO470^2
-SYO453^3
-SYO273^5
-SYO263^5
-SYO406^1
-SYO450^2
-SYO460^4
-SYO011^1
-SYO066^4.002
-SYO075^5
-SYO093^5
-SYO237^5
-SYO179^5
-SYO374^5
-SYO328^5
-SYO429^1
-SYO458^1
-SYO443^1
-SYO050^2
-SYO343^5
-SYO323^5
-SYO053^1
-SYO082^5
-SYO067^4.003
-SYO108^5
-SYO261^5
-SYO387^5
-SYO449^1
-SYO238^5
-SYO407^1
-SYO276^5
-SYO084^5
-SYO467^3
-SYO051^2
-SYO435^1
-SYO474^6
-SYO115^5
-SYO056^2
-SYO244^5
-SYO243^5
-SYO464^6
-SYO037^1
-SYO465^4
-SYO111^5
-SYO462^5
-SYO456^4
-SYO458^2
-SYO038^1
-SYO132^5
-SYO473^2
-SYO027^1
-SYO190^5
-SYO197^5
-SYO195^5
-SYO030^1
-SYO286^5
-SYO134^5
-SYO368^5
-SYO456^3
-SYO460^3
-SYO307^5
-SYO344^5
-SYO355^5
-SYO202^5
-SYO365^5
-SYO095^5
-SYO253^5
-SYO459^1
-SYO057^1
-SYO246^5
-SYO442^1
-SYO053^2
-SYO152^5
-SYO070^4.001
-SYO474^1
-SYO066^4.003
-SYO468^6
-SYO300^5
-SYO125^5
-SYO470^4
-SYO402^1
-SYO440^1
-SYO456^2
-SYO214^5
-SYO308^5
-SYO070^4.002
-SYO375^5
-SYO468^2
-SYO016^1
-SYO383^5
-SYO467^4
-SYO090^5
-SYO242^5
-SYO148^5
-SYO196^5
-SYO453^1
-SYO047^1
-SYO370^5
-SYO145^5
-SYO194^5
-SYO126^5
-SYO139^5
-SYO466^3
-SYO485^6
-SYO455^4
-SYO017^1
-SYO066^4.001
-SYO486^6
-SYO209^5
-SYO461^5
-SYO169^5
-SYO433^1
-SYO265^5
-SYO225^5
-SYO459^2
-SYO064^4.003
-SYO057^2
-SYO472^1
-SYO463^4
-SYO450^3
-SYO469^6
-SYO452^5
-SYO161^5
-SYO460^2
-SYO071^4.003
-SYO496^6
-SYO260^5
-SYO301^5
-SYO466^4
-SYO062^4.002
-SYO185^5
-SYO461^3
-SYO211^5
-SYO357^5
-SYO454^5
-SYO089^5
-SYO360^5
-SYO137^5
-SYO455^1
-SYO457^6
-SYO289^5
-SYO474^4
-SYO388^5
-SYO414^1
-SYO451^3
-SYO118^5
-SYO463^2
-SYO277^5
-SYO327^5
-SYO421^1
-SYO464^1
-SYO151^5
-SYO283^5
-SYO133^5
-SYO124^5
-SYO227^5
-SYO338^5
-SYO409^1
-SYO404^1
-SYO236^5
-SYO266^5
-SYO138^5
-SYO128^5
-SYO270^5
-SYO068^4.010
-SYO230^5
-SYO468^1
-SYO330^5
-SYO456^5
-SYO068^4.005
-SYO310^5
-SYO398^1
-SYO215^5
-SYO459^5
-SYO461^4
-SYO318^5
-SYO500^1
-SYO361^5
-SYO473^3
-SYO156^5
-SYO422^1
-SYO434^1
-SYO453^6
-SYO364^5
-SYO411^1
-SYO052^1
-SYO072^4.004
-SYO469^4
-SYO441^1
-SYO457^4
-SYO055^1
-SYO060^4
-SYO390^5
-SYO044^1
-SYO077^5
-SYO181^5
-SYO096^5
-SYO359^5
-SYO013^1
-SYO372^5
-SYO480^6
-SYO282^5
-SYO461^1
-SYO293^5
-SYO439^1
-SYO056^1
-SYO072^4.002
-SYO477^6
-SYO465^6
-SYO233^5
-SYO150^5
-SYO091^5
-SYO281^5
-SYO259^5
-SYO452^2
-SYO492^6
-SYO466^5
-SYO446^1
-SYO104^5
-SYO083^5
-SYO299^5
-LCL613^1
-LCL690^1
-LCL612^1
-LCL600^1
-LCL586^1
-LCL739^5
-LCL718^1
-LCL606^1
-LCL615^1
-LCL618^1
-LCL585^1
-LCL587^1
-LCL623^1
-LCL583^1
-LCL742^5
-LCL230^4
-LCL723^1
-LCL594^1
-LCL624^1
-LCL737^5
-LCL634^1
-LCL584^1
-LCL703^1
-LCL695^1
-LCL607^1
-LCL692^1
-LCL593^1
-LCL591^1
-LCL604^1
-LCL698^1
-LCL706^1
-LCL720^1
-LCL694^1
-LCL588^1
-LCL708^1
-LCL626^1
-LCL595^1
-LCL711^1
-LCL621^1
-LCL596^1
-LCL732^5
-LCL693^1
-LCL710^1
-LCL590^1
-LCL741^5
-LCL731^5
-LCL740^5
-LCL629^1
-LCL627^1
-LCL738^5
-LCL735^5
-LCL743^5
-LCL619^1
-LCL592^1
-LCL699^1
-LCL609^1
-LCL598^1
-LCL705^1
-LCL697^1
-LCL724^1
-LCL721^1
-LCL712^1
-LCL730^5
-LCL625^1
-LCL691^1
-LCL614^1
-LCL715^1
-LCL580^1
-LCL736^5
-LCL716^1
-LCL599^1
-LCL631^1
-LCL597^1
-LCL700^1
-LCL582^1
-LCL696^1
-LCL603^1
-LCL608^1
-LCL717^1
-LCL727^5
-LCL704^1
-LCL632^1
-LCL733^5
-LCL713^1
-LCL601^1
-LCL729^5
-LCL714^1
-LCL725^1
-LCL630^1
-LCL709^1
-LCL620^1
-LCL728^5
-LCL602^1
-LCL726^5
-LCL581^1
-LCL719^1
-LCL707^1
-LCL633^1
-LCL617^1
-LCL722^1
-LCL701^1
-LCL702^1
-LCL181^4
-LCL611^1
-LCL589^1
-LCL734^5
-LCL579^1
-SYN987^1
-SYN977^4
-SYN731^5
-SYN392^4
-SYN992^1
-SYN007^4.014
-SYN045^4
-SYN386^5
-SYN393^4.003
-SYN416^4
-SYN381^5
-SYN049^5
-SYN046^4
-SYN983^1
-SYN374^5
-SYN382^5
-SYN064^5
-SYN393^4.004
-SYN997^1
-SYN998^1
-SYN978^4
-SYN055^5
-SYN389^4
-SYN984^1
-SYN036^5
-SYN001^4.003
-SYN363^5
-SYN358^5
-SYN001^4.004
-SYN996^1
-SYN988^1
-SYN361^5
-SYN355^5
-SYN391^4
-SYN041^4
-SYN991^1
-SYN390^4
-SYN388^4
-SYN364^5
-SYN001^4.001
-SYN040^4
-SYN989^2
-SYN988^2
-SYN365^5
-SYN044^4
-SYN995^1
-SYN387^4
-SYN000^1
-SYN985^1
-SYN357^5
-SYN393^4.002
-SYN990^1
-SYN001^4.002
-SYN360^5
-SYN047^4
-SYN059^5
-SYN375^5
-SYN000^2
-SYN057^5
-SYN994^1
-SYN356^5
-SYN987^2
-SYN058^5
-SYN051^5
-SYN989^1
-SYN916^4
-SYN377^5
-SYN999^1
-SYN915^4
-SYN056^5
-SYN732^5
-SYN993^1
-ALG282^5
-ALG298^5
-ALG256^1
-ALG248^1
-ALG268^4
-ALG290^5
-ALG258^2
-ALG249^3
-ALG251^3
-ALG278^5
-ALG265^2
-ALG257^1
-ALG275^5
-ALG272^5
-ALG270^5
-ALG263^1
-ALG264^2
-ALG266^1
-ALG266^2
-ALG261^2
-ALG292^5
-ALG274^5
-ALG258^1
-ALG253^2
-ALG260^1
-ALG268^1
-ALG251^1
-ALG285^5
-ALG277^5
-ALG263^2
-ALG280^5
-ALG287^5
-ALG284^5
-ALG267^2
-ALG289^5
-ALG286^5
-ALG254^2
-ALG269^2
-ALG257^2
-ALG252^2
-ALG251^2
-ALG288^5
-ALG273^5
-ALG248^3
-ALG268^5
-ALG268^3
-ALG297^5
-ALG269^3
-ALG259^2
-ALG295^5
-ALG281^5
-ALG296^5
-ALG269^4
-ALG001^5
-ALG262^2
-ALG294^5
-ALG254^1
-ALG293^5
-ALG276^5
-ALG264^3
-ALG264^1
-ALG269^1
-ALG253^1
-ALG250^3
-ALG271^5
-ALG283^5
-ALG255^1
-ALG260^2
-ALG268^6
-ALG259^1
-ALG279^5
-ALG263^3
-ALG248^2
-ALG261^1
-ALG247^2
-ALG252^1
-ALG256^2
-ALG291^5
-ALG268^2
-ALG267^1
-GRP001^5
-SEV236^5
-SEV341^5
-SEV299^5
-SEV206^5
-SEV069^5
-SEV251^5
-SEV309^5
-SEV286^5
-SEV356^5
-SEV227^5
-SEV102^5
-SEV040^5
-SEV157^5
-SEV055^5
-SEV059^5
-SEV303^5
-SEV008^5
-SEV129^5
-SEV262^5
-SEV099^5
-SEV295^5
-SEV047^5
-SEV337^5
-SEV006^5
-SEV390^5
-SEV339^5
-SEV306^5
-SEV193^5
-SEV345^5
-SEV138^5
-SEV241^5
-SEV344^5
-SEV070^5
-SEV121^5
-SEV253^5
-SEV403^5
-SEV229^5
-SEV016^5
-SEV273^5
-SEV035^5
-SEV134^5
-SEV252^5
-SEV272^5
-SEV145^5
-SEV338^5
-SEV304^5
-SEV208^5
-SEV233^5
-SEV131^5
-SEV077^5
-SEV413^5
-SEV392^5
-SEV122^5
-SEV275^5
-SEV051^5
-SEV065^5
-SEV380^5
-SEV329^5
-SEV120^5
-SEV048^5
-SEV343^5
-SEV375^5
-SEV014^5
-SEV147^5
-SEV033^5
-SEV091^5
-SEV287^5
-SEV290^5
-SEV311^5
-SEV152^5
-SEV115^5
-SEV171^5
-SEV360^5
-SEV310^5
-SEV036^5
-SEV342^5
-SEV293^5
-SEV271^5
-SEV294^5
-SEV011^5
-SEV210^5
-SEV219^5
-SEV226^5
-SEV019^5
-SEV354^5
-SEV186^5
-SEV312^5
-SEV175^5
-SEV325^5
-SEV018^5
-SEV334^5
-SEV137^5
-SEV280^5
-SEV201^5
-SEV258^5
-SEV034^5
-SEV288^5
-SEV263^5
-SEV100^5
-SEV410^5
-SEV140^5
-SEV020^5
-SEV216^5
-SEV142^5
-SEV162^5
-SEV195^5
-SEV406^5
-SEV355^5
-SEV202^5
-SEV265^5
-SEV071^5
-SEV317^5
-SEV281^5
-SEV207^5
-SEV296^5
-SEV007^5
-SEV298^5
-SEV073^5
-SEV083^5
-SEV028^5
-SEV139^5
-SEV221^5
-SEV234^5
-SEV119^5
-SEV245^5
-SEV373^5
-SEV319^5
-SEV400^5
-SEV151^5
-SEV094^5
-SEV218^5
-SEV377^5
-SEV165^5
-SEV358^5
-SEV246^5
-SEV090^5
-SEV143^5
-SEV079^5
-SEV062^5
-SEV114^5
-SEV331^5
-SEV209^5
-SEV057^5
-SEV243^5
-SEV402^5
-SEV188^5
-SEV023^5
-SEV418^5
-SEV166^5
-SEV316^5
-SEV395^5
-SEV178^5
-SEV156^5
-SEV066^5
-SEV061^5
-SEV323^5
-SEV397^5
-SEV126^5
-SEV283^5
-SEV414^5
-SEV135^5
-SEV371^5
-SEV060^5
-SEV387^5
-SEV068^5
-SEV256^5
-SEV074^5
-SEV198^5
-SEV044^5
-SEV108^5
-SEV124^5
-SEV001^5
-SEV179^5
-SEV197^5
-SEV385^5
-SEV043^5
-SEV200^5
-SEV314^5
-SEV112^5
-SEV277^5
-SEV411^5
-SEV012^5
-SEV089^5
-SEV105^5
-SEV184^5
-SEV381^5
-SEV204^5
-SEV169^5
-SEV223^5
-SEV086^5
-SEV024^5
-SEV106^5
-SEV285^5
-SEV097^5
-SEV374^5
-SEV230^5
-SEV003^5
-SEV328^5
-SEV075^5
-SEV333^5
-SEV146^5
-SEV396^5
-SEV389^5
-SEV181^5
-SEV103^5
-SEV196^5
-SEV408^5
-SEV340^5
-SEV274^5
-SEV409^5
-SEV203^5
-SEV087^5
-SEV282^5
-SEV407^5
-SEV353^5
-SEV168^5
-SEV249^5
-SEV096^5
-SEV133^5
-SEV125^5
-SEV379^5
-SEV199^5
-SEV067^5
-SEV362^5
-SEV350^5
-SEV404^5
-SEV010^5
-SEV365^5
-SEV352^5
-SEV098^5
-SEV026^5
-SEV084^5
-SEV078^5
-SEV158^5
-SEV419^5
-SEV153^5
-SEV161^5
-SEV113^5
-SEV191^5
-SEV190^5
-SEV017^5
-SEV056^5
-SEV307^5
-SEV412^5
-SEV013^5
-SEV394^5
-SEV318^5
-SEV111^5
-SEV058^5
-SEV349^5
-SEV167^5
-SEV361^5
-SEV369^5
-SEV388^5
-SEV150^5
-SEV085^5
-SEV052^5
-SEV242^5
-SEV046^5
-SEV330^5
-SEV382^5
-SEV192^5
-SEV239^5
-SEV118^5
-SEV320^5
-SEV417^5
-SEV027^5
-SEV391^5
-SEV093^5
-SEV183^5
-SEV127^5
-SEV176^5
-SEV212^5
-SEV050^5
-SEV004^5
-SEV015^5
-SEV081^5
-SEV235^5
-SEV261^5
-SEV370^5
-SEV141^5
-SEV185^5
-SEV259^5
-SEV163^5
-SEV025^5
-SEV187^5
-SEV000^5
-SEV238^5
-SEV080^5
-SEV315^5
-SEV278^5
-SEV031^5
-SEV301^5
-SEV297^5
-SEV250^5
-SEV332^5
-SEV363^5
-SEV364^5
-SEV170^5
-SEV326^5
-SEV228^5
-SEV155^5
-SEV030^5
-SEV130^5
-SEV267^5
-SEV205^5
-SEV064^5
-SEV289^5
-SEV042^5
-SEV092^5
-SEV231^5
-SEV159^5
-SEV132^5
-SEV095^5
-SEV401^5
-SEV254^5
-SEV292^5
-SEV291^5
-SEV110^5
-SEV128^5
-SEV107^5
-SEV211^5
-SEV041^5
-SEV247^5
-SEV372^5
-SEV045^5
-SEV109^5
-SEV257^5
-SEV376^5
-SEV225^5
-SEV321^5
-SEV279^5
-SEV039^5
-SEV268^5
-SEV240^5
-SEV386^5
-SEV378^5
-SEV327^5
-SEV313^5
-SEV104^5
-SEV154^5
-SEV393^5
-SEV305^5
-SEV222^5
-SEV368^5
-SEV116^5
-SEV255^5
-SEV177^5
-SEV217^5
-SEV260^5
-SEV182^5
-SEV123^5
-SEV136^5
-SEV002^5
-SEV101^5
-SEV284^5
-SEV220^5
-SEV148^5
-SEV032^5
-SEV322^5
-SEV244^5
-SEV117^5
-SEV053^5
-SEV324^5
-SEV276^5
-SEV248^5
-SEV172^5
-SEV149^5
-SEV054^5
-SEV346^5
-SEV357^5
-SEV348^5
-SEV021^5
-SEV405^5
-SEV384^5
-SEV232^5
-SEV029^5
-SEV308^5
-SEV383^5
-SEV270^5
-SEV072^5
-SEV088^5
-SEV144^5
-SEV359^5
-SEV160^5
-SEV180^5
-SEV237^5
-SEV173^5
-SEV224^5
-SEV266^5
-SEV269^5
-SEV214^5
-SEV367^5
-SEV076^5
-SEV336^5
-SEV022^5
-SEV194^5
-SEV063^5
-SEV038^5
-SEV398^5
-SEV215^5
-SEV351^5
-SEV264^5
-SEV174^5
-SEV082^5
-SEV415^5
-SEV009^5
-SEV164^5
-SEV399^5
-SEV347^5
-SEV213^5
-SEV189^5
-SEV049^5
-SEV335^5
-SEV005^5
-SEV037^5
-SEV366^5
-SEV302^5
-SEV416^5
-SEV300^5
-SET171^3
-SET612^3
-SET587^5
-SET008^5
-SET636^5
-SET683^3
-SET647^3
-SET624^5
-SET621^5
-SET604^5
-SET557^1
-SET585^5
-SET606^5
-SET616^5
-SET027^5
-SET657^3
-SET200^5
-SET753^4
-SET586^5
-SET593^5
-SET063^5
-SET605^5
-SET680^3
-SET615^5
-SET613^5
-SET589^5
-SET724^4
-SET582^5
-SET629^5
-SET557^5
-SET618^5
-SET591^5
-SET014^4
-SET598^5
-SET592^5
-SET171^5
-SET185^5
-SET628^5
-SET609^5
-SET594^5
-SET606^3
-SET199^5
-SET615^3
-SET162^5
-SET066^1
-SET044^5
-SET011^5
-SET631^5
-SET614^3
-SET580^5
-SET752^4
-SET619^5
-SET143^5
-SET611^3
-SET067^1
-SET599^5
-SET196^5
-SET183^5
-SET603^5
-SET086^1
-SET669^3
-SET580^3
-SET009^5
-SET596^5
-SET673^3
-SET590^5
-SET622^5
-SET610^5
-SET194^5
-SET635^5
-SET595^5
-SET608^5
-SET607^5
-SET716^4
-SET169^5
-SET741^4
-SET624^3
-SET626^5
-SET201^5
-SET588^5
-SET634^5
-SET640^3
-SET601^5
-SET764^4
-SET649^3
-SET017^1
-SET614^5
-SET648^3
-SET607^3
-SET625^5
-SET630^3
-SET175^5
-SET627^5
-SET671^3
-SET143^3
-SET584^5
-SET043^5
-SET623^5
-SET646^3
-SET620^5
-SET623^3
-SET747^4
-SET597^5
-SET062^5
-SET096^1
-SET010^5
-SET173^5
-SET076^1
-SET014^5
-SET633^5
-SET651^3
-SET144^5
-SET159^5
-SET045^5
-SET672^3
-SET632^5
-SET670^3
-SET617^5
-SET630^5
-SET638^5
-SET600^5
-SET684^3
-SET609^3
-SET046^5
-SET601^3
-SET612^5
-SET611^5
-COM024^5
-GRA039^2
-GRA032^1
-GRA062^2
-GRA065^1
-GRA059^2
-GRA039^1
-GRA073^1
-GRA037^1
-GRA068^2
-GRA048^1
-GRA057^2
-GRA060^1
-GRA036^1
-GRA032^2
-GRA043^1
-GRA070^1
-GRA067^1
-GRA051^1
-GRA051^2
-GRA046^1
-GRA050^1
-GRA055^2
-GRA073^2
-GRA033^2
-GRA053^2
-GRA041^2
-GRA044^2
-GRA064^1
-GRA074^1
-GRA068^1
-GRA057^1
-GRA049^2
-GRA041^1
-GRA028^1
-GRA045^2
-GRA048^2
-GRA031^2
-GRA038^1
-GRA058^1
-GRA074^2
-GRA058^2
-GRA047^1
-GRA049^1
-GRA072^1
-GRA063^1
-GRA044^1
-GRA030^1
-GRA027^1
-GRA035^2
-GRA064^2
-GRA038^2
-GRA052^1
-GRA033^1
-GRA071^1
-GRA047^2
-GRA052^2
-GRA063^2
-GRA071^2
-GRA069^2
-GRA070^2
-GRA043^2
-GRA062^1
-GRA037^2
-GRA059^1
-GRA065^2
-GRA042^1
-GRA050^2
-GRA034^1
-GRA031^1
-GRA029^2
-GRA029^1
-GRA061^2
-GRA040^2
-GRA054^2
-GRA034^2
-GRA046^2
-GRA072^2
-GRA040^1
-GRA056^2
-GRA066^2
-GRA060^2
-GRA056^1
-GRA066^1
-GRA055^1
-GRA053^1
-GRA036^2
-GRA061^1
-GRA035^1
-GRA042^2
-GRA045^1
-GRA054^1
-GRA067^2
-GRA069^1
-PUZ096^5
-PUZ120^5
-PUZ110^5
-PUZ125^5
-PUZ090^5
-PUZ093^5
-PUZ111^5
-PUZ122^5
-PUZ099^5
-PUZ081^3
-PUZ109^5
-PUZ082^1
-PUZ085^1
-PUZ083^1
-PUZ117^5
-PUZ102^5
-PUZ105^5
-PUZ113^5
-PUZ091^5
-PUZ108^5
-PUZ097^5
-PUZ047^5
-PUZ094^5
-PUZ081^2
-PUZ106^5
-PUZ101^5
-PUZ112^5
-PUZ031^5
-PUZ118^5
-PUZ100^5
-PUZ124^5
-PUZ123^5
-PUZ116^5
-PUZ126^5
-PUZ103^5
-PUZ127^5
-PUZ089^5
-PUZ114^5
-PUZ119^5
-PUZ081^1
-PUZ088^5
-PUZ115^5
-PUZ087^1
-PUZ098^5
-PUZ092^5
-PUZ086^1
-PUZ095^5
-PUZ104^5
-PUZ084^1
-PUZ121^5
-PUZ107^5
-SEU546^1
-SEU666^2
-SEU918^5
-SEU543^2
-SEU659^2
-SEU819^2
-SEU852^5
-SEU929^5
-SEU873^5
-SEU965^5
-SEU949^5
-SEU732^1
-SEU713^2
-SEU490^1
-SEU778^2
-SEU975^5
-SEU560^1
-SEU663^1
-SEU673^1
-SEU787^1
-SEU957^5
-SEU741^2
-SEU629^2
-SEU792^1
-SEU684^2
-SEU553^2
-SEU854^5
-SEU800^1
-SEU470^1
-SEU790^2
-SEU974^5
-SEU888^5
-SEU552^1
-SEU832^5
-SEU700^1
-SEU591^2
-SEU587^1
-SEU771^2
-SEU952^5
-SEU712^1
-SEU608^2
-SEU784^2
-SEU579^1
-SEU718^2
-SEU827^1
-SEU656^1
-SEU697^1
-SEU660^1
-SEU637^1
-SEU594^1
-SEU791^1
-SEU548^2
-SEU665^1
-SEU495^1
-SEU865^5
-SEU472^1
-SEU740^2
-SEU463^1
-SEU904^5
-SEU502^2
-SEU499^1
-SEU970^5
-SEU546^2
-SEU513^1
-SEU512^1
-SEU548^1
-SEU634^1
-SEU761^2
-SEU921^5
-SEU619^1
-SEU588^1
-SEU571^1
-SEU740^1
-SEU706^1
-SEU769^1
-SEU989^5
-SEU871^5
-SEU695^1
-SEU642^2
-SEU526^1
-SEU824^2
-SEU465^1
-SEU759^1
-SEU953^5
-SEU513^2
-SEU643^1
-SEU503^2
-SEU645^2
-SEU684^1
-SEU569^2
-SEU452^1
-SEU799^2
-SEU928^5
-SEU651^2
-SEU968^5
-SEU916^5
-SEU702^2
-SEU863^5
-SEU644^2
-SEU917^5
-SEU774^2
-SEU940^5
-SEU461^1
-SEU464^1
-SEU670^2
-SEU743^1
-SEU650^1
-SEU663^2
-SEU543^1
-SEU922^5
-SEU826^1
-SEU609^2
-SEU747^2
-SEU582^1
-SEU942^5
-SEU931^5
-SEU550^1
-SEU941^5
-SEU920^5
-SEU626^1
-SEU605^2
-SEU950^5
-SEU770^2
-SEU717^2
-SEU607^2
-SEU466^1
-SEU818^2
-SEU788^2
-SEU530^2
-SEU563^2
-SEU866^5
-SEU633^1
-SEU596^1
-SEU807^1
-SEU848^5
-SEU597^2
-SEU725^2
-SEU535^1
-SEU685^2
-SEU676^2
-SEU615^2
-SEU935^5
-SEU884^5
-SEU653^1
-SEU696^2
-SEU673^2
-SEU655^1
-SEU721^2
-SEU558^2
-SEU575^2
-SEU640^1
-SEU521^1
-SEU804^1
-SEU875^5
-SEU741^1
-SEU514^1
-SEU674^1
-SEU664^1
-SEU788^1
-SEU593^2
-SEU487^1
-SEU575^1
-SEU913^5
-SEU812^2
-SEU523^2
-SEU946^5
-SEU705^2
-SEU674^2
-SEU841^5
-SEU905^5
-SEU629^1
-SEU619^2
-SEU693^1
-SEU512^2
-SEU579^2
-SEU462^1
-SEU493^1
-SEU627^2
-SEU500^2
-SEU577^1
-SEU699^1
-SEU767^1
-SEU885^5
-SEU803^1
-SEU565^2
-SEU816^1
-SEU820^2
-SEU793^2
-SEU760^2
-SEU783^1
-SEU816^2
-SEU892^5
-SEU707^1
-SEU881^5
-SEU622^2
-SEU563^1
-SEU644^1
-SEU606^2
-SEU855^5
-SEU765^1
-SEU636^1
-SEU507^2
-SEU769^2
-SEU776^1
-SEU668^1
-SEU723^2
-SEU744^2
-SEU582^2
-SEU497^1
-SEU843^5
-SEU677^1
-SEU692^1
-SEU610^1
-SEU786^1
-SEU688^2
-SEU636^2
-SEU600^2
-SEU577^2
-SEU726^2
-SEU906^5
-SEU992^5
-SEU901^5
-SEU625^2
-SEU574^2
-SEU589^1
-SEU737^1
-SEU479^1
-SEU539^2
-SEU729^1
-SEU729^2
-SEU511^1
-SEU638^2
-SEU880^5
-SEU555^1
-SEU939^5
-SEU998^5
-SEU504^2
-SEU679^1
-SEU823^1
-SEU701^1
-SEU710^2
-SEU768^2
-SEU573^2
-SEU525^1
-SEU648^2
-SEU786^2
-SEU558^1
-SEU706^2
-SEU510^2
-SEU712^2
-SEU976^5
-SEU926^5
-SEU652^1
-SEU990^5
-SEU822^2
-SEU962^5
-SEU637^2
-SEU635^2
-SEU753^2
-SEU853^5
-SEU477^1
-SEU584^1
-SEU590^2
-SEU640^2
-SEU800^2
-SEU567^2
-SEU986^5
-SEU802^1
-SEU574^1
-SEU569^1
-SEU538^2
-SEU993^5
-SEU724^1
-SEU762^1
-SEU628^2
-SEU655^2
-SEU641^2
-SEU654^1
-SEU494^1
-SEU604^2
-SEU676^1
-SEU578^2
-SEU623^2
-SEU625^1
-SEU956^5
-SEU780^1
-SEU778^1
-SEU744^1
-SEU724^2
-SEU524^2
-SEU459^1
-SEU478^1
-SEU908^5
-SEU847^5
-SEU669^1
-SEU987^5
-SEU588^2
-SEU810^1
-SEU509^1
-SEU639^1
-SEU481^1
-SEU523^1
-SEU981^5
-SEU647^2
-SEU995^5
-SEU626^2
-SEU671^1
-SEU802^2
-SEU787^2
-SEU750^2
-SEU603^1
-SEU586^2
-SEU882^5
-SEU687^1
-SEU711^2
-SEU638^1
-SEU609^1
-SEU585^2
-SEU746^2
-SEU831^5
-SEU733^1
-SEU742^2
-SEU710^1
-SEU766^1
-SEU809^2
-SEU564^2
-SEU912^5
-SEU680^1
-SEU507^1
-SEU476^1
-SEU948^5
-SEU611^1
-SEU622^1
-SEU678^1
-SEU570^1
-SEU836^5
-SEU780^2
-SEU639^2
-SEU624^1
-SEU878^5
-SEU902^5
-SEU654^2
-SEU483^1
-SEU988^5
-SEU814^2
-SEU890^5
-SEU667^1
-SEU945^5
-SEU934^5
-SEU782^1
-SEU595^1
-SEU551^1
-SEU489^1
-SEU704^2
-SEU969^5
-SEU746^1
-SEU821^1
-SEU725^1
-SEU534^1
-SEU496^1
-SEU554^1
-SEU757^1
-SEU977^5
-SEU618^1
-SEU947^5
-SEU565^1
-SEU549^1
-SEU506^2
-SEU595^2
-SEU803^2
-SEU685^1
-SEU606^1
-SEU594^2
-SEU698^1
-SEU761^1
-SEU732^2
-SEU642^1
-SEU616^1
-SEU840^5
-SEU797^2
-SEU527^1
-SEU469^1
-SEU933^5
-SEU722^2
-SEU943^5
-SEU547^1
-SEU653^2
-SEU659^1
-SEU615^1
-SEU628^1
-SEU717^1
-SEU796^1
-SEU571^2
-SEU966^5
-SEU752^1
-SEU893^5
-SEU783^2
-SEU541^1
-SEU735^1
-SEU756^1
-SEU500^1
-SEU822^1
-SEU869^5
-SEU518^1
-SEU561^1
-SEU475^1
-SEU651^1
-SEU883^5
-SEU728^1
-SEU754^2
-SEU899^5
-SEU515^2
-SEU891^5
-SEU508^2
-SEU667^2
-SEU566^1
-SEU657^1
-SEU503^1
-SEU806^1
-SEU731^1
-SEU598^1
-SEU557^1
-SEU844^5
-SEU996^5
-SEU486^1
-SEU682^1
-SEU779^2
-SEU658^2
-SEU567^1
-SEU610^2
-SEU887^5
-SEU781^1
-SEU596^2
-SEU613^2
-SEU647^1
-SEU568^2
-SEU868^5
-SEU824^3
-SEU815^1
-SEU897^5
-SEU811^2
-SEU605^1
-SEU752^2
-SEU549^2
-SEU796^2
-SEU509^2
-SEU751^1
-SEU485^1
-SEU896^5
-SEU664^2
-SEU620^1
-SEU932^5
-SEU773^2
-SEU680^2
-SEU576^1
-SEU851^5
-SEU833^5
-SEU745^2
-SEU919^5
-SEU508^1
-SEU601^1
-SEU691^1
-SEU856^5
-SEU617^2
-SEU618^2
-SEU799^1
-SEU559^2
-SEU614^2
-SEU791^2
-SEU645^1
-SEU620^2
-SEU689^2
-SEU562^2
-SEU727^1
-SEU694^1
-SEU805^1
-SEU879^5
-SEU776^2
-SEU775^1
-SEU709^2
-SEU818^1
-SEU656^2
-SEU458^1
-SEU978^5
-SEU529^2
-SEU536^2
-SEU747^1
-SEU551^2
-SEU474^1
-SEU621^2
-SEU603^2
-SEU544^2
-SEU795^1
-SEU755^1
-SEU999^5
-SEU792^2
-SEU900^5
-SEU937^5
-SEU737^2
-SEU665^2
-SEU699^2
-SEU708^1
-SEU972^5
-SEU817^1
-SEU814^1
-SEU719^1
-SEU556^1
-SEU789^1
-SEU867^5
-SEU915^5
-SEU601^2
-SEU535^2
-SEU482^1
-SEU612^2
-SEU515^1
-SEU504^1
-SEU456^1
-SEU798^1
-SEU911^5
-SEU714^1
-SEU963^5
-SEU984^5
-SEU714^2
-SEU672^2
-SEU617^1
-SEU820^1
-SEU745^1
-SEU774^1
-SEU672^1
-SEU795^2
-SEU514^2
-SEU669^2
-SEU521^2
-SEU849^5
-SEU516^1
-SEU632^2
-SEU692^2
-SEU681^2
-SEU696^1
-SEU997^5
-SEU960^5
-SEU580^1
-SEU764^2
-SEU522^1
-SEU602^2
-SEU964^5
-SEU528^1
-SEU789^2
-SEU707^2
-SEU708^2
-SEU804^2
-SEU924^5
-SEU604^1
-SEU683^2
-SEU661^1
-SEU785^2
-SEU631^2
-SEU537^2
-SEU484^1
-SEU501^2
-SEU516^2
-SEU686^1
-SEU677^2
-SEU860^5
-SEU632^1
-SEU909^5
-SEU573^1
-SEU607^1
-SEU813^1
-SEU510^1
-SEU695^2
-SEU755^2
-SEU581^2
-SEU529^1
-SEU821^2
-SEU592^1
-SEU794^1
-SEU748^1
-SEU688^1
-SEU834^5
-SEU506^1
-SEU679^2
-SEU562^1
-SEU734^1
-SEU790^1
-SEU566^2
-SEU467^1
-SEU641^1
-SEU511^2
-SEU693^2
-SEU591^1
-SEU817^2
-SEU502^1
-SEU734^2
-SEU537^1
-SEU621^1
-SEU815^2
-SEU793^1
-SEU536^1
-SEU797^1
-SEU726^1
-SEU488^1
-SEU690^2
-SEU733^2
-SEU643^2
-SEU608^1
-SEU697^2
-SEU526^2
-SEU683^1
-SEU650^2
-SEU738^2
-SEU675^2
-SEU578^1
-SEU570^2
-SEU798^2
-SEU825^3
-SEU771^1
-SEU611^2
-SEU649^2
-SEU839^5
-SEU961^5
-SEU531^2
-SEU480^1
-SEU775^2
-SEU662^1
-SEU715^2
-SEU750^1
-SEU801^2
-SEU552^2
-SEU473^1
-SEU525^2
-SEU630^1
-SEU772^1
-SEU808^1
-SEU877^5
-SEU614^1
-SEU613^1
-SEU824^1
-SEU547^2
-SEU652^2
-SEU991^5
-SEU808^2
-SEU805^2
-SEU561^2
-SEU973^5
-SEU876^5
-SEU903^5
-SEU857^5
-SEU716^2
-SEU646^2
-SEU460^1
-SEU498^1
-SEU660^2
-SEU735^2
-SEU557^2
-SEU823^2
-SEU730^2
-SEU720^2
-SEU634^2
-SEU731^2
-SEU925^5
-SEU980^5
-SEU813^2
-SEU612^1
-SEU874^5
-SEU686^2
-SEU898^5
-SEU568^1
-SEU736^1
-SEU739^1
-SEU597^1
-SEU532^2
-SEU661^2
-SEU592^2
-SEU930^5
-SEU586^1
-SEU763^1
-SEU627^1
-SEU907^5
-SEU955^5
-SEU539^1
-SEU709^1
-SEU914^5
-SEU718^1
-SEU553^1
-SEU861^5
-SEU758^1
-SEU671^2
-SEU864^5
-SEU728^2
-SEU759^2
-SEU540^1
-SEU738^1
-SEU517^1
-SEU550^2
-SEU542^1
-SEU895^5
-SEU845^5
-SEU770^1
-SEU784^1
-SEU657^2
-SEU951^5
-SEU690^1
-SEU777^1
-SEU519^2
-SEU687^2
-SEU545^2
-SEU635^1
-SEU703^2
-SEU772^2
-SEU468^1
-SEU648^1
-SEU700^2
-SEU983^5
-SEU649^1
-SEU520^1
-SEU705^1
-SEU703^1
-SEU542^2
-SEU527^2
-SEU538^1
-SEU593^1
-SEU518^2
-SEU572^2
-SEU519^1
-SEU689^1
-SEU630^2
-SEU505^1
-SEU631^1
-SEU944^5
-SEU850^5
-SEU810^2
-SEU560^2
-SEU678^2
-SEU564^1
-SEU819^1
-SEU682^2
-SEU580^2
-SEU894^5
-SEU721^1
-SEU828^1
-SEU524^1
-SEU958^5
-SEU829^1
-SEU530^1
-SEU938^5
-SEU730^1
-SEU982^5
-SEU454^1
-SEU794^2
-SEU698^2
-SEU716^1
-SEU623^1
-SEU701^2
-SEU491^1
-SEU501^1
-SEU533^1
-SEU675^1
-SEU858^5
-SEU959^5
-SEU711^1
-SEU985^5
-SEU492^1
-SEU751^2
-SEU455^1
-SEU781^2
-SEU779^1
-SEU979^5
-SEU872^5
-SEU782^2
-SEU545^1
-SEU846^5
-SEU599^1
-SEU589^2
-SEU505^2
-SEU722^1
-SEU471^1
-SEU602^1
-SEU801^1
-SEU662^2
-SEU694^2
-SEU749^1
-SEU540^2
-SEU760^1
-SEU715^1
-SEU576^2
-SEU719^2
-SEU809^1
-SEU599^2
-SEU811^1
-SEU633^2
-SEU994^5
-SEU886^5
-SEU531^1
-SEU768^1
-SEU583^1
-SEU704^1
-SEU743^2
-SEU764^1
-SEU528^2
-SEU584^2
-SEU756^2
-SEU757^2
-SEU835^5
-SEU559^1
-SEU581^1
-SEU889^5
-SEU923^5
-SEU727^2
-SEU587^2
-SEU773^1
-SEU910^5
-SEU691^2
-SEU600^1
-SEU544^1
-SEU646^1
-SEU666^1
-SEU541^2
-SEU532^1
-SEU807^2
-SEU927^5
-SEU658^1
-SEU681^1
-SEU859^5
-SEU720^1
-SEU749^2
-SEU534^2
-SEU742^1
-SEU777^2
-SEU517^2
-SEU572^1
-SEU723^1
-SEU739^2
-SEU499^2
-SEU585^1
-SEU590^1
-SEU812^1
-SEU762^2
-SEU670^1
-SEU785^1
-SEU754^1
-SEU862^5
-SEU954^5
-SEU837^5
-SEU842^5
-SEU522^2
-SEU533^2
-SEU457^1
-SEU758^2
-SEU702^1
-SEU753^1
-SEU936^5
-SEU668^2
-SEU736^2
-SEU967^5
-SEU971^5
-SEU806^2
-SEU453^1
-SEU713^1
-SEU598^2
-MSC021^5
-MSC020^5
-NUM661^1
-NUM728^1
-NUM697^1
-NUM653^1
-NUM790^1
-NUM772^1
-NUM637^2
-NUM833^5
-NUM792^1
-NUM815^5
-NUM016^5
-NUM678^1
-NUM726^1
-NUM648^1
-NUM676^1
-NUM801^1
-NUM754^1
-NUM756^1
-NUM799^1
-NUM702^1
-NUM708^1
-NUM677^1
-NUM727^1
-NUM663^1
-NUM021^1
-NUM765^1
-NUM814^5
-NUM773^1
-NUM758^1
-NUM724^1
-NUM689^1
-NUM691^1
-NUM684^1
-NUM780^1
-NUM742^1
-NUM710^1
-NUM664^1
-NUM639^1
-NUM686^1
-NUM636^2
-NUM646^1
-NUM734^1
-NUM642^1
-NUM020^1
-NUM746^1
-NUM774^1
-NUM695^1
-NUM744^1
-NUM709^1
-NUM782^1
-NUM701^1
-NUM812^5
-NUM660^1
-NUM643^1
-NUM798^1
-NUM688^1
-NUM636^3
-NUM652^1
-NUM740^1
-NUM644^1
-NUM671^1
-NUM669^1
-NUM749^1
-NUM681^1
-NUM690^1
-NUM737^1
-NUM797^1
-NUM820^5
-NUM721^1
-NUM760^1
-NUM757^1
-NUM764^1
-NUM821^5
-NUM739^1
-NUM771^1
-NUM818^5
-NUM803^5
-NUM656^1
-NUM636^1
-NUM649^1
-NUM692^1
-NUM730^1
-NUM743^1
-NUM768^1
-NUM826^5
-NUM417^1
-NUM675^1
-NUM419^1
-NUM418^1
-NUM732^1
-NUM791^1
-NUM723^1
-NUM805^5
-NUM637^1
-NUM645^1
-NUM729^1
-NUM647^1
-NUM787^1
-NUM680^1
-NUM806^5
-NUM770^1
-NUM788^1
-NUM670^1
-NUM733^1
-NUM722^1
-NUM786^1
-NUM716^1
-NUM731^1
-NUM785^1
-NUM828^5
-NUM682^1
-NUM717^1
-NUM635^1
-NUM685^1
-NUM635^2
-NUM831^5
-NUM816^5
-NUM703^1
-NUM767^1
-NUM783^1
-NUM650^1
-NUM659^1
-NUM651^1
-NUM641^1
-NUM795^1
-NUM662^1
-NUM715^1
-NUM683^1
-NUM705^1
-NUM657^1
-NUM810^5
-NUM699^1
-NUM811^5
-NUM696^1
-NUM673^1
-NUM658^1
-NUM694^1
-NUM822^5
-NUM830^5
-NUM415^1
-NUM781^1
-NUM638^1
-NUM763^1
-NUM800^1
-NUM804^5
-NUM707^1
-NUM777^1
-NUM809^5
-NUM769^1
-NUM719^1
-NUM759^1
-NUM824^5
-NUM666^1
-NUM784^1
-NUM700^1
-NUM687^1
-NUM668^1
-NUM766^1
-NUM735^1
-NUM796^1
-NUM819^5
-NUM755^1
-NUM654^1
-NUM750^1
-NUM693^1
-NUM667^1
-NUM808^5
-NUM751^1
-NUM829^5
-NUM827^5
-NUM665^1
-NUM747^1
-NUM779^1
-NUM736^1
-NUM825^5
-NUM679^1
-NUM711^1
-NUM789^1
-NUM807^5
-NUM794^1
-NUM776^1
-NUM761^1
-NUM672^1
-NUM775^1
-NUM713^1
-NUM706^1
-NUM748^1
-NUM655^1
-NUM720^1
-NUM416^1
-NUM741^1
-NUM762^1
-NUM793^1
-NUM753^1
-NUM714^1
-NUM718^1
-NUM752^1
-NUM674^1
-NUM823^5
-NUM802^5
-NUM712^1
-NUM640^1
-NUM698^1
-NUM738^1
-NUM832^5
-NUM704^1
-NUM745^1
-NUM834^5
-NUM817^5
-NUM725^1
-NUM813^5
-NUM778^1
+++ /dev/null
-module GA = GrafiteAst;;
-module LA = LexiconAst;;
-module PT = CicNotationPt;;
-module A = Ast;;
-
-type sort = Prop | Univ;;
-
-let floc = HExtlib.dummy_floc;;
-
-
-let paramod_timeout = ref 600;;
-let depth = ref 10;;
-
-let universe = "Univ" ;;
-let prop = "Prop";;
-
-let kw = [
- "and","myand"
-];;
-
-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,Univ)]
- | A.Variable name -> [name,(0,Univ)]
- | A.Function (name,l) ->
- (name,(List.length l,Univ))::
- 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 -> [name,(0,Prop)]
- | A.Predicate (name,args) ->
- (name,(List.length args,Prop)) ::
- (List.flatten (List.map collect_arities_from_term args))
- | A.True -> []
- | A.False -> []
- | A.Eq (t1,t2) ->
- collect_arities_from_term t1 @ collect_arities_from_term t2
- | A.NotEq (t1,t2) ->
- collect_arities_from_term t1 @ collect_arities_from_term t2
- in
- HExtlib.list_uniq (List.sort compare (List.flatten (List.map aux a)))
-;;
-
-let collect_fv_from_atom a =
- let aux = function
- | A.Proposition name -> [name]
- | A.Predicate (name,args) ->
- name :: List.flatten (List.map collect_fv_from_term args)
- | A.True -> []
- | A.False -> []
- | A.Eq (t1,t2) -> collect_fv_from_term t1 @ collect_fv_from_term t2
- | A.NotEq (t1,t2) -> collect_fv_from_term t1 @ collect_fv_from_term t2
- in
- let rec aux2 = function
- | [] -> []
- | hd::tl -> aux hd @ aux2 tl
- in
- HExtlib.list_uniq (List.sort compare (aux2 a))
-;;
-
-let rec collect_fv_from_formulae = function
- | A.Disjunction (a,b) ->
- collect_fv_from_formulae a @ collect_fv_from_formulae b
- | A.NegAtom a
- | A.Atom a -> collect_fv_from_atom [a]
-;;
-
-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 rec atom_of_formula neg pos = function
- | A.Disjunction (a,b) ->
- let neg, pos = atom_of_formula neg pos a in
- atom_of_formula neg pos b
- | A.NegAtom a -> a::neg, pos
- | A.Atom (A.NotEq (a,b)) -> (A.Eq (a,b) :: neg), pos
- | A.Atom a -> neg, a::pos
-;;
-
-let atom_of_formula f =
- let neg, pos = atom_of_formula [] [] f in
- neg @ pos
-;;
-
-let rec mk_arrow component tail = function
- | 0 -> begin
- match tail with
- | Prop -> mk_ident prop
- | Univ -> mk_ident universe
- end
- | n ->
- PT.Binder
- (`Forall,
- ((mk_ident "_"),Some (mk_ident component)),
- mk_arrow component tail (n-1))
-;;
-
-let build_ctx_for_arities univesally arities t =
- let binder = if univesally then `Forall else `Exists in
- let rec aux = function
- | [] -> t
- | (name,(nargs,sort))::tl ->
- PT.Binder
- (binder,
- (mk_ident name,Some (mk_arrow universe sort nargs)),
- aux tl)
- in
- aux arities
-;;
-
-let convert_atom universally a =
- let aux = function
- | A.Proposition p -> mk_ident p
- | A.Predicate (name,params) ->
- PT.Appl ((mk_ident name) :: (List.map convert_term params))
- | A.True -> mk_ident "True"
- | A.False -> mk_ident "False"
- | A.Eq (l,r)
- | A.NotEq (l,r) -> (* removes the negation *)
- PT.Appl [mk_ident "eq";mk_ident universe;convert_term l;convert_term r]
- in
- let rec aux2 = function
- | [] -> assert false
- | [x] -> aux x
- | he::tl ->
- if universally then
- PT.Binder (`Forall, (mk_ident "_", Some (aux he)), aux2 tl)
- else
- PT.Appl [mk_ident "And";aux he;aux2 tl]
- in
- let arities = collect_arities_from_atom a in
- let fv = collect_fv_from_atom a in
- build_ctx_for_arities universally
- (List.filter
- (function (x,(0,Univ)) -> List.mem x fv | _-> false)
- arities)
- (aux2 a)
-;;
-
-let collect_arities atom ctx =
- let atoms = atom@(List.flatten (List.map atom_of_formula ctx)) in
- collect_arities_from_atom atoms
-;;
-
-let collect_arities_from_formulae f =
- let rec collect_arities_from_formulae = function
- | A.Disjunction (a,b) ->
- collect_arities_from_formulae a @ collect_arities_from_formulae b
- | A.NegAtom a
- | A.Atom a -> collect_arities_from_atom [a]
- in
- HExtlib.list_uniq (List.sort compare (collect_arities_from_formulae f))
-;;
-
-let is_formulae_1eq_negated f =
- let atom = atom_of_formula f in
- match atom with
- | [A.NotEq (l,r)] -> true
- | _ -> false
-;;
-
-let collect_fv_1stord_from_formulae f =
- let arities = collect_arities_from_formulae f in
- let fv = collect_fv_from_formulae f in
- List.map fst
- (List.filter (function (x,(0,Univ)) -> List.mem x fv | _-> false) arities)
-;;
-
-let rec convert_formula fv no_arities context f =
- let atom = atom_of_formula f in
- let t = convert_atom (fv = []) atom in
- 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 -> false
- | A.False -> true
- | A.Proposition _ -> false
- | A.Predicate _ -> false
- | A.Eq _ -> false
- | A.NotEq _ -> true
-;;
-
-let rec check_if_formula_is_negative = function
- | A.Disjunction (a,b) ->
- check_if_formula_is_negative a && check_if_formula_is_negative b
- | A.NegAtom a -> not (check_if_atom_is_negative a)
- | A.Atom a -> check_if_atom_is_negative a
-;;
-
-let ng_generate_tactics fv ueq_case context arities =
- [ GA.Executable(floc,GA.NTactic(floc,
- [GA.NIntro (floc,"Univ") ; GA.NDot(floc)])) ]
- @
- (HExtlib.list_mapi
- (fun (name,_) _->
- GA.Executable(floc,GA.NTactic(floc,
- [GA.NIntro (floc,(try List.assoc name kw with Not_found -> name));
- GA.NDot(floc)])))
- arities)
- @
- (HExtlib.list_mapi
- (fun _ i->
- GA.Executable(floc,GA.NTactic(floc,
- [GA.NIntro (floc,"H"^string_of_int i);GA.NDot(floc)])))
- context)
- @
-(if fv <> [] then
- (List.flatten
- (List.map
- (fun _ ->
- [GA.Executable(floc,GA.NTactic(floc,
- [GA.NApply (floc,
- PT.Appl
- [mk_ident "ex_intro";PT.Implicit `JustOne;PT.Implicit `JustOne;
- PT.Implicit `JustOne;PT.Implicit `JustOne]);GA.NBranch floc]));
- GA.Executable(floc,GA.NTactic(floc,
- [GA.NPos (floc,[2])]))])
- fv))
- else [])@
- [GA.Executable(floc,GA.NTactic(floc, [
- if (*ueq_case*) true then
- GA.NAuto (floc,(Some
- HExtlib.list_mapi
- (fun _ i ->
- mk_ident ("H" ^ string_of_int i))
- context
- ,[]))
- else
- GA.NAuto (floc,(None,[
- "depth",string_of_int 5;
- "width",string_of_int 5;
- "size",string_of_int 20;
- "timeout",string_of_int 10;
- ]))
- ;
- GA.NSemicolon(floc)]));
-(*
- GA.Executable(floc,GA.NTactic(floc, Some (GA.Try(floc,
- GA.Assumption floc)), GA.Dot(floc)))
-*)
- ]@
-(if fv <> [] then
- (List.flatten
- (List.map
- (fun _ ->
- [GA.Executable(floc,GA.NTactic(floc, [GA.NShift floc;
- GA.NSkip floc; GA.NMerge floc]))])
- fv))
- else [])@
- [GA.Executable(floc,GA.NTactic(floc,[GA.NTry(floc, GA.NAssumption(floc));
- GA.NSemicolon(floc)]))]@
- [GA.Executable(floc,GA.NCommand(floc, GA.NQed(floc)))]
-;;
-
-let generate_tactics fv ueq_case =
- [GA.Executable(floc,GA.Tactic(floc, Some
- (GA.Intros (floc,(None,[]))),GA.Dot(floc)))] @
-(if fv <> [] then
- (List.flatten
- (List.map
- (fun _ ->
- [GA.Executable(floc,GA.Tactic(floc, Some
- (GA.Exists floc),GA.Branch floc));
- GA.Executable(floc,GA.Tactic(floc, None,
- (GA.Pos (floc,[2]))))])
- fv))
- else [])@
- [GA.Executable(floc,GA.Tactic(floc, Some (
- if true (*ueq_case*) then
- GA.AutoBatch (floc,(None,["paramodulation","";
- "timeout",string_of_int !paramod_timeout]))
- else
- GA.AutoBatch (floc,(None,[
- "depth",string_of_int 5;
- "width",string_of_int 5;
- "size",string_of_int 20;
- "timeout",string_of_int 10;
- ]))
- ),
- GA.Semicolon(floc)));
- GA.Executable(floc,GA.Tactic(floc, Some (GA.Try(floc,
- GA.Assumption floc)), GA.Dot(floc)))
- ]@
-(if fv <> [] then
- (List.flatten
- (List.map
- (fun _ ->
- [GA.Executable(floc,GA.Tactic(floc, None, GA.Shift floc));
- GA.Executable(floc,GA.NonPunctuationTactical(floc, GA.Skip floc,
- (GA.Merge floc)))])
- fv))
- else [])@
- [GA.Executable(floc,GA.Command(floc, GA.Print(floc,"proofterm")));
- GA.Executable(floc,GA.Command(floc, GA.Qed(floc)))]
-;;
-
-let convert_ast ng statements context = function
- | A.Comment s ->
- let s = String.sub s 1 (String.length s - 1) in
- let s =
- 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 ->
- let ueq_case = is_formulae_1eq_negated f in
- let fv = collect_fv_1stord_from_formulae f in
- let old_f = f in
- let f =
- PT.Binder
- (`Forall,
- (mk_ident universe,Some (PT.Sort (`Type (CicUniv.fresh ())))),
- convert_formula fv false context f)
- in
- let o = PT.Theorem (`Theorem,name,f,None,`Regular) in
- (statements @
- [ GA.Executable(floc,GA.Command(floc,
- (*if ng then GA.NObj (floc,o) else*) GA.Obj(floc,o))); ] @
- if ng then
- ng_generate_tactics fv ueq_case context
- (let atom = atom_of_formula old_f in collect_arities atom context)
- else generate_tactics fv ueq_case),
- context
- | A.Definition
- | A.Lemma
- | 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 ?(timeout=600) ?(def_depth=10) ?raw_preamble ~tptppath ~filename ~ng () =
- paramod_timeout := timeout;
- depth := def_depth;
- let rec aux = function
- | [] -> []
- | ((A.Inclusion (file,_)) as hd) :: tl ->
- 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 ng 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 prec content_term =
- let pres_term = TermContentPres.pp_ast content_term in
- let lookup_uri = fun _ -> None in
- let markup = CicNotationPres.render ~lookup_uri ~prec pres_term in
- let s = BoxPp.render_to_string List.hd width markup ~map_unicode_to_tex:false in
- Pcre.substitute
- ~rex:(Pcre.regexp ~flags:[`UTF8] "∀[Ha-z][a-z0-9_]*") ~subst:(fun x -> "\n" ^ x)
- s
- in
- CicNotationPp.set_pp_term (term_pp 90);
- let lazy_term_pp = fun x -> assert false in
- let obj_pp = CicNotationPp.pp_obj CicNotationPp.pp_term in
- Pcre.replace ~pat:"theorem" ~templ:"ntheorem"
- (GrafiteAstPp.pp_statement
- ~map_unicode_to_tex:false ~term_pp:(term_pp 19) ~lazy_term_pp ~obj_pp t)
- in
- let buri = Pcre.replace ~pat:"\\.p$" ("cic:/matita/TPTP/" ^ filename) in
- let extra_statements_start = [
- (*GA.Executable(floc,GA.Command(floc,
- GA.Set(floc,"baseuri",buri)))*)]
- in
- let preamble =
- match raw_preamble with
- | None ->
- pp
- (GA.Executable(floc,
- GA.Command(floc,GA.Include(floc,true,`OldAndNew,"logic/equality.ma"))))
- | Some s -> s buri
- in
- let extra_statements_end = [] in
- let aliases = []
- (*[("eq","cic:/Coq/Init/Logic/eq.ind#xpointer(1/1)");
- ("trans_eq","cic:/Coq/Init/Logic/trans_eq.con");
- ("eq_ind_r","cic:/Coq/Init/Logic/eq_ind_r.con");
- ("eq_ind","cic:/Coq/Init/Logic/eq_ind.con");
- ("sym_eq","cic:/Coq/Init/Logic/sym_eq.con");
- ("refl_equal","cic:/Coq/Init/Logic/eq.ind#xpointer(1/1/1)")] *)
- in
- let s1 = List.map pp extra_statements_start in
- let s2 =
- List.map
- (fun (n,s) ->
- LexiconAstPp.pp_command (LA.Alias(floc, LA.Ident_alias(n,s))) ^ ".")
- aliases
- in
- let s3 = List.map pp grafite_ast_statements in
- let s4 = List.map pp extra_statements_end in
- String.concat "\n" (s1@[preamble]@s2@s3@s4)
-;;
+++ /dev/null
-(* Copyright (C) 2006, HELM Team.
- *
- * This file is part of HELM, an Hypertextual, Electronic
- * Library of Mathematics, developed at the Computer Science
- * Department, University of Bologna, Italy.
- *
- * HELM is free software; you can redistribute it and/or
- * modify it under the terms of the GNU General Public License
- * as published by the Free Software Foundation; either version 2
- * of the License, or (at your option) any later version.
- *
- * HELM is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
- * GNU General Public License for more details.
- *
- * You should have received a copy of the GNU General Public License
- * along with HELM; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
- * MA 02111-1307, USA.
- *
- * For details, see the HELM World-Wide-Web page,
- * http://helm.cs.unibo.it/
- *)
-
-val tptp2grafite:
- ?timeout:int ->
- ?def_depth:int ->
- ?raw_preamble:(string -> string) ->
- tptppath:string -> filename:string -> ng:bool -> unit ->
- string
+++ /dev/null
-ALG005-1
-ALG006-1
-ALG007-1
-ALG235-1
-ALG236-1
-ALG237-1
-ALG238-1
-ALG239-1
-ALG240-1
-ALG241-1
-ALG242-1
-ALG243-1
-ALG244-1
-ALG245-1
-ALG246-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-12
-COL003-13
-COL003-14
-COL003-15
-COL003-16
-COL003-17
-COL003-18
-COL003-19
-COL003-20
-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-10
-COL064-11
-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
-COM010-2
-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
-GRP661-1
-GRP662-1
-GRP663-1
-GRP666-2
-GRP666-3
-GRP666-4
-GRP666-5
-GRP667-2
-GRP667-3
-GRP667-4
-GRP667-5
-GRP668-1
-GRP669-1
-GRP670-1
-GRP671-1
-GRP675-1
-GRP676-1
-GRP677-1
-GRP678-1
-GRP679-1
-GRP680-1
-GRP681-1
-GRP684-1
-GRP686-1
-GRP687-1
-GRP688-1
-GRP689-1
-GRP690-1
-GRP691-1
-GRP692-1
-GRP693-1
-GRP694-1
-GRP695-1
-GRP696-1
-GRP697-1
-GRP698-1
-GRP699-1
-GRP701-1
-GRP705-1
-GRP706-1
-GRP707-1
-GRP708-1
-GRP709-1
-GRP712-1
-GRP713-1
-GRP714-1
-GRP716-1
-GRP717-1
-GRP718-1
-GRP719-1
-GRP720-2
-GRP721-1
-GRP722-1
-GRP723-1
-GRP724-1
-GRP725-1
-GRP726-1
-GRP727-1
-GRP728-1
-GRP729-1
-GRP730-1
-GRP731-1
-GRP732-1
-GRP735-1
-GRP736-1
-GRP737-1
-GRP738-1
-GRP739-1
-GRP740-1
-GRP741-1
-GRP742-1
-GRP743-1
-GRP744-1
-GRP749-1
-GRP750-1
-GRP751-1
-GRP752-1
-GRP753-1
-GRP754-1
-GRP756-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
-LAT389-1
-LAT390-1
-LAT391-1
-LAT392-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
-REL001-1
-REL002-1
-REL004-1
-REL004-2
-REL004-3
-REL005-1
-REL005-3
-REL006-1
-REL007-1
-REL008-1
-REL008-3
-REL010-1
-REL010-2
-REL011-1
-REL011-2
-REL012-1
-REL012-2
-REL014-1
-REL015-1
-REL016-1
-REL016-3
-REL017-1
-REL017-3
-REL018-1
-REL019-1
-REL019-2
-REL020-1
-REL020-2
-REL021-1
-REL021-2
-REL022-1
-REL022-2
-REL023-1
-REL023-2
-REL024-1
-REL024-2
-REL025-1
-REL026-1
-REL026-3
-REL027-1
-REL027-3
-REL028-1
-REL028-2
-REL029-1
-REL029-3
-REL030-1
-REL030-3
-REL031-1
-REL031-2
-REL032-1
-REL032-2
-REL033-1
-REL033-3
-REL034-1
-REL034-2
-REL035-1
-REL035-2
-REL036-1
-REL036-2
-REL037-1
-REL037-2
-REL038-1
-REL039-1
-REL040-1
-REL040-3
-REL041-1
-REL041-2
-REL042-1
-REL042-2
-REL043-1
-REL043-2
-REL044-1
-REL044-2
-REL045-1
-REL045-2
-REL047-1
-REL049-1
-REL050-1
-REL050-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
-SWV243-2
-SWV262-2
-SYN080-1
-SYN083-1
-SYN305-1
-SYN552-1
\ No newline at end of file
projects / helm.git / commitdiff