- initial support for abstractions with explicit levels

[helm.git] / helm / software / lambda-delta / src / basic_rg / brg.ml

diff --git a/helm/software/lambda-delta/src/basic_rg/brg.ml b/helm/software/lambda-delta/src/basic_rg/brg.ml
index d2a0b99873cd93fd146801a7e17fb53bbb1355c7..bc6eb57277787753485621798a8b3949597f7e92 100644 (file)
--- a/helm/software/lambda-delta/src/basic_rg/brg.ml
+++ b/helm/software/lambda-delta/src/basic_rg/brg.ml
@@ -13,14 +13,15 @@
 (* note          : ufficial basic lambda-delta *) 
 
 module E = Entity
+module N = Level
 
 type uri = E.uri
 type id = E.id
 type attrs = E.attrs
 
-type bind = Void         (*      *)
-          | Abst of term (* type *)
-          | Abbr of term (* body *)
+type bind = Void                   (*             *)
+          | Abst of N.level * term (* level, type *)
+          | Abbr of term           (* body        *)
 
 and term = Sort of attrs * int         (* attrs, hierarchy index *)
          | LRef of attrs * int         (* attrs, position index *)
@@ -43,7 +44,7 @@ let mk_uri si root s =
 
 (* Currified constructors ***************************************************)
 
-let abst w = Abst w
+let abst n w = Abst (n, w)
 
 let abbr v = Abbr v
 
@@ -55,7 +56,7 @@ 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_abst n a u t = Bind (a, Abst (n, u), t)
 
 let bind_abbr a v t = Bind (a, Abbr v, t)