From: Enrico Tassi Date: Fri, 12 May 2006 15:15:29 +0000 (+0000) Subject: added parser (and future converter) of tptp files X-Git-Tag: make_still_working~7380 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=bf079bd9d7313b95c9892202290a1572399b0d4c;p=helm.git added parser (and future converter) of tptp files --- diff --git a/helm/software/components/binaries/tptp2grafite/Makefile b/helm/software/components/binaries/tptp2grafite/Makefile new file mode 100644 index 000000000..ad3557b7a --- /dev/null +++ b/helm/software/components/binaries/tptp2grafite/Makefile @@ -0,0 +1,14 @@ +all: tptp2grafite + +tptp2grafite: + 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 -o tptp2grafite ast.cmo lexer.cmo parser.cmo main.cmo + +clean: + rm -r tptp2grafite *.cmo *.cmi parser.mli parser.ml lexer.ml diff --git a/helm/software/components/binaries/tptp2grafite/ast.ml b/helm/software/components/binaries/tptp2grafite/ast.ml new file mode 100644 index 000000000..b8f855dd1 --- /dev/null +++ b/helm/software/components/binaries/tptp2grafite/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/helm/software/components/binaries/tptp2grafite/lexer.mll b/helm/software/components/binaries/tptp2grafite/lexer.mll new file mode 100644 index 000000000..273d1b79b --- /dev/null +++ b/helm/software/components/binaries/tptp2grafite/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/helm/software/components/binaries/tptp2grafite/main.ml b/helm/software/components/binaries/tptp2grafite/main.ml new file mode 100644 index 000000000..97c4b3014 --- /dev/null +++ b/helm/software/components/binaries/tptp2grafite/main.ml @@ -0,0 +1,4 @@ +let _ = + let lexbuf = Lexing.from_channel stdin in + let _ = Parser.main Lexer.yylex lexbuf in + exit 0 diff --git a/helm/software/components/binaries/tptp2grafite/parser.mly b/helm/software/components/binaries/tptp2grafite/parser.mly new file mode 100644 index 000000000..7d1c64336 --- /dev/null +++ b/helm/software/components/binaries/tptp2grafite/parser.mly @@ -0,0 +1,150 @@ +%{ + (* 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 formula_infos + RPAREN DOT { + AnnotatedFormula ($3,$5,$7,$8,$9) + } + ; + + 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: + | { NoSource } + | COMMA { assert false } + ; + + formula_infos: + | { [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 *)