refactoring ...

[helm.git] / helm / software / lambda-delta / src / text / txtTxt.ml

diff --git a/helm/software/lambda-delta/src/text/txtTxt.ml b/helm/software/lambda-delta/src/text/txtTxt.ml
deleted file mode 100644 (file)
index fe09884..0000000
--- a/helm/software/lambda-delta/src/text/txtTxt.ml
+++ /dev/null
@@ -1,62 +0,0 @@
-(*
-    ||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