add full support for datatypes to the SMT interface (only used by Z3 in oracle mode so far); added store to keep track of datatype selector functions

--- a/src/HOL/IsaMakefile	Fri Sep 17 08:41:07 2010 +0200
+++ b/src/HOL/IsaMakefile	Fri Sep 17 10:52:35 2010 +0200
@@ -271,6 +271,7 @@
   Tools/ATP/atp_proof.ML \
   Tools/ATP/atp_systems.ML \
   Tools/choice_specification.ML \
+  Tools/Datatype/datatype_selectors.ML \
   Tools/int_arith.ML \
   Tools/groebner.ML \
   Tools/list_code.ML \

--- a/src/HOL/SMT.thy	Fri Sep 17 08:41:07 2010 +0200
+++ b/src/HOL/SMT.thy	Fri Sep 17 10:52:35 2010 +0200
@@ -7,6 +7,7 @@
 theory SMT
 imports List
 uses
+  "Tools/Datatype/datatype_selectors.ML"
   ("Tools/SMT/smt_monomorph.ML")
   ("Tools/SMT/smt_normalize.ML")
   ("Tools/SMT/smt_translate.ML")
@@ -323,4 +324,13 @@
 hide_const Pattern term_eq
 hide_const (open) trigger pat nopat fun_app z3div z3mod
 
+
+
+subsection {* Selectors for datatypes *}
+
+setup {* Datatype_Selectors.setup *}
+
+declare [[ selector Pair 1 = fst, selector Pair 2 = snd ]]
+declare [[ selector Cons 1 = hd, selector Cons 2 = tl ]]
+
 end

--- a/src/HOL/SMT_Examples/SMT_Tests.thy	Fri Sep 17 08:41:07 2010 +0200
+++ b/src/HOL/SMT_Examples/SMT_Tests.thy	Fri Sep 17 10:52:35 2010 +0200
@@ -607,7 +607,7 @@
 
 
 
-section {* Pairs *}
+section {* Pairs *}  (* FIXME: tests for datatypes and records *)
 
 lemma
   "x = fst (x, y)"

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/Datatype/datatype_selectors.ML	Fri Sep 17 10:52:35 2010 +0200
@@ -0,0 +1,83 @@
+(*  Title:      HOL/Tools/Datatype/datatype_selectors.ML
+    Author:     Sascha Boehme, TU Muenchen
+
+Selector functions for datatype constructor arguments.
+*)
+
+signature DATATYPE_SELECTORS =
+sig
+  val add_selector: ((string * typ) * int) * (string * typ) ->
+    Context.generic -> Context.generic
+  val lookup_selector: Proof.context -> string * int -> string option
+  val setup: theory -> theory
+end
+
+structure Datatype_Selectors: DATATYPE_SELECTORS =
+struct
+
+structure Stringinttab = Table
+(
+  type key = string * int
+  val ord = prod_ord fast_string_ord int_ord
+)
+
+structure Data = Generic_Data
+(
+  type T = string Stringinttab.table
+  val empty = Stringinttab.empty
+  val extend = I
+  val merge = Stringinttab.merge (K true)
+)
+
+fun pretty_term context = Syntax.pretty_term (Context.proof_of context)
+
+fun sanity_check context (((con as (n, _), i), sel as (m, _))) =
+  let
+    val thy = Context.theory_of context
+    val varify_const =
+      Const #> Type.varify_global [] #> snd #> Term.dest_Const #>
+      snd #> Term.strip_type
+
+    val (Ts, T) = varify_const con
+    val (Us, U) = varify_const sel
+    val _ = (0 < i andalso i <= length Ts) orelse
+      error (Pretty.string_of (Pretty.block [
+        Pretty.str "The constructor ",
+        Pretty.quote (pretty_term context (Const con)),
+        Pretty.str " has no argument position ",
+        Pretty.str (string_of_int i),
+        Pretty.str "."]))
+    val _ = length Us = 1 orelse
+      error (Pretty.string_of (Pretty.block [
+        Pretty.str "The term ", Pretty.quote (pretty_term context (Const sel)),
+        Pretty.str " might not be a selector ",
+        Pretty.str "(it accepts more than one argument)."]))
+    val _ =
+     (Sign.typ_equiv thy (T, hd Us) andalso
+      Sign.typ_equiv thy (nth Ts (i-1), U)) orelse
+      error (Pretty.string_of (Pretty.block [
+        Pretty.str "The types of the constructor ",
+        Pretty.quote (pretty_term context (Const con)),
+        Pretty.str " and of the selector ",
+        Pretty.quote (pretty_term context (Const sel)),
+        Pretty.str " do not fit to each other."]))
+  in ((n, i), m) end
+
+fun add_selector (entry as ((con as (n, _), i), (_, T))) context =
+  (case Stringinttab.lookup (Data.get context) (n, i) of
+    NONE => Data.map (Stringinttab.update (sanity_check context entry)) context
+  | SOME c => error (Pretty.string_of (Pretty.block [
+      Pretty.str "There is already a selector assigned to constructor ",
+      Pretty.quote (pretty_term context (Const con)), Pretty.str ", namely ",
+      Pretty.quote (pretty_term context (Const (c, T))), Pretty.str "."])))
+
+fun lookup_selector ctxt = Stringinttab.lookup (Data.get (Context.Proof ctxt))
+
+val setup =
+  Attrib.setup @{binding selector}
+   ((Args.term >> Term.dest_Const) -- Scan.lift (Parse.nat) --|
+    Scan.lift (Parse.$$$ "=") -- (Args.term >> Term.dest_Const) >>
+    (Thm.declaration_attribute o K o add_selector))
+  "assign a selector function to a datatype constructor argument"
+
+end

