--- a/NEWS Mon Nov 08 09:10:44 2010 +0100
+++ b/NEWS Mon Nov 08 13:25:00 2010 +0100
@@ -350,9 +350,10 @@
z3_trace_assms ~> smt_trace_used_facts
INCOMPATIBILITY.
- Added:
+ smt_verbose
+ smt_datatypes
cvc3_options
yices_options
- smt_datatypes
* Removed [split_format ... and ... and ...] version of
[split_format]. Potential INCOMPATIBILITY.
--- a/src/HOL/IsaMakefile Mon Nov 08 09:10:44 2010 +0100
+++ b/src/HOL/IsaMakefile Mon Nov 08 13:25:00 2010 +0100
@@ -270,6 +270,7 @@
Semiring_Normalization.thy \
SetInterval.thy \
Sledgehammer.thy \
+ Smallcheck.thy \
SMT.thy \
String.thy \
Typerep.thy \
@@ -336,8 +337,11 @@
Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML \
Tools/Sledgehammer/sledgehammer_atp_translate.ML \
Tools/Sledgehammer/sledgehammer_util.ML \
+ Tools/smallvalue_generators.ML \
Tools/SMT/smtlib_interface.ML \
Tools/SMT/smt_builtin.ML \
+ Tools/SMT/smt_config.ML \
+ Tools/SMT/smt_failure.ML \
Tools/SMT/smt_monomorph.ML \
Tools/SMT/smt_normalize.ML \
Tools/SMT/smt_setup_solvers.ML \
--- a/src/HOL/Main.thy Mon Nov 08 09:10:44 2010 +0100
+++ b/src/HOL/Main.thy Mon Nov 08 13:25:00 2010 +0100
@@ -1,7 +1,7 @@
header {* Main HOL *}
theory Main
-imports Plain Record Predicate_Compile Nitpick
+imports Plain Record Predicate_Compile Smallcheck Nitpick
begin
text {*
--- a/src/HOL/SMT.thy Mon Nov 08 09:10:44 2010 +0100
+++ b/src/HOL/SMT.thy Mon Nov 08 13:25:00 2010 +0100
@@ -8,7 +8,9 @@
imports List
uses
"Tools/Datatype/datatype_selectors.ML"
- ("Tools/SMT/smt_monomorph.ML")
+ "Tools/SMT/smt_failure.ML"
+ "Tools/SMT/smt_config.ML"
+ "Tools/SMT/smt_monomorph.ML"
("Tools/SMT/smt_builtin.ML")
("Tools/SMT/smt_normalize.ML")
("Tools/SMT/smt_translate.ML")
@@ -126,7 +128,6 @@
subsection {* Setup *}
-use "Tools/SMT/smt_monomorph.ML"
use "Tools/SMT/smt_builtin.ML"
use "Tools/SMT/smt_normalize.ML"
use "Tools/SMT/smt_translate.ML"
@@ -141,6 +142,7 @@
use "Tools/SMT/smt_setup_solvers.ML"
setup {*
+ SMT_Config.setup #>
SMT_Solver.setup #>
Z3_Proof_Reconstruction.setup #>
SMT_Setup_Solvers.setup
@@ -241,6 +243,13 @@
subsection {* Tracing *}
text {*
+The SMT method, when applied, traces important information. To
+make it entirely silent, set the following option to @{text false}.
+*}
+
+declare [[ smt_verbose = true ]]
+
+text {*
For tracing the generated problem file given to the SMT solver as
well as the returned result of the solver, the option
@{text smt_trace} should be set to @{text true}.
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Smallcheck.thy Mon Nov 08 13:25:00 2010 +0100
@@ -0,0 +1,69 @@
+(* Author: Lukas Bulwahn, TU Muenchen *)
+
+header {* Another simple counterexample generator *}
+
+theory Smallcheck
+imports Quickcheck
+uses ("Tools/smallvalue_generators.ML")
+begin
+
+
+section {* small value generator type classes *}
+
+class small = term_of +
+fixes small :: "('a \<Rightarrow> term list option) \<Rightarrow> code_numeral \<Rightarrow> term list option"
+
+instantiation unit :: small
+begin
+
+definition "find_first f d = f ()"
+
+instance ..
+
+end
+
+instantiation int :: small
+begin
+
+function small' :: "(int => term list option) => int => int => term list option"
+where "small' f d i = (if d < i then None else (case f i of Some t => Some t | None => small' f d (i + 1)))"
+by pat_completeness auto
+
+termination
+ by (relation "measure (%(_, d, i). nat (d + 1 - i))") auto
+
+definition "small f d = small' f (Code_Numeral.int_of d) (- (Code_Numeral.int_of d))"
+
+instance ..
+
+end
+
+instantiation prod :: (small, small) small
+begin
+
+definition
+ "small f d = small (%x. small (%y. f (x, y)) d) d"
+
+instance ..
+
+end
+
+section {* Defining combinators for any first-order data type *}
+
+definition catch_match :: "term list option => term list option => term list option"
+where
+ [code del]: "catch_match t1 t2 = (SOME t. t = t1 \<or> t = t2)"
+
+code_const catch_match
+ (SML "(_) handle Match => _")
+
+use "Tools/smallvalue_generators.ML"
+
+(* We do not activate smallcheck yet.
+setup {* Smallvalue_Generators.setup *}
+*)
+
+hide_fact catch_match_def
+hide_const (open) catch_match
+
+end
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/SMT/smt_config.ML Mon Nov 08 13:25:00 2010 +0100
@@ -0,0 +1,232 @@
+(* Title: HOL/Tools/SMT/smt_config.ML
+ Author: Sascha Boehme, TU Muenchen
+
+Configuration options and diagnostic tools for SMT.
+*)
+
+signature SMT_CONFIG =
+sig
+ (*solver*)
+ val add_solver: string -> Context.generic -> Context.generic
+ val set_solver_options: string * string -> Context.generic -> Context.generic
+ val select_solver: string -> Context.generic -> Context.generic
+ val solver_of: Proof.context -> string
+ val solver_options_of: Proof.context -> string list
+
+ (*options*)
+ val oracle: bool Config.T
+ val datatypes: bool Config.T
+ val timeout: real Config.T
+ val fixed: bool Config.T
+ val verbose: bool Config.T
+ val traceN: string
+ val trace: bool Config.T
+ val trace_used_facts: bool Config.T
+ val monomorph_limit: int Config.T
+ val drop_bad_facts: bool Config.T
+ val filter_only_facts: bool Config.T
+
+ (*tools*)
+ val with_timeout: Proof.context -> ('a -> 'b) -> 'a -> 'b
+
+ (*diagnostics*)
+ val trace_msg: Proof.context -> ('a -> string) -> 'a -> unit
+ val verbose_msg: Proof.context -> ('a -> string) -> 'a -> unit
+
+ (*certificates*)
+ val select_certificates: string -> Context.generic -> Context.generic
+ val certificates_of: Proof.context -> Cache_IO.cache option
+
+ (*setup*)
+ val setup: theory -> theory
+ val print_setup: Proof.context -> unit
+end
+
+structure SMT_Config: SMT_CONFIG =
+struct
+
+(* solver *)
+
+structure Solvers = Generic_Data
+(
+ type T = string list Symtab.table * string option
+ val empty = (Symtab.empty, NONE)
+ val extend = I
+ fun merge ((ss1, s), (ss2, _)) = (Symtab.merge (K true) (ss1, ss2), s)
+)
+
+fun set_solver_options (name, options) =
+ let val opts = String.tokens (Symbol.is_ascii_blank o str) options
+ in Solvers.map (apfst (Symtab.map_entry name (K opts))) end
+
+fun add_solver name context =
+ if Symtab.defined (fst (Solvers.get context)) name then
+ error ("Solver already registered: " ^ quote name)
+ else
+ context
+ |> Solvers.map (apfst (Symtab.update (name, [])))
+ |> Context.map_theory (Attrib.setup (Binding.name (name ^ "_options"))
+ (Scan.lift (Parse.$$$ "=" |-- Args.name) >>
+ (Thm.declaration_attribute o K o set_solver_options o pair name))
+ ("Additional command line options for SMT solver " ^ quote name))
+
+fun select_solver name context =
+ if Symtab.defined (fst (Solvers.get context)) name then
+ Solvers.map (apsnd (K (SOME name))) context
+ else error ("Trying to select unknown solver: " ^ quote name)
+
+val lookup_solver = snd o Solvers.get o Context.Proof
+
+fun solver_of ctxt =
+ (case lookup_solver ctxt of
+ SOME name => name
+ | NONE => error "No SMT solver selected")
+
+fun solver_options_of ctxt =
+ (case lookup_solver ctxt of
+ NONE => []
+ | SOME name =>
+ Symtab.lookup_list (fst (Solvers.get (Context.Proof ctxt))) name)
+
+val setup_solver =
+ Attrib.setup @{binding smt_solver}
+ (Scan.lift (Parse.$$$ "=" |-- Args.name) >>
+ (Thm.declaration_attribute o K o select_solver))
+ "SMT solver configuration"
+
+
+(* options *)
+
+val oracleN = "smt_oracle"
+val (oracle, setup_oracle) = Attrib.config_bool oracleN (K true)
+
+val datatypesN = "smt_datatypes"
+val (datatypes, setup_datatypes) = Attrib.config_bool datatypesN (K false)
+
+val timeoutN = "smt_timeout"
+val (timeout, setup_timeout) = Attrib.config_real timeoutN (K 30.0)
+
+val fixedN = "smt_fixed"
+val (fixed, setup_fixed) = Attrib.config_bool fixedN (K false)
+
+val verboseN = "smt_verbose"
+val (verbose, setup_verbose) = Attrib.config_bool verboseN (K true)
+
+val traceN = "smt_trace"
+val (trace, setup_trace) = Attrib.config_bool traceN (K false)
+
+val trace_used_factsN = "smt_trace_used_facts"
+val (trace_used_facts, setup_trace_used_facts) =
+ Attrib.config_bool trace_used_factsN (K false)
+
+val monomorph_limitN = "smt_monomorph_limit"
+val (monomorph_limit, setup_monomorph_limit) =
+ Attrib.config_int monomorph_limitN (K 10)
+
+val drop_bad_factsN = "smt_drop_bad_facts"
+val (drop_bad_facts, setup_drop_bad_facts) =
+ Attrib.config_bool drop_bad_factsN (K false)
+
+val filter_only_factsN = "smt_filter_only_facts"
+val (filter_only_facts, setup_filter_only_facts) =
+ Attrib.config_bool filter_only_factsN (K false)
+
+val setup_options =
+ setup_oracle #>
+ setup_datatypes #>
+ setup_timeout #>
+ setup_fixed #>
+ setup_trace #>
+ setup_verbose #>
+ setup_monomorph_limit #>
+ setup_drop_bad_facts #>
+ setup_filter_only_facts #>
+ setup_trace_used_facts
+
+
+(* diagnostics *)
+
+fun cond_trace flag f x = if flag then tracing ("SMT: " ^ f x) else ()
+
+fun verbose_msg ctxt = cond_trace (Config.get ctxt verbose)
+
+fun trace_msg ctxt = cond_trace (Config.get ctxt trace)
+
+
+(* tools *)
+
+fun with_timeout ctxt f x =
+ TimeLimit.timeLimit (seconds (Config.get ctxt timeout)) f x
+ handle TimeLimit.TimeOut => raise SMT_Failure.SMT SMT_Failure.Time_Out
+
+
+(* certificates *)
+
+structure Certificates = Generic_Data
+(
+ type T = Cache_IO.cache option
+ val empty = NONE
+ val extend = I
+ fun merge (s, _) = s
+)
+
+val get_certificates_path =
+ Option.map (Cache_IO.cache_path_of) o Certificates.get o Context.Proof
+
+fun select_certificates name = Certificates.put (
+ if name = "" then NONE
+ else SOME (Cache_IO.make (Path.explode name)))
+
+val certificates_of = Certificates.get o Context.Proof
+
+val setup_certificates =
+ Attrib.setup @{binding smt_certificates}
+ (Scan.lift (Parse.$$$ "=" |-- Args.name) >>
+ (Thm.declaration_attribute o K o select_certificates))
+ "SMT certificates configuration"
+
+
+(* setup *)
+
+val setup =
+ setup_solver #>
+ setup_options #>
+ setup_certificates
+
+fun print_setup ctxt =
+ let
+ fun string_of_bool b = if b then "true" else "false"
+
+ val (names, sel) = Solvers.get (Context.Proof ctxt) |> apfst Symtab.keys
+ val ns = if null names then ["(none)"] else sort_strings names
+ val n = the_default "(none)" sel
+ val opts = solver_options_of ctxt
+
+ val t = string_of_real (Config.get ctxt timeout)
+
+ val certs_filename =
+ (case get_certificates_path ctxt of
+ SOME path => Path.implode path
+ | NONE => "(disabled)")
+ in
+ Pretty.writeln (Pretty.big_list "SMT setup:" [
+ Pretty.str ("Current SMT solver: " ^ n),
+ Pretty.str ("Current SMT solver options: " ^ space_implode " " opts),
+ Pretty.str_list "Available SMT solvers: " "" ns,
+ Pretty.str ("Current timeout: " ^ t ^ " seconds"),
+ Pretty.str ("With proofs: " ^
+ string_of_bool (not (Config.get ctxt oracle))),
+ Pretty.str ("Certificates cache: " ^ certs_filename),
+ Pretty.str ("Fixed certificates: " ^
+ string_of_bool (Config.get ctxt fixed))])
+ end
+
+val _ =
+ Outer_Syntax.improper_command "smt_status"
+ ("show the available SMT solvers, the currently selected SMT solver, " ^
+ "and the values of SMT configuration options")
+ Keyword.diag
+ (Scan.succeed (Toplevel.no_timing o Toplevel.keep (fn state =>
+ print_setup (Toplevel.context_of state))))
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/SMT/smt_failure.ML Mon Nov 08 13:25:00 2010 +0100
@@ -0,0 +1,41 @@
+(* Title: HOL/Tools/SMT/smt_failure.ML
+ Author: Sascha Boehme, TU Muenchen
+
+Failures and exception of SMT.
+*)
+
+signature SMT_FAILURE =
+sig
+ datatype failure =
+ Counterexample of bool * term list |
+ Time_Out |
+ Out_Of_Memory |
+ Other_Failure of string
+ val string_of_failure: Proof.context -> failure -> string
+ exception SMT of failure
+end
+
+structure SMT_Failure: SMT_FAILURE =
+struct
+
+datatype failure =
+ Counterexample of bool * term list |
+ Time_Out |
+ Out_Of_Memory |
+ Other_Failure of string
+
+fun string_of_failure ctxt (Counterexample (real, ex)) =
+ let
+ val msg = (if real then "C" else "Potential c") ^ "ounterexample found"
+ in
+ if null ex then msg
+ else Pretty.string_of (Pretty.big_list (msg ^ ":")
+ (map (Syntax.pretty_term ctxt) ex))
+ end
+ | string_of_failure _ Time_Out = "Timed out"
+ | string_of_failure _ Out_Of_Memory = "Ran out of memory"
+ | string_of_failure _ (Other_Failure msg) = msg
+
+exception SMT of failure
+
+end
--- a/src/HOL/Tools/SMT/smt_monomorph.ML Mon Nov 08 09:10:44 2010 +0100
+++ b/src/HOL/Tools/SMT/smt_monomorph.ML Mon Nov 08 13:25:00 2010 +0100
@@ -92,16 +92,19 @@
computation uses only the constants occurring with schematic type
variables in the propositions. To ease comparisons, such sets of
costants are always kept in their initial order. *)
-fun incremental_monomorph thy limit all_grounds new_grounds irules =
+fun incremental_monomorph ctxt limit all_grounds new_grounds irules =
let
+ val thy = ProofContext.theory_of ctxt
val all_grounds' = Symtab.merge_list (op =) (all_grounds, new_grounds)
val spec = specialize thy all_grounds' new_grounds
val (irs, new_grounds') = fold_map spec irules Symtab.empty
in
if Symtab.is_empty new_grounds' then irs
else if limit > 0
- then incremental_monomorph thy (limit-1) all_grounds' new_grounds' irs
- else (warning "SMT: monomorphization limit reached"; irs)
+ then incremental_monomorph ctxt (limit-1) all_grounds' new_grounds' irs
+ else
+ (SMT_Config.verbose_msg ctxt (K "Warning: Monomorphization limit reached")
+ (); irs)
end
@@ -175,7 +178,7 @@
in
polys
|> map (fn (i, thm) => ((i, thm), [(Vartab.empty, tvar_consts_of thm)]))
- |> incremental_monomorph thy limit Symtab.empty grounds
+ |> incremental_monomorph ctxt' limit Symtab.empty grounds
|> map (apsnd (filter_most_specific thy))
|> flat o map2 (instantiate thy) Tenvs
|> append monos
@@ -183,9 +186,6 @@
end
-val monomorph_limit = 10
-
-
(* Instantiate all polymorphic constants (i.e., constants occurring
both with ground types and type variables) with all (necessary)
ground types; thereby create copies of theorems containing those
@@ -199,6 +199,6 @@
irules
|> List.partition (Term.exists_type typ_has_tvars o Thm.prop_of o snd)
|>> incr_indexes
- |-> mono_all ctxt monomorph_limit
+ |-> mono_all ctxt (Config.get ctxt SMT_Config.monomorph_limit)
end
--- a/src/HOL/Tools/SMT/smt_normalize.ML Mon Nov 08 09:10:44 2010 +0100
+++ b/src/HOL/Tools/SMT/smt_normalize.ML Mon Nov 08 13:25:00 2010 +0100
@@ -19,8 +19,7 @@
sig
type extra_norm = bool -> (int * thm) list -> Proof.context ->
(int * thm) list * Proof.context
- val normalize: (Proof.context -> (thm -> string) -> thm -> unit) -> bool ->
- extra_norm -> bool -> (int * thm) list -> Proof.context ->
+ val normalize: extra_norm -> bool -> (int * thm) list -> Proof.context ->
(int * thm) list * Proof.context
val atomize_conv: Proof.context -> conv
val eta_expand_conv: (Proof.context -> conv) -> Proof.context -> conv
@@ -247,7 +246,7 @@
then eta_args_conv norm_conv
(length (Term.binder_types T) - length ts)
else args_conv o norm_conv
- | (_, ts) => args_conv o norm_conv)) ctxt ct
+ | _ => args_conv o norm_conv)) ctxt ct
fun is_normed ctxt t =
(case t of
@@ -516,15 +515,15 @@
fun with_context f irules ctxt = (f ctxt irules, ctxt)
-fun normalize trace keep_assms extra_norm with_datatypes irules ctxt =
+fun normalize extra_norm with_datatypes irules ctxt =
let
fun norm f ctxt' (i, thm) =
- if keep_assms then SOME (i, f ctxt' thm)
- else
+ if Config.get ctxt' SMT_Config.drop_bad_facts then
(case try (f ctxt') thm of
SOME thm' => SOME (i, thm')
- | NONE => (trace ctxt' (prefix ("SMT warning: " ^
+ | NONE => (SMT_Config.verbose_msg ctxt' (prefix ("Warning: " ^
"dropping assumption: ") o Display.string_of_thm ctxt') thm; NONE))
+ else SOME (i, f ctxt' thm)
in
irules
|> trivial_distinct ctxt
--- a/src/HOL/Tools/SMT/smt_setup_solvers.ML Mon Nov 08 09:10:44 2010 +0100
+++ b/src/HOL/Tools/SMT/smt_setup_solvers.ML Mon Nov 08 13:25:00 2010 +0100
@@ -16,9 +16,9 @@
if String.isPrefix unsat line then SMT_Solver.Unsat
else if String.isPrefix sat line then SMT_Solver.Sat
else if String.isPrefix unknown line then SMT_Solver.Unknown
- else raise SMT_Solver.SMT (SMT_Solver.Other_Failure ("Solver " ^
+ else raise SMT_Failure.SMT (SMT_Failure.Other_Failure ("Solver " ^
quote solver_name ^ " failed. Enable SMT tracing by setting the " ^
- "configuration option " ^ quote SMT_Solver.traceN ^ " and " ^
+ "configuration option " ^ quote SMT_Config.traceN ^ " and " ^
" see the trace for details."))
fun on_first_line test_outcome solver_name lines =
@@ -60,14 +60,14 @@
fun z3_options ctxt =
["MODEL=true", "PRE_SIMPLIFY_EXPR=false", "CONTEXT_SIMPLIFIER=false", "-smt"]
- |> not (Config.get ctxt SMT_Solver.oracle) ?
+ |> not (Config.get ctxt SMT_Config.oracle) ?
append ["DISPLAY_PROOF=true","PROOF_MODE=2"]
fun z3_on_last_line solver_name lines =
let
fun junk l =
if String.isPrefix "WARNING: Out of allocated virtual memory" l
- then raise SMT_Solver.SMT SMT_Solver.Out_Of_Memory
+ then raise SMT_Failure.SMT SMT_Failure.Out_Of_Memory
else
String.isPrefix "WARNING" l orelse
String.isPrefix "ERROR" l orelse
--- a/src/HOL/Tools/SMT/smt_solver.ML Mon Nov 08 09:10:44 2010 +0100
+++ b/src/HOL/Tools/SMT/smt_solver.ML Mon Nov 08 13:25:00 2010 +0100
@@ -6,14 +6,7 @@
signature SMT_SOLVER =
sig
- datatype failure =
- Counterexample of bool * term list |
- Time_Out |
- Out_Of_Memory |
- Other_Failure of string
- val string_of_failure: Proof.context -> string -> failure -> string
- exception SMT of failure
-
+ (*configuration*)
type interface = {
extra_norm: SMT_Normalize.extra_norm,
translate: SMT_Translate.config }
@@ -30,37 +23,16 @@
reconstruct: (Proof.context -> SMT_Translate.recon -> string list ->
(int list * thm) * Proof.context) option }
- (*options*)
- val oracle: bool Config.T
- val filter_only: bool Config.T
- val datatypes: bool Config.T
- val keep_assms: bool Config.T
- val timeout: real Config.T
- val with_timeout: Proof.context -> ('a -> 'b) -> 'a -> 'b
- val traceN: string
- val trace: bool Config.T
- val trace_msg: Proof.context -> ('a -> string) -> 'a -> unit
- val trace_used_facts: bool Config.T
-
- (*certificates*)
- val fixed_certificates: bool Config.T
- val select_certificates: string -> Context.generic -> Context.generic
-
- (*solvers*)
+ (*registry*)
type solver = bool option -> Proof.context -> (int * thm) list ->
int list * thm
val add_solver: solver_config -> theory -> theory
- val set_solver_options: string -> string -> Context.generic ->
- Context.generic
- val all_solver_names_of: Context.generic -> string list
- val solver_name_of: Context.generic -> string
- val select_solver: string -> Context.generic -> Context.generic
- val solver_of: Context.generic -> solver
+ val solver_of: Proof.context -> solver
val is_locally_installed: Proof.context -> bool
(*filter*)
val smt_filter: bool -> Time.time -> Proof.state -> ('a * thm) list -> int ->
- {outcome: failure option, used_facts: 'a list,
+ {outcome: SMT_Failure.failure option, used_facts: 'a list,
run_time_in_msecs: int option}
(*tactic*)
@@ -69,31 +41,15 @@
(*setup*)
val setup: theory -> theory
- val print_setup: Context.generic -> unit
end
structure SMT_Solver: SMT_SOLVER =
struct
-datatype failure =
- Counterexample of bool * term list |
- Time_Out |
- Out_Of_Memory |
- Other_Failure of string
+structure C = SMT_Config
-fun string_of_failure ctxt _ (Counterexample (real, ex)) =
- let
- val msg = (if real then "C" else "Potential c") ^ "ounterexample found"
- in
- if null ex then msg ^ "."
- else Pretty.string_of (Pretty.big_list (msg ^ ":")
- (map (Syntax.pretty_term ctxt) ex))
- end
- | string_of_failure _ name Time_Out = name ^ " timed out."
- | string_of_failure _ name Out_Of_Memory = name ^ " ran out of memory."
- | string_of_failure _ _ (Other_Failure msg) = msg
-exception SMT of failure
+(* configuration *)
type interface = {
extra_norm: SMT_Normalize.extra_norm,
@@ -114,57 +70,6 @@
(int list * thm) * Proof.context) option }
-
-(* SMT options *)
-
-val (oracle, setup_oracle) = Attrib.config_bool "smt_oracle" (K true)
-
-val (filter_only, setup_filter_only) =
- Attrib.config_bool "smt_filter_only" (K false)
-
-val (datatypes, setup_datatypes) = Attrib.config_bool "smt_datatypes" (K false)
-
-val (keep_assms, setup_keep_assms) =
- Attrib.config_bool "smt_keep_assms" (K true)
-
-val (timeout, setup_timeout) = Attrib.config_real "smt_timeout" (K 30.0)
-
-fun with_timeout ctxt f x =
- TimeLimit.timeLimit (seconds (Config.get ctxt timeout)) f x
- handle TimeLimit.TimeOut => raise SMT Time_Out
-
-val traceN = "smt_trace"
-val (trace, setup_trace) = Attrib.config_bool traceN (K false)
-
-fun trace_msg ctxt f x =
- if Config.get ctxt trace then tracing (f x) else ()
-
-val (trace_used_facts, setup_trace_used_facts) =
- Attrib.config_bool "smt_trace_used_facts" (K false)
-
-
-(* SMT certificates *)
-
-val (fixed_certificates, setup_fixed_certificates) =
- Attrib.config_bool "smt_fixed" (K false)
-
-structure Certificates = Generic_Data
-(
- type T = Cache_IO.cache option
- val empty = NONE
- val extend = I
- fun merge (s, _) = s
-)
-
-val get_certificates_path =
- Option.map (Cache_IO.cache_path_of) o Certificates.get
-
-fun select_certificates name = Certificates.put (
- if name = "" then NONE
- else SOME (Cache_IO.make (Path.explode name)))
-
-
-
(* interface to external solvers *)
fun get_local_solver env_var =
@@ -202,12 +107,16 @@
[File.shell_path problem_path, "2>&1", ">", File.shell_path proof_path])
fun run ctxt cmd args input =
- (case Certificates.get (Context.Proof ctxt) of
- NONE => Cache_IO.run (make_cmd (choose cmd) args) input
+ (case C.certificates_of ctxt of
+ NONE =>
+ let
+ val {output, redirected_output, ...} =
+ Cache_IO.run (make_cmd (choose cmd) args) input
+ in (redirected_output, output) end
| SOME certs =>
(case Cache_IO.lookup certs input of
(NONE, key) =>
- if Config.get ctxt fixed_certificates
+ if Config.get ctxt C.fixed
then error ("Bad certificates cache: missing certificate")
else Cache_IO.run_and_cache certs key (make_cmd (choose cmd) args)
input
@@ -223,36 +132,37 @@
fun pretty tag ls = Pretty.string_of (Pretty.big_list tag
(map Pretty.str ls))
- val _ = trace_msg ctxt (pretty "SMT problem:" o split_lines) input
+ val _ = C.trace_msg ctxt (pretty "Problem:" o split_lines) input
- val (res, err) = with_timeout ctxt (run ctxt cmd args) input
- val _ = trace_msg ctxt (pretty "SMT solver:") err
+ val (res, err) = C.with_timeout ctxt (run ctxt cmd args) input
+ val _ = C.trace_msg ctxt (pretty "Solver:") err
val ls = rev (snd (chop_while (equal "") (rev res)))
- val _ = trace_msg ctxt (pretty "SMT result:") ls
+ val _ = C.trace_msg ctxt (pretty "Result:") ls
in ls end
end
-fun trace_assms ctxt = trace_msg ctxt (Pretty.string_of o
- Pretty.big_list "SMT assertions:" o map (Display.pretty_thm ctxt o snd))
+fun trace_assms ctxt = C.trace_msg ctxt (Pretty.string_of o
+ Pretty.big_list "Assertions:" o map (Display.pretty_thm ctxt o snd))
fun trace_recon_data ctxt ({typs, terms, ...} : SMT_Translate.recon) =
let
fun pretty_eq n p = Pretty.block [Pretty.str n, Pretty.str " = ", p]
- fun pretty_typ (n, T) = pretty_eq n (Syntax.pretty_typ ctxt T)
- fun pretty_term (n, t) = pretty_eq n (Syntax.pretty_term ctxt t)
+ fun p_typ (n, T) = pretty_eq n (Syntax.pretty_typ ctxt T)
+ fun p_term (n, t) = pretty_eq n (Syntax.pretty_term ctxt t)
in
- trace_msg ctxt (fn () => Pretty.string_of (Pretty.big_list "SMT names:" [
- Pretty.big_list "sorts:" (map pretty_typ (Symtab.dest typs)),
- Pretty.big_list "functions:" (map pretty_term (Symtab.dest terms))])) ()
+ C.trace_msg ctxt (fn () =>
+ Pretty.string_of (Pretty.big_list "Names:" [
+ Pretty.big_list "sorts:" (map p_typ (Symtab.dest typs)),
+ Pretty.big_list "functions:" (map p_term (Symtab.dest terms))])) ()
end
-fun invoke translate_config name cmd more_opts options irules ctxt =
+fun invoke translate_config name cmd options irules ctxt =
let
- val args = more_opts @ options ctxt
+ val args = C.solver_options_of ctxt @ options ctxt
val comments = ("solver: " ^ name) ::
- ("timeout: " ^ Time.toString (seconds (Config.get ctxt timeout))) ::
+ ("timeout: " ^ Time.toString (seconds (Config.get ctxt C.timeout))) ::
"arguments:" :: args
in
irules
@@ -283,7 +193,7 @@
val thms = filter (fn i => i >= 0) idxs
|> map_filter (AList.lookup (op =) irules)
in
- if Config.get ctxt trace_used_facts andalso length thms > 0
+ if Config.get ctxt C.trace_used_facts andalso length thms > 0
then
tracing (Pretty.string_of (Pretty.big_list "SMT used facts:"
(map (Display.pretty_thm ctxt) thms)))
@@ -292,17 +202,15 @@
fun gen_solver name info rm ctxt irules =
let
- val {env_var, is_remote, options, more_options, interface, reconstruct} =
- info
+ val {env_var, is_remote, options, interface, reconstruct} = info
val {extra_norm, translate} = interface
val (with_datatypes, translate') =
- set_has_datatypes (Config.get ctxt datatypes) translate
+ set_has_datatypes (Config.get ctxt C.datatypes) translate
val cmd = (rm, env_var, is_remote, name)
- val keep = Config.get ctxt keep_assms
in
(irules, ctxt)
- |-> SMT_Normalize.normalize trace_msg keep extra_norm with_datatypes
- |-> invoke translate' name cmd more_options options
+ |-> SMT_Normalize.normalize extra_norm with_datatypes
+ |-> invoke translate' name cmd options
|-> reconstruct
|-> (fn (idxs, thm) => fn ctxt' => thm
|> singleton (ProofContext.export ctxt' ctxt)
@@ -313,7 +221,7 @@
-(* solver store *)
+(* registry *)
type solver = bool option -> Proof.context -> (int * thm) list -> int list * thm
@@ -321,7 +229,6 @@
env_var: string,
is_remote: bool,
options: Proof.context -> string list,
- more_options: string list,
interface: interface,
reconstruct: string list * SMT_Translate.recon -> Proof.context ->
(int list * thm) * Proof.context }
@@ -335,24 +242,18 @@
handle Symtab.DUP name => error ("Duplicate SMT solver: " ^ quote name)
)
-val no_solver = "(none)"
-
-fun set_solver_options name opts = Solvers.map (Symtab.map_entry name (fn
- {env_var, is_remote, options, interface, reconstruct, ...} =>
- {env_var=env_var, is_remote=is_remote, options=options,
- more_options=String.tokens (Symbol.is_ascii_blank o str) opts,
- interface=interface, reconstruct=reconstruct}))
-
local
fun finish outcome cex_parser reconstruct ocl (output, recon) ctxt =
(case outcome output of
(Unsat, ls) =>
- if not (Config.get ctxt oracle) andalso is_some reconstruct
+ if not (Config.get ctxt C.oracle) andalso is_some reconstruct
then the reconstruct ctxt recon ls
else (([], ocl ()), ctxt)
| (result, ls) =>
let val ts = (case cex_parser of SOME f => f ctxt recon ls | _ => [])
- in raise SMT (Counterexample (result = Sat, ts)) end)
+ in
+ raise SMT_Failure.SMT (SMT_Failure.Counterexample (result = Sat, ts))
+ end)
in
fun add_solver cfg =
@@ -363,59 +264,31 @@
fun core_oracle () = @{cprop False}
fun solver ocl = { env_var=env_var, is_remote=is_remote, options=options,
- more_options=[], interface=interface,
+ interface=interface,
reconstruct=finish (outcome name) cex_parser reconstruct ocl }
in
Thm.add_oracle (Binding.name name, core_oracle) #-> (fn (_, ocl) =>
Context.theory_map (Solvers.map (Symtab.update_new (name, solver ocl)))) #>
- Attrib.setup (Binding.name (name ^ "_options"))
- (Scan.lift (Parse.$$$ "=" |-- Args.name) >>
- (Thm.declaration_attribute o K o set_solver_options name))
- ("Additional command line options for SMT solver " ^ quote name)
+ Context.theory_map (C.add_solver name)
end
end
-val all_solver_names_of = Symtab.keys o Solvers.get
-val lookup_solver = Symtab.lookup o Solvers.get
-
-
-
-(* selected solver *)
-
-structure Selected_Solver = Generic_Data
-(
- type T = string
- val empty = no_solver
- val extend = I
- fun merge (s, _) = s
-)
+fun name_and_solver_of ctxt =
+ let val name = C.solver_of ctxt
+ in (name, the (Symtab.lookup (Solvers.get (Context.Proof ctxt)) name)) end
-val solver_name_of = Selected_Solver.get
-
-fun select_solver name context =
- if is_none (lookup_solver context name)
- then error ("SMT solver not registered: " ^ quote name)
- else Selected_Solver.map (K name) context
-
-fun raw_solver_of context name =
- (case lookup_solver context name of
- NONE => error "No SMT solver selected"
- | SOME s => s)
-
-fun solver_of context =
- let val name = solver_name_of context
- in gen_solver name (raw_solver_of context name) end
+fun solver_of ctxt =
+ let val (name, raw_solver) = name_and_solver_of ctxt
+ in gen_solver name raw_solver end
fun is_locally_installed ctxt =
- let
- val name = solver_name_of (Context.Proof ctxt)
- val {env_var, ...} = raw_solver_of (Context.Proof ctxt) name
+ let val (_, {env_var, ...}) = name_and_solver_of ctxt
in is_some (get_local_solver env_var) end
-(* SMT filter *)
+(* filter *)
val has_topsort = Term.exists_type (Term.exists_subtype (fn
TFree (_, []) => true
@@ -424,19 +297,20 @@
fun smt_solver rm ctxt irules =
(* without this test, we would run into problems when atomizing the rules: *)
- if exists (has_topsort o Thm.prop_of o snd) irules
- then raise SMT (Other_Failure "proof state contains the universal sort {}")
- else solver_of (Context.Proof ctxt) rm ctxt irules
+ if exists (has_topsort o Thm.prop_of o snd) irules then
+ raise SMT_Failure.SMT (SMT_Failure.Other_Failure ("proof state " ^
+ "contains the universal sort {}"))
+ else solver_of ctxt rm ctxt irules
fun smt_filter run_remote time_limit st xrules i =
let
val {facts, goal, ...} = Proof.goal st
val ctxt =
Proof.context_of st
- |> Config.put timeout (Real.fromInt (Time.toSeconds time_limit))
- |> Config.put oracle false
- |> Config.put filter_only true
- |> Config.put keep_assms false
+ |> Config.put C.oracle false
+ |> Config.put C.timeout (Real.fromInt (Time.toSeconds time_limit))
+ |> Config.put C.drop_bad_facts true
+ |> Config.put C.filter_only_facts true
val ({context=ctxt', prems, concl, ...}, _) = Subgoal.focus ctxt i goal
val cprop =
concl
@@ -450,7 +324,8 @@
|-> map_filter o try o nth
|> (fn xs => {outcome=NONE, used_facts=xs, run_time_in_msecs=NONE})
end
- handle SMT fail => {outcome=SOME fail, used_facts=[], run_time_in_msecs=NONE}
+ handle SMT_Failure.SMT fail => {outcome=SOME fail, used_facts=[],
+ run_time_in_msecs=NONE}
(* FIXME: measure runtime *)
@@ -460,14 +335,17 @@
fun smt_tac' pass_exns ctxt rules =
CONVERSION (SMT_Normalize.atomize_conv ctxt)
THEN' Tactic.rtac @{thm ccontr}
- THEN' SUBPROOF (fn {context=cx, prems, ...} =>
+ THEN' SUBPROOF (fn {context=ctxt', prems, ...} =>
let
- fun solve () = snd (smt_solver NONE cx (map (pair ~1) (rules @ prems)))
- val name = solver_name_of (Context.Proof cx)
- val trace = trace_msg cx (prefix "SMT: " o string_of_failure cx name)
+ fun solve irules = snd (smt_solver NONE ctxt' irules)
+ val tag = "Solver " ^ C.solver_of ctxt' ^ ": "
+ val str_of = SMT_Failure.string_of_failure ctxt'
+ fun safe_solve irules =
+ if pass_exns then SOME (solve irules)
+ else (SOME (solve irules) handle SMT_Failure.SMT fail =>
+ (C.trace_msg ctxt' (prefix tag o str_of) fail; NONE))
in
- (if pass_exns then SOME (solve ())
- else (SOME (solve ()) handle SMT fail => (trace fail; NONE)))
+ safe_solve (map (pair ~1) (rules @ prems))
|> (fn SOME thm => Tactic.rtac thm 1 | _ => Tactical.no_tac)
end) ctxt
@@ -483,60 +361,7 @@
(* setup *)
val setup =
- Attrib.setup @{binding smt_solver}
- (Scan.lift (Parse.$$$ "=" |-- Args.name) >>
- (Thm.declaration_attribute o K o select_solver))
- "SMT solver configuration" #>
- setup_oracle #>
- setup_filter_only #>
- setup_datatypes #>
- setup_keep_assms #>
- setup_timeout #>
- setup_trace #>
- setup_trace_used_facts #>
- setup_fixed_certificates #>
- Attrib.setup @{binding smt_certificates}
- (Scan.lift (Parse.$$$ "=" |-- Args.name) >>
- (Thm.declaration_attribute o K o select_certificates))
- "SMT certificates" #>
Method.setup @{binding smt} smt_method
"Applies an SMT solver to the current goal."
-
-fun print_setup context =
- let
- val t = Time.toString (seconds (Config.get_generic context timeout))
- val names = sort_strings (all_solver_names_of context)
- val ns = if null names then [no_solver] else names
- val n = solver_name_of context
- val opts =
- (case Symtab.lookup (Solvers.get context) n of
- NONE => []
- | SOME {more_options, options, ...} =>
- more_options @ options (Context.proof_of context))
- val certs_filename =
- (case get_certificates_path context of
- SOME path => Path.implode path
- | NONE => "(disabled)")
- val fixed = if Config.get_generic context fixed_certificates then "true"
- else "false"
- in
- Pretty.writeln (Pretty.big_list "SMT setup:" [
- Pretty.str ("Current SMT solver: " ^ n),
- Pretty.str ("Current SMT solver options: " ^ space_implode " " opts),
- Pretty.str_list "Available SMT solvers: " "" ns,
- Pretty.str ("Current timeout: " ^ t ^ " seconds"),
- Pretty.str ("With proofs: " ^
- (if Config.get_generic context oracle then "false" else "true")),
- Pretty.str ("Certificates cache: " ^ certs_filename),
- Pretty.str ("Fixed certificates: " ^ fixed)])
- end
-
-val _ =
- Outer_Syntax.improper_command "smt_status"
- "show the available SMT solvers and the currently selected solver"
- Keyword.diag
- (Scan.succeed (Toplevel.no_timing o Toplevel.keep (fn state =>
- print_setup (Context.Proof (Toplevel.context_of state)))))
-
end
--- a/src/HOL/Tools/SMT/z3_proof_parser.ML Mon Nov 08 09:10:44 2010 +0100
+++ b/src/HOL/Tools/SMT/z3_proof_parser.ML Mon Nov 08 13:25:00 2010 +0100
@@ -240,7 +240,7 @@
(* core parser *)
-fun parse_exn line_no msg = raise SMT_Solver.SMT (SMT_Solver.Other_Failure
+fun parse_exn line_no msg = raise SMT_Failure.SMT (SMT_Failure.Other_Failure
("Z3 proof parser (line " ^ string_of_int line_no ^ "): " ^ msg))
fun scan_exn msg ((line_no, _), _) = parse_exn line_no msg
--- a/src/HOL/Tools/SMT/z3_proof_reconstruction.ML Mon Nov 08 09:10:44 2010 +0100
+++ b/src/HOL/Tools/SMT/z3_proof_reconstruction.ML Mon Nov 08 13:25:00 2010 +0100
@@ -19,7 +19,7 @@
structure T = Z3_Proof_Tools
structure L = Z3_Proof_Literals
-fun z3_exn msg = raise SMT_Solver.SMT (SMT_Solver.Other_Failure
+fun z3_exn msg = raise SMT_Failure.SMT (SMT_Failure.Other_Failure
("Z3 proof reconstruction: " ^ msg))
@@ -66,11 +66,11 @@
(** proof tools **)
fun named ctxt name prover ct =
- let val _ = SMT_Solver.trace_msg ctxt I ("Z3: trying " ^ name ^ " ...")
+ let val _ = SMT_Config.trace_msg ctxt I ("Z3: trying " ^ name ^ " ...")
in prover ct end
fun NAMED ctxt name tac i st =
- let val _ = SMT_Solver.trace_msg ctxt I ("Z3: trying " ^ name ^ " ...")
+ let val _ = SMT_Config.trace_msg ctxt I ("Z3: trying " ^ name ^ " ...")
in tac i st end
fun pretty_goal ctxt thms t =
@@ -90,7 +90,7 @@
fun apply [] ct = error (try_apply_err ct)
| apply (prover :: provers) ct =
(case try prover ct of
- SOME thm => (SMT_Solver.trace_msg ctxt I "Z3: succeeded"; thm)
+ SOME thm => (SMT_Config.trace_msg ctxt I "Z3: succeeded"; thm)
| NONE => apply provers ct)
in apply o cons (named ctxt "schematic rules" (by_schematic_rule ctxt)) end
@@ -732,9 +732,9 @@
in
fun trace_rule idx prove r ps ct (cxp as (ctxt, ptab)) =
let
- val _ = SMT_Solver.trace_msg ctxt (header idx r o count_rules) ptab
+ val _ = SMT_Config.trace_msg ctxt (header idx r o count_rules) ptab
val result as (p, (ctxt', _)) = prove r ps ct cxp
- val _ = if not (Config.get ctxt' SMT_Solver.trace) then ()
+ val _ = if not (Config.get ctxt' SMT_Config.trace) then ()
else check ctxt' idx r ps ct p
in result end
end
@@ -844,7 +844,7 @@
val (idx, (ptab, vars, cx)) = P.parse ctxt typs terms output
val assms' = prepare_assms cx unfolds assms
in
- if Config.get cx SMT_Solver.filter_only
+ if Config.get cx SMT_Config.filter_only_facts
then ((filter_assms cx assms' ptab idx [], @{thm TrueI}), cx)
else apfst (pair []) (prove cx assms' vars idx ptab)
end
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Mon Nov 08 09:10:44 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Mon Nov 08 13:25:00 2010 +0100
@@ -409,9 +409,9 @@
run_time_in_msecs = msecs}
end
-fun failure_from_smt_failure (SMT_Solver.Counterexample _) = Unprovable
- | failure_from_smt_failure SMT_Solver.Time_Out = TimedOut
- | failure_from_smt_failure SMT_Solver.Out_Of_Memory = OutOfResources
+fun failure_from_smt_failure (SMT_Failure.Counterexample _) = Unprovable
+ | failure_from_smt_failure SMT_Failure.Time_Out = TimedOut
+ | failure_from_smt_failure SMT_Failure.Out_Of_Memory = OutOfResources
| failure_from_smt_failure _ = UnknownError
val smt_max_iter = 5
@@ -473,10 +473,10 @@
(apply_on_subgoal subgoal subgoal_count ^
command_call smtN (map fst used_facts)) ^
minimize_line minimize_command (map fst used_facts)
- | SOME SMT_Solver.Time_Out => "Timed out."
- | SOME (SMT_Solver.Counterexample _) => "The SMT problem is unprovable."
+ | SOME SMT_Failure.Time_Out => "Timed out."
+ | SOME (SMT_Failure.Counterexample _) => "The SMT problem is unprovable."
| SOME failure =>
- SMT_Solver.string_of_failure ctxt "The SMT solver" failure
+ SMT_Failure.string_of_failure ctxt failure
val outcome = outcome |> Option.map failure_from_smt_failure (* FIXME *)
in
{outcome = outcome, used_facts = used_facts,
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/smallvalue_generators.ML Mon Nov 08 13:25:00 2010 +0100
@@ -0,0 +1,249 @@
+(* Title: HOL/Tools/smallvalue_generators.ML
+ Author: Lukas Bulwahn, TU Muenchen
+
+Generators for small values for various types.
+*)
+
+signature SMALLVALUE_GENERATORS =
+sig
+ val ensure_smallvalue_datatype: Datatype.config -> string list -> theory -> theory
+ val compile_generator_expr:
+ Proof.context -> term -> int -> term list option * (bool list * bool)
+ val put_counterexample: (unit -> int -> term list option)
+ -> Proof.context -> Proof.context
+ val setup: theory -> theory
+end;
+
+structure Smallvalue_Generators : SMALLVALUE_GENERATORS =
+struct
+
+(** general term functions **)
+
+fun dest_funT (Type ("fun",[S, T])) = (S, T)
+ | dest_funT T = raise TYPE ("dest_funT", [T], [])
+
+fun mk_fun_comp (t, u) =
+ let
+ val (_, B) = dest_funT (fastype_of t)
+ val (C, A) = dest_funT (fastype_of u)
+ in
+ Const(@{const_name "Fun.comp"}, (A --> B) --> (C --> A) --> C --> B) $ t $ u
+ end;
+
+fun mk_measure f =
+ let
+ val Type ("fun", [T, @{typ nat}]) = fastype_of f
+ in
+ Const (@{const_name Wellfounded.measure},
+ (T --> @{typ nat}) --> HOLogic.mk_prodT (T, T) --> @{typ bool})
+ $ f
+ end
+
+fun mk_sumcases rT f (Type (@{type_name Sum_Type.sum}, [TL, TR])) =
+ let
+ val lt = mk_sumcases rT f TL
+ val rt = mk_sumcases rT f TR
+ in
+ SumTree.mk_sumcase TL TR rT lt rt
+ end
+ | mk_sumcases _ f T = f T
+
+
+(** abstract syntax **)
+
+val size = @{term "i :: code_numeral"}
+val size_pred = @{term "(i :: code_numeral) - 1"}
+val size_ge_zero = @{term "(i :: code_numeral) > 0"}
+fun test_function T = Free ("f", T --> @{typ "term list option"})
+
+fun mk_none_continuation (x, y) =
+ let
+ val (T as Type(@{type_name "option"}, [T'])) = fastype_of x
+ in
+ Const (@{const_name Option.option_case}, T --> (T' --> T) --> T --> T)
+ $ y $ Const (@{const_name Some}, T' --> T) $ x
+ end
+
+(** datatypes **)
+
+(* constructing smallvalue generator instances on datatypes *)
+
+exception FUNCTION_TYPE;
+
+val smallN = "small";
+
+fun smallT T = (T --> @{typ "Code_Evaluation.term list option"}) --> @{typ code_numeral}
+ --> @{typ "Code_Evaluation.term list option"}
+
+fun mk_equations thy descr vs tycos (names, auxnames) (Ts, Us) =
+ let
+ val smallsN = map (prefix (smallN ^ "_")) (names @ auxnames);
+ val smalls = map2 (fn name => fn T => Free (name, smallT T))
+ smallsN (Ts @ Us)
+ fun mk_small_call T =
+ let
+ val small = Const (@{const_name "Smallcheck.small_class.small"}, smallT T)
+ in
+ (T, (fn t => small $ absdummy (T, t) $ size_pred))
+ end
+ fun mk_small_aux_call fTs (k, _) (tyco, Ts) =
+ let
+ val T = Type (tyco, Ts)
+ val _ = if not (null fTs) then raise FUNCTION_TYPE else ()
+ val small = nth smalls k
+ in
+ (T, (fn t => small $ absdummy (T, t) $ size_pred))
+ end
+ fun mk_consexpr simpleT (c, xs) =
+ let
+ val (Ts, fns) = split_list xs
+ val constr = Const (c, Ts ---> simpleT)
+ val bounds = map Bound (((length xs) - 1) downto 0)
+ val start_term = test_function simpleT $ (list_comb (constr, bounds))
+ in fold_rev (fn f => fn t => f t) fns start_term end
+ fun mk_rhs exprs =
+ @{term "If :: bool => term list option => term list option => term list option"}
+ $ size_ge_zero $ (foldr1 mk_none_continuation exprs) $ @{term "None :: term list option"}
+ val rhss =
+ Datatype_Aux.interpret_construction descr vs
+ { atyp = mk_small_call, dtyp = mk_small_aux_call }
+ |> (map o apfst) Type
+ |> map (fn (T, cs) => map (mk_consexpr T) cs)
+ |> map mk_rhs
+ val lhss = map2 (fn t => fn T => t $ test_function T $ size) smalls (Ts @ Us);
+ val eqs = map (HOLogic.mk_Trueprop o HOLogic.mk_eq) (lhss ~~ rhss)
+ in
+ (Ts @ Us ~~ (smallsN ~~ eqs))
+ end
+
+val less_int_pred = @{lemma "i > 0 ==> Code_Numeral.nat_of ((i :: code_numeral) - 1) < Code_Numeral.nat_of i" by auto}
+
+fun gen_inst_state_tac ctxt rel st =
+ case Term.add_vars (prop_of st) [] of
+ [v as (_, T)] =>
+ let
+ val cert = Thm.cterm_of (ProofContext.theory_of ctxt)
+ val rel' = cert rel
+ val st' = Thm.incr_indexes (#maxidx (Thm.rep_cterm rel') + 1) st (*FIXME??*)
+ in
+ PRIMITIVE (Drule.cterm_instantiate [(cert (Var v), rel')]) st'
+ end
+ | _ => Seq.empty;
+
+fun instantiate_smallvalue_datatype config descr vs tycos prfx (names, auxnames) (Ts, Us) thy =
+ let
+ val _ = Datatype_Aux.message config "Creating smallvalue generators ...";
+ val eqs = mk_equations thy descr vs tycos (names, auxnames) (Ts, Us)
+ fun my_relation_tac ctxt st =
+ let
+ val ((_ $ (_ $ rel)) :: tl) = prems_of st
+ val domT = (HOLogic.dest_setT (fastype_of rel))
+ fun mk_single_measure T = mk_fun_comp (@{term "Code_Numeral.nat_of"},
+ Const (@{const_name "Product_Type.snd"}, T --> @{typ "code_numeral"}))
+ val measure = mk_measure (mk_sumcases @{typ nat} mk_single_measure domT)
+ in
+ (Function_Common.apply_termination_rule ctxt 1
+ THEN gen_inst_state_tac ctxt measure) st
+ end
+ fun termination_tac ctxt =
+ my_relation_tac ctxt
+ THEN rtac @{thm wf_measure} 1
+ THEN (REPEAT_DETERM (Simplifier.asm_full_simp_tac
+ (HOL_basic_ss addsimps [@{thm in_measure}, @{thm o_def}, @{thm snd_conv},
+ @{thm nat_mono_iff}, less_int_pred] @ @{thms sum.cases}) 1))
+ fun pat_completeness_auto ctxt =
+ Pat_Completeness.pat_completeness_tac ctxt 1
+ THEN auto_tac (clasimpset_of ctxt)
+ in
+ thy
+ |> Class.instantiation (tycos, vs, @{sort small})
+ |> Function.add_function
+ (map (fn (T, (name, _)) =>
+ Syntax.no_syn (Binding.conceal (Binding.name name), SOME (smallT T))) eqs)
+ (map (pair (apfst Binding.conceal Attrib.empty_binding) o snd o snd) eqs)
+ Function_Common.default_config pat_completeness_auto
+ |> snd
+ |> Local_Theory.restore
+ |> (fn lthy => Function.prove_termination NONE (termination_tac lthy) lthy)
+ |> snd
+ |> Class.prove_instantiation_exit (K (Class.intro_classes_tac []))
+ end;
+
+fun ensure_smallvalue_datatype config raw_tycos thy =
+ let
+ val algebra = Sign.classes_of thy;
+ val (descr, raw_vs, tycos, prfx, (names, auxnames), raw_TUs) =
+ Datatype.the_descr thy raw_tycos;
+ val typerep_vs = (map o apsnd)
+ (curry (Sorts.inter_sort algebra) @{sort typerep}) raw_vs;
+ val smallvalue_insts = (map (rpair @{sort small}) o flat o maps snd o maps snd)
+ (Datatype_Aux.interpret_construction descr typerep_vs
+ { atyp = single, dtyp = (K o K o K) [] });
+ (*val term_of_insts = (map (rpair @{sort term_of}) o flat o maps snd o maps snd)
+ (Datatype_Aux.interpret_construction descr typerep_vs
+ { atyp = K [], dtyp = K o K });*)
+ val has_inst = exists (fn tyco =>
+ can (Sorts.mg_domain algebra tyco) @{sort small}) tycos;
+ in if has_inst then thy
+ else case Quickcheck_Generators.perhaps_constrain thy smallvalue_insts typerep_vs
+ of SOME constrain => (instantiate_smallvalue_datatype config descr
+ (map constrain typerep_vs) tycos prfx (names, auxnames)
+ ((pairself o map o map_atyps) (fn TFree v => TFree (constrain v)) raw_TUs) thy
+ handle FUNCTION_TYPE =>
+ (Datatype_Aux.message config
+ "Creation of smallvalue generators failed because the datatype contains a function type";
+ thy))
+ | NONE => thy
+ end;
+
+(** building and compiling generator expressions **)
+
+structure Counterexample = Proof_Data (
+ type T = unit -> int -> term list option
+ fun init _ () = error "Counterexample"
+);
+val put_counterexample = Counterexample.put;
+
+val target = "Quickcheck";
+
+fun mk_generator_expr thy prop Ts =
+ let
+ val bound_max = length Ts - 1;
+ val bounds = map Bound (bound_max downto 0)
+ val result = list_comb (prop, bounds);
+ val terms = HOLogic.mk_list @{typ term} (map2 HOLogic.mk_term_of Ts bounds);
+ val check =
+ @{term "Smallcheck.catch_match :: term list option => term list option => term list option"} $
+ (@{term "If :: bool => term list option => term list option => term list option"}
+ $ result $ @{term "None :: term list option"}
+ $ (@{term "Some :: term list => term list option"} $ terms))
+ $ @{term "None :: term list option"};
+ fun mk_small_closure (depth, T) t =
+ Const (@{const_name "Smallcheck.small_class.small"}, smallT T)
+ $ absdummy (T, t) $ depth
+ in Abs ("d", @{typ code_numeral}, fold_rev mk_small_closure (rev bounds ~~ Ts) check) end
+
+fun compile_generator_expr ctxt t =
+ let
+ val Ts = (map snd o fst o strip_abs) t;
+ val thy = ProofContext.theory_of ctxt
+ in if Quickcheck.report ctxt then
+ error "Compilation with reporting facility is not supported"
+ else
+ let
+ val t' = mk_generator_expr thy t Ts;
+ val compile = Code_Runtime.dynamic_value_strict
+ (Counterexample.get, put_counterexample, "Smallvalue_Generators.put_counterexample")
+ thy (SOME target) (fn proc => fn g => g #> (Option.map o map) proc) t' [];
+ val dummy_report = ([], false)
+ in compile #> rpair dummy_report end
+ end;
+
+(** setup **)
+
+val setup =
+ Datatype.interpretation ensure_smallvalue_datatype
+ #> Context.theory_map
+ (Quickcheck.add_generator ("small", compile_generator_expr));
+
+end;
--- a/src/Tools/Code/code_runtime.ML Mon Nov 08 09:10:44 2010 +0100
+++ b/src/Tools/Code/code_runtime.ML Mon Nov 08 13:25:00 2010 +0100
@@ -25,8 +25,8 @@
-> ((term -> term) -> 'a -> 'a) -> string list -> term -> 'a Exn.result
val dynamic_holds_conv: conv
val static_holds_conv: theory -> string list -> conv
- val code_reflect: (string * string list) list -> string list -> string -> string option
- -> theory -> theory
+ val code_reflect: (string * string list option) list -> string list -> string
+ -> string option -> theory -> theory
datatype truth = Holds
val put_truth: (unit -> truth) -> Proof.context -> Proof.context
val trace: bool Unsynchronized.ref
@@ -213,8 +213,8 @@
structure Code_Antiq_Data = Proof_Data
(
type T = (string list * string list) * (bool
- * (string * ((string * string) list * (string * string) list)) lazy);
- fun init _ = (([], []), (true, (Lazy.value ("", ([], [])))));
+ * (string * (string * string) list) lazy);
+ fun init _ = (([], []), (true, (Lazy.value ("", []))));
);
val is_first_occ = fst o snd o Code_Antiq_Data.get;
@@ -225,24 +225,22 @@
val tycos' = fold (insert (op =)) new_tycos tycos;
val consts' = fold (insert (op =)) new_consts consts;
val acc_code = Lazy.lazy (fn () =>
- evaluation_code (ProofContext.theory_of ctxt) "Code" tycos' consts');
+ evaluation_code (ProofContext.theory_of ctxt) "Code" tycos' consts'
+ |> apsnd snd);
in Code_Antiq_Data.put ((tycos', consts'), (false, acc_code)) ctxt end;
fun register_const const = register_code [] [const];
-fun register_datatype tyco constrs = register_code [tyco] constrs;
-
-fun print_const const all_struct_name tycos_map consts_map =
+fun print_const const all_struct_name consts_map =
(Long_Name.append all_struct_name o the o AList.lookup (op =) consts_map) const;
-fun print_code is_first print_it ctxt =
+fun print_code is_first const ctxt =
let
val (_, (_, acc_code)) = Code_Antiq_Data.get ctxt;
- val (ml_code, (tycos_map, consts_map)) = Lazy.force acc_code;
- val ml_code = if is_first then ml_code
- else "";
+ val (ml_code, consts_map) = Lazy.force acc_code;
+ val ml_code = if is_first then ml_code else "";
val all_struct_name = "Isabelle";
- in (ml_code, print_it all_struct_name tycos_map consts_map) end;
+ in (ml_code, print_const const all_struct_name consts_map) end;
in
@@ -251,33 +249,38 @@
val const = Code.check_const (ProofContext.theory_of background) raw_const;
val is_first = is_first_occ background;
val background' = register_const const background;
- in (print_code is_first (print_const const), background') end;
+ in (print_code is_first const, background') end;
end; (*local*)
(* reflection support *)
-fun check_datatype thy tyco consts =
+fun check_datatype thy tyco some_consts =
let
val constrs = (map (fst o fst) o snd o Code.get_type thy) tyco;
- val missing_constrs = subtract (op =) consts constrs;
- val _ = if null missing_constrs then []
- else error ("Missing constructor(s) " ^ commas (map quote missing_constrs)
- ^ " for datatype " ^ quote tyco);
- val false_constrs = subtract (op =) constrs consts;
- val _ = if null false_constrs then []
- else error ("Non-constructor(s) " ^ commas (map quote false_constrs)
- ^ " for datatype " ^ quote tyco);
- in () end;
+ val _ = case some_consts
+ of SOME consts =>
+ let
+ val missing_constrs = subtract (op =) consts constrs;
+ val _ = if null missing_constrs then []
+ else error ("Missing constructor(s) " ^ commas (map quote missing_constrs)
+ ^ " for datatype " ^ quote tyco);
+ val false_constrs = subtract (op =) constrs consts;
+ val _ = if null false_constrs then []
+ else error ("Non-constructor(s) " ^ commas (map quote false_constrs)
+ ^ " for datatype " ^ quote tyco)
+ in () end
+ | NONE => ();
+ in (tyco, constrs) end;
fun add_eval_tyco (tyco, tyco') thy =
let
val k = Sign.arity_number thy tyco;
- fun pr pr' fxy [] = tyco'
- | pr pr' fxy [ty] =
+ fun pr pr' _ [] = tyco'
+ | pr pr' _ [ty] =
Code_Printer.concat [pr' Code_Printer.BR ty, tyco']
- | pr pr' fxy tys =
+ | pr pr' _ tys =
Code_Printer.concat [Code_Printer.enum "," "(" ")" (map (pr' Code_Printer.BR) tys), tyco']
in
thy
@@ -317,10 +320,9 @@
fun gen_code_reflect prep_type prep_const raw_datatypes raw_functions module_name some_file thy =
let
val datatypes = map (fn (raw_tyco, raw_cos) =>
- (prep_type thy raw_tyco, map (prep_const thy) raw_cos)) raw_datatypes;
- val _ = map (uncurry (check_datatype thy)) datatypes;
- val tycos = map fst datatypes;
- val constrs = maps snd datatypes;
+ (prep_type thy raw_tyco, (Option.map o map) (prep_const thy) raw_cos)) raw_datatypes;
+ val (tycos, constrs) = map_split (uncurry (check_datatype thy)) datatypes
+ |> apsnd flat;
val functions = map (prep_const thy) raw_functions;
val result = evaluation_code thy module_name tycos (constrs @ functions)
|> (apsnd o apsnd) (chop (length constrs));
@@ -347,7 +349,8 @@
val _ = List.app Keyword.keyword [datatypesK, functionsK];
val parse_datatype =
- Parse.name --| Parse.$$$ "=" -- (Parse.term ::: (Scan.repeat (Parse.$$$ "|" |-- Parse.term)));
+ Parse.name --| Parse.$$$ "=" -- ((Parse.string >> (fn "*" => NONE | _ => Scan.fail ()))
+ || ((Parse.term ::: (Scan.repeat (Parse.$$$ "|" |-- Parse.term))) >> SOME));
in
--- a/src/Tools/cache_io.ML Mon Nov 08 09:10:44 2010 +0100
+++ b/src/Tools/cache_io.ML Mon Nov 08 13:25:00 2010 +0100
@@ -6,10 +6,13 @@
signature CACHE_IO =
sig
+ (*IO wrapper*)
val with_tmp_file: string -> (Path.T -> 'a) -> 'a
val with_tmp_dir: string -> (Path.T -> 'a) -> 'a
- val run: (Path.T -> Path.T -> string) -> string -> string list * string list
+ val run: (Path.T -> Path.T -> string) -> string ->
+ {output: string list, redirected_output: string list, return_code: int}
+ (*cache*)
type cache
val make: Path.T -> cache
val cache_path_of: cache -> Path.T
@@ -23,6 +26,8 @@
structure Cache_IO : CACHE_IO =
struct
+(* IO wrapper *)
+
val cache_io_prefix = "cache-io-"
fun with_tmp_file name f =
@@ -45,21 +50,20 @@
with_tmp_file cache_io_prefix (fn out_path =>
let
val _ = File.write in_path str
- val (out2, _) = bash_output (make_cmd in_path out_path)
+ val (out2, rc) = bash_output (make_cmd in_path out_path)
val out1 = the_default [] (try (rev o File.fold_lines cons out_path) [])
- in (out1, split_lines out2) end))
+ in {output=split_lines out2, redirected_output=out1, return_code=rc} end))
+(* cache *)
abstype cache = Cache of {
path: Path.T,
table: (int * (int * int * int) Symtab.table) Synchronized.var }
with
-
fun cache_path_of (Cache {path, ...}) = path
-
fun load cache_path =
let
fun err () = error ("Cache IO: corrupted cache file: " ^
@@ -87,7 +91,6 @@
let val table = if File.exists path then load path else (1, Symtab.empty)
in Cache {path=path, table=Synchronized.var (Path.implode path) table} end
-
fun load_cached_result cache_path (p, len1, len2) =
let
fun load line (i, xsp) =
@@ -97,7 +100,6 @@
else (i, xsp)
in pairself rev (snd (File.fold_lines load cache_path (1, ([], [])))) end
-
fun lookup (Cache {path=cache_path, table}) str =
let val key = SHA1.digest str
in
@@ -106,10 +108,10 @@
| SOME pos => (SOME (load_cached_result cache_path pos), key))
end
-
fun run_and_cache (Cache {path=cache_path, table}) key make_cmd str =
let
- val res as (out, err) = run make_cmd str
+ val {output=err, redirected_output=out, ...} = run make_cmd str
+ val res = (out, err)
val (l1, l2) = pairself length res
val header = key ^ " " ^ string_of_int l1 ^ " " ^ string_of_int l2
val lines = map (suffix "\n") (header :: out @ err)
@@ -121,11 +123,11 @@
in (p+l1+l2+1, Symtab.update (key, (p+1, l1, l2)) tab) end)
in res end
-
fun run_cached cache make_cmd str =
(case lookup cache str of
(NONE, key) => run_and_cache cache key make_cmd str
| (SOME output, _) => output)
end
+
end