X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fhelena%2Fsrc%2Fbasic_ag%2FbagCrg.ml;h=31ce2afa549b0e36ff92d14714aacc5cf5dd1262;hb=88977b2d546e547e23b046792fe2ad8f6ff192a4;hp=9724290f930fae807383420ba90713a658ba5ec9;hpb=977faf4820cd8ff5e2f0a5249161bbb92ae4b097;p=helm.git

diff --git a/helm/software/helena/src/basic_ag/bagCrg.ml b/helm/software/helena/src/basic_ag/bagCrg.ml
index 9724290f9..31ce2afa5 100644
--- a/helm/software/helena/src/basic_ag/bagCrg.ml
+++ b/helm/software/helena/src/basic_ag/bagCrg.ml
@@ -10,75 +10,75 @@
       V_______________________________________________________________ *)
 
 module C = Cps
+module P = Marks
+module N = Layer
 module E = Entity
-module J = Marks
-module N = Level
 module D = Crg
 module Z = Bag
 
 (* internal functions: crg to bag term **************************************)
 
-let rec xlate_term f c = function
-   | D.TSort (_, h)    -> f (Z.Sort h)
+let rec xlate_term st f c = function
+   | D.TSort k         -> f (Z.Sort k)
    | D.TGRef (_, s)    -> f (Z.GRef s)
-   | D.TLRef (a, i)    ->
+   | D.TLRef (_, i)    ->
       let _, l, _ = List.nth c i in f (Z.LRef l)
-   | D.TCast (_, u, t) ->
+   | D.TCast (u, t)    ->
       let f tt uu = f (Z.Cast (uu, tt)) in
-      let f tt = xlate_term (f tt) c u in
-      xlate_term f c t
+      let f tt = xlate_term st (f tt) c u in
+      xlate_term st f c t
    | D.TAppl (_, v, t) ->
       let f tt vv = f (Z.Appl (vv, tt)) in
-      let f tt = xlate_term (f tt) c v in
-      xlate_term f c t
-   | D.TProj (_, e, t) ->
-      D.shift (xlate_term f c) e t
+      let f tt = xlate_term st (f tt) c v in
+      xlate_term st f c t
+   | D.TProj (e, t)    ->
+      D.shift (xlate_term st f c) 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 f c (D.TCast (ac, D.TBind (ab, D.Abst (N.minus n 1, ws), u), D.TBind (ab, D.Abst (n, ws), t)))
-   | D.TBind (a, b, t) ->
+   | D.TBind (y, D.Abst (x, n, ws), D.TCast (u, t)) ->
+      xlate_term st f c (D.TCast (D.TBind (y, D.Abst (x, N.minus st n 1, ws), u), D.TBind (y, D.Abst (x, n, ws), t)))
+   | D.TBind (y, b, t) ->
       let f cc =
          let a, l, b = List.hd cc in
          let f tt = f (Z.Bind (a, l, b, tt)) in
-         xlate_term f cc t
+         xlate_term st f cc t
       in
-      xlate_bind f c a b
+      xlate_bind st f c y b
 
-and xlate_bind f c a = function
-   | D.Abst (_, w) ->
-      let f ww = Z.push "xlate_bind" f c a (J.new_mark ()) (Z.Abst ww) in 
-      xlate_term f c w
-   | D.Abbr v      -> 
-      let f vv = Z.push "xlate_bind" f c a (J.new_mark ()) (Z.Abbr vv) in
-      xlate_term f c v
-   | D.Void        ->
-      Z.push "xlate_bind" f c a (J.new_mark ()) Z.Void
+and xlate_bind st f c y = function
+   | D.Abst (_, _, w) ->
+      let f ww = Z.push "xlate_bind" f c y (P.new_mark ()) (Z.Abst ww) in 
+      xlate_term st f c w
+   | D.Abbr v         -> 
+      let f vv = Z.push "xlate_bind" f c y (P.new_mark ()) (Z.Abbr vv) in
+      xlate_term st f c v
+   | D.Void           ->
+      Z.push "xlate_bind" f c y (P.new_mark ()) Z.Void
 
 (* internal functions: bag to crg term **************************************)
 
 let rec xlate_bk_term f c = function
-   | Z.Sort h            -> f (D.TSort (E.empty_node, h))
+   | Z.Sort k            -> f (D.TSort k)
    | Z.GRef s            -> f (D.TGRef (E.empty_node, s))
    | Z.LRef l            -> 
        let f i = f (D.TLRef (E.empty_node, i)) in
        Z.nth C.err f l c
    | Z.Cast (u, t)  ->
-      let f tt uu = f (D.TCast (E.empty_node, uu, tt)) in
+      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 (E.empty_node, uu, tt)) in
+      let f tt uu = f (D.TAppl (E.appl_attrs false, 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      
+   | Z.Bind (y, l, b, t) ->
+      let f tt bb = f (D.TBind (y, 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
+      let cc = Z.push "xlate_bk_term" C.start c y 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
+      let f tt = f (D.Abst (false, N.infinity, tt)) in
       xlate_bk_term f c t
    | Z.Abbr t ->
       let f tt = f (D.Abbr tt) in
@@ -87,7 +87,7 @@ and xlate_bk_bind f c = function
 
 (* interface functions ******************************************************)
 
-let bag_of_crg f t =
-   xlate_term f Z.empty_lenv t
+let bag_of_crg st f t =
+   xlate_term st f Z.empty_lenv t
 
 let crg_of_bag f t = xlate_bk_term f Z.empty_lenv t