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
projects / helm.git / blobdiff