helm/software/helena/src/text/txtCrg.ml

   1 (*
   2     ||M||  This file is part of HELM, an Hypertextual, Electronic
   3     ||A||  Library of Mathematics, developed at the Computer Science
   4     ||T||  Department, University of Bologna, Italy.
   5     ||I||
   6     ||T||  HELM is free software; you can redistribute it and/or
   7     ||A||  modify it under the terms of the GNU General Public License
   8     \   /  version 2 or (at your option) any later version.
   9      \ /   This software is distributed as is, NO WARRANTY.
  10       V_______________________________________________________________ *)
  11
  12 module KF = Filename
  13 module KH = Hashtbl
  14 module KL = List
  15
  16 module U  = NUri
  17 module C  = Cps
  18 module G  = Options
  19 module H  = Hierarchy
  20 module E  = Entity
  21 module T  = Txt
  22 module D  = Crg
  23
  24 type status = {
  25    path  : T.id list;      (* current section path *)
  26    line  : int;            (* line number *)
  27    sort  : int;            (* first default sort index *)
  28    mk_uri: G.uri_generator (* uri generator *)
  29 }
  30
  31 let henv_size = 7000 (* hash tables initial size *)
  32
  33 let henv = KH.create henv_size (* optimized global environment *)
  34
  35 let xerr s () =
  36    Printf.printf "%s\n%!" s; C.err ()
  37
  38 (* Internal functions *******************************************************)
  39
  40 let mk_lref f a i = f a (D.TLRef (a, i))
  41
  42 let mk_gref f a uri = f a (D.TGRef (a, uri))
  43
  44 let get err f e i = match D.get e i with
  45    | _, _, D.Void -> err ()
  46    | _, a, _      -> mk_lref f a i
  47
  48 let resolve_gref err f st id =
  49    try
  50       let a, uri = KH.find henv id in f a uri
  51    with Not_found -> err ()
  52
  53 let name_of_id ?(r=true) id =
  54    if id = "" then None else Some (id, r)
  55
  56 let uri_of_id st id path =
  57    let str = String.concat "/" path in
  58    let str = KF.concat str id in
  59    let str = st.mk_uri str in
  60    U.uri_of_string str
  61
  62 let rec xlate_term f st lenv = function
  63 (*
  64    CrgOutput.pp_lenv print_string (Layer.initial_status ()) lenv;
  65    Printf.printf "\n";
  66 *)
  67    | T.Sort h         ->
  68       let a = E.node_attrs ~sort:h () in
  69       f a (D.TSort (a, h))
  70    | T.NSrt id        ->
  71       let f h = xlate_term f st lenv (T.Sort h) in
  72       H.sort_of_string (xerr "sort not found") f id
  73    | T.LRef i         ->
  74       get (xerr "index out of bounds") f lenv i
  75    | T.NRef id        ->
  76       let err () = resolve_gref (xerr "global constant not found") (mk_gref f) st id in
  77       D.resolve_lref err (mk_lref f) id lenv
  78    | T.Cast (u, t)    ->
  79       let f uu a tt = f a (D.TCast (a, uu, tt)) in
  80       let f _ uu = xlate_term (f uu) st lenv t in
  81       xlate_term f st lenv u
  82    | T.Appl (v, t)    ->
  83       let f vv a tt = f a (D.TAppl (a, vv, tt)) in
  84       let f _ vv = xlate_term (f vv) st lenv t in
  85       xlate_term f st lenv v
  86    | T.Proj (bs, t)   ->
  87       let f e a tt = f a (D.TProj (a, e, tt)) in
  88       let f (lenv, e) = xlate_term (f e) st lenv t in
  89       C.list_fold_left f (xlate_bind st) (lenv, D.empty_lenv) bs
  90    | T.Inst (t, vs)   ->
  91       let map f v e =
  92          let f _ vv = D.push_appl f E.empty_node vv e in
  93          xlate_term f st lenv v
  94       in
  95       let f e a tt = f a (D.TProj (a, e, tt)) in
  96       let f e = xlate_term (f e) st lenv t in
  97       C.list_fold_right f map vs D.empty_lenv
  98
  99 and xlate_bind st f (lenv, e) b =
 100    let f lenv e = f (lenv, e) in
 101    let f a b lenv = D.push_bind (f lenv) a b e in
 102    let f a b = D.push_bind (f a b) a b lenv in
 103    match b with
 104       | T.Abst (n, id, r, w) ->
 105          let f a ww =
 106             let a = {a with E.n_name = name_of_id ~r id} in
 107             f a (D.Abst (n, ww))
 108          in
 109          xlate_term f st lenv w
 110       | T.Abbr (id, v)       ->
 111          let f a vv =
 112             let a = {a with E.n_name = name_of_id id} in
 113             f a (D.Abbr vv)
 114          in
 115          xlate_term f st lenv v
 116       | T.Void id           ->
 117          let a = E.node_attrs ?name:(name_of_id id) ~sort:st.sort () in
 118          f a D.Void
 119
 120 let mk_contents main kind tt =
 121    let ms, b = match kind with
 122       | T.Decl -> []                    , E.Abst tt
 123       | T.Ax   -> [E.InProp]            , E.Abst tt
 124       | T.Cong -> [E.InProp; E.Progress], E.Abst tt
 125       | T.Def  -> []                    , E.Abbr tt
 126       | T.Th   -> [E.InProp]            , E.Abbr tt
 127    in
 128    if main then E.Main :: ms, b else ms, b
 129
 130 let xlate_entity err f gen st = function
 131    | T.Require _                          ->
 132       err st
 133    | T.Section (Some name)                ->
 134       err {st with path = name :: st.path}
 135    | T.Section None                       ->
 136       begin match st.path with
 137          | _ :: ptl ->
 138             err {st with path = ptl}
 139          | _        -> assert false
 140       end
 141    | T.Sorts sorts                        ->
 142       let map st (xix, s) =
 143          let ix = match xix with
 144             | None    -> st.sort
 145             | Some ix -> ix
 146          in
 147          {st with sort = H.set_sorts ix [s]}
 148       in
 149       err (KL.fold_left map st sorts)
 150    | T.Graph id                           ->
 151       assert (H.set_graph id); err st
 152    | T.Constant (main, kind, id, info, t) ->
 153       let uri = uri_of_id st id st.path in
 154       let g na tt =
 155 (*
 156          print_newline (); CrgOutput.pp_term print_string tt;
 157 *)
 158          let na = {na with E.n_apix = st.line} in
 159          KH.add henv id (na, uri);
 160          let meta, b = mk_contents main kind tt in
 161          let ra = E.root_attrs ~meta ~info () in
 162          let entity = ra, na, uri, b in
 163          f {st with line = succ st.line} entity
 164
 165       in
 166       xlate_term g st D.empty_lenv t
 167    | T.Generate _                         ->
 168       err st
 169
 170 (* Interface functions ******************************************************)
 171
 172 let initial_status () =
 173    KH.clear henv; {
 174    path = []; line = 1; sort = 0; mk_uri = G.get_mk_uri ()
 175 }
 176
 177 let refresh_status st = {st with
 178    mk_uri = G.get_mk_uri ()
 179 }
 180
 181 let crg_of_txt = xlate_entity