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 D = Crg
  18
  19 type status = {
  20    path: T.id list;          (* current section path *)
  21    line: int;                (* line number *)
  22    sort: int;                (* first default sort index *)
  23    mk_uri:Y.uri_generator    (* uri generator *)
  24 }
  25
  26 let henv_size = 7000 (* hash tables initial size *)
  27
  28 let henv = Hashtbl.create henv_size (* optimized global environment *)
  29
  30 (* Internal functions *******************************************************)
  31
  32 let initial_status mk_uri = {
  33    path = []; line = 1; sort = 0; mk_uri = mk_uri
  34 }
  35
  36 let name_of_id id = Y.Name (id, true)
  37
  38 let mk_lref f i j k = f (D.TLRef ([Y.Apix k], i, j))
  39
  40 let mk_gref f uri = f (D.TGRef ([], uri))
  41
  42 let uri_of_id st id path =
  43    let str = String.concat "/" path in
  44    let str = Filename.concat str id in
  45    let str = st.mk_uri str in
  46    U.uri_of_string str
  47
  48 let resolve_gref err f st id =
  49    try f (Hashtbl.find henv id)
  50    with Not_found -> err ()
  51
  52 let rec xlate_term f st lenv = function
  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 (b, t)       ->
  73       let map1 (lenv, a, wws) (id, w) =
  74          let attr = name_of_id 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 map2 (lenv, a, n) id =
  79          let attr = name_of_id id in
  80          D.push2 C.err C.start lenv attr (), attr :: a, succ n
  81       in
  82       let lenv, aa, bb = match b with
  83          | T.Abst xws ->
  84             let lenv = D.push_bind C.start lenv [] (D.Abst []) in
  85             let lenv, aa, wws = List.fold_left map1 (lenv, [], []) xws in
  86             lenv, aa, D.Abst wws
  87          | T.Abbr xvs ->
  88             let lenv = D.push_bind C.start lenv [] (D.Abbr []) in
  89             let lenv, aa, vvs = List.fold_left map1 (lenv, [], []) xvs in
  90             lenv, aa, D.Abbr vvs
  91          | T.Void ids ->
  92             let lenv = D.push_bind C.start lenv [] (D.Void 0) in
  93             let lenv, aa, n = List.fold_left map2 (lenv, [], 0) ids in
  94             lenv, aa, D.Void n
  95       in
  96       let f tt = f (D.TBind (aa, bb, tt)) in
  97       xlate_term f st lenv t
  98
  99 let mk_contents tt = function
 100    | T.Decl -> [], Y.Abst tt
 101    | T.Ax   -> [], Y.Abst tt
 102    | T.Def  -> [], Y.Abbr tt
 103    | T.Th   -> [], Y.Abbr tt
 104
 105 let xlate_entity err f st = function
 106    | T.Section (Some name)        ->
 107       err {st with path = name :: st.path}
 108    | T.Section None               ->
 109       begin match st.path with
 110          | _ :: ptl ->
 111             err {st with path = ptl}
 112          | _        -> assert false
 113       end
 114    | T.Sorts sorts                ->
 115       let map st (xix, s) =
 116          let ix = match xix with
 117             | None    -> st.sort
 118             | Some ix -> ix
 119          in
 120          {st with sort = H.set_sorts ix [s]}
 121       in
 122       err (List.fold_left map st sorts)
 123    | T.Graph id                   ->
 124       assert (H.set_graph id); err st
 125    | T.Entity (kind, id, meta, t) ->
 126       let uri = uri_of_id st id st.path in
 127       Hashtbl.add henv id uri;
 128       let tt = xlate_term C.start st D.empty_lenv t in
 129 (*
 130       print_newline (); CrgOutput.pp_term print_string tt;
 131 *)
 132       let a, b = mk_contents tt kind in
 133       let a = if meta <> "" then Y.Meta meta :: a else a in
 134       let entity = Y.Mark st.line :: a, uri, b in
 135       f {st with line = succ st.line} entity
 136
 137 (* Interface functions ******************************************************)
 138
 139 let initial_status mk_uri =
 140    initial_status mk_uri
 141
 142 let crg_of_txt = xlate_entity