\ / This software is distributed as is, NO WARRANTY.
V_______________________________________________________________ *)
-module U = NUri
-module H = Hierarchy
-module C = Cps
-module Y = Entity
-module T = Txt
-module D = Crg
+module U = NUri
+module H = Hierarchy
+module C = Cps
+module Y = Entity
+module T = Txt
+module TT = TxtTxt
+module D = Crg
type status = {
path: T.id list; (* current section path *)
path = []; line = 1; sort = 0; mk_uri = mk_uri
}
-let name_of_id id = Y.Name (id, true)
+let name_of_id ?(r=true) id = Y.Name (id, r)
let mk_lref f i j k = f (D.TLRef ([Y.Apix k], i, j))
with Not_found -> err ()
let rec xlate_term f st lenv = function
- | T.Sort h ->
+ | T.Inst _
+ | 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) ->
- let map1 (lenv, a, wws) (id, w) =
+ | T.Bind (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
+ D.push2 C.err C.start lenv attr ~t:ww (), attr :: a, ww :: wws
+ in
+ let abbr_map (lenv, a, wws) (id, w) =
let attr = name_of_id id in
let ww = xlate_term C.start st lenv w in
D.push2 C.err C.start lenv attr ~t:ww (), attr :: a, ww :: wws
in
- let map2 (lenv, a, n) id =
+ let void_map (lenv, a, n) id =
let attr = name_of_id id in
D.push2 C.err C.start lenv attr (), attr :: a, succ n
in
let lenv, aa, bb = match b with
| T.Abst xws ->
let lenv = D.push_bind C.start lenv [] (D.Abst []) in
- let lenv, aa, wws = List.fold_left map1 (lenv, [], []) xws in
+ let lenv, aa, wws = List.fold_left abst_map (lenv, [], []) xws in
lenv, aa, D.Abst wws
| T.Abbr xvs ->
let lenv = D.push_bind C.start lenv [] (D.Abbr []) in
- let lenv, aa, vvs = List.fold_left map1 (lenv, [], []) xvs 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 map2 (lenv, [], 0) ids 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 tt = function
| T.Decl -> [], Y.Abst tt
| T.Ax -> [], Y.Abst tt