helm/software/components/tptp_grafite/parserTHF.mly

   1 %{
   2   (* header *)
   3   open AstTHF
   4   open Parsing
   5   open Lexing
   6   module T = CicNotationPt
   7
   8   let parse_error s = Printf.eprintf "%s: " s ;;
   9   let rm_q s = String.sub s 1 (String.length s - 2) ;;
  10
  11 %}
  12   %token <string> TYPE
  13   %token <string> COMMENT
  14   %token <int> NUM
  15   %token <string> LNAME
  16   %token <string> UNAME
  17   %token <string> QSTRING
  18   %token COMMA
  19   %token INCLUSION
  20   %token LPAREN
  21   %token RPAREN
  22   %token CNF
  23   %token TRUE
  24   %token FALSE
  25   %token NOT
  26   %token IAND
  27   %token IOR
  28   %token NIEQ
  29   %token IEQ
  30   %token IMPLY
  31   %token PEQ
  32   %token DOT
  33   %token EOF
  34   %token FORALL
  35   %token EXISTS
  36   %token LAMBDA
  37   %token COLON
  38   %token BEGINVARLIST
  39   %token ENDVARLIST
  40   %token APPLY
  41   %token TYPE_I
  42   %token TYPE_O
  43   %token TYPE_U
  44   %token TO
  45   %token THF
  46
  47   %left IOR
  48   %left IAND
  49   %nonassoc NOT
  50   %right TO
  51   %left APPLY
  52
  53   %type <AstTHF.ast list> main
  54   %start main
  55 %%
  56   main:
  57     | tptp_input EOF {[$1]}
  58     | tptp_input main {$1::$2}
  59     | error {
  60         let start_pos = rhs_start_pos 1 in
  61                                 let end_pos = rhs_end_pos 1 in
  62                                 Printf.eprintf "from line %d char %d to line %d char %d\n"
  63           start_pos.pos_lnum (start_pos.pos_cnum - start_pos.pos_bol)
  64           end_pos.pos_lnum (end_pos.pos_cnum - end_pos.pos_bol);
  65         exit 1
  66        }
  67   ;
  68
  69   tptp_input:
  70     | annot_formula {$1}
  71     | include_ {$1}
  72     | comment {$1}
  73   ;
  74
  75   formula_source_and_infos:
  76     | { () }
  77     | COMMA { assert false }
  78   ;
  79
  80   annot_formula:
  81     | THF LPAREN
  82             name COMMA formula_type COMMA term formula_source_and_infos
  83           RPAREN DOT {
  84             Formula($3,$5,$7)
  85       }
  86   ;
  87
  88   formula_type:
  89     | TYPE {
  90         match $1 with
  91         | "axiom" -> Axiom
  92         | "hypothesis" -> Hypothesis
  93         | "definition" -> Definition
  94         | "lemma" -> Lemma
  95         | "theorem" -> Theorem
  96         | "conjecture" -> Conjecture
  97         | "lemma_conjecture" -> Lemma_conjecture
  98         | "negated_conjecture" -> Negated_conjecture
  99         | "plain" -> Plain
 100         | "unknown" -> Unknown
 101         | "type" -> Type
 102         | _ -> assert false
 103       }
 104   ;
 105
 106   quantifier :
 107     | FORALL {`Forall}
 108     | EXISTS {`Exists}
 109     | LAMBDA {`Lambda}
 110
 111   vardecl :
 112     | UNAME { T.Implicit `JustOne,Some (T.Ident($1,None)) }
 113     | UNAME COLON term { $3,Some (T.Ident($1,None)) }
 114
 115   varlist :
 116     | vardecl { [$1] }
 117     | vardecl COMMA varlist { $1 :: $3 }
 118
 119   term:
 120     | quantifier BEGINVARLIST varlist ENDVARLIST COLON term {
 121         List.fold_right (fun v t -> T.Binder($1,v,t)) $3 $6
 122         }
 123     | term IMPLY term {
 124         match $1 with
 125         | T.Appl l -> T.Appl (l @ [$3])
 126         | x -> T.Appl ([$1; $3])
 127     }
 128     | term APPLY term {
 129         match $1 with
 130         | T.Appl l -> T.Appl (l @ [$3])
 131         | x -> T.Appl ([$1; $3])
 132     }
 133     | LPAREN term COLON term RPAREN { T.Cast ($2,$4) }
 134     | term TO term { T.Binder (`Pi,($1,None),$3) }
 135     | term IEQ term { T.Appl [T.Symbol("'eq",0);$1;$3] }
 136     | term IAND term { T.Appl [T.Symbol("'and",0);$1;$3] }
 137     | term IOR term { T.Appl [T.Symbol("'or",0);$1;$3] }
 138     | NOT term { T.Appl [T.Symbol("'not",0);$2] }
 139     | LPAREN term RPAREN {$2}
 140     | LNAME { T.Ident($1,None) }
 141     | UNAME { T.Ident($1,None) }
 142     | TYPE_I { T.Symbol("'i",0) }
 143     | TYPE_O { T.Symbol("'o",0) }
 144     | TYPE_U { T.Sort `Set }
 145     | FALSE { T.Symbol("'false",0)}
 146     | TRUE { T.Symbol("'true",0)}
 147   ;
 148
 149   include_:
 150     | INCLUSION LPAREN QSTRING selection_of_formulae RPAREN DOT {
 151         let fname = rm_q $3 in
 152         Inclusion (fname,$4)
 153     }
 154   ;
 155
 156   selection_of_formulae:
 157     | { [] }
 158     | COMMA name selection_of_formulae { $2::$3 }
 159   ;
 160
 161   comment: COMMENT {Comment $1} ;
 162
 163   name: NUM { string_of_int $1} | LNAME { $1 } | UNAME { $1 } ;
 164 %%
 165   (* trailer *)