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 let reserved = [
  12   "in","In";
  13   "to","To";
  14   "theorem","Theorem";
  15 ];;
  16
  17 let unreserve k =
  18   try List.assoc k reserved with Not_found -> k
  19 ;;
  20
  21
  22 %}
  23   %token <string> TYPE
  24   %token <string> COMMENT
  25   %token <int> NUM
  26   %token <string> LNAME
  27   %token <string> UNAME
  28   %token <string> QSTRING
  29   %token COMMA
  30   %token INCLUSION
  31   %token LPAREN
  32   %token RPAREN
  33   %token CNF
  34   %token TRUE
  35   %token FALSE
  36   %token NOT
  37   %token IAND
  38   %token IOR
  39   %token NIEQ
  40   %token IEQ
  41   %token XOR
  42   %token IMPLY
  43   %token IMPLYLR
  44   %token COIMPLY
  45   %token PEQ
  46   %token DOT
  47   %token EOF
  48   %token FORALL
  49   %token EXISTS
  50   %token LAMBDA
  51   %token COLON
  52   %token BEGINVARLIST
  53   %token ENDVARLIST
  54   %token APPLY
  55   %token TYPE_I
  56   %token TYPE_O
  57   %token TYPE_U
  58   %token TO
  59   %token THF
  60
  61   %left IOR
  62   %left IAND
  63   %nonassoc NOT
  64   %right TO
  65   %left APPLY
  66
  67   %type <AstTHF.ast list> main
  68   %start main
  69 %%
  70   main:
  71     | tptp_input EOF {[$1]}
  72     | tptp_input main {$1::$2}
  73     | error {
  74         let start_pos = rhs_start_pos 1 in
  75                                 let end_pos = rhs_end_pos 1 in
  76                                 Printf.eprintf "from line %d char %d to line %d char %d\n"
  77           start_pos.pos_lnum (start_pos.pos_cnum - start_pos.pos_bol)
  78           end_pos.pos_lnum (end_pos.pos_cnum - end_pos.pos_bol);
  79         exit 1
  80        }
  81   ;
  82
  83   tptp_input:
  84     | annot_formula {$1}
  85     | include_ {$1}
  86     | comment {$1}
  87   ;
  88
  89   formula_source_and_infos:
  90     | { () }
  91     | COMMA { assert false }
  92   ;
  93
  94   annot_formula:
  95     | THF LPAREN name COMMA formula_type COMMA
  96       term formula_source_and_infos RPAREN DOT {
  97          match $5 with
  98          | Definition ->
  99              (match $7 with
 100              | T.Appl [T.Symbol("Eq",_);T.Ident(name,_);body] ->
 101                    ThfDefinition($3,unreserve name,body)
 102              | _ -> prerr_endline ("near " ^ $3); assert false)
 103          | Type ->
 104              (match $7 with
 105              | T.Cast (T.Ident(name,_),ty) -> ThfType($3,unreserve name,ty)
 106              | _ -> assert false)
 107          | _ -> ThfFormula($3,$5,$7)
 108       }
 109   ;
 110
 111   formula_type:
 112     | TYPE {
 113         match $1 with
 114         | "axiom" -> Axiom
 115         | "hypothesis" -> Hypothesis
 116         | "definition" -> Definition
 117         | "lemma" -> Lemma
 118         | "theorem" -> Theorem
 119         | "conjecture" -> Conjecture
 120         | "lemma_conjecture" -> Lemma_conjecture
 121         | "negated_conjecture" -> Negated_conjecture
 122         | "plain" -> Plain
 123         | "unknown" -> Unknown
 124         | "type" -> Type
 125         | _ -> assert false
 126       }
 127   ;
 128
 129   quantifier :
 130     | FORALL {`Forall}
 131     | EXISTS {`Exists}
 132     | LAMBDA {`Lambda}
 133
 134   vardecl :
 135     | UNAME { T.Ident($1,None), None }
 136     | UNAME COLON term { T.Ident($1,None),Some $3 }
 137
 138   varlist :
 139     | vardecl { [$1] }
 140     | vardecl COMMA varlist { $1 :: $3 }
 141
 142   term:
 143     | quantifier BEGINVARLIST varlist ENDVARLIST COLON term {
 144         List.fold_right (fun v t -> T.Binder($1,v,t)) $3 $6
 145         }
 146     | term APPLY term {
 147         match $1 with
 148         | T.Appl l -> T.Appl (l @ [$3])
 149         | x -> T.Appl ([$1; $3])
 150     }
 151     | LPAREN term COLON term RPAREN { T.Cast ($2,$4) }
 152     | term TO term { T.Binder (`Forall,(T.Ident("_",None),Some $1),$3) }
 153     | term IMPLY term { T.Binder (`Forall,(T.Ident("_",None),Some $1),$3) }
 154     | term IMPLYLR term { T.Binder (`Forall,(T.Ident("_",None),Some $3),$1) }
 155     | term COIMPLY term { T.Appl [T.Symbol("Iff",0);$1;$3] }
 156     | term XOR term { T.Appl [T.Symbol("Xor",0);$1;$3] }
 157     | term IEQ term { T.Appl [T.Symbol("Eq",0);$1;$3] }
 158     | term NIEQ term { T.Appl [T.Symbol("NotEq",0);$1;$3] }
 159     | term IAND term { T.Appl [T.Symbol("And",0);$1;$3] }
 160     | term IOR term { T.Appl [T.Symbol("Or",0);$1;$3] }
 161     | NOT term { T.Appl [T.Symbol("Not",0);$2] }
 162     | LPAREN term RPAREN {$2}
 163     | LNAME { T.Ident(unreserve $1,None) }
 164     | UNAME { T.Ident($1,None) }
 165     | TYPE_I { T.Symbol("i",0) }
 166     | TYPE_O { T.Symbol("o",0) }
 167     | TYPE_U { T.Sort (`NType "0") }
 168     | FALSE { T.Symbol("False",0)}
 169     | TRUE { T.Symbol("True",0)}
 170   ;
 171
 172   include_:
 173     | INCLUSION LPAREN QSTRING selection_of_formulae RPAREN DOT {
 174         let fname = rm_q $3 in
 175         Inclusion (fname,$4)
 176     }
 177   ;
 178
 179   selection_of_formulae:
 180     | { [] }
 181     | COMMA name selection_of_formulae { $2::$3 }
 182   ;
 183
 184   comment: COMMENT {Comment $1} ;
 185
 186   name: NUM { string_of_int $1} | LNAME { $1 } | UNAME { $1 } ;
 187 %%
 188   (* trailer *)