Commit 90054255 authored by Andrei Paskevich's avatar Andrei Paskevich

Util: provide [all] and [any] combinators, with variants

these generalize numerous type-specific X_all and X_any functions.
These are now defined as [Util.all X_fold] or [Util.any X_fold].
parent 72f7ddbc
......@@ -150,11 +150,8 @@ let pat_fold fn acc pat = match pat.pat_node with
| Pas (p, _) -> fn acc p
| Por (p, q) -> fn (fn acc p) q
let pat_all pr pat =
try pat_fold (Util.all_fn pr) true pat with Util.FoldSkip -> false
let pat_any pr pat =
try pat_fold (Util.any_fn pr) false pat with Util.FoldSkip -> true
let pat_all pr pat = Util.all pat_fold pr pat
let pat_any pr pat = Util.any pat_fold pr pat
(* smart constructors for patterns *)
......@@ -1052,13 +1049,8 @@ let rec t_gen_fold fnT fnL acc t =
let t_s_fold = t_gen_fold
let t_s_all prT prL t =
try t_s_fold (Util.all_fn prT) (Util.all_fn prL) true t
with Util.FoldSkip -> false
let t_s_any prT prL t =
try t_s_fold (Util.any_fn prT) (Util.any_fn prL) false t
with Util.FoldSkip -> true
let t_s_all prT prL t = Util.alld t_s_fold prT prL t
let t_s_any prT prL t = Util.anyd t_s_fold prT prL t
(* map/fold over types in terms and formulas *)
......@@ -1135,8 +1127,8 @@ let t_fold fn acc t = match t.t_node with
let _, tl, f1 = t_open_quant b in tr_fold fn (fn acc f1) tl
| _ -> t_fold_unsafe fn acc t
let t_all pr t = try t_fold (Util.all_fn pr) true t with Util.FoldSkip -> false
let t_any pr t = try t_fold (Util.any_fn pr) false t with Util.FoldSkip -> true
let t_all pr t = Util.all t_fold pr t
let t_any pr t = Util.any t_fold pr t
(* safe opening map_fold *)
......@@ -1274,13 +1266,10 @@ let rec t_v_fold fn acc t = match t.t_node with
| Tquant (_,(_,b,_,_)) -> bnd_v_fold fn acc b
| _ -> t_fold_unsafe (t_v_fold fn) acc t
let t_v_all pr t =
try t_v_fold (Util.all_fn pr) true t with Util.FoldSkip -> false
let t_v_any pr t =
try t_v_fold (Util.any_fn pr) false t with Util.FoldSkip -> true
let t_v_all pr t = Util.all t_v_fold pr t
let t_v_any pr t = Util.any t_v_fold pr t
let t_closed t = t_v_all (fun _ -> false) t
let t_closed t = t_v_all Util.ffalse t
let bnd_v_count fn acc b = Mvs.fold (fun v n acc -> fn acc v n) b.bv_vars acc
......
......@@ -126,11 +126,8 @@ let ty_fold fn acc ty = match ty.ty_node with
| Tyvar _ -> acc
| Tyapp (_, tl) -> List.fold_left fn acc tl
let ty_all pr ty =
try ty_fold (Util.all_fn pr) true ty with Util.FoldSkip -> false
let ty_any pr ty =
try ty_fold (Util.any_fn pr) false ty with Util.FoldSkip -> true
let ty_all pr ty = Util.all ty_fold pr ty
let ty_any pr ty = Util.any ty_fold pr ty
(* traversal functions on type variables *)
......@@ -142,11 +139,8 @@ let rec ty_v_fold fn acc ty = match ty.ty_node with
| Tyvar v -> fn acc v
| Tyapp (_, tl) -> List.fold_left (ty_v_fold fn) acc tl
let ty_v_all pr ty =
try ty_v_fold (Util.all_fn pr) true ty with Util.FoldSkip -> false
let ty_v_any pr ty =
try ty_v_fold (Util.any_fn pr) false ty with Util.FoldSkip -> true
let ty_v_all pr ty = Util.all ty_v_fold pr ty
let ty_v_any pr ty = Util.any ty_v_fold pr ty
let ty_full_inst m ty = ty_v_map (fun v -> Mtv.find v m) ty
let ty_freevars s ty = ty_v_fold (fun s v -> Stv.add v s) s ty
......@@ -185,11 +179,8 @@ let rec ty_s_fold fn acc ty = match ty.ty_node with
| Tyvar _ -> acc
| Tyapp (f, tl) -> List.fold_left (ty_s_fold fn) (fn acc f) tl
let ty_s_all pr ty =
try ty_s_fold (Util.all_fn pr) true ty with Util.FoldSkip -> false
let ty_s_any pr ty =
try ty_s_fold (Util.any_fn pr) false ty with Util.FoldSkip -> true
let ty_s_all pr ty = Util.all ty_s_fold pr ty
let ty_s_any pr ty = Util.any ty_s_fold pr ty
(* type matching *)
......
......@@ -22,6 +22,7 @@ let flip f x y = f y x
(* useful iterator on int *)
let rec foldi f acc min max =
if min > max then acc else foldi f (f acc min) (succ min) max
let mapi f = foldi (fun acc i -> f i::acc) []
(* useful iterator on float *)
......@@ -33,8 +34,30 @@ let rec iterf f min max step =
exception FoldSkip
let all_fn pr _ t = pr t || raise FoldSkip
let any_fn pr _ t = pr t && raise FoldSkip
let all_fn pr = (fun _ x -> pr x || raise FoldSkip)
let any_fn pr = (fun _ x -> pr x && raise FoldSkip)
let all2_fn pr = (fun _ x y -> pr x y || raise FoldSkip)
let any2_fn pr = (fun _ x y -> pr x y && raise FoldSkip)
type ('z,'a,'c) fold = ('z -> 'a -> 'z) -> 'z -> 'c -> 'z
let all fold pr x = try fold (all_fn pr) true x with FoldSkip -> false
let any fold pr x = try fold (any_fn pr) false x with FoldSkip -> true
type ('z,'a,'b,'c,'d) fold2 = ('z -> 'a -> 'b -> 'z) -> 'z -> 'c -> 'd -> 'z
let all2 fold pr x y = try fold (all2_fn pr) true x y with FoldSkip -> false
let any2 fold pr x y = try fold (any2_fn pr) false x y with FoldSkip -> true
type ('z,'a,'b,'c) foldd =
('z -> 'a -> 'z) -> ('z -> 'b -> 'z) -> 'z -> 'c -> 'z
let alld fold pr1 pr2 x =
try fold (all_fn pr1) (all_fn pr2) true x with FoldSkip -> false
let anyd fold pr1 pr2 x =
try fold (any_fn pr1) (any_fn pr2) false x with FoldSkip -> true
(* constant boolean function *)
let ttrue _ = true
......
......@@ -26,15 +26,44 @@ val mapi : (int -> 'a) -> int -> int -> 'a list
val iterf : (float -> unit) -> float -> float -> float -> unit
(** [iterf f min max step] *)
(* boolean fold accumulators *)
(* Convert fold-like functions into [for_all] and [exists] functions.
Predicates passed to [all], [all2], and [alld] may raise FoldSkip to
signalize [false]. Predicates passed to [any], [any2], and [anyd] may
raise FoldSkip to signalize [true]. *)
exception FoldSkip
val all_fn : ('a -> bool) -> 'b -> 'a -> bool
(* [all_fn pr b a] return true if pr is true on a, otherwise raise FoldSkip *)
val any_fn : ('a -> bool) -> 'b -> 'a -> bool
(* [all_fn pr b a] return false if pr is false on a,
otherwise raise FoldSkip *)
val all_fn : ('a -> bool) -> 'z -> 'a -> bool
(* [all_fn pr z a] return true if [pr a] is true,
otherwise raises FoldSkip *)
val any_fn : ('a -> bool) -> 'z -> 'a -> bool
(* [all_fn pr z a] return false if [pr a] is false,
otherwise raises FoldSkip *)
val all2_fn : ('a -> 'b -> bool) -> 'z -> 'a -> 'b -> bool
(* [all_fn pr z a b] return true if [pr a b] is true,
otherwise raises FoldSkip *)
val any2_fn : ('a -> 'b -> bool) -> 'z -> 'a -> 'b -> bool
(* [all_fn pr z a b] return false if [pr a b] is false,
otherwise raises FoldSkip *)
type ('z,'a,'c) fold = ('z -> 'a -> 'z) -> 'z -> 'c -> 'z
val all : (bool,'a,'c) fold -> ('a -> bool) -> 'c -> bool
val any : (bool,'a,'c) fold -> ('a -> bool) -> 'c -> bool
type ('z,'a,'b,'c,'d) fold2 = ('z -> 'a -> 'b -> 'z) -> 'z -> 'c -> 'd -> 'z
val all2 : (bool,'a,'b,'c,'d) fold2 -> ('a -> 'b -> bool) -> 'c -> 'd -> bool
val any2 : (bool,'a,'b,'c,'d) fold2 -> ('a -> 'b -> bool) -> 'c -> 'd -> bool
type ('z,'a,'b,'c) foldd =
('z -> 'a -> 'z) -> ('z -> 'b -> 'z) -> 'z -> 'c -> 'z
val alld : (bool,'a,'b,'c) foldd -> ('a -> bool) -> ('b -> bool) -> 'c -> bool
val anyd : (bool,'a,'b,'c) foldd -> ('a -> bool) -> ('b -> bool) -> 'c -> bool
val ffalse : 'a -> bool
(** [ffalse] constant function [false] *)
......
......@@ -205,11 +205,8 @@ let ity_fold fn acc ity = match ity.ity_node with
| Itypur (_,tl)
| Ityapp (_,tl,_) -> List.fold_left fn acc tl
let ity_all pr ity =
try ity_fold (Util.all_fn pr) true ity with Util.FoldSkip -> false
let ity_any pr ity =
try ity_fold (Util.any_fn pr) false ity with Util.FoldSkip -> true
let ity_all pr ity = Util.all ity_fold pr ity
let ity_any pr ity = Util.any ity_fold pr ity
(* symbol-wise map/fold *)
......@@ -220,13 +217,8 @@ let rec ity_s_fold fn fts acc ity = match ity.ity_node with
let acc = List.fold_left (ity_s_fold fn fts) (fn acc f) tl in
List.fold_left (fun acc r -> ity_s_fold fn fts acc r.reg_ity) acc rl
let ity_s_all pr pts ity =
try ity_s_fold (Util.all_fn pr) (Util.all_fn pts) true ity
with Util.FoldSkip -> false
let ity_s_any pr pts ity =
try ity_s_fold (Util.any_fn pr) (Util.any_fn pts) false ity
with Util.FoldSkip -> true
let ity_s_all pr pts ity = Util.alld ity_s_fold pr pts ity
let ity_s_any pr pts ity = Util.anyd ity_s_fold pr pts ity
(* traversal functions on type variables and regions *)
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment