Commit c27ee110 authored by Andrei Paskevich's avatar Andrei Paskevich

minor

parent d6538090
...@@ -1896,33 +1896,32 @@ let f_map_simp fnT fnF f = f_label_copy f (match f.f_node with ...@@ -1896,33 +1896,32 @@ 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) let f_map_simp fnT = f_map_simp (protect fnT)
(** Proposition of another fold *) (* Fold over types in terms and formulas *)
(* Type in terms and formulae *)
let rec t_fold_ty fty s t = let rec t_fold_ty fty acc t =
let s = t_fold_unsafe (t_fold_ty fty) (f_fold_ty fty) s t in let acc = t_fold_unsafe (t_fold_ty fty) (f_fold_ty fty) acc t in
let s = fty s t.t_ty in let acc = fty acc t.t_ty in
match t.t_node with match t.t_node with
| Teps fb -> | Teps (vs,_,_) -> fty acc vs.vs_ty
let vs,_,_ = fb in | _ -> acc
fty s vs.vs_ty
| _ -> s
and f_fold_ty fty s f = and f_fold_ty fty acc f =
let s = f_fold_unsafe (t_fold_ty fty) (f_fold_ty fty) s f in let acc = f_fold_unsafe (t_fold_ty fty) (f_fold_ty fty) acc f in
match f.f_node with match f.f_node with
| Fquant (_,fq) -> | Fquant (_,(vsl,_,_,_)) ->
let (vsl,_,_,_) = fq in List.fold_left (fun acc vs -> fty acc vs.vs_ty) acc vsl
List.fold_left (fun s vs -> fty s vs.vs_ty) s vsl | _ -> acc
| _ -> s
(* Fold over EXACTLY WHAT? in terms and formulas *)
let rec t_fold_sig fty s t = let rec t_fold_sig fty acc t =
let s = t_fold_unsafe (t_fold_sig fty) (f_fold_sig fty) s t in let acc = t_fold_unsafe (t_fold_sig fty) (f_fold_sig fty) acc t in
match t.t_node with match t.t_node with
| Tapp (fs,tl) -> fty s fs (List.map (fun t -> t.t_ty) tl) | Tapp (fs,tl) -> fty acc fs (List.map (fun t -> t.t_ty) tl)
| _ -> s | _ -> acc
and f_fold_sig fty s f = and f_fold_sig fty acc f =
let s = f_fold_unsafe (t_fold_sig fty) (f_fold_sig fty) s f in let acc = f_fold_unsafe (t_fold_sig fty) (f_fold_sig fty) acc f in
match f.f_node with match f.f_node with
| Fapp (fs,tl) -> fty s fs (List.map (fun t -> t.t_ty) tl) | Fapp (fs,tl) -> fty acc fs (List.map (fun t -> t.t_ty) tl)
| _ -> s | _ -> acc
...@@ -424,6 +424,7 @@ val list_map_cont : (('a -> 'b) -> 'c -> 'b) -> ...@@ -424,6 +424,7 @@ val list_map_cont : (('a -> 'b) -> 'c -> 'b) ->
('a list -> 'b) -> 'c list -> 'b ('a list -> 'b) -> 'c list -> 'b
(** simplification map *) (** simplification map *)
val f_map_simp : (term -> term) -> (fmla -> fmla) -> fmla -> fmla val f_map_simp : (term -> term) -> (fmla -> fmla) -> fmla -> fmla
(** map/fold over free variables *) (** map/fold over free variables *)
...@@ -472,6 +473,7 @@ val f_ty_freevars : Stv.t -> fmla -> Stv.t ...@@ -472,6 +473,7 @@ val f_ty_freevars : Stv.t -> fmla -> Stv.t
val t_equal_alpha : term -> term -> bool val t_equal_alpha : term -> term -> bool
val f_equal_alpha : fmla -> fmla -> bool val f_equal_alpha : fmla -> fmla -> bool
module Hterm_alpha : Hashtbl.S with type key = term module Hterm_alpha : Hashtbl.S with type key = term
module Hfmla_alpha : Hashtbl.S with type key = fmla module Hfmla_alpha : Hashtbl.S with type key = fmla
...@@ -506,7 +508,8 @@ exception NoMatch ...@@ -506,7 +508,8 @@ exception NoMatch
val t_match : term Mvs.t -> term -> term -> term Mvs.t val t_match : term Mvs.t -> term -> term -> term Mvs.t
val f_match : term Mvs.t -> fmla -> fmla -> term Mvs.t val f_match : term Mvs.t -> fmla -> fmla -> term Mvs.t
(** Proposition of another fold *) (** fold over types in terms and formulas *)
val t_fold_ty : ('a -> ty -> 'a) -> 'a -> term -> 'a val t_fold_ty : ('a -> ty -> 'a) -> 'a -> term -> 'a
val f_fold_ty : ('a -> ty -> 'a) -> 'a -> fmla -> 'a val f_fold_ty : ('a -> ty -> 'a) -> 'a -> fmla -> 'a
......
...@@ -87,7 +87,7 @@ val ty_all : (ty -> bool) -> ty -> bool ...@@ -87,7 +87,7 @@ val ty_all : (ty -> bool) -> ty -> bool
val ty_any : (ty -> bool) -> ty -> bool val ty_any : (ty -> bool) -> ty -> bool
(** {3 symbol-wise map/fold} *) (** {3 symbol-wise map/fold} *)
(** visites every symbol of the type} *) (** visits every symbol of the type} *)
val ty_s_map : (tysymbol -> tysymbol) -> ty -> ty val ty_s_map : (tysymbol -> tysymbol) -> ty -> ty
val ty_s_fold : ('a -> tysymbol -> 'a) -> 'a -> ty -> 'a val ty_s_fold : ('a -> tysymbol -> 'a) -> 'a -> ty -> 'a
val ty_s_all : (tysymbol -> bool) -> ty -> bool val ty_s_all : (tysymbol -> bool) -> ty -> bool
......
...@@ -13,7 +13,6 @@ val load : ?dirs:string list -> plugin -> unit ...@@ -13,7 +13,6 @@ val load : ?dirs:string list -> plugin -> unit
plugin named [plugin]. It add the extension .cmo or .cmxs to the plugin named [plugin]. It add the extension .cmo or .cmxs to the
filename according to the compilation used for the main program *) filename according to the compilation used for the main program *)
type plu = type plu =
(* not a plugin extension *) (* not a plugin extension *)
| Plubad | Plubad
......
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