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
authorboehmes
Fri Sep 17 10:52:35 2010 +0200 (2010-09-17)
changeset 394839f0e5684f04b
parent 39482 1c37d19e3d58
child 39488 742435a3a992
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
src/HOL/IsaMakefile
src/HOL/SMT.thy
src/HOL/SMT_Examples/SMT_Tests.thy
src/HOL/Tools/Datatype/datatype_selectors.ML
src/HOL/Tools/SMT/smt_normalize.ML
src/HOL/Tools/SMT/smt_solver.ML
src/HOL/Tools/SMT/smt_translate.ML
     1.1 --- a/src/HOL/IsaMakefile	Fri Sep 17 08:41:07 2010 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Fri Sep 17 10:52:35 2010 +0200
     1.3 @@ -271,6 +271,7 @@
     1.4    Tools/ATP/atp_proof.ML \
     1.5    Tools/ATP/atp_systems.ML \
     1.6    Tools/choice_specification.ML \
     1.7 +  Tools/Datatype/datatype_selectors.ML \
     1.8    Tools/int_arith.ML \
     1.9    Tools/groebner.ML \
    1.10    Tools/list_code.ML \
     2.1 --- a/src/HOL/SMT.thy	Fri Sep 17 08:41:07 2010 +0200
     2.2 +++ b/src/HOL/SMT.thy	Fri Sep 17 10:52:35 2010 +0200
     2.3 @@ -7,6 +7,7 @@
     2.4  theory SMT
     2.5  imports List
     2.6  uses
     2.7 +  "Tools/Datatype/datatype_selectors.ML"
     2.8    ("Tools/SMT/smt_monomorph.ML")
     2.9    ("Tools/SMT/smt_normalize.ML")
    2.10    ("Tools/SMT/smt_translate.ML")
    2.11 @@ -323,4 +324,13 @@
    2.12  hide_const Pattern term_eq
    2.13  hide_const (open) trigger pat nopat fun_app z3div z3mod
    2.14  
    2.15 +
    2.16 +
    2.17 +subsection {* Selectors for datatypes *}
    2.18 +
    2.19 +setup {* Datatype_Selectors.setup *}
    2.20 +
    2.21 +declare [[ selector Pair 1 = fst, selector Pair 2 = snd ]]
    2.22 +declare [[ selector Cons 1 = hd, selector Cons 2 = tl ]]
    2.23 +
    2.24  end
     3.1 --- a/src/HOL/SMT_Examples/SMT_Tests.thy	Fri Sep 17 08:41:07 2010 +0200
     3.2 +++ b/src/HOL/SMT_Examples/SMT_Tests.thy	Fri Sep 17 10:52:35 2010 +0200
     3.3 @@ -607,7 +607,7 @@
     3.4  
     3.5  
     3.6  
     3.7 -section {* Pairs *}
     3.8 +section {* Pairs *}  (* FIXME: tests for datatypes and records *)
     3.9  
    3.10  lemma
    3.11    "x = fst (x, y)"
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/HOL/Tools/Datatype/datatype_selectors.ML	Fri Sep 17 10:52:35 2010 +0200
     4.3 @@ -0,0 +1,83 @@
     4.4 +(*  Title:      HOL/Tools/Datatype/datatype_selectors.ML
     4.5 +    Author:     Sascha Boehme, TU Muenchen
     4.6 +
     4.7 +Selector functions for datatype constructor arguments.
     4.8 +*)
     4.9 +
    4.10 +signature DATATYPE_SELECTORS =
    4.11 +sig
    4.12 +  val add_selector: ((string * typ) * int) * (string * typ) ->
    4.13 +    Context.generic -> Context.generic
    4.14 +  val lookup_selector: Proof.context -> string * int -> string option
    4.15 +  val setup: theory -> theory
    4.16 +end
    4.17 +
    4.18 +structure Datatype_Selectors: DATATYPE_SELECTORS =
    4.19 +struct
    4.20 +
    4.21 +structure Stringinttab = Table
    4.22 +(
    4.23 +  type key = string * int
    4.24 +  val ord = prod_ord fast_string_ord int_ord
    4.25 +)
    4.26 +
    4.27 +structure Data = Generic_Data
    4.28 +(
    4.29 +  type T = string Stringinttab.table
    4.30 +  val empty = Stringinttab.empty
    4.31 +  val extend = I
    4.32 +  val merge = Stringinttab.merge (K true)
    4.33 +)
    4.34 +
    4.35 +fun pretty_term context = Syntax.pretty_term (Context.proof_of context)
    4.36 +
    4.37 +fun sanity_check context (((con as (n, _), i), sel as (m, _))) =
    4.38 +  let
    4.39 +    val thy = Context.theory_of context
    4.40 +    val varify_const =
    4.41 +      Const #> Type.varify_global [] #> snd #> Term.dest_Const #>
    4.42 +      snd #> Term.strip_type
    4.43 +
    4.44 +    val (Ts, T) = varify_const con
    4.45 +    val (Us, U) = varify_const sel
    4.46 +    val _ = (0 < i andalso i <= length Ts) orelse
    4.47 +      error (Pretty.string_of (Pretty.block [
    4.48 +        Pretty.str "The constructor ",
    4.49 +        Pretty.quote (pretty_term context (Const con)),
    4.50 +        Pretty.str " has no argument position ",
    4.51 +        Pretty.str (string_of_int i),
    4.52 +        Pretty.str "."]))
    4.53 +    val _ = length Us = 1 orelse
    4.54 +      error (Pretty.string_of (Pretty.block [
    4.55 +        Pretty.str "The term ", Pretty.quote (pretty_term context (Const sel)),
    4.56 +        Pretty.str " might not be a selector ",
    4.57 +        Pretty.str "(it accepts more than one argument)."]))
    4.58 +    val _ =
    4.59 +     (Sign.typ_equiv thy (T, hd Us) andalso
    4.60 +      Sign.typ_equiv thy (nth Ts (i-1), U)) orelse
    4.61 +      error (Pretty.string_of (Pretty.block [
    4.62 +        Pretty.str "The types of the constructor ",
    4.63 +        Pretty.quote (pretty_term context (Const con)),
    4.64 +        Pretty.str " and of the selector ",
    4.65 +        Pretty.quote (pretty_term context (Const sel)),
    4.66 +        Pretty.str " do not fit to each other."]))
    4.67 +  in ((n, i), m) end
    4.68 +
    4.69 +fun add_selector (entry as ((con as (n, _), i), (_, T))) context =
    4.70 +  (case Stringinttab.lookup (Data.get context) (n, i) of
    4.71 +    NONE => Data.map (Stringinttab.update (sanity_check context entry)) context
    4.72 +  | SOME c => error (Pretty.string_of (Pretty.block [
    4.73 +      Pretty.str "There is already a selector assigned to constructor ",
    4.74 +      Pretty.quote (pretty_term context (Const con)), Pretty.str ", namely ",
    4.75 +      Pretty.quote (pretty_term context (Const (c, T))), Pretty.str "."])))
    4.76 +
    4.77 +fun lookup_selector ctxt = Stringinttab.lookup (Data.get (Context.Proof ctxt))
    4.78 +
    4.79 +val setup =
    4.80 +  Attrib.setup @{binding selector}
    4.81 +   ((Args.term >> Term.dest_Const) -- Scan.lift (Parse.nat) --|
    4.82 +    Scan.lift (Parse.$$$ "=") -- (Args.term >> Term.dest_Const) >>
    4.83 +    (Thm.declaration_attribute o K o add_selector))
    4.84 +  "assign a selector function to a datatype constructor argument"
    4.85 +
    4.86 +end
     5.1 --- a/src/HOL/Tools/SMT/smt_normalize.ML	Fri Sep 17 08:41:07 2010 +0200
     5.2 +++ b/src/HOL/Tools/SMT/smt_normalize.ML	Fri Sep 17 10:52:35 2010 +0200
     5.3 @@ -9,14 +9,16 @@
     5.4    * embed natural numbers into integers,
     5.5    * add extra rules specifying types and constants which occur frequently,
     5.6    * fully translate into object logic, add universal closure,
     5.7 +  * monomorphize (create instances of schematic rules),
     5.8    * lift lambda terms,
     5.9    * make applications explicit for functions with varying number of arguments.
    5.10 +  * add (hypothetical definitions for) missing datatype selectors,
    5.11  *)
    5.12  
    5.13  signature SMT_NORMALIZE =
    5.14  sig
    5.15    type extra_norm = thm list -> Proof.context -> thm list * Proof.context
    5.16 -  val normalize: extra_norm -> thm list -> Proof.context ->
    5.17 +  val normalize: extra_norm -> bool -> thm list -> Proof.context ->
    5.18      thm list * Proof.context
    5.19    val atomize_conv: Proof.context -> conv
    5.20    val eta_expand_conv: (Proof.context -> conv) -> Proof.context -> conv
    5.21 @@ -427,13 +429,60 @@
    5.22  
    5.23  
    5.24  
    5.25 +(* add missing datatype selectors via hypothetical definitions *)
    5.26 +
    5.27 +local
    5.28 +  val add = (fn Type (n, _) => Symtab.update (n, ()) | _ => I)
    5.29 +
    5.30 +  fun collect t =
    5.31 +    (case Term.strip_comb t of
    5.32 +      (Abs (_, T, t), _) => add T #> collect t
    5.33 +    | (Const (_, T), ts) => collects T ts
    5.34 +    | (Free (_, T), ts) => collects T ts
    5.35 +    | _ => I)
    5.36 +  and collects T ts =
    5.37 +    let val ((Ts, Us), U) = Term.strip_type T |> apfst (chop (length ts))
    5.38 +    in fold add Ts #> add (Us ---> U) #> fold collect ts end
    5.39 +
    5.40 +  fun add_constructors thy n =
    5.41 +    (case Datatype.get_info thy n of
    5.42 +      NONE => I
    5.43 +    | SOME {descr, ...} => fold (fn (_, (_, _, cs)) => fold (fn (n, ds) =>
    5.44 +        fold (insert (op =) o pair n) (1 upto length ds)) cs) descr)
    5.45 +
    5.46 +  fun add_selector (c as (n, i)) ctxt =
    5.47 +    (case Datatype_Selectors.lookup_selector ctxt c of
    5.48 +      SOME _ => ctxt
    5.49 +    | NONE =>
    5.50 +        let
    5.51 +          val T = Sign.the_const_type (ProofContext.theory_of ctxt) n
    5.52 +          val U = Term.body_type T --> nth (Term.binder_types T) (i-1)
    5.53 +        in
    5.54 +          ctxt
    5.55 +          |> yield_singleton Variable.variant_fixes Name.uu
    5.56 +          |>> pair ((n, T), i) o rpair U
    5.57 +          |-> Context.proof_map o Datatype_Selectors.add_selector
    5.58 +        end)
    5.59 +in
    5.60 +
    5.61 +fun datatype_selectors thms ctxt =
    5.62 +  let
    5.63 +    val ns = Symtab.keys (fold (collect o Thm.prop_of) thms Symtab.empty)
    5.64 +    val cs = fold (add_constructors (ProofContext.theory_of ctxt)) ns []
    5.65 +  in (thms, fold add_selector cs ctxt) end
    5.66 +    (* FIXME: also generate hypothetical definitions for the selectors *)
    5.67 +
    5.68 +end
    5.69 +
    5.70 +
    5.71 +
    5.72  (* combined normalization *)
    5.73  
    5.74  type extra_norm = thm list -> Proof.context -> thm list * Proof.context
    5.75  
    5.76  fun with_context f thms ctxt = (f ctxt thms, ctxt)
    5.77  
    5.78 -fun normalize extra_norm thms ctxt =
    5.79 +fun normalize extra_norm with_datatypes thms ctxt =
    5.80    thms
    5.81    |> trivial_distinct ctxt
    5.82    |> rewrite_bool_cases ctxt
    5.83 @@ -445,5 +494,6 @@
    5.84    |-> SMT_Monomorph.monomorph
    5.85    |-> lift_lambdas
    5.86    |-> with_context explicit_application
    5.87 +  |-> (if with_datatypes then datatype_selectors else pair)
    5.88  
    5.89  end
     6.1 --- a/src/HOL/Tools/SMT/smt_solver.ML	Fri Sep 17 08:41:07 2010 +0200
     6.2 +++ b/src/HOL/Tools/SMT/smt_solver.ML	Fri Sep 17 10:52:35 2010 +0200
     6.3 @@ -195,9 +195,11 @@
     6.4        ("timeout: " ^ string_of_int (Config.get ctxt timeout)) ::
     6.5        "arguments:" :: arguments
     6.6      val {extra_norm, translate} = interface
     6.7 +    val {builtins, ...} = translate
     6.8 +    val {has_datatypes, ...} = builtins
     6.9    in
    6.10      (prems, ctxt)
    6.11 -    |-> SMT_Normalize.normalize extra_norm
    6.12 +    |-> SMT_Normalize.normalize extra_norm has_datatypes
    6.13      |-> invoke translate comments command arguments
    6.14      |-> reconstruct
    6.15      |-> (fn thm => fn ctxt' => thm
     7.1 --- a/src/HOL/Tools/SMT/smt_translate.ML	Fri Sep 17 08:41:07 2010 +0200
     7.2 +++ b/src/HOL/Tools/SMT/smt_translate.ML	Fri Sep 17 10:52:35 2010 +0200
     7.3 @@ -291,28 +291,31 @@
     7.4      SOME (f, _) => (f, cx)
     7.5    | NONE => new_fun func_prefix t ss cx)
     7.6  
     7.7 -fun inst_const f Ts t =
     7.8 -  let
     7.9 -    val (n, T) = Term.dest_Const (snd (Type.varify_global [] t))
    7.10 -    val inst = map Term.dest_TVar (snd (Term.dest_Type (f T))) ~~ Ts
    7.11 -  in Const (n, Term_Subst.instantiateT inst T) end
    7.12 +fun mk_type (_, Tfs) (d as Datatype.DtTFree _) = the (AList.lookup (op =) Tfs d)
    7.13 +  | mk_type Ts (Datatype.DtType (n, ds)) = Type (n, map (mk_type Ts) ds)
    7.14 +  | mk_type (Tds, _) (Datatype.DtRec i) = nth Tds i
    7.15  
    7.16 -fun inst_constructor Ts = inst_const Term.body_type Ts
    7.17 -fun inst_selector Ts = inst_const Term.domain_type Ts
    7.18 +fun mk_selector ctxt Ts T n (i, d) =
    7.19 +  (case Datatype_Selectors.lookup_selector ctxt (n, i+1) of
    7.20 +    NONE => raise Fail ("missing selector for datatype constructor " ^ quote n)
    7.21 +  | SOME m => mk_type Ts d |> (fn U => (Const (m, T --> U), U)))
    7.22 +
    7.23 +fun mk_constructor ctxt Ts T (n, args) =
    7.24 +  let val (sels, Us) = split_list (map_index (mk_selector ctxt Ts T n) args)
    7.25 +  in (Const (n, Us ---> T), sels) end
    7.26  
    7.27 -fun lookup_datatype ctxt n Ts = (* FIXME: use Datatype/Record.get_info *)
    7.28 -  if n = @{type_name prod}
    7.29 -  then SOME [
    7.30 -    (Type (n, Ts), [
    7.31 -      (inst_constructor Ts @{term Pair},
    7.32 -        map (inst_selector Ts) [@{term fst}, @{term snd}])])]
    7.33 -  else if n = @{type_name list}
    7.34 -  then SOME [
    7.35 -    (Type (n, Ts), [
    7.36 -      (inst_constructor Ts @{term Nil}, []),
    7.37 -      (inst_constructor Ts @{term Cons},
    7.38 -        map (inst_selector Ts) [@{term hd}, @{term tl}])])]
    7.39 -  else NONE
    7.40 +fun lookup_datatype ctxt n Ts = if n = @{type_name bool} then NONE else
    7.41 +  (case Datatype.get_info (ProofContext.theory_of ctxt) n of
    7.42 +    NONE => NONE  (* FIXME: also use Record.get_info *)
    7.43 +  | SOME {descr, ...} =>
    7.44 +      let
    7.45 +        val Tds = map (fn (_, (tn, _, _)) => Type (tn, Ts))
    7.46 +          (sort (int_ord o pairself fst) descr)
    7.47 +        val Tfs = (case hd descr of (_, (_, tfs, _)) => tfs ~~ Ts)
    7.48 +      in
    7.49 +        SOME (descr |> map (fn (i, (_, _, cs)) =>
    7.50 +          (nth Tds i, map (mk_constructor ctxt (Tds, Tfs) (nth Tds i)) cs)))
    7.51 +      end)
    7.52  
    7.53  fun relaxed thms = (([], thms), map prop_of thms)
    7.54