V_______________________________________________________________ *)
module P = Printf
+module C = Cps
module L = Log
module A = Aut
module R = AutProcess
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
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 ()
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
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
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)
| 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
| _ :: 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 ->
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 ->
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
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 =
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
)
(* 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 *)
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
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
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)
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
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
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
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)
(****************************************************************************)
projects / helm.git / commitdiff