]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/lambda-delta/src/toplevel/metaAut.ml
we renamed the module abbreviations according to src/modules.ml
[helm.git] / helm / software / lambda-delta / src / toplevel / metaAut.ml
index dd6c4a6f689208e76a9c4dba771790aa6a664baa..6a45518b5bbf1210f5f46d6ffa620a66e000fc3e 100644 (file)
       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 M = Meta
 module A = Aut
 
@@ -35,9 +35,9 @@ 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 *******************************************************)
 
@@ -89,7 +89,7 @@ let resolve_lref_strict f st l lenv id =
    resolve_lref f st l lenv id
 
 let resolve_gref f st qid =
-   try let args = H.find henv (uri_of_qid qid) in f qid (Some args)
+   try let args = K.find henv (uri_of_qid qid) in f qid (Some args)
    with Not_found -> f qid None
 
 let resolve_gref_relaxed f st qid =
@@ -103,7 +103,7 @@ let resolve_gref_relaxed f st qid =
 let get_pars f st = function
    | None              -> f [] None
    | Some qid as node ->
-      try let pars = H.find hcnt (uri_of_qid qid) in f pars None
+      try let pars = K.find hcnt (uri_of_qid qid) in f pars None
       with Not_found -> f [] (Some node)
 
 let get_pars_relaxed f st =
@@ -164,7 +164,7 @@ let xlate_entity err f st = function
       let f qid = 
          let f pars =
            let f ww = 
-              H.add hcnt (uri_of_qid qid) ((name, ww) :: pars);
+              K.add hcnt (uri_of_qid qid) ((name, ww) :: pars);
               err {st with node = Some qid}
            in
             xlate_term f st pars w
@@ -176,10 +176,10 @@ let xlate_entity err f st = function
       let f pars = 
          let f qid = 
             let f ww =
-              H.add henv (uri_of_qid qid) pars;
-              let a = [Y.Mark st.line] in
+              K.add henv (uri_of_qid qid) pars;
+              let a = [E.Mark st.line] in
               let entry = pars, ww, None in
-              let entity = a, uri_of_qid qid, Y.Abst entry in
+              let entity = a, uri_of_qid qid, E.Abst entry in
               f {st with line = succ st.line} entity
            in
            xlate_term f st pars w
@@ -191,10 +191,10 @@ let xlate_entity err f st = function
       let f pars = 
          let f qid = 
             let f ww vv = 
-              H.add henv (uri_of_qid qid) pars;
-              let a = Y.Mark st.line :: if trans then [] else [Y.Priv] in 
+              K.add henv (uri_of_qid qid) pars;
+              let a = E.Mark st.line :: if trans then [] else [E.Priv] in 
               let entry = pars, ww, Some vv in
-              let entity = a, uri_of_qid qid, Y.Abbr entry in
+              let entity = a, uri_of_qid qid, E.Abbr entry in
               f {st with line = succ st.line} entity
            in
            let f ww = xlate_term (f ww) st pars v in
@@ -207,12 +207,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; cover = !O.cover
+   K.clear henv; K.clear hcnt; {
+   path = []; node = None; nodes = []; line = 1; cover = !G.cover
 }
 
 let refresh_status st = {st with
-  cover = !O.cover
+  cover = !G.cover
 }  
 
 let meta_of_aut = xlate_entity