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 =
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> LET IN TH PROOF QED VAR IND SEC REQ XP IP SET NOT LOAD ID COERC
+ %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
| { "" }
| 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 };
| CC { $1 }
| COE { $1 }
| STR { $1 }
- | xlet extends0 IN { $1 ^ $2 ^ $3 }
+ | abbr extends0 IN { $1 ^ $2 ^ $3 }
| op extends1 CP { $1 ^ $2 ^ $3 }
;
| COE { $1 }
| STR { $1 }
| OP { $1 }
- | LET { $1 }
+ | ABBR { $1 }
| IN { $1 }
| CP { $1 }
| DEF { $1 }
;
field:
| ident cn unexports_r
- { $1 ^ $2 ^ fst $3, snd $3 }
+ { $1 ^ $2 ^ fst $3, snd $3 }
| ident coe unexports_r
- { $1 ^ $2 ^ fst $3, snd $3 @ [T.Coercion (trim $1)] }
+ { $1 ^ $2 ^ fst $3, snd $3 @ coercion (trim $1) }
;
fields:
| field { $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 }
;
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); [T.Coercion (hd $2)] }
+ { out "COERCE" (hd $2); coercion (hd $2) }
| id coerc qid spcs cn unexports FS
- { out "COERCE" (hd $3); [T.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] }
| macro_step { $1 }
| set unexports FS { [T.Unexport ($1 ^ fst $2 ^ trim $3)] }
- | notation unexports FS { [T.Notation ($1 ^ fst $2 ^ trim $3)] }
+ | notation unexports FS { notation ($1 ^ fst $2 ^ trim $3) }
| error { out "ERROR" "item"; failwith "item" }
;
items:
projects / helm.git / blobdiff