X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fhelena%2Fsrc%2Ftext%2FtxtCrg.ml;h=4580d2d867eb7b29ec5dbf4de2e5b3da5129deae;hb=88977b2d546e547e23b046792fe2ad8f6ff192a4;hp=1ba830669610da12bf40f36fbf134c48f9b24078;hpb=2cf2e883f91164ce614bdc86b5c5e2419b98f68d;p=helm.git diff --git a/helm/software/helena/src/text/txtCrg.ml b/helm/software/helena/src/text/txtCrg.ml index 1ba830669..4580d2d86 100644 --- a/helm/software/helena/src/text/txtCrg.ml +++ b/helm/software/helena/src/text/txtCrg.ml @@ -25,7 +25,7 @@ type status = { path : T.id list; (* current section path *) line : int; (* line number *) sort : int; (* first default sort index *) - ext : bool; (* extended applications *) + rest : bool; (* restricted applications *) mk_uri: G.uri_generator (* uri generator *) } @@ -38,17 +38,17 @@ let xerr s () = (* Internal functions *******************************************************) -let mk_lref f a i = f a (D.TLRef (a, i)) +let mk_lref f a y i = f y (D.TLRef (a, i)) -let mk_gref f a uri = f a (D.TGRef (a, uri)) +let mk_gref f y uri = f y (D.TGRef (E.empty_node, uri)) let get err f e i = match D.get e i with - | _, _, D.Void -> err () - | _, a, _ -> mk_lref f a i + | _, _, _, D.Void -> err () + | _, a, y, _ -> mk_lref f a y i let resolve_gref err f st id = try - let a, uri = KH.find henv id in f a uri + let y, uri = KH.find henv id in f y uri with Not_found -> err () let name_of_id ?(r=true) id = @@ -65,9 +65,9 @@ let rec xlate_term f st lenv = function CrgOutput.pp_lenv print_string (Layer.initial_status ()) lenv; Printf.printf "\n"; *) - | T.Sort h -> - let a = E.node_attrs ~main:(h, 0) () in - f a (D.TSort (a, h)) + | T.Sort k -> + let y = E.bind_attrs ~main:(k, 0) () in + f y (D.TSort k) | T.NSrt id -> let f h = xlate_term f st lenv (T.Sort h) in H.sort_of_string (xerr "sort not found") f id @@ -77,54 +77,54 @@ let rec xlate_term f st lenv = function let err () = resolve_gref (xerr "global constant not found") (mk_gref f) st id in D.resolve_lref err (mk_lref f) id lenv | T.Cast (u, t) -> - let f uu a tt = f a (D.TCast (a, uu, tt)) in + let f uu y tt = f y (D.TCast (uu, tt)) in let f _ uu = xlate_term (f uu) st lenv t in xlate_term f st lenv u | T.Appl (v, t) -> - let f vv a tt = f a (D.TAppl (a, st.ext, vv, tt)) in + let f vv y tt = f y (D.TAppl (E.appl_attrs st.rest, vv, tt)) in let f _ vv = xlate_term (f vv) st lenv t in xlate_term f st lenv v | T.Proj (bs, t) -> - let f e a tt = f a (D.TProj (a, e, tt)) in + let f e y tt = f y (D.TProj (e, tt)) in let f (lenv, e) = xlate_term (f e) st lenv t in C.list_fold_left f (xlate_bind st) (lenv, D.empty_lenv) bs | T.Inst (t, vs) -> let map f v e = - let f _ vv = D.push_appl f E.empty_node st.ext vv e in + let f _ vv = D.push_appl f (E.appl_attrs st.rest) vv e in xlate_term f st lenv v in - let f e a tt = f a (D.TProj (a, e, tt)) in + let f e y tt = f y (D.TProj (e, tt)) in let f e = xlate_term (f e) st lenv t in C.list_fold_right f map vs D.empty_lenv and xlate_bind st f (lenv, e) b = let f lenv e = f (lenv, e) in - let f a b lenv = D.push_bind (f lenv) a b e in - let f a b = D.push_bind (f a b) a b lenv in + let f y b lenv = D.push_bind (f lenv) E.empty_node y b e in + let f y b = D.push_bind (f y b) E.empty_node y b lenv in match b with | T.Abst (n, id, r, w) -> - let f a ww = - let a = {a with E.n_name = name_of_id ~r id} in - f a (D.Abst (false, n, ww)) + let f y ww = + let y = E.bind_attrs ?name:(name_of_id id) () in + f y (D.Abst (false, n, ww)) in xlate_term f st lenv w | T.Abbr (id, v) -> - let f a vv = - let a = {a with E.n_name = name_of_id id} in - f a (D.Abbr vv) + let f y vv = + let y = E.bind_attrs ?name:(name_of_id id) () in + f y (D.Abbr vv) in xlate_term f st lenv v | T.Void id -> - let a = E.node_attrs ?name:(name_of_id id) ~main:(st.sort, 0) () in - f a D.Void + let y = E.bind_attrs ?name:(name_of_id id) ~main:(st.sort, 0) () in + f y D.Void let mk_contents main kind tt = let ms, b = match kind with - | T.Decl -> [] , E.Abst tt - | T.Ax -> [E.InProp] , E.Abst tt - | T.Cong -> [E.InProp; E.Progress], E.Abst tt - | T.Def -> [] , E.Abbr tt - | T.Th -> [E.InProp] , E.Abbr tt + | T.Decl -> [] , E.abst E.empty_env tt + | T.Ax -> [E.InProp] , E.abst E.empty_env tt + | T.Cong -> [E.InProp; E.Progress], E.abst E.empty_env tt + | T.Def -> [] , E.abbr E.empty_env tt + | T.Th -> [E.InProp] , E.abbr E.empty_env tt in if main then E.Main :: ms, b else ms, b @@ -152,17 +152,16 @@ let xlate_entity err f gen st = function assert (H.set_graph id); err st | T.Constant (main, kind, id, info, t) -> let uri = uri_of_id st id st.path in - let g na tt = + let g ya tt = + KH.add henv id (ya, uri); (* print_newline (); CrgOutput.pp_term print_string tt; *) - let na = {na with E.n_apix = st.line} in - KH.add henv id (na, uri); let meta, b = mk_contents main kind tt in + let na = E.node_attrs ~apix:st.line () in let ra = E.root_attrs ~meta ~info () in let entity = ra, na, uri, b in f {st with line = succ st.line} entity - in xlate_term g st D.empty_lenv t | T.Generate _ -> @@ -172,7 +171,7 @@ let xlate_entity err f gen st = function let initial_status () = KH.clear henv; { - path = []; line = 1; sort = 0; ext = false; mk_uri = G.get_mk_uri () + path = []; line = 1; sort = 0; rest = true; mk_uri = G.get_mk_uri () } let refresh_status st = {st with