(*
    ||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