X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Flambda-delta%2Fdual_rg%2Fdrg.ml;h=b20bdb3d387468fccf6c7436ec34ea3c0cdcb403;hb=6753156ae1618ef3fc7ff401808f769abd9eb03d;hp=4557aadb349f7a3cd12d833eb164988482a80f2b;hpb=ece36f3adcdf55739b4686168b49506439bff2ba;p=helm.git

diff --git a/helm/software/lambda-delta/dual_rg/drg.ml b/helm/software/lambda-delta/dual_rg/drg.ml
index 4557aadb3..b20bdb3d3 100644
--- a/helm/software/lambda-delta/dual_rg/drg.ml
+++ b/helm/software/lambda-delta/dual_rg/drg.ml
@@ -41,15 +41,38 @@ let mk_uri root s =
 
 let empty_lenv = ESort
 
-let push f lenv a b = f (EBind (lenv, a, b))
+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 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