-(*
- ||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 (n, false, id, w, t) ->
- let tt = T.Bind (n, T.Abst [id, false, w], t) in
- contract f tt
- | T.Impl (n, true, id, w, t) ->
- let f = function
- | T.Bind (_, T.Abst [xw], T.Bind (n, T.Abst xws, tt)) ->
- f (T.Bind (n, T.Abst (xw :: xws), tt))
- | tt -> f tt
- in
- let tt = T.Impl (n, 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 (n, b, t) ->
- let f tt bb = f (T.Bind (n, 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