added Nunchaku integration
authorblanchet
Mon Oct 24 22:42:07 2016 +0200 (2016-10-24)
changeset 643896273d4c8325b
parent 64388 14571c9e1d50
child 64390 ad2c5f37f659
added Nunchaku integration
CONTRIBUTORS
NEWS
src/HOL/Nunchaku/Nunchaku.thy
src/HOL/Nunchaku/Tools/nunchaku.ML
src/HOL/Nunchaku/Tools/nunchaku_collect.ML
src/HOL/Nunchaku/Tools/nunchaku_commands.ML
src/HOL/Nunchaku/Tools/nunchaku_display.ML
src/HOL/Nunchaku/Tools/nunchaku_model.ML
src/HOL/Nunchaku/Tools/nunchaku_problem.ML
src/HOL/Nunchaku/Tools/nunchaku_reconstruct.ML
src/HOL/Nunchaku/Tools/nunchaku_tool.ML
src/HOL/Nunchaku/Tools/nunchaku_translate.ML
src/HOL/Nunchaku/Tools/nunchaku_util.ML
src/HOL/ROOT
     1.1 --- a/CONTRIBUTORS	Mon Oct 24 21:14:38 2016 +0200
     1.2 +++ b/CONTRIBUTORS	Mon Oct 24 22:42:07 2016 +0200
     1.3 @@ -48,6 +48,10 @@
     1.4    Ported remaining theories of Old_Number_Theory to the new 
     1.5    Number_Theory and removed Old_Number_Theory.
     1.6  
     1.7 +* October 2016: Jasmin Blanchette
     1.8 +  Integration of Nunchaku model finder.
     1.9 +
    1.10 +
    1.11  Contributions to Isabelle2016
    1.12  -----------------------------
    1.13  
     2.1 --- a/NEWS	Mon Oct 24 21:14:38 2016 +0200
     2.2 +++ b/NEWS	Mon Oct 24 22:42:07 2016 +0200
     2.3 @@ -910,6 +910,9 @@
     2.4  * Renamed HOL/Quotient_Examples/FSet.thy to
     2.5  HOL/Quotient_Examples/Quotient_FSet.thy INCOMPATIBILITY.
     2.6  
     2.7 +* The "nunchaku" program integrates the Nunchaku model finder. The tool
     2.8 +is experimental. See ~~/src/HOL/Nunchaku/Nunchaku.thy for details.
     2.9 +
    2.10  
    2.11  *** ML ***
    2.12  
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/Nunchaku/Nunchaku.thy	Mon Oct 24 22:42:07 2016 +0200
     3.3 @@ -0,0 +1,41 @@
     3.4 +(*  Title:      HOL/Nunchaku/Nunchaku.thy
     3.5 +    Author:     Jasmin Blanchette, Inria Nancy, LORIA, MPII
     3.6 +    Copyright   2015, 2016
     3.7 +
     3.8 +Nunchaku: Yet another counterexample generator for Isabelle/HOL.
     3.9 +
    3.10 +Nunchaku relies on an external program of the same name. The program is still
    3.11 +being actively developed. The sources are available at
    3.12 +
    3.13 +    https://github.com/nunchaku-inria
    3.14 +*)
    3.15 +
    3.16 +theory Nunchaku
    3.17 +imports Main
    3.18 +keywords
    3.19 +  "nunchaku" :: diag and
    3.20 +  "nunchaku_params" :: thy_decl
    3.21 +begin
    3.22 +
    3.23 +consts unreachable :: 'a
    3.24 +
    3.25 +definition The_unsafe :: "('a \<Rightarrow> bool) \<Rightarrow> 'a" where
    3.26 +  "The_unsafe = The"
    3.27 +
    3.28 +definition rmember :: "'a set \<Rightarrow> 'a \<Rightarrow> bool" where
    3.29 +  "rmember A x \<longleftrightarrow> x \<in> A"
    3.30 +
    3.31 +ML_file "Tools/nunchaku_util.ML"
    3.32 +ML_file "Tools/nunchaku_collect.ML"
    3.33 +ML_file "Tools/nunchaku_problem.ML"
    3.34 +ML_file "Tools/nunchaku_translate.ML"
    3.35 +ML_file "Tools/nunchaku_model.ML"
    3.36 +ML_file "Tools/nunchaku_reconstruct.ML"
    3.37 +ML_file "Tools/nunchaku_display.ML"
    3.38 +ML_file "Tools/nunchaku_tool.ML"
    3.39 +ML_file "Tools/nunchaku.ML"
    3.40 +ML_file "Tools/nunchaku_commands.ML"
    3.41 +
    3.42 +hide_const (open) unreachable The_unsafe rmember
    3.43 +
    3.44 +end
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/HOL/Nunchaku/Tools/nunchaku.ML	Mon Oct 24 22:42:07 2016 +0200
     4.3 @@ -0,0 +1,325 @@
     4.4 +(*  Title:      HOL/Nunchaku/Tools/nunchaku.ML
     4.5 +    Author:     Jasmin Blanchette, Inria Nancy, LORIA, MPII
     4.6 +    Copyright   2015, 2016
     4.7 +
     4.8 +The core of the Nunchaku integration in Isabelle.
     4.9 +*)
    4.10 +
    4.11 +signature NUNCHAKU =
    4.12 +sig
    4.13 +  type isa_model = Nunchaku_Reconstruct.isa_model
    4.14 +
    4.15 +  datatype mode = Auto_Try | Try | Normal
    4.16 +
    4.17 +  type mode_of_operation_params =
    4.18 +    {falsify: bool,
    4.19 +     assms: bool,
    4.20 +     spy: bool,
    4.21 +     overlord: bool,
    4.22 +     expect: string}
    4.23 +
    4.24 +  type scope_of_search_params =
    4.25 +    {wfs: ((string * typ) option * bool option) list,
    4.26 +     whacks: (term option * bool) list,
    4.27 +     cards: (typ option * (int option * int option)) list,
    4.28 +     monos: (typ option * bool option) list}
    4.29 +
    4.30 +  type output_format_params =
    4.31 +    {verbose: bool,
    4.32 +     debug: bool,
    4.33 +     max_potential: int,
    4.34 +     max_genuine: int,
    4.35 +     evals: term list,
    4.36 +     atomss: (typ option * string list) list}
    4.37 +
    4.38 +  type optimization_params =
    4.39 +    {specialize: bool,
    4.40 +     multithread: bool}
    4.41 +
    4.42 +  type timeout_params =
    4.43 +    {timeout: Time.time,
    4.44 +     wf_timeout: Time.time}
    4.45 +
    4.46 +  type params =
    4.47 +    {mode_of_operation_params: mode_of_operation_params,
    4.48 +     scope_of_search_params: scope_of_search_params,
    4.49 +     output_format_params: output_format_params,
    4.50 +     optimization_params: optimization_params,
    4.51 +     timeout_params: timeout_params}
    4.52 +
    4.53 +  val genuineN: string
    4.54 +  val quasi_genuineN: string
    4.55 +  val potentialN: string
    4.56 +  val noneN: string
    4.57 +  val unknownN: string
    4.58 +  val no_nunchakuN: string
    4.59 +
    4.60 +  val run_chaku_on_prop: Proof.state -> params -> mode -> int -> term list -> term ->
    4.61 +    string * isa_model option
    4.62 +  val run_chaku_on_subgoal: Proof.state -> params -> mode -> int -> string * isa_model option
    4.63 +end;
    4.64 +
    4.65 +structure Nunchaku : NUNCHAKU =
    4.66 +struct
    4.67 +
    4.68 +open Nunchaku_Util;
    4.69 +open Nunchaku_Collect;
    4.70 +open Nunchaku_Problem;
    4.71 +open Nunchaku_Translate;
    4.72 +open Nunchaku_Model;
    4.73 +open Nunchaku_Reconstruct;
    4.74 +open Nunchaku_Display;
    4.75 +open Nunchaku_Tool;
    4.76 +
    4.77 +datatype mode = Auto_Try | Try | Normal;
    4.78 +
    4.79 +type mode_of_operation_params =
    4.80 +  {falsify: bool,
    4.81 +   assms: bool,
    4.82 +   spy: bool,
    4.83 +   overlord: bool,
    4.84 +   expect: string};
    4.85 +
    4.86 +type scope_of_search_params =
    4.87 +  {wfs: ((string * typ) option * bool option) list,
    4.88 +   whacks: (term option * bool) list,
    4.89 +   cards: (typ option * (int option * int option)) list,
    4.90 +   monos: (typ option * bool option) list};
    4.91 +
    4.92 +type output_format_params =
    4.93 +  {verbose: bool,
    4.94 +   debug: bool,
    4.95 +   max_potential: int,
    4.96 +   max_genuine: int,
    4.97 +   evals: term list,
    4.98 +   atomss: (typ option * string list) list};
    4.99 +
   4.100 +type optimization_params =
   4.101 +  {specialize: bool,
   4.102 +   multithread: bool};
   4.103 +
   4.104 +type timeout_params =
   4.105 +  {timeout: Time.time,
   4.106 +   wf_timeout: Time.time};
   4.107 +
   4.108 +type params =
   4.109 +  {mode_of_operation_params: mode_of_operation_params,
   4.110 +   scope_of_search_params: scope_of_search_params,
   4.111 +   output_format_params: output_format_params,
   4.112 +   optimization_params: optimization_params,
   4.113 +   timeout_params: timeout_params};
   4.114 +
   4.115 +val genuineN = "genuine";
   4.116 +val quasi_genuineN = "quasi_genuine";
   4.117 +val potentialN = "potential";
   4.118 +val noneN = "none";
   4.119 +val unknownN = "unknown";
   4.120 +
   4.121 +val no_nunchakuN = "no_nunchaku";
   4.122 +
   4.123 +fun str_of_mode Auto_Try = "Auto_Try"
   4.124 +  | str_of_mode Try = "Try"
   4.125 +  | str_of_mode Normal = "Normal";
   4.126 +
   4.127 +fun none_true assigns = forall (curry (op <>) (SOME true) o snd) assigns;
   4.128 +
   4.129 +fun has_lonely_bool_var (@{const Pure.conjunction} $ (@{const Trueprop} $ Free _) $ _) = true
   4.130 +  | has_lonely_bool_var _ = false;
   4.131 +
   4.132 +val syntactic_sorts =
   4.133 +  @{sort "{default,zero,one,plus,minus,uminus,times,inverse,abs,sgn,ord,equal}"} @ @{sort numeral};
   4.134 +
   4.135 +fun has_tfree_syntactic_sort (TFree (_, S as _ :: _)) = subset (op =) (S, syntactic_sorts)
   4.136 +  | has_tfree_syntactic_sort _ = false;
   4.137 +
   4.138 +val has_syntactic_sorts = exists_type (exists_subtype has_tfree_syntactic_sort);
   4.139 +
   4.140 +(* Give the soft timeout a chance. *)
   4.141 +val timeout_slack = seconds 1.0;
   4.142 +
   4.143 +fun run_chaku_on_prop state
   4.144 +    ({mode_of_operation_params = {falsify, assms, spy, overlord, expect},
   4.145 +      scope_of_search_params = {wfs, whacks, cards, monos},
   4.146 +      output_format_params = {verbose, debug, evals, atomss, ...},
   4.147 +      optimization_params = {specialize, ...},
   4.148 +      timeout_params = {timeout, wf_timeout}})
   4.149 +    mode i all_assms subgoal =
   4.150 +  let
   4.151 +    val ctxt = Proof.context_of state;
   4.152 +
   4.153 +    val timer = Timer.startRealTimer ()
   4.154 +
   4.155 +    val print = writeln;
   4.156 +    val print_n = if mode = Normal then writeln else K ();
   4.157 +    fun print_v f = if verbose then writeln (f ()) else ();
   4.158 +    fun print_d f = if debug then writeln (f ()) else ();
   4.159 +
   4.160 +    val das_wort_Model = if falsify then "Countermodel" else "Model";
   4.161 +    val das_wort_model = if falsify then "countermodel" else "model";
   4.162 +
   4.163 +    val tool_params = {overlord = overlord, debug = debug, specialize = specialize,
   4.164 +      timeout = timeout};
   4.165 +
   4.166 +    fun run () =
   4.167 +      let
   4.168 +        val outcome as (outcome_code, _) =
   4.169 +          let
   4.170 +            val (poly_axioms, isa_problem as {sound, complete, ...}) =
   4.171 +              isa_problem_of_subgoal ctxt falsify wfs whacks cards debug wf_timeout evals
   4.172 +                (if assms then all_assms else []) subgoal;
   4.173 +            val _ = print_d (fn () => "*** Isabelle problem ***\n" ^
   4.174 +              str_of_isa_problem ctxt isa_problem);
   4.175 +            val ugly_nun_problem = nun_problem_of_isa ctxt isa_problem;
   4.176 +            val _ = print_d (fn () => "*** Ugly Nunchaku problem ***\n" ^
   4.177 +              str_of_nun_problem ugly_nun_problem);
   4.178 +            val (nice_nun_problem, pool) = nice_nun_problem ugly_nun_problem;
   4.179 +            val _ = print_d (fn () => "*** Nice Nunchaku problem ***\n" ^
   4.180 +              str_of_nun_problem nice_nun_problem);
   4.181 +
   4.182 +            fun print_any_hints () =
   4.183 +              if has_lonely_bool_var subgoal then
   4.184 +                print "Hint: Maybe you forgot a colon after the lemma's name?"
   4.185 +              else if has_syntactic_sorts subgoal then
   4.186 +                print "Hint: Maybe you forgot a type constraint?"
   4.187 +              else
   4.188 +                ();
   4.189 +
   4.190 +            fun get_isa_model_opt output =
   4.191 +              let
   4.192 +                val nice_nun_model = nun_model_of_str output;
   4.193 +                val _ = print_d (fn () => "*** Nice Nunchaku model ***\n" ^
   4.194 +                  str_of_nun_model nice_nun_model);
   4.195 +                val ugly_nun_model = ugly_nun_model pool nice_nun_model;
   4.196 +                val _ = print_d (fn () => "*** Ugly Nunchaku model ***\n" ^
   4.197 +                  str_of_nun_model ugly_nun_model);
   4.198 +
   4.199 +                val pat_completes = pat_completes_of_isa_problem isa_problem;
   4.200 +                val isa_model = isa_model_of_nun ctxt pat_completes atomss ugly_nun_model;
   4.201 +                val _ = print_d (fn () => "*** Isabelle model ***\n" ^
   4.202 +                  str_of_isa_model ctxt isa_model);
   4.203 +              in
   4.204 +                isa_model
   4.205 +              end;
   4.206 +
   4.207 +            fun isa_model_opt output =
   4.208 +              if debug then SOME (get_isa_model_opt output) else try get_isa_model_opt output;
   4.209 +
   4.210 +            val model_str = isa_model_opt #> pretty_of_isa_model_opt ctxt #> Pretty.string_of;
   4.211 +
   4.212 +            fun unsat_means_theorem () =
   4.213 +              null whacks andalso null cards andalso null monos;
   4.214 +
   4.215 +            fun unknown () =
   4.216 +              (print_n ("No " ^ das_wort_model ^ " can be found \<midarrow> the problem lies \
   4.217 +                 \outside Nunchaku's fragment");
   4.218 +               (unknownN, NONE));
   4.219 +
   4.220 +            fun unsat_or_unknown complete =
   4.221 +              if complete then
   4.222 +                (print_n ("No " ^ das_wort_model ^ " exists" ^
   4.223 +                   (if falsify andalso unsat_means_theorem () then
   4.224 +                      " \<midarrow> the goal is a theorem"
   4.225 +                    else
   4.226 +                      ""));
   4.227 +                 (noneN, NONE))
   4.228 +              else
   4.229 +                unknown ();
   4.230 +
   4.231 +            fun sat_or_maybe_sat sound output =
   4.232 +              let val header = if sound then das_wort_Model else "Potential " ^ das_wort_model in
   4.233 +                (case (null poly_axioms, none_true wfs) of
   4.234 +                  (true, true) =>
   4.235 +                  (print (header ^ ":\n" ^
   4.236 +                     model_str output); print_any_hints ();
   4.237 +                   (genuineN, isa_model_opt output))
   4.238 +                | (no_poly, no_wf) =>
   4.239 +                  let
   4.240 +                    val ignorings = []
   4.241 +                      |> not no_poly ? cons "polymorphic axioms"
   4.242 +                      |> not no_wf ? cons "unchecked well-foundedness";
   4.243 +                  in
   4.244 +                    (print (header ^ " (ignoring " ^ space_implode " and " ignorings ^ "):\n" ^
   4.245 +                       model_str output ^
   4.246 +                       (if no_poly then
   4.247 +                          ""
   4.248 +                        else
   4.249 +                          "\nIgnored axioms:\n" ^
   4.250 +                          cat_lines (map (prefix "  " o Syntax.string_of_term ctxt) poly_axioms)));
   4.251 +                     print_any_hints ();
   4.252 +                     (quasi_genuineN, isa_model_opt output))
   4.253 +                  end)
   4.254 +              end;
   4.255 +          in
   4.256 +            (case solve_nun_problem tool_params nice_nun_problem of
   4.257 +              Unsat => unsat_or_unknown complete
   4.258 +            | Sat (output, _) => sat_or_maybe_sat sound output
   4.259 +            | Unknown NONE => unknown ()
   4.260 +            | Unknown (SOME (output, _)) => sat_or_maybe_sat false output
   4.261 +            | Timeout => (print_n "Time out"; (unknownN, NONE))
   4.262 +            | Nunchaku_Var_Not_Set =>
   4.263 +              (print_n ("Variable $" ^ nunchaku_env_var ^ " not set"); (unknownN, NONE))
   4.264 +            | Nunchaku_Cannot_Execute =>
   4.265 +              (print_n "External tool \"nunchaku\" cannot execute"; (unknownN, NONE))
   4.266 +            | Nunchaku_Not_Found =>
   4.267 +              (print_n "External tool \"nunchaku\" not found"; (unknownN, NONE))
   4.268 +            | CVC4_Cannot_Execute =>
   4.269 +              (print_n "External tool \"cvc4\" cannot execute"; (unknownN, NONE))
   4.270 +            | CVC4_Not_Found => (print_n "External tool \"cvc4\" not found"; (unknownN, NONE))
   4.271 +            | Unknown_Error (code, msg) =>
   4.272 +              (print_n ("Unknown error: " ^ msg ^
   4.273 +                 (if code = 0 then "" else " (code " ^ string_of_int code ^ ")"));
   4.274 +               (unknownN, NONE)))
   4.275 +          end
   4.276 +          handle
   4.277 +            CYCLIC_DEPS () =>
   4.278 +            (print_n "Cyclic dependencies (or bug in Nunchaku)"; (unknownN, NONE))
   4.279 +          | TOO_DEEP_DEPS () =>
   4.280 +            (print_n "Too deep dependencies (or bug in Nunchaku)"; (unknownN, NONE))
   4.281 +          | TOO_META t =>
   4.282 +            (print_n ("Formula too meta for Nunchaku:\n" ^ Syntax.string_of_term ctxt t);
   4.283 +             (unknownN, NONE))
   4.284 +          | UNEXPECTED_POLYMORPHISM t =>
   4.285 +            (print_n ("Unexpected polymorphism in term\n" ^ Syntax.string_of_term ctxt t);
   4.286 +             (unknownN, NONE))
   4.287 +          | UNEXPECTED_VAR t =>
   4.288 +            (print_n ("Unexpected schematic variables in term\n" ^ Syntax.string_of_term ctxt t);
   4.289 +             (unknownN, NONE))
   4.290 +          | UNSUPPORTED_FUNC t =>
   4.291 +            (print_n ("Unsupported low-level constant in problem: " ^ Syntax.string_of_term ctxt t);
   4.292 +             (unknownN, NONE));
   4.293 +      in
   4.294 +        if expect = "" orelse outcome_code = expect then outcome
   4.295 +        else error ("Unexpected outcome: " ^ quote outcome_code)
   4.296 +      end;
   4.297 +
   4.298 +    val _ = spying spy (fn () => (state, i, "starting " ^ str_of_mode mode ^ " mode"));
   4.299 +
   4.300 +    val outcome as (outcome_code, _) =
   4.301 +      Timeout.apply (Time.+ (timeout, timeout_slack)) run ()
   4.302 +      handle Timeout.TIMEOUT _ => (print_n "Time out"; (unknownN, NONE));
   4.303 +
   4.304 +    val _ = print_v (fn () => "Total time: " ^ string_of_time (Timer.checkRealTimer timer));
   4.305 +
   4.306 +    val _ = spying spy (fn () => (state, i, "outcome: " ^ outcome_code));
   4.307 +  in
   4.308 +    if expect = "" orelse outcome_code = expect then outcome
   4.309 +    else error ("Unexpected outcome: " ^ quote outcome_code)
   4.310 +  end;
   4.311 +
   4.312 +fun run_chaku_on_subgoal state params mode i =
   4.313 +  let
   4.314 +    val ctxt = Proof.context_of state;
   4.315 +    val goal = Thm.prop_of (#goal (Proof.raw_goal state));
   4.316 +  in
   4.317 +    if Logic.count_prems goal = 0 then
   4.318 +      (writeln "No subgoal!"; (noneN, NONE))
   4.319 +    else
   4.320 +      let
   4.321 +        val subgoal = fst (Logic.goal_params goal i);
   4.322 +        val all_assms = map Thm.term_of (Assumption.all_assms_of ctxt);
   4.323 +      in
   4.324 +        run_chaku_on_prop state params mode i all_assms subgoal
   4.325 +      end
   4.326 +  end;
   4.327 +
   4.328 +end;
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/HOL/Nunchaku/Tools/nunchaku_collect.ML	Mon Oct 24 22:42:07 2016 +0200
     5.3 @@ -0,0 +1,1109 @@
     5.4 +(*  Title:      HOL/Nunchaku/Tools/nunchaku_collect.ML
     5.5 +    Author:     Jasmin Blanchette, Inria Nancy, LORIA, MPII
     5.6 +    Copyright   2015, 2016
     5.7 +
     5.8 +Collecting of Isabelle/HOL definitions etc. for Nunchaku.
     5.9 +*)
    5.10 +
    5.11 +signature NUNCHAKU_COLLECT =
    5.12 +sig
    5.13 +  val dest_co_datatype_case: Proof.context -> string * typ -> (string * typ) list
    5.14 +
    5.15 +  type isa_type_spec =
    5.16 +    {abs_typ: typ,
    5.17 +     rep_typ: typ,
    5.18 +     wrt: term,
    5.19 +     abs: term,
    5.20 +     rep: term}
    5.21 +
    5.22 +  type isa_co_data_spec =
    5.23 +    {typ: typ,
    5.24 +     ctrs: term list}
    5.25 +
    5.26 +  type isa_const_spec =
    5.27 +    {const: term,
    5.28 +     props: term list}
    5.29 +
    5.30 +  type isa_rec_spec =
    5.31 +    {const: term,
    5.32 +     props: term list,
    5.33 +     pat_complete: bool}
    5.34 +
    5.35 +  type isa_consts_spec =
    5.36 +    {consts: term list,
    5.37 +     props: term list}
    5.38 +
    5.39 +  datatype isa_command =
    5.40 +    ITVal of typ * (int option * int option)
    5.41 +  | ICopy of isa_type_spec
    5.42 +  | IQuotient of isa_type_spec
    5.43 +  | ICoData of BNF_Util.fp_kind * isa_co_data_spec list
    5.44 +  | IVal of term
    5.45 +  | ICoPred of BNF_Util.fp_kind * bool * isa_const_spec list
    5.46 +  | IRec of isa_rec_spec list
    5.47 +  | ISpec of isa_consts_spec
    5.48 +  | IAxiom of term
    5.49 +  | IGoal of term
    5.50 +  | IEval of term
    5.51 +
    5.52 +  type isa_problem =
    5.53 +    {commandss: isa_command list list,
    5.54 +     sound: bool,
    5.55 +     complete: bool}
    5.56 +
    5.57 +  exception CYCLIC_DEPS of unit
    5.58 +  exception TOO_DEEP_DEPS of unit
    5.59 +  exception TOO_META of term
    5.60 +  exception UNEXPECTED_POLYMORPHISM of term
    5.61 +  exception UNEXPECTED_VAR of term
    5.62 +  exception UNSUPPORTED_FUNC of term
    5.63 +
    5.64 +  val isa_problem_of_subgoal: Proof.context -> bool -> ((string * typ) option * bool option) list ->
    5.65 +    (term option * bool) list -> (typ option * (int option * int option)) list -> bool ->
    5.66 +    Time.time -> term list -> term list -> term -> term list * isa_problem
    5.67 +  val pat_completes_of_isa_problem: isa_problem -> term list
    5.68 +  val str_of_isa_problem: Proof.context -> isa_problem -> string
    5.69 +end;
    5.70 +
    5.71 +structure Nunchaku_Collect : NUNCHAKU_COLLECT =
    5.72 +struct
    5.73 +
    5.74 +open Nunchaku_Util;
    5.75 +
    5.76 +type isa_type_spec =
    5.77 +  {abs_typ: typ,
    5.78 +   rep_typ: typ,
    5.79 +   wrt: term,
    5.80 +   abs: term,
    5.81 +   rep: term};
    5.82 +
    5.83 +type isa_co_data_spec =
    5.84 +  {typ: typ,
    5.85 +   ctrs: term list};
    5.86 +
    5.87 +type isa_const_spec =
    5.88 +  {const: term,
    5.89 +   props: term list};
    5.90 +
    5.91 +type isa_rec_spec =
    5.92 +  {const: term,
    5.93 +   props: term list,
    5.94 +   pat_complete: bool};
    5.95 +
    5.96 +type isa_consts_spec =
    5.97 +  {consts: term list,
    5.98 +   props: term list};
    5.99 +
   5.100 +datatype isa_command =
   5.101 +  ITVal of typ * (int option * int option)
   5.102 +| ICopy of isa_type_spec
   5.103 +| IQuotient of isa_type_spec
   5.104 +| ICoData of BNF_Util.fp_kind * isa_co_data_spec list
   5.105 +| IVal of term
   5.106 +| ICoPred of BNF_Util.fp_kind * bool * isa_const_spec list
   5.107 +| IRec of isa_rec_spec list
   5.108 +| ISpec of isa_consts_spec
   5.109 +| IAxiom of term
   5.110 +| IGoal of term
   5.111 +| IEval of term;
   5.112 +
   5.113 +type isa_problem =
   5.114 +  {commandss: isa_command list list,
   5.115 +   sound: bool,
   5.116 +   complete: bool};
   5.117 +
   5.118 +exception CYCLIC_DEPS of unit;
   5.119 +exception TOO_DEEP_DEPS of unit;
   5.120 +exception TOO_META of term;
   5.121 +exception UNEXPECTED_POLYMORPHISM of term;
   5.122 +exception UNEXPECTED_VAR of term;
   5.123 +exception UNSUPPORTED_FUNC of term;
   5.124 +
   5.125 +fun str_of_and_list str_of_elem =
   5.126 +  map str_of_elem #> space_implode ("\nand ");
   5.127 +
   5.128 +val key_of_typ =
   5.129 +  let
   5.130 +    fun key_of (Type (s, [])) = s
   5.131 +      | key_of (Type (s, Ts)) = s ^ "(" ^ commas (map key_of Ts) ^ ")"
   5.132 +      | key_of (TFree (s, _)) = s;
   5.133 +  in
   5.134 +    prefix "y" o key_of
   5.135 +  end;
   5.136 +
   5.137 +fun key_of_const ctxt =
   5.138 +  let
   5.139 +    val thy = Proof_Context.theory_of ctxt;
   5.140 +
   5.141 +    fun key_of (Const (x as (s, _))) =
   5.142 +        (case Sign.const_typargs thy x of
   5.143 +          [] => s
   5.144 +        | Ts => s ^ "(" ^ commas (map key_of_typ Ts) ^ ")")
   5.145 +      | key_of (Free (s, _)) = s;
   5.146 +  in
   5.147 +    prefix "t" o key_of
   5.148 +  end;
   5.149 +
   5.150 +val add_type_keys = fold_subtypes (insert (op =) o key_of_typ);
   5.151 +
   5.152 +fun add_aterm_keys ctxt t =
   5.153 +  if is_Const t orelse is_Free t then insert (op =) (key_of_const ctxt t) else I;
   5.154 +
   5.155 +fun add_keys ctxt t =
   5.156 +  fold_aterms (add_aterm_keys ctxt) t
   5.157 +  #> fold_types add_type_keys t;
   5.158 +
   5.159 +fun close_form except t =
   5.160 +  fold (fn ((s, i), T) => fn t' =>
   5.161 +      HOLogic.all_const T $ Abs (s, T, abstract_over (Var ((s, i), T), t')))
   5.162 +    (Term.add_vars t [] |> subtract (op =) except) t;
   5.163 +
   5.164 +(* "imp_conjL[symmetric]" is important for inductive predicates with multiple assumptions. *)
   5.165 +val basic_defs =
   5.166 +  @{thms Ball_def[abs_def] Bex_def[abs_def] case_bool_if Ex1_def[abs_def]
   5.167 +    imp_conjL[symmetric, abs_def] Let_def[abs_def] rmember_def[symmetric, abs_def]};
   5.168 +
   5.169 +fun unfold_basic_def ctxt =
   5.170 +  let val thy = Proof_Context.theory_of ctxt in
   5.171 +    Pattern.rewrite_term thy (map (Logic.dest_equals o Thm.prop_of) basic_defs) []
   5.172 +  end;
   5.173 +
   5.174 +val has_polymorphism = exists_type (exists_subtype is_TVar);
   5.175 +
   5.176 +fun whack_term thy whacks =
   5.177 +  let
   5.178 +    fun whk t =
   5.179 +      if triple_lookup (term_match thy o swap) whacks t = SOME true then
   5.180 +        Const (@{const_name unreachable}, fastype_of t)
   5.181 +      else
   5.182 +        (case t of
   5.183 +          u $ v => whk u $ whk v
   5.184 +        | Abs (s, T, u) => Abs (s, T, whk u)
   5.185 +        | _ => t);
   5.186 +  in
   5.187 +    whk
   5.188 +  end;
   5.189 +
   5.190 +fun preprocess_term_basic falsify ctxt whacks t =
   5.191 +  let val thy = Proof_Context.theory_of ctxt in
   5.192 +    if has_polymorphism t then
   5.193 +      raise UNEXPECTED_POLYMORPHISM t
   5.194 +    else
   5.195 +      t
   5.196 +      |> attach_typeS
   5.197 +      |> whack_term thy whacks
   5.198 +      |> Object_Logic.atomize_term ctxt
   5.199 +      |> tap (fn t' => fastype_of t' <> @{typ prop} orelse raise TOO_META t)
   5.200 +      |> falsify ? HOLogic.mk_not
   5.201 +      |> unfold_basic_def ctxt
   5.202 +  end;
   5.203 +
   5.204 +val check_closed = tap (fn t => null (Term.add_vars t []) orelse raise UNEXPECTED_VAR t);
   5.205 +
   5.206 +val preprocess_prop = close_form [] oooo preprocess_term_basic;
   5.207 +val preprocess_closed_term = check_closed ooo preprocess_term_basic false;
   5.208 +
   5.209 +val is_type_builtin = member (op =) [@{type_name bool}, @{type_name fun}];
   5.210 +
   5.211 +val is_const_builtin =
   5.212 +  member (op =) [@{const_name All}, @{const_name conj}, @{const_name disj}, @{const_name Eps},
   5.213 +    @{const_name HOL.eq}, @{const_name Ex}, @{const_name False}, @{const_name If},
   5.214 +    @{const_name implies}, @{const_name Not}, @{const_name The}, @{const_name The_unsafe},
   5.215 +    @{const_name True}];
   5.216 +
   5.217 +datatype type_classification = Builtin | TVal | Copy | Quotient | Co_Datatype;
   5.218 +
   5.219 +fun classify_type_name ctxt T_name =
   5.220 +  if is_type_builtin T_name then
   5.221 +    Builtin
   5.222 +  else if T_name = @{type_name itself} then
   5.223 +    Co_Datatype
   5.224 +  else
   5.225 +    (case BNF_FP_Def_Sugar.fp_sugar_of ctxt T_name of
   5.226 +      SOME _ => Co_Datatype
   5.227 +    | NONE =>
   5.228 +      (case Ctr_Sugar.ctr_sugar_of ctxt T_name of
   5.229 +        SOME _ => Co_Datatype
   5.230 +      | NONE =>
   5.231 +        (case Quotient_Info.lookup_quotients ctxt T_name of
   5.232 +          SOME _ => Quotient
   5.233 +        | NONE =>
   5.234 +          if T_name = @{type_name set} then
   5.235 +            Copy
   5.236 +          else
   5.237 +            (case Typedef.get_info ctxt T_name of
   5.238 +              _ :: _ => Copy
   5.239 +            | [] => TVal))));
   5.240 +
   5.241 +fun fp_kind_of_ctr_sugar_kind Ctr_Sugar.Codatatype = BNF_Util.Greatest_FP
   5.242 +  | fp_kind_of_ctr_sugar_kind _ = BNF_Util.Least_FP;
   5.243 +
   5.244 +fun mutual_co_datatypes_of ctxt (T_name, Ts) =
   5.245 +  (if T_name = @{type_name itself} then
   5.246 +     (BNF_Util.Least_FP, [@{typ "'a itself"}], [[@{const Pure.type ('a)}]])
   5.247 +   else
   5.248 +     let
   5.249 +       val (fp, ctr_sugars) =
   5.250 +         (case BNF_FP_Def_Sugar.fp_sugar_of ctxt T_name of
   5.251 +           SOME (fp_sugar as {fp, fp_res = {Ts, ...}, ...}) =>
   5.252 +           (fp,
   5.253 +            (case Ts of
   5.254 +              [_] => [fp_sugar]
   5.255 +            | _ => map (the o BNF_FP_Def_Sugar.fp_sugar_of ctxt o fst o dest_Type) Ts)
   5.256 +            |> map (#ctr_sugar o #fp_ctr_sugar))
   5.257 +         | NONE =>
   5.258 +           (case Ctr_Sugar.ctr_sugar_of ctxt T_name of
   5.259 +             SOME (ctr_sugar as {kind, ...}) =>
   5.260 +             (* Any freely constructed type that is not a codatatype is considered a datatype. This
   5.261 +                is sound (but incomplete) for model finding. *)
   5.262 +             (fp_kind_of_ctr_sugar_kind kind, [ctr_sugar])));
   5.263 +     in
   5.264 +       (fp, map #T ctr_sugars, map #ctrs ctr_sugars)
   5.265 +     end)
   5.266 +  |> @{apply 3(2)} (map ((fn Type (s, _) => Type (s, Ts))))
   5.267 +  |> @{apply 3(3)} (map (map (Ctr_Sugar.mk_ctr Ts)));
   5.268 +
   5.269 +fun quotient_of ctxt T_name =
   5.270 +  (case Quotient_Info.lookup_quotients ctxt T_name of
   5.271 +    SOME {equiv_rel, qtyp, rtyp, quot_thm, ...} =>
   5.272 +    let val _ $ (_ $ _ $ abs $ rep) = Thm.prop_of quot_thm in
   5.273 +      (qtyp, rtyp, equiv_rel, abs, rep)
   5.274 +    end);
   5.275 +
   5.276 +fun copy_of ctxt T_name =
   5.277 +  if T_name = @{type_name set} then
   5.278 +    let
   5.279 +      val A = Logic.varifyT_global @{typ 'a};
   5.280 +      val absT = Type (@{type_name set}, [A]);
   5.281 +      val repT = A --> HOLogic.boolT;
   5.282 +      val wrt = Abs (Name.uu, repT, @{const True});
   5.283 +      val abs = Const (@{const_name Collect}, repT --> absT);
   5.284 +      val rep = Const (@{const_name rmember}, absT --> repT);
   5.285 +    in
   5.286 +      (absT, repT, wrt, abs, rep)
   5.287 +    end
   5.288 +  else
   5.289 +    (case Typedef.get_info ctxt T_name of
   5.290 +      (* When several entries are returned, it shouldn't matter much which one we take (according to
   5.291 +         Florian Haftmann). The "Logic.varifyT_global" calls are a workaround because these types'
   5.292 +         variables sometimes clash with locally fixed type variables. *)
   5.293 +      ({abs_type, rep_type, Abs_name, Rep_name, ...}, {Rep, ...}) :: _ =>
   5.294 +      let
   5.295 +        val absT = Logic.varifyT_global abs_type;
   5.296 +        val repT = Logic.varifyT_global rep_type;
   5.297 +        val wrt = Thm.prop_of Rep
   5.298 +          |> HOLogic.dest_Trueprop
   5.299 +          |> HOLogic.dest_mem
   5.300 +          |> snd;
   5.301 +        val abs = Const (Abs_name, repT --> absT);
   5.302 +        val rep = Const (Rep_name, absT --> repT);
   5.303 +      in
   5.304 +        (absT, repT, wrt, abs, rep)
   5.305 +      end);
   5.306 +
   5.307 +fun is_co_datatype_ctr ctxt (s, T) =
   5.308 +  (case body_type T of
   5.309 +    Type (fpT_name, Ts) =>
   5.310 +    classify_type_name ctxt fpT_name = Co_Datatype andalso
   5.311 +    let
   5.312 +      val ctrs =
   5.313 +        if fpT_name = @{type_name itself} then
   5.314 +          [Const (@{const_name Pure.type}, @{typ "'a itself"})]
   5.315 +        else
   5.316 +          (case BNF_FP_Def_Sugar.fp_sugar_of ctxt fpT_name of
   5.317 +            SOME {fp_ctr_sugar = {ctr_sugar = {ctrs, ...}, ...}, ...} => ctrs
   5.318 +          | NONE =>
   5.319 +            (case Ctr_Sugar.ctr_sugar_of ctxt fpT_name of
   5.320 +              SOME {ctrs, ...} => ctrs
   5.321 +            | _ => []));
   5.322 +
   5.323 +      fun is_right_ctr (t' as Const (s', _)) =
   5.324 +        s = s' andalso fastype_of (Ctr_Sugar.mk_ctr Ts t') = T;
   5.325 +    in
   5.326 +      exists is_right_ctr ctrs
   5.327 +    end
   5.328 +  | _  => false);
   5.329 +
   5.330 +fun dest_co_datatype_case ctxt (s, T) =
   5.331 +  let val thy = Proof_Context.theory_of ctxt in
   5.332 +    (case strip_fun_type (Sign.the_const_type thy s) of
   5.333 +      (gen_branch_Ts, gen_body_fun_T) =>
   5.334 +      (case gen_body_fun_T of
   5.335 +        Type (@{type_name fun}, [Type (fpT_name, _), _]) =>
   5.336 +        if classify_type_name ctxt fpT_name = Co_Datatype then
   5.337 +          let
   5.338 +            val Type (_, fpTs) = domain_type (funpow (length gen_branch_Ts) range_type T);
   5.339 +            val (ctrs0, Const (case_name, _)) =
   5.340 +              (case BNF_FP_Def_Sugar.fp_sugar_of ctxt fpT_name of
   5.341 +                SOME {fp_ctr_sugar = {ctr_sugar = {ctrs, casex, ...}, ...}, ...} => (ctrs, casex)
   5.342 +              | NONE =>
   5.343 +                (case Ctr_Sugar.ctr_sugar_of ctxt fpT_name of
   5.344 +                  SOME {ctrs, casex, ...} => (ctrs, casex)));
   5.345 +          in
   5.346 +            if s = case_name then map (dest_Const o Ctr_Sugar.mk_ctr fpTs) ctrs0
   5.347 +            else raise Fail "non-case"
   5.348 +          end
   5.349 +        else
   5.350 +          raise Fail "non-case"))
   5.351 +  end;
   5.352 +
   5.353 +val is_co_datatype_case = can o dest_co_datatype_case;
   5.354 +
   5.355 +fun is_quotient_abs ctxt (s, T) =
   5.356 +  (case T of
   5.357 +    Type (@{type_name fun}, [_, Type (absT_name, _)]) =>
   5.358 +    classify_type_name ctxt absT_name = Quotient andalso
   5.359 +    (case quotient_of ctxt absT_name of
   5.360 +      (_, _, _, Const (s', _), _) => s' = s)
   5.361 +  | _ => false);
   5.362 +
   5.363 +fun is_quotient_rep ctxt (s, T) =
   5.364 +  (case T of
   5.365 +    Type (@{type_name fun}, [Type (absT_name, _), _]) =>
   5.366 +    classify_type_name ctxt absT_name = Quotient andalso
   5.367 +    (case quotient_of ctxt absT_name of
   5.368 +      (_, _, _, _, Const (s', _)) => s' = s)
   5.369 +  | _ => false);
   5.370 +
   5.371 +fun is_maybe_copy_abs ctxt absT_name s =
   5.372 +  if absT_name = @{type_name set} then
   5.373 +    s = @{const_name Collect}
   5.374 +  else
   5.375 +    (case try (copy_of ctxt) absT_name of
   5.376 +      SOME (_, _, _, Const (s', _), _) => s' = s
   5.377 +    | NONE => false);
   5.378 +
   5.379 +fun is_maybe_copy_rep ctxt absT_name s =
   5.380 +  if absT_name = @{type_name set} then
   5.381 +    s = @{const_name rmember}
   5.382 +  else
   5.383 +    (case try (copy_of ctxt) absT_name of
   5.384 +      SOME (_, _, _, _, Const (s', _)) => s' = s
   5.385 +    | NONE => false);
   5.386 +
   5.387 +fun is_copy_abs ctxt (s, T) =
   5.388 +  (case T of
   5.389 +    Type (@{type_name fun}, [_, Type (absT_name, _)]) =>
   5.390 +    classify_type_name ctxt absT_name = Copy andalso is_maybe_copy_abs ctxt absT_name s
   5.391 +  | _ => false);
   5.392 +
   5.393 +fun is_copy_rep ctxt (s, T) =
   5.394 +  (case T of
   5.395 +    Type (@{type_name fun}, [Type (absT_name, _), _]) =>
   5.396 +    classify_type_name ctxt absT_name = Copy andalso is_maybe_copy_rep ctxt absT_name s
   5.397 +  | _ => false);
   5.398 +
   5.399 +fun is_stale_copy_abs ctxt (s, T) =
   5.400 +  (case T of
   5.401 +    Type (@{type_name fun}, [_, Type (absT_name, _)]) =>
   5.402 +    classify_type_name ctxt absT_name <> Copy andalso is_maybe_copy_abs ctxt absT_name s
   5.403 +  | _ => false);
   5.404 +
   5.405 +fun is_stale_copy_rep ctxt (s, T) =
   5.406 +  (case T of
   5.407 +    Type (@{type_name fun}, [Type (absT_name, _), _]) =>
   5.408 +    classify_type_name ctxt absT_name <> Copy andalso is_maybe_copy_rep ctxt absT_name s
   5.409 +  | _ => false);
   5.410 +
   5.411 +fun instantiate_constant_types_in_term ctxt csts target =
   5.412 +  let
   5.413 +    val thy = Proof_Context.theory_of ctxt;
   5.414 +
   5.415 +    fun try_const _ _ (res as SOME _) = res
   5.416 +      | try_const (s', T') cst NONE =
   5.417 +        (case cst of
   5.418 +          Const (s, T) =>
   5.419 +          if s = s' then
   5.420 +            SOME (Sign.typ_match thy (T', T) Vartab.empty)
   5.421 +            handle Type.TYPE_MATCH => NONE
   5.422 +          else
   5.423 +            NONE
   5.424 +        | _ => NONE);
   5.425 +
   5.426 +    fun subst_for (Const x) = fold (try_const x) csts NONE
   5.427 +      | subst_for (t as Free _) = if member (op aconv) csts t then SOME Vartab.empty else NONE
   5.428 +      | subst_for (t1 $ t2) = (case subst_for t1 of SOME subst => SOME subst | NONE => subst_for t2)
   5.429 +      | subst_for (Abs (_, _, t')) = subst_for t'
   5.430 +      | subst_for _ = NONE;
   5.431 +  in
   5.432 +    (case subst_for target of
   5.433 +      SOME subst => Envir.subst_term_types subst target
   5.434 +    | NONE => raise Type.TYPE_MATCH)
   5.435 +  end;
   5.436 +
   5.437 +datatype card = One | Fin | Fin_or_Inf | Inf
   5.438 +
   5.439 +(* Similar to "ATP_Util.tiny_card_of_type". *)
   5.440 +fun card_of_type ctxt =
   5.441 +  let
   5.442 +    fun max_card Inf _ = Inf
   5.443 +      | max_card _ Inf = Inf
   5.444 +      | max_card Fin_or_Inf _ = Fin_or_Inf
   5.445 +      | max_card _ Fin_or_Inf = Fin_or_Inf
   5.446 +      | max_card Fin _ = Fin
   5.447 +      | max_card _ Fin = Fin
   5.448 +      | max_card One One = One;
   5.449 +
   5.450 +    fun card_of avoid T =
   5.451 +      if member (op =) avoid T then
   5.452 +        Inf
   5.453 +      else
   5.454 +        (case T of
   5.455 +          TFree _ => Fin_or_Inf
   5.456 +        | TVar _ => Inf
   5.457 +        | Type (@{type_name fun}, [T1, T2]) =>
   5.458 +          (case (card_of avoid T1, card_of avoid T2) of
   5.459 +            (_, One) => One
   5.460 +          | (k1, k2) => max_card k1 k2)
   5.461 +        | Type (@{type_name prod}, [T1, T2]) =>
   5.462 +          (case (card_of avoid T1, card_of avoid T2) of
   5.463 +            (k1, k2) => max_card k1 k2)
   5.464 +        | Type (@{type_name set}, [T']) => card_of avoid (T' --> HOLogic.boolT)
   5.465 +        | Type (T_name, Ts) =>
   5.466 +          (case try (mutual_co_datatypes_of ctxt) (T_name, Ts) of
   5.467 +            NONE => Inf
   5.468 +          | SOME (_, fpTs, ctrss) =>
   5.469 +            (case ctrss of [[_]] => One | _ => Fin)
   5.470 +            |> fold (fold (fold (max_card o card_of (fpTs @ avoid)) o binder_types o fastype_of))
   5.471 +              ctrss));
   5.472 +  in
   5.473 +    card_of []
   5.474 +  end;
   5.475 +
   5.476 +fun int_of_classif Spec_Rules.Equational = 1
   5.477 +  | int_of_classif Spec_Rules.Inductive = 2
   5.478 +  | int_of_classif Spec_Rules.Co_Inductive = 3
   5.479 +  | int_of_classif Spec_Rules.Unknown = 4;
   5.480 +
   5.481 +val classif_ord = int_ord o apply2 int_of_classif;
   5.482 +
   5.483 +fun spec_rules_of ctxt (x as (s, T)) =
   5.484 +  let
   5.485 +    val thy = Proof_Context.theory_of ctxt;
   5.486 +
   5.487 +    fun subst_of t0 =
   5.488 +      try (Sign.typ_match thy (fastype_of t0, T)) Vartab.empty;
   5.489 +
   5.490 +    fun process_spec _ (res as SOME _) = res
   5.491 +      | process_spec (classif, (ts0, ths as _ :: _)) NONE =
   5.492 +        (case get_first subst_of ts0 of
   5.493 +          SOME subst =>
   5.494 +          (let
   5.495 +             val ts = map (Envir.subst_term_types subst) ts0;
   5.496 +             val poly_props = map Thm.prop_of ths;
   5.497 +             val props = map (instantiate_constant_types_in_term ctxt ts) poly_props;
   5.498 +           in
   5.499 +             if exists (exists (exists_type (exists_subtype is_TVar))) [ts, props] then NONE
   5.500 +             else SOME (classif, ts, props, poly_props)
   5.501 +           end
   5.502 +           handle Type.TYPE_MATCH => NONE)
   5.503 +        | NONE => NONE)
   5.504 +      | process_spec _ NONE = NONE;
   5.505 +
   5.506 +    fun spec_rules () =
   5.507 +      Spec_Rules.retrieve ctxt (Const x)
   5.508 +      |> sort (classif_ord o apply2 fst);
   5.509 +
   5.510 +    val specs =
   5.511 +      if s = @{const_name The} then
   5.512 +        [(Spec_Rules.Unknown, ([Logic.varify_global @{term The}], [@{thm theI_unique}]))]
   5.513 +      else if s = @{const_name finite} then
   5.514 +        let val card = card_of_type ctxt T in
   5.515 +          if card = Inf orelse card = Fin_or_Inf then
   5.516 +            spec_rules ()
   5.517 +          else
   5.518 +            [(Spec_Rules.Equational, ([Logic.varify_global @{term finite}],
   5.519 +               [Skip_Proof.make_thm thy (Logic.varify_global @{prop "finite A = True"})]))]
   5.520 +        end
   5.521 +      else
   5.522 +        spec_rules ();
   5.523 +  in
   5.524 +    fold process_spec specs NONE
   5.525 +  end;
   5.526 +
   5.527 +fun lhs_of_equation (Const (@{const_name Pure.eq}, _) $ t $ _) = t
   5.528 +  | lhs_of_equation (@{const Trueprop} $ (Const (@{const_name HOL.eq}, _) $ t $ _)) = t;
   5.529 +
   5.530 +fun specialize_definition_type thy x def0 =
   5.531 +  let
   5.532 +    val def = specialize_type thy x def0;
   5.533 +    val lhs = lhs_of_equation def;
   5.534 +  in
   5.535 +    if exists_Const (curry (op =) x) lhs then def else raise Fail "cannot specialize"
   5.536 +  end;
   5.537 +
   5.538 +fun definition_of thy (x as (s, _)) =
   5.539 +  Defs.specifications_of (Theory.defs_of thy) (Defs.Const, s)
   5.540 +  |> map_filter #def
   5.541 +  |> map_filter (try (specialize_definition_type thy x o Thm.prop_of o Thm.axiom thy))
   5.542 +  |> try hd;
   5.543 +
   5.544 +fun is_builtin_theory thy_id =
   5.545 +  Context.subthy_id (thy_id, Context.theory_id @{theory Hilbert_Choice});
   5.546 +
   5.547 +val orphan_axioms_of =
   5.548 +  Spec_Rules.get
   5.549 +  #> filter (curry (op =) Spec_Rules.Unknown o fst)
   5.550 +  #> map snd
   5.551 +  #> filter (null o fst)
   5.552 +  #> maps snd
   5.553 +  #> filter_out (is_builtin_theory o Thm.theory_id_of_thm)
   5.554 +  #> map Thm.prop_of;
   5.555 +
   5.556 +fun keys_of _ (ITVal (T, _)) = [key_of_typ T]
   5.557 +  | keys_of _ (ICopy {abs_typ, ...}) = [key_of_typ abs_typ]
   5.558 +  | keys_of _ (IQuotient {abs_typ, ...}) = [key_of_typ abs_typ]
   5.559 +  | keys_of _ (ICoData (_, specs)) = map (key_of_typ o #typ) specs
   5.560 +  | keys_of ctxt (IVal const) = [key_of_const ctxt const]
   5.561 +  | keys_of ctxt (ICoPred (_, _, specs)) = map (key_of_const ctxt o #const) specs
   5.562 +  | keys_of ctxt (IRec specs) = map (key_of_const ctxt o #const) specs
   5.563 +  | keys_of ctxt (ISpec {consts, ...}) = map (key_of_const ctxt) consts
   5.564 +  | keys_of _ (IAxiom _) = []
   5.565 +  | keys_of _ (IGoal _) = []
   5.566 +  | keys_of _ (IEval _) = [];
   5.567 +
   5.568 +fun co_data_spec_deps_of ctxt ({ctrs, ...} : isa_co_data_spec) =
   5.569 +  fold (add_keys ctxt) ctrs [];
   5.570 +fun const_spec_deps_of ctxt consts props =
   5.571 +  fold (add_keys ctxt) props [] |> subtract (op =) (map (key_of_const ctxt) consts);
   5.572 +fun consts_spec_deps_of ctxt {consts, props} =
   5.573 +  fold (add_keys ctxt) props [] |> subtract (op =) (map (key_of_const ctxt) consts);
   5.574 +
   5.575 +fun deps_of _ (ITVal _) = []
   5.576 +  | deps_of ctxt (ICopy {wrt, ...}) = add_keys ctxt wrt []
   5.577 +  | deps_of ctxt (IQuotient {wrt, ...}) = add_keys ctxt wrt []
   5.578 +  | deps_of ctxt (ICoData (_, specs)) = maps (co_data_spec_deps_of ctxt) specs
   5.579 +  | deps_of _ (IVal const) = add_type_keys (fastype_of const) []
   5.580 +  | deps_of ctxt (ICoPred (_, _, specs)) =
   5.581 +    maps (const_spec_deps_of ctxt (map #const specs) o #props) specs
   5.582 +  | deps_of ctxt (IRec specs) = maps (const_spec_deps_of ctxt (map #const specs) o #props) specs
   5.583 +  | deps_of ctxt (ISpec spec) = consts_spec_deps_of ctxt spec
   5.584 +  | deps_of ctxt (IAxiom prop) = add_keys ctxt prop []
   5.585 +  | deps_of ctxt (IGoal prop) = add_keys ctxt prop []
   5.586 +  | deps_of ctxt (IEval t) = add_keys ctxt t [];
   5.587 +
   5.588 +fun consts_of_rec_or_spec (IRec specs) = map #const specs
   5.589 +  | consts_of_rec_or_spec (ISpec {consts, ...}) = consts;
   5.590 +
   5.591 +fun props_of_rec_or_spec (IRec specs) = maps #props specs
   5.592 +  | props_of_rec_or_spec (ISpec {props, ...}) = props;
   5.593 +
   5.594 +fun merge_two_rec_or_spec cmd cmd' =
   5.595 +  ISpec {consts = consts_of_rec_or_spec cmd @ consts_of_rec_or_spec cmd',
   5.596 +    props = props_of_rec_or_spec cmd @ props_of_rec_or_spec cmd'};
   5.597 +
   5.598 +fun merge_two (ICoData (fp, specs)) (ICoData (fp', specs'), complete) =
   5.599 +    (ICoData (BNF_Util.case_fp fp fp fp', specs @ specs'), complete andalso fp = fp')
   5.600 +  | merge_two (IRec specs) (IRec specs', complete) = (IRec (specs @ specs'), complete)
   5.601 +  | merge_two (cmd as IRec _) (cmd' as ISpec _, complete) =
   5.602 +    (merge_two_rec_or_spec cmd cmd', complete)
   5.603 +  | merge_two (cmd as ISpec _) (cmd' as IRec _, complete) =
   5.604 +    (merge_two_rec_or_spec cmd cmd', complete)
   5.605 +  | merge_two (cmd as ISpec _) (cmd' as ISpec _, complete) =
   5.606 +    (merge_two_rec_or_spec cmd cmd', complete)
   5.607 +  | merge_two _ _ = raise CYCLIC_DEPS ();
   5.608 +
   5.609 +fun sort_isa_commands_topologically ctxt cmds =
   5.610 +  let
   5.611 +    fun normal_pairs [] = []
   5.612 +      | normal_pairs (all as normal :: _) = map (rpair normal) all;
   5.613 +
   5.614 +    fun add_node [] _ = I
   5.615 +      | add_node (normal :: _) cmd = Graph.new_node (normal, cmd);
   5.616 +
   5.617 +    fun merge_scc (cmd :: cmds) complete = fold merge_two cmds (cmd, complete);
   5.618 +
   5.619 +    fun sort_problem (cmds, complete) =
   5.620 +      let
   5.621 +        val keyss = map (keys_of ctxt) cmds;
   5.622 +        val normal_keys = Symtab.make (maps normal_pairs keyss);
   5.623 +        val normalize = Symtab.lookup normal_keys;
   5.624 +
   5.625 +        fun add_deps [] _ = I
   5.626 +          | add_deps (normal :: _) cmd =
   5.627 +            let
   5.628 +              val deps = deps_of ctxt cmd
   5.629 +                |> map_filter normalize
   5.630 +                |> remove (op =) normal;
   5.631 +            in
   5.632 +              fold (fn dep => Graph.add_edge (dep, normal)) deps
   5.633 +            end;
   5.634 +
   5.635 +        val cmd_of_key = the o AList.lookup (op =) (map hd keyss ~~ cmds);
   5.636 +
   5.637 +        val G = Graph.empty
   5.638 +          |> fold2 add_node keyss cmds
   5.639 +          |> fold2 add_deps keyss cmds;
   5.640 +
   5.641 +        val cmd_sccs = rev (Graph.strong_conn G)
   5.642 +          |> map (map cmd_of_key);
   5.643 +      in
   5.644 +        if exists (can (fn _ :: _ :: _ => ())) cmd_sccs then
   5.645 +          sort_problem (fold_map merge_scc cmd_sccs complete)
   5.646 +        else
   5.647 +          (Graph.schedule (K snd) G, complete)
   5.648 +      end;
   5.649 +
   5.650 +    val typedecls = filter (can (fn ITVal _ => ())) cmds;
   5.651 +    val (mixed, complete) =
   5.652 +      (filter (can (fn ICopy _ => () | IQuotient _ => () | ICoData _ => () | IVal _ => ()
   5.653 +         | ICoPred _ => () | IRec _ => () | ISpec _ => ())) cmds, true)
   5.654 +      |> sort_problem;
   5.655 +    val axioms = filter (can (fn IAxiom _ => ())) cmds;
   5.656 +    val goals = filter (can (fn IGoal _ => ())) cmds;
   5.657 +    val evals = filter (can (fn IEval _ => ())) cmds;
   5.658 +  in
   5.659 +    (typedecls @ mixed @ axioms @ goals @ evals, complete)
   5.660 +  end;
   5.661 +
   5.662 +fun group_of (ITVal _) = 1
   5.663 +  | group_of (ICopy _) = 2
   5.664 +  | group_of (IQuotient _) = 3
   5.665 +  | group_of (ICoData _) = 4
   5.666 +  | group_of (IVal _) = 5
   5.667 +  | group_of (ICoPred _) = 6
   5.668 +  | group_of (IRec _) = 7
   5.669 +  | group_of (ISpec _) = 8
   5.670 +  | group_of (IAxiom _) = 9
   5.671 +  | group_of (IGoal _) = 10
   5.672 +  | group_of (IEval _) = 11;
   5.673 +
   5.674 +fun group_isa_commands [] = []
   5.675 +  | group_isa_commands [cmd] = [[cmd]]
   5.676 +  | group_isa_commands (cmd :: cmd' :: cmds) =
   5.677 +    let val (group :: groups) = group_isa_commands (cmd' :: cmds) in
   5.678 +      if group_of cmd = group_of cmd' then
   5.679 +        (cmd :: group) :: groups
   5.680 +      else
   5.681 +        [cmd] :: (group :: groups)
   5.682 +    end;
   5.683 +
   5.684 +fun defined_by (Const (@{const_name All}, _) $ t) = defined_by t
   5.685 +  | defined_by (Abs (_, _, t)) = defined_by t
   5.686 +  | defined_by (@{const implies} $ _ $ u) = defined_by u
   5.687 +  | defined_by (Const (@{const_name HOL.eq}, _) $ t $ _) = head_of t
   5.688 +  | defined_by t = head_of t;
   5.689 +
   5.690 +fun partition_props [_] props = SOME [props]
   5.691 +  | partition_props consts props =
   5.692 +    let
   5.693 +      val propss = map (fn const => filter (fn prop => defined_by prop aconv const) props) consts;
   5.694 +    in
   5.695 +      if eq_set (op aconv) (props, flat propss) andalso forall (not o null) propss then SOME propss
   5.696 +      else NONE
   5.697 +    end;
   5.698 +
   5.699 +fun hol_concl_head (Const (@{const_name All}, _) $ Abs (_, _, t)) = hol_concl_head t
   5.700 +  | hol_concl_head (Const (@{const_name implies}, _) $ _ $ t) = hol_concl_head t
   5.701 +  | hol_concl_head (t $ _) = hol_concl_head t
   5.702 +  | hol_concl_head t = t;
   5.703 +
   5.704 +fun is_inductive_set_intro t =
   5.705 +  (case hol_concl_head t of
   5.706 +    Const (@{const_name rmember}, _) => true
   5.707 +  | _ => false);
   5.708 +
   5.709 +exception NO_TRIPLE of unit;
   5.710 +
   5.711 +fun triple_for_intro_rule ctxt x rule =
   5.712 +  let
   5.713 +    val (prems, concl) = Logic.strip_horn rule
   5.714 +      |>> map (Object_Logic.atomize_term ctxt)
   5.715 +      ||> Object_Logic.atomize_term ctxt;
   5.716 +
   5.717 +    val (mains, sides) = List.partition (exists_Const (curry (op =) x)) prems;
   5.718 +
   5.719 +    val is_right_head = curry (op aconv) (Const x) o head_of;
   5.720 +  in
   5.721 +    if forall is_right_head mains then (sides, mains, concl) else raise NO_TRIPLE ()
   5.722 +  end;
   5.723 +
   5.724 +val tuple_for_args = HOLogic.mk_tuple o snd o strip_comb;
   5.725 +
   5.726 +fun wf_constraint_for rel sides concl mains =
   5.727 +  HOLogic.mk_mem (HOLogic.mk_prod (apply2 tuple_for_args (mains, concl)), Var rel)
   5.728 +  |> fold (curry HOLogic.mk_imp) sides
   5.729 +  |> close_form [rel];
   5.730 +
   5.731 +fun wf_constraint_for_triple rel (sides, mains, concl) =
   5.732 +  map (wf_constraint_for rel sides concl) mains
   5.733 +  |> foldr1 HOLogic.mk_conj;
   5.734 +
   5.735 +fun terminates_by ctxt timeout goal tac =
   5.736 +  can (SINGLE (Classical.safe_tac ctxt) #> the
   5.737 +    #> SINGLE (DETERM_TIMEOUT timeout (tac ctxt (auto_tac ctxt))) #> the
   5.738 +    #> Goal.finish ctxt) goal;
   5.739 +
   5.740 +val max_cached_wfs = 50;
   5.741 +val cached_timeout = Synchronized.var "Nunchaku_Collect.cached_timeout" Time.zeroTime;
   5.742 +val cached_wf_props = Synchronized.var "Nunchaku_Collect.cached_wf_props" ([] : (term * bool) list);
   5.743 +
   5.744 +val termination_tacs = [Lexicographic_Order.lex_order_tac true, ScnpReconstruct.sizechange_tac];
   5.745 +
   5.746 +fun is_wellfounded_inductive_predicate ctxt wfs debug wf_timeout const intros =
   5.747 +  let
   5.748 +    val thy = Proof_Context.theory_of ctxt;
   5.749 +
   5.750 +    val Const (x as (_, T)) = head_of (HOLogic.dest_Trueprop (Logic.strip_imp_concl (hd intros)));
   5.751 +  in
   5.752 +    (case triple_lookup (const_match thy o swap) wfs (dest_Const const) of
   5.753 +      SOME (SOME wf) => wf
   5.754 +    | _ =>
   5.755 +      (case map (triple_for_intro_rule ctxt x) intros |> filter_out (null o #2) of
   5.756 +        [] => true
   5.757 +      | triples =>
   5.758 +        let
   5.759 +          val binders_T = HOLogic.mk_tupleT (binder_types T);
   5.760 +          val rel_T = HOLogic.mk_setT (HOLogic.mk_prodT (binders_T, binders_T));
   5.761 +          val j = fold (Integer.max o maxidx_of_term) intros 0 + 1;
   5.762 +          val rel = (("R", j), rel_T);
   5.763 +          val prop =
   5.764 +            Const (@{const_name wf}, rel_T --> HOLogic.boolT) $ Var rel ::
   5.765 +            map (wf_constraint_for_triple rel) triples
   5.766 +            |> foldr1 HOLogic.mk_conj
   5.767 +            |> HOLogic.mk_Trueprop;
   5.768 +        in
   5.769 +          if debug then writeln ("Wellfoundedness goal: " ^ Syntax.string_of_term ctxt prop)
   5.770 +          else ();
   5.771 +          if wf_timeout = Synchronized.value cached_timeout andalso
   5.772 +             length (Synchronized.value cached_wf_props) < max_cached_wfs then
   5.773 +            ()
   5.774 +          else
   5.775 +            (Synchronized.change cached_wf_props (K []);
   5.776 +             Synchronized.change cached_timeout (K wf_timeout));
   5.777 +          (case AList.lookup (op =) (Synchronized.value cached_wf_props) prop of
   5.778 +            SOME wf => wf
   5.779 +          | NONE =>
   5.780 +            let
   5.781 +              val goal = Goal.init (Thm.cterm_of ctxt prop);
   5.782 +              val wf = exists (terminates_by ctxt wf_timeout goal) termination_tacs;
   5.783 +            in
   5.784 +              Synchronized.change cached_wf_props (cons (prop, wf)); wf
   5.785 +            end)
   5.786 +        end)
   5.787 +      handle
   5.788 +        List.Empty => false
   5.789 +      | NO_TRIPLE () => false)
   5.790 +  end;
   5.791 +
   5.792 +datatype lhs_pat =
   5.793 +  Only_Vars
   5.794 +| Prim_Pattern of string
   5.795 +| Any_Pattern;
   5.796 +
   5.797 +fun is_likely_pat_complete ctxt props =
   5.798 +  let
   5.799 +    val is_Var_or_Bound = is_Var orf is_Bound;
   5.800 +
   5.801 +    fun lhs_pat_of t =
   5.802 +      (case t of
   5.803 +        Const (@{const_name All}, _) $ Abs (_, _, t) => lhs_pat_of t
   5.804 +      | Const (@{const_name HOL.eq}, _) $ u $ _ =>
   5.805 +        (case filter_out is_Var_or_Bound (snd (strip_comb u)) of
   5.806 +          [] => Only_Vars
   5.807 +        | [v] =>
   5.808 +          (case strip_comb v of
   5.809 +            (cst as Const (_, T), args) =>
   5.810 +            (case body_type T of
   5.811 +              Type (T_name, _) =>
   5.812 +              if can (Ctr_Sugar.dest_ctr ctxt T_name) cst andalso forall is_Var_or_Bound args then
   5.813 +                Prim_Pattern T_name
   5.814 +              else
   5.815 +                Any_Pattern
   5.816 +            | _ => Any_Pattern)
   5.817 +          | _ => Any_Pattern)
   5.818 +        | _ => Any_Pattern)
   5.819 +      | _ => Any_Pattern);
   5.820 +  in
   5.821 +    (case map lhs_pat_of props of
   5.822 +      [] => false
   5.823 +    | pats as Prim_Pattern T_name :: _ =>
   5.824 +      forall (can (fn Prim_Pattern _ => ())) pats andalso
   5.825 +      length pats = length (#ctrs (the (Ctr_Sugar.ctr_sugar_of ctxt T_name)))
   5.826 +    | pats => forall (curry (op =) Only_Vars) pats)
   5.827 +  end;
   5.828 +
   5.829 +(* Prevents divergence in case of cyclic or infinite axiom dependencies. *)
   5.830 +val axioms_max_depth = 255
   5.831 +
   5.832 +fun isa_problem_of_subgoal ctxt falsify wfs whacks cards debug wf_timeout evals0 some_assms0
   5.833 +    subgoal0 =
   5.834 +  let
   5.835 +    val thy = Proof_Context.theory_of ctxt;
   5.836 +
   5.837 +    fun card_of T =
   5.838 +      (case triple_lookup (typ_match thy o swap) cards T of
   5.839 +        NONE => (NONE, NONE)
   5.840 +      | SOME (c1, c2) => (if c1 = SOME 1 then NONE else c1, c2));
   5.841 +
   5.842 +    fun axioms_of_class class =
   5.843 +      #axioms (Axclass.get_info thy class)
   5.844 +      handle ERROR _ => [];
   5.845 +
   5.846 +    fun monomorphize_class_axiom T t =
   5.847 +      (case Term.add_tvars t [] of
   5.848 +        [] => t
   5.849 +      | [(x, S)] => Envir.subst_term_types (Vartab.make [(x, (S, T))]) t);
   5.850 +
   5.851 +    fun consider_sort depth T S (seens as (seenS, seenT, seen), problem) =
   5.852 +      if member (op =) seenS S then
   5.853 +        (seens, problem)
   5.854 +      else if depth > axioms_max_depth then
   5.855 +        raise TOO_DEEP_DEPS ()
   5.856 +      else
   5.857 +        let
   5.858 +          val seenS = S :: seenS;
   5.859 +          val seens = (seenS, seenT, seen);
   5.860 +
   5.861 +          val supers = Sign.complete_sort thy S;
   5.862 +          val axioms0 = maps (map Thm.prop_of o axioms_of_class) supers;
   5.863 +          val axioms = map (preprocess_prop false ctxt whacks o monomorphize_class_axiom T) axioms0;
   5.864 +        in
   5.865 +          (seens, map IAxiom axioms @ problem)
   5.866 +          |> fold (consider_term (depth + 1)) axioms
   5.867 +        end
   5.868 +    and consider_type depth T =
   5.869 +      (case T of
   5.870 +        Type (s, Ts) =>
   5.871 +        if is_type_builtin s then fold (consider_type depth) Ts
   5.872 +        else consider_non_builtin_type depth T
   5.873 +      | _ => consider_non_builtin_type depth T)
   5.874 +    and consider_non_builtin_type depth T (seens as (seenS, seenT, seen), problem) =
   5.875 +      if member (op =) seenT T then
   5.876 +        (seens, problem)
   5.877 +      else
   5.878 +        let
   5.879 +          val seenT = T :: seenT;
   5.880 +          val seens = (seenS, seenT, seen);
   5.881 +
   5.882 +          fun consider_quotient_or_copy tuple_of s =
   5.883 +            let
   5.884 +              val (T0, repT0, wrt0, abs0, rep0) = tuple_of ctxt s;
   5.885 +              val tyenv = Sign.typ_match thy (T0, T) Vartab.empty;
   5.886 +              val substT = Envir.subst_type tyenv;
   5.887 +              val subst = Envir.subst_term_types tyenv;
   5.888 +              val repT = substT repT0;
   5.889 +              val wrt = subst wrt0;
   5.890 +              val abs = subst abs0;
   5.891 +              val rep = subst rep0;
   5.892 +            in
   5.893 +              apsnd (cons (ICopy {abs_typ = T, rep_typ = repT, wrt = wrt, abs = abs,
   5.894 +                rep = rep}))
   5.895 +              #> consider_term (depth + 1) wrt
   5.896 +            end;
   5.897 +        in
   5.898 +          (seens, problem)
   5.899 +          |> (case T of
   5.900 +               TFree (_, S) =>
   5.901 +               apsnd (cons (ITVal (T, card_of T)))
   5.902 +               #> consider_sort depth T S
   5.903 +             | TVar (_, S) => consider_sort depth T S
   5.904 +             | Type (s, Ts) =>
   5.905 +               fold (consider_type depth) Ts
   5.906 +               #> (case classify_type_name ctxt s of
   5.907 +                    Co_Datatype =>
   5.908 +                    let
   5.909 +                      val (fp, fpTs, ctrss) = mutual_co_datatypes_of ctxt (s, Ts);
   5.910 +                      val specs = map2 (fn T => fn ctrs => {typ = T, ctrs = ctrs}) fpTs ctrss;
   5.911 +                    in
   5.912 +                      (fn ((seenS, seenT, seen), problem) =>
   5.913 +                          ((seenS, union (op =) fpTs seenT, seen), ICoData (fp, specs) :: problem))
   5.914 +                      #> fold (fold (consider_type (depth + 1) o fastype_of)) ctrss
   5.915 +                    end
   5.916 +                  | Quotient => consider_quotient_or_copy quotient_of s
   5.917 +                  | Copy => consider_quotient_or_copy copy_of s
   5.918 +                  | TVal => apsnd (cons (ITVal (T, card_of T)))))
   5.919 +        end
   5.920 +    and consider_term depth t =
   5.921 +      (case t of
   5.922 +        t1 $ t2 => fold (consider_term depth) [t1, t2]
   5.923 +      | Var (_, T) => consider_type depth T
   5.924 +      | Bound _ => I
   5.925 +      | Abs (_, T, t') =>
   5.926 +        consider_term depth t'
   5.927 +        #> consider_type depth T
   5.928 +      | _ => (fn (seens as (seenS, seenT, seen), problem) =>
   5.929 +          if member (op aconv) seen t then
   5.930 +            (seens, problem)
   5.931 +          else if depth > axioms_max_depth then
   5.932 +            raise TOO_DEEP_DEPS ()
   5.933 +          else
   5.934 +            let
   5.935 +              val seen = t :: seen;
   5.936 +              val seens = (seenS, seenT, seen);
   5.937 +            in
   5.938 +              (case t of
   5.939 +                Const (x as (s, T)) =>
   5.940 +                (if is_const_builtin s orelse is_co_datatype_ctr ctxt x orelse
   5.941 +                    is_co_datatype_case ctxt x orelse is_quotient_abs ctxt x orelse
   5.942 +                    is_quotient_rep ctxt x orelse is_copy_abs ctxt x orelse
   5.943 +                    is_copy_rep ctxt x then
   5.944 +                   (seens, problem)
   5.945 +                 else if is_stale_copy_abs ctxt x orelse is_stale_copy_rep ctxt x then
   5.946 +                   raise UNSUPPORTED_FUNC t
   5.947 +                 else
   5.948 +                   (case spec_rules_of ctxt x of
   5.949 +                     SOME (classif, consts, props0, poly_props) =>
   5.950 +                     let
   5.951 +                       val props = map (preprocess_prop false ctxt whacks) props0;
   5.952 +
   5.953 +                       fun def_or_spec () =
   5.954 +                         (case definition_of thy x of
   5.955 +                           SOME eq0 =>
   5.956 +                           let val eq = preprocess_prop false ctxt whacks eq0 in
   5.957 +                             ([eq], [IRec [{const = t, props = [eq], pat_complete = true}]])
   5.958 +                           end
   5.959 +                         | NONE => (props, [ISpec {consts = consts, props = props}]));
   5.960 +
   5.961 +                       val (props', cmds) =
   5.962 +                         if null props then
   5.963 +                           ([], map IVal consts)
   5.964 +                         else if classif = Spec_Rules.Equational then
   5.965 +                           (case partition_props consts props of
   5.966 +                             SOME propss =>
   5.967 +                             (props,
   5.968 +                              [IRec (map2 (fn const => fn props =>
   5.969 +                                   {const = const, props = props,
   5.970 +                                    pat_complete = is_likely_pat_complete ctxt props})
   5.971 +                                 consts propss)])
   5.972 +                           | NONE => def_or_spec ())
   5.973 +                         else if member (op =) [Spec_Rules.Inductive, Spec_Rules.Co_Inductive]
   5.974 +                             classif then
   5.975 +                           if is_inductive_set_intro (hd props) then
   5.976 +                             def_or_spec ()
   5.977 +                           else
   5.978 +                             (case partition_props consts props of
   5.979 +                               SOME propss =>
   5.980 +                               (props,
   5.981 +                                [ICoPred (if classif = Spec_Rules.Inductive then BNF_Util.Least_FP
   5.982 +                                   else BNF_Util.Greatest_FP,
   5.983 +                                 length consts = 1 andalso
   5.984 +                                 is_wellfounded_inductive_predicate ctxt wfs debug wf_timeout
   5.985 +                                   (the_single consts) poly_props,
   5.986 +                                 map2 (fn const => fn props => {const = const, props = props})
   5.987 +                                   consts propss)])
   5.988 +                             | NONE => def_or_spec ())
   5.989 +                         else
   5.990 +                           def_or_spec ();
   5.991 +                     in
   5.992 +                       ((seenS, seenT, union (op aconv) consts seen), cmds @ problem)
   5.993 +                       |> fold (consider_term (depth + 1)) props'
   5.994 +                     end
   5.995 +                   | NONE =>
   5.996 +                     (case definition_of thy x of
   5.997 +                       SOME eq0 =>
   5.998 +                       let val eq = preprocess_prop false ctxt whacks eq0 in
   5.999 +                         (seens, IRec [{const = t, props = [eq], pat_complete = true}] :: problem)
  5.1000 +                         |> consider_term (depth + 1) eq
  5.1001 +                       end
  5.1002 +                     | NONE => (seens, IVal t :: problem))))
  5.1003 +                |> consider_type depth T
  5.1004 +              | Free (_, T) =>
  5.1005 +                (seens, IVal t :: problem)
  5.1006 +                |> consider_type depth T)
  5.1007 +            end));
  5.1008 +
  5.1009 +    val (poly_axioms, mono_axioms0) = orphan_axioms_of ctxt
  5.1010 +      |> List.partition has_polymorphism;
  5.1011 +
  5.1012 +    fun implicit_evals_of pol (@{const Not} $ t) = implicit_evals_of (not pol) t
  5.1013 +      | implicit_evals_of pol (@{const implies} $ t $ u) =
  5.1014 +        (case implicit_evals_of pol u of
  5.1015 +          [] => implicit_evals_of (not pol) t
  5.1016 +        | ts => ts)
  5.1017 +      | implicit_evals_of pol (@{const conj} $ t $ u) =
  5.1018 +        union (op aconv) (implicit_evals_of pol t) (implicit_evals_of pol u)
  5.1019 +      | implicit_evals_of pol (@{const disj} $ t $ u) =
  5.1020 +        union (op aconv) (implicit_evals_of pol t) (implicit_evals_of pol u)
  5.1021 +      | implicit_evals_of false (Const (@{const_name HOL.eq}, _) $ t $ u) =
  5.1022 +        distinct (op aconv) [t, u]
  5.1023 +      | implicit_evals_of true (Const (@{const_name HOL.eq}, _) $ t $ _) = [t]
  5.1024 +      | implicit_evals_of _ _ = [];
  5.1025 +
  5.1026 +    val mono_axioms_and_some_assms =
  5.1027 +      map (preprocess_prop false ctxt whacks) (mono_axioms0 @ some_assms0);
  5.1028 +    val subgoal = preprocess_prop falsify ctxt whacks subgoal0;
  5.1029 +    val implicit_evals = implicit_evals_of true subgoal;
  5.1030 +    val evals = map (preprocess_closed_term ctxt whacks) evals0;
  5.1031 +    val seens = ([], [], []);
  5.1032 +
  5.1033 +    val (commandss, complete) =
  5.1034 +      (seens,
  5.1035 +       map IAxiom mono_axioms_and_some_assms @ [IGoal subgoal] @ map IEval (implicit_evals @ evals))
  5.1036 +      |> fold (consider_term 0) (subgoal :: evals @ mono_axioms_and_some_assms)
  5.1037 +      |> snd
  5.1038 +      |> rev (* prettier *)
  5.1039 +      |> sort_isa_commands_topologically ctxt
  5.1040 +      |>> group_isa_commands;
  5.1041 +  in
  5.1042 +    (poly_axioms, {commandss = commandss, sound = true, complete = complete})
  5.1043 +  end;
  5.1044 +
  5.1045 +fun add_pat_complete_of_command cmd =
  5.1046 +  (case cmd of
  5.1047 +    ICoPred (_, _, specs) => union (op =) (map #const specs)
  5.1048 +  | IRec specs =>
  5.1049 +    union (op =) (map_filter (try (fn {const, pat_complete = true, ...} => const)) specs)
  5.1050 +  | _ => I);
  5.1051 +
  5.1052 +fun pat_completes_of_isa_problem {commandss, ...} =
  5.1053 +  fold (fold add_pat_complete_of_command) commandss [];
  5.1054 +
  5.1055 +fun str_of_isa_term_with_type ctxt t =
  5.1056 +  Syntax.string_of_term ctxt t ^ " : " ^ Syntax.string_of_typ ctxt (fastype_of t);
  5.1057 +
  5.1058 +fun is_triv_wrt (Abs (_, _, body)) = is_triv_wrt body
  5.1059 +  | is_triv_wrt @{const True} = true
  5.1060 +  | is_triv_wrt _ = false;
  5.1061 +
  5.1062 +fun str_of_isa_type_spec ctxt {abs_typ, rep_typ, wrt, abs, rep} =
  5.1063 +  Syntax.string_of_typ ctxt abs_typ ^ " := " ^ Syntax.string_of_typ ctxt rep_typ ^
  5.1064 +  (if is_triv_wrt wrt then "" else "\n  wrt " ^ Syntax.string_of_term ctxt wrt) ^
  5.1065 +  "\n  abstract " ^ Syntax.string_of_term ctxt abs ^
  5.1066 +  "\n  concrete " ^ Syntax.string_of_term ctxt rep;
  5.1067 +
  5.1068 +fun str_of_isa_co_data_spec ctxt {typ, ctrs} =
  5.1069 +  Syntax.string_of_typ ctxt typ ^ " :=\n  " ^
  5.1070 +  space_implode "\n| " (map (str_of_isa_term_with_type ctxt) ctrs);
  5.1071 +
  5.1072 +fun str_of_isa_const_spec ctxt {const, props} =
  5.1073 +  str_of_isa_term_with_type ctxt const ^ " :=\n  " ^
  5.1074 +  space_implode ";\n  " (map (Syntax.string_of_term ctxt) props);
  5.1075 +
  5.1076 +fun str_of_isa_rec_spec ctxt {const, props, pat_complete} =
  5.1077 +  str_of_isa_term_with_type ctxt const ^ (if pat_complete then " [pat_complete]" else "") ^
  5.1078 +  " :=\n " ^ space_implode ";\n " (map (Syntax.string_of_term ctxt) props);
  5.1079 +
  5.1080 +fun str_of_isa_consts_spec ctxt {consts, props} =
  5.1081 +  space_implode " and\n     " (map (str_of_isa_term_with_type ctxt) consts) ^ " :=\n  " ^
  5.1082 +  space_implode ";\n  " (map (Syntax.string_of_term ctxt) props);
  5.1083 +
  5.1084 +fun str_of_isa_card NONE = ""
  5.1085 +  | str_of_isa_card (SOME k) = signed_string_of_int k;
  5.1086 +
  5.1087 +fun str_of_isa_cards_suffix (NONE, NONE) = ""
  5.1088 +  | str_of_isa_cards_suffix (c1, c2) = " " ^ str_of_isa_card c1 ^ "-" ^ str_of_isa_card c2;
  5.1089 +
  5.1090 +fun str_of_isa_command ctxt (ITVal (T, cards)) =
  5.1091 +    "type " ^ Syntax.string_of_typ ctxt T ^ str_of_isa_cards_suffix cards
  5.1092 +  | str_of_isa_command ctxt (ICopy spec) = "copy " ^ str_of_isa_type_spec ctxt spec
  5.1093 +  | str_of_isa_command ctxt (IQuotient spec) = "quotient " ^ str_of_isa_type_spec ctxt spec
  5.1094 +  | str_of_isa_command ctxt (ICoData (fp, specs)) =
  5.1095 +    BNF_Util.case_fp fp "data" "codata" ^ " " ^ str_of_and_list (str_of_isa_co_data_spec ctxt) specs
  5.1096 +  | str_of_isa_command ctxt (IVal t) = "val " ^ str_of_isa_term_with_type ctxt t
  5.1097 +  | str_of_isa_command ctxt (ICoPred (fp, wf, specs)) =
  5.1098 +    BNF_Util.case_fp fp "pred" "copred" ^ " " ^ (if wf then "[wf] " else "") ^
  5.1099 +    str_of_and_list (str_of_isa_const_spec ctxt) specs
  5.1100 +  | str_of_isa_command ctxt (IRec specs) = "rec " ^ str_of_and_list (str_of_isa_rec_spec ctxt) specs
  5.1101 +  | str_of_isa_command ctxt (ISpec spec) = "spec " ^ str_of_isa_consts_spec ctxt spec
  5.1102 +  | str_of_isa_command ctxt (IAxiom prop) = "axiom " ^ Syntax.string_of_term ctxt prop
  5.1103 +  | str_of_isa_command ctxt (IGoal prop) = "goal " ^ Syntax.string_of_term ctxt prop
  5.1104 +  | str_of_isa_command ctxt (IEval t) = "eval " ^ Syntax.string_of_term ctxt t;
  5.1105 +
  5.1106 +fun str_of_isa_problem ctxt {commandss, sound, complete} =
  5.1107 +  map (cat_lines o map (suffix "." o str_of_isa_command ctxt)) commandss
  5.1108 +  |> space_implode "\n\n" |> suffix "\n"
  5.1109 +  |> prefix ("# " ^ (if sound then "sound" else "unsound") ^ "\n")
  5.1110 +  |> prefix ("# " ^ (if complete then "complete" else "incomplete") ^ "\n");
  5.1111 +
  5.1112 +end;
     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/src/HOL/Nunchaku/Tools/nunchaku_commands.ML	Mon Oct 24 22:42:07 2016 +0200
     6.3 @@ -0,0 +1,258 @@
     6.4 +(*  Title:      HOL/Nunchaku/Tools/nunchaku_commands.ML
     6.5 +    Author:     Jasmin Blanchette, Inria Nancy, LORIA, MPII
     6.6 +    Copyright   2015, 2016
     6.7 +
     6.8 +Adds the "nunchaku" and "nunchaku_params" commands to Isabelle/Isar's outer syntax.
     6.9 +*)
    6.10 +
    6.11 +signature NUNCHAKU_COMMANDS =
    6.12 +sig
    6.13 +  type params = Nunchaku.params
    6.14 +
    6.15 +  val default_params: theory -> (string * string) list -> params
    6.16 +end;
    6.17 +
    6.18 +structure Nunchaku_Commands : NUNCHAKU_COMMANDS =
    6.19 +struct
    6.20 +
    6.21 +open Nunchaku_Util;
    6.22 +open Nunchaku;
    6.23 +
    6.24 +type raw_param = string * string list;
    6.25 +
    6.26 +val default_default_params =
    6.27 +  [("assms", "true"),
    6.28 +   ("debug", "false"),
    6.29 +   ("falsify", "true"),
    6.30 +   ("max_genuine", "1"),
    6.31 +   ("max_potential", "1"),
    6.32 +   ("overlord", "false"),
    6.33 +   ("specialize", "true"),
    6.34 +   ("spy", "false"),
    6.35 +   ("timeout", "30"),
    6.36 +   ("verbose", "false"),
    6.37 +   ("wf_timeout", "0.5")];
    6.38 +
    6.39 +val negated_params =
    6.40 +  [("dont_whack", "whack"),
    6.41 +   ("dont_specialize", "specialize"),
    6.42 +   ("dont_spy", "spy"),
    6.43 +   ("no_assms", "assms"),
    6.44 +   ("no_debug", "debug"),
    6.45 +   ("no_overlord", "overlord"),
    6.46 +   ("non_mono", "mono"),
    6.47 +   ("non_wf", "wf"),
    6.48 +   ("quiet", "verbose"),
    6.49 +   ("satisfy", "falsify")];
    6.50 +
    6.51 +fun is_known_raw_param s =
    6.52 +  AList.defined (op =) default_default_params s orelse
    6.53 +  AList.defined (op =) negated_params s orelse
    6.54 +  member (op =) ["atoms", "card", "eval", "expect"] s orelse
    6.55 +  exists (fn p => String.isPrefix (p ^ " ") s)
    6.56 +    ["atoms", "card", "dont_whack", "mono", "non_mono", "non_wf", "wf", "whack"];
    6.57 +
    6.58 +fun check_raw_param (s, _) =
    6.59 +  if is_known_raw_param s then () else error ("Unknown parameter: " ^ quote s);
    6.60 +
    6.61 +fun unnegate_param_name name =
    6.62 +  (case AList.lookup (op =) negated_params name of
    6.63 +    NONE =>
    6.64 +    if String.isPrefix "dont_" name then SOME (unprefix "dont_" name)
    6.65 +    else if String.isPrefix "non_" name then SOME (unprefix "non_" name)
    6.66 +    else NONE
    6.67 +  | some_name => some_name);
    6.68 +
    6.69 +fun normalize_raw_param (name, value) =
    6.70 +  (case unnegate_param_name name of
    6.71 +    SOME name' =>
    6.72 +    [(name',
    6.73 +      (case value of
    6.74 +        ["false"] => ["true"]
    6.75 +      | ["true"] => ["false"]
    6.76 +      | [] => ["false"]
    6.77 +      | _ => value))]
    6.78 +  | NONE => [(name, value)]);
    6.79 +
    6.80 +structure Data = Theory_Data
    6.81 +(
    6.82 +  type T = raw_param list
    6.83 +  val empty = default_default_params |> map (apsnd single)
    6.84 +  val extend = I
    6.85 +  fun merge data = AList.merge (op =) (K true) data
    6.86 +);
    6.87 +
    6.88 +val set_default_raw_param = Data.map o fold (AList.update (op =)) o normalize_raw_param;
    6.89 +val default_raw_params = Data.get;
    6.90 +
    6.91 +fun is_punctuation s = (s = "," orelse s = "-");
    6.92 +
    6.93 +fun stringify_raw_param_value [] = ""
    6.94 +  | stringify_raw_param_value [s] = s
    6.95 +  | stringify_raw_param_value (s1 :: s2 :: ss) =
    6.96 +    s1 ^ (if is_punctuation s1 orelse is_punctuation s2 then "" else " ") ^
    6.97 +    stringify_raw_param_value (s2 :: ss);
    6.98 +
    6.99 +fun extract_params ctxt mode default_params override_params =
   6.100 +  let
   6.101 +    val override_params = maps normalize_raw_param override_params;
   6.102 +    val raw_params = rev override_params @ rev default_params;
   6.103 +    val raw_lookup = AList.lookup (op =) raw_params;
   6.104 +    val lookup = Option.map stringify_raw_param_value o raw_lookup;
   6.105 +    val lookup_string = the_default "" o lookup;
   6.106 +
   6.107 +    fun general_lookup_bool option default_value name =
   6.108 +      (case lookup name of
   6.109 +        SOME s => parse_bool_option option name s
   6.110 +      | NONE => default_value);
   6.111 +
   6.112 +    val lookup_bool = the o general_lookup_bool false (SOME false);
   6.113 +
   6.114 +    fun lookup_int name =
   6.115 +      (case lookup name of
   6.116 +        SOME s =>
   6.117 +        (case Int.fromString s of
   6.118 +          SOME i => i
   6.119 +        | NONE => error ("Parameter " ^ quote name ^ " must be assigned an integer value"))
   6.120 +      | NONE => 0);
   6.121 +
   6.122 +    fun int_range_from_string name s =
   6.123 +      (case space_explode "-" s of
   6.124 +         [s] => (s, s)
   6.125 +       | [s1, s2] => (s1, s2)
   6.126 +       | _ => error ("Parameter " ^ quote name ^ " must be assigned a range of integers"))
   6.127 +      |> apply2 Int.fromString;
   6.128 +
   6.129 +    fun lookup_assigns read pre of_str =
   6.130 +      (case lookup pre of
   6.131 +        SOME s => [(NONE, of_str s)]
   6.132 +      | NONE => []) @
   6.133 +      map (fn (name, value) => (SOME (read (String.extract (name, size pre + 1, NONE))),
   6.134 +          of_str (stringify_raw_param_value value)))
   6.135 +        (filter (String.isPrefix (pre ^ " ") o fst) raw_params);
   6.136 +
   6.137 +    fun lookup_int_range_assigns read pre =
   6.138 +      lookup_assigns read pre (int_range_from_string pre);
   6.139 +
   6.140 +    fun lookup_bool_assigns read pre =
   6.141 +      lookup_assigns read pre (the o parse_bool_option false pre);
   6.142 +
   6.143 +    fun lookup_bool_option_assigns read pre =
   6.144 +      lookup_assigns read pre (parse_bool_option true pre);
   6.145 +
   6.146 +    fun lookup_strings_assigns read pre =
   6.147 +      lookup_assigns read pre (space_explode " ");
   6.148 +
   6.149 +    fun lookup_time name =
   6.150 +      (case lookup name of
   6.151 +        SOME s => parse_time name s
   6.152 +      | NONE => Time.zeroTime);
   6.153 +
   6.154 +    val read_type_polymorphic =
   6.155 +      Syntax.read_typ ctxt #> Logic.mk_type
   6.156 +      #> singleton (Variable.polymorphic ctxt) #> Logic.dest_type;
   6.157 +    val read_term_polymorphic =
   6.158 +      Syntax.read_term ctxt #> singleton (Variable.polymorphic ctxt);
   6.159 +    val lookup_term_list_option_polymorphic =
   6.160 +      AList.lookup (op =) raw_params #> Option.map (map read_term_polymorphic);
   6.161 +
   6.162 +    fun read_const_polymorphic s =
   6.163 +      (case read_term_polymorphic s of
   6.164 +        Const x => x
   6.165 +      | t => error ("Not a constant: " ^ Syntax.string_of_term ctxt t));
   6.166 +
   6.167 +    val wfs = lookup_bool_option_assigns read_const_polymorphic "wf";
   6.168 +    val whacks = lookup_bool_assigns read_term_polymorphic "whack";
   6.169 +    val cards = lookup_int_range_assigns read_type_polymorphic "card";
   6.170 +    val monos = lookup_bool_option_assigns read_type_polymorphic "mono";
   6.171 +    val falsify = lookup_bool "falsify";
   6.172 +    val debug = (mode <> Auto_Try andalso lookup_bool "debug");
   6.173 +    val verbose = debug orelse (mode <> Auto_Try andalso lookup_bool "verbose");
   6.174 +    val overlord = lookup_bool "overlord";
   6.175 +    val spy = getenv "NUNCHAKU_SPY" = "yes" orelse lookup_bool "spy";
   6.176 +    val assms = lookup_bool "assms";
   6.177 +    val specialize = lookup_bool "specialize";
   6.178 +    val timeout = lookup_time "timeout";
   6.179 +    val wf_timeout = lookup_time "wf_timeout";
   6.180 +    val multithread = mode = Normal andalso lookup_bool "multithread";
   6.181 +    val evals = these (lookup_term_list_option_polymorphic "eval");
   6.182 +    val atomss = lookup_strings_assigns read_type_polymorphic "atoms";
   6.183 +    val max_potential = if mode = Normal then Int.max (0, lookup_int "max_potential") else 0;
   6.184 +    val max_genuine = Int.max (0, lookup_int "max_genuine");
   6.185 +    val expect = lookup_string "expect";
   6.186 +
   6.187 +    val mode_of_operation_params =
   6.188 +      {falsify = falsify, assms = assms, spy = spy, overlord = overlord,
   6.189 +       expect = expect};
   6.190 +
   6.191 +    val scope_of_search_params =
   6.192 +      {wfs = wfs, whacks = whacks, cards = cards, monos = monos};
   6.193 +
   6.194 +    val output_format_params =
   6.195 +      {verbose = verbose, debug = debug, max_potential = max_potential, max_genuine = max_genuine,
   6.196 +       evals = evals, atomss = atomss};
   6.197 +
   6.198 +    val optimization_params =
   6.199 +      {specialize = specialize, multithread = multithread};
   6.200 +
   6.201 +    val timeout_params =
   6.202 +      {timeout = timeout, wf_timeout = wf_timeout};
   6.203 +  in
   6.204 +    {mode_of_operation_params = mode_of_operation_params,
   6.205 +     scope_of_search_params = scope_of_search_params,
   6.206 +     output_format_params = output_format_params,
   6.207 +     optimization_params = optimization_params,
   6.208 +     timeout_params = timeout_params}
   6.209 +  end;
   6.210 +
   6.211 +fun default_params thy =
   6.212 +  extract_params (Proof_Context.init_global thy) Normal (default_raw_params thy)
   6.213 +  o map (apsnd single);
   6.214 +
   6.215 +val parse_key = Scan.repeat1 Parse.embedded >> space_implode " ";
   6.216 +val parse_value =
   6.217 +  Scan.repeat1 (Parse.minus >> single
   6.218 +    || Scan.repeat1 (Scan.unless Parse.minus (Parse.name || Parse.float_number))
   6.219 +    || @{keyword ","} |-- Parse.number >> prefix "," >> single)
   6.220 +  >> flat;
   6.221 +val parse_param = parse_key -- Scan.optional (@{keyword "="} |-- parse_value) [];
   6.222 +val parse_params = Scan.optional (@{keyword "["} |-- Parse.list parse_param --| @{keyword "]"}) [];
   6.223 +
   6.224 +fun run_chaku override_params mode i state0 =
   6.225 +  let
   6.226 +    val state = Proof.map_contexts (Try0.silence_methods false) state0;
   6.227 +    val thy = Proof.theory_of state;
   6.228 +    val ctxt = Proof.context_of state;
   6.229 +    val _ = List.app check_raw_param override_params;
   6.230 +    val params = extract_params ctxt mode (default_raw_params thy) override_params;
   6.231 +  in
   6.232 +    (if mode = Auto_Try then perhaps o try else fn f => fn x => f x)
   6.233 +      (fn _ => run_chaku_on_subgoal state params mode i) (unknownN, NONE)
   6.234 +    |> `(fn (outcome_code, _) => outcome_code = genuineN)
   6.235 +  end;
   6.236 +
   6.237 +fun string_for_raw_param (name, value) =
   6.238 +  name ^ " = " ^ stringify_raw_param_value value;
   6.239 +
   6.240 +fun nunchaku_params_trans params =
   6.241 +  Toplevel.theory (fold set_default_raw_param params
   6.242 +    #> tap (fn thy =>
   6.243 +      let val params = rev (default_raw_params thy) in
   6.244 +        List.app check_raw_param params;
   6.245 +        writeln ("Default parameters for Nunchaku:\n" ^
   6.246 +          (params |> map string_for_raw_param |> sort_strings |> cat_lines))
   6.247 +      end));
   6.248 +
   6.249 +val _ =
   6.250 +  Outer_Syntax.command @{command_keyword nunchaku}
   6.251 +    "try to find a countermodel using Nunchaku"
   6.252 +    (parse_params -- Scan.optional Parse.nat 1 >> (fn (params, i) =>
   6.253 +       Toplevel.keep_proof (fn state =>
   6.254 +         ignore (run_chaku params Normal i (Toplevel.proof_of state)))));
   6.255 +
   6.256 +val _ =
   6.257 +  Outer_Syntax.command @{command_keyword nunchaku_params}
   6.258 +    "set and display the default parameters for Nunchaku"
   6.259 +    (parse_params #>> nunchaku_params_trans);
   6.260 +
   6.261 +end;
     7.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.2 +++ b/src/HOL/Nunchaku/Tools/nunchaku_display.ML	Mon Oct 24 22:42:07 2016 +0200
     7.3 @@ -0,0 +1,91 @@
     7.4 +(*  Title:      HOL/Nunchaku/Tools/nunchaku_display.ML
     7.5 +    Author:     Jasmin Blanchette, Inria Nancy, LORIA, MPII
     7.6 +    Copyright   2015, 2016
     7.7 +
     7.8 +Pretty printing of Isabelle/HOL models for Nunchaku.
     7.9 +*)
    7.10 +
    7.11 +signature NUNCHAKU_DISPLAY =
    7.12 +sig
    7.13 +  type isa_model = Nunchaku_Reconstruct.isa_model
    7.14 +
    7.15 +  val pretty_of_isa_model_opt: Proof.context -> isa_model option -> Pretty.T
    7.16 +end;
    7.17 +
    7.18 +structure Nunchaku_Display : NUNCHAKU_DISPLAY =
    7.19 +struct
    7.20 +
    7.21 +open Nunchaku_Util;
    7.22 +open Nunchaku_Reconstruct;
    7.23 +
    7.24 +val indent_size = 2;
    7.25 +
    7.26 +val pretty_indent = Pretty.indent indent_size;
    7.27 +
    7.28 +fun sorting_str_of_typ (TFree (s, _)) = "a" ^ s
    7.29 +  | sorting_str_of_typ (Type (s, Ts)) = "b" ^ s ^ space_implode " " (map sorting_str_of_typ Ts)
    7.30 +  | sorting_str_of_typ (TVar _) = "X";
    7.31 +
    7.32 +fun sorting_str_of_term (Const (s, T)) = "b" ^ s ^ sorting_str_of_typ T
    7.33 +  | sorting_str_of_term (Free (s, _)) = "a" ^ s
    7.34 +  | sorting_str_of_term (t $ u) = sorting_str_of_term t ^ " " ^ sorting_str_of_term u
    7.35 +  | sorting_str_of_term (Abs (_, T, t)) = "c" ^ sorting_str_of_typ T ^ " " ^ sorting_str_of_term t
    7.36 +  | sorting_str_of_term _ = "X";
    7.37 +
    7.38 +fun pretty_of_isa_model_opt _ NONE =
    7.39 +    pretty_indent (Pretty.str "Model unavailable (internal error)")
    7.40 +  | pretty_of_isa_model_opt ctxt0
    7.41 +      (SOME {type_model, free_model, pat_complete_model, pat_incomplete_model, skolem_model}) =
    7.42 +    let
    7.43 +      val ctxt = ctxt0 |> Config.put show_question_marks false;
    7.44 +
    7.45 +      val pat_incomplete_model' = pat_incomplete_model
    7.46 +        |> filter_out (can (fn Const (@{const_name unreachable}, _) => ()) o fst);
    7.47 +
    7.48 +      fun pretty_of_typ_entry (T, atoms) =
    7.49 +        Pretty.block (Pretty.breaks [Syntax.pretty_typ ctxt T, Pretty.str "=",
    7.50 +           Pretty.enum "," "{" "}" (map (Syntax.pretty_term ctxt) atoms)]);
    7.51 +
    7.52 +      fun pretty_of_term_entry (t, value) =
    7.53 +        let
    7.54 +          val no_types_ctxt = ctxt |> Config.put show_types false;
    7.55 +          val schematic_ctxt = ctxt |> Proof_Context.set_mode Proof_Context.mode_schematic;
    7.56 +
    7.57 +          val show_types = Config.get ctxt show_types;
    7.58 +          val value' = value |> perhaps (try (Syntax.check_term schematic_ctxt));
    7.59 +          val T = fastype_of t;
    7.60 +          val T' = if T = dummyT then try fastype_of value' |> the_default T else T;
    7.61 +          val t' = t |> show_types ? Type.constraint T';
    7.62 +        in
    7.63 +          Pretty.block (Pretty.breaks
    7.64 +            [Syntax.pretty_term ctxt t'
    7.65 +             |> (show_types andalso T' <> dummyT) ? (single #> Pretty.enclose "(" ")"),
    7.66 +             Pretty.str "=", Syntax.pretty_term no_types_ctxt value'])
    7.67 +        end;
    7.68 +
    7.69 +      fun chunks_of_entries sorting_str_of pretty_of title entries =
    7.70 +        if not (null entries) then
    7.71 +          (if title = "" then [] else [Pretty.str (title ^ plural_s_for_list entries ^ ":")]) @
    7.72 +          map (pretty_indent o pretty_of) (sort_by (sorting_str_of o fst) entries)
    7.73 +        else
    7.74 +          [];
    7.75 +
    7.76 +      val chunks =
    7.77 +        (if null free_model then
    7.78 +           [pretty_indent (Pretty.str "No free variables")]
    7.79 +         else
    7.80 +           chunks_of_entries sorting_str_of_term pretty_of_term_entry "" free_model) @
    7.81 +        chunks_of_entries sorting_str_of_term pretty_of_term_entry "Skolem constant" skolem_model @
    7.82 +        chunks_of_entries sorting_str_of_term pretty_of_term_entry "Underspecified constant"
    7.83 +          pat_incomplete_model' @
    7.84 +        (if Config.get ctxt show_consts then
    7.85 +           chunks_of_entries sorting_str_of_term pretty_of_term_entry "Fully specified constant"
    7.86 +             pat_complete_model
    7.87 +         else
    7.88 +           []) @
    7.89 +        chunks_of_entries sorting_str_of_typ pretty_of_typ_entry "Type" type_model;
    7.90 +    in
    7.91 +      Pretty.chunks chunks
    7.92 +    end;
    7.93 +
    7.94 +end;
     8.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.2 +++ b/src/HOL/Nunchaku/Tools/nunchaku_model.ML	Mon Oct 24 22:42:07 2016 +0200
     8.3 @@ -0,0 +1,284 @@
     8.4 +(*  Title:      HOL/Nunchaku/Tools/nunchaku_model.ML
     8.5 +    Author:     Jasmin Blanchette, Inria Nancy, LORIA, MPII
     8.6 +    Copyright   2015, 2016
     8.7 +
     8.8 +Abstract syntax tree for Nunchaku models.
     8.9 +*)
    8.10 +
    8.11 +signature NUNCHAKU_MODEL =
    8.12 +sig
    8.13 +  type ident = Nunchaku_Problem.ident
    8.14 +  type ty = Nunchaku_Problem.ty
    8.15 +  type tm = Nunchaku_Problem.tm
    8.16 +  type name_pool = Nunchaku_Problem.name_pool
    8.17 +
    8.18 +  type ty_entry = ty * tm list
    8.19 +  type tm_entry = tm * tm
    8.20 +
    8.21 +  type nun_model =
    8.22 +    {type_model: ty_entry list,
    8.23 +     const_model: tm_entry list,
    8.24 +     skolem_model: tm_entry list}
    8.25 +
    8.26 +  val str_of_nun_model: nun_model -> string
    8.27 +
    8.28 +  val allocate_ugly: name_pool -> string * string -> string * name_pool
    8.29 +
    8.30 +  val ugly_nun_model: name_pool -> nun_model -> nun_model
    8.31 +
    8.32 +  datatype token =
    8.33 +    Ident of ident
    8.34 +  | Symbol of ident
    8.35 +  | Atom of ident * int
    8.36 +  | End_of_Stream
    8.37 +
    8.38 +  val parse_tok: ''a -> ''a list -> ''a * ''a list
    8.39 +  val parse_ident: token list -> ident * token list
    8.40 +  val parse_id: ident -> token list -> token * token list
    8.41 +  val parse_sym: ident -> token list -> token * token list
    8.42 +  val parse_atom: token list -> (ident * int) * token list
    8.43 +  val nun_model_of_str: string -> nun_model
    8.44 +end;
    8.45 +
    8.46 +structure Nunchaku_Model : NUNCHAKU_MODEL =
    8.47 +struct
    8.48 +
    8.49 +open Nunchaku_Problem;
    8.50 +
    8.51 +type ty_entry = ty * tm list;
    8.52 +type tm_entry = tm * tm;
    8.53 +
    8.54 +type nun_model =
    8.55 +  {type_model: ty_entry list,
    8.56 +   const_model: tm_entry list,
    8.57 +   skolem_model: tm_entry list};
    8.58 +
    8.59 +val nun_SAT = str_of_ident "SAT";
    8.60 +
    8.61 +fun str_of_ty_entry (ty, tms) =
    8.62 +  "type " ^ str_of_ty ty ^ " := {" ^ commas (map str_of_tm tms) ^ "}.";
    8.63 +
    8.64 +fun str_of_tm_entry (tm, value) =
    8.65 +  "val " ^ str_of_tm tm ^ " := " ^ str_of_tm value ^ ".";
    8.66 +
    8.67 +fun str_of_nun_model {type_model, const_model, skolem_model} =
    8.68 +  map str_of_ty_entry type_model @ "" :: map str_of_tm_entry const_model @ "" ::
    8.69 +  map str_of_tm_entry skolem_model
    8.70 +  |> cat_lines;
    8.71 +
    8.72 +fun fold_map_ty_entry_idents f (ty, atoms) =
    8.73 +  fold_map_ty_idents f ty
    8.74 +  ##>> fold_map (fold_map_tm_idents f) atoms;
    8.75 +
    8.76 +fun fold_map_tm_entry_idents f (tm, value) =
    8.77 +  fold_map_tm_idents f tm
    8.78 +  ##>> fold_map_tm_idents f value;
    8.79 +
    8.80 +fun fold_map_nun_model_idents f {type_model, const_model, skolem_model} =
    8.81 +  fold_map (fold_map_ty_entry_idents f) type_model
    8.82 +  ##>> fold_map (fold_map_tm_entry_idents f) const_model
    8.83 +  ##>> fold_map (fold_map_tm_entry_idents f) skolem_model
    8.84 +  #>> (fn ((type_model, const_model), skolem_model) =>
    8.85 +    {type_model = type_model, const_model = const_model, skolem_model = skolem_model});
    8.86 +
    8.87 +fun swap_name_pool ({nice_of_ugly, ugly_of_nice} : name_pool) =
    8.88 +  {nice_of_ugly = ugly_of_nice, ugly_of_nice = nice_of_ugly};
    8.89 +
    8.90 +fun allocate_ugly pool (nice, ugly_sugg) =
    8.91 +  allocate_nice (swap_name_pool pool) (nice, ugly_sugg) ||> swap_name_pool;
    8.92 +
    8.93 +fun ugly_ident nice (pool as {ugly_of_nice, ...}) =
    8.94 +  (case Symtab.lookup ugly_of_nice nice of
    8.95 +    NONE => allocate_ugly pool (nice, nice)
    8.96 +  | SOME ugly => (ugly, pool));
    8.97 +
    8.98 +fun ugly_nun_model pool model =
    8.99 +  fst (fold_map_nun_model_idents ugly_ident model pool);
   8.100 +
   8.101 +datatype token =
   8.102 +  Ident of ident
   8.103 +| Symbol of ident
   8.104 +| Atom of ident * int
   8.105 +| End_of_Stream;
   8.106 +
   8.107 +val rev_str = String.implode o rev o String.explode;
   8.108 +
   8.109 +fun atom_of_str s =
   8.110 +  (case first_field "_" (rev_str s) of
   8.111 +    SOME (rev_suf, rev_pre) =>
   8.112 +    let
   8.113 +      val pre = rev_str rev_pre;
   8.114 +      val suf = rev_str rev_suf;
   8.115 +    in
   8.116 +      (case Int.fromString suf of
   8.117 +        SOME j => Atom (ident_of_str pre, j)
   8.118 +      | NONE => raise Fail "ill-formed atom")
   8.119 +    end
   8.120 +  | NONE => raise Fail "ill-formed atom");
   8.121 +
   8.122 +fun is_alnum_etc_char c = Char.isAlphaNum c orelse c = #"_" orelse c = #"/";
   8.123 +
   8.124 +val multi_ids =
   8.125 +  [nun_arrow, nun_assign, nun_conj, nun_disj, nun_implies, nun_unparsable, nun_irrelevant];
   8.126 +
   8.127 +val nun_anon_fun_prefix_exploded = String.explode nun_anon_fun_prefix;
   8.128 +val [nun_dollar_char] = String.explode nun_dollar;
   8.129 +
   8.130 +fun next_token [] = (End_of_Stream, [])
   8.131 +  | next_token (c :: cs) =
   8.132 +    if Char.isSpace c then
   8.133 +      next_token cs
   8.134 +    else if c = nun_dollar_char then
   8.135 +      let val n = find_index (not o is_alnum_etc_char) cs in
   8.136 +        (if n = ~1 then (cs, []) else chop n cs)
   8.137 +        |>> (String.implode
   8.138 +          #> (if is_prefix (op =) nun_anon_fun_prefix_exploded cs then ident_of_str #> Ident
   8.139 +            else atom_of_str))
   8.140 +      end
   8.141 +    else if is_alnum_etc_char c then
   8.142 +      let val n = find_index (not o is_alnum_etc_char) cs in
   8.143 +        (if n = ~1 then (cs, []) else chop n cs)
   8.144 +        |>> (cons c #> String.implode #> ident_of_str #> Ident)
   8.145 +      end
   8.146 +    else
   8.147 +      let
   8.148 +        fun next_multi id =
   8.149 +          let
   8.150 +            val s = str_of_ident id;
   8.151 +            val n = String.size s - 1;
   8.152 +          in
   8.153 +            if c = String.sub (s, 0) andalso
   8.154 +               is_prefix (op =) (String.explode (String.substring (s, 1, n))) cs then
   8.155 +              SOME (Symbol id, drop n cs)
   8.156 +            else
   8.157 +              NONE
   8.158 +          end;
   8.159 +      in
   8.160 +        (case get_first next_multi multi_ids of
   8.161 +          SOME res => res
   8.162 +        | NONE => (Symbol (ident_of_str (String.str c)), cs))
   8.163 +      end;
   8.164 +
   8.165 +val tokenize =
   8.166 +  let
   8.167 +    fun toks cs =
   8.168 +      (case next_token cs of
   8.169 +        (End_of_Stream, []) => []
   8.170 +      | (tok, cs') => tok :: toks cs');
   8.171 +  in
   8.172 +    toks o String.explode
   8.173 +  end;
   8.174 +
   8.175 +fun parse_enum sep scan = scan ::: Scan.repeat (sep |-- scan);
   8.176 +
   8.177 +fun parse_tok tok = Scan.one (curry (op =) tok);
   8.178 +
   8.179 +val parse_ident = Scan.some (try (fn Ident id => id));
   8.180 +val parse_id = parse_tok o Ident;
   8.181 +val parse_sym = parse_tok o Symbol;
   8.182 +val parse_atom = Scan.some (try (fn Atom id_j => id_j));
   8.183 +
   8.184 +val confusing_ids = [nun_else, nun_then, nun_with];
   8.185 +
   8.186 +val parse_confusing_id = Scan.one (fn Ident id => member (op =) confusing_ids id | _ => false);
   8.187 +
   8.188 +fun parse_ty toks =
   8.189 +  (parse_ty_arg -- Scan.option (parse_sym nun_arrow -- parse_ty)
   8.190 +   >> (fn (ty, NONE) => ty
   8.191 +     | (lhs, SOME (Symbol id, rhs)) => NType (id, [lhs, rhs]))) toks
   8.192 +and parse_ty_arg toks =
   8.193 +  (parse_ident >> (rpair [] #> NType)
   8.194 +   || parse_sym nun_lparen |-- parse_ty --| parse_sym nun_rparen) toks;
   8.195 +
   8.196 +val parse_choice_or_unique =
   8.197 +  (parse_tok (Ident nun_choice) || parse_tok (Ident nun_unique)
   8.198 +   || parse_tok (Ident nun_unique_unsafe))
   8.199 +  -- parse_ty_arg
   8.200 +  >> (fn (Ident id, ty) => NConst (id, [ty], mk_arrows_ty ([ty, prop_ty], ty)));
   8.201 +
   8.202 +fun parse_tm toks =
   8.203 +  (parse_id nun_lambda |-- Scan.repeat parse_arg --| parse_sym nun_dot -- parse_tm >> nabss
   8.204 +  || parse_id nun_mu |-- parse_arg --| parse_sym nun_dot -- parse_tm
   8.205 +     >> (fn (var, body) =>
   8.206 +       let val ty = safe_ty_of body in
   8.207 +         NApp (NConst (nun_mu, [ty], mk_arrow_ty (mk_arrow_ty (ty, ty), ty)), NAbs (var, body))
   8.208 +       end)
   8.209 +   || parse_id nun_if |-- parse_tm --| parse_id nun_then -- parse_tm --| parse_id nun_else
   8.210 +       -- parse_tm
   8.211 +     >> (fn ((cond, th), el) =>
   8.212 +       let val ty = safe_ty_of th in
   8.213 +         napps (NConst (nun_if, [ty], mk_arrows_ty ([prop_ty, ty, ty], ty)), [cond, th, el])
   8.214 +       end)
   8.215 +   || parse_implies) toks
   8.216 +and parse_implies toks =
   8.217 +  (parse_disj -- Scan.option (parse_sym nun_implies -- parse_implies)
   8.218 +   >> (fn (tm, NONE) => tm
   8.219 +     | (lhs, SOME (Symbol id, rhs)) => napps (NConst (id, [], dummy_ty), [lhs, rhs]))) toks
   8.220 +and parse_disj toks =
   8.221 +  (parse_conj -- Scan.option (parse_sym nun_disj -- parse_disj)
   8.222 +   >> (fn (tm, NONE) => tm
   8.223 +     | (lhs, SOME (Symbol id, rhs)) => napps (NConst (id, [], dummy_ty), [lhs, rhs]))) toks
   8.224 +and parse_conj toks =
   8.225 +  (parse_equals -- Scan.option (parse_sym nun_conj -- parse_conj)
   8.226 +   >> (fn (tm, NONE) => tm
   8.227 +     | (lhs, SOME (Symbol id, rhs)) => napps (NConst (id, [], dummy_ty), [lhs, rhs]))) toks
   8.228 +and parse_equals toks =
   8.229 +  (parse_comb -- Scan.option (parse_sym nun_equals -- parse_comb)
   8.230 +   >> (fn (tm, NONE) => tm
   8.231 +     | (lhs, SOME (Symbol id, rhs)) => napps (NConst (id, [], dummy_ty), [lhs, rhs]))) toks
   8.232 +and parse_comb toks =
   8.233 +  (parse_arg -- Scan.repeat (Scan.unless parse_confusing_id parse_arg) >> napps) toks
   8.234 +and parse_arg toks =
   8.235 +  (parse_choice_or_unique
   8.236 +   || parse_ident >> (fn id => NConst (id, [], dummy_ty))
   8.237 +   || parse_sym nun_irrelevant
   8.238 +      |-- Scan.option (parse_sym nun_lparen |-- parse_tm --| parse_sym nun_rparen) (* FIXME *)
   8.239 +     >> (fn _ => NConst (nun_irrelevant, [], dummy_ty))
   8.240 +   || parse_sym nun_unparsable |-- parse_ty >> (fn ty => NConst (nun_unparsable, [], ty))
   8.241 +   || parse_sym nun_lparen |-- parse_tm -- Scan.option (parse_sym nun_colon |-- parse_ty)
   8.242 +      --| parse_sym nun_rparen
   8.243 +     >> (fn (NConst (id, [], _), SOME ty) => NConst (id, [], ty)
   8.244 +       | (tm, _) => tm)
   8.245 +   || parse_atom >> (fn (id, j) => NAtom (j, NType (id, [])))) toks;
   8.246 +
   8.247 +val parse_witness_name =
   8.248 +  parse_ident >> (fn id => NConst (hd (space_explode "/" id), [], dummy_ty));
   8.249 +
   8.250 +val parse_witness =
   8.251 +  parse_id nun__witness_of |-- parse_sym nun_lparen |-- (parse_id nun_forall || parse_id nun_exists)
   8.252 +  |-- Scan.option (parse_sym nun_lparen) |-- parse_witness_name
   8.253 +  --| Scan.repeat (Scan.one (curry (op <>) (Symbol nun_assign)));
   8.254 +
   8.255 +datatype entry =
   8.256 +  Type_Entry of ty_entry
   8.257 +| Skolem_Entry of tm_entry
   8.258 +| Const_Entry of tm_entry;
   8.259 +
   8.260 +val parse_entry =
   8.261 +  (parse_id nun_type |-- parse_ty --| parse_sym nun_assign --| parse_sym nun_lbrace --
   8.262 +       parse_enum (parse_sym nun_comma) parse_tm --| parse_sym nun_rbrace
   8.263 +     >> Type_Entry
   8.264 +   || parse_id nun_val |-- parse_witness --| parse_sym nun_assign -- parse_tm >> Skolem_Entry
   8.265 +   || parse_id nun_val |-- parse_tm --| parse_sym nun_assign -- parse_tm >> Const_Entry)
   8.266 +  --| parse_sym nun_dot;
   8.267 +
   8.268 +val parse_model =
   8.269 +  parse_id nun_SAT |-- parse_sym nun_colon |-- parse_sym nun_lbrace |-- Scan.repeat parse_entry
   8.270 +  --| parse_sym nun_rbrace;
   8.271 +
   8.272 +fun add_entry entry ({type_model, const_model, skolem_model} : nun_model) =
   8.273 +  (case entry of
   8.274 +    Type_Entry e =>
   8.275 +    {type_model = e :: type_model, const_model = const_model, skolem_model = skolem_model}
   8.276 +  | Skolem_Entry e =>
   8.277 +    {type_model = type_model, const_model = const_model, skolem_model = e :: skolem_model}
   8.278 +  | Const_Entry e =>
   8.279 +    {type_model = type_model, const_model = e :: const_model, skolem_model = skolem_model});
   8.280 +
   8.281 +fun nun_model_of_str str =
   8.282 +  let val (entries, _) = parse_model (tokenize str) in
   8.283 +    {type_model = [], const_model = [], skolem_model = []}
   8.284 +    |> fold_rev add_entry entries
   8.285 +  end;
   8.286 +
   8.287 +end;
     9.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     9.2 +++ b/src/HOL/Nunchaku/Tools/nunchaku_problem.ML	Mon Oct 24 22:42:07 2016 +0200
     9.3 @@ -0,0 +1,791 @@
     9.4 +(*  Title:      HOL/Nunchaku/Tools/nunchaku_problem.ML
     9.5 +    Author:     Jasmin Blanchette, Inria Nancy, LORIA, MPII
     9.6 +    Copyright   2015, 2016
     9.7 +
     9.8 +Abstract syntax tree for Nunchaku problems.
     9.9 +*)
    9.10 +
    9.11 +signature NUNCHAKU_PROBLEM =
    9.12 +sig
    9.13 +  eqtype ident
    9.14 +
    9.15 +  datatype ty =
    9.16 +    NType of ident * ty list
    9.17 +
    9.18 +  datatype tm =
    9.19 +    NAtom of int * ty
    9.20 +  | NConst of ident * ty list * ty
    9.21 +  | NAbs of tm * tm
    9.22 +  | NMatch of tm * (ident * tm list * tm) list
    9.23 +  | NApp of tm * tm
    9.24 +
    9.25 +  type nun_type_spec =
    9.26 +    {abs_ty: ty,
    9.27 +     rep_ty: ty,
    9.28 +     wrt: tm,
    9.29 +     abs: tm,
    9.30 +     rep: tm}
    9.31 +
    9.32 +  type nun_ctr_spec =
    9.33 +    {ctr: tm,
    9.34 +     arg_tys: ty list}
    9.35 +
    9.36 +  type nun_co_data_spec =
    9.37 +    {ty: ty,
    9.38 +     ctrs: nun_ctr_spec list}
    9.39 +
    9.40 +  type nun_const_spec =
    9.41 +    {const: tm,
    9.42 +     props: tm list}
    9.43 +
    9.44 +  type nun_consts_spec =
    9.45 +    {consts: tm list,
    9.46 +     props: tm list}
    9.47 +
    9.48 +  datatype nun_command =
    9.49 +    NTVal of ty * (int option * int option)
    9.50 +  | NCopy of nun_type_spec
    9.51 +  | NQuotient of nun_type_spec
    9.52 +  | NData of nun_co_data_spec list
    9.53 +  | NCodata of nun_co_data_spec list
    9.54 +  | NVal of tm * ty
    9.55 +  | NPred of bool * nun_const_spec list
    9.56 +  | NCopred of nun_const_spec list
    9.57 +  | NRec of nun_const_spec list
    9.58 +  | NSpec of nun_consts_spec
    9.59 +  | NAxiom of tm
    9.60 +  | NGoal of tm
    9.61 +  | NEval of tm
    9.62 +
    9.63 +  type nun_problem =
    9.64 +    {commandss: nun_command list list,
    9.65 +     sound: bool,
    9.66 +     complete: bool}
    9.67 +
    9.68 +  type name_pool =
    9.69 +    {nice_of_ugly: string Symtab.table,
    9.70 +     ugly_of_nice: string Symtab.table}
    9.71 +
    9.72 +  val nun_abstract: string
    9.73 +  val nun_and: string
    9.74 +  val nun_anon_fun_prefix: string
    9.75 +  val nun_arrow: string
    9.76 +  val nun_asserting: string
    9.77 +  val nun_assign: string
    9.78 +  val nun_at: string
    9.79 +  val nun_axiom: string
    9.80 +  val nun_bar: string
    9.81 +  val nun_choice: string
    9.82 +  val nun_codata: string
    9.83 +  val nun_colon: string
    9.84 +  val nun_comma: string
    9.85 +  val nun_concrete: string
    9.86 +  val nun_conj: string
    9.87 +  val nun_copred: string
    9.88 +  val nun_copy: string
    9.89 +  val nun_data: string
    9.90 +  val nun_disj: string
    9.91 +  val nun_dollar: string
    9.92 +  val nun_dot: string
    9.93 +  val nun_dummy: string
    9.94 +  val nun_else: string
    9.95 +  val nun_end: string
    9.96 +  val nun_equals: string
    9.97 +  val nun_eval: string
    9.98 +  val nun_exists: string
    9.99 +  val nun_false: string
   9.100 +  val nun_forall: string
   9.101 +  val nun_goal: string
   9.102 +  val nun_hash: string
   9.103 +  val nun_if: string
   9.104 +  val nun_implies: string
   9.105 +  val nun_irrelevant: string
   9.106 +  val nun_lambda: string
   9.107 +  val nun_lbrace: string
   9.108 +  val nun_lbracket: string
   9.109 +  val nun_lparen: string
   9.110 +  val nun_match: string
   9.111 +  val nun_mu: string
   9.112 +  val nun_not: string
   9.113 +  val nun_pred: string
   9.114 +  val nun_prop: string
   9.115 +  val nun_quotient: string
   9.116 +  val nun_rbrace: string
   9.117 +  val nun_rbracket: string
   9.118 +  val nun_rec: string
   9.119 +  val nun_rparen: string
   9.120 +  val nun_semicolon: string
   9.121 +  val nun_spec: string
   9.122 +  val nun_then: string
   9.123 +  val nun_true: string
   9.124 +  val nun_type: string
   9.125 +  val nun_unparsable: string
   9.126 +  val nun_unique: string
   9.127 +  val nun_unique_unsafe: string
   9.128 +  val nun_val: string
   9.129 +  val nun_wf: string
   9.130 +  val nun_with: string
   9.131 +  val nun_wrt: string
   9.132 +  val nun__witness_of: string
   9.133 +
   9.134 +  val ident_of_str: string -> ident
   9.135 +  val str_of_ident: ident -> string
   9.136 +  val encode_args: string list -> string
   9.137 +  val nun_const_of_str: string list -> string -> ident
   9.138 +  val nun_tconst_of_str: string list -> string -> ident
   9.139 +  val nun_free_of_str: string -> ident
   9.140 +  val nun_tfree_of_str: string -> ident
   9.141 +  val nun_var_of_str: string -> ident
   9.142 +  val str_of_nun_const: ident -> string list * string
   9.143 +  val str_of_nun_tconst: ident -> string list * string
   9.144 +  val str_of_nun_free: ident -> string
   9.145 +  val str_of_nun_tfree: ident -> string
   9.146 +  val str_of_nun_var: ident -> string
   9.147 +
   9.148 +  val dummy_ty: ty
   9.149 +  val prop_ty: ty
   9.150 +  val mk_arrow_ty: ty * ty -> ty
   9.151 +  val mk_arrows_ty: ty list * ty -> ty
   9.152 +  val nabss: tm list * tm -> tm
   9.153 +  val napps: tm * tm list -> tm
   9.154 +
   9.155 +  val ty_of: tm -> ty
   9.156 +  val safe_ty_of: tm -> ty
   9.157 +
   9.158 +  val fold_map_ty_idents: (string -> 'a -> string * 'a) -> ty -> 'a -> ty * 'a
   9.159 +  val fold_map_tm_idents: (string -> 'a -> string * 'a) -> tm -> 'a -> tm * 'a
   9.160 +  val fold_map_nun_command_idents: (string -> 'a -> string * 'a) -> nun_command -> 'a ->
   9.161 +    nun_command * 'a
   9.162 +  val fold_map_nun_problem_idents: (string -> 'a -> string * 'a) -> nun_problem -> 'a ->
   9.163 +    nun_problem * 'a
   9.164 +
   9.165 +  val allocate_nice: name_pool -> string * string -> string * name_pool
   9.166 +
   9.167 +  val rcomb_tms: tm list -> tm -> tm
   9.168 +  val abs_tms: tm list -> tm -> tm
   9.169 +  val beta_reduce_tm: tm -> tm
   9.170 +  val eta_expandN_tm: int -> tm -> tm
   9.171 +  val eta_expand_builtin_tm: tm -> tm
   9.172 +
   9.173 +  val str_of_ty: ty -> string
   9.174 +  val str_of_tm: tm -> string
   9.175 +  val str_of_tmty: tm -> string
   9.176 +
   9.177 +  val nice_nun_problem: nun_problem -> nun_problem * name_pool
   9.178 +  val str_of_nun_problem: nun_problem -> string
   9.179 +end;
   9.180 +
   9.181 +structure Nunchaku_Problem : NUNCHAKU_PROBLEM =
   9.182 +struct
   9.183 +
   9.184 +open Nunchaku_Util;
   9.185 +
   9.186 +type ident = string;
   9.187 +
   9.188 +datatype ty =
   9.189 +  NType of ident * ty list;
   9.190 +
   9.191 +datatype tm =
   9.192 +  NAtom of int * ty
   9.193 +| NConst of ident * ty list * ty
   9.194 +| NAbs of tm * tm
   9.195 +| NMatch of tm * (ident * tm list * tm) list
   9.196 +| NApp of tm * tm;
   9.197 +
   9.198 +type nun_type_spec =
   9.199 +  {abs_ty: ty,
   9.200 +   rep_ty: ty,
   9.201 +   wrt: tm,
   9.202 +   abs: tm,
   9.203 +   rep: tm};
   9.204 +
   9.205 +type nun_ctr_spec =
   9.206 +  {ctr: tm,
   9.207 +   arg_tys: ty list};
   9.208 +
   9.209 +type nun_co_data_spec =
   9.210 +  {ty: ty,
   9.211 +   ctrs: nun_ctr_spec list};
   9.212 +
   9.213 +type nun_const_spec =
   9.214 +  {const: tm,
   9.215 +   props: tm list};
   9.216 +
   9.217 +type nun_consts_spec =
   9.218 +  {consts: tm list,
   9.219 +   props: tm list};
   9.220 +
   9.221 +datatype nun_command =
   9.222 +  NTVal of ty * (int option * int option)
   9.223 +| NCopy of nun_type_spec
   9.224 +| NQuotient of nun_type_spec
   9.225 +| NData of nun_co_data_spec list
   9.226 +| NCodata of nun_co_data_spec list
   9.227 +| NVal of tm * ty
   9.228 +| NPred of bool * nun_const_spec list
   9.229 +| NCopred of nun_const_spec list
   9.230 +| NRec of nun_const_spec list
   9.231 +| NSpec of nun_consts_spec
   9.232 +| NAxiom of tm
   9.233 +| NGoal of tm
   9.234 +| NEval of tm;
   9.235 +
   9.236 +type nun_problem =
   9.237 +  {commandss: nun_command list list,
   9.238 +   sound: bool,
   9.239 +   complete: bool};
   9.240 +
   9.241 +type name_pool =
   9.242 +  {nice_of_ugly: string Symtab.table,
   9.243 +   ugly_of_nice: string Symtab.table};
   9.244 +
   9.245 +val nun_abstract = "abstract";
   9.246 +val nun_and = "and";
   9.247 +val nun_anon_fun_prefix = "anon_fun_";
   9.248 +val nun_arrow = "->";
   9.249 +val nun_asserting = "asserting";
   9.250 +val nun_assign = ":=";
   9.251 +val nun_at = "@";
   9.252 +val nun_axiom = "axiom";
   9.253 +val nun_bar = "|";
   9.254 +val nun_choice = "choice";
   9.255 +val nun_codata = "codata";
   9.256 +val nun_colon = ":";
   9.257 +val nun_comma = ",";
   9.258 +val nun_concrete = "concrete";
   9.259 +val nun_conj = "&&";
   9.260 +val nun_copred = "copred";
   9.261 +val nun_copy = "copy";
   9.262 +val nun_data = "data";
   9.263 +val nun_disj = "||";
   9.264 +val nun_dollar = "$";
   9.265 +val nun_dot = ".";
   9.266 +val nun_dummy = "_";
   9.267 +val nun_else = "else";
   9.268 +val nun_end = "end";
   9.269 +val nun_equals = "=";
   9.270 +val nun_eval = "eval";
   9.271 +val nun_exists = "exists";
   9.272 +val nun_false = "false";
   9.273 +val nun_forall = "forall";
   9.274 +val nun_goal = "goal";
   9.275 +val nun_hash = "#";
   9.276 +val nun_if = "if";
   9.277 +val nun_implies = "=>";
   9.278 +val nun_irrelevant = "?__";
   9.279 +val nun_lambda = "fun";
   9.280 +val nun_lbrace = "{";
   9.281 +val nun_lbracket = "[";
   9.282 +val nun_lparen = "(";
   9.283 +val nun_match = "match";
   9.284 +val nun_mu = "mu";
   9.285 +val nun_not = "~";
   9.286 +val nun_pred = "pred";
   9.287 +val nun_prop = "prop";
   9.288 +val nun_quotient = "quotient";
   9.289 +val nun_rbrace = "}";
   9.290 +val nun_rbracket = "]";
   9.291 +val nun_rec = "rec";
   9.292 +val nun_rparen = ")";
   9.293 +val nun_semicolon = ";";
   9.294 +val nun_spec = "spec";
   9.295 +val nun_then = "then";
   9.296 +val nun_true = "true";
   9.297 +val nun_type = "type";
   9.298 +val nun_unique = "unique";
   9.299 +val nun_unique_unsafe = "unique_unsafe";
   9.300 +val nun_unparsable = "?__unparsable";
   9.301 +val nun_val = "val";
   9.302 +val nun_wf = "wf";
   9.303 +val nun_with = "with";
   9.304 +val nun_wrt = "wrt";
   9.305 +val nun__witness_of = "_witness_of";
   9.306 +
   9.307 +val nun_parens = enclose nun_lparen nun_rparen;
   9.308 +
   9.309 +fun nun_parens_if_space s = s |> String.isSubstring " " s ? nun_parens;
   9.310 +
   9.311 +fun str_of_nun_arg_list str_of_arg =
   9.312 +  map (prefix " " o nun_parens_if_space o str_of_arg) #> space_implode "";
   9.313 +
   9.314 +fun str_of_nun_and_list str_of_elem =
   9.315 +  map str_of_elem #> space_implode ("\n" ^ nun_and ^ " ");
   9.316 +
   9.317 +val is_nun_const_quantifier = member (op =) [nun_forall, nun_exists];
   9.318 +val is_nun_const_connective = member (op =) [nun_conj, nun_disj, nun_implies];
   9.319 +
   9.320 +val nun_builtin_arity =
   9.321 +  [(nun_asserting, 2),
   9.322 +   (nun_conj, 2),
   9.323 +   (nun_disj, 2),
   9.324 +   (nun_equals, 2),
   9.325 +   (nun_exists, 1),
   9.326 +   (nun_false, 0),
   9.327 +   (nun_forall, 1),
   9.328 +   (nun_if, 3),
   9.329 +   (nun_implies, 2),
   9.330 +   (nun_not, 1),
   9.331 +   (nun_true, 0)];
   9.332 +
   9.333 +val arity_of_nun_builtin = AList.lookup (op =) nun_builtin_arity #> the_default 0;
   9.334 +
   9.335 +val nun_const_prefix = "c.";
   9.336 +val nun_free_prefix = "f.";
   9.337 +val nun_var_prefix = "v.";
   9.338 +val nun_tconst_prefix = "C.";
   9.339 +val nun_tfree_prefix = "F.";
   9.340 +val nun_custom_id_suffix = "_";
   9.341 +
   9.342 +val ident_of_str = I : string -> ident;
   9.343 +val str_of_ident = I : ident -> string;
   9.344 +
   9.345 +val encode_args = enclose "(" ")" o commas;
   9.346 +
   9.347 +fun decode_args s =
   9.348 +  let
   9.349 +    fun delta #"(" = 1
   9.350 +      | delta #")" = ~1
   9.351 +      | delta _ = 0;
   9.352 +
   9.353 +    fun dec 0 (#"(" :: #")" :: cs) _ = ([], String.implode cs)
   9.354 +      | dec 0 (#"(" :: cs) [] = dec 1 cs [[]]
   9.355 +      | dec 0 cs _ = ([], String.implode cs)
   9.356 +      | dec _ [] _ = raise Fail ("ill-formed arguments in " ^ quote s)
   9.357 +      | dec 1 (#")" :: cs) args = (rev (map (String.implode o rev) args), String.implode cs)
   9.358 +      | dec 1 (#"," :: cs) args = dec 1 cs ([] :: args)
   9.359 +      | dec n (c :: cs) (arg :: args) = dec (n + delta c) cs ((c :: arg) :: args);
   9.360 +  in
   9.361 +    dec 0 (String.explode s) []
   9.362 +  end;
   9.363 +
   9.364 +fun nun_const_of_str args =
   9.365 +  suffix nun_custom_id_suffix #> prefix nun_const_prefix #> prefix (encode_args args);
   9.366 +fun nun_tconst_of_str args =
   9.367 +  suffix nun_custom_id_suffix #> prefix nun_tconst_prefix #> prefix (encode_args args);
   9.368 +
   9.369 +val nun_free_of_str = suffix nun_custom_id_suffix #> prefix nun_free_prefix;
   9.370 +val nun_tfree_of_str = suffix nun_custom_id_suffix #> prefix nun_tfree_prefix;
   9.371 +val nun_var_of_str = suffix nun_custom_id_suffix #> prefix nun_var_prefix;
   9.372 +val str_of_nun_const = decode_args ##> unprefix nun_const_prefix ##> unsuffix nun_custom_id_suffix;
   9.373 +val str_of_nun_tconst = decode_args ##> unprefix nun_tconst_prefix ##> unsuffix nun_custom_id_suffix;
   9.374 +val str_of_nun_free = unprefix nun_free_prefix #> unsuffix nun_custom_id_suffix;
   9.375 +val str_of_nun_tfree = unprefix nun_tfree_prefix #> unsuffix nun_custom_id_suffix;
   9.376 +val str_of_nun_var = unprefix nun_var_prefix #> unsuffix nun_custom_id_suffix;
   9.377 +
   9.378 +fun index_name s 0 = s
   9.379 +  | index_name s j =
   9.380 +    let
   9.381 +      val n = size s;
   9.382 +      val m = n - 1;
   9.383 +    in
   9.384 +      String.substring (s, 0, m) ^ string_of_int j ^ String.substring (s, m, n - m)
   9.385 +    end;
   9.386 +
   9.387 +val dummy_ty = NType (nun_dummy, []);
   9.388 +val prop_ty = NType (nun_prop, []);
   9.389 +
   9.390 +fun mk_arrow_ty (dom, ran) = NType (nun_arrow, [dom, ran]);
   9.391 +val mk_arrows_ty = Library.foldr mk_arrow_ty;
   9.392 +
   9.393 +val nabss = Library.foldr NAbs;
   9.394 +val napps = Library.foldl NApp;
   9.395 +
   9.396 +fun domain_ty (NType (_, [ty, _])) = ty
   9.397 +  | domain_ty ty = ty;
   9.398 +
   9.399 +fun range_ty (NType (_, [_, ty])) = ty
   9.400 +  | range_ty ty = ty;
   9.401 +
   9.402 +fun domain_tys 0 _ = []
   9.403 +  | domain_tys n ty = domain_ty ty :: domain_tys (n - 1) (range_ty ty);
   9.404 +
   9.405 +fun ty_of (NAtom (_, ty)) = ty
   9.406 +  | ty_of (NConst (_, _, ty)) = ty
   9.407 +  | ty_of (NAbs (var, body)) = mk_arrow_ty (ty_of var, ty_of body)
   9.408 +  | ty_of (NMatch (_, (_, _, body1) :: _)) = ty_of body1
   9.409 +  | ty_of (NApp (const, _)) = range_ty (ty_of const);
   9.410 +
   9.411 +val safe_ty_of = try ty_of #> the_default dummy_ty;
   9.412 +
   9.413 +fun strip_nun_binders binder (app as NApp (NConst (id, _, _), NAbs (var, body))) =
   9.414 +    if id = binder then
   9.415 +      strip_nun_binders binder body
   9.416 +      |>> cons var
   9.417 +    else
   9.418 +      ([], app)
   9.419 +  | strip_nun_binders _ tm = ([], tm);
   9.420 +
   9.421 +fun fold_map_ty_idents f (NType (id, tys)) =
   9.422 +    f id
   9.423 +    ##>> fold_map (fold_map_ty_idents f) tys
   9.424 +    #>> NType;
   9.425 +
   9.426 +fun fold_map_match_branch_idents f (id, vars, body) =
   9.427 +    f id
   9.428 +    ##>> fold_map (fold_map_tm_idents f) vars
   9.429 +    ##>> fold_map_tm_idents f body
   9.430 +    #>> Scan.triple1
   9.431 +and fold_map_tm_idents f (NAtom (j, ty)) =
   9.432 +    fold_map_ty_idents f ty
   9.433 +    #>> curry NAtom j
   9.434 +  | fold_map_tm_idents f (NConst (id, tys, ty)) =
   9.435 +    f id
   9.436 +    ##>> fold_map (fold_map_ty_idents f) tys
   9.437 +    ##>> fold_map_ty_idents f ty
   9.438 +    #>> (Scan.triple1 #> NConst)
   9.439 +  | fold_map_tm_idents f (NAbs (var, body)) =
   9.440 +    fold_map_tm_idents f var
   9.441 +    ##>> fold_map_tm_idents f body
   9.442 +    #>> NAbs
   9.443 +  | fold_map_tm_idents f (NMatch (obj, branches)) =
   9.444 +    fold_map_tm_idents f obj
   9.445 +    ##>> fold_map (fold_map_match_branch_idents f) branches
   9.446 +    #>> NMatch
   9.447 +  | fold_map_tm_idents f (NApp (const, arg)) =
   9.448 +    fold_map_tm_idents f const
   9.449 +    ##>> fold_map_tm_idents f arg
   9.450 +    #>> NApp;
   9.451 +
   9.452 +fun fold_map_nun_type_spec_idents f {abs_ty, rep_ty, wrt, abs, rep} =
   9.453 +  fold_map_ty_idents f abs_ty
   9.454 +  ##>> fold_map_ty_idents f rep_ty
   9.455 +  ##>> fold_map_tm_idents f wrt
   9.456 +  ##>> fold_map_tm_idents f abs
   9.457 +  ##>> fold_map_tm_idents f rep
   9.458 +  #>> (fn ((((abs_ty, rep_ty), wrt), abs), rep) =>
   9.459 +    {abs_ty = abs_ty, rep_ty = rep_ty, wrt = wrt, abs = abs, rep = rep});
   9.460 +
   9.461 +fun fold_map_nun_ctr_spec_idents f {ctr, arg_tys} =
   9.462 +  fold_map_tm_idents f ctr
   9.463 +  ##>> fold_map (fold_map_ty_idents f) arg_tys
   9.464 +  #>> (fn (ctr, arg_tys) => {ctr = ctr, arg_tys = arg_tys});
   9.465 +
   9.466 +fun fold_map_nun_co_data_spec_idents f {ty, ctrs} =
   9.467 +  fold_map_ty_idents f ty
   9.468 +  ##>> fold_map (fold_map_nun_ctr_spec_idents f) ctrs
   9.469 +  #>> (fn (ty, ctrs) => {ty = ty, ctrs = ctrs});
   9.470 +
   9.471 +fun fold_map_nun_const_spec_idents f {const, props} =
   9.472 +  fold_map_tm_idents f const
   9.473 +  ##>> fold_map (fold_map_tm_idents f) props
   9.474 +  #>> (fn (const, props) => {const = const, props = props});
   9.475 +
   9.476 +fun fold_map_nun_consts_spec_idents f {consts, props} =
   9.477 +  fold_map (fold_map_tm_idents f) consts
   9.478 +  ##>> fold_map (fold_map_tm_idents f) props
   9.479 +  #>> (fn (consts, props) => {consts = consts, props = props});
   9.480 +
   9.481 +fun fold_map_nun_command_idents f (NTVal (ty, cards)) =
   9.482 +    fold_map_ty_idents f ty
   9.483 +    #>> (rpair cards #> NTVal)
   9.484 +  | fold_map_nun_command_idents f (NCopy spec) =
   9.485 +    fold_map_nun_type_spec_idents f spec
   9.486 +    #>> NCopy
   9.487 +  | fold_map_nun_command_idents f (NQuotient spec) =
   9.488 +    fold_map_nun_type_spec_idents f spec
   9.489 +    #>> NQuotient
   9.490 +  | fold_map_nun_command_idents f (NData specs) =
   9.491 +    fold_map (fold_map_nun_co_data_spec_idents f) specs
   9.492 +    #>> NData
   9.493 +  | fold_map_nun_command_idents f (NCodata specs) =
   9.494 +    fold_map (fold_map_nun_co_data_spec_idents f) specs
   9.495 +    #>> NCodata
   9.496 +  | fold_map_nun_command_idents f (NVal (tm, ty)) =
   9.497 +    fold_map_tm_idents f tm
   9.498 +    ##>> fold_map_ty_idents f ty
   9.499 +    #>> NVal
   9.500 +  | fold_map_nun_command_idents f (NPred (wf, specs)) =
   9.501 +    fold_map (fold_map_nun_const_spec_idents f) specs
   9.502 +    #>> curry NPred wf
   9.503 +  | fold_map_nun_command_idents f (NCopred specs) =
   9.504 +    fold_map (fold_map_nun_const_spec_idents f) specs
   9.505 +    #>> NCopred
   9.506 +  | fold_map_nun_command_idents f (NRec specs) =
   9.507 +    fold_map (fold_map_nun_const_spec_idents f) specs
   9.508 +    #>> NRec
   9.509 +  | fold_map_nun_command_idents f (NSpec spec) =
   9.510 +    fold_map_nun_consts_spec_idents f spec
   9.511 +    #>> NSpec
   9.512 +  | fold_map_nun_command_idents f (NAxiom tm) =
   9.513 +    fold_map_tm_idents f tm
   9.514 +    #>> NAxiom
   9.515 +  | fold_map_nun_command_idents f (NGoal tm) =
   9.516 +    fold_map_tm_idents f tm
   9.517 +    #>> NGoal
   9.518 +  | fold_map_nun_command_idents f (NEval tm) =
   9.519 +    fold_map_tm_idents f tm
   9.520 +    #>> NEval;
   9.521 +
   9.522 +fun fold_map_nun_problem_idents f ({commandss, sound, complete} : nun_problem) =
   9.523 +  fold_map (fold_map (fold_map_nun_command_idents f)) commandss
   9.524 +  #>> (fn commandss' => {commandss = commandss', sound = sound, complete = complete});
   9.525 +
   9.526 +fun dest_rassoc_args oper arg0 rest =
   9.527 +  (case rest of
   9.528 +    NApp (NApp (oper', arg1), rest') =>
   9.529 +    if oper' = oper then arg0 :: dest_rassoc_args oper arg1 rest' else [arg0, rest]
   9.530 +  | _ => [arg0, rest]);
   9.531 +
   9.532 +fun replace_tm from to =
   9.533 +  let
   9.534 +    (* This code assumes all enclosing binders bind distinct variables and bound variables are
   9.535 +       distinct from any other variables. *)
   9.536 +    fun repl_br (id, vars, body) = (id, map repl vars, repl body)
   9.537 +    and repl (NApp (const, arg)) = NApp (repl const, repl arg)
   9.538 +      | repl (NAbs (var, body)) = NAbs (var, repl body)
   9.539 +      | repl (NMatch (obj, branches)) = NMatch (repl obj, map repl_br branches)
   9.540 +      | repl tm = if tm = from then to else tm;
   9.541 +  in
   9.542 +    repl
   9.543 +  end;
   9.544 +
   9.545 +val rcomb_tms = fold (fn arg => fn func => NApp (func, arg));
   9.546 +val abs_tms = fold_rev (curry NAbs);
   9.547 +
   9.548 +fun fresh_var_names_wrt_tm n tm =
   9.549 +  let
   9.550 +    fun max_var_br (_, vars, body) = fold max_var (body :: vars)
   9.551 +    and max_var (NAtom _) = I
   9.552 +      | max_var (NConst (id, _, _)) =
   9.553 +        (fn max => if String.isPrefix nun_var_prefix id andalso size id > size max then id else max)
   9.554 +      | max_var (NApp (func, arg)) = fold max_var [func, arg]
   9.555 +      | max_var (NAbs (var, body)) = fold max_var [var, body]
   9.556 +      | max_var (NMatch (obj, branches)) = max_var obj #> fold max_var_br branches;
   9.557 +
   9.558 +    val dummy_name = nun_var_of_str Name.uu;
   9.559 +    val max_name = max_var tm dummy_name;
   9.560 +  in
   9.561 +    map (index_name max_name) (1 upto n)
   9.562 +  end;
   9.563 +
   9.564 +fun beta_reduce_tm (NApp (NAbs (var, body), arg)) = beta_reduce_tm (replace_tm var arg body)
   9.565 +  | beta_reduce_tm (NApp (const, arg)) =
   9.566 +    (case beta_reduce_tm const of
   9.567 +      const' as NAbs _ => beta_reduce_tm (NApp (const', arg))
   9.568 +    | const' => NApp (const', beta_reduce_tm arg))
   9.569 +  | beta_reduce_tm (NAbs (var, body)) = NAbs (var, beta_reduce_tm body)
   9.570 +  | beta_reduce_tm (NMatch (obj, branches)) =
   9.571 +    NMatch (beta_reduce_tm obj, map (@{apply 3(3)} beta_reduce_tm) branches)
   9.572 +  | beta_reduce_tm tm = tm;
   9.573 +
   9.574 +fun eta_expandN_tm 0 tm = tm
   9.575 +  | eta_expandN_tm n tm =
   9.576 +    let
   9.577 +      val var_names = fresh_var_names_wrt_tm n tm;
   9.578 +      val arg_tys = domain_tys n (ty_of tm);
   9.579 +      val vars = map2 (fn id => fn ty => NConst (id, [], ty)) var_names arg_tys;
   9.580 +    in
   9.581 +      abs_tms vars (rcomb_tms vars tm)
   9.582 +    end;
   9.583 +
   9.584 +val eta_expand_builtin_tm =
   9.585 +  let
   9.586 +    fun expand_quant_arg (NAbs (var, body)) = NAbs (var, expand_quant_arg body)
   9.587 +      | expand_quant_arg (NMatch (obj, branches)) =
   9.588 +        NMatch (obj, map (@{apply 3(3)} expand_quant_arg) branches)
   9.589 +      | expand_quant_arg (tm as NApp (_, NAbs _)) = tm
   9.590 +      | expand_quant_arg (NApp (quant, arg)) = NApp (quant, eta_expandN_tm 1 arg)
   9.591 +      | expand_quant_arg tm = tm;
   9.592 +
   9.593 +    fun expand args (NApp (func, arg)) = expand (expand [] arg :: args) func
   9.594 +      | expand args (func as NConst (id, _, _)) =
   9.595 +        let val missing = Int.max (0, arity_of_nun_builtin id - length args) in
   9.596 +          rcomb_tms args func
   9.597 +          |> eta_expandN_tm missing
   9.598 +          |> is_nun_const_quantifier id ? expand_quant_arg
   9.599 +        end
   9.600 +      | expand args (func as NAtom _) = rcomb_tms args func
   9.601 +      | expand args (NAbs (var, body)) = rcomb_tms args (NAbs (var, expand [] body))
   9.602 +      | expand args (NMatch (obj, branches)) =
   9.603 +        rcomb_tms args (NMatch (obj, map (@{apply 3(3)} (expand [])) branches));
   9.604 +  in
   9.605 +    expand []
   9.606 +  end;
   9.607 +
   9.608 +val str_of_ty =
   9.609 +  let
   9.610 +    fun str_of maybe_parens (NType (id, tys)) =
   9.611 +      if id = nun_arrow then
   9.612 +        (case tys of
   9.613 +          [ty, ty'] => maybe_parens (str_of nun_parens ty ^ " " ^ nun_arrow ^ " " ^ str_of I ty'))
   9.614 +      else
   9.615 +        id ^ str_of_nun_arg_list (str_of I) tys
   9.616 +  in
   9.617 +    str_of I
   9.618 +  end;
   9.619 +
   9.620 +val (str_of_tmty, str_of_tm) =
   9.621 +  let
   9.622 +    fun is_triv_head (NConst (id, _, _)) = (arity_of_nun_builtin id = 0)
   9.623 +      | is_triv_head (NAtom _) = true
   9.624 +      | is_triv_head (NApp (const, _)) = is_triv_head const
   9.625 +      | is_triv_head (NAbs _) = false
   9.626 +      | is_triv_head (NMatch _) = false;
   9.627 +
   9.628 +    fun str_of_at_const id tys =
   9.629 +      nun_at ^ str_of_ident id ^ str_of_nun_arg_list str_of_ty tys;
   9.630 +
   9.631 +    fun str_of_app ty_opt const arg =
   9.632 +      let
   9.633 +        val ty_opt' =
   9.634 +          try (Option.map (fn ty => mk_arrow_ty (ty_of arg, ty))) ty_opt
   9.635 +          |> the_default NONE;
   9.636 +      in
   9.637 +        (str_of ty_opt' const |> (case const of NAbs _ => nun_parens | _ => I)) ^
   9.638 +        str_of_nun_arg_list (str_of NONE) [arg]
   9.639 +      end
   9.640 +    and str_of_br ty_opt (id, vars, body) =
   9.641 +      " " ^ nun_bar ^ " " ^ id ^ space_implode "" (map (prefix " " o str_of NONE) vars) ^ " " ^
   9.642 +      nun_arrow ^ " " ^ str_of ty_opt body
   9.643 +    and str_of_tmty tm =
   9.644 +      let val ty = ty_of tm in
   9.645 +        str_of (SOME ty) tm ^ " " ^ nun_colon ^ " " ^ str_of_ty ty
   9.646 +      end
   9.647 +    and str_of _ (NAtom (j, _)) = nun_dollar ^ string_of_int j
   9.648 +      | str_of _ (NConst (id, [], _)) = str_of_ident id
   9.649 +      | str_of (SOME ty0) (NConst (id, tys, ty)) =
   9.650 +        if ty = ty0 then str_of_ident id else str_of_at_const id tys
   9.651 +      | str_of _ (NConst (id, tys, _)) = str_of_at_const id tys
   9.652 +      | str_of ty_opt (NAbs (var, body)) =
   9.653 +        nun_lambda ^ " " ^
   9.654 +        (case ty_opt of
   9.655 +          SOME ty => str_of (SOME (domain_ty ty))
   9.656 +        | NONE => nun_parens o str_of_tmty) var ^
   9.657 +        nun_dot ^ " " ^ str_of (Option.map range_ty ty_opt) body
   9.658 +      | str_of ty_opt (NMatch (obj, branches)) =
   9.659 +        nun_match ^ " " ^ str_of NONE obj ^ " " ^ nun_with ^ " " ^
   9.660 +        space_implode "" (map (str_of_br ty_opt) branches) ^ " " ^ nun_end
   9.661 +      | str_of ty_opt (app as NApp (func, argN)) =
   9.662 +        (case (func, argN) of
   9.663 +          (NApp (oper as NConst (id, _, _), arg1), arg2) =>
   9.664 +          if id = nun_asserting then
   9.665 +            str_of ty_opt arg1 ^ " " ^ nun_asserting ^ " " ^ str_of (SOME prop_ty) arg2
   9.666 +            |> nun_parens
   9.667 +          else if id = nun_equals then
   9.668 +            (str_of NONE arg1 |> not (is_triv_head arg1) ? nun_parens) ^ " " ^ id ^ " " ^
   9.669 +            (str_of (try ty_of arg2) arg2 |> not (is_triv_head arg2) ? nun_parens)
   9.670 +          else if is_nun_const_connective id then
   9.671 +            let val args = dest_rassoc_args oper arg1 arg2 in
   9.672 +              space_implode (" " ^ id ^ " ")
   9.673 +                (map (fn arg => str_of NONE arg |> not (is_triv_head arg) ? nun_parens) args)
   9.674 +            end
   9.675 +          else
   9.676 +            str_of_app ty_opt func argN
   9.677 +        | (NApp (NApp (NConst (id, _, _), arg1), arg2), arg3) =>
   9.678 +          if id = nun_if then
   9.679 +            nun_if ^ " " ^ str_of NONE arg1 ^ " " ^ nun_then ^ " " ^ str_of NONE arg2 ^ " " ^
   9.680 +            nun_else ^ " " ^ str_of NONE arg3
   9.681 +            |> nun_parens
   9.682 +          else
   9.683 +            str_of_app ty_opt func argN
   9.684 +        | (NConst (id, _, _), NAbs _) =>
   9.685 +          if is_nun_const_quantifier id then
   9.686 +            let val (vars, body) = strip_nun_binders id app in
   9.687 +              id ^ " " ^ space_implode " " (map (nun_parens o str_of_tmty) vars) ^ nun_dot ^ " " ^
   9.688 +              str_of NONE body
   9.689 +            end
   9.690 +          else
   9.691 +            str_of_app ty_opt func argN
   9.692 +        | _ => str_of_app ty_opt func argN);
   9.693 +  in
   9.694 +    (str_of_tmty, str_of NONE)
   9.695 +  end;
   9.696 +
   9.697 +val empty_name_pool = {nice_of_ugly = Symtab.empty, ugly_of_nice = Symtab.empty};
   9.698 +
   9.699 +val nice_of_ugly_suggestion =
   9.700 +  unascii_of #> Long_Name.base_name #> ascii_of #> unsuffix nun_custom_id_suffix
   9.701 +  #> (fn s => if s = "" orelse not (Char.isAlpha (String.sub (s, 0))) then "x" ^ s else s);
   9.702 +
   9.703 +fun allocate_nice ({nice_of_ugly, ugly_of_nice} : name_pool) (ugly, nice_sugg0) =
   9.704 +  let
   9.705 +    fun alloc j =
   9.706 +      let val nice_sugg = index_name nice_sugg0 j in
   9.707 +        (case Symtab.lookup ugly_of_nice nice_sugg of
   9.708 +          NONE =>
   9.709 +          (nice_sugg,
   9.710 +           {nice_of_ugly = Symtab.update_new (ugly, nice_sugg) nice_of_ugly,
   9.711 +            ugly_of_nice = Symtab.update_new (nice_sugg, ugly) ugly_of_nice})
   9.712 +        | SOME _ => alloc (j + 1))
   9.713 +      end;
   9.714 +  in
   9.715 +    alloc 0
   9.716 +  end;
   9.717 +
   9.718 +fun nice_ident ugly (pool as {nice_of_ugly, ...}) =
   9.719 +  if String.isSuffix nun_custom_id_suffix ugly then
   9.720 +    (case Symtab.lookup nice_of_ugly ugly of
   9.721 +      NONE => allocate_nice pool (ugly, nice_of_ugly_suggestion ugly)
   9.722 +    | SOME nice => (nice, pool))
   9.723 +  else
   9.724 +    (ugly, pool);
   9.725 +
   9.726 +fun nice_nun_problem problem =
   9.727 +  fold_map_nun_problem_idents nice_ident problem empty_name_pool;
   9.728 +
   9.729 +fun str_of_tval (NType (id, tys)) =
   9.730 +  str_of_ident id ^ " " ^ nun_colon ^ " " ^
   9.731 +  fold (K (prefix (nun_type ^ " " ^ nun_arrow ^ " "))) tys nun_type;
   9.732 +
   9.733 +fun is_triv_wrt (NAbs (_, body)) = is_triv_wrt body
   9.734 +  | is_triv_wrt (NConst (id, _, _)) = (id = nun_true)
   9.735 +  | is_triv_wrt _ = false;
   9.736 +
   9.737 +fun str_of_nun_type_spec {abs_ty, rep_ty, wrt, abs, rep} =
   9.738 +  str_of_ty abs_ty ^ " " ^ nun_assign ^ " " ^ str_of_ty rep_ty ^
   9.739 +  (if is_triv_wrt wrt then "" else "\n  " ^ nun_wrt ^ " " ^ str_of_tm wrt) ^
   9.740 +  "\n  " ^ nun_abstract ^ " " ^ str_of_tm abs ^ "\n  " ^ nun_concrete ^ " " ^ str_of_tm rep;
   9.741 +
   9.742 +fun str_of_nun_ctr_spec {ctr, arg_tys} =
   9.743 +  str_of_tm ctr ^ str_of_nun_arg_list str_of_ty arg_tys;
   9.744 +
   9.745 +fun str_of_nun_co_data_spec {ty, ctrs} =
   9.746 +  str_of_ty ty ^ " " ^ nun_assign ^ "\n  " ^
   9.747 +  space_implode ("\n" ^ nun_bar ^ " ") (map str_of_nun_ctr_spec ctrs);
   9.748 +
   9.749 +fun str_of_nun_const_spec {const, props} =
   9.750 +  str_of_tmty const ^ " " ^ nun_assign ^ "\n  " ^
   9.751 +  space_implode (nun_semicolon ^ "\n  ") (map str_of_tm props);
   9.752 +
   9.753 +fun str_of_nun_consts_spec {consts, props} =
   9.754 +  space_implode (" " ^ nun_and ^ "\n     ") (map str_of_tmty consts) ^ " " ^ nun_assign ^ "\n  " ^
   9.755 +  space_implode (nun_semicolon ^ "\n  ") (map str_of_tm props);
   9.756 +
   9.757 +fun str_of_nun_cards_suffix (NONE, NONE) = ""
   9.758 +  | str_of_nun_cards_suffix (c1, c2) =
   9.759 +    let
   9.760 +      val s1 = Option.map (prefix "min_card " o signed_string_of_int) c1;
   9.761 +      val s2 = Option.map (prefix "max_card " o signed_string_of_int) c2;
   9.762 +    in
   9.763 +      enclose " [" "]" (space_implode ", " (map_filter I [s1, s2]))
   9.764 +    end;
   9.765 +
   9.766 +fun str_of_nun_command (NTVal (ty, cards)) =
   9.767 +    nun_val ^ " " ^ str_of_tval ty ^ str_of_nun_cards_suffix cards
   9.768 +  | str_of_nun_command (NCopy spec) = nun_copy ^ " " ^ str_of_nun_type_spec spec
   9.769 +  | str_of_nun_command (NQuotient spec) = nun_quotient ^ " " ^ str_of_nun_type_spec spec
   9.770 +  | str_of_nun_command (NData specs) =
   9.771 +    nun_data ^ " " ^ str_of_nun_and_list str_of_nun_co_data_spec specs
   9.772 +  | str_of_nun_command (NCodata specs) =
   9.773 +    nun_codata ^ " " ^ str_of_nun_and_list str_of_nun_co_data_spec specs
   9.774 +  | str_of_nun_command (NVal (tm, ty)) =
   9.775 +    nun_val ^ " " ^ str_of_tm tm ^ " " ^ nun_colon ^ " " ^ str_of_ty ty
   9.776 +  | str_of_nun_command (NPred (wf, specs)) =
   9.777 +    nun_pred ^ " " ^ (if wf then nun_lbracket ^ nun_wf ^ nun_rbracket ^ " " else "") ^
   9.778 +    str_of_nun_and_list str_of_nun_const_spec specs
   9.779 +  | str_of_nun_command (NCopred specs) =
   9.780 +    nun_copred ^ " " ^ str_of_nun_and_list str_of_nun_const_spec specs
   9.781 +  | str_of_nun_command (NRec specs) =
   9.782 +    nun_rec ^ " " ^ str_of_nun_and_list str_of_nun_const_spec specs
   9.783 +  | str_of_nun_command (NSpec spec) = nun_spec ^ " " ^ str_of_nun_consts_spec spec
   9.784 +  | str_of_nun_command (NAxiom tm) = nun_axiom ^ " " ^ str_of_tm tm
   9.785 +  | str_of_nun_command (NGoal tm) = nun_goal ^ " " ^ str_of_tm tm
   9.786 +  | str_of_nun_command (NEval tm) = nun_hash ^ " " ^ nun_eval ^ " " ^ str_of_tm tm;
   9.787 +
   9.788 +fun str_of_nun_problem {commandss, sound, complete} =
   9.789 +  map (cat_lines o map (suffix nun_dot o str_of_nun_command)) commandss
   9.790 +  |> space_implode "\n\n" |> suffix "\n"
   9.791 +  |> prefix (nun_hash ^ " " ^ (if sound then "sound" else "unsound") ^ "\n")
   9.792 +  |> prefix (nun_hash ^ " " ^ (if complete then "complete" else "incomplete") ^ "\n");
   9.793 +
   9.794 +end;
    10.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    10.2 +++ b/src/HOL/Nunchaku/Tools/nunchaku_reconstruct.ML	Mon Oct 24 22:42:07 2016 +0200
    10.3 @@ -0,0 +1,244 @@
    10.4 +(*  Title:      HOL/Nunchaku/Tools/nunchaku_reconstruct.ML
    10.5 +    Author:     Jasmin Blanchette, Inria Nancy, LORIA, MPII
    10.6 +    Copyright   2015, 2016
    10.7 +
    10.8 +Reconstruction of Nunchaku models in Isabelle/HOL.
    10.9 +*)
   10.10 +
   10.11 +signature NUNCHAKU_RECONSTRUCT =
   10.12 +sig
   10.13 +  type nun_model = Nunchaku_Model.nun_model
   10.14 +
   10.15 +  type typ_entry = typ * term list
   10.16 +  type term_entry = term * term
   10.17 +
   10.18 +  type isa_model =
   10.19 +    {type_model: typ_entry list,
   10.20 +     free_model: term_entry list,
   10.21 +     pat_complete_model: term_entry list,
   10.22 +     pat_incomplete_model: term_entry list,
   10.23 +     skolem_model: term_entry list}
   10.24 +
   10.25 +  val str_of_isa_model: Proof.context -> isa_model -> string
   10.26 +
   10.27 +  val isa_model_of_nun: Proof.context -> term list -> (typ option * string list) list ->
   10.28 +    nun_model -> isa_model
   10.29 +end;
   10.30 +
   10.31 +structure Nunchaku_Reconstruct : NUNCHAKU_RECONSTRUCT =
   10.32 +struct
   10.33 +
   10.34 +open Nunchaku_Util;
   10.35 +open Nunchaku_Problem;
   10.36 +open Nunchaku_Translate;
   10.37 +open Nunchaku_Model;
   10.38 +
   10.39 +type typ_entry = typ * term list;
   10.40 +type term_entry = term * term;
   10.41 +
   10.42 +type isa_model =
   10.43 +  {type_model: typ_entry list,
   10.44 +   free_model: term_entry list,
   10.45 +   pat_complete_model: term_entry list,
   10.46 +   pat_incomplete_model: term_entry list,
   10.47 +   skolem_model: term_entry list};
   10.48 +
   10.49 +val anonymousN = "anonymous";
   10.50 +val irrelevantN = "irrelevant";
   10.51 +val unparsableN = "unparsable";
   10.52 +
   10.53 +val nun_arrow_exploded = String.explode nun_arrow;
   10.54 +
   10.55 +val is_ty_meta = member (op =) (String.explode "()->,");
   10.56 +
   10.57 +fun next_token_lowlevel [] = (End_of_Stream, [])
   10.58 +  | next_token_lowlevel (c :: cs) =
   10.59 +    if Char.isSpace c then
   10.60 +      next_token_lowlevel cs
   10.61 +    else if not (is_ty_meta c) then
   10.62 +      let val n = find_index (Char.isSpace orf is_ty_meta) cs in
   10.63 +        (if n = ~1 then (cs, []) else chop n cs)
   10.64 +        |>> (cons c #> String.implode #> ident_of_str #> Ident)
   10.65 +      end
   10.66 +    else if is_prefix (op =) nun_arrow_exploded (c :: cs) then
   10.67 +      (Ident nun_arrow, tl cs)
   10.68 +    else
   10.69 +      (Symbol (String.str c), cs);
   10.70 +
   10.71 +val tokenize_lowlevel =
   10.72 +  let
   10.73 +    fun toks cs =
   10.74 +      (case next_token_lowlevel cs of
   10.75 +        (End_of_Stream, []) => []
   10.76 +      | (tok, cs') => tok :: toks cs');
   10.77 +  in
   10.78 +    toks o String.explode
   10.79 +  end;
   10.80 +
   10.81 +fun parse_lowlevel_ty tok =
   10.82 +  (Scan.optional
   10.83 +     (parse_sym "(" |-- Scan.repeat (parse_lowlevel_ty --| Scan.option (parse_sym ",")) --|
   10.84 +      parse_sym ")")
   10.85 +     []
   10.86 +   -- parse_ident >> (swap #> NType)) tok;
   10.87 +
   10.88 +val ty_of_lowlevel_str = fst o parse_lowlevel_ty o tokenize_lowlevel;
   10.89 +
   10.90 +fun ident_of_const (NConst (id, _, _)) = id
   10.91 +  | ident_of_const _ = nun_dummy;
   10.92 +
   10.93 +fun str_of_typ_entry ctxt (T, ts) =
   10.94 +  "type " ^ Syntax.string_of_typ ctxt T  ^
   10.95 +  " := {" ^ commas (map (Syntax.string_of_term ctxt) ts) ^ "}.";
   10.96 +
   10.97 +fun str_of_term_entry ctxt (tm, value) =
   10.98 +  "val " ^ Syntax.string_of_term ctxt tm ^ " := " ^ Syntax.string_of_term ctxt value ^ ".";
   10.99 +
  10.100 +fun str_of_isa_model ctxt
  10.101 +    {type_model, free_model, pat_complete_model, pat_incomplete_model, skolem_model} =
  10.102 +  map (str_of_typ_entry ctxt) type_model @ "" ::
  10.103 +  map (str_of_term_entry ctxt) free_model @ "" ::
  10.104 +  map (str_of_term_entry ctxt) pat_complete_model @ "" ::
  10.105 +  map (str_of_term_entry ctxt) pat_incomplete_model @ "" ::
  10.106 +  map (str_of_term_entry ctxt) skolem_model
  10.107 +  |> cat_lines;
  10.108 +
  10.109 +fun typ_of_nun ctxt =
  10.110 +  let
  10.111 +    fun typ_of (NType (id, tys)) =
  10.112 +      let val Ts = map typ_of tys in
  10.113 +        if id = nun_dummy then
  10.114 +          dummyT
  10.115 +        else if id = nun_prop then
  10.116 +          @{typ bool}
  10.117 +        else if id = nun_arrow then
  10.118 +          Type (@{type_name fun}, Ts)
  10.119 +        else
  10.120 +          (case try str_of_nun_tconst id of
  10.121 +            SOME (args, s) =>
  10.122 +            let val tys' = map ty_of_lowlevel_str args in
  10.123 +              Type (s, map typ_of (tys' @ tys))
  10.124 +            end
  10.125 +          | NONE =>
  10.126 +            (case try str_of_nun_tfree id of
  10.127 +              SOME s => TFree (Proof_Context.check_tfree ctxt (flip_quote s, dummyS))
  10.128 +            | NONE => raise Fail ("unknown type constructor: " ^ quote (str_of_ident id))))
  10.129 +      end;
  10.130 +  in
  10.131 +    typ_of
  10.132 +  end;
  10.133 +
  10.134 +fun one_letter_of s =
  10.135 +  let val c = String.sub (Long_Name.base_name s, 0) in
  10.136 +    String.str (if Char.isAlpha c then c else #"x")
  10.137 +  end;
  10.138 +
  10.139 +fun base_of_typ (Type (s, _)) = s
  10.140 +  | base_of_typ (TFree (s, _)) = flip_quote s
  10.141 +  | base_of_typ (TVar ((s, _), _)) = flip_quote s;
  10.142 +
  10.143 +fun term_of_nun ctxt atomss =
  10.144 +  let
  10.145 +    val thy = Proof_Context.theory_of ctxt;
  10.146 +
  10.147 +    val typ_of = typ_of_nun ctxt;
  10.148 +
  10.149 +    fun nth_atom T j =
  10.150 +      let val ss = these (triple_lookup (typ_match thy) atomss T) in
  10.151 +        if j >= 0 andalso j < length ss then nth ss j
  10.152 +        else one_letter_of (base_of_typ T) ^ nat_subscript (j + 1)
  10.153 +      end;
  10.154 +
  10.155 +    fun term_of _ (NAtom (j, ty)) =
  10.156 +        let val T = typ_of ty in Var ((nth_atom T j, 0), T) end
  10.157 +      | term_of bounds (NConst (id, tys0, ty)) =
  10.158 +        if id = nun_conj then
  10.159 +          HOLogic.conj
  10.160 +        else if id = nun_disj then
  10.161 +          HOLogic.disj
  10.162 +        else if id = nun_choice then
  10.163 +          Const (@{const_name Eps}, typ_of ty)
  10.164 +        else if id = nun_equals then
  10.165 +          Const (@{const_name HOL.eq}, typ_of ty)
  10.166 +        else if id = nun_false then
  10.167 +          @{const False}
  10.168 +        else if id = nun_if then
  10.169 +          Const (@{const_name If}, typ_of ty)
  10.170 +        else if id = nun_implies then
  10.171 +          @{term implies}
  10.172 +        else if id = nun_unique then
  10.173 +          Const (@{const_name The}, typ_of ty)
  10.174 +        else if id = nun_unique_unsafe then
  10.175 +          Const (@{const_name The_unsafe}, typ_of ty)
  10.176 +        else if id = nun_true then
  10.177 +          @{const True}
  10.178 +        else if String.isPrefix nun_anon_fun_prefix id then
  10.179 +          let val j = Int.fromString (unprefix nun_anon_fun_prefix id) |> the_default ~1 in
  10.180 +            Var ((anonymousN ^ nat_subscript (j + 1), 0), typ_of ty)
  10.181 +          end
  10.182 +        else if id = nun_irrelevant then
  10.183 +          (* FIXME: get bounds from Nunchaku *)
  10.184 +          list_comb (Var ((irrelevantN, 0), map (typ_of o safe_ty_of) bounds ---> typ_of ty),
  10.185 +            map Bound (length bounds - 1 downto 0))
  10.186 +        else if id = nun_unparsable then
  10.187 +          (* FIXME: get bounds from Nunchaku *)
  10.188 +          list_comb (Var ((unparsableN, 0), typ_of ty), map Bound (length bounds - 1 downto 0))
  10.189 +        else
  10.190 +          (case try str_of_nun_const id of
  10.191 +            SOME (args, s) =>
  10.192 +            let val tys = map ty_of_lowlevel_str args in
  10.193 +              Sign.mk_const thy (s, map typ_of (tys @ tys0))
  10.194 +            end
  10.195 +          | NONE =>
  10.196 +            (case try str_of_nun_free id of
  10.197 +              SOME s => Free (s, typ_of ty)
  10.198 +            | NONE =>
  10.199 +              (case try str_of_nun_var id of
  10.200 +                SOME s => Var ((s, 0), typ_of ty)
  10.201 +              | NONE =>
  10.202 +                (case find_index (fn bound => ident_of_const bound = id) bounds of
  10.203 +                  ~1 => Var ((str_of_ident id, 0), typ_of ty) (* shouldn't happen? *)
  10.204 +                | j => Bound j))))
  10.205 +      | term_of bounds (NAbs (var, body)) =
  10.206 +        let val T = typ_of (safe_ty_of var) in
  10.207 +          Abs (one_letter_of (base_of_typ T), T, term_of (var :: bounds) body)
  10.208 +        end
  10.209 +      | term_of bounds (NApp (func, arg)) =
  10.210 +        let
  10.211 +          fun same () = term_of bounds func $ term_of bounds arg;
  10.212 +        in
  10.213 +          (case (func, arg) of
  10.214 +            (NConst (id, _, _), NAbs _) =>
  10.215 +            if id = nun_mu then
  10.216 +              let val Abs (s, T, body) = term_of bounds arg in
  10.217 +                Const (@{const_name The}, (T --> HOLogic.boolT) --> T)
  10.218 +                $ Abs (s, T, HOLogic.eq_const T $ Bound 0 $ body)
  10.219 +              end
  10.220 +            else
  10.221 +              same ()
  10.222 +          | _ => same ())
  10.223 +        end
  10.224 +      | term_of _ (NMatch _) = raise Fail "unexpected match";
  10.225 +  in
  10.226 +    term_of []
  10.227 +  end;
  10.228 +
  10.229 +fun isa_typ_entry_of_nun ctxt atomss (ty, atoms) =
  10.230 +  (typ_of_nun ctxt ty, map (term_of_nun ctxt atomss) atoms);
  10.231 +
  10.232 +fun isa_term_entry_of_nun ctxt atomss (tm, value) =
  10.233 +  (term_of_nun ctxt atomss tm, term_of_nun ctxt atomss value);
  10.234 +
  10.235 +fun isa_model_of_nun ctxt pat_completes atomss {type_model, const_model, skolem_model} =
  10.236 +  let
  10.237 +    val free_and_const_model = map (isa_term_entry_of_nun ctxt atomss) const_model;
  10.238 +    val (free_model, (pat_complete_model, pat_incomplete_model)) =
  10.239 +      List.partition (is_Free o fst) free_and_const_model
  10.240 +      ||> List.partition (member (op aconv) pat_completes o fst);
  10.241 +  in
  10.242 +    {type_model = map (isa_typ_entry_of_nun ctxt atomss) type_model, free_model = free_model,
  10.243 +     pat_complete_model = pat_complete_model, pat_incomplete_model = pat_incomplete_model,
  10.244 +     skolem_model = map (isa_term_entry_of_nun ctxt atomss) skolem_model}
  10.245 +  end;
  10.246 +
  10.247 +end;
    11.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    11.2 +++ b/src/HOL/Nunchaku/Tools/nunchaku_tool.ML	Mon Oct 24 22:42:07 2016 +0200
    11.3 @@ -0,0 +1,134 @@
    11.4 +(*  Title:      HOL/Nunchaku/Tools/nunchaku_tool.ML
    11.5 +    Author:     Jasmin Blanchette, Inria Nancy, LORIA, MPII
    11.6 +    Copyright   2015, 2016
    11.7 +
    11.8 +Interface to the external "nunchaku" tool.
    11.9 +*)
   11.10 +
   11.11 +signature NUNCHAKU_TOOL =
   11.12 +sig
   11.13 +  type ty = Nunchaku_Problem.ty
   11.14 +  type tm = Nunchaku_Problem.tm
   11.15 +  type nun_problem = Nunchaku_Problem.nun_problem
   11.16 +
   11.17 +  type tool_params =
   11.18 +    {overlord: bool,
   11.19 +     debug: bool,
   11.20 +     specialize: bool,
   11.21 +     timeout: Time.time}
   11.22 +
   11.23 +  type nun_solution =
   11.24 +    {tys: (ty * tm list) list,
   11.25 +     tms: (tm * tm) list}
   11.26 +
   11.27 +  datatype nun_outcome =
   11.28 +    Unsat
   11.29 +  | Sat of string * nun_solution
   11.30 +  | Unknown of (string * nun_solution) option
   11.31 +  | Timeout
   11.32 +  | Nunchaku_Var_Not_Set
   11.33 +  | Nunchaku_Cannot_Execute
   11.34 +  | Nunchaku_Not_Found
   11.35 +  | CVC4_Cannot_Execute
   11.36 +  | CVC4_Not_Found
   11.37 +  | Unknown_Error of int * string
   11.38 +
   11.39 +  val nunchaku_env_var: string
   11.40 +
   11.41 +  val solve_nun_problem: tool_params -> nun_problem -> nun_outcome
   11.42 +end;
   11.43 +
   11.44 +structure Nunchaku_Tool : NUNCHAKU_TOOL =
   11.45 +struct
   11.46 +
   11.47 +open Nunchaku_Util;
   11.48 +open Nunchaku_Problem;
   11.49 +
   11.50 +type tool_params =
   11.51 +  {overlord: bool,
   11.52 +   debug: bool,
   11.53 +   specialize: bool,
   11.54 +   timeout: Time.time};
   11.55 +
   11.56 +type nun_solution =
   11.57 +  {tys: (ty * tm list) list,
   11.58 +   tms: (tm * tm) list};
   11.59 +
   11.60 +datatype nun_outcome =
   11.61 +  Unsat
   11.62 +| Sat of string * nun_solution
   11.63 +| Unknown of (string * nun_solution) option
   11.64 +| Timeout
   11.65 +| Nunchaku_Var_Not_Set
   11.66 +| Nunchaku_Cannot_Execute
   11.67 +| Nunchaku_Not_Found
   11.68 +| CVC4_Cannot_Execute
   11.69 +| CVC4_Not_Found
   11.70 +| Unknown_Error of int * string;
   11.71 +
   11.72 +fun bash_output_error s =
   11.73 +  let val {out, err, rc, ...} = Bash.process s in
   11.74 +    ((out, err), rc)
   11.75 +  end;
   11.76 +
   11.77 +val nunchaku_env_var = "NUNCHAKU";
   11.78 +
   11.79 +val cached_outcome =
   11.80 +  Synchronized.var "Nunchaku_Tool.cached_outcome" (NONE : (nun_problem * nun_outcome) option);
   11.81 +
   11.82 +fun uncached_solve_nun_problem ({overlord, specialize, timeout, ...} : tool_params)
   11.83 +    (problem as {sound, complete, ...}) =
   11.84 +  with_tmp_or_overlord_file overlord "nunchaku" "nun" (fn prob_path =>
   11.85 +    if getenv nunchaku_env_var = "" then
   11.86 +      Nunchaku_Var_Not_Set
   11.87 +    else
   11.88 +      let
   11.89 +        val bash_cmd =
   11.90 +          "\"$" ^ nunchaku_env_var ^ "\" \
   11.91 +          \--skolems-in-model --no-color " ^
   11.92 +          (if specialize then "" else "--no-specialize ") ^
   11.93 +          "--timeout " ^ string_of_int (Time.toSeconds timeout) ^ " " ^
   11.94 +          File.bash_path prob_path;
   11.95 +        val comments =
   11.96 +          [bash_cmd, "This file was generated by Isabelle (most likely Nunchaku)", timestamp ()];
   11.97 +        val prob_str = cat_lines (map (prefix "# ") comments) ^ "\n\n" ^ str_of_nun_problem problem;
   11.98 +        val _ = File.write prob_path prob_str;
   11.99 +        val ((output, error), code) = bash_output_error bash_cmd;
  11.100 +      in
  11.101 +        if String.isPrefix "SAT" output then
  11.102 +          (if sound then Sat else Unknown o SOME) (output, {tys = [], tms = []})
  11.103 +        else if String.isPrefix "UNSAT" output then
  11.104 +          if complete then Unsat else Unknown NONE
  11.105 +        else if String.isPrefix "UNKNOWN" output then
  11.106 +          Unknown NONE
  11.107 +        else if String.isPrefix "TIMEOUT" output then
  11.108 +          Timeout
  11.109 +        else if code = 126 then
  11.110 +          Nunchaku_Cannot_Execute
  11.111 +        else if code = 127 then
  11.112 +          Nunchaku_Not_Found
  11.113 +        else
  11.114 +          Unknown_Error (code,
  11.115 +            simplify_spaces (elide_string 1000 (if error <> "" then error else output)))
  11.116 +      end);
  11.117 +
  11.118 +fun solve_nun_problem (params as {overlord, debug, ...}) problem =
  11.119 +  (case (overlord orelse debug,
  11.120 +      AList.lookup (op =) (the_list (Synchronized.value cached_outcome)) problem) of
  11.121 +    (false, SOME outcome) => outcome
  11.122 +  | _ =>
  11.123 +    let
  11.124 +      val outcome = uncached_solve_nun_problem params problem;
  11.125 +
  11.126 +      fun update_cache () =
  11.127 +        Synchronized.change cached_outcome (K (SOME (problem, outcome)));
  11.128 +    in
  11.129 +      (case outcome of
  11.130 +        Unsat => update_cache ()
  11.131 +      | Sat _ => update_cache ()
  11.132 +      | Unknown _ => update_cache ()
  11.133 +      | _ => ());
  11.134 +      outcome
  11.135 +    end);
  11.136 +
  11.137 +end;
    12.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    12.2 +++ b/src/HOL/Nunchaku/Tools/nunchaku_translate.ML	Mon Oct 24 22:42:07 2016 +0200
    12.3 @@ -0,0 +1,189 @@
    12.4 +(*  Title:      HOL/Nunchaku/Tools/nunchaku_translate.ML
    12.5 +    Author:     Jasmin Blanchette, Inria Nancy, LORIA, MPII
    12.6 +    Copyright   2015, 2016
    12.7 +
    12.8 +Translation of Isabelle/HOL problems to Nunchaku.
    12.9 +*)
   12.10 +
   12.11 +signature NUNCHAKU_TRANSLATE =
   12.12 +sig
   12.13 +  type isa_problem = Nunchaku_Collect.isa_problem
   12.14 +  type ty = Nunchaku_Problem.ty
   12.15 +  type nun_problem = Nunchaku_Problem.nun_problem
   12.16 +
   12.17 +  val flip_quote: string -> string
   12.18 +  val lowlevel_str_of_ty: ty -> string
   12.19 +
   12.20 +  val nun_problem_of_isa: Proof.context -> isa_problem -> nun_problem
   12.21 +end;
   12.22 +
   12.23 +structure Nunchaku_Translate : NUNCHAKU_TRANSLATE =
   12.24 +struct
   12.25 +
   12.26 +open Nunchaku_Util;
   12.27 +open Nunchaku_Collect;
   12.28 +open Nunchaku_Problem;
   12.29 +
   12.30 +fun flip_quote s =
   12.31 +  (case try (unprefix "'") s of
   12.32 +    SOME s' => s'
   12.33 +  | NONE => prefix "'" s);
   12.34 +
   12.35 +fun lowlevel_str_of_ty (NType (id, tys)) =
   12.36 +  (if null tys then "" else encode_args (map lowlevel_str_of_ty tys)) ^ id;
   12.37 +
   12.38 +fun strip_nun_abs 0 tm = ([], tm)
   12.39 +  | strip_nun_abs n (NAbs (var, body)) =
   12.40 +    strip_nun_abs (n - 1) body
   12.41 +    |>> cons var;
   12.42 +
   12.43 +val strip_nun_comb =
   12.44 +  let
   12.45 +    fun strip args (NApp (func, arg)) = strip (arg :: args) func
   12.46 +      | strip args tm = (tm, args);
   12.47 +  in
   12.48 +    strip []
   12.49 +  end;
   12.50 +
   12.51 +fun ty_of_isa (Type (s, Ts)) =
   12.52 +    let val tys = map ty_of_isa Ts in
   12.53 +      (case s of
   12.54 +        @{type_name bool} => prop_ty
   12.55 +      | @{type_name fun} => NType (nun_arrow, tys)
   12.56 +      | _ =>
   12.57 +        let
   12.58 +          val args = map lowlevel_str_of_ty tys;
   12.59 +          val id = nun_tconst_of_str args s;
   12.60 +        in
   12.61 +          NType (id, [])
   12.62 +        end)
   12.63 +    end
   12.64 +  | ty_of_isa (TFree (s, _)) = NType (nun_tfree_of_str (flip_quote s), [])
   12.65 +  | ty_of_isa (TVar _) = raise Fail "unexpected TVar";
   12.66 +
   12.67 +fun gen_tm_of_isa in_prop ctxt t =
   12.68 +  let
   12.69 +    val thy = Proof_Context.theory_of ctxt;
   12.70 +
   12.71 +    fun id_of_const (x as (s, _)) =
   12.72 +      let val args = map (lowlevel_str_of_ty o ty_of_isa) (Sign.const_typargs thy x) in
   12.73 +        nun_const_of_str args s
   12.74 +      end;
   12.75 +
   12.76 +    fun tm_of_branch ctr_id var_count f_arg_tm =
   12.77 +      let val (vars, body) = strip_nun_abs var_count f_arg_tm in
   12.78 +        (ctr_id, vars, body)
   12.79 +      end;
   12.80 +
   12.81 +    fun tm_of bounds (Const (x as (s, T))) =
   12.82 +        (case try (dest_co_datatype_case ctxt) x of
   12.83 +          SOME ctrs =>
   12.84 +          let
   12.85 +            val num_f_args = length ctrs;
   12.86 +            val min_args = num_f_args + 1;
   12.87 +            val var_counts = map (num_binder_types o snd) ctrs;
   12.88 +
   12.89 +            val dummy_free = Free (Name.uu, T);
   12.90 +            val tm = tm_of bounds dummy_free;
   12.91 +            val tm' = eta_expandN_tm min_args tm;
   12.92 +            val (vars, body) = strip_nun_abs min_args tm';
   12.93 +            val (_, (f_args, obj :: other_args)) = strip_nun_comb body ||> chop num_f_args;
   12.94 +            val f_args' = map2 eta_expandN_tm var_counts f_args;
   12.95 +
   12.96 +            val ctr_ids = map id_of_const ctrs;
   12.97 +          in
   12.98 +            NMatch (obj, @{map 3} tm_of_branch ctr_ids var_counts f_args')
   12.99 +            |> rcomb_tms other_args
  12.100 +            |> abs_tms vars
  12.101 +          end
  12.102 +        | NONE =>
  12.103 +          if s = @{const_name unreachable} andalso in_prop then
  12.104 +            let val ty = ty_of_isa T in
  12.105 +              napps (NConst (nun_asserting, [ty], mk_arrows_ty ([ty, prop_ty], ty)),
  12.106 +                [NConst (id_of_const x, [], ty), NConst (nun_false, [], prop_ty)])
  12.107 +            end
  12.108 +          else
  12.109 +            let
  12.110 +              val id =
  12.111 +                (case s of
  12.112 +                  @{const_name All} => nun_forall
  12.113 +                | @{const_name conj} => nun_conj
  12.114 +                | @{const_name disj} => nun_disj
  12.115 +                | @{const_name HOL.eq} => nun_equals
  12.116 +                | @{const_name Eps} => nun_choice
  12.117 +                | @{const_name Ex} => nun_exists
  12.118 +                | @{const_name False} => nun_false
  12.119 +                | @{const_name If} => nun_if
  12.120 +                | @{const_name implies} => nun_implies
  12.121 +                | @{const_name Not} => nun_not
  12.122 +                | @{const_name The} => nun_unique
  12.123 +                | @{const_name The_unsafe} => nun_unique_unsafe
  12.124 +                | @{const_name True} => nun_true
  12.125 +                | _ => id_of_const x);
  12.126 +            in
  12.127 +              NConst (id, [], ty_of_isa T)
  12.128 +            end)
  12.129 +      | tm_of _ (Free (s, T)) = NConst (nun_free_of_str s, [], ty_of_isa T)
  12.130 +      | tm_of _ (Var ((s, _), T)) = NConst (nun_var_of_str s, [], ty_of_isa T)
  12.131 +      | tm_of bounds (Abs (s, T, t)) =
  12.132 +        let
  12.133 +          val (s', bounds') = Name.variant s bounds;
  12.134 +          val x = Var ((s', 0), T);
  12.135 +        in
  12.136 +          NAbs (tm_of bounds' x, tm_of bounds' (subst_bound (x, t)))
  12.137 +        end
  12.138 +      | tm_of bounds (t $ u) = NApp (tm_of bounds t, tm_of bounds u)
  12.139 +      | tm_of _ (Bound _) = raise Fail "unexpected Bound";
  12.140 +  in
  12.141 +    t
  12.142 +    |> tm_of Name.context
  12.143 +    |> beta_reduce_tm
  12.144 +    |> eta_expand_builtin_tm
  12.145 +  end;
  12.146 +
  12.147 +val tm_of_isa = gen_tm_of_isa false;
  12.148 +val prop_of_isa = gen_tm_of_isa true;
  12.149 +
  12.150 +fun nun_type_spec_of_isa ctxt {abs_typ, rep_typ, wrt, abs, rep} =
  12.151 +  {abs_ty = ty_of_isa abs_typ, rep_ty = ty_of_isa rep_typ, wrt = tm_of_isa ctxt wrt,
  12.152 +   abs = tm_of_isa ctxt abs, rep = tm_of_isa ctxt rep};
  12.153 +
  12.154 +fun nun_ctr_of_isa ctxt ctr =
  12.155 +  {ctr = tm_of_isa ctxt ctr, arg_tys = map ty_of_isa (binder_types (fastype_of ctr))};
  12.156 +
  12.157 +fun nun_co_data_spec_of_isa ctxt {typ, ctrs} =
  12.158 +  {ty = ty_of_isa typ, ctrs = map (nun_ctr_of_isa ctxt) ctrs};
  12.159 +
  12.160 +fun nun_const_spec_of_isa ctxt {const, props} =
  12.161 +  {const = tm_of_isa ctxt const, props = map (prop_of_isa ctxt) props};
  12.162 +
  12.163 +fun nun_rec_spec_of_isa ctxt {const, props, ...} =
  12.164 +  {const = tm_of_isa ctxt const, props = map (prop_of_isa ctxt) props};
  12.165 +
  12.166 +fun nun_consts_spec_of_isa ctxt {consts, props} =
  12.167 +  {consts = map (tm_of_isa ctxt) consts, props = map (prop_of_isa ctxt) props};
  12.168 +
  12.169 +fun nun_problem_of_isa ctxt {commandss, sound, complete} =
  12.170 +  let
  12.171 +    fun cmd_of cmd =
  12.172 +      (case cmd of
  12.173 +        ITVal (T, cards) => NTVal (ty_of_isa T, cards)
  12.174 +      | ICopy spec => NCopy (nun_type_spec_of_isa ctxt spec)
  12.175 +      | IQuotient spec => NQuotient (nun_type_spec_of_isa ctxt spec)
  12.176 +      | ICoData (fp, specs) =>
  12.177 +        BNF_Util.case_fp fp NData NCodata (map (nun_co_data_spec_of_isa ctxt) specs)
  12.178 +      | IVal t => NVal (tm_of_isa ctxt t, ty_of_isa (fastype_of t))
  12.179 +      | ICoPred (fp, wf, specs) =>
  12.180 +        (if wf then curry NPred true
  12.181 +         else if fp = BNF_Util.Least_FP then curry NPred false
  12.182 +         else NCopred) (map (nun_const_spec_of_isa ctxt) specs)
  12.183 +      | IRec specs => NRec (map (nun_rec_spec_of_isa ctxt) specs)
  12.184 +      | ISpec spec => NSpec (nun_consts_spec_of_isa ctxt spec)
  12.185 +      | IAxiom prop => NAxiom (prop_of_isa ctxt prop)
  12.186 +      | IGoal prop => NGoal (prop_of_isa ctxt prop)
  12.187 +      | IEval t => NEval (tm_of_isa ctxt t));
  12.188 +  in
  12.189 +    {commandss = map (map cmd_of) commandss, sound = sound, complete = complete}
  12.190 +  end;
  12.191 +
  12.192 +end;
    13.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    13.2 +++ b/src/HOL/Nunchaku/Tools/nunchaku_util.ML	Mon Oct 24 22:42:07 2016 +0200
    13.3 @@ -0,0 +1,95 @@
    13.4 +(*  Title:      HOL/Nunchaku/Tools/nunchaku_util.ML
    13.5 +    Author:     Jasmin Blanchette, Inria Nancy, LORIA, MPII
    13.6 +    Copyright   2015, 2016
    13.7 +
    13.8 +General-purpose functions used by Nunchaku.
    13.9 +*)
   13.10 +
   13.11 +signature NUNCHAKU_UTIL =
   13.12 +sig
   13.13 +  val elide_string: int -> string -> string
   13.14 +  val nat_subscript: int -> string
   13.15 +  val timestamp: unit -> string
   13.16 +  val parse_bool_option: bool -> string -> string -> bool option
   13.17 +  val parse_time: string -> string -> Time.time
   13.18 +  val string_of_time: Time.time -> string
   13.19 +  val simplify_spaces: string -> string
   13.20 +  val ascii_of: string -> string
   13.21 +  val unascii_of: string -> string
   13.22 +  val double_lookup: ('a * 'a -> bool) -> ('a option * 'b) list -> 'a -> 'b option
   13.23 +  val triple_lookup: (''a * ''a -> bool) -> (''a option * 'b) list -> ''a -> 'b option
   13.24 +  val plural_s_for_list: 'a list -> string
   13.25 +  val with_overlord_file: string -> string -> (Path.T -> 'a) -> 'a
   13.26 +  val with_tmp_or_overlord_file: bool -> string -> string -> (Path.T -> 'a) -> 'a
   13.27 +  val num_binder_types: typ -> int
   13.28 +  val strip_fun_type: typ -> typ list * typ
   13.29 +  val attach_typeS: term -> term
   13.30 +  val specialize_type: theory -> string * typ -> term -> term
   13.31 +  val typ_match: theory -> typ * typ -> bool
   13.32 +  val term_match: theory -> term * term -> bool
   13.33 +  val const_match: theory -> (string * typ) * (string * typ) -> bool
   13.34 +  val DETERM_TIMEOUT: Time.time -> tactic -> tactic
   13.35 +  val spying: bool -> (unit -> Proof.state * int * string) -> unit
   13.36 +end;
   13.37 +
   13.38 +structure Nunchaku_Util : NUNCHAKU_UTIL =
   13.39 +struct
   13.40 +
   13.41 +val elide_string = ATP_Util.elide_string;
   13.42 +val nat_subscript = Nitpick_Util.nat_subscript;
   13.43 +val timestamp = ATP_Util.timestamp;
   13.44 +
   13.45 +val parse_bool_option = Sledgehammer_Util.parse_bool_option;
   13.46 +val parse_time = Sledgehammer_Util.parse_time;
   13.47 +val string_of_time = ATP_Util.string_of_time;
   13.48 +val simplify_spaces = Sledgehammer_Util.simplify_spaces;
   13.49 +val ascii_of = ATP_Problem_Generate.ascii_of;
   13.50 +val unascii_of = ATP_Problem_Generate.unascii_of;
   13.51 +val double_lookup = Nitpick_Util.double_lookup;
   13.52 +val triple_lookup = Nitpick_Util.triple_lookup;
   13.53 +val plural_s_for_list = Nitpick_Util.plural_s_for_list;
   13.54 +
   13.55 +fun with_overlord_file name ext f =
   13.56 +  f (Path.explode ("$ISABELLE_HOME_USER/" ^ name ^ "." ^ ext));
   13.57 +
   13.58 +fun with_tmp_or_overlord_file overlord =
   13.59 +  if overlord then with_overlord_file else Isabelle_System.with_tmp_file;
   13.60 +
   13.61 +val num_binder_types = BNF_Util.num_binder_types
   13.62 +val strip_fun_type = BNF_Util.strip_fun_type;
   13.63 +
   13.64 +(* Clone from "HOL/Tools/inductive_realizer.ML". *)
   13.65 +val attach_typeS =
   13.66 +  map_types (map_atyps
   13.67 +    (fn TFree (s, []) => TFree (s, @{sort type})
   13.68 +      | TVar (ixn, []) => TVar (ixn, @{sort type})
   13.69 +      | T => T));
   13.70 +
   13.71 +val specialize_type = ATP_Util.specialize_type;
   13.72 +
   13.73 +fun typ_match thy TU = can (Sign.typ_match thy TU) Vartab.empty;
   13.74 +fun term_match thy tu = can (Pattern.match thy tu) (Vartab.empty, Vartab.empty);
   13.75 +fun const_match thy = term_match thy o apply2 Const;
   13.76 +
   13.77 +val DETERM_TIMEOUT = Nitpick_Util.DETERM_TIMEOUT;
   13.78 +
   13.79 +val spying_version = "a"
   13.80 +
   13.81 +val hackish_string_of_term = Sledgehammer_Util.hackish_string_of_term;
   13.82 +
   13.83 +fun spying spy f =
   13.84 +  if spy then
   13.85 +    let
   13.86 +      val (state, i, message) = f ();
   13.87 +      val ctxt = Proof.context_of state;
   13.88 +      val goal = Logic.get_goal (Thm.prop_of (#goal (Proof.goal state))) i;
   13.89 +      val hash =
   13.90 +        String.substring (SHA1.rep (SHA1.digest (hackish_string_of_term ctxt goal)), 0, 12);
   13.91 +    in
   13.92 +      File.append (Path.explode "$ISABELLE_HOME_USER/spy_nunchaku")
   13.93 +        (spying_version ^ " " ^ timestamp () ^ ": " ^ hash ^ ": " ^ message ^ "\n")
   13.94 +    end
   13.95 +  else
   13.96 +    ();
   13.97 +
   13.98 +end;
    14.1 --- a/src/HOL/ROOT	Mon Oct 24 21:14:38 2016 +0200
    14.2 +++ b/src/HOL/ROOT	Mon Oct 24 22:42:07 2016 +0200
    14.3 @@ -282,6 +282,16 @@
    14.4    options [document = false]
    14.5    theories [quick_and_dirty] Nitpick_Examples
    14.6  
    14.7 +session "HOL-Nunchaku" in Nunchaku = HOL +
    14.8 +  description {*
    14.9 +    Author:     Jasmin Blanchette, Inria Nancy, LORIA, MPII
   14.10 +    Copyright   2015, 2016
   14.11 +
   14.12 +    Nunchaku: Yet another counterexample generator for Isabelle/HOL.
   14.13 +  *}
   14.14 +  options [document = false]
   14.15 +  theories Nunchaku
   14.16 +
   14.17  session "HOL-Algebra" (main timing) in Algebra = HOL +
   14.18    description {*
   14.19      Author: Clemens Ballarin, started 24 September 1999