(* NOTE: the inner binders are alpha-converted first *)
let y = R.alpha D.mem e y in
map_bind st e a y b out tab; D.EBind (e, a, y, b)
- | D.EAppl (e, x, v) ->
+ | D.EAppl (e, a, v) ->
let e = aux e in
- map_appl st e x v out tab; D.EAppl (e, x, v)
+ map_appl st e a v out tab; D.EAppl (e, a, v)
| D.EProj (e, d) ->
let e = aux e in
map_proj st e d out tab; D.EProj (e, d)
let attrs = [] in
XL.tag XL.cast attrs ~contents:(exp_term st e u) out tab;
exp_term st e t out tab
- | D.TAppl (x, v, t) ->
- let attrs = [] in
- XL.tag (XL.appl x) attrs ~contents:(exp_term st e v) out tab;
+ | D.TAppl (a, v, t) ->
+ let attrs = XL.restricted a.E.a_rest :: XL.side a.E.a_side @ XL.main a.E.a_main in
+ XL.tag XL.appl attrs ~contents:(exp_term st e v) out tab;
exp_term st e t out tab
| D.TProj (lenv, t) ->
let attrs = [] in
XL.tag XL.proj attrs ~contents:(lenv_iter exp_bind exp_appl exp_proj st e lenv) out tab;
exp_term st (D.push_proj C.start lenv e) t out tab
- | D.TBind (y, b, t) ->
+ | D.TBind (a, b, t) ->
(* NOTE: the inner binders are alpha-converted first *)
- let y = R.alpha D.mem e y in
- exp_bind st e E.empty_node y b out tab;
- exp_term st (D.push_bind C.start E.empty_node y b e) t out tab
+ let a = R.alpha D.mem e a in
+ exp_bind st e E.empty_node a b out tab;
+ exp_term st (D.push_bind C.start E.empty_node a b e) t out tab
-and exp_appl st e x v out tab =
- let attrs = [] in
- XL.tag (XL.appl x) attrs ~contents:(exp_term st e v) out tab;
+and exp_appl st e a v out tab =
+ let attrs = XL.restricted a.E.a_rest :: XL.side a.E.a_side @ XL.main a.E.a_main in
+ XL.tag XL.appl attrs ~contents:(exp_term st e v) out tab;
-and exp_bind st e a y b out tab = match b with
+and exp_bind st e y a b out tab = match b with
| D.Abst (_, n, w) ->
- let attrs = XL.layer st n :: XL.name y :: XL.side y @ XL.main y in
+ let attrs = XL.layer st n :: XL.name a :: XL.side a.E.b_side @ XL.main a.E.b_main in
XL.tag XL.abst attrs ~contents:(exp_term st e w) out tab
| D.Abbr v ->
- let attrs = [XL.name y] in
+ let attrs = [XL.name a] in
XL.tag XL.abbr attrs ~contents:(exp_term st e v) out tab
| D.Void ->
- let attrs = [XL.name y] in
+ let attrs = [XL.name a] in
XL.tag XL.void attrs out tab
and exp_proj st e lenv out tab =