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 xlate_term st f c = function
22 | D.TSort (_, h) -> f (Z.Sort h)
23 | D.TGRef (_, s) -> f (Z.GRef s)
25 let _, l, _ = List.nth c i in f (Z.LRef l)
26 | D.TCast (_, u, t) ->
27 let f tt uu = f (Z.Cast (uu, tt)) in
28 let f tt = xlate_term st (f tt) c u in
30 | D.TAppl (_, v, t) ->
31 let f tt vv = f (Z.Appl (vv, tt)) in
32 let f tt = xlate_term st (f tt) c v in
34 | D.TProj (_, e, t) ->
35 D.shift (xlate_term st f c) e t
36 (* this case should be removed by improving alpha-conversion *)
37 | D.TBind (ab, D.Abst (n, ws), D.TCast (ac, u, t)) ->
38 xlate_term st f c (D.TCast (ac, D.TBind (ab, D.Abst (N.minus st n 1, ws), u), D.TBind (ab, D.Abst (n, ws), t)))
39 | D.TBind (a, b, t) ->
41 let a, l, b = List.hd cc in
42 let f tt = f (Z.Bind (a, l, b, tt)) in
47 and xlate_bind st f c a = function
49 let f ww = Z.push "xlate_bind" f c a (P.new_mark ()) (Z.Abst ww) in
52 let f vv = Z.push "xlate_bind" f c a (P.new_mark ()) (Z.Abbr vv) in
55 Z.push "xlate_bind" f c a (P.new_mark ()) Z.Void
57 (* internal functions: bag to crg term **************************************)
59 let rec xlate_bk_term f c = function
60 | Z.Sort h -> f (D.TSort (E.empty_node, h))
61 | Z.GRef s -> f (D.TGRef (E.empty_node, s))
63 let f i = f (D.TLRef (E.empty_node, i)) in
66 let f tt uu = f (D.TCast (E.empty_node, uu, tt)) in
67 let f tt = xlate_bk_term (f tt) c u in
70 let f tt uu = f (D.TAppl (E.empty_node, uu, tt)) in
71 let f tt = xlate_bk_term (f tt) c u in
73 | Z.Bind (a, l, b, t) ->
74 let f tt bb = f (D.TBind (a, bb, tt)) in
75 let f tt = xlate_bk_bind (f tt) c b in
76 let cc = Z.push "xlate_bk_term" C.start c a l b in
79 and xlate_bk_bind f c = function
81 let f tt = f (D.Abst (N.infinite, tt)) in
84 let f tt = f (D.Abbr tt) in
88 (* interface functions ******************************************************)
90 let bag_of_crg st f t =
91 xlate_term st f Z.empty_lenv t
93 let crg_of_bag f t = xlate_bk_term f Z.empty_lenv t