\ / This software is distributed as is, NO WARRANTY.
V_______________________________________________________________ *)
-type uri = NUri.uri
-type id = Aut.id
+(* kernel version: basic, absolute, global *)
+(* note : experimental *)
+
+type uri = Entity.uri
+type id = Entity.id
type bind = Void (* exclusion *)
| Abst of term (* abstraction *)
and term = Sort of int (* hierarchy index *)
| LRef of int (* location *)
| GRef of uri (* reference *)
- | Cast of term * term (* type, term *)
+ | Cast of term * term (* domain, element *)
| Appl of term * term (* argument, function *)
| Bind of int * id * bind * term (* location, name, binder, scope *)
-type obj = int * uri * bind (* age, uri, binder, contents *)
-
-type item = obj option
+type entity = term Entity.entity (* attrs, uri, binder *)
-type context = (int * id * bind) list (* location, name, binder *)
+type lenv = (int * id * bind) list (* location, name, binder *)
-type message = (context, term) Log.item list
+type message = (lenv, term) Log.item list
(* Currified constructors ***************************************************)
let locations () = !location
-(* context handling functions ***********************************************)
+(* local environment handling functions *************************************)
-let empty_context = []
+let empty_lenv = []
-let push f es l id b =
+let push msg f es l id 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 = (l, id, b) :: es in f c
let append f es1 es2 =