src/HOL/Tools/SMT/smt_datatypes.ML
author blanchet
Wed, 17 Sep 2014 21:35:58 +0200
changeset 58362 cf32eb8001b8
parent 58361 7f2b3b6f6ad1
child 58364 efc56d935728
permissions -rw-r--r--
register Isabelle selectors as SMT selectors when possible
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
58061
3d060f43accb renamed new SMT module from 'SMT2' to 'SMT'
blanchet
parents: 57229
diff changeset
     1
(*  Title:      HOL/Tools/SMT/smt_datatypes.ML
56078
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
     2
    Author:     Sascha Boehme, TU Muenchen
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
     3
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
     4
Collector functions for common type declarations and their representation
58361
7f2b3b6f6ad1 added codatatype support for CVC4
blanchet
parents: 58360
diff changeset
     5
as (co)algebraic datatypes.
56078
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
     6
*)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
     7
58061
3d060f43accb renamed new SMT module from 'SMT2' to 'SMT'
blanchet
parents: 57229
diff changeset
     8
signature SMT_DATATYPES =
56078
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
     9
sig
58360
dee1fd1cc631 added interface for CVC4 extensions
blanchet
parents: 58061
diff changeset
    10
  val add_decls: BNF_Util.fp_kind -> typ ->
56078
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    11
    (typ * (term * term list) list) list list * Proof.context ->
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    12
    (typ * (term * term list) list) list list * Proof.context
57229
blanchet
parents: 57226
diff changeset
    13
end;
56078
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    14
58061
3d060f43accb renamed new SMT module from 'SMT2' to 'SMT'
blanchet
parents: 57229
diff changeset
    15
structure SMT_Datatypes: SMT_DATATYPES =
56078
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    16
struct
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    17
58362
cf32eb8001b8 register Isabelle selectors as SMT selectors when possible
blanchet
parents: 58361
diff changeset
    18
fun mk_selectors T Ts sels =
cf32eb8001b8 register Isabelle selectors as SMT selectors when possible
blanchet
parents: 58361
diff changeset
    19
  if null sels then
cf32eb8001b8 register Isabelle selectors as SMT selectors when possible
blanchet
parents: 58361
diff changeset
    20
    Variable.variant_fixes (replicate (length Ts) "select")
cf32eb8001b8 register Isabelle selectors as SMT selectors when possible
blanchet
parents: 58361
diff changeset
    21
    #>> map2 (fn U => fn n => Free (n, T --> U)) Ts
cf32eb8001b8 register Isabelle selectors as SMT selectors when possible
blanchet
parents: 58361
diff changeset
    22
  else
cf32eb8001b8 register Isabelle selectors as SMT selectors when possible
blanchet
parents: 58361
diff changeset
    23
    pair sels
56078
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    24
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    25
57226
c22ad39c3b4b use 'ctr_sugar' abstraction in SMT(2)
blanchet
parents: 57213
diff changeset
    26
(* free constructor type declarations *)
56078
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    27
58362
cf32eb8001b8 register Isabelle selectors as SMT selectors when possible
blanchet
parents: 58361
diff changeset
    28
fun get_ctr_sugar_decl ({ctrs = ctrs0, selss = selss0, ...} : Ctr_Sugar.ctr_sugar) T Ts ctxt =
56078
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    29
  let
58362
cf32eb8001b8 register Isabelle selectors as SMT selectors when possible
blanchet
parents: 58361
diff changeset
    30
    fun mk_constr ctr0 sels0 =
cf32eb8001b8 register Isabelle selectors as SMT selectors when possible
blanchet
parents: 58361
diff changeset
    31
      let
cf32eb8001b8 register Isabelle selectors as SMT selectors when possible
blanchet
parents: 58361
diff changeset
    32
        val sels = map (Ctr_Sugar.mk_disc_or_sel Ts) sels0
cf32eb8001b8 register Isabelle selectors as SMT selectors when possible
blanchet
parents: 58361
diff changeset
    33
        val ctr = Ctr_Sugar.mk_ctr Ts ctr0
cf32eb8001b8 register Isabelle selectors as SMT selectors when possible
blanchet
parents: 58361
diff changeset
    34
        val binder_Ts = binder_types (fastype_of ctr)
cf32eb8001b8 register Isabelle selectors as SMT selectors when possible
blanchet
parents: 58361
diff changeset
    35
      in
cf32eb8001b8 register Isabelle selectors as SMT selectors when possible
blanchet
parents: 58361
diff changeset
    36
        mk_selectors T binder_Ts sels #>> pair ctr
57226
c22ad39c3b4b use 'ctr_sugar' abstraction in SMT(2)
blanchet
parents: 57213
diff changeset
    37
      end
