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_______________________________________________________________ *)
17 module XL = XmlLibrary
20 (* internal functions *******************************************************)
22 let rec list_iter map l out tab = match l with
24 | hd :: tl -> map hd out tab; list_iter map tl out tab
26 let list_rev_iter map e ns l out tab =
27 let rec aux err f e = function
29 | n :: ns, hd :: tl ->
32 pp_lenv print_string e; print_string " |- ";
33 pp_term print_string hd; print_newline ();
35 map e hd out tab; f (D.push2 C.err C.start e ~attr:n ~t:hd ())
40 ignore (aux C.err C.start e (ns, l))
42 let lenv_iter map1 map2 l out tab =
43 let rec aux f = function
45 | D.EBind (lenv, a, b) -> aux (fun () -> map1 a b out tab; f ()) lenv
46 | D.EProj (lenv, a, e) -> aux (fun () -> map2 a e out tab; f ()) lenv
50 let rec exp_term e t out tab = match t with
54 let f s = Y.Name (s, true) :: a in
55 H.string_of_sort err f l
57 let attrs = [XL.position l; XL.name a] in
58 XL.tag XL.sort attrs out tab
59 | D.TLRef (a, i, j) ->
62 let f n r = Y.Name (n, r) :: a in
63 D.get_name err f i j e
65 let attrs = [XL.position i; XL.offset j; XL.name a] in
66 XL.tag XL.lref attrs out tab
68 let a = Y.Name (U.name_of_uri n, true) :: a in
69 let attrs = [XL.uri n; XL.name a] in
70 XL.tag XL.gref attrs out tab
71 | D.TCast (a, u, t) ->
73 XL.tag XL.cast attrs ~contents:(exp_term e u) out tab;
75 | D.TAppl (a, vs, t) ->
76 let attrs = [XL.arity vs] in
77 XL.tag XL.appl attrs ~contents:(list_iter (exp_term e) vs) out tab;
79 | D.TProj (a, lenv, t) ->
81 XL.tag XL.proj attrs ~contents:(lenv_iter (exp_bind e) (exp_eproj e) lenv) out tab;
82 exp_term (D.push_proj C.start e a lenv) t out tab
83 | D.TBind (a, b, t) ->
84 (* NOTE: the inner binders are alpha-converted first *)
85 let a = R.alpha (D.names_of_lenv [] e) a in
86 exp_bind e a b out tab;
87 exp_term (D.push_bind C.start e a b) t out tab
89 and exp_bind e a b out tab =
91 let a, ns = Y.get_names f a in
94 let e = D.push_bind C.start e a (D.Abst (n, [])) in
95 let attrs = [XL.level n; XL.name ns; XL.mark a; XL.arity ws] in
96 XL.tag XL.abst attrs ~contents:(list_rev_iter exp_term e ns ws) out tab
98 let e = D.push_bind C.start e a (D.Abbr []) in
99 let attrs = [XL.name ns; XL.mark a; XL.arity vs] in
100 XL.tag XL.abbr attrs ~contents:(list_rev_iter exp_term e ns vs) out tab
102 let attrs = [XL.name a; XL.mark a; XL.arity ~n []] in
103 XL.tag XL.void attrs out tab
105 and exp_eproj e a lenv out tab =
107 XL.tag XL.proj attrs ~contents:(lenv_iter (exp_bind e) (exp_eproj e) lenv) out tab
109 (* interface functions ******************************************************)
111 let export_term = exp_term D.empty_lenv