Commit 1501f43a authored by Andrei Paskevich's avatar Andrei Paskevich

make term traversal functions take one fnT function

move old fnT+fnF versions of t_map, t_fold, etc. to a submodule
parent 903df0ef
......@@ -34,17 +34,17 @@ let fmla1 : Term.fmla = Term.f_or fmla_true fmla_false
(* printing it *)
open Format
let () = printf "@[formula 1 is:@ %a@]@." Pretty.print_fmla fmla1
let () = printf "@[formula 1 is:@ %a@]@." Pretty.print_term fmla1
(* a propositional goal: A and B implies A *)
let prop_var_A : Term.lsymbol = Term.create_psymbol (Ident.id_fresh "A") []
let prop_var_B : Term.lsymbol = Term.create_psymbol (Ident.id_fresh "B") []
let atom_A : Term.fmla = Term.f_app prop_var_A []
let atom_B : Term.fmla = Term.f_app prop_var_B []
let atom_A : Term.fmla = Term.ps_app prop_var_A []
let atom_B : Term.fmla = Term.ps_app prop_var_B []
let fmla2 : Term.fmla = Term.f_implies (Term.f_and atom_A atom_B) atom_A
let () = printf "@[formula 2 is:@ %a@]@." Pretty.print_fmla fmla2
let () = printf "@[formula 2 is:@ %a@]@." Pretty.print_term fmla2
(* building the task for formula 1 alone *)
......@@ -122,7 +122,7 @@ let int_theory : Theory.theory =
Env.find_theory env ["int"] "Int"
let plus_symbol : Term.lsymbol =
Theory.ns_find_ls int_theory.Theory.th_export ["infix +"]
let two_plus_two : Term.term = Term.t_app plus_symbol [two;two] Ty.ty_int
let two_plus_two : Term.term = Term.fs_app plus_symbol [two;two] Ty.ty_int
let two_plus_two : Term.term = Term.t_app_infer plus_symbol [two;two]
let fmla3 : Term.fmla = Term.f_equ two_plus_two four
......@@ -157,7 +157,7 @@ let x : Term.term = Term.t_var var_x
let x_times_x : Term.term =
Term.t_app_infer mult_symbol [x;x]
let fmla4_aux : Term.fmla =
Term.f_app ge_symbol [x_times_x;zero]
Term.ps_app ge_symbol [x_times_x;zero]
let fmla4_quant : Term.fmla_quant =
Term.f_close_quant [var_x] [] fmla4_aux
let fmla4 : Term.fmla =
......
......@@ -44,39 +44,26 @@ let check_fvs f =
Svs.iter (fun vs -> raise (UnboundVar vs)) fvs;
f
let check_ty = Ty.check_ty_equal
let check_vl ty v = ty_equal_check ty v.vs_ty
let check_tl ty t = ty_equal_check ty (t_type t)
let check_vl ty v = check_ty ty v.vs_ty
let check_tl ty t = check_ty ty (t_type t)
let make_fs_defn fs vl t =
let hd = e_app fs (List.map t_var vl) t.t_ty in
let fd = f_forall_close vl [] (f_equ hd t) in
check_t_ty fs.ls_value t;
List.iter2 check_vl fs.ls_args vl;
fs, Some (fs, check_fvs fd)
let make_ps_defn ps vl f =
let hd = f_app ps (List.map t_var vl) in
let pd = f_forall_close vl [] (f_iff hd f) in
List.iter2 check_vl ps.ls_args vl;
ps, Some (ps, check_fvs pd)
let make_ls_defn ls vl = e_map (make_fs_defn ls vl) (make_ps_defn ls vl)
let make_ls_defn ls vl t =
let hd = t_app ls (List.map t_var vl) t.t_ty in
let hd = e_fold f_equ f_iff hd t in
let fd = f_forall_close vl [] hd in
List.iter2 check_vl ls.ls_args vl;
t_ty_check t ls.ls_value;
ls, Some (ls, check_fvs fd)
let open_ls_defn (_,f) =
let vl, ef = f_open_forall f in
match ef.t_node with
| Tapp (_, [_; t2]) -> vl, t2
| Fbinop (_, _, f2) -> vl, f2
let vl,_,f = match f.t_node with
| Fquant (Fforall,b) -> f_open_quant b
| _ -> [],[],f in
match f.t_node with
| Tapp (_, [_; f])
| Fbinop (_, _, f) -> vl,f
| _ -> assert false
let open_fs_defn ld = let vl,e = open_ls_defn ld in
if e.t_ty = None then assert false else vl,e
let open_ps_defn ld = let vl,e = open_ls_defn ld in
if e.t_ty = None then vl,e else assert false
let ls_defn_axiom (_,f) = f
(** Termination checking for mutually recursive logic declarations *)
......@@ -128,7 +115,7 @@ let build_call_graph cgr syms ls =
in
let rec term vm () t = match t.t_node with
| Tapp (s,tl) when Mls.mem s syms ->
t_fold (term vm) (fmla vm) () t; call vm s tl
t_fold (term vm) () t; call vm s tl
| Tlet ({t_node = Tvar v}, b) when Mvs.mem v vm ->
let u,e = t_open_bound b in
term (Mvs.add u (Mvs.find v vm) vm) () e
......@@ -137,27 +124,15 @@ let build_call_graph cgr syms ls =
let p,t = t_open_branch b in
let vml = match_term vm e [vm] p in
List.iter (fun vm -> term vm () t) vml) bl
| _ -> t_fold (term vm) (fmla vm) () t
and fmla vm () f = match f.t_node with
| Tapp (s,tl) when Mls.mem s syms ->
t_fold (term vm) (fmla vm) () f; call vm s tl
| Tlet ({t_node = Tvar v}, b) when Mvs.mem v vm ->
let u,e = t_open_bound b in
fmla (Mvs.add u (Mvs.find v vm) vm) () e
| Tcase (e,bl) ->
term vm () e; List.iter (fun b ->
let p,f = t_open_branch b in
let vml = match_term vm e [vm] p in
List.iter (fun vm -> fmla vm () f) vml) bl
| Fquant (_,b) ->
let _,_,f = f_open_quant b in fmla vm () f
| _ -> t_fold (term vm) (fmla vm) () f
let _,_,f = f_open_quant b in term vm () f
| _ -> t_fold (term vm) () t
in
fun (vl,e) ->
let i = ref (-1) in
let add vm v = incr i; Mvs.add v (Equal !i) vm in
let vm = List.fold_left add Mvs.empty vl in
e_map (term vm ()) (fmla vm ()) e
term vm () e
let build_call_list cgr ls =
let htb = Hls.create 5 in
......@@ -389,15 +364,14 @@ let syms_ts s ts = Sid.add ts.ts_name s
let syms_ls s ls = Sid.add ls.ls_name s
let syms_ty s ty = ty_s_fold syms_ts s ty
let syms_term s t = t_s_fold syms_ts syms_ls s t
let syms_fmla s f = t_s_fold syms_ts syms_ls s f
let syms_term s t = t_s_fold syms_ty syms_ls s t
let create_ty_decl tdl =
if tdl = [] then raise EmptyDecl;
let add s (ts,_) = Sts.add ts s in
let tss = List.fold_left add Sts.empty tdl in
let check_constr tys ty (syms,news) fs =
check_ty ty (of_option fs.ls_value);
ty_equal_check ty (of_option fs.ls_value);
let add s ty = match ty.ty_node with
| Tyvar v -> Stv.add v s
| _ -> assert false
......@@ -437,7 +411,7 @@ let create_logic_decl ldl =
| Some (s,_) when not (ls_equal s ls) ->
raise (BadLogicDecl (ls, s))
| Some (_,f) ->
syms_fmla syms f, news_id news ls.ls_name
syms_term syms f, news_id news ls.ls_name
| None ->
let syms = option_apply syms (syms_ty syms) ls.ls_value in
let syms = List.fold_left syms_ty syms ls.ls_args in
......@@ -465,7 +439,7 @@ let rec f_pos_ps sps pol f = match f.t_node, pol with
f_pos_ps sps (option_map not pol) f
| Tif (f,g,h), _ ->
f_pos_ps sps None f && f_pos_ps sps pol g && f_pos_ps sps pol h
| _ -> t_all (t_pos_ps sps) (f_pos_ps sps pol) f
| _ -> TermTF.t_all (t_pos_ps sps) (f_pos_ps sps pol) f
let create_ind_decl idl =
if idl = [] then raise EmptyDecl;
......@@ -484,7 +458,7 @@ let create_ind_decl idl =
List.iter2 check_tl ps.ls_args tl;
(try ignore (List.for_all (f_pos_ps sps (Some true)) cls)
with Found ls -> raise (NonPositiveIndDecl (ps, pr, ls)));
syms_fmla syms f, news_id news pr.pr_name
syms_term syms f, news_id news pr.pr_name
| _ -> raise (InvalidIndDecl (ps, pr))
in
let check_decl (syms,news) (ps,al) =
......@@ -496,70 +470,72 @@ let create_ind_decl idl =
mk_decl (Dind idl) syms news
let create_prop_decl k p f =
let syms = syms_fmla Sid.empty f in
let syms = syms_term Sid.empty f in
let news = news_id Sid.empty p.pr_name in
mk_decl (Dprop (k,p,check_fvs f)) syms news
(** Utilities *)
let decl_map fnT fnF d = match d.d_node with
| Dtype _ ->
d
let decl_map fn d = match d.d_node with
| Dtype _ -> d
| Dlogic l ->
let fn = function
| ls, Some ld ->
let vl,e = open_ls_defn ld in
make_ls_defn ls vl (e_map fnT fnF e)
make_ls_defn ls vl (fn e)
| ld -> ld
in
create_logic_decl (List.map fn l)
| Dind l ->
let fn (pr,f) = pr, fnF f in
let fn (pr,f) = pr, fn f in
let fn (ps,l) = ps, List.map fn l in
create_ind_decl (List.map fn l)
| Dprop (k,pr,f) ->
create_prop_decl k pr (fnF f)
create_prop_decl k pr (fn f)
let decl_fold fnT fnF acc d = match d.d_node with
let decl_fold fn acc d = match d.d_node with
| Dtype _ -> acc
| Dlogic l ->
let fn acc = function
| _, Some ld ->
let _,e = open_ls_defn ld in
e_fold fnT fnF acc e
fn acc e
| _ -> acc
in
List.fold_left fn acc l
| Dind l ->
let fn acc (_,f) = fnF acc f in
let fn acc (_,f) = fn acc f in
let fn acc (_,l) = List.fold_left fn acc l in
List.fold_left fn acc l
| Dprop (_,_,f) ->
fnF acc f
fn acc f
let rpair_map_fold f acc (x1,x2) =
let acc, x2 = f acc x2 in
acc, (x1, x2)
let acc, x2 = f acc x2 in acc, (x1, x2)
let list_rpair_map_fold f =
Util.map_fold_left (rpair_map_fold f)
let list_rpair_map_fold f = Util.map_fold_left (rpair_map_fold f)
let decl_map_fold fnT fnF acc d =
match d.d_node with
let decl_map_fold fn acc d = match d.d_node with
| Dtype _ -> acc, d
| Dprop (k,pr,f) ->
let acc, f = t_map_fold fnT fnF acc f in
acc, create_prop_decl k pr f
| Dind l ->
let acc, l =
list_rpair_map_fold (list_rpair_map_fold (t_map_fold fnT fnF)) acc l in
acc, create_ind_decl l
| Dlogic l ->
let acc, l =
list_rpair_map_fold (option_map_fold
(rpair_map_fold (t_map_fold fnT fnF))) acc l in
list_rpair_map_fold (option_map_fold
(rpair_map_fold (t_map_fold fn))) acc l in
acc, create_logic_decl l
| Dind l ->
let acc, l =
list_rpair_map_fold (list_rpair_map_fold
(t_map_fold fn)) acc l in
acc, create_ind_decl l
| Dprop (k,pr,f) ->
let acc, f = t_map_fold fn acc f in
acc, create_prop_decl k pr f
module DeclTF = struct
let decl_map fnT fnF = decl_map (e_map fnT fnF)
let decl_fold fnT fnF = decl_fold (e_fold fnT fnF)
let decl_map_fold fnT fnF = decl_map_fold (e_fold fnT fnF)
end
(** Known identifiers *)
......@@ -630,25 +606,17 @@ let find_prop_decl kn pr =
| Dprop (k,_,f) -> k,f
| _ -> assert false
exception NonExhaustiveExpr of pattern list * expr
exception NonExhaustiveCase of pattern list * term
let rec check_matchT kn () t = match t.t_node with
| Tcase (t1,bl) ->
let bl = List.map (fun b -> let p,t = t_open_branch b in [p],t) bl in
ignore (try Pattern.CompileTerm.compile (find_constructors kn) [t1] bl
with Pattern.NonExhaustive p -> raise (NonExhaustiveExpr (p,t)));
t_fold (check_matchT kn) (check_matchF kn) () t
| _ -> t_fold (check_matchT kn) (check_matchF kn) () t
and check_matchF kn () f = match f.t_node with
| Tcase (t1,bl) ->
let bl = List.map (fun b -> let p,f = t_open_branch b in [p],f) bl in
ignore (try Pattern.CompileTerm.compile (find_constructors kn) [t1] bl
with Pattern.NonExhaustive p -> raise (NonExhaustiveExpr (p,f)));
t_fold (check_matchT kn) (check_matchF kn) () f
| _ -> t_fold (check_matchT kn) (check_matchF kn) () f
with Pattern.NonExhaustive p -> raise (NonExhaustiveCase (p,t)));
t_fold (check_matchT kn) () t
| _ -> t_fold (check_matchT kn) () t
let check_match kn d = decl_fold (check_matchT kn) (check_matchF kn) () d
let check_match kn d = decl_fold (check_matchT kn) () d
exception NonFoundedTypeDecl of tysymbol
......
......@@ -39,13 +39,9 @@ type ls_defn
type logic_decl = lsymbol * ls_defn option
val make_ls_defn : lsymbol -> vsymbol list -> expr -> logic_decl
val make_fs_defn : lsymbol -> vsymbol list -> term -> logic_decl
val make_ps_defn : lsymbol -> vsymbol list -> fmla -> logic_decl
val make_ls_defn : lsymbol -> vsymbol list -> term -> logic_decl
val open_ls_defn : ls_defn -> vsymbol list * expr
val open_fs_defn : ls_defn -> vsymbol list * term
val open_ps_defn : ls_defn -> vsymbol list * fmla
val open_ls_defn : ls_defn -> vsymbol list * term
val ls_defn_axiom : ls_defn -> fmla
......@@ -133,12 +129,21 @@ exception EmptyIndDecl of lsymbol
(** {2 Utilities} *)
val decl_map : (term -> term) -> decl -> decl
val decl_fold : ('a -> term -> 'a) -> 'a -> decl -> 'a
val decl_map_fold : ('a -> term -> 'a * term) -> 'a -> decl -> 'a * decl
module DeclTF : sig
val decl_map : (term -> term) -> (fmla -> fmla) -> decl -> decl
val decl_fold : ('a -> term -> 'a) -> ('a -> fmla -> 'a) -> 'a -> decl -> 'a
val decl_map_fold :
('a -> term -> 'a * term) -> ('a -> fmla -> 'a * fmla) ->
'a -> decl -> 'a * decl
val decl_map_fold : ('a -> term -> 'a * term) ->
('a -> fmla -> 'a * fmla) -> 'a -> decl -> 'a * decl
end
(** {2 Known identifiers} *)
......@@ -151,7 +156,7 @@ val merge_known : known_map -> known_map -> known_map
exception KnownIdent of ident
exception UnknownIdent of ident
exception RedeclaredIdent of ident
exception NonExhaustiveExpr of pattern list * expr
exception NonExhaustiveCase of pattern list * term
exception NonFoundedTypeDecl of tysymbol
val find_constructors : known_map -> tysymbol -> lsymbol list
......
......@@ -136,7 +136,7 @@ let unambig_fs fs =
| Tyvar u when not (lookup u) -> false
| _ -> ty_all inspect ty
in
inspect (of_option fs.ls_value)
option_apply true inspect fs.ls_value
(** Patterns, terms, and formulas *)
......@@ -190,7 +190,6 @@ let print_ident_labels fmt id =
else ()
let rec print_term fmt t = print_lterm 0 fmt t
and print_fmla fmt f = print_lfmla 0 fmt f
and print_lterm pri fmt t = match t.t_label with
| _ when Debug.nottest_flag debug_print_labels
......@@ -199,13 +198,6 @@ and print_lterm pri fmt t = match t.t_label with
| ll -> fprintf fmt (protect_on (pri > 0) "%a %a")
(print_list space print_label) ll (print_tnode 0) t
and print_lfmla pri fmt f = match f.t_label with
| _ when Debug.nottest_flag debug_print_labels
-> print_fnode pri fmt f
| [] -> print_fnode pri fmt f
| ll -> fprintf fmt (protect_on (pri > 0) "%a %a")
(print_list space print_label) ll (print_fnode 0) f
and print_app pri ls fmt tl = match extract_op ls, tl with
| _, [] ->
print_ls fmt ls
......@@ -236,7 +228,7 @@ and print_tnode pri fmt t = match t.t_node with
(print_app 5 fs) tl print_ty (t_type t)
| Tif (f,t1,t2) ->
fprintf fmt (protect_on (pri > 0) "if @[%a@] then %a@ else %a")
print_fmla f print_term t1 print_term t2
print_term f print_term t1 print_term t2
| Tlet (t1,tb) ->
let v,t2 = t_open_bound tb in
fprintf fmt (protect_on (pri > 0) "let %a = @[%a@] in@ %a")
......@@ -248,17 +240,12 @@ and print_tnode pri fmt t = match t.t_node with
| Teps fb ->
let v,f = t_open_bound fb in
fprintf fmt (protect_on (pri > 0) "epsilon %a.@ %a")
print_vsty v print_fmla f;
print_vsty v print_term f;
forget_var v
| Fquant _ | Fbinop _ | Fnot _ | Ftrue | Ffalse -> raise (TermExpected t)
and print_fnode pri fmt f = match f.t_node with
| Tapp (ps,tl) ->
print_app pri ps fmt tl
| Fquant (q,fq) ->
let vl,tl,f = f_open_quant fq in
fprintf fmt (protect_on (pri > 0) "%a %a%a.@ %a") print_quant q
(print_list comma print_vsty) vl print_tl tl print_fmla f;
(print_list comma print_vsty) vl print_tl tl print_term f;
List.iter forget_var vl
| Ftrue ->
fprintf fmt "true"
......@@ -267,37 +254,18 @@ and print_fnode pri fmt f = match f.t_node with
| Fbinop (b,f1,f2) ->
let p = prio_binop b in
fprintf fmt (protect_on (pri > p) "%a %a@ %a")
(print_lfmla (p + 1)) f1 print_binop b (print_lfmla p) f2
(print_lterm (p + 1)) f1 print_binop b (print_lterm p) f2
| Fnot f ->
fprintf fmt (protect_on (pri > 4) "not %a") (print_lfmla 4) f
| Tif (f1,f2,f3) ->
fprintf fmt (protect_on (pri > 0) "if @[%a@] then %a@ else %a")
print_fmla f1 print_fmla f2 print_fmla f3
| Tlet (t,f) ->
let v,f = t_open_bound f in
fprintf fmt (protect_on (pri > 0) "let %a = @[%a@] in@ %a")
print_vs v (print_lterm 4) t print_fmla f;
forget_var v
| Tcase (t,bl) ->
fprintf fmt "match @[%a@] with@\n@[<hov>%a@]@\nend"
print_term t (print_list newline print_fbranch) bl
| Tvar _ | Tconst _ | Teps _ -> raise (FmlaExpected f)
fprintf fmt (protect_on (pri > 4) "not %a") (print_lterm 4) f
and print_tbranch fmt br =
let p,t = t_open_branch br in
fprintf fmt "@[<hov 4>| %a ->@ %a@]" print_pat p print_term t;
Svs.iter forget_var p.pat_vars
and print_fbranch fmt br =
let p,f = t_open_branch br in
fprintf fmt "@[<hov 4>| %a ->@ %a@]" print_pat p print_fmla f;
Svs.iter forget_var p.pat_vars
and print_tl fmt tl =
if tl = [] then () else fprintf fmt "@ [%a]"
(print_list alt (print_list comma print_expr)) tl
and print_expr fmt = e_map (print_term fmt) (print_fmla fmt)
(print_list alt (print_list comma print_term)) tl
(** Declarations *)
......@@ -340,7 +308,7 @@ let print_logic_decl fst fmt (ls,ld) = match ld with
fprintf fmt "@[<hov 2>%s %a%a%a =@ %a@]"
(if fst then "logic" else "with") print_ls ls
(print_list nothing print_vs_arg) vl
(print_option print_ls_type) ls.ls_value print_expr e;
(print_option print_ls_type) ls.ls_value print_term e;
List.iter forget_var vl
| None ->
fprintf fmt "@[<hov 2>%s %a%a%a@]"
......@@ -352,7 +320,7 @@ let print_logic_decl fst fmt d = print_logic_decl fst fmt d; forget_tvs ()
let print_ind fmt (pr,f) =
fprintf fmt "@[<hov 4>| %a%a : %a@]"
print_pr pr print_ident_labels pr.pr_name print_fmla f
print_pr pr print_ident_labels pr.pr_name print_term f
let print_ind_decl fst fmt (ps,bl) =
fprintf fmt "@[<hov 2>%s %a%a =@ @[<hov>%a@]@]"
......@@ -371,7 +339,7 @@ let print_pkind fmt k = pp_print_string fmt (sprint_pkind k)
let print_prop_decl fmt (k,pr,f) =
fprintf fmt "@[<hov 2>%a %a%a : %a@]" print_pkind k
print_pr pr print_ident_labels pr.pr_name print_fmla f;
print_pr pr print_ident_labels pr.pr_name print_term f;
forget_tvs ()
let print_list_next sep print fmt = function
......@@ -513,7 +481,7 @@ let () = Exn_printer.register
| Term.PredicateSymbolExpected ls ->
fprintf fmt "Not a predicate symbol: %a" print_ls ls
| Term.TermExpected t ->
fprintf fmt "Not a term: %a" print_fmla t
fprintf fmt "Not a term: %a" print_term t
| Term.FmlaExpected t ->
fprintf fmt "Not a formula: %a" print_term t
| Term.NoMatch ->
......@@ -563,9 +531,9 @@ let () = Exn_printer.register
id.id_string
| Decl.NoTerminationProof ls ->
fprintf fmt "Cannot prove the termination of %a" print_ls ls
| Decl.NonExhaustiveExpr (pl, e) ->
| Decl.NonExhaustiveCase (pl, e) ->
fprintf fmt "Pattern @[%a@] is not covered in expression:@\n @[%a@]"
(print_list comma print_pat) pl print_expr e
(print_list comma print_pat) pl print_term e
| _ -> raise exn
end
......@@ -45,8 +45,6 @@ val print_binop : formatter -> binop -> unit (* binary operator *)
val print_const : formatter -> constant -> unit (* int/real constant *)
val print_pat : formatter -> pattern -> unit (* pattern *)
val print_term : formatter -> term -> unit (* term *)
val print_fmla : formatter -> fmla -> unit (* formula *)
val print_expr : formatter -> expr -> unit (* term or formula *)
val print_label : formatter -> label -> unit
val print_pkind : formatter -> prop_kind -> unit
......
......@@ -282,7 +282,7 @@ let () = Exn_printer.register (fun fmt exn -> match exn with
Pretty.print_ts e s
| UnsupportedTerm (e,s) ->
fprintf fmt "@[<hov 3> This expression isn't supported:@\n%a@\n%s@]"
Pretty.print_expr e s
Pretty.print_term e s
| UnsupportedDecl (d,s) ->
fprintf fmt "@[<hov 3> This declaration isn't supported:@\n%a@\n%s@]"
Pretty.print_decl d s
......
......@@ -51,7 +51,7 @@ let create_vsymbol name ty = {
type lsymbol = {
ls_name : ident;
ls_args : ty list;
ls_value : oty;
ls_value : ty option;
}
module Lsym = WeakStructMake (struct
......@@ -178,12 +178,8 @@ let pat_map fn pat = match pat.pat_node with
| Pas (p, v) -> pat_as (fn p) v
| Por (p, q) -> pat_or (fn p) (fn q)
let protect fn pat =
let res = fn pat in
check_ty_equal pat.pat_ty res.pat_ty;
res
let pat_map fn = pat_map (protect fn)
let pat_map fn = pat_map (fun p ->
let res = fn p in ty_equal_check p.pat_ty res.pat_ty; res)
let pat_fold fn acc pat = match pat.pat_node with
| Pwild | Pvar _ -> acc
......@@ -191,11 +187,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 (all_fn pr) true pat with FoldSkip -> false
let pat_any pr pat =
try pat_fold (any_fn pr) false pat with FoldSkip -> true
let pat_all pr pat = try pat_fold (all_fn pr) true pat with FoldSkip -> false
let pat_any pr pat = try pat_fold (any_fn pr) false pat with FoldSkip -> true
(* smart constructors for patterns *)
......@@ -215,11 +208,11 @@ let pat_app fs pl ty =
pat_app fs pl ty
let pat_as p v =
check_ty_equal p.pat_ty v.vs_ty;
ty_equal_check p.pat_ty v.vs_ty;
pat_as p v
let pat_or p q =
check_ty_equal p.pat_ty q.pat_ty;
ty_equal_check p.pat_ty q.pat_ty;
pat_or p q
(* symbol-wise map/fold *)
......@@ -265,10 +258,10 @@ type constant =
type term = {
t_node : term_node;
t_ty : ty option;
t_label : label list;
t_loc : Loc.position option;
t_vars : Svs.t;
t_ty : oty;
t_tag : int;
}
......@@ -286,31 +279,25 @@ and term_node =
| Ftrue
| Ffalse
and fmla = term
and expr = term
and fmla = term
and term_bound = vsymbol * bind_info * term
and fmla_bound = term_bound
and term_branch = pattern * bind_info * term
and fmla_branch = term_branch
and fmla_quant = vsymbol list * bind_info * trigger * term
and fmla_quant = vsymbol list * bind_info * trigger list * term
and trigger = term list list
and bind_info = {
bv_vars : Svs.t; (* free variables *)
bv_subst : term Mvs.t (* deferred substitution *)
}
and trigger = expr list
(* term equality *)
(* term equality and hash *)
let t_equal : term -> term -> bool = (==)
let t_hash t = t.t_tag
(* extract the type of a term *)
(* type checking *)
exception TermExpected of term
exception FmlaExpected of term
......@@ -322,29 +309,22 @@ let t_type t = match t.t_ty with
let t_prop f =
if f.t_ty = None then f else raise (FmlaExpected f)
let check_t_ty o t = match o, t.t_ty with
| Some l, Some r -> check_ty_equal l r
let t_ty_check t ty = match ty, t.t_ty with
| Some l, Some r -> ty_equal_check l r
| Some _, None -> raise (TermExpected t)
| None, Some _ -> raise (FmlaExpected t)
| None, None -> ()
(* expr and trigger equality *)
let tr_equal = list_all2 (list_all2 t_equal)
let e_map fnT fnF e = if e.t_ty = None then fnF e else fnT e
let e_fold fnT fnF acc e = if e.t_ty = None then fnF acc e else fnT acc e
(* expr and trigger traversal *)
(* trigger equality and traversal *)
let e_map fnT fnF e =
if e.t_ty = None then fnF e else fnT e
let e_fold fnT fnF acc e =
if e.t_ty = None then fnF acc e else fnT acc e
let tr_map fnT fnF = List.map (List.map (e_map fnT fnF))
let tr_fold fnT fnF = List.fold_left (List.fold_left (e_fold fnT fnF))
let tr_equal = list_all2 (list_all2 t_equal)
let tr_map_fold fnT fnF =
Util.map_fold_left (Util.map_fold_left (e_fold fnT fnF))
let tr_map fn = List.map (List.map fn)
let tr_fold fn = List.fold_left (List.fold_left fn)
let tr_map_fold fn = Util.map_fold_left (Util.map_fold_left fn)
(* bind_info equality, hash, and traversal *)
......@@ -355,6 +335,7 @@ let bnd_hash bv =
Mvs.fold comb bv.bv_subst
let bnd_map fn bv = { bv with bv_subst = Mvs.map fn bv.bv_subst }
let bnd_fold fn acc bv = Mvs.fold (fun _ t a -> fn a t) bv.bv_subst acc
let bnd_map_fold fn acc bv =
......@@ -496,85 +477,77 @@ let t_label_copy { t_label = l; t_loc = p } t =
(* unsafe map *)
let bound_map fnT fnE (u,b,e) = (u, bnd_map fnT b, fnE e)
let bound_map fn (u,b,e) = (u, bnd_map fn b, fn e)
let t_map_unsafe fnT fnF t = t_label_copy t (match t.t_node with
let t_map_unsafe fn t = t_label_copy t (match t.t_node with
| Tvar _ | Tconst _ -> t
| Tapp (f,tl) -> t_app f (List.map fnT tl) t.t_ty
| Tif (f,t1,t2) -> t_if (fnF f) (fnT t1) (fnT t2)