\ / This software is distributed as is, NO WARRANTY.
V_______________________________________________________________ *)
+module U = NUri
+module C = Cps
+module H = Hierarchy
+module Y = Entity
module X = Library
module D = Drg
-let rec list_iter map l f = match l with
- | [] -> f
- | hd :: tl -> map hd (list_iter map tl f)
+let rec list_iter map l out tab = match l with
+ | [] -> ()
+ | hd :: tl -> map hd out tab; list_iter map tl out tab
-let rec lenv_iter map l f = match l with
- | D.Null -> f
- | D.Cons (lenv, a, b) -> lenv_iter map lenv (map a b f)
+let list_rev_iter map e ns l out tab =
+ let rec aux err f e = function
+ | [], [] -> f e
+ | n :: ns, hd :: tl ->
+ let f e = map e hd out tab; f (D.push2 C.err C.start e n ~t:hd) in
+ aux err f e (ns, tl)
+ | _ -> err ()
+ in
+ ignore (aux C.err C.start e (ns, l))
-let rec exp_term t f = match t with
- | D.Sort (a, h) ->
- let attrs = [X.position h; X.name a] in
- X.tag X.sort attrs f
- | D.LRef (a, i, j) ->
+let lenv_iter map1 map2 l out tab =
+ let rec aux f = function
+ | D.ESort -> f ()
+ | D.EBind (lenv, a, b) -> aux (fun () -> map1 a b out tab; f ()) lenv
+ | D.EProj (lenv, a, e) -> aux (fun () -> map2 a e out tab; f ()) lenv
+ in
+ aux C.start l
+
+let rec exp_term e t out tab = match t with
+ | D.TSort (a, l) ->
+ let a =
+ let err _ = a in
+ let f s = Y.Name (s, true) :: a in
+ H.get_sort err f l
+ in
+ let attrs = [X.position l; X.name a] in
+ X.tag X.sort attrs out tab
+ | D.TLRef (a, i, j) ->
+ let a =
+ let err _ = a in
+ let f n r = Y.Name (n, r) :: a in
+ D.get_name err f i j e
+ in
let attrs = [X.position i; X.offset j; X.name a] in
- X.tag X.lref attrs f
- | D.GRef (a, n) ->
+ X.tag X.lref attrs out tab
+ | D.TGRef (a, n) ->
+ let a = Y.Name (U.name_of_uri n, true) :: a in
let attrs = [X.uri n; X.name a] in
- X.tag X.gref attrs f
- | D.Cast (a, u, t) ->
+ X.tag X.gref attrs out tab
+ | D.TCast (a, u, t) ->
let attrs = [] in
- X.tag X.cast attrs (exp_term t f) ~contents:(exp_term u)
- | D.Appl (a, vs, t) ->
+ X.tag X.cast attrs ~contents:(exp_term e u) out tab;
+ exp_term e t out tab
+ | D.TAppl (a, vs, t) ->
let attrs = [X.arity (List.length vs)] in
- X.tag X.appl attrs (exp_term t f) ~contents:(list_iter exp_term vs)
- | D.Proj (a, lenv, t) ->
+ X.tag X.appl attrs ~contents:(list_iter (exp_term e) vs) out tab;
+ exp_term e t out tab
+ | D.TProj (a, lenv, t) ->
let attrs = [] in
- X.tag X.proj attrs (exp_term t f) ~contents:(lenv_iter exp_lenv lenv)
- | D.Bind (a, b, t) ->
- exp_lenv a b (exp_term t f)
-
-and exp_lenv a b f = match b with
- | D.Abst ws ->
- let attrs = [X.name a; X.mark a; X.arity (List.length ws)] in
- X.tag X.abst attrs f ~contents:(list_iter exp_term ws)
- | D.Abbr vs ->
- let attrs = [X.name a; X.mark a; X.arity (List.length vs)] in
- X.tag X.abbr attrs f ~contents:(list_iter exp_term vs)
- | D.Void n ->
- let attrs = [X.name a; X.mark a; X.arity n] in
- X.tag X.void attrs f
-
-let export_term = exp_term
+ X.tag X.proj attrs ~contents:(lenv_iter (exp_bind e) (exp_eproj e) lenv) out tab;
+ exp_term (D.push_proj C.start e a lenv) t out tab
+ | D.TBind (a, b, t) ->
+ exp_bind e a b out tab;
+ exp_term (D.push_bind C.start e a b) t out tab
+
+and exp_bind e a b out tab =
+ let f a ns = a, ns in
+ let a, ns = Y.get_names f a in
+ match b with
+ | D.Abst ws ->
+ let e = D.push_bind C.start e a (D.Abst []) in
+ let attrs = [X.name ns; X.mark a; X.arity (List.length ws)] in
+ X.tag X.abst attrs ~contents:(list_rev_iter exp_term e ns ws) out tab
+ | D.Abbr vs ->
+ let e = D.push_bind C.start e a (D.Abbr []) in
+ let attrs = [X.name ns; X.mark a; X.arity (List.length vs)] in
+ X.tag X.abbr attrs ~contents:(list_rev_iter exp_term e ns vs) out tab
+ | D.Void n ->
+ let attrs = [X.name a; X.mark a; X.arity n] in
+ X.tag X.void attrs out tab
+
+and exp_eproj e a lenv out tab =
+ let attrs = [] in
+ X.tag X.proj attrs ~contents:(lenv_iter (exp_bind e) (exp_eproj e) lenv) out tab
+
+let export_term = exp_term D.empty_lenv