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_______________________________________________________________ *)
20 (****************************************************************************)
24 | Y.Name (s, true) -> out (P.sprintf "%s;" s)
25 | Y.Name (s, false) -> out (P.sprintf "~%s;" s)
26 | Y.Apix i -> out (P.sprintf "+%i;" i)
27 | Y.Mark i -> out (P.sprintf "@%i;" i)
28 | Y.Meta s -> out (P.sprintf "\"%s\";" s)
29 | Y.Priv -> out (P.sprintf "%s;" "~")
33 let rec pp_term out = function
34 | D.TSort (a, l) -> pp_attrs out a; out (P.sprintf "*%u" l)
35 | D.TLRef (a, i, j) -> pp_attrs out a; out (P.sprintf "#(%u,%u)" i j)
36 | D.TGRef (a, u) -> pp_attrs out a; out (P.sprintf "$")
37 | D.TCast (a, x, y) -> pp_attrs out a; out "<"; pp_term out x; out ">."; pp_term out y
38 | D.TProj (a, x, y) -> assert false
39 | D.TAppl (a, x, y) -> pp_attrs out a; pp_terms "(" ")" out x; pp_term out y
40 | D.TBind (a, x, y) -> pp_attrs out a; pp_bind out x; pp_term out y
42 and pp_terms bg eg out vs =
43 let rec aux = function
45 | [v] -> pp_term out v
46 | v :: vs -> pp_term out v; out ", "; aux vs
48 out bg; aux vs; out (eg ^ ".")
50 and pp_bind out = function
51 | D.Abst x -> pp_terms "[:" "]" out x
52 | D.Abbr x -> pp_terms "[=" "]" out x
53 | D.Void x -> out (P.sprintf "[%u]" x)
55 let rec pp_lenv out = function
57 | D.EProj (x, a, y) -> assert false
58 | D.EBind (x, a, y) -> pp_lenv out x; pp_attrs out a; pp_bind out y
60 (****************************************************************************)
62 let rec list_iter map l out tab = match l with
64 | hd :: tl -> map hd out tab; list_iter map tl out tab
66 let list_rev_iter map e ns l out tab =
67 let rec aux err f e = function
69 | n :: ns, hd :: tl ->
72 pp_lenv print_string e; print_string " |- ";
73 pp_term print_string hd; print_newline ();
75 map e hd out tab; f (D.push2 C.err C.start e n ~t:hd ())
80 ignore (aux C.err C.start e (ns, l))
82 let lenv_iter map1 map2 l out tab =
83 let rec aux f = function
85 | D.EBind (lenv, a, b) -> aux (fun () -> map1 a b out tab; f ()) lenv
86 | D.EProj (lenv, a, e) -> aux (fun () -> map2 a e out tab; f ()) lenv
90 let rec exp_term e t out tab = match t with
94 let f s = Y.Name (s, true) :: a in
95 H.string_of_sort err f l
97 let attrs = [X.position l; X.name a] in
98 X.tag X.sort attrs out tab
99 | D.TLRef (a, i, j) ->
102 let f n r = Y.Name (n, r) :: a in
103 D.get_name err f i j e
105 let attrs = [X.position i; X.offset j; X.name a] in
106 X.tag X.lref attrs out tab
108 let a = Y.Name (U.name_of_uri n, true) :: a in
109 let attrs = [X.uri n; X.name a] in
110 X.tag X.gref attrs out tab
111 | D.TCast (a, u, t) ->
113 X.tag X.cast attrs ~contents:(exp_term e u) out tab;
115 | D.TAppl (a, vs, t) ->
116 let attrs = [X.arity (List.length vs)] in
117 X.tag X.appl attrs ~contents:(list_iter (exp_term e) vs) out tab;
119 | D.TProj (a, lenv, t) ->
121 X.tag X.proj attrs ~contents:(lenv_iter (exp_bind e) (exp_eproj e) lenv) out tab;
122 exp_term (D.push_proj C.start e a lenv) t out tab
123 | D.TBind (a, b, t) ->
124 exp_bind e a b out tab;
125 exp_term (D.push_bind C.start e a b) t out tab
127 and exp_bind e a b out tab =
128 let f a ns = a, ns in
129 let a, ns = Y.get_names f a in
132 let e = D.push_bind C.start e a (D.Abst []) in
133 let attrs = [X.name ns; X.mark a; X.arity (List.length ws)] in
134 X.tag X.abst attrs ~contents:(list_rev_iter exp_term e ns ws) out tab
136 let e = D.push_bind C.start e a (D.Abbr []) in
137 let attrs = [X.name ns; X.mark a; X.arity (List.length vs)] in
138 X.tag X.abbr attrs ~contents:(list_rev_iter exp_term e ns vs) out tab
140 let attrs = [X.name a; X.mark a; X.arity n] in
141 X.tag X.void attrs out tab
143 and exp_eproj e a lenv out tab =
145 X.tag X.proj attrs ~contents:(lenv_iter (exp_bind e) (exp_eproj e) lenv) out tab
147 (****************************************************************************)
149 let export_term = exp_term D.empty_lenv