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 cat x = String.concat " " x
34 let map ident = T.Inline (T.Var, ident) in
38 String.sub s 1 (String.length s - 2)
41 String.sub s 1 (String.length s - 1)
45 %token <string> SPC STR IDENT INT EXTRA AC OP CP OC CC OQ CQ DEF FS COE CN SC
46 %token <string> LET IN TH PROOF QED VAR IND SEC REQ XP IP SET NOT LOAD ID COERC
50 %type <Types.items> items
53 | OQ verbatims CQ { $1 ^ $2 ^ $3 }
61 | spc spcs { $1 ^ $2 }
65 | SPC rspcs { $1 ^ $2 }
67 fs: FS spcs { $1 ^ $2 };
68 ident: IDENT spcs { $1 ^ $2 };
69 th: TH spcs { $1 ^ $2 };
70 proof: PROOF spcs { $1 ^ $2 };
71 qed: QED spcs { $1 ^ $2 };
72 sec: SEC spcs { $1 ^ $2 };
73 def: DEF spcs { $1 ^ $2 };
74 op: OP spcs { $1 ^ $2 };
75 xlet: LET spcs { $1 ^ $2 };
76 var: VAR spcs { $1 ^ $2 };
77 req: REQ spcs { $1 ^ $2 };
78 load: LOAD spcs { $1 ^ $2 };
79 xp: XP spcs { $1 ^ $2 };
80 ip: IP spcs { $1 ^ $2 };
81 ind: IND spcs { $1 ^ $2 };
82 set: SET spcs { $1 ^ $2 };
83 notation: NOT spcs { $1 ^ $2 };
84 oc: OC spcs { $1 ^ $2 };
85 coe: COE spcs { $1 ^ $2 };
86 cn: CN spcs { $1 ^ $2 };
87 sc: SC spcs { $1 ^ $2 };
88 str: STR spcs { $1 ^ $2 };
89 id: ID spcs { $1 ^ $2 };
90 coerc: COERC spcs { $1 ^ $2 };
95 | ident idents { $1 :: $2 }
103 | cnot spcs { $1 ^ $2 }
104 | cnot spcs cnots { $1 ^ $2 ^ $3 }
117 | xlet extends0 IN { $1 ^ $2 ^ $3 }
118 | op extends1 CP { $1 ^ $2 ^ $3 }
138 | restrict spcs { $1 ^ $2 }
139 | restrict spcs restricts { $1 ^ $2 ^ $3 }
142 | xre spcs { $1 ^ $2 }
143 | xre spcs restricts { $1 ^ $2 ^ $3 }
150 | extend0 spcs { $1 ^ $2 }
151 | extend0 spcs extends0 { $1 ^ $2 ^ $3 }
159 | extend1 spcs { $1 ^ $2 }
160 | extend1 spcs extends1 { $1 ^ $2 ^ $3 }
182 | unexport_rr { $1, [] }
183 | oc fields CC { $1 ^ fst $2 ^ $3, snd $2 }
186 | unexport_r spcs { fst $1 ^ $2, snd $1 }
187 | unexport_r spcs unexports_r { fst $1 ^ $2 ^ fst $3, snd $1 @ snd $3 }
190 | ident cn unexports_r { $1 ^ $2 ^ fst $3, snd $3 }
191 | ident coe unexports_r { $1 ^ $2 ^ fst $3, snd $3 @ [T.Coercion $1] }
195 | field sc fields { fst $1 ^ $2 ^ fst $3, snd $1 @ snd $3 }
197 | error { out "ERROR" "fields"; failwith "fields" }
205 | unexport spcs { fst $1 ^ $2, snd $1 }
206 | unexport spcs unexports { fst $1 ^ $2 ^ fst $3, snd $1 @ snd $3 }
227 | verbatim verbatims { $1 ^ $2 }
231 | restricts FS { [] }
235 | step spcs steps { $1 @ $3 }
240 | qid AC { strip1 $2 :: $1 }
244 | th ident restricts fs proof FS steps qed FS
245 { out "TH" $2; $7 @ [T.Inline (T.Con, $2)] }
246 | th ident restricts fs proof restricts FS
247 { out "TH" $2; [T.Inline (T.Con, $2)] }
248 | th ident restricts fs steps qed FS
249 { out "TH" $2; $5 @ [T.Inline (T.Con, $2)] }
250 | th ident restricts def restricts FS
251 { out "TH" $2; [T.Inline (T.Con, $2)] }
252 | th ident def restricts FS
253 { out "TH" $2; [T.Inline (T.Con, $2)] }
255 { out "VAR" (cat $2); mk_vars $2 }
256 | ind ident unexports FS
257 { out "IND" $2; snd $3 @ [T.Inline (T.Ind, $2)] }
259 { out "UNX" (fst $2); [T.Unexport ($1 ^ fst $2 ^ $3)] }
261 { out "REQ" $3; [T.Include $3] }
263 { out "REQ" $3; [T.Include $3] }
265 { out "REQ" $2; [T.Include $2] }
267 { out "REQ" $2; [T.Include (strip2 $2)] }
268 | coerc qid spcs cn unexports FS
269 { out "COERCE" (hd $2); [T.Coercion (hd $2)] }
270 | id coerc qid spcs cn unexports FS
271 { out "COERCE" (hd $3); [T.Coercion (hd $3)] }
273 { out "ERROR" $2; failwith ("macro_step " ^ $2) }
275 { out "ERROR" $2; failwith ("macro_step " ^ $2) }
278 out "ERROR" vs; failwith ("macro_step " ^ vs) }
281 | comment { [T.Comment $1] }
283 | set unexports FS { [T.Unexport ($1 ^ fst $2 ^ $3)] }
284 | notation unexports FS { [T.Notation ($1 ^ fst $2 ^ $3)] }
285 | error { out "ERROR" "item"; failwith "item" }
289 | rspcs item items { $2 @ $3 }