X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Flambda-delta%2Fsrc%2Fbasic_ag%2FbagCrg.ml;fp=helm%2Fsoftware%2Flambda-delta%2Fsrc%2Fbasic_ag%2FbagCrg.ml;h=d4366b60b37583c89377f84c077a568bdeae1ae1;hb=d145ea48ed0bdb9642ced01283231f3f13d476b8;hp=0000000000000000000000000000000000000000;hpb=e7f64fe2cc67f3514131c8831f87311ff600d005;p=helm.git

diff --git a/helm/software/lambda-delta/src/basic_ag/bagCrg.ml b/helm/software/lambda-delta/src/basic_ag/bagCrg.ml
new file mode 100644
index 000000000..d4366b60b
--- /dev/null
+++ b/helm/software/lambda-delta/src/basic_ag/bagCrg.ml
@@ -0,0 +1,102 @@
+(*
+    ||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 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 (Z.Sort (a, l))
+   | D.TGRef (a, n)     -> f (Z.GRef (a, n))
+   | D.TLRef (a, _, _)  -> let f i = f (Z.LRef (a, i)) in E.apix C.err f a
+   | D.TCast (a, u, t)  ->
+      let f uu tt = f (Z.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 (Z.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 (n, ws), D.TCast (ac, u, t)) ->
+      xlate_term f (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 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 = E.get_names f a in 
+   match b with
+      | D.Abst (m, ws) ->
+         let map x n w = 
+	    let f ww = Z.Bind (n :: J.new_mark () :: a, Z.Abst (m, 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 = Z.Bind (n :: a, Z.Abbr vv, x) in 
+	    xlate_term f v
+	 in
+	 List.fold_left2 map x ns vs
+      | D.Void _       ->
+         let map x n = Z.Bind (n :: a, Z.Void, x) in
+	 List.fold_left map x ns
+
+and xlate_proj x _ e =
+   lenv_fold_left xlate_bind xlate_proj x e
+
+(* internal functions: bag to crg term **************************************)
+
+let rec xlate_bk_term f = function
+   | Z.Sort (a, l)     -> f (D.TSort (a, l))
+   | Z.GRef (a, n)     -> f (D.TGRef (a, n))
+   | Z.LRef (a, i)     -> f (D.TLRef (a, i, 0))
+   | Z.Cast (a, u, t)  ->
+      let f uu tt = f (D.TCast (a, uu, tt)) in
+      let f uu = xlate_bk_term (f uu) t in
+      xlate_bk_term f u 
+   | Z.Appl (a, u, t)  ->
+      let f uu tt = f (D.TAppl (a, [uu], tt)) in
+      let f uu = xlate_bk_term (f uu) t in
+      xlate_bk_term f u 
+   | Z.Bind (a, b, t)  ->
+      let f bb tt = f (D.TBind (a, bb, tt)) in
+      let f bb = xlate_bk_term (f bb) t in
+      xlate_bk_bind f b
+
+and xlate_bk_bind f = function
+   | Z.Abst (n, t) ->
+      let f tt = f (D.Abst (n, [tt])) in
+      xlate_bk_term f t
+   | Z.Abbr t      ->
+      let f tt = f (D.Abbr [tt]) in
+      xlate_bk_term f t
+   | Z.Void        -> f (D.Void 1)
+   
+(* interface functions ******************************************************)
+
+let bag_of_crg f t =
+   f (xlate_term C.start t)
+
+let crg_of_bag = xlate_bk_term