helm/software/lambda-delta/toplevel/metaAut.ml

   1 (* Copyright (C) 2000, HELM Team.
   2  *
   3  * This file is part of HELM, an Hypertextual, Electronic
   4  * Library of Mathematics, developed at the Computer Science
   5  * Department, University of Bologna, Italy.
   6  *
   7  * HELM is free software; you can redistribute it and/or
   8  * modify it under the terms of the GNU General Public License
   9  * as published by the Free Software Foundation; either version 2
  10  * of the License, or (at your option) any later version.
  11  *
  12  * HELM is distributed in the hope that it will be useful,
  13  * but WITHOUT ANY WARRANTY; without even the implied warranty of
  14  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
  15  * GNU General Public License for more details.
  16  *
  17  * You should have received a copy of the GNU General Public License
  18  * along with HELM; if not, write to the Free Software
  19  * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
  20  * MA  02111-1307, USA.
  21  *
  22  * For details, see the HELM World-Wide-Web page,
  23  * http://cs.unibo.it/helm/.
  24  *)
  25
  26 module H = Hashtbl
  27 module U = NUri
  28 module M = Meta
  29 module A = Aut
  30
  31 type qid = M.id * M.id list (* qualified identifier: name, qualifiers *)
  32
  33 type environment = (qid, M.pars) H.t
  34
  35 type context_node = qid option (* context node: None = root *)
  36
  37 type status = {
  38    henv: environment;        (* optimized global environment *)
  39    path: M.id list;          (* current section path *)
  40    hcnt: environment;        (* optimized context *)
  41    node: context_node;       (* current context node *)
  42    nodes: context_node list; (* context node list *)
  43    line: int;                (* line number *)
  44    explicit: bool            (* need explicit context root? *)
  45 }
  46
  47 type resolver = Local of int
  48               | Global of M.pars
  49
  50 let hsize = 11 (* hash tables initial size *)
  51
  52 (* Internal functions *******************************************************)
  53
  54 let initial_status size = {
  55    path = []; node = None; nodes = []; line = 1; explicit = true;
  56    henv = H.create size; hcnt = H.create size
  57 }
  58
  59 let id_of_name (id, _, _) = id
  60
  61 let uri_of_qid (id, path) =
  62    let path = String.concat "/" path in
  63    let str = Filename.concat path id in
  64    U.uri_of_string ("ld:/" ^ str)
  65
  66 let complete_qid f st (id, is_local, qs) =
  67    let f qs = f (id, qs) in
  68    let f path = Cps.list_rev_append f path ~tail:qs in
  69    let rec skip f = function
  70       | phd :: ptl, qshd :: _ when phd = qshd -> f ptl
  71       | _ :: ptl, _ :: _                      -> skip f (ptl, qs)
  72       | _                                     -> f []
  73    in
  74    if is_local then f st.path else skip f (st.path, qs)
  75
  76 let relax_qid f (id, path) =
  77    let f path = f (id, path) in
  78    let f = function
  79       | _ :: tl -> Cps.list_rev f tl
  80       | []      -> assert false
  81    in
  82    Cps.list_rev f path
  83
  84 let relax_opt_qid f = function
  85    | None     -> f None
  86    | Some qid -> let f qid = f (Some qid) in relax_qid f qid
  87
  88 let resolve_lref f st l lenv id =
  89    let rec aux f i = function
  90      | []                            -> f None
  91      | (name, _) :: _ when name = id -> f (Some (M.LRef (l, i)))
  92      | _ :: tl                       -> aux f (succ i) tl
  93    in
  94    aux f 0 lenv
  95
  96 let resolve_lref_strict f st l lenv id =
  97    let f = function
  98       | Some t -> f t
  99       | None   -> assert false
 100    in
 101    resolve_lref f st l lenv id
 102
 103 let resolve_gref f st qid =
 104    try let args = H.find st.henv qid in f qid (Some args)
 105    with Not_found -> f qid None
 106
 107 let resolve_gref_relaxed f st qid =
 108    let rec g qid = function
 109       | None      -> relax_qid (resolve_gref g st) qid
 110       | Some args -> f qid args
 111    in
 112    resolve_gref g st qid
 113
 114 let get_pars f st = function
 115    | None              -> f [] None
 116    | Some name as node ->
 117       try let pars = H.find st.hcnt name in f pars None
 118       with Not_found -> f [] (Some node)
 119
 120 let get_pars_relaxed f st =
 121    let rec g pars = function
 122       | None      -> f pars
 123       | Some node -> relax_opt_qid (get_pars g st) node
 124    in
 125    get_pars g st st.node
 126
 127 let rec xlate_term f st lenv = function
 128    | A.Sort sort         ->
 129       f (M.Sort sort)
 130    | A.Appl (v, t)       ->
 131       let f vv tt = f (M.Appl (vv, tt)) in
 132       let f vv = xlate_term (f vv) st lenv t in
 133       xlate_term f st lenv v
 134    | A.Abst (name, w, t) ->
 135       let add name w lenv = (name, w) :: lenv in
 136       let f ww tt = f (M.Abst (name, ww, tt)) in
 137       let f ww = xlate_term (f ww) st (add name ww lenv) t in
 138       xlate_term f st lenv w
 139    | A.GRef (name, args) ->
 140       let l = List.length lenv in
 141       let g qid defs =
 142          let map1 f = xlate_term f st lenv in
 143          let map2 f (id, _) = resolve_lref_strict f st l lenv id in
 144          let f tail =
 145             let f args = f (M.GRef (l, uri_of_qid qid, args)) in
 146             let f defs = Cps.list_rev_map_append f map2 defs ~tail in
 147             Cps.list_sub_strict f defs args
 148          in
 149          Cps.list_map f map1 args
 150       in
 151       let g qid = resolve_gref_relaxed g st qid in
 152       let f = function
 153          | Some t -> f t
 154          | None   -> complete_qid g st name
 155       in
 156       resolve_lref f st l lenv (id_of_name name)
 157
 158 let xlate_item f st = function
 159    | A.Section (Some name)     ->
 160       f {st with path = name :: st.path; nodes = st.node :: st.nodes} None
 161    | A.Section None            ->
 162       begin match st.path, st.nodes with
 163          | _ :: ptl, nhd :: ntl ->
 164             f {st with path = ptl; node = nhd; nodes = ntl} None
 165          | _                    -> assert false
 166       end
 167    | A.Context None            ->
 168       f {st with node = None} None
 169    | A.Context (Some name)     ->
 170       let f name = f {st with node = Some name} None in
 171       complete_qid f st name
 172    | A.Block (name, w)         ->
 173       let f qid =
 174          let f pars =
 175             let f ww =
 176                H.add st.hcnt qid ((name, ww) :: pars);
 177                f {st with node = Some qid} None
 178             in
 179             xlate_term f st pars w
 180          in
 181          get_pars_relaxed f st
 182       in
 183       complete_qid f st (name, true, [])
 184    | A.Decl (name, w)          ->
 185       let f pars =
 186          let f qid =
 187             let f ww =
 188                let entry = (st.line, pars, uri_of_qid qid, ww, None) in
 189                H.add st.henv qid pars;
 190                f {st with line = succ st.line} (Some entry)
 191             in
 192             xlate_term f st pars w
 193          in
 194          complete_qid f st (name, true, [])
 195       in
 196       get_pars_relaxed f st
 197    | A.Def (name, w, trans, v) ->
 198       let f pars =
 199          let f qid =
 200             let f ww vv =
 201                let entry = (st.line, pars, uri_of_qid qid, ww, Some (trans, vv)) in
 202                H.add st.henv qid pars;
 203                f {st with line = succ st.line} (Some entry)
 204             in
 205             let f ww = xlate_term (f ww) st pars v in
 206             xlate_term f st pars w
 207          in
 208          complete_qid f st (name, true, [])
 209       in
 210       get_pars_relaxed f st
 211
 212 (* Interface functions ******************************************************)
 213
 214 let initial_status = initial_status hsize
 215
 216 let meta_of_aut = xlate_item