module E = Entity
type uri = E.uri
-type attrs = E.node_attrs
+type b_attrs = E.bind_attrs
type bind = Void (* exclusion *)
| Abst of term (* abstraction *)
| Abbr of term (* abbreviation *)
-and term = Sort of int (* hierarchy index *)
- | LRef of P.mark (* location *)
- | GRef of uri (* reference *)
- | Cast of term * term (* domain, element *)
- | Appl of term * term (* argument, function *)
- | Bind of attrs * P.mark * bind * term (* name, location, binder, scope *)
+and term = Sort of int (* hierarchy index *)
+ | LRef of P.mark (* location *)
+ | GRef of uri (* reference *)
+ | Cast of term * term (* domain, element *)
+ | Appl of term * term (* argument, function *)
+ | Bind of b_attrs * P.mark * bind * term (* name, location, binder, scope *)
type entity = term E.entity (* attrs, uri, binder *)
-type lenv = (attrs * P.mark * bind) list (* name, location, binder *)
+type lenv = (b_attrs * P.mark * bind) list (* name, location, binder *)
type message = (lenv, term) Log.item list
let appl u t = Appl (u, t)
-let bind a l b t = Bind (a, l, b, t)
+let bind y l b t = Bind (y, l, b, t)
-let bind_abst a l u t = Bind (a, l, Abst u, t)
+let bind_abst y l u t = Bind (y, l, Abst u, t)
-let bind_abbr a l v t = Bind (a, l, Abbr v, t)
+let bind_abbr y l v t = Bind (y, l, Abbr v, t)
(* local environment handling functions *************************************)
let empty_lenv = []
-let push msg f es a l b =
+let push msg f es y l b =
let rec does_not_occur loc = function
| [] -> true
| (_, 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 = (a, l, b) :: es in f c
+ let c = (y, l, b) :: es in f c
let append f es1 es2 =
f (List.append es2 es1)
let get err f es i =
let rec aux = function
| [] -> err ()
- | (a, l, b) :: tl -> if l = i then f a b else aux tl
+ | (y, l, b) :: tl -> if l = i then f y b else aux tl
in
aux es