let rec xlate_term f st lenv = function
| T.Inst _
- | T.Impl _ -> assert false
- | T.Sort h ->
+ | T.Impl _ -> assert false
+ | T.Sort h ->
f (D.TSort ([], h))
- | T.NSrt id ->
+ | T.NSrt id ->
let f h = f (D.TSort ([], h)) in
H.sort_of_string C.err f id
- | T.LRef (i, j) ->
+ | T.LRef (i, j) ->
D.get_index C.err (mk_lref f i j) i j lenv
- | T.NRef id ->
+ | T.NRef id ->
let err () = resolve_gref C.err (mk_gref f) st id in
D.resolve_lref err (mk_lref f) id lenv
- | T.Cast (u, t) ->
+ | T.Cast (u, t) ->
let f uu tt = f (D.TCast ([], uu, tt)) in
let f uu = xlate_term (f uu) st lenv t in
xlate_term f st lenv u
- | T.Appl (vs, t) ->
+ | 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 (b, t) ->
+ | 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
in
let lenv, aa, bb = match b with
| T.Abst xws ->
- let lenv = D.push_bind C.start lenv [] (D.Abst []) in
+ 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 wws
+ 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
let xlate_term f st lenv t =
TT.contract (xlate_term f st lenv) t
-let mk_contents tt = function
- | T.Decl -> [], E.Abst tt
- | T.Ax -> [], E.Abst tt
+let mk_contents n tt = function
+ | T.Decl -> [], E.Abst (n, tt)
+ | T.Ax -> [], E.Abst (n, tt)
+ | T.Cong -> [], E.Abst (n, tt)
| T.Def -> [], E.Abbr tt
| T.Th -> [], E.Abbr tt
{st with sort = H.set_sorts ix [s]}
in
err (List.fold_left map st sorts)
- | T.Graph id ->
+ | T.Graph id ->
assert (H.set_graph id); err st
- | T.Entity (kind, id, meta, t) ->
+ | T.Entity (kind, n, id, meta, t) ->
let uri = uri_of_id st id st.path in
Hashtbl.add henv id uri;
let tt = xlate_term C.start st D.empty_lenv t in
(*
print_newline (); CrgOutput.pp_term print_string tt;
*)
- let a, b = mk_contents tt kind in
+ let a, b = mk_contents n tt kind in
let a = if meta <> "" then E.Meta meta :: a else a in
let entity = E.Mark st.line :: a, uri, b in
f {st with line = succ st.line} entity
- | T.Generate _ ->
+ | T.Generate _ ->
err st
(* Interface functions ******************************************************)