2 ||M|| This file is part of HELM, an Hypertextual, Electronic
3 ||A|| Library of Mathematics, developed at the Computer Science
4 ||T|| Department, University of Bologna, Italy.
6 ||T|| HELM is free software; you can redistribute it and/or
7 ||A|| modify it under the terms of the GNU General Public License
8 \ / version 2 or (at your option) any later version.
9 \ / This software is distributed as is, NO WARRANTY.
10 V_______________________________________________________________ *)
19 let list_iter map l out tab =
20 let rec aux f = function
22 | hd :: tl -> aux (fun () -> map hd out tab; f ()) tl
26 let list_rev_iter map e ns l out tab =
27 let rec aux err f e = function
29 | n :: ns, hd :: tl ->
30 let f e = map e hd out tab; f (D.push2 C.err C.start e n ~t:hd) in
34 ignore (aux C.err C.start e (ns, l))
36 let lenv_iter map1 map2 l out tab =
37 let rec aux f = function
39 | D.EBind (lenv, a, b) -> aux (fun () -> map1 a b out tab; f ()) lenv
40 | D.EProj (lenv, a, e) -> aux (fun () -> map2 a e out tab; f ()) lenv
44 let rec exp_term e t out tab = match t with
48 let f s = Y.Name (s, true) :: a in
51 let attrs = [X.position l; X.name a] in
52 X.tag X.sort attrs out tab
53 | D.TLRef (a, i, j) ->
56 let f n r = Y.Name (n, r) :: a in
57 D.get_name err f i j e
59 let attrs = [X.position i; X.offset j; X.name a] in
60 X.tag X.lref attrs out tab
62 let a = Y.Name (U.name_of_uri n, true) :: a in
63 let attrs = [X.uri n; X.name a] in
64 X.tag X.gref attrs out tab
65 | D.TCast (a, u, t) ->
67 X.tag X.cast attrs ~contents:(exp_term e u) out tab;
69 | D.TAppl (a, vs, t) ->
70 let attrs = [X.arity (List.length vs)] in
71 X.tag X.appl attrs ~contents:(list_iter (exp_term e) vs) out tab;
73 | D.TProj (a, lenv, t) ->
75 X.tag X.proj attrs ~contents:(lenv_iter (exp_bind e) (exp_eproj e) lenv) out tab;
76 exp_term (D.push_proj C.start e a lenv) t out tab
77 | D.TBind (a, b, t) ->
78 exp_bind e a b out tab;
79 exp_term (D.push_bind C.start e a b) t out tab
81 and exp_bind e a b out tab =
83 let a, ns = Y.get_names f a in
86 let e = D.push_bind C.start e a (D.Abst []) in
87 let attrs = [X.name ns; X.mark a; X.arity (List.length ws)] in
88 X.tag X.abst attrs ~contents:(list_rev_iter exp_term e ns ws) out tab
90 let e = D.push_bind C.start e a (D.Abbr []) in
91 let attrs = [X.name ns; X.mark a; X.arity (List.length vs)] in
92 X.tag X.abbr attrs ~contents:(list_rev_iter exp_term e ns vs) out tab
94 let attrs = [X.name a; X.mark a; X.arity n] in
95 X.tag X.void attrs out tab
97 and exp_eproj e a lenv out tab =
99 X.tag X.proj attrs ~contents:(lenv_iter (exp_bind e) (exp_eproj e) lenv) out tab
101 let export_term = exp_term D.empty_lenv