X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=components%2Fbinaries%2Ftranscript%2Fv8Parser.mly;fp=components%2Fbinaries%2Ftranscript%2Fv8Parser.mly;h=ff70df7138011031cbdbd5d74bf7db8ab1689712;hp=0000000000000000000000000000000000000000;hb=f61af501fb4608cc4fb062a0864c774e677f0d76;hpb=58ae1809c352e71e7b5530dc41e2bfc834e1aef1 diff --git a/components/binaries/transcript/v8Parser.mly b/components/binaries/transcript/v8Parser.mly new file mode 100644 index 000000000..ff70df713 --- /dev/null +++ b/components/binaries/transcript/v8Parser.mly @@ -0,0 +1,344 @@ +/* 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 SPC STR IDENT INT EXTRA AC OP CP OC CC OQ CQ DEF FS COE CN SC + %token 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 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 } + ;