X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Flambda-delta%2Fsrc%2Fbasic_rg%2FbrgCrg.ml;fp=helm%2Fsoftware%2Flambda-delta%2Fsrc%2Fbasic_rg%2FbrgCrg.ml;h=2b3129339e9a6acb41b69cbf831f6da03e53b364;hb=fb74956a335a9cc38a6ced92e16256f10c4eed6e;hp=0000000000000000000000000000000000000000;hpb=ab13cfa248f0ee58d239ceeddfb50ec49a6b5c6d;p=helm.git

diff --git a/helm/software/lambda-delta/src/basic_rg/brgCrg.ml b/helm/software/lambda-delta/src/basic_rg/brgCrg.ml
new file mode 100644
index 000000000..2b3129339
--- /dev/null
+++ b/helm/software/lambda-delta/src/basic_rg/brgCrg.ml
@@ -0,0 +1,101 @@
+(*
+    ||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 M = Marks
+module D = Crg
+module B = Brg
+
+(* internal functions: crg to brg 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 (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 (n :: M.new_mark () :: a, B.Abst 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 (n :: a, B.Abbr vv, x) in 
+	    xlate_term f v
+	 in
+	 List.fold_left2 map x ns vs
+      | D.Void _  ->
+         let map x n = B.Bind (n :: a, B.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: brg to crg term **************************************)
+
+let rec xlate_bk_term f = function
+   | B.Sort (a, l)     -> f (D.TSort (a, l))
+   | B.GRef (a, n)     -> f (D.TGRef (a, n))
+   | B.LRef (a, i)     -> f (D.TLRef (a, i, 0))
+   | B.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 
+   | B.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 
+   | B.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
+   | B.Abst t ->
+      let f tt = f (D.Abst [tt]) in
+      xlate_bk_term f t
+   | B.Abbr t ->
+      let f tt = f (D.Abbr [tt]) in
+      xlate_bk_term f t
+   | B.Void   -> f (D.Void 1)
+   
+(* interface functions ******************************************************)
+
+let brg_of_crg f t =
+   f (xlate_term C.start t)
+
+let crg_of_brg = xlate_bk_term