src/HOL/Library/Old_SMT/old_smt_builtin.ML
author wenzelm
Wed, 08 Mar 2017 10:50:59 +0100
changeset 65151 a7394aa4d21c
parent 58058 1a0b18176548
permissions -rw-r--r--
tuned proofs;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
     1
(*  Title:      HOL/Library/Old_SMT/old_smt_builtin.ML
40277
4e3a3461c1a6 added crafted list of SMT built-in constants
boehmes
parents:
diff changeset
     2
    Author:     Sascha Boehme, TU Muenchen
4e3a3461c1a6 added crafted list of SMT built-in constants
boehmes
parents:
diff changeset
     3
41059
d2b1fc1b8e19 centralized handling of built-in types and constants;
boehmes
parents: 40691
diff changeset
     4
Tables of types and terms directly supported by SMT solvers.
40277
4e3a3461c1a6 added crafted list of SMT built-in constants
boehmes
parents:
diff changeset
     5
*)
4e3a3461c1a6 added crafted list of SMT built-in constants
boehmes
parents:
diff changeset
     6
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
     7
signature OLD_SMT_BUILTIN =
40277
4e3a3461c1a6 added crafted list of SMT built-in constants
boehmes
parents:
diff changeset
     8
sig
53999
ba9254f3111b added possibility to reset builtins (for experimentation)
blanchet
parents: 53998
diff changeset
     9
  (*for experiments*)
54000
9cfff7f61d0d added experimental configuration options to tune use of builtin symbols in SMT
blanchet
parents: 53999
diff changeset
    10
  val filter_builtins: (typ -> bool) -> Proof.context -> Proof.context
53999
ba9254f3111b added possibility to reset builtins (for experimentation)
blanchet
parents: 53998
diff changeset
    11
41059
d2b1fc1b8e19 centralized handling of built-in types and constants;
boehmes
parents: 40691
diff changeset
    12
  (*built-in types*)
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
    13
  val add_builtin_typ: Old_SMT_Utils.class ->
41072
9f9bc1bdacef be more flexible: store SMT built-in symbols in generic contexts (not in theory contexts)
boehmes
parents: 41059
diff changeset
    14
    typ * (typ -> string option) * (typ -> int -> string option) ->
9f9bc1bdacef be more flexible: store SMT built-in symbols in generic contexts (not in theory contexts)
boehmes
parents: 41059
diff changeset
    15
    Context.generic -> Context.generic
9f9bc1bdacef be more flexible: store SMT built-in symbols in generic contexts (not in theory contexts)
boehmes
parents: 41059
diff changeset
    16
  val add_builtin_typ_ext: typ * (typ -> bool) -> Context.generic ->
9f9bc1bdacef be more flexible: store SMT built-in symbols in generic contexts (not in theory contexts)
boehmes
parents: 41059
diff changeset
    17
    Context.generic
41281
679118e35378 removed odd decoration of built-in symbols as Vars (instead provide built-in desctructor functions along with their inverse functions);
boehmes
parents: 41280
diff changeset
    18
  val dest_builtin_typ: Proof.context -> typ -> string option
41059
d2b1fc1b8e19 centralized handling of built-in types and constants;
boehmes
parents: 40691
diff changeset
    19
  val is_builtin_typ_ext: Proof.context -> typ -> bool
d2b1fc1b8e19 centralized handling of built-in types and constants;
boehmes
parents: 40691
diff changeset
    20
d2b1fc1b8e19 centralized handling of built-in types and constants;
boehmes
parents: 40691
diff changeset
    21
  (*built-in numbers*)
41281
679118e35378 removed odd decoration of built-in symbols as Vars (instead provide built-in desctructor functions along with their inverse functions);
boehmes
parents: 41280
diff changeset
    22
  val dest_builtin_num: Proof.context -> term -> (string * typ) option
41059
d2b1fc1b8e19 centralized handling of built-in types and constants;
boehmes
parents: 40691
diff changeset
    23
  val is_builtin_num: Proof.context -> term -> bool
d2b1fc1b8e19 centralized handling of built-in types and constants;
boehmes
parents: 40691
diff changeset
    24
  val is_builtin_num_ext: Proof.context -> term -> bool
d2b1fc1b8e19 centralized handling of built-in types and constants;
boehmes
parents: 40691
diff changeset
    25
d2b1fc1b8e19 centralized handling of built-in types and constants;
boehmes
parents: 40691
diff changeset
    26
  (*built-in functions*)
d2b1fc1b8e19 centralized handling of built-in types and constants;
boehmes
parents: 40691
diff changeset
    27
  type 'a bfun = Proof.context -> typ -> term list -> 'a
41281
679118e35378 removed odd decoration of built-in symbols as Vars (instead provide built-in desctructor functions along with their inverse functions);
boehmes
parents: 41280
diff changeset
    28
  type bfunr = string * int * term list * (term list -> term)
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
    29
  val add_builtin_fun: Old_SMT_Utils.class ->
