# HG changeset patch # User blanchet # Date 1477341727 -7200 # Node ID 6273d4c8325be9e28b18c495f5e5f052e479ed07 # Parent 14571c9e1d5077993f4558a44b2c087c2e3e3b13 added Nunchaku integration diff -r 14571c9e1d50 -r 6273d4c8325b CONTRIBUTORS --- a/CONTRIBUTORS Mon Oct 24 21:14:38 2016 +0200 +++ b/CONTRIBUTORS Mon Oct 24 22:42:07 2016 +0200 @@ -48,6 +48,10 @@ Ported remaining theories of Old_Number_Theory to the new Number_Theory and removed Old_Number_Theory. +* October 2016: Jasmin Blanchette + Integration of Nunchaku model finder. + + Contributions to Isabelle2016 ----------------------------- diff -r 14571c9e1d50 -r 6273d4c8325b NEWS --- a/NEWS Mon Oct 24 21:14:38 2016 +0200 +++ b/NEWS Mon Oct 24 22:42:07 2016 +0200 @@ -910,6 +910,9 @@ * Renamed HOL/Quotient_Examples/FSet.thy to HOL/Quotient_Examples/Quotient_FSet.thy INCOMPATIBILITY. +* The "nunchaku" program integrates the Nunchaku model finder. The tool +is experimental. See ~~/src/HOL/Nunchaku/Nunchaku.thy for details. + *** ML *** diff -r 14571c9e1d50 -r 6273d4c8325b src/HOL/Nunchaku/Nunchaku.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Nunchaku/Nunchaku.thy Mon Oct 24 22:42:07 2016 +0200 @@ -0,0 +1,41 @@ +(* Title: HOL/Nunchaku/Nunchaku.thy + Author: Jasmin Blanchette, Inria Nancy, LORIA, MPII + Copyright 2015, 2016 + +Nunchaku: Yet another counterexample generator for Isabelle/HOL. + +Nunchaku relies on an external program of the same name. The program is still +being actively developed. The sources are available at + + https://github.com/nunchaku-inria +*) + +theory Nunchaku +imports Main +keywords + "nunchaku" :: diag and + "nunchaku_params" :: thy_decl +begin + +consts unreachable :: 'a + +definition The_unsafe :: "('a \ bool) \ 'a" where + "The_unsafe = The" + +definition rmember :: "'a set \ 'a \ bool" where + "rmember A x \ x \ A" + +ML_file "Tools/nunchaku_util.ML" +ML_file "Tools/nunchaku_collect.ML" +ML_file "Tools/nunchaku_problem.ML" +ML_file "Tools/nunchaku_translate.ML" +ML_file "Tools/nunchaku_model.ML" +ML_file "Tools/nunchaku_reconstruct.ML" +ML_file "Tools/nunchaku_display.ML" +ML_file "Tools/nunchaku_tool.ML" +ML_file "Tools/nunchaku.ML" +ML_file "Tools/nunchaku_commands.ML" + +hide_const (open) unreachable The_unsafe rmember + +end diff -r 14571c9e1d50 -r 6273d4c8325b src/HOL/Nunchaku/Tools/nunchaku.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Nunchaku/Tools/nunchaku.ML Mon Oct 24 22:42:07 2016 +0200 @@ -0,0 +1,325 @@ +(* Title: HOL/Nunchaku/Tools/nunchaku.ML + Author: Jasmin Blanchette, Inria Nancy, LORIA, MPII + Copyright 2015, 2016 + +The core of the Nunchaku integration in Isabelle. +*) + +signature NUNCHAKU = +sig + type isa_model = Nunchaku_Reconstruct.isa_model + + datatype mode = Auto_Try | Try | Normal + + type mode_of_operation_params = + {falsify: bool, + assms: bool, + spy: bool, + overlord: bool, + expect: string} + + type scope_of_search_params = + {wfs: ((string * typ) option * bool option) list, + whacks: (term option * bool) list, + cards: (typ option * (int option * int option)) list, + monos: (typ option * bool option) list} + + type output_format_params = + {verbose: bool, + debug: bool, + max_potential: int, + max_genuine: int, + evals: term list, + atomss: (typ option * string list) list} + + type optimization_params = + {specialize: bool, + multithread: bool} + + type timeout_params = + {timeout: Time.time, + wf_timeout: Time.time} + + type params = + {mode_of_operation_params: mode_of_operation_params, + scope_of_search_params: scope_of_search_params, + output_format_params: output_format_params, + optimization_params: optimization_params, + timeout_params: timeout_params} + + val genuineN: string + val quasi_genuineN: string + val potentialN: string + val noneN: string + val unknownN: string + val no_nunchakuN: string + + val run_chaku_on_prop: Proof.state -> params -> mode -> int -> term list -> term -> + string * isa_model option + val run_chaku_on_subgoal: Proof.state -> params -> mode -> int -> string * isa_model option +end; + +structure Nunchaku : NUNCHAKU = +struct + +open Nunchaku_Util; +open Nunchaku_Collect; +open Nunchaku_Problem; +open Nunchaku_Translate; +open Nunchaku_Model; +open Nunchaku_Reconstruct; +open Nunchaku_Display; +open Nunchaku_Tool; + +datatype mode = Auto_Try | Try | Normal; + +type mode_of_operation_params = + {falsify: bool, + assms: bool, + spy: bool, + overlord: bool, + expect: string}; + +type scope_of_search_params = + {wfs: ((string * typ) option * bool option) list, + whacks: (term option * bool) list, + cards: (typ option * (int option * int option)) list, + monos: (typ option * bool option) list}; + +type output_format_params = + {verbose: bool, + debug: bool, + max_potential: int, + max_genuine: int, + evals: term list, + atomss: (typ option * string list) list}; + +type optimization_params = + {specialize: bool, + multithread: bool}; + +type timeout_params = + {timeout: Time.time, + wf_timeout: Time.time}; + +type params = + {mode_of_operation_params: mode_of_operation_params, + scope_of_search_params: scope_of_search_params, + output_format_params: output_format_params, + optimization_params: optimization_params, + timeout_params: timeout_params}; + +val genuineN = "genuine"; +val quasi_genuineN = "quasi_genuine"; +val potentialN = "potential"; +val noneN = "none"; +val unknownN = "unknown"; + +val no_nunchakuN = "no_nunchaku"; + +fun str_of_mode Auto_Try = "Auto_Try" + | str_of_mode Try = "Try" + | str_of_mode Normal = "Normal"; + +fun none_true assigns = forall (curry (op <>) (SOME true) o snd) assigns; + +fun has_lonely_bool_var (@{const Pure.conjunction} $ (@{const Trueprop} $ Free _) $ _) = true + | has_lonely_bool_var _ = false; + +val syntactic_sorts = + @{sort "{default,zero,one,plus,minus,uminus,times,inverse,abs,sgn,ord,equal}"} @ @{sort numeral}; + +fun has_tfree_syntactic_sort (TFree (_, S as _ :: _)) = subset (op =) (S, syntactic_sorts) + | has_tfree_syntactic_sort _ = false; + +val has_syntactic_sorts = exists_type (exists_subtype has_tfree_syntactic_sort); + +(* Give the soft timeout a chance. *) +val timeout_slack = seconds 1.0; + +fun run_chaku_on_prop state + ({mode_of_operation_params = {falsify, assms, spy, overlord, expect}, + scope_of_search_params = {wfs, whacks, cards, monos}, + output_format_params = {verbose, debug, evals, atomss, ...}, + optimization_params = {specialize, ...}, + timeout_params = {timeout, wf_timeout}}) + mode i all_assms subgoal = + let + val ctxt = Proof.context_of state; + + val timer = Timer.startRealTimer () + + val print = writeln; + val print_n = if mode = Normal then writeln else K (); + fun print_v f = if verbose then writeln (f ()) else (); + fun print_d f = if debug then writeln (f ()) else (); + + val das_wort_Model = if falsify then "Countermodel" else "Model"; + val das_wort_model = if falsify then "countermodel" else "model"; + + val tool_params = {overlord = overlord, debug = debug, specialize = specialize, + timeout = timeout}; + + fun run () = + let + val outcome as (outcome_code, _) = + let + val (poly_axioms, isa_problem as {sound, complete, ...}) = + isa_problem_of_subgoal ctxt falsify wfs whacks cards debug wf_timeout evals + (if assms then all_assms else []) subgoal; + val _ = print_d (fn () => "*** Isabelle problem ***\n" ^ + str_of_isa_problem ctxt isa_problem); + val ugly_nun_problem = nun_problem_of_isa ctxt isa_problem; + val _ = print_d (fn () => "*** Ugly Nunchaku problem ***\n" ^ + str_of_nun_problem ugly_nun_problem); + val (nice_nun_problem, pool) = nice_nun_problem ugly_nun_problem; + val _ = print_d (fn () => "*** Nice Nunchaku problem ***\n" ^ + str_of_nun_problem nice_nun_problem); + + fun print_any_hints () = + if has_lonely_bool_var subgoal then + print "Hint: Maybe you forgot a colon after the lemma's name?" + else if has_syntactic_sorts subgoal then + print "Hint: Maybe you forgot a type constraint?" + else + (); + + fun get_isa_model_opt output = + let + val nice_nun_model = nun_model_of_str output; + val _ = print_d (fn () => "*** Nice Nunchaku model ***\n" ^ + str_of_nun_model nice_nun_model); + val ugly_nun_model = ugly_nun_model pool nice_nun_model; + val _ = print_d (fn () => "*** Ugly Nunchaku model ***\n" ^ + str_of_nun_model ugly_nun_model); + + val pat_completes = pat_completes_of_isa_problem isa_problem; + val isa_model = isa_model_of_nun ctxt pat_completes atomss ugly_nun_model; + val _ = print_d (fn () => "*** Isabelle model ***\n" ^ + str_of_isa_model ctxt isa_model); + in + isa_model + end; + + fun isa_model_opt output = + if debug then SOME (get_isa_model_opt output) else try get_isa_model_opt output; + + val model_str = isa_model_opt #> pretty_of_isa_model_opt ctxt #> Pretty.string_of; + + fun unsat_means_theorem () = + null whacks andalso null cards andalso null monos; + + fun unknown () = + (print_n ("No " ^ das_wort_model ^ " can be found \ the problem lies \ + \outside Nunchaku's fragment"); + (unknownN, NONE)); + + fun unsat_or_unknown complete = + if complete then + (print_n ("No " ^ das_wort_model ^ " exists" ^ + (if falsify andalso unsat_means_theorem () then + " \ the goal is a theorem" + else + "")); + (noneN, NONE)) + else + unknown (); + + fun sat_or_maybe_sat sound output = + let val header = if sound then das_wort_Model else "Potential " ^ das_wort_model in + (case (null poly_axioms, none_true wfs) of + (true, true) => + (print (header ^ ":\n" ^ + model_str output); print_any_hints (); + (genuineN, isa_model_opt output)) + | (no_poly, no_wf) => + let + val ignorings = [] + |> not no_poly ? cons "polymorphic axioms" + |> not no_wf ? cons "unchecked well-foundedness"; + in + (print (header ^ " (ignoring " ^ space_implode " and " ignorings ^ "):\n" ^ + model_str output ^ + (if no_poly then + "" + else + "\nIgnored axioms:\n" ^ + cat_lines (map (prefix " " o Syntax.string_of_term ctxt) poly_axioms))); + print_any_hints (); + (quasi_genuineN, isa_model_opt output)) + end) + end; + in + (case solve_nun_problem tool_params nice_nun_problem of + Unsat => unsat_or_unknown complete + | Sat (output, _) => sat_or_maybe_sat sound output + | Unknown NONE => unknown () + | Unknown (SOME (output, _)) => sat_or_maybe_sat false output + | Timeout => (print_n "Time out"; (unknownN, NONE)) + | Nunchaku_Var_Not_Set => + (print_n ("Variable $" ^ nunchaku_env_var ^ " not set"); (unknownN, NONE)) + | Nunchaku_Cannot_Execute => + (print_n "External tool \"nunchaku\" cannot execute"; (unknownN, NONE)) + | Nunchaku_Not_Found => + (print_n "External tool \"nunchaku\" not found"; (unknownN, NONE)) + | CVC4_Cannot_Execute => + (print_n "External tool \"cvc4\" cannot execute"; (unknownN, NONE)) + | CVC4_Not_Found => (print_n "External tool \"cvc4\" not found"; (unknownN, NONE)) + | Unknown_Error (code, msg) => + (print_n ("Unknown error: " ^ msg ^ + (if code = 0 then "" else " (code " ^ string_of_int code ^ ")")); + (unknownN, NONE))) + end + handle + CYCLIC_DEPS () => + (print_n "Cyclic dependencies (or bug in Nunchaku)"; (unknownN, NONE)) + | TOO_DEEP_DEPS () => + (print_n "Too deep dependencies (or bug in Nunchaku)"; (unknownN, NONE)) + | TOO_META t => + (print_n ("Formula too meta for Nunchaku:\n" ^ Syntax.string_of_term ctxt t); + (unknownN, NONE)) + | UNEXPECTED_POLYMORPHISM t => + (print_n ("Unexpected polymorphism in term\n" ^ Syntax.string_of_term ctxt t); + (unknownN, NONE)) + | UNEXPECTED_VAR t => + (print_n ("Unexpected schematic variables in term\n" ^ Syntax.string_of_term ctxt t); + (unknownN, NONE)) + | UNSUPPORTED_FUNC t => + (print_n ("Unsupported low-level constant in problem: " ^ Syntax.string_of_term ctxt t); + (unknownN, NONE)); + in + if expect = "" orelse outcome_code = expect then outcome + else error ("Unexpected outcome: " ^ quote outcome_code) + end; + + val _ = spying spy (fn () => (state, i, "starting " ^ str_of_mode mode ^ " mode")); + + val outcome as (outcome_code, _) = + Timeout.apply (Time.+ (timeout, timeout_slack)) run () + handle Timeout.TIMEOUT _ => (print_n "Time out"; (unknownN, NONE)); + + val _ = print_v (fn () => "Total time: " ^ string_of_time (Timer.checkRealTimer timer)); + + val _ = spying spy (fn () => (state, i, "outcome: " ^ outcome_code)); + in + if expect = "" orelse outcome_code = expect then outcome + else error ("Unexpected outcome: " ^ quote outcome_code) + end; + +fun run_chaku_on_subgoal state params mode i = + let + val ctxt = Proof.context_of state; + val goal = Thm.prop_of (#goal (Proof.raw_goal state)); + in + if Logic.count_prems goal = 0 then + (writeln "No subgoal!"; (noneN, NONE)) + else + let + val subgoal = fst (Logic.goal_params goal i); + val all_assms = map Thm.term_of (Assumption.all_assms_of ctxt); + in + run_chaku_on_prop state params mode i all_assms subgoal + end + end; + +end; diff -r 14571c9e1d50 -r 6273d4c8325b src/HOL/Nunchaku/Tools/nunchaku_collect.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Nunchaku/Tools/nunchaku_collect.ML Mon Oct 24 22:42:07 2016 +0200 @@ -0,0 +1,1109 @@ +(* Title: HOL/Nunchaku/Tools/nunchaku_collect.ML + Author: Jasmin Blanchette, Inria Nancy, LORIA, MPII + Copyright 2015, 2016 + +Collecting of Isabelle/HOL definitions etc. for Nunchaku. +*) + +signature NUNCHAKU_COLLECT = +sig + val dest_co_datatype_case: Proof.context -> string * typ -> (string * typ) list + + type isa_type_spec = + {abs_typ: typ, + rep_typ: typ, + wrt: term, + abs: term, + rep: term} + + type isa_co_data_spec = + {typ: typ, + ctrs: term list} + + type isa_const_spec = + {const: term, + props: term list} + + type isa_rec_spec = + {const: term, + props: term list, + pat_complete: bool} + + type isa_consts_spec = + {consts: term list, + props: term list} + + datatype isa_command = + ITVal of typ * (int option * int option) + | ICopy of isa_type_spec + | IQuotient of isa_type_spec + | ICoData of BNF_Util.fp_kind * isa_co_data_spec list + | IVal of term + | ICoPred of BNF_Util.fp_kind * bool * isa_const_spec list + | IRec of isa_rec_spec list + | ISpec of isa_consts_spec + | IAxiom of term + | IGoal of term + | IEval of term + + type isa_problem = + {commandss: isa_command list list, + sound: bool, + complete: bool} + + exception CYCLIC_DEPS of unit + exception TOO_DEEP_DEPS of unit + exception TOO_META of term + exception UNEXPECTED_POLYMORPHISM of term + exception UNEXPECTED_VAR of term + exception UNSUPPORTED_FUNC of term + + val isa_problem_of_subgoal: Proof.context -> bool -> ((string * typ) option * bool option) list -> + (term option * bool) list -> (typ option * (int option * int option)) list -> bool -> + Time.time -> term list -> term list -> term -> term list * isa_problem + val pat_completes_of_isa_problem: isa_problem -> term list + val str_of_isa_problem: Proof.context -> isa_problem -> string +end; + +structure Nunchaku_Collect : NUNCHAKU_COLLECT = +struct + +open Nunchaku_Util; + +type isa_type_spec = + {abs_typ: typ, + rep_typ: typ, + wrt: term, + abs: term, + rep: term}; + +type isa_co_data_spec = + {typ: typ, + ctrs: term list}; + +type isa_const_spec = + {const: term, + props: term list}; + +type isa_rec_spec = + {const: term, + props: term list, + pat_complete: bool}; + +type isa_consts_spec = + {consts: term list, + props: term list}; + +datatype isa_command = + ITVal of typ * (int option * int option) +| ICopy of isa_type_spec +| IQuotient of isa_type_spec +| ICoData of BNF_Util.fp_kind * isa_co_data_spec list +| IVal of term +| ICoPred of BNF_Util.fp_kind * bool * isa_const_spec list +| IRec of isa_rec_spec list +| ISpec of isa_consts_spec +| IAxiom of term +| IGoal of term +| IEval of term; + +type isa_problem = + {commandss: isa_command list list, + sound: bool, + complete: bool}; + +exception CYCLIC_DEPS of unit; +exception TOO_DEEP_DEPS of unit; +exception TOO_META of term; +exception UNEXPECTED_POLYMORPHISM of term; +exception UNEXPECTED_VAR of term; +exception UNSUPPORTED_FUNC of term; + +fun str_of_and_list str_of_elem = + map str_of_elem #> space_implode ("\nand "); + +val key_of_typ = + let + fun key_of (Type (s, [])) = s + | key_of (Type (s, Ts)) = s ^ "(" ^ commas (map key_of Ts) ^ ")" + | key_of (TFree (s, _)) = s; + in + prefix "y" o key_of + end; + +fun key_of_const ctxt = + let + val thy = Proof_Context.theory_of ctxt; + + fun key_of (Const (x as (s, _))) = + (case Sign.const_typargs thy x of + [] => s + | Ts => s ^ "(" ^ commas (map key_of_typ Ts) ^ ")") + | key_of (Free (s, _)) = s; + in + prefix "t" o key_of + end; + +val add_type_keys = fold_subtypes (insert (op =) o key_of_typ); + +fun add_aterm_keys ctxt t = + if is_Const t orelse is_Free t then insert (op =) (key_of_const ctxt t) else I; + +fun add_keys ctxt t = + fold_aterms (add_aterm_keys ctxt) t + #> fold_types add_type_keys t; + +fun close_form except t = + fold (fn ((s, i), T) => fn t' => + HOLogic.all_const T $ Abs (s, T, abstract_over (Var ((s, i), T), t'))) + (Term.add_vars t [] |> subtract (op =) except) t; + +(* "imp_conjL[symmetric]" is important for inductive predicates with multiple assumptions. *) +val basic_defs = + @{thms Ball_def[abs_def] Bex_def[abs_def] case_bool_if Ex1_def[abs_def] + imp_conjL[symmetric, abs_def] Let_def[abs_def] rmember_def[symmetric, abs_def]}; + +fun unfold_basic_def ctxt = + let val thy = Proof_Context.theory_of ctxt in + Pattern.rewrite_term thy (map (Logic.dest_equals o Thm.prop_of) basic_defs) [] + end; + +val has_polymorphism = exists_type (exists_subtype is_TVar); + +fun whack_term thy whacks = + let + fun whk t = + if triple_lookup (term_match thy o swap) whacks t = SOME true then + Const (@{const_name unreachable}, fastype_of t) + else + (case t of + u $ v => whk u $ whk v + | Abs (s, T, u) => Abs (s, T, whk u) + | _ => t); + in + whk + end; + +fun preprocess_term_basic falsify ctxt whacks t = + let val thy = Proof_Context.theory_of ctxt in + if has_polymorphism t then + raise UNEXPECTED_POLYMORPHISM t + else + t + |> attach_typeS + |> whack_term thy whacks + |> Object_Logic.atomize_term ctxt + |> tap (fn t' => fastype_of t' <> @{typ prop} orelse raise TOO_META t) + |> falsify ? HOLogic.mk_not + |> unfold_basic_def ctxt + end; + +val check_closed = tap (fn t => null (Term.add_vars t []) orelse raise UNEXPECTED_VAR t); + +val preprocess_prop = close_form [] oooo preprocess_term_basic; +val preprocess_closed_term = check_closed ooo preprocess_term_basic false; + +val is_type_builtin = member (op =) [@{type_name bool}, @{type_name fun}]; + +val is_const_builtin = + member (op =) [@{const_name All}, @{const_name conj}, @{const_name disj}, @{const_name Eps}, + @{const_name HOL.eq}, @{const_name Ex}, @{const_name False}, @{const_name If}, + @{const_name implies}, @{const_name Not}, @{const_name The}, @{const_name The_unsafe}, + @{const_name True}]; + +datatype type_classification = Builtin | TVal | Copy | Quotient | Co_Datatype; + +fun classify_type_name ctxt T_name = + if is_type_builtin T_name then + Builtin + else if T_name = @{type_name itself} then + Co_Datatype + else + (case BNF_FP_Def_Sugar.fp_sugar_of ctxt T_name of + SOME _ => Co_Datatype + | NONE => + (case Ctr_Sugar.ctr_sugar_of ctxt T_name of + SOME _ => Co_Datatype + | NONE => + (case Quotient_Info.lookup_quotients ctxt T_name of + SOME _ => Quotient + | NONE => + if T_name = @{type_name set} then + Copy + else + (case Typedef.get_info ctxt T_name of + _ :: _ => Copy + | [] => TVal)))); + +fun fp_kind_of_ctr_sugar_kind Ctr_Sugar.Codatatype = BNF_Util.Greatest_FP + | fp_kind_of_ctr_sugar_kind _ = BNF_Util.Least_FP; + +fun mutual_co_datatypes_of ctxt (T_name, Ts) = + (if T_name = @{type_name itself} then + (BNF_Util.Least_FP, [@{typ "'a itself"}], [[@{const Pure.type ('a)}]]) + else + let + val (fp, ctr_sugars) = + (case BNF_FP_Def_Sugar.fp_sugar_of ctxt T_name of + SOME (fp_sugar as {fp, fp_res = {Ts, ...}, ...}) => + (fp, + (case Ts of + [_] => [fp_sugar] + | _ => map (the o BNF_FP_Def_Sugar.fp_sugar_of ctxt o fst o dest_Type) Ts) + |> map (#ctr_sugar o #fp_ctr_sugar)) + | NONE => + (case Ctr_Sugar.ctr_sugar_of ctxt T_name of + SOME (ctr_sugar as {kind, ...}) => + (* Any freely constructed type that is not a codatatype is considered a datatype. This + is sound (but incomplete) for model finding. *) + (fp_kind_of_ctr_sugar_kind kind, [ctr_sugar]))); + in + (fp, map #T ctr_sugars, map #ctrs ctr_sugars) + end) + |> @{apply 3(2)} (map ((fn Type (s, _) => Type (s, Ts)))) + |> @{apply 3(3)} (map (map (Ctr_Sugar.mk_ctr Ts))); + +fun quotient_of ctxt T_name = + (case Quotient_Info.lookup_quotients ctxt T_name of + SOME {equiv_rel, qtyp, rtyp, quot_thm, ...} => + let val _ $ (_ $ _ $ abs $ rep) = Thm.prop_of quot_thm in + (qtyp, rtyp, equiv_rel, abs, rep) + end); + +fun copy_of ctxt T_name = + if T_name = @{type_name set} then + let + val A = Logic.varifyT_global @{typ 'a}; + val absT = Type (@{type_name set}, [A]); + val repT = A --> HOLogic.boolT; + val wrt = Abs (Name.uu, repT, @{const True}); + val abs = Const (@{const_name Collect}, repT --> absT); + val rep = Const (@{const_name rmember}, absT --> repT); + in + (absT, repT, wrt, abs, rep) + end + else + (case Typedef.get_info ctxt T_name of + (* When several entries are returned, it shouldn't matter much which one we take (according to + Florian Haftmann). The "Logic.varifyT_global" calls are a workaround because these types' + variables sometimes clash with locally fixed type variables. *) + ({abs_type, rep_type, Abs_name, Rep_name, ...}, {Rep, ...}) :: _ => + let + val absT = Logic.varifyT_global abs_type; + val repT = Logic.varifyT_global rep_type; + val wrt = Thm.prop_of Rep + |> HOLogic.dest_Trueprop + |> HOLogic.dest_mem + |> snd; + val abs = Const (Abs_name, repT --> absT); + val rep = Const (Rep_name, absT --> repT); + in + (absT, repT, wrt, abs, rep) + end); + +fun is_co_datatype_ctr ctxt (s, T) = + (case body_type T of + Type (fpT_name, Ts) => + classify_type_name ctxt fpT_name = Co_Datatype andalso + let + val ctrs = + if fpT_name = @{type_name itself} then + [Const (@{const_name Pure.type}, @{typ "'a itself"})] + else + (case BNF_FP_Def_Sugar.fp_sugar_of ctxt fpT_name of + SOME {fp_ctr_sugar = {ctr_sugar = {ctrs, ...}, ...}, ...} => ctrs + | NONE => + (case Ctr_Sugar.ctr_sugar_of ctxt fpT_name of + SOME {ctrs, ...} => ctrs + | _ => [])); + + fun is_right_ctr (t' as Const (s', _)) = + s = s' andalso fastype_of (Ctr_Sugar.mk_ctr Ts t') = T; + in + exists is_right_ctr ctrs + end + | _ => false); + +fun dest_co_datatype_case ctxt (s, T) = + let val thy = Proof_Context.theory_of ctxt in + (case strip_fun_type (Sign.the_const_type thy s) of + (gen_branch_Ts, gen_body_fun_T) => + (case gen_body_fun_T of + Type (@{type_name fun}, [Type (fpT_name, _), _]) => + if classify_type_name ctxt fpT_name = Co_Datatype then + let + val Type (_, fpTs) = domain_type (funpow (length gen_branch_Ts) range_type T); + val (ctrs0, Const (case_name, _)) = + (case BNF_FP_Def_Sugar.fp_sugar_of ctxt fpT_name of + SOME {fp_ctr_sugar = {ctr_sugar = {ctrs, casex, ...}, ...}, ...} => (ctrs, casex) + | NONE => + (case Ctr_Sugar.ctr_sugar_of ctxt fpT_name of + SOME {ctrs, casex, ...} => (ctrs, casex))); + in + if s = case_name then map (dest_Const o Ctr_Sugar.mk_ctr fpTs) ctrs0 + else raise Fail "non-case" + end + else + raise Fail "non-case")) + end; + +val is_co_datatype_case = can o dest_co_datatype_case; + +fun is_quotient_abs ctxt (s, T) = + (case T of + Type (@{type_name fun}, [_, Type (absT_name, _)]) => + classify_type_name ctxt absT_name = Quotient andalso + (case quotient_of ctxt absT_name of + (_, _, _, Const (s', _), _) => s' = s) + | _ => false); + +fun is_quotient_rep ctxt (s, T) = + (case T of + Type (@{type_name fun}, [Type (absT_name, _), _]) => + classify_type_name ctxt absT_name = Quotient andalso + (case quotient_of ctxt absT_name of + (_, _, _, _, Const (s', _)) => s' = s) + | _ => false); + +fun is_maybe_copy_abs ctxt absT_name s = + if absT_name = @{type_name set} then + s = @{const_name Collect} + else + (case try (copy_of ctxt) absT_name of + SOME (_, _, _, Const (s', _), _) => s' = s + | NONE => false); + +fun is_maybe_copy_rep ctxt absT_name s = + if absT_name = @{type_name set} then + s = @{const_name rmember} + else + (case try (copy_of ctxt) absT_name of + SOME (_, _, _, _, Const (s', _)) => s' = s + | NONE => false); + +fun is_copy_abs ctxt (s, T) = + (case T of + Type (@{type_name fun}, [_, Type (absT_name, _)]) => + classify_type_name ctxt absT_name = Copy andalso is_maybe_copy_abs ctxt absT_name s + | _ => false); + +fun is_copy_rep ctxt (s, T) = + (case T of + Type (@{type_name fun}, [Type (absT_name, _), _]) => + classify_type_name ctxt absT_name = Copy andalso is_maybe_copy_rep ctxt absT_name s + | _ => false); + +fun is_stale_copy_abs ctxt (s, T) = + (case T of + Type (@{type_name fun}, [_, Type (absT_name, _)]) => + classify_type_name ctxt absT_name <> Copy andalso is_maybe_copy_abs ctxt absT_name s + | _ => false); + +fun is_stale_copy_rep ctxt (s, T) = + (case T of + Type (@{type_name fun}, [Type (absT_name, _), _]) => + classify_type_name ctxt absT_name <> Copy andalso is_maybe_copy_rep ctxt absT_name s + | _ => false); + +fun instantiate_constant_types_in_term ctxt csts target = + let + val thy = Proof_Context.theory_of ctxt; + + fun try_const _ _ (res as SOME _) = res + | try_const (s', T') cst NONE = + (case cst of + Const (s, T) => + if s = s' then + SOME (Sign.typ_match thy (T', T) Vartab.empty) + handle Type.TYPE_MATCH => NONE + else + NONE + | _ => NONE); + + fun subst_for (Const x) = fold (try_const x) csts NONE + | subst_for (t as Free _) = if member (op aconv) csts t then SOME Vartab.empty else NONE + | subst_for (t1 $ t2) = (case subst_for t1 of SOME subst => SOME subst | NONE => subst_for t2) + | subst_for (Abs (_, _, t')) = subst_for t' + | subst_for _ = NONE; + in + (case subst_for target of + SOME subst => Envir.subst_term_types subst target + | NONE => raise Type.TYPE_MATCH) + end; + +datatype card = One | Fin | Fin_or_Inf | Inf + +(* Similar to "ATP_Util.tiny_card_of_type". *) +fun card_of_type ctxt = + let + fun max_card Inf _ = Inf + | max_card _ Inf = Inf + | max_card Fin_or_Inf _ = Fin_or_Inf + | max_card _ Fin_or_Inf = Fin_or_Inf + | max_card Fin _ = Fin + | max_card _ Fin = Fin + | max_card One One = One; + + fun card_of avoid T = + if member (op =) avoid T then + Inf + else + (case T of + TFree _ => Fin_or_Inf + | TVar _ => Inf + | Type (@{type_name fun}, [T1, T2]) => + (case (card_of avoid T1, card_of avoid T2) of + (_, One) => One + | (k1, k2) => max_card k1 k2) + | Type (@{type_name prod}, [T1, T2]) => + (case (card_of avoid T1, card_of avoid T2) of + (k1, k2) => max_card k1 k2) + | Type (@{type_name set}, [T']) => card_of avoid (T' --> HOLogic.boolT) + | Type (T_name, Ts) => + (case try (mutual_co_datatypes_of ctxt) (T_name, Ts) of + NONE => Inf + | SOME (_, fpTs, ctrss) => + (case ctrss of [[_]] => One | _ => Fin) + |> fold (fold (fold (max_card o card_of (fpTs @ avoid)) o binder_types o fastype_of)) + ctrss)); + in + card_of [] + end; + +fun int_of_classif Spec_Rules.Equational = 1 + | int_of_classif Spec_Rules.Inductive = 2 + | int_of_classif Spec_Rules.Co_Inductive = 3 + | int_of_classif Spec_Rules.Unknown = 4; + +val classif_ord = int_ord o apply2 int_of_classif; + +fun spec_rules_of ctxt (x as (s, T)) = + let + val thy = Proof_Context.theory_of ctxt; + + fun subst_of t0 = + try (Sign.typ_match thy (fastype_of t0, T)) Vartab.empty; + + fun process_spec _ (res as SOME _) = res + | process_spec (classif, (ts0, ths as _ :: _)) NONE = + (case get_first subst_of ts0 of + SOME subst => + (let + val ts = map (Envir.subst_term_types subst) ts0; + val poly_props = map Thm.prop_of ths; + val props = map (instantiate_constant_types_in_term ctxt ts) poly_props; + in + if exists (exists (exists_type (exists_subtype is_TVar))) [ts, props] then NONE + else SOME (classif, ts, props, poly_props) + end + handle Type.TYPE_MATCH => NONE) + | NONE => NONE) + | process_spec _ NONE = NONE; + + fun spec_rules () = + Spec_Rules.retrieve ctxt (Const x) + |> sort (classif_ord o apply2 fst); + + val specs = + if s = @{const_name The} then + [(Spec_Rules.Unknown, ([Logic.varify_global @{term The}], [@{thm theI_unique}]))] + else if s = @{const_name finite} then + let val card = card_of_type ctxt T in + if card = Inf orelse card = Fin_or_Inf then + spec_rules () + else + [(Spec_Rules.Equational, ([Logic.varify_global @{term finite}], + [Skip_Proof.make_thm thy (Logic.varify_global @{prop "finite A = True"})]))] + end + else + spec_rules (); + in + fold process_spec specs NONE + end; + +fun lhs_of_equation (Const (@{const_name Pure.eq}, _) $ t $ _) = t + | lhs_of_equation (@{const Trueprop} $ (Const (@{const_name HOL.eq}, _) $ t $ _)) = t; + +fun specialize_definition_type thy x def0 = + let + val def = specialize_type thy x def0; + val lhs = lhs_of_equation def; + in + if exists_Const (curry (op =) x) lhs then def else raise Fail "cannot specialize" + end; + +fun definition_of thy (x as (s, _)) = + Defs.specifications_of (Theory.defs_of thy) (Defs.Const, s) + |> map_filter #def + |> map_filter (try (specialize_definition_type thy x o Thm.prop_of o Thm.axiom thy)) + |> try hd; + +fun is_builtin_theory thy_id = + Context.subthy_id (thy_id, Context.theory_id @{theory Hilbert_Choice}); + +val orphan_axioms_of = + Spec_Rules.get + #> filter (curry (op =) Spec_Rules.Unknown o fst) + #> map snd + #> filter (null o fst) + #> maps snd + #> filter_out (is_builtin_theory o Thm.theory_id_of_thm) + #> map Thm.prop_of; + +fun keys_of _ (ITVal (T, _)) = [key_of_typ T] + | keys_of _ (ICopy {abs_typ, ...}) = [key_of_typ abs_typ] + | keys_of _ (IQuotient {abs_typ, ...}) = [key_of_typ abs_typ] + | keys_of _ (ICoData (_, specs)) = map (key_of_typ o #typ) specs + | keys_of ctxt (IVal const) = [key_of_const ctxt const] + | keys_of ctxt (ICoPred (_, _, specs)) = map (key_of_const ctxt o #const) specs + | keys_of ctxt (IRec specs) = map (key_of_const ctxt o #const) specs + | keys_of ctxt (ISpec {consts, ...}) = map (key_of_const ctxt) consts + | keys_of _ (IAxiom _) = [] + | keys_of _ (IGoal _) = [] + | keys_of _ (IEval _) = []; + +fun co_data_spec_deps_of ctxt ({ctrs, ...} : isa_co_data_spec) = + fold (add_keys ctxt) ctrs []; +fun const_spec_deps_of ctxt consts props = + fold (add_keys ctxt) props [] |> subtract (op =) (map (key_of_const ctxt) consts); +fun consts_spec_deps_of ctxt {consts, props} = + fold (add_keys ctxt) props [] |> subtract (op =) (map (key_of_const ctxt) consts); + +fun deps_of _ (ITVal _) = [] + | deps_of ctxt (ICopy {wrt, ...}) = add_keys ctxt wrt [] + | deps_of ctxt (IQuotient {wrt, ...}) = add_keys ctxt wrt [] + | deps_of ctxt (ICoData (_, specs)) = maps (co_data_spec_deps_of ctxt) specs + | deps_of _ (IVal const) = add_type_keys (fastype_of const) [] + | deps_of ctxt (ICoPred (_, _, specs)) = + maps (const_spec_deps_of ctxt (map #const specs) o #props) specs + | deps_of ctxt (IRec specs) = maps (const_spec_deps_of ctxt (map #const specs) o #props) specs + | deps_of ctxt (ISpec spec) = consts_spec_deps_of ctxt spec + | deps_of ctxt (IAxiom prop) = add_keys ctxt prop [] + | deps_of ctxt (IGoal prop) = add_keys ctxt prop [] + | deps_of ctxt (IEval t) = add_keys ctxt t []; + +fun consts_of_rec_or_spec (IRec specs) = map #const specs + | consts_of_rec_or_spec (ISpec {consts, ...}) = consts; + +fun props_of_rec_or_spec (IRec specs) = maps #props specs + | props_of_rec_or_spec (ISpec {props, ...}) = props; + +fun merge_two_rec_or_spec cmd cmd' = + ISpec {consts = consts_of_rec_or_spec cmd @ consts_of_rec_or_spec cmd', + props = props_of_rec_or_spec cmd @ props_of_rec_or_spec cmd'}; + +fun merge_two (ICoData (fp, specs)) (ICoData (fp', specs'), complete) = + (ICoData (BNF_Util.case_fp fp fp fp', specs @ specs'), complete andalso fp = fp') + | merge_two (IRec specs) (IRec specs', complete) = (IRec (specs @ specs'), complete) + | merge_two (cmd as IRec _) (cmd' as ISpec _, complete) = + (merge_two_rec_or_spec cmd cmd', complete) + | merge_two (cmd as ISpec _) (cmd' as IRec _, complete) = + (merge_two_rec_or_spec cmd cmd', complete) + | merge_two (cmd as ISpec _) (cmd' as ISpec _, complete) = + (merge_two_rec_or_spec cmd cmd', complete) + | merge_two _ _ = raise CYCLIC_DEPS (); + +fun sort_isa_commands_topologically ctxt cmds = + let + fun normal_pairs [] = [] + | normal_pairs (all as normal :: _) = map (rpair normal) all; + + fun add_node [] _ = I + | add_node (normal :: _) cmd = Graph.new_node (normal, cmd); + + fun merge_scc (cmd :: cmds) complete = fold merge_two cmds (cmd, complete); + + fun sort_problem (cmds, complete) = + let + val keyss = map (keys_of ctxt) cmds; + val normal_keys = Symtab.make (maps normal_pairs keyss); + val normalize = Symtab.lookup normal_keys; + + fun add_deps [] _ = I + | add_deps (normal :: _) cmd = + let + val deps = deps_of ctxt cmd + |> map_filter normalize + |> remove (op =) normal; + in + fold (fn dep => Graph.add_edge (dep, normal)) deps + end; + + val cmd_of_key = the o AList.lookup (op =) (map hd keyss ~~ cmds); + + val G = Graph.empty + |> fold2 add_node keyss cmds + |> fold2 add_deps keyss cmds; + + val cmd_sccs = rev (Graph.strong_conn G) + |> map (map cmd_of_key); + in + if exists (can (fn _ :: _ :: _ => ())) cmd_sccs then + sort_problem (fold_map merge_scc cmd_sccs complete) + else + (Graph.schedule (K snd) G, complete) + end; + + val typedecls = filter (can (fn ITVal _ => ())) cmds; + val (mixed, complete) = + (filter (can (fn ICopy _ => () | IQuotient _ => () | ICoData _ => () | IVal _ => () + | ICoPred _ => () | IRec _ => () | ISpec _ => ())) cmds, true) + |> sort_problem; + val axioms = filter (can (fn IAxiom _ => ())) cmds; + val goals = filter (can (fn IGoal _ => ())) cmds; + val evals = filter (can (fn IEval _ => ())) cmds; + in + (typedecls @ mixed @ axioms @ goals @ evals, complete) + end; + +fun group_of (ITVal _) = 1 + | group_of (ICopy _) = 2 + | group_of (IQuotient _) = 3 + | group_of (ICoData _) = 4 + | group_of (IVal _) = 5 + | group_of (ICoPred _) = 6 + | group_of (IRec _) = 7 + | group_of (ISpec _) = 8 + | group_of (IAxiom _) = 9 + | group_of (IGoal _) = 10 + | group_of (IEval _) = 11; + +fun group_isa_commands [] = [] + | group_isa_commands [cmd] = [[cmd]] + | group_isa_commands (cmd :: cmd' :: cmds) = + let val (group :: groups) = group_isa_commands (cmd' :: cmds) in + if group_of cmd = group_of cmd' then + (cmd :: group) :: groups + else + [cmd] :: (group :: groups) + end; + +fun defined_by (Const (@{const_name All}, _) $ t) = defined_by t + | defined_by (Abs (_, _, t)) = defined_by t + | defined_by (@{const implies} $ _ $ u) = defined_by u + | defined_by (Const (@{const_name HOL.eq}, _) $ t $ _) = head_of t + | defined_by t = head_of t; + +fun partition_props [_] props = SOME [props] + | partition_props consts props = + let + val propss = map (fn const => filter (fn prop => defined_by prop aconv const) props) consts; + in + if eq_set (op aconv) (props, flat propss) andalso forall (not o null) propss then SOME propss + else NONE + end; + +fun hol_concl_head (Const (@{const_name All}, _) $ Abs (_, _, t)) = hol_concl_head t + | hol_concl_head (Const (@{const_name implies}, _) $ _ $ t) = hol_concl_head t + | hol_concl_head (t $ _) = hol_concl_head t + | hol_concl_head t = t; + +fun is_inductive_set_intro t = + (case hol_concl_head t of + Const (@{const_name rmember}, _) => true + | _ => false); + +exception NO_TRIPLE of unit; + +fun triple_for_intro_rule ctxt x rule = + let + val (prems, concl) = Logic.strip_horn rule + |>> map (Object_Logic.atomize_term ctxt) + ||> Object_Logic.atomize_term ctxt; + + val (mains, sides) = List.partition (exists_Const (curry (op =) x)) prems; + + val is_right_head = curry (op aconv) (Const x) o head_of; + in + if forall is_right_head mains then (sides, mains, concl) else raise NO_TRIPLE () + end; + +val tuple_for_args = HOLogic.mk_tuple o snd o strip_comb; + +fun wf_constraint_for rel sides concl mains = + HOLogic.mk_mem (HOLogic.mk_prod (apply2 tuple_for_args (mains, concl)), Var rel) + |> fold (curry HOLogic.mk_imp) sides + |> close_form [rel]; + +fun wf_constraint_for_triple rel (sides, mains, concl) = + map (wf_constraint_for rel sides concl) mains + |> foldr1 HOLogic.mk_conj; + +fun terminates_by ctxt timeout goal tac = + can (SINGLE (Classical.safe_tac ctxt) #> the + #> SINGLE (DETERM_TIMEOUT timeout (tac ctxt (auto_tac ctxt))) #> the + #> Goal.finish ctxt) goal; + +val max_cached_wfs = 50; +val cached_timeout = Synchronized.var "Nunchaku_Collect.cached_timeout" Time.zeroTime; +val cached_wf_props = Synchronized.var "Nunchaku_Collect.cached_wf_props" ([] : (term * bool) list); + +val termination_tacs = [Lexicographic_Order.lex_order_tac true, ScnpReconstruct.sizechange_tac]; + +fun is_wellfounded_inductive_predicate ctxt wfs debug wf_timeout const intros = + let + val thy = Proof_Context.theory_of ctxt; + + val Const (x as (_, T)) = head_of (HOLogic.dest_Trueprop (Logic.strip_imp_concl (hd intros))); + in + (case triple_lookup (const_match thy o swap) wfs (dest_Const const) of + SOME (SOME wf) => wf + | _ => + (case map (triple_for_intro_rule ctxt x) intros |> filter_out (null o #2) of + [] => true + | triples => + let + val binders_T = HOLogic.mk_tupleT (binder_types T); + val rel_T = HOLogic.mk_setT (HOLogic.mk_prodT (binders_T, binders_T)); + val j = fold (Integer.max o maxidx_of_term) intros 0 + 1; + val rel = (("R", j), rel_T); + val prop = + Const (@{const_name wf}, rel_T --> HOLogic.boolT) $ Var rel :: + map (wf_constraint_for_triple rel) triples + |> foldr1 HOLogic.mk_conj + |> HOLogic.mk_Trueprop; + in + if debug then writeln ("Wellfoundedness goal: " ^ Syntax.string_of_term ctxt prop) + else (); + if wf_timeout = Synchronized.value cached_timeout andalso + length (Synchronized.value cached_wf_props) < max_cached_wfs then + () + else + (Synchronized.change cached_wf_props (K []); + Synchronized.change cached_timeout (K wf_timeout)); + (case AList.lookup (op =) (Synchronized.value cached_wf_props) prop of + SOME wf => wf + | NONE => + let + val goal = Goal.init (Thm.cterm_of ctxt prop); + val wf = exists (terminates_by ctxt wf_timeout goal) termination_tacs; + in + Synchronized.change cached_wf_props (cons (prop, wf)); wf + end) + end) + handle + List.Empty => false + | NO_TRIPLE () => false) + end; + +datatype lhs_pat = + Only_Vars +| Prim_Pattern of string +| Any_Pattern; + +fun is_likely_pat_complete ctxt props = + let + val is_Var_or_Bound = is_Var orf is_Bound; + + fun lhs_pat_of t = + (case t of + Const (@{const_name All}, _) $ Abs (_, _, t) => lhs_pat_of t + | Const (@{const_name HOL.eq}, _) $ u $ _ => + (case filter_out is_Var_or_Bound (snd (strip_comb u)) of + [] => Only_Vars + | [v] => + (case strip_comb v of + (cst as Const (_, T), args) => + (case body_type T of + Type (T_name, _) => + if can (Ctr_Sugar.dest_ctr ctxt T_name) cst andalso forall is_Var_or_Bound args then + Prim_Pattern T_name + else + Any_Pattern + | _ => Any_Pattern) + | _ => Any_Pattern) + | _ => Any_Pattern) + | _ => Any_Pattern); + in + (case map lhs_pat_of props of + [] => false + | pats as Prim_Pattern T_name :: _ => + forall (can (fn Prim_Pattern _ => ())) pats andalso + length pats = length (#ctrs (the (Ctr_Sugar.ctr_sugar_of ctxt T_name))) + | pats => forall (curry (op =) Only_Vars) pats) + end; + +(* Prevents divergence in case of cyclic or infinite axiom dependencies. *) +val axioms_max_depth = 255 + +fun isa_problem_of_subgoal ctxt falsify wfs whacks cards debug wf_timeout evals0 some_assms0 + subgoal0 = + let + val thy = Proof_Context.theory_of ctxt; + + fun card_of T = + (case triple_lookup (typ_match thy o swap) cards T of + NONE => (NONE, NONE) + | SOME (c1, c2) => (if c1 = SOME 1 then NONE else c1, c2)); + + fun axioms_of_class class = + #axioms (Axclass.get_info thy class) + handle ERROR _ => []; + + fun monomorphize_class_axiom T t = + (case Term.add_tvars t [] of + [] => t + | [(x, S)] => Envir.subst_term_types (Vartab.make [(x, (S, T))]) t); + + fun consider_sort depth T S (seens as (seenS, seenT, seen), problem) = + if member (op =) seenS S then + (seens, problem) + else if depth > axioms_max_depth then + raise TOO_DEEP_DEPS () + else + let + val seenS = S :: seenS; + val seens = (seenS, seenT, seen); + + val supers = Sign.complete_sort thy S; + val axioms0 = maps (map Thm.prop_of o axioms_of_class) supers; + val axioms = map (preprocess_prop false ctxt whacks o monomorphize_class_axiom T) axioms0; + in + (seens, map IAxiom axioms @ problem) + |> fold (consider_term (depth + 1)) axioms + end + and consider_type depth T = + (case T of + Type (s, Ts) => + if is_type_builtin s then fold (consider_type depth) Ts + else consider_non_builtin_type depth T + | _ => consider_non_builtin_type depth T) + and consider_non_builtin_type depth T (seens as (seenS, seenT, seen), problem) = + if member (op =) seenT T then + (seens, problem) + else + let + val seenT = T :: seenT; + val seens = (seenS, seenT, seen); + + fun consider_quotient_or_copy tuple_of s = + let + val (T0, repT0, wrt0, abs0, rep0) = tuple_of ctxt s; + val tyenv = Sign.typ_match thy (T0, T) Vartab.empty; + val substT = Envir.subst_type tyenv; + val subst = Envir.subst_term_types tyenv; + val repT = substT repT0; + val wrt = subst wrt0; + val abs = subst abs0; + val rep = subst rep0; + in + apsnd (cons (ICopy {abs_typ = T, rep_typ = repT, wrt = wrt, abs = abs, + rep = rep})) + #> consider_term (depth + 1) wrt + end; + in + (seens, problem) + |> (case T of + TFree (_, S) => + apsnd (cons (ITVal (T, card_of T))) + #> consider_sort depth T S + | TVar (_, S) => consider_sort depth T S + | Type (s, Ts) => + fold (consider_type depth) Ts + #> (case classify_type_name ctxt s of + Co_Datatype => + let + val (fp, fpTs, ctrss) = mutual_co_datatypes_of ctxt (s, Ts); + val specs = map2 (fn T => fn ctrs => {typ = T, ctrs = ctrs}) fpTs ctrss; + in + (fn ((seenS, seenT, seen), problem) => + ((seenS, union (op =) fpTs seenT, seen), ICoData (fp, specs) :: problem)) + #> fold (fold (consider_type (depth + 1) o fastype_of)) ctrss + end + | Quotient => consider_quotient_or_copy quotient_of s + | Copy => consider_quotient_or_copy copy_of s + | TVal => apsnd (cons (ITVal (T, card_of T))))) + end + and consider_term depth t = + (case t of + t1 $ t2 => fold (consider_term depth) [t1, t2] + | Var (_, T) => consider_type depth T + | Bound _ => I + | Abs (_, T, t') => + consider_term depth t' + #> consider_type depth T + | _ => (fn (seens as (seenS, seenT, seen), problem) => + if member (op aconv) seen t then + (seens, problem) + else if depth > axioms_max_depth then + raise TOO_DEEP_DEPS () + else + let + val seen = t :: seen; + val seens = (seenS, seenT, seen); + in + (case t of + Const (x as (s, T)) => + (if is_const_builtin s orelse is_co_datatype_ctr ctxt x orelse + is_co_datatype_case ctxt x orelse is_quotient_abs ctxt x orelse + is_quotient_rep ctxt x orelse is_copy_abs ctxt x orelse + is_copy_rep ctxt x then + (seens, problem) + else if is_stale_copy_abs ctxt x orelse is_stale_copy_rep ctxt x then + raise UNSUPPORTED_FUNC t + else + (case spec_rules_of ctxt x of + SOME (classif, consts, props0, poly_props) => + let + val props = map (preprocess_prop false ctxt whacks) props0; + + fun def_or_spec () = + (case definition_of thy x of + SOME eq0 => + let val eq = preprocess_prop false ctxt whacks eq0 in + ([eq], [IRec [{const = t, props = [eq], pat_complete = true}]]) + end + | NONE => (props, [ISpec {consts = consts, props = props}])); + + val (props', cmds) = + if null props then + ([], map IVal consts) + else if classif = Spec_Rules.Equational then + (case partition_props consts props of + SOME propss => + (props, + [IRec (map2 (fn const => fn props => + {const = const, props = props, + pat_complete = is_likely_pat_complete ctxt props}) + consts propss)]) + | NONE => def_or_spec ()) + else if member (op =) [Spec_Rules.Inductive, Spec_Rules.Co_Inductive] + classif then + if is_inductive_set_intro (hd props) then + def_or_spec () + else + (case partition_props consts props of + SOME propss => + (props, + [ICoPred (if classif = Spec_Rules.Inductive then BNF_Util.Least_FP + else BNF_Util.Greatest_FP, + length consts = 1 andalso + is_wellfounded_inductive_predicate ctxt wfs debug wf_timeout + (the_single consts) poly_props, + map2 (fn const => fn props => {const = const, props = props}) + consts propss)]) + | NONE => def_or_spec ()) + else + def_or_spec (); + in + ((seenS, seenT, union (op aconv) consts seen), cmds @ problem) + |> fold (consider_term (depth + 1)) props' + end + | NONE => + (case definition_of thy x of + SOME eq0 => + let val eq = preprocess_prop false ctxt whacks eq0 in + (seens, IRec [{const = t, props = [eq], pat_complete = true}] :: problem) + |> consider_term (depth + 1) eq + end + | NONE => (seens, IVal t :: problem)))) + |> consider_type depth T + | Free (_, T) => + (seens, IVal t :: problem) + |> consider_type depth T) + end)); + + val (poly_axioms, mono_axioms0) = orphan_axioms_of ctxt + |> List.partition has_polymorphism; + + fun implicit_evals_of pol (@{const Not} $ t) = implicit_evals_of (not pol) t + | implicit_evals_of pol (@{const implies} $ t $ u) = + (case implicit_evals_of pol u of + [] => implicit_evals_of (not pol) t + | ts => ts) + | implicit_evals_of pol (@{const conj} $ t $ u) = + union (op aconv) (implicit_evals_of pol t) (implicit_evals_of pol u) + | implicit_evals_of pol (@{const disj} $ t $ u) = + union (op aconv) (implicit_evals_of pol t) (implicit_evals_of pol u) + | implicit_evals_of false (Const (@{const_name HOL.eq}, _) $ t $ u) = + distinct (op aconv) [t, u] + | implicit_evals_of true (Const (@{const_name HOL.eq}, _) $ t $ _) = [t] + | implicit_evals_of _ _ = []; + + val mono_axioms_and_some_assms = + map (preprocess_prop false ctxt whacks) (mono_axioms0 @ some_assms0); + val subgoal = preprocess_prop falsify ctxt whacks subgoal0; + val implicit_evals = implicit_evals_of true subgoal; + val evals = map (preprocess_closed_term ctxt whacks) evals0; + val seens = ([], [], []); + + val (commandss, complete) = + (seens, + map IAxiom mono_axioms_and_some_assms @ [IGoal subgoal] @ map IEval (implicit_evals @ evals)) + |> fold (consider_term 0) (subgoal :: evals @ mono_axioms_and_some_assms) + |> snd + |> rev (* prettier *) + |> sort_isa_commands_topologically ctxt + |>> group_isa_commands; + in + (poly_axioms, {commandss = commandss, sound = true, complete = complete}) + end; + +fun add_pat_complete_of_command cmd = + (case cmd of + ICoPred (_, _, specs) => union (op =) (map #const specs) + | IRec specs => + union (op =) (map_filter (try (fn {const, pat_complete = true, ...} => const)) specs) + | _ => I); + +fun pat_completes_of_isa_problem {commandss, ...} = + fold (fold add_pat_complete_of_command) commandss []; + +fun str_of_isa_term_with_type ctxt t = + Syntax.string_of_term ctxt t ^ " : " ^ Syntax.string_of_typ ctxt (fastype_of t); + +fun is_triv_wrt (Abs (_, _, body)) = is_triv_wrt body + | is_triv_wrt @{const True} = true + | is_triv_wrt _ = false; + +fun str_of_isa_type_spec ctxt {abs_typ, rep_typ, wrt, abs, rep} = + Syntax.string_of_typ ctxt abs_typ ^ " := " ^ Syntax.string_of_typ ctxt rep_typ ^ + (if is_triv_wrt wrt then "" else "\n wrt " ^ Syntax.string_of_term ctxt wrt) ^ + "\n abstract " ^ Syntax.string_of_term ctxt abs ^ + "\n concrete " ^ Syntax.string_of_term ctxt rep; + +fun str_of_isa_co_data_spec ctxt {typ, ctrs} = + Syntax.string_of_typ ctxt typ ^ " :=\n " ^ + space_implode "\n| " (map (str_of_isa_term_with_type ctxt) ctrs); + +fun str_of_isa_const_spec ctxt {const, props} = + str_of_isa_term_with_type ctxt const ^ " :=\n " ^ + space_implode ";\n " (map (Syntax.string_of_term ctxt) props); + +fun str_of_isa_rec_spec ctxt {const, props, pat_complete} = + str_of_isa_term_with_type ctxt const ^ (if pat_complete then " [pat_complete]" else "") ^ + " :=\n " ^ space_implode ";\n " (map (Syntax.string_of_term ctxt) props); + +fun str_of_isa_consts_spec ctxt {consts, props} = + space_implode " and\n " (map (str_of_isa_term_with_type ctxt) consts) ^ " :=\n " ^ + space_implode ";\n " (map (Syntax.string_of_term ctxt) props); + +fun str_of_isa_card NONE = "" + | str_of_isa_card (SOME k) = signed_string_of_int k; + +fun str_of_isa_cards_suffix (NONE, NONE) = "" + | str_of_isa_cards_suffix (c1, c2) = " " ^ str_of_isa_card c1 ^ "-" ^ str_of_isa_card c2; + +fun str_of_isa_command ctxt (ITVal (T, cards)) = + "type " ^ Syntax.string_of_typ ctxt T ^ str_of_isa_cards_suffix cards + | str_of_isa_command ctxt (ICopy spec) = "copy " ^ str_of_isa_type_spec ctxt spec + | str_of_isa_command ctxt (IQuotient spec) = "quotient " ^ str_of_isa_type_spec ctxt spec + | str_of_isa_command ctxt (ICoData (fp, specs)) = + BNF_Util.case_fp fp "data" "codata" ^ " " ^ str_of_and_list (str_of_isa_co_data_spec ctxt) specs + | str_of_isa_command ctxt (IVal t) = "val " ^ str_of_isa_term_with_type ctxt t + | str_of_isa_command ctxt (ICoPred (fp, wf, specs)) = + BNF_Util.case_fp fp "pred" "copred" ^ " " ^ (if wf then "[wf] " else "") ^ + str_of_and_list (str_of_isa_const_spec ctxt) specs + | str_of_isa_command ctxt (IRec specs) = "rec " ^ str_of_and_list (str_of_isa_rec_spec ctxt) specs + | str_of_isa_command ctxt (ISpec spec) = "spec " ^ str_of_isa_consts_spec ctxt spec + | str_of_isa_command ctxt (IAxiom prop) = "axiom " ^ Syntax.string_of_term ctxt prop + | str_of_isa_command ctxt (IGoal prop) = "goal " ^ Syntax.string_of_term ctxt prop + | str_of_isa_command ctxt (IEval t) = "eval " ^ Syntax.string_of_term ctxt t; + +fun str_of_isa_problem ctxt {commandss, sound, complete} = + map (cat_lines o map (suffix "." o str_of_isa_command ctxt)) commandss + |> space_implode "\n\n" |> suffix "\n" + |> prefix ("# " ^ (if sound then "sound" else "unsound") ^ "\n") + |> prefix ("# " ^ (if complete then "complete" else "incomplete") ^ "\n"); + +end; diff -r 14571c9e1d50 -r 6273d4c8325b src/HOL/Nunchaku/Tools/nunchaku_commands.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Nunchaku/Tools/nunchaku_commands.ML Mon Oct 24 22:42:07 2016 +0200 @@ -0,0 +1,258 @@ +(* Title: HOL/Nunchaku/Tools/nunchaku_commands.ML + Author: Jasmin Blanchette, Inria Nancy, LORIA, MPII + Copyright 2015, 2016 + +Adds the "nunchaku" and "nunchaku_params" commands to Isabelle/Isar's outer syntax. +*) + +signature NUNCHAKU_COMMANDS = +sig + type params = Nunchaku.params + + val default_params: theory -> (string * string) list -> params +end; + +structure Nunchaku_Commands : NUNCHAKU_COMMANDS = +struct + +open Nunchaku_Util; +open Nunchaku; + +type raw_param = string * string list; + +val default_default_params = + [("assms", "true"), + ("debug", "false"), + ("falsify", "true"), + ("max_genuine", "1"), + ("max_potential", "1"), + ("overlord", "false"), + ("specialize", "true"), + ("spy", "false"), + ("timeout", "30"), + ("verbose", "false"), + ("wf_timeout", "0.5")]; + +val negated_params = + [("dont_whack", "whack"), + ("dont_specialize", "specialize"), + ("dont_spy", "spy"), + ("no_assms", "assms"), + ("no_debug", "debug"), + ("no_overlord", "overlord"), + ("non_mono", "mono"), + ("non_wf", "wf"), + ("quiet", "verbose"), + ("satisfy", "falsify")]; + +fun is_known_raw_param s = + AList.defined (op =) default_default_params s orelse + AList.defined (op =) negated_params s orelse + member (op =) ["atoms", "card", "eval", "expect"] s orelse + exists (fn p => String.isPrefix (p ^ " ") s) + ["atoms", "card", "dont_whack", "mono", "non_mono", "non_wf", "wf", "whack"]; + +fun check_raw_param (s, _) = + if is_known_raw_param s then () else error ("Unknown parameter: " ^ quote s); + +fun unnegate_param_name name = + (case AList.lookup (op =) negated_params name of + NONE => + if String.isPrefix "dont_" name then SOME (unprefix "dont_" name) + else if String.isPrefix "non_" name then SOME (unprefix "non_" name) + else NONE + | some_name => some_name); + +fun normalize_raw_param (name, value) = + (case unnegate_param_name name of + SOME name' => + [(name', + (case value of + ["false"] => ["true"] + | ["true"] => ["false"] + | [] => ["false"] + | _ => value))] + | NONE => [(name, value)]); + +structure Data = Theory_Data +( + type T = raw_param list + val empty = default_default_params |> map (apsnd single) + val extend = I + fun merge data = AList.merge (op =) (K true) data +); + +val set_default_raw_param = Data.map o fold (AList.update (op =)) o normalize_raw_param; +val default_raw_params = Data.get; + +fun is_punctuation s = (s = "," orelse s = "-"); + +fun stringify_raw_param_value [] = "" + | stringify_raw_param_value [s] = s + | stringify_raw_param_value (s1 :: s2 :: ss) = + s1 ^ (if is_punctuation s1 orelse is_punctuation s2 then "" else " ") ^ + stringify_raw_param_value (s2 :: ss); + +fun extract_params ctxt mode default_params override_params = + let + val override_params = maps normalize_raw_param override_params; + val raw_params = rev override_params @ rev default_params; + val raw_lookup = AList.lookup (op =) raw_params; + val lookup = Option.map stringify_raw_param_value o raw_lookup; + val lookup_string = the_default "" o lookup; + + fun general_lookup_bool option default_value name = + (case lookup name of + SOME s => parse_bool_option option name s + | NONE => default_value); + + val lookup_bool = the o general_lookup_bool false (SOME false); + + fun lookup_int name = + (case lookup name of + SOME s => + (case Int.fromString s of + SOME i => i + | NONE => error ("Parameter " ^ quote name ^ " must be assigned an integer value")) + | NONE => 0); + + fun int_range_from_string name s = + (case space_explode "-" s of + [s] => (s, s) + | [s1, s2] => (s1, s2) + | _ => error ("Parameter " ^ quote name ^ " must be assigned a range of integers")) + |> apply2 Int.fromString; + + fun lookup_assigns read pre of_str = + (case lookup pre of + SOME s => [(NONE, of_str s)] + | NONE => []) @ + map (fn (name, value) => (SOME (read (String.extract (name, size pre + 1, NONE))), + of_str (stringify_raw_param_value value))) + (filter (String.isPrefix (pre ^ " ") o fst) raw_params); + + fun lookup_int_range_assigns read pre = + lookup_assigns read pre (int_range_from_string pre); + + fun lookup_bool_assigns read pre = + lookup_assigns read pre (the o parse_bool_option false pre); + + fun lookup_bool_option_assigns read pre = + lookup_assigns read pre (parse_bool_option true pre); + + fun lookup_strings_assigns read pre = + lookup_assigns read pre (space_explode " "); + + fun lookup_time name = + (case lookup name of + SOME s => parse_time name s + | NONE => Time.zeroTime); + + val read_type_polymorphic = + Syntax.read_typ ctxt #> Logic.mk_type + #> singleton (Variable.polymorphic ctxt) #> Logic.dest_type; + val read_term_polymorphic = + Syntax.read_term ctxt #> singleton (Variable.polymorphic ctxt); + val lookup_term_list_option_polymorphic = + AList.lookup (op =) raw_params #> Option.map (map read_term_polymorphic); + + fun read_const_polymorphic s = + (case read_term_polymorphic s of + Const x => x + | t => error ("Not a constant: " ^ Syntax.string_of_term ctxt t)); + + val wfs = lookup_bool_option_assigns read_const_polymorphic "wf"; + val whacks = lookup_bool_assigns read_term_polymorphic "whack"; + val cards = lookup_int_range_assigns read_type_polymorphic "card"; + val monos = lookup_bool_option_assigns read_type_polymorphic "mono"; + val falsify = lookup_bool "falsify"; + val debug = (mode <> Auto_Try andalso lookup_bool "debug"); + val verbose = debug orelse (mode <> Auto_Try andalso lookup_bool "verbose"); + val overlord = lookup_bool "overlord"; + val spy = getenv "NUNCHAKU_SPY" = "yes" orelse lookup_bool "spy"; + val assms = lookup_bool "assms"; + val specialize = lookup_bool "specialize"; + val timeout = lookup_time "timeout"; + val wf_timeout = lookup_time "wf_timeout"; + val multithread = mode = Normal andalso lookup_bool "multithread"; + val evals = these (lookup_term_list_option_polymorphic "eval"); + val atomss = lookup_strings_assigns read_type_polymorphic "atoms"; + val max_potential = if mode = Normal then Int.max (0, lookup_int "max_potential") else 0; + val max_genuine = Int.max (0, lookup_int "max_genuine"); + val expect = lookup_string "expect"; + + val mode_of_operation_params = + {falsify = falsify, assms = assms, spy = spy, overlord = overlord, + expect = expect}; + + val scope_of_search_params = + {wfs = wfs, whacks = whacks, cards = cards, monos = monos}; + + val output_format_params = + {verbose = verbose, debug = debug, max_potential = max_potential, max_genuine = max_genuine, + evals = evals, atomss = atomss}; + + val optimization_params = + {specialize = specialize, multithread = multithread}; + + val timeout_params = + {timeout = timeout, wf_timeout = wf_timeout}; + in + {mode_of_operation_params = mode_of_operation_params, + scope_of_search_params = scope_of_search_params, + output_format_params = output_format_params, + optimization_params = optimization_params, + timeout_params = timeout_params} + end; + +fun default_params thy = + extract_params (Proof_Context.init_global thy) Normal (default_raw_params thy) + o map (apsnd single); + +val parse_key = Scan.repeat1 Parse.embedded >> space_implode " "; +val parse_value = + Scan.repeat1 (Parse.minus >> single + || Scan.repeat1 (Scan.unless Parse.minus (Parse.name || Parse.float_number)) + || @{keyword ","} |-- Parse.number >> prefix "," >> single) + >> flat; +val parse_param = parse_key -- Scan.optional (@{keyword "="} |-- parse_value) []; +val parse_params = Scan.optional (@{keyword "["} |-- Parse.list parse_param --| @{keyword "]"}) []; + +fun run_chaku override_params mode i state0 = + let + val state = Proof.map_contexts (Try0.silence_methods false) state0; + val thy = Proof.theory_of state; + val ctxt = Proof.context_of state; + val _ = List.app check_raw_param override_params; + val params = extract_params ctxt mode (default_raw_params thy) override_params; + in + (if mode = Auto_Try then perhaps o try else fn f => fn x => f x) + (fn _ => run_chaku_on_subgoal state params mode i) (unknownN, NONE) + |> `(fn (outcome_code, _) => outcome_code = genuineN) + end; + +fun string_for_raw_param (name, value) = + name ^ " = " ^ stringify_raw_param_value value; + +fun nunchaku_params_trans params = + Toplevel.theory (fold set_default_raw_param params + #> tap (fn thy => + let val params = rev (default_raw_params thy) in + List.app check_raw_param params; + writeln ("Default parameters for Nunchaku:\n" ^ + (params |> map string_for_raw_param |> sort_strings |> cat_lines)) + end)); + +val _ = + Outer_Syntax.command @{command_keyword nunchaku} + "try to find a countermodel using Nunchaku" + (parse_params -- Scan.optional Parse.nat 1 >> (fn (params, i) => + Toplevel.keep_proof (fn state => + ignore (run_chaku params Normal i (Toplevel.proof_of state))))); + +val _ = + Outer_Syntax.command @{command_keyword nunchaku_params} + "set and display the default parameters for Nunchaku" + (parse_params #>> nunchaku_params_trans); + +end; diff -r 14571c9e1d50 -r 6273d4c8325b src/HOL/Nunchaku/Tools/nunchaku_display.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Nunchaku/Tools/nunchaku_display.ML Mon Oct 24 22:42:07 2016 +0200 @@ -0,0 +1,91 @@ +(* Title: HOL/Nunchaku/Tools/nunchaku_display.ML + Author: Jasmin Blanchette, Inria Nancy, LORIA, MPII + Copyright 2015, 2016 + +Pretty printing of Isabelle/HOL models for Nunchaku. +*) + +signature NUNCHAKU_DISPLAY = +sig + type isa_model = Nunchaku_Reconstruct.isa_model + + val pretty_of_isa_model_opt: Proof.context -> isa_model option -> Pretty.T +end; + +structure Nunchaku_Display : NUNCHAKU_DISPLAY = +struct + +open Nunchaku_Util; +open Nunchaku_Reconstruct; + +val indent_size = 2; + +val pretty_indent = Pretty.indent indent_size; + +fun sorting_str_of_typ (TFree (s, _)) = "a" ^ s + | sorting_str_of_typ (Type (s, Ts)) = "b" ^ s ^ space_implode " " (map sorting_str_of_typ Ts) + | sorting_str_of_typ (TVar _) = "X"; + +fun sorting_str_of_term (Const (s, T)) = "b" ^ s ^ sorting_str_of_typ T + | sorting_str_of_term (Free (s, _)) = "a" ^ s + | sorting_str_of_term (t $ u) = sorting_str_of_term t ^ " " ^ sorting_str_of_term u + | sorting_str_of_term (Abs (_, T, t)) = "c" ^ sorting_str_of_typ T ^ " " ^ sorting_str_of_term t + | sorting_str_of_term _ = "X"; + +fun pretty_of_isa_model_opt _ NONE = + pretty_indent (Pretty.str "Model unavailable (internal error)") + | pretty_of_isa_model_opt ctxt0 + (SOME {type_model, free_model, pat_complete_model, pat_incomplete_model, skolem_model}) = + let + val ctxt = ctxt0 |> Config.put show_question_marks false; + + val pat_incomplete_model' = pat_incomplete_model + |> filter_out (can (fn Const (@{const_name unreachable}, _) => ()) o fst); + + fun pretty_of_typ_entry (T, atoms) = + Pretty.block (Pretty.breaks [Syntax.pretty_typ ctxt T, Pretty.str "=", + Pretty.enum "," "{" "}" (map (Syntax.pretty_term ctxt) atoms)]); + + fun pretty_of_term_entry (t, value) = + let + val no_types_ctxt = ctxt |> Config.put show_types false; + val schematic_ctxt = ctxt |> Proof_Context.set_mode Proof_Context.mode_schematic; + + val show_types = Config.get ctxt show_types; + val value' = value |> perhaps (try (Syntax.check_term schematic_ctxt)); + val T = fastype_of t; + val T' = if T = dummyT then try fastype_of value' |> the_default T else T; + val t' = t |> show_types ? Type.constraint T'; + in + Pretty.block (Pretty.breaks + [Syntax.pretty_term ctxt t' + |> (show_types andalso T' <> dummyT) ? (single #> Pretty.enclose "(" ")"), + Pretty.str "=", Syntax.pretty_term no_types_ctxt value']) + end; + + fun chunks_of_entries sorting_str_of pretty_of title entries = + if not (null entries) then + (if title = "" then [] else [Pretty.str (title ^ plural_s_for_list entries ^ ":")]) @ + map (pretty_indent o pretty_of) (sort_by (sorting_str_of o fst) entries) + else + []; + + val chunks = + (if null free_model then + [pretty_indent (Pretty.str "No free variables")] + else + chunks_of_entries sorting_str_of_term pretty_of_term_entry "" free_model) @ + chunks_of_entries sorting_str_of_term pretty_of_term_entry "Skolem constant" skolem_model @ + chunks_of_entries sorting_str_of_term pretty_of_term_entry "Underspecified constant" + pat_incomplete_model' @ + (if Config.get ctxt show_consts then + chunks_of_entries sorting_str_of_term pretty_of_term_entry "Fully specified constant" + pat_complete_model + else + []) @ + chunks_of_entries sorting_str_of_typ pretty_of_typ_entry "Type" type_model; + in + Pretty.chunks chunks + end; + +end; diff -r 14571c9e1d50 -r 6273d4c8325b src/HOL/Nunchaku/Tools/nunchaku_model.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Nunchaku/Tools/nunchaku_model.ML Mon Oct 24 22:42:07 2016 +0200 @@ -0,0 +1,284 @@ +(* Title: HOL/Nunchaku/Tools/nunchaku_model.ML + Author: Jasmin Blanchette, Inria Nancy, LORIA, MPII + Copyright 2015, 2016 + +Abstract syntax tree for Nunchaku models. +*) + +signature NUNCHAKU_MODEL = +sig + type ident = Nunchaku_Problem.ident + type ty = Nunchaku_Problem.ty + type tm = Nunchaku_Problem.tm + type name_pool = Nunchaku_Problem.name_pool + + type ty_entry = ty * tm list + type tm_entry = tm * tm + + type nun_model = + {type_model: ty_entry list, + const_model: tm_entry list, + skolem_model: tm_entry list} + + val str_of_nun_model: nun_model -> string + + val allocate_ugly: name_pool -> string * string -> string * name_pool + + val ugly_nun_model: name_pool -> nun_model -> nun_model + + datatype token = + Ident of ident + | Symbol of ident + | Atom of ident * int + | End_of_Stream + + val parse_tok: ''a -> ''a list -> ''a * ''a list + val parse_ident: token list -> ident * token list + val parse_id: ident -> token list -> token * token list + val parse_sym: ident -> token list -> token * token list + val parse_atom: token list -> (ident * int) * token list + val nun_model_of_str: string -> nun_model +end; + +structure Nunchaku_Model : NUNCHAKU_MODEL = +struct + +open Nunchaku_Problem; + +type ty_entry = ty * tm list; +type tm_entry = tm * tm; + +type nun_model = + {type_model: ty_entry list, + const_model: tm_entry list, + skolem_model: tm_entry list}; + +val nun_SAT = str_of_ident "SAT"; + +fun str_of_ty_entry (ty, tms) = + "type " ^ str_of_ty ty ^ " := {" ^ commas (map str_of_tm tms) ^ "}."; + +fun str_of_tm_entry (tm, value) = + "val " ^ str_of_tm tm ^ " := " ^ str_of_tm value ^ "."; + +fun str_of_nun_model {type_model, const_model, skolem_model} = + map str_of_ty_entry type_model @ "" :: map str_of_tm_entry const_model @ "" :: + map str_of_tm_entry skolem_model + |> cat_lines; + +fun fold_map_ty_entry_idents f (ty, atoms) = + fold_map_ty_idents f ty + ##>> fold_map (fold_map_tm_idents f) atoms; + +fun fold_map_tm_entry_idents f (tm, value) = + fold_map_tm_idents f tm + ##>> fold_map_tm_idents f value; + +fun fold_map_nun_model_idents f {type_model, const_model, skolem_model} = + fold_map (fold_map_ty_entry_idents f) type_model + ##>> fold_map (fold_map_tm_entry_idents f) const_model + ##>> fold_map (fold_map_tm_entry_idents f) skolem_model + #>> (fn ((type_model, const_model), skolem_model) => + {type_model = type_model, const_model = const_model, skolem_model = skolem_model}); + +fun swap_name_pool ({nice_of_ugly, ugly_of_nice} : name_pool) = + {nice_of_ugly = ugly_of_nice, ugly_of_nice = nice_of_ugly}; + +fun allocate_ugly pool (nice, ugly_sugg) = + allocate_nice (swap_name_pool pool) (nice, ugly_sugg) ||> swap_name_pool; + +fun ugly_ident nice (pool as {ugly_of_nice, ...}) = + (case Symtab.lookup ugly_of_nice nice of + NONE => allocate_ugly pool (nice, nice) + | SOME ugly => (ugly, pool)); + +fun ugly_nun_model pool model = + fst (fold_map_nun_model_idents ugly_ident model pool); + +datatype token = + Ident of ident +| Symbol of ident +| Atom of ident * int +| End_of_Stream; + +val rev_str = String.implode o rev o String.explode; + +fun atom_of_str s = + (case first_field "_" (rev_str s) of + SOME (rev_suf, rev_pre) => + let + val pre = rev_str rev_pre; + val suf = rev_str rev_suf; + in + (case Int.fromString suf of + SOME j => Atom (ident_of_str pre, j) + | NONE => raise Fail "ill-formed atom") + end + | NONE => raise Fail "ill-formed atom"); + +fun is_alnum_etc_char c = Char.isAlphaNum c orelse c = #"_" orelse c = #"/"; + +val multi_ids = + [nun_arrow, nun_assign, nun_conj, nun_disj, nun_implies, nun_unparsable, nun_irrelevant]; + +val nun_anon_fun_prefix_exploded = String.explode nun_anon_fun_prefix; +val [nun_dollar_char] = String.explode nun_dollar; + +fun next_token [] = (End_of_Stream, []) + | next_token (c :: cs) = + if Char.isSpace c then + next_token cs + else if c = nun_dollar_char then + let val n = find_index (not o is_alnum_etc_char) cs in + (if n = ~1 then (cs, []) else chop n cs) + |>> (String.implode + #> (if is_prefix (op =) nun_anon_fun_prefix_exploded cs then ident_of_str #> Ident + else atom_of_str)) + end + else if is_alnum_etc_char c then + let val n = find_index (not o is_alnum_etc_char) cs in + (if n = ~1 then (cs, []) else chop n cs) + |>> (cons c #> String.implode #> ident_of_str #> Ident) + end + else + let + fun next_multi id = + let + val s = str_of_ident id; + val n = String.size s - 1; + in + if c = String.sub (s, 0) andalso + is_prefix (op =) (String.explode (String.substring (s, 1, n))) cs then + SOME (Symbol id, drop n cs) + else + NONE + end; + in + (case get_first next_multi multi_ids of + SOME res => res + | NONE => (Symbol (ident_of_str (String.str c)), cs)) + end; + +val tokenize = + let + fun toks cs = + (case next_token cs of + (End_of_Stream, []) => [] + | (tok, cs') => tok :: toks cs'); + in + toks o String.explode + end; + +fun parse_enum sep scan = scan ::: Scan.repeat (sep |-- scan); + +fun parse_tok tok = Scan.one (curry (op =) tok); + +val parse_ident = Scan.some (try (fn Ident id => id)); +val parse_id = parse_tok o Ident; +val parse_sym = parse_tok o Symbol; +val parse_atom = Scan.some (try (fn Atom id_j => id_j)); + +val confusing_ids = [nun_else, nun_then, nun_with]; + +val parse_confusing_id = Scan.one (fn Ident id => member (op =) confusing_ids id | _ => false); + +fun parse_ty toks = + (parse_ty_arg -- Scan.option (parse_sym nun_arrow -- parse_ty) + >> (fn (ty, NONE) => ty + | (lhs, SOME (Symbol id, rhs)) => NType (id, [lhs, rhs]))) toks +and parse_ty_arg toks = + (parse_ident >> (rpair [] #> NType) + || parse_sym nun_lparen |-- parse_ty --| parse_sym nun_rparen) toks; + +val parse_choice_or_unique = + (parse_tok (Ident nun_choice) || parse_tok (Ident nun_unique) + || parse_tok (Ident nun_unique_unsafe)) + -- parse_ty_arg + >> (fn (Ident id, ty) => NConst (id, [ty], mk_arrows_ty ([ty, prop_ty], ty))); + +fun parse_tm toks = + (parse_id nun_lambda |-- Scan.repeat parse_arg --| parse_sym nun_dot -- parse_tm >> nabss + || parse_id nun_mu |-- parse_arg --| parse_sym nun_dot -- parse_tm + >> (fn (var, body) => + let val ty = safe_ty_of body in + NApp (NConst (nun_mu, [ty], mk_arrow_ty (mk_arrow_ty (ty, ty), ty)), NAbs (var, body)) + end) + || parse_id nun_if |-- parse_tm --| parse_id nun_then -- parse_tm --| parse_id nun_else + -- parse_tm + >> (fn ((cond, th), el) => + let val ty = safe_ty_of th in + napps (NConst (nun_if, [ty], mk_arrows_ty ([prop_ty, ty, ty], ty)), [cond, th, el]) + end) + || parse_implies) toks +and parse_implies toks = + (parse_disj -- Scan.option (parse_sym nun_implies -- parse_implies) + >> (fn (tm, NONE) => tm + | (lhs, SOME (Symbol id, rhs)) => napps (NConst (id, [], dummy_ty), [lhs, rhs]))) toks +and parse_disj toks = + (parse_conj -- Scan.option (parse_sym nun_disj -- parse_disj) + >> (fn (tm, NONE) => tm + | (lhs, SOME (Symbol id, rhs)) => napps (NConst (id, [], dummy_ty), [lhs, rhs]))) toks +and parse_conj toks = + (parse_equals -- Scan.option (parse_sym nun_conj -- parse_conj) + >> (fn (tm, NONE) => tm + | (lhs, SOME (Symbol id, rhs)) => napps (NConst (id, [], dummy_ty), [lhs, rhs]))) toks +and parse_equals toks = + (parse_comb -- Scan.option (parse_sym nun_equals -- parse_comb) + >> (fn (tm, NONE) => tm + | (lhs, SOME (Symbol id, rhs)) => napps (NConst (id, [], dummy_ty), [lhs, rhs]))) toks +and parse_comb toks = + (parse_arg -- Scan.repeat (Scan.unless parse_confusing_id parse_arg) >> napps) toks +and parse_arg toks = + (parse_choice_or_unique + || parse_ident >> (fn id => NConst (id, [], dummy_ty)) + || parse_sym nun_irrelevant + |-- Scan.option (parse_sym nun_lparen |-- parse_tm --| parse_sym nun_rparen) (* FIXME *) + >> (fn _ => NConst (nun_irrelevant, [], dummy_ty)) + || parse_sym nun_unparsable |-- parse_ty >> (fn ty => NConst (nun_unparsable, [], ty)) + || parse_sym nun_lparen |-- parse_tm -- Scan.option (parse_sym nun_colon |-- parse_ty) + --| parse_sym nun_rparen + >> (fn (NConst (id, [], _), SOME ty) => NConst (id, [], ty) + | (tm, _) => tm) + || parse_atom >> (fn (id, j) => NAtom (j, NType (id, [])))) toks; + +val parse_witness_name = + parse_ident >> (fn id => NConst (hd (space_explode "/" id), [], dummy_ty)); + +val parse_witness = + parse_id nun__witness_of |-- parse_sym nun_lparen |-- (parse_id nun_forall || parse_id nun_exists) + |-- Scan.option (parse_sym nun_lparen) |-- parse_witness_name + --| Scan.repeat (Scan.one (curry (op <>) (Symbol nun_assign))); + +datatype entry = + Type_Entry of ty_entry +| Skolem_Entry of tm_entry +| Const_Entry of tm_entry; + +val parse_entry = + (parse_id nun_type |-- parse_ty --| parse_sym nun_assign --| parse_sym nun_lbrace -- + parse_enum (parse_sym nun_comma) parse_tm --| parse_sym nun_rbrace + >> Type_Entry + || parse_id nun_val |-- parse_witness --| parse_sym nun_assign -- parse_tm >> Skolem_Entry + || parse_id nun_val |-- parse_tm --| parse_sym nun_assign -- parse_tm >> Const_Entry) + --| parse_sym nun_dot; + +val parse_model = + parse_id nun_SAT |-- parse_sym nun_colon |-- parse_sym nun_lbrace |-- Scan.repeat parse_entry + --| parse_sym nun_rbrace; + +fun add_entry entry ({type_model, const_model, skolem_model} : nun_model) = + (case entry of + Type_Entry e => + {type_model = e :: type_model, const_model = const_model, skolem_model = skolem_model} + | Skolem_Entry e => + {type_model = type_model, const_model = const_model, skolem_model = e :: skolem_model} + | Const_Entry e => + {type_model = type_model, const_model = e :: const_model, skolem_model = skolem_model}); + +fun nun_model_of_str str = + let val (entries, _) = parse_model (tokenize str) in + {type_model = [], const_model = [], skolem_model = []} + |> fold_rev add_entry entries + end; + +end; diff -r 14571c9e1d50 -r 6273d4c8325b src/HOL/Nunchaku/Tools/nunchaku_problem.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Nunchaku/Tools/nunchaku_problem.ML Mon Oct 24 22:42:07 2016 +0200 @@ -0,0 +1,791 @@ +(* Title: HOL/Nunchaku/Tools/nunchaku_problem.ML + Author: Jasmin Blanchette, Inria Nancy, LORIA, MPII + Copyright 2015, 2016 + +Abstract syntax tree for Nunchaku problems. +*) + +signature NUNCHAKU_PROBLEM = +sig + eqtype ident + + datatype ty = + NType of ident * ty list + + datatype tm = + NAtom of int * ty + | NConst of ident * ty list * ty + | NAbs of tm * tm + | NMatch of tm * (ident * tm list * tm) list + | NApp of tm * tm + + type nun_type_spec = + {abs_ty: ty, + rep_ty: ty, + wrt: tm, + abs: tm, + rep: tm} + + type nun_ctr_spec = + {ctr: tm, + arg_tys: ty list} + + type nun_co_data_spec = + {ty: ty, + ctrs: nun_ctr_spec list} + + type nun_const_spec = + {const: tm, + props: tm list} + + type nun_consts_spec = + {consts: tm list, + props: tm list} + + datatype nun_command = + NTVal of ty * (int option * int option) + | NCopy of nun_type_spec + | NQuotient of nun_type_spec + | NData of nun_co_data_spec list + | NCodata of nun_co_data_spec list + | NVal of tm * ty + | NPred of bool * nun_const_spec list + | NCopred of nun_const_spec list + | NRec of nun_const_spec list + | NSpec of nun_consts_spec + | NAxiom of tm + | NGoal of tm + | NEval of tm + + type nun_problem = + {commandss: nun_command list list, + sound: bool, + complete: bool} + + type name_pool = + {nice_of_ugly: string Symtab.table, + ugly_of_nice: string Symtab.table} + + val nun_abstract: string + val nun_and: string + val nun_anon_fun_prefix: string + val nun_arrow: string + val nun_asserting: string + val nun_assign: string + val nun_at: string + val nun_axiom: string + val nun_bar: string + val nun_choice: string + val nun_codata: string + val nun_colon: string + val nun_comma: string + val nun_concrete: string + val nun_conj: string + val nun_copred: string + val nun_copy: string + val nun_data: string + val nun_disj: string + val nun_dollar: string + val nun_dot: string + val nun_dummy: string + val nun_else: string + val nun_end: string + val nun_equals: string + val nun_eval: string + val nun_exists: string + val nun_false: string + val nun_forall: string + val nun_goal: string + val nun_hash: string + val nun_if: string + val nun_implies: string + val nun_irrelevant: string + val nun_lambda: string + val nun_lbrace: string + val nun_lbracket: string + val nun_lparen: string + val nun_match: string + val nun_mu: string + val nun_not: string + val nun_pred: string + val nun_prop: string + val nun_quotient: string + val nun_rbrace: string + val nun_rbracket: string + val nun_rec: string + val nun_rparen: string + val nun_semicolon: string + val nun_spec: string + val nun_then: string + val nun_true: string + val nun_type: string + val nun_unparsable: string + val nun_unique: string + val nun_unique_unsafe: string + val nun_val: string + val nun_wf: string + val nun_with: string + val nun_wrt: string + val nun__witness_of: string + + val ident_of_str: string -> ident + val str_of_ident: ident -> string + val encode_args: string list -> string + val nun_const_of_str: string list -> string -> ident + val nun_tconst_of_str: string list -> string -> ident + val nun_free_of_str: string -> ident + val nun_tfree_of_str: string -> ident + val nun_var_of_str: string -> ident + val str_of_nun_const: ident -> string list * string + val str_of_nun_tconst: ident -> string list * string + val str_of_nun_free: ident -> string + val str_of_nun_tfree: ident -> string + val str_of_nun_var: ident -> string + + val dummy_ty: ty + val prop_ty: ty + val mk_arrow_ty: ty * ty -> ty + val mk_arrows_ty: ty list * ty -> ty + val nabss: tm list * tm -> tm + val napps: tm * tm list -> tm + + val ty_of: tm -> ty + val safe_ty_of: tm -> ty + + val fold_map_ty_idents: (string -> 'a -> string * 'a) -> ty -> 'a -> ty * 'a + val fold_map_tm_idents: (string -> 'a -> string * 'a) -> tm -> 'a -> tm * 'a + val fold_map_nun_command_idents: (string -> 'a -> string * 'a) -> nun_command -> 'a -> + nun_command * 'a + val fold_map_nun_problem_idents: (string -> 'a -> string * 'a) -> nun_problem -> 'a -> + nun_problem * 'a + + val allocate_nice: name_pool -> string * string -> string * name_pool + + val rcomb_tms: tm list -> tm -> tm + val abs_tms: tm list -> tm -> tm + val beta_reduce_tm: tm -> tm + val eta_expandN_tm: int -> tm -> tm + val eta_expand_builtin_tm: tm -> tm + + val str_of_ty: ty -> string + val str_of_tm: tm -> string + val str_of_tmty: tm -> string + + val nice_nun_problem: nun_problem -> nun_problem * name_pool + val str_of_nun_problem: nun_problem -> string +end; + +structure Nunchaku_Problem : NUNCHAKU_PROBLEM = +struct + +open Nunchaku_Util; + +type ident = string; + +datatype ty = + NType of ident * ty list; + +datatype tm = + NAtom of int * ty +| NConst of ident * ty list * ty +| NAbs of tm * tm +| NMatch of tm * (ident * tm list * tm) list +| NApp of tm * tm; + +type nun_type_spec = + {abs_ty: ty, + rep_ty: ty, + wrt: tm, + abs: tm, + rep: tm}; + +type nun_ctr_spec = + {ctr: tm, + arg_tys: ty list}; + +type nun_co_data_spec = + {ty: ty, + ctrs: nun_ctr_spec list}; + +type nun_const_spec = + {const: tm, + props: tm list}; + +type nun_consts_spec = + {consts: tm list, + props: tm list}; + +datatype nun_command = + NTVal of ty * (int option * int option) +| NCopy of nun_type_spec +| NQuotient of nun_type_spec +| NData of nun_co_data_spec list +| NCodata of nun_co_data_spec list +| NVal of tm * ty +| NPred of bool * nun_const_spec list +| NCopred of nun_const_spec list +| NRec of nun_const_spec list +| NSpec of nun_consts_spec +| NAxiom of tm +| NGoal of tm +| NEval of tm; + +type nun_problem = + {commandss: nun_command list list, + sound: bool, + complete: bool}; + +type name_pool = + {nice_of_ugly: string Symtab.table, + ugly_of_nice: string Symtab.table}; + +val nun_abstract = "abstract"; +val nun_and = "and"; +val nun_anon_fun_prefix = "anon_fun_"; +val nun_arrow = "->"; +val nun_asserting = "asserting"; +val nun_assign = ":="; +val nun_at = "@"; +val nun_axiom = "axiom"; +val nun_bar = "|"; +val nun_choice = "choice"; +val nun_codata = "codata"; +val nun_colon = ":"; +val nun_comma = ","; +val nun_concrete = "concrete"; +val nun_conj = "&&"; +val nun_copred = "copred"; +val nun_copy = "copy"; +val nun_data = "data"; +val nun_disj = "||"; +val nun_dollar = "$"; +val nun_dot = "."; +val nun_dummy = "_"; +val nun_else = "else"; +val nun_end = "end"; +val nun_equals = "="; +val nun_eval = "eval"; +val nun_exists = "exists"; +val nun_false = "false"; +val nun_forall = "forall"; +val nun_goal = "goal"; +val nun_hash = "#"; +val nun_if = "if"; +val nun_implies = "=>"; +val nun_irrelevant = "?__"; +val nun_lambda = "fun"; +val nun_lbrace = "{"; +val nun_lbracket = "["; +val nun_lparen = "("; +val nun_match = "match"; +val nun_mu = "mu"; +val nun_not = "~"; +val nun_pred = "pred"; +val nun_prop = "prop"; +val nun_quotient = "quotient"; +val nun_rbrace = "}"; +val nun_rbracket = "]"; +val nun_rec = "rec"; +val nun_rparen = ")"; +val nun_semicolon = ";"; +val nun_spec = "spec"; +val nun_then = "then"; +val nun_true = "true"; +val nun_type = "type"; +val nun_unique = "unique"; +val nun_unique_unsafe = "unique_unsafe"; +val nun_unparsable = "?__unparsable"; +val nun_val = "val"; +val nun_wf = "wf"; +val nun_with = "with"; +val nun_wrt = "wrt"; +val nun__witness_of = "_witness_of"; + +val nun_parens = enclose nun_lparen nun_rparen; + +fun nun_parens_if_space s = s |> String.isSubstring " " s ? nun_parens; + +fun str_of_nun_arg_list str_of_arg = + map (prefix " " o nun_parens_if_space o str_of_arg) #> space_implode ""; + +fun str_of_nun_and_list str_of_elem = + map str_of_elem #> space_implode ("\n" ^ nun_and ^ " "); + +val is_nun_const_quantifier = member (op =) [nun_forall, nun_exists]; +val is_nun_const_connective = member (op =) [nun_conj, nun_disj, nun_implies]; + +val nun_builtin_arity = + [(nun_asserting, 2), + (nun_conj, 2), + (nun_disj, 2), + (nun_equals, 2), + (nun_exists, 1), + (nun_false, 0), + (nun_forall, 1), + (nun_if, 3), + (nun_implies, 2), + (nun_not, 1), + (nun_true, 0)]; + +val arity_of_nun_builtin = AList.lookup (op =) nun_builtin_arity #> the_default 0; + +val nun_const_prefix = "c."; +val nun_free_prefix = "f."; +val nun_var_prefix = "v."; +val nun_tconst_prefix = "C."; +val nun_tfree_prefix = "F."; +val nun_custom_id_suffix = "_"; + +val ident_of_str = I : string -> ident; +val str_of_ident = I : ident -> string; + +val encode_args = enclose "(" ")" o commas; + +fun decode_args s = + let + fun delta #"(" = 1 + | delta #")" = ~1 + | delta _ = 0; + + fun dec 0 (#"(" :: #")" :: cs) _ = ([], String.implode cs) + | dec 0 (#"(" :: cs) [] = dec 1 cs [[]] + | dec 0 cs _ = ([], String.implode cs) + | dec _ [] _ = raise Fail ("ill-formed arguments in " ^ quote s) + | dec 1 (#")" :: cs) args = (rev (map (String.implode o rev) args), String.implode cs) + | dec 1 (#"," :: cs) args = dec 1 cs ([] :: args) + | dec n (c :: cs) (arg :: args) = dec (n + delta c) cs ((c :: arg) :: args); + in + dec 0 (String.explode s) [] + end; + +fun nun_const_of_str args = + suffix nun_custom_id_suffix #> prefix nun_const_prefix #> prefix (encode_args args); +fun nun_tconst_of_str args = + suffix nun_custom_id_suffix #> prefix nun_tconst_prefix #> prefix (encode_args args); + +val nun_free_of_str = suffix nun_custom_id_suffix #> prefix nun_free_prefix; +val nun_tfree_of_str = suffix nun_custom_id_suffix #> prefix nun_tfree_prefix; +val nun_var_of_str = suffix nun_custom_id_suffix #> prefix nun_var_prefix; +val str_of_nun_const = decode_args ##> unprefix nun_const_prefix ##> unsuffix nun_custom_id_suffix; +val str_of_nun_tconst = decode_args ##> unprefix nun_tconst_prefix ##> unsuffix nun_custom_id_suffix; +val str_of_nun_free = unprefix nun_free_prefix #> unsuffix nun_custom_id_suffix; +val str_of_nun_tfree = unprefix nun_tfree_prefix #> unsuffix nun_custom_id_suffix; +val str_of_nun_var = unprefix nun_var_prefix #> unsuffix nun_custom_id_suffix; + +fun index_name s 0 = s + | index_name s j = + let + val n = size s; + val m = n - 1; + in + String.substring (s, 0, m) ^ string_of_int j ^ String.substring (s, m, n - m) + end; + +val dummy_ty = NType (nun_dummy, []); +val prop_ty = NType (nun_prop, []); + +fun mk_arrow_ty (dom, ran) = NType (nun_arrow, [dom, ran]); +val mk_arrows_ty = Library.foldr mk_arrow_ty; + +val nabss = Library.foldr NAbs; +val napps = Library.foldl NApp; + +fun domain_ty (NType (_, [ty, _])) = ty + | domain_ty ty = ty; + +fun range_ty (NType (_, [_, ty])) = ty + | range_ty ty = ty; + +fun domain_tys 0 _ = [] + | domain_tys n ty = domain_ty ty :: domain_tys (n - 1) (range_ty ty); + +fun ty_of (NAtom (_, ty)) = ty + | ty_of (NConst (_, _, ty)) = ty + | ty_of (NAbs (var, body)) = mk_arrow_ty (ty_of var, ty_of body) + | ty_of (NMatch (_, (_, _, body1) :: _)) = ty_of body1 + | ty_of (NApp (const, _)) = range_ty (ty_of const); + +val safe_ty_of = try ty_of #> the_default dummy_ty; + +fun strip_nun_binders binder (app as NApp (NConst (id, _, _), NAbs (var, body))) = + if id = binder then + strip_nun_binders binder body + |>> cons var + else + ([], app) + | strip_nun_binders _ tm = ([], tm); + +fun fold_map_ty_idents f (NType (id, tys)) = + f id + ##>> fold_map (fold_map_ty_idents f) tys + #>> NType; + +fun fold_map_match_branch_idents f (id, vars, body) = + f id + ##>> fold_map (fold_map_tm_idents f) vars + ##>> fold_map_tm_idents f body + #>> Scan.triple1 +and fold_map_tm_idents f (NAtom (j, ty)) = + fold_map_ty_idents f ty + #>> curry NAtom j + | fold_map_tm_idents f (NConst (id, tys, ty)) = + f id + ##>> fold_map (fold_map_ty_idents f) tys + ##>> fold_map_ty_idents f ty + #>> (Scan.triple1 #> NConst) + | fold_map_tm_idents f (NAbs (var, body)) = + fold_map_tm_idents f var + ##>> fold_map_tm_idents f body + #>> NAbs + | fold_map_tm_idents f (NMatch (obj, branches)) = + fold_map_tm_idents f obj + ##>> fold_map (fold_map_match_branch_idents f) branches + #>> NMatch + | fold_map_tm_idents f (NApp (const, arg)) = + fold_map_tm_idents f const + ##>> fold_map_tm_idents f arg + #>> NApp; + +fun fold_map_nun_type_spec_idents f {abs_ty, rep_ty, wrt, abs, rep} = + fold_map_ty_idents f abs_ty + ##>> fold_map_ty_idents f rep_ty + ##>> fold_map_tm_idents f wrt + ##>> fold_map_tm_idents f abs + ##>> fold_map_tm_idents f rep + #>> (fn ((((abs_ty, rep_ty), wrt), abs), rep) => + {abs_ty = abs_ty, rep_ty = rep_ty, wrt = wrt, abs = abs, rep = rep}); + +fun fold_map_nun_ctr_spec_idents f {ctr, arg_tys} = + fold_map_tm_idents f ctr + ##>> fold_map (fold_map_ty_idents f) arg_tys + #>> (fn (ctr, arg_tys) => {ctr = ctr, arg_tys = arg_tys}); + +fun fold_map_nun_co_data_spec_idents f {ty, ctrs} = + fold_map_ty_idents f ty + ##>> fold_map (fold_map_nun_ctr_spec_idents f) ctrs + #>> (fn (ty, ctrs) => {ty = ty, ctrs = ctrs}); + +fun fold_map_nun_const_spec_idents f {const, props} = + fold_map_tm_idents f const + ##>> fold_map (fold_map_tm_idents f) props + #>> (fn (const, props) => {const = const, props = props}); + +fun fold_map_nun_consts_spec_idents f {consts, props} = + fold_map (fold_map_tm_idents f) consts + ##>> fold_map (fold_map_tm_idents f) props + #>> (fn (consts, props) => {consts = consts, props = props}); + +fun fold_map_nun_command_idents f (NTVal (ty, cards)) = + fold_map_ty_idents f ty + #>> (rpair cards #> NTVal) + | fold_map_nun_command_idents f (NCopy spec) = + fold_map_nun_type_spec_idents f spec + #>> NCopy + | fold_map_nun_command_idents f (NQuotient spec) = + fold_map_nun_type_spec_idents f spec + #>> NQuotient + | fold_map_nun_command_idents f (NData specs) = + fold_map (fold_map_nun_co_data_spec_idents f) specs + #>> NData + | fold_map_nun_command_idents f (NCodata specs) = + fold_map (fold_map_nun_co_data_spec_idents f) specs + #>> NCodata + | fold_map_nun_command_idents f (NVal (tm, ty)) = + fold_map_tm_idents f tm + ##>> fold_map_ty_idents f ty + #>> NVal + | fold_map_nun_command_idents f (NPred (wf, specs)) = + fold_map (fold_map_nun_const_spec_idents f) specs + #>> curry NPred wf + | fold_map_nun_command_idents f (NCopred specs) = + fold_map (fold_map_nun_const_spec_idents f) specs + #>> NCopred + | fold_map_nun_command_idents f (NRec specs) = + fold_map (fold_map_nun_const_spec_idents f) specs + #>> NRec + | fold_map_nun_command_idents f (NSpec spec) = + fold_map_nun_consts_spec_idents f spec + #>> NSpec + | fold_map_nun_command_idents f (NAxiom tm) = + fold_map_tm_idents f tm + #>> NAxiom + | fold_map_nun_command_idents f (NGoal tm) = + fold_map_tm_idents f tm + #>> NGoal + | fold_map_nun_command_idents f (NEval tm) = + fold_map_tm_idents f tm + #>> NEval; + +fun fold_map_nun_problem_idents f ({commandss, sound, complete} : nun_problem) = + fold_map (fold_map (fold_map_nun_command_idents f)) commandss + #>> (fn commandss' => {commandss = commandss', sound = sound, complete = complete}); + +fun dest_rassoc_args oper arg0 rest = + (case rest of + NApp (NApp (oper', arg1), rest') => + if oper' = oper then arg0 :: dest_rassoc_args oper arg1 rest' else [arg0, rest] + | _ => [arg0, rest]); + +fun replace_tm from to = + let + (* This code assumes all enclosing binders bind distinct variables and bound variables are + distinct from any other variables. *) + fun repl_br (id, vars, body) = (id, map repl vars, repl body) + and repl (NApp (const, arg)) = NApp (repl const, repl arg) + | repl (NAbs (var, body)) = NAbs (var, repl body) + | repl (NMatch (obj, branches)) = NMatch (repl obj, map repl_br branches) + | repl tm = if tm = from then to else tm; + in + repl + end; + +val rcomb_tms = fold (fn arg => fn func => NApp (func, arg)); +val abs_tms = fold_rev (curry NAbs); + +fun fresh_var_names_wrt_tm n tm = + let + fun max_var_br (_, vars, body) = fold max_var (body :: vars) + and max_var (NAtom _) = I + | max_var (NConst (id, _, _)) = + (fn max => if String.isPrefix nun_var_prefix id andalso size id > size max then id else max) + | max_var (NApp (func, arg)) = fold max_var [func, arg] + | max_var (NAbs (var, body)) = fold max_var [var, body] + | max_var (NMatch (obj, branches)) = max_var obj #> fold max_var_br branches; + + val dummy_name = nun_var_of_str Name.uu; + val max_name = max_var tm dummy_name; + in + map (index_name max_name) (1 upto n) + end; + +fun beta_reduce_tm (NApp (NAbs (var, body), arg)) = beta_reduce_tm (replace_tm var arg body) + | beta_reduce_tm (NApp (const, arg)) = + (case beta_reduce_tm const of + const' as NAbs _ => beta_reduce_tm (NApp (const', arg)) + | const' => NApp (const', beta_reduce_tm arg)) + | beta_reduce_tm (NAbs (var, body)) = NAbs (var, beta_reduce_tm body) + | beta_reduce_tm (NMatch (obj, branches)) = + NMatch (beta_reduce_tm obj, map (@{apply 3(3)} beta_reduce_tm) branches) + | beta_reduce_tm tm = tm; + +fun eta_expandN_tm 0 tm = tm + | eta_expandN_tm n tm = + let + val var_names = fresh_var_names_wrt_tm n tm; + val arg_tys = domain_tys n (ty_of tm); + val vars = map2 (fn id => fn ty => NConst (id, [], ty)) var_names arg_tys; + in + abs_tms vars (rcomb_tms vars tm) + end; + +val eta_expand_builtin_tm = + let + fun expand_quant_arg (NAbs (var, body)) = NAbs (var, expand_quant_arg body) + | expand_quant_arg (NMatch (obj, branches)) = + NMatch (obj, map (@{apply 3(3)} expand_quant_arg) branches) + | expand_quant_arg (tm as NApp (_, NAbs _)) = tm + | expand_quant_arg (NApp (quant, arg)) = NApp (quant, eta_expandN_tm 1 arg) + | expand_quant_arg tm = tm; + + fun expand args (NApp (func, arg)) = expand (expand [] arg :: args) func + | expand args (func as NConst (id, _, _)) = + let val missing = Int.max (0, arity_of_nun_builtin id - length args) in + rcomb_tms args func + |> eta_expandN_tm missing + |> is_nun_const_quantifier id ? expand_quant_arg + end + | expand args (func as NAtom _) = rcomb_tms args func + | expand args (NAbs (var, body)) = rcomb_tms args (NAbs (var, expand [] body)) + | expand args (NMatch (obj, branches)) = + rcomb_tms args (NMatch (obj, map (@{apply 3(3)} (expand [])) branches)); + in + expand [] + end; + +val str_of_ty = + let + fun str_of maybe_parens (NType (id, tys)) = + if id = nun_arrow then + (case tys of + [ty, ty'] => maybe_parens (str_of nun_parens ty ^ " " ^ nun_arrow ^ " " ^ str_of I ty')) + else + id ^ str_of_nun_arg_list (str_of I) tys + in + str_of I + end; + +val (str_of_tmty, str_of_tm) = + let + fun is_triv_head (NConst (id, _, _)) = (arity_of_nun_builtin id = 0) + | is_triv_head (NAtom _) = true + | is_triv_head (NApp (const, _)) = is_triv_head const + | is_triv_head (NAbs _) = false + | is_triv_head (NMatch _) = false; + + fun str_of_at_const id tys = + nun_at ^ str_of_ident id ^ str_of_nun_arg_list str_of_ty tys; + + fun str_of_app ty_opt const arg = + let + val ty_opt' = + try (Option.map (fn ty => mk_arrow_ty (ty_of arg, ty))) ty_opt + |> the_default NONE; + in + (str_of ty_opt' const |> (case const of NAbs _ => nun_parens | _ => I)) ^ + str_of_nun_arg_list (str_of NONE) [arg] + end + and str_of_br ty_opt (id, vars, body) = + " " ^ nun_bar ^ " " ^ id ^ space_implode "" (map (prefix " " o str_of NONE) vars) ^ " " ^ + nun_arrow ^ " " ^ str_of ty_opt body + and str_of_tmty tm = + let val ty = ty_of tm in + str_of (SOME ty) tm ^ " " ^ nun_colon ^ " " ^ str_of_ty ty + end + and str_of _ (NAtom (j, _)) = nun_dollar ^ string_of_int j + | str_of _ (NConst (id, [], _)) = str_of_ident id + | str_of (SOME ty0) (NConst (id, tys, ty)) = + if ty = ty0 then str_of_ident id else str_of_at_const id tys + | str_of _ (NConst (id, tys, _)) = str_of_at_const id tys + | str_of ty_opt (NAbs (var, body)) = + nun_lambda ^ " " ^ + (case ty_opt of + SOME ty => str_of (SOME (domain_ty ty)) + | NONE => nun_parens o str_of_tmty) var ^ + nun_dot ^ " " ^ str_of (Option.map range_ty ty_opt) body + | str_of ty_opt (NMatch (obj, branches)) = + nun_match ^ " " ^ str_of NONE obj ^ " " ^ nun_with ^ " " ^ + space_implode "" (map (str_of_br ty_opt) branches) ^ " " ^ nun_end + | str_of ty_opt (app as NApp (func, argN)) = + (case (func, argN) of + (NApp (oper as NConst (id, _, _), arg1), arg2) => + if id = nun_asserting then + str_of ty_opt arg1 ^ " " ^ nun_asserting ^ " " ^ str_of (SOME prop_ty) arg2 + |> nun_parens + else if id = nun_equals then + (str_of NONE arg1 |> not (is_triv_head arg1) ? nun_parens) ^ " " ^ id ^ " " ^ + (str_of (try ty_of arg2) arg2 |> not (is_triv_head arg2) ? nun_parens) + else if is_nun_const_connective id then + let val args = dest_rassoc_args oper arg1 arg2 in + space_implode (" " ^ id ^ " ") + (map (fn arg => str_of NONE arg |> not (is_triv_head arg) ? nun_parens) args) + end + else + str_of_app ty_opt func argN + | (NApp (NApp (NConst (id, _, _), arg1), arg2), arg3) => + if id = nun_if then + nun_if ^ " " ^ str_of NONE arg1 ^ " " ^ nun_then ^ " " ^ str_of NONE arg2 ^ " " ^ + nun_else ^ " " ^ str_of NONE arg3 + |> nun_parens + else + str_of_app ty_opt func argN + | (NConst (id, _, _), NAbs _) => + if is_nun_const_quantifier id then + let val (vars, body) = strip_nun_binders id app in + id ^ " " ^ space_implode " " (map (nun_parens o str_of_tmty) vars) ^ nun_dot ^ " " ^ + str_of NONE body + end + else + str_of_app ty_opt func argN + | _ => str_of_app ty_opt func argN); + in + (str_of_tmty, str_of NONE) + end; + +val empty_name_pool = {nice_of_ugly = Symtab.empty, ugly_of_nice = Symtab.empty}; + +val nice_of_ugly_suggestion = + unascii_of #> Long_Name.base_name #> ascii_of #> unsuffix nun_custom_id_suffix + #> (fn s => if s = "" orelse not (Char.isAlpha (String.sub (s, 0))) then "x" ^ s else s); + +fun allocate_nice ({nice_of_ugly, ugly_of_nice} : name_pool) (ugly, nice_sugg0) = + let + fun alloc j = + let val nice_sugg = index_name nice_sugg0 j in + (case Symtab.lookup ugly_of_nice nice_sugg of + NONE => + (nice_sugg, + {nice_of_ugly = Symtab.update_new (ugly, nice_sugg) nice_of_ugly, + ugly_of_nice = Symtab.update_new (nice_sugg, ugly) ugly_of_nice}) + | SOME _ => alloc (j + 1)) + end; + in + alloc 0 + end; + +fun nice_ident ugly (pool as {nice_of_ugly, ...}) = + if String.isSuffix nun_custom_id_suffix ugly then + (case Symtab.lookup nice_of_ugly ugly of + NONE => allocate_nice pool (ugly, nice_of_ugly_suggestion ugly) + | SOME nice => (nice, pool)) + else + (ugly, pool); + +fun nice_nun_problem problem = + fold_map_nun_problem_idents nice_ident problem empty_name_pool; + +fun str_of_tval (NType (id, tys)) = + str_of_ident id ^ " " ^ nun_colon ^ " " ^ + fold (K (prefix (nun_type ^ " " ^ nun_arrow ^ " "))) tys nun_type; + +fun is_triv_wrt (NAbs (_, body)) = is_triv_wrt body + | is_triv_wrt (NConst (id, _, _)) = (id = nun_true) + | is_triv_wrt _ = false; + +fun str_of_nun_type_spec {abs_ty, rep_ty, wrt, abs, rep} = + str_of_ty abs_ty ^ " " ^ nun_assign ^ " " ^ str_of_ty rep_ty ^ + (if is_triv_wrt wrt then "" else "\n " ^ nun_wrt ^ " " ^ str_of_tm wrt) ^ + "\n " ^ nun_abstract ^ " " ^ str_of_tm abs ^ "\n " ^ nun_concrete ^ " " ^ str_of_tm rep; + +fun str_of_nun_ctr_spec {ctr, arg_tys} = + str_of_tm ctr ^ str_of_nun_arg_list str_of_ty arg_tys; + +fun str_of_nun_co_data_spec {ty, ctrs} = + str_of_ty ty ^ " " ^ nun_assign ^ "\n " ^ + space_implode ("\n" ^ nun_bar ^ " ") (map str_of_nun_ctr_spec ctrs); + +fun str_of_nun_const_spec {const, props} = + str_of_tmty const ^ " " ^ nun_assign ^ "\n " ^ + space_implode (nun_semicolon ^ "\n ") (map str_of_tm props); + +fun str_of_nun_consts_spec {consts, props} = + space_implode (" " ^ nun_and ^ "\n ") (map str_of_tmty consts) ^ " " ^ nun_assign ^ "\n " ^ + space_implode (nun_semicolon ^ "\n ") (map str_of_tm props); + +fun str_of_nun_cards_suffix (NONE, NONE) = "" + | str_of_nun_cards_suffix (c1, c2) = + let + val s1 = Option.map (prefix "min_card " o signed_string_of_int) c1; + val s2 = Option.map (prefix "max_card " o signed_string_of_int) c2; + in + enclose " [" "]" (space_implode ", " (map_filter I [s1, s2])) + end; + +fun str_of_nun_command (NTVal (ty, cards)) = + nun_val ^ " " ^ str_of_tval ty ^ str_of_nun_cards_suffix cards + | str_of_nun_command (NCopy spec) = nun_copy ^ " " ^ str_of_nun_type_spec spec + | str_of_nun_command (NQuotient spec) = nun_quotient ^ " " ^ str_of_nun_type_spec spec + | str_of_nun_command (NData specs) = + nun_data ^ " " ^ str_of_nun_and_list str_of_nun_co_data_spec specs + | str_of_nun_command (NCodata specs) = + nun_codata ^ " " ^ str_of_nun_and_list str_of_nun_co_data_spec specs + | str_of_nun_command (NVal (tm, ty)) = + nun_val ^ " " ^ str_of_tm tm ^ " " ^ nun_colon ^ " " ^ str_of_ty ty + | str_of_nun_command (NPred (wf, specs)) = + nun_pred ^ " " ^ (if wf then nun_lbracket ^ nun_wf ^ nun_rbracket ^ " " else "") ^ + str_of_nun_and_list str_of_nun_const_spec specs + | str_of_nun_command (NCopred specs) = + nun_copred ^ " " ^ str_of_nun_and_list str_of_nun_const_spec specs + | str_of_nun_command (NRec specs) = + nun_rec ^ " " ^ str_of_nun_and_list str_of_nun_const_spec specs + | str_of_nun_command (NSpec spec) = nun_spec ^ " " ^ str_of_nun_consts_spec spec + | str_of_nun_command (NAxiom tm) = nun_axiom ^ " " ^ str_of_tm tm + | str_of_nun_command (NGoal tm) = nun_goal ^ " " ^ str_of_tm tm + | str_of_nun_command (NEval tm) = nun_hash ^ " " ^ nun_eval ^ " " ^ str_of_tm tm; + +fun str_of_nun_problem {commandss, sound, complete} = + map (cat_lines o map (suffix nun_dot o str_of_nun_command)) commandss + |> space_implode "\n\n" |> suffix "\n" + |> prefix (nun_hash ^ " " ^ (if sound then "sound" else "unsound") ^ "\n") + |> prefix (nun_hash ^ " " ^ (if complete then "complete" else "incomplete") ^ "\n"); + +end; diff -r 14571c9e1d50 -r 6273d4c8325b src/HOL/Nunchaku/Tools/nunchaku_reconstruct.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Nunchaku/Tools/nunchaku_reconstruct.ML Mon Oct 24 22:42:07 2016 +0200 @@ -0,0 +1,244 @@ +(* Title: HOL/Nunchaku/Tools/nunchaku_reconstruct.ML + Author: Jasmin Blanchette, Inria Nancy, LORIA, MPII + Copyright 2015, 2016 + +Reconstruction of Nunchaku models in Isabelle/HOL. +*) + +signature NUNCHAKU_RECONSTRUCT = +sig + type nun_model = Nunchaku_Model.nun_model + + type typ_entry = typ * term list + type term_entry = term * term + + type isa_model = + {type_model: typ_entry list, + free_model: term_entry list, + pat_complete_model: term_entry list, + pat_incomplete_model: term_entry list, + skolem_model: term_entry list} + + val str_of_isa_model: Proof.context -> isa_model -> string + + val isa_model_of_nun: Proof.context -> term list -> (typ option * string list) list -> + nun_model -> isa_model +end; + +structure Nunchaku_Reconstruct : NUNCHAKU_RECONSTRUCT = +struct + +open Nunchaku_Util; +open Nunchaku_Problem; +open Nunchaku_Translate; +open Nunchaku_Model; + +type typ_entry = typ * term list; +type term_entry = term * term; + +type isa_model = + {type_model: typ_entry list, + free_model: term_entry list, + pat_complete_model: term_entry list, + pat_incomplete_model: term_entry list, + skolem_model: term_entry list}; + +val anonymousN = "anonymous"; +val irrelevantN = "irrelevant"; +val unparsableN = "unparsable"; + +val nun_arrow_exploded = String.explode nun_arrow; + +val is_ty_meta = member (op =) (String.explode "()->,"); + +fun next_token_lowlevel [] = (End_of_Stream, []) + | next_token_lowlevel (c :: cs) = + if Char.isSpace c then + next_token_lowlevel cs + else if not (is_ty_meta c) then + let val n = find_index (Char.isSpace orf is_ty_meta) cs in + (if n = ~1 then (cs, []) else chop n cs) + |>> (cons c #> String.implode #> ident_of_str #> Ident) + end + else if is_prefix (op =) nun_arrow_exploded (c :: cs) then + (Ident nun_arrow, tl cs) + else + (Symbol (String.str c), cs); + +val tokenize_lowlevel = + let + fun toks cs = + (case next_token_lowlevel cs of + (End_of_Stream, []) => [] + | (tok, cs') => tok :: toks cs'); + in + toks o String.explode + end; + +fun parse_lowlevel_ty tok = + (Scan.optional + (parse_sym "(" |-- Scan.repeat (parse_lowlevel_ty --| Scan.option (parse_sym ",")) --| + parse_sym ")") + [] + -- parse_ident >> (swap #> NType)) tok; + +val ty_of_lowlevel_str = fst o parse_lowlevel_ty o tokenize_lowlevel; + +fun ident_of_const (NConst (id, _, _)) = id + | ident_of_const _ = nun_dummy; + +fun str_of_typ_entry ctxt (T, ts) = + "type " ^ Syntax.string_of_typ ctxt T ^ + " := {" ^ commas (map (Syntax.string_of_term ctxt) ts) ^ "}."; + +fun str_of_term_entry ctxt (tm, value) = + "val " ^ Syntax.string_of_term ctxt tm ^ " := " ^ Syntax.string_of_term ctxt value ^ "."; + +fun str_of_isa_model ctxt + {type_model, free_model, pat_complete_model, pat_incomplete_model, skolem_model} = + map (str_of_typ_entry ctxt) type_model @ "" :: + map (str_of_term_entry ctxt) free_model @ "" :: + map (str_of_term_entry ctxt) pat_complete_model @ "" :: + map (str_of_term_entry ctxt) pat_incomplete_model @ "" :: + map (str_of_term_entry ctxt) skolem_model + |> cat_lines; + +fun typ_of_nun ctxt = + let + fun typ_of (NType (id, tys)) = + let val Ts = map typ_of tys in + if id = nun_dummy then + dummyT + else if id = nun_prop then + @{typ bool} + else if id = nun_arrow then + Type (@{type_name fun}, Ts) + else + (case try str_of_nun_tconst id of + SOME (args, s) => + let val tys' = map ty_of_lowlevel_str args in + Type (s, map typ_of (tys' @ tys)) + end + | NONE => + (case try str_of_nun_tfree id of + SOME s => TFree (Proof_Context.check_tfree ctxt (flip_quote s, dummyS)) + | NONE => raise Fail ("unknown type constructor: " ^ quote (str_of_ident id)))) + end; + in + typ_of + end; + +fun one_letter_of s = + let val c = String.sub (Long_Name.base_name s, 0) in + String.str (if Char.isAlpha c then c else #"x") + end; + +fun base_of_typ (Type (s, _)) = s + | base_of_typ (TFree (s, _)) = flip_quote s + | base_of_typ (TVar ((s, _), _)) = flip_quote s; + +fun term_of_nun ctxt atomss = + let + val thy = Proof_Context.theory_of ctxt; + + val typ_of = typ_of_nun ctxt; + + fun nth_atom T j = + let val ss = these (triple_lookup (typ_match thy) atomss T) in + if j >= 0 andalso j < length ss then nth ss j + else one_letter_of (base_of_typ T) ^ nat_subscript (j + 1) + end; + + fun term_of _ (NAtom (j, ty)) = + let val T = typ_of ty in Var ((nth_atom T j, 0), T) end + | term_of bounds (NConst (id, tys0, ty)) = + if id = nun_conj then + HOLogic.conj + else if id = nun_disj then + HOLogic.disj + else if id = nun_choice then + Const (@{const_name Eps}, typ_of ty) + else if id = nun_equals then + Const (@{const_name HOL.eq}, typ_of ty) + else if id = nun_false then + @{const False} + else if id = nun_if then + Const (@{const_name If}, typ_of ty) + else if id = nun_implies then + @{term implies} + else if id = nun_unique then + Const (@{const_name The}, typ_of ty) + else if id = nun_unique_unsafe then + Const (@{const_name The_unsafe}, typ_of ty) + else if id = nun_true then + @{const True} + else if String.isPrefix nun_anon_fun_prefix id then + let val j = Int.fromString (unprefix nun_anon_fun_prefix id) |> the_default ~1 in + Var ((anonymousN ^ nat_subscript (j + 1), 0), typ_of ty) + end + else if id = nun_irrelevant then + (* FIXME: get bounds from Nunchaku *) + list_comb (Var ((irrelevantN, 0), map (typ_of o safe_ty_of) bounds ---> typ_of ty), + map Bound (length bounds - 1 downto 0)) + else if id = nun_unparsable then + (* FIXME: get bounds from Nunchaku *) + list_comb (Var ((unparsableN, 0), typ_of ty), map Bound (length bounds - 1 downto 0)) + else + (case try str_of_nun_const id of + SOME (args, s) => + let val tys = map ty_of_lowlevel_str args in + Sign.mk_const thy (s, map typ_of (tys @ tys0)) + end + | NONE => + (case try str_of_nun_free id of + SOME s => Free (s, typ_of ty) + | NONE => + (case try str_of_nun_var id of + SOME s => Var ((s, 0), typ_of ty) + | NONE => + (case find_index (fn bound => ident_of_const bound = id) bounds of + ~1 => Var ((str_of_ident id, 0), typ_of ty) (* shouldn't happen? *) + | j => Bound j)))) + | term_of bounds (NAbs (var, body)) = + let val T = typ_of (safe_ty_of var) in + Abs (one_letter_of (base_of_typ T), T, term_of (var :: bounds) body) + end + | term_of bounds (NApp (func, arg)) = + let + fun same () = term_of bounds func $ term_of bounds arg; + in + (case (func, arg) of + (NConst (id, _, _), NAbs _) => + if id = nun_mu then + let val Abs (s, T, body) = term_of bounds arg in + Const (@{const_name The}, (T --> HOLogic.boolT) --> T) + $ Abs (s, T, HOLogic.eq_const T $ Bound 0 $ body) + end + else + same () + | _ => same ()) + end + | term_of _ (NMatch _) = raise Fail "unexpected match"; + in + term_of [] + end; + +fun isa_typ_entry_of_nun ctxt atomss (ty, atoms) = + (typ_of_nun ctxt ty, map (term_of_nun ctxt atomss) atoms); + +fun isa_term_entry_of_nun ctxt atomss (tm, value) = + (term_of_nun ctxt atomss tm, term_of_nun ctxt atomss value); + +fun isa_model_of_nun ctxt pat_completes atomss {type_model, const_model, skolem_model} = + let + val free_and_const_model = map (isa_term_entry_of_nun ctxt atomss) const_model; + val (free_model, (pat_complete_model, pat_incomplete_model)) = + List.partition (is_Free o fst) free_and_const_model + ||> List.partition (member (op aconv) pat_completes o fst); + in + {type_model = map (isa_typ_entry_of_nun ctxt atomss) type_model, free_model = free_model, + pat_complete_model = pat_complete_model, pat_incomplete_model = pat_incomplete_model, + skolem_model = map (isa_term_entry_of_nun ctxt atomss) skolem_model} + end; + +end; diff -r 14571c9e1d50 -r 6273d4c8325b src/HOL/Nunchaku/Tools/nunchaku_tool.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Nunchaku/Tools/nunchaku_tool.ML Mon Oct 24 22:42:07 2016 +0200 @@ -0,0 +1,134 @@ +(* Title: HOL/Nunchaku/Tools/nunchaku_tool.ML + Author: Jasmin Blanchette, Inria Nancy, LORIA, MPII + Copyright 2015, 2016 + +Interface to the external "nunchaku" tool. +*) + +signature NUNCHAKU_TOOL = +sig + type ty = Nunchaku_Problem.ty + type tm = Nunchaku_Problem.tm + type nun_problem = Nunchaku_Problem.nun_problem + + type tool_params = + {overlord: bool, + debug: bool, + specialize: bool, + timeout: Time.time} + + type nun_solution = + {tys: (ty * tm list) list, + tms: (tm * tm) list} + + datatype nun_outcome = + Unsat + | Sat of string * nun_solution + | Unknown of (string * nun_solution) option + | Timeout + | Nunchaku_Var_Not_Set + | Nunchaku_Cannot_Execute + | Nunchaku_Not_Found + | CVC4_Cannot_Execute + | CVC4_Not_Found + | Unknown_Error of int * string + + val nunchaku_env_var: string + + val solve_nun_problem: tool_params -> nun_problem -> nun_outcome +end; + +structure Nunchaku_Tool : NUNCHAKU_TOOL = +struct + +open Nunchaku_Util; +open Nunchaku_Problem; + +type tool_params = + {overlord: bool, + debug: bool, + specialize: bool, + timeout: Time.time}; + +type nun_solution = + {tys: (ty * tm list) list, + tms: (tm * tm) list}; + +datatype nun_outcome = + Unsat +| Sat of string * nun_solution +| Unknown of (string * nun_solution) option +| Timeout +| Nunchaku_Var_Not_Set +| Nunchaku_Cannot_Execute +| Nunchaku_Not_Found +| CVC4_Cannot_Execute +| CVC4_Not_Found +| Unknown_Error of int * string; + +fun bash_output_error s = + let val {out, err, rc, ...} = Bash.process s in + ((out, err), rc) + end; + +val nunchaku_env_var = "NUNCHAKU"; + +val cached_outcome = + Synchronized.var "Nunchaku_Tool.cached_outcome" (NONE : (nun_problem * nun_outcome) option); + +fun uncached_solve_nun_problem ({overlord, specialize, timeout, ...} : tool_params) + (problem as {sound, complete, ...}) = + with_tmp_or_overlord_file overlord "nunchaku" "nun" (fn prob_path => + if getenv nunchaku_env_var = "" then + Nunchaku_Var_Not_Set + else + let + val bash_cmd = + "\"$" ^ nunchaku_env_var ^ "\" \ + \--skolems-in-model --no-color " ^ + (if specialize then "" else "--no-specialize ") ^ + "--timeout " ^ string_of_int (Time.toSeconds timeout) ^ " " ^ + File.bash_path prob_path; + val comments = + [bash_cmd, "This file was generated by Isabelle (most likely Nunchaku)", timestamp ()]; + val prob_str = cat_lines (map (prefix "# ") comments) ^ "\n\n" ^ str_of_nun_problem problem; + val _ = File.write prob_path prob_str; + val ((output, error), code) = bash_output_error bash_cmd; + in + if String.isPrefix "SAT" output then + (if sound then Sat else Unknown o SOME) (output, {tys = [], tms = []}) + else if String.isPrefix "UNSAT" output then + if complete then Unsat else Unknown NONE + else if String.isPrefix "UNKNOWN" output then + Unknown NONE + else if String.isPrefix "TIMEOUT" output then + Timeout + else if code = 126 then + Nunchaku_Cannot_Execute + else if code = 127 then + Nunchaku_Not_Found + else + Unknown_Error (code, + simplify_spaces (elide_string 1000 (if error <> "" then error else output))) + end); + +fun solve_nun_problem (params as {overlord, debug, ...}) problem = + (case (overlord orelse debug, + AList.lookup (op =) (the_list (Synchronized.value cached_outcome)) problem) of + (false, SOME outcome) => outcome + | _ => + let + val outcome = uncached_solve_nun_problem params problem; + + fun update_cache () = + Synchronized.change cached_outcome (K (SOME (problem, outcome))); + in + (case outcome of + Unsat => update_cache () + | Sat _ => update_cache () + | Unknown _ => update_cache () + | _ => ()); + outcome + end); + +end; diff -r 14571c9e1d50 -r 6273d4c8325b src/HOL/Nunchaku/Tools/nunchaku_translate.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Nunchaku/Tools/nunchaku_translate.ML Mon Oct 24 22:42:07 2016 +0200 @@ -0,0 +1,189 @@ +(* Title: HOL/Nunchaku/Tools/nunchaku_translate.ML + Author: Jasmin Blanchette, Inria Nancy, LORIA, MPII + Copyright 2015, 2016 + +Translation of Isabelle/HOL problems to Nunchaku. +*) + +signature NUNCHAKU_TRANSLATE = +sig + type isa_problem = Nunchaku_Collect.isa_problem + type ty = Nunchaku_Problem.ty + type nun_problem = Nunchaku_Problem.nun_problem + + val flip_quote: string -> string + val lowlevel_str_of_ty: ty -> string + + val nun_problem_of_isa: Proof.context -> isa_problem -> nun_problem +end; + +structure Nunchaku_Translate : NUNCHAKU_TRANSLATE = +struct + +open Nunchaku_Util; +open Nunchaku_Collect; +open Nunchaku_Problem; + +fun flip_quote s = + (case try (unprefix "'") s of + SOME s' => s' + | NONE => prefix "'" s); + +fun lowlevel_str_of_ty (NType (id, tys)) = + (if null tys then "" else encode_args (map lowlevel_str_of_ty tys)) ^ id; + +fun strip_nun_abs 0 tm = ([], tm) + | strip_nun_abs n (NAbs (var, body)) = + strip_nun_abs (n - 1) body + |>> cons var; + +val strip_nun_comb = + let + fun strip args (NApp (func, arg)) = strip (arg :: args) func + | strip args tm = (tm, args); + in + strip [] + end; + +fun ty_of_isa (Type (s, Ts)) = + let val tys = map ty_of_isa Ts in + (case s of + @{type_name bool} => prop_ty + | @{type_name fun} => NType (nun_arrow, tys) + | _ => + let + val args = map lowlevel_str_of_ty tys; + val id = nun_tconst_of_str args s; + in + NType (id, []) + end) + end + | ty_of_isa (TFree (s, _)) = NType (nun_tfree_of_str (flip_quote s), []) + | ty_of_isa (TVar _) = raise Fail "unexpected TVar"; + +fun gen_tm_of_isa in_prop ctxt t = + let + val thy = Proof_Context.theory_of ctxt; + + fun id_of_const (x as (s, _)) = + let val args = map (lowlevel_str_of_ty o ty_of_isa) (Sign.const_typargs thy x) in + nun_const_of_str args s + end; + + fun tm_of_branch ctr_id var_count f_arg_tm = + let val (vars, body) = strip_nun_abs var_count f_arg_tm in + (ctr_id, vars, body) + end; + + fun tm_of bounds (Const (x as (s, T))) = + (case try (dest_co_datatype_case ctxt) x of + SOME ctrs => + let + val num_f_args = length ctrs; + val min_args = num_f_args + 1; + val var_counts = map (num_binder_types o snd) ctrs; + + val dummy_free = Free (Name.uu, T); + val tm = tm_of bounds dummy_free; + val tm' = eta_expandN_tm min_args tm; + val (vars, body) = strip_nun_abs min_args tm'; + val (_, (f_args, obj :: other_args)) = strip_nun_comb body ||> chop num_f_args; + val f_args' = map2 eta_expandN_tm var_counts f_args; + + val ctr_ids = map id_of_const ctrs; + in + NMatch (obj, @{map 3} tm_of_branch ctr_ids var_counts f_args') + |> rcomb_tms other_args + |> abs_tms vars + end + | NONE => + if s = @{const_name unreachable} andalso in_prop then + let val ty = ty_of_isa T in + napps (NConst (nun_asserting, [ty], mk_arrows_ty ([ty, prop_ty], ty)), + [NConst (id_of_const x, [], ty), NConst (nun_false, [], prop_ty)]) + end + else + let + val id = + (case s of + @{const_name All} => nun_forall + | @{const_name conj} => nun_conj + | @{const_name disj} => nun_disj + | @{const_name HOL.eq} => nun_equals + | @{const_name Eps} => nun_choice + | @{const_name Ex} => nun_exists + | @{const_name False} => nun_false + | @{const_name If} => nun_if + | @{const_name implies} => nun_implies + | @{const_name Not} => nun_not + | @{const_name The} => nun_unique + | @{const_name The_unsafe} => nun_unique_unsafe + | @{const_name True} => nun_true + | _ => id_of_const x); + in + NConst (id, [], ty_of_isa T) + end) + | tm_of _ (Free (s, T)) = NConst (nun_free_of_str s, [], ty_of_isa T) + | tm_of _ (Var ((s, _), T)) = NConst (nun_var_of_str s, [], ty_of_isa T) + | tm_of bounds (Abs (s, T, t)) = + let + val (s', bounds') = Name.variant s bounds; + val x = Var ((s', 0), T); + in + NAbs (tm_of bounds' x, tm_of bounds' (subst_bound (x, t))) + end + | tm_of bounds (t $ u) = NApp (tm_of bounds t, tm_of bounds u) + | tm_of _ (Bound _) = raise Fail "unexpected Bound"; + in + t + |> tm_of Name.context + |> beta_reduce_tm + |> eta_expand_builtin_tm + end; + +val tm_of_isa = gen_tm_of_isa false; +val prop_of_isa = gen_tm_of_isa true; + +fun nun_type_spec_of_isa ctxt {abs_typ, rep_typ, wrt, abs, rep} = + {abs_ty = ty_of_isa abs_typ, rep_ty = ty_of_isa rep_typ, wrt = tm_of_isa ctxt wrt, + abs = tm_of_isa ctxt abs, rep = tm_of_isa ctxt rep}; + +fun nun_ctr_of_isa ctxt ctr = + {ctr = tm_of_isa ctxt ctr, arg_tys = map ty_of_isa (binder_types (fastype_of ctr))}; + +fun nun_co_data_spec_of_isa ctxt {typ, ctrs} = + {ty = ty_of_isa typ, ctrs = map (nun_ctr_of_isa ctxt) ctrs}; + +fun nun_const_spec_of_isa ctxt {const, props} = + {const = tm_of_isa ctxt const, props = map (prop_of_isa ctxt) props}; + +fun nun_rec_spec_of_isa ctxt {const, props, ...} = + {const = tm_of_isa ctxt const, props = map (prop_of_isa ctxt) props}; + +fun nun_consts_spec_of_isa ctxt {consts, props} = + {consts = map (tm_of_isa ctxt) consts, props = map (prop_of_isa ctxt) props}; + +fun nun_problem_of_isa ctxt {commandss, sound, complete} = + let + fun cmd_of cmd = + (case cmd of + ITVal (T, cards) => NTVal (ty_of_isa T, cards) + | ICopy spec => NCopy (nun_type_spec_of_isa ctxt spec) + | IQuotient spec => NQuotient (nun_type_spec_of_isa ctxt spec) + | ICoData (fp, specs) => + BNF_Util.case_fp fp NData NCodata (map (nun_co_data_spec_of_isa ctxt) specs) + | IVal t => NVal (tm_of_isa ctxt t, ty_of_isa (fastype_of t)) + | ICoPred (fp, wf, specs) => + (if wf then curry NPred true + else if fp = BNF_Util.Least_FP then curry NPred false + else NCopred) (map (nun_const_spec_of_isa ctxt) specs) + | IRec specs => NRec (map (nun_rec_spec_of_isa ctxt) specs) + | ISpec spec => NSpec (nun_consts_spec_of_isa ctxt spec) + | IAxiom prop => NAxiom (prop_of_isa ctxt prop) + | IGoal prop => NGoal (prop_of_isa ctxt prop) + | IEval t => NEval (tm_of_isa ctxt t)); + in + {commandss = map (map cmd_of) commandss, sound = sound, complete = complete} + end; + +end; diff -r 14571c9e1d50 -r 6273d4c8325b src/HOL/Nunchaku/Tools/nunchaku_util.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Nunchaku/Tools/nunchaku_util.ML Mon Oct 24 22:42:07 2016 +0200 @@ -0,0 +1,95 @@ +(* Title: HOL/Nunchaku/Tools/nunchaku_util.ML + Author: Jasmin Blanchette, Inria Nancy, LORIA, MPII + Copyright 2015, 2016 + +General-purpose functions used by Nunchaku. +*) + +signature NUNCHAKU_UTIL = +sig + val elide_string: int -> string -> string + val nat_subscript: int -> string + val timestamp: unit -> string + val parse_bool_option: bool -> string -> string -> bool option + val parse_time: string -> string -> Time.time + val string_of_time: Time.time -> string + val simplify_spaces: string -> string + val ascii_of: string -> string + val unascii_of: string -> string + val double_lookup: ('a * 'a -> bool) -> ('a option * 'b) list -> 'a -> 'b option + val triple_lookup: (''a * ''a -> bool) -> (''a option * 'b) list -> ''a -> 'b option + val plural_s_for_list: 'a list -> string + val with_overlord_file: string -> string -> (Path.T -> 'a) -> 'a + val with_tmp_or_overlord_file: bool -> string -> string -> (Path.T -> 'a) -> 'a + val num_binder_types: typ -> int + val strip_fun_type: typ -> typ list * typ + val attach_typeS: term -> term + val specialize_type: theory -> string * typ -> term -> term + val typ_match: theory -> typ * typ -> bool + val term_match: theory -> term * term -> bool + val const_match: theory -> (string * typ) * (string * typ) -> bool + val DETERM_TIMEOUT: Time.time -> tactic -> tactic + val spying: bool -> (unit -> Proof.state * int * string) -> unit +end; + +structure Nunchaku_Util : NUNCHAKU_UTIL = +struct + +val elide_string = ATP_Util.elide_string; +val nat_subscript = Nitpick_Util.nat_subscript; +val timestamp = ATP_Util.timestamp; + +val parse_bool_option = Sledgehammer_Util.parse_bool_option; +val parse_time = Sledgehammer_Util.parse_time; +val string_of_time = ATP_Util.string_of_time; +val simplify_spaces = Sledgehammer_Util.simplify_spaces; +val ascii_of = ATP_Problem_Generate.ascii_of; +val unascii_of = ATP_Problem_Generate.unascii_of; +val double_lookup = Nitpick_Util.double_lookup; +val triple_lookup = Nitpick_Util.triple_lookup; +val plural_s_for_list = Nitpick_Util.plural_s_for_list; + +fun with_overlord_file name ext f = + f (Path.explode ("$ISABELLE_HOME_USER/" ^ name ^ "." ^ ext)); + +fun with_tmp_or_overlord_file overlord = + if overlord then with_overlord_file else Isabelle_System.with_tmp_file; + +val num_binder_types = BNF_Util.num_binder_types +val strip_fun_type = BNF_Util.strip_fun_type; + +(* Clone from "HOL/Tools/inductive_realizer.ML". *) +val attach_typeS = + map_types (map_atyps + (fn TFree (s, []) => TFree (s, @{sort type}) + | TVar (ixn, []) => TVar (ixn, @{sort type}) + | T => T)); + +val specialize_type = ATP_Util.specialize_type; + +fun typ_match thy TU = can (Sign.typ_match thy TU) Vartab.empty; +fun term_match thy tu = can (Pattern.match thy tu) (Vartab.empty, Vartab.empty); +fun const_match thy = term_match thy o apply2 Const; + +val DETERM_TIMEOUT = Nitpick_Util.DETERM_TIMEOUT; + +val spying_version = "a" + +val hackish_string_of_term = Sledgehammer_Util.hackish_string_of_term; + +fun spying spy f = + if spy then + let + val (state, i, message) = f (); + val ctxt = Proof.context_of state; + val goal = Logic.get_goal (Thm.prop_of (#goal (Proof.goal state))) i; + val hash = + String.substring (SHA1.rep (SHA1.digest (hackish_string_of_term ctxt goal)), 0, 12); + in + File.append (Path.explode "$ISABELLE_HOME_USER/spy_nunchaku") + (spying_version ^ " " ^ timestamp () ^ ": " ^ hash ^ ": " ^ message ^ "\n") + end + else + (); + +end; diff -r 14571c9e1d50 -r 6273d4c8325b src/HOL/ROOT --- a/src/HOL/ROOT Mon Oct 24 21:14:38 2016 +0200 +++ b/src/HOL/ROOT Mon Oct 24 22:42:07 2016 +0200 @@ -282,6 +282,16 @@ options [document = false] theories [quick_and_dirty] Nitpick_Examples +session "HOL-Nunchaku" in Nunchaku = HOL + + description {* + Author: Jasmin Blanchette, Inria Nancy, LORIA, MPII + Copyright 2015, 2016 + + Nunchaku: Yet another counterexample generator for Isabelle/HOL. + *} + options [document = false] + theories Nunchaku + session "HOL-Algebra" (main timing) in Algebra = HOL + description {* Author: Clemens Ballarin, started 24 September 1999