X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Flambda-delta%2Ftoplevel%2FmetaAut.ml;h=2ef3ec737e0b0bef84b3a1992855e15c439e5a7c;hb=cca5f6b7431b846b7bdcbf813632cb79580d5874;hp=370bf4cfd6cee01bfc68f5c1d78a8f9e248b5060;hpb=ac6e72ade957c5ad253362b149140f7f9fd5ec5d;p=helm.git diff --git a/helm/software/lambda-delta/toplevel/metaAut.ml b/helm/software/lambda-delta/toplevel/metaAut.ml index 370bf4cfd..2ef3ec737 100644 --- a/helm/software/lambda-delta/toplevel/metaAut.ml +++ b/helm/software/lambda-delta/toplevel/metaAut.ml @@ -1,59 +1,60 @@ -(* 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 - +(* + ||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 M = Meta module A = Aut -type environment = (M.qid, M.pars) H.t +(* qualified identifier: uri, name, qualifiers *) +type qid = U.uri * M.id * M.id list + +type environment = M.pars H.t -type context_node = M.qid option (* context node: None = root *) +type context_node = qid option (* context node: None = root *) type status = { - genv: M.environment; (* global environment *) 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 *) - explicit: bool (* need explicit context root? *) + line: int; (* line number *) + cover: string (* initial segment of URI hierarchy *) } type resolver = Local of int | Global of M.pars -let hsize = 11 (* hash tables initial size *) +let hsize = 7000 (* hash tables initial size *) + +(* Internal functions *******************************************************) -let initial_status size = { - genv = []; path = []; node = None; nodes = []; explicit = true; +let initial_status size cover = { + path = []; node = None; nodes = []; line = 1; cover = cover; henv = H.create size; hcnt = H.create size } +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 (id, qs) in + let f qs = f (mk_qid st 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 @@ -62,109 +63,108 @@ let complete_qid f st (id, is_local, qs) = 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 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 | [] -> assert false in Cps.list_rev f path -let relax_opt_qid f = function +let relax_opt_qid f st = function | None -> f None - | Some qid -> let f qid = f (Some qid) in relax_qid f qid - -let resolve_gref f st local lenv gref = - let rec get_local f i = function - | [] -> f None - | (name, _) :: _ when fst name = fst gref -> f (Some i) - | _ :: tl -> get_local f (succ i) tl - in - let get_global f = - try - let args = H.find st.henv gref in f (Some args) - with Not_found -> f None - in - let g = function - | Some args -> f gref (Some (Global args)) - | None -> f gref None - in - let f = function - | Some i -> f gref (Some (Local i)) - | None -> get_global g - in - if local then get_local f 0 lenv else f None - -let resolve_gref_relaxed f st lenv gref = - let rec g gref = function - | None -> relax_qid (resolve_gref g st false lenv) gref - | Some resolved -> f gref resolved + | 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_gref g st true lenv gref + 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) + 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) 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 + | Some qid as node -> + try let pars = H.find st.hcnt (uri_of_qid qid) 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 + | Some node -> relax_opt_qid (get_pars g st) 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.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 = - let f name = (name, w) :: lenv in - complete_qid f st (name, true, []) - in + 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 f name = function - | Local i -> f (M.LRef i) - | Global defs -> - let map1 f = xlate_term f st lenv in - let map2 f (name, _) = f (M.GRef (name, [])) in - let f tail = - let f args = f (M.GRef (name, 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 + 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 - let f name = resolve_gref_relaxed f st lenv name in - complete_qid f st name + 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} + | 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} + f {st with path = ptl; node = nhd; nodes = ntl} None | _ -> assert false end | A.Context None -> - f {st with node = None} + f {st with node = None} None | A.Context (Some name) -> - let f name = f {st with node = Some name} in - complete_qid f st name + let f name = f {st with node = Some name} None in + complete_qid f st name | A.Block (name, w) -> - let f name = + let f qid = let f pars = let f ww = - H.add st.hcnt name ((name, ww) :: pars); - f {st with node = Some name} + H.add st.hcnt (uri_of_qid qid) ((name, ww) :: pars); + f {st with node = Some qid} None in xlate_term f st pars w in @@ -173,11 +173,11 @@ let xlate_item f st = function complete_qid f st (name, true, []) | A.Decl (name, w) -> let f pars = - let f name = + let f qid = let f ww = - let entry = (pars, name, ww, None) in - H.add st.henv name pars; - f {st with genv = entry :: st.genv} + 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) in xlate_term f st pars w in @@ -186,11 +186,11 @@ let xlate_item f st = function get_pars_relaxed f st | A.Def (name, w, trans, v) -> let f pars = - let f name = + let f qid = let f ww vv = - let entry = (pars, name, ww, Some (trans, vv)) in - H.add st.henv name pars; - f {st with genv = entry :: st.genv} + 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) in let f ww = xlate_term (f ww) st pars v in xlate_term f st pars w @@ -199,6 +199,9 @@ let xlate_item f st = function in get_pars_relaxed f st -let meta_of_aut f book = - let f st = f st.genv in - Cps.list_fold_left f xlate_item (initial_status hsize) book +(* Interface functions ******************************************************) + +let initial_status ?(cover="") () = + initial_status hsize cover + +let meta_of_aut = xlate_item