src/HOL/Library/Old_SMT/old_smt_translate.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_translate.ML
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
     2
    Author:     Sascha Boehme, TU Muenchen
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
     3
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
     4
Translate theorems into an SMT intermediate format and serialize them.
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
     5
*)
8e55aa1306c5 integrated SMT into the HOL image
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_TRANSLATE =
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
     8
sig
41123
boehmes
parents: 41059
diff changeset
     9
  (*intermediate term structure*)
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    10
  datatype squant = SForall | SExists
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    11
  datatype 'a spattern = SPat of 'a list | SNoPat of 'a list
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    12
  datatype sterm =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    13
    SVar of int |
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    14
    SApp of string * sterm list |
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    15
    SLet of string * sterm * sterm |
40664
e023788a91a1 added support for quantifier weight annotations
boehmes
parents: 40663
diff changeset
    16
    SQua of squant * string list * sterm spattern list * int option * sterm
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    17
41127
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41123
diff changeset
    18
  (*translation configuration*)
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    19
  type prefixes = {sort_prefix: string, func_prefix: string}
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    20
  type sign = {
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
    21
    header: string list,
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    22
    sorts: string list,
39298
5aefb5bc8a93 added preliminary support for SMT datatypes (for now restricted to tuples and lists); only the Z3 interface (in oracle mode) makes use of it, there is especially no Z3 proof reconstruction support for datatypes yet
boehmes
parents: 37124
diff changeset
    23
    dtyps: (string * (string * (string * string) list) list) list list,
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    24
    funcs: (string * (string list * string)) list }
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    25
  type config = {
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    26
    prefixes: prefixes,
41127
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41123
diff changeset
    27
    header: term list -> string list,
41059
d2b1fc1b8e19 centralized handling of built-in types and constants;
boehmes
parents: 41057
diff changeset
    28
    is_fol: bool,
d2b1fc1b8e19 centralized handling of built-in types and constants;
boehmes
parents: 41057
diff changeset
    29
    has_datatypes: bool,
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    30
    serialize: string list -> sign -> sterm list -> string }
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    31
  type recon = {
41127
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41123
diff changeset
    32
    context: Proof.context,
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    33
    typs: typ Symtab.table,
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    34
    terms: term Symtab.table,
41127
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41123
diff changeset
    35
    rewrite_rules: thm list,
40161
539d07b00e5f keep track of theorems initially given to SMT (even if they are rewritten); provide interface to filter theorems necessary for SMT proofs
boehmes
parents: 39535
diff changeset
    36
    assms: (int * thm) list }
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    37
41127
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41123
diff changeset
    38
  (*translation*)
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
    39
  val add_config: Old_SMT_Utils.class * (Proof.context -> config) ->
41127
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41123
diff changeset
    40
    Context.generic -> Context.generic 
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41123
diff changeset
    41
  val translate: Proof.context -> string list -> (int * thm) list ->
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    42
    string * recon
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    43
end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    44
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
    45
structure Old_SMT_Translate: OLD_SMT_TRANSLATE =
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    46
struct
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    47
40663
e080c9e68752 share and use more utility functions;
boehmes
parents: 40579
diff changeset
    48
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    49
(* intermediate term structure *)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    50
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    51
datatype squant = SForall | SExists
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    52
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    53
datatype 'a spattern = SPat of 'a list | SNoPat of 'a list
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    54
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    55
datatype sterm =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    56
  SVar of int |
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    57
  SApp of string * sterm list |
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    58
  SLet of string * sterm * sterm |
40664
e023788a91a1 added support for quantifier weight annotations
boehmes
parents: 40663
diff changeset
    59
  SQua of squant * string list * sterm spattern list * int option * sterm
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    60
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    61
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    62
41127
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41123
diff changeset
    63
(* translation configuration *)
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    64
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    65
type prefixes = {sort_prefix: string, func_prefix: string}
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    66
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    67
type sign = {
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
    68
  header: string list,
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    69
  sorts: string list,
39298
5aefb5bc8a93 added preliminary support for SMT datatypes (for now restricted to tuples and lists); only the Z3 interface (in oracle mode) makes use of it, there is especially no Z3 proof reconstruction support for datatypes yet
boehmes
parents: 37124
diff changeset
    70
  dtyps: (string * (string * (string * string) list) list) list list,
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    71
  funcs: (string * (string list * string)) list }
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    72
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    73
type config = {
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    74
  prefixes: prefixes,
41127
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41123
diff changeset
    75
  header: term list -> string list,
41059
d2b1fc1b8e19 centralized handling of built-in types and constants;
boehmes
parents: 41057
diff changeset
    76
  is_fol: bool,
d2b1fc1b8e19 centralized handling of built-in types and constants;
boehmes
parents: 41057
diff changeset
    77
  has_datatypes: bool,
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    78
  serialize: string list -> sign -> sterm list -> string }
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    79
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    80
type recon = {
41127
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41123
diff changeset
    81
  context: Proof.context,
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    82
  typs: typ Symtab.table,
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    83
  terms: term Symtab.table,
41127
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41123
diff changeset
    84
  rewrite_rules: thm list,
40161
539d07b00e5f keep track of theorems initially given to SMT (even if they are rewritten); provide interface to filter theorems necessary for SMT proofs
boehmes
parents: 39535
diff changeset
    85
  assms: (int * thm) list }
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    86
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    87
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    88
41127
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41123
diff changeset
    89
(* translation context *)
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41123
diff changeset
    90
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41123
diff changeset
    91
fun make_tr_context {sort_prefix, func_prefix} =
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41123
diff changeset
    92
  (sort_prefix, 1, Typtab.empty, func_prefix, 1, Termtab.empty)
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41123
diff changeset
    93
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41123
diff changeset
    94
fun string_of_index pre i = pre ^ string_of_int i
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41123
diff changeset
    95
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41123
diff changeset
    96
