+++ /dev/null
-(*
- ||M|| This file is part of HELM, an Hypertextual, Electronic
- ||A|| Library of Mathematics, developed at the Computer Science
- ||T|| Department, University of Bologna, Italy.
- ||I||
- ||T|| HELM is free software; you can redistribute it and/or
- ||A|| modify it under the terms of the GNU General Public License
- \ / version 2 or (at your option) any later version.
- \ / This software is distributed as is, NO WARRANTY.
- V_______________________________________________________________ *)
-
-module U = NUri
-module H = U.UriHash
-module C = Cps
-module O = Options
-module Y = Entity
-module M = Meta
-module A = Aut
-
-(* qualified identifier: uri, name, qualifiers *)
-type qid = M.uri * M.id * M.id list
-
-type context_node = qid option (* context node: None = root *)
-
-type status = {
- path: M.id list; (* current section path *)
- node: context_node; (* current context node *)
- nodes: context_node list; (* context node list *)
- line: int; (* line number *)
- cover: string (* initial segment of URI hierarchy *)
-}
-
-type resolver = Local of int
- | Global of M.pars
-
-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 id_of_name (id, _, _) = id
-
-let mk_qid st id path =
- let uripath = if st.cover = "" then path else st.cover :: path in
- let str = String.concat "/" uripath in
- let str = Filename.concat str id in
- U.uri_of_string ("ld:/" ^ str ^ ".ld"), id, path
-
-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 = 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)
- | _ -> f []
- in
- if is_local then f st.path else skip f (st.path, qs)
-
-let relax_qid f st (_, id, path) =
- let f path = f (mk_qid st id path) in
- let f = function
- | _ :: tl -> C.list_rev f tl
- | [] -> assert false
- in
- C.list_rev f path
-
-let relax_opt_qid f st = function
- | None -> f None
- | Some qid -> let f qid = f (Some qid) in relax_qid f st 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 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
- in
- resolve_gref g 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
- 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)
- | 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 = C.list_rev_map_append f map2 defs ~tail in
- C.list_sub_strict f defs args
- in
- C.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_entity err f st = function
- | A.Section (Some (_, name)) ->
- 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 ->
- err {st with path = ptl; node = nhd; nodes = ntl}
- | _ -> assert false
- end
- | A.Context None ->
- err {st with node = None}
- | A.Context (Some name) ->
- 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 hcnt (uri_of_qid qid) ((name, ww) :: pars);
- err {st with node = Some qid}
- 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 =
- 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
- 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 =
- 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
- in
- complete_qid f st (name, true, [])
- in
- get_pars_relaxed f st
-
-(* Interface functions ******************************************************)
-
-let initial_status () =
- H.clear henv; H.clear hcnt; {
- path = []; node = None; nodes = []; line = 1; cover = !O.cover
-}
-
-let refresh_status st = {st with
- cover = !O.cover
-}
-
-let meta_of_aut = xlate_entity
projects / helm.git / blobdiff