diff --git a/drivers/beagle.drv b/drivers/beagle.drv index 9c5dbe6c19141e9d4c8ad95bce92bca524c1cda3..707e0832185d0ee42e947b4710ca872ea3123478 100644 --- a/drivers/beagle.drv +++ b/drivers/beagle.drv @@ -1,7 +1,7 @@ (* Why3 driver for beagle see http://users.cecs.anu.edu.au/~baumgart/systems/beagle/ *) -printer "tptp-tff" +printer "tptp-tff0" filename "%f-%t-%g.p" valid "Proof found" @@ -34,8 +34,10 @@ transformation "eliminate_algebraic" transformation "eliminate_let" transformation "eliminate_if" +transformation "discriminate" transformation "encoding_smt" -transformation "encoding_sort" + +import "discrimination.gen" theory BuiltIn syntax predicate (=) "(%1 = %2)" @@ -45,11 +47,6 @@ theory BuiltIn meta "encoding : kept" type int meta "encoding : kept" type real meta "eliminate_algebraic" "no_index" - - meta "select_inst" "all" - meta "select_lskept" "all" - meta "select_lsinst" "all" - meta "select_kept" "all" end theory int.Int diff --git a/drivers/princess.drv b/drivers/princess.drv index 54ebd9e2a4b11b6a46ecc660cee5de82084d9d19..1827bfc25515d98de47faa1bee381b7a9a03f998 100644 --- a/drivers/princess.drv +++ b/drivers/princess.drv @@ -1,7 +1,7 @@ (* Why3 driver for princess see http://www.philipp.ruemmer.org/princess.shtml *) -printer "tptp-tff" +printer "tptp-tff0" filename "%f-%t-%g.p" valid "Proof found" @@ -36,7 +36,8 @@ transformation "eliminate_if" transformation "discriminate" transformation "encoding_smt" -transformation "encoding_sort" + +import "discrimination.gen" theory BuiltIn syntax predicate (=) "(%1 = %2)" @@ -46,11 +47,6 @@ theory BuiltIn meta "encoding : kept" type int meta "encoding : kept" type real meta "eliminate_algebraic" "no_index" - - meta "select_inst" "all" - meta "select_lskept" "all" - meta "select_lsinst" "all" - meta "select_kept" "all" end theory int.Int diff --git a/drivers/simplify.drv b/drivers/simplify.drv index b76b897a0b2e06232c89cba3abc8b0d0c4ae704c..b3c2dddbf903718f1e73e73c79e42091d0ec1ccd 100644 --- a/drivers/simplify.drv +++ b/drivers/simplify.drv @@ -28,18 +28,12 @@ trigger they can't appear since = can't appear *) (*transformation "filter_trigger_builtin"*) (* this is sound as long as int is the only kept type *) -transformation "encoding_smt" +transformation "encoding_tptp" theory BuiltIn syntax predicate (=) "(EQ %1 %2)" - meta "encoding : kept" type int - - (* no symbol discrimination, no kept types *) - meta "select_inst" "none" - meta "select_lskept" "none" - meta "select_lsinst" "none" - meta "select_kept" "none" + meta "encoding : base" type int end theory int.Int diff --git a/drivers/tptp-tff.drv b/drivers/tptp-tff0.drv similarity index 97% rename from drivers/tptp-tff.drv rename to drivers/tptp-tff0.drv index 3e52c1f54a8fc384f45c17e9c3939aab63036364..224bc7d1723b83649dd4e5f7cb5bf84082b6fcf1 100644 --- a/drivers/tptp-tff.drv +++ b/drivers/tptp-tff0.drv @@ -1,6 +1,6 @@ (* Why driver for first-order tptp provers supporting TFF0 *) -printer "tptp-tff" +printer "tptp-tff0" filename "%f-%t-%g.p" valid "Proof found" @@ -29,8 +29,10 @@ transformation "eliminate_definition" transformation "eliminate_inductive" transformation "eliminate_algebraic" +transformation "discriminate" transformation "encoding_smt" -transformation "encoding_sort" + +import "discrimination.gen" theory BuiltIn syntax predicate (=) "(%1 = %2)" @@ -40,11 +42,6 @@ theory BuiltIn meta "encoding : kept" type int meta "encoding : kept" type real meta "eliminate_algebraic" "no_index" - - meta "select_inst" "all" - meta "select_lskept" "all" - meta "select_lsinst" "all" - meta "select_kept" "all" end theory int.Int diff --git a/drivers/tptp-tff1.drv b/drivers/tptp-tff1.drv new file mode 100644 index 0000000000000000000000000000000000000000..351e7aedf84427e199164a7ea4b1dc8b871d5d02 --- /dev/null +++ b/drivers/tptp-tff1.drv @@ -0,0 +1,279 @@ +(* Why driver for first-order tptp provers supporting TFF1 *) + +printer "tptp-tff1" +filename "%f-%t-%g.p" + +valid "Proof found" +invalid "Completion found" +valid "^% SZS status Theorem" +valid "^% SZS status Unsatisfiable" +unknown "^% SZS status CounterSatisfiable" "" +unknown "^% SZS status Satisfiable" "" +timeout "^% SZS status Timeout" +unknown "^% SZS status GaveUp" "" +fail "^% SZS status Error" "" +timeout "Ran out of time" +timeout "CPU time limit exceeded" +outofmemory "Out of Memory" +unknown "No Proof Found" "" +fail "Failure.*" "\"\\0\"" +time "why3cpulimit time : %s s" + + +(* to be improved *) + +transformation "inline_trivial" + +transformation "eliminate_builtin" +transformation "eliminate_definition" +transformation "eliminate_inductive" +transformation "eliminate_algebraic" + +theory BuiltIn + syntax predicate (=) "(%1 = %2)" + syntax type int "$int" + syntax type real "$real" + + meta "eliminate_algebraic" "no_index" +end + +theory int.Int + syntax function zero "0" + syntax function one "1" + + syntax function (+) "$sum(%1,%2)" + syntax function (-) "$difference(%1,%2)" + syntax function (*) "$product(%1,%2)" + syntax function (-_) "$uminus(%1)" + + syntax predicate (<=) "$lesseq(%1,%2)" + syntax predicate (<) "$less(%1,%2)" + syntax predicate (>=) "$greatereq(%1,%2)" + syntax predicate (>) "$greater(%1,%2)" + + remove prop CommutativeGroup.Comm.Comm + remove prop CommutativeGroup.Assoc + remove prop CommutativeGroup.Unit_def_l + remove prop CommutativeGroup.Unit_def_r + remove prop CommutativeGroup.Inv_def_l + remove prop CommutativeGroup.Inv_def_r + remove prop Assoc.Assoc + remove prop Mul_distr_l + remove prop Mul_distr_r + remove prop Comm.Comm + remove prop Unitary + remove prop Refl + remove prop Trans + remove prop Antisymm + remove prop Total + remove prop NonTrivialRing + remove prop CompatOrderAdd + remove prop ZeroLessOne +end + +theory real.Real + syntax function zero "0.0" + syntax function one "1.0" + + syntax function (+) "$sum(%1,%2)" + syntax function (-) "$difference(%1,%2)" + syntax function (*) "$product(%1,%2)" + syntax function (-_) "$uminus(%1)" + + syntax function (/) "$quotient(%1,%2)" + syntax function inv "$quotient(1.0,%1)" + + syntax predicate (<=) "$lesseq(%1,%2)" + syntax predicate (<) "$less(%1,%2)" + syntax predicate (>=) "$greatereq(%1,%2)" + syntax predicate (>) "$greater(%1,%2)" + + remove prop CommutativeGroup.Comm.Comm + remove prop CommutativeGroup.Assoc + remove prop CommutativeGroup.Unit_def_l + remove prop CommutativeGroup.Unit_def_r + remove prop CommutativeGroup.Inv_def_l + remove prop CommutativeGroup.Inv_def_r + remove prop Assoc.Assoc + remove prop Mul_distr_l + remove prop Mul_distr_r + remove prop Comm.Comm + remove prop Unitary + remove prop Inverse + remove prop Refl + remove prop Trans + remove prop Antisymm + remove prop Total + remove prop NonTrivialRing + remove prop CompatOrderAdd + remove prop ZeroLessOne +end + +theory int.EuclideanDivision + syntax function div "$quotient_e(%1,%2)" + syntax function mod "$remainder_e(%1,%2)" + + remove prop Div_mod + remove prop Div_bound + remove prop Mod_bound + remove prop Mod_1 + remove prop Div_1 + remove prop Div_inf + remove prop Div_inf_neg + remove prop Mod_0 + remove prop Div_1_left + remove prop Div_minus1_left + remove prop Mod_1_left + remove prop Mod_minus1_left +end + +theory tptp.Univ + syntax type iType "$i" +end + +theory tptp.IntTrunc + syntax function floor "$floor(%1)" + syntax function ceil "$ceil(%1)" + syntax function truncate "$truncate(%1)" + syntax function round "$round(%1)" + + syntax function to_int "$to_int(%1)" + + syntax predicate is_int "$is_int(%1)" + syntax predicate is_rat "$is_rat(%1)" +end + +theory tptp.IntDivT + syntax function div_t "$quotient_t(%1,%2)" + syntax function mod_t "$remainder_t(%1,%2)" +end + +theory tptp.IntDivF + syntax function div_f "$quotient_f(%1,%2)" + syntax function mod_f "$remainder_f(%1,%2)" +end + +theory tptp.Rat + syntax type rat "$rat" + + syntax function zero "0/1" + syntax function one "1/1" + + syntax function (+) "$sum(%1,%2)" + syntax function (-) "$difference(%1,%2)" + syntax function (*) "$product(%1,%2)" + syntax function (-_) "$uminus(%1)" + + syntax function (/) "$quotient(%1,%2)" + syntax function inv "$quotient(1.0,%1)" + + syntax predicate (<=) "$lesseq(%1,%2)" + syntax predicate (<) "$less(%1,%2)" + syntax predicate (>=) "$greatereq(%1,%2)" + syntax predicate (>) "$greater(%1,%2)" + + syntax function to_rat "$to_rat(%1)" + + syntax predicate is_int "$is_int(%1)" + syntax predicate is_rat "$is_rat(%1)" + + remove prop CommutativeGroup.Comm.Comm + remove prop CommutativeGroup.Assoc + remove prop CommutativeGroup.Unit_def_l + remove prop CommutativeGroup.Unit_def_r + remove prop CommutativeGroup.Inv_def_l + remove prop CommutativeGroup.Inv_def_r + remove prop Assoc.Assoc + remove prop Mul_distr_l + remove prop Mul_distr_r + remove prop Comm.Comm + remove prop Unitary + remove prop Refl + remove prop Trans + remove prop Antisymm + remove prop Total + remove prop NonTrivialRing + remove prop CompatOrderAdd + remove prop ZeroLessOne +end + +theory tptp.RatTrunc + syntax function floor "$floor(%1)" + syntax function ceil "$ceil(%1)" + syntax function truncate "$truncate(%1)" + syntax function round "$round(%1)" + + syntax function to_int "$to_int(%1)" +end + +theory tptp.RatDivE + syntax function div "$quotient_e(%1,%2)" + syntax function mod "$remainder_e(%1,%2)" +end + +theory tptp.RatDivT + syntax function div_t "$quotient_t(%1,%2)" + syntax function mod_t "$remainder_t(%1,%2)" +end + +theory tptp.RatDivF + syntax function div_f "$quotient_f(%1,%2)" + syntax function mod_f "$remainder_f(%1,%2)" +end + +theory tptp.Real + syntax function to_real "$to_real(%1)" +end + +theory real.Truncate + syntax function floor "$floor(%1)" + syntax function ceil "$ceil(%1)" + syntax function truncate "$truncate(%1)" +end + +theory tptp.RealTrunc + syntax function round "$round(%1)" + + syntax function to_int "$to_int(%1)" + + syntax predicate is_int "$is_int(%1)" + syntax predicate is_rat "$is_rat(%1)" +end + +theory tptp.RealDivE + syntax function div "$quotient_e(%1,%2)" + syntax function mod "$remainder_e(%1,%2)" +end + +theory tptp.RealDivT + syntax function div_t "$quotient_t(%1,%2)" + syntax function mod_t "$remainder_t(%1,%2)" +end + +theory tptp.RealDivF + syntax function div_f "$quotient_f(%1,%2)" + syntax function mod_f "$remainder_f(%1,%2)" +end + +theory tptp.IntToRat + syntax function to_rat "$to_rat(%1)" +end + +theory tptp.IntToReal + syntax function to_real "$to_real(%1)" +end + +theory tptp.RealToRat + syntax function to_rat "$to_rat(%1)" +end + +theory tptp.RatToReal + syntax function to_real "$to_real(%1)" +end + +(* +Local Variables: +mode: why +compile-command: "unset LANG; make -C .. bench" +End: +*) diff --git a/drivers/z3_smtv1.drv b/drivers/z3_smtv1.drv index f6d5fd31c23429daef9159e1f36a6f71c325dcf6..d2acd89c73fc07c1c839623b97fcffb601f2ddc8 100644 --- a/drivers/z3_smtv1.drv +++ b/drivers/z3_smtv1.drv @@ -22,7 +22,6 @@ transformation "simplify_formula" (*transformation "simplify_trivial_quantification"*) transformation "encoding_smt" -transformation "encoding_sort" theory BuiltIn syntax type int "Int" diff --git a/plugins/tptp/tptp_printer.ml b/plugins/tptp/tptp_printer.ml index 6937a21dea076dde37a82ecf3d3ae2498a77f9c4..e2f7718c11ceca17f5ed885182f1282093cd86a8 100644 --- a/plugins/tptp/tptp_printer.ml +++ b/plugins/tptp/tptp_printer.ml @@ -45,22 +45,46 @@ let print_pr fmt pr = let forget_var v = forget_id ident_printer v.vs_name let forget_tvar v = forget_id ident_printer v.tv_name +type tptp_format = FOF | TFF0 | TFF1 + type info = { info_syn : syntax_map; - info_fof : bool; + info_fmt : tptp_format; + info_srt : ty Mty.t ref; + info_urg : string list ref; } +let complex_type = Wty.memoize 3 (fun ty -> + let s = Pp.string_of_wnl Pretty.print_ty ty in + create_tysymbol (id_fresh s) [] None) + let rec print_type info fmt ty = match ty.ty_node with + | Tyvar _ when info.info_fmt = TFF0 -> + unsupported "TFF0 does not support polymorphic types" | Tyvar tv -> print_tvar fmt tv - | Tyapp (ts, tl) -> begin match query_syntax info.info_syn ts.ts_name with - | Some s -> syntax_arguments s (print_type info) fmt tl - | None -> begin match tl with - | [] -> print_symbol fmt ts.ts_name - | _ -> fprintf fmt "@[%a(%a)@]" print_symbol ts.ts_name - (print_list comma (print_type info)) tl + | Tyapp (ts, tl) -> + begin match query_syntax info.info_syn ts.ts_name, tl with + | Some s, _ -> syntax_arguments s (print_type info) fmt tl + | None, [] -> print_symbol fmt ts.ts_name + | None, _ when info.info_fmt = TFF0 -> + begin match Mty.find_opt ty !(info.info_srt) with + | Some ty -> print_type info fmt ty + | None -> + let ts = complex_type ty in let cty = ty_app ts [] in + let us = sprintf "@[tff(%s, type,@ %a:@ $tType).@]@\n@\n" + (id_unique pr_printer ts.ts_name) print_symbol ts.ts_name in + info.info_srt := Mty.add ty cty !(info.info_srt); + info.info_urg := us :: !(info.info_urg); + print_type info fmt cty end + | None, tl -> + fprintf fmt "@[%a(%a)@]" print_symbol ts.ts_name + (print_list comma (print_type info)) tl end +let print_type info fmt ty = try print_type info fmt ty + with Unsupported s -> raise (UnsupportedType (ty,s)) + let number_format = { Number.long_int_support = true; Number.extra_leading_zeros_support = false; @@ -73,8 +97,7 @@ let number_format = { Number.hex_real_support = Number.Number_unsupported; Number.frac_real_support = Number.Number_custom (Number.PrintFracReal ("%s", "(%s * %s)", "(%s / %s)")); - Number.def_real_support = Number.Number_unsupported - ; + Number.def_real_support = Number.Number_unsupported; } let rec print_app info fmt ls tl oty = @@ -131,7 +154,7 @@ and print_fmla info fmt f = match f.t_node with let q = match q with Tforall -> "!" | Texists -> "?" in let vl, _tl, f = t_open_quant fq in let print_vsty fmt vs = - if info.info_fof then fprintf fmt "%a" print_var vs + if info.info_fmt = FOF then fprintf fmt "%a" print_var vs else fprintf fmt "%a:@,%a" print_var vs (print_type info) vs.vs_ty in fprintf fmt "%s[%a]:@ %a" q (print_list comma print_vsty) vl (print_fmla info) f; @@ -160,8 +183,9 @@ let print_fmla info fmt f = Stv.iter forget_tvar tvs let print_decl info fmt d = match d.d_node with - | Dtype _ when info.info_fof -> () + | Dtype _ when info.info_fmt = FOF -> () | Dtype { ts_def = Some _ } -> () + | Dtype { ts_args = _::_ } when info.info_fmt = TFF0 -> () | Dtype ts when query_syntax info.info_syn ts.ts_name <> None -> () | Dtype ts -> let print_arg fmt _ = fprintf fmt "$tType" in @@ -173,7 +197,7 @@ let print_decl info fmt d = match d.d_node with fprintf fmt "@[tff(%s, type,@ %a:@ %a).@]@\n@\n" (id_unique pr_printer ts.ts_name) print_symbol ts.ts_name print_sig ts - | Dparam _ when info.info_fof -> () + | Dparam _ when info.info_fmt = FOF -> () | Dparam ls when query_syntax info.info_syn ls.ls_name <> None -> () | Dparam ls -> let print_type = print_type info in @@ -208,30 +232,43 @@ let print_decl info fmt d = match d.d_node with "TPTP does not support inductive predicates, use eliminate_inductive" | Dprop (Paxiom, pr, _) when Mid.mem pr.pr_name info.info_syn -> () | Dprop (Paxiom, pr, f) -> - let head = if info.info_fof then "fof" else "tff" in + let head = if info.info_fmt = FOF then "fof" else "tff" in fprintf fmt "@[%s(%a, axiom,@ %a).@]@\n@\n" head print_pr pr (print_fmla info) f | Dprop (Pgoal, pr, f) -> - let head = if info.info_fof then "fof" else "tff" in + let head = if info.info_fmt = FOF then "fof" else "tff" in fprintf fmt "@[%s(%a, conjecture,@ %a).@]@\n" head print_pr pr (print_fmla info) f | Dprop ((Plemma|Pskip), _, _) -> assert false -let print_decl info fmt = catch_unsupportedDecl (print_decl info fmt) - -let print_task fof _env pr thpr _blacklist ?old:_ fmt task = - forget_all ident_printer; - forget_all pr_printer; - print_prelude fmt pr; - print_th_prelude task fmt thpr; - let info = { info_syn = get_syntax_map task; info_fof = fof } in - fprintf fmt "@[%a@]@." - (print_list nothing (print_decl info)) (Task.task_decls task) - -let () = register_printer "tptp-tff" (print_task false) ~desc:"TPTP TFF format" -let () = register_printer "tptp-fof" (print_task true) ~desc:"TPTP FOF format" - - +let print_decls fm = + let print_decl (sm,fm,ct) fmt d = + let info = { info_syn = sm; info_fmt = fm; + info_srt = ref ct; info_urg = ref [] } in + try print_decl info fmt d; + (sm,fm,!(info.info_srt)), !(info.info_urg) + with Unsupported s -> raise (UnsupportedDecl (d,s)) in + let print_decl = Printer.sprint_decl print_decl in + let print_decl task acc = print_decl task.Task.task_decl acc in + Discriminate.on_syntax_map (fun sm -> + Trans.fold print_decl ((sm,fm,Mty.empty),[])) + +let print_task fm = + let print_decls = print_decls fm in + fun _env pr thpr _blacklist ?old:_ fmt task -> + (* In trans-based p-printing [forget_all] is a no-no *) + (* forget_all ident_printer; *) + print_prelude fmt pr; + print_th_prelude task fmt thpr; + let rec print = function + | x :: r -> print r; Pp.string fmt x + | [] -> () in + print (snd (Trans.apply print_decls task)); + pp_print_flush fmt () + +let () = register_printer "tptp-tff0" (print_task TFF0) ~desc:"TPTP TFF0 format" +let () = register_printer "tptp-tff1" (print_task TFF1) ~desc:"TPTP TFF1 format" +let () = register_printer "tptp-fof" (print_task FOF) ~desc:"TPTP FOF format" (** DFG input format for SPASS >= 3.8 (with the help of Daniel Wand) @@ -364,7 +401,11 @@ let print_dfg _env pr thpr _blacklist ?old:_ fmt task = fprintf fmt "name({**}). author({**}). status(unknown). description({**}).@\n"; fprintf fmt "end_of_list.@\n@\n"; - let info = { info_syn = get_syntax_map task; info_fof = true } in + let info = { + info_syn = get_syntax_map task; + info_fmt = FOF; + info_urg = ref []; + info_srt = ref Mty.empty } in let dl = Task.task_decls task in let tl = List.filter (is_type info) dl in let fl = List.filter (is_function info) dl in diff --git a/plugins/tptp/tptp_typing.ml b/plugins/tptp/tptp_typing.ml index 7f2cf25ed5e466605a25d95c5aaa2741be9ad6a8..96edbd20218bfaabf448662db342bf68e2a1fdd2 100644 --- a/plugins/tptp/tptp_typing.ml +++ b/plugins/tptp/tptp_typing.ml @@ -649,7 +649,7 @@ let typecheck lib path ast = let f,_ = fmla denv env impl (Some pol) [] e in let f = if strict then f else let q = if pol then Texists else Tforall in - let vl = Mvs.keys f.t_vars in + let vl = Mvs.keys (t_vars f) in t_quant_close q vl [] f in let env,uc = flush_impl ~strict env uc impl in diff --git a/src/core/decl.ml b/src/core/decl.ml index 04d0042e08f795060d369242acaade9525d9b735..927b4fbc49a2e757992785f2aa2bcd839a8671d1 100644 --- a/src/core/decl.ml +++ b/src/core/decl.ml @@ -30,7 +30,7 @@ type logic_decl = lsymbol * ls_defn exception UnboundVar of vsymbol let check_fvs f = - Mvs.iter (fun vs _ -> raise (UnboundVar vs)) f.t_vars; + t_v_fold (fun _ vs -> raise (UnboundVar vs)) () f; t_prop f let check_vl ty v = ty_equal_check ty v.vs_ty diff --git a/src/core/dterm.ml b/src/core/dterm.ml index e1c6570ccd2c4ac347ca91b27720267d605e408e..2647b958f00b1f0b1b8982001f85f7bd421aa968 100644 --- a/src/core/dterm.ml +++ b/src/core/dterm.ml @@ -356,8 +356,8 @@ let quant_vars ~strict env vl = let acc, vl = Lists.map_fold_left add Mstr.empty vl in Mstr.set_union acc env, vl -let check_used_var vars vs = - if not (Mvs.mem vs vars) then +let check_used_var t vs = + if t_v_occurs vs t = 0 then let s = vs.vs_name.id_string in if not (String.length s > 0 && s.[0] = '_') then Warning.emit ?loc:vs.vs_name.id_loc "unused variable %s" s @@ -389,26 +389,26 @@ let term ~strict ~keep_loc env dt = let v = create_vsymbol id (t_type t) in let env = Mstr.add (preid_name id) v env in let f = get uloc env df in - check_used_var f.t_vars v; + check_used_var f v; t_let_close v t f | DTcase (dt,bl) -> let branch (dp,df) = let env, p = pattern ~strict env dp in let f = get uloc env df in - Svs.iter (check_used_var f.t_vars) p.pat_vars; + Svs.iter (check_used_var f) p.pat_vars; t_close_branch p f in t_case (get uloc env dt) (List.map branch bl) | DTeps (id,dty,df) -> let v = create_vsymbol id (ty_of_dty ~strict dty) in let env = Mstr.add (preid_name id) v env in let f = get uloc env df in - check_used_var f.t_vars v; + check_used_var f v; t_eps_close v f | DTquant (q,vl,dll,df) -> let env, vl = quant_vars ~strict env vl in let trl = List.map (List.map (get uloc env)) dll in let f = get uloc env df in - List.iter (check_used_var f.t_vars) vl; + List.iter (check_used_var f) vl; check_exists_implies q f; t_quant_close q vl trl f | DTbinop (op,df1,df2) -> diff --git a/src/core/ident.ml b/src/core/ident.ml index 6dd2e8b09eeab408cd55f501da5ad10dc9a1f573..ab7c8d1e42d8ec578949e5cbd5e6854dd97f2611 100644 --- a/src/core/ident.ml +++ b/src/core/ident.ml @@ -39,8 +39,8 @@ let create_label s = Hslab.hashcons { } let lab_equal : label -> label -> bool = (==) - -let lab_hash (lab : label) = lab.lab_tag +let lab_hash lab = lab.lab_tag +let lab_compare l1 l2 = Pervasives.compare l1.lab_tag l2.lab_tag (** Identifiers *) @@ -64,8 +64,8 @@ module Wid = Id.W type preid = ident let id_equal : ident -> ident -> bool = (==) - let id_hash id = Weakhtbl.tag_hash id.id_tag +let id_compare id1 id2 = Pervasives.compare (id_hash id1) (id_hash id2) (* constructors *) diff --git a/src/core/ident.mli b/src/core/ident.mli index f989e5f68f11d40a37a20c537cea5733cd645e85..ac2716a4fc54ac6ec9b127ce18a26853e401efca 100644 --- a/src/core/ident.mli +++ b/src/core/ident.mli @@ -23,8 +23,9 @@ type label = private { module Mlab : Extmap.S with type key = label module Slab : Extset.S with module M = Mlab +val lab_compare : label -> label -> int val lab_equal : label -> label -> bool -val lab_hash : label -> int +val lab_hash : label -> int val create_label : string -> label @@ -42,8 +43,8 @@ module Sid : Extset.S with module M = Mid module Hid : Exthtbl.S with type key = ident module Wid : Weakhtbl.S with type key = ident +val id_compare : ident -> ident -> int val id_equal : ident -> ident -> bool - val id_hash : ident -> int (* a user-created type of unregistered identifiers *) diff --git a/src/core/printer.ml b/src/core/printer.ml index e2f1d36992d9161d267cf5c8acafe7a2e61e527c..64e4d0cf3b236bf9281c4a832f22c199ec3619a9 100644 --- a/src/core/printer.ml +++ b/src/core/printer.ml @@ -266,7 +266,7 @@ let add_syntax_map td sm = match td.td_node with let query_syntax sm id = Mid.find_opt id sm -let fold_tdecls fn acc = +let on_syntax_map fn = Trans.on_meta meta_syntax_type (fun sts -> Trans.on_meta meta_syntax_logic (fun sls -> Trans.on_meta meta_remove_prop (fun spr -> @@ -274,27 +274,27 @@ let fold_tdecls fn acc = let sm = List.fold_left sm_add_ts sm sts in let sm = List.fold_left sm_add_ls sm sls in let sm = List.fold_left sm_add_pr sm spr in - Trans.fold (fun t -> fn sm t.task_decl) acc))) + fn sm))) -let sprint_tdecls (fn : syntax_map -> tdecl pp) = - let buf = Buffer.create 512 in +let sprint_tdecl (fn : 'a -> Format.formatter -> tdecl -> 'a * string list) = + let buf = Buffer.create 2048 in let fmt = Format.formatter_of_buffer buf in - let print sm td acc = + fun td (acc,strl) -> Buffer.reset buf; - Format.fprintf fmt "%a@?" (fn sm) td; - Buffer.contents buf :: acc in - fold_tdecls print [] + let acc, urg = fn acc fmt td in + Format.pp_print_flush fmt (); + acc, Buffer.contents buf :: List.rev_append urg strl -let sprint_decls (fn : syntax_map -> decl pp) = - let buf = Buffer.create 512 in +let sprint_decl (fn : 'a -> Format.formatter -> decl -> 'a * string list) = + let buf = Buffer.create 2048 in let fmt = Format.formatter_of_buffer buf in - let print sm td acc = match td.td_node with + fun td (acc,strl) -> match td.td_node with | Decl d -> Buffer.reset buf; - Format.fprintf fmt "%a@?" (fn sm) d; - Buffer.contents buf :: acc - | _ -> acc in - fold_tdecls print [] + let acc, urg = fn acc fmt d in + Format.pp_print_flush fmt (); + acc, Buffer.contents buf :: List.rev_append urg strl + | _ -> acc, strl (** {2 exceptions to use in transformations and printers} *) diff --git a/src/core/printer.mli b/src/core/printer.mli index 8426dc46f5984bddb5943f6e6799a4efccac6d71..59df559bc5774ae32c9e52759de8732a5bfa95fc 100644 --- a/src/core/printer.mli +++ b/src/core/printer.mli @@ -72,10 +72,15 @@ val syntax_arguments_typed : (** {2 pretty-printing transformations (useful for caching)} *) -val fold_tdecls : (syntax_map -> tdecl -> 'a -> 'a) -> 'a -> 'a Trans.trans +val on_syntax_map : (syntax_map -> 'a Trans.trans) -> 'a Trans.trans -val sprint_tdecls : (syntax_map -> tdecl pp) -> string list Trans.trans -val sprint_decls : (syntax_map -> decl pp) -> string list Trans.trans +val sprint_tdecl : + ('a -> Format.formatter -> Theory.tdecl -> 'a * string list) -> + Theory.tdecl -> 'a * string list -> 'a * string list + +val sprint_decl : + ('a -> Format.formatter -> Decl.decl -> 'a * string list) -> + Theory.tdecl -> 'a * string list -> 'a * string list (** {2 exceptions to use in transformations and printers} *) diff --git a/src/core/term.ml b/src/core/term.ml index 8f93b7d6071b3264102c8d69b634060df871e8d8..8c3ba32f04eb56f8a5fc24c4dadbe06df9da2c7c 100644 --- a/src/core/term.ml +++ b/src/core/term.ml @@ -31,8 +31,8 @@ module Hvs = Vsym.H module Wvs = Vsym.W let vs_equal : vsymbol -> vsymbol -> bool = (==) - let vs_hash vs = id_hash vs.vs_name +let vs_compare vs1 vs2 = id_compare vs1.vs_name vs2.vs_name let create_vsymbol name ty = { vs_name = id_register name; @@ -60,8 +60,8 @@ module Hls = Lsym.H module Wls = Lsym.W let ls_equal : lsymbol -> lsymbol -> bool = (==) - let ls_hash ls = id_hash ls.ls_name +let ls_compare ls1 ls2 = id_compare ls1.ls_name ls2.ls_name let check_opaque opaque args value = if Stv.is_empty opaque then opaque else @@ -94,7 +94,6 @@ type pattern = { pat_node : pattern_node; pat_vars : Svs.t; pat_ty : ty; - pat_tag : int; } and pattern_node = @@ -104,55 +103,12 @@ and pattern_node = | Por of pattern * pattern | Pas of pattern * vsymbol -let pat_equal : pattern -> pattern -> bool = (==) - -let pat_hash p = p.pat_tag - -module Hspat = Hashcons.Make (struct - type t = pattern - - let equal_node p1 p2 = match p1, p2 with - | Pwild, Pwild -> true - | Pvar v1, Pvar v2 -> vs_equal v1 v2 - | Papp (s1, l1), Papp (s2, l2) -> - ls_equal s1 s2 && List.for_all2 pat_equal l1 l2 - | Por (p1, q1), Por (p2, q2) -> - pat_equal p1 p2 && pat_equal q1 q2 - | Pas (p1, n1), Pas (p2, n2) -> - pat_equal p1 p2 && vs_equal n1 n2 - | _ -> false - - let equal p1 p2 = - equal_node p1.pat_node p2.pat_node && ty_equal p1.pat_ty p2.pat_ty - - let hash_node = function - | Pwild -> 0 - | Pvar v -> vs_hash v - | Papp (s, pl) -> Hashcons.combine_list pat_hash (ls_hash s) pl - | Por (p, q) -> Hashcons.combine (pat_hash p) (pat_hash q) - | Pas (p, v) -> Hashcons.combine (pat_hash p) (vs_hash v) - - let hash p = Hashcons.combine (hash_node p.pat_node) (ty_hash p.pat_ty) - - let tag n p = { p with pat_tag = n } -end) - -module Pat = MakeMSH (struct - type t = pattern - let tag pat = pat.pat_tag -end) - -module Spat = Pat.S -module Mpat = Pat.M -module Hpat = Pat.H - (* h-consing constructors for patterns *) -let mk_pattern n vs ty = Hspat.hashcons { +let mk_pattern n vs ty = { pat_node = n; pat_vars = vs; pat_ty = ty; - pat_tag = -1 } exception UncoveredVar of vsymbol @@ -271,8 +227,6 @@ type term = { t_ty : ty option; t_label : Slab.t; t_loc : Loc.position option; - t_vars : int Mvs.t; - t_tag : int; } and term_node = @@ -300,10 +254,248 @@ and bind_info = { bv_subst : term Mvs.t (* deferred substitution *) } -(* term equality and hash *) - -let t_equal : term -> term -> bool = (==) -let t_hash t = t.t_tag +(* term equality modulo alpha-equivalence and location *) + +exception CompLT +exception CompGT + +type frame = int Mvs.t * term Mvs.t + +type term_or_bound = + | Trm of term * frame list + | Bnd of int + +let rec descend vml t = match t.t_node with + | Tvar vs -> + let rec find vs = function + | (bv,vm)::vml -> + begin match Mvs.find_opt vs bv with + | Some i -> Bnd i + | None -> + begin match Mvs.find_opt vs vm with + | Some t -> descend vml t + | None -> find vs vml + end + end + | [] -> Trm (t, []) + in + find vs vml + | _ -> Trm (t, vml) + +let t_compare t1 t2 = + let comp_raise c = + if c < 0 then raise CompLT else if c > 0 then raise CompGT in + let perv_compare h1 h2 = comp_raise (Pervasives.compare h1 h2) in + let rec pat_compare (bnd,bv1,bv2 as state) p1 p2 = + match p1.pat_node, p2.pat_node with + | Pwild, Pwild -> + bnd, bv1, bv2 + | Pvar v1, Pvar v2 -> + bnd + 1, Mvs.add v1 bnd bv1, Mvs.add v2 bnd bv2 + | Papp (s1, l1), Papp (s2, l2) -> + comp_raise (ls_compare s1 s2); + List.fold_left2 pat_compare state l1 l2 + | Por (p1, q1), Por (p2, q2) -> + let (_,bv1,bv2 as res) = pat_compare state p1 p2 in + let rec or_cmp q1 q2 = match q1.pat_node, q2.pat_node with + | Pwild, Pwild -> () + | Pvar v1, Pvar v2 -> + perv_compare (Mvs.find v1 bv1) (Mvs.find v2 bv2) + | Papp (s1, l1), Papp (s2, l2) -> + comp_raise (ls_compare s1 s2); + List.iter2 or_cmp l1 l2 + | Por (p1, q1), Por (p2, q2) -> + or_cmp p1 p2; or_cmp q1 q2 + | Pas (p1, v1), Pas (p2, v2) -> + or_cmp p1 p2; + perv_compare (Mvs.find v1 bv1) (Mvs.find v2 bv2) + | Pwild, _ -> raise CompLT | _, Pwild -> raise CompGT + | Pvar _, _ -> raise CompLT | _, Pvar _ -> raise CompGT + | Papp _, _ -> raise CompLT | _, Papp _ -> raise CompGT + | Por _, _ -> raise CompLT | _, Por _ -> raise CompGT + in + or_cmp q1 q2; + res + | Pas (p1, v1), Pas (p2, v2) -> + let bnd, bv1, bv2 = pat_compare state p1 p2 in + bnd + 1, Mvs.add v1 bnd bv1, Mvs.add v2 bnd bv2 + | Pwild, _ -> raise CompLT | _, Pwild -> raise CompGT + | Pvar _, _ -> raise CompLT | _, Pvar _ -> raise CompGT + | Papp _, _ -> raise CompLT | _, Papp _ -> raise CompGT + | Por _, _ -> raise CompLT | _, Por _ -> raise CompGT + in + let rec t_compare bnd vml1 vml2 t1 t2 = + if t1 != t2 || vml1 <> [] || vml2 <> [] then begin + comp_raise (oty_compare t1.t_ty t2.t_ty); + comp_raise (Slab.compare t1.t_label t2.t_label); + match descend vml1 t1, descend vml2 t2 with + | Bnd i1, Bnd i2 -> perv_compare i1 i2 + | Bnd _, Trm _ -> raise CompLT + | Trm _, Bnd _ -> raise CompGT + | Trm (t1,vml1), Trm (t2,vml2) -> + begin match t1.t_node, t2.t_node with + | Tvar v1, Tvar v2 -> + comp_raise (vs_compare v1 v2) + | Tconst c1, Tconst c2 -> + perv_compare c1 c2 + | Tapp (s1,l1), Tapp (s2,l2) -> + comp_raise (ls_compare s1 s2); + List.iter2 (t_compare bnd vml1 vml2) l1 l2 + | Tif (f1,t1,e1), Tif (f2,t2,e2) -> + t_compare bnd vml1 vml2 f1 f2; + t_compare bnd vml1 vml2 t1 t2; + t_compare bnd vml1 vml2 e1 e2 + | Tlet (t1,(v1,b1,e1)), Tlet (t2,(v2,b2,e2)) -> + t_compare bnd vml1 vml2 t1 t2; + let vml1 = (Mvs.singleton v1 bnd, b1.bv_subst) :: vml1 in + let vml2 = (Mvs.singleton v2 bnd, b2.bv_subst) :: vml2 in + t_compare (bnd + 1) vml1 vml2 e1 e2 + | Tcase (t1,bl1), Tcase (t2,bl2) -> + t_compare bnd vml1 vml2 t1 t2; + let b_compare (p1,b1,t1) (p2,b2,t2) = + let bnd,bv1,bv2 = pat_compare (bnd,Mvs.empty,Mvs.empty) p1 p2 in + let vml1 = (bv1, b1.bv_subst) :: vml1 in + let vml2 = (bv2, b2.bv_subst) :: vml2 in + t_compare bnd vml1 vml2 t1 t2; 0 in + comp_raise (Lists.compare b_compare bl1 bl2) + | Teps (v1,b1,e1), Teps (v2,b2,e2) -> + let vml1 = (Mvs.singleton v1 bnd, b1.bv_subst) :: vml1 in + let vml2 = (Mvs.singleton v2 bnd, b2.bv_subst) :: vml2 in + t_compare (bnd + 1) vml1 vml2 e1 e2 + | Tquant (q1,(vl1,b1,tr1,f1)), Tquant (q2,(vl2,b2,tr2,f2)) -> + perv_compare q1 q2; + let rec add bnd bv1 bv2 vl1 vl2 = match vl1, vl2 with + | (v1::vl1), (v2::vl2) -> + let bv1 = Mvs.add v1 bnd bv1 in + let bv2 = Mvs.add v2 bnd bv2 in + add (bnd + 1) bv1 bv2 vl1 vl2 + | [], (_::_) -> raise CompLT + | (_::_), [] -> raise CompGT + | [], [] -> bnd, bv1, bv2 in + let bnd, bv1, bv2 = add bnd Mvs.empty Mvs.empty vl1 vl2 in + let vml1 = (bv1, b1.bv_subst) :: vml1 in + let vml2 = (bv2, b2.bv_subst) :: vml2 in + let tr_cmp t1 t2 = t_compare bnd vml1 vml2 t1 t2; 0 in + comp_raise (Lists.compare (Lists.compare tr_cmp) tr1 tr2); + t_compare bnd vml1 vml2 f1 f2 + | Tbinop (op1,f1,g1), Tbinop (op2,f2,g2) -> + perv_compare op1 op2; + t_compare bnd vml1 vml2 f1 f2; + t_compare bnd vml1 vml2 g1 g2 + | Tnot f1, Tnot f2 -> + t_compare bnd vml1 vml2 f1 f2 + | Ttrue, Ttrue -> () + | Tfalse, Tfalse -> () + | Tvar _, _ -> raise CompLT | _, Tvar _ -> raise CompGT + | Tconst _, _ -> raise CompLT | _, Tconst _ -> raise CompGT + | Tapp _, _ -> raise CompLT | _, Tapp _ -> raise CompGT + | Tif _, _ -> raise CompLT | _, Tif _ -> raise CompGT + | Tlet _, _ -> raise CompLT | _, Tlet _ -> raise CompGT + | Tcase _, _ -> raise CompLT | _, Tcase _ -> raise CompGT + | Teps _, _ -> raise CompLT | _, Teps _ -> raise CompGT + | Tquant _, _ -> raise CompLT | _, Tquant _ -> raise CompGT + | Tbinop _, _ -> raise CompLT | _, Tbinop _ -> raise CompGT + | Tnot _, _ -> raise CompLT | _, Tnot _ -> raise CompGT + | Ttrue, _ -> raise CompLT | _, Ttrue -> raise CompGT + end + end in + try t_compare 0 [] [] t1 t2; 0 + with CompLT -> -1 | CompGT -> 1 + +let t_equal t1 t2 = (t_compare t1 t2 = 0) + +let t_similar t1 t2 = + oty_equal t1.t_ty t2.t_ty && + match t1.t_node, t2.t_node with + | Tvar v1, Tvar v2 -> vs_equal v1 v2 + | Tconst c1, Tconst c2 -> c1 = c2 + | Tapp (s1,l1), Tapp (s2,l2) -> ls_equal s1 s2 && Lists.equal (==) l1 l2 + | Tif (f1,t1,e1), Tif (f2,t2,e2) -> f1 == f2 && t1 == t2 && e1 == e2 + | Tlet (t1,bv1), Tlet (t2,bv2) -> t1 == t2 && bv1 == bv2 + | Tcase (t1,bl1), Tcase (t2,bl2) -> t1 == t2 && Lists.equal (==) bl1 bl2 + | Teps bv1, Teps bv2 -> bv1 == bv2 + | Tquant (q1,bv1), Tquant (q2,bv2) -> q1 = q2 && bv1 == bv2 + | Tbinop (o1,f1,g1), Tbinop (o2,f2,g2) -> o1 = o2 && f1 == f2 && g1 == g2 + | Tnot f1, Tnot f2 -> f1 == f2 + | Ttrue, Ttrue | Tfalse, Tfalse -> true + | _, _ -> false + +let t_hash t = + let rec pat_hash bnd bv p = match p.pat_node with + | Pwild -> bnd, bv, 0 + | Pvar v -> bnd + 1, Mvs.add v bnd bv, bnd + 1 + | Papp (s,l) -> + let hash (bnd,bv,h) p = + let bnd,bv,hp = pat_hash bnd bv p in + bnd, bv, Hashcons.combine h hp in + List.fold_left hash (bnd,bv,ls_hash s) l + | Por (p,q) -> + let bnd,bv,hp = pat_hash bnd bv p in + let rec or_hash q = match q.pat_node with + | Pwild -> 0 + | Pvar v -> Mvs.find v bv + 1 + | Papp (s,l) -> Hashcons.combine_list or_hash (ls_hash s) l + | Por (p,q) -> Hashcons.combine (or_hash p) (or_hash q) + | Pas (p,v) -> Hashcons.combine (or_hash p) (Mvs.find v bv + 1) + in + bnd, bv, Hashcons.combine hp (or_hash q) + | Pas (p,v) -> + let bnd,bv,hp = pat_hash bnd bv p in + bnd + 1, Mvs.add v bnd bv, Hashcons.combine hp (bnd + 1) + in + let rec t_hash bnd vml t = + let comb l h = Hashcons.combine (lab_hash l) h in + let h = Slab.fold comb t.t_label (oty_hash t.t_ty) in + Hashcons.combine h + begin match descend vml t with + | Bnd i -> i + 1 + | Trm (t,vml) -> + begin match t.t_node with + | Tvar v -> vs_hash v + | Tconst c -> Hashtbl.hash c + | Tapp (s,l) -> + Hashcons.combine_list (t_hash bnd vml) (ls_hash s) l + | Tif (f,t,e) -> + let hf = t_hash bnd vml f in + let ht = t_hash bnd vml t in + let he = t_hash bnd vml e in + Hashcons.combine2 hf ht he + | Tlet (t,(v,b,e)) -> + let h = t_hash bnd vml t in + let vml = (Mvs.singleton v bnd, b.bv_subst) :: vml in + Hashcons.combine h (t_hash (bnd + 1) vml e) + | Tcase (t,bl) -> + let h = t_hash bnd vml t in + let b_hash (p,b,t) = + let bnd,bv,hp = pat_hash bnd Mvs.empty p in + let vml = (bv, b.bv_subst) :: vml in + Hashcons.combine hp (t_hash bnd vml t) in + Hashcons.combine_list b_hash h bl + | Teps (v,b,e) -> + let vml = (Mvs.singleton v bnd, b.bv_subst) :: vml in + t_hash (bnd + 1) vml e + | Tquant (q,(vl,b,tr,f)) -> + let h = Hashtbl.hash q in + let rec add bnd bv vl = match vl with + | v::vl -> add (bnd + 1) (Mvs.add v bnd bv) vl + | [] -> bnd, bv in + let bnd, bv = add bnd Mvs.empty vl in + let vml = (bv, b.bv_subst) :: vml in + let h = List.fold_left + (Hashcons.combine_list (t_hash bnd vml)) h tr in + Hashcons.combine h (t_hash bnd vml f) + | Tbinop (op,f,g) -> + let ho = Hashtbl.hash op in + let hf = t_hash bnd vml f in + let hg = t_hash bnd vml g in + Hashcons.combine2 ho hf hg + | Tnot f -> + Hashcons.combine 1 (t_hash bnd vml f) + | Ttrue -> 2 + | Tfalse -> 3 + end + end in + t_hash 0 [] t (* type checking *) @@ -335,12 +527,6 @@ let tr_map_fold fn = Lists.map_fold_left (Lists.map_fold_left fn) (* bind_info equality, hash, and traversal *) -let bnd_equal b1 b2 = Mvs.equal t_equal b1.bv_subst b2.bv_subst - -let bnd_hash bv = - let comb v t acc = Hashcons.combine2 (vs_hash v) (t_hash t) acc in - 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 @@ -351,119 +537,46 @@ let bnd_map_fold fn acc bv = (* hash-consing for terms and formulas *) -let some_plus _ m n = Some (m + n) -let add_t_vars s t = Mvs.union some_plus s t.t_vars -let add_b_vars s (_,b,_) = Mvs.union some_plus s b.bv_vars -let add_nt_vars _ n t s = Mvs.union some_plus s - (if n = 1 then t.t_vars else Mvs.map (( * ) n) t.t_vars) - -module Hsterm = Hashcons.Make (struct +let vars_union s1 s2 = Mvs.union (fun _ m n -> Some (m + n)) s1 s2 - type t = term +let add_b_vars s (_,b,_) = vars_union s b.bv_vars - let t_eq_bound (v1,b1,t1) (v2,b2,t2) = - vs_equal v1 v2 && bnd_equal b1 b2 && t_equal t1 t2 +let rec t_vars t = match t.t_node with + | Tvar v -> Mvs.singleton v 1 + | Tconst _ -> Mvs.empty + | Tapp (_,tl) -> List.fold_left add_t_vars Mvs.empty tl + | Tif (f,t,e) -> add_t_vars (add_t_vars (t_vars f) t) e + | Tlet (t,bt) -> add_b_vars (t_vars t) bt + | Tcase (t,bl) -> List.fold_left add_b_vars (t_vars t) bl + | Teps (_,b,_) -> b.bv_vars + | Tquant (_,(_,b,_,_)) -> b.bv_vars + | Tbinop (_,f1,f2) -> add_t_vars (t_vars f1) f2 + | Tnot f -> t_vars f + | Ttrue | Tfalse -> Mvs.empty - let t_eq_branch (p1,b1,t1) (p2,b2,t2) = - pat_equal p1 p2 && bnd_equal b1 b2 && t_equal t1 t2 +and add_t_vars s t = vars_union s (t_vars t) - let t_eq_quant (vl1,b1,tl1,f1) (vl2,b2,tl2,f2) = - t_equal f1 f2 && Lists.equal vs_equal vl1 vl2 && - bnd_equal b1 b2 && tr_equal tl1 tl2 - - let t_equal_node t1 t2 = match t1,t2 with - | Tvar v1, Tvar v2 -> vs_equal v1 v2 - | Tconst c1, Tconst c2 -> c1 = c2 - | Tapp (s1,l1), Tapp (s2,l2) -> - ls_equal s1 s2 && List.for_all2 t_equal l1 l2 - | Tif (f1,t1,e1), Tif (f2,t2,e2) -> - t_equal f1 f2 && t_equal t1 t2 && t_equal e1 e2 - | Tlet (t1,b1), Tlet (t2,b2) -> - t_equal t1 t2 && t_eq_bound b1 b2 - | Tcase (t1,bl1), Tcase (t2,bl2) -> - t_equal t1 t2 && Lists.equal t_eq_branch bl1 bl2 - | Teps f1, Teps f2 -> t_eq_bound f1 f2 - | Tquant (q1,b1), Tquant (q2,b2) -> - q1 = q2 && t_eq_quant b1 b2 - | Tbinop (op1,f1,g1), Tbinop (op2,f2,g2) -> - op1 = op2 && t_equal f1 f2 && t_equal g1 g2 - | Tnot f1, Tnot f2 -> t_equal f1 f2 - | Ttrue, Ttrue | Tfalse, Tfalse -> true - | _ -> false - - let equal t1 t2 = - oty_equal t1.t_ty t2.t_ty && - t_equal_node t1.t_node t2.t_node && - Slab.equal t1.t_label t2.t_label && - Opt.equal Loc.equal t1.t_loc t2.t_loc - - let t_hash_bound (v,b,t) = - Hashcons.combine (vs_hash v) (bnd_hash b (t_hash t)) - - let t_hash_branch (p,b,t) = - Hashcons.combine (pat_hash p) (bnd_hash b (t_hash t)) - - let t_hash_quant (vl,b,tl,f) = - let h = bnd_hash b (t_hash f) in - let h = Hashcons.combine_list vs_hash h vl in - List.fold_left (fun acc t -> Hashcons.combine_list t_hash acc t) h tl - - let t_hash_node = function - | Tvar v -> vs_hash v - | Tconst c -> Hashtbl.hash c - | Tapp (f,tl) -> Hashcons.combine_list t_hash (ls_hash f) tl - | Tif (f,t,e) -> Hashcons.combine2 (t_hash f) (t_hash t) (t_hash e) - | Tlet (t,bt) -> Hashcons.combine (t_hash t) (t_hash_bound bt) - | Tcase (t,bl) -> Hashcons.combine_list t_hash_branch (t_hash t) bl - | Teps f -> t_hash_bound f - | Tquant (q,bf) -> Hashcons.combine (Hashtbl.hash q) (t_hash_quant bf) - | Tbinop (op,f1,f2) -> - Hashcons.combine2 (Hashtbl.hash op) (t_hash f1) (t_hash f2) - | Tnot f -> Hashcons.combine 1 (t_hash f) - | Ttrue -> 0 - | Tfalse -> 1 - - let hash t = - let comb l = Hashcons.combine (lab_hash l) in - Hashcons.combine2 (t_hash_node t.t_node) - (Hashcons.combine_option Loc.hash t.t_loc) - (Slab.fold comb t.t_label (oty_hash t.t_ty)) - - let t_vars_node = function - | Tvar v -> Mvs.singleton v 1 - | Tconst _ -> Mvs.empty - | Tapp (_,tl) -> List.fold_left add_t_vars Mvs.empty tl - | Tif (f,t,e) -> add_t_vars (add_t_vars f.t_vars t) e - | Tlet (t,bt) -> add_b_vars t.t_vars bt - | Tcase (t,bl) -> List.fold_left add_b_vars t.t_vars bl - | Teps (_,b,_) -> b.bv_vars - | Tquant (_,(_,b,_,_)) -> b.bv_vars - | Tbinop (_,f1,f2) -> add_t_vars f1.t_vars f2 - | Tnot f -> f.t_vars - | Ttrue | Tfalse -> Mvs.empty - - let tag n t = { t with t_tag = n ; t_vars = t_vars_node t.t_node } - -end) +let add_nt_vars _ n t s = vars_union s + (if n = 1 then t_vars t else Mvs.map (( * ) n) (t_vars t)) -module Term = MakeMSH (struct +module TermOHT = struct type t = term - let tag term = term.t_tag -end) + let hash = t_hash + let equal = t_equal + let compare = t_compare +end -module Sterm = Term.S -module Mterm = Term.M -module Hterm = Term.H +module Mterm = Extmap.Make(TermOHT) +module Sterm = Extset.MakeOfMap(Mterm) +module Hterm = Exthtbl.Make(TermOHT) (* hash-consing constructors for terms *) -let mk_term n ty = Hsterm.hashcons { +let mk_term n ty = { t_node = n; t_label = Slab.empty; t_loc = None; - t_vars = Mvs.empty; t_ty = ty; - t_tag = -1 } let t_var v = mk_term (Tvar v) (Some v.vs_ty) @@ -479,20 +592,18 @@ let t_not f = mk_term (Tnot f) None let t_true = mk_term (Ttrue) None let t_false = mk_term (Tfalse) None -let t_label ?loc l t = - Hsterm.hashcons { t with t_label = l; t_loc = loc } +let t_label ?loc l t = { t with t_label = l; t_loc = loc } -let t_label_add l t = - Hsterm.hashcons { t with t_label = Slab.add l t.t_label } +let t_label_add l t = { t with t_label = Slab.add l t.t_label } -let t_label_remove l t = - Hsterm.hashcons { t with t_label = Slab.remove l t.t_label } +let t_label_remove l t = { t with t_label = Slab.remove l t.t_label } let t_label_copy s t = - if t_equal s t then s else + if s == t then s else + if t_similar s t && Slab.is_empty t.t_label && t.t_loc = None then s else let lab = Slab.union s.t_label t.t_label in let loc = if t.t_loc = None then s.t_loc else t.t_loc in - Hsterm.hashcons { t with t_label = lab; t_loc = loc } + { t with t_label = lab; t_loc = loc } (* unsafe map *) @@ -500,30 +611,14 @@ let bound_map fn (u,b,e) = (u, bnd_map fn b, fn e) let t_map_unsafe fn t = t_label_copy t (match t.t_node with | Tvar _ | Tconst _ -> t - | Tapp (f,tl) -> - let sl = List.map fn tl in - if List.for_all2 t_equal sl tl then t else - t_app f sl t.t_ty - | Tif (f,t1,t2) -> - let g = fn f and s1 = fn t1 and s2 = fn t2 in - if t_equal g f && t_equal s1 t1 && t_equal s2 t2 then t else - t_if g s1 s2 - | Tlet (e,b) -> - t_let (fn e) (bound_map fn b) t.t_ty - | Tcase (e,bl) -> - t_case (fn e) (List.map (bound_map fn) bl) t.t_ty - | Teps b -> - t_eps (bound_map fn b) t.t_ty - | Tquant (q,(vl,b,tl,f1)) -> - t_quant q (vl, bnd_map fn b, tr_map fn tl, fn f1) - | Tbinop (op,f1,f2) -> - let g1 = fn f1 and g2 = fn f2 in - if t_equal g1 f1 && t_equal g2 f2 then t else - t_binary op g1 g2 - | Tnot f1 -> - let g1 = fn f1 in - if t_equal g1 f1 then t else - t_not g1 + | Tapp (f,tl) -> t_app f (List.map fn tl) t.t_ty + | Tif (f,t1,t2) -> t_if (fn f) (fn t1) (fn t2) + | Tlet (e,b) -> t_let (fn e) (bound_map fn b) t.t_ty + | Tcase (e,bl) -> t_case (fn e) (List.map (bound_map fn) bl) t.t_ty + | Teps b -> t_eps (bound_map fn b) t.t_ty + | Tquant (q,(vl,b,tl,f)) -> t_quant q (vl, bnd_map fn b, tr_map fn tl, fn f) + | Tbinop (op,f1,f2) -> t_binary op (fn f1) (fn f2) + | Tnot f1 -> t_not (fn f1) | Ttrue | Tfalse -> t) (* unsafe fold *) @@ -554,13 +649,11 @@ let t_map_fold_unsafe fn acc t = match t.t_node with acc, t | Tapp (f,tl) -> let acc,sl = Lists.map_fold_left fn acc tl in - if List.for_all2 t_equal sl tl then acc,t else acc, t_label_copy t (t_app f sl t.t_ty) | Tif (f,t1,t2) -> let acc, g = fn acc f in let acc, s1 = fn acc t1 in let acc, s2 = fn acc t2 in - if t_equal g f && t_equal s1 t1 && t_equal s2 t2 then acc,t else acc, t_label_copy t (t_if g s1 s2) | Tlet (e,b) -> let acc, e = fn acc e in @@ -581,11 +674,9 @@ let t_map_fold_unsafe fn acc t = match t.t_node with | Tbinop (op,f1,f2) -> let acc, g1 = fn acc f1 in let acc, g2 = fn acc f2 in - if t_equal g1 f1 && t_equal g2 f2 then acc,t else acc, t_label_copy t (t_binary op g1 g2) | Tnot f1 -> let acc, g1 = fn acc f1 in - if t_equal g1 f1 then acc,t else acc, t_label_copy t (t_not g1) | Ttrue | Tfalse -> acc, t @@ -594,27 +685,26 @@ let t_map_fold_unsafe fn acc t = match t.t_node with let rec t_subst_unsafe m t = let t_subst t = t_subst_unsafe m t in - let b_subst (u,b,e) = (u, bv_subst_unsafe m b, e) in - let nosubst (_,b,_) = Mvs.set_disjoint m b.bv_vars in + let b_subst (u,b,e as bv) = + if Mvs.set_disjoint m b.bv_vars then bv else + (u, bv_subst_unsafe m b, e) in match t.t_node with | Tvar u -> Mvs.find_def t u m | Tlet (e, bt) -> let d = t_subst e in - if t_equal d e && nosubst bt then t else t_label_copy t (t_let d (b_subst bt) t.t_ty) | Tcase (e, bl) -> let d = t_subst e in - if t_equal d e && List.for_all nosubst bl then t else let bl = List.map b_subst bl in t_label_copy t (t_case d bl t.t_ty) | Teps bf -> - if nosubst bf then t else t_label_copy t (t_eps (b_subst bf) t.t_ty) - | Tquant (q, (vl,b,tl,f1)) -> - if Mvs.set_disjoint m b.bv_vars then t else - let b = bv_subst_unsafe m b in - t_label_copy t (t_quant q (vl,b,tl,f1)) + | Tquant (q, (vl,b,tl,f1 as bq)) -> + let bq = + if Mvs.set_disjoint m b.bv_vars then bq else + (vl,bv_subst_unsafe m b,tl,f1) in + t_label_copy t (t_quant q bq) | _ -> t_map_unsafe t_subst t @@ -641,13 +731,13 @@ let t_subst_unsafe m t = let bnd_new s = { bv_vars = s ; bv_subst = Mvs.empty } -let t_close_bound v t = (v, bnd_new (Mvs.remove v t.t_vars), t) +let t_close_bound v t = (v, bnd_new (Mvs.remove v (t_vars t)), t) -let t_close_branch p t = (p, bnd_new (Mvs.set_diff t.t_vars p.pat_vars), t) +let t_close_branch p t = (p, bnd_new (Mvs.set_diff (t_vars t) p.pat_vars), t) let t_close_quant vl tl f = let del_v s v = Mvs.remove v s in - let s = tr_fold add_t_vars f.t_vars tl in + let s = tr_fold add_t_vars (t_vars f) tl in let s = List.fold_left del_v s vl in (vl, bnd_new s, tl, t_prop f) @@ -687,21 +777,23 @@ let t_open_quant (vl,b,tl,f) = let t_open_bound_cb tb = let v, t = t_open_bound tb in let close v' t' = - if t_equal t t' && vs_equal v v' then tb else t_close_bound v' t' + if t == t' && vs_equal v v' then tb else t_close_bound v' t' in v, t, close let t_open_branch_cb tbr = let p, t = t_open_branch tbr in let close p' t' = - if t_equal t t' && pat_equal p p' then tbr else t_close_branch p' t' + if t == t' && p == p' then tbr else t_close_branch p' t' in p, t, close let t_open_quant_cb fq = let vl, tl, f = t_open_quant fq in let close vl' tl' f' = - if t_equal f f' && tr_equal tl tl' && Lists.equal vs_equal vl vl' + if f == f' && + Lists.equal (Lists.equal ((==) : term -> term -> bool)) tl tl' && + Lists.equal vs_equal vl vl' then fq else t_close_quant vl' tl' f' in vl, tl, f, close @@ -926,13 +1018,13 @@ let t_gen_map fnT fnL mapV t = t_gen_map (Wty.memoize 17 fnT) fnL mapV t let gen_mapV fnT = Mvs.mapi (fun v _ -> gen_fresh_vsymbol fnT v) -let t_s_map fnT fnL t = t_gen_map fnT fnL (gen_mapV fnT t.t_vars) t +let t_s_map fnT fnL t = t_gen_map fnT fnL (gen_mapV fnT (t_vars t)) t (* simultaneous substitution into types and terms *) let t_ty_subst mapT mapV t = let fnT = ty_inst mapT in - let m = gen_mapV fnT t.t_vars in + let m = gen_mapV fnT (t_vars t) in let t = t_gen_map fnT (fun ls -> ls) m t in let add _ v t m = vs_check v t; Mvs.add v t m in let m = Mvs.fold2_inter add m mapV Mvs.empty in @@ -1001,8 +1093,8 @@ let t_map fn t = match t.t_node with | Tlet (t1, b) -> let u,t2 = t_open_bound b in let s1 = fn t1 and s2 = fn t2 in - if t_equal s2 t2 - then if t_equal s1 t1 then t + if s2 == t2 + then if s1 == t1 then t else t_label_copy t (t_let s1 b) else t_label_copy t (t_let_close u s1 s2) | Tcase (t1, bl) -> @@ -1010,21 +1102,21 @@ let t_map fn t = match t.t_node with let brn same b = let p,t = t_open_branch b in let s = fn t in - if t_equal s t then same, b + if s == t then same, b else false, t_close_branch p s in let same, bl = Lists.map_fold_left brn true bl in - if t_equal s1 t1 && same then t + if s1 == t1 && same then t else t_label_copy t (t_case s1 bl) | Teps b -> let u,t1 = t_open_bound b in let s1 = fn t1 in - if t_equal s1 t1 then t + if s1 == t1 then t else t_label_copy t (t_eps_close u s1) | Tquant (q, b) -> let vl,tl,f1 = t_open_quant b in let g1 = fn f1 and sl = tr_map fn tl in - if t_equal g1 f1 && List.for_all2 (List.for_all2 t_equal) sl tl then t + if g1 == f1 && List.for_all2 (List.for_all2 (==)) sl tl then t else t_label_copy t (t_quant_close q vl sl g1) | _ -> t_map_unsafe fn t @@ -1056,8 +1148,8 @@ let t_map_fold fn acc t = match t.t_node with let acc, s1 = fn acc t1 in let u,t2 = t_open_bound b in let acc, s2 = fn acc t2 in - acc, if t_equal s2 t2 - then if t_equal s1 t1 then t + acc, if s2 == t2 + then if s1 == t1 then t else t_label_copy t (t_let s1 b) else t_label_copy t (t_let_close u s1 s2) | Tcase (t1, bl) -> @@ -1065,22 +1157,22 @@ let t_map_fold fn acc t = match t.t_node with let brn (acc,same) b = let p,t = t_open_branch b in let acc, s = fn acc t in - if t_equal s t then (acc,same), b + if s == t then (acc,same), b else (acc,false), t_close_branch p s in let (acc,same), bl = Lists.map_fold_left brn (acc,true) bl in - acc, if t_equal s1 t1 && same then t + acc, if s1 == t1 && same then t else t_label_copy t (t_case s1 bl) | Teps b -> let u,t1 = t_open_bound b in let acc, s1 = fn acc t1 in - acc, if t_equal s1 t1 then t + acc, if s1 == t1 then t else t_label_copy t (t_eps_close u s1) | Tquant (q, b) -> let vl,tl,f1 = t_open_quant b in let acc, sl = tr_map_fold fn acc tl in let acc, g1 = fn acc f1 in - acc, if t_equal g1 f1 && List.for_all2 (List.for_all2 t_equal) sl tl + acc, if g1 == f1 && List.for_all2 (List.for_all2 (==)) sl tl then t else t_label_copy t (t_quant_close q vl sl g1) | _ -> t_map_fold_unsafe fn acc t @@ -1171,204 +1263,58 @@ let t_map_cont fn = t_map_cont (fun cont t -> let t_v_map fn t = let fn v _ = let res = fn v in vs_check v res; res in - t_subst_unsafe (Mvs.mapi fn t.t_vars) t + t_subst_unsafe (Mvs.mapi fn (t_vars t)) t -let t_v_fold fn acc t = Mvs.fold (fun v _ a -> fn a v) t.t_vars acc +let bnd_v_fold fn acc b = Mvs.fold (fun v _ acc -> fn acc v) b.bv_vars acc -let t_v_all pr t = Mvs.for_all (fun v _ -> pr v) t.t_vars -let t_v_any pr t = Mvs.exists (fun v _ -> pr v) t.t_vars +let bound_v_fold fn acc (_,b,_) = bnd_v_fold fn acc b -(* replaces variables with terms in term [t] using map [m] *) +let rec t_v_fold fn acc t = match t.t_node with + | Tvar v -> fn acc v + | Tlet (e,b) -> bound_v_fold fn (t_v_fold fn acc e) b + | Tcase (e,bl) -> List.fold_left (bound_v_fold fn) (t_v_fold fn acc e) bl + | Teps b -> bound_v_fold fn acc b + | Tquant (_,(_,b,_,_)) -> bnd_v_fold fn acc b + | _ -> t_fold_unsafe (t_v_fold fn) acc t -let t_subst m t = Mvs.iter vs_check m; t_subst_unsafe m t +let t_v_all pr t = + try t_v_fold (Util.all_fn pr) true t with Util.FoldSkip -> false -let t_subst_single v t1 t = t_subst (Mvs.singleton v t1) t +let t_v_any pr t = + try t_v_fold (Util.any_fn pr) false t with Util.FoldSkip -> true -(* set of free variables *) +let t_closed t = t_v_all (fun _ -> false) t -let t_freevars = add_t_vars +let bnd_v_count fn acc b = Mvs.fold (fun v n acc -> fn acc v n) b.bv_vars acc -(* alpha-equality *) +let bound_v_count fn acc (_,b,_) = bnd_v_count fn acc b -let vs_rename_alpha c h vs = incr c; Mvs.add vs !c h +let rec t_v_count fn acc t = match t.t_node with + | Tvar v -> fn acc v 1 + | Tlet (e,b) -> bound_v_count fn (t_v_count fn acc e) b + | Tcase (e,bl) -> List.fold_left (bound_v_count fn) (t_v_count fn acc e) bl + | Teps b -> bound_v_count fn acc b + | Tquant (_,(_,b,_,_)) -> bnd_v_count fn acc b + | _ -> t_fold_unsafe (t_v_count fn) acc t -let vl_rename_alpha c h vl = List.fold_left (vs_rename_alpha c) h vl +let t_v_occurs v t = + t_v_count (fun c u n -> if vs_equal u v then c + n else c) 0 t -let rec pat_rename_alpha c h p = match p.pat_node with - | Pvar v -> vs_rename_alpha c h v - | Pas (p, v) -> pat_rename_alpha c (vs_rename_alpha c h v) p - | Por (p, _) -> pat_rename_alpha c h p - | _ -> pat_fold (pat_rename_alpha c) h p - -let rec pat_equal_alpha p1 p2 = - pat_equal p1 p2 || - ty_equal p1.pat_ty p2.pat_ty && - match p1.pat_node, p2.pat_node with - | Pwild, Pwild | Pvar _, Pvar _ -> true - | Papp (f1, l1), Papp (f2, l2) -> - ls_equal f1 f2 && List.for_all2 pat_equal_alpha l1 l2 - | Pas (p1, _), Pas (p2, _) -> pat_equal_alpha p1 p2 - | Por (p1, q1), Por (p2, q2) -> - pat_equal_alpha p1 p2 && pat_equal_alpha q1 q2 - | _ -> false +(* replaces variables with terms in term [t] using map [m] *) -let rec t_equal_alpha c1 c2 m1 m2 t1 t2 = - t_equal t1 t2 || oty_equal t1.t_ty t2.t_ty && - let t_eq = t_equal_alpha c1 c2 m1 m2 in - match t1.t_node, t2.t_node with - | Tvar v1, Tvar v2 when Mvs.mem v1 m1 -> - Mvs.mem v2 m2 && Mvs.find v1 m1 = Mvs.find v2 m2 - | Tvar v1, Tvar v2 when not (Mvs.mem v2 m2) -> - vs_equal v1 v2 - | Tconst c1, Tconst c2 -> - c1 = c2 - | Tapp (s1,l1), Tapp (s2,l2) -> - ls_equal s1 s2 && List.for_all2 t_eq l1 l2 - | Tif (f1,t1,e1), Tif (f2,t2,e2) -> - t_eq f1 f2 && t_eq t1 t2 && t_eq e1 e2 - | Tlet (t1,b1), Tlet (t2,b2) -> - t_eq t1 t2 && - let u1,e1 = t_open_bound b1 in - let u2,e2 = t_open_bound b2 in - let m1 = vs_rename_alpha c1 m1 u1 in - let m2 = vs_rename_alpha c2 m2 u2 in - t_equal_alpha c1 c2 m1 m2 e1 e2 - | Tcase (t1,bl1), Tcase (t2,bl2) -> - t_eq t1 t2 && - let br_eq ((p1,_,_) as b1) ((p2,_,_) as b2) = - pat_equal_alpha p1 p2 && - let p1,e1 = t_open_branch b1 in - let p2,e2 = t_open_branch b2 in - let m1 = pat_rename_alpha c1 m1 p1 in - let m2 = pat_rename_alpha c2 m2 p2 in - t_equal_alpha c1 c2 m1 m2 e1 e2 - in - Lists.equal br_eq bl1 bl2 - | Teps b1, Teps b2 -> - let u1,e1 = t_open_bound b1 in - let u2,e2 = t_open_bound b2 in - let m1 = vs_rename_alpha c1 m1 u1 in - let m2 = vs_rename_alpha c2 m2 u2 in - t_equal_alpha c1 c2 m1 m2 e1 e2 - | Tquant (q1,((vl1,_,_,_) as b1)), Tquant (q2,((vl2,_,_,_) as b2)) -> - q1 = q2 && - Lists.equal (fun v1 v2 -> ty_equal v1.vs_ty v2.vs_ty) vl1 vl2 && - let vl1,_,e1 = t_open_quant b1 in - let vl2,_,e2 = t_open_quant b2 in - let m1 = vl_rename_alpha c1 m1 vl1 in - let m2 = vl_rename_alpha c2 m2 vl2 in - t_equal_alpha c1 c2 m1 m2 e1 e2 - | Tbinop (a,f1,g1), Tbinop (b,f2,g2) -> - a = b && t_eq f1 f2 && t_eq g1 g2 - | Tnot f1, Tnot f2 -> - t_eq f1 f2 - | Ttrue, Ttrue | Tfalse, Tfalse -> - true - | _ -> false - -let t_equal_alpha = t_equal_alpha (ref (-1)) (ref (-1)) Mvs.empty Mvs.empty - -(* hash modulo alpha *) - -(* dead code -let rec pat_hash_alpha p = - match p.pat_node with - | Pwild -> 0 - | Pvar _ -> 1 - | Papp (f, l) -> - let acc = Hashcons.combine 2 (ls_hash f) in - Hashcons.combine_list pat_hash_alpha acc l - | Pas (p, _) -> Hashcons.combine 3 (pat_hash_alpha p) - | Por (p, q) -> - Hashcons.combine - (Hashcons.combine 4 (pat_hash_alpha p)) (pat_hash_alpha q) -*) - -let rec t_hash_alpha c m t = - let fn = t_hash_alpha c m in - match t.t_node with - | Tvar v -> - Hashcons.combine 0 (Mvs.find_def (vs_hash v) v m) - | Tconst c -> - Hashcons.combine 1 (Hashtbl.hash c) - | Tapp (s,l) -> - let acc = Hashcons.combine 2 (ls_hash s) in - Hashcons.combine_list fn acc l - | Tif (f,t1,t2) -> - Hashcons.combine3 3 (fn f) (fn t1) (fn t2) - | Tlet (t1,b) -> - let u,t2 = t_open_bound b in - let m = vs_rename_alpha c m u in - Hashcons.combine2 4 (fn t1) (t_hash_alpha c m t2) - | Tcase (t1,bl) -> - let hash_br b = - let p,t2 = t_open_branch b in - let m = pat_rename_alpha c m p in - t_hash_alpha c m t2 - in - let acc = Hashcons.combine 5 (fn t1) in - Hashcons.combine_list hash_br acc bl - | Teps b -> - let u,f = t_open_bound b in - let m = vs_rename_alpha c m u in - Hashcons.combine 6 (t_hash_alpha c m f) - | Tquant (q,b) -> - let vl,_,f1 = t_open_quant b in - let m = vl_rename_alpha c m vl in - let hq = match q with Tforall -> 1 | Texists -> 2 in - Hashcons.combine2 1 hq (t_hash_alpha c m f1) - | Tbinop (o,f,g) -> - let ho = match o with - | Tand -> 3 | Tor -> 4 | Timplies -> 5 | Tiff -> 7 - in - Hashcons.combine3 2 ho (fn f) (fn g) - | Tnot f -> - Hashcons.combine 3 (fn f) - | Ttrue -> 4 - | Tfalse -> 5 +let t_subst m t = Mvs.iter vs_check m; t_subst_unsafe m t -let t_hash_alpha = t_hash_alpha (ref (-1)) Mvs.empty +let t_subst_single v t1 t = t_subst (Mvs.singleton v t1) t -module Hterm_alpha = Exthtbl.Make (struct - type t = term - let equal = t_equal_alpha - let hash = t_hash_alpha -end) +(* set of free variables *) -(* binder-free term/formula matching *) - -(* exception NoMatch *) - -(* let rec t_match s t1 t2 = *) -(* if not (oty_equal t1.t_ty t2.t_ty) then raise NoMatch else *) -(* match t1.t_node, t2.t_node with *) -(* | Tconst c1, Tconst c2 when c1 = c2 -> s *) -(* | Tvar v1, _ -> *) -(* Mvs.change v1 (function *) -(* | None -> Some t2 *) -(* | Some t1 as r when t_equal t1 t2 -> r *) -(* | _ -> raise NoMatch) s *) -(* | Tapp (s1,l1), Tapp (s2,l2) when ls_equal s1 s2 -> *) -(* List.fold_left2 t_match s l1 l2 *) -(* | Tif (f1,t1,e1), Tif (f2,t2,e2) -> *) -(* t_match (t_match (t_match s f1 f2) t1 t2) e1 e2 *) -(* | Tbinop (op1,f1,g1), Tbinop (op2,f2,g2) when op1 = op2 -> *) -(* t_match (t_match s f1 f2) g1 g2 *) -(* | Tnot f1, Tnot f2 -> *) -(* t_match s f1 f2 *) -(* | Ttrue, Ttrue *) -(* | Tfalse, Tfalse -> *) -(* s *) -(* | _ -> raise NoMatch *) +let t_freevars = add_t_vars (* occurrence check *) let rec t_occurs r t = t_equal r t || t_any (t_occurs r) t -let rec t_occurs_alpha r t = - t_equal_alpha r t || t_any (t_occurs_alpha r) t - (* substitutes term [t2] for term [t1] in term [t] *) let rec t_replace t1 t2 t = @@ -1378,13 +1324,6 @@ let t_replace t1 t2 t = t_ty_check t2 t1.t_ty; t_replace t1 t2 t -let rec t_replace_alpha t1 t2 t = - if t_equal_alpha t t1 then t2 else t_map (t_replace_alpha t1 t2) t - -let t_replace_alpha t1 t2 t = - t_ty_check t2 t1.t_ty; - t_replace_alpha t1 t2 t - (* constructors with propositional simplification *) let keep_on_simp_label = create_label "keep_on_simp" @@ -1474,7 +1413,7 @@ let small t = match t.t_node with | _ -> false let t_let_simp e ((v,b,t) as bt) = - let n = Mvs.find_def 0 v t.t_vars in + let n = t_v_occurs v t in if n = 0 && can_simp e then t_subst_unsafe b.bv_subst t else if n = 1 || small e then begin @@ -1484,7 +1423,7 @@ let t_let_simp e ((v,b,t) as bt) = t_let e bt let t_let_close_simp v e t = - let n = Mvs.find_def 0 v t.t_vars in + let n = t_v_occurs v t in if n = 0 && can_simp e then t else if n = 1 || small e then t_subst_single v e t @@ -1503,7 +1442,7 @@ let t_case_simp t bl = | Ttrue when can_simp e -> e0_true | Tfalse when can_simp e -> e0_false | _ -> t_equal e e0 in - if can_simp t && Mvs.is_empty e0.t_vars && List.for_all is_e0 tl then e0 + if can_simp t && t_closed e0 && List.for_all is_e0 tl then e0 else t_case t bl let t_case_close_simp t bl = @@ -1518,29 +1457,31 @@ let t_case_close_simp t bl = | Ttrue when can_simp e -> e0_true | Tfalse when can_simp e -> e0_false | _ -> t_equal e e0 in - if can_simp t && Mvs.is_empty e0.t_vars && List.for_all is_e0 tl then e0 + if can_simp t && t_closed e0 && List.for_all is_e0 tl then e0 else t_case_close t bl -let v_occurs f v = Mvs.mem v f.t_vars -let v_subset f e = Mvs.set_submap e.t_vars f.t_vars - -let vl_filter f vl = List.filter (v_occurs f) vl -let tr_filter f tl = List.filter (List.for_all (v_subset f)) tl - let t_quant_simp q ((vl,_,_,f) as qf) = - if List.for_all (v_occurs f) vl then + let fvs = t_vars f in + let check v = Mvs.mem v fvs in + if List.for_all check vl then t_quant q qf else let vl,tl,f = t_open_quant qf in - let vl = vl_filter f vl in - if vl = [] then f else t_quant_close q vl (tr_filter f tl) f + let fvs = t_vars f in + let check v = Mvs.mem v fvs in + let vl = List.filter check vl in + if vl = [] then f + else t_quant_close q vl (List.filter (List.for_all (t_v_all check)) tl) f let t_quant_close_simp q vl tl f = - if List.for_all (v_occurs f) vl then + let fvs = t_vars f in + let check v = Mvs.mem v fvs in + if List.for_all check vl then t_quant_close q vl tl f else - let vl = vl_filter f vl in - if vl = [] then f else t_quant_close q vl (tr_filter f tl) f + let vl = List.filter check vl in + if vl = [] then f + else t_quant_close q vl (List.filter (List.for_all (t_v_all check)) tl) f let t_forall_simp = t_quant_simp Tforall let t_exists_simp = t_quant_simp Texists diff --git a/src/core/term.mli b/src/core/term.mli index b10a85d86da6884a4960149063b3dcba5cfe35f8..6eb7d1660f6ff4cdd96c5ea807550abcbe1b1ff5 100644 --- a/src/core/term.mli +++ b/src/core/term.mli @@ -27,6 +27,7 @@ module Svs : Extset.S with module M = Mvs module Hvs : Exthtbl.S with type key = vsymbol module Wvs : Weakhtbl.S with type key = vsymbol +val vs_compare : vsymbol -> vsymbol -> int val vs_equal : vsymbol -> vsymbol -> bool val vs_hash : vsymbol -> int @@ -47,6 +48,7 @@ module Sls : Extset.S with module M = Mls module Hls : Exthtbl.S with type key = lsymbol module Wls : Weakhtbl.S with type key = lsymbol +val ls_compare : lsymbol -> lsymbol -> int val ls_equal : lsymbol -> lsymbol -> bool val ls_hash : lsymbol -> int @@ -77,7 +79,6 @@ type pattern = private { pat_node : pattern_node; pat_vars : Svs.t; pat_ty : ty; - pat_tag : int; } and pattern_node = private @@ -87,9 +88,6 @@ and pattern_node = private | Por of pattern * pattern | Pas of pattern * vsymbol -val pat_equal : pattern -> pattern -> bool -val pat_hash : pattern -> int - (** Smart constructors for patterns *) val pat_wild : ty -> pattern @@ -122,8 +120,6 @@ type term = private { t_ty : ty option; t_label : Slab.t; t_loc : Loc.position option; - t_vars : int Mvs.t; - t_tag : int; } and term_node = private @@ -150,6 +146,7 @@ module Mterm : Extmap.S with type key = term module Sterm : Extset.S with module M = Mterm module Hterm : Exthtbl.S with type key = term +val t_compare : term -> term -> int val t_equal : term -> term -> bool val t_hash : term -> int @@ -383,6 +380,10 @@ val t_v_fold : ('a -> vsymbol -> 'a) -> 'a -> term -> 'a val t_v_all : (vsymbol -> bool) -> term -> bool val t_v_any : (vsymbol -> bool) -> term -> bool +val t_v_count : ('a -> vsymbol -> int -> 'a) -> 'a -> term -> 'a + +val t_v_occurs : vsymbol -> term -> int + (** Variable substitution *) val t_subst : term Mvs.t -> term -> term @@ -392,7 +393,12 @@ val t_ty_subst : ty Mtv.t -> term Mvs.t -> term -> term (** Find free variables and type variables *) -val t_freevars : int Mvs.t -> term -> int Mvs.t +val t_closed : term -> bool + +val t_vars : term -> int Mvs.t + +val t_freevars : int Mvs.t -> term -> int Mvs.t + val t_ty_freevars : Stv.t -> term -> Stv.t (** Map/fold over types and logical symbols in terms and patterns *) @@ -417,17 +423,7 @@ val t_app_map : val t_app_fold : ('a -> lsymbol -> ty list -> ty option -> 'a) -> 'a -> term -> 'a -(** Equality modulo alpha *) - -val t_equal_alpha : term -> term -> bool - -module Hterm_alpha : Exthtbl.S with type key = term - (** Subterm occurrence check and replacement *) -val t_occurs : term -> term -> bool -val t_occurs_alpha : term -> term -> bool - +val t_occurs : term -> term -> bool val t_replace : term -> term -> term -> term -val t_replace_alpha : term -> term -> term -> term - diff --git a/src/core/trans.ml b/src/core/trans.ml index 8b2bc7baf2c3835d8779c5d19bb55d19a55c6831..6d21d7892bf2dbdeb510fe0707f14b8d5957a654 100644 --- a/src/core/trans.ml +++ b/src/core/trans.ml @@ -47,7 +47,9 @@ module Wtask = Weakhtbl.Make (struct let tag t = t.task_tag end) -let store fn = Wtask.memoize_option 63 fn +let store fn = let tr = Wtask.memoize_option 63 fn in fun t -> match t with + | Some {task_decl = {td_node = Decl {d_node = Dprop (Pgoal,_,_)}}} -> fn t + | _ -> tr t let bind f g = store (fun task -> g (f task) task) @@ -60,8 +62,9 @@ let fold fn v = | Use _ -> 'U' | Meta _ -> 'M') (task.task_decl.td_tag); *) let acc = fn task acc in - Wtask.set h task acc; - acc + match task.task_decl.td_node with + | Decl {d_node = Dprop (Pgoal,_,_)} -> acc + | _ -> Wtask.set h task acc; acc in let current task = try Some (Wtask.find h task) @@ -82,8 +85,12 @@ let fold_map fn v t = conv_res snd (fold fn (v, t)) let fold_map_l fn v t = conv_res (List.map snd) (fold_l fn (v, t)) (* we use List.map instead of List.map_rev to preserve the order *) +let store_decl fn = let tr = Wdecl.memoize 63 fn in function + | {d_node = Dprop (Pgoal,_,_)} as d -> fn d + | d -> tr d + let gen_decl add fn = - let fn = Wdecl.memoize 63 fn in + let fn = store_decl fn in let fn task acc = match task.task_decl.td_node with | Decl d -> List.fold_left add acc (fn d) | _ -> add_tdecl acc task.task_decl @@ -91,7 +98,7 @@ let gen_decl add fn = fold fn let gen_decl_l add fn = - let fn = Wdecl.memoize 63 fn in + let fn = store_decl fn in let fn task acc = match task.task_decl.td_node with | Decl d -> List.map (List.fold_left add acc) (fn d) | _ -> [add_tdecl acc task.task_decl] @@ -107,17 +114,15 @@ let apply_to_goal fn d = match d.d_node with | Dprop (Pgoal,pr,f) -> fn pr f | _ -> assert false -let gen_goal add fn = - let fn = Wdecl.memoize 5 (apply_to_goal fn) in store (function - | Some { task_decl = { td_node = Decl d }; task_prev = prev } -> - List.fold_left add prev (fn d) - | _ -> assert false) - -let gen_goal_l add fn = - let fn = Wdecl.memoize 5 (apply_to_goal fn) in store (function - | Some { task_decl = { td_node = Decl d }; task_prev = prev } -> - List.map (List.fold_left add prev) (fn d) - | _ -> assert false) +let gen_goal add fn = function + | Some { task_decl = { td_node = Decl d }; task_prev = prev } -> + List.fold_left add prev (apply_to_goal fn d) + | _ -> assert false + +let gen_goal_l add fn = function + | Some { task_decl = { td_node = Decl d }; task_prev = prev } -> + List.map (List.fold_left add prev) (apply_to_goal fn d) + | _ -> assert false let goal = gen_goal add_decl let goal_l = gen_goal_l add_decl diff --git a/src/core/ty.ml b/src/core/ty.ml index c9a7c066a56713d2a6e9d4842ad70ccb8a82900e..58932485f99ba135e534998c7953e9f3008eb3c8 100644 --- a/src/core/ty.ml +++ b/src/core/ty.ml @@ -28,8 +28,8 @@ module Mtv = Tvar.M module Htv = Tvar.H let tv_equal : tvsymbol -> tvsymbol -> bool = (==) - let tv_hash tv = id_hash tv.tv_name +let tv_compare tv1 tv2 = id_compare tv1.tv_name tv2.tv_name let create_tvsymbol n = { tv_name = id_register n } @@ -66,6 +66,9 @@ let ty_equal : ty -> ty -> bool = (==) let ts_hash ts = id_hash ts.ts_name let ty_hash ty = Weakhtbl.tag_hash ty.ty_tag +let ts_compare ts1 ts2 = id_compare ts1.ts_name ts2.ts_name +let ty_compare ty1 ty2 = Pervasives.compare (ty_hash ty1) (ty_hash ty2) + let mk_ts name args def = { ts_name = id_register name; ts_args = args; @@ -252,6 +255,8 @@ let oty_type = function Some ty -> ty | None -> raise UnexpectedProp let oty_equal = Opt.equal ty_equal let oty_hash = Opt.fold (fun _ -> ty_hash) 1 +let oty_compare o1 o2 = Opt.compare ty_compare o1 o2 + let oty_match m o1 o2 = match o1,o2 with | Some ty1, Some ty2 -> ty_match m ty1 ty2 | None, None -> m diff --git a/src/core/ty.mli b/src/core/ty.mli index ba7b6878d02d29584122f8850af4fa17e0250f62..65a6363267dd2e91d9db3d180a930d33560346de 100644 --- a/src/core/ty.mli +++ b/src/core/ty.mli @@ -55,6 +55,9 @@ module Sty : Extset.S with module M = Mty module Hty : Exthtbl.S with type key = ty module Wty : Weakhtbl.S with type key = ty +val ts_compare : tysymbol -> tysymbol -> int +val ty_compare : ty -> ty -> int + val ts_equal : tysymbol -> tysymbol -> bool val ty_equal : ty -> ty -> bool @@ -127,6 +130,7 @@ val is_ts_tuple_id : ident -> int option exception UnexpectedProp +val oty_compare : ty option -> ty option -> int val oty_equal : ty option -> ty option -> bool val oty_hash : ty option -> int diff --git a/src/driver/driver.ml b/src/driver/driver.ml index bbffcd4e3d5edc81cd9cb70f5438110a84ce8bb4..1f3021121663fb770a09bda66287dea3436d1743 100644 --- a/src/driver/driver.ml +++ b/src/driver/driver.ml @@ -248,36 +248,26 @@ let call_on_buffer ~command ?timelimit ?memlimit ?inplace ~filename drv buffer = exception NoPrinter -let update_task drv task_orig = - (** task_orig is the task for looking for theories - task is the task for adding new metas - goal is the last decl that we want to keep at the end (goal or clone) - *) - let task, goal = match task_orig with - | Some { task_decl = g ; task_prev = t } -> t,g - | None -> raise Task.GoalNotFound - in - let task = +let update_task = let ht = Hint.create 5 in fun drv -> + let update task0 = Mid.fold (fun _ (th,s) task -> Task.on_theory th (fun task sm -> Stdecl.fold (fun tdm task -> add_tdecl task (clone_meta tdm sm) ) s task - ) task task_orig - ) drv.drv_meta task + ) task task0 + ) drv.drv_meta task0 in - add_tdecl task goal - -let update_task = - let h = Hint.create 5 in - fun drv -> - let update = try Hint.find h drv.drv_tag with - | Not_found -> - let upd = Trans.store (update_task drv) in - Hint.add h drv.drv_tag upd; - upd - in - Trans.apply update + function + | Some {task_decl = {td_node = Decl {d_node = Dprop (Pgoal,_,_)}} as goal; + task_prev = task} -> + (* we cannot add metas nor memoize after goal *) + let update = try Hint.find ht drv.drv_tag with Not_found -> + let upd = Trans.store update in + Hint.add ht drv.drv_tag upd; upd in + let task = Trans.apply update task in + add_tdecl task goal + | task -> update task let prepare_task drv task = let lookup_transform t = lookup_transform t drv.drv_env in diff --git a/src/parser/denv.ml b/src/parser/denv.ml index 232d5647dbb9f82ed3ab34c658fda089702d6d8f..76189510b75b3c3ec5749088d1fc1c76da03bc70 100644 --- a/src/parser/denv.ml +++ b/src/parser/denv.ml @@ -192,14 +192,14 @@ and dtrigger = let allowed_unused s = String.length s > 0 && s.[0] = '_' -let check_used_var vars v = - if not (Mvs.mem v vars) then +let check_used_var t v = + if t_v_occurs v t = 0 then let s = v.vs_name.id_string in if not (allowed_unused s) then Warning.emit ?loc:v.vs_name.Ident.id_loc "unused variable %s" s -let check_used_vars vars = - List.iter (check_used_var vars) +let check_used_vars t vl = + List.iter (check_used_var t) vl let check_exists_implies q f = match q,f.t_node with @@ -224,7 +224,7 @@ let rec term env t = match t.dt_node with let v = create_user_vs id (t_type e1) in let env = Mstr.add id.id v env in let e2 = term env e2 in - check_used_var e2.t_vars v; + check_used_var e2 v; t_let_close v e1 e2 | Tmatch (t1, bl) -> let branch (p,e) = @@ -267,7 +267,7 @@ and fmla env = function in let trl = List.map (List.map trigger) trl in let f = fmla env f1 in - check_used_vars f.Term.t_vars vl; + check_used_vars f vl; check_exists_implies q f; t_quant_close q vl trl f | Fapp (s, tl) -> @@ -277,7 +277,7 @@ and fmla env = function let v = create_user_vs id (t_type e1) in let env = Mstr.add id.id v env in let f2 = fmla env f2 in - check_used_var f2.t_vars v; + check_used_var f2 v; t_let_close v e1 f2 | Fmatch (t, bl) -> let branch (p,e) = diff --git a/src/printer/alt_ergo.ml b/src/printer/alt_ergo.ml index d6f21c11d1b0acc17b600bc16dd9ef5c4983950b..44ffdaf85cd5768a90e037e7adfddc3245b075fa 100644 --- a/src/printer/alt_ergo.ml +++ b/src/printer/alt_ergo.ml @@ -251,6 +251,7 @@ let print_enum_decl fmt ts csl = (print_list alt2 print_cs) csl let print_ty_decl info fmt ts = + if ts.ts_def <> None then () else if Mid.mem ts.ts_name info.info_syn then () else (fprintf fmt "%a@\n@\n" print_type_decl ts; forget_tvs ()) @@ -333,8 +334,6 @@ let print_decl info fmt d = match d.d_node with "alt-ergo: inductive definitions are not supported" | Dprop (k,pr,f) -> print_prop_decl info fmt k pr f -let print_decl info fmt = catch_unsupportedDecl (print_decl info fmt) - let add_projection (csm,pjs,axs) = function | [Theory.MAls ls; Theory.MAls cs; Theory.MAint ind; Theory.MApr pr] -> let csm = try Array.set (Mls.find cs csm) ind ls; csm @@ -353,66 +352,41 @@ let check_typecasts acc = function | [Theory.MAstr _] -> acc | _ -> assert false -(* -let print_task_old pr thpr fmt task = - print_prelude fmt pr; - print_th_prelude task fmt thpr; - let csm,pjs,axs = Task.on_meta Eliminate_algebraic.meta_proj - add_projection (Mls.empty,Sls.empty,Spr.empty) task in - let info = { - info_syn = get_syntax_map task; - info_ac = Task.on_tagged_ls meta_ac task; - info_show_labels = - Task.on_meta meta_printer_option check_showlabels false task; - info_csm = Mls.map Array.to_list csm; - info_pjs = pjs; - info_axs = axs; - } in - let decls = Task.task_decls task in - fprintf fmt "%a@." (print_list nothing (print_decl info)) decls - -let () = register_printer "alt-ergo-old" - (fun _env pr thpr ?old:_ fmt task -> - forget_all ident_printer; - print_task_old pr thpr fmt task) -*) - let print_decls = - let print inv_trig ac sl tc csm pjs axs sm fmt d = + let print_decl info fmt d = + try print_decl info fmt d; info, [] + with Unsupported s -> raise (UnsupportedDecl (d,s)) in + let print_decl = Printer.sprint_decl print_decl in + let print_decl task acc = print_decl task.Task.task_decl acc in + Discriminate.on_syntax_map (fun sm -> + Trans.on_tagged_ls meta_ac (fun ac -> + Trans.on_meta meta_printer_option (fun args -> + Trans.on_meta Eliminate_algebraic.meta_proj (fun mal -> + Trans.on_tagged_ls meta_invalid_trigger (fun inv_trig -> + let csm,pjs,axs = + List.fold_left add_projection (Mls.empty,Sls.empty,Spr.empty) mal in let info = { info_syn = sm; info_ac = ac; - info_show_labels = sl; - info_type_casts = tc; + info_show_labels = List.fold_left check_showlabels false args; + info_type_casts = List.fold_left check_typecasts true args; info_csm = Mls.map Array.to_list csm; info_pjs = pjs; info_axs = axs; info_inv_trig = Sls.add ps_equ inv_trig; } in - print_decl info fmt d in - Trans.on_tagged_ls meta_invalid_trigger (fun inv_trig -> - Trans.on_tagged_ls meta_ac (fun ac -> - Trans.on_meta meta_printer_option (fun args -> - let sl = List.fold_left check_showlabels false args in - let tc = List.fold_left check_typecasts true args in - Trans.on_meta Eliminate_algebraic.meta_proj (fun mal -> - let csm,pjs,axs = List.fold_left - add_projection (Mls.empty,Sls.empty,Spr.empty) mal in - Printer.sprint_decls (print inv_trig ac sl tc csm pjs axs))))) + Trans.fold print_decl (info,[])))))) let print_task _env pr thpr _blacklist ?old:_ fmt task = (* In trans-based p-printing [forget_all] is a no-no *) (* forget_all ident_printer; *) print_prelude fmt pr; print_th_prelude task fmt thpr; - fprintf fmt "%a@." (print_list nothing string) - (List.rev (Trans.apply print_decls task)) + let rec print = function + | x :: r -> print r; Pp.string fmt x + | [] -> () in + print (snd (Trans.apply print_decls task)); + pp_print_flush fmt () let () = register_printer "alt-ergo" print_task ~desc:"Printer for the Alt-Ergo theorem prover." -(* -let print_goal info fmt (id, f, task) = - print_task info fmt task; - fprintf fmt "@\n@[goal %a : %a@]@\n" print_ident id (print_fmla info) f -*) - diff --git a/src/printer/cvc3.ml b/src/printer/cvc3.ml index 377eecc99d626f5bea291c2675208fd9f93cd5dd..4955de0548f0c05bfe89f49d709dc8bd8ab7cd33 100644 --- a/src/printer/cvc3.ml +++ b/src/printer/cvc3.ml @@ -47,56 +47,37 @@ let ident_printer = let print_ident fmt id = fprintf fmt "%s" (id_unique ident_printer id) -(** type *) type info = { - info_syn : syntax_map; - complex_type : ty Hty.t; + info_syn : syntax_map; + complex_type : ty Mty.t ref; + urg_output : string list ref; } -let rec print_type info fmt ty = match ty.ty_node with - | Tyvar _ -> unsupported "cvc3 : you must encode the polymorphism" - | Tyapp (ts, []) -> begin match query_syntax info.info_syn ts.ts_name with - | Some s -> syntax_arguments s (print_type info) fmt [] - | None -> fprintf fmt "%a" print_ident ts.ts_name - end - | Tyapp (ts, l) -> - begin match query_syntax info.info_syn ts.ts_name with - | Some s -> syntax_arguments s (print_type info) fmt l - | None -> print_type info fmt (Hty.find info.complex_type ty) - end - -(* and print_tyapp info fmt = function *) -(* | [] -> () *) -(* | [ty] -> fprintf fmt "%a " (print_type info) ty *) -(* | tl -> fprintf fmt "(%a) " (print_list comma (print_type info)) tl *) +(** type *) +let complex_type = Wty.memoize 3 (fun ty -> + let s = Pp.string_of_wnl Pretty.print_ty ty in + create_tysymbol (id_fresh s) [] None) -let rec iter_complex_type info fmt () ty = match ty.ty_node with - | Tyvar _ -> unsupported "cvc3 : you must encode the polymorphism" - | Tyapp (_, []) -> () +let rec print_type info fmt ty = match ty.ty_node with + | Tyvar _ -> unsupported "cvc3: you must encode the polymorphism" | Tyapp (ts, l) -> - begin match query_syntax info.info_syn ts.ts_name with - | Some _ -> List.iter (iter_complex_type info fmt ()) l - | None when not (Hty.mem info.complex_type ty) -> - let id = id_fresh (Pp.string_of_wnl Pretty.print_ty ty) in - let ts = create_tysymbol id [] None in - let cty = ty_app ts [] in - fprintf fmt "%a: TYPE;@." - print_ident ts.ts_name; - Hty.add info.complex_type ty cty - | None -> () - end - -let find_complex_type info fmt f = - t_ty_fold (iter_complex_type info fmt) () f + begin match query_syntax info.info_syn ts.ts_name, l with + | Some s, _ -> syntax_arguments s (print_type info) fmt l + | None, [] -> fprintf fmt "%a" print_ident ts.ts_name + | None, _ -> + begin match Mty.find_opt ty !(info.complex_type) with + | Some ty -> print_type info fmt ty + | None -> + let ts = complex_type ty in let cty = ty_app ts [] in + let us = sprintf "%a: TYPE;@\n@\n" print_ident ts.ts_name in + info.complex_type := Mty.add ty cty !(info.complex_type); + info.urg_output := us :: !(info.urg_output); + print_type info fmt cty + end + end -let find_complex_type_expr info fmt f = - TermTF.t_selecti - (t_ty_fold (iter_complex_type info fmt)) - (t_ty_fold (iter_complex_type info fmt)) - () f - -let print_type info fmt = - catch_unsupportedType (print_type info fmt) +let print_type info fmt ty = try print_type info fmt ty + with Unsupported s -> raise (UnsupportedType (ty,s)) let print_type_value info fmt = function | None -> fprintf fmt "BOOLEAN" @@ -221,42 +202,28 @@ and print_triggers info fmt = function (print_list comma (print_expr info)) a (print_triggers info) l -let _print_logic_binder info fmt v = - fprintf fmt "%a: %a" print_ident v.vs_name - (print_type info) v.vs_ty - let print_type_decl info fmt ts = - if Mid.mem ts.ts_name info.info_syn then false else - if ts.ts_args = [] then - (fprintf fmt "%a : TYPE;" print_ident ts.ts_name; true) - else false + if ts.ts_args = [] && ts.ts_def = None then + if not (Mid.mem ts.ts_name info.info_syn) then + fprintf fmt "%a : TYPE;@\n@\n" print_ident ts.ts_name + +let print_lsargs info fmt = function + | [] -> () + | l -> fprintf fmt "(%a) -> " (print_list comma (print_type info)) l let print_param_decl info fmt ls = - let print_lsargs info fmt = function - | [] -> () - | l -> fprintf fmt "(%a) -> " - (print_list comma (print_type info)) l in - List.iter (iter_complex_type info fmt ()) ls.ls_args; - Opt.iter (iter_complex_type info fmt ()) ls.ls_value; - fprintf fmt "@[%a: %a%a;@]@\n" + fprintf fmt "@[%a: %a%a;@]@\n@\n" print_ident ls.ls_name (print_lsargs info) ls.ls_args (print_type_value info) ls.ls_value let print_param_decl info fmt ls = - if Mid.mem ls.ls_name info.info_syn then - false else (print_param_decl info fmt ls; true) + if not (Mid.mem ls.ls_name info.info_syn) + then print_param_decl info fmt ls let print_logic_decl info fmt (ls,def) = - let print_lsargs info fmt = function - | [] -> () - | l -> fprintf fmt "(%a) -> " - (print_list comma (print_type info)) l in - List.iter (iter_complex_type info fmt ()) ls.ls_args; - Opt.iter (iter_complex_type info fmt ()) ls.ls_value; let vsl,expr = Decl.open_ls_defn def in - find_complex_type_expr info fmt expr; - fprintf fmt "@[%a: %a%a = LAMBDA (%a): %a;@]@\n" + fprintf fmt "@[%a: %a%a = LAMBDA (%a): %a;@]@\n@\n" print_ident ls.ls_name (print_lsargs info) ls.ls_args (print_type_value info) ls.ls_value @@ -265,8 +232,8 @@ let print_logic_decl info fmt (ls,def) = List.iter forget_var vsl let print_logic_decl info fmt d = - if Mid.mem (fst d).ls_name info.info_syn then - false else (print_logic_decl info fmt d; true) + if not (Mid.mem (fst d).ls_name info.info_syn) + then print_logic_decl info fmt d let print_decl info fmt d = match d.d_node with | Dtype ts -> @@ -276,59 +243,42 @@ let print_decl info fmt d = match d.d_node with | Dparam ls -> print_param_decl info fmt ls | Dlogic dl -> - print_list_opt newline (print_logic_decl info) fmt dl + print_list nothing (print_logic_decl info) fmt dl | Dind _ -> unsupportedDecl d "cvc3 : inductive definition are not supported" - | Dprop (Paxiom, pr, _) when Mid.mem pr.pr_name info.info_syn -> false + | Dprop (Paxiom, pr, _) when Mid.mem pr.pr_name info.info_syn -> () | Dprop (Paxiom, pr, f) -> - find_complex_type info fmt f; - fprintf fmt "@[%% %s@\nASSERT@ %a;@]@\n" - pr.pr_name.id_string - (print_fmla info) f; true + fprintf fmt "@[%% %s@\nASSERT@ %a;@]@\n@\n" + pr.pr_name.id_string (print_fmla info) f | Dprop (Pgoal, pr, f) -> - find_complex_type info fmt f; fprintf fmt "@[QUERY@\n"; fprintf fmt "@[%% %a@]@\n" print_ident pr.pr_name; (match pr.pr_name.id_loc with - | None -> () - | Some loc -> fprintf fmt " @[%% %a@]@\n" - Loc.gen_report_position loc); - fprintf fmt " @[%a;@]@]" (print_fmla info) f; - true + | Some loc -> fprintf fmt " @[%% %a@]@\n" Loc.gen_report_position loc + | None -> ()); + fprintf fmt " @[%a;@]@]@\n" (print_fmla info) f | Dprop ((Plemma|Pskip), _, _) -> assert false -let print_decl info fmt = catch_unsupportedDecl (print_decl info fmt) - -let distingued = - let dist_syntax mls = function - | [MAls ls;MAstr s] -> Mls.add ls s mls - | _ -> assert false in - let dist_dist syntax mls = function - | [MAls ls;MAls lsdis] -> - begin try - Mid.add lsdis.ls_name (Mls.find ls syntax) mls - with Not_found -> mls end - | _ -> assert false in - Trans.on_meta meta_syntax_logic (fun syntax -> - let syntax = List.fold_left dist_syntax Mls.empty syntax in - Trans.on_meta Discriminate.meta_lsinst (fun dis -> - let dis2 = List.fold_left (dist_dist syntax) Mid.empty dis in - Trans.return dis2)) +let print_decls = + let print_decl (sm,ct) fmt d = + let info = {info_syn = sm; complex_type = ref ct; urg_output = ref []} in + try print_decl info fmt d; (sm, !(info.complex_type)), !(info.urg_output) + with Unsupported s -> raise (UnsupportedDecl (d,s)) in + let print_decl = Printer.sprint_decl print_decl in + let print_decl task acc = print_decl task.Task.task_decl acc in + Discriminate.on_syntax_map (fun sm -> + Trans.fold print_decl ((sm,Mty.empty),[])) -let print_task pr thpr _blacklist fmt task = +let print_task _env pr thpr _blacklist ?old:_ fmt task = + (* In trans-based p-printing [forget_all] is a no-no *) + (* forget_all ident_printer; *) print_prelude fmt pr; print_th_prelude task fmt thpr; - let info = { - info_syn = Mid.union (fun _ _ s -> Some s) - (get_syntax_map task) (Trans.apply distingued task); - complex_type = Hty.create 5; - } - in - let decls = Task.task_decls task in - ignore (print_list_opt (add_flush newline2) (print_decl info) fmt decls) + let rec print = function + | x :: r -> print r; Pp.string fmt x + | [] -> () in + print (snd (Trans.apply print_decls task)); + pp_print_flush fmt () -let () = register_printer "cvc3" - (fun _env pr thpr blacklist ?old:_ fmt task -> - forget_all ident_printer; - print_task pr thpr blacklist fmt task) +let () = register_printer "cvc3" print_task ~desc:"Printer@ for@ the@ CVC3@ theorem@ prover." diff --git a/src/printer/simplify.ml b/src/printer/simplify.ml index 1a56dcf8076d93d945cc34c782b3a4779309f100..a1fb4dfef6a3057684272d81773d9d6f7e9f00be 100644 --- a/src/printer/simplify.ml +++ b/src/printer/simplify.ml @@ -123,46 +123,44 @@ and print_triggers info fmt = function | tl -> fprintf fmt "@ (PATS %a)" (print_list space (print_trigger info)) tl let print_decl info fmt d = match d.d_node with - | Dtype _ | Dparam _ -> - false + | Dtype _ | Dparam _ -> () | Ddata _ -> unsupportedDecl d "Algebraic datatypes are not supported" | Dlogic _ -> unsupportedDecl d "Predicate and function definition aren't supported" | Dind _ -> unsupportedDecl d "simplify : inductive definition are not supported" - | Dprop (Paxiom, pr, _) when Mid.mem pr.pr_name info.info_syn -> - false + | Dprop (Paxiom, pr, _) when Mid.mem pr.pr_name info.info_syn -> () | Dprop (Paxiom, pr, f) -> - fprintf fmt "@[(BG_PUSH@\n ;; axiom %s@\n @[%a@])@]@\n" - pr.pr_name.id_string (print_fmla info) f; - true + fprintf fmt "@[(BG_PUSH@\n ;; axiom %s@\n @[%a@])@]@\n@\n" + pr.pr_name.id_string (print_fmla info) f | Dprop (Pgoal, pr, f) -> fprintf fmt "@[;; %a@]@\n" print_ident pr.pr_name; - begin match pr.pr_name.id_loc with - | None -> () - | Some loc -> fprintf fmt " @[;; %a@]@\n" - Loc.gen_report_position loc - end; - fprintf fmt "@[%a@]@\n" (print_fmla info) f; - true + (match pr.pr_name.id_loc with + | Some loc -> fprintf fmt " @[;; %a@]@\n" Loc.gen_report_position loc + | None -> ()); + fprintf fmt "@[%a@]@\n" (print_fmla info) f | Dprop ((Plemma|Pskip), _, _) -> assert false -let print_decl info fmt = catch_unsupportedDecl (print_decl info fmt) - -let print_task pr thpr _blacklist fmt task = +let print_decls = + let print_decl sm fmt d = + try print_decl {info_syn = sm} fmt d; sm, [] + with Unsupported s -> raise (UnsupportedDecl (d,s)) in + let print_decl = Printer.sprint_decl print_decl in + let print_decl task acc = print_decl task.Task.task_decl acc in + Discriminate.on_syntax_map (fun sm -> Trans.fold print_decl (sm,[])) + +let print_task _env pr thpr _blacklist ?old:_ fmt task = + (* In trans-based p-printing [forget_all] is a no-no *) + (* forget_all ident_printer; *) print_prelude fmt pr; print_th_prelude task fmt thpr; - let info = { - info_syn = get_syntax_map task } - in - let decls = Task.task_decls task in - ignore (print_list_opt (add_flush newline2) (print_decl info) fmt decls) - -let () = register_printer "simplify" - (fun _env pr thpr blacklist ?old:_ fmt task -> - forget_all ident_printer; - print_task pr thpr blacklist fmt task) - ~desc:"Printer@ for@ the@ Simplify@ theorem@ prover." + let rec print = function + | x :: r -> print r; Pp.string fmt x + | [] -> () in + print (snd (Trans.apply print_decls task)); + pp_print_flush fmt () +let () = register_printer "simplify" print_task + ~desc:"Printer@ for@ the@ Simplify@ theorem@ prover." diff --git a/src/printer/smtv1.ml b/src/printer/smtv1.ml index 2cc9d49aa05161b03d087b8aef2b9b2c88c6d18b..f47fcf3dd8b7c0121fa575fa96adbba8124264ae 100644 --- a/src/printer/smtv1.ml +++ b/src/printer/smtv1.ml @@ -41,23 +41,36 @@ let print_var fmt {vs_name = id} = fprintf fmt "%s" n type info = { - info_syn : syntax_map; + info_syn : syntax_map; + complex_type : ty Mty.t ref; + urg_output : string list ref; } -let rec print_type info fmt ty = match ty.ty_node with - | Tyvar _ -> unsupported "smt : you must encode the polymorphism" - | Tyapp (ts, []) -> begin match query_syntax info.info_syn ts.ts_name with - | Some s -> syntax_arguments s (print_type info) fmt [] - | None -> fprintf fmt "%a" print_ident ts.ts_name - end - | Tyapp (_, _) -> unsupported "smt : you must encode the complexe type" - -(* and print_tyapp info fmt = function *) -(* | [] -> () *) -(* | [ty] -> fprintf fmt "%a " (print_type info) ty *) -(* | tl -> fprintf fmt "(%a) " (print_list comma (print_type info)) tl *) +let complex_type = Wty.memoize 3 (fun ty -> + let s = Pp.string_of_wnl Pretty.print_ty ty in + create_tysymbol (id_fresh s) [] None) -let print_type info fmt = catch_unsupportedType (print_type info fmt) +let rec print_type info fmt ty = match ty.ty_node with + | Tyvar _ -> unsupported "smtv1: you must encode the polymorphism" + | Tyapp (ts, l) -> + begin match query_syntax info.info_syn ts.ts_name, l with + | Some s, _ -> syntax_arguments s (print_type info) fmt l + | None, [] -> fprintf fmt "%a" print_ident ts.ts_name + | None, _ -> + begin match Mty.find_opt ty !(info.complex_type) with + | Some ty -> print_type info fmt ty + | None -> + let ts = complex_type ty in let cty = ty_app ts [] in + let us = sprintf + ":extrasorts (%a)@\n@\n" print_ident ts.ts_name in + info.complex_type := Mty.add ty cty !(info.complex_type); + info.urg_output := us :: !(info.urg_output); + print_type info fmt cty + end + end + +let print_type info fmt ty = try print_type info fmt ty + with Unsupported s -> raise (UnsupportedType (ty,s)) let rec print_term info fmt t = match t.t_node with | Tconst c -> @@ -148,80 +161,82 @@ and print_fmla info fmt f = match f.t_node with "smtv1 : you must eliminate match" | Tvar _ | Tconst _ | Teps _ -> raise (FmlaExpected f) +(* and _print_expr info fmt = TermTF.t_select (print_term info fmt) (print_fmla info fmt) and _print_triggers info fmt tl = print_list comma (_print_expr info) fmt tl - let _print_logic_binder info fmt v = fprintf fmt "%a: %a" print_ident v.vs_name (print_type info) v.vs_ty +*) let print_type_decl info fmt ts = - if Mid.mem ts.ts_name info.info_syn then false else - if ts.ts_args = [] then - (fprintf fmt ":extrasorts (%a)" print_ident ts.ts_name; true) - else unsupported "smtv1 : type with argument are not supported" + if ts.ts_args = [] && ts.ts_def = None then + if not (Mid.mem ts.ts_name info.info_syn) then + fprintf fmt ":extrasorts (%a)@\n@\n" print_ident ts.ts_name let print_param_decl info fmt ls = match ls.ls_value with | None -> - fprintf fmt "@[:extrapreds ((%a %a))@]@\n" + fprintf fmt "@[:extrapreds ((%a %a))@]@\n@\n" print_ident ls.ls_name (print_list space (print_type info)) ls.ls_args | Some value -> - fprintf fmt "@[:extrafuns ((%a %a %a))@]@\n" + fprintf fmt "@[:extrafuns ((%a %a %a))@]@\n@\n" print_ident ls.ls_name (print_list space (print_type info)) ls.ls_args (print_type info) value let print_param_decl info fmt ls = - if Mid.mem ls.ls_name info.info_syn then - false else (print_param_decl info fmt ls; true) + if not (Mid.mem ls.ls_name info.info_syn) then + print_param_decl info fmt ls let print_decl info fmt d = match d.d_node with | Dtype ts -> print_type_decl info fmt ts - | Ddata _ -> unsupported - "smtv1 : algebraic type are not supported" + | Ddata _ -> unsupportedDecl d + "smtv1 : algebraic types are not supported" | Dparam ls -> print_param_decl info fmt ls - | Dlogic _ -> unsupported - "Predicate and function definition aren't supported" + | Dlogic _ -> unsupportedDecl d + "smtv1 : predicate and function definitions are not supported" | Dind _ -> unsupportedDecl d - "smt : inductive definition are not supported" - | Dprop (Paxiom, pr, _) when Mid.mem pr.pr_name info.info_syn -> false + "smtv1 : inductive definitions are not supported" + | Dprop (Paxiom, pr, _) when Mid.mem pr.pr_name info.info_syn -> () | Dprop (Paxiom, pr, f) -> - fprintf fmt "@[;; %s@\n:assumption@ %a@]@\n" - pr.pr_name.id_string - (print_fmla info) f; true + fprintf fmt "@[;; %s@\n:assumption@ %a@]@\n@\n" + pr.pr_name.id_string (print_fmla info) f | Dprop (Pgoal, pr, f) -> fprintf fmt "@[:formula@\n"; fprintf fmt "@[;; %a@]@\n" print_ident pr.pr_name; (match pr.pr_name.id_loc with - | None -> () - | Some loc -> fprintf fmt " @[;; %a@]@\n" - Loc.gen_report_position loc); - fprintf fmt " @[(not@ %a)@]" (print_fmla info) f;true + | Some loc -> fprintf fmt " @[;; %a@]@\n" Loc.gen_report_position loc + | None -> ()); + fprintf fmt " @[(not@ %a)@]@\n" (print_fmla info) f | Dprop ((Plemma|Pskip), _, _) -> assert false -let print_decl info fmt = catch_unsupportedDecl (print_decl info fmt) - -let print_task pr thpr _blacklist fmt task = - fprintf fmt "(benchmark why3@\n" - (*print_ident (Task.task_goal task).pr_name*); +let print_decls = + let print_decl (sm,ct) fmt d = + let info = {info_syn = sm; complex_type = ref ct; urg_output = ref []} in + try print_decl info fmt d; (sm, !(info.complex_type)), !(info.urg_output) + with Unsupported s -> raise (UnsupportedDecl (d,s)) in + let print_decl = Printer.sprint_decl print_decl in + let print_decl task acc = print_decl task.Task.task_decl acc in + Discriminate.on_syntax_map (fun sm -> + Trans.fold print_decl ((sm,Mty.empty),[])) + +let print_task _env pr thpr _blacklist ?old:_ fmt task = + (* In trans-based p-printing [forget_all] is a no-no *) + (* forget_all ident_printer; *) + fprintf fmt "(benchmark why3@\n"; fprintf fmt " :status unknown@\n"; print_prelude fmt pr; print_th_prelude task fmt thpr; - let info = { - info_syn = get_syntax_map task; - } - in - let decls = Task.task_decls task in - ignore (print_list_opt (add_flush newline2) (print_decl info) fmt decls); - fprintf fmt "@\n)@." - -let () = register_printer "smtv1" - (fun _env pr thpr blacklist ?old:_ fmt task -> - forget_all ident_printer; - print_task pr thpr blacklist fmt task) + let rec print = function + | x :: r -> print r; Pp.string fmt x + | [] -> () in + print (snd (Trans.apply print_decls task)); + fprintf fmt ")@." + +let () = register_printer "smtv1" print_task ~desc:"Printer@ for@ the@ SMTlib@ version@ 1@ format." diff --git a/src/printer/smtv2.ml b/src/printer/smtv2.ml index 2bd2cd4a9162721f411f498910844b1afbc6b093..80660e7ef5ba74ec80504fedcfecadb9f10fe3ba 100644 --- a/src/printer/smtv2.ml +++ b/src/printer/smtv2.ml @@ -71,55 +71,23 @@ let ident_printer = let print_ident fmt id = fprintf fmt "%s" (id_unique ident_printer id) -(** type *) type info = { info_syn : syntax_map; -(* complex_type : ty Hty.t; *) } +(** type *) let rec print_type info fmt ty = match ty.ty_node with | Tyvar _ -> unsupported "smt : you must encode the polymorphism" - | Tyapp (ts, []) -> begin match query_syntax info.info_syn ts.ts_name with - | Some s -> syntax_arguments s (print_type info) fmt [] - | None -> fprintf fmt "%a" print_ident ts.ts_name - end | Tyapp (ts, l) -> - begin match query_syntax info.info_syn ts.ts_name with - | Some s -> syntax_arguments s (print_type info) fmt l - | None -> fprintf fmt "(%a %a)" print_ident ts.ts_name - (print_list space (print_type info)) l + begin match query_syntax info.info_syn ts.ts_name, l with + | Some s, _ -> syntax_arguments s (print_type info) fmt l + | None, [] -> fprintf fmt "%a" print_ident ts.ts_name + | None, _ -> fprintf fmt "(%a %a)" print_ident ts.ts_name + (print_list space (print_type info)) l end -(* -let iter_complex_type info fmt () ty = - match ty.ty_node with - | Tyapp (_,_::_) when not (Hty.mem info.complex_type ty) -> - let id = id_fresh (Pp.string_of_wnl Pretty.print_ty ty) in - let ts = create_tysymbol id [] None in - let cty = ty_app ts [] in - fprintf fmt "(define-sorts ((%a %a)))@\n" - print_ident ts.ts_name - (print_type info) ty; - Hty.add info.complex_type ty cty - | _ -> () - -let find_complex_type info fmt f = - t_ty_fold (iter_complex_type info fmt) () f - -let print_type info fmt ty = - print_type info fmt - (try - Hty.find info.complex_type ty - with Not_found -> ty) -*) - -(* and print_tyapp info fmt = function *) -(* | [] -> () *) -(* | [ty] -> fprintf fmt "%a " (print_type info) ty *) -(* | tl -> fprintf fmt "(%a) " (print_list comma (print_type info)) tl *) - -let print_type info fmt = - catch_unsupportedType (print_type info fmt) +let print_type info fmt ty = try print_type info fmt ty + with Unsupported s -> raise (UnsupportedType (ty,s)) let print_type_value info fmt = function | None -> fprintf fmt "Bool" @@ -246,10 +214,6 @@ and print_triggers info fmt = function (print_list space (print_trigger info)) a (print_triggers info) l -let _print_logic_binder info fmt v = - fprintf fmt "%a: %a" print_ident v.vs_name - (print_type info) v.vs_ty - let print_type_decl info fmt ts = if ts.ts_def <> None then () else if Mid.mem ts.ts_name info.info_syn then () else @@ -304,66 +268,24 @@ let print_decl info fmt d = match d.d_node with if Mid.mem pr.pr_name info.info_syn then () else print_prop_decl info fmt k pr f -let print_decl info fmt = catch_unsupportedDecl (print_decl info fmt) - -let distingued = - let dist_syntax mls = function - | [MAls ls;MAstr s] -> Mls.add ls s mls - | _ -> assert false in - let dist_dist syntax mls = function - | [MAls ls;MAls lsdis] -> - begin try - Mid.add lsdis.ls_name (Mls.find ls syntax) mls - with Not_found -> mls end - | _ -> assert false in - Trans.on_meta meta_syntax_logic (fun syntax -> - let syntax = List.fold_left dist_syntax Mls.empty syntax in - Trans.on_meta Discriminate.meta_lsinst (fun dis -> - let dis2 = List.fold_left (dist_dist syntax) Mid.empty dis in - Trans.return dis2)) - -let print_task_old pr thpr _blacklist fmt task = - print_prelude fmt pr; - print_th_prelude task fmt thpr; - let info = { - info_syn = Mid.union (fun _ _ s -> Some s) - (get_syntax_map task) (Trans.apply distingued task); - (* complex_type = Hty.create 5; *) - } - in - let decls = Task.task_decls task in - fprintf fmt "%a@." (print_list nothing (print_decl info)) decls - -let () = register_printer "smtv2" - (fun _env pr thpr blacklist ?old:_ fmt task -> - forget_all ident_printer; - print_task_old pr thpr blacklist fmt task) - ~desc:"Printer for the SMTlib version 2 format." - -(* let print_decls = - let add_ls sm acc = function - | [MAls ls; MAls lsdis] -> - begin try - Mid.add lsdis.ls_name (Mid.find ls.ls_name sm) acc - with Not_found -> acc end - | _ -> assert false in - let print dls sm fmt d = - let info = { - info_syn = List.fold_left (add_ls sm) sm dls; - } in - print_decl info fmt d in - Trans.on_meta Discriminate.meta_lsinst (fun dls -> - Printer.sprint_decls (print dls)) + let print_decl sm fmt d = + try print_decl {info_syn = sm} fmt d; sm, [] + with Unsupported s -> raise (UnsupportedDecl (d,s)) in + let print_decl = Printer.sprint_decl print_decl in + let print_decl task acc = print_decl task.Task.task_decl acc in + Discriminate.on_syntax_map (fun sm -> Trans.fold print_decl (sm,[])) let print_task _env pr thpr _blacklist ?old:_ fmt task = - (* In trans-based p-printing [forget_all] is taboo *) + (* In trans-based p-printing [forget_all] is a no-no *) (* forget_all ident_printer; *) print_prelude fmt pr; print_th_prelude task fmt thpr; - fprintf fmt "%a@." (print_list nothing string) - (List.rev (Trans.apply print_decls task)) - -let () = register_printer "smtv2new" print_task - ~desc:"Printer for the SMTlib version 2 format." -*) + let rec print = function + | x :: r -> print r; Pp.string fmt x + | [] -> () in + print (snd (Trans.apply print_decls task)); + pp_print_flush fmt () + +let () = register_printer "smtv2" print_task + ~desc:"Printer@ for@ the@ SMTlib@ version@ 2@ format." diff --git a/src/printer/why3printer.ml b/src/printer/why3printer.ml index 9f83356386792e758353344fe7ffba3b5cd2f74d..6d1d46df32b6c784685e207c8180107832be136d 100644 --- a/src/printer/why3printer.ml +++ b/src/printer/why3printer.ml @@ -377,23 +377,12 @@ let print_tdecl fmt td = match td.td_node with fprintf fmt "@[(* meta %s %a *)@]@\n@\n" m.meta_name (print_list comma print_meta_arg) al -(* -let print_task_old _env pr thpr _blacklist ?old:_ fmt task = - forget_all (); - print_prelude fmt pr; - print_th_prelude task fmt thpr; - info := { info_syn = get_syntax_map task }; - fprintf fmt "theory Task@\n%a@\nend@." - (print_list nothing print_tdecl) (Task.task_tdecls task) - -let () = register_printer "why3old" print_task_old ~desc:"" -*) - let print_tdecls = - let print sm fmt td = - info := { info_syn = sm }; - print_tdecl fmt td in - Printer.sprint_tdecls print + let print_tdecl sm fmt td = + info := {info_syn = sm}; print_tdecl fmt td; sm, [] in + let print_tdecl = Printer.sprint_tdecl print_tdecl in + let print_tdecl task acc = print_tdecl task.Task.task_decl acc in + Discriminate.on_syntax_map (fun sm -> Trans.fold print_tdecl (sm,[])) let print_task _env pr thpr _blacklist ?old:_ fmt task = (* In trans-based p-printing [forget_all] IST STRENG VERBOTEN *) @@ -401,10 +390,11 @@ let print_task _env pr thpr _blacklist ?old:_ fmt task = print_prelude fmt pr; fprintf fmt "theory Task@\n"; print_th_prelude task fmt thpr; - fprintf fmt "%a@\nend@." - (print_list nothing string) - (List.rev (Trans.apply print_tdecls task)) + let rec print = function + | x :: r -> print r; Pp.string fmt x + | [] -> () in + print (snd (Trans.apply print_tdecls task)); + fprintf fmt "end@." let () = register_printer "why3" print_task - ~desc:"Printer@ for@ the@ logical@ format@ of@ Why3.@ \ - Used@ for@ debugging." + ~desc:"Printer@ for@ the@ logical@ format@ of@ Why3.@ Used@ for@ debugging." diff --git a/src/printer/yices.ml b/src/printer/yices.ml index a6cc08db681da774403d0d7162efd5818189f8a0..38ce6f5a8af957903997040706c2b450444c2bc2 100644 --- a/src/printer/yices.ml +++ b/src/printer/yices.ml @@ -52,56 +52,38 @@ let ident_printer = let print_ident fmt id = fprintf fmt "%s" (id_unique ident_printer id) -(** type *) type info = { - info_syn : syntax_map; - complex_type : ty Hty.t; + info_syn : syntax_map; + complex_type : ty Mty.t ref; + urg_output : string list ref; } -let rec print_type info fmt ty = match ty.ty_node with - | Tyvar _ -> unsupported "yices: you must encode polymorphism" - | Tyapp (ts, []) -> begin match query_syntax info.info_syn ts.ts_name with - | Some s -> syntax_arguments s (print_type info) fmt [] - | None -> fprintf fmt "%a" print_ident ts.ts_name - end - | Tyapp (ts, l) -> - begin match query_syntax info.info_syn ts.ts_name with - | Some s -> syntax_arguments s (print_type info) fmt l - | None -> print_type info fmt (Hty.find info.complex_type ty) - end - -(* and print_tyapp info fmt = function *) -(* | [] -> () *) -(* | [ty] -> fprintf fmt "%a " (print_type info) ty *) -(* | tl -> fprintf fmt "(%a) " (print_list comma (print_type info)) tl *) +(** type *) +let complex_type = Wty.memoize 3 (fun ty -> + let s = Pp.string_of_wnl Pretty.print_ty ty in + create_tysymbol (id_fresh s) [] None) -let rec iter_complex_type info fmt () ty = match ty.ty_node with - | Tyvar _ -> unsupported "yices: you must encode polymorphism" - | Tyapp (_, []) -> () +let rec print_type info fmt ty = match ty.ty_node with + | Tyvar _ -> unsupported "cvc3: you must encode the polymorphism" | Tyapp (ts, l) -> - begin match query_syntax info.info_syn ts.ts_name with - | Some _ -> List.iter (iter_complex_type info fmt ()) l - | None when not (Hty.mem info.complex_type ty) -> - let id = id_fresh (Pp.string_of_wnl Pretty.print_ty ty) in - let ts = create_tysymbol id [] None in - let cty = ty_app ts [] in - fprintf fmt "(define-type %a)@." - print_ident ts.ts_name; - Hty.add info.complex_type ty cty - | None -> () - end - -let find_complex_type info fmt f = - t_ty_fold (iter_complex_type info fmt) () f - -let find_complex_type_expr info fmt f = - TermTF.t_selecti - (t_ty_fold (iter_complex_type info fmt)) - (t_ty_fold (iter_complex_type info fmt)) - () f + begin match query_syntax info.info_syn ts.ts_name, l with + | Some s, _ -> syntax_arguments s (print_type info) fmt l + | None, [] -> fprintf fmt "%a" print_ident ts.ts_name + | None, _ -> + begin match Mty.find_opt ty !(info.complex_type) with + | Some ty -> print_type info fmt ty + | None -> + let ts = complex_type ty in let cty = ty_app ts [] in + let us = sprintf + "(define-type %a)@\n@\n" print_ident ts.ts_name in + info.complex_type := Mty.add ty cty !(info.complex_type); + info.urg_output := us :: !(info.urg_output); + print_type info fmt cty + end + end -let print_type info fmt = - catch_unsupportedType (print_type info fmt) +let print_type info fmt ty = try print_type info fmt ty + with Unsupported s -> raise (UnsupportedType (ty,s)) let print_type_value info fmt = function | None -> fprintf fmt "bool" @@ -175,20 +157,13 @@ and print_fmla info fmt f = match f.t_node with end end | Tquant (q, fq) -> let q = match q with Tforall -> "forall" | Texists -> "exists" in - let vl, tl, f = t_open_quant fq in + let vl, _tl, f = t_open_quant fq in (* TODO trigger dépend des capacités du prover : 2 printers? smtwithtriggers/smtstrict *) - if true (*tl = []*) then - fprintf fmt "@[(%s@ (%a)@ %a)@]" - q - (print_var_list info) vl - (print_fmla info) f - else - fprintf fmt "@[(%s@ (%a)%a@ %a)@]" - q - (print_var_list info) vl - (print_triggers info) tl - (print_fmla info) f; + fprintf fmt "@[(%s@ (%a)@ %a)@]" + q + (print_var_list info) vl + (print_fmla info) f; List.iter forget_var vl | Tbinop (Tand, f1, f2) -> fprintf fmt "@[(and %a@ %a)@]" (print_fmla info) f1 (print_fmla info) f2 @@ -219,6 +194,7 @@ and print_fmla info fmt f = match f.t_node with "yices: you must eliminate match" | Tvar _ | Tconst _ | Teps _ -> raise (FmlaExpected f) +(* and print_expr info fmt = TermTF.t_select (print_term info fmt) (print_fmla info fmt) @@ -232,12 +208,12 @@ and print_triggers info fmt = function let print_logic_binder info fmt v = fprintf fmt "%a: %a" print_ident v.vs_name (print_type info) v.vs_ty +*) let print_type_decl info fmt ts = - if Mid.mem ts.ts_name info.info_syn then false else - if ts.ts_args = [] then - (fprintf fmt "(define-type %a)" print_ident ts.ts_name; true) - else false + if ts.ts_args = [] && ts.ts_def = None then + if not (Mid.mem ts.ts_name info.info_syn) then + fprintf fmt "(define-type %a)@\n@\n" print_ident ts.ts_name let print_data_decl _info fmt = function | ts, csl (* monomorphic enumeration *) @@ -249,88 +225,69 @@ let print_data_decl _info fmt = function unsupported "yices: algebraic types are not supported" let print_data_decl info fmt (ts, _ as d) = - if Mid.mem ts.ts_name info.info_syn then false - else begin print_data_decl info fmt d; true end + if not (Mid.mem ts.ts_name info.info_syn) then + print_data_decl info fmt d let print_param_decl info fmt ls = - List.iter (iter_complex_type info fmt ()) ls.ls_args; - Opt.iter (iter_complex_type info fmt ()) ls.ls_value; match ls.ls_args with | [] -> - fprintf fmt "@[(define %a::%a)@]@\n" + fprintf fmt "@[(define %a::%a)@]@\n@\n" print_ident ls.ls_name (print_type_value info) ls.ls_value | _ -> - fprintf fmt "@[(define %a::(-> %a %a))@]@\n" + fprintf fmt "@[(define %a::(-> %a %a))@]@\n@\n" print_ident ls.ls_name (print_list space (print_type info)) ls.ls_args (print_type_value info) ls.ls_value let print_param_decl info fmt ls = - if Mid.mem ls.ls_name info.info_syn then - false else (print_param_decl info fmt ls; true) + if not (Mid.mem ls.ls_name info.info_syn) then + print_param_decl info fmt ls let print_decl info fmt d = match d.d_node with | Dtype ts -> print_type_decl info fmt ts | Ddata dl -> - print_list_opt nothing (print_data_decl info) fmt dl + print_list nothing (print_data_decl info) fmt dl | Dparam ls -> print_param_decl info fmt ls | Dlogic _ -> unsupportedDecl d "yices: function and predicate definitions are not supported" | Dind _ -> unsupportedDecl d "yices: inductive definitions are not supported" - | Dprop (Paxiom, pr, _) when Mid.mem pr.pr_name info.info_syn -> false + | Dprop (Paxiom, pr, _) when Mid.mem pr.pr_name info.info_syn -> () | Dprop (Paxiom, pr, f) -> - find_complex_type info fmt f; - fprintf fmt "@[;; %s@\n(assert@ %a);@]@\n" - pr.pr_name.id_string - (print_fmla info) f; true + fprintf fmt "@[;; %s@\n(assert@ %a);@]@\n@\n" + pr.pr_name.id_string (print_fmla info) f | Dprop (Pgoal, pr, f) -> - find_complex_type info fmt f; fprintf fmt "@[(assert@\n"; fprintf fmt "@[;; %a@]@\n" print_ident pr.pr_name; (match pr.pr_name.id_loc with - | None -> () - | Some loc -> fprintf fmt " @[;; %a@]@\n" - Loc.gen_report_position loc); - fprintf fmt " @[(not %a)@])@]@\n(check)" (print_fmla info) f; - true + | Some loc -> fprintf fmt " @[;; %a@]@\n" Loc.gen_report_position loc + | None -> ()); + fprintf fmt " @[(not %a)@])@]@\n(check)@\n" (print_fmla info) f | Dprop ((Plemma|Pskip), _, _) -> assert false -let print_decl info fmt = catch_unsupportedDecl (print_decl info fmt) +let print_decls = + let print_decl (sm,ct) fmt d = + let info = {info_syn = sm; complex_type = ref ct; urg_output = ref []} in + try print_decl info fmt d; (sm, !(info.complex_type)), !(info.urg_output) + with Unsupported s -> raise (UnsupportedDecl (d,s)) in + let print_decl = Printer.sprint_decl print_decl in + let print_decl task acc = print_decl task.Task.task_decl acc in + Discriminate.on_syntax_map (fun sm -> + Trans.fold print_decl ((sm,Mty.empty),[])) -let distingued = - let dist_syntax mls = function - | [MAls ls;MAstr s] -> Mls.add ls s mls - | _ -> assert false in - let dist_dist syntax mls = function - | [MAls ls;MAls lsdis] -> - begin try - Mid.add lsdis.ls_name (Mls.find ls syntax) mls - with Not_found -> mls end - | _ -> assert false in - Trans.on_meta meta_syntax_logic (fun syntax -> - let syntax = List.fold_left dist_syntax Mls.empty syntax in - Trans.on_meta Discriminate.meta_lsinst (fun dis -> - let dis2 = List.fold_left (dist_dist syntax) Mid.empty dis in - Trans.return dis2)) - -let print_task pr thpr _blacklist fmt task = +let print_task _env pr thpr _blacklist ?old:_ fmt task = + (* In trans-based p-printing [forget_all] is a no-no *) + (* forget_all ident_printer; *) print_prelude fmt pr; print_th_prelude task fmt thpr; - let info = { - info_syn = Mid.union (fun _ _ s -> Some s) - (get_syntax_map task) (Trans.apply distingued task); - complex_type = Hty.create 5; - } - in - let decls = Task.task_decls task in - ignore (print_list_opt (add_flush newline2) (print_decl info) fmt decls) + let rec print = function + | x :: r -> print r; Pp.string fmt x + | [] -> () in + print (snd (Trans.apply print_decls task)); + pp_print_flush fmt () -let () = register_printer "yices" - (fun _env pr thpr blacklist ?old:_ fmt task -> - forget_all ident_printer; - print_task pr thpr blacklist fmt task) +let () = register_printer "yices" print_task ~desc:"Printer@ for@ the@ Yices@ theorem@ prover version 1." diff --git a/src/session/session_scheduler.ml b/src/session/session_scheduler.ml index 45eb9ae07a9adbeec6760de292e2e66ec8dd8f78..ab2651f9d1198b52145e6db13ce98b50732ee82f 100644 --- a/src/session/session_scheduler.ml +++ b/src/session/session_scheduler.ml @@ -250,7 +250,7 @@ let idle_handler t = in Queue.push (callback,pre_call) t.proof_attempts_queue; run_timeout_handler t - with e -> + with e when not (Debug.test_flag Debug.stack_trace) -> Format.eprintf "@[Exception raise in Session.idle_handler:@ \ %a@.@]" Exn_printer.exn_printer e; @@ -263,7 +263,7 @@ let idle_handler t = t.idle_handler_activated <- false; dprintf debug "[Sched] idle_handler stopped@."; false - | e -> + | e when not (Debug.test_flag Debug.stack_trace) -> Format.eprintf "@[Exception raise in Session.idle_handler:@ %a@.@]" Exn_printer.exn_printer e; eprintf "Session.idle_handler stopped@."; diff --git a/src/session/termcode.ml b/src/session/termcode.ml index a4dcdee9d0ed1e1e41bf4c0bafa5fce3dc2d9ca0..dde0aae4c606a3d6e08c778abc88a453ededc8d0 100644 --- a/src/session/termcode.ml +++ b/src/session/termcode.ml @@ -61,7 +61,9 @@ let debug = Debug.register_info_flag "session_pairing" ~desc:"Print@ debugging@ messages@ about@ reconstruction@ of@ \ session@ trees@ after@ modification@ of@ source@ files." -let current_shape_version = 3 +let current_shape_version = 4 + +type shape_version = SV1 | SV2 | SV3 (* similarity code of terms, or of "shapes" @@ -138,32 +140,29 @@ let rec t_shape ~version ~(push:string->'a->'a) c m (acc:'a) t : 'a = l | Tif (f,t1,t2) -> begin match version with - | 1 | 2 -> fn (fn (fn (push tag_if acc) f) t1) t2 - | 3 -> fn (fn (fn (push tag_if acc) t2) t1) f - | _ -> assert false + | SV1 | SV2 -> fn (fn (fn (push tag_if acc) f) t1) t2 + | SV3 -> fn (fn (fn (push tag_if acc) t2) t1) f end | Tcase (t1,bl) -> let br_shape acc b = let p,t2 = t_open_branch b in match version with - | 1 | 2 -> + | SV1 | SV2 -> let acc = pat_shape ~push c m acc p in let m = pat_rename_alpha c m p in t_shape ~version ~push c m acc t2 - | 3 -> + | SV3 -> let m1 = pat_rename_alpha c m p in let acc = t_shape ~version ~push c m1 acc t2 in pat_shape ~push c m acc p - | _ -> assert false in begin match version with - | 1 | 2 -> + | SV1 | SV2 -> List.fold_left br_shape (fn (push tag_case acc) t1) bl - | 3 -> + | SV3 -> let acc = push tag_case acc in let acc = List.fold_left br_shape acc bl in fn acc t1 - | _ -> assert false end | Teps b -> let u,f = t_open_bound b in @@ -197,18 +196,16 @@ let rec t_shape ~version ~(push:string->'a->'a) c m (acc:'a) t : 'a = let m = vs_rename_alpha c m u in begin match version with - | 1 -> + | SV1 -> t_shape ~version ~push c m (fn (push tag_let acc) t1) t2 - | 2 | 3 -> + | SV2 | SV3 -> (* t2 first, intentionally *) fn (push tag_let (t_shape ~version ~push c m acc t2)) t1 - | _ -> assert false end | Tnot f -> begin match version with - | 1 | 2 -> push tag_not (fn acc f) - | 3 -> fn (push tag_not acc) f - | _ -> assert false + | SV1 | SV2 -> push tag_not (fn acc f) + | SV3 -> fn (push tag_not acc) f end | Ttrue -> push tag_true acc | Tfalse -> push tag_false acc @@ -221,20 +218,26 @@ let t_shape_buf ?(version=current_shape_version) t = Buffer.contents b *) -let t_shape_task ?(version=current_shape_version) t = +let t_shape_task ~version t = let b = Buffer.create 17 in let push t () = Buffer.add_string b t in begin match version with - | 1 | 2 -> () - | 3 -> + | SV1 | SV2 -> () + | SV3 -> let _, expl, _ = goal_expl_task ~root:false t in Opt.iter (Buffer.add_string b) expl - | _ -> assert false end; let f = Task.task_goal_fmla t in let () = t_shape ~version ~push (ref (-1)) Mvs.empty () f in Buffer.contents b +let t_shape_task ?(version=current_shape_version) t = + let version = match version with + | 1 -> SV1 | 2 -> SV2 | 3 | 4 -> SV3 + | _ -> assert false + in + t_shape_task ~version t + (* Checksums *) type checksum = string @@ -244,16 +247,19 @@ let checksum_of_string x = x let equal_checksum x y = (x : checksum) = y let dumb_checksum = "" +type checksum_version = CV1 | CV2 + module Checksum = struct - let char = Buffer.add_char - let int b i = char b 'i'; Buffer.add_string b (string_of_int i) - let string b s = - char b '"'; Buffer.add_string b (String.escaped s); char b '"' + let char (_,_,_,buf) c = Buffer.add_char buf c + let int (_,_,_,buf as b) i = + char b 'i'; Buffer.add_string buf (string_of_int i) + let string (_,_,_,buf as b) s = + char b '"'; Buffer.add_string buf (String.escaped s); char b '"' let option e b = function None -> char b 'n' | Some x -> char b 's'; e b x let list e b l = char b '['; List.iter (e b) l; char b ']' - let ident, clear_ident = + let ident_v1, clear_ident_v1 = let hident = Ident.Hid.create 17 in let c = ref 0 in (fun b id -> @@ -261,6 +267,17 @@ module Checksum = struct with Not_found -> incr c; Ident.Hid.add hident id !c; !c)), (fun () -> Ident.Hid.clear hident; c := 0) + let ident_v2 (_,c,m,_ as b) id = + let i = match Ident.Mid.find_opt id !m with + | Some i -> i + | None -> incr c; m := Ident.Mid.add id !c !m; !c + in + int b i + + let ident (v,_,_,_ as b) id = match v with + | CV1 -> ident_v1 b id + | CV2 -> ident_v2 b id + let const b c = let buf = Buffer.create 17 in Format.bprintf buf "%a" Pretty.print_const c; @@ -272,8 +289,9 @@ module Checksum = struct | Ty.Tyvar tv -> char b 'v'; tvsymbol b tv | Ty.Tyapp (ts, tyl) -> char b 'a'; ident b ts.Ty.ts_name; list ty b tyl - (* variable: the type, but not the name (we want alpha-equivalence) *) - let vsymbol b vs = ty b vs.vs_ty + let vsymbol (v,_,_,_ as b) vs = match v with + | CV1 -> ty b vs.vs_ty + | CV2 -> ident b vs.vs_name; ty b vs.vs_ty (* start: _ V ident a o *) let rec pat b p = match p.pat_node with @@ -395,17 +413,52 @@ module Checksum = struct char b 'C'; ident b th.Theory.th_name; list string b th.Theory.th_path | Theory.Meta (m, mal) -> char b 'M'; meta b m; list meta_arg b mal - let task t = + let task_v1 = + let c = ref 0 in + let m = ref Ident.Mid.empty in let b = Buffer.create 8192 in - Task.task_iter (tdecl b) t; - clear_ident (); - let s = Buffer.contents b in - Digest.to_hex (Digest.string s) - + fun t -> + Task.task_iter (tdecl (CV1,c,m,b)) t; + clear_ident_v1 (); + let dnew = Digest.string (Buffer.contents b) in + Buffer.clear b; + Digest.to_hex dnew + + let task_v2 = + let c = ref 0 in + let m = ref Ident.Mid.empty in + let b = Buffer.create 8192 in + let task_hd t (cold,mold,dold) = + c := cold; + m := mold; + tdecl (CV2,c,m,b) t.Task.task_decl; + Buffer.add_string b (Digest.to_hex dold); + let dnew = Digest.string (Buffer.contents b) in + Buffer.clear b; + let mnew = match t.Task.task_decl.Theory.td_node with + | Theory.Decl { Decl.d_news = s } -> + Ident.Sid.fold (fun id a -> + Ident.Mid.add id (Ident.Mid.find id !m) a) s mold + | _ -> !m in + !c, mnew, dnew + in + let tr = Trans.fold task_hd (0, Ident.Mid.empty, Digest.string "") in + fun t -> + let _,_,dnew = Trans.apply tr t in + Digest.to_hex dnew + + let task ~version t = match version with + | CV1 -> task_v1 t + | CV2 -> task_v2 t end -let task_checksum ?(version=0) t = ignore version; Checksum.task t - +let task_checksum ?(version=current_shape_version) t = + let version = match version with + | 1 | 2 | 3 -> CV1 + | 4 -> CV2 + | _ -> assert false + in + Checksum.task ~version t (*************************************************************) (* Pairing of new and old subgoals *) diff --git a/src/transform/abstraction.ml b/src/transform/abstraction.ml index e3b22774a277c0c7d3ac08ee311108b5d3c5e0f5..b0425fc53d89b25c718539cff94b3d10a9b18695 100644 --- a/src/transform/abstraction.ml +++ b/src/transform/abstraction.ml @@ -15,7 +15,7 @@ open Term open Decl let abstraction (keep : lsymbol -> bool) = - let term_table = Hterm_alpha.create 257 in + let term_table = Hterm.create 257 in let extra_decls = ref [] in let rec abstract t : term = @@ -26,10 +26,10 @@ let abstraction (keep : lsymbol -> bool) = | Tnot _ | Tbinop _ -> t_map abstract t | _ -> - let (ls, tabs) = try Hterm_alpha.find term_table t with Not_found -> + let (ls, tabs) = try Hterm.find term_table t with Not_found -> let ls = create_lsymbol (id_fresh "abstr") [] t.t_ty in let tabs = t_app ls [] t.t_ty in - Hterm_alpha.add term_table t (ls, tabs); + Hterm.add term_table t (ls, tabs); ls, tabs in extra_decls := ls :: !extra_decls; tabs in diff --git a/src/transform/close_epsilon.ml b/src/transform/close_epsilon.ml index 23bdeea88cf8f0d1737a0b948c35ea6e07a0e004..f867149c33754bc617883af808acbf000f864870 100644 --- a/src/transform/close_epsilon.ml +++ b/src/transform/close_epsilon.ml @@ -46,7 +46,7 @@ let is_lambda t = destruct_lambda t <> LNone let rec rewriteT t = match t.t_node with | Teps fb when is_lambda t -> - let fv = Mvs.keys t.t_vars in + let fv = Mvs.keys (t_vars t) in let x, f = t_open_bound fb in let f = rewriteF f in if fv = [] then t_eps_close x f diff --git a/src/transform/discriminate.ml b/src/transform/discriminate.ml index 4f830e06a076ea1fff9a518ca0b19c8f924fdc5e..9d8e53fb9a36a27ca811f6480d778ec57182b318 100644 --- a/src/transform/discriminate.ml +++ b/src/transform/discriminate.ml @@ -73,6 +73,17 @@ module Lsmap = struct instantié. Un tag sur un logique polymorphe doit être un tag sur toute la famille de fonctions *) + let ls_inst = Wls.memoize 3 (fun ls -> + let m = ref Mtyl.empty in + fun tyl tyv -> + let l = oty_cons tyl tyv in + match Mtyl.find_opt l !m with + | Some ls -> ls + | None -> + let nls = create_lsymbol (id_clone ls.ls_name) tyl tyv in + m := Mtyl.add l nls !m; + nls) + type t = lsymbol Mtyl.t Mls.t let empty = Mls.empty @@ -81,9 +92,8 @@ module Lsmap = struct if ls_equal ls ps_equ then lsmap else if not (List.for_all Ty.ty_closed (oty_cons tyl tyv)) then lsmap else let newls = function - | None -> Some (create_lsymbol (id_clone ls.ls_name) tyl tyv) - | nls -> nls - in + | None -> Some (ls_inst ls tyl tyv) + | nls -> nls in let insts = Mls.find_def Mtyl.empty ls lsmap in Mls.add ls (Mtyl.change newls (oty_cons tyl tyv) insts) lsmap @@ -295,3 +305,22 @@ let discriminate env = Trans.seq [ let () = Trans.register_env_transform "discriminate" discriminate ~desc:"Generate@ monomorphic@ type@ instances@ of@ function@ and@ \ predicate@ symbols@ and@ monomorphize@ task@ premises." + +let on_lsinst fn = + let add_ls acc = function + | [MAls ls; MAls nls] -> Mls.add nls ls acc + | _ -> assert false in + Trans.on_meta meta_lsinst (fun dls -> + fn (List.fold_left add_ls Mls.empty dls)) + +let on_syntax_map fn = + let add_ls sm0 sm = function + | [MAls ls; MAls nls] -> + begin match Mid.find_opt ls.ls_name sm0 with + | Some s -> Mid.add nls.ls_name s sm + | None -> sm + end + | _ -> assert false in + Printer.on_syntax_map (fun sm0 -> + Trans.on_meta meta_lsinst (fun dls -> + fn (List.fold_left (fun sm dl -> add_ls sm0 sm dl) sm0 dls))) diff --git a/src/transform/discriminate.mli b/src/transform/discriminate.mli index 13f96c4cca885763d99092ee3c8ae20302b71398..3a24f273c0cb3848b32e07c1c84991ec6543eaaa 100644 --- a/src/transform/discriminate.mli +++ b/src/transform/discriminate.mli @@ -22,3 +22,6 @@ end val ft_select_inst : (Env.env,Ty.Sty.t) Trans.flag_trans val ft_select_lskept : (Env.env,Term.Sls.t) Trans.flag_trans val ft_select_lsinst : (Env.env,Lsmap.t) Trans.flag_trans + +val on_lsinst : (Term.lsymbol Term.Mls.t -> 'a Trans.trans) -> 'a Trans.trans +val on_syntax_map : (Printer.syntax_map -> 'a Trans.trans) -> 'a Trans.trans diff --git a/src/transform/eliminate_algebraic.ml b/src/transform/eliminate_algebraic.ml index e57f3cfb3c33e861db2d13a0ff3c96484997f287..df47371a1a9f08d640bc384fe9158cb4877bc643 100644 --- a/src/transform/eliminate_algebraic.ml +++ b/src/transform/eliminate_algebraic.ml @@ -132,7 +132,7 @@ let rec rewriteT kn state t = match t.t_node with and rewriteF kn state av sign f = match f.t_node with | Tcase (t1,bl) -> let t1 = rewriteT kn state t1 in - let av' = Mvs.set_diff av t1.t_vars in + let av' = Mvs.set_diff av (t_vars t1) in let mk_br (w,m) br = let (p,e) = t_open_branch br in let e = rewriteF kn state av' sign e in @@ -182,7 +182,7 @@ and rewriteF kn state av sign f = match f.t_node with TermTF.t_map_sign (Util.const (rewriteT kn state)) (rewriteF kn state av) sign f | Tlet (t1, _) -> - let av = Mvs.set_diff av t1.t_vars in + let av = Mvs.set_diff av (t_vars t1) in TermTF.t_map_sign (Util.const (rewriteT kn state)) (rewriteF kn state av) sign f | _ -> diff --git a/src/transform/encoding_twin.ml b/src/transform/encoding_twin.ml index 29982ad07043b2988b8b71518bbe5e939fd15c6b..c70f7669709d38b404f44aa3dad3b5b21f7ffc3e 100644 --- a/src/transform/encoding_twin.ml +++ b/src/transform/encoding_twin.ml @@ -15,7 +15,7 @@ open Ty open Term open Decl -let make_pont ty () = +let make_pont = Wty.memoize 3 (fun ty -> let t2tb = let t2tb_name = "t2tb" in let t2tb_id = Libencoding.id_unprotected t2tb_name in @@ -44,7 +44,7 @@ let make_pont ty () = let ax = t_forall_close [x_vs] [[t2tb_tb2t_x]] eq in let pr = create_prsymbol (id_fresh "BridgeR") in create_prop_decl Paxiom pr ax in - t2tb, tb2t, [t2tb_def; tb2t_def; bridge_l; bridge_r] + t2tb, tb2t, [t2tb_def; tb2t_def; bridge_l; bridge_r]) let seen = Hty.create 7 @@ -109,6 +109,6 @@ let decl tenv d = add_decls tenv decls let t = Trans.on_tagged_ty Libencoding.meta_kept (fun s -> - Trans.decl (decl (Mty.mapi make_pont s)) None) + Trans.decl (decl (Mty.mapi (fun ty () -> make_pont ty) s)) None) let () = Hstr.replace Encoding.ft_enco_kept "twin" (Util.const t) diff --git a/src/transform/inlining.ml b/src/transform/inlining.ml index 5abaec02b87d5c1c6d379fb18e1c33a12b237902..6675015e9bab43f947437c4159b8e7eddb1d28f1 100644 --- a/src/transform/inlining.ml +++ b/src/transform/inlining.ml @@ -102,7 +102,7 @@ let trivial tl = let add vs t = match t.t_node with | Tvar v when Mvs.mem v vs -> raise Util.FoldSkip | Tvar v -> Svs.add v vs - | _ when Mvs.is_empty t.t_vars -> vs + | _ when t_closed t -> vs | _ -> raise Util.FoldSkip in try ignore (List.fold_left add Svs.empty tl); true diff --git a/src/transform/libencoding.ml b/src/transform/libencoding.ml index 9f26957ee9ba25f718c375cec92edf6162e0f21a..bb4038641e6928830a772ea5abe1b065e51b36e4 100644 --- a/src/transform/libencoding.ml +++ b/src/transform/libencoding.ml @@ -118,9 +118,8 @@ let t_monomorph ty_base kept lsmap consts vmap t = let rec t_mono vmap t = t_label_copy t (match t.t_node with | Tvar v -> Mvs.find v vmap - | Tconst _ when ty_equal (t_type t) ty_base -> - t - | Tconst _ when Sty.mem (t_type t) kept -> + | Tconst _ when ty_equal (t_type t) ty_base || + Sty.mem (t_type t) kept -> t | Tconst _ -> let ls = ls_of_const ty_base t in @@ -221,11 +220,14 @@ let monomorphise_task = Trans.decl decl (Task.add_decl None d_ts_base))) (* replace type variables in a goal with fresh type constants *) +let ts_of_tv = Htv.memo 63 (fun tv -> + create_tysymbol (id_clone tv.tv_name) [] None) + let monomorphise_goal = Trans.goal (fun pr f -> let stv = t_ty_freevars Stv.empty f in if Stv.is_empty stv then [create_prop_decl Pgoal pr f] else let mty,ltv = Stv.fold (fun tv (mty,ltv) -> - let ts = create_tysymbol (id_clone tv.tv_name) [] None in + let ts = ts_of_tv tv in Mtv.add tv (ty_app ts []) mty, ts::ltv) stv (Mtv.empty,[]) in let f = t_ty_subst mty Mvs.empty f in List.fold_left diff --git a/src/transform/lift_epsilon.ml b/src/transform/lift_epsilon.ml index feb5d84a4d960fc00d21c309ef7060ed5f345a6e..5da95575019d03d9258ecf69ed07c68762c4c77c 100644 --- a/src/transform/lift_epsilon.ml +++ b/src/transform/lift_epsilon.ml @@ -23,7 +23,7 @@ let lift kind = let rec term acc t = match t.t_node with | Teps fb -> - let fv = Mvs.keys t.t_vars in + let fv = Mvs.keys (t_vars t) in let x, f = t_open_bound fb in let acc, f = form acc f in let tys = List.map (fun x -> x.vs_ty) fv in diff --git a/src/transform/simplify_array.ml b/src/transform/simplify_array.ml index 0827739113903d81a3fc538e54a1ae4489e00605..6e586d668136462570fadc994c1429d102d16e75 100644 --- a/src/transform/simplify_array.ml +++ b/src/transform/simplify_array.ml @@ -33,7 +33,7 @@ let make_rt_rf env = | Tapp (lselect,[{t_node=Tapp(lstore,[_;a1;b])};a2]) when lselect.ls_name == select && lstore.ls_name == store && - t_equal_alpha a1 a2 -> b + t_equal a1 a2 -> b | _ -> t and rf f = TermTF.t_map rt rf f in rt,rf diff --git a/src/transform/simplify_formula.ml b/src/transform/simplify_formula.ml index db5161e2dff2cb8f20107d997a9b63e582d43566..6d8ac34117dbf777700dffa5ebe25a96dd58553a 100644 --- a/src/transform/simplify_formula.ml +++ b/src/transform/simplify_formula.ml @@ -201,7 +201,7 @@ let fmla_cond_subst filter f = for j = 0 to subl - 1 do if j <> i then let (f, s) = subf.(j) in - subf.(j) <- (t_replace_alpha t1 t2 f, s); + subf.(j) <- (t_replace t1 t2 f, s); done in let (f, s) = subf.(i) in match f.t_node with diff --git a/src/whyml/mlw_decl.ml b/src/whyml/mlw_decl.ml index 956c1bb5af99c54a6b43bd8d2ead3cbc2e9d6ca4..18005c6900d86e9b60f7e6174681556ec20a9490 100644 --- a/src/whyml/mlw_decl.ml +++ b/src/whyml/mlw_decl.ml @@ -131,7 +131,7 @@ let create_data_decl tdl = let add_invariant pd its p = if not its.its_inv then invalid_arg "Mlw_decl.add_invariant"; - Mvs.iter (fun vs _ -> raise (Decl.UnboundVar vs)) p.t_vars; + t_v_fold (fun _ vs -> raise (Decl.UnboundVar vs)) () p; let rec add = function | (s, cls, inv) :: tdl when its_equal s its -> check_post (t_type inv) p; diff --git a/src/whyml/mlw_expr.ml b/src/whyml/mlw_expr.ml index 47955e989f106d5eac7a0711d85df5810f7036f1..d1407701229e557a9e80dd4b0551f6ac4ddcb61b 100644 --- a/src/whyml/mlw_expr.ml +++ b/src/whyml/mlw_expr.ml @@ -1006,10 +1006,10 @@ let spec_purify sp = let vs, f = Mlw_ty.open_post sp.c_post in match f.t_node with | Tapp (ps, [{t_node = Tvar us}; t]) - when ls_equal ps ps_equ && vs_equal vs us && not (Mvs.mem vs t.t_vars) -> + when ls_equal ps ps_equ && vs_equal vs us && t_v_occurs vs t = 0 -> t | Tbinop (Tiff, {t_node = Tapp (ps,[{t_node = Tvar us};{t_node = Ttrue}])},f) - when ls_equal ps ps_equ && vs_equal vs us && not (Mvs.mem vs f.t_vars) -> + when ls_equal ps ps_equ && vs_equal vs us && t_v_occurs vs f = 0 -> t_if f t_bool_true t_bool_false | _ -> raise Exit diff --git a/src/whyml/mlw_interp.ml b/src/whyml/mlw_interp.ml index cf841d4d73d26381f7d04b7fdc8da85038fba211..46d330e4716ce693616f0e402db2b28369493261 100644 --- a/src/whyml/mlw_interp.ml +++ b/src/whyml/mlw_interp.ml @@ -162,7 +162,7 @@ let eval_int_rel op _ty ls l = | _ -> assert false let term_equality t1 t2 = - if t_equal_alpha t1 t2 then Some true + if t_equal t1 t2 then Some true else try let i1 = big_int_of_term t1 in diff --git a/src/whyml/mlw_ty.ml b/src/whyml/mlw_ty.ml index d22a943f54a49fbdd1b6bc659e791ca8a1a7e6b7..e3038aa8abf608d6c10a1a085b02c96668bf72af 100644 --- a/src/whyml/mlw_ty.ml +++ b/src/whyml/mlw_ty.ml @@ -800,8 +800,8 @@ let spec_subst sbs c = } let spec_vsset c = - let add f s = Mvs.set_union f.t_vars s in - let s = add c.c_pre c.c_post.t_vars in + let add f s = Mvs.set_union (t_vars f) s in + let s = add c.c_pre (t_vars c.c_post) in let s = Mexn.fold (fun _ f s -> add f s) c.c_xpost s in List.fold_left (fun s (t,_) -> add t s) s c.c_variant @@ -872,7 +872,7 @@ let create_pvsymbol, restore_pv = let pvs_of_vss pvs vss = Mvs.fold (fun vs _ s -> Spv.add (restore_pv vs) s) vss pvs -let t_pvset pvs t = pvs_of_vss pvs t.t_vars +let t_pvset pvs t = pvs_of_vss pvs (t_vars t) let spec_pvset pvs spec = pvs_of_vss pvs (spec_vsset spec) diff --git a/src/whyml/mlw_typing.ml b/src/whyml/mlw_typing.ml index 8a4b27d981d74d3c2010cda1d520268fb0c101ac..810cb5db4240cbebbf819044f39243a4534ed4b0 100644 --- a/src/whyml/mlw_typing.ml +++ b/src/whyml/mlw_typing.ml @@ -76,9 +76,10 @@ let ts_tuple n = Hint.replace ht_tuple n (); ts_tuple n let fs_tuple n = Hint.replace ht_tuple n (); fs_tuple n let check_at f0 = + let fvs0 = t_vars f0 in let rec check f = match f.t_node with | Term.Tapp (ls, _) when ls_equal ls fs_at -> - let d = Mvs.set_diff f.t_vars f0.t_vars in + let d = Mvs.set_diff (t_vars f) fvs0 in if not (Mvs.is_empty d) then errorm ?loc:f.t_loc "locally bound variable %a under `at'" Pretty.print_vs (fst (Mvs.choose d)) @@ -786,7 +787,7 @@ let rec check_reset rvs t = match t.t_node with under `old' in the postcondition" vs.vs_name.id_string | Tapp (ls,_) when ls_equal ls fs_at -> false | Tlet _ | Tcase _ | Teps _ | Tquant _ -> - let rvs = Mvs.set_inter rvs t.t_vars in + let rvs = Mvs.set_inter rvs (t_vars t) in if Mvs.is_empty rvs then false else t_any (check_reset rvs) t | _ -> @@ -1117,7 +1118,7 @@ let rec type_c lenv pvs vars otv (dtyv, dsp) = ignored outside of "let rec" definitions, so WP are not affected. *) let del_pv pv s = Svs.remove pv.pv_vs s in let esvs = Spv.fold del_pv pvs esvs in - let drop _ t s = Mvs.set_diff s t.t_vars in + let drop _ t s = Mvs.set_diff s (t_vars t) in let esvs = drop () spec.c_pre esvs in let esvs = drop () spec.c_post esvs in let esvs = Mexn.fold drop spec.c_xpost esvs in diff --git a/src/whyml/mlw_wp.ml b/src/whyml/mlw_wp.ml index 5f0c3a232b100db00971f4eacb137ca9f2f6eb1d..78a3bae263c9128f6db1a6bcad3f17c05cc8bec2 100644 --- a/src/whyml/mlw_wp.ml +++ b/src/whyml/mlw_wp.ml @@ -152,7 +152,7 @@ let wp_forall vl f = t_forall_close_simp vl [] f let is_equality_for v f = match f.t_node with | Tapp (ps, [{ t_node = Tvar u }; t]) - when ls_equal ps ps_equ && vs_equal u v && not (Mvs.mem v t.t_vars) -> + when ls_equal ps ps_equ && vs_equal u v && t_v_occurs v t = 0 -> Some t | _ -> None @@ -294,7 +294,7 @@ let rec subst_at_now now mvs t = match t.t_node with t_map (subst_at_now now mvs) t | Tlet _ | Tcase _ | Teps _ | Tquant _ -> (* do not open unless necessary *) - let mvs = Mvs.set_inter mvs t.t_vars in + let mvs = Mvs.set_inter mvs (t_vars t) in if Mvs.is_empty mvs then t else t_map (subst_at_now now mvs) t | _ -> @@ -330,7 +330,7 @@ let update_term env (mreg : vsymbol Mreg.t) f = let update vs _ = match update_var env mreg vs with | { t_node = Tvar nv } when vs_equal vs nv -> None | t -> Some t in - let vars = Mvs.mapi_filter update f.t_vars in + let vars = Mvs.mapi_filter update (t_vars f) in (* [vv'] : modified variable -> fresh variable *) let new_var vs _ = mk_var vs.vs_name model2_lab vs.vs_ty in let vv' = Mvs.mapi new_var vars in @@ -345,11 +345,11 @@ let get_single_region_of_var vs = (* look for a variable with a single region equal to [reg] *) let var_of_region reg f = - let test vs _ acc = + let test acc vs = match get_single_region_of_var vs with | Some r when reg_equal r reg -> Some vs | _ -> acc in - Mvs.fold test f.t_vars None + t_v_fold test None f let quantify env regs f = (* mreg : modified region -> vs *) @@ -980,7 +980,7 @@ let wp_let env km th { let_sym = lv; let_expr = e } = let env = mk_env env km th in let q, xq = default_post e.e_vty e.e_effect in let f = wp_expr env e q xq in - let f = wp_forall (Mvs.keys f.t_vars) f in + let f = wp_forall (Mvs.keys (t_vars f)) f in let id = match lv with | LetV pv -> pv.pv_vs.vs_name | LetA ps -> ps.ps_name in @@ -992,7 +992,7 @@ let wp_rec env km th fdl = let add_one th d f = Debug.dprintf debug "wp %s = %a@\n----------------@." d.fun_ps.ps_name.id_string Pretty.print_term f; - let f = wp_forall (Mvs.keys f.t_vars) f in + let f = wp_forall (Mvs.keys (t_vars f)) f in add_wp_decl km d.fun_ps.ps_name f th in List.fold_left2 add_one th fdl fl @@ -1213,7 +1213,7 @@ end = struct t_map (term subst) subterm | Tlet _ | Tcase _ | Teps _ | Tquant _ -> (* do not open unless necessary *) - let mvs = Mvs.set_inter s.now.subst_vars t.t_vars in + let mvs = Mvs.set_inter s.now.subst_vars (t_vars t) in if Mvs.is_empty mvs then t else t_map (term s) t | _ -> @@ -1881,8 +1881,8 @@ and fast_wp_fun_defn env { fun_lambda = l } = let args = List.map (fun pv -> pv.pv_vs) l.l_args in let build_set svs = Mvs.fold (fun x _ acc -> Spv.add (restore_pv x) acc) svs Spv.empty in - let pre_vars = build_set c.c_pre.t_vars in - let post_vars = build_set c.c_post.t_vars in + let pre_vars = build_set (t_vars c.c_pre) in + let post_vars = build_set (t_vars c.c_post) in let all_vars = Spv.union l.l_expr.e_syms.syms_pv pre_vars in let all_vars = Spv.union all_vars post_vars in let prestate = Subst.init all_vars in @@ -1914,7 +1914,7 @@ and fast_wp_fun_defn env { fun_lambda = l } = t_and_simp res.ok (wp_nimplies res.post.ne res.exn ((result, q.ne), xq)) in let f = wp_implies pre f in - let f = wp_forall args (t_forall_close (Mvs.keys f.t_vars) [] f) in + let f = wp_forall args (t_forall_close (Mvs.keys (t_vars f)) [] f) in f and fast_wp_rec_defn env fdl = List.map (fast_wp_fun_defn env) fdl @@ -1923,7 +1923,7 @@ let fast_wp_let env km th { let_sym = lv; let_expr = e } = let env = mk_env env km th in let res = fast_wp_expr env (Subst.init e.e_syms.syms_pv) (result e) e in - let f = wp_forall (Mvs.keys res.ok.t_vars) res.ok in + let f = wp_forall (Mvs.keys (t_vars res.ok)) res.ok in let id = match lv with | LetV pv -> pv.pv_vs.vs_name | LetA ps -> ps.ps_name in @@ -1935,7 +1935,7 @@ let fast_wp_rec env km th fdl = let add_one th d f = Debug.dprintf debug "wp %s = %a@\n----------------@." d.fun_ps.ps_name.id_string Pretty.print_term f; - let f = wp_forall (Mvs.keys f.t_vars) f in + let f = wp_forall (Mvs.keys (t_vars f)) f in add_wp_decl km d.fun_ps.ps_name f th in List.fold_left2 add_one th fdl fl @@ -1973,7 +1973,7 @@ let wp_rec ~wp env kn th fdl = let f = wp_expr env e_void q Mexn.empty in let f = wp_implies spec.c_pre (erase_mark lab f) in let f = wp_forall args (quantify env (wp_fun_regs ps l) f) in - let f = t_forall_close (Mvs.keys f.t_vars) [] f in + let f = t_forall_close (Mvs.keys (t_vars f)) [] f in let lkn = Theory.get_known th in let f = if Debug.test_flag no_track then f else track_values lkn kn f in (*let f = if Debug.test_flag no_eval then f else