fun add_typ T proper (cx as (sp, Tidx, typs, fp, idx, terms)) =
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41123
diff changeset
    97
  (case Typtab.lookup typs T of
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41123
diff changeset
    98
    SOME (n, _) => (n, cx)
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41123
diff changeset
    99
  | NONE =>
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41123
diff changeset
   100
      let
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41123
diff changeset
   101
        val n = string_of_index sp Tidx
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41123
diff changeset
   102
        val typs' = Typtab.update (T, (n, proper)) typs
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41123
diff changeset
   103
      in (n, (sp, Tidx+1, typs', fp, idx, terms)) end)
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41123
diff changeset
   104
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41123
diff changeset
   105
fun add_fun t sort (cx as (sp, Tidx, typs, fp, idx, terms)) =
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41123
diff changeset
   106
  (case Termtab.lookup terms t of
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41123
diff changeset
   107
    SOME (n, _) => (n, cx)
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41123
diff changeset
   108
  | NONE => 
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41123
diff changeset
   109
      let
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41123
diff changeset
   110
        val n = string_of_index fp idx
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41123
diff changeset
   111
        val terms' = Termtab.update (t, (n, sort)) terms
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41123
diff changeset
   112
      in (n, (sp, Tidx, typs, fp, idx+1, terms')) end)
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41123
diff changeset
   113
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41123
diff changeset
   114
fun sign_of header dtyps (_, _, typs, _, _, terms) = {
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41123
diff changeset
   115
  header = header,
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41123
diff changeset
   116
  sorts = Typtab.fold (fn (_, (n, true)) => cons n | _ => I) typs [],
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41123
diff changeset
   117
  dtyps = dtyps,
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41123
diff changeset
   118
  funcs = Termtab.fold (fn (_, (n, SOME ss)) => cons (n,ss) | _ => I) terms []}
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41123
diff changeset
   119
41281
679118e35378 removed odd decoration of built-in symbols as Vars (instead provide built-in desctructor functions along with their inverse functions);
boehmes
parents: 41250
diff changeset
   120
fun recon_of ctxt rules thms ithms (_, _, typs, _, _, terms) =
41127
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41123
diff changeset
   121
  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: 41250
diff changeset
   122
    fun add_typ (T, (n, _)) = Symtab.update (n, T)
41127
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41123
diff changeset
   123
    val typs' = Typtab.fold add_typ typs Symtab.empty
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41123
diff changeset
   124
41281
679118e35378 removed odd decoration of built-in symbols as Vars (instead provide built-in desctructor functions along with their inverse functions);
boehmes
parents: 41250
diff changeset
   125
    fun add_fun (t, (n, _)) = Symtab.update (n, t)
41127
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41123
diff changeset
   126
    val terms' = Termtab.fold add_fun terms Symtab.empty
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41123
diff changeset
   127
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41123
diff changeset
   128
    val assms = map (pair ~1) thms @ ithms
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41123
diff changeset
   129
  in
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41123
diff changeset
   130
    {context=ctxt, typs=typs', terms=terms', rewrite_rules=rules, assms=assms}
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41123
diff changeset
   131
  end
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41123
diff changeset
   132
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41123
diff changeset
   133
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41123
diff changeset
   134
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41123
diff changeset
   135
(* preprocessing *)
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41123
diff changeset
   136
41426
09615ed31f04 re-implemented support for datatypes (including records and typedefs);
boehmes
parents: 41328
diff changeset
   137
(** datatype declarations **)
41127
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41123
diff changeset
   138
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41123
diff changeset
   139
fun collect_datatypes_and_records (tr_context, ctxt) ts =
41426
09615ed31f04 re-implemented support for datatypes (including records and typedefs);
boehmes
parents: 41328
diff changeset
   140
  let
09615ed31f04 re-implemented support for datatypes (including records and typedefs);
boehmes
parents: 41328
diff changeset
   141
    val (declss, ctxt') =
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   142
      fold (Term.fold_types Old_SMT_Datatypes.add_decls) ts ([], ctxt)
41426
09615ed31f04 re-implemented support for datatypes (including records and typedefs);
boehmes
parents: 41328
diff changeset
   143
09615ed31f04 re-implemented support for datatypes (including records and typedefs);
boehmes
parents: 41328
diff changeset
   144
    fun is_decl_typ T = exists (exists (equal T o fst)) declss
09615ed31f04 re-implemented support for datatypes (including records and typedefs);
boehmes
parents: 41328
diff changeset
   145
09615ed31f04 re-implemented support for datatypes (including records and typedefs);
boehmes
parents: 41328
diff changeset
   146
    fun add_typ' T proper =
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   147
      (case Old_SMT_Builtin.dest_builtin_typ ctxt' T of
41426
09615ed31f04 re-implemented support for datatypes (including records and typedefs);
boehmes
parents: 41328
diff changeset
   148
        SOME n => pair n
09615ed31f04 re-implemented support for datatypes (including records and typedefs);
boehmes
parents: 41328
diff changeset
   149
      | NONE => add_typ T proper)
41127
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41123
diff changeset
   150
41426
09615ed31f04 re-implemented support for datatypes (including records and typedefs);
boehmes
parents: 41328
diff changeset
   151
    fun tr_select sel =
09615ed31f04 re-implemented support for datatypes (including records and typedefs);
boehmes
parents: 41328
diff changeset
   152
      let val T = Term.range_type (Term.fastype_of sel)
09615ed31f04 re-implemented support for datatypes (including records and typedefs);
boehmes
parents: 41328
diff changeset
   153
      in add_fun sel NONE ##>> add_typ' T (not (is_decl_typ T)) end
09615ed31f04 re-implemented support for datatypes (including records and typedefs);
boehmes
parents: 41328
diff changeset
   154
    fun tr_constr (constr, selects) =
09615ed31f04 re-implemented support for datatypes (including records and typedefs);
boehmes
parents: 41328
diff changeset
   155
      add_fun constr NONE ##>> fold_map tr_select selects
09615ed31f04 re-implemented support for datatypes (including records and typedefs);
boehmes
parents: 41328
diff changeset
   156
    fun tr_typ (T, cases) = add_typ' T false ##>> fold_map tr_constr cases
09615ed31f04 re-implemented support for datatypes (including records and typedefs);
boehmes
parents: 41328
diff changeset
   157
    val (declss', tr_context') = fold_map (fold_map tr_typ) declss tr_context
09615ed31f04 re-implemented support for datatypes (including records and typedefs);
boehmes
parents: 41328
diff changeset
   158
09615ed31f04 re-implemented support for datatypes (including records and typedefs);
boehmes
parents: 41328
diff changeset
   159
    fun add (constr, selects) =
09615ed31f04 re-implemented support for datatypes (including records and typedefs);
boehmes
parents: 41328
diff changeset
   160
      Termtab.update (constr, length selects) #>
09615ed31f04 re-implemented support for datatypes (including records and typedefs);
boehmes
parents: 41328
diff changeset
   161
      fold (Termtab.update o rpair 1) selects
09615ed31f04 re-implemented support for datatypes (including records and typedefs);
boehmes
parents: 41328
diff changeset
   162
    val funcs = fold (fold (fold add o snd)) declss Termtab.empty
09615ed31f04 re-implemented support for datatypes (including records and typedefs);
boehmes
parents: 41328
diff changeset
   163
  in ((funcs, declss', tr_context', ctxt'), ts) end
09615ed31f04 re-implemented support for datatypes (including records and typedefs);
boehmes
parents: 41328
diff changeset
   164
    (* FIXME: also return necessary datatype and record theorems *)
41127
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41123
diff changeset
   165
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41123
diff changeset
   166
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41123
diff changeset
   167
(** eta-expand quantifiers, let expressions and built-ins *)
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41123
diff changeset
   168
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41123
diff changeset
   169
local
42319
9a8ba59aed06 unfold and eta-contract let expressions before lambda-lifting to avoid bad terms
boehmes
parents: 41785
diff changeset
   170
  fun eta f T t = Abs (Name.uu, T, f (Term.incr_boundvars 1 t $ Bound 0))
41127
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41123
diff changeset
   171
42319
9a8ba59aed06 unfold and eta-contract let expressions before lambda-lifting to avoid bad terms
boehmes
parents: 41785
diff changeset
   172
  fun exp f T = eta f (Term.domain_type (Term.domain_type T))
41127
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41123
diff changeset
   173
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41123
diff changeset
   174
  fun exp2 T q =
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41123
diff changeset
   175
    let val U = Term.domain_type T
42319
9a8ba59aed06 unfold and eta-contract let expressions before lambda-lifting to avoid bad terms
boehmes
parents: 41785
diff changeset
   176
    in Abs (Name.uu, U, q $ eta I (Term.domain_type U) (Bound 0)) end
41127
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41123
diff changeset
   177
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41123
diff changeset
   178
  fun exp2' T l =
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41123
diff changeset
   179
    let val (U1, U2) = Term.dest_funT T ||> Term.domain_type
42319
9a8ba59aed06 unfold and eta-contract let expressions before lambda-lifting to avoid bad terms
boehmes
parents: 41785
diff changeset
   180
    in Abs (Name.uu, U1, eta I U2 (l $ Bound 0)) end
41127
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41123
diff changeset
   181
41281
679118e35378 removed odd decoration of built-in symbols as Vars (instead provide built-in desctructor functions along with their inverse functions);
boehmes
parents: 41250
diff changeset
   182
  fun expf k i T t =
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   183
    let val Ts = drop i (fst (Old_SMT_Utils.dest_funT k T))
41195
f59491d56327 fixed eta-expansion: introduce a couple of abstractions at once
boehmes
parents: 41173
diff changeset
   184
    in
41281
679118e35378 removed odd decoration of built-in symbols as Vars (instead provide built-in desctructor functions along with their inverse functions);
boehmes
parents: 41250
diff changeset
   185
      Term.incr_boundvars (length Ts) t
42321
ce83c1654b86 fixed eta-expansion: use correct order to apply new bound variables
boehmes
parents: 42319
diff changeset
   186
      |> fold_rev (fn i => fn u => u $ Bound i) (0 upto length Ts - 1)
41195
f59491d56327 fixed eta-expansion: introduce a couple of abstractions at once
boehmes
parents: 41173
diff changeset
   187
      |> fold_rev (fn T => fn u => Abs (Name.uu, T, u)) Ts
f59491d56327 fixed eta-expansion: introduce a couple of abstractions at once
boehmes
parents: 41173
diff changeset
   188
    end
41127
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41123
diff changeset
   189
in
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41123
diff changeset
   190
42319
9a8ba59aed06 unfold and eta-contract let expressions before lambda-lifting to avoid bad terms
boehmes
parents: 41785
diff changeset
   191
fun eta_expand ctxt is_fol funcs =
41281
679118e35378 removed odd decoration of built-in symbols as Vars (instead provide built-in desctructor functions along with their inverse functions);
boehmes
parents: 41250
diff changeset
   192
  let
41426
09615ed31f04 re-implemented support for datatypes (including records and typedefs);
boehmes
parents: 41328
diff changeset
   193
    fun exp_func t T ts =
09615ed31f04 re-implemented support for datatypes (including records and typedefs);
boehmes
parents: 41328
diff changeset
   194
      (case Termtab.lookup funcs t of
09615ed31f04 re-implemented support for datatypes (including records and typedefs);
boehmes
parents: 41328
diff changeset
   195
        SOME k =>
09615ed31f04 re-implemented support for datatypes (including records and typedefs);
boehmes
parents: 41328
diff changeset
   196
          Term.list_comb (t, ts)
09615ed31f04 re-implemented support for datatypes (including records and typedefs);
boehmes
parents: 41328
diff changeset
   197
          |> k <> length ts ? expf k (length ts) T
09615ed31f04 re-implemented support for datatypes (including records and typedefs);
boehmes
parents: 41328
diff changeset
   198
      | NONE => Term.list_comb (t, ts))
09615ed31f04 re-implemented support for datatypes (including records and typedefs);
boehmes
parents: 41328
diff changeset
   199
41281
679118e35378 removed odd decoration of built-in symbols as Vars (instead provide built-in desctructor functions along with their inverse functions);
boehmes
parents: 41250
diff changeset
   200
    fun expand ((q as Const (@{const_name All}, _)) $ Abs a) = q $ abs_expand a
42319
9a8ba59aed06 unfold and eta-contract let expressions before lambda-lifting to avoid bad terms
boehmes
parents: 41785
diff changeset
   201
      | expand ((q as Const (@{const_name All}, T)) $ t) = q $ exp expand T t
41281
679118e35378 removed odd decoration of built-in symbols as Vars (instead provide built-in desctructor functions along with their inverse functions);
boehmes
parents: 41250
diff changeset
   202
      | expand (q as Const (@{const_name All}, T)) = exp2 T q
679118e35378 removed odd decoration of built-in symbols as Vars (instead provide built-in desctructor functions along with their inverse functions);
boehmes
parents: 41250
diff changeset
   203
      | expand ((q as Const (@{const_name Ex}, _)) $ Abs a) = q $ abs_expand a
42319
9a8ba59aed06 unfold and eta-contract let expressions before lambda-lifting to avoid bad terms
boehmes
parents: 41785
diff changeset
   204
      | expand ((q as Const (@{const_name Ex}, T)) $ t) = q $ exp expand T t
41281
679118e35378 removed odd decoration of built-in symbols as Vars (instead provide built-in desctructor functions along with their inverse functions);
boehmes
parents: 41250
diff changeset
   205
      | expand (q as Const (@{const_name Ex}, T)) = exp2 T q
679118e35378 removed odd decoration of built-in symbols as Vars (instead provide built-in desctructor functions along with their inverse functions);
boehmes
parents: 41250
diff changeset
   206
      | expand ((l as Const (@{const_name Let}, _)) $ t $ Abs a) =
42319
9a8ba59aed06 unfold and eta-contract let expressions before lambda-lifting to avoid bad terms
boehmes
parents: 41785
diff changeset
   207
          if is_fol then expand (Term.betapply (Abs a, t))
9a8ba59aed06 unfold and eta-contract let expressions before lambda-lifting to avoid bad terms
boehmes
parents: 41785
diff changeset
   208
          else l $ expand t $ abs_expand 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: 41250
diff changeset
   209
      | expand ((l as Const (@{const_name Let}, T)) $ t $ u) =
42319
9a8ba59aed06 unfold and eta-contract let expressions before lambda-lifting to avoid bad terms
boehmes
parents: 41785
diff changeset
   210
          if is_fol then expand (u $ t)
9a8ba59aed06 unfold and eta-contract let expressions before lambda-lifting to avoid bad terms
boehmes
parents: 41785
diff changeset
   211
          else l $ expand t $ exp expand (Term.range_type T) u
41281
679118e35378 removed odd decoration of built-in symbols as Vars (instead provide built-in desctructor functions along with their inverse functions);
boehmes
parents: 41250
diff changeset
   212
      | expand ((l as Const (@{const_name Let}, T)) $ t) =
42319
9a8ba59aed06 unfold and eta-contract let expressions before lambda-lifting to avoid bad terms
boehmes
parents: 41785
diff changeset
   213
          if is_fol then
9a8ba59aed06 unfold and eta-contract let expressions before lambda-lifting to avoid bad terms
boehmes
parents: 41785
diff changeset
   214
            let val U = Term.domain_type (Term.range_type T)
9a8ba59aed06 unfold and eta-contract let expressions before lambda-lifting to avoid bad terms
boehmes
parents: 41785
diff changeset
   215
            in Abs (Name.uu, U, Bound 0 $ Term.incr_boundvars 1 t) end
9a8ba59aed06 unfold and eta-contract let expressions before lambda-lifting to avoid bad terms
boehmes
parents: 41785
diff changeset
   216
          else exp2 T (l $ expand t)
9a8ba59aed06 unfold and eta-contract let expressions before lambda-lifting to avoid bad terms
boehmes
parents: 41785
diff changeset
   217
      | expand (l as Const (@{const_name Let}, T)) =
9a8ba59aed06 unfold and eta-contract let expressions before lambda-lifting to avoid bad terms
boehmes
parents: 41785
diff changeset
   218
          if is_fol then 
9a8ba59aed06 unfold and eta-contract let expressions before lambda-lifting to avoid bad terms
boehmes
parents: 41785
diff changeset
   219
            let val U = Term.domain_type (Term.range_type T)
9a8ba59aed06 unfold and eta-contract let expressions before lambda-lifting to avoid bad terms
boehmes
parents: 41785
diff changeset
   220
            in
9a8ba59aed06 unfold and eta-contract let expressions before lambda-lifting to avoid bad terms
boehmes
parents: 41785
diff changeset
   221
              Abs (Name.uu, Term.domain_type T, Abs (Name.uu, U,
9a8ba59aed06 unfold and eta-contract let expressions before lambda-lifting to avoid bad terms
boehmes
parents: 41785
diff changeset
   222
                Bound 0 $ Bound 1))
9a8ba59aed06 unfold and eta-contract let expressions before lambda-lifting to avoid bad terms
boehmes
parents: 41785
diff changeset
   223
            end
9a8ba59aed06 unfold and eta-contract let expressions before lambda-lifting to avoid bad terms
boehmes
parents: 41785
diff changeset
   224
          else exp2' T l
41281
679118e35378 removed odd decoration of built-in symbols as Vars (instead provide built-in desctructor functions along with their inverse functions);
boehmes
parents: 41250
diff changeset
   225
      | expand t =
679118e35378 removed odd decoration of built-in symbols as Vars (instead provide built-in desctructor functions along with their inverse functions);
boehmes
parents: 41250
diff changeset
   226
          (case Term.strip_comb 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: 41250
diff changeset
   227
            (u as Const (c as (_, T)), ts) =>
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   228
              (case Old_SMT_Builtin.dest_builtin ctxt c ts of
41281
679118e35378 removed odd decoration of built-in symbols as Vars (instead provide built-in desctructor functions along with their inverse functions);
boehmes
parents: 41250
diff changeset
   229
                SOME (_, k, us, mk) =>
679118e35378 removed odd decoration of built-in symbols as Vars (instead provide built-in desctructor functions along with their inverse functions);
boehmes
parents: 41250
diff changeset
   230
                  if k = length us then mk (map expand us)
46529
a018d542e0ae corrected treatment of applications of built-in functions to higher-order terms
boehmes
parents: 43932
diff changeset
   231
                  else if k < length us then
a018d542e0ae corrected treatment of applications of built-in functions to higher-order terms
boehmes
parents: 43932
diff changeset
   232
                    chop k (map expand us) |>> mk |> Term.list_comb
41281
679118e35378 removed odd decoration of built-in symbols as Vars (instead provide built-in desctructor functions along with their inverse functions);
boehmes
parents: 41250
diff changeset
   233
                  else expf k (length ts) T (mk (map expand us))
41426
09615ed31f04 re-implemented support for datatypes (including records and typedefs);
boehmes
parents: 41328
diff changeset
   234
              | NONE => exp_func u T (map expand ts))
09615ed31f04 re-implemented support for datatypes (including records and typedefs);
boehmes
parents: 41328
diff changeset
   235
          | (u as Free (_, T), ts) => exp_func u T (map expand 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: 41250
diff changeset
   236
          | (Abs a, ts) => Term.list_comb (abs_expand a, map expand ts)
679118e35378 removed odd decoration of built-in symbols as Vars (instead provide built-in desctructor functions along with their inverse functions);
boehmes
parents: 41250
diff changeset
   237
          | (u, ts) => Term.list_comb (u, map expand ts))
679118e35378 removed odd decoration of built-in symbols as Vars (instead provide built-in desctructor functions along with their inverse functions);
boehmes
parents: 41250
diff changeset
   238
679118e35378 removed odd decoration of built-in symbols as Vars (instead provide built-in desctructor functions along with their inverse functions);
boehmes
parents: 41250
diff changeset
   239
    and abs_expand (n, T, t) = Abs (n, T, expand t)
679118e35378 removed odd decoration of built-in symbols as Vars (instead provide built-in desctructor functions along with their inverse functions);
boehmes
parents: 41250
diff changeset
   240
  
679118e35378 removed odd decoration of built-in symbols as Vars (instead provide built-in desctructor functions along with their inverse functions);
boehmes
parents: 41250
diff changeset
   241
  in map expand end
41127
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41123
diff changeset
   242
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41123
diff changeset
   243
end
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41123
diff changeset
   244
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41123
diff changeset
   245
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41123
diff changeset
   246
(** introduce explicit applications **)
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41123
diff changeset
   247
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41123
diff changeset
   248
local
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41123
diff changeset
   249
  (*
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41123
diff changeset
   250
    Make application explicit for functions with varying number of arguments.
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41123
diff changeset
   251
  *)
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41123
diff changeset
   252
43154
72e4753a6677 made introduction of explicit application stable under removal of vacuous facts (which only lower the rank of constants but do not participate in the proof)
boehmes
parents: 42321
diff changeset
   253
  fun add t i = apfst (Termtab.map_default (t, i) (Integer.min i))
72e4753a6677 made introduction of explicit application stable under removal of vacuous facts (which only lower the rank of constants but do not participate in the proof)
boehmes
parents: 42321
diff changeset
   254
  fun add_type T = apsnd (Typtab.update (T, ()))
41127
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41123
diff changeset
   255
41232
4ea9f2a8c093 fixed lambda-lifting: shift indices of bound variables correctly (after locking the required bound variables) and apply bound variables to the new function symbol in the right order;
boehmes
parents: 41198
diff changeset
   256
  fun min_arities t =
4ea9f2a8c093 fixed lambda-lifting: shift indices of bound variables correctly (after locking the required bound variables) and apply bound variables to the new function symbol in the right order;
boehmes
parents: 41198
diff changeset
   257
    (case Term.strip_comb t of
4ea9f2a8c093 fixed lambda-lifting: shift indices of bound variables correctly (after locking the required bound variables) and apply bound variables to the new function symbol in the right order;
boehmes
parents: 41198
diff changeset
   258
      (u as Const _, ts) => add u (length ts) #> fold min_arities ts
4ea9f2a8c093 fixed lambda-lifting: shift indices of bound variables correctly (after locking the required bound variables) and apply bound variables to the new function symbol in the right order;
boehmes
parents: 41198
diff changeset
   259
    | (u as Free _, ts) => add u (length ts) #> fold min_arities ts
43154
72e4753a6677 made introduction of explicit application stable under removal of vacuous facts (which only lower the rank of constants but do not participate in the proof)
boehmes
parents: 42321
diff changeset
   260
    | (Abs (_, T, u), ts) => add_type T #> min_arities u #> fold min_arities ts
41232
4ea9f2a8c093 fixed lambda-lifting: shift indices of bound variables correctly (after locking the required bound variables) and apply bound variables to the new function symbol in the right order;
boehmes
parents: 41198
diff changeset
   261
    | (_, ts) => fold min_arities ts)
41127
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41123
diff changeset
   262
43154
72e4753a6677 made introduction of explicit application stable under removal of vacuous facts (which only lower the rank of constants but do not participate in the proof)
boehmes
parents: 42321
diff changeset
   263
  fun minimize types t i =
43554
9bece8cbb5be generalized introduction of explicit application constant: consider more functions as possible witness/instance of quantifiers than before (a constant of type T1 -> T2 -> T3 should be considered to have a rank less or equal to 1 if variables of type T2 -> T3 occur bound in a problem);
boehmes
parents: 43507
diff changeset
   264
    let
9bece8cbb5be generalized introduction of explicit application constant: consider more functions as possible witness/instance of quantifiers than before (a constant of type T1 -> T2 -> T3 should be considered to have a rank less or equal to 1 if variables of type T2 -> T3 occur bound in a problem);
boehmes
parents: 43507
diff changeset
   265
      fun find_min j [] _ = j
9bece8cbb5be generalized introduction of explicit application constant: consider more functions as possible witness/instance of quantifiers than before (a constant of type T1 -> T2 -> T3 should be considered to have a rank less or equal to 1 if variables of type T2 -> T3 occur bound in a problem);
boehmes
parents: 43507
diff changeset
   266
        | find_min j (U :: Us) T =
9bece8cbb5be generalized introduction of explicit application constant: consider more functions as possible witness/instance of quantifiers than before (a constant of type T1 -> T2 -> T3 should be considered to have a rank less or equal to 1 if variables of type T2 -> T3 occur bound in a problem);
boehmes
parents: 43507
diff changeset
   267
            if Typtab.defined types T then j
9bece8cbb5be generalized introduction of explicit application constant: consider more functions as possible witness/instance of quantifiers than before (a constant of type T1 -> T2 -> T3 should be considered to have a rank less or equal to 1 if variables of type T2 -> T3 occur bound in a problem);
boehmes
parents: 43507
diff changeset
   268
            else find_min (j + 1) Us (U --> T)
9bece8cbb5be generalized introduction of explicit application constant: consider more functions as possible witness/instance of quantifiers than before (a constant of type T1 -> T2 -> T3 should be considered to have a rank less or equal to 1 if variables of type T2 -> T3 occur bound in a problem);
boehmes
parents: 43507
diff changeset
   269
9bece8cbb5be generalized introduction of explicit application constant: consider more functions as possible witness/instance of quantifiers than before (a constant of type T1 -> T2 -> T3 should be considered to have a rank less or equal to 1 if variables of type T2 -> T3 occur bound in a problem);
boehmes
parents: 43507
diff changeset
   270
      val (Ts, T) = Term.strip_type (Term.type_of t)
9bece8cbb5be generalized introduction of explicit application constant: consider more functions as possible witness/instance of quantifiers than before (a constant of type T1 -> T2 -> T3 should be considered to have a rank less or equal to 1 if variables of type T2 -> T3 occur bound in a problem);
boehmes
parents: 43507
diff changeset
   271
    in find_min 0 (take i (rev Ts)) T end
43154
72e4753a6677 made introduction of explicit application stable under removal of vacuous facts (which only lower the rank of constants but do not participate in the proof)
boehmes
parents: 42321
diff changeset
   272
41232
4ea9f2a8c093 fixed lambda-lifting: shift indices of bound variables correctly (after locking the required bound variables) and apply bound variables to the new function symbol in the right order;
boehmes
parents: 41198
diff changeset
   273
  fun app u (t, T) =
58057
883f3c4c928e renaming theory 'Old_SMT'
blanchet
parents: 58055
diff changeset
   274
    (Const (@{const_name fun_app}, T --> T) $ t $ u, Term.range_type T)
41127
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41123
diff changeset
   275
41232
4ea9f2a8c093 fixed lambda-lifting: shift indices of bound variables correctly (after locking the required bound variables) and apply bound variables to the new function symbol in the right order;
boehmes
parents: 41198
diff changeset
   276
  fun apply i t T ts =
41328
6792a5c92a58 avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents: 41281
diff changeset
   277
    let
6792a5c92a58 avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents: 41281
diff changeset
   278
      val (ts1, ts2) = chop i ts
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   279
      val (_, U) = Old_SMT_Utils.dest_funT i T
41328
6792a5c92a58 avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents: 41281
diff changeset
   280
    in fst (fold app ts2 (Term.list_comb (t, ts1), U)) end
41127
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41123
diff changeset
   281
in
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41123
diff changeset
   282
43385
9cd4b4ecb4dd slightly more general treatment of mutually recursive datatypes;
boehmes
parents: 43154
diff changeset
   283
fun intro_explicit_application ctxt funcs ts =
41127
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41123
diff changeset
   284
  let
43154
72e4753a6677 made introduction of explicit application stable under removal of vacuous facts (which only lower the rank of constants but do not participate in the proof)
boehmes
parents: 42321
diff changeset
   285
    val (arities, types) = fold min_arities ts (Termtab.empty, Typtab.empty)
72e4753a6677 made introduction of explicit application stable under removal of vacuous facts (which only lower the rank of constants but do not participate in the proof)
boehmes
parents: 42321
diff changeset
   286
    val arities' = Termtab.map (minimize types) arities
43385
9cd4b4ecb4dd slightly more general treatment of mutually recursive datatypes;
boehmes
parents: 43154
diff changeset
   287
9cd4b4ecb4dd slightly more general treatment of mutually recursive datatypes;
boehmes
parents: 43154
diff changeset
   288
    fun app_func t T ts =
9cd4b4ecb4dd slightly more general treatment of mutually recursive datatypes;
boehmes
parents: 43154
diff changeset
   289
      if is_some (Termtab.lookup funcs t) then Term.list_comb (t, ts)
9cd4b4ecb4dd slightly more general treatment of mutually recursive datatypes;
boehmes
parents: 43154
diff changeset
   290
      else apply (the (Termtab.lookup arities' t)) t T ts
41127
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41123
diff changeset
   291
43554
9bece8cbb5be generalized introduction of explicit application constant: consider more functions as possible witness/instance of quantifiers than before (a constant of type T1 -> T2 -> T3 should be considered to have a rank less or equal to 1 if variables of type T2 -> T3 occur bound in a problem);
boehmes
parents: 43507
diff changeset
   292
    fun in_list T f t = HOLogic.mk_list T (map f (HOLogic.dest_list t))
9bece8cbb5be generalized introduction of explicit application constant: consider more functions as possible witness/instance of quantifiers than before (a constant of type T1 -> T2 -> T3 should be considered to have a rank less or equal to 1 if variables of type T2 -> T3 occur bound in a problem);
boehmes
parents: 43507
diff changeset
   293
41232
4ea9f2a8c093 fixed lambda-lifting: shift indices of bound variables correctly (after locking the required bound variables) and apply bound variables to the new function symbol in the right order;
boehmes
parents: 41198
diff changeset
   294
    fun traverse Ts t =
41127
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41123
diff changeset
   295
      (case Term.strip_comb t of
43554
9bece8cbb5be generalized introduction of explicit application constant: consider more functions as possible witness/instance of quantifiers than before (a constant of type T1 -> T2 -> T3 should be considered to have a rank less or equal to 1 if variables of type T2 -> T3 occur bound in a problem);
boehmes
parents: 43507
diff changeset
   296
        (q as Const (@{const_name All}, _), [Abs (x, T, u)]) =>
9bece8cbb5be generalized introduction of explicit application constant: consider more functions as possible witness/instance of quantifiers than before (a constant of type T1 -> T2 -> T3 should be considered to have a rank less or equal to 1 if variables of type T2 -> T3 occur bound in a problem);
boehmes
parents: 43507
diff changeset
   297
          q $ Abs (x, T, in_trigger (T :: Ts) u)
9bece8cbb5be generalized introduction of explicit application constant: consider more functions as possible witness/instance of quantifiers than before (a constant of type T1 -> T2 -> T3 should be considered to have a rank less or equal to 1 if variables of type T2 -> T3 occur bound in a problem);
boehmes
parents: 43507
diff changeset
   298
      | (q as Const (@{const_name Ex}, _), [Abs (x, T, u)]) =>
9bece8cbb5be generalized introduction of explicit application constant: consider more functions as possible witness/instance of quantifiers than before (a constant of type T1 -> T2 -> T3 should be considered to have a rank less or equal to 1 if variables of type T2 -> T3 occur bound in a problem);
boehmes
parents: 43507
diff changeset
   299
          q $ Abs (x, T, in_trigger (T :: Ts) u)
43929
61d432e51aff generalized lambda-lifting such that it is less specifically tailored for SMT (it does not anymore dependent on any SMT-specific code)
boehmes
parents: 43928
diff changeset
   300
      | (q as Const (@{const_name Let}, _), [u1, u2 as Abs _]) =>
43154
72e4753a6677 made introduction of explicit application stable under removal of vacuous facts (which only lower the rank of constants but do not participate in the proof)
boehmes
parents: 42321
diff changeset
   301
          q $ traverse Ts u1 $ traverse Ts u2
72e4753a6677 made introduction of explicit application stable under removal of vacuous facts (which only lower the rank of constants but do not participate in the proof)
boehmes
parents: 42321
diff changeset
   302
      | (u as Const (c as (_, T)), ts) =>
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   303
          (case Old_SMT_Builtin.dest_builtin ctxt c ts of
46529
a018d542e0ae corrected treatment of applications of built-in functions to higher-order terms
boehmes
parents: 43932
diff changeset
   304
            SOME (_, k, us, mk) =>
a018d542e0ae corrected treatment of applications of built-in functions to higher-order terms
boehmes
parents: 43932
diff changeset
   305
              let
a018d542e0ae corrected treatment of applications of built-in functions to higher-order terms
boehmes
parents: 43932
diff changeset
   306
                val (ts1, ts2) = chop k (map (traverse Ts) us)
a018d542e0ae corrected treatment of applications of built-in functions to higher-order terms
boehmes
parents: 43932
diff changeset
   307
                val U = Term.strip_type T |>> snd o chop k |> (op --->)
a018d542e0ae corrected treatment of applications of built-in functions to higher-order terms
boehmes
parents: 43932
diff changeset
   308
              in apply 0 (mk ts1) U ts2 end
43385
9cd4b4ecb4dd slightly more general treatment of mutually recursive datatypes;
boehmes
parents: 43154
diff changeset
   309
          | NONE => app_func u T (map (traverse Ts) ts))
9cd4b4ecb4dd slightly more general treatment of mutually recursive datatypes;
boehmes
parents: 43154
diff changeset
   310
      | (u as Free (_, T), ts) => app_func u T (map (traverse Ts) ts)
41232
4ea9f2a8c093 fixed lambda-lifting: shift indices of bound variables correctly (after locking the required bound variables) and apply bound variables to the new function symbol in the right order;
boehmes
parents: 41198
diff changeset
   311
      | (u as Bound i, ts) => apply 0 u (nth Ts i) (map (traverse Ts) ts)
4ea9f2a8c093 fixed lambda-lifting: shift indices of bound variables correctly (after locking the required bound variables) and apply bound variables to the new function symbol in the right order;
boehmes
parents: 41198
diff changeset
   312
      | (Abs (n, T, u), ts) => traverses Ts (Abs (n, T, traverse (T::Ts) u)) ts
4ea9f2a8c093 fixed lambda-lifting: shift indices of bound variables correctly (after locking the required bound variables) and apply bound variables to the new function symbol in the right order;
boehmes
parents: 41198
diff changeset
   313
      | (u, ts) => traverses Ts u ts)
58057
883f3c4c928e renaming theory 'Old_SMT'
blanchet
parents: 58055
diff changeset
   314
    and in_trigger Ts ((c as @{const trigger}) $ p $ t) =
43554
9bece8cbb5be generalized introduction of explicit application constant: consider more functions as possible witness/instance of quantifiers than before (a constant of type T1 -> T2 -> T3 should be considered to have a rank less or equal to 1 if variables of type T2 -> T3 occur bound in a problem);
boehmes
parents: 43507
diff changeset
   315
          c $ in_pats Ts p $ in_weight Ts t
9bece8cbb5be generalized introduction of explicit application constant: consider more functions as possible witness/instance of quantifiers than before (a constant of type T1 -> T2 -> T3 should be considered to have a rank less or equal to 1 if variables of type T2 -> T3 occur bound in a problem);
boehmes
parents: 43507
diff changeset
   316
      | in_trigger Ts t = in_weight Ts t
9bece8cbb5be generalized introduction of explicit application constant: consider more functions as possible witness/instance of quantifiers than before (a constant of type T1 -> T2 -> T3 should be considered to have a rank less or equal to 1 if variables of type T2 -> T3 occur bound in a problem);
boehmes
parents: 43507
diff changeset
   317
    and in_pats Ts ps =
58057
883f3c4c928e renaming theory 'Old_SMT'
blanchet
parents: 58055
diff changeset
   318
      in_list @{typ "pattern list"}
883f3c4c928e renaming theory 'Old_SMT'
blanchet
parents: 58055
diff changeset
   319
        (in_list @{typ pattern} (in_pat Ts)) ps
883f3c4c928e renaming theory 'Old_SMT'
blanchet
parents: 58055
diff changeset
   320
    and in_pat Ts ((p as Const (@{const_name pat}, _)) $ t) =
43554
9bece8cbb5be generalized introduction of explicit application constant: consider more functions as possible witness/instance of quantifiers than before (a constant of type T1 -> T2 -> T3 should be considered to have a rank less or equal to 1 if variables of type T2 -> T3 occur bound in a problem);
boehmes
parents: 43507
diff changeset
   321
          p $ traverse Ts t
58057
883f3c4c928e renaming theory 'Old_SMT'
blanchet
parents: 58055
diff changeset
   322
      | in_pat Ts ((p as Const (@{const_name nopat}, _)) $ t) =
43554
9bece8cbb5be generalized introduction of explicit application constant: consider more functions as possible witness/instance of quantifiers than before (a constant of type T1 -> T2 -> T3 should be considered to have a rank less or equal to 1 if variables of type T2 -> T3 occur bound in a problem);
boehmes
parents: 43507
diff changeset
   323
          p $ traverse Ts t
9bece8cbb5be generalized introduction of explicit application constant: consider more functions as possible witness/instance of quantifiers than before (a constant of type T1 -> T2 -> T3 should be considered to have a rank less or equal to 1 if variables of type T2 -> T3 occur bound in a problem);
boehmes
parents: 43507
diff changeset
   324
      | in_pat _ t = raise TERM ("bad pattern", [t])
58057
883f3c4c928e renaming theory 'Old_SMT'
blanchet
parents: 58055
diff changeset
   325
    and in_weight Ts ((c as @{const weight}) $ w $ t) =
43554
9bece8cbb5be generalized introduction of explicit application constant: consider more functions as possible witness/instance of quantifiers than before (a constant of type T1 -> T2 -> T3 should be considered to have a rank less or equal to 1 if variables of type T2 -> T3 occur bound in a problem);
boehmes
parents: 43507
diff changeset
   326
          c $ w $ traverse Ts t
9bece8cbb5be generalized introduction of explicit application constant: consider more functions as possible witness/instance of quantifiers than before (a constant of type T1 -> T2 -> T3 should be considered to have a rank less or equal to 1 if variables of type T2 -> T3 occur bound in a problem);
boehmes
parents: 43507
diff changeset
   327
      | in_weight Ts t = traverse Ts t 
41232
4ea9f2a8c093 fixed lambda-lifting: shift indices of bound variables correctly (after locking the required bound variables) and apply bound variables to the new function symbol in the right order;
boehmes
parents: 41198
diff changeset
   328
    and traverses Ts t ts = Term.list_comb (t, map (traverse Ts) ts)
4ea9f2a8c093 fixed lambda-lifting: shift indices of bound variables correctly (after locking the required bound variables) and apply bound variables to the new function symbol in the right order;
boehmes
parents: 41198
diff changeset
   329
  in map (traverse []) ts end
41127
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41123
diff changeset
   330
58057
883f3c4c928e renaming theory 'Old_SMT'
blanchet
parents: 58055
diff changeset
   331
val fun_app_eq = mk_meta_eq @{thm fun_app_def}
41127
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41123
diff changeset
   332
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41123
diff changeset
   333
end
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41123
diff changeset
   334
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41123
diff changeset
   335
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41123
diff changeset
   336
(** map HOL formulas to FOL formulas (i.e., separate formulas froms terms) **)
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41123
diff changeset
   337
41281
679118e35378 removed odd decoration of built-in symbols as Vars (instead provide built-in desctructor functions along with their inverse functions);
boehmes
parents: 41250
diff changeset
   338
local
58057
883f3c4c928e renaming theory 'Old_SMT'
blanchet
parents: 58055
diff changeset
   339
  val term_bool = @{lemma "term_true ~= term_false"
883f3c4c928e renaming theory 'Old_SMT'
blanchet
parents: 58055
diff changeset
   340
    by (simp add: term_true_def term_false_def)}
41127
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41123
diff changeset
   341
41785
77dcc197df9a wrap occurrences of quantifiers in first-order terms (i.e., outside first-order formulas) in If-expressions
boehmes
parents: 41426
diff changeset
   342
  val is_quant = member (op =) [@{const_name All}, @{const_name Ex}]
77dcc197df9a wrap occurrences of quantifiers in first-order terms (i.e., outside first-order formulas) in If-expressions
boehmes
parents: 41426
diff changeset
   343
41281
679118e35378 removed odd decoration of built-in symbols as Vars (instead provide built-in desctructor functions along with their inverse functions);
boehmes
parents: 41250
diff changeset
   344
  val fol_rules = [
679118e35378 removed odd decoration of built-in symbols as Vars (instead provide built-in desctructor functions along with their inverse functions);
boehmes
parents: 41250
diff changeset
   345
    Let_def,
58057
883f3c4c928e renaming theory 'Old_SMT'
blanchet
parents: 58055
diff changeset
   346
    mk_meta_eq @{thm term_true_def},
883f3c4c928e renaming theory 'Old_SMT'
blanchet
parents: 58055
diff changeset
   347
    mk_meta_eq @{thm term_false_def},
41281
679118e35378 removed odd decoration of built-in symbols as Vars (instead provide built-in desctructor functions along with their inverse functions);
boehmes
parents: 41250
diff changeset
   348
    @{lemma "P = True == P" by (rule eq_reflection) simp},
679118e35378 removed odd decoration of built-in symbols as Vars (instead provide built-in desctructor functions along with their inverse functions);
boehmes
parents: 41250
diff changeset
   349
    @{lemma "if P then True else False == P" by (rule eq_reflection) simp}]
41127
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41123
diff changeset
   350
58057
883f3c4c928e renaming theory 'Old_SMT'
blanchet
parents: 58055
diff changeset
   351
  fun as_term t = @{const HOL.eq (bool)} $ t $ @{const term_true}
41127
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41123
diff changeset
   352
47533
5afe54e05406 avoid generating syntactically invalid patterns (with "if_then_else") in SMT-LIB files
blanchet
parents: 46529
diff changeset
   353
  exception BAD_PATTERN of unit
5afe54e05406 avoid generating syntactically invalid patterns (with "if_then_else") in SMT-LIB files
blanchet
parents: 46529
diff changeset
   354
5afe54e05406 avoid generating syntactically invalid patterns (with "if_then_else") in SMT-LIB files
blanchet
parents: 46529
diff changeset
   355
  fun wrap_in_if pat t =
5afe54e05406 avoid generating syntactically invalid patterns (with "if_then_else") in SMT-LIB files
blanchet
parents: 46529
diff changeset
   356
    if pat then
5afe54e05406 avoid generating syntactically invalid patterns (with "if_then_else") in SMT-LIB files
blanchet
parents: 46529
diff changeset
   357
      raise BAD_PATTERN ()
5afe54e05406 avoid generating syntactically invalid patterns (with "if_then_else") in SMT-LIB files
blanchet
parents: 46529
diff changeset
   358
    else
58057
883f3c4c928e renaming theory 'Old_SMT'
blanchet
parents: 58055
diff changeset
   359
      @{const If (bool)} $ t $ @{const term_true} $ @{const term_false}
41281
679118e35378 removed odd decoration of built-in symbols as Vars (instead provide built-in desctructor functions along with their inverse functions);
boehmes
parents: 41250
diff changeset
   360
679118e35378 removed odd decoration of built-in symbols as Vars (instead provide built-in desctructor functions along with their inverse functions);
boehmes
parents: 41250
diff changeset
   361
  fun is_builtin_conn_or_pred ctxt c ts =
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   362
    is_some (Old_SMT_Builtin.dest_builtin_conn ctxt c ts) orelse
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   363
    is_some (Old_SMT_Builtin.dest_builtin_pred ctxt c ts)
41127
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41123
diff changeset
   364
41281
679118e35378 removed odd decoration of built-in symbols as Vars (instead provide built-in desctructor functions along with their inverse functions);
boehmes
parents: 41250
diff changeset
   365
  fun builtin b 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: 41250
diff changeset
   366
    (case (Const c, ts) of
679118e35378 removed odd decoration of built-in symbols as Vars (instead provide built-in desctructor functions along with their inverse functions);
boehmes
parents: 41250
diff changeset
   367
      (@{const HOL.eq (bool)}, [t, u]) =>
58057
883f3c4c928e renaming theory 'Old_SMT'
blanchet
parents: 58055
diff changeset
   368
        if t = @{const term_true} orelse u = @{const term_true} then
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   369
          Old_SMT_Builtin.dest_builtin_eq ctxt t u
41281
679118e35378 removed odd decoration of built-in symbols as Vars (instead provide built-in desctructor functions along with their inverse functions);
boehmes
parents: 41250
diff changeset
   370
        else b 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: 41250
diff changeset
   371
    | _ => b 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: 41250
diff changeset
   372
in
41127
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41123
diff changeset
   373
41281
679118e35378 removed odd decoration of built-in symbols as Vars (instead provide built-in desctructor functions along with their inverse functions);
boehmes
parents: 41250
diff changeset
   374
fun folify ctxt =
41127
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41123
diff changeset
   375
  let
47533
5afe54e05406 avoid generating syntactically invalid patterns (with "if_then_else") in SMT-LIB files
blanchet
parents: 46529
diff changeset
   376
    fun in_list T f t = HOLogic.mk_list T (map_filter f (HOLogic.dest_list t))
41127
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41123
diff changeset
   377
47533
5afe54e05406 avoid generating syntactically invalid patterns (with "if_then_else") in SMT-LIB files
blanchet
parents: 46529
diff changeset
   378
    fun in_term pat t =
41127
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41123
diff changeset
   379
      (case Term.strip_comb t of
58057
883f3c4c928e renaming theory 'Old_SMT'
blanchet
parents: 58055
diff changeset
   380
        (@{const True}, []) => @{const term_true}
883f3c4c928e renaming theory 'Old_SMT'
blanchet
parents: 58055
diff changeset
   381
      | (@{const False}, []) => @{const term_false}
41281
679118e35378 removed odd decoration of built-in symbols as Vars (instead provide built-in desctructor functions along with their inverse functions);
boehmes
parents: 41250
diff changeset
   382
      | (u as Const (@{const_name If}, _), [t1, t2, t3]) =>
47533
5afe54e05406 avoid generating syntactically invalid patterns (with "if_then_else") in SMT-LIB files
blanchet
parents: 46529
diff changeset
   383
          if pat then raise BAD_PATTERN ()
5afe54e05406 avoid generating syntactically invalid patterns (with "if_then_else") in SMT-LIB files
blanchet
parents: 46529
diff changeset
   384
          else u $ in_form t1 $ in_term pat t2 $ in_term pat t3
41785
77dcc197df9a wrap occurrences of quantifiers in first-order terms (i.e., outside first-order formulas) in If-expressions
boehmes
parents: 41426
diff changeset
   385
      | (Const (c as (n, _)), ts) =>
47533
5afe54e05406 avoid generating syntactically invalid patterns (with "if_then_else") in SMT-LIB files
blanchet
parents: 46529
diff changeset
   386
          if is_builtin_conn_or_pred ctxt c ts then wrap_in_if pat (in_form t)
5afe54e05406 avoid generating syntactically invalid patterns (with "if_then_else") in SMT-LIB files
blanchet
parents: 46529
diff changeset
   387
          else if is_quant n then wrap_in_if pat (in_form t)
5afe54e05406 avoid generating syntactically invalid patterns (with "if_then_else") in SMT-LIB files
blanchet
parents: 46529
diff changeset
   388
          else Term.list_comb (Const c, map (in_term pat) ts)
5afe54e05406 avoid generating syntactically invalid patterns (with "if_then_else") in SMT-LIB files
blanchet
parents: 46529
diff changeset
   389
      | (Free c, ts) => Term.list_comb (Free c, map (in_term pat) ts)
41127
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41123
diff changeset
   390
      | _ => t)
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41123
diff changeset
   391
58057
883f3c4c928e renaming theory 'Old_SMT'
blanchet
parents: 58055
diff changeset
   392
    and in_weight ((c as @{const weight}) $ w $ t) = c $ w $ in_form t
41127
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41123
diff changeset
   393
      | in_weight t = in_form t 
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41123
diff changeset
   394
58057
883f3c4c928e renaming theory 'Old_SMT'
blanchet
parents: 58055
diff changeset
   395
    and in_pat ((p as Const (@{const_name pat}, _)) $ t) =
47533
5afe54e05406 avoid generating syntactically invalid patterns (with "if_then_else") in SMT-LIB files
blanchet
parents: 46529
diff changeset
   396
          p $ in_term true t
58057
883f3c4c928e renaming theory 'Old_SMT'
blanchet
parents: 58055
diff changeset
   397
      | in_pat ((p as Const (@{const_name nopat}, _)) $ t) =
47533
5afe54e05406 avoid generating syntactically invalid patterns (with "if_then_else") in SMT-LIB files
blanchet
parents: 46529
diff changeset
   398
          p $ in_term true t
41127
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41123
diff changeset
   399
      | in_pat t = raise TERM ("bad pattern", [t])
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41123
diff changeset
   400
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41123
diff changeset
   401
    and in_pats ps =
58057
883f3c4c928e renaming theory 'Old_SMT'
blanchet
parents: 58055
diff changeset
   402
      in_list @{typ "pattern list"}
883f3c4c928e renaming theory 'Old_SMT'
blanchet
parents: 58055
diff changeset
   403
        (SOME o in_list @{typ pattern} (try in_pat)) ps
41127
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41123
diff changeset
   404
58057
883f3c4c928e renaming theory 'Old_SMT'
blanchet
parents: 58055
diff changeset
   405
    and in_trigger ((c as @{const trigger}) $ p $ t) =
41232
4ea9f2a8c093 fixed lambda-lifting: shift indices of bound variables correctly (after locking the required bound variables) and apply bound variables to the new function symbol in the right order;
boehmes
parents: 41198
diff changeset
   406
          c $ in_pats p $ in_weight t
41281
679118e35378 removed odd decoration of built-in symbols as Vars (instead provide built-in desctructor functions along with their inverse functions);
boehmes
parents: 41250
diff changeset
   407
      | in_trigger t = in_weight t
41127
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41123
diff changeset
   408
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41123
diff changeset
   409
    and in_form t =
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41123
diff changeset
   410
      (case Term.strip_comb t of
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41123
diff changeset
   411
        (q as Const (qn, _), [Abs (n, T, u)]) =>
41785
77dcc197df9a wrap occurrences of quantifiers in first-order terms (i.e., outside first-order formulas) in If-expressions
boehmes
parents: 41426
diff changeset
   412
          if is_quant qn then q $ Abs (n, T, in_trigger u)
47533
5afe54e05406 avoid generating syntactically invalid patterns (with "if_then_else") in SMT-LIB files
blanchet
parents: 46529
diff changeset
   413
          else as_term (in_term false t)
41281
679118e35378 removed odd decoration of built-in symbols as Vars (instead provide built-in desctructor functions along with their inverse functions);
boehmes
parents: 41250
diff changeset
   414
      | (Const c, ts) =>
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   415
          (case Old_SMT_Builtin.dest_builtin_conn ctxt c ts of
41281
679118e35378 removed odd decoration of built-in symbols as Vars (instead provide built-in desctructor functions along with their inverse functions);
boehmes
parents: 41250
diff changeset
   416
            SOME (_, _, us, mk) => mk (map in_form us)
679118e35378 removed odd decoration of built-in symbols as Vars (instead provide built-in desctructor functions along with their inverse functions);
boehmes
parents: 41250
diff changeset
   417
          | NONE =>
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   418
              (case Old_SMT_Builtin.dest_builtin_pred ctxt c ts of
47533
5afe54e05406 avoid generating syntactically invalid patterns (with "if_then_else") in SMT-LIB files
blanchet
parents: 46529
diff changeset
   419
                SOME (_, _, us, mk) => mk (map (in_term false) us)
5afe54e05406 avoid generating syntactically invalid patterns (with "if_then_else") in SMT-LIB files
blanchet
parents: 46529
diff changeset
   420
              | NONE => as_term (in_term false t)))
5afe54e05406 avoid generating syntactically invalid patterns (with "if_then_else") in SMT-LIB files
blanchet
parents: 46529
diff changeset
   421
      | _ => as_term (in_term false t))
41127
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41123
diff changeset
   422
  in
42319
9a8ba59aed06 unfold and eta-contract let expressions before lambda-lifting to avoid bad terms
boehmes
parents: 41785
diff changeset
   423
    map in_form #>
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   424
    cons (Old_SMT_Utils.prop_of term_bool) #>
41281
679118e35378 removed odd decoration of built-in symbols as Vars (instead provide built-in desctructor functions along with their inverse functions);
boehmes
parents: 41250
diff changeset
   425
    pair (fol_rules, [term_bool], builtin)
41127
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41123
diff changeset
   426
  end
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41123
diff changeset
   427
41281
679118e35378 removed odd decoration of built-in symbols as Vars (instead provide built-in desctructor functions along with their inverse functions);
boehmes
parents: 41250
diff changeset
   428
end
41127
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41123
diff changeset
   429
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41123
diff changeset
   430
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41123
diff changeset
   431
(* translation into intermediate format *)
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41123
diff changeset
   432
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41123
diff changeset
   433
(** utility functions **)
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   434
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   435
val quantifier = (fn
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   436
    @{const_name All} => SOME SForall
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   437
  | @{const_name Ex} => SOME SExists
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   438
  | _ => NONE)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   439
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   440
fun group_quant qname Ts (t as Const (q, _) $ Abs (_, T, u)) =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   441
      if q = qname then group_quant qname (T :: Ts) u else (Ts, t)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   442
  | group_quant _ Ts t = (Ts, t)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   443
58057
883f3c4c928e renaming theory 'Old_SMT'
blanchet
parents: 58055
diff changeset
   444
fun dest_weight (@{const weight} $ w $ t) =
41173
7c6178d45cc8 fixed checking and translation of weights (previously, weights occurring in terms were rejected, and weight numbers were unintended translated into Vars)
boehmes
parents: 41172
diff changeset
   445
      (SOME (snd (HOLogic.dest_number w)), t)
40664
e023788a91a1 added support for quantifier weight annotations
boehmes
parents: 40663
diff changeset
   446
  | dest_weight t = (NONE, t)
e023788a91a1 added support for quantifier weight annotations
boehmes
parents: 40663
diff changeset
   447
58057
883f3c4c928e renaming theory 'Old_SMT'
blanchet
parents: 58055
diff changeset
   448
fun dest_pat (Const (@{const_name pat}, _) $ t) = (t, true)
883f3c4c928e renaming theory 'Old_SMT'
blanchet
parents: 58055
diff changeset
   449
  | dest_pat (Const (@{const_name nopat}, _) $ t) = (t, false)
41127
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41123
diff changeset
   450
  | dest_pat t = raise TERM ("bad pattern", [t])
37124
fe22fc54b876 hide constants and types introduced by SMT,
boehmes
parents: 36899
diff changeset
   451
fe22fc54b876 hide constants and types introduced by SMT,
boehmes
parents: 36899
diff changeset
   452
fun dest_pats [] = I
fe22fc54b876 hide constants and types introduced by SMT,
boehmes
parents: 36899
diff changeset
   453
  | dest_pats ts =
fe22fc54b876 hide constants and types introduced by SMT,
boehmes
parents: 36899
diff changeset
   454
      (case map dest_pat ts |> split_list ||> distinct (op =) of
fe22fc54b876 hide constants and types introduced by SMT,
boehmes
parents: 36899
diff changeset
   455
        (ps, [true]) => cons (SPat ps)
fe22fc54b876 hide constants and types introduced by SMT,
boehmes
parents: 36899
diff changeset
   456
      | (ps, [false]) => cons (SNoPat ps)
41127
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41123
diff changeset
   457
      | _ => raise TERM ("bad multi-pattern", ts))
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   458
58057
883f3c4c928e renaming theory 'Old_SMT'
blanchet
parents: 58055
diff changeset
   459
fun dest_trigger (@{const trigger} $ tl $ t) =
37124
fe22fc54b876 hide constants and types introduced by SMT,
boehmes
parents: 36899
diff changeset
   460
      (rev (fold (dest_pats o HOLogic.dest_list) (HOLogic.dest_list tl) []), t)
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   461
  | dest_trigger t = ([], t)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   462
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   463
fun dest_quant qn T t = quantifier qn |> Option.map (fn q =>
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   464
  let
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   465
    val (Ts, u) = group_quant qn [T] t
40664
e023788a91a1 added support for quantifier weight annotations
boehmes
parents: 40663
diff changeset
   466
    val (ps, p) = dest_trigger u
e023788a91a1 added support for quantifier weight annotations
boehmes
parents: 40663
diff changeset
   467
    val (w, b) = dest_weight p
e023788a91a1 added support for quantifier weight annotations
boehmes
parents: 40663
diff changeset
   468
  in (q, rev Ts, ps, w, b) end)
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   469
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   470
fun fold_map_pat f (SPat ts) = fold_map f ts #>> SPat
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   471
  | fold_map_pat f (SNoPat ts) = fold_map f ts #>> SNoPat
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   472
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   473
41127
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41123
diff changeset
   474
(** translation from Isabelle terms into SMT intermediate terms **)
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   475
41281
679118e35378 removed odd decoration of built-in symbols as Vars (instead provide built-in desctructor functions along with their inverse functions);
boehmes
parents: 41250
diff changeset
   476
fun intermediate header dtyps builtin ctxt ts trx =
41059
d2b1fc1b8e19 centralized handling of built-in types and constants;
boehmes
parents: 41057
diff changeset
   477
  let
41127
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41123
diff changeset
   478
    fun transT (T as TFree _) = add_typ T true
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41123
diff changeset
   479
      | transT (T as TVar _) = (fn _ => raise TYPE ("bad SMT type", [T], []))
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41123
diff changeset
   480
      | transT (T as Type _) =
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   481
          (case Old_SMT_Builtin.dest_builtin_typ ctxt T of
39298
5aefb5bc8a93 added preliminary support for SMT datatypes (for now restricted to tuples and lists); only the Z3 interface (in oracle mode) makes use of it, there is especially no Z3 proof reconstruction support for datatypes yet
boehmes
parents: 37124
diff changeset
   482
            SOME n => pair n
41127
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41123
diff changeset
   483
          | NONE => add_typ T true)
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   484
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   485
    fun app n ts = SApp (n, ts)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   486
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   487
    fun trans t =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   488
      (case Term.strip_comb t of
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   489
        (Const (qn, _), [Abs (_, T, t1)]) =>
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   490
          (case dest_quant qn T t1 of
40664
e023788a91a1 added support for quantifier weight annotations
boehmes
parents: 40663
diff changeset
   491
            SOME (q, Ts, ps, w, b) =>
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   492
              fold_map transT Ts ##>> fold_map (fold_map_pat trans) ps ##>>
40664
e023788a91a1 added support for quantifier weight annotations
boehmes
parents: 40663
diff changeset
   493
              trans b #>> (fn ((Ts', ps'), b') => SQua (q, Ts', ps', w, b'))
41127
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41123
diff changeset
   494
          | NONE => raise TERM ("unsupported quantifier", [t]))
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   495
      | (Const (@{const_name Let}, _), [t1, Abs (_, T, t2)]) =>
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   496
          transT T ##>> trans t1 ##>> trans t2 #>>
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   497
          (fn ((U, u1), u2) => SLet (U, u1, u2))
41281
679118e35378 removed odd decoration of built-in symbols as Vars (instead provide built-in desctructor functions along with their inverse functions);
boehmes
parents: 41250
diff changeset
   498
      | (u as Const (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: 41250
diff changeset
   499
          (case builtin ctxt c ts of
679118e35378 removed odd decoration of built-in symbols as Vars (instead provide built-in desctructor functions along with their inverse functions);
boehmes
parents: 41250
diff changeset
   500
            SOME (n, _, us, _) => fold_map trans us #>> app n
679118e35378 removed odd decoration of built-in symbols as Vars (instead provide built-in desctructor functions along with their inverse functions);
boehmes
parents: 41250
diff changeset
   501
          | NONE => transs u T ts)
41127
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41123
diff changeset
   502
      | (u as Free (_, T), ts) => transs u T ts
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   503
      | (Bound i, []) => pair (SVar i)
41127
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41123
diff changeset
   504
      | _ => raise TERM ("bad SMT term", [t]))
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41123
diff changeset
   505
 
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   506
    and transs t T ts =
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   507
      let val (Us, U) = Old_SMT_Utils.dest_funT (length ts) T
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   508
      in
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   509
        fold_map transT Us ##>> transT U #-> (fn Up =>
41127
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41123
diff changeset
   510
        add_fun t (SOME Up) ##>> fold_map trans ts #>> SApp)
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   511
      end
41127
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41123
diff changeset
   512
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41123
diff changeset
   513
    val (us, trx') = fold_map trans ts trx
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41123
diff changeset
   514
  in ((sign_of (header ts) dtyps trx', us), trx') end
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41123
diff changeset
   515
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41123
diff changeset
   516
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41123
diff changeset
   517
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41123
diff changeset
   518
(* translation *)
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41123
diff changeset
   519
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41123
diff changeset
   520
structure Configs = Generic_Data
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41123
diff changeset
   521
(
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   522
  type T = (Proof.context -> config) Old_SMT_Utils.dict
41127
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41123
diff changeset
   523
  val empty = []
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41123
diff changeset
   524
  val extend = I
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   525
  fun merge data = Old_SMT_Utils.dict_merge fst data
41127
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41123
diff changeset
   526
)
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41123
diff changeset
   527
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   528
fun add_config (cs, cfg) = Configs.map (Old_SMT_Utils.dict_update (cs, cfg))
41127
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41123
diff changeset
   529
41232
4ea9f2a8c093 fixed lambda-lifting: shift indices of bound variables correctly (after locking the required bound variables) and apply bound variables to the new function symbol in the right order;
boehmes
parents: 41198
diff changeset
   530
fun get_config ctxt = 
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   531
  let val cs = Old_SMT_Config.solver_class_of ctxt
41232
4ea9f2a8c093 fixed lambda-lifting: shift indices of bound variables correctly (after locking the required bound variables) and apply bound variables to the new function symbol in the right order;
boehmes
parents: 41198
diff changeset
   532
  in
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   533
    (case Old_SMT_Utils.dict_get (Configs.get (Context.Proof ctxt)) cs of
41232
4ea9f2a8c093 fixed lambda-lifting: shift indices of bound variables correctly (after locking the required bound variables) and apply bound variables to the new function symbol in the right order;
boehmes
parents: 41198
diff changeset
   534
      SOME cfg => cfg ctxt
4ea9f2a8c093 fixed lambda-lifting: shift indices of bound variables correctly (after locking the required bound variables) and apply bound variables to the new function symbol in the right order;
boehmes
parents: 41198
diff changeset
   535
    | NONE => error ("SMT: no translation configuration found " ^
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   536
        "for solver class " ^ quote (Old_SMT_Utils.string_of_class cs)))
41232
4ea9f2a8c093 fixed lambda-lifting: shift indices of bound variables correctly (after locking the required bound variables) and apply bound variables to the new function symbol in the right order;
boehmes
parents: 41198
diff changeset
   537
  end
4ea9f2a8c093 fixed lambda-lifting: shift indices of bound variables correctly (after locking the required bound variables) and apply bound variables to the new function symbol in the right order;
boehmes
parents: 41198
diff changeset
   538
41127
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41123
diff changeset
   539
fun translate ctxt comments ithms =
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41123
diff changeset
   540
  let
41232
4ea9f2a8c093 fixed lambda-lifting: shift indices of bound variables correctly (after locking the required bound variables) and apply bound variables to the new function symbol in the right order;
boehmes
parents: 41198
diff changeset
   541
    val {prefixes, is_fol, header, has_datatypes, serialize} = get_config ctxt
4ea9f2a8c093 fixed lambda-lifting: shift indices of bound variables correctly (after locking the required bound variables) and apply bound variables to the new function symbol in the right order;
boehmes
parents: 41198
diff changeset
   542
41127
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41123
diff changeset
   543
    val with_datatypes =
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   544
      has_datatypes andalso Config.get ctxt Old_SMT_Config.datatypes
41127
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41123
diff changeset
   545
41426
09615ed31f04 re-implemented support for datatypes (including records and typedefs);
boehmes
parents: 41328
diff changeset
   546
    fun no_dtyps (tr_context, ctxt) ts =
09615ed31f04 re-implemented support for datatypes (including records and typedefs);
boehmes
parents: 41328
diff changeset
   547
      ((Termtab.empty, [], tr_context, ctxt), ts)
41127
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41123
diff changeset
   548
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   549
    val ts1 = map (Envir.beta_eta_contract o Old_SMT_Utils.prop_of o snd) ithms
41127
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41123
diff changeset
   550
41426
09615ed31f04 re-implemented support for datatypes (including records and typedefs);
boehmes
parents: 41328
diff changeset
   551
    val ((funcs, dtyps, tr_context, ctxt1), ts2) =
41127
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41123
diff changeset
   552
      ((make_tr_context prefixes, ctxt), ts1)
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41123
diff changeset
   553
      |-> (if with_datatypes then collect_datatypes_and_records else no_dtyps)
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41123
diff changeset
   554
43929
61d432e51aff generalized lambda-lifting such that it is less specifically tailored for SMT (it does not anymore dependent on any SMT-specific code)
boehmes
parents: 43928
diff changeset
   555
    fun is_binder (Const (@{const_name Let}, _) $ _) = true
61d432e51aff generalized lambda-lifting such that it is less specifically tailored for SMT (it does not anymore dependent on any SMT-specific code)
boehmes
parents: 43928
diff changeset
   556
      | is_binder t = Lambda_Lifting.is_quantifier t
61d432e51aff generalized lambda-lifting such that it is less specifically tailored for SMT (it does not anymore dependent on any SMT-specific code)
boehmes
parents: 43928
diff changeset
   557
61d432e51aff generalized lambda-lifting such that it is less specifically tailored for SMT (it does not anymore dependent on any SMT-specific code)
boehmes
parents: 43928
diff changeset
   558
    fun mk_trigger ((q as Const (@{const_name All}, _)) $ Abs (n, T, t)) =
61d432e51aff generalized lambda-lifting such that it is less specifically tailored for SMT (it does not anymore dependent on any SMT-specific code)
boehmes
parents: 43928
diff changeset
   559
          q $ Abs (n, T, mk_trigger t)
61d432e51aff generalized lambda-lifting such that it is less specifically tailored for SMT (it does not anymore dependent on any SMT-specific code)
boehmes
parents: 43928
diff changeset
   560
      | mk_trigger (eq as (Const (@{const_name HOL.eq}, T) $ lhs $ _)) =
58057
883f3c4c928e renaming theory 'Old_SMT'
blanchet
parents: 58055
diff changeset
   561
          Term.domain_type T --> @{typ pattern}
883f3c4c928e renaming theory 'Old_SMT'
blanchet
parents: 58055
diff changeset
   562
          |> (fn T => Const (@{const_name pat}, T) $ lhs)
883f3c4c928e renaming theory 'Old_SMT'
blanchet
parents: 58055
diff changeset
   563
          |> HOLogic.mk_list @{typ pattern} o single
883f3c4c928e renaming theory 'Old_SMT'
blanchet
parents: 58055
diff changeset
   564
          |> HOLogic.mk_list @{typ "pattern list"} o single
883f3c4c928e renaming theory 'Old_SMT'
blanchet
parents: 58055
diff changeset
   565
          |> (fn t => @{const trigger} $ t $ eq)
43929
61d432e51aff generalized lambda-lifting such that it is less specifically tailored for SMT (it does not anymore dependent on any SMT-specific code)
boehmes
parents: 43928
diff changeset
   566
      | mk_trigger t = t
61d432e51aff generalized lambda-lifting such that it is less specifically tailored for SMT (it does not anymore dependent on any SMT-specific code)
boehmes
parents: 43928
diff changeset
   567
41127
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41123
diff changeset
   568
    val (ctxt2, ts3) =
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41123
diff changeset
   569
      ts2
42319
9a8ba59aed06 unfold and eta-contract let expressions before lambda-lifting to avoid bad terms
boehmes
parents: 41785
diff changeset
   570
      |> eta_expand ctxt1 is_fol funcs
43929
61d432e51aff generalized lambda-lifting such that it is less specifically tailored for SMT (it does not anymore dependent on any SMT-specific code)
boehmes
parents: 43928
diff changeset
   571
      |> rpair ctxt1
61d432e51aff generalized lambda-lifting such that it is less specifically tailored for SMT (it does not anymore dependent on any SMT-specific code)
boehmes
parents: 43928
diff changeset
   572
      |-> Lambda_Lifting.lift_lambdas NONE is_binder
61d432e51aff generalized lambda-lifting such that it is less specifically tailored for SMT (it does not anymore dependent on any SMT-specific code)
boehmes
parents: 43928
diff changeset
   573
      |-> (fn (ts', defs) => fn ctxt' =>
61d432e51aff generalized lambda-lifting such that it is less specifically tailored for SMT (it does not anymore dependent on any SMT-specific code)
boehmes
parents: 43928
diff changeset
   574
          map mk_trigger defs @ ts'
61d432e51aff generalized lambda-lifting such that it is less specifically tailored for SMT (it does not anymore dependent on any SMT-specific code)
boehmes
parents: 43928
diff changeset
   575
          |> intro_explicit_application ctxt' funcs 
61d432e51aff generalized lambda-lifting such that it is less specifically tailored for SMT (it does not anymore dependent on any SMT-specific code)
boehmes
parents: 43928
diff changeset
   576
          |> pair ctxt')
41127
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41123
diff changeset
   577
41281
679118e35378 removed odd decoration of built-in symbols as Vars (instead provide built-in desctructor functions along with their inverse functions);
boehmes
parents: 41250
diff changeset
   578
    val ((rewrite_rules, extra_thms, builtin), ts4) =
679118e35378 removed odd decoration of built-in symbols as Vars (instead provide built-in desctructor functions along with their inverse functions);
boehmes
parents: 41250
diff changeset
   579
      (if is_fol then folify ctxt2 else pair ([], [], I)) ts3
41127
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41123
diff changeset
   580
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41123
diff changeset
   581
    val rewrite_rules' = fun_app_eq :: rewrite_rules
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   582
  in
41127
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41123
diff changeset
   583
    (ts4, tr_context)
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   584
    |-> intermediate header dtyps (builtin Old_SMT_Builtin.dest_builtin) ctxt2
41127
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41123
diff changeset
   585
    |>> uncurry (serialize comments)
41281
679118e35378 removed odd decoration of built-in symbols as Vars (instead provide built-in desctructor functions along with their inverse functions);
boehmes
parents: 41250
diff changeset
   586
    ||> recon_of ctxt2 rewrite_rules' extra_thms ithms
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   587
  end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   588
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   589
end