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
37 let mk_vars local idents =
38 let map ident = T.Inline (local, 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> ABBR IN LET TH PROOF QED VAR AX IND SEC END UNX 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 }
93 fs: FS spcs { $1 ^ $2 };
94 ident: xident spcs { $1 ^ $2 };
95 th: TH spcs { $1 ^ $2 };
96 xlet: LET spcs { $1 ^ $2 };
97 proof: PROOF spcs { $1 ^ $2 };
98 qed: QED spcs { $1 ^ $2 };
99 sec: SEC spcs { $1 ^ $2 };
100 xend: END spcs { $1 ^ $2 };
101 unx: UNX spcs { $1 ^ $2 };
102 def: DEF spcs { $1 ^ $2 };
103 op: OP spcs { $1 ^ $2 };
104 abbr: ABBR spcs { $1 ^ $2 };
105 var: VAR spcs { $1 ^ $2 };
106 ax: AX spcs { $1 ^ $2 };
107 req: REQ spcs { $1 ^ $2 };
108 load: LOAD spcs { $1 ^ $2 };
109 xp: XP spcs { $1 ^ $2 };
110 ip: IP spcs { $1 ^ $2 };
111 ind: IND spcs { $1 ^ $2 };
112 set: SET spcs { $1 ^ $2 };
113 notation: NOT spcs { $1 ^ $2 };
114 oc: OC spcs { $1 ^ $2 };
115 coe: COE spcs { $1 ^ $2 };
116 cn: CN spcs { $1 ^ $2 };
117 sc: SC spcs { $1 ^ $2 };
118 str: STR spcs { $1 ^ $2 };
119 id: ID spcs { $1 ^ $2 };
120 coerc: COERC spcs { $1 ^ $2 };
124 | ident idents { $1 :: $2 }
132 | cnot spcs { $1 ^ $2 }
133 | cnot spcs cnots { $1 ^ $2 ^ $3 }
146 | abbr extends0 IN { $1 ^ $2 ^ $3 }
147 | op extends1 CP { $1 ^ $2 ^ $3 }
167 | restrict spcs { $1 ^ $2 }
168 | restrict spcs restricts { $1 ^ $2 ^ $3 }
171 | xre spcs { $1 ^ $2 }
172 | xre spcs restricts { $1 ^ $2 ^ $3 }
179 | extend0 spcs { $1 ^ $2 }
180 | extend0 spcs extends0 { $1 ^ $2 ^ $3 }
188 | extend1 spcs { $1 ^ $2 }
189 | extend1 spcs extends1 { $1 ^ $2 ^ $3 }
211 | unexport_rr { $1, [] }
212 | oc fields CC { $1 ^ fst $2 ^ $3, snd $2 }
215 | unexport_r spcs { fst $1 ^ $2, snd $1 }
216 | unexport_r spcs unexports_r { fst $1 ^ $2 ^ fst $3, snd $1 @ snd $3 }
219 | ident cn unexports_r
220 { $1 ^ $2 ^ fst $3, snd $3 }
221 | ident coe unexports_r
222 { $1 ^ $2 ^ fst $3, snd $3 @ coercion (trim $1) }
226 | field sc fields { fst $1 ^ $2 ^ fst $3, snd $1 @ snd $3 }
228 | error { out "ERROR" "fields"; failwith "fields" }
236 | unexport spcs { fst $1 ^ $2, snd $1 }
237 | unexport spcs unexports { fst $1 ^ $2 ^ fst $3, snd $1 @ snd $3 }
262 | verbatim verbatims { $1 ^ $2 }
266 | restricts FS { [] }
270 | step spcs steps { $1 @ $3 }
275 | qid AC { strip1 $2 :: $1 }
279 | th ident restricts fs proof FS steps qed FS
280 { out "TH" $2; $7 @ [T.Inline (false, T.Con, trim $2, "")] }
281 | th ident restricts fs proof restricts FS
282 { out "TH" $2; [T.Inline (false, T.Con, trim $2, "")] }
283 | th ident restricts fs steps qed FS
284 { out "TH" $2; $5 @ [T.Inline (false, T.Con, trim $2, "")] }
285 | th ident restricts def restricts FS
286 { out "TH" $2; [T.Inline (false, T.Con, trim $2, "")] }
287 | th ident def restricts FS
288 { out "TH" $2; [T.Inline (false, T.Con, trim $2, "")] }
289 | xlet ident restricts fs proof FS steps qed FS
290 { out "LET" $2; $7 @ [T.Inline (true, T.Con, trim $2, "")] }
291 | xlet ident restricts fs proof restricts FS
292 { out "LET" $2; [T.Inline (true, T.Con, trim $2, "")] }
293 | xlet ident restricts fs steps qed FS
294 { out "LET" $2; $5 @ [T.Inline (true, T.Con, trim $2, "")] }
295 | xlet ident restricts def restricts FS
296 { out "LET" $2; [T.Inline (true, T.Con, trim $2, "")] }
297 | xlet ident def restricts FS
298 { out "LET" $2; [T.Inline (true, T.Con, trim $2, "")] }
300 { out "VAR" (cat $2); mk_vars true $2 }
302 { out "AX" (cat $2); mk_vars false $2 }
303 | ind ident unexports FS
304 { out "IND" $2; T.Inline (false, T.Ind, trim $2, "") :: snd $3 }
306 { out "SEC" $2; [T.Section (true, trim $2, $1 ^ $2)] }
308 { out "END" $2; [T.Section (false, trim $2, $1 ^ $2)] }
310 { out "UNX" (fst $2); [T.Unexport ($1 ^ fst $2 ^ trim $3)] }
312 { out "REQ" $3; [T.Include (trim $3)] }
314 { out "REQ" $3; [T.Include (trim $3)] }
316 { out "REQ" $2; [T.Include (trim $2)] }
318 { out "REQ" $2; [T.Include (strip2 (trim $2))] }
319 | coerc qid spcs cn unexports FS
320 { out "COERCE" (hd $2); coercion (hd $2) }
321 | id coerc qid spcs cn unexports FS
322 { out "COERCE" (hd $3); coercion (hd $3) }
324 { out "ERROR" $2; failwith ("macro_step " ^ $2) }
326 { out "ERROR" $2; failwith ("macro_step " ^ $2) }
329 out "ERROR" vs; failwith ("macro_step " ^ vs) }
332 out "ERROR" vs; failwith ("macro_step " ^ vs) }
335 | OQ verbatims CQ { [T.Comment $2] }
337 | set unexports FS { [T.Unexport ($1 ^ fst $2 ^ trim $3)] }
338 | notation unexports FS { notation ($1 ^ fst $2 ^ trim $3) }
339 | error { out "ERROR" "item"; failwith "item" }
343 | rspcs item items { $2 @ $3 }