X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Flambda-delta%2Fcomplete_rg%2FcrgOutput.ml;fp=helm%2Fsoftware%2Flambda-delta%2Fcomplete_rg%2FcrgOutput.ml;h=6da54cbc3dc9cb48dc870687369c147c69b0d87a;hb=2b1375e4b44e2ef351a6341a5bb0a4823e8daae5;hp=3634f9e80171e01ddb7b9ca0fa55973d41c7b13d;hpb=a3b9fc77770f42070632bcb575546678025e09b2;p=helm.git

diff --git a/helm/software/lambda-delta/complete_rg/crgOutput.ml b/helm/software/lambda-delta/complete_rg/crgOutput.ml
index 3634f9e80..6da54cbc3 100644
--- a/helm/software/lambda-delta/complete_rg/crgOutput.ml
+++ b/helm/software/lambda-delta/complete_rg/crgOutput.ml
@@ -14,7 +14,6 @@ module U = NUri
 module C = Cps
 module H = Hierarchy
 module Y = Entity
-module X = Library
 module D = Crg
 
 (****************************************************************************)
@@ -58,92 +57,3 @@ let rec pp_lenv out = function
    | 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.string_of_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 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 out tab
-   | D.TCast (a, u, t)    ->
-      let attrs = [] in
-      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 ~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 ~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