- let f name = function
- | Local i -> f (M.LRef i)
- | Global defs ->
- let map1 f = xlate_term f st lenv in
- let map2 f (name, _) = f (M.GRef (name, [])) in
- let f tail =
- let f args = f (M.GRef (name, args)) in
- let f defs = Cps.list_rev_map_append f map2 defs ~tail in
- Cps.list_sub_strict f defs args
+ let l = List.length lenv in
+ let g qid defs =
+ let map1 f = xlate_term f st lenv in
+ let map2 f (id, _) = resolve_lref_strict f st l lenv id in
+ let f tail =
+ let f args = f (M.GRef (l, uri_of_qid qid, args)) in
+ let f defs = Cps.list_rev_map_append f map2 defs ~tail in
+ Cps.list_sub_strict f defs args
+ in
+ Cps.list_map f map1 args
+ in
+ let g qid = resolve_gref_relaxed g st qid in
+ let f = function
+ | Some t -> f t
+ | None -> complete_qid g st name
+ in
+ resolve_lref f st l lenv (id_of_name name)
+
+let xlate_item f st = function
+ | A.Section (Some name) ->
+ f {st with path = name :: st.path; nodes = st.node :: st.nodes} None
+ | A.Section None ->
+ begin match st.path, st.nodes with
+ | _ :: ptl, nhd :: ntl ->
+ f {st with path = ptl; node = nhd; nodes = ntl} None
+ | _ -> assert false
+ end
+ | A.Context None ->
+ f {st with node = None} None
+ | A.Context (Some name) ->
+ let f name = f {st with node = Some name} None in
+ complete_qid f st name
+ | A.Block (name, w) ->
+ let f qid =
+ let f pars =
+ let f ww =
+ H.add st.hcnt qid ((name, ww) :: pars);
+ f {st with node = Some qid} None
+ 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 qid =
+ let f ww =
+ let entry = (st.line, pars, uri_of_qid qid, ww, None) in
+ H.add st.henv qid pars;
+ f {st with line = succ st.line} (Some entry)
+ 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 qid =
+ let f ww vv =
+ let entry = (st.line, pars, uri_of_qid qid, ww, Some (trans, vv)) in
+ H.add st.henv qid pars;
+ f {st with line = succ st.line} (Some entry)