first version of kernel "basic_rg"

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

diff --git a/helm/software/lambda-delta/basic_rg/brg.ml b/helm/software/lambda-delta/basic_rg/brg.ml
index 45777ead4f41d41dcc1ab793d5473a35b54df016..36e4fefe811adb1228d84443c76b4302fb1b17ac 100644 (file)
--- a/helm/software/lambda-delta/basic_rg/brg.ml
+++ b/helm/software/lambda-delta/basic_rg/brg.ml
@@ -24,3 +24,13 @@ type term = Sort of int                     (* hierarchy index *)
 type obj = int * uri * bind * term (* age, uri, binder, contents *)
 
 type item = obj option
+
+type hierarchy = int -> int
+
+(* Currified constructors ***************************************************)
+
+let cast u t = Cast (u, t)
+
+let appl u t = Appl (u, t)
+
+let bind id b u t = Bind (id, b, u, t)