- | T.Appl (vs, t) ->
- let map f = xlate_term f st lenv in
- let f vvs tt = f (D.TAppl ([], vvs, tt)) in
- let f vvs = xlate_term (f vvs) st lenv t in
- C.list_map f map vs
- | T.Bind (n, b, t) ->
- let abst_map (lenv, a, wws) (id, r, w) =
- let attr = name_of_id ~r id in
- let ww = xlate_term C.start st lenv w in
- D.push2 C.err C.start lenv ~attr ~t:ww (), attr :: a, ww :: wws
- in
- let abbr_map (lenv, a, wws) (id, w) =
- let attr = name_of_id id in
- let ww = xlate_term C.start st lenv w in
- D.push2 C.err C.start lenv ~attr ~t:ww (), attr :: a, ww :: wws
- in
- let void_map (lenv, a, n) id =
- let attr = name_of_id id in
- D.push2 C.err C.start lenv ~attr (), attr :: a, succ n
- in
- let lenv, aa, bb = match b with
- | T.Abst xws ->
- let lenv = D.push_bind C.start lenv [] (D.Abst (n, [])) in
- let lenv, aa, wws = List.fold_left abst_map (lenv, [], []) xws in
- lenv, aa, D.Abst (n, wws)
- | T.Abbr xvs ->
- let lenv = D.push_bind C.start lenv [] (D.Abbr []) in
- let lenv, aa, vvs = List.fold_left abbr_map (lenv, [], []) xvs in
- lenv, aa, D.Abbr vvs
- | T.Void ids ->
- let lenv = D.push_bind C.start lenv [] (D.Void 0) in
- let lenv, aa, n = List.fold_left void_map (lenv, [], 0) ids in
- lenv, aa, D.Void n
+ | T.Appl (v, t) ->
+ let f vv y tt = f y (D.TAppl (E.appl_attrs st.rest, vv, tt)) in
+ let f _ vv = xlate_term (f vv) st lenv t in
+ xlate_term f st lenv v
+ | T.Proj (bs, t) ->
+ let f e y tt = f y (D.TProj (e, tt)) in
+ let f (lenv, e) = xlate_term (f e) st lenv t in
+ C.list_fold_left f (xlate_bind st) (lenv, D.empty_lenv) bs
+ | T.Inst (t, vs) ->
+ let map f v e =
+ let f _ vv = D.push_appl f (E.appl_attrs st.rest) vv e in
+ xlate_term f st lenv v