helm/software/lambda-delta/complete_rg/crgTxt.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 Y  = Entity
  16 module T  = Txt
  17 module TT = TxtTxt
  18 module D  = Crg
  19
  20 type status = {
  21    path: T.id list;          (* current section path *)
  22    line: int;                (* line number *)
  23    sort: int;                (* first default sort index *)
  24    mk_uri:Y.uri_generator    (* uri generator *)
  25 }
  26
  27 let henv_size = 7000 (* hash tables initial size *)
  28
  29 let henv = Hashtbl.create henv_size (* optimized global environment *)
  30
  31 (* Internal functions *******************************************************)
  32
  33 let initial_status mk_uri = {
  34    path = []; line = 1; sort = 0; mk_uri = mk_uri
  35 }
  36
  37 let name_of_id ?(r=true) id = Y.Name (id, r)
  38
  39 let mk_lref f i j k = f (D.TLRef ([Y.Apix k], i, j))
  40
  41 let mk_gref f uri = f (D.TGRef ([], uri))
  42
  43 let uri_of_id st id path =
  44    let str = String.concat "/" path in
  45    let str = Filename.concat str id in
  46    let str = st.mk_uri str in
  47    U.uri_of_string str
  48
  49 let resolve_gref err f st id =
  50    try f (Hashtbl.find henv id)
  51    with Not_found -> err ()
  52
  53 let rec xlate_term f st lenv = function
  54    | T.Inst _
  55    | T.Impl _       -> assert false
  56    | T.Sort h       ->
  57       f (D.TSort ([], h))
  58    | T.NSrt id      ->
  59       let f h = f (D.TSort ([], h)) in
  60       H.sort_of_string C.err f id
  61    | T.LRef (i, j)  ->
  62       D.get_index C.err (mk_lref f i j) i j lenv
  63    | T.NRef id      ->
  64       let err () = resolve_gref C.err (mk_gref f) st id in
  65       D.resolve_lref err (mk_lref f) id lenv
  66    | T.Cast (u, t)  ->
  67       let f uu tt = f (D.TCast ([], uu, tt)) in
  68       let f uu = xlate_term (f uu) st lenv t in
  69       xlate_term f st lenv u
  70    | T.Appl (vs, t) ->
  71       let map f = xlate_term f st lenv in
  72       let f vvs tt = f (D.TAppl ([], vvs, tt)) in
  73       let f vvs = xlate_term (f vvs) st lenv t in
  74       C.list_map f map vs
  75    | T.Bind (b, t)  ->
  76       let abst_map (lenv, a, wws) (id, r, w) =
  77          let attr = name_of_id ~r id in
  78          let ww = xlate_term C.start st lenv w in
  79          D.push2 C.err C.start lenv attr ~t:ww (), attr :: a, ww :: wws
  80       in
  81       let abbr_map (lenv, a, wws) (id, w) =
  82          let attr = name_of_id id in
  83          let ww = xlate_term C.start st lenv w in
  84          D.push2 C.err C.start lenv attr ~t:ww (), attr :: a, ww :: wws
  85       in
  86       let void_map (lenv, a, n) id =
  87          let attr = name_of_id id in
  88          D.push2 C.err C.start lenv attr (), attr :: a, succ n
  89       in
  90       let lenv, aa, bb = match b with
  91          | T.Abst xws ->
  92             let lenv = D.push_bind C.start lenv [] (D.Abst []) in
  93             let lenv, aa, wws = List.fold_left abst_map (lenv, [], []) xws in
  94             lenv, aa, D.Abst wws
  95          | T.Abbr xvs ->
  96             let lenv = D.push_bind C.start lenv [] (D.Abbr []) in
  97             let lenv, aa, vvs = List.fold_left abbr_map (lenv, [], []) xvs in
  98             lenv, aa, D.Abbr vvs
  99          | T.Void ids ->
 100             let lenv = D.push_bind C.start lenv [] (D.Void 0) in
 101             let lenv, aa, n = List.fold_left void_map (lenv, [], 0) ids in
 102             lenv, aa, D.Void n
 103       in
 104       let f tt = f (D.TBind (aa, bb, tt)) in
 105       xlate_term f st lenv t
 106
 107 let xlate_term f st lenv t =
 108    TT.contract (xlate_term f st lenv) t
 109
 110 let mk_contents tt = function
 111    | T.Decl -> [], Y.Abst tt
 112    | T.Ax   -> [], Y.Abst tt
 113    | T.Def  -> [], Y.Abbr tt
 114    | T.Th   -> [], Y.Abbr tt
 115
 116 let xlate_entity err f st = function
 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 (kind, id, meta, 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, b = mk_contents tt kind in
 144       let a = if meta <> "" then Y.Meta meta :: a else a in
 145       let entity = Y.Mark st.line :: a, uri, b in
 146       f {st with line = succ st.line} entity
 147
 148 (* Interface functions ******************************************************)
 149
 150 let initial_status mk_uri =
 151    initial_status mk_uri
 152
 153 let crg_of_txt = xlate_entity