X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Flambda-delta%2Ftoplevel%2FmetaAut.ml;h=5b85e46cbea703dd21fafe6f53b7242c6b5025b5;hb=93d31ce53c47c6b68582cc8ed6f9475047865a89;hp=e94fd37bcd0288a32ccb8fb75bd1d3fcee3006c8;hpb=b00b8de85c5ae6c5fbb6f47dc559bf4cfcf2a5b6;p=helm.git diff --git a/helm/software/lambda-delta/toplevel/metaAut.ml b/helm/software/lambda-delta/toplevel/metaAut.ml index e94fd37bc..5b85e46cb 100644 --- a/helm/software/lambda-delta/toplevel/metaAut.ml +++ b/helm/software/lambda-delta/toplevel/metaAut.ml @@ -23,36 +23,35 @@ * 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 *) + line: int; (* line number *) explicit: bool (* need explicit context root? *) } 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 = []; line = 1; 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 @@ -76,16 +75,16 @@ let relax_opt_qid f = function | None -> f None | Some qid -> let f qid = f (Some qid) in relax_qid f qid -let resolve_gref f st lenv gref = +let resolve_gref f st local lenv gref = let rec get_local f i = function | [] -> f None | (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,37 +92,29 @@ 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 + if local then get_local f 0 lenv else f None let resolve_gref_relaxed f st lenv gref = let rec g gref = function - | None -> relax_qid (resolve_gref g st lenv) gref + | None -> relax_qid (resolve_gref g st false lenv) gref | Some resolved -> f gref resolved 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 + resolve_gref g st true lenv gref + +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) @@ -143,10 +134,11 @@ let rec xlate_term f st lenv = function 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 l = List.length lenv in + let map1 f = xlate_term f st lenv in + let map2 f (name, _) = f (M.GRef (l, name, [])) in let f tail = - let f args = f (M.GRef (name, args)) in + let f args = f (M.GRef (l, name, args)) in let f defs = Cps.list_rev_map_append f map2 defs ~tail in Cps.list_sub_strict f defs args in @@ -171,11 +163,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, []) @@ -183,8 +177,9 @@ let xlate_item f st = function let f pars = let f name = let f ww = - let entry = (pars, name, ww, None) in - f {st with genv = entry :: st.genv} + let entry = (st.line, pars, name, ww, None) in + H.add st.henv name pars; + f {st with genv = entry :: st.genv; line = succ st.line} in xlate_term f st pars w in @@ -195,8 +190,9 @@ let xlate_item f st = function let f pars = let f name = let f ww vv = - let entry = (pars, name, ww, Some (trans, vv)) in - f {st with genv = entry :: st.genv} + let entry = (st.line, pars, name, ww, Some (trans, vv)) in + H.add st.henv name pars; + f {st with genv = entry :: st.genv; line = succ st.line} in let f ww = xlate_term (f ww) st pars v in xlate_term f st pars w @@ -207,4 +203,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