41281
679118e35378 removed odd decoration of built-in symbols as Vars (instead provide built-in desctructor functions along with their inverse functions);
boehmes
parents: 41280
diff changeset
    30
    (string * typ) * bfunr option bfun -> Context.generic -> Context.generic
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
    31
  val add_builtin_fun': Old_SMT_Utils.class -> term * string -> Context.generic ->
41072
9f9bc1bdacef be more flexible: store SMT built-in symbols in generic contexts (not in theory contexts)
boehmes
parents: 41059
diff changeset
    32
    Context.generic
41354
0abe5db19f3a also provide a view on arguments for "external" built-in symbols (similar to "internal" (real) built-in symbols)
boehmes
parents: 41336
diff changeset
    33
  val add_builtin_fun_ext: (string * typ) * term list bfun ->
0abe5db19f3a also provide a view on arguments for "external" built-in symbols (similar to "internal" (real) built-in symbols)
boehmes
parents: 41336
diff changeset
    34
    Context.generic -> Context.generic
41072
9f9bc1bdacef be more flexible: store SMT built-in symbols in generic contexts (not in theory contexts)
boehmes
parents: 41059
diff changeset
    35
  val add_builtin_fun_ext': string * typ -> Context.generic -> Context.generic
9f9bc1bdacef be more flexible: store SMT built-in symbols in generic contexts (not in theory contexts)
boehmes
parents: 41059
diff changeset
    36
  val add_builtin_fun_ext'': string -> Context.generic -> Context.generic
41281
679118e35378 removed odd decoration of built-in symbols as Vars (instead provide built-in desctructor functions along with their inverse functions);
boehmes
parents: 41280
diff changeset
    37
  val dest_builtin_fun: Proof.context -> string * typ -> term list ->
679118e35378 removed odd decoration of built-in symbols as Vars (instead provide built-in desctructor functions along with their inverse functions);
boehmes
parents: 41280
diff changeset
    38
    bfunr option
679118e35378 removed odd decoration of built-in symbols as Vars (instead provide built-in desctructor functions along with their inverse functions);
boehmes
parents: 41280
diff changeset
    39
  val dest_builtin_eq: Proof.context -> term -> term -> bfunr option
679118e35378 removed odd decoration of built-in symbols as Vars (instead provide built-in desctructor functions along with their inverse functions);
boehmes
parents: 41280
diff changeset
    40
  val dest_builtin_pred: Proof.context -> string * typ -> term list ->
679118e35378 removed odd decoration of built-in symbols as Vars (instead provide built-in desctructor functions along with their inverse functions);
boehmes
parents: 41280
diff changeset
    41
    bfunr option
679118e35378 removed odd decoration of built-in symbols as Vars (instead provide built-in desctructor functions along with their inverse functions);
boehmes
parents: 41280
diff changeset
    42
  val dest_builtin_conn: Proof.context -> string * typ -> term list ->
679118e35378 removed odd decoration of built-in symbols as Vars (instead provide built-in desctructor functions along with their inverse functions);
boehmes
parents: 41280
diff changeset
    43
    bfunr option
679118e35378 removed odd decoration of built-in symbols as Vars (instead provide built-in desctructor functions along with their inverse functions);
boehmes
parents: 41280
diff changeset
    44
  val dest_builtin: Proof.context -> string * typ -> term list -> bfunr option
41354
0abe5db19f3a also provide a view on arguments for "external" built-in symbols (similar to "internal" (real) built-in symbols)
boehmes
parents: 41336
diff changeset
    45
  val dest_builtin_ext: Proof.context -> string * typ -> term list ->
0abe5db19f3a also provide a view on arguments for "external" built-in symbols (similar to "internal" (real) built-in symbols)
boehmes
parents: 41336
diff changeset
    46
    term list option
41059
d2b1fc1b8e19 centralized handling of built-in types and constants;
boehmes
parents: 40691
diff changeset
    47
  val is_builtin_fun: Proof.context -> string * typ -> term list -> bool
41126
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41124
diff changeset
    48
  val is_builtin_fun_ext: Proof.context -> string * typ -> term list -> bool
40277
4e3a3461c1a6 added crafted list of SMT built-in constants
boehmes
parents:
diff changeset
    49
end
4e3a3461c1a6 added crafted list of SMT built-in constants
boehmes
parents:
diff changeset
    50
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
    51
structure Old_SMT_Builtin: OLD_SMT_BUILTIN =
40277
4e3a3461c1a6 added crafted list of SMT built-in constants
boehmes
parents:
diff changeset
    52
struct
4e3a3461c1a6 added crafted list of SMT built-in constants
boehmes
parents:
diff changeset
    53
41059
d2b1fc1b8e19 centralized handling of built-in types and constants;
boehmes
parents: 40691
diff changeset
    54
d2b1fc1b8e19 centralized handling of built-in types and constants;
boehmes
parents: 40691
diff changeset
    55
(* built-in tables *)
d2b1fc1b8e19 centralized handling of built-in types and constants;
boehmes
parents: 40691
diff changeset
    56
d2b1fc1b8e19 centralized handling of built-in types and constants;
boehmes
parents: 40691
diff changeset
    57
