--- /dev/null
+/* Copyright (C) 2000, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://cs.unibo.it/helm/.
+ */
+
+%{
+ module T = Types
+
+ let out t s = () (* prerr_endline ("-- " ^ t ^ " " ^ s) *)
+
+ let trim = HExtlib.trim_blanks
+
+ let hd = List.hd
+
+ let cat x = String.concat " " x
+
+ let mk_vars local idents =
+ let map ident = T.Inline (local, T.Var, trim ident, "") in
+ List.map map idents
+
+ let strip2 s =
+ String.sub s 1 (String.length s - 2)
+
+ let strip1 s =
+ String.sub s 1 (String.length s - 1)
+
+ let coercion str =
+ [T.Coercion (false, str); T.Coercion (true, str)]
+
+ let notation str =
+ [T.Notation (false, str); T.Notation (true, str)]
+%}
+ %token <string> SPC STR IDENT INT EXTRA AC OP CP OC CC OQ CQ DEF FS COE CN SC
+ %token <string> ABBR IN LET TH PROOF QED VAR AX IND SEC END UNX REQ XP IP SET NOT LOAD ID COERC
+ %token EOF
+
+ %start items
+ %type <Types.items> items
+%%
+ comment:
+ | OQ verbatims CQ { $1 ^ $2 ^ $3 }
+ ;
+ spc:
+ | SPC { $1 }
+ | comment { $1 }
+ ;
+ spcs:
+ | { "" }
+ | spc spcs { $1 ^ $2 }
+ ;
+ rspcs:
+ | { "" }
+ | SPC rspcs { $1 ^ $2 }
+ ;
+ xident:
+ | IDENT { $1 }
+ | LET { $1 }
+ | TH { $1 }
+ | QED { $1 }
+ | PROOF { $1 }
+ | VAR { $1 }
+ | AX { $1 }
+ | IND { $1 }
+ | SEC { $1 }
+ | END { $1 }
+ | UNX { $1 }
+ | REQ { $1 }
+ | LOAD { $1 }
+ | NOT { $1 }
+ | ID { $1 }
+ | COERC { $1 }
+ ;
+ fs: FS spcs { $1 ^ $2 };
+ ident: xident spcs { $1 ^ $2 };
+ th: TH spcs { $1 ^ $2 };
+ xlet: LET spcs { $1 ^ $2 };
+ proof: PROOF spcs { $1 ^ $2 };
+ qed: QED spcs { $1 ^ $2 };
+ sec: SEC spcs { $1 ^ $2 };
+ xend: END spcs { $1 ^ $2 };
+ unx: UNX spcs { $1 ^ $2 };
+ def: DEF spcs { $1 ^ $2 };
+ op: OP spcs { $1 ^ $2 };
+ abbr: ABBR spcs { $1 ^ $2 };
+ var: VAR spcs { $1 ^ $2 };
+ ax: AX spcs { $1 ^ $2 };
+ req: REQ spcs { $1 ^ $2 };
+ load: LOAD spcs { $1 ^ $2 };
+ xp: XP spcs { $1 ^ $2 };
+ ip: IP spcs { $1 ^ $2 };
+ ind: IND spcs { $1 ^ $2 };
+ set: SET spcs { $1 ^ $2 };
+ notation: NOT spcs { $1 ^ $2 };
+ oc: OC spcs { $1 ^ $2 };
+ coe: COE spcs { $1 ^ $2 };
+ cn: CN spcs { $1 ^ $2 };
+ sc: SC spcs { $1 ^ $2 };
+ str: STR spcs { $1 ^ $2 };
+ id: ID spcs { $1 ^ $2 };
+ coerc: COERC spcs { $1 ^ $2 };
+
+ idents:
+ | ident { [$1] }
+ | ident idents { $1 :: $2 }
+ ;
+
+ cnot:
+ | EXTRA { $1 }
+ | INT { $1 }
+ ;
+ cnots:
+ | cnot spcs { $1 ^ $2 }
+ | cnot spcs cnots { $1 ^ $2 ^ $3 }
+ ;
+
+ xstrict:
+ | AC { $1 }
+ | INT { $1 }
+ | EXTRA { $1 }
+ | CN { $1 }
+ | SC { $1 }
+ | OC { $1 }
+ | CC { $1 }
+ | COE { $1 }
+ | STR { $1 }
+ | abbr extends0 IN { $1 ^ $2 ^ $3 }
+ | op extends1 CP { $1 ^ $2 ^ $3 }
+
+ ;
+ strict:
+ | xstrict { $1 }
+ | IDENT { $1 }
+ | SET { $1 }
+ | NOT { $1 }
+ ;
+ restrict:
+ | strict { $1 }
+ | IN { $1 }
+ | CP { $1 }
+ ;
+ xre:
+ | xstrict { $1 }
+ | IN { $1 }
+ | CP { $1 }
+ ;
+ restricts:
+ | restrict spcs { $1 ^ $2 }
+ | restrict spcs restricts { $1 ^ $2 ^ $3 }
+ ;
+ xres:
+ | xre spcs { $1 ^ $2 }
+ | xre spcs restricts { $1 ^ $2 ^ $3 }
+ ;
+ extend0:
+ | strict { $1 }
+ | DEF { $1 }
+ ;
+ extends0:
+ | extend0 spcs { $1 ^ $2 }
+ | extend0 spcs extends0 { $1 ^ $2 ^ $3 }
+ ;
+ extend1:
+ | strict { $1 }
+ | DEF { $1 }
+ | IN { $1 }
+ ;
+ extends1:
+ | extend1 spcs { $1 ^ $2 }
+ | extend1 spcs extends1 { $1 ^ $2 ^ $3 }
+ ;
+ unexport_rr:
+ | AC { $1 }
+ | INT { $1 }
+ | IDENT { $1 }
+ | EXTRA { $1 }
+ | CN { $1 }
+ | COE { $1 }
+ | STR { $1 }
+ | OP { $1 }
+ | ABBR { $1 }
+ | IN { $1 }
+ | CP { $1 }
+ | DEF { $1 }
+ | SET { $1 }
+ | NOT { $1 }
+ | LOAD { $1 }
+ | ID { $1 }
+ | COERC { $1 }
+ ;
+ unexport_r:
+ | unexport_rr { $1, [] }
+ | oc fields CC { $1 ^ fst $2 ^ $3, snd $2 }
+ ;
+ unexports_r:
+ | unexport_r spcs { fst $1 ^ $2, snd $1 }
+ | unexport_r spcs unexports_r { fst $1 ^ $2 ^ fst $3, snd $1 @ snd $3 }
+ ;
+ field:
+ | ident cn unexports_r
+ { $1 ^ $2 ^ fst $3, snd $3 }
+ | ident coe unexports_r
+ { $1 ^ $2 ^ fst $3, snd $3 @ coercion (trim $1) }
+ ;
+ fields:
+ | field { $1 }
+ | field sc fields { fst $1 ^ $2 ^ fst $3, snd $1 @ snd $3 }
+ | cnots { $1, [] }
+ | error { out "ERROR" "fields"; failwith "fields" }
+ ;
+ unexport:
+ | unexport_r { $1 }
+ | SC { $1, [] }
+ | CC { $1, [] }
+ ;
+ unexports:
+ | unexport spcs { fst $1 ^ $2, snd $1 }
+ | unexport spcs unexports { fst $1 ^ $2 ^ fst $3, snd $1 @ snd $3 }
+ ;
+ verbatim:
+ | unexport_rr { $1 }
+ | OC { $1 }
+ | CC { $1 }
+ | SC { $1 }
+ | TH { $1 }
+ | LET { $1 }
+ | VAR { $1 }
+ | AX { $1 }
+ | IND { $1 }
+ | SEC { $1 }
+ | END { $1 }
+ | UNX { $1 }
+ | REQ { $1 }
+ | XP { $1 }
+ | IP { $1 }
+ | QED { $1 }
+ | PROOF { $1 }
+ | FS { $1 }
+ | SPC { $1 }
+ ;
+ verbatims:
+ | { "" }
+ | verbatim verbatims { $1 ^ $2 }
+ ;
+ step:
+ | macro_step { $1 }
+ | restricts FS { [] }
+ ;
+ steps:
+ | step spcs { [] }
+ | step spcs steps { $1 @ $3 }
+ ;
+
+ qid:
+ | xident { [$1] }
+ | qid AC { strip1 $2 :: $1 }
+ ;
+
+ macro_step:
+ | th ident restricts fs proof FS steps qed FS
+ { out "TH" $2; $7 @ [T.Inline (false, T.Con, trim $2, "")] }
+ | th ident restricts fs proof restricts FS
+ { out "TH" $2; [T.Inline (false, T.Con, trim $2, "")] }
+ | th ident restricts fs steps qed FS
+ { out "TH" $2; $5 @ [T.Inline (false, T.Con, trim $2, "")] }
+ | th ident restricts def restricts FS
+ { out "TH" $2; [T.Inline (false, T.Con, trim $2, "")] }
+ | th ident def restricts FS
+ { out "TH" $2; [T.Inline (false, T.Con, trim $2, "")] }
+ | xlet ident restricts fs proof FS steps qed FS
+ { out "LET" $2; $7 @ [T.Inline (true, T.Con, trim $2, "")] }
+ | xlet ident restricts fs proof restricts FS
+ { out "LET" $2; [T.Inline (true, T.Con, trim $2, "")] }
+ | xlet ident restricts fs steps qed FS
+ { out "LET" $2; $5 @ [T.Inline (true, T.Con, trim $2, "")] }
+ | xlet ident restricts def restricts FS
+ { out "LET" $2; [T.Inline (true, T.Con, trim $2, "")] }
+ | xlet ident def restricts FS
+ { out "LET" $2; [T.Inline (true, T.Con, trim $2, "")] }
+ | var idents xres FS
+ { out "VAR" (cat $2); mk_vars true $2 }
+ | ax idents xres FS
+ { out "AX" (cat $2); mk_vars false $2 }
+ | ind ident unexports FS
+ { out "IND" $2; T.Inline (false, T.Ind, trim $2, "") :: snd $3 }
+ | sec ident FS
+ { out "SEC" $2; [T.Section (true, trim $2, $1 ^ $2)] }
+ | xend ident FS
+ { out "END" $2; [T.Section (false, trim $2, $1 ^ $2)] }
+ | unx unexports FS
+ { out "UNX" (fst $2); [T.Unexport ($1 ^ fst $2 ^ trim $3)] }
+ | req xp ident FS
+ { out "REQ" $3; [T.Include (trim $3)] }
+ | req ip ident FS
+ { out "REQ" $3; [T.Include (trim $3)] }
+ | req ident FS
+ { out "REQ" $2; [T.Include (trim $2)] }
+ | load str FS
+ { out "REQ" $2; [T.Include (strip2 (trim $2))] }
+ | coerc qid spcs cn unexports FS
+ { out "COERCE" (hd $2); coercion (hd $2) }
+ | id coerc qid spcs cn unexports FS
+ { out "COERCE" (hd $3); coercion (hd $3) }
+ | th ident error
+ { out "ERROR" $2; failwith ("macro_step " ^ $2) }
+ | ind ident error
+ { out "ERROR" $2; failwith ("macro_step " ^ $2) }
+ | var idents error
+ { let vs = cat $2 in
+ out "ERROR" vs; failwith ("macro_step " ^ vs) }
+ | ax idents error
+ { let vs = cat $2 in
+ out "ERROR" vs; failwith ("macro_step " ^ vs) }
+ ;
+ item:
+ | OQ verbatims CQ { [T.Comment $2] }
+ | macro_step { $1 }
+ | set unexports FS { [T.Unexport ($1 ^ fst $2 ^ trim $3)] }
+ | notation unexports FS { notation ($1 ^ fst $2 ^ trim $3) }
+ | error { out "ERROR" "item"; failwith "item" }
+ ;
+ items:
+ | rspcs EOF { [] }
+ | rspcs item items { $2 @ $3 }
+ ;
projects / helm.git / blobdiff