new syntax of abstractions propagated to complete_rg

[helm.git] / helm / software / helena / src / complete_rg / crg.ml

diff --git a/helm/software/helena/src/complete_rg/crg.ml b/helm/software/helena/src/complete_rg/crg.ml
index 455eb6ed4547b193ca52becf1e6fcd4c0e07554e..ae1a8122238451477aeab5040f9838c380aa52bf 100644 (file)
--- a/helm/software/helena/src/complete_rg/crg.ml
+++ b/helm/software/helena/src/complete_rg/crg.ml
@@ -20,22 +20,22 @@ type uri = E.uri
 type id = E.id
 type attrs = E.node_attrs
 
-type bind = Abst of N.layer * term      (* layer, type *)
-          | Abbr of term                (* body *)
-          | Void                        (* *)
-
-and term = TSort of attrs * int         (* attrs, hierarchy index *)
-         | TLRef of attrs * int         (* attrs, position indexe *)
-         | TGRef of attrs * uri         (* attrs, reference *)
-         | TCast of attrs * term * term (* attrs, domain, element *)
-         | TAppl of attrs * term * term (* attrs, argument, function *)
-        | TBind of attrs * bind * term (* attrs, binder, scope *)
-        | TProj of attrs * lenv * term (* attrs, closure, member *)
-
-and lenv = ESort                        (* top *)
-         | EBind of lenv * attrs * bind (* environment, attrs, binder *)
-         | EAppl of lenv * attrs * term (* environment, attrs, argument *)
-         | EProj of lenv * attrs * lenv (* environment, attrs, closure *) 
+type bind = Abst of bool * N.layer * term (* x-reduced?, layer, type *)
+          | Abbr of term                  (* body *)
+          | Void                          (* *)
+
+and term = TSort of attrs * int           (* attrs, hierarchy index *)
+         | TLRef of attrs * int           (* attrs, position indexe *)
+         | TGRef of attrs * uri           (* attrs, reference *)
+         | TCast of attrs * term * term   (* attrs, domain, element *)
+         | TAppl of attrs * term * term   (* attrs, argument, function *)
+        | TBind of attrs * bind * term   (* attrs, binder, scope *)
+        | TProj of attrs * lenv * term   (* attrs, closure, member *)
+
+and lenv = ESort                          (* top *)
+         | EBind of lenv * attrs * bind   (* environment, attrs, binder *)
+         | EAppl of lenv * attrs * term   (* environment, attrs, argument *)
+         | EProj of lenv * attrs * lenv   (* environment, attrs, closure *) 
 
 type entity = term E.entity
 
@@ -117,11 +117,11 @@ let rec mem err f e b = match e with
 
 let replace f n0 e =
    let rec aux f = function
-      | ESort                     -> f ESort
-      | EBind (e, a, Abst (n, w)) -> aux (push_bind f a (Abst (n0, w))) e
-      | EBind (e, a, b)           -> aux (push_bind f a b) e
-      | EAppl (e, a, v)           -> aux (push_appl f a v) e
-      | EProj (e, a, d)           -> let f d = aux (push_proj f a d) e in aux f d
+      | ESort                        -> f ESort
+      | EBind (e, a, Abst (x, n, w)) -> aux (push_bind f a (Abst (x, n0, w))) e
+      | EBind (e, a, b)              -> aux (push_bind f a b) e
+      | EAppl (e, a, v)              -> aux (push_appl f a v) e
+      | EProj (e, a, d)              -> let f d = aux (push_proj f a d) e in aux f d
 
    in
    aux f e