datatype ('a, 'b) kind = Ext of 'a | Int of 'b
d2b1fc1b8e19 centralized handling of built-in types and constants;
boehmes
parents: 40691
diff changeset
    58
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
    59
type ('a, 'b) ttab = ((typ * ('a, 'b) kind) Ord_List.T) Old_SMT_Utils.dict 
40677
f5caf58e9cdb more precise characterization of built-in constants "number_of", "0", and "1"
blanchet
parents: 40664
diff changeset
    60
41059
d2b1fc1b8e19 centralized handling of built-in types and constants;
boehmes
parents: 40691
diff changeset
    61
fun typ_ord ((T, _), (U, _)) =
d2b1fc1b8e19 centralized handling of built-in types and constants;
boehmes
parents: 40691
diff changeset
    62
  let
d2b1fc1b8e19 centralized handling of built-in types and constants;
boehmes
parents: 40691
diff changeset
    63
    fun tord (TVar _, Type _) = GREATER
d2b1fc1b8e19 centralized handling of built-in types and constants;
boehmes
parents: 40691
diff changeset
    64
      | tord (Type _, TVar _) = LESS
d2b1fc1b8e19 centralized handling of built-in types and constants;
boehmes
parents: 40691
diff changeset
    65
      | tord (Type (n, Ts), Type (m, Us)) =
d2b1fc1b8e19 centralized handling of built-in types and constants;
boehmes
parents: 40691
diff changeset
    66
          if n = m then list_ord tord (Ts, Us)
d2b1fc1b8e19 centralized handling of built-in types and constants;
boehmes
parents: 40691
diff changeset
    67
          else Term_Ord.typ_ord (T, U)
d2b1fc1b8e19 centralized handling of built-in types and constants;
boehmes
parents: 40691
diff changeset
    68
      | tord TU = Term_Ord.typ_ord TU
d2b1fc1b8e19 centralized handling of built-in types and constants;
boehmes
parents: 40691
diff changeset
    69
  in tord (T, U) end
40277
4e3a3461c1a6 added crafted list of SMT built-in constants
boehmes
parents:
diff changeset
    70
41059
d2b1fc1b8e19 centralized handling of built-in types and constants;
boehmes
parents: 40691
diff changeset
    71
fun insert_ttab cs T f =
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
    72
  Old_SMT_Utils.dict_map_default (cs, [])
41059
d2b1fc1b8e19 centralized handling of built-in types and constants;
boehmes
parents: 40691
diff changeset
    73
    (Ord_List.insert typ_ord (perhaps (try Logic.varifyT_global) T, f))
d2b1fc1b8e19 centralized handling of built-in types and constants;
boehmes
parents: 40691
diff changeset
    74
d2b1fc1b8e19 centralized handling of built-in types and constants;
boehmes
parents: 40691
diff changeset
    75
fun merge_ttab ttabp =
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
    76
  Old_SMT_Utils.dict_merge (Ord_List.merge typ_ord) ttabp
40277
4e3a3461c1a6 added crafted list of SMT built-in constants
boehmes
parents:
diff changeset
    77
41059
d2b1fc1b8e19 centralized handling of built-in types and constants;
boehmes
parents: 40691
diff changeset
    78
fun lookup_ttab ctxt ttab T =
42361
23f352990944 modernized structure Proof_Context;
wenzelm
parents: 41473
diff changeset
    79
  let fun match (U, _) = Sign.typ_instance (Proof_Context.theory_of ctxt) (T, U)
41124
1de17a2de5ad moved SMT classes and dictionary functions to SMT_Utils
boehmes
parents: 41073
diff changeset
    80
  in
41328
6792a5c92a58 avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents: 41281
diff changeset
    81
    get_first (find_first match)
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
    82
      (Old_SMT_Utils.dict_lookup ttab (Old_SMT_Config.solver_class_of ctxt))
41124
1de17a2de5ad moved SMT classes and dictionary functions to SMT_Utils
boehmes
parents: 41073
diff changeset
    83
  end
41059
d2b1fc1b8e19 centralized handling of built-in types and constants;
boehmes
parents: 40691
diff changeset
    84
d2b1fc1b8e19 centralized handling of built-in types and constants;
boehmes
parents: 40691
diff changeset
    85
type ('a, 'b) btab = ('a, 'b) ttab Symtab.table
d2b1fc1b8e19 centralized handling of built-in types and constants;
boehmes
parents: 40691
diff changeset
    86
d2b1fc1b8e19 centralized handling of built-in types and constants;
boehmes
parents: 40691
diff changeset
    87
fun insert_btab cs n T f =
d2b1fc1b8e19 centralized handling of built-in types and constants;
boehmes
parents: 40691
diff changeset
    88
  Symtab.map_default (n, []) (insert_ttab cs T f)
d2b1fc1b8e19 centralized handling of built-in types and constants;
boehmes
parents: 40691
diff changeset
    89
d2b1fc1b8e19 centralized handling of built-in types and constants;
boehmes
parents: 40691
diff changeset
    90
