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_______________________________________________________________ *)
15 (* this is not tail recursive *)
16 let rec list_iter map l f = match l with
18 | hd :: tl -> map hd (list_iter map tl f)
20 let rec lenv_iter map1 map2 l f = match l with
22 | D.EBind (lenv, a, b) -> lenv_iter map1 map2 lenv (map1 a b f)
23 | D.EProj (lenv, a, e) -> lenv_iter map1 map2 lenv (map2 a e f)
25 (* these are not tail recursive *)
26 let rec exp_term t f = match t with
28 let attrs = [X.position h; X.name a] in
30 | D.TLRef (a, i, j) ->
31 let attrs = [X.position i; X.offset j; X.name a] in
34 let attrs = [X.uri n; X.name a] in
36 | D.TCast (a, u, t) ->
38 X.tag X.cast attrs (exp_term t f) ~contents:(exp_term u)
39 | D.TAppl (a, vs, t) ->
40 let attrs = [X.arity (List.length vs)] in
41 X.tag X.appl attrs (exp_term t f) ~contents:(list_iter exp_term vs)
42 | D.TProj (a, lenv, t) ->
44 X.tag X.proj attrs (exp_term t f) ~contents:(lenv_iter exp_bind exp_eproj lenv)
45 | D.TBind (a, b, t) ->
46 exp_bind a b (exp_term t f)
48 and exp_bind a b f = match b with
50 let attrs = [X.name a; X.mark a; X.arity (List.length ws)] in
51 X.tag X.abst attrs f ~contents:(list_iter exp_term ws)
53 let attrs = [X.name a; X.mark a; X.arity (List.length vs)] in
54 X.tag X.abbr attrs f ~contents:(list_iter exp_term vs)
56 let attrs = [X.name a; X.mark a; X.arity n] in
59 and exp_eproj a lenv f =
61 X.tag X.proj attrs f ~contents:(lenv_iter exp_bind exp_eproj lenv)
63 let export_term = exp_term