--- a/src/HOL/Tools/SMT/smt_normalize.ML	Fri Sep 17 08:41:07 2010 +0200
+++ b/src/HOL/Tools/SMT/smt_normalize.ML	Fri Sep 17 10:52:35 2010 +0200
@@ -9,14 +9,16 @@
   * embed natural numbers into integers,
   * add extra rules specifying types and constants which occur frequently,
   * fully translate into object logic, add universal closure,
+  * monomorphize (create instances of schematic rules),
   * lift lambda terms,
   * make applications explicit for functions with varying number of arguments.
+  * add (hypothetical definitions for) missing datatype selectors,
 *)
 
 signature SMT_NORMALIZE =
 sig
   type extra_norm = thm list -> Proof.context -> thm list * Proof.context
-  val normalize: extra_norm -> thm list -> Proof.context ->
+  val normalize: extra_norm -> bool -> thm list -> Proof.context ->
     thm list * Proof.context
   val atomize_conv: Proof.context -> conv
   val eta_expand_conv: (Proof.context -> conv) -> Proof.context -> conv
@@ -427,13 +429,60 @@
 
 
 
+(* add missing datatype selectors via hypothetical definitions *)
+
+local
+  val add = (fn Type (n, _) => Symtab.update (n, ()) | _ => I)
+
+  fun collect t =
+    (case Term.strip_comb t of
+      (Abs (_, T, t), _) => add T #> collect t
+    | (Const (_, T), ts) => collects T ts
+    | (Free (_, T), ts) => collects T ts
+    | _ => I)
+  and collects T ts =
+    let val ((Ts, Us), U) = Term.strip_type T |> apfst (chop (length ts))
+    in fold add Ts #> add (Us ---> U) #> fold collect ts end
+
+  fun add_constructors thy n =
+    (case Datatype.get_info thy n of
+      NONE => I
+    | SOME {descr, ...} => fold (fn (_, (_, _, cs)) => fold (fn (n, ds) =>
+        fold (insert (op =) o pair n) (1 upto length ds)) cs) descr)
+
+  fun add_selector (c as (n, i)) ctxt =
+    (case Datatype_Selectors.lookup_selector ctxt c of
+      SOME _ => ctxt
+    | NONE =>
+        let
+          val T = Sign.the_const_type (ProofContext.theory_of ctxt) n
+          val U = Term.body_type T --> nth (Term.binder_types T) (i-1)
+        in
+          ctxt
+          |> yield_singleton Variable.variant_fixes Name.uu
+          |>> pair ((n, T), i) o rpair U
+          |-> Context.proof_map o Datatype_Selectors.add_selector
+        end)
+in
+
+fun datatype_selectors thms ctxt =
+  let
+    val ns = Symtab.keys (fold (collect o Thm.prop_of) thms Symtab.empty)
+    val cs = fold (add_constructors (ProofContext.theory_of ctxt)) ns []
+  in (thms, fold add_selector cs ctxt) end
+    (* FIXME: also generate hypothetical definitions for the selectors *)
+
+end
+
+
+
 (* combined normalization *)
 
 type extra_norm = thm list -> Proof.context -> thm list * Proof.context
 
 fun with_context f thms ctxt = (f ctxt thms, ctxt)
 
