X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Flambda-delta%2Ftoplevel%2FmetaAut.ml;h=71759f79ad1f07dd38531352bb1f8d15502b7ca9;hb=e86383ae4805a526b3acca2ef3c936b3f22daaad;hp=2cce50a83fdeb9cb16b224aeda7230b4921b1d39;hpb=cbdccfa38c3e05d697318cfbb9903a451e4e80d6;p=helm.git diff --git a/helm/software/lambda-delta/toplevel/metaAut.ml b/helm/software/lambda-delta/toplevel/metaAut.ml index 2cce50a83..71759f79a 100644 --- a/helm/software/lambda-delta/toplevel/metaAut.ml +++ b/helm/software/lambda-delta/toplevel/metaAut.ml @@ -1,104 +1,202 @@ -(* 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/. - *) +(* + ||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 H = Hashtbl +module U = NUri module M = Meta module A = Aut -type context_node = M.qid option (* context node: None = root *) +type qid = M.id * M.id list (* qualified identifier: name, qualifiers *) -type context = (M.qid, context_node) H.t (* context: son, parent *) +type environment = (qid, M.pars) H.t + +type context_node = qid option (* context node: None = root *) type status = { - genv: M.environment; (* global environment *) - path: M.id list; (* current section path *) - cnt: context; (* context *) - node: context_node; (* current context node *) - explicit: bool (* need explicit context root? *) + 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 - | Unresolved -let initial_status = { - genv = []; path = []; cnt = H.create 11; node = None; explicit = true +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 - if is_local then Cps.list_rev_append f st.path ~tail:qs else f qs - -let resolve_gref f st lenv gref = - let rec get_local f i = function - | [] -> f None - | (name, _) :: _ when name = gref -> f (Some i) - | _ :: tl -> get_local f (succ i) tl - in - let rec get_global f = function - | [] -> None - | (args, name, _, _) :: _ when name = gref -> f (Some args) - | _ :: tl -> get_global f tl - in - let g = function - | Some args -> f (Global args) - | None -> f Unresolved - in - let f = function - | Some i -> f (Local i) - | None -> get_global g st.genv - in - get_local f 0 lenv + 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.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 + 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 - Cps.list_map f map1 args - | Unresolved -> assert false + 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 - let f name = resolve_gref (f name) st lenv name in - complete_qid f st name + get_pars_relaxed f st + +(* Interface functions ******************************************************) + +let initial_status = initial_status hsize + +let meta_of_aut = xlate_item