metaAut.xlate_item started

[helm.git] / helm / software / lambda-delta / toplevel / metaAut.ml

diff --git a/helm/software/lambda-delta/toplevel/metaAut.ml b/helm/software/lambda-delta/toplevel/metaAut.ml
index 2cce50a83fdeb9cb16b224aeda7230b4921b1d39..ac481a21d0f2b0ab95979b74aca7d73da411eadd 100644 (file)
--- a/helm/software/lambda-delta/toplevel/metaAut.ml
+++ b/helm/software/lambda-delta/toplevel/metaAut.ml
@@ -29,7 +29,7 @@ module A = Aut
 
 type context_node = M.qid option (* context node: None = root *)
 
-type context = (M.qid, context_node) H.t (* context: son, parent *)
+type context = (M.qid, M.term * context_node) H.t (* context: son, parent *)
 
 type status = {
    genv: M.environment; (* global environment *)
@@ -58,7 +58,7 @@ let resolve_gref f st lenv gref =
      | _ :: tl                         -> get_local f (succ i) tl
   in
   let rec get_global f = function
-     | []                                       -> None
+     | []                                       -> f None
      | (args, name, _, _) :: _ when name = gref -> f (Some args)
      | _ :: tl                                  -> get_global f tl
   in
@@ -102,3 +102,27 @@ let rec xlate_term f st lenv = function
       in
       let f name = resolve_gref (f name) st lenv name in
       complete_qid f st name
+
+let xlate_item f st = function
+   | A.Section (Some name)     ->
+      f {st with path = name :: st.path}
+   | A.Section None            ->
+      begin match st.path with
+         | []      -> assert false
+        | _ :: tl -> f {st with path = tl}
+      end
+   | A.Context None            ->
+      f {st with node = None}
+   | A.Context (Some name)     ->
+      let f name = f {st with node = Some name} in
+      complete_qid f st name
+   | A.Block (name, w)         ->
+      let f name ww = H.add st.cnt name (ww, st.node); f st in
+      let f name = xlate_term (f name) st [] w in
+      complete_qid f st (name, true, [])   
+   | A.Decl (name, w)          -> f st 
+   | A.Def (name, w, trans, v) -> f st
+
+let meta_of_aut f book =
+   let f st = f st.genv in
+   Cps.list_fold_left f xlate_item initial_status book