X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fhelena%2Fsrc%2Fautomath%2FautCrg.ml;h=5ed896306dfcf0558d6858ad499f57398b3f94f0;hb=f7d7f2459b3b0409be5f168822be3b836ccc929b;hp=637aa4a89ceec68233bae4a0584f90a12b764976;hpb=b37863d4598516a06241f18ad0db963399015bf2;p=helm.git

diff --git a/helm/software/helena/src/automath/autCrg.ml b/helm/software/helena/src/automath/autCrg.ml
index 637aa4a89..5ed896306 100644
--- a/helm/software/helena/src/automath/autCrg.ml
+++ b/helm/software/helena/src/automath/autCrg.ml
@@ -46,19 +46,19 @@ let alpha id =
 
 let attrs_for_abst id aw =
    let id = if !G.alpha <> "" then alpha id else id in
-   let main = E.succ aw.E.n_main in
-   E.node_attrs ~name:(id, true) ~side:aw.E.n_main ~main ()
+   let main = E.succ aw.E.b_main in
+   E.bind_attrs ~name:(id, true) ~side:aw.E.b_main ~main ()
 
 let attrs_for_decl aw =
-   let main = E.succ aw.E.n_main in
-   E.node_attrs ~side:aw.E.n_main ~main ()
+   let main = E.succ aw.E.b_main in
+   E.bind_attrs ~side:aw.E.b_main ~main ()
 
 let add_abst cnt id aw w =
-   let a = attrs_for_abst id aw in
+   let y = attrs_for_abst id aw in
    let l = if !G.infinity then N.infinity else N.two in
-   D.EBind (cnt, a, D.Abst (false, l, w))
+   D.EBind (cnt, E.empty_node, y, D.Abst (false, l, w))
 
-let mk_lref f a i = f a (D.TLRef (a, i))
+let mk_lref f _ y i = f y (D.TLRef (E.empty_node, i))
 
 let id_of_name (id, _, _) =
    if !G.alpha <> "" then alpha id else id
@@ -92,7 +92,7 @@ let relax_opt_qid f lst = function
    | Some qid -> let f qid = f (Some qid) in relax_qid f lst qid
 
 let resolve_gref err f lst qid =
-   try let a, cnt = UH.find henv (uri_of_qid qid) in f qid a cnt
+   try let y, cnt = UH.find henv (uri_of_qid qid) in f qid y cnt
    with Not_found -> err qid
 
 let resolve_gref_relaxed f lst qid =
@@ -111,40 +111,41 @@ let get_cnt_relaxed f lst =
    let rec err node = relax_opt_qid (get_cnt err f lst) lst node in
    get_cnt err f lst lst.node
 
-let push_abst f a w lenv =
+let push_abst f y w lenv =
    let bw = D.Abst (false, N.infinity, w) in
-   D.push_bind f a bw lenv
-
-let add_proj at e t = match e with
-   | D.ESort                 -> t
-   | D.EBind (D.ESort, a, b) -> D.TBind (E.compose a at, b, t) 
-   | _                       ->
-IFDEF MANAGER OR OBJS THEN
-      D.TProj (at, D.set_attrs C.start at e, t)
-ELSE
-      D.TProj (at, e, t)
-END
+   D.push_bind f E.empty_node y bw lenv
+(*
+let rec set_name_y f = function
+   | D.ESort              -> f D.ESort
+   | D.EBind (e, a, y, b) -> set_name_y (D.push_bind f a {y with E.b_name = Some ("Y", true)} b) e
+   | D.EAppl (e, x, v)    -> set_name_y (D.push_appl f x v) e
+   | D.EProj (e, d)       -> let f d = set_name_y (D.push_proj f d) e in set_name_y f d
+*)
+let add_proj yt e t = match e with
+   | D.ESort                    -> t
+   | D.EBind (D.ESort, _, y, b) -> D.TBind (E.compose y yt, b, t) 
+   | e                          ->
+      D.TProj (D.set_attrs C.start yt e, t)
 
 (* this is not tail recursive in the GRef branch *)
-let rec xlate_term f st lst y lenv = function
+let rec xlate_term f st lst z lenv = function
    | A.Sort s            ->
-      let h = if s then 0 else 1 in
-      let a = E.node_attrs ~main:(h, 0) () in
-      f a (D.TSort (a, h))
+      let k = if s then 0 else 1 in
+      let y = E.bind_attrs ~main:(k, 0) () in
+      f y (D.TSort k)
    | A.Appl (v, t)       ->
-      let f av vv at tt =
-         let at = E.compose av at in
-         f at (D.TAppl (at, !G.extended, vv, tt))
+      let f vv yt tt =
+         f yt (D.TAppl (!G.extended, vv, tt))
       in
-      let f av vv = xlate_term (f av vv) st lst y lenv t in
+      let f _ vv = xlate_term (f vv) st lst z lenv t in
       xlate_term f st lst false lenv v
    | A.Abst (name, w, t) ->
