- 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
- in
- let f tt = f (D.TBind (aa, bb, tt)) in
- xlate_term f st lenv t
-
-let xlate_term f st lenv t =
- TT.contract (xlate_term f st lenv) t
-
-let mk_contents n tt = function
- | T.Decl -> [] , E.Abst (n, tt)
- | T.Ax -> [E.InProp] , E.Abst (n, tt)
- | T.Cong -> [E.InProp; E.Progress], E.Abst (n, tt)
- | T.Def -> [] , E.Abbr tt
- | T.Th -> [E.InProp] , E.Abbr tt
+ let f e y tt = f y (D.TProj (e, tt)) in
+ let f e = xlate_term (f e) st lenv t in
+ C.list_fold_right f map vs D.empty_lenv
+
+and xlate_bind st f (lenv, e) b =
+ let f lenv e = f (lenv, e) in
+ let f y b lenv = D.push_bind (f lenv) E.empty_node y b e in
+ let f y b = D.push_bind (f y b) E.empty_node y b lenv in
+ match b with
+ | T.Abst (n, id, r, w) ->
+ let f y ww =
+ let y = E.bind_attrs ?name:(name_of_id id) () in
+ f y (D.Abst (false, n, ww))
+ in
+ xlate_term f st lenv w
+ | T.Abbr (id, v) ->
+ let f y vv =
+ let y = E.bind_attrs ?name:(name_of_id id) () in
+ f y (D.Abbr vv)
+ in
+ xlate_term f st lenv v
+ | T.Void id ->
+ let y = E.bind_attrs ?name:(name_of_id id) ~main:(st.sort, 0) () in
+ f y D.Void
+
+let mk_contents main kind tt =
+ let ms, b = match kind with
+ | T.Decl -> [] , E.abst E.empty_env tt
+ | T.Ax -> [E.InProp] , E.abst E.empty_env tt
+ | T.Cong -> [E.InProp; E.Progress], E.abst E.empty_env tt
+ | T.Def -> [] , E.abbr E.empty_env tt
+ | T.Th -> [E.InProp] , E.abbr E.empty_env tt
+ in
+ if main then E.Main :: ms, b else ms, b