type item = obj option
+type context = int * (id * bind) list
+
+type message = (context, term) Log.item list
+
type hierarchy = int -> int
(* Currified constructors ***************************************************)
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)
+