]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/lambda-delta/basic_rg/brg.ml
- basic_rg: architectural bug fix
[helm.git] / helm / software / lambda-delta / basic_rg / brg.ml
index e9897c08a942f74880b7633fe9b4d893b93716be..17532c970f32f234a4f5d5654e852a36834b63a4 100644 (file)
@@ -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)
+