the old intermediate language (meta) is now obsolete

[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 9020048af077f7f8e95f7797afc5188b3887fb47..07305e9c124630eac45bbad21c6de59b2683c006 100644 (file)
--- a/helm/software/lambda-delta/src/complete_rg/crg.ml
+++ b/helm/software/lambda-delta/src/complete_rg/crg.ml
@@ -45,14 +45,20 @@ let push_bind f lenv a b = f (EBind (lenv, a, b))
 
 let push_proj f lenv a e = f (EProj (lenv, a, e))
 
-let push2 err f lenv attr ?t () = match lenv, t with
-   | EBind (e, a, Abst (n, ws)), Some t -> 
+let push2 err f lenv ?attr ?t () = match lenv, attr, t with
+   | EBind (e, a, Abst (n, ws)), Some attr, Some t -> 
       f (EBind (e, (attr :: a), Abst (n, t :: ws)))
-   | EBind (e, a, Abbr vs), Some t      ->
+   | EBind (e, a, Abst (n, ws)), None, Some t      -> 
+      f (EBind (e, a, Abst (n, t :: ws)))
+   | EBind (e, a, Abbr vs), Some attr, Some t      ->
       f (EBind (e, (attr :: a), Abbr (t :: vs)))
-   | EBind (e, a, Void n), None         ->
+   | EBind (e, a, Abbr vs), None, Some t           ->
+      f (EBind (e, a, Abbr (t :: vs)))
+   | EBind (e, a, Void n), Some attr, None         ->
       f (EBind (e, (attr :: a), Void (succ n)))
-   | _                             -> err ()
+   | EBind (e, a, Void n), None, None              ->
+      f (EBind (e, a, Void (succ n)))
+   | _                                             -> err ()
 
 (* this id not tail recursive *)
 let resolve_lref err f id lenv =
@@ -101,3 +107,14 @@ let rec names_of_lenv ns = function
    | ESort            -> ns
    | EBind (tl, a, _) -> names_of_lenv (E.rev_append_names ns a) tl
    | EProj (tl, _, e) -> names_of_lenv (names_of_lenv ns e) tl
+
+let rec get i = function
+   | ESort                      -> ESort, [], Void 0 
+   | EBind (e, _, Abst (_, []))
+   | EBind (e, _, Abbr [])
+   | 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 *)
+ 
+let get e i = get i e