+
+let xlate_item f st = function
+ | A.Section (Some name) ->
+ f {st with path = name :: st.path; nodes = st.node :: st.nodes}
+ | A.Section None ->
+ begin match st.path, st.nodes with
+ | _ :: ptl, nhd :: ntl ->
+ f {st with path = ptl; node = nhd; nodes = ntl}
+ | _ -> assert false
+ end
+ | A.Context None ->
+ f {st with node = None}
+ | A.Context (Some name) ->
+ let f name = f {st with node = Some name} in
+ complete_qid f st name
+ | A.Block (name, w) ->
+ let f name =
+ let f pars =
+ let f ww =
+ H.add st.hcnt name ((name, ww) :: pars);
+ f {st with node = Some name}
+ in
+ xlate_term f st pars w
+ in
+ get_pars_relaxed f st
+ in
+ complete_qid f st (name, true, [])
+ | A.Decl (name, w) ->
+ let f pars =
+ let f name =
+ let f ww =
+ let entry = (st.line, pars, name, ww, None) in
+ H.add st.henv name pars;
+ f {st with genv = entry :: st.genv; line = succ st.line}
+ in
+ xlate_term f st pars w
+ in
+ complete_qid f st (name, true, [])
+ in
+ get_pars_relaxed f st
+ | A.Def (name, w, trans, v) ->
+ let f pars =
+ let f name =
+ let f ww vv =
+ let entry = (st.line, pars, name, ww, Some (trans, vv)) in
+ H.add st.henv name pars;
+ f {st with genv = entry :: st.genv; line = succ st.line}
+ in
+ let f ww = xlate_term (f ww) st pars v in
+ xlate_term f st pars w
+ in
+ complete_qid f st (name, true, [])
+ in
+ get_pars_relaxed f st
+
+let meta_of_aut f book =
+ let f st = f st.genv in
+ Cps.list_fold_left f xlate_item (initial_status hsize) book