X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Flambda-delta%2Fdual_rg%2FdrgOutput.ml;h=5cb9538ddd52e1baba81c08d216d68e4b2c9c15f;hb=6753156ae1618ef3fc7ff401808f769abd9eb03d;hp=f6782d5569d122ca817e0f22cba57da86de5c87c;hpb=cd798346d31b14b8947e5801b87dc4f363607862;p=helm.git

diff --git a/helm/software/lambda-delta/dual_rg/drgOutput.ml b/helm/software/lambda-delta/dual_rg/drgOutput.ml
index f6782d556..5cb9538dd 100644
--- a/helm/software/lambda-delta/dual_rg/drgOutput.ml
+++ b/helm/software/lambda-delta/dual_rg/drgOutput.ml
@@ -9,48 +9,140 @@
      \ /   This software is distributed as is, NO WARRANTY.              
       V_______________________________________________________________ *)
 
+module P = Printf
+module U = NUri
+module C = Cps
+module H = Hierarchy
+module Y = Entity
 module X = Library
 module D = Drg
 
-let rec list_iter map l f = match l with
-   | []       -> f
-   | hd :: tl -> map hd (list_iter map tl f)
+(****************************************************************************)
 
-let rec lenv_iter map l f = match l with
-   | D.Null              -> f
-   | D.Cons (lenv, a, b) -> lenv_iter map lenv (map a b f)
+let pp_attrs out a =
+   let map = function
+      | Y.Name (s, true)  -> out (P.sprintf "%s;" s)
+      | Y.Name (s, false) -> out (P.sprintf "~%s;" s)
+      | Y.Apix i          -> out (P.sprintf "+%i;" i)
+      | Y.Mark i          -> out (P.sprintf "@%i;" i)
+      | Y.Priv            -> out (P.sprintf "%s;" "~") 
+   in
+   List.iter map a
 
-let rec exp_term t f = match t with
-   | D.Sort (a, h)       ->
-      let attrs = [X.position h; X.name a] in
-      X.tag X.sort attrs f
-   | D.LRef (a, i, j)    ->
+let rec pp_term out = function
+   | D.TSort (a, l)    -> pp_attrs out a; out (P.sprintf "*%u" l)
+   | D.TLRef (a, i, j) -> pp_attrs out a; out (P.sprintf "#(%u,%u)" i j)
+   | D.TGRef (a, u)    -> pp_attrs out a; out (P.sprintf "$")
+   | D.TCast (a, x, y) -> pp_attrs out a; out "<"; pp_term out x; out ">."; pp_term out y
+   | D.TProj (a, x, y) -> assert false
+   | D.TAppl (a, x, y) -> pp_attrs out a; pp_terms "(" ")" out x; pp_term out y
+   | D.TBind (a, x, y) -> pp_attrs out a; pp_bind out x; pp_term out y
+
+and pp_terms bg eg out vs =
+   let rec aux = function
+      | []      -> ()
+      | [v]     -> pp_term out v
+      | v :: vs -> pp_term out v; out ", "; aux vs
+   in
+   out bg; aux vs; out (eg ^ ".")
+
+and pp_bind out = function
+   | D.Abst x -> pp_terms "[:" "]" out x
+   | D.Abbr x -> pp_terms "[=" "]" out x
+   | D.Void x -> out (P.sprintf "[%u]" x)
+
+let rec pp_lenv out = function
+   | D.ESort           -> ()
+   | D.EProj (x, a, y) -> assert false
+   | D.EBind (x, a, y) -> pp_lenv out x; pp_attrs out a; pp_bind out y
+
+(****************************************************************************)
+
+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 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.get_sort err f l
+      in
+      let attrs = [X.position l; X.name a] in
+      X.tag X.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 = [X.position i; X.offset j; X.name a] in
-      X.tag X.lref attrs f
-   | D.GRef (a, n)       ->
+      X.tag X.lref attrs out tab
+   | D.TGRef (a, n)       ->
+      let a = Y.Name (U.name_of_uri n, true) :: a in
       let attrs = [X.uri n; X.name a] in
-      X.tag X.gref attrs f   
-   | D.Cast (a, u, t)    ->
+      X.tag X.gref attrs out tab
+   | D.TCast (a, u, t)    ->
       let attrs = [] in
-      X.tag X.cast attrs (exp_term t f) ~contents:(exp_term u)
-   | D.Appl (a, vs, t)   ->
+      X.tag X.cast attrs ~contents:(exp_term e u) out tab;
+      exp_term e t out tab
+   | D.TAppl (a, vs, t)   ->
       let attrs = [X.arity (List.length vs)] in
-      X.tag X.appl attrs (exp_term t f) ~contents:(list_iter exp_term vs)
-   | D.Proj (a, lenv, t) ->
+      X.tag X.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
-      X.tag X.proj attrs (exp_term t f) ~contents:(lenv_iter exp_lenv lenv)
-   | D.Bind (a, b, t) ->
-      exp_lenv a b (exp_term t f)
-
-and exp_lenv a b f = match b with
-   | D.Abst ws ->
-      let attrs = [X.name a; X.mark a; X.arity (List.length ws)] in
-      X.tag X.abst attrs f ~contents:(list_iter exp_term ws)
-   | D.Abbr vs ->
-      let attrs = [X.name a; X.mark a; X.arity (List.length vs)] in
-      X.tag X.abbr attrs f ~contents:(list_iter exp_term vs)
-   | D.Void n ->
-      let attrs = [X.name a; X.mark a; X.arity n] in
-      X.tag X.void attrs f
-
-let export_term = exp_term
+      X.tag X.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) ->
+      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 ws ->
+         let e = D.push_bind C.start e a (D.Abst []) in
+	 let attrs = [X.name ns; X.mark a; X.arity (List.length ws)] in
+         X.tag X.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 = [X.name ns; X.mark a; X.arity (List.length vs)] in
+         X.tag X.abbr attrs ~contents:(list_rev_iter exp_term e ns vs) out tab
+      | D.Void n ->
+         let attrs = [X.name a; X.mark a; X.arity n] in
+         X.tag X.void attrs out tab
+
+and exp_eproj e a lenv out tab =
+   let attrs = [] in
+   X.tag X.proj attrs ~contents:(lenv_iter (exp_bind e) (exp_eproj e) lenv) out tab
+
+(****************************************************************************)
+
+let export_term = exp_term D.empty_lenv