+++ /dev/null
-(*
- ||M|| This file is part of HELM, an Hypertextual, Electronic
- ||A|| Library of Mathematics, developed at the Computer Science
- ||T|| Department, University of Bologna, Italy.
- ||I||
- ||T|| HELM is free software; you can redistribute it and/or
- ||A|| modify it under the terms of the GNU General Public License
- \ / version 2 or (at your option) any later version.
- \ / This software is distributed as is, NO WARRANTY.
- V_______________________________________________________________ *)
-
-module U = NUri
-module H = Hierarchy
-module C = Cps
-module G = Options
-module E = Entity
-module T = Txt
-module TT = TxtTxt
-module D = Crg
-
-type status = {
- path : T.id list; (* current section path *)
- line : int; (* line number *)
- sort : int; (* first default sort index *)
- mk_uri: G.uri_generator (* uri generator *)
-}
-
-let henv_size = 7000 (* hash tables initial size *)
-
-let henv = Hashtbl.create henv_size (* optimized global environment *)
-
-(* Internal functions *******************************************************)
-
-let name_of_id ?(r=true) id = E.Name (id, r)
-
-let mk_lref f i j k = f (D.TLRef ([E.Apix k], i, j))
-
-let mk_gref f uri = f (D.TGRef ([], uri))
-
-let uri_of_id st id path =
- let str = String.concat "/" path in
- let str = Filename.concat str id in
- let str = st.mk_uri str in
- U.uri_of_string str
-
-let resolve_gref err f st id =
- try f (Hashtbl.find henv id)
- with Not_found -> err ()
-
-let rec xlate_term f st lenv = function
- | T.Inst _
- | T.Impl _ -> assert false
- | T.Sort h ->
- f (D.TSort ([], h))
- | T.NSrt id ->
- let f h = f (D.TSort ([], h)) in
- H.sort_of_string C.err f id
- | T.LRef (i, j) ->
- D.get_index C.err (mk_lref f i j) i j lenv
- | T.NRef id ->
- let err () = resolve_gref C.err (mk_gref f) st id in
- D.resolve_lref err (mk_lref f) id lenv
- | T.Cast (u, t) ->
- let f uu tt = f (D.TCast ([], uu, tt)) in
- let f uu = xlate_term (f uu) st lenv t in
- xlate_term f st lenv u
- | T.Appl (vs, t) ->
- let map f = xlate_term f st lenv in
- let f vvs tt = f (D.TAppl ([], vvs, tt)) in
- let f vvs = xlate_term (f vvs) st lenv t in
- C.list_map f map vs
- | T.Bind (n, b, t) ->
- let abst_map (lenv, a, wws) (id, r, w) =
- let attr = name_of_id ~r id in
- let ww = xlate_term C.start st lenv w in
- D.push2 C.err C.start lenv ~attr ~t:ww (), attr :: a, ww :: wws
- in
- let abbr_map (lenv, a, wws) (id, w) =
- let attr = name_of_id id in
- let ww = xlate_term C.start st lenv w in
- D.push2 C.err C.start lenv ~attr ~t:ww (), attr :: a, ww :: wws
- in
- let void_map (lenv, a, n) id =
- let attr = name_of_id id in
- D.push2 C.err C.start lenv ~attr (), attr :: a, succ n
- in
- let lenv, aa, bb = match b with
- | T.Abst xws ->
- let lenv = D.push_bind C.start lenv [] (D.Abst (n, [])) in
- let lenv, aa, wws = List.fold_left abst_map (lenv, [], []) xws in
- lenv, aa, D.Abst (n, wws)
- | T.Abbr xvs ->
- let lenv = D.push_bind C.start lenv [] (D.Abbr []) in
- let lenv, aa, vvs = List.fold_left abbr_map (lenv, [], []) xvs in
- lenv, aa, D.Abbr vvs
- | T.Void ids ->
- let lenv = D.push_bind C.start lenv [] (D.Void 0) in
- let lenv, aa, n = List.fold_left void_map (lenv, [], 0) ids in
- lenv, aa, D.Void n
- in
- let f tt = f (D.TBind (aa, bb, tt)) in
- xlate_term f st lenv t
-
-let xlate_term f st lenv t =
- TT.contract (xlate_term f st lenv) t
-
-let mk_contents n tt = function
- | T.Decl -> [], E.Abst (n, tt)
- | T.Ax -> [], E.Abst (n, tt)
- | T.Cong -> [], E.Abst (n, tt)
- | T.Def -> [], E.Abbr tt
- | T.Th -> [], E.Abbr tt
-
-let xlate_entity err f gen st = function
- | T.Require _ ->
- err st
- | T.Section (Some name) ->
- err {st with path = name :: st.path}
- | T.Section None ->
- begin match st.path with
- | _ :: ptl ->
- err {st with path = ptl}
- | _ -> assert false
- end
- | T.Sorts sorts ->
- let map st (xix, s) =
- let ix = match xix with
- | None -> st.sort
- | Some ix -> ix
- in
- {st with sort = H.set_sorts ix [s]}
- in
- err (List.fold_left map st sorts)
- | T.Graph id ->
- assert (H.set_graph id); err st
- | T.Entity (kind, n, id, meta, t) ->
- let uri = uri_of_id st id st.path in
- Hashtbl.add henv id uri;
- let tt = xlate_term C.start st D.empty_lenv t in
-(*
- print_newline (); CrgOutput.pp_term print_string tt;
-*)
- let a, b = mk_contents n tt kind in
- let a = if meta <> "" then E.Meta meta :: a else a in
- let entity = E.Mark st.line :: a, uri, b in
- f {st with line = succ st.line} entity
- | T.Generate _ ->
- err st
-
-(* Interface functions ******************************************************)
-
-let initial_status () =
- Hashtbl.clear henv; {
- path = []; line = 1; sort = 0; mk_uri = G.get_mk_uri ()
-}
-
-let refresh_status st = {st with
- mk_uri = G.get_mk_uri ()
-}
-
-let crg_of_txt = xlate_entity
projects / helm.git / blobdiff