From: Ferruccio Guidi Date: Sat, 6 Dec 2008 14:42:09 +0000 (+0000) Subject: metaAut: now we use hash tables properly (processing time: 2s) X-Git-Tag: make_still_working~4442 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=a3ebffd30c70d8c93a40d06eff578703a586f2b9;p=helm.git metaAut: now we use hash tables properly (processing time: 2s) brgReduction: started --- diff --git a/helm/software/lambda-delta/.depend.opt b/helm/software/lambda-delta/.depend.opt index bfe5ffb87..a00ee1636 100644 --- a/helm/software/lambda-delta/.depend.opt +++ b/helm/software/lambda-delta/.depend.opt @@ -24,6 +24,10 @@ basic_rg/brgEnvironment.cmo: lib/nUri.cmi basic_rg/brg.cmx \ basic_rg/brgEnvironment.cmi basic_rg/brgEnvironment.cmx: lib/nUri.cmx basic_rg/brg.cmx \ basic_rg/brgEnvironment.cmi +basic_rg/brgReduction.cmo: lib/nUri.cmi basic_rg/brgEnvironment.cmi \ + basic_rg/brg.cmx basic_rg/brgReduction.cmi +basic_rg/brgReduction.cmx: lib/nUri.cmx basic_rg/brgEnvironment.cmx \ + basic_rg/brg.cmx basic_rg/brgReduction.cmi toplevel/meta.cmo: lib/nUri.cmi automath/aut.cmx toplevel/meta.cmx: lib/nUri.cmx automath/aut.cmx toplevel/metaOutput.cmi: toplevel/meta.cmx diff --git a/helm/software/lambda-delta/Makefile.common b/helm/software/lambda-delta/Makefile.common index 0adedde84..c4a276b82 100644 --- a/helm/software/lambda-delta/Makefile.common +++ b/helm/software/lambda-delta/Makefile.common @@ -64,5 +64,9 @@ tgz: clean $(H)$(OCAMLOPT) -c $< ifeq ($(MAKECMDGOALS), $(MAIN).opt) - include .depend.opt + include .depend.opt +endif + +ifeq ($(MAKECMDGOALS), test) + include .depend.opt endif diff --git a/helm/software/lambda-delta/basic_rg/Make b/helm/software/lambda-delta/basic_rg/Make index 783502bdc..c40f0cc46 100644 --- a/helm/software/lambda-delta/basic_rg/Make +++ b/helm/software/lambda-delta/basic_rg/Make @@ -1 +1 @@ -brg brgOutput brgEnvironment +brg brgOutput brgEnvironment brgReduction diff --git a/helm/software/lambda-delta/basic_rg/brgReduction.ml b/helm/software/lambda-delta/basic_rg/brgReduction.ml new file mode 100644 index 000000000..b194b00bf --- /dev/null +++ b/helm/software/lambda-delta/basic_rg/brgReduction.ml @@ -0,0 +1,77 @@ +(* + ||M|| This file is part of HELM, an Hypertextual, Electronic + ||A|| Library of Mathematics, developed at the Computer Science + ||T|| Department, University of Bologna, Italy. + ||I|| + ||T|| HELM is free software; you can redistribute it and/or + ||A|| modify it under the terms of the GNU General Public License + \ / version 2 or (at your option) any later version. + \ / This software is distributed as is, NO WARRANTY. + V_______________________________________________________________ *) + +module U = NUri +module B = Brg +module E = BrgEnvironment + +exception LRefNotFound of string Lazy.t + +type environment = int * (B.bind * B.term) list + +type stack = B.term list + +type context = { + g: environment; + l: environment; + s: stack +} + +type whd_result = + | Sort_ of int + | LRef_ of int + | GRef_ of int * U.uri * B.bind + | Abst_ of B.term + +(* Internal functions *******************************************************) + +let push_e f b t (l, e) = + f (succ l, (b, t) :: e) + +let rec find_e f c i = + let (gl, ge), (ll, le) = c.g, c.l in + if i >= gl + ll then raise (LRefNotFound (lazy (string_of_int i))); + let b, t = + if i < gl then List.nth ge (gl - (succ i)) + else List.nth le (gl + ll - (succ i)) + in + f t b + +let rec whd f c t = match t with + | B.Sort h -> f c t (Sort_ h) + | B.GRef uri -> + let f (i, _, b, t) = f c t (GRef_ (i, uri, b)) in + E.get_obj f uri + | B.LRef i -> + let f t = function + | B.Abst -> f c t (LRef_ i) + | B.Abbr -> whd f c t + in + find_e f c i + | B.Appl (v, t) -> whd f {c with s = v :: c.s} t + | B.Bind (_, B.Abbr, v, t) -> + let f l = whd f {c with l = l} t in + push_e f B.Abbr v c.l + | B.Bind (_, B.Abst, w, t) -> + begin match c.s with + | [] -> f c t (Abst_ w) + | v :: tl -> + let f tl l = whd f {c with l = l; s = tl} t in + push_e (f tl) B.Abbr v c.l + end + | B.Cast (_, t) -> whd f c t + +(* Interface functions ******************************************************) + +let push f c b t = + assert (fst c.l = 0 && c.s = []); + let f g = f {c with g = g} in + push_e f b t c.g diff --git a/helm/software/lambda-delta/basic_rg/brgReduction.mli b/helm/software/lambda-delta/basic_rg/brgReduction.mli new file mode 100644 index 000000000..fecf29b83 --- /dev/null +++ b/helm/software/lambda-delta/basic_rg/brgReduction.mli @@ -0,0 +1,14 @@ +(* + ||M|| This file is part of HELM, an Hypertextual, Electronic + ||A|| Library of Mathematics, developed at the Computer Science + ||T|| Department, University of Bologna, Italy. + ||I|| + ||T|| HELM is free software; you can redistribute it and/or + ||A|| modify it under the terms of the GNU General Public License + \ / version 2 or (at your option) any later version. + \ / This software is distributed as is, NO WARRANTY. + V_______________________________________________________________ *) + +exception LRefNotFound of string Lazy.t + +type context diff --git a/helm/software/lambda-delta/toplevel/metaAut.ml b/helm/software/lambda-delta/toplevel/metaAut.ml index 59801dac7..7e18bd1e5 100644 --- a/helm/software/lambda-delta/toplevel/metaAut.ml +++ b/helm/software/lambda-delta/toplevel/metaAut.ml @@ -9,14 +9,15 @@ \ / This software is distributed as is, NO WARRANTY. V_______________________________________________________________ *) -module H = Hashtbl module U = NUri +module H = U.UriHash module M = Meta module A = Aut -type qid = M.id * M.id list (* qualified identifier: name, qualifiers *) +(* qualified identifier: uri, name, qualifiers *) +type qid = U.uri * M.id * M.id list -type environment = (qid, M.pars) H.t +type environment = M.pars H.t type context_node = qid option (* context node: None = root *) @@ -44,13 +45,15 @@ let initial_status size = { let id_of_name (id, _, _) = id -let uri_of_qid (id, path) = - let path = String.concat "/" path in - let str = Filename.concat path id in - U.uri_of_string ("ld:/" ^ str) +let mk_qid id path = + let str = String.concat "/" path in + let str = Filename.concat str id in + U.uri_of_string ("ld:/" ^ str), id, path + +let uri_of_qid (uri, _, _) = uri let complete_qid f st (id, is_local, qs) = - let f qs = f (id, qs) in + let f qs = f (mk_qid id qs) in let f path = Cps.list_rev_append f path ~tail:qs in let rec skip f = function | phd :: ptl, qshd :: _ when phd = qshd -> f ptl @@ -59,8 +62,8 @@ let complete_qid f st (id, is_local, qs) = in if is_local then f st.path else skip f (st.path, qs) -let relax_qid f (id, path) = - let f path = f (id, path) in +let relax_qid f (_, id, path) = + let f path = f (mk_qid id path) in let f = function | _ :: tl -> Cps.list_rev f tl | [] -> assert false @@ -87,7 +90,7 @@ let resolve_lref_strict f st l lenv id = resolve_lref f st l lenv id let resolve_gref f st qid = - try let args = H.find st.henv qid in f qid (Some args) + try let args = H.find st.henv (uri_of_qid qid) in f qid (Some args) with Not_found -> f qid None let resolve_gref_relaxed f st qid = @@ -99,8 +102,8 @@ let resolve_gref_relaxed f st qid = 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 + | Some qid as node -> + try let pars = H.find st.hcnt (uri_of_qid qid) in f pars None with Not_found -> f [] (Some node) let get_pars_relaxed f st = @@ -159,7 +162,7 @@ let xlate_item f st = function let f qid = let f pars = let f ww = - H.add st.hcnt qid ((name, ww) :: pars); + H.add st.hcnt (uri_of_qid qid) ((name, ww) :: pars); f {st with node = Some qid} None in xlate_term f st pars w @@ -172,7 +175,7 @@ let xlate_item f st = function let f qid = let f ww = let entry = (st.line, pars, uri_of_qid qid, ww, None) in - H.add st.henv qid pars; + H.add st.henv (uri_of_qid qid) pars; f {st with line = succ st.line} (Some entry) in xlate_term f st pars w @@ -185,7 +188,7 @@ let xlate_item f st = function let f qid = let f ww vv = let entry = (st.line, pars, uri_of_qid qid, ww, Some (trans, vv)) in - H.add st.henv qid pars; + H.add st.henv (uri_of_qid qid) pars; f {st with line = succ st.line} (Some entry) in let f ww = xlate_term (f ww) st pars v in