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     | CNF LPAREN
  61           TYPE COMMA formula_type COMMA formula formula_source_and_infos
  62         RPAREN DOT {
  63           AnnotatedFormula ($3,$5,$7,fst $8,snd $8)
  64         }
  65   ;
  66
  67   formula_type:
  68     | TYPE {
  69         match $1 with
  70         | "axiom" -> Axiom
  71         | "hypothesis" -> Hypothesis
  72         | "definition" -> Definition
  73         | "lemma" -> Lemma
  74         | "theorem" -> Theorem
  75         | "conjecture" -> Conjecture
  76         | "lemma_conjecture" -> Lemma_conjecture
  77         | "negated_conjecture" -> Negated_conjecture
  78         | "plain" -> Plain
  79         | "unknown" -> Unknown
  80         | _ -> assert false
  81       }
  82   ;
  83
  84   formula:
  85     | LPAREN disjunction RPAREN {$2}
  86     | disjunction {$1}
  87   ;
  88
  89   disjunction:
  90     | literal {$1}
  91     | literal IOR disjunction {
  92         Disjunction ($1,$3)
  93       }
  94   ;
  95
  96   literal:
  97     | NOT atom { NegAtom $2 }
  98     | atom { Atom $1 }
  99   ;
 100
 101   atom:
 102     | atomic_word LPAREN term_list RPAREN { Predicate ($1,$3) }
 103     | atomic_word { Proposition $1 }
 104     | TRUE { True }
 105     | FALSE { False }
 106     | term IEQ term { Eq ($1,$3) }
 107     | term NIEQ term { NotEq ($1,$3) }
 108     | PEQ LPAREN term COMMA term RPAREN { Eq ($3,$5) }
 109   ;
 110
 111   term_list:
 112     | term { [$1] }
 113     | term COMMA term_list { $1 :: $3 }
 114   ;
 115
 116   term:
 117     | upper_word { Variable $1 }
 118     | atomic_word LPAREN term_list RPAREN { Function ($1,$3) }
 119     | atomic_word { Constant $1 }
 120   ;
 121
 122   upper_word: UNAME { $1 } ;
 123
 124   atomic_word:
 125     | LNAME { $1 }
 126     | QSTRING { rm_q $1 }
 127     | TYPE { (* workaround! *)
 128       match $1 with
 129       | "theorem" -> "theoremP"
 130       | "axiom" -> "axiomP"
 131       | s -> prerr_endline s;assert false }
 132   ;
 133
 134   formula_source_and_infos:
 135         | { NoSource, [NoInfo] }
 136     | COMMA { assert false }
 137   ;
 138
 139   include_:
 140     | INCLUSION LPAREN QSTRING selection_of_formulae RPAREN DOT {
 141         let fname = rm_q $3 in
 142         Inclusion (fname,$4)
 143     }
 144   ;
 145
 146   selection_of_formulae:
 147     | { [] }
 148     | COMMA name selection_of_formulae { $2::$3 }
 149   ;
 150
 151   comment: COMMENT {Comment $1} ;
 152
 153   name: NUM { string_of_int $1} | LNAME { $1 } | UNAME { $1 } ;
 154 %%
 155   (* trailer *)