--- a/src/HOL/Nunchaku/Tools/nunchaku.ML Thu Sep 07 23:13:15 2017 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,327 +0,0 @@
-(* 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 =
- {solvers: string list,
- 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 =
- {solvers: string list,
- 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 = {solvers, 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 =
- {solvers = solvers, 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\n\
- \The problem lies outside Nunchaku's fragment, or the Nunchaku backends are not \
- \installed properly");
- (unknownN, NONE));
-
- fun unsat_or_unknown complete =
- if complete then
- (print_n ("No " ^ das_wort_model ^ " exists" ^
- (if falsify andalso unsat_means_theorem () then "\nThe 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_home_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;