From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Mon, 23 Jun 2008 21:04:44 +0000 (+0000)
Subject: metaAut.xlate_item started
X-Git-Tag: make_still_working~4996
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=98d596e4a26c596ef17b3c7ed48c86f1cf4d4061;p=helm.git

metaAut.xlate_item started
---

diff --git a/helm/software/lambda-delta/.depend.opt b/helm/software/lambda-delta/.depend.opt
index 4df20fa26..a0d42bdd9 100644
--- a/helm/software/lambda-delta/.depend.opt
+++ b/helm/software/lambda-delta/.depend.opt
@@ -8,8 +8,11 @@ automath/autLexer.cmo: automath/autParser.cmi
 automath/autLexer.cmx: automath/autParser.cmx 
 toplevel/meta.cmo: automath/aut.cmx 
 toplevel/meta.cmx: automath/aut.cmx 
-toplevel/metaAut.cmo: toplevel/meta.cmx cps/cps.cmx automath/aut.cmx 
-toplevel/metaAut.cmx: toplevel/meta.cmx cps/cps.cmx automath/aut.cmx 
+toplevel/metaAut.cmi: toplevel/meta.cmx automath/aut.cmx 
+toplevel/metaAut.cmo: toplevel/meta.cmx cps/cps.cmx automath/aut.cmx \
+    toplevel/metaAut.cmi 
+toplevel/metaAut.cmx: toplevel/meta.cmx cps/cps.cmx automath/aut.cmx \
+    toplevel/metaAut.cmi 
 toplevel/top.cmo: cps/cps.cmx automath/autParser.cmi automath/autLexer.cmx \
     automath/autHelpers.cmi 
 toplevel/top.cmx: cps/cps.cmx automath/autParser.cmx automath/autLexer.cmx \
diff --git a/helm/software/lambda-delta/toplevel/metaAut.ml b/helm/software/lambda-delta/toplevel/metaAut.ml
index 2cce50a83..ac481a21d 100644
--- 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
diff --git a/helm/software/lambda-delta/toplevel/metaAut.mli b/helm/software/lambda-delta/toplevel/metaAut.mli
new file mode 100644
index 000000000..1172424c7
--- /dev/null
+++ b/helm/software/lambda-delta/toplevel/metaAut.mli
@@ -0,0 +1,26 @@
+(* Copyright (C) 2000, HELM Team.
+ * 
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ * 
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ * 
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA  02111-1307, USA.
+ * 
+ * For details, see the HELM World-Wide-Web page,
+ * http://cs.unibo.it/helm/.
+ *)
+
+val meta_of_aut: (Meta.environment -> 'a) -> Aut.book -> 'a