Commit f2569144 authored by François Bobot's avatar François Bobot

Term : fold on type and applications

parent dd7215a0
......@@ -1896,3 +1896,33 @@ 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)
(** Proposition of another fold *)
(* Type in terms and formulae *)
let rec t_fold_ty fty s t =
let s = t_fold_unsafe (t_fold_ty fty) (f_fold_ty fty) s t in
let s = fty s t.t_ty in
match t.t_node with
| Teps fb ->
let vs,_,_ = fb in
fty s vs.vs_ty
| _ -> s
and f_fold_ty fty s f =
let s = f_fold_unsafe (t_fold_ty fty) (f_fold_ty fty) s f in
match f.f_node with
| Fquant (_,fq) ->
let (vsl,_,_,_) = fq in
List.fold_left (fun s vs -> fty s vs.vs_ty) s vsl
| _ -> s
let rec t_fold_sig fty s t =
let s = t_fold_unsafe (t_fold_sig fty) (f_fold_sig fty) s t in
match t.t_node with
| Tapp (fs,tl) -> fty s fs (List.map (fun t -> t.t_ty) tl)
| _ -> s
and f_fold_sig fty s f =
let s = f_fold_unsafe (t_fold_sig fty) (f_fold_sig fty) s f in
match f.f_node with
| Fapp (fs,tl) -> fty s fs (List.map (fun t -> t.t_ty) tl)
| _ -> s
......@@ -506,3 +506,9 @@ exception NoMatch
val t_match : term Mvs.t -> term -> term -> term Mvs.t
val f_match : term Mvs.t -> fmla -> fmla -> term Mvs.t
(** Proposition of another fold *)
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
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