X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Flambda-delta%2Fbasic_rg%2Fbrg.ml;h=17532c970f32f234a4f5d5654e852a36834b63a4;hb=41bf338d7e638ebb5d97e525055bff05b1f0f045;hp=e9897c08a942f74880b7633fe9b4d893b93716be;hpb=40b85b6717785a7b24f2bc0680e716655b8faf99;p=helm.git

diff --git a/helm/software/lambda-delta/basic_rg/brg.ml b/helm/software/lambda-delta/basic_rg/brg.ml
index e9897c08a..17532c970 100644
--- a/helm/software/lambda-delta/basic_rg/brg.ml
+++ b/helm/software/lambda-delta/basic_rg/brg.ml
@@ -27,6 +27,10 @@ type obj = int * uri * bind (* age, uri, binder, contents *)
 
 type item = obj option
 
+type context = int * (id * bind) list
+
+type message = (context, term) Log.item list
+
 type hierarchy = int -> int
 
 (* Currified constructors ***************************************************)
@@ -40,3 +44,26 @@ let cast u t = Cast (u, t)
 let appl u t = Appl (u, t)
 
 let bind id b t = Bind (id, b, t)
+
+(* context handling functions ***********************************************)
+
+let empty_context = 0, []
+
+let push f (l, es) id b =
+   let c = succ l, (id, b) :: es in 
+   f c
+
+let append f (l1, es1) (l2, es2) =
+   f (l2 + l1, List.append es2 es1)
+
+let map f map (l, es) =
+   let f es = f (l, es) in
+   Cps.list_map f map es
+
+let contents f (l, es) = f l es
+
+let get f (l, es) i =
+   if i < 0 || i >= l then f None else 
+   let result = List.nth es (l - succ i) in
+   f (Some result)
+