From: Ferruccio Guidi Date: Mon, 30 Jun 2008 19:34:06 +0000 (+0000) Subject: we improved the data structures used in the translation to the intermediate X-Git-Tag: make_still_working~4980 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=f4683c14c4b45e1844a4cfa91b706f41096ad98e;p=helm.git 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 e94fd37bc..52aa7314d 100644 --- 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 c6ad99df9..f7839a6f9 100644 --- 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 ] ..." in - let help_S = " Set summary level" in + let help = "Usage: helena [ -V | -Ss ] ..." in + let help_S = " Set summary level" in let help_V = " Show version information" in + let help_s = " 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