refactoring ...

[helm.git] / helm / software / lambda-delta / dual_rg / drgBrg.ml

diff --git a/helm/software/lambda-delta/dual_rg/drgBrg.ml b/helm/software/lambda-delta/dual_rg/drgBrg.ml
deleted file mode 100644 (file)
index 9ff63fb..0000000
--- a/helm/software/lambda-delta/dual_rg/drgBrg.ml
+++ /dev/null
@@ -1,67 +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 Y = Entity
-module D = Drg
-module B = Brg
-
-let rec lenv_fold_left map1 map2 x = function
-   | D.ESort            -> x
-   | D.EBind (tl, a, b) -> lenv_fold_left map1 map2 (map1 x a b) tl
-   | D.EProj (tl, a, e) -> lenv_fold_left map1 map2 (map2 x a e) tl
-
-let rec xlate_term f = function
-   | D.TSort (a, l)     -> f (B.Sort (a, l))
-   | D.TGRef (a, n)     -> f (B.GRef (a, n))
-   | D.TLRef (a, _, _)  -> let f i = f (B.LRef (a, i)) in Y.apix C.err f a
-   | D.TCast (a, u, t)  ->
-      let f uu tt = f (B.Cast (a, uu, tt)) in
-      let f uu = xlate_term (f uu) t in
-      xlate_term f u 
-   | D.TAppl (a, vs, t) ->
-      let map f v tt = let f vv = f (B.Appl (a, vv, tt)) in xlate_term f v in
-      let f tt = C.list_fold_right f map vs tt in
-      xlate_term f t
-   | D.TProj (a, e, t)  ->
-      let f tt = f (lenv_fold_left xlate_bind xlate_proj tt e) in
-      xlate_term f t
-   | D.TBind (ab, D.Abst ws, D.TCast (ac, u, t)) ->
-      xlate_term f (D.TCast (ac, D.TBind (ab, D.Abst ws, u), D.TBind (ab, D.Abst ws, t)))
-   | D.TBind (a, b, t)  ->
-      let f tt = f (xlate_bind tt a b) in xlate_term f t
-
-and xlate_bind x a b =
-   let f a ns = a, ns in
-   let a, ns = Y.get_names f a in 
-   match b with
-      | D.Abst ws ->
-         let map x n w = 
-           let f ww = B.Bind (B.Abst (n :: a, ww), x) in xlate_term f w
-        in
-        List.fold_left2 map x ns ws 
-      | D.Abbr vs ->
-         let map x n v = 
-           let f vv = B.Bind (B.Abbr (n :: a, vv), x) in xlate_term f v
-        in
-        List.fold_left2 map x ns vs
-      | D.Void _  ->
-         let map x n = B.Bind (B.Void (n :: a), x) in
-        List.fold_left map x ns
-
-and xlate_proj x _ e =
-   lenv_fold_left xlate_bind xlate_proj x e
-
-let brg_of_drg f t =
-(*   
-   print_newline (); DrgOutput.pp_term print_string t;
-*)
-   f (xlate_term C.start t)