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 U  = NUri
  13 module H  = Hierarchy
  14 module C  = Cps
  15 module G  = Options
  16 module E  = Entity
  17 module T  = Txt
  18 module TT = TxtTxt
  19 module D  = Crg
  20
  21 type status = {
  22    path  : T.id list;      (* current section path *)
  23    line  : int;            (* line number *)
  24    sort  : int;            (* first default sort index *)
  25    mk_uri: G.uri_generator (* uri generator *)
  26 }
  27
  28 let henv_size = 7000 (* hash tables initial size *)
  29
  30 let henv = Hashtbl.create henv_size (* optimized global environment *)
  31
  32 (* Internal functions *******************************************************)
  33
  34 let name_of_id ?(r=true) id = E.Name (id, r)
  35
  36 let mk_lref f i j k = f (D.TLRef ([E.Apix k], i, j))
  37
  38 let mk_gref f uri = f (D.TGRef ([], uri))
  39
  40 let uri_of_id st id path =
  41    let str = String.concat "/" path in
  42    let str = Filename.concat str id in
  43    let str = st.mk_uri str in
  44    U.uri_of_string str
  45
  46 let resolve_gref err f st id =
  47    try f (Hashtbl.find henv id)
  48    with Not_found -> err ()
  49
  50 let rec xlate_term f st lenv = function
  51    | T.Inst _
  52    | T.Impl _         -> assert false
  53    | T.Sort h         ->
  54       f (D.TSort ([], h))
  55    | T.NSrt id        ->
  56       let f h = f (D.TSort ([], h)) in
  57       H.sort_of_string C.err f id
  58    | T.LRef (i, j)    ->
  59       D.get_index C.err (mk_lref f i j) i j lenv
  60    | T.NRef id        ->
  61       let err () = resolve_gref C.err (mk_gref f) st id in
  62       D.resolve_lref err (mk_lref f) id lenv
  63    | T.Cast (u, t)    ->
  64       let f uu tt = f (D.TCast ([], uu, tt)) in
  65       let f uu = xlate_term (f uu) st lenv t in
  66       xlate_term f st lenv u
  67    | T.Appl (vs, t)   ->
  68       let map f = xlate_term f st lenv in
  69       let f vvs tt = f (D.TAppl ([], vvs, tt)) in
  70       let f vvs = xlate_term (f vvs) st lenv t in
  71       C.list_map f map vs
  72    | T.Bind (n, b, t) ->
  73       let abst_map (lenv, a, wws) (id, r, w) =
  74          let attr = name_of_id ~r id in
  75          let ww = xlate_term C.start st lenv w in
  76          D.push2 C.err C.start lenv ~attr ~t:ww (), attr :: a, ww :: wws
  77       in
  78       let abbr_map (lenv, a, wws) (id, w) =
  79          let attr = name_of_id id in
  80          let ww = xlate_term C.start st lenv w in
  81          D.push2 C.err C.start lenv ~attr ~t:ww (), attr :: a, ww :: wws
  82       in
  83       let void_map (lenv, a, n) id =
  84          let attr = name_of_id id in
  85          D.push2 C.err C.start lenv ~attr (), attr :: a, succ n
  86       in
  87       let lenv, aa, bb = match b with
  88          | T.Abst xws ->
  89             let lenv = D.push_bind C.start lenv [] (D.Abst (n, [])) in
  90             let lenv, aa, wws = List.fold_left abst_map (lenv, [], []) xws in
  91             lenv, aa, D.Abst (n, wws)
  92          | T.Abbr xvs ->
  93             let lenv = D.push_bind C.start lenv [] (D.Abbr []) in
  94             let lenv, aa, vvs = List.fold_left abbr_map (lenv, [], []) xvs in
  95             lenv, aa, D.Abbr vvs
  96          | T.Void ids ->
  97             let lenv = D.push_bind C.start lenv [] (D.Void 0) in
  98             let lenv, aa, n = List.fold_left void_map (lenv, [], 0) ids in
  99             lenv, aa, D.Void n
 100       in
 101       let f tt = f (D.TBind (aa, bb, tt)) in
 102       xlate_term f st lenv t
 103
 104 let xlate_term f st lenv t =
 105    TT.contract (xlate_term f st lenv) t
 106
 107 let mk_contents n tt = function
 108    | T.Decl -> []                    , E.Abst (n, tt)
 109    | T.Ax   -> [E.InProp]            , E.Abst (n, tt)
 110    | T.Cong -> [E.InProp; E.Progress], E.Abst (n, tt)
 111    | T.Def  -> []                    , E.Abbr tt
 112    | T.Th   -> [E.InProp]            , E.Abbr tt
 113
 114 let xlate_entity err f gen st = function
 115    | T.Require _                           ->
 116       err st
 117    | T.Section (Some name)                 ->
 118       err {st with path = name :: st.path}
 119    | T.Section None                        ->
 120       begin match st.path with
 121          | _ :: ptl ->
 122             err {st with path = ptl}
 123          | _        -> assert false
 124       end
 125    | T.Sorts sorts                         ->
 126       let map st (xix, s) =
 127          let ix = match xix with
 128             | None    -> st.sort
 129             | Some ix -> ix
 130          in
 131          {st with sort = H.set_sorts ix [s]}
 132       in
 133       err (List.fold_left map st sorts)
 134    | T.Graph id                            ->
 135       assert (H.set_graph id); err st
 136    | T.Entity (main, kind, n, id, info, t) ->
 137       let uri = uri_of_id st id st.path in
 138       Hashtbl.add henv id uri;
 139       let tt = xlate_term C.start st D.empty_lenv t in
 140 (*
 141       print_newline (); CrgOutput.pp_term print_string tt;
 142 *)
 143       let a = [] in
 144       let ms, b = mk_contents n tt kind in
 145       let ms = if main then E.Main :: ms else ms in
 146       let a = if ms <> [] then E.Meta ms :: a else a in
 147       let a = if info <> ("", "") then E.Info info :: a else a in
 148       let entity = E.Mark st.line :: a, uri, b in
 149       f {st with line = succ st.line} entity
 150    | T.Generate _                          ->
 151       err st
 152
 153 (* Interface functions ******************************************************)
 154
 155 let initial_status () =
 156    Hashtbl.clear henv; {
 157    path = []; line = 1; sort = 0; mk_uri = G.get_mk_uri ()
 158 }
 159
 160 let refresh_status st = {st with
 161    mk_uri = G.get_mk_uri ()
 162 }
 163
 164 let crg_of_txt = xlate_entity