+(*
+ ||M|| This file is part of HELM, an Hypertextual, Electronic
+ ||A|| Library of Mathematics, developed at the Computer Science
+ ||T|| Department, University of Bologna, Italy.
+ ||I||
+ ||T|| HELM is free software; you can redistribute it and/or
+ ||A|| modify it under the terms of the GNU General Public License
+ \ / version 2 or (at your option) any later version.
+ \ / This software is distributed as is, NO WARRANTY.
+ V_______________________________________________________________ *)
+
+module C = Cps
+module T = Txt
+
+(* Interface functions ******************************************************)
+
+let rec contract f = function
+ | T.Inst (t, vs) ->
+ let tt = T.Appl (List.rev vs, t) in
+ contract f tt
+ | T.Impl (false, id, w, t) ->
+ let tt = T.Bind (T.Abst [id, false, w], t) in
+ contract f tt
+ | T.Impl (true, id, w, t) ->
+ let f = function
+ | T.Bind (T.Abst [xw], T.Bind (T.Abst xws, tt)) ->
+ f (T.Bind (T.Abst (xw :: xws), tt))
+ | tt -> f tt
+ in
+ let tt = T.Impl (false, id, w, t) in
+ contract f tt
+ | T.Sort _
+ | T.NSrt _
+ | T.LRef _
+ | T.NRef _ as t -> f t
+ | T.Cast (u, t) ->
+ let f tt uu = f (T.Cast (uu, tt)) in
+ let f tt = contract (f tt) u in
+ contract f t
+ | T.Appl (vs, t) ->
+ let f tt vvs = f (T.Appl (vvs, tt)) in
+ let f tt = C.list_map (f tt) contract vs in
+ contract f t
+ | T.Bind (b, t) ->
+ let f tt bb = f (T.Bind (bb, tt)) in
+ let f tt = contract_binder (f tt) b in
+ contract f t
+
+and contract_binder f = function
+ | T.Void n as b -> f b
+ | T.Abbr xvs ->
+ let map f (id, v) =
+ let f vv = f (id, vv) in contract f v
+ in
+ let f xvvs = f (T.Abbr xvvs) in
+ C.list_map f map xvs
+ | T.Abst xws ->
+ let map f (id, real, w) =
+ let f ww = f (id, real, ww) in contract f w
+ in
+ let f xwws = f (T.Abst xwws) in
+ C.list_map f map xws
+