\ / This software is distributed as is, NO WARRANTY.
V_______________________________________________________________ *)
+(* kernel version: basic, relative, global *)
+(* note : ufficial basic lambda-delta *)
+
type uri = NUri.uri
type id = Aut.id
| Abst of term (* abstraction *)
| Abbr of term (* abbreviation *)
-and term = Sort of int (* hierarchy index *)
- | LRef of int (* reverse de Bruijn index *)
- | GRef of uri (* reference *)
- | Cast of term * term (* type, term *)
- | Appl of term * term (* argument, function *)
- | Bind of id * bind * term (* name, binder, scope *)
+and term = Sort of attrs * int (* attrs, hierarchy index *)
+ | LRef of attrs * int (* attrs, position index *)
+ | GRef of attrs * uri (* attrs, reference *)
+ | Cast of attrs * term * term (* attrs, type, term *)
+ | Appl of attrs * term * term (* attrs, argument, function *)
+ | Bind of attrs * bind * term (* attrs, binder, scope *)
+
+and attr = Name of bool * id (* real?, name *)
+ | Entry of int * bind (* age, binder *)
+
+and attrs = attr list
type obj = int * uri * bind (* age, uri, binder, contents *)
type item = obj option
-type context = int * (id * bind) list
+type context = (attrs * bind) list (* attrs, binder *)
type message = (context, term) Log.item list
let abbr v = Abbr v
-let cast u t = Cast (u, t)
+let lref a i = LRef (a, i)
-let appl u t = Appl (u, t)
+let cast a u t = Cast (a, u, t)
-let bind id b t = Bind (id, b, t)
+let appl a u t = Appl (a, u, t)
-let bind_abst id u t = Bind (id, Abst u, t)
+let bind a b t = Bind (a, b, t)
-let bind_abbr id v t = Bind (id, Abbr v, 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 = 0, []
+let empty_context = []
-let push f (l, es) id b =
- let c = succ l, (id, b) :: es in
- f c
+let push f es a b =
+ let c = (a, b) :: es in f c
-let append f (l1, es1) (l2, es2) =
- f (l2 + l1, List.append es2 es1)
+let append f es1 es2 =
+ f (List.append es2 es1)
-let map f map (l, es) =
- let f es = f (l, es) in
+let map f map es =
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)
-
+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