-      let f aw ww =
-         let aw = attrs_for_abst name aw in
-         let f at tt =
-	    let at = E.compose aw at in
+      let f yw ww =
+         let yw = attrs_for_abst name yw in
+         let f yt tt =
+	    let yt = E.compose yw yt in
             let l = 
-               if !G.cc then match y, snd at.E.n_main with
+               if !G.cc then match z, snd yt.E.b_main with
                   | true, _ -> N.one
                   | _   , 0 -> N.one
                   | _   , 1 -> N.unknown st
@@ -153,31 +154,25 @@ let rec xlate_term f st lst y lenv = function
                else N.infinity
             in
 	    let b = D.Abst (false, l, ww) in
-	    f at (D.TBind (at, b, tt))
+(*            let yt = {yt with E.b_name = Some ("P", true)} in *)
+	    f yt (D.TBind (yt, b, tt))
 	 in
-         let f lenv = xlate_term f st lst y lenv t in
-	 push_abst f aw ww lenv
+         let f lenv = xlate_term f st lst z lenv t in
+	 push_abst f yw ww lenv
       in
       xlate_term f st lst true lenv w
    | A.GRef (name, args) ->
       let map1 args (id, _) = A.GRef ((id, true, []), []) :: args in
       let map2 f arg args = 
-         let f av v = f (D.EAppl (args, E.shift av, !G.extended, v)) in 
+         let f _ v = f (D.EAppl (args, !G.extended, v)) in 
          xlate_term f st lst false lenv arg
       in
-      let g qid a cnt =
-         let gref = D.TGRef (a, uri_of_qid qid) in
-	 if cnt = D.ESort then f a gref else
+      let g qid y cnt =
+         let gref = D.TGRef (E.empty_node, uri_of_qid qid) in
+	 if cnt = D.ESort then f y gref else
 	 let f = function 
-            | D.EAppl (D.ESort, av, x, v) ->
-               let a = E.compose av a in
-               f a (D.TAppl (a, x, v, gref))
-            | args                        ->
-IFDEF MANAGER OR OBJS THEN
-               f a (D.TProj (a, D.set_attrs C.start a args, gref))
-ELSE               
-               f a (D.TProj (a, args, gref))
-END
+            | D.EAppl (D.ESort, x, v) -> f y (D.TAppl (x, v, gref))
+            | args                    -> f y (D.TProj (args, gref))
          in
 	 let f args = C.list_fold_right f map2 args D.ESort in
 	 D.sub_list_strict (D.fold_names f map1 args) cnt args
@@ -215,16 +210,15 @@ let xlate_entity err f st lst = function
    | A.Decl (name, w)          ->
       let f lenv =
 	 let f qid = 
-            let f aw ww =
-               let a = attrs_for_decl aw in
-               UH.add henv (uri_of_qid qid) (a, lenv);
-	       let t = add_proj aw lenv ww in
-(*
-	    print_newline (); CrgOutput.pp_term print_string t;
-*)
-               let na = {aw with E.n_apix = lst.line} in
+            let f yw ww =
+               let y = attrs_for_decl yw in
+               UH.add henv (uri_of_qid qid) (y, lenv);
+	       let t = add_proj yw lenv ww in
+               let na = E.node_attrs ~apix:lst.line () in
 	       let entity = E.empty_root, na, uri_of_qid qid, E.Abst t in
-               G.set_current_trace lst.line;
+IFDEF TRACE THEN
+               G.set_current_trace lst.line
+ELSE () END;
 	       f {lst with line = succ lst.line} entity
 	    in
 	    xlate_term f st lst true lenv w
@@ -236,17 +230,20 @@ let xlate_entity err f st lst = function
    | A.Def (name, w, trans, v) ->
       let f lenv =
          let f qid = 
-            let f _ ww =
-	       let f av vv =
-                  UH.add henv (uri_of_qid qid) (av, lenv);
-                  let t = add_proj av lenv (D.TCast (av, ww, vv)) in
+            let f yw ww =
+	       let f yv vv =
+                  UH.add henv (uri_of_qid qid) (yv, lenv);
+                  let t = add_proj yv lenv (D.TCast (ww, vv)) in
 (*
-	    print_newline (); CrgOutput.pp_term print_string t;
+                  let lenv0 = D.set_layer C.start N.one lenv in
+                  let t = D.TCast (add_proj yw lenv0 ww, add_proj yv lenv vv) in
 *)
-                  let na = {av with E.n_apix = lst.line} in
+                  let na = E.node_attrs ~apix:lst.line () in
                   let ra = if trans then E.empty_root else E.root_attrs ~meta:[E.Private] () in
 	          let entity = ra, na, uri_of_qid qid, E.Abbr t in
-                  G.set_current_trace lst.line;
+IFDEF TRACE THEN
+                  G.set_current_trace lst.line
+ELSE () END;
 	          f {lst with line = succ lst.line} entity
 	       in
 	       xlate_term f st lst false lenv v