fun merge_btab btabp = Symtab.join (K merge_ttab) btabp
40277
4e3a3461c1a6 added crafted list of SMT built-in constants
boehmes
parents:
diff changeset
    91
41059
d2b1fc1b8e19 centralized handling of built-in types and constants;
boehmes
parents: 40691
diff changeset
    92
fun lookup_btab ctxt btab (n, T) =
d2b1fc1b8e19 centralized handling of built-in types and constants;
boehmes
parents: 40691
diff changeset
    93
  (case Symtab.lookup btab n of
d2b1fc1b8e19 centralized handling of built-in types and constants;
boehmes
parents: 40691
diff changeset
    94
    NONE => NONE
d2b1fc1b8e19 centralized handling of built-in types and constants;
boehmes
parents: 40691
diff changeset
    95
  | SOME ttab => lookup_ttab ctxt ttab T)
40277
4e3a3461c1a6 added crafted list of SMT built-in constants
boehmes
parents:
diff changeset
    96
53998
b352d3d4a58a just one data slot (record) per program unit
blanchet
parents: 46042
diff changeset
    97
type 'a bfun = Proof.context -> typ -> term list -> 'a
b352d3d4a58a just one data slot (record) per program unit
blanchet
parents: 46042
diff changeset
    98
b352d3d4a58a just one data slot (record) per program unit
blanchet
parents: 46042
diff changeset
    99
type bfunr = string * int * term list * (term list -> term)
b352d3d4a58a just one data slot (record) per program unit
blanchet
parents: 46042
diff changeset
   100
b352d3d4a58a just one data slot (record) per program unit
blanchet
parents: 46042
diff changeset
   101
structure Builtins = Generic_Data
b352d3d4a58a just one data slot (record) per program unit
blanchet
parents: 46042
diff changeset
   102
(
b352d3d4a58a just one data slot (record) per program unit
blanchet
parents: 46042
diff changeset
   103
  type T =
b352d3d4a58a just one data slot (record) per program unit
blanchet
parents: 46042
diff changeset
   104
    (typ -> bool, (typ -> string option) * (typ -> int -> string option)) ttab *
b352d3d4a58a just one data slot (record) per program unit
blanchet
parents: 46042
diff changeset
   105
    (term list bfun, bfunr option bfun) btab
b352d3d4a58a just one data slot (record) per program unit
blanchet
parents: 46042
diff changeset
   106
  val empty = ([], Symtab.empty)
b352d3d4a58a just one data slot (record) per program unit
blanchet
parents: 46042
diff changeset
   107
  val extend = I
b352d3d4a58a just one data slot (record) per program unit
blanchet
parents: 46042
diff changeset
   108
  fun merge ((t1, b1), (t2, b2)) = (merge_ttab (t1, t2), merge_btab (b1, b2))
b352d3d4a58a just one data slot (record) per program unit
blanchet
parents: 46042
diff changeset
   109
)
41059
d2b1fc1b8e19 centralized handling of built-in types and constants;
boehmes
parents: 40691
diff changeset
   110
54000
9cfff7f61d0d added experimental configuration options to tune use of builtin symbols in SMT
blanchet
parents: 53999
diff changeset
   111
fun filter_ttab keep_T = map (apsnd (filter (keep_T o fst)))
9cfff7f61d0d added experimental configuration options to tune use of builtin symbols in SMT
blanchet
parents: 53999
diff changeset
   112
9cfff7f61d0d added experimental configuration options to tune use of builtin symbols in SMT
blanchet
parents: 53999
diff changeset
   113
fun filter_builtins keep_T =
9cfff7f61d0d added experimental configuration options to tune use of builtin symbols in SMT
blanchet
parents: 53999
diff changeset
   114
  Context.proof_map (Builtins.map (fn (ttab, btab) =>
9cfff7f61d0d added experimental configuration options to tune use of builtin symbols in SMT
blanchet
parents: 53999
diff changeset
   115
    (filter_ttab keep_T ttab, Symtab.map (K (filter_ttab keep_T)) btab)))
53999
ba9254f3111b added possibility to reset builtins (for experimentation)
blanchet
parents: 53998
diff changeset
   116
ba9254f3111b added possibility to reset builtins (for experimentation)
blanchet
parents: 53998
diff changeset
   117
41059
d2b1fc1b8e19 centralized handling of built-in types and constants;
boehmes
parents: 40691
diff changeset
   118
(* built-in types *)
40277
4e3a3461c1a6 added crafted list of SMT built-in constants
boehmes
parents:
diff changeset
   119
41059
d2b1fc1b8e19 centralized handling of built-in types and constants;
boehmes
parents: 40691
diff changeset
   120
fun add_builtin_typ cs (T, f, g) =
53998
b352d3d4a58a just one data slot (record) per program unit
blanchet
parents: 46042
diff changeset
   121
  Builtins.map (apfst (insert_ttab cs T (Int (f, g))))
41059
d2b1fc1b8e19 centralized handling of built-in types and constants;
boehmes
parents: 40691
diff changeset
   122
