X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Flambda-delta%2Fdual_rg%2Fdrg.ml;h=ac4021c08db2a4a8e99b1bf6dcb288d6f932c98f;hb=d88c6bdb650d69ffccac2031cecf7a50cd7e6917;hp=1d94a26437708f409a98f2a5520097554471fd0a;hpb=a9f15ca61aac8089fb4b599af72533c4a432ba7b;p=helm.git

diff --git a/helm/software/lambda-delta/dual_rg/drg.ml b/helm/software/lambda-delta/dual_rg/drg.ml
index 1d94a2643..ac4021c08 100644
--- a/helm/software/lambda-delta/dual_rg/drg.ml
+++ b/helm/software/lambda-delta/dual_rg/drg.ml
@@ -14,52 +14,62 @@
 
 type uri = Entity.uri
 type id = Entity.id
+type attrs = Entity.attrs
 
-type attr = Name of id * bool  (* name, real? *)
-	  | Priv               (* private global definition *)
+type bind = Abst of term list (* domains *)
+          | Abbr of term list (* bodies  *)
+          | Void of int       (* number of exclusions *)
 
-type attrs = attr list (* attributes *)
+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 *)
 
-type bind = Abst of attrs * term (* attrs, domain *)
-          | Abbr of attrs * term (* attrs, body   *)
-          | Void of attrs        (* attrs         *)
+and lenv = ESort                        (* top *)
+         | EProj of lenv * attrs * lenv (* environment, attrs, closure *) 
+         | EBind of lenv * attrs * bind (* environment, attrs, binder *)
 
-and term = Sort of attrs * int              (* attrs, hierarchy index *)
-         | LRef of attrs * int              (* attrs, position index *)
-         | GRef of attrs * uri              (* attrs, reference *)
-         | Cast of attrs * term * term      (* attrs, domain, element *)
-         | Proj of attrs * lenv * term      (* attrs, closure, scope *)
-         | Appl of attrs * term list * term (* attrs, arguments, function *)
-	 | Bind of bind * term              (* binder, scope *)
+type entity = term Entity.entity
 
-and lenv = bind list (* local environment *)
-
-type entry = bind Entity.entry (* age, uri, binder *)
+(* helpers ******************************************************************)
 
-type entity = bind Entity.entity
+let mk_uri root s =
+   String.concat "/" ["ld:"; "drg"; root; s ^ ".ld"]
 
-(* helpers ******************************************************************)
+let empty_lenv = ESort
 
-let mk_uri root f s =
-   let str = String.concat "/" ["ld:"; "drg"; root; s ^ ".ld"] in
-   f str
+let push_bind f lenv a b = f (EBind (lenv, a, b))
 
-let rec name_of err f = function
-   | Name (n, r) :: _ -> f n r
-   | _ :: tl          -> name_of err f tl
-   | []               -> err ()
+let push_proj f lenv a e = f (EProj (lenv, a, e))
 
-let name_of_binder err f = function
-   | Abst (a, _) -> name_of err f a
-   | Abbr (a, _) -> name_of err f a
-   | Void a      -> name_of err f a
+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 = function
-     | []      -> err ()
-     | b :: tl ->
-        let err () = aux f (succ i) tl in
-	let f name _ = if name = id then f i else err () in
-	name_of_binder err f b
+   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
+	Entity.resolve err f id a
+     | EProj _          -> assert false (* TODO *)
    in
-   aux f 0 lenv
+   aux f 0 0 lenv
+
+let rec get_name err f i j = function
+   | ESort                      -> err i
+   | 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