Commit a481bbc5 authored by Andrei Paskevich's avatar Andrei Paskevich
Browse files

- use a correct type for triggers

- preserve labels on t_map/f_map/...
- comment out t_map_trans/f_map_trans
- rename X_forall/X_exists to X_all/X_any
- rename X_map_open/X_fold_open to X_map/X_fold
parent 2cc04ca9
This diff is collapsed.
......@@ -89,8 +89,8 @@ val pat_as : pattern -> vsymbol -> pattern
val pat_map : (pattern -> pattern) -> pattern -> pattern
val pat_fold : ('a -> pattern -> 'a) -> 'a -> pattern -> 'a
val pat_forall : (pattern -> bool) -> pattern -> bool
val pat_exists : (pattern -> bool) -> pattern -> bool
val pat_all : (pattern -> bool) -> pattern -> bool
val pat_any : (pattern -> bool) -> pattern -> bool
(* symbol-wise map/fold *)
......@@ -100,8 +100,8 @@ val pat_s_map : (tysymbol -> tysymbol) -> (vsymbol -> ty -> vsymbol)
val pat_s_fold :
('a -> tysymbol -> 'a) -> ('a -> fsymbol -> 'a) -> 'a -> pattern -> 'a
val pat_s_forall : (tysymbol -> bool) -> (fsymbol -> bool) -> pattern -> bool
val pat_s_exists : (tysymbol -> bool) -> (fsymbol -> bool) -> pattern -> bool
val pat_s_all : (tysymbol -> bool) -> (fsymbol -> bool) -> pattern -> bool
val pat_s_any : (tysymbol -> bool) -> (fsymbol -> bool) -> pattern -> bool
(* equality modulo alpha *)
......@@ -172,7 +172,11 @@ and term_branch
and fmla_branch
and trigger = term list
and trigger_elt =
| TrTerm of term
| TrFmla of fmla
and trigger = trigger_elt list
module Mterm : Map.S with type key = term
module Sterm : Set.S with type elt = term
......@@ -188,7 +192,7 @@ val t_let : vsymbol -> term -> term -> term
val t_case : term -> (pattern * term) list -> ty -> term
val t_eps : vsymbol -> fmla -> term
val t_label : label list -> term -> term
val t_label_set : label list -> term -> term
val t_label_add : label -> term -> term
(* smart constructors for fmla *)
......@@ -209,7 +213,7 @@ val f_if : fmla -> fmla -> fmla -> fmla
val f_let : vsymbol -> term -> fmla -> fmla
val f_case : term -> (pattern * fmla) list -> fmla
val f_label : label list -> fmla -> fmla
val f_label_set : label list -> fmla -> fmla
val f_label_add : label -> fmla -> fmla
(* bindings *)
......@@ -224,35 +228,19 @@ val f_open_quant : fmla_quant -> vsymbol list * trigger list * fmla
(* opening map/fold *)
val t_map_open : (term -> term) -> (fmla -> fmla) -> term -> term
val f_map_open : (term -> term) -> (fmla -> fmla) -> fmla -> fmla
val t_map : (term -> term) -> (fmla -> fmla) -> term -> term
val f_map : (term -> term) -> (fmla -> fmla) -> fmla -> fmla
val t_fold_open : ('a -> term -> 'a) -> ('a -> fmla -> 'a)
val t_fold : ('a -> term -> 'a) -> ('a -> fmla -> 'a)
-> 'a -> term -> 'a
val f_fold_open : ('a -> term -> 'a) -> ('a -> fmla -> 'a)
val f_fold : ('a -> term -> 'a) -> ('a -> fmla -> 'a)
-> 'a -> fmla -> 'a
val t_forall_open : (term -> bool) -> (fmla -> bool) -> term -> bool
val f_forall_open : (term -> bool) -> (fmla -> bool) -> fmla -> bool
val t_exists_open : (term -> bool) -> (fmla -> bool) -> term -> bool
val f_exists_open : (term -> bool) -> (fmla -> bool) -> fmla -> bool
(* transparent map/fold *)
val t_map_trans : (term -> term) -> (fmla -> fmla) -> term -> term
val f_map_trans : (term -> term) -> (fmla -> fmla) -> fmla -> fmla
val t_fold_trans : ('a -> term -> 'a) -> ('a -> fmla -> 'a)
-> 'a -> term -> 'a
val f_fold_trans : ('a -> term -> 'a) -> ('a -> fmla -> 'a)
-> 'a -> fmla -> 'a
val t_forall_trans : (term -> bool) -> (fmla -> bool) -> term -> bool
val f_forall_trans : (term -> bool) -> (fmla -> bool) -> fmla -> bool
val t_exists_trans : (term -> bool) -> (fmla -> bool) -> term -> bool
val f_exists_trans : (term -> bool) -> (fmla -> bool) -> fmla -> bool
val t_all : (term -> bool) -> (fmla -> bool) -> term -> bool
val f_all : (term -> bool) -> (fmla -> bool) -> fmla -> bool
val t_any : (term -> bool) -> (fmla -> bool) -> term -> bool
val f_any : (term -> bool) -> (fmla -> bool) -> fmla -> bool
(* symbol-wise map/fold *)
......@@ -268,16 +256,16 @@ val t_s_fold : ('a -> tysymbol -> 'a) -> ('a -> fsymbol -> 'a)
val f_s_fold : ('a -> tysymbol -> 'a) -> ('a -> fsymbol -> 'a)
-> ('a -> psymbol -> 'a) -> 'a -> fmla -> 'a
val t_s_forall : (tysymbol -> bool) -> (fsymbol -> bool)
val t_s_all : (tysymbol -> bool) -> (fsymbol -> bool)
-> (psymbol -> bool) -> term -> bool
val f_s_forall : (tysymbol -> bool) -> (fsymbol -> bool)
val f_s_all : (tysymbol -> bool) -> (fsymbol -> bool)
-> (psymbol -> bool) -> fmla -> bool
val t_s_exists : (tysymbol -> bool) -> (fsymbol -> bool)
val t_s_any : (tysymbol -> bool) -> (fsymbol -> bool)
-> (psymbol -> bool) -> term -> bool
val f_s_exists : (tysymbol -> bool) -> (fsymbol -> bool)
val f_s_any : (tysymbol -> bool) -> (fsymbol -> bool)
-> (psymbol -> bool) -> fmla -> bool
(* map/fold over free variables *)
......@@ -288,11 +276,11 @@ val f_v_map : (vsymbol -> term) -> fmla -> fmla
val t_v_fold : ('a -> vsymbol -> 'a) -> 'a -> term -> 'a
val f_v_fold : ('a -> vsymbol -> 'a) -> 'a -> fmla -> 'a
val t_v_forall : (vsymbol -> bool) -> term -> bool
val f_v_forall : (vsymbol -> bool) -> fmla -> bool
val t_v_all : (vsymbol -> bool) -> term -> bool
val f_v_all : (vsymbol -> bool) -> fmla -> bool
val t_v_exists : (vsymbol -> bool) -> term -> bool
val f_v_exists : (vsymbol -> bool) -> fmla -> bool
val t_v_any : (vsymbol -> bool) -> term -> bool
val f_v_any : (vsymbol -> bool) -> fmla -> bool
(* variable occurrence check *)
......
......@@ -95,11 +95,11 @@ let ty_fold fn acc ty = match ty.ty_node with
| Tyvar _ -> acc
| Tyapp (f, tl) -> List.fold_left fn acc tl
let ty_forall pr ty =
try ty_fold (forall_fn pr) true ty with FoldSkip -> false
let ty_all pr ty =
try ty_fold (all_fn pr) true ty with FoldSkip -> false
let ty_exists pr ty =
try ty_fold (exists_fn pr) false ty with FoldSkip -> true
let ty_any pr ty =
try ty_fold (any_fn pr) false ty with FoldSkip -> true
(* smart constructors *)
......@@ -108,7 +108,7 @@ exception UnboundTypeVariable
let rec tv_known vs ty = match ty.ty_node with
| Tyvar n -> Sid.mem n vs
| _ -> ty_forall (tv_known vs) ty
| _ -> ty_all (tv_known vs) ty
let create_tysymbol name args def =
let add s v =
......@@ -147,11 +147,11 @@ 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_forall pr ty =
try ty_s_fold (forall_fn pr) true ty with FoldSkip -> false
let ty_s_all pr ty =
try ty_s_fold (all_fn pr) true ty with FoldSkip -> false
let ty_s_exists pr ty =
try ty_s_fold (exists_fn pr) false ty with FoldSkip -> true
let ty_s_any pr ty =
try ty_s_fold (any_fn pr) false ty with FoldSkip -> true
(* type matching *)
......
......@@ -57,13 +57,13 @@ val ty_app : tysymbol -> ty list -> ty
val ty_map : (ty -> ty) -> ty -> ty
val ty_fold : ('a -> ty -> 'a) -> 'a -> ty -> 'a
val ty_forall : (ty -> bool) -> ty -> bool
val ty_exists : (ty -> bool) -> ty -> bool
val ty_all : (ty -> bool) -> ty -> bool
val ty_any : (ty -> bool) -> ty -> bool
val ty_s_map : (tysymbol -> tysymbol) -> ty -> ty
val ty_s_fold : ('a -> tysymbol -> 'a) -> 'a -> ty -> 'a
val ty_s_forall : (tysymbol -> bool) -> ty -> bool
val ty_s_exists : (tysymbol -> bool) -> ty -> bool
val ty_s_all : (tysymbol -> bool) -> ty -> bool
val ty_s_any : (tysymbol -> bool) -> ty -> bool
exception TypeMismatch
......
......@@ -65,9 +65,6 @@ let rec print_term fmt t = match t.t_node with
let print_vs fmt vs =
fprintf fmt "%a :@ %a" print_ident vs.vs_name print_ty vs.vs_ty
let print_tl fmt tl =
fprintf fmt "[%a]" (print_list alt (print_list comma print_term)) tl
let rec print_fmla fmt f = match f.f_node with
| Fapp (s,tl) ->
fprintf fmt "(%a(%a))"
......@@ -89,6 +86,13 @@ let rec print_fmla fmt f = match f.f_node with
| Fnot f -> fprintf fmt "(not@ %a)" print_fmla f
| _ -> assert false (*TODO*)
and print_tl fmt tl =
fprintf fmt "[%a]" (print_list alt (print_list comma print_tr)) tl
and print_tr fmt = function
| TrTerm t -> print_term fmt t
| TrFmla f -> print_fmla fmt f
let print_fsymbol fmt {fs_name = fs_name; fs_scheme = tyl,ty} =
fprintf fmt "%a%a :@ %a"
......
......@@ -15,15 +15,15 @@
(**************************************************************************)
let map_fold_left f acc l =
let acc, rev =
List.fold_left
(fun (acc, rev) e -> let acc, e = f acc e in acc, e :: rev)
(acc, []) l
let acc, rev =
List.fold_left
(fun (acc, rev) e -> let acc, e = f acc e in acc, e :: rev)
(acc, []) l
in
acc, List.rev rev
exception FoldSkip
let forall_fn pr _ t = pr t || raise FoldSkip
let exists_fn pr _ t = pr t && raise FoldSkip
let all_fn pr _ t = pr t || raise FoldSkip
let any_fn pr _ t = pr t && raise FoldSkip
......@@ -19,7 +19,7 @@ val map_fold_left :
exception FoldSkip
val forall_fn : ('a -> bool) -> 'b -> 'a -> bool
val exists_fn : ('a -> bool) -> 'b -> 'a -> bool
val all_fn : ('a -> bool) -> 'b -> 'a -> bool
val any_fn : ('a -> bool) -> 'b -> 'a -> bool
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