58362
cf32eb8001b8 register Isabelle selectors as SMT selectors when possible
blanchet
parents: 58361
diff changeset
    38
cf32eb8001b8 register Isabelle selectors as SMT selectors when possible
blanchet
parents: 58361
diff changeset
    39
    val selss = if has_duplicates (op aconv) (flat selss0) then [] else selss0
57226
c22ad39c3b4b use 'ctr_sugar' abstraction in SMT(2)
blanchet
parents: 57213
diff changeset
    40
  in
58362
cf32eb8001b8 register Isabelle selectors as SMT selectors when possible
blanchet
parents: 58361
diff changeset
    41
    Ctr_Sugar_Util.fold_map2 mk_constr ctrs0 (Ctr_Sugar_Util.pad_list [] (length ctrs0) selss) ctxt
57226
c22ad39c3b4b use 'ctr_sugar' abstraction in SMT(2)
blanchet
parents: 57213
diff changeset
    42
    |>> (pair T #> single)
c22ad39c3b4b use 'ctr_sugar' abstraction in SMT(2)
blanchet
parents: 57213
diff changeset
    43
  end
56078
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    44
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    45
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    46
(* typedef declarations *)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    47
57213
9daec42f6784 fixed unsoundness in SMT(2) as oracle: don't register typedef Abs_x as constructor unless it is known to be injective
blanchet
parents: 56078
diff changeset
    48
fun get_typedef_decl (({Abs_name, Rep_name, abs_type, rep_type, ...}, {Abs_inverse, ...})
9daec42f6784 fixed unsoundness in SMT(2) as oracle: don't register typedef Abs_x as constructor unless it is known to be injective
blanchet
parents: 56078
diff changeset
    49
    : Typedef.info) T Ts =
9daec42f6784 fixed unsoundness in SMT(2) as oracle: don't register typedef Abs_x as constructor unless it is known to be injective
blanchet
parents: 56078
diff changeset
    50
  if can (curry (op RS) @{thm UNIV_I}) Abs_inverse then
9daec42f6784 fixed unsoundness in SMT(2) as oracle: don't register typedef Abs_x as constructor unless it is known to be injective
blanchet
parents: 56078
diff changeset
    51
    let
9daec42f6784 fixed unsoundness in SMT(2) as oracle: don't register typedef Abs_x as constructor unless it is known to be injective
blanchet
parents: 56078
diff changeset
    52
      val env = snd (Term.dest_Type abs_type) ~~ Ts
9daec42f6784 fixed unsoundness in SMT(2) as oracle: don't register typedef Abs_x as constructor unless it is known to be injective
blanchet
parents: 56078
diff changeset
    53
      val instT = Term.map_atyps (perhaps (AList.lookup (op =) env))
56078
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    54
57213
9daec42f6784 fixed unsoundness in SMT(2) as oracle: don't register typedef Abs_x as constructor unless it is known to be injective
blanchet
parents: 56078
diff changeset
    55
      val constr = Const (Abs_name, instT (rep_type --> abs_type))
9daec42f6784 fixed unsoundness in SMT(2) as oracle: don't register typedef Abs_x as constructor unless it is known to be injective
blanchet
parents: 56078
diff changeset
    56
      val select = Const (Rep_name, instT (abs_type --> rep_type))
9daec42f6784 fixed unsoundness in SMT(2) as oracle: don't register typedef Abs_x as constructor unless it is known to be injective
blanchet
parents: 56078
diff changeset
    57
    in [(T, [(constr, [select])])] end
9daec42f6784 fixed unsoundness in SMT(2) as oracle: don't register typedef Abs_x as constructor unless it is known to be injective
blanchet
parents: 56078
diff changeset
    58
  else
9daec42f6784 fixed unsoundness in SMT(2) as oracle: don't register typedef Abs_x as constructor unless it is known to be injective
blanchet
parents: 56078
diff changeset
    59
    []
56078
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    60
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    61
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    62
(* collection of declarations *)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    63
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    64
fun declared declss T = exists (exists (equal T o fst)) declss
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    65
fun declared' dss T = exists (exists (equal T o fst) o snd) dss
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    66
58361
7f2b3b6f6ad1 added codatatype support for CVC4
blanchet
parents: 58360
diff changeset
    67
(* Simplification: We assume that every type that is not a codatatype is a datatype (or a
7f2b3b6f6ad1 added codatatype support for CVC4
blanchet
parents: 58360
diff changeset
    68
   record). *)
7f2b3b6f6ad1 added codatatype support for CVC4
blanchet
parents: 58360
diff changeset
    69
fun fp_kind_of ctxt n =
7f2b3b6f6ad1 added codatatype support for CVC4
blanchet
parents: 58360
diff changeset
    70
  (case BNF_FP_Def_Sugar.fp_sugar_of ctxt n of
7f2b3b6f6ad1 added codatatype support for CVC4
blanchet
parents: 58360
diff changeset
    71
    SOME {fp, ...} => fp
7f2b3b6f6ad1 added codatatype support for CVC4
blanchet
parents: 58360
diff changeset
    72
  | NONE => BNF_Util.Least_FP)
7f2b3b6f6ad1 added codatatype support for CVC4
blanchet
parents: 58360
diff changeset
    73
7f2b3b6f6ad1 added codatatype support for CVC4
blanchet
parents: 58360
diff changeset
    74
fun get_decls fp T n Ts ctxt =
7f2b3b6f6ad1 added codatatype support for CVC4
blanchet
parents: 58360
diff changeset
    75
  let
7f2b3b6f6ad1 added codatatype support for CVC4
blanchet
parents: 58360
diff changeset
    76
    fun fallback () =
57226
c22ad39c3b4b use 'ctr_sugar' abstraction in SMT(2)
blanchet
parents: 57213
diff changeset
    77
      (case Typedef.get_info ctxt n of
c22ad39c3b4b use 'ctr_sugar' abstraction in SMT(2)
blanchet
parents: 57213
diff changeset
    78
        [] => ([], ctxt)
58361
7f2b3b6f6ad1 added codatatype support for CVC4
blanchet
parents: 58360
diff changeset
    79
      | info :: _ => (get_typedef_decl info T Ts, ctxt))
7f2b3b6f6ad1 added codatatype support for CVC4
blanchet
parents: 58360
diff changeset
    80
  in
7f2b3b6f6ad1 added codatatype support for CVC4
blanchet
parents: 58360
diff changeset
    81
    (case Ctr_Sugar.ctr_sugar_of ctxt n of
7f2b3b6f6ad1 added codatatype support for CVC4
blanchet
parents: 58360
diff changeset
    82
      SOME ctr_sugar =>
7f2b3b6f6ad1 added codatatype support for CVC4
blanchet
parents: 58360
diff changeset
    83
      if fp_kind_of ctxt n = fp then get_ctr_sugar_decl ctr_sugar T Ts ctxt else fallback ()
7f2b3b6f6ad1 added codatatype support for CVC4
blanchet
parents: 58360
diff changeset
    84
    | NONE => fallback ())
7f2b3b6f6ad1 added codatatype support for CVC4
blanchet
parents: 58360
diff changeset
    85
  end
56078
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    86
58360
dee1fd1cc631 added interface for CVC4 extensions
blanchet
parents: 58061
diff changeset
    87
fun add_decls fp T (declss, ctxt) =
56078
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    88
  let
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    89
    fun depends Ts ds = exists (member (op =) (map fst ds)) Ts
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    90
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    91
    fun add (TFree _) = I
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    92
      | add (TVar _) = I
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    93
      | add (T as Type (@{type_name fun}, _)) =
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    94
          fold add (Term.body_type T :: Term.binder_types T)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    95
      | add @{typ bool} = I
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    96
      | add (T as Type (n, Ts)) = (fn (dss, ctxt1) =>
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    97
          if declared declss T orelse declared' dss T then (dss, ctxt1)
58061
3d060f43accb renamed new SMT module from 'SMT2' to 'SMT'
blanchet
parents: 57229
diff changeset
    98
          else if SMT_Builtin.is_builtin_typ_ext ctxt1 T then (dss, ctxt1)
56078
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    99
          else
58361
7f2b3b6f6ad1 added codatatype support for CVC4
blanchet
parents: 58360
diff changeset
   100
            (case get_decls fp T n Ts ctxt1 of
56078
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   101
              ([], _) => (dss, ctxt1)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   102
            | (ds, ctxt2) =>
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   103
                let
57226
c22ad39c3b4b use 'ctr_sugar' abstraction in SMT(2)
blanchet
parents: 57213
diff changeset
   104
                  val constrTs = maps (map (snd o Term.dest_Const o fst) o snd) ds
56078
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   105
                  val Us = fold (union (op =) o Term.binder_types) constrTs []
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   106
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   107
                  fun ins [] = [(Us, ds)]
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   108
                    | ins ((Uds as (Us', _)) :: Udss) =
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   109
                        if depends Us' ds then (Us, ds) :: Uds :: Udss
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   110
                        else Uds :: ins Udss
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   111
            in fold add Us (ins dss, ctxt2) end))
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   112
  in add T ([], ctxt) |>> append declss o map snd end
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   113
57229
blanchet
parents: 57226
diff changeset
   114
end;