hints polished and fixed to allow recursive inference of ext_carr

[helm.git] / helm / software / lambda-delta / src / complete_rg / crgAut.ml

diff --git a/helm/software/lambda-delta/src/complete_rg/crgAut.ml b/helm/software/lambda-delta/src/complete_rg/crgAut.ml
index 0b95adf41569b16aee67026be901a4d04c6899b6..2221c3c06a88ff4b925f2d0ac9b43c8dd41d6c92 100644 (file)
--- a/helm/software/lambda-delta/src/complete_rg/crgAut.ml
+++ b/helm/software/lambda-delta/src/complete_rg/crgAut.ml
@@ -10,17 +10,17 @@
       V_______________________________________________________________ *)
 
 module U = NUri
-module H = U.UriHash
+module K = U.UriHash
 module C = Cps
-module O = Options
-module Y = Entity
+module G = Options
+module E = Entity
 module A = Aut
 module D = Crg
 
 (* qualified identifier: uri, name, qualifiers *)
 type qid = D.uri * D.id * D.id list
 
-type context = Y.attrs * D.term list
+type context = E.attrs * D.term list
 
 type context_node = qid option (* context node: None = root *)
 
@@ -29,7 +29,7 @@ type status = {
    node: context_node;       (* current context node *)
    nodes: context_node list; (* context node list *)
    line: int;                (* line number *)
-   mk_uri:O.uri_generator    (* uri generator *) 
+   mk_uri:G.uri_generator    (* uri generator *) 
 }
 
 type resolver = Local of int
@@ -37,21 +37,21 @@ type resolver = Local of int
 
 let henv_size, hcnt_size = 7000, 4300 (* hash tables initial sizes *)
 
-let henv = H.create henv_size (* optimized global environment *)
+let henv = K.create henv_size (* optimized global environment *)
 
-let hcnt = H.create hcnt_size (* optimized context *)
+let hcnt = K.create hcnt_size (* optimized context *)
 
 (* Internal functions *******************************************************)
 
 let empty_cnt = [], []
 
 let add_abst (a, ws) id w = 
-   Y.Name (id, true) :: a, w :: ws 
+   E.Name (id, true) :: a, w :: ws 
 
 let lenv_of_cnt (a, ws) = 
    D.push_bind C.start D.empty_lenv a (D.Abst ws)
 
-let mk_lref f i j k = f (D.TLRef ([Y.Apix k], i, j))
+let mk_lref f i j k = f (D.TLRef ([E.Apix k], i, j))
 
 let id_of_name (id, _, _) = id
 
@@ -84,7 +84,7 @@ let relax_opt_qid f st = function
    | Some qid -> let f qid = f (Some qid) in relax_qid f st qid
 
 let resolve_gref err f st qid =
-   try let cnt = H.find henv (uri_of_qid qid) in f qid cnt
+   try let cnt = K.find henv (uri_of_qid qid) in f qid cnt
    with Not_found -> err qid 
 
 let resolve_gref_relaxed f st qid =
@@ -95,7 +95,7 @@ let resolve_gref_relaxed f st qid =
 let get_cnt err f st = function
    | None              -> f empty_cnt
    | Some qid as node ->
-      try let cnt = H.find hcnt (uri_of_qid qid) in f cnt
+      try let cnt = K.find hcnt (uri_of_qid qid) in f cnt
       with Not_found -> err node
 
 let get_cnt_relaxed f st =
@@ -114,7 +114,7 @@ let rec xlate_term f st lenv = function
       xlate_term f st lenv v
    | A.Abst (name, w, t) ->
       let f ww = 
-         let a, b = [Y.Name (name, true)], (D.Abst [ww]) in
+         let a, b = [E.Name (name, true)], (D.Abst [ww]) in
         let f tt = f (D.TBind (a, b, tt)) in
          let f lenv = xlate_term f st lenv t in
         D.push_bind f lenv a b
@@ -122,7 +122,7 @@ let rec xlate_term f st lenv = function
       xlate_term f st lenv w
    | A.GRef (name, args) ->
       let map1 f = function
-           | Y.Name (id, _) -> f (A.GRef ((id, true, []), []))
+           | E.Name (id, _) -> f (A.GRef ((id, true, []), []))
            | _              -> C.err ()
       in
       let map2 f = xlate_term f st lenv in
@@ -159,7 +159,7 @@ let xlate_entity err f st = function
          let f cnt =
            let lenv = lenv_of_cnt cnt in
            let ww = xlate_term C.start st lenv w in
-           H.add hcnt (uri_of_qid qid) (add_abst cnt name ww);
+           K.add hcnt (uri_of_qid qid) (add_abst cnt name ww);
            err {st with node = Some qid}
         in
          get_cnt_relaxed f st
@@ -171,7 +171,7 @@ let xlate_entity err f st = function
          let lenv = lenv_of_cnt cnt in
         let f qid = 
             let ww = xlate_term C.start st lenv w in
-           H.add henv (uri_of_qid qid) cnt;
+           K.add henv (uri_of_qid qid) cnt;
            let t = match ws with
               | [] -> ww
               | _  -> D.TBind (a, D.Abst ws, ww)
@@ -179,8 +179,8 @@ let xlate_entity err f st = function
 (*
            print_newline (); CrgOutput.pp_term print_string t;
 *)
-           let b = Y.Abst t in
-           let entity = [Y.Mark st.line], uri_of_qid qid, b in
+           let b = E.Abst t in
+           let entity = [E.Mark st.line], uri_of_qid qid, b in
            f {st with line = succ st.line} entity
         in
          complete_qid f st (name, true, [])
@@ -193,7 +193,7 @@ let xlate_entity err f st = function
          let f qid = 
             let ww = xlate_term C.start st lenv w in
            let vv = xlate_term C.start st lenv v in
-           H.add henv (uri_of_qid qid) cnt;
+           K.add henv (uri_of_qid qid) cnt;
             let t = match ws with
               | [] -> D.TCast ([], ww, vv)
               | _  -> D.TBind (a, D.Abst ws, D.TCast ([], ww, vv))
@@ -201,8 +201,8 @@ let xlate_entity err f st = function
 (*
            print_newline (); CrgOutput.pp_term print_string t;
 *)
-           let b = Y.Abbr t in
-           let a = Y.Mark st.line :: if trans then [] else [Y.Priv] in
+           let b = E.Abbr t in
+           let a = E.Mark st.line :: if trans then [] else [E.Priv] in
            let entity = a, uri_of_qid qid, b in
            f {st with line = succ st.line} entity
         in
@@ -213,12 +213,12 @@ let xlate_entity err f st = function
 (* Interface functions ******************************************************)
 
 let initial_status () =
-   H.clear henv; H.clear hcnt; {
-   path = []; node = None; nodes = []; line = 1; mk_uri = O.get_mk_uri ()
+   K.clear henv; K.clear hcnt; {
+   path = []; node = None; nodes = []; line = 1; mk_uri = G.get_mk_uri ()
 }
 
 let refresh_status st = {st with
-   mk_uri = O.get_mk_uri ()
+   mk_uri = G.get_mk_uri ()
 }
 
 let crg_of_aut = xlate_entity