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 bag term **************************************)
21 let rec shift t = function
23 | (a, l, b) :: c, _ :: ns -> shift (Z.Bind (a, l, b, t)) (c, ns)
26 let rec xlate_term xlate_bind f c = function
27 | D.TSort (_, h) -> f (Z.Sort h)
28 | D.TGRef (_, s) -> f (Z.GRef s)
29 | D.TLRef (a, _, _) ->
31 let _, l, _ = List.nth c i in
35 | D.TCast (_, u, t) ->
36 let f tt uu = f (Z.Cast (uu, tt)) in
37 let f tt = xlate_term xlate_bind (f tt) c u in
38 xlate_term xlate_bind f c t
39 | D.TAppl (_, vs, t) ->
40 let map f v tt = let f vv = f (Z.Appl (vv, tt)) in xlate_term xlate_bind f c v in
41 let f tt = C.list_fold_right f map vs tt in
42 xlate_term xlate_bind f c t
43 | D.TProj (_, e, t) ->
44 xlate_term xlate_bind f c (D.tshift e t)
45 (* this case should be removed by improving alpha-conversion *)
46 | D.TBind (ab, D.Abst (n, ws), D.TCast (ac, u, t)) ->
47 xlate_term xlate_bind f c (D.TCast (ac, D.TBind (ab, D.Abst (N.pred n, ws), u), D.TBind (ab, D.Abst (n, ws), t)))
48 | D.TBind (a, b, t) ->
50 let ns = E.get_names g a in
51 let cc = xlate_bind C.start c ns b in
52 let f tt = f (shift tt (cc, ns)) in
53 xlate_term xlate_bind f cc t
55 let rec xlate_bind f c ns = function
58 let f ww = Z.push "xlate_bind" f c [n] (J.new_location ()) (Z.Abst ww) in
59 xlate_term xlate_bind f c w
61 C.list_fold_right2 f map ns ws c
64 let f vv = Z.push "xlate_bind" f c [n] (J.new_location ()) (Z.Abbr vv) in
65 xlate_term xlate_bind f c v
67 C.list_fold_right2 f map ns vs c
69 let map f n c = Z.push "xlate_bind" f c [n] (J.new_location ()) Z.Void in
70 C.list_fold_right f map ns c
72 (* internal functions: bag to crg term **************************************)
74 let rec xlate_bk_term f c = function
75 | Z.Sort h -> f (D.TSort ([], h))
76 | Z.GRef s -> f (D.TGRef ([], s))
78 let f i = f (D.TLRef ([], i, 0)) in
81 let f tt uu = f (D.TCast ([], uu, tt)) in
82 let f tt = xlate_bk_term (f tt) c u in
85 let f tt uu = f (D.TAppl ([], [uu], tt)) in
86 let f tt = xlate_bk_term (f tt) c u in
88 | Z.Bind (a, l, b, t) ->
89 let f tt bb = f (D.TBind (a, bb, tt)) in
90 let f tt = xlate_bk_bind (f tt) c b in
91 let cc = Z.push "xlate_bk_term" C.start c a l b in
94 and xlate_bk_bind f c = function
96 let f tt = f (D.Abst (N.infinite, [tt])) in
99 let f tt = f (D.Abbr [tt]) in
101 | Z.Void -> f (D.Void 1)
103 (* interface functions ******************************************************)
106 xlate_term xlate_bind f Z.empty_lenv t
108 let crg_of_bag f t = xlate_bk_term f Z.empty_lenv t