From: Ferruccio Guidi Date: Tue, 6 Oct 2009 18:20:27 +0000 (+0000) Subject: drgOutput: bug fix X-Git-Tag: make_still_working~3364 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=3d23faf2969e2591db93f8bacc61952f3b66e2ca;hp=3698de5ee6abc713534b0ee884e87e4046a087dd;p=helm.git drgOutput: bug fix we maked the non-tail recursive functions in: lib, common, automath, dual_rg --- diff --git a/helm/software/lambda-delta/automath/autOutput.ml b/helm/software/lambda-delta/automath/autOutput.ml index 5b415ff0b..668de7462 100644 --- a/helm/software/lambda-delta/automath/autOutput.ml +++ b/helm/software/lambda-delta/automath/autOutput.ml @@ -10,6 +10,7 @@ V_______________________________________________________________ *) module P = Printf +module C = Cps module L = Log module A = Aut module R = AutProcess @@ -40,7 +41,7 @@ let rec count_term f c = function let c = {c with grefs = succ c.grefs} in let c = {c with pars = c.pars + List.length ts} in let c = {c with xnodes = succ c.xnodes + List.length ts} in - Cps.list_fold_left f count_term c ts + C.list_fold_left f count_term c ts | A.Appl (v, t) -> let c = {c with appls = succ c.appls; xnodes = succ c.xnodes} in let f c = count_term f c t in diff --git a/helm/software/lambda-delta/dual_rg/drg.ml b/helm/software/lambda-delta/dual_rg/drg.ml index 4557aadb3..d44029615 100644 --- a/helm/software/lambda-delta/dual_rg/drg.ml +++ b/helm/software/lambda-delta/dual_rg/drg.ml @@ -43,6 +43,7 @@ let empty_lenv = ESort let push f lenv a b = f (EBind (lenv, a, b)) +(* this id not tail recursive *) let resolve_lref err f id lenv = let rec aux f i k = function | ESort -> err () diff --git a/helm/software/lambda-delta/dual_rg/drgAut.ml b/helm/software/lambda-delta/dual_rg/drgAut.ml index 3e1944408..aaf9d20c7 100644 --- a/helm/software/lambda-delta/dual_rg/drgAut.ml +++ b/helm/software/lambda-delta/dual_rg/drgAut.ml @@ -89,10 +89,11 @@ let relax_opt_qid f st = function let resolve_gref err f st qid = try let cnt = H.find st.henv (uri_of_qid qid) in f qid cnt - with Not_found -> err () + with Not_found -> err qid let resolve_gref_relaxed f st qid = - let rec err () = relax_qid (resolve_gref err f st) st qid in +(* this is not tail recursive *) + let rec err qid = relax_qid (resolve_gref err f st) st qid in resolve_gref err f st qid let get_cnt err f st = function @@ -102,9 +103,11 @@ let get_cnt err f st = function with Not_found -> err node let get_cnt_relaxed f st = +(* this is not tail recursive *) let rec err node = relax_opt_qid (get_cnt err f st) st node in get_cnt err f st st.node +(* this is not tail recursive in the GRef branch *) let rec xlate_term f st lenv = function | A.Sort s -> let f h = f (D.TSort ([], h)) in diff --git a/helm/software/lambda-delta/dual_rg/drgOutput.ml b/helm/software/lambda-delta/dual_rg/drgOutput.ml index c291cbf8a..2522b59f1 100644 --- a/helm/software/lambda-delta/dual_rg/drgOutput.ml +++ b/helm/software/lambda-delta/dual_rg/drgOutput.ml @@ -12,6 +12,7 @@ module X = Library module D = Drg +(* this is not tail recursive *) let rec list_iter map l f = match l with | [] -> f | hd :: tl -> map hd (list_iter map tl f) @@ -21,6 +22,7 @@ let rec lenv_iter map1 map2 l f = match l with | D.EBind (lenv, a, b) -> lenv_iter map1 map2 lenv (map1 a b f) | D.EProj (lenv, a, e) -> lenv_iter map1 map2 lenv (map2 a e f) +(* these are not tail recursive *) let rec exp_term t f = match t with | D.TSort (a, h) -> let attrs = [X.position h; X.name a] in diff --git a/helm/software/lambda-delta/lib/cps.ml b/helm/software/lambda-delta/lib/cps.ml index e42faba49..aa0dbc7c1 100644 --- a/helm/software/lambda-delta/lib/cps.ml +++ b/helm/software/lambda-delta/lib/cps.ml @@ -20,18 +20,21 @@ let rec list_sub_strict f l1 l2 = match l1, l2 with | _ :: tl1, _ :: tl2 -> list_sub_strict f tl1 tl2 | _ -> assert false +(* this is not tail recursive *) let rec list_fold_left f map a = function | [] -> f a | hd :: tl -> let f a = list_fold_left f map a tl in map f a hd +(* this is not tail recursive *) let rec list_rev_map_append f map ~tail = function | [] -> f tail | hd :: tl -> let f hd = list_rev_map_append f map ~tail:(hd :: tail) tl in map f hd +(* this is not tail recursive *) let rec list_forall2 f map l1 l2 = match l1, l2 with | [], [] -> f true | hd1 :: tl1, hd2 :: tl2 -> @@ -48,17 +51,11 @@ let list_rev_map = let list_rev = list_rev_append ~tail:[] -let list_fold_right f map l a = - let map f a m = map f m a in - list_rev (list_fold_left f map a) l - -let list_map f = - list_rev_map (list_rev f) - let list_iter f map l = let map f () x = map f x in list_fold_left f map () l +(* this is not tail recursive *) let rec list_fold_left2 f map a l1 l2 = match l1, l2 with | [], [] -> f a | hd1 :: tl1, hd2 :: tl2 -> @@ -70,6 +67,18 @@ let list_iter2 f map l1 l2 = let map f () x1 x2 = map f x1 x2 in list_fold_left2 f map () l1 l2 +let rec list_fold_right f map l a = match l with + | [] -> f a + | hd :: tl -> + let f a = map f hd a in + list_fold_right f map tl a + +let list_map f map l = + let map f hd a = + let f hd = f (hd :: a) in map f hd + in + list_fold_right f map l [] + let rec list_mem ?(eq=(=)) a = function | [] -> false | hd :: _ when eq a hd -> true diff --git a/helm/software/lambda-delta/lib/time.ml b/helm/software/lambda-delta/lib/time.ml index 2eec540c9..13a4c0aba 100644 --- a/helm/software/lambda-delta/lib/time.ml +++ b/helm/software/lambda-delta/lib/time.ml @@ -18,7 +18,7 @@ let utime_stamp = let times = Unix.times () in let stamp = times.Unix.tms_utime in let lap = stamp -. !old in - L.warn (P.sprintf "UTIME STAMP (%s): %f (%f)" msg stamp lap); + L.warn (P.sprintf "UTC STAMP (%s): %f (%f)" msg stamp lap); old := stamp let gmtime msg = @@ -30,5 +30,5 @@ let gmtime msg = let m = gmt.Unix.tm_min in let s = gmt.Unix.tm_sec in L.warn ( - P.sprintf "UTC TIME STAMP (%s): %u/%u/%u %u:%u:%u" msg yy mm dd h m s + P.sprintf "UTC STAMP (%s): %u/%u/%u %u:%u:%u" msg yy mm dd h m s ) diff --git a/helm/software/lambda-delta/toplevel/metaAut.ml b/helm/software/lambda-delta/toplevel/metaAut.ml index 75aaa71e6..d686c0f2c 100644 --- a/helm/software/lambda-delta/toplevel/metaAut.ml +++ b/helm/software/lambda-delta/toplevel/metaAut.ml @@ -19,14 +19,10 @@ module A = Aut (* qualified identifier: uri, name, qualifiers *) type qid = M.uri * M.id * M.id list -type environment = M.pars H.t - type context_node = qid option (* context node: None = root *) type status = { - henv: environment; (* optimized global environment *) path: M.id list; (* current section path *) - hcnt: environment; (* optimized context *) node: context_node; (* current context node *) nodes: context_node list; (* context node list *) line: int; (* line number *) @@ -38,11 +34,15 @@ type resolver = Local of int let henv_size, hcnt_size = 7000, 4300 (* hash tables initial sizes *) +let henv = H.create henv_size (* optimized global environment *) + +let hcnt = H.create hcnt_size (* optimized context *) + (* Internal functions *******************************************************) -let initial_status cover = { +let initial_status cover = + H.clear henv; H.clear hcnt; { path = []; node = None; nodes = []; line = 1; cover = cover; - henv = H.create henv_size; hcnt = H.create hcnt_size } let id_of_name (id, _, _) = id @@ -93,10 +93,11 @@ 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 (uri_of_qid qid) in f qid (Some args) + try let args = H.find henv (uri_of_qid qid) in f qid (Some args) with Not_found -> f qid None let resolve_gref_relaxed f st qid = +(* this is not tail recursive *) let rec g qid = function | None -> relax_qid (resolve_gref g st) st qid | Some args -> f qid args @@ -106,16 +107,18 @@ let resolve_gref_relaxed f st qid = let get_pars f st = function | None -> f [] None | Some qid as node -> - try let pars = H.find st.hcnt (uri_of_qid qid) in f pars None + try let pars = H.find hcnt (uri_of_qid qid) in f pars None with Not_found -> f [] (Some node) let get_pars_relaxed f st = +(* this is not tail recursive *) let rec g pars = function | None -> f pars | Some node -> relax_opt_qid (get_pars g st) st node in get_pars g st st.node +(* this is not tail recursive on the GRef branch *) let rec xlate_term f st lenv = function | A.Sort sort -> f (M.Sort sort) @@ -165,7 +168,7 @@ let xlate_entity err f st = function let f qid = let f pars = let f ww = - H.add st.hcnt (uri_of_qid qid) ((name, ww) :: pars); + H.add hcnt (uri_of_qid qid) ((name, ww) :: pars); err {st with node = Some qid} in xlate_term f st pars w @@ -177,7 +180,7 @@ let xlate_entity err f st = function let f pars = let f qid = let f ww = - H.add st.henv (uri_of_qid qid) pars; + H.add henv (uri_of_qid qid) pars; let a = [Y.Mark st.line] in let entry = pars, ww, None in let entity = a, uri_of_qid qid, Y.Abst entry in @@ -192,7 +195,7 @@ let xlate_entity err f st = function let f pars = let f qid = let f ww vv = - H.add st.henv (uri_of_qid qid) pars; + H.add henv (uri_of_qid qid) pars; let a = Y.Mark st.line :: if trans then [] else [Y.Priv] in let entry = pars, ww, Some vv in let entity = a, uri_of_qid qid, Y.Abbr entry in diff --git a/helm/software/lambda-delta/toplevel/top.ml b/helm/software/lambda-delta/toplevel/top.ml index 3556db37a..4c1ee1903 100644 --- a/helm/software/lambda-delta/toplevel/top.ml +++ b/helm/software/lambda-delta/toplevel/top.ml @@ -163,8 +163,8 @@ let process_0 f st entity = let rec process f book st = match book with | [] -> f st | entity :: tl -> - process f tl (process_0 C.start st entity) -(* process_0 (process f tl) st entity *) (* CPS variant of the above *) +(* we exploit tail recursion rather than CPS *) + process f tl (process_0 C.start st entity) (****************************************************************************)