d2b1fc1b8e19 centralized handling of built-in types and constants;
boehmes
parents: 40691
diff changeset
   123
fun add_builtin_typ_ext (T, f) =
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   124
  Builtins.map (apfst (insert_ttab Old_SMT_Utils.basicC T (Ext f)))
40277
4e3a3461c1a6 added crafted list of SMT built-in constants
boehmes
parents:
diff changeset
   125
41059
d2b1fc1b8e19 centralized handling of built-in types and constants;
boehmes
parents: 40691
diff changeset
   126
fun lookup_builtin_typ ctxt =
53998
b352d3d4a58a just one data slot (record) per program unit
blanchet
parents: 46042
diff changeset
   127
  lookup_ttab ctxt (fst (Builtins.get (Context.Proof ctxt)))
40277
4e3a3461c1a6 added crafted list of SMT built-in constants
boehmes
parents:
diff changeset
   128
41281
679118e35378 removed odd decoration of built-in symbols as Vars (instead provide built-in desctructor functions along with their inverse functions);
boehmes
parents: 41280
diff changeset
   129
fun dest_builtin_typ ctxt T =
41059
d2b1fc1b8e19 centralized handling of built-in types and constants;
boehmes
parents: 40691
diff changeset
   130
  (case lookup_builtin_typ ctxt T of
d2b1fc1b8e19 centralized handling of built-in types and constants;
boehmes
parents: 40691
diff changeset
   131
    SOME (_, Int (f, _)) => f T
d2b1fc1b8e19 centralized handling of built-in types and constants;
boehmes
parents: 40691
diff changeset
   132
  | _ => NONE) 
40277
4e3a3461c1a6 added crafted list of SMT built-in constants
boehmes
parents:
diff changeset
   133
41059
d2b1fc1b8e19 centralized handling of built-in types and constants;
boehmes
parents: 40691
diff changeset
   134
fun is_builtin_typ_ext ctxt T =
d2b1fc1b8e19 centralized handling of built-in types and constants;
boehmes
parents: 40691
diff changeset
   135
  (case lookup_builtin_typ ctxt T of
d2b1fc1b8e19 centralized handling of built-in types and constants;
boehmes
parents: 40691
diff changeset
   136
    SOME (_, Int (f, _)) => is_some (f T)
d2b1fc1b8e19 centralized handling of built-in types and constants;
boehmes
parents: 40691
diff changeset
   137
  | SOME (_, Ext f) => f T
40277
4e3a3461c1a6 added crafted list of SMT built-in constants
boehmes
parents:
diff changeset
   138
  | NONE => false)
4e3a3461c1a6 added crafted list of SMT built-in constants
boehmes
parents:
diff changeset
   139
41059
d2b1fc1b8e19 centralized handling of built-in types and constants;
boehmes
parents: 40691
diff changeset
   140
d2b1fc1b8e19 centralized handling of built-in types and constants;
boehmes
parents: 40691
diff changeset
   141
(* built-in numbers *)
d2b1fc1b8e19 centralized handling of built-in types and constants;
boehmes
parents: 40691
diff changeset
   142
41281
679118e35378 removed odd decoration of built-in symbols as Vars (instead provide built-in desctructor functions along with their inverse functions);
boehmes
parents: 41280
diff changeset
   143
fun dest_builtin_num ctxt t =
41059
d2b1fc1b8e19 centralized handling of built-in types and constants;
boehmes
parents: 40691
diff changeset
   144
  (case try HOLogic.dest_number t of
d2b1fc1b8e19 centralized handling of built-in types and constants;
boehmes
parents: 40691
diff changeset
   145
    NONE => NONE
d2b1fc1b8e19 centralized handling of built-in types and constants;
boehmes
parents: 40691
diff changeset
   146
  | SOME (T, i) =>
54489
03ff4d1e6784 eliminiated neg_numeral in favour of - (numeral _)
haftmann
parents: 54000
diff changeset
   147
      if i < 0 then NONE else
03ff4d1e6784 eliminiated neg_numeral in favour of - (numeral _)
haftmann
parents: 54000
diff changeset
   148
        (case lookup_builtin_typ ctxt T of
03ff4d1e6784 eliminiated neg_numeral in favour of - (numeral _)
haftmann
parents: 54000
diff changeset
   149
          SOME (_, Int (_, g)) => g T i |> Option.map (rpair T)
03ff4d1e6784 eliminiated neg_numeral in favour of - (numeral _)
haftmann
parents: 54000
diff changeset
   150
        | _ => NONE))
41059
d2b1fc1b8e19 centralized handling of built-in types and constants;
boehmes
parents: 40691
diff changeset
   151
41281
679118e35378 removed odd decoration of built-in symbols as Vars (instead provide built-in desctructor functions along with their inverse functions);
boehmes
parents: 41280
diff changeset
   152
val is_builtin_num = is_some oo dest_builtin_num
41059
d2b1fc1b8e19 centralized handling of built-in types and constants;
boehmes
parents: 40691
diff changeset
   153