-fun normalize extra_norm thms ctxt =
+fun normalize extra_norm with_datatypes thms ctxt =
   thms
   |> trivial_distinct ctxt
   |> rewrite_bool_cases ctxt
@@ -445,5 +494,6 @@
   |-> SMT_Monomorph.monomorph
   |-> lift_lambdas
   |-> with_context explicit_application
+  |-> (if with_datatypes then datatype_selectors else pair)
 
 end

--- a/src/HOL/Tools/SMT/smt_solver.ML	Fri Sep 17 08:41:07 2010 +0200
+++ b/src/HOL/Tools/SMT/smt_solver.ML	Fri Sep 17 10:52:35 2010 +0200
@@ -195,9 +195,11 @@
       ("timeout: " ^ string_of_int (Config.get ctxt timeout)) ::
       "arguments:" :: arguments
     val {extra_norm, translate} = interface
+    val {builtins, ...} = translate
+    val {has_datatypes, ...} = builtins
   in
     (prems, ctxt)
-    |-> SMT_Normalize.normalize extra_norm
+    |-> SMT_Normalize.normalize extra_norm has_datatypes
     |-> invoke translate comments command arguments
     |-> reconstruct
     |-> (fn thm => fn ctxt' => thm

--- a/src/HOL/Tools/SMT/smt_translate.ML	Fri Sep 17 08:41:07 2010 +0200
+++ b/src/HOL/Tools/SMT/smt_translate.ML	Fri Sep 17 10:52:35 2010 +0200
@@ -291,28 +291,31 @@
     SOME (f, _) => (f, cx)
   | 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 mk_type (_, Tfs) (d as Datatype.DtTFree _) = the (AList.lookup (op =) Tfs d)
+  | mk_type Ts (Datatype.DtType (n, ds)) = Type (n, map (mk_type Ts) ds)
+  | mk_type (Tds, _) (Datatype.DtRec i) = nth Tds i
 
-fun inst_constructor Ts = inst_const Term.body_type Ts
-fun inst_selector Ts = inst_const Term.domain_type Ts
+fun mk_selector ctxt Ts T n (i, d) =
+  (case Datatype_Selectors.lookup_selector ctxt (n, i+1) of
+    NONE => raise Fail ("missing selector for datatype constructor " ^ quote n)
+  | SOME m => mk_type Ts d |> (fn U => (Const (m, T --> U), U)))
+
+fun mk_constructor ctxt Ts T (n, args) =
+  let val (sels, Us) = split_list (map_index (mk_selector ctxt Ts T n) args)
+  in (Const (n, Us ---> T), sels) end
 
-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 lookup_datatype ctxt n Ts = if n = @{type_name bool} then NONE else
+  (case Datatype.get_info (ProofContext.theory_of ctxt) n of
+    NONE => NONE  (* FIXME: also use Record.get_info *)
+  | SOME {descr, ...} =>
+      let
+        val Tds = map (fn (_, (tn, _, _)) => Type (tn, Ts))
+          (sort (int_ord o pairself fst) descr)
+        val Tfs = (case hd descr of (_, (_, tfs, _)) => tfs ~~ Ts)
+      in
+        SOME (descr |> map (fn (i, (_, _, cs)) =>
+          (nth Tds i, map (mk_constructor ctxt (Tds, Tfs) (nth Tds i)) cs)))
+      end)
 
 fun relaxed thms = (([], thms), map prop_of thms)