1 /* Copyright (C) 2000, HELM Team.
3 * This file is part of HELM, an Hypertextual, Electronic
4 * Library of Mathematics, developed at the Computer Science
5 * Department, University of Bologna, Italy.
7 * HELM is free software; you can redistribute it and/or
8 * modify it under the terms of the GNU General Public License
9 * as published by the Free Software Foundation; either version 2
10 * of the License, or (at your option) any later version.
12 * HELM is distributed in the hope that it will be useful,
13 * but WITHOUT ANY WARRANTY; without even the implied warranty of
14 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
15 * GNU General Public License for more details.
17 * You should have received a copy of the GNU General Public License
18 * along with HELM; if not, write to the Free Software
19 * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
22 * For details, see the HELM World-Wide-Web page,
23 * http://cs.unibo.it/helm/.
29 let out t s = () (* prerr_endline ("-- " ^ t ^ " " ^ s) *)
31 let trim = HExtlib.trim_blanks
35 let cat x = String.concat " " x
38 let map ident = T.Inline (T.Var, trim ident) in
42 String.sub s 1 (String.length s - 2)
45 String.sub s 1 (String.length s - 1)
48 [T.Coercion (false, str); T.Coercion (true, str)]
51 [T.Notation (false, str); T.Notation (true, str)]
53 %token <string> SPC STR IDENT INT EXTRA AC OP CP OC CC OQ CQ DEF FS COE CN SC
54 %token <string> LET IN TH PROOF QED VAR IND SEC REQ XP IP SET NOT LOAD ID COERC
58 %type <Types.items> items
61 | OQ verbatims CQ { $1 ^ $2 ^ $3 }
69 | spc spcs { $1 ^ $2 }
73 | SPC rspcs { $1 ^ $2 }
75 fs: FS spcs { $1 ^ $2 };
76 ident: IDENT spcs { $1 ^ $2 };
77 th: TH spcs { $1 ^ $2 };
78 proof: PROOF spcs { $1 ^ $2 };
79 qed: QED spcs { $1 ^ $2 };
80 sec: SEC spcs { $1 ^ $2 };
81 def: DEF spcs { $1 ^ $2 };
82 op: OP spcs { $1 ^ $2 };
83 xlet: LET spcs { $1 ^ $2 };
84 var: VAR spcs { $1 ^ $2 };
85 req: REQ spcs { $1 ^ $2 };
86 load: LOAD spcs { $1 ^ $2 };
87 xp: XP spcs { $1 ^ $2 };
88 ip: IP spcs { $1 ^ $2 };
89 ind: IND spcs { $1 ^ $2 };
90 set: SET spcs { $1 ^ $2 };
91 notation: NOT spcs { $1 ^ $2 };
92 oc: OC spcs { $1 ^ $2 };
93 coe: COE spcs { $1 ^ $2 };
94 cn: CN spcs { $1 ^ $2 };
95 sc: SC spcs { $1 ^ $2 };
96 str: STR spcs { $1 ^ $2 };
97 id: ID spcs { $1 ^ $2 };
98 coerc: COERC spcs { $1 ^ $2 };
102 | ident idents { $1 :: $2 }
110 | cnot spcs { $1 ^ $2 }
111 | cnot spcs cnots { $1 ^ $2 ^ $3 }
124 | xlet extends0 IN { $1 ^ $2 ^ $3 }
125 | op extends1 CP { $1 ^ $2 ^ $3 }
145 | restrict spcs { $1 ^ $2 }
146 | restrict spcs restricts { $1 ^ $2 ^ $3 }
149 | xre spcs { $1 ^ $2 }
150 | xre spcs restricts { $1 ^ $2 ^ $3 }
157 | extend0 spcs { $1 ^ $2 }
158 | extend0 spcs extends0 { $1 ^ $2 ^ $3 }
166 | extend1 spcs { $1 ^ $2 }
167 | extend1 spcs extends1 { $1 ^ $2 ^ $3 }
189 | unexport_rr { $1, [] }
190 | oc fields CC { $1 ^ fst $2 ^ $3, snd $2 }
193 | unexport_r spcs { fst $1 ^ $2, snd $1 }
194 | unexport_r spcs unexports_r { fst $1 ^ $2 ^ fst $3, snd $1 @ snd $3 }
197 | ident cn unexports_r
198 { $1 ^ $2 ^ fst $3, snd $3 }
199 | ident coe unexports_r
200 { $1 ^ $2 ^ fst $3, snd $3 @ coercion (trim $1) }
204 | field sc fields { fst $1 ^ $2 ^ fst $3, snd $1 @ snd $3 }
206 | error { out "ERROR" "fields"; failwith "fields" }
214 | unexport spcs { fst $1 ^ $2, snd $1 }
215 | unexport spcs unexports { fst $1 ^ $2 ^ fst $3, snd $1 @ snd $3 }
236 | verbatim verbatims { $1 ^ $2 }
240 | restricts FS { [] }
244 | step spcs steps { $1 @ $3 }
249 | qid AC { strip1 $2 :: $1 }
253 | th ident restricts fs proof FS steps qed FS
254 { out "TH" $2; $7 @ [T.Inline (T.Con, trim $2)] }
255 | th ident restricts fs proof restricts FS
256 { out "TH" $2; [T.Inline (T.Con, trim $2)] }
257 | th ident restricts fs steps qed FS
258 { out "TH" $2; $5 @ [T.Inline (T.Con, trim $2)] }
259 | th ident restricts def restricts FS
260 { out "TH" $2; [T.Inline (T.Con, trim $2)] }
261 | th ident def restricts FS
262 { out "TH" $2; [T.Inline (T.Con, trim $2)] }
264 { out "VAR" (cat $2); mk_vars $2 }
265 | ind ident unexports FS
266 { out "IND" $2; T.Inline (T.Ind, trim $2) :: snd $3 }
268 { out "UNX" (fst $2); [T.Unexport ($1 ^ fst $2 ^ trim $3)] }
270 { out "REQ" $3; [T.Include (trim $3)] }
272 { out "REQ" $3; [T.Include (trim $3)] }
274 { out "REQ" $2; [T.Include (trim $2)] }
276 { out "REQ" $2; [T.Include (strip2 (trim $2))] }
277 | coerc qid spcs cn unexports FS
278 { out "COERCE" (hd $2); coercion (hd $2) }
279 | id coerc qid spcs cn unexports FS
280 { out "COERCE" (hd $3); coercion (hd $3) }
282 { out "ERROR" $2; failwith ("macro_step " ^ $2) }
284 { out "ERROR" $2; failwith ("macro_step " ^ $2) }
287 out "ERROR" vs; failwith ("macro_step " ^ vs) }
290 | OQ verbatims CQ { [T.Comment $2] }
292 | set unexports FS { [T.Unexport ($1 ^ fst $2 ^ trim $3)] }
293 | notation unexports FS { notation ($1 ^ fst $2 ^ trim $3) }
294 | error { out "ERROR" "item"; failwith "item" }
298 | rspcs item items { $2 @ $3 }