d2b1fc1b8e19 centralized handling of built-in types and constants;
boehmes
parents: 40691
diff changeset
   154
fun is_builtin_num_ext ctxt t =
d2b1fc1b8e19 centralized handling of built-in types and constants;
boehmes
parents: 40691
diff changeset
   155
  (case try HOLogic.dest_number t of
d2b1fc1b8e19 centralized handling of built-in types and constants;
boehmes
parents: 40691
diff changeset
   156
    NONE => false
d2b1fc1b8e19 centralized handling of built-in types and constants;
boehmes
parents: 40691
diff changeset
   157
  | SOME (T, _) => is_builtin_typ_ext ctxt T)
d2b1fc1b8e19 centralized handling of built-in types and constants;
boehmes
parents: 40691
diff changeset
   158
d2b1fc1b8e19 centralized handling of built-in types and constants;
boehmes
parents: 40691
diff changeset
   159
d2b1fc1b8e19 centralized handling of built-in types and constants;
boehmes
parents: 40691
diff changeset
   160
(* built-in functions *)
d2b1fc1b8e19 centralized handling of built-in types and constants;
boehmes
parents: 40691
diff changeset
   161
d2b1fc1b8e19 centralized handling of built-in types and constants;
boehmes
parents: 40691
diff changeset
   162
fun add_builtin_fun cs ((n, T), f) =
53998
b352d3d4a58a just one data slot (record) per program unit
blanchet
parents: 46042
diff changeset
   163
  Builtins.map (apsnd (insert_btab cs n T (Int f)))
40277
4e3a3461c1a6 added crafted list of SMT built-in constants
boehmes
parents:
diff changeset
   164
41059
d2b1fc1b8e19 centralized handling of built-in types and constants;
boehmes
parents: 40691
diff changeset
   165
fun add_builtin_fun' cs (t, n) =
41127
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41126
diff changeset
   166
  let
41281
679118e35378 removed odd decoration of built-in symbols as Vars (instead provide built-in desctructor functions along with their inverse functions);
boehmes
parents: 41280
diff changeset
   167
    val c as (m, T) = Term.dest_Const t
679118e35378 removed odd decoration of built-in symbols as Vars (instead provide built-in desctructor functions along with their inverse functions);
boehmes
parents: 41280
diff changeset
   168
    fun app U ts = Term.list_comb (Const (m, U), ts)
679118e35378 removed odd decoration of built-in symbols as Vars (instead provide built-in desctructor functions along with their inverse functions);
boehmes
parents: 41280
diff changeset
   169
    fun bfun _ U ts = SOME (n, length (Term.binder_types T), ts, app U)
679118e35378 removed odd decoration of built-in symbols as Vars (instead provide built-in desctructor functions along with their inverse functions);
boehmes
parents: 41280
diff changeset
   170
  in add_builtin_fun cs (c, bfun) end
41059
d2b1fc1b8e19 centralized handling of built-in types and constants;
boehmes
parents: 40691
diff changeset
   171
d2b1fc1b8e19 centralized handling of built-in types and constants;
boehmes
parents: 40691
diff changeset
   172
fun add_builtin_fun_ext ((n, T), f) =
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   173
  Builtins.map (apsnd (insert_btab Old_SMT_Utils.basicC n T (Ext f)))
41059
d2b1fc1b8e19 centralized handling of built-in types and constants;
boehmes
parents: 40691
diff changeset
   174
41354
0abe5db19f3a also provide a view on arguments for "external" built-in symbols (similar to "internal" (real) built-in symbols)
boehmes
parents: 41336
diff changeset
   175
fun add_builtin_fun_ext' c = add_builtin_fun_ext (c, fn _ => fn _ => I)
41059
d2b1fc1b8e19 centralized handling of built-in types and constants;
boehmes
parents: 40691
diff changeset
   176
41072
9f9bc1bdacef be more flexible: store SMT built-in symbols in generic contexts (not in theory contexts)
boehmes
parents: 41059
diff changeset
   177
fun add_builtin_fun_ext'' n context =
9f9bc1bdacef be more flexible: store SMT built-in symbols in generic contexts (not in theory contexts)
boehmes
parents: 41059
diff changeset
   178
  let val thy = Context.theory_of context
9f9bc1bdacef be more flexible: store SMT built-in symbols in generic contexts (not in theory contexts)
boehmes
parents: 41059
diff changeset
   179
  in add_builtin_fun_ext' (n, Sign.the_const_type thy n) context end
41059
d2b1fc1b8e19 centralized handling of built-in types and constants;
boehmes
parents: 40691
diff changeset
   180
d2b1fc1b8e19 centralized handling of built-in types and constants;
boehmes
parents: 40691
diff changeset
   181
fun lookup_builtin_fun ctxt =
53998
b352d3d4a58a just one data slot (record) per program unit
blanchet
parents: 46042
diff changeset
   182
  lookup_btab ctxt (snd (Builtins.get (Context.Proof ctxt)))
41059
d2b1fc1b8e19 centralized handling of built-in types and constants;
boehmes
parents: 40691
diff changeset
   183
