--- /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.InProp] , E.Abst (n, tt)
+ | T.Cong -> [E.InProp; E.Progress], E.Abst (n, tt)
+ | T.Def -> [] , E.Abbr tt
+ | T.Th -> [E.InProp] , 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 (main, kind, n, id, info, 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 = [] in
+ let ms, b = mk_contents n tt kind in
+ let ms = if main then E.Main :: ms else ms in
+ let a = if ms <> [] then E.Meta ms :: a else a in
+ let a = if info <> ("", "") then E.Info info :: 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