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, _, _) -> let f i = f (B.LRef (a, i)) in E.apix C.err f a
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, vs, t) ->
30 let map f v tt = let f vv = f (B.Appl (a, vv, tt)) in xlate_term f v in
31 let f tt = C.list_fold_right f map vs tt in
33 | D.TProj (_, e, t) ->
34 xlate_term f (D.tshift e t)
35 | D.TBind (a, b, t) ->
36 let f tt = f (xlate_bind tt a b) in xlate_term f t
38 and xlate_bind x a b =
40 let a, ns = E.get_names f a in
44 let f ww = B.Bind (n :: J.new_mark () :: a, B.Abst (m, ww), x) in
47 List.fold_left2 map x ns ws
50 let f vv = B.Bind (n :: a, B.Abbr vv, x) in
53 List.fold_left2 map x ns vs
55 let map x n = B.Bind (n :: a, B.Void, x) in
56 List.fold_left map x ns
58 (* internal functions: brg to crg term **************************************)
60 let rec xlate_bk_term f = function
61 | B.Sort (a, l) -> f (D.TSort (a, l))
62 | B.GRef (a, n) -> f (D.TGRef (a, n))
63 | B.LRef (a, i) -> f (D.TLRef (a, i, 0))
65 let f tt uu = f (D.TCast (a, uu, tt)) in
66 let f tt = xlate_bk_term (f tt) u in
69 let f tt uu = f (D.TAppl (a, [uu], tt)) in
70 let f tt = xlate_bk_term (f tt) u in
73 let f tt bb = f (D.TBind (a, bb, tt)) in
74 let f tt = xlate_bk_bind (f tt) b in
77 and xlate_bk_bind f = function
79 let f tt = f (D.Abst (n, [tt])) in
82 let f tt = f (D.Abbr [tt]) in
84 | B.Void -> f (D.Void 1)
86 (* interface functions ******************************************************)
88 let brg_of_crg f t = f (xlate_term C.start t)
90 let crg_of_brg = xlate_bk_term