41281
679118e35378 removed odd decoration of built-in symbols as Vars (instead provide built-in desctructor functions along with their inverse functions);
boehmes
parents: 41280
diff changeset
   184
fun dest_builtin_fun ctxt (c as (_, T)) ts =
41059
d2b1fc1b8e19 centralized handling of built-in types and constants;
boehmes
parents: 40691
diff changeset
   185
  (case lookup_builtin_fun ctxt c of
d2b1fc1b8e19 centralized handling of built-in types and constants;
boehmes
parents: 40691
diff changeset
   186
    SOME (_, Int f) => f ctxt T ts
d2b1fc1b8e19 centralized handling of built-in types and constants;
boehmes
parents: 40691
diff changeset
   187
  | _ => NONE)
d2b1fc1b8e19 centralized handling of built-in types and constants;
boehmes
parents: 40691
diff changeset
   188
41281
679118e35378 removed odd decoration of built-in symbols as Vars (instead provide built-in desctructor functions along with their inverse functions);
boehmes
parents: 41280
diff changeset
   189
fun dest_builtin_eq ctxt t u =
679118e35378 removed odd decoration of built-in symbols as Vars (instead provide built-in desctructor functions along with their inverse functions);
boehmes
parents: 41280
diff changeset
   190
  let
679118e35378 removed odd decoration of built-in symbols as Vars (instead provide built-in desctructor functions along with their inverse functions);
boehmes
parents: 41280
diff changeset
   191
    val aT = TFree (Name.aT, @{sort type})
679118e35378 removed odd decoration of built-in symbols as Vars (instead provide built-in desctructor functions along with their inverse functions);
boehmes
parents: 41280
diff changeset
   192
    val c = (@{const_name HOL.eq}, aT --> aT --> @{typ bool})
679118e35378 removed odd decoration of built-in symbols as Vars (instead provide built-in desctructor functions along with their inverse functions);
boehmes
parents: 41280
diff changeset
   193
    fun mk ts = Term.list_comb (HOLogic.eq_const (Term.fastype_of (hd ts)), ts)
679118e35378 removed odd decoration of built-in symbols as Vars (instead provide built-in desctructor functions along with their inverse functions);
boehmes
parents: 41280
diff changeset
   194
  in
679118e35378 removed odd decoration of built-in symbols as Vars (instead provide built-in desctructor functions along with their inverse functions);
boehmes
parents: 41280
diff changeset
   195
    dest_builtin_fun ctxt c []
679118e35378 removed odd decoration of built-in symbols as Vars (instead provide built-in desctructor functions along with their inverse functions);
boehmes
parents: 41280
diff changeset
   196
    |> Option.map (fn (n, i, _, _) => (n, i, [t, u], mk))
679118e35378 removed odd decoration of built-in symbols as Vars (instead provide built-in desctructor functions along with their inverse functions);
boehmes
parents: 41280
diff changeset
   197
  end
679118e35378 removed odd decoration of built-in symbols as Vars (instead provide built-in desctructor functions along with their inverse functions);
boehmes
parents: 41280
diff changeset
   198
679118e35378 removed odd decoration of built-in symbols as Vars (instead provide built-in desctructor functions along with their inverse functions);
boehmes
parents: 41280
diff changeset
   199
fun special_builtin_fun pred ctxt (c as (_, T)) ts =
679118e35378 removed odd decoration of built-in symbols as Vars (instead provide built-in desctructor functions along with their inverse functions);
boehmes
parents: 41280
diff changeset
   200
  if pred (Term.body_type T, Term.binder_types T) then
679118e35378 removed odd decoration of built-in symbols as Vars (instead provide built-in desctructor functions along with their inverse functions);
boehmes
parents: 41280
diff changeset
   201
    dest_builtin_fun ctxt c ts
679118e35378 removed odd decoration of built-in symbols as Vars (instead provide built-in desctructor functions along with their inverse functions);
boehmes
parents: 41280
diff changeset
   202
  else NONE
679118e35378 removed odd decoration of built-in symbols as Vars (instead provide built-in desctructor functions along with their inverse functions);
boehmes
parents: 41280
diff changeset
   203
679118e35378 removed odd decoration of built-in symbols as Vars (instead provide built-in desctructor functions along with their inverse functions);
boehmes
parents: 41280
diff changeset
   204
fun dest_builtin_pred ctxt = special_builtin_fun (equal @{typ bool} o fst) ctxt
679118e35378 removed odd decoration of built-in symbols as Vars (instead provide built-in desctructor functions along with their inverse functions);
boehmes
parents: 41280
diff changeset
   205
679118e35378 removed odd decoration of built-in symbols as Vars (instead provide built-in desctructor functions along with their inverse functions);
boehmes
parents: 41280
diff changeset
   206
fun dest_builtin_conn ctxt =
679118e35378 removed odd decoration of built-in symbols as Vars (instead provide built-in desctructor functions along with their inverse functions);
boehmes
parents: 41280
diff changeset
   207
  special_builtin_fun (forall (equal @{typ bool}) o (op ::)) ctxt
