transformation from automath to intermediate language 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
new file mode 100644 (file)
index 0000000..2cce50a
--- /dev/null
+++ b/helm/software/lambda-delta/toplevel/metaAut.ml
@@ -0,0 +1,104 @@
+(* 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/.
+ *)
+
+module H = Hashtbl
+module M = Meta
+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 status = {
+   genv: M.environment; (* global environment *)
+   path: M.id list;     (* current section path *) 
+   cnt: context;        (* context *)
+   node: context_node;  (* current context node *)
+   explicit: bool       (* need explicit context root? *)
+}
+
+type resolver = Local of int
+              | Global of M.pars
+             | Unresolved
+
+let initial_status = {
+   genv = []; path = []; cnt = H.create 11; node = None; explicit = true
+}
+
+let complete_qid f st (id, is_local, qs) =
+   let f qs = f (id, qs) in
+   if is_local then Cps.list_rev_append f st.path ~tail:qs else f qs
+
+let resolve_gref f st lenv gref =
+  let rec get_local f i = function
+     | []                              -> f None
+     | (name, _) :: _ when name = gref -> f (Some i)
+     | _ :: tl                         -> get_local f (succ i) tl
+  in
+  let rec get_global f = function
+     | []                                       -> None
+     | (args, name, _, _) :: _ when name = gref -> f (Some args)
+     | _ :: tl                                  -> get_global f tl
+  in
+  let g = function
+      | Some args -> f (Global args)
+      | None      -> f Unresolved
+  in
+  let f = function
+      | Some i -> f (Local i)
+      | None   -> get_global g st.genv
+  in
+  get_local f 0 lenv
+
+let rec xlate_term f st lenv = function
+   | A.Sort sort         -> f (M.Sort sort)
+   | A.Appl (v, t)       ->
+      let f vv tt = f (M.Appl (vv, tt)) in
+      let f vv = xlate_term (f vv) st lenv t in
+      xlate_term f st lenv v
+   | A.Abst (name, w, t) ->
+      let add name w lenv = 
+         let f name = (name, w) :: lenv in
+         complete_qid f st (name, true, []) 
+      in
+      let f ww tt = f (M.Abst (name, ww, tt)) in
+      let f ww = xlate_term (f ww) st (add name ww lenv) t in
+      xlate_term f st lenv w
+   | A.GRef (name, args) ->
+      let f name = function
+        | Local i     -> f (M.LRef i)
+         | Global defs -> 
+            let map1 f = xlate_term f st lenv in
+           let map2 f (name, _) = f (M.GRef (name, [])) in
+            let f tail =          
+              let f args = f (M.GRef (name, args)) in
+               let f defs = Cps.list_rev_map_append f map2 defs ~tail in
+              Cps.list_sub_strict f defs args
+           in
+           Cps.list_map f map1 args
+        | Unresolved  -> assert false
+      in
+      let f name = resolve_gref (f name) st lenv name in
+      complete_qid f st name