- the connections between the intermediate language and the "bag"

[helm.git] / helm / software / lambda-delta / src / complete_rg / crg.ml

diff --git a/helm/software/lambda-delta/src/complete_rg/crg.ml b/helm/software/lambda-delta/src/complete_rg/crg.ml
index 07305e9c124630eac45bbad21c6de59b2683c006..5a394f4f8372f3411430137b45e3da9f9a61d827 100644 (file)
--- a/helm/software/lambda-delta/src/complete_rg/crg.ml
+++ b/helm/software/lambda-delta/src/complete_rg/crg.ml
@@ -12,6 +12,7 @@
 (* kernel version: complete, relative, global *)
 (* note          : fragment of complete lambda-delta serving as abstract layer *) 
 
+module C = Cps
 module E = Entity
 module N = Level
 
@@ -39,6 +40,18 @@ type entity = term E.entity
 
 (* helpers ******************************************************************)
 
+let rec tshift t = function
+   | ESort           -> t
+   | EBind (e, a, b) -> tshift (TBind (a, b, t)) e
+   | EProj (e, a, d) -> tshift (TProj (a, d, t)) e
+
+let tshift c t = tshift t c
+
+let rec eshift f c = function
+   | ESort           -> f c
+   | EBind (e, a, b) -> let f ee = f (EBind (ee, a, b)) in eshift f c e
+   | EProj (e, a, d) -> let f ee = f (EProj (ee, a, d)) in eshift f c e
+
 let empty_lenv = ESort
 
 let push_bind f lenv a b = f (EBind (lenv, a, b))
@@ -71,7 +84,7 @@ let resolve_lref err f id lenv =
        let err kk = aux f (succ i) (k + kk) tl in
        let f j = f i j (k + j) in
        E.resolve err f id a
-     | EProj _                -> assert false (* TODO *)
+     | EProj (tl, _, d)       -> aux f i k (eshift C.start tl d)
    in
    aux f 0 0 lenv
 
@@ -99,7 +112,7 @@ let get_index err f i j lenv =
         if E.count_names a > j then f (k + j) else err i
       | EBind (tl, a, _)           -> 
          aux f (pred i) (k + E.count_names a) tl
-      | EProj _                    -> assert false (* TODO *)
+      | EProj (tl, _, d)           -> aux f i k (eshift C.start tl d)
    in
    aux f i 0 lenv
 
@@ -115,6 +128,6 @@ let rec get i = function
    | EBind (e, _, Void 0)       -> get i e
    | EBind (e, a, b) when i = 0 -> e, a, b
    | EBind (e, _, _)            -> get (pred i) e
-   | EProj _                    -> assert false (* TODO *)
+   | EProj (e, _, d)            -> get i (eshift C.start e d)
  
 let get e i = get i e