# HG changeset patch
# User bulwahn
# Date 1284362983 -7200
# Node ID ad79b89b4351f670e243b95a81ae413005a8dad1
# Parent  e98a061455300864751b620e0095d4919d0a3b4a# Parent  5aefb5bc8a938030c4d7463522846fcb960c4b7c
merged

diff -r e98a06145530 -r ad79b89b4351 etc/isar-keywords-ZF.el
--- 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"
diff -r e98a06145530 -r ad79b89b4351 etc/isar-keywords.el
--- 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"
diff -r e98a06145530 -r ad79b89b4351 src/HOL/SMT.thy
--- 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 *}
diff -r e98a06145530 -r ad79b89b4351 src/HOL/Tools/SMT/smt_translate.ML
--- 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) #>
diff -r e98a06145530 -r ad79b89b4351 src/HOL/Tools/SMT/smtlib_interface.ML
--- 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
diff -r e98a06145530 -r ad79b89b4351 src/HOL/Tools/SMT/z3_interface.ML
--- 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
diff -r e98a06145530 -r ad79b89b4351 src/HOL/Tools/SMT/z3_solver.ML
--- 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))
diff -r e98a06145530 -r ad79b89b4351 src/Provers/hypsubst.ML
--- 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*)