we improved the data structures used in the translation to the intermediate

language

diff --git a/helm/software/lambda-delta/toplevel/metaAut.ml b/helm/software/lambda-delta/toplevel/metaAut.ml
index e94fd37bcd0288a32ccb8fb75bd1d3fcee3006c8..52aa7314dfd2aa48c945b7769e8028be956da152 100644 (file)
--- a/helm/software/lambda-delta/toplevel/metaAut.ml
+++ b/helm/software/lambda-delta/toplevel/metaAut.ml
@@ -23,17 +23,20 @@
  * 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 environment = (M.qid, M.pars) H.t
 
-type context = (M.qid * M.term * context_node) list (* context: son, parent *)
+type context_node = M.qid option (* context node: None = root *)
 
 type status = {
    genv: M.environment;      (* global environment *)
+   henv: environment;        (* optimized global environment *)
    path: M.id list;          (* current section path *) 
-   cnt: context;             (* context *)
+   hcnt: environment;        (* optimized context *)   
    node: context_node;       (* current context node *)
    nodes: context_node list; (* context node list *)
    explicit: bool            (* need explicit context root? *)
@@ -42,17 +45,12 @@ type status = {
 type resolver = Local of int
               | Global of M.pars
 
-let initial_status = {
-   genv = []; path = []; cnt = []; node = None; nodes = []; explicit = true
-}
+let hsize = 11 (* hash tables initial size *)
 
-let find f cnt qid =
-   let rec aux f = function
-      | (name, w, node) :: tl when name = qid -> f tl (Some (w, node))
-      | _ :: tl                               -> aux f tl
-      | []                                    -> f cnt None
-   in
-   aux f cnt
+let initial_status size = {
+   genv = []; path = []; node = None; nodes = []; explicit = true;
+   henv = H.create size; hcnt = H.create size
+}
 
 let complete_qid f st (id, is_local, qs) =
    let f qs = f (id, qs) in
@@ -82,10 +80,10 @@ let resolve_gref f st lenv gref =
      | (name, _) :: _ when fst name = fst gref -> f (Some i)
      | _ :: tl                                 -> get_local f (succ i) tl
   in
-  let rec get_global f = function
-     | []                                       -> f None
-     | (args, name, _, _) :: _ when name = gref -> f (Some args)
-     | _ :: tl                                  -> get_global f tl
+  let get_global f =
+     try 
+        let args = H.find st.henv gref in f (Some args)
+     with Not_found -> f None
   in
   let g = function
       | Some args -> f gref (Some (Global args))
@@ -93,7 +91,7 @@ let resolve_gref f st lenv gref =
   in
   let f = function
       | Some i -> f gref (Some (Local i))
-      | None   -> get_global g st.genv
+      | None   -> get_global g
   in
   get_local f 0 lenv
 
@@ -104,26 +102,18 @@ let resolve_gref_relaxed f st lenv gref =
    in
    resolve_gref g st lenv gref
 
-let get_pars f st pars node =
-   let rec aux f cnt pars = function
-      | None              -> 
-         let f pars = f pars None in
-        Cps.list_rev f pars
-      | Some name as node ->
-        let f cnt = function
-           | Some (w, node) -> aux f cnt ((name, w) :: pars) node
-           | None           -> f pars (Some node)
-        in
-        find f cnt name
-   in
-   aux f st.cnt pars node
+let get_pars f st = function
+   | None              -> f [] None
+   | Some name as node ->
+      try let pars = H.find st.hcnt name in f pars None
+      with Not_found -> f [] (Some node)
 
 let get_pars_relaxed f st =
    let rec g pars = function
       | None      -> f pars 
-      | Some node -> relax_opt_qid (get_pars g st pars) node
+      | Some node -> relax_opt_qid (get_pars g st) node
    in
-   get_pars g st [] st.node
+   get_pars g st st.node
 
 let rec xlate_term f st lenv = function
    | A.Sort sort         -> f (M.Sort sort)
@@ -171,11 +161,13 @@ let xlate_item f st = function
       complete_qid f st name
    | A.Block (name, w)         ->
       let f name = 
-         let f ww = 
-           let st = {st with cnt = (name, ww, st.node) :: st.cnt} in
-           f {st with node = Some name}
+         let f pars =
+           let f ww = 
+              H.add st.hcnt name ((name, ww) :: pars);
+              f {st with node = Some name}
+           in
+            xlate_term f st pars w
         in
-         let f pars = xlate_term f st pars w in
          get_pars_relaxed f st
       in
       complete_qid f st (name, true, [])
@@ -184,6 +176,7 @@ let xlate_item f st = function
          let f name = 
             let f ww =
               let entry = (pars, name, ww, None) in
+              H.add st.henv name pars;
               f {st with genv = entry :: st.genv}
            in
            xlate_term f st pars w
@@ -196,6 +189,7 @@ let xlate_item f st = function
          let f name = 
             let f ww vv = 
               let entry = (pars, name, ww, Some (trans, vv)) in
+              H.add st.henv name pars;
               f {st with genv = entry :: st.genv}
            in
            let f ww = xlate_term (f ww) st pars v in
@@ -207,4 +201,4 @@ let xlate_item f st = function
 
 let meta_of_aut f book =
    let f st = f st.genv in
-   Cps.list_fold_left f xlate_item initial_status book
+   Cps.list_fold_left f xlate_item (initial_status hsize) book

diff --git a/helm/software/lambda-delta/toplevel/top.ml b/helm/software/lambda-delta/toplevel/top.ml
index c6ad99df972646b9137ba67c3d5bde713f349fc6..f7839a6f9c939fa59c7b56d391b1e148bcb430dc 100644 (file)
--- a/helm/software/lambda-delta/toplevel/top.ml
+++ b/helm/software/lambda-delta/toplevel/top.ml
@@ -30,8 +30,10 @@ module MO = MetaOutput
 let main =
    let version_string = "Helena Checker 0.8.0 M (June 2008)" in
    let summary = ref 0 in
+   let stage = ref 1 in
    let set_summary i = summary := i in
    let print_version () = print_endline version_string; exit 0 in
+   let set_stage i = stage := i in
    let read_file name =
       if !summary > 0 then
          Printf.printf "Processing file: %s\n" name; flush stdout;
@@ -45,12 +47,14 @@ let main =
          if !summary > 1 then
            MO.count (MO.print_counters Cps.id) MO.initial_counters env
       in
-      MA.meta_of_aut f book
+      if !stage > 0 then MA.meta_of_aut f book
    in
-   let help = "Usage: helena [ -V | -S <number> ] <file> ..." in
-   let help_S = "<number>  Set summary level" in   
+   let help = "Usage: helena [ -V | -Ss <number> ] <file> ..." in
+   let help_S = "<number>  Set summary level" in
    let help_V = " Show version information" in   
+   let help_s = "<number>  Set translation stage" in
    Arg.parse [
       ("-S", Arg.Int set_summary, help_S);
-      ("-V", Arg.Unit print_version, help_V)
+      ("-V", Arg.Unit print_version, help_V);
+      ("-s", Arg.Int set_stage, help_s);
    ] read_file help