X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fhelena%2Fsrc%2Fxml%2FxmlCrg.ml;h=34c78dd9e0a1b78c591ae832cb2d3feca3b60ecc;hb=88977b2d546e547e23b046792fe2ad8f6ff192a4;hp=45e33178a4ffacc651b4f1eb897e80e6326d36b1;hpb=95872555aaa040a22ad2d93cb1278f79e20da70c;p=helm.git diff --git a/helm/software/helena/src/xml/xmlCrg.ml b/helm/software/helena/src/xml/xmlCrg.ml index 45e33178a..34c78dd9e 100644 --- a/helm/software/helena/src/xml/xmlCrg.ml +++ b/helm/software/helena/src/xml/xmlCrg.ml @@ -12,100 +12,92 @@ module U = NUri module C = Cps module H = Hierarchy -module Y = Entity +module E = Entity module R = Alpha module XL = XmlLibrary module D = Crg -(* internal functions *******************************************************) +IFDEF OBJECTS THEN -let rec list_iter map l out tab = match l with - | [] -> () - | hd :: tl -> map hd out tab; list_iter map tl out tab +(* internal functions *******************************************************) -let list_rev_iter map e ns l out tab = - let rec aux err f e = function - | [], [] -> f e - | n :: ns, hd :: tl -> - let f e = -(* - pp_lenv print_string e; print_string " |- "; - pp_term print_string hd; print_newline (); -*) - map e hd out tab; f (D.push2 C.err C.start e ~attr:n ~t:hd ()) - in - aux err f e (ns, tl) - | _ -> err () +let lenv_iter map_bind map_appl map_proj st e lenv out tab = + let rec aux = function + | D.ESort -> e + | D.EBind (e, a, y, b) -> + let e = aux e in +(* NOTE: the inner binders are alpha-converted first *) + let y = R.alpha D.mem e y in + map_bind st e a y b out tab; D.EBind (e, a, y, b) + | D.EAppl (e, a, v) -> + let e = aux e in + map_appl st e a v out tab; D.EAppl (e, a, v) + | D.EProj (e, d) -> + let e = aux e in + map_proj st e d out tab; D.EProj (e, d) in - ignore (aux C.err C.start e (ns, l)) + ignore (aux lenv) -let lenv_iter map1 map2 l out tab = - let rec aux f = function - | D.ESort -> f () - | D.EBind (lenv, a, b) -> aux (fun () -> map1 a b out tab; f ()) lenv - | D.EProj (lenv, a, e) -> aux (fun () -> map2 a e out tab; f ()) lenv - in - aux C.start l - -let rec exp_term e t out tab = match t with - | D.TSort (a, l) -> - let a = - let err _ = a in - let f s = Y.Name (s, true) :: a in - H.string_of_sort err f l +let rec exp_term st e t out tab = match t with + | D.TSort k -> + let y = + let err _ = E.empty_bind in + let f s = E.bind_attrs ~name:(s, true) () in + H.string_of_sort err f k in - let attrs = [XL.position l; XL.name a] in + let attrs = [XL.position k; XL.name y] in XL.tag XL.sort attrs out tab - | D.TLRef (a, i, j) -> - let a = - let err _ = a in - let f n r = Y.Name (n, r) :: a in - D.get_name err f i j e + | D.TLRef (_, i) -> + let y = + let err _ = E.empty_bind in + let f s r = E.bind_attrs ~name:(s, r) () in + D.get_name err f i e in - let attrs = [XL.position i; XL.offset j; XL.name a] in + let attrs = [XL.depth i; XL.name y] in XL.tag XL.lref attrs out tab - | D.TGRef (a, n) -> - let a = Y.Name (U.name_of_uri n, true) :: a in - let attrs = [XL.uri n; XL.name a] in + | D.TGRef (_, n) -> + let y = E.bind_attrs ~name:(U.name_of_uri n, true) () in + let attrs = [XL.uri n; XL.name y] in XL.tag XL.gref attrs out tab - | D.TCast (a, u, t) -> + | D.TCast (u, t) -> let attrs = [] in - XL.tag XL.cast attrs ~contents:(exp_term e u) out tab; - exp_term e t out tab - | D.TAppl (a, vs, t) -> - let attrs = [XL.arity vs] in - XL.tag XL.appl attrs ~contents:(list_iter (exp_term e) vs) out tab; - exp_term e t out tab - | D.TProj (a, lenv, t) -> + XL.tag XL.cast attrs ~contents:(exp_term st e u) out tab; + exp_term st e t out tab + | D.TAppl (a, v, t) -> + let attrs = XL.restricted a.E.a_rest :: XL.side a.E.a_side @ XL.main a.E.a_main in + XL.tag XL.appl attrs ~contents:(exp_term st e v) out tab; + exp_term st e t out tab + | D.TProj (lenv, t) -> let attrs = [] in - XL.tag XL.proj attrs ~contents:(lenv_iter (exp_bind e) (exp_eproj e) lenv) out tab; - exp_term (D.push_proj C.start e a lenv) t out tab + XL.tag XL.proj attrs ~contents:(lenv_iter exp_bind exp_appl exp_proj st e lenv) out tab; + exp_term st (D.push_proj C.start lenv e) t out tab | D.TBind (a, b, t) -> (* NOTE: the inner binders are alpha-converted first *) - let a = R.alpha (D.names_of_lenv [] e) a in - exp_bind e a b out tab; - exp_term (D.push_bind C.start e a b) t out tab + let a = R.alpha D.mem e a in + exp_bind st e E.empty_node a b out tab; + exp_term st (D.push_bind C.start E.empty_node a b e) t out tab + +and exp_appl st e a v out tab = + let attrs = XL.restricted a.E.a_rest :: XL.side a.E.a_side @ XL.main a.E.a_main in + XL.tag XL.appl attrs ~contents:(exp_term st e v) out tab; -and exp_bind e a b out tab = - let f a ns = a, ns in - let a, ns = Y.get_names f a in - match b with - | D.Abst (n, ws) -> - let e = D.push_bind C.start e a (D.Abst (n, [])) in - let attrs = [XL.level n; XL.name ns; XL.mark a; XL.arity ws] in - XL.tag XL.abst attrs ~contents:(list_rev_iter exp_term e ns ws) out tab - | D.Abbr vs -> - let e = D.push_bind C.start e a (D.Abbr []) in - let attrs = [XL.name ns; XL.mark a; XL.arity vs] in - XL.tag XL.abbr attrs ~contents:(list_rev_iter exp_term e ns vs) out tab - | D.Void n -> - let attrs = [XL.name a; XL.mark a; XL.arity ~n []] in - XL.tag XL.void attrs out tab +and exp_bind st e y a b out tab = match b with + | D.Abst (_, n, w) -> + let attrs = XL.layer st n :: XL.name a :: XL.side a.E.b_side @ XL.main a.E.b_main in + XL.tag XL.abst attrs ~contents:(exp_term st e w) out tab + | D.Abbr v -> + let attrs = [XL.name a] in + XL.tag XL.abbr attrs ~contents:(exp_term st e v) out tab + | D.Void -> + let attrs = [XL.name a] in + XL.tag XL.void attrs out tab -and exp_eproj e a lenv out tab = +and exp_proj st e lenv out tab = let attrs = [] in - XL.tag XL.proj attrs ~contents:(lenv_iter (exp_bind e) (exp_eproj e) lenv) out tab + XL.tag XL.proj attrs ~contents:(lenv_iter exp_bind exp_appl exp_proj st e lenv) out tab (* interface functions ******************************************************) -let export_term = exp_term D.empty_lenv +let export_term st = exp_term st D.empty_lenv + +END