refactoring ...

[helm.git] / helm / software / helena / src / basic_ag / bagCrg.ml

diff --git a/helm/software/helena/src/basic_ag/bagCrg.ml b/helm/software/helena/src/basic_ag/bagCrg.ml
new file mode 100644 (file)
index 0000000..8fbf7cf
--- /dev/null
+++ b/helm/software/helena/src/basic_ag/bagCrg.ml
@@ -0,0 +1,108 @@
+(*
+    ||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 E = Entity
+module J = Marks
+module N = Level
+module D = Crg
+module Z = Bag
+
+(* internal functions: crg to bag term **************************************)
+
+let rec shift t = function
+   | _, []                    -> t
+   | (a, l, b) :: c, _ :: ns -> shift (Z.Bind (a, l, b, t)) (c, ns)
+   | _                        -> assert false
+
+let rec xlate_term xlate_bind f c = function
+   | D.TSort (_, h)     -> f (Z.Sort h)
+   | D.TGRef (_, s)     -> f (Z.GRef s)
+   | D.TLRef (a, _, _)  -> 
+      let f i = 
+         let _, l, _ = List.nth c i in 
+        f (Z.LRef l)
+      in 
+      E.apix C.err f a
+   | D.TCast (_, u, t)  ->
+      let f tt uu = f (Z.Cast (uu, tt)) in
+      let f tt = xlate_term xlate_bind (f tt) c u in
+      xlate_term xlate_bind f c t
+   | D.TAppl (_, vs, t) ->
+      let map f v tt = let f vv = f (Z.Appl (vv, tt)) in xlate_term xlate_bind f c v in
+      let f tt = C.list_fold_right f map vs tt in
+      xlate_term xlate_bind f c t
+   | D.TProj (_, e, t)  ->
+      xlate_term xlate_bind f c (D.tshift e t)
+(* this case should be removed by improving alpha-conversion *)
+   | D.TBind (ab, D.Abst (n, ws), D.TCast (ac, u, t)) ->
+      xlate_term xlate_bind f c (D.TCast (ac, D.TBind (ab, D.Abst (N.pred n, ws), u), D.TBind (ab, D.Abst (n, ws), t)))
+   | D.TBind (a, b, t)  ->
+      let g _ ns = ns in
+      let ns = E.get_names g a in  
+      let cc = xlate_bind C.start c ns b in
+      let f tt = f (shift tt (cc, ns)) in
+      xlate_term xlate_bind f cc t
+
+let rec xlate_bind f c ns = function
+   | D.Abst (_, ws) ->
+      let map f n w c =
+         let f ww = Z.push "xlate_bind" f c [n] (J.new_location ()) (Z.Abst ww) in 
+        xlate_term xlate_bind f c w
+      in
+      C.list_fold_right2 f map ns ws c
+   | D.Abbr vs      ->
+      let map f n v c = 
+        let f vv = Z.push "xlate_bind" f c [n] (J.new_location ()) (Z.Abbr vv) in
+        xlate_term xlate_bind f c v
+      in
+      C.list_fold_right2 f map ns vs c
+   | D.Void _       ->
+      let map f n c = Z.push "xlate_bind" f c [n] (J.new_location ()) Z.Void in
+      C.list_fold_right f map ns c
+
+(* internal functions: bag to crg term **************************************)
+
+let rec xlate_bk_term f c = function
+   | Z.Sort h            -> f (D.TSort ([], h))
+   | Z.GRef s            -> f (D.TGRef ([], s))
+   | Z.LRef l            -> 
+       let f i = f (D.TLRef ([], i, 0)) in
+       Z.nth C.err f l c
+   | Z.Cast (u, t)  ->
+      let f tt uu = f (D.TCast ([], uu, tt)) in
+      let f tt = xlate_bk_term (f tt) c u in
+      xlate_bk_term f c t 
+   | Z.Appl (u, t)       ->
+      let f tt uu = f (D.TAppl ([], [uu], tt)) in
+      let f tt = xlate_bk_term (f tt) c u in
+      xlate_bk_term f c t 
+   | Z.Bind (a, l, b, t) ->
+      let f tt bb = f (D.TBind (a, bb, tt)) in      
+      let f tt = xlate_bk_bind (f tt) c b in
+      let cc = Z.push "xlate_bk_term" C.start c a l b in
+      xlate_bk_term f cc t
+
+and xlate_bk_bind f c = function
+   | Z.Abst t ->
+      let f tt = f (D.Abst (N.infinite, [tt])) in
+      xlate_bk_term f c t
+   | Z.Abbr t ->
+      let f tt = f (D.Abbr [tt]) in
+      xlate_bk_term f c t
+   | Z.Void   -> f (D.Void 1)
+
+(* interface functions ******************************************************)
+
+let bag_of_crg f t =
+   xlate_term xlate_bind f Z.empty_lenv t
+
+let crg_of_bag f t = xlate_bk_term f Z.empty_lenv t