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 (file)
index 0000000..ad3557b
--- /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 (file)
index 0000000..b8f855d
--- /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 (file)
index 0000000..273d1b7
--- /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 (file)
index 0000000..97c4b30
--- /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 (file)
index 0000000..7d1c643
--- /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 <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 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 *)