V_______________________________________________________________ *)
(* kernel version: basic, relative, global *)
-(* note : ufficial basic \lambda\delta *)
+(* note : ufficial basic \lambda\delta version 3 *)
module N = Layer
module E = Entity
type uri = E.uri
type attrs = E.node_attrs
-type bind = Void (* *)
- | Abst of N.layer * term (* layer, type *)
- | Abbr of term (* body *)
+(* x-reduced abstractions are output by RTM only *)
+type bind = Void (* *)
+ | Abst of bool * N.layer * term (* x-reduced?, layer, type *)
+ | Abbr of term (* body *)
and term = Sort of attrs * int (* attrs, hierarchy index *)
| LRef of attrs * int (* attrs, position index *)
(* Currified constructors ***************************************************)
-let abst n w = Abst (n, w)
+let abst x n w = Abst (x, n, w)
let abbr v = Abbr v
let bind a b t = Bind (a, b, t)
-let bind_abst n a u t = Bind (a, Abst (n, u), t)
+let bind_abst x n a u t = Bind (a, Abst (x, n, u), t)
-let bind_abbr a v t = Bind (a, Abbr v, t)
+let bind_abbr a u t = Bind (a, Abbr u, t)
let bind_void a t = Bind (a, Void, t)