+
+type context = (attrs * bind) list (* attrs, binder *)
+
+type message = (context, term) Log.item list
+
+(* Currified constructors ***************************************************)
+
+let abst w = Abst w
+
+let abbr v = Abbr v
+
+let lref a i = LRef (a, i)
+
+let cast a u t = Cast (a, u, t)
+
+let appl a u t = Appl (a, u, t)
+
+let bind a b t = Bind (a, b, t)
+
+let bind_abst a u t = Bind (a, Abst u, t)
+
+let bind_abbr a v t = Bind (a, Abbr v, t)
+
+(* context handling functions ***********************************************)
+
+let empty_context = []
+
+let push f es a b =
+ let c = (a, b) :: es in f c
+
+let append f es1 es2 =
+ f (List.append es2 es1)
+
+let map f map es =
+ Cps.list_map f map es
+
+let contents f es = f es
+
+let get f es i =
+ let rec aux e i = function
+ | [] -> f e None
+ | hd :: tl ->
+ if i = 0 then f e (Some hd) else
+ let e = match hd with _, Abst _ -> succ e | _ -> e in
+ aux e (pred i) tl
+ in
+ aux 0 i es
+
+let rec name f = function
+ | [] -> f None
+ | Name (r, n) :: _ -> f (Some (r, n))
+ | _ :: tl -> name f tl