- let f name ww = H.add st.cnt name (ww, st.node); f st in
- let f name = xlate_term (f name) st [] w in
- complete_qid f st (name, true, [])
- | A.Decl (name, w) -> f st
- | A.Def (name, w, trans, v) -> f st
+ 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