-module U = NUri
-module A = Aut
+(*
+ ||M|| This file is part of HELM, an Hypertextual, Electronic
+ ||A|| Library of Mathematics, developed at the Computer Science
+ ||T|| Department, University of Bologna, Italy.
+ ||I||
+ ||T|| HELM is free software; you can redistribute it and/or
+ ||A|| modify it under the terms of the GNU General Public License
+ \ / version 2 or (at your option) any later version.
+ \ / This software is distributed as is, NO WARRANTY.
+ V_______________________________________________________________ *)
-type uri = U.uri
-type id = A.id
+(* kernel version: basic, relative, global *)
+(* note : ufficial basic lambda-delta *)
-type binder = Abst | Abbr
+type uri = NUri.uri
+type id = Aut.id
-type term = Sort of int
- | LRef of int
- | GRef of uri
- | Cast of term * term
- | Appl of term * term
- | Bind of id * binder * term * term
-
+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
+
+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