helm/software/components/tptp_grafite/parser.mly

   1 %{
   2   (* header *)
   3   open Ast
   4   open Parsing
   5   open Lexing
   6
   7   let parse_error s = Printf.eprintf "%s: " s ;;
   8   let rm_q s = String.sub s 1 (String.length s - 2) ;;
   9
  10 %}
  11   %token <string> TYPE
  12   %token <string> COMMENT
  13   %token <int> NUM
  14   %token <string> LNAME
  15   %token <string> UNAME
  16   %token <string> QSTRING
  17   %token COMMA
  18   %token INCLUSION
  19   %token LPAREN
  20   %token RPAREN
  21   %token CNF
  22   %token TRUE
  23   %token FALSE
  24   %token IOR
  25   %token NOT
  26   %token NIEQ
  27   %token IEQ
  28   %token PEQ
  29   %token DOT
  30   %token EOF
  31
  32   %type <Ast.ast list> main
  33   %start main
  34 %%
  35   main:
  36     | tptp_input EOF {[$1]}
  37     | tptp_input main {$1::$2}
  38     | error {
  39         let start_pos = rhs_start_pos 1 in
  40                                 let end_pos = rhs_end_pos 1 in
  41                                 Printf.eprintf "from line %d char %d to line %d char %d\n"
  42           start_pos.pos_lnum (start_pos.pos_cnum - start_pos.pos_bol)
  43           end_pos.pos_lnum (end_pos.pos_cnum - end_pos.pos_bol);
  44         exit 1
  45        }
  46   ;
  47
  48   tptp_input:
  49     | annot_formula {$1}
  50     | include_ {$1}
  51     | comment {$1}
  52   ;
  53
  54   annot_formula:
  55     | CNF LPAREN
  56             name COMMA formula_type COMMA formula formula_source_and_infos
  57           RPAREN DOT {
  58             AnnotatedFormula ($3,$5,$7,fst $8,snd $8)
  59       }
  60   ;
  61
  62   formula_type:
  63     | TYPE {
  64         match $1 with
  65         | "axiom" -> Axiom
  66         | "hypothesis" -> Hypothesis
  67         | "definition" -> Definition
  68         | "lemma" -> Lemma
  69         | "theorem" -> Theorem
  70         | "conjecture" -> Conjecture
  71         | "lemma_conjecture" -> Lemma_conjecture
  72         | "negated_conjecture" -> Negated_conjecture
  73         | "plain" -> Plain
  74         | "unknown" -> Unknown
  75         | _ -> assert false
  76       }
  77   ;
  78
  79   formula:
  80     | LPAREN disjunction RPAREN {$2}
  81     | disjunction {$1}
  82   ;
  83
  84   disjunction:
  85     | literal {$1}
  86     | literal IOR disjunction {
  87         Disjunction ($1,$3)
  88       }
  89   ;
  90
  91   literal:
  92     | NOT atom { NegAtom $2 }
  93     | atom { Atom $1 }
  94   ;
  95
  96   atom:
  97     | atomic_word LPAREN term_list RPAREN { Predicate ($1,$3) }
  98     | atomic_word { Proposition $1 }
  99     | TRUE { True }
 100     | FALSE { False }
 101     | term IEQ term { Eq ($1,$3) }
 102     | term NIEQ term { NotEq ($1,$3) }
 103     | PEQ LPAREN term COMMA term RPAREN { Eq ($3,$5) }
 104   ;
 105
 106   term_list:
 107     | term { [$1] }
 108     | term COMMA term_list { $1 :: $3 }
 109   ;
 110
 111   term:
 112     | upper_word { Variable $1 }
 113     | atomic_word LPAREN term_list RPAREN { Function ($1,$3) }
 114     | atomic_word { Constant $1 }
 115   ;
 116
 117   upper_word: UNAME { $1 } ;
 118
 119   atomic_word:
 120     | LNAME { $1 }
 121     | QSTRING { rm_q $1 }
 122     | TYPE { (* workaround! *)
 123       match $1 with
 124       | "theorem" -> "theoremP"
 125       | "axiom" -> "axiomP"
 126       | s -> prerr_endline s;assert false }
 127   ;
 128
 129   formula_source_and_infos:
 130         | { NoSource, [NoInfo] }
 131     | COMMA { assert false }
 132   ;
 133
 134   include_:
 135     | INCLUSION LPAREN QSTRING selection_of_formulae RPAREN DOT {
 136         let fname = rm_q $3 in
 137         Inclusion (fname,$4)
 138     }
 139   ;
 140
 141   selection_of_formulae:
 142     | { [] }
 143     | COMMA name selection_of_formulae { $2::$3 }
 144   ;
 145
 146   comment: COMMENT {Comment $1} ;
 147
 148   name: NUM { string_of_int $1} | LNAME { $1 } | UNAME { $1 } ;
 149 %%
 150   (* trailer *)