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_______________________________________________________________ *)
19 (* qualified identifier: uri, name, qualifiers *)
20 type qid = D.uri * D.id * D.id list
22 type environment = D.lenv H.t
24 type context_node = qid option (* context node: None = root *)
27 henv: environment; (* optimized global environment *)
28 path: D.id list; (* current section path *)
29 hcnt: environment; (* optimized context *)
30 node: context_node; (* current context node *)
31 nodes: context_node list; (* context node list *)
32 line: int; (* line number *)
33 mk_uri:'b E.uri_generator (* uri generator *)
36 type resolver = Local of int
39 let hsize = 7000 (* hash tables initial size *)
41 (* Internal functions *******************************************************)
43 let initial_status size mk_uri = {
44 path = []; node = None; nodes = []; line = 1; mk_uri = mk_uri;
45 henv = H.create size; hcnt = H.create size
48 let mk_lref f i = f (D.LRef ([], i))
50 let mk_abst id w = D.Abst ([D.Name (id, true)], w)
52 let id_of_name (id, _, _) = id
54 let mk_qid f st id path =
55 let str = String.concat "/" path in
56 let str = Filename.concat str id in
57 let f str = f (U.uri_of_string str, id, path) in
60 let uri_of_qid (uri, _, _) = uri
62 let complete_qid f st (id, is_local, qs) =
63 let f path = C.list_rev_append (mk_qid f st id) path ~tail:qs in
64 let rec skip f = function
65 | phd :: ptl, qshd :: _ when phd = qshd -> f ptl
66 | _ :: ptl, _ :: _ -> skip f (ptl, qs)
69 if is_local then f st.path else skip f (st.path, qs)
71 let relax_qid f st (_, id, path) =
73 | _ :: tl -> C.list_rev (mk_qid f st id) tl
78 let relax_opt_qid f st = function
80 | Some qid -> let f qid = f (Some qid) in relax_qid f st qid
82 let resolve_gref err f st qid =
83 try let cnt = H.find st.henv (uri_of_qid qid) in f qid cnt
84 with Not_found -> err ()
86 let resolve_gref_relaxed f st qid =
87 let rec err () = relax_qid (resolve_gref err f st) st qid in
88 resolve_gref err f st qid
90 let get_cnt err f st = function
93 try let cnt = H.find st.hcnt (uri_of_qid qid) in f cnt
94 with Not_found -> err node
96 let get_cnt_relaxed f st =
97 let rec err node = relax_opt_qid (get_cnt err f st) st node in
98 get_cnt err f st st.node
100 let rec xlate_term f st lenv = function
102 let f h = f (D.Sort ([], h)) in
103 if s then f 0 else f 1
105 let f vv tt = f (D.Appl ([], [vv], tt)) in
106 let f vv = xlate_term (f vv) st lenv t in
107 xlate_term f st lenv v
108 | A.Abst (name, w, t) ->
110 let b = mk_abst name ww in
111 let f tt = f (D.Bind ([b], tt)) in
112 xlate_term f st (b :: lenv) t
114 xlate_term f st lenv w
115 | A.GRef (name, args) ->
117 let map1 f = xlate_term f st lenv in
119 let f id _ = D.resolve_lref Cps.err (mk_lref f) id lenv in
120 D.name_of_binder C.err f b
123 let f args = f (D.Appl ([], args, D.GRef ([], uri_of_qid qid))) in
124 let f cnt = C.list_rev_map_append f map2 cnt ~tail in
125 C.list_sub_strict f cnt args
127 C.list_map f map1 args
129 let g qid = resolve_gref_relaxed g st qid in
130 let err () = complete_qid g st name in
131 D.resolve_lref err (mk_lref f) (id_of_name name) lenv
133 let xlate_entity f st = function
134 | A.Section (Some (_, name)) ->
135 f {st with path = name :: st.path; nodes = st.node :: st.nodes} None
137 begin match st.path, st.nodes with
138 | _ :: ptl, nhd :: ntl ->
139 f {st with path = ptl; node = nhd; nodes = ntl} None
143 f {st with node = None} None
144 | A.Context (Some name) ->
145 let f name = f {st with node = Some name} None in
146 complete_qid f st name
147 | A.Block (name, w) ->
151 H.add st.hcnt (uri_of_qid qid) (mk_abst name ww :: cnt);
152 f {st with node = Some qid} None
154 xlate_term f st cnt w
158 complete_qid f st (name, true, [])
159 | A.Decl (name, w) ->
163 let b = D.Abst ([], D.Bind (cnt, ww)) in
164 let entry = st.line, uri_of_qid qid, b in
165 H.add st.henv (uri_of_qid qid) cnt;
166 f {st with line = succ st.line} (Some entry)
168 xlate_term f st cnt w
170 complete_qid f st (name, true, [])
173 | A.Def (name, w, trans, v) ->
177 let a = if trans then [] else [D.Priv] in
178 let b = D.Abbr (a, D.Bind (cnt, D.Cast ([], ww, vv))) in
179 let entry = st.line, uri_of_qid qid, b in
180 H.add st.henv (uri_of_qid qid) cnt;
181 f {st with line = succ st.line} (Some entry)
183 let f ww = xlate_term (f ww) st cnt v in
184 xlate_term f st cnt w
186 complete_qid f st (name, true, [])
190 (* Interface functions ******************************************************)
192 let initial_status mk_uri =
193 initial_status hsize mk_uri
195 let drg_of_aut = xlate_entity