minor bug fixes ...

[helm.git] / helm / software / helena / src / automath / autCrg.ml

diff --git a/helm/software/helena/src/automath/autCrg.ml b/helm/software/helena/src/automath/autCrg.ml
index 7a6600898b3def2e7321114dd93f9374bbf9b7f7..5ed896306dfcf0558d6858ad499f57398b3f94f0 100644 (file)
--- a/helm/software/helena/src/automath/autCrg.ml
+++ b/helm/software/helena/src/automath/autCrg.ml
@@ -114,11 +114,17 @@ let get_cnt_relaxed f lst =
 let push_abst f y w lenv =
    let bw = D.Abst (false, N.infinity, w) in
    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 *)
@@ -148,6 +154,7 @@ let rec xlate_term f st lst z lenv = function
                else N.infinity
             in
            let b = D.Abst (false, l, ww) in
+(*            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 z lenv t in
@@ -207,12 +214,11 @@ let xlate_entity err f st lst = function
                let y = attrs_for_decl yw in
                UH.add henv (uri_of_qid qid) (y, lenv);
               let t = add_proj yw lenv ww in
-(*
-           print_newline (); CrgOutput.pp_term print_string t;
-*)
                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
@@ -224,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 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 = 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