THF parser for TPTP

[helm.git] / helm / software / components / tptp_grafite / parserTHF.mly

diff --git a/helm/software/components/tptp_grafite/parserTHF.mly b/helm/software/components/tptp_grafite/parserTHF.mly
new file mode 100644 (file)
index 0000000..35bc870
--- /dev/null
+++ b/helm/software/components/tptp_grafite/parserTHF.mly
@@ -0,0 +1,165 @@
+%{
+  (* 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) ;;
+  
+%}
+  %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 IMPLY
+  %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 {
+            Formula($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.Implicit `JustOne,Some (T.Ident($1,None)) }
+    | UNAME COLON term { $3,Some (T.Ident($1,None)) }
+   
+  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 IMPLY term { 
+        match $1 with 
+        | T.Appl l -> T.Appl (l @ [$3])
+        | x -> T.Appl ([$1; $3]) 
+    }
+    | 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 (`Pi,($1,None),$3) }
+    | term IEQ term { T.Appl [T.Symbol("'eq",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($1,None) }
+    | UNAME { T.Ident($1,None) }
+    | TYPE_I { T.Symbol("'i",0) }
+    | TYPE_O { T.Symbol("'o",0) }
+    | TYPE_U { T.Sort `Set }
+    | 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 *)