X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Flambda-delta%2Ftoplevel%2FmetaAut.ml;h=d686c0f2c3e4abbe0476d3633eedd8b5787c0879;hb=28430d599505ac26b51e4887e5196d9b380c898a;hp=2ef3ec737e0b0bef84b3a1992855e15c439e5a7c;hpb=cca5f6b7431b846b7bdcbf813632cb79580d5874;p=helm.git diff --git a/helm/software/lambda-delta/toplevel/metaAut.ml b/helm/software/lambda-delta/toplevel/metaAut.ml index 2ef3ec737..d686c0f2c 100644 --- a/helm/software/lambda-delta/toplevel/metaAut.ml +++ b/helm/software/lambda-delta/toplevel/metaAut.ml @@ -11,20 +11,18 @@ module U = NUri module H = U.UriHash +module C = Cps +module Y = Entity module M = Meta module A = Aut (* qualified identifier: uri, name, qualifiers *) -type qid = U.uri * M.id * M.id list - -type environment = M.pars H.t +type qid = M.uri * M.id * M.id list type context_node = qid option (* context node: None = root *) type status = { - henv: environment; (* optimized global environment *) path: M.id list; (* current section path *) - hcnt: environment; (* optimized context *) node: context_node; (* current context node *) nodes: context_node list; (* context node list *) line: int; (* line number *) @@ -34,13 +32,17 @@ type status = { type resolver = Local of int | Global of M.pars -let hsize = 7000 (* hash tables initial size *) +let henv_size, hcnt_size = 7000, 4300 (* hash tables initial sizes *) + +let henv = H.create henv_size (* optimized global environment *) + +let hcnt = H.create hcnt_size (* optimized context *) (* Internal functions *******************************************************) -let initial_status size cover = { +let initial_status cover = + H.clear henv; H.clear hcnt; { path = []; node = None; nodes = []; line = 1; cover = cover; - henv = H.create size; hcnt = H.create size } let id_of_name (id, _, _) = id @@ -55,7 +57,7 @@ let uri_of_qid (uri, _, _) = uri let complete_qid f st (id, is_local, qs) = let f qs = f (mk_qid st id qs) in - let f path = Cps.list_rev_append f path ~tail:qs in + let f path = C.list_rev_append f path ~tail:qs in let rec skip f = function | phd :: ptl, qshd :: _ when phd = qshd -> f ptl | _ :: ptl, _ :: _ -> skip f (ptl, qs) @@ -66,10 +68,10 @@ let complete_qid f st (id, is_local, qs) = let relax_qid f st (_, id, path) = let f path = f (mk_qid st id path) in let f = function - | _ :: tl -> Cps.list_rev f tl + | _ :: tl -> C.list_rev f tl | [] -> assert false in - Cps.list_rev f path + C.list_rev f path let relax_opt_qid f st = function | None -> f None @@ -91,10 +93,11 @@ 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 st.henv (uri_of_qid qid) in f qid (Some args) + try let args = H.find henv (uri_of_qid qid) in f qid (Some args) with Not_found -> f qid None let resolve_gref_relaxed f st qid = +(* this is not tail recursive *) let rec g qid = function | None -> relax_qid (resolve_gref g st) st qid | Some args -> f qid args @@ -104,16 +107,18 @@ 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 st.hcnt (uri_of_qid qid) in f pars None + try let pars = H.find hcnt (uri_of_qid qid) in f pars None with Not_found -> f [] (Some node) let get_pars_relaxed f st = +(* this is not tail recursive *) let rec g pars = function | None -> f pars | Some node -> relax_opt_qid (get_pars g st) st node in get_pars g st st.node +(* this is not tail recursive on the GRef branch *) let rec xlate_term f st lenv = function | A.Sort sort -> f (M.Sort sort) @@ -133,10 +138,10 @@ let rec xlate_term f st lenv = function let map2 f (id, _) = resolve_lref_strict f st l lenv id in let f tail = let f args = f (M.GRef (l, uri_of_qid qid, args)) in - let f defs = Cps.list_rev_map_append f map2 defs ~tail in - Cps.list_sub_strict f defs args + let f defs = C.list_rev_map_append f map2 defs ~tail in + C.list_sub_strict f defs args in - Cps.list_map f map1 args + C.list_map f map1 args in let g qid = resolve_gref_relaxed g st qid in let f = function @@ -145,26 +150,26 @@ let rec xlate_term f st lenv = function in resolve_lref f st l lenv (id_of_name name) -let xlate_item f st = function +let xlate_entity err f st = function | A.Section (Some (_, name)) -> - f {st with path = name :: st.path; nodes = st.node :: st.nodes} None + err {st with path = name :: st.path; nodes = st.node :: st.nodes} | A.Section None -> begin match st.path, st.nodes with | _ :: ptl, nhd :: ntl -> - f {st with path = ptl; node = nhd; nodes = ntl} None + err {st with path = ptl; node = nhd; nodes = ntl} | _ -> assert false end | A.Context None -> - f {st with node = None} None + err {st with node = None} | A.Context (Some name) -> - let f name = f {st with node = Some name} None in + let f name = err {st with node = Some name} in complete_qid f st name | A.Block (name, w) -> let f qid = let f pars = let f ww = - H.add st.hcnt (uri_of_qid qid) ((name, ww) :: pars); - f {st with node = Some qid} None + H.add hcnt (uri_of_qid qid) ((name, ww) :: pars); + err {st with node = Some qid} in xlate_term f st pars w in @@ -175,9 +180,11 @@ let xlate_item f st = function let f pars = let f qid = let f ww = - let entry = (st.line, pars, uri_of_qid qid, ww, None) in - H.add st.henv (uri_of_qid qid) pars; - f {st with line = succ st.line} (Some entry) + H.add henv (uri_of_qid qid) pars; + let a = [Y.Mark st.line] in + let entry = pars, ww, None in + let entity = a, uri_of_qid qid, Y.Abst entry in + f {st with line = succ st.line} entity in xlate_term f st pars w in @@ -188,9 +195,11 @@ let xlate_item f st = function let f pars = let f qid = let f ww vv = - let entry = (st.line, pars, uri_of_qid qid, ww, Some (trans, vv)) in - H.add st.henv (uri_of_qid qid) pars; - f {st with line = succ st.line} (Some entry) + H.add henv (uri_of_qid qid) pars; + let a = Y.Mark st.line :: if trans then [] else [Y.Priv] in + let entry = pars, ww, Some vv in + let entity = a, uri_of_qid qid, Y.Abbr entry in + f {st with line = succ st.line} entity in let f ww = xlate_term (f ww) st pars v in xlate_term f st pars w @@ -202,6 +211,6 @@ let xlate_item f st = function (* Interface functions ******************************************************) let initial_status ?(cover="") () = - initial_status hsize cover + initial_status cover -let meta_of_aut = xlate_item +let meta_of_aut = xlate_entity