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_______________________________________________________________ *)
15 (* Interface functions ******************************************************)
17 let rec contract f = function
19 let tt = T.Appl (List.rev vs, t) in
21 | T.Impl (n, false, id, w, t) ->
22 let tt = T.Bind (n, T.Abst [id, false, w], t) in
24 | T.Impl (n, true, id, w, t) ->
26 | T.Bind (_, T.Abst [xw], T.Bind (n, T.Abst xws, tt)) ->
27 f (T.Bind (n, T.Abst (xw :: xws), tt))
30 let tt = T.Impl (n, false, id, w, t) in
35 | T.NRef _ as t -> f t
37 let f tt uu = f (T.Cast (uu, tt)) in
38 let f tt = contract (f tt) u in
41 let f tt vvs = f (T.Appl (vvs, tt)) in
42 let f tt = C.list_map (f tt) contract vs in
45 let f tt bb = f (T.Bind (n, bb, tt)) in
46 let f tt = contract_binder (f tt) b in
49 and contract_binder f = function
50 | T.Void n as b -> f b
53 let f vv = f (id, vv) in contract f v
55 let f xvvs = f (T.Abbr xvvs) in
58 let map f (id, real, w) =
59 let f ww = f (id, real, ww) in contract f w
61 let f xwws = f (T.Abst xwws) in