- bug fix in the static disambiguation of unified binders

[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 0a7a46de47a21f762db9bf6b56181c8ee535437a..2bfef6b0f458d37ead69e28cb4589b8f933599ec 100644 (file)
--- a/helm/software/helena/src/automath/autCrg.ml
+++ b/helm/software/helena/src/automath/autCrg.ml
@@ -9,15 +9,15 @@
      \ /   This software is distributed as is, NO WARRANTY.              
       V_______________________________________________________________ *)
 
-module U = NUri
-module K = U.UriHash
-module C = Cps
-module N = Level
-module E = Entity
-module G = Options
-module S = Status
-module A = Aut
-module D = Crg
+module U  = NUri
+module UH = U.UriHash
+module C  = Cps
+module G  = Options
+module N  = Level
+module E  = Entity
+module S  = Status
+module A  = Aut
+module D  = Crg
 
 (* qualified identifier: uri, name, qualifiers *)
 type qid = D.uri * D.id * D.id list
@@ -34,9 +34,9 @@ type status = {
 
 let henv_size, hcnt_size = 7000, 4300 (* hash tables initial sizes *)
 
-let henv = K.create henv_size (* optimized global environment *)
+let henv = UH.create henv_size (* optimized global environment *)
 
-let hcnt = K.create hcnt_size (* optimized context *)
+let hcnt = UH.create hcnt_size (* optimized context *)
 
 (* Internal functions *******************************************************)
 
@@ -79,7 +79,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 = K.find henv (uri_of_qid qid) in f qid a cnt
+   try let a, cnt = UH.find henv (uri_of_qid qid) in f qid a cnt
    with Not_found -> err qid
 
 let resolve_gref_relaxed f lst qid =
@@ -90,7 +90,7 @@ let resolve_gref_relaxed f lst qid =
 let get_cnt err f lst = function
    | None             -> f empty_cnt
    | Some qid as node ->
-      try let cnt = K.find hcnt (uri_of_qid qid) in f cnt
+      try let cnt = UH.find hcnt (uri_of_qid qid) in f cnt
       with Not_found -> err node
 
 let get_cnt_relaxed f lst =
@@ -117,10 +117,11 @@ let rec xlate_term f st lst y lenv = function
       let f _ vv = xlate_term (f vv) st lst y lenv t in
       xlate_term f st lst false lenv v
    | A.Abst (name, w, t) ->
-      let f d ww = 
+      let f dw ww = 
          let a = E.node_attrs ~name:(name, true) () in
-        let f d tt =
-            let l = if !G.cc then match y, d with
+         let f dt tt =
+(*         let a = {a with E.n_degr = dt} in *)
+            let l = if !G.cc then match y, dt with
                | true, _ -> N.one
                | _   , 0 -> N.one
                | _   , 1 -> N.unknown st.S.lenv
@@ -129,10 +130,10 @@ let rec xlate_term f st lst y lenv = function
                else N.infinite
             in
            let b = D.Abst (l, ww) in
-           f d (D.TBind (a, b, tt))
+           f dt (D.TBind (a, b, tt))
         in
          let f lenv = xlate_term f st lst y lenv t in
-        push_abst f {a with E.n_degr = succ d} ww lenv
+        push_abst f {a with E.n_degr = succ dw} ww lenv
       in
       xlate_term f st lst true lenv w
    | A.GRef (name, args) ->
@@ -145,7 +146,7 @@ let rec xlate_term f st lst y lenv = function
          let gref = D.TGRef (a, uri_of_qid qid) in
         if cnt = D.ESort then f a.E.n_degr gref else
         let f = function 
-            | D.EAppl (D.ESort, a, v) -> f a.E.n_degr (D.TAppl (a, v, gref))
+            | D.EAppl (D.ESort, b, v) -> f a.E.n_degr (D.TAppl (b, v, gref))
             | args                    -> f a.E.n_degr (D.TProj (E.empty_node, args, gref))
          in
         let f args = C.list_fold_right f map2 args D.ESort in
@@ -173,7 +174,7 @@ let xlate_entity err f st lst = function
       let f qid = 
          let f cnt =
            let f d ww = 
-              K.add hcnt (uri_of_qid qid) (add_abst cnt name d ww);
+              UH.add hcnt (uri_of_qid qid) (add_abst cnt name d ww);
               err {lst with node = Some qid}
            in
            xlate_term f st lst true cnt w
@@ -186,7 +187,7 @@ let xlate_entity err f st lst = function
         let f qid = 
             let f d ww =
                let a = E.node_attrs ~apix:lst.line ~degr:(succ d) () in
-               K.add henv (uri_of_qid qid) (a, lenv);
+               UH.add henv (uri_of_qid qid) (a, lenv);
               let t = add_proj lenv ww in
 (*
            print_newline (); CrgOutput.pp_term print_string t;
@@ -206,7 +207,7 @@ let xlate_entity err f st lst = function
             let f _ ww =
               let f d vv =
                   let na = E.node_attrs ~apix:lst.line ~degr:d () in
-                  K.add henv (uri_of_qid qid) (na, lenv);
+                  UH.add henv (uri_of_qid qid) (na, lenv);
                   let t = add_proj lenv (D.TCast (E.empty_node, ww, vv)) in
 (*
            print_newline (); CrgOutput.pp_term print_string t;
@@ -227,7 +228,7 @@ let xlate_entity err f st lst = function
 (* Interface functions ******************************************************)
 
 let initial_status () =
-   K.clear henv; K.clear hcnt; {
+   UH.clear henv; UH.clear hcnt; {
    path = []; node = None; nodes = []; line = 1; mk_uri = G.get_mk_uri ();
 }