--- a/etc/isar-keywords-ZF.el Fri Sep 10 17:53:25 2010 +0200
+++ b/etc/isar-keywords-ZF.el Mon Sep 13 09:29:43 2010 +0200
@@ -44,7 +44,6 @@
"code_module"
"coinductive"
"commit"
- "constdefs"
"consts"
"consts_code"
"context"
@@ -354,7 +353,6 @@
"code_library"
"code_module"
"coinductive"
- "constdefs"
"consts"
"consts_code"
"context"
--- a/etc/isar-keywords.el Fri Sep 10 17:53:25 2010 +0200
+++ b/etc/isar-keywords.el Mon Sep 13 09:29:43 2010 +0200
@@ -63,7 +63,6 @@
"coinductive"
"coinductive_set"
"commit"
- "constdefs"
"consts"
"consts_code"
"context"
@@ -449,7 +448,6 @@
"code_type"
"coinductive"
"coinductive_set"
- "constdefs"
"consts"
"consts_code"
"context"
--- a/src/HOL/SMT.thy Fri Sep 10 17:53:25 2010 +0200
+++ b/src/HOL/SMT.thy Mon Sep 13 09:29:43 2010 +0200
@@ -241,6 +241,13 @@
declare [[ z3_options = "" ]]
+text {*
+The following configuration option may be used to enable mapping of
+HOL datatypes and records to native datatypes provided by Z3.
+*}
+
+declare [[ z3_datatypes = false ]]
+
subsection {* Schematic rules for Z3 proof reconstruction *}
--- a/src/HOL/Tools/SMT/smt_translate.ML Fri Sep 10 17:53:25 2010 +0200
+++ b/src/HOL/Tools/SMT/smt_translate.ML Mon Sep 13 09:29:43 2010 +0200
@@ -26,10 +26,12 @@
builtin_typ: Proof.context -> typ -> string option,
builtin_num: Proof.context -> typ -> int -> string option,
builtin_fun: Proof.context -> string * typ -> term list ->
- (string * term list) option }
+ (string * term list) option,
+ has_datatypes: bool }
type sign = {
header: string list,
sorts: string list,
+ dtyps: (string * (string * (string * string) list) list) list list,
funcs: (string * (string list * string)) list }
type config = {
prefixes: prefixes,
@@ -79,11 +81,13 @@
builtin_typ: Proof.context -> typ -> string option,
builtin_num: Proof.context -> typ -> int -> string option,
builtin_fun: Proof.context -> string * typ -> term list ->
- (string * term list) option }
+ (string * term list) option,
+ has_datatypes: bool }
type sign = {
header: string list,
sorts: string list,
+ dtyps: (string * (string * (string * string) list) list) list list,
funcs: (string * (string list * string)) list }
type config = {
@@ -248,38 +252,67 @@
(* translation from Isabelle terms into SMT intermediate terms *)
-val empty_context = (1, Typtab.empty, 1, Termtab.empty)
+val empty_context = (1, Typtab.empty, [], 1, Termtab.empty)
-fun make_sign header (_, typs, _, terms) = {
+fun make_sign header (_, typs, dtyps, _, terms) = {
header = header,
- sorts = Typtab.fold (cons o snd) typs [],
- funcs = Termtab.fold (cons o snd) terms [] }
+ sorts = Typtab.fold (fn (_, (n, true)) => cons n | _ => I) typs [],
+ funcs = Termtab.fold (fn (_, (n, SOME ss)) => cons (n,ss) | _ => I) terms [],
+ dtyps = dtyps }
-fun make_recon (unfolds, assms) (_, typs, _, terms) = {
- typs = Symtab.make (map swap (Typtab.dest typs)),
+fun make_recon (unfolds, assms) (_, typs, _, _, terms) = {
+ typs = Symtab.make (map (apfst fst o swap) (Typtab.dest typs)),
+ (*FIXME: don't drop the datatype information! *)
terms = Symtab.make (map (fn (t, (n, _)) => (n, t)) (Termtab.dest terms)),
unfolds = unfolds,
assms = assms }
fun string_of_index pre i = pre ^ string_of_int i
-fun fresh_typ sort_prefix T (cx as (Tidx, typs, idx, terms)) =
- (case Typtab.lookup typs T of
- SOME s => (s, cx)
- | NONE =>
- let
- val s = string_of_index sort_prefix Tidx
- val typs' = Typtab.update (T, s) typs
- in (s, (Tidx+1, typs', idx, terms)) end)
+fun new_typ sort_prefix proper T (Tidx, typs, dtyps, idx, terms) =
+ let val s = string_of_index sort_prefix Tidx
+ in (s, (Tidx+1, Typtab.update (T, (s, proper)) typs, dtyps, idx, terms)) end
+
+fun lookup_typ (_, typs, _, _, _) = Typtab.lookup typs
-fun fresh_fun func_prefix t ss (cx as (Tidx, typs, idx, terms)) =
+fun fresh_typ T f cx =
+ (case lookup_typ cx T of
+ SOME (s, _) => (s, cx)
+ | NONE => f T cx)
+
+fun new_fun func_prefix t ss (Tidx, typs, dtyps, idx, terms) =
+ let
+ val f = string_of_index func_prefix idx
+ val terms' = Termtab.update (revert_types t, (f, ss)) terms
+ in (f, (Tidx, typs, dtyps, idx+1, terms')) end
+
+fun fresh_fun func_prefix t ss (cx as (_, _, _, _, terms)) =
(case Termtab.lookup terms t of
SOME (f, _) => (f, cx)
- | NONE =>
- let
- val f = string_of_index func_prefix idx
- val terms' = Termtab.update (revert_types t, (f, ss)) terms
- in (f, (Tidx, typs, idx+1, terms')) end)
+ | NONE => new_fun func_prefix t ss cx)
+
+fun inst_const f Ts t =
+ let
+ val (n, T) = Term.dest_Const (snd (Type.varify_global [] t))
+ val inst = map Term.dest_TVar (snd (Term.dest_Type (f T))) ~~ Ts
+ in Const (n, Term_Subst.instantiateT inst T) end
+
+fun inst_constructor Ts = inst_const Term.body_type Ts
+fun inst_selector Ts = inst_const Term.domain_type Ts
+
+fun lookup_datatype ctxt n Ts = (* FIXME: use Datatype/Record.get_info *)
+ if n = @{type_name prod}
+ then SOME [
+ (Type (n, Ts), [
+ (inst_constructor Ts @{term Pair},
+ map (inst_selector Ts) [@{term fst}, @{term snd}])])]
+ else if n = @{type_name list}
+ then SOME [
+ (Type (n, Ts), [
+ (inst_constructor Ts @{term Nil}, []),
+ (inst_constructor Ts @{term Cons},
+ map (inst_selector Ts) [@{term hd}, @{term tl}])])]
+ else NONE
fun relaxed thms = (([], thms), map prop_of thms)
@@ -291,12 +324,40 @@
fun translate {prefixes, strict, header, builtins, serialize} ctxt comments =
let
val {sort_prefix, func_prefix} = prefixes
- val {builtin_typ, builtin_num, builtin_fun} = builtins
+ val {builtin_typ, builtin_num, builtin_fun, has_datatypes} = builtins
+
+ fun transT (T as TFree _) = fresh_typ T (new_typ sort_prefix true)
+ | transT (T as TVar _) = (fn _ => raise TYPE ("smt_translate", [T], []))
+ | transT (T as Type (n, Ts)) =
+ (case builtin_typ ctxt T of
+ SOME n => pair n
+ | NONE => fresh_typ T (fn _ => fn cx =>
+ if not has_datatypes then new_typ sort_prefix true T cx
+ else
+ (case lookup_datatype ctxt n Ts of
+ NONE => new_typ sort_prefix true T cx
+ | SOME dts =>
+ let val cx' = new_dtyps dts cx
+ in (fst (the (lookup_typ cx' T)), cx') end)))
- fun transT T =
- (case builtin_typ ctxt T of
- SOME n => pair n
- | NONE => fresh_typ sort_prefix T)
+ and new_dtyps dts cx =
+ let
+ fun new_decl i t =
+ let val (Ts, T) = dest_funT i (Term.fastype_of t)
+ in
+ fold_map transT Ts ##>> transT T ##>>
+ new_fun func_prefix t NONE #>> swap
+ end
+ fun new_dtyp_decl (con, sels) =
+ new_decl (length sels) con ##>> fold_map (new_decl 1) sels #>>
+ (fn ((con', _), sels') => (con', map (apsnd snd) sels'))
+ in
+ cx
+ |> fold_map (new_typ sort_prefix false o fst) dts
+ ||>> fold_map (fold_map new_dtyp_decl o snd) dts
+ |-> (fn (ss, decls) => fn (Tidx, typs, dtyps, idx, terms) =>
+ (Tidx, typs, (ss ~~ decls) :: dtyps, idx, terms))
+ end
fun app n ts = SApp (n, ts)
@@ -327,13 +388,13 @@
| NONE => transs h T ts))
| (h as Free (_, T), ts) => transs h T ts
| (Bound i, []) => pair (SVar i)
- | _ => raise TERM ("intermediate", [t]))
+ | _ => raise TERM ("smt_translate", [t]))
and transs t T ts =
let val (Us, U) = dest_funT (length ts) T
in
fold_map transT Us ##>> transT U #-> (fn Up =>
- fresh_fun func_prefix t Up ##>> fold_map trans ts #>> SApp)
+ fresh_fun func_prefix t (SOME Up) ##>> fold_map trans ts #>> SApp)
end
in
(case strict of SOME strct => strictify strct ctxt | NONE => relaxed) #>
--- a/src/HOL/Tools/SMT/smtlib_interface.ML Fri Sep 10 17:53:25 2010 +0200
+++ b/src/HOL/Tools/SMT/smtlib_interface.ML Mon Sep 13 09:29:43 2010 +0200
@@ -15,6 +15,7 @@
val add_builtins: builtins -> Context.generic -> Context.generic
val add_logic: (term list -> string option) -> Context.generic ->
Context.generic
+ val extra_norm: bool -> SMT_Normalize.extra_norm
val interface: SMT_Solver.interface
end
@@ -87,9 +88,9 @@
(* include additional facts *)
-fun extra_norm thms ctxt =
+fun extra_norm has_datatypes thms ctxt =
thms
- |> add_pair_rules
+ |> not has_datatypes ? add_pair_rules
|> add_fun_upd_rules
|> map (unfold_abs_min_max_defs ctxt)
|> rpair ctxt
@@ -251,13 +252,22 @@
fun ssort sorts = sort fast_string_ord sorts
fun fsort funcs = sort (prod_ord fast_string_ord (K EQUAL)) funcs
-fun serialize comments {header, sorts, funcs} ts =
+fun sdatatypes decls =
+ let
+ fun con (n, []) = add n
+ | con (n, sels) = par (add n #>
+ fold (fn (n, s) => sep (par (add n #> sep (add s)))) sels)
+ fun dtyp (n, decl) = add n #> fold (sep o con) decl
+ in line (add ":datatypes " #> par (fold (par o dtyp) decls)) end
+
+fun serialize comments {header, sorts, dtyps, funcs} ts =
Buffer.empty
|> line (add "(benchmark Isabelle")
|> line (add ":status unknown")
|> fold (line o add) header
|> length sorts > 0 ?
line (add ":extrasorts" #> par (fold (sep o add) (ssort sorts)))
+ |> fold sdatatypes dtyps
|> length funcs > 0 ? (
line (add ":extrafuns" #> add " (") #>
fold (fn (f, (ss, s)) =>
@@ -273,7 +283,7 @@
(** interfaces **)
val interface = {
- extra_norm = extra_norm,
+ extra_norm = extra_norm false,
translate = {
prefixes = {
sort_prefix = "S",
@@ -286,7 +296,8 @@
builtins = {
builtin_typ = builtin_typ,
builtin_num = builtin_num,
- builtin_fun = builtin_fun},
+ builtin_fun = builtin_fun,
+ has_datatypes = false},
serialize = serialize}}
end
--- a/src/HOL/Tools/SMT/z3_interface.ML Fri Sep 10 17:53:25 2010 +0200
+++ b/src/HOL/Tools/SMT/z3_interface.ML Mon Sep 13 09:29:43 2010 +0200
@@ -8,7 +8,7 @@
sig
type builtin_fun = string * typ -> term list -> (string * term list) option
val add_builtin_funs: builtin_fun -> Context.generic -> Context.generic
- val interface: SMT_Solver.interface
+ val interface: bool -> SMT_Solver.interface
datatype sym = Sym of string * sym list
type mk_builtins = {
@@ -68,7 +68,7 @@
val {extra_norm, translate} = SMTLIB_Interface.interface
val {prefixes, strict, header, builtins, serialize} = translate
val {is_builtin_pred, ...}= the strict
- val {builtin_typ, builtin_num, builtin_fun} = builtins
+ val {builtin_typ, builtin_num, builtin_fun, ...} = builtins
fun is_int_div_mod @{term "op div :: int => _"} = true
| is_int_div_mod @{term "op mod :: int => _"} = true
@@ -79,7 +79,8 @@
then [@{thm div_by_z3div}, @{thm mod_by_z3mod}] @ thms
else thms
- fun extra_norm' thms = extra_norm (add_div_mod thms)
+ fun extra_norm' has_datatypes thms =
+ SMTLIB_Interface.extra_norm has_datatypes (add_div_mod thms)
fun z3_builtin_fun' _ (@{const_name z3div}, _) ts = SOME ("div", ts)
| z3_builtin_fun' _ (@{const_name z3mod}, _) ts = SOME ("mod", ts)
@@ -94,8 +95,8 @@
is_some (z3_builtin_fun' ctxt c ts) orelse
is_builtin_pred ctxt (n, Term.strip_type T ||> as_propT |> (op --->))
-val interface = {
- extra_norm = extra_norm',
+fun interface has_datatypes = {
+ extra_norm = extra_norm' has_datatypes,
translate = {
prefixes = prefixes,
strict = strict,
@@ -103,7 +104,8 @@
builtins = {
builtin_typ = builtin_typ,
builtin_num = builtin_num,
- builtin_fun = z3_builtin_fun'},
+ builtin_fun = z3_builtin_fun',
+ has_datatypes = has_datatypes},
serialize = serialize}}
end
--- a/src/HOL/Tools/SMT/z3_solver.ML Fri Sep 10 17:53:25 2010 +0200
+++ b/src/HOL/Tools/SMT/z3_solver.ML Mon Sep 13 09:29:43 2010 +0200
@@ -8,6 +8,7 @@
sig
val proofs: bool Config.T
val options: string Config.T
+ val datatypes: bool Config.T
val setup: theory -> theory
end
@@ -19,6 +20,7 @@
val (proofs, proofs_setup) = Attrib.config_bool "z3_proofs" (K false)
val (options, options_setup) = Attrib.config_string "z3_options" (K "")
+val (datatypes, datatypes_setup) = Attrib.config_bool "z3_datatypes" (K false)
fun add xs ys = ys @ xs
@@ -62,17 +64,21 @@
val prover = if_unsat Z3_Proof_Reconstruction.reconstruct
fun solver oracle ctxt =
- let val with_proof = Config.get ctxt proofs
+ let
+ val with_datatypes = Config.get ctxt datatypes
+ val with_proof = not with_datatypes andalso Config.get ctxt proofs
+ (* FIXME: implement proof reconstruction for datatypes *)
in
{command = {env_var=env_var, remote_name=SOME solver_name},
arguments = cmdline_options ctxt,
- interface = Z3_Interface.interface,
+ interface = Z3_Interface.interface with_datatypes,
reconstruct = if with_proof then prover else pair o oracle}
end
val setup =
proofs_setup #>
options_setup #>
+ datatypes_setup #>
Thm.add_oracle (Binding.name solver_name, core_oracle) #-> (fn (_, oracle) =>
Context.theory_map (SMT_Solver.add_solver (solver_name, solver oracle))) #>
Context.theory_map (SMT_Solver.add_solver_info (solver_name, pretty_config))
--- a/src/Provers/hypsubst.ML Fri Sep 10 17:53:25 2010 +0200
+++ b/src/Provers/hypsubst.ML Mon Sep 13 09:29:43 2010 +0200
@@ -115,11 +115,11 @@
| (_, Bound i) => if loose(i,t) orelse novars andalso has_vars t
then raise Match
else false (*eliminates u*)
- | (Free _, _) => if bnd orelse Logic.occs(t,u) orelse
+ | (t' as Free _, _) => if bnd orelse Logic.occs(t',u) orelse
novars andalso has_vars u
then raise Match
else true (*eliminates t*)
- | (_, Free _) => if bnd orelse Logic.occs(u,t) orelse
+ | (_, u' as Free _) => if bnd orelse Logic.occs(u',t) orelse
novars andalso has_vars t
then raise Match
else false (*eliminates u*)