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