]> matita.cs.unibo.it Git - helm.git/blob - helm/software/components/tptp_grafite/parser.mly
ncopy partially implemented and fixed (a ?) chain to print elimintaors
[helm.git] / 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 *)