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 lenv_fold_left map1 map2 x = function
23 | D.EBind (tl, a, b) -> lenv_fold_left map1 map2 (map1 x a b) tl
24 | D.EProj (tl, a, e) -> lenv_fold_left map1 map2 (map2 x a e) tl
26 let rec xlate_term f = function
27 | D.TSort (a, l) -> f (B.Sort (a, l))
28 | D.TGRef (a, n) -> f (B.GRef (a, n))
29 | D.TLRef (a, _, _) -> let f i = f (B.LRef (a, i)) in E.apix C.err f a
30 | D.TCast (a, u, t) ->
31 let f uu tt = f (B.Cast (a, uu, tt)) in
32 let f uu = xlate_term (f uu) t in
34 | D.TAppl (a, vs, t) ->
35 let map f v tt = let f vv = f (B.Appl (a, vv, tt)) in xlate_term f v in
36 let f tt = C.list_fold_right f map vs tt in
38 | D.TProj (a, e, t) ->
39 let f tt = f (lenv_fold_left xlate_bind xlate_proj tt e) in
41 | D.TBind (ab, D.Abst (n, ws), D.TCast (ac, u, t)) ->
42 xlate_term f (D.TCast (ac, D.TBind (ab, D.Abst (N.pred n, ws), u), D.TBind (ab, D.Abst (n, ws), t)))
43 | D.TBind (a, b, t) ->
44 let f tt = f (xlate_bind tt a b) in xlate_term f t
46 and xlate_bind x a b =
48 let a, ns = E.get_names f a in
52 let f ww = B.Bind (n :: J.new_mark () :: a, B.Abst (m, ww), x) in
55 List.fold_left2 map x ns ws
58 let f vv = B.Bind (n :: a, B.Abbr vv, x) in
61 List.fold_left2 map x ns vs
63 let map x n = B.Bind (n :: a, B.Void, x) in
64 List.fold_left map x ns
66 and xlate_proj x _ e =
67 lenv_fold_left xlate_bind xlate_proj x e
69 (* internal functions: brg to crg term **************************************)
71 let rec xlate_bk_term f = function
72 | B.Sort (a, l) -> f (D.TSort (a, l))
73 | B.GRef (a, n) -> f (D.TGRef (a, n))
74 | B.LRef (a, i) -> f (D.TLRef (a, i, 0))
76 let f uu tt = f (D.TCast (a, uu, tt)) in
77 let f uu = xlate_bk_term (f uu) t in
80 let f uu tt = f (D.TAppl (a, [uu], tt)) in
81 let f uu = xlate_bk_term (f uu) t in
84 let f bb tt = f (D.TBind (a, bb, tt)) in
85 let f bb = xlate_bk_term (f bb) t in
88 and xlate_bk_bind f = function
90 let f tt = f (D.Abst (n, [tt])) in
93 let f tt = f (D.Abbr [tt]) in
95 | B.Void -> f (D.Void 1)
97 (* interface functions ******************************************************)
100 f (xlate_term C.start t)
102 let crg_of_brg = xlate_bk_term