refactoring ...

[helm.git] / helm / software / helena / src / xml / xmlCrg.ml

diff --git a/helm/software/helena/src/xml/xmlCrg.ml b/helm/software/helena/src/xml/xmlCrg.ml
new file mode 100644 (file)
index 0000000..45e3317
--- /dev/null
+++ b/helm/software/helena/src/xml/xmlCrg.ml
@@ -0,0 +1,111 @@
+(*
+    ||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 C  = Cps
+module H  = Hierarchy
+module Y  = Entity
+module R  = Alpha
+module XL = XmlLibrary
+module D  = Crg
+
+(* internal functions *******************************************************)
+
+let rec list_iter map l out tab = match l with
+   | []       -> ()
+   | hd :: tl -> map hd out tab; list_iter map tl out tab
+
+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 ()
+   in
+   ignore (aux C.err C.start e (ns, l))
+
+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
+      in
+      let attrs = [XL.position l; XL.name a] 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
+      in
+      let attrs = [XL.position i; XL.offset j; XL.name a] 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
+      XL.tag XL.gref attrs out tab
+   | D.TCast (a, 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) ->
+      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
+   | 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 
+
+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_eproj e a lenv out tab =
+   let attrs = [] in
+   XL.tag XL.proj attrs ~contents:(lenv_iter (exp_bind e) (exp_eproj e) lenv) out tab
+
+(* interface functions ******************************************************)
+
+let export_term = exp_term D.empty_lenv