Commit cce88691 authored by Andrei Paskevich's avatar Andrei Paskevich

rename and generalise [tf]_fold_sig functions in Term

parent d696f495
......@@ -765,10 +765,6 @@ let bnd_find i m =
let bnd_inst m nv { bv_bound = d ; bv_open = b ; bv_defer = s } =
let s = Sint.fold (fun i -> Mint.add (i + d) (bnd_find i m)) b s in
(* assert (Mint.submap (const3 true) b m);
let m = Mint.inter (fun _ () x -> Some x) b m in
let m = Mint.translate ((+) d) m in
let s = Mint.union (fun _ _ _ -> assert false) m s in *)
{ bv_bound = d + nv ; bv_open = Sint.empty ; bv_defer = s }
let rec t_inst m nv t = t_label_copy t (match t.t_node with
......@@ -1193,6 +1189,34 @@ let t_s_any prT prL t =
let f_s_any prT prL f =
try f_s_fold (any_fn prT) (any_fn prL) false f with FoldSkip -> true
(* fold over types in terms and formulas *)
let rec t_ty_fold fn acc t =
let acc = t_fold_unsafe (t_ty_fold fn) (f_ty_fold fn) acc t in
fn acc t.t_ty
and f_ty_fold fn acc f =
let acc = f_fold_unsafe (t_ty_fold fn) (f_ty_fold fn) acc f in
match f.f_node with
| Fquant (_,(vsl,_,_,_)) ->
(* these variables (and their types) may never appear below *)
List.fold_left (fun acc vs -> fn acc vs.vs_ty) acc vsl
| _ -> acc
(* fold over applications in terms and formulas *)
let rec t_app_fold fn acc t =
let acc = t_fold_unsafe (t_app_fold fn) (f_app_fold fn) acc t in
match t.t_node with
| Tapp (ls,tl) -> fn acc ls (List.map (fun t -> t.t_ty) tl) (Some t.t_ty)
| _ -> acc
and f_app_fold fn acc f =
let acc = f_fold_unsafe (t_app_fold fn) (f_app_fold fn) acc f in
match f.f_node with
| Fapp (ls,tl) -> fn acc ls (List.map (fun t -> t.t_ty) tl) None
| _ -> acc
(* free type variables *)
let t_ty_freevars s t =
......@@ -1896,32 +1920,3 @@ let f_map_simp fnT fnF f = f_label_copy f (match f.f_node with
let f_map_simp fnT = f_map_simp (protect fnT)
(* Fold over types in terms and formulas *)
let rec t_fold_ty fty acc t =
let acc = t_fold_unsafe (t_fold_ty fty) (f_fold_ty fty) acc t in
let acc = fty acc t.t_ty in
match t.t_node with
| Teps (vs,_,_) -> fty acc vs.vs_ty
| _ -> acc
and f_fold_ty fty acc f =
let acc = f_fold_unsafe (t_fold_ty fty) (f_fold_ty fty) acc f in
match f.f_node with
| Fquant (_,(vsl,_,_,_)) ->
List.fold_left (fun acc vs -> fty acc vs.vs_ty) acc vsl
| _ -> acc
(* Fold over EXACTLY WHAT? in terms and formulas *)
let rec t_fold_sig fty acc t =
let acc = t_fold_unsafe (t_fold_sig fty) (f_fold_sig fty) acc t in
match t.t_node with
| Tapp (fs,tl) -> fty acc fs (List.map (fun t -> t.t_ty) tl)
| _ -> acc
and f_fold_sig fty acc f =
let acc = f_fold_unsafe (t_fold_sig fty) (f_fold_sig fty) acc f in
match f.f_node with
| Fapp (fs,tl) -> fty acc fs (List.map (fun t -> t.t_ty) tl)
| _ -> acc
......@@ -310,12 +310,10 @@ val f_quant_close_simp : quant -> vsymbol list -> trigger list -> fmla -> fmla
val f_forall_close_simp : vsymbol list -> trigger list -> fmla -> fmla
val f_exists_close_simp : vsymbol list -> trigger list -> fmla -> fmla
val f_forall_close_merge : vsymbol list -> fmla -> fmla
(** [forall_close_merge vs f] - put a universal quantifier on top of [f]; merge
variable lists if [f] is already a universally quantified formula; reuse
triggers of [f], if any, otherwise the quantifier has no triggers. *)
(** [forall_close_merge vs f] puts a universal quantifier over [f];
merges variable lists if [f] is already universally quantified;
reuses triggers of [f], if any, otherwise puts no triggers. *)
(** Expr and trigger traversal *)
......@@ -351,6 +349,19 @@ val f_s_all : (tysymbol -> bool) -> (lsymbol -> bool) -> fmla -> bool
val t_s_any : (tysymbol -> bool) -> (lsymbol -> bool) -> term -> bool
val f_s_any : (tysymbol -> bool) -> (lsymbol -> bool) -> fmla -> bool
(** fold over types in terms and formulas *)
val t_ty_fold : ('a -> ty -> 'a) -> 'a -> term -> 'a
val f_ty_fold : ('a -> ty -> 'a) -> 'a -> fmla -> 'a
(* fold over applications in terms and formulas *)
val t_app_fold :
('a -> lsymbol -> ty list -> ty option -> 'a) -> 'a -> term -> 'a
val f_app_fold :
('a -> lsymbol -> ty list -> ty option -> 'a) -> 'a -> fmla -> 'a
(** built-in symbols *)
(* equality predicate *)
......@@ -508,10 +519,3 @@ exception NoMatch
val t_match : term Mvs.t -> term -> term -> term Mvs.t
val f_match : term Mvs.t -> fmla -> fmla -> term Mvs.t
(** fold over types in terms and formulas *)
val t_fold_ty : ('a -> ty -> 'a) -> 'a -> term -> 'a
val f_fold_ty : ('a -> ty -> 'a) -> 'a -> fmla -> 'a
val t_fold_sig : ('a -> lsymbol -> ty list -> 'a) -> 'a -> term -> 'a
val f_fold_sig : ('a -> lsymbol -> ty list -> 'a) -> 'a -> fmla -> 'a
......@@ -227,7 +227,7 @@ let ty_quant env =
Mty.fold (fun uty _ s -> Ssubst.add (ty_match Mtv.empty ty uty) s)
env.keep s
| _ -> s in
f_fold_ty add_vs Ssubst.empty
f_ty_fold add_vs Ssubst.empty
(* The Core of the transformation *)
let fold_map task_hd ((env:env),task) =
......@@ -291,7 +291,7 @@ let ty_all_quant =
let rec add_vs s ty = match ty.ty_node with
| Tyvar vs -> Stv.add vs s
| _ -> ty_fold add_vs s ty in
f_fold_ty add_vs Stv.empty
f_ty_fold add_vs Stv.empty
let monomorphise_goal =
Trans.goal (fun pr f ->
......@@ -417,12 +417,12 @@ let is_ty_mono ~only_mono ty =
(* select the type array which appear as argument of set and get.
set and get must be in sls *)
let find_mono_array ~only_mono sls sty f =
let add sty ls tyl =
let add sty ls tyl _ =
match tyl with
| ty::_ when Sls.mem ls sls && is_ty_mono ~only_mono ty ->
Sty.add ty sty
| _ -> sty in
f_fold_sig add sty f
f_app_fold add sty f
let create_meta_ty ty =
let name = id_fresh "meta_ty" in
......
......@@ -356,7 +356,7 @@ let ty_quant =
let rec add_vs s ty = match ty.ty_node with
| Tyvar vs -> Stv.add vs s
| _ -> ty_fold add_vs s ty in
f_fold_ty add_vs Stv.empty
f_ty_fold add_vs Stv.empty
(* The Core of the transformation *)
let fold_map task_hd ((env:env),task) =
......@@ -506,7 +506,7 @@ let find_mono ~only_mono sty f =
let rec ty_add sty ty = ty_fold ty_add (Sty.add ty sty) ty in
let add sty ty = if is_ty_mono ~only_mono ty then
ty_add sty ty else sty in
f_fold_ty add sty f
f_ty_fold add sty f
let create_meta_ty ty =
let name = id_fresh "meta_ty" in
......@@ -561,12 +561,12 @@ let meta_kept_array = register_meta "encoding : kept_array" [MTtysymbol]
(* select the type array which appear as argument of set and get.
set and get must be in sls *)
let find_mono_array ~only_mono sls sty f =
let add sty ls tyl =
let add sty ls tyl _ =
match tyl with
| ty::_ when Sls.mem ls sls && is_ty_mono ~only_mono ty ->
Sty.add ty sty
| _ -> sty in
f_fold_sig add sty f
f_app_fold add sty f
let create_meta_ty ty =
let name = id_fresh "meta_ty" in
......
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