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 (* internal functions: crg to brg term **************************************)
21 let rec xlate_term f = function
22 | D.TSort (a, l) -> f (B.Sort (a, l))
23 | D.TGRef (a, n) -> f (B.GRef (a, n))
24 | D.TLRef (a, i) -> f (B.LRef (a, i))
25 | D.TCast (a, u, t) ->
26 let f tt uu = f (B.Cast (a, uu, tt)) in
27 let f tt = xlate_term (f tt) u in
29 | D.TAppl (a, v, t) ->
30 let f tt vv = f (B.Appl (a, vv, tt)) in
31 let f tt = xlate_term (f tt) v in
33 | D.TProj (_, e, t) ->
34 D.shift (xlate_term f) e t
35 | D.TBind (a, b, t) ->
36 xlate_term (xlate_bind f a b) t
38 and xlate_bind f a b x = match b with
40 let f ww = f (B.Bind (J.new_mark () :: a, B.Abst (n, ww), x)) in
43 let f vv = f (B.Bind (a, B.Abbr vv, x)) in
46 f (B.Bind (a, B.Void, x))
48 (* internal functions: brg to crg term **************************************)
50 let rec xlate_bk_term f = function
51 | B.Sort (a, l) -> f (D.TSort (a, l))
52 | B.GRef (a, n) -> f (D.TGRef (a, n))
53 | B.LRef (a, i) -> f (D.TLRef (a, i))
55 let f tt uu = f (D.TCast (a, uu, tt)) in
56 let f tt = xlate_bk_term (f tt) u in
59 let f tt uu = f (D.TAppl (a, uu, tt)) in
60 let f tt = xlate_bk_term (f tt) u in
63 let f tt bb = f (D.TBind (a, bb, tt)) in
64 let f tt = xlate_bk_bind (f tt) b in
67 and xlate_bk_bind f = function
69 let f tt = f (D.Abst (n, tt)) in
72 let f tt = f (D.Abbr tt) in
76 (* interface functions ******************************************************)
78 let brg_of_crg f t = f (xlate_term C.start t)
80 let crg_of_brg = xlate_bk_term