]> matita.cs.unibo.it Git - helm.git/commitdiff
refactoring ...
authorFerruccio Guidi <ferruccio.guidi@unibo.it>
Thu, 29 Oct 2009 18:21:54 +0000 (18:21 +0000)
committerFerruccio Guidi <ferruccio.guidi@unibo.it>
Thu, 29 Oct 2009 18:21:54 +0000 (18:21 +0000)
17 files changed:
helm/software/lambda-delta/Make
helm/software/lambda-delta/complete_rg/Make [new file with mode: 0644]
helm/software/lambda-delta/complete_rg/drg.ml [new file with mode: 0644]
helm/software/lambda-delta/complete_rg/drgAut.ml [new file with mode: 0644]
helm/software/lambda-delta/complete_rg/drgAut.mli [new file with mode: 0644]
helm/software/lambda-delta/complete_rg/drgBrg.ml [new file with mode: 0644]
helm/software/lambda-delta/complete_rg/drgBrg.mli [new file with mode: 0644]
helm/software/lambda-delta/complete_rg/drgOutput.ml [new file with mode: 0644]
helm/software/lambda-delta/complete_rg/drgOutput.mli [new file with mode: 0644]
helm/software/lambda-delta/dual_rg/Make [deleted file]
helm/software/lambda-delta/dual_rg/drg.ml [deleted file]
helm/software/lambda-delta/dual_rg/drgAut.ml [deleted file]
helm/software/lambda-delta/dual_rg/drgAut.mli [deleted file]
helm/software/lambda-delta/dual_rg/drgBrg.ml [deleted file]
helm/software/lambda-delta/dual_rg/drgBrg.mli [deleted file]
helm/software/lambda-delta/dual_rg/drgOutput.ml [deleted file]
helm/software/lambda-delta/dual_rg/drgOutput.mli [deleted file]

index 5179d30aa8da6b390bafe280c8a1aedf7bc9081d..5730e32e680f050f449c73454c29a6ecd8720740 100644 (file)
@@ -1 +1 @@
-lib automath common basic_ag basic_rg dual_rg toplevel
+lib automath common basic_ag basic_rg complete_rg toplevel
diff --git a/helm/software/lambda-delta/complete_rg/Make b/helm/software/lambda-delta/complete_rg/Make
new file mode 100644 (file)
index 0000000..71e141c
--- /dev/null
@@ -0,0 +1 @@
+crg crgOutput crgAut crgBrg
diff --git a/helm/software/lambda-delta/complete_rg/drg.ml b/helm/software/lambda-delta/complete_rg/drg.ml
new file mode 100644 (file)
index 0000000..87e973c
--- /dev/null
@@ -0,0 +1,78 @@
+(*
+    ||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_______________________________________________________________ *)
+
+(* kernel version: dual, relative, global *)
+(* note          : fragment of dual lambda-delta serving as abstract layer *) 
+
+type uri = Entity.uri
+type id = Entity.id
+type attrs = Entity.attrs
+
+type bind = Abst of term list (* domains *)
+          | Abbr of term list (* bodies  *)
+          | Void of int       (* number of exclusions *)
+
+and term = TSort of attrs * int              (* attrs, hierarchy index *)
+         | TLRef of attrs * int * int        (* attrs, position indexes *)
+         | TGRef of attrs * uri              (* attrs, reference *)
+         | TCast of attrs * term * term      (* attrs, domain, element *)
+         | TAppl of attrs * term list * term (* attrs, arguments, function *)
+        | TProj of attrs * lenv * term      (* attrs, closure, member *)
+        | TBind of attrs * bind * term      (* attrs, binder, scope *)
+
+and lenv = ESort                        (* top *)
+         | EProj of lenv * attrs * lenv (* environment, attrs, closure *) 
+         | EBind of lenv * attrs * bind (* environment, attrs, binder *)
+
+type entity = term Entity.entity
+
+(* helpers ******************************************************************)
+
+let mk_uri root s =
+   String.concat "/" ["ld:"; "crg"; root; s ^ ".ld"]
+
+let empty_lenv = ESort
+
+let push_bind f lenv a b = f (EBind (lenv, a, b))
+
+let push_proj f lenv a e = f (EProj (lenv, a, e))
+
+let push2 err f lenv attr ?t = match lenv, t with
+   | EBind (e, a, Abst ws), Some t -> f (EBind (e, (attr :: a), Abst (t :: ws)))
+   | EBind (e, a, Abbr vs), Some t -> f (EBind (e, (attr :: a), Abbr (t :: vs)))
+   | EBind (e, a, Void n), None    -> f (EBind (e, (attr :: a), Void (succ n)))
+   | _                             -> err ()
+
+(* this id not tail recursive *)
+let resolve_lref err f id lenv =
+   let rec aux f i k = function
+     | ESort            -> err ()
+     | EBind (tl, a, _) ->
+        let err kk = aux f (succ i) (k + kk) tl in
+       let f j = f i j (k + j) in
+       Entity.resolve err f id a
+     | EProj _          -> assert false (* TODO *)
+   in
+   aux f 0 0 lenv
+
+let rec get_name err f i j = function
+   | ESort                      -> err i
+   | EBind (tl, a, Abst [])     -> get_name err f i j tl
+   | EBind (tl, a, Abbr [])     -> get_name err f i j tl
+   | EBind (tl, a, Void 0)      -> get_name err f i j tl
+   | EBind (_, a, _) when i = 0 -> 
+      let err () = err i in
+      Entity.get_name err f j a
+   | EBind (tl, _, _)           -> 
+      get_name err f (pred i) j tl
+   | EProj (tl, _, e)           ->
+      let err i = get_name err f i j tl in 
+      get_name err f i j e
diff --git a/helm/software/lambda-delta/complete_rg/drgAut.ml b/helm/software/lambda-delta/complete_rg/drgAut.ml
new file mode 100644 (file)
index 0000000..4b17faa
--- /dev/null
@@ -0,0 +1,222 @@
+(*
+    ||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 H = U.UriHash
+module C = Cps
+module Y = Entity
+module A = Aut
+module D = Drg
+
+(* qualified identifier: uri, name, qualifiers *)
+type qid = D.uri * D.id * D.id list
+
+type context = Y.attrs * D.term list
+
+type context_node = qid option (* context node: None = root *)
+
+type status = {
+   path: D.id list;          (* current section path *) 
+   node: context_node;       (* current context node *)
+   nodes: context_node list; (* context node list *)
+   line: int;                (* line number *)
+   mk_uri:Y.uri_generator    (* uri generator *) 
+}
+
+type resolver = Local of int
+              | Global of context
+
+let henv_size, hcnt_size = 7000, 4300 (* hash tables initial sizes *)
+
+let henv = H.create henv_size (* optimized global environment *)
+
+let hcnt = H.create hcnt_size (* optimized context *)
+
+(* Internal functions *******************************************************)
+
+let initial_status mk_uri =
+   H.clear henv; H.clear hcnt; {
+   path = []; node = None; nodes = []; line = 1; mk_uri = mk_uri
+}
+
+let empty_cnt = [], []
+
+let add_abst (a, ws) id w = 
+   Y.Name (id, true) :: a, w :: ws 
+
+let lenv_of_cnt (a, ws) = 
+   D.push_bind C.start D.empty_lenv a (D.Abst ws)
+
+let mk_lref f i j k = f (D.TLRef ([Y.Apix k], i, j))
+
+let id_of_name (id, _, _) = id
+
+let mk_qid f st id path =
+   let str = String.concat "/" path in
+   let str = Filename.concat str id in 
+   let f str = f (U.uri_of_string str, id, path) in
+   f (st.mk_uri str)
+   
+let uri_of_qid (uri, _, _) = uri
+
+let complete_qid f st (id, is_local, qs) =
+   let f path = C.list_rev_append (mk_qid f st id) path ~tail:qs in
+   let rec skip f = function
+      | phd :: ptl, qshd :: _ when phd = qshd -> f ptl
+      | _ :: ptl, _ :: _                      -> skip f (ptl, qs)
+      | _                                     -> f []
+   in
+   if is_local then f st.path else skip f (st.path, qs)
+
+let relax_qid f st (_, id, path) =
+   let f = function
+      | _ :: tl -> C.list_rev (mk_qid f st id) tl
+      | []      -> assert false
+   in
+   C.list_rev f path
+
+let relax_opt_qid f st = function
+   | None     -> f None
+   | Some qid -> let f qid = f (Some qid) in relax_qid f st qid
+
+let resolve_gref err f st qid =
+   try let cnt = H.find henv (uri_of_qid qid) in f qid cnt
+   with Not_found -> err qid 
+
+let resolve_gref_relaxed f st qid =
+(* this is not tail recursive *)   
+   let rec err qid = relax_qid (resolve_gref err f st) st qid in
+   resolve_gref err f st qid
+
+let get_cnt err f st = function
+   | None              -> f empty_cnt
+   | Some qid as node ->
+      try let cnt = H.find hcnt (uri_of_qid qid) in f cnt
+      with Not_found -> err node
+
+let get_cnt_relaxed f st =
+(* this is not tail recursive *)   
+   let rec err node = relax_opt_qid (get_cnt err f st) st node in
+   get_cnt err f st st.node
+
+(* this is not tail recursive in the GRef branch *)
+let rec xlate_term f st lenv = function
+   | A.Sort s            -> 
+      let f h = f (D.TSort ([], h)) in
+      if s then f 0 else f 1
+   | A.Appl (v, t)       ->
+      let f vv tt = f (D.TAppl ([], [vv], tt)) in
+      let f vv = xlate_term (f vv) st lenv t in
+      xlate_term f st lenv v
+   | A.Abst (name, w, t) ->
+      let f ww = 
+         let a, b = [Y.Name (name, true)], (D.Abst [ww]) in
+        let f tt = f (D.TBind (a, b, tt)) in
+         let f lenv = xlate_term f st lenv t in
+        D.push_bind f lenv a b
+      in
+      xlate_term f st lenv w
+   | A.GRef (name, args) ->
+      let map1 f = function
+           | Y.Name (id, _) -> f (A.GRef ((id, true, []), []))
+           | _              -> C.err ()
+      in
+      let map2 f = xlate_term f st lenv in
+      let g qid (a, _) =
+         let gref = D.TGRef ([], uri_of_qid qid) in
+        match args, a with
+           | [], [] -> f gref
+           | _      -> 
+              let f args = f (D.TAppl ([], args, gref)) in
+              let f args = f (List.rev_map (map2 C.start) args) in
+              let f a = C.list_rev_map_append f map1 a ~tail:args in
+              C.list_sub_strict f a args
+      in
+      let g qid = resolve_gref_relaxed g st qid in
+      let err () = complete_qid g st name in
+      D.resolve_lref err (mk_lref f) (id_of_name name) lenv
+
+let xlate_entity err f st = function
+   | A.Section (Some (_, name))     ->
+      err {st with path = name :: st.path; nodes = st.node :: st.nodes}
+   | A.Section None            ->
+      begin match st.path, st.nodes with
+        | _ :: ptl, nhd :: ntl -> 
+           err {st with path = ptl; node = nhd; nodes = ntl}
+         | _                    -> assert false
+      end
+   | A.Context None            ->
+      err {st with node = None}
+   | A.Context (Some name)     ->
+      let f name = err {st with node = Some name} in
+      complete_qid f st name 
+   | A.Block (name, w)         ->
+      let f qid = 
+         let f cnt =
+           let lenv = lenv_of_cnt cnt in
+           let ww = xlate_term C.start st lenv w in
+           H.add hcnt (uri_of_qid qid) (add_abst cnt name ww);
+           err {st with node = Some qid}
+        in
+         get_cnt_relaxed f st
+      in
+      complete_qid f st (name, true, [])
+   | A.Decl (name, w)          ->
+      let f cnt =
+         let a, ws = cnt in
+         let lenv = lenv_of_cnt cnt in
+        let f qid = 
+            let ww = xlate_term C.start st lenv w in
+           H.add henv (uri_of_qid qid) cnt;
+           let t = match ws with
+              | [] -> ww
+              | _  -> D.TBind (a, D.Abst ws, ww)
+           in
+(*
+           DrgOutput.pp_term print_string t; print_newline ();
+*)
+           let b = Y.Abst t in
+           let entity = [Y.Mark st.line], uri_of_qid qid, b in
+           f {st with line = succ st.line} entity
+        in
+         complete_qid f st (name, true, [])
+      in
+      get_cnt_relaxed f st
+   | A.Def (name, w, trans, v) ->
+      let f cnt = 
+        let a, ws = cnt in
+        let lenv = lenv_of_cnt cnt in
+         let f qid = 
+            let ww = xlate_term C.start st lenv w in
+           let vv = xlate_term C.start st lenv v in
+           H.add henv (uri_of_qid qid) cnt;
+            let t = match ws with
+              | [] -> D.TCast ([], ww, vv)
+              | _  -> D.TBind (a, D.Abst ws, D.TCast ([], ww, vv))
+           in
+(*
+            Printf.printf "%s\n" (U.string_of_uri (uri_of_qid qid));
+*)
+           let b = Y.Abbr t in
+           let a = Y.Mark st.line :: if trans then [] else [Y.Priv] in
+           let entity = a, uri_of_qid qid, b in
+           f {st with line = succ st.line} entity
+        in
+         complete_qid f st (name, true, [])
+      in
+      get_cnt_relaxed f st
+
+(* Interface functions ******************************************************)
+
+let initial_status mk_uri =
+   initial_status mk_uri
+
+let drg_of_aut = xlate_entity
diff --git a/helm/software/lambda-delta/complete_rg/drgAut.mli b/helm/software/lambda-delta/complete_rg/drgAut.mli
new file mode 100644 (file)
index 0000000..5de7f7e
--- /dev/null
@@ -0,0 +1,17 @@
+(*
+    ||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_______________________________________________________________ *)
+
+type status
+
+val initial_status: Entity.uri_generator -> status 
+
+val drg_of_aut: (status -> 'a) -> (status -> Drg.entity -> 'a) -> 
+                status -> Aut.entity -> 'a
diff --git a/helm/software/lambda-delta/complete_rg/drgBrg.ml b/helm/software/lambda-delta/complete_rg/drgBrg.ml
new file mode 100644 (file)
index 0000000..9ff63fb
--- /dev/null
@@ -0,0 +1,67 @@
+(*
+    ||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 C = Cps
+module Y = Entity
+module D = Drg
+module B = Brg
+
+let rec lenv_fold_left map1 map2 x = function
+   | D.ESort            -> x
+   | D.EBind (tl, a, b) -> lenv_fold_left map1 map2 (map1 x a b) tl
+   | D.EProj (tl, a, e) -> lenv_fold_left map1 map2 (map2 x a e) tl
+
+let rec xlate_term f = function
+   | D.TSort (a, l)     -> f (B.Sort (a, l))
+   | D.TGRef (a, n)     -> f (B.GRef (a, n))
+   | D.TLRef (a, _, _)  -> let f i = f (B.LRef (a, i)) in Y.apix C.err f a
+   | D.TCast (a, u, t)  ->
+      let f uu tt = f (B.Cast (a, uu, tt)) in
+      let f uu = xlate_term (f uu) t in
+      xlate_term f u 
+   | D.TAppl (a, vs, t) ->
+      let map f v tt = let f vv = f (B.Appl (a, vv, tt)) in xlate_term f v in
+      let f tt = C.list_fold_right f map vs tt in
+      xlate_term f t
+   | D.TProj (a, e, t)  ->
+      let f tt = f (lenv_fold_left xlate_bind xlate_proj tt e) in
+      xlate_term f t
+   | D.TBind (ab, D.Abst ws, D.TCast (ac, u, t)) ->
+      xlate_term f (D.TCast (ac, D.TBind (ab, D.Abst ws, u), D.TBind (ab, D.Abst ws, t)))
+   | D.TBind (a, b, t)  ->
+      let f tt = f (xlate_bind tt a b) in xlate_term f t
+
+and xlate_bind x a b =
+   let f a ns = a, ns in
+   let a, ns = Y.get_names f a in 
+   match b with
+      | D.Abst ws ->
+         let map x n w = 
+           let f ww = B.Bind (B.Abst (n :: a, ww), x) in xlate_term f w
+        in
+        List.fold_left2 map x ns ws 
+      | D.Abbr vs ->
+         let map x n v = 
+           let f vv = B.Bind (B.Abbr (n :: a, vv), x) in xlate_term f v
+        in
+        List.fold_left2 map x ns vs
+      | D.Void _  ->
+         let map x n = B.Bind (B.Void (n :: a), x) in
+        List.fold_left map x ns
+
+and xlate_proj x _ e =
+   lenv_fold_left xlate_bind xlate_proj x e
+
+let brg_of_drg f t =
+(*   
+   print_newline (); DrgOutput.pp_term print_string t;
+*)
+   f (xlate_term C.start t)
diff --git a/helm/software/lambda-delta/complete_rg/drgBrg.mli b/helm/software/lambda-delta/complete_rg/drgBrg.mli
new file mode 100644 (file)
index 0000000..900dad9
--- /dev/null
@@ -0,0 +1,12 @@
+(*
+    ||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_______________________________________________________________ *)
+
+val brg_of_drg: (Brg.term -> 'a) -> Drg.term -> 'a
diff --git a/helm/software/lambda-delta/complete_rg/drgOutput.ml b/helm/software/lambda-delta/complete_rg/drgOutput.ml
new file mode 100644 (file)
index 0000000..5cb9538
--- /dev/null
@@ -0,0 +1,148 @@
+(*
+    ||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 P = Printf
+module U = NUri
+module C = Cps
+module H = Hierarchy
+module Y = Entity
+module X = Library
+module D = Drg
+
+(****************************************************************************)
+
+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 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 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
diff --git a/helm/software/lambda-delta/complete_rg/drgOutput.mli b/helm/software/lambda-delta/complete_rg/drgOutput.mli
new file mode 100644 (file)
index 0000000..e02161b
--- /dev/null
@@ -0,0 +1,14 @@
+(*
+    ||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_______________________________________________________________ *)
+
+val export_term: Drg.term -> Library.pp
+
+val pp_term: (string -> unit) -> Drg.term -> unit
diff --git a/helm/software/lambda-delta/dual_rg/Make b/helm/software/lambda-delta/dual_rg/Make
deleted file mode 100644 (file)
index ca96189..0000000
+++ /dev/null
@@ -1 +0,0 @@
-drg drgOutput drgAut drgBrg
diff --git a/helm/software/lambda-delta/dual_rg/drg.ml b/helm/software/lambda-delta/dual_rg/drg.ml
deleted file mode 100644 (file)
index 87e973c..0000000
+++ /dev/null
@@ -1,78 +0,0 @@
-(*
-    ||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_______________________________________________________________ *)
-
-(* kernel version: dual, relative, global *)
-(* note          : fragment of dual lambda-delta serving as abstract layer *) 
-
-type uri = Entity.uri
-type id = Entity.id
-type attrs = Entity.attrs
-
-type bind = Abst of term list (* domains *)
-          | Abbr of term list (* bodies  *)
-          | Void of int       (* number of exclusions *)
-
-and term = TSort of attrs * int              (* attrs, hierarchy index *)
-         | TLRef of attrs * int * int        (* attrs, position indexes *)
-         | TGRef of attrs * uri              (* attrs, reference *)
-         | TCast of attrs * term * term      (* attrs, domain, element *)
-         | TAppl of attrs * term list * term (* attrs, arguments, function *)
-        | TProj of attrs * lenv * term      (* attrs, closure, member *)
-        | TBind of attrs * bind * term      (* attrs, binder, scope *)
-
-and lenv = ESort                        (* top *)
-         | EProj of lenv * attrs * lenv (* environment, attrs, closure *) 
-         | EBind of lenv * attrs * bind (* environment, attrs, binder *)
-
-type entity = term Entity.entity
-
-(* helpers ******************************************************************)
-
-let mk_uri root s =
-   String.concat "/" ["ld:"; "crg"; root; s ^ ".ld"]
-
-let empty_lenv = ESort
-
-let push_bind f lenv a b = f (EBind (lenv, a, b))
-
-let push_proj f lenv a e = f (EProj (lenv, a, e))
-
-let push2 err f lenv attr ?t = match lenv, t with
-   | EBind (e, a, Abst ws), Some t -> f (EBind (e, (attr :: a), Abst (t :: ws)))
-   | EBind (e, a, Abbr vs), Some t -> f (EBind (e, (attr :: a), Abbr (t :: vs)))
-   | EBind (e, a, Void n), None    -> f (EBind (e, (attr :: a), Void (succ n)))
-   | _                             -> err ()
-
-(* this id not tail recursive *)
-let resolve_lref err f id lenv =
-   let rec aux f i k = function
-     | ESort            -> err ()
-     | EBind (tl, a, _) ->
-        let err kk = aux f (succ i) (k + kk) tl in
-       let f j = f i j (k + j) in
-       Entity.resolve err f id a
-     | EProj _          -> assert false (* TODO *)
-   in
-   aux f 0 0 lenv
-
-let rec get_name err f i j = function
-   | ESort                      -> err i
-   | EBind (tl, a, Abst [])     -> get_name err f i j tl
-   | EBind (tl, a, Abbr [])     -> get_name err f i j tl
-   | EBind (tl, a, Void 0)      -> get_name err f i j tl
-   | EBind (_, a, _) when i = 0 -> 
-      let err () = err i in
-      Entity.get_name err f j a
-   | EBind (tl, _, _)           -> 
-      get_name err f (pred i) j tl
-   | EProj (tl, _, e)           ->
-      let err i = get_name err f i j tl in 
-      get_name err f i j e
diff --git a/helm/software/lambda-delta/dual_rg/drgAut.ml b/helm/software/lambda-delta/dual_rg/drgAut.ml
deleted file mode 100644 (file)
index 4b17faa..0000000
+++ /dev/null
@@ -1,222 +0,0 @@
-(*
-    ||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 H = U.UriHash
-module C = Cps
-module Y = Entity
-module A = Aut
-module D = Drg
-
-(* qualified identifier: uri, name, qualifiers *)
-type qid = D.uri * D.id * D.id list
-
-type context = Y.attrs * D.term list
-
-type context_node = qid option (* context node: None = root *)
-
-type status = {
-   path: D.id list;          (* current section path *) 
-   node: context_node;       (* current context node *)
-   nodes: context_node list; (* context node list *)
-   line: int;                (* line number *)
-   mk_uri:Y.uri_generator    (* uri generator *) 
-}
-
-type resolver = Local of int
-              | Global of context
-
-let henv_size, hcnt_size = 7000, 4300 (* hash tables initial sizes *)
-
-let henv = H.create henv_size (* optimized global environment *)
-
-let hcnt = H.create hcnt_size (* optimized context *)
-
-(* Internal functions *******************************************************)
-
-let initial_status mk_uri =
-   H.clear henv; H.clear hcnt; {
-   path = []; node = None; nodes = []; line = 1; mk_uri = mk_uri
-}
-
-let empty_cnt = [], []
-
-let add_abst (a, ws) id w = 
-   Y.Name (id, true) :: a, w :: ws 
-
-let lenv_of_cnt (a, ws) = 
-   D.push_bind C.start D.empty_lenv a (D.Abst ws)
-
-let mk_lref f i j k = f (D.TLRef ([Y.Apix k], i, j))
-
-let id_of_name (id, _, _) = id
-
-let mk_qid f st id path =
-   let str = String.concat "/" path in
-   let str = Filename.concat str id in 
-   let f str = f (U.uri_of_string str, id, path) in
-   f (st.mk_uri str)
-   
-let uri_of_qid (uri, _, _) = uri
-
-let complete_qid f st (id, is_local, qs) =
-   let f path = C.list_rev_append (mk_qid f st id) path ~tail:qs in
-   let rec skip f = function
-      | phd :: ptl, qshd :: _ when phd = qshd -> f ptl
-      | _ :: ptl, _ :: _                      -> skip f (ptl, qs)
-      | _                                     -> f []
-   in
-   if is_local then f st.path else skip f (st.path, qs)
-
-let relax_qid f st (_, id, path) =
-   let f = function
-      | _ :: tl -> C.list_rev (mk_qid f st id) tl
-      | []      -> assert false
-   in
-   C.list_rev f path
-
-let relax_opt_qid f st = function
-   | None     -> f None
-   | Some qid -> let f qid = f (Some qid) in relax_qid f st qid
-
-let resolve_gref err f st qid =
-   try let cnt = H.find henv (uri_of_qid qid) in f qid cnt
-   with Not_found -> err qid 
-
-let resolve_gref_relaxed f st qid =
-(* this is not tail recursive *)   
-   let rec err qid = relax_qid (resolve_gref err f st) st qid in
-   resolve_gref err f st qid
-
-let get_cnt err f st = function
-   | None              -> f empty_cnt
-   | Some qid as node ->
-      try let cnt = H.find hcnt (uri_of_qid qid) in f cnt
-      with Not_found -> err node
-
-let get_cnt_relaxed f st =
-(* this is not tail recursive *)   
-   let rec err node = relax_opt_qid (get_cnt err f st) st node in
-   get_cnt err f st st.node
-
-(* this is not tail recursive in the GRef branch *)
-let rec xlate_term f st lenv = function
-   | A.Sort s            -> 
-      let f h = f (D.TSort ([], h)) in
-      if s then f 0 else f 1
-   | A.Appl (v, t)       ->
-      let f vv tt = f (D.TAppl ([], [vv], tt)) in
-      let f vv = xlate_term (f vv) st lenv t in
-      xlate_term f st lenv v
-   | A.Abst (name, w, t) ->
-      let f ww = 
-         let a, b = [Y.Name (name, true)], (D.Abst [ww]) in
-        let f tt = f (D.TBind (a, b, tt)) in
-         let f lenv = xlate_term f st lenv t in
-        D.push_bind f lenv a b
-      in
-      xlate_term f st lenv w
-   | A.GRef (name, args) ->
-      let map1 f = function
-           | Y.Name (id, _) -> f (A.GRef ((id, true, []), []))
-           | _              -> C.err ()
-      in
-      let map2 f = xlate_term f st lenv in
-      let g qid (a, _) =
-         let gref = D.TGRef ([], uri_of_qid qid) in
-        match args, a with
-           | [], [] -> f gref
-           | _      -> 
-              let f args = f (D.TAppl ([], args, gref)) in
-              let f args = f (List.rev_map (map2 C.start) args) in
-              let f a = C.list_rev_map_append f map1 a ~tail:args in
-              C.list_sub_strict f a args
-      in
-      let g qid = resolve_gref_relaxed g st qid in
-      let err () = complete_qid g st name in
-      D.resolve_lref err (mk_lref f) (id_of_name name) lenv
-
-let xlate_entity err f st = function
-   | A.Section (Some (_, name))     ->
-      err {st with path = name :: st.path; nodes = st.node :: st.nodes}
-   | A.Section None            ->
-      begin match st.path, st.nodes with
-        | _ :: ptl, nhd :: ntl -> 
-           err {st with path = ptl; node = nhd; nodes = ntl}
-         | _                    -> assert false
-      end
-   | A.Context None            ->
-      err {st with node = None}
-   | A.Context (Some name)     ->
-      let f name = err {st with node = Some name} in
-      complete_qid f st name 
-   | A.Block (name, w)         ->
-      let f qid = 
-         let f cnt =
-           let lenv = lenv_of_cnt cnt in
-           let ww = xlate_term C.start st lenv w in
-           H.add hcnt (uri_of_qid qid) (add_abst cnt name ww);
-           err {st with node = Some qid}
-        in
-         get_cnt_relaxed f st
-      in
-      complete_qid f st (name, true, [])
-   | A.Decl (name, w)          ->
-      let f cnt =
-         let a, ws = cnt in
-         let lenv = lenv_of_cnt cnt in
-        let f qid = 
-            let ww = xlate_term C.start st lenv w in
-           H.add henv (uri_of_qid qid) cnt;
-           let t = match ws with
-              | [] -> ww
-              | _  -> D.TBind (a, D.Abst ws, ww)
-           in
-(*
-           DrgOutput.pp_term print_string t; print_newline ();
-*)
-           let b = Y.Abst t in
-           let entity = [Y.Mark st.line], uri_of_qid qid, b in
-           f {st with line = succ st.line} entity
-        in
-         complete_qid f st (name, true, [])
-      in
-      get_cnt_relaxed f st
-   | A.Def (name, w, trans, v) ->
-      let f cnt = 
-        let a, ws = cnt in
-        let lenv = lenv_of_cnt cnt in
-         let f qid = 
-            let ww = xlate_term C.start st lenv w in
-           let vv = xlate_term C.start st lenv v in
-           H.add henv (uri_of_qid qid) cnt;
-            let t = match ws with
-              | [] -> D.TCast ([], ww, vv)
-              | _  -> D.TBind (a, D.Abst ws, D.TCast ([], ww, vv))
-           in
-(*
-            Printf.printf "%s\n" (U.string_of_uri (uri_of_qid qid));
-*)
-           let b = Y.Abbr t in
-           let a = Y.Mark st.line :: if trans then [] else [Y.Priv] in
-           let entity = a, uri_of_qid qid, b in
-           f {st with line = succ st.line} entity
-        in
-         complete_qid f st (name, true, [])
-      in
-      get_cnt_relaxed f st
-
-(* Interface functions ******************************************************)
-
-let initial_status mk_uri =
-   initial_status mk_uri
-
-let drg_of_aut = xlate_entity
diff --git a/helm/software/lambda-delta/dual_rg/drgAut.mli b/helm/software/lambda-delta/dual_rg/drgAut.mli
deleted file mode 100644 (file)
index 5de7f7e..0000000
+++ /dev/null
@@ -1,17 +0,0 @@
-(*
-    ||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_______________________________________________________________ *)
-
-type status
-
-val initial_status: Entity.uri_generator -> status 
-
-val drg_of_aut: (status -> 'a) -> (status -> Drg.entity -> 'a) -> 
-                status -> Aut.entity -> 'a
diff --git a/helm/software/lambda-delta/dual_rg/drgBrg.ml b/helm/software/lambda-delta/dual_rg/drgBrg.ml
deleted file mode 100644 (file)
index 9ff63fb..0000000
+++ /dev/null
@@ -1,67 +0,0 @@
-(*
-    ||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 C = Cps
-module Y = Entity
-module D = Drg
-module B = Brg
-
-let rec lenv_fold_left map1 map2 x = function
-   | D.ESort            -> x
-   | D.EBind (tl, a, b) -> lenv_fold_left map1 map2 (map1 x a b) tl
-   | D.EProj (tl, a, e) -> lenv_fold_left map1 map2 (map2 x a e) tl
-
-let rec xlate_term f = function
-   | D.TSort (a, l)     -> f (B.Sort (a, l))
-   | D.TGRef (a, n)     -> f (B.GRef (a, n))
-   | D.TLRef (a, _, _)  -> let f i = f (B.LRef (a, i)) in Y.apix C.err f a
-   | D.TCast (a, u, t)  ->
-      let f uu tt = f (B.Cast (a, uu, tt)) in
-      let f uu = xlate_term (f uu) t in
-      xlate_term f u 
-   | D.TAppl (a, vs, t) ->
-      let map f v tt = let f vv = f (B.Appl (a, vv, tt)) in xlate_term f v in
-      let f tt = C.list_fold_right f map vs tt in
-      xlate_term f t
-   | D.TProj (a, e, t)  ->
-      let f tt = f (lenv_fold_left xlate_bind xlate_proj tt e) in
-      xlate_term f t
-   | D.TBind (ab, D.Abst ws, D.TCast (ac, u, t)) ->
-      xlate_term f (D.TCast (ac, D.TBind (ab, D.Abst ws, u), D.TBind (ab, D.Abst ws, t)))
-   | D.TBind (a, b, t)  ->
-      let f tt = f (xlate_bind tt a b) in xlate_term f t
-
-and xlate_bind x a b =
-   let f a ns = a, ns in
-   let a, ns = Y.get_names f a in 
-   match b with
-      | D.Abst ws ->
-         let map x n w = 
-           let f ww = B.Bind (B.Abst (n :: a, ww), x) in xlate_term f w
-        in
-        List.fold_left2 map x ns ws 
-      | D.Abbr vs ->
-         let map x n v = 
-           let f vv = B.Bind (B.Abbr (n :: a, vv), x) in xlate_term f v
-        in
-        List.fold_left2 map x ns vs
-      | D.Void _  ->
-         let map x n = B.Bind (B.Void (n :: a), x) in
-        List.fold_left map x ns
-
-and xlate_proj x _ e =
-   lenv_fold_left xlate_bind xlate_proj x e
-
-let brg_of_drg f t =
-(*   
-   print_newline (); DrgOutput.pp_term print_string t;
-*)
-   f (xlate_term C.start t)
diff --git a/helm/software/lambda-delta/dual_rg/drgBrg.mli b/helm/software/lambda-delta/dual_rg/drgBrg.mli
deleted file mode 100644 (file)
index 900dad9..0000000
+++ /dev/null
@@ -1,12 +0,0 @@
-(*
-    ||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_______________________________________________________________ *)
-
-val brg_of_drg: (Brg.term -> 'a) -> Drg.term -> 'a
diff --git a/helm/software/lambda-delta/dual_rg/drgOutput.ml b/helm/software/lambda-delta/dual_rg/drgOutput.ml
deleted file mode 100644 (file)
index 5cb9538..0000000
+++ /dev/null
@@ -1,148 +0,0 @@
-(*
-    ||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 P = Printf
-module U = NUri
-module C = Cps
-module H = Hierarchy
-module Y = Entity
-module X = Library
-module D = Drg
-
-(****************************************************************************)
-
-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 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 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
diff --git a/helm/software/lambda-delta/dual_rg/drgOutput.mli b/helm/software/lambda-delta/dual_rg/drgOutput.mli
deleted file mode 100644 (file)
index e02161b..0000000
+++ /dev/null
@@ -1,14 +0,0 @@
-(*
-    ||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_______________________________________________________________ *)
-
-val export_term: Drg.term -> Library.pp
-
-val pp_term: (string -> unit) -> Drg.term -> unit