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    rest  : bool;           (* restricted applications *)
  29    mk_uri: G.uri_generator (* uri generator *)
  30 }
  31
  32 let henv_size = 7000 (* hash tables initial size *)
  33
  34 let henv = KH.create henv_size (* optimized global environment *)
  35
  36 let xerr s () =
  37    Printf.printf "%s\n%!" s; C.err ()
  38
  39 (* Internal functions *******************************************************)
  40
  41 let mk_lref f a y i = f y (D.TLRef (a, i))
  42
  43 let mk_gref f y uri = f y (D.TGRef (E.empty_node, uri))
  44
  45 let get err f e i = match D.get e i with
  46    | _, _, _, D.Void -> err ()
  47    | _, a, y, _      -> mk_lref f a y i
  48
  49 let resolve_gref err f st id =
  50    try
  51       let y, uri = KH.find henv id in f y uri
  52    with Not_found -> err ()
  53
  54 let name_of_id ?(r=true) id =
  55    if id = "" then None else Some (id, r)
  56
  57 let uri_of_id st id path =
  58    let str = String.concat "/" path in
  59    let str = KF.concat str id in
  60    let str = st.mk_uri str in
  61    U.uri_of_string str
  62
  63 let rec xlate_term f st lenv = function
  64 (*
  65    CrgOutput.pp_lenv print_string (Layer.initial_status ()) lenv;
  66    Printf.printf "\n";
  67 *)
  68    | T.Sort k         ->
  69       let y = E.bind_attrs ~main:(k, 0) () in
  70       f y (D.TSort k)
  71    | T.NSrt id        ->
  72       let f h = xlate_term f st lenv (T.Sort h) in
  73       H.sort_of_string (xerr "sort not found") f id
  74    | T.LRef i         ->
  75       get (xerr "index out of bounds") f lenv i
  76    | T.NRef id        ->
  77       let err () = resolve_gref (xerr "global constant not found") (mk_gref f) st id in
  78       D.resolve_lref err (mk_lref f) id lenv
  79    | T.Cast (u, t)    ->
  80       let f uu y tt = f y (D.TCast (uu, tt)) in
  81       let f _ uu = xlate_term (f uu) st lenv t in
  82       xlate_term f st lenv u
  83    | T.Appl (v, t)    ->
  84       let f vv y tt = f y (D.TAppl (E.appl_attrs st.rest, vv, tt)) in
  85       let f _ vv = xlate_term (f vv) st lenv t in
  86       xlate_term f st lenv v
  87    | T.Proj (bs, t)   ->
  88       let f e y tt = f y (D.TProj (e, tt)) in
  89       let f (lenv, e) = xlate_term (f e) st lenv t in
  90       C.list_fold_left f (xlate_bind st) (lenv, D.empty_lenv) bs
  91    | T.Inst (t, vs)   ->
  92       let map f v e =
  93          let f _ vv = D.push_appl f (E.appl_attrs st.rest) vv e in
  94          xlate_term f st lenv v
  95       in
  96       let f e y tt = f y (D.TProj (e, tt)) in
  97       let f e = xlate_term (f e) st lenv t in
  98       C.list_fold_right f map vs D.empty_lenv
  99
 100 and xlate_bind st f (lenv, e) b =
 101    let f lenv e = f (lenv, e) in
 102    let f y b lenv = D.push_bind (f lenv) E.empty_node y b e in
 103    let f y b = D.push_bind (f y b) E.empty_node y b lenv in
 104    match b with
 105       | T.Abst (n, id, r, w) ->
 106          let f y ww =
 107             let y = E.bind_attrs ?name:(name_of_id id) () in
 108             f y (D.Abst (false, n, ww))
 109          in
 110          xlate_term f st lenv w
 111       | T.Abbr (id, v)       ->
 112          let f y vv =
 113             let y = E.bind_attrs ?name:(name_of_id id) () in
 114             f y (D.Abbr vv)
 115          in
 116          xlate_term f st lenv v
 117       | T.Void id           ->
 118          let y = E.bind_attrs ?name:(name_of_id id) ~main:(st.sort, 0) () in
 119          f y D.Void
 120
 121 let mk_contents main kind tt =
 122    let ms, b = match kind with
 123       | T.Decl -> []                    , E.abst E.empty_env tt
 124       | T.Ax   -> [E.InProp]            , E.abst E.empty_env tt
 125       | T.Cong -> [E.InProp; E.Progress], E.abst E.empty_env tt
 126       | T.Def  -> []                    , E.abbr E.empty_env tt
 127       | T.Th   -> [E.InProp]            , E.abbr E.empty_env tt
 128    in
 129    if main then E.Main :: ms, b else ms, b
 130
 131 let xlate_entity err f gen st = function
 132    | T.Require _                          ->
 133       err st
 134    | T.Section (Some name)                ->
 135       err {st with path = name :: st.path}
 136    | T.Section None                       ->
 137       begin match st.path with
 138          | _ :: ptl ->
 139             err {st with path = ptl}
 140          | _        -> assert false
 141       end
 142    | T.Sorts sorts                        ->
 143       let map st (xix, s) =
 144          let ix = match xix with
 145             | None    -> st.sort
 146             | Some ix -> ix
 147          in
 148          {st with sort = H.set_sorts ix [s]}
 149       in
 150       err (KL.fold_left map st sorts)
 151    | T.Graph id                           ->
 152       assert (H.set_graph id); err st
 153    | T.Constant (main, kind, id, info, t) ->
 154       let uri = uri_of_id st id st.path in
 155       let g ya tt =
 156          KH.add henv id (ya, uri);
 157 (*
 158          print_newline (); CrgOutput.pp_term print_string tt;
 159 *)
 160          let meta, b = mk_contents main kind tt in
 161          let na = E.node_attrs ~apix:st.line () in
 162          let ra = E.root_attrs ~meta ~info () in
 163          let entity = ra, na, uri, b in
 164          f {st with line = succ st.line} entity
 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; rest = true; 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