679118e35378 removed odd decoration of built-in symbols as Vars (instead provide built-in desctructor functions along with their inverse functions);
boehmes
parents: 41280
diff changeset
   208
679118e35378 removed odd decoration of built-in symbols as Vars (instead provide built-in desctructor functions along with their inverse functions);
boehmes
parents: 41280
diff changeset
   209
fun dest_builtin ctxt c ts =
53999
ba9254f3111b added possibility to reset builtins (for experimentation)
blanchet
parents: 53998
diff changeset
   210
  let val t = Term.list_comb (Const c, ts)
41281
679118e35378 removed odd decoration of built-in symbols as Vars (instead provide built-in desctructor functions along with their inverse functions);
boehmes
parents: 41280
diff changeset
   211
  in
679118e35378 removed odd decoration of built-in symbols as Vars (instead provide built-in desctructor functions along with their inverse functions);
boehmes
parents: 41280
diff changeset
   212
    (case dest_builtin_num ctxt t of
679118e35378 removed odd decoration of built-in symbols as Vars (instead provide built-in desctructor functions along with their inverse functions);
boehmes
parents: 41280
diff changeset
   213
      SOME (n, _) => SOME (n, 0, [], K t)
679118e35378 removed odd decoration of built-in symbols as Vars (instead provide built-in desctructor functions along with their inverse functions);
boehmes
parents: 41280
diff changeset
   214
    | NONE => dest_builtin_fun ctxt c ts)
679118e35378 removed odd decoration of built-in symbols as Vars (instead provide built-in desctructor functions along with their inverse functions);
boehmes
parents: 41280
diff changeset
   215
  end
679118e35378 removed odd decoration of built-in symbols as Vars (instead provide built-in desctructor functions along with their inverse functions);
boehmes
parents: 41280
diff changeset
   216
41354
0abe5db19f3a also provide a view on arguments for "external" built-in symbols (similar to "internal" (real) built-in symbols)
boehmes
parents: 41336
diff changeset
   217
fun dest_builtin_fun_ext ctxt (c as (_, T)) ts =    
0abe5db19f3a also provide a view on arguments for "external" built-in symbols (similar to "internal" (real) built-in symbols)
boehmes
parents: 41336
diff changeset
   218
  (case lookup_builtin_fun ctxt c of
0abe5db19f3a also provide a view on arguments for "external" built-in symbols (similar to "internal" (real) built-in symbols)
boehmes
parents: 41336
diff changeset
   219
    SOME (_, Int f) => f ctxt T ts |> Option.map (fn (_, _, us, _) => us)
0abe5db19f3a also provide a view on arguments for "external" built-in symbols (similar to "internal" (real) built-in symbols)
boehmes
parents: 41336
diff changeset
   220
  | SOME (_, Ext f) => SOME (f ctxt T ts)
0abe5db19f3a also provide a view on arguments for "external" built-in symbols (similar to "internal" (real) built-in symbols)
boehmes
parents: 41336
diff changeset
   221
  | NONE => NONE)
0abe5db19f3a also provide a view on arguments for "external" built-in symbols (similar to "internal" (real) built-in symbols)
boehmes
parents: 41336
diff changeset
   222
0abe5db19f3a also provide a view on arguments for "external" built-in symbols (similar to "internal" (real) built-in symbols)
boehmes
parents: 41336
diff changeset
   223
fun dest_builtin_ext ctxt c ts =
0abe5db19f3a also provide a view on arguments for "external" built-in symbols (similar to "internal" (real) built-in symbols)
boehmes
parents: 41336
diff changeset
   224
  if is_builtin_num_ext ctxt (Term.list_comb (Const c, ts)) then SOME []
0abe5db19f3a also provide a view on arguments for "external" built-in symbols (similar to "internal" (real) built-in symbols)
boehmes
parents: 41336
diff changeset
   225
  else dest_builtin_fun_ext ctxt c ts
0abe5db19f3a also provide a view on arguments for "external" built-in symbols (similar to "internal" (real) built-in symbols)
boehmes
parents: 41336
diff changeset
   226
41281
679118e35378 removed odd decoration of built-in symbols as Vars (instead provide built-in desctructor functions along with their inverse functions);
boehmes
parents: 41280
diff changeset
   227
fun is_builtin_fun ctxt c ts = is_some (dest_builtin_fun ctxt c ts)
41059
d2b1fc1b8e19 centralized handling of built-in types and constants;
boehmes
parents: 40691
diff changeset
   228
41354
0abe5db19f3a also provide a view on arguments for "external" built-in symbols (similar to "internal" (real) built-in symbols)
boehmes
parents: 41336
diff changeset
   229
fun is_builtin_fun_ext ctxt c ts = is_some (dest_builtin_fun_ext ctxt c ts)
41059
d2b1fc1b8e19 centralized handling of built-in types and constants;
boehmes
parents: 40691
diff changeset
   230
40277
4e3a3461c1a6 added crafted list of SMT built-in constants
boehmes
parents:
diff changeset
   231
end