(* Copyright (C) 2000, HELM Team. * * This file is part of HELM, an Hypertextual, Electronic * Library of Mathematics, developed at the Computer Science * Department, University of Bologna, Italy. * * HELM is free software; you can redistribute it and/or * modify it under the terms of the GNU General Public License * as published by the Free Software Foundation; either version 2 * of the License, or (at your option) any later version. * * HELM is distributed in the hope that it will be useful, * but WITHOUT ANY WARRANTY; without even the implied warranty of * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the * GNU General Public License for more details. * * You should have received a copy of the GNU General Public License * along with HELM; if not, write to the Free Software * Foundation, Inc., 59 Temple Place - Suite 330, Boston, * MA 02111-1307, USA. * * For details, see the HELM World-Wide-Web page, * http://cs.unibo.it/helm/. *) module H = Hashtbl module U = NUri module M = Meta module A = Aut type qid = M.id * M.id list (* qualified identifier: name, qualifiers *) type environment = (qid, M.pars) H.t 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 *) explicit: bool (* need explicit context root? *) } type resolver = Local of int | Global of M.pars let hsize = 11 (* hash tables initial size *) (* Internal functions *******************************************************) let initial_status size = { path = []; node = None; nodes = []; line = 1; explicit = true; henv = H.create size; hcnt = H.create size } let id_of_name (id, _, _) = id let uri_of_qid (id, path) = let path = String.concat "/" path in let str = Filename.concat path id in U.uri_of_string ("ld:/" ^ str) let complete_qid f st (id, is_local, qs) = let f qs = f (id, qs) in let f path = Cps.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) | _ -> f [] in if is_local then f st.path else skip f (st.path, qs) let relax_qid f (id, path) = let f path = f (id, path) in let f = function | _ :: tl -> Cps.list_rev f tl | [] -> assert false in Cps.list_rev f path let relax_opt_qid f = function | None -> f None | Some qid -> let f qid = f (Some qid) in relax_qid f qid let resolve_lref f st l lenv id = let rec aux f i = function | [] -> f None | (name, _) :: _ when name = id -> f (Some (M.LRef (l, i))) | _ :: tl -> aux f (succ i) tl in aux f 0 lenv let resolve_lref_strict f st l lenv id = let f = function | Some t -> f t | None -> assert false in resolve_lref f st l lenv id let resolve_gref f st qid = try let args = H.find st.henv qid in f qid (Some args) with Not_found -> f qid None let resolve_gref_relaxed f st qid = let rec g qid = function | None -> relax_qid (resolve_gref g st) qid | Some args -> f qid args in resolve_gref g st qid let get_pars f st = function | None -> f [] None | Some name as node -> try let pars = H.find st.hcnt name in f pars None with Not_found -> f [] (Some node) let get_pars_relaxed f st = let rec g pars = function | None -> f pars | Some node -> relax_opt_qid (get_pars g st) node in get_pars g st st.node let rec xlate_term f st lenv = function | A.Sort sort -> f (M.Sort sort) | A.Appl (v, t) -> let f vv tt = f (M.Appl (vv, tt)) in let f vv = xlate_term (f vv) st lenv t in xlate_term f st lenv v | A.Abst (name, w, t) -> let add name w lenv = (name, w) :: lenv in let f ww tt = f (M.Abst (name, ww, tt)) in let f ww = xlate_term (f ww) st (add name ww lenv) t in xlate_term f st lenv w | A.GRef (name, args) -> let l = List.length lenv in let g qid defs = let map1 f = xlate_term f st lenv in 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 in Cps.list_map f map1 args in let g qid = resolve_gref_relaxed g st qid in let f = function | Some t -> f t | None -> complete_qid g st name in resolve_lref f st l lenv (id_of_name name) let xlate_item f st = function | A.Section (Some name) -> f {st with path = name :: st.path; nodes = st.node :: st.nodes} None | A.Section None -> begin match st.path, st.nodes with | _ :: ptl, nhd :: ntl -> f {st with path = ptl; node = nhd; nodes = ntl} None | _ -> assert false end | A.Context None -> f {st with node = None} None | A.Context (Some name) -> let f name = f {st with node = Some name} None in complete_qid f st name | A.Block (name, w) -> let f qid = let f pars = let f ww = H.add st.hcnt qid ((name, ww) :: pars); f {st with node = Some qid} None in xlate_term f st pars w in get_pars_relaxed f st in complete_qid f st (name, true, []) | A.Decl (name, w) -> 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 qid pars; f {st with line = succ st.line} (Some entry) in xlate_term f st pars w in complete_qid f st (name, true, []) in get_pars_relaxed f st | A.Def (name, w, trans, v) -> 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 qid pars; f {st with line = succ st.line} (Some entry) in let f ww = xlate_term (f ww) st pars v in xlate_term f st pars w in complete_qid f st (name, true, []) in get_pars_relaxed f st (* Interface functions ******************************************************) let initial_status = initial_status hsize let meta_of_aut = xlate_item