X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Flambda-delta%2Fsrc%2Ftext%2FtxtCrg.ml;fp=helm%2Fsoftware%2Flambda-delta%2Fsrc%2Ftext%2FtxtCrg.ml;h=0000000000000000000000000000000000000000;hb=95872555aaa040a22ad2d93cb1278f79e20da70c;hp=ce3853fcb479f6317a8cfc25beb4362f7ddc4ce6;hpb=4025c3f5b36025380dcad84bb7a97045d08652f6;p=helm.git diff --git a/helm/software/lambda-delta/src/text/txtCrg.ml b/helm/software/lambda-delta/src/text/txtCrg.ml deleted file mode 100644 index ce3853fcb..000000000 --- a/helm/software/lambda-delta/src/text/txtCrg.ml +++ /dev/null @@ -1,164 +0,0 @@ -(* - ||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