drg: we added the "positive projection" in environments

[helm.git] / helm / software / lambda-delta / dual_rg / drgOutput.ml

diff --git a/helm/software/lambda-delta/dual_rg/drgOutput.ml b/helm/software/lambda-delta/dual_rg/drgOutput.ml
index f6782d5569d122ca817e0f22cba57da86de5c87c..c291cbf8a60df19827974e34f8f5c237d3e70210 100644 (file)
--- a/helm/software/lambda-delta/dual_rg/drgOutput.ml
+++ b/helm/software/lambda-delta/dual_rg/drgOutput.ml
@@ -16,33 +16,34 @@ let rec list_iter map l f = match l with
    | []       -> f
    | hd :: tl -> map hd (list_iter map tl f)
 
-let rec lenv_iter map l f = match l with
-   | D.Null              -> f
-   | D.Cons (lenv, a, b) -> lenv_iter map lenv (map a b f)
+let rec lenv_iter map1 map2 l f = match l with
+   | D.ESort              -> f
+   | D.EBind (lenv, a, b) -> lenv_iter map1 map2 lenv (map1 a b f)
+   | D.EProj (lenv, a, e) -> lenv_iter map1 map2 lenv (map2 a e f)
 
 let rec exp_term t f = match t with
-   | D.Sort (a, h)       ->
+   | D.TSort (a, h)       ->
       let attrs = [X.position h; X.name a] in
       X.tag X.sort attrs f
-   | D.LRef (a, i, j)    ->
+   | D.TLRef (a, i, j)    ->
       let attrs = [X.position i; X.offset j; X.name a] in
       X.tag X.lref attrs f
-   | D.GRef (a, n)       ->
+   | D.TGRef (a, n)       ->
       let attrs = [X.uri n; X.name a] in
       X.tag X.gref attrs f   
-   | D.Cast (a, u, t)    ->
+   | D.TCast (a, u, t)    ->
       let attrs = [] in
       X.tag X.cast attrs (exp_term t f) ~contents:(exp_term u)
-   | D.Appl (a, vs, t)   ->
+   | D.TAppl (a, vs, t)   ->
       let attrs = [X.arity (List.length vs)] in
       X.tag X.appl attrs (exp_term t f) ~contents:(list_iter exp_term vs)
-   | D.Proj (a, lenv, t) ->
+   | D.TProj (a, lenv, t) ->
       let attrs = [] in
-      X.tag X.proj attrs (exp_term t f) ~contents:(lenv_iter exp_lenv lenv)
-   | D.Bind (a, b, t) ->
-      exp_lenv a b (exp_term t f)
+      X.tag X.proj attrs (exp_term t f) ~contents:(lenv_iter exp_bind exp_eproj lenv)
+   | D.TBind (a, b, t) ->
+      exp_bind a b (exp_term t f)
 
-and exp_lenv a b f = match b with
+and exp_bind a b f = match b with
    | D.Abst ws ->
       let attrs = [X.name a; X.mark a; X.arity (List.length ws)] in
       X.tag X.abst attrs f ~contents:(list_iter exp_term ws)
@@ -53,4 +54,8 @@ and exp_lenv a b f = match b with
       let attrs = [X.name a; X.mark a; X.arity n] in
       X.tag X.void attrs f
 
+and exp_eproj a lenv f =
+   let attrs = [] in
+   X.tag X.proj attrs f ~contents:(lenv_iter exp_bind exp_eproj lenv)
+
 let export_term = exp_term