new options activated

[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 ae1a8122238451477aeab5040f9838c380aa52bf..ea3ec54bfc4b101799e1b59ca9316ddfe010f598 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 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 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 * bool * term * term  (* attrs, extended?, 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 * bool * term  (* environment, attrs, extended?, argument *)
+         | EProj of lenv * attrs * lenv         (* environment, attrs, closure *)
 
 type entity = term E.entity
 
@@ -45,43 +45,43 @@ let empty_lenv = ESort
 
 let push_bind f a b lenv = f (EBind (lenv, a, b))
 
-let push_appl f a t lenv = f (EAppl (lenv, a, t))
+let push_appl f a x t lenv = f (EAppl (lenv, a, x, t))
 
 let push_proj f a e lenv = f (EProj (lenv, a, e))
 
 let add_bind f a b t = f (TBind (a, b, t))
 
-let add_appl f a v t = f (TAppl (a, v, t))
+let add_appl f a x v t = f (TAppl (a, x, v, t))
 
 let add_proj f a e t = f (TProj (a, e, t))
 
 let rec shift f c t = match c with
-   | ESort           -> f t
-   | EBind (e, a, b) -> add_bind (shift f e) a b t
-   | EAppl (e, a, v) -> add_appl (shift f e) a v t
-   | EProj (e, a, d) -> add_proj (shift f e) a d t
+   | ESort              -> f t
+   | EBind (e, a, b)    -> add_bind (shift f e) a b t
+   | EAppl (e, a, x, v) -> add_appl (shift f e) a x v t
+   | EProj (e, a, d)    -> add_proj (shift f e) a d t
 
 let rec append f c = function
-   | ESort           -> f c
-   | EBind (e, a, b) -> append (push_bind f a b) c e
-   | EAppl (e, a, t) -> append (push_appl f a t) c e
-   | EProj (e, a, d) -> append (push_proj f a d) c e
+   | ESort              -> f c
+   | EBind (e, a, b)    -> append (push_bind f a b) c e
+   | EAppl (e, a, x, t) -> append (push_appl f a x t) c e
+   | EProj (e, a, d)    -> append (push_proj f a d) c e
 
 let resolve_lref err f id lenv =
    let rec aux i = function
-     | ESort             -> err ()
-     | EAppl (tl, _, _)  -> aux i tl
-     | EBind (tl, a, _)  ->
+     | ESort                -> err ()
+     | EAppl (tl, _, _, _)  -> aux i tl
+     | EBind (tl, a, _)     ->
         let f id0 _ = if id0 = id then f a i else aux (succ i) tl in
         let err () = aux (succ i) tl in
         E.name err f a
-     | EProj (tl, _, d)  -> append (aux i) tl d
+     | EProj (tl, _, d)     -> append (aux i) tl d
    in
    aux 0 lenv
 
 let rec get_name err f i = function
    | ESort                      -> err i
-   | EAppl (tl, _, _)           -> get_name err f i tl
+   | EAppl (tl, _, _, _)        -> get_name err f i tl
    | EBind (_, a, _) when i = 0 -> 
       let err () = err i in
       E.name err f a
@@ -94,7 +94,7 @@ let rec get e i = match e with
    | ESort                      -> ESort, E.empty_node, Void
    | EBind (e, a, b) when i = 0 -> e, a, b
    | EBind (e, _, _)            -> get e (pred i)
-   | EAppl (e, _, _)            -> get e i
+   | EAppl (e, _, _, _)         -> get e i
    | EProj (e, _, d)            -> get (append C.start e d) i
 
 let rec sub_list_strict f e l = match e, l with
@@ -108,19 +108,19 @@ let rec fold_names f map x = function
    | _                                      -> assert false
 
 let rec mem err f e b = match e with
-   | ESort           -> err ()
-   | EBind (e, a, _) ->
+   | ESort              -> err ()
+   | EBind (e, a, _)    ->
       if a.E.n_name = b.E.n_name then f () else mem err f e b
-   | EAppl (e, _, _) -> mem err f e b
-   | EProj (e, _, d) -> 
+   | EAppl (e, _, _, _) -> mem err f e b
+   | EProj (e, _, d)    -> 
       let err () = mem err f e b in mem err f d b
 
 let replace f n0 e =
    let rec aux f = function
       | ESort                        -> f ESort
-      | EBind (e, a, Abst (x, n, w)) -> aux (push_bind f a (Abst (x, n0, w))) e
+      | EBind (e, a, Abst (r, n, w)) -> aux (push_bind f a (Abst (r, 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
+      | EAppl (e, a, x, v)           -> aux (push_appl f a x v) e
       | EProj (e, a, d)              -> let f d = aux (push_proj f a d) e in aux f d
 
    in