module E = Entity
type uri = E.uri
-type id = E.id
+type attrs = E.attrs
type bind = Void (* exclusion *)
| Abst of term (* abstraction *)
| Abbr of term (* abbreviation *)
-and term = Sort of int (* hierarchy index *)
- | LRef of int (* location *)
- | GRef of uri (* reference *)
- | Cast of term * term (* domain, element *)
- | Appl of term * term (* argument, function *)
- | Bind of int * id * bind * term (* location, name, binder, scope *)
+and term = Sort of int (* hierarchy index *)
+ | LRef of int (* location *)
+ | GRef of uri (* reference *)
+ | Cast of term * term (* domain, element *)
+ | Appl of term * term (* argument, function *)
+ | Bind of attrs * int * bind * term (* name, location, binder, scope *)
type entity = term E.entity (* attrs, uri, binder *)
-type lenv = (int * id * bind) list (* location, name, binder *)
+type lenv = (attrs * int * bind) list (* location, name, binder *)
type message = (lenv, term) Log.item list
let appl u t = Appl (u, t)
-let bind l id b t = Bind (l, id, b, t)
+let bind a l b t = Bind (a, l, b, t)
-let bind_abst l id u t = Bind (l, id, Abst u, t)
+let bind_abst a l u t = Bind (a, l, Abst u, t)
-let bind_abbr l id v t = Bind (l, id, Abbr v, t)
-
-(* location handling functions **********************************************)
-
-let location = ref 0
-
-let new_location () = let loc = !location in incr location; loc
-
-let locations () = !location
+let bind_abbr a l v t = Bind (a, l, Abbr v, t)
(* local environment handling functions *************************************)
let empty_lenv = []
-let push msg f es l id b =
+let push msg f es a l b =
let rec does_not_occur loc = function
| [] -> true
- | (l, _, _) :: _ when l = loc -> false
+ | (_, l, _) :: _ when l = loc -> false
| _ :: es -> does_not_occur l es
in
if not (does_not_occur l es) then failwith msg else
- let c = (l, id, b) :: es in f c
+ let c = (a, l, b) :: es in f c
let append f es1 es2 =
f (List.append es2 es1)
let contents f es = f es
-let get f es i =
+let get err f es i =
let rec aux = function
- | [] -> f None
- | (l, id, b) :: tl -> if l = i then f (Some (id, b)) else aux tl
+ | [] -> err ()
+ | (a, l, b) :: tl -> if l = i then f a b else aux tl
in
aux es
+
+let nth err f loc e =
+ let rec aux n = function
+ | [] -> err loc
+ | (_, l, _) :: _ when l = loc -> f n
+ | _ :: e -> aux (succ n) e
+ in
+ aux 0 e