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
22 (* internal functions *******************************************************)
24 let lenv_iter map_bind map_appl map_proj st e lenv out tab =
25 let rec aux = function
27 | D.EBind (e, a, y, b) ->
29 (* NOTE: the inner binders are alpha-converted first *)
30 let y = R.alpha D.mem e y in
31 map_bind st e a y b out tab; D.EBind (e, a, y, b)
32 | D.EAppl (e, a, v) ->
34 map_appl st e a v out tab; D.EAppl (e, a, v)
37 map_proj st e d out tab; D.EProj (e, d)
41 let rec exp_term st e t out tab = match t with
44 let err _ = E.empty_bind in
45 let f s = E.bind_attrs ~name:(s, true) () in
46 H.string_of_sort err f k
48 let attrs = [XL.position k; XL.name y] in
49 XL.tag XL.sort attrs out tab
52 let err _ = E.empty_bind in
53 let f s r = E.bind_attrs ~name:(s, r) () in
56 let attrs = [XL.depth i; XL.name y] in
57 XL.tag XL.lref attrs out tab
59 let y = E.bind_attrs ~name:(U.name_of_uri n, true) () in
60 let attrs = [XL.uri n; XL.name y] in
61 XL.tag XL.gref attrs out tab
64 XL.tag XL.cast attrs ~contents:(exp_term st e u) out tab;
65 exp_term st e t out tab
66 | D.TAppl (a, v, t) ->
67 let attrs = XL.restricted a.E.a_rest :: XL.side a.E.a_side @ XL.main a.E.a_main in
68 XL.tag XL.appl attrs ~contents:(exp_term st e v) out tab;
69 exp_term st e t out tab
70 | D.TProj (lenv, t) ->
72 XL.tag XL.proj attrs ~contents:(lenv_iter exp_bind exp_appl exp_proj st e lenv) out tab;
73 exp_term st (D.push_proj C.start lenv e) t out tab
74 | D.TBind (a, b, t) ->
75 (* NOTE: the inner binders are alpha-converted first *)
76 let a = R.alpha D.mem e a in
77 exp_bind st e E.empty_node a b out tab;
78 exp_term st (D.push_bind C.start E.empty_node a b e) t out tab
80 and exp_appl st e a v out tab =
81 let attrs = XL.restricted a.E.a_rest :: XL.side a.E.a_side @ XL.main a.E.a_main in
82 XL.tag XL.appl attrs ~contents:(exp_term st e v) out tab;
84 and exp_bind st e y a b out tab = match b with
86 let attrs = XL.layer st n :: XL.name a :: XL.side a.E.b_side @ XL.main a.E.b_main in
87 XL.tag XL.abst attrs ~contents:(exp_term st e w) out tab
89 let attrs = [XL.name a] in
90 XL.tag XL.abbr attrs ~contents:(exp_term st e v) out tab
92 let attrs = [XL.name a] in
93 XL.tag XL.void attrs out tab
95 and exp_proj st e lenv out tab =
97 XL.tag XL.proj attrs ~contents:(lenv_iter exp_bind exp_appl exp_proj st e lenv) out tab
99 (* interface functions ******************************************************)
101 let export_term st = exp_term st D.empty_lenv