2 ||M|| This file is part of HELM, an Hypertextual, Electronic
3 ||A|| Library of Mathematics, developed at the Computer Science
4 ||T|| Department, University of Bologna, Italy.
6 ||T|| HELM is free software; you can redistribute it and/or
7 ||A|| modify it under the terms of the GNU General Public License
8 \ / version 2 or (at your option) any later version.
9 \ / This software is distributed as is, NO WARRANTY.
10 V_______________________________________________________________ *)
20 (* qualified identifier: uri, name, qualifiers *)
21 type qid = M.uri * M.id * M.id list
23 type context_node = qid option (* context node: None = root *)
26 path: M.id list; (* current section path *)
27 node: context_node; (* current context node *)
28 nodes: context_node list; (* context node list *)
29 line: int; (* line number *)
30 cover: string (* initial segment of URI hierarchy *)
33 type resolver = Local of int
36 let henv_size, hcnt_size = 7000, 4300 (* hash tables initial sizes *)
38 let henv = H.create henv_size (* optimized global environment *)
40 let hcnt = H.create hcnt_size (* optimized context *)
42 (* Internal functions *******************************************************)
44 let id_of_name (id, _, _) = id
46 let mk_qid st id path =
47 let uripath = if st.cover = "" then path else st.cover :: path in
48 let str = String.concat "/" uripath in
49 let str = Filename.concat str id in
50 U.uri_of_string ("ld:/" ^ str ^ ".ld"), id, path
52 let uri_of_qid (uri, _, _) = uri
54 let complete_qid f st (id, is_local, qs) =
55 let f qs = f (mk_qid st id qs) in
56 let f path = C.list_rev_append f path ~tail:qs in
57 let rec skip f = function
58 | phd :: ptl, qshd :: _ when phd = qshd -> f ptl
59 | _ :: ptl, _ :: _ -> skip f (ptl, qs)
62 if is_local then f st.path else skip f (st.path, qs)
64 let relax_qid f st (_, id, path) =
65 let f path = f (mk_qid st id path) in
67 | _ :: tl -> C.list_rev f tl
72 let relax_opt_qid f st = function
74 | Some qid -> let f qid = f (Some qid) in relax_qid f st qid
76 let resolve_lref f st l lenv id =
77 let rec aux f i = function
79 | (name, _) :: _ when name = id -> f (Some (M.LRef (l, i)))
80 | _ :: tl -> aux f (succ i) tl
84 let resolve_lref_strict f st l lenv id =
87 | None -> assert false
89 resolve_lref f st l lenv id
91 let resolve_gref f st qid =
92 try let args = H.find henv (uri_of_qid qid) in f qid (Some args)
93 with Not_found -> f qid None
95 let resolve_gref_relaxed f st qid =
96 (* this is not tail recursive *)
97 let rec g qid = function
98 | None -> relax_qid (resolve_gref g st) st qid
99 | Some args -> f qid args
101 resolve_gref g st qid
103 let get_pars f st = function
105 | Some qid as node ->
106 try let pars = H.find hcnt (uri_of_qid qid) in f pars None
107 with Not_found -> f [] (Some node)
109 let get_pars_relaxed f st =
110 (* this is not tail recursive *)
111 let rec g pars = function
113 | Some node -> relax_opt_qid (get_pars g st) st node
115 get_pars g st st.node
117 (* this is not tail recursive on the GRef branch *)
118 let rec xlate_term f st lenv = function
122 let f vv tt = f (M.Appl (vv, tt)) in
123 let f vv = xlate_term (f vv) st lenv t in
124 xlate_term f st lenv v
125 | A.Abst (name, w, t) ->
126 let add name w lenv = (name, w) :: lenv in
127 let f ww tt = f (M.Abst (name, ww, tt)) in
128 let f ww = xlate_term (f ww) st (add name ww lenv) t in
129 xlate_term f st lenv w
130 | A.GRef (name, args) ->
131 let l = List.length lenv in
133 let map1 f = xlate_term f st lenv in
134 let map2 f (id, _) = resolve_lref_strict f st l lenv id in
136 let f args = f (M.GRef (l, uri_of_qid qid, args)) in
137 let f defs = C.list_rev_map_append f map2 defs ~tail in
138 C.list_sub_strict f defs args
140 C.list_map f map1 args
142 let g qid = resolve_gref_relaxed g st qid in
145 | None -> complete_qid g st name
147 resolve_lref f st l lenv (id_of_name name)
149 let xlate_entity err f st = function
150 | A.Section (Some (_, name)) ->
151 err {st with path = name :: st.path; nodes = st.node :: st.nodes}
153 begin match st.path, st.nodes with
154 | _ :: ptl, nhd :: ntl ->
155 err {st with path = ptl; node = nhd; nodes = ntl}
159 err {st with node = None}
160 | A.Context (Some name) ->
161 let f name = err {st with node = Some name} in
162 complete_qid f st name
163 | A.Block (name, w) ->
167 H.add hcnt (uri_of_qid qid) ((name, ww) :: pars);
168 err {st with node = Some qid}
170 xlate_term f st pars w
172 get_pars_relaxed f st
174 complete_qid f st (name, true, [])
175 | A.Decl (name, w) ->
179 H.add henv (uri_of_qid qid) pars;
180 let a = [Y.Mark st.line] in
181 let entry = pars, ww, None in
182 let entity = a, uri_of_qid qid, Y.Abst entry in
183 f {st with line = succ st.line} entity
185 xlate_term f st pars w
187 complete_qid f st (name, true, [])
189 get_pars_relaxed f st
190 | A.Def (name, w, trans, v) ->
194 H.add henv (uri_of_qid qid) pars;
195 let a = Y.Mark st.line :: if trans then [] else [Y.Priv] in
196 let entry = pars, ww, Some vv in
197 let entity = a, uri_of_qid qid, Y.Abbr entry in
198 f {st with line = succ st.line} entity
200 let f ww = xlate_term (f ww) st pars v in
201 xlate_term f st pars w
203 complete_qid f st (name, true, [])
205 get_pars_relaxed f st
207 (* Interface functions ******************************************************)
209 let initial_status () =
210 H.clear henv; H.clear hcnt; {
211 path = []; node = None; nodes = []; line = 1; cover = !O.cover
214 let refresh_status st = {st with
218 let meta_of_aut = xlate_entity