\ / 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
-type bind = Abst | Abbr (* abstraction, abbreviation *)
+type bind = Void (* exclusion *)
+ | Abst of term (* abstraction *)
+ | Abbr of term (* abbreviation *)
+
+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 = (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
-type 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 * term (* name, binder, content, scope *)
+let contents f es = f es
-type entry = uri * bind * term (* uri, binder, contents *)
+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
-type item = entry option
+let rec name f = function
+ | [] -> f None
+ | Name (r, n) :: _ -> f (Some (r, n))
+ | _ :: tl -> name f tl