X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Fbinaries%2Ftranscript%2Fv8Parser.mly;h=ff70df7138011031cbdbd5d74bf7db8ab1689712;hb=refs%2Ftags%2F0.4.95%407852;hp=06d4d908ba2fd7d9c49e8794e4d413a222279dff;hpb=52206fa1c090fcdc8386ec8d7e88beca089c7e39;p=helm.git diff --git a/components/binaries/transcript/v8Parser.mly b/components/binaries/transcript/v8Parser.mly index 06d4d908b..ff70df713 100644 --- a/components/binaries/transcript/v8Parser.mly +++ b/components/binaries/transcript/v8Parser.mly @@ -34,8 +34,8 @@ let cat x = String.concat " " x - let mk_vars idents = - let map ident = T.Inline (T.Var, trim ident) in + let mk_vars local idents = + let map ident = T.Inline (local, T.Var, trim ident, "") in List.map map idents let strip2 s = @@ -51,7 +51,7 @@ [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 LET IN TH PROOF QED VAR IND SEC REQ XP IP SET NOT LOAD ID COERC + %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 @@ -72,16 +72,38 @@ | { "" } | 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: IDENT 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 }; - xlet: LET 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 }; @@ -121,7 +143,7 @@ | CC { $1 } | COE { $1 } | STR { $1 } - | xlet extends0 IN { $1 ^ $2 ^ $3 } + | abbr extends0 IN { $1 ^ $2 ^ $3 } | op extends1 CP { $1 ^ $2 ^ $3 } ; @@ -175,7 +197,7 @@ | COE { $1 } | STR { $1 } | OP { $1 } - | LET { $1 } + | ABBR { $1 } | IN { $1 } | CP { $1 } | DEF { $1 } @@ -220,9 +242,13 @@ | 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 } @@ -245,46 +271,65 @@ ; qid: - | IDENT { [$1] } + | xident { [$1] } | qid AC { strip1 $2 :: $1 } ; macro_step: | th ident restricts fs proof FS steps qed FS - { out "TH" $2; $7 @ [T.Inline (T.Con, trim $2)] } + { out "TH" $2; $7 @ [T.Inline (false, T.Con, trim $2, "")] } | th ident restricts fs proof restricts FS - { out "TH" $2; [T.Inline (T.Con, trim $2)] } + { out "TH" $2; [T.Inline (false, T.Con, trim $2, "")] } | th ident restricts fs steps qed FS - { out "TH" $2; $5 @ [T.Inline (T.Con, trim $2)] } + { out "TH" $2; $5 @ [T.Inline (false, T.Con, trim $2, "")] } | th ident restricts def restricts FS - { out "TH" $2; [T.Inline (T.Con, trim $2)] } + { out "TH" $2; [T.Inline (false, T.Con, trim $2, "")] } | th ident def restricts FS - { out "TH" $2; [T.Inline (T.Con, trim $2)] } + { 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 $2 } + { 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 (T.Ind, trim $2) :: snd $3 } - | sec unexports FS - { out "UNX" (fst $2); [T.Unexport ($1 ^ fst $2 ^ trim $3)] } + { 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)] } + { out "REQ" $3; [T.Include (trim $3)] } | req ip ident FS - { out "REQ" $3; [T.Include (trim $3)] } + { out "REQ" $3; [T.Include (trim $3)] } | req ident FS - { out "REQ" $2; [T.Include (trim $2)] } + { out "REQ" $2; [T.Include (trim $2)] } | load str FS - { out "REQ" $2; [T.Include (strip2 (trim $2))] } + { out "REQ" $2; [T.Include (strip2 (trim $2))] } | coerc qid spcs cn unexports FS - { out "COERCE" (hd $2); coercion (hd $2) } + { out "COERCE" (hd $2); coercion (hd $2) } | id coerc qid spcs cn unexports FS - { out "COERCE" (hd $3); coercion (hd $3) } + { out "COERCE" (hd $3); coercion (hd $3) } | th ident error - { out "ERROR" $2; failwith ("macro_step " ^ $2) } + { out "ERROR" $2; failwith ("macro_step " ^ $2) } | ind ident error - { out "ERROR" $2; failwith ("macro_step " ^ $2) } + { out "ERROR" $2; failwith ("macro_step " ^ $2) } | var idents error { let vs = cat $2 in - out "ERROR" vs; failwith ("macro_step " ^ vs) } + 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] }