src/HOL/Tools/SMT/z3_proof_parser.ML
author boehmes
Wed, 12 May 2010 23:54:02 +0200
changeset 36898 8e55aa1306c5
child 36899 bcd6fce5bf06
permissions -rw-r--r--
integrated SMT into the HOL image
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
     1
(*  Title:      HOL/Tools/SMT/z3_proof_parser.ML
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
Parser for Z3 proofs.
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
     5
*)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
     6
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
     7
signature Z3_PROOF_PARSER =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
     8
sig
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
     9
  (* proof rules *)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    10
  datatype rule = TrueAxiom | Asserted | Goal | ModusPonens | Reflexivity |
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    11
    Symmetry | Transitivity | TransitivityStar | Monotonicity | QuantIntro |
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    12
    Distributivity | AndElim | NotOrElim | Rewrite | RewriteStar | PullQuant |
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    13
    PullQuantStar | PushQuant | ElimUnusedVars | DestEqRes | QuantInst |
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    14
    Hypothesis | Lemma | UnitResolution | IffTrue | IffFalse | Commutativity |
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    15
    DefAxiom | IntroDef | ApplyDef | IffOeq | NnfPos | NnfNeg | NnfStar |
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    16
    CnfStar | Skolemize | ModusPonensOeq | ThLemma
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    17
  val string_of_rule: rule -> string
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    18
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    19
  (* proof parser *)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    20
  datatype proof_step = Proof_Step of {
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    21
    rule: rule,
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    22
    prems: int list,
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    23
    prop: cterm }
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    24
  val parse: Proof.context -> typ Symtab.table -> term Symtab.table ->
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    25
    string list ->
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    26
    int * (proof_step Inttab.table * string list * Proof.context)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    27
end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    28
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    29
structure Z3_Proof_Parser: Z3_PROOF_PARSER =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    30
struct
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    31
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    32
(** proof rules **)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    33
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    34
datatype rule = TrueAxiom | Asserted | Goal | ModusPonens | Reflexivity |
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    35
  Symmetry | Transitivity | TransitivityStar | Monotonicity | QuantIntro |
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    36
  Distributivity | AndElim | NotOrElim | Rewrite | RewriteStar | PullQuant |
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    37
  PullQuantStar | PushQuant | ElimUnusedVars | DestEqRes | QuantInst |
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    38
  Hypothesis | Lemma | UnitResolution | IffTrue | IffFalse | Commutativity |
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    39
  DefAxiom | IntroDef | ApplyDef | IffOeq | NnfPos | NnfNeg | NnfStar |
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    40
  CnfStar | Skolemize | ModusPonensOeq | ThLemma
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    41
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    42
val rule_names = Symtab.make [
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    43
  ("true-axiom", TrueAxiom),
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    44
  ("asserted", Asserted),
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    45
  ("goal", Goal),
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    46
  ("mp", ModusPonens),
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    47
  ("refl", Reflexivity),
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    48
  ("symm", Symmetry),
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    49
  ("trans", Transitivity),
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    50
  ("trans*", TransitivityStar),
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    51
  ("monotonicity", Monotonicity),
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    52
  ("quant-intro", QuantIntro),
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    53
  ("distributivity", Distributivity),
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    54
  ("and-elim", AndElim),
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    55
  ("not-or-elim", NotOrElim),
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    56
  ("rewrite", Rewrite),
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    57
  ("rewrite*", RewriteStar),
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    58
  ("pull-quant", PullQuant),
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    59
  ("pull-quant*", PullQuantStar),
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    60
  ("push-quant", PushQuant),
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    61
  ("elim-unused", ElimUnusedVars),
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    62
  ("der", DestEqRes),
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    63
  ("quant-inst", QuantInst),
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    64
  ("hypothesis", Hypothesis),
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    65
  ("lemma", Lemma),
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    66
  ("unit-resolution", UnitResolution),
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    67
  ("iff-true", IffTrue),
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    68
  ("iff-false", IffFalse),
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    69
  ("commutativity", Commutativity),
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    70
  ("def-axiom", DefAxiom),
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    71
  ("intro-def", IntroDef),
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    72
  ("apply-def", ApplyDef),
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    73
  ("iff~", IffOeq),
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    74
  ("nnf-pos", NnfPos),
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    75
  ("nnf-neg", NnfNeg),
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    76
  ("nnf*", NnfStar),
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    77
  ("cnf*", CnfStar),
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    78
  ("sk", Skolemize),
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    79
  ("mp~", ModusPonensOeq),
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    80
  ("th-lemma", ThLemma)]
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    81
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    82
fun string_of_rule r =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    83
  let fun eq_rule (s, r') = if r = r' then SOME s else NONE 
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    84
  in the (Symtab.get_first eq_rule rule_names) end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    85
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
(** certified terms and variables **)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    89
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    90
val (var_prefix, decl_prefix) = ("v", "sk")  (* must be distinct *)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    91
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    92
fun instTs cUs (cTs, ct) = Thm.instantiate_cterm (cTs ~~ cUs, []) ct
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    93
fun instT cU (cT, ct) = instTs [cU] ([cT], ct)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    94
fun mk_inst_pair destT cpat = (destT (Thm.ctyp_of_term cpat), cpat)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    95
val destT1 = hd o Thm.dest_ctyp
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    96
val destT2 = hd o tl o Thm.dest_ctyp
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    97
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    98
fun ctyp_of (ct, _) = Thm.ctyp_of_term ct
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    99
fun instT' t = instT (ctyp_of t)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   100
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   101
fun certify ctxt = Thm.cterm_of (ProofContext.theory_of ctxt)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   102
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   103
val maxidx_of = #maxidx o Thm.rep_cterm
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   104
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   105
fun mk_inst ctxt vars =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   106
  let
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   107
    val max = fold (Integer.max o fst) vars 0
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   108
    val ns = fst (Variable.variant_fixes (replicate (max + 1) var_prefix) ctxt)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   109
    fun mk (i, v) = (v, certify ctxt (Free (nth ns i, #T (Thm.rep_cterm v))))
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   110
  in map mk vars end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   111
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   112
fun close ctxt (ct, vars) =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   113
  let
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   114
    val inst = mk_inst ctxt vars
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   115
    val mk_prop = Thm.capply @{cterm Trueprop}
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   116
    val names = fold (Term.add_free_names o Thm.term_of o snd) inst []
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   117
  in (mk_prop (Thm.instantiate_cterm ([], inst) ct), names) end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   118
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   119
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   120
fun mk_bound thy (i, T) =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   121
  let val ct = Thm.cterm_of thy (Var ((Name.uu, 0), T))
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   122
  in (ct, [(i, ct)]) end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   123
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   124
local
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   125
  fun mk_quant thy q T (ct, vars) =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   126
    let
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   127
      val cv =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   128
        (case AList.lookup (op =) vars 0 of
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   129
          SOME cv => cv
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   130
        | _ => Thm.cterm_of thy (Var ((Name.uu, maxidx_of ct + 1), T)))
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   131
      val cq = instT (Thm.ctyp_of_term cv) q
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   132
      fun dec (i, v) = if i = 0 then NONE else SOME (i-1, v)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   133
    in (Thm.capply cq (Thm.cabs cv ct), map_filter dec vars) end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   134
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   135
  val forall = mk_inst_pair (destT1 o destT1) @{cpat All}
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   136
  val exists = mk_inst_pair (destT1 o destT1) @{cpat Ex}
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   137
in
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   138
fun mk_forall thy = fold_rev (mk_quant thy forall)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   139
fun mk_exists thy = fold_rev (mk_quant thy exists)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   140
end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   141
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   142
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   143
local
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   144
  fun equal_var cv (_, cu) = (cv aconvc cu)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   145
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   146
  fun apply (ct2, vars2) (ct1, vars1) =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   147
    let
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   148
      val incr = Thm.incr_indexes_cterm (maxidx_of ct1 + maxidx_of ct2 + 2)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   149
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   150
      fun part (v as (i, cv)) =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   151
        (case AList.lookup (op =) vars1 i of
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   152
          SOME cu => apfst (if cu aconvc cv then I else cons (cv, cu))
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   153
        | NONE =>
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   154
            if not (exists (equal_var cv) vars1) then apsnd (cons v)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   155
            else
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   156
              let val cv' = incr cv
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   157
              in apfst (cons (cv, cv')) #> apsnd (cons (i, cv')) end)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   158
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   159
      val (ct2', vars2') =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   160
        if null vars1 then (ct2, vars2)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   161
        else fold part vars2 ([], [])
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   162
          |>> (fn inst => Thm.instantiate_cterm ([], inst) ct2)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   163
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   164
    in (Thm.capply ct1 ct2', vars1 @ vars2') end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   165
in
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   166
fun mk_fun ct ts = fold apply ts (ct, [])
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   167
fun mk_binop f t u = mk_fun f [t, u]
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   168
fun mk_nary _ e [] = e
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   169
  | mk_nary ct _ es = uncurry (fold_rev (mk_binop ct)) (split_last es)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   170
end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   171
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   172
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   173
val mk_true = mk_fun @{cterm "~False"} []
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   174
val mk_false = mk_fun @{cterm "False"} []
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   175
fun mk_not t = mk_fun @{cterm Not} [t]
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   176
val mk_imp = mk_binop @{cterm "op -->"}
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   177
val mk_iff = mk_binop @{cterm "op = :: bool => _"}
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   178
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   179
val eq = mk_inst_pair destT1 @{cpat "op ="}
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   180
fun mk_eq t u = mk_binop (instT' t eq) t u
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   181
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   182
val if_term = mk_inst_pair (destT1 o destT2) @{cpat If}
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   183
fun mk_if c t u = mk_fun (instT' t if_term) [c, t, u]
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   184
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   185
val nil_term = mk_inst_pair destT1 @{cpat Nil}
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   186
val cons_term = mk_inst_pair destT1 @{cpat Cons}
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   187
fun mk_list cT es =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   188
  fold_rev (mk_binop (instT cT cons_term)) es (mk_fun (instT cT nil_term) [])
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   189
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   190
val distinct = mk_inst_pair (destT1 o destT1) @{cpat distinct}
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   191
fun mk_distinct [] = mk_true
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   192
  | mk_distinct (es as (e :: _)) =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   193
      mk_fun (instT' e distinct) [mk_list (ctyp_of e) es]
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   194
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   195
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   196
(* arithmetic *)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   197
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   198
fun mk_int_num i = mk_fun (Numeral.mk_cnumber @{ctyp int} i) []
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   199
fun mk_real_num i = mk_fun (Numeral.mk_cnumber @{ctyp real} i) []
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   200
fun mk_real_frac_num (e, NONE) = mk_real_num e
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   201
  | mk_real_frac_num (e, SOME d) =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   202
      mk_binop @{cterm "op / :: real => _"} (mk_real_num e) (mk_real_num d)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   203
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   204
fun has_int_type e = (Thm.typ_of (ctyp_of e) = @{typ int})
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   205
fun choose e i r = if has_int_type e then i else r
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   206
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   207
val uminus_i = @{cterm "uminus :: int => _"}
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   208
val uminus_r = @{cterm "uminus :: real => _"}
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   209
fun mk_uminus e = mk_fun (choose e uminus_i uminus_r) [e]
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   210
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   211
fun arith_op int_op real_op t u = mk_binop (choose t int_op real_op) t u
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   212
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   213
val mk_add = arith_op @{cterm "op + :: int => _"} @{cterm "op + :: real => _"}
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   214
val mk_sub = arith_op @{cterm "op - :: int => _"} @{cterm "op - :: real => _"}
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   215
val mk_mul = arith_op @{cterm "op * :: int => _"} @{cterm "op * :: real => _"}
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   216
val mk_int_div = mk_binop @{cterm "op div :: int => _"}
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   217
val mk_real_div = mk_binop @{cterm "op / :: real => _"}
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   218
val mk_mod = mk_binop @{cterm "op mod :: int => _"}
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   219
val mk_lt = arith_op @{cterm "op < :: int => _"} @{cterm "op < :: real => _"}
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   220
val mk_le = arith_op @{cterm "op <= :: int => _"} @{cterm "op <= :: real => _"}
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   221
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   222
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   223
(* arrays *)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   224
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   225
val access = mk_inst_pair (Thm.dest_ctyp o destT1) @{cpat apply}
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   226
fun mk_access array index =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   227
  let val cTs = Thm.dest_ctyp (ctyp_of array)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   228
  in mk_fun (instTs cTs access) [array, index] end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   229
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   230
val update = mk_inst_pair (Thm.dest_ctyp o destT1) @{cpat fun_upd}
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   231
fun mk_update array index value =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   232
  let val cTs = Thm.dest_ctyp (ctyp_of array)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   233
  in mk_fun (instTs cTs update) [array, index, value] end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   234
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   235
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   236
(* bitvectors *)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   237
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   238
fun mk_binT size =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   239
  let
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   240
    fun bitT i T =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   241
      if i = 0
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   242
      then Type (@{type_name "Numeral_Type.bit0"}, [T])
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   243
      else Type (@{type_name "Numeral_Type.bit1"}, [T])
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   244
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   245
    fun binT i =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   246
      if i = 0 then @{typ "Numeral_Type.num0"}
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   247
      else if i = 1 then @{typ "Numeral_Type.num1"}
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   248
      else let val (q, r) = Integer.div_mod i 2 in bitT r (binT q) end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   249
  in
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   250
    if size >= 0 then binT size
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   251
    else raise TYPE ("mk_binT: " ^ string_of_int size, [], [])
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   252
  end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   253
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   254
fun mk_wordT size = Type (@{type_name "word"}, [mk_binT size])
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   255
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   256
fun mk_bv_num thy (num, size) =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   257
  mk_fun (Numeral.mk_cnumber (Thm.ctyp_of thy (mk_wordT size)) num) []
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   258
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   259
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   260
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   261
(** proof parser **)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   262
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   263
datatype proof_step = Proof_Step of {
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   264
  rule: rule,
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   265
  prems: int list,
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   266
  prop: cterm }
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   267
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   268
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   269
(* parser context *)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   270
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   271
fun make_context ctxt typs terms =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   272
  let
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   273
    val ctxt' = 
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   274
      ctxt
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   275
      |> Symtab.fold (Variable.declare_typ o snd) typs
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   276
      |> Symtab.fold (Variable.declare_term o snd) terms
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   277
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   278
    fun cert @{term True} = @{cterm "~False"}
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   279
      | cert t = certify ctxt' t
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   280
  in (typs, Symtab.map cert terms, Inttab.empty, Inttab.empty, [], ctxt') end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   281
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   282
fun fresh_name n (typs, terms, exprs, steps, vars, ctxt) =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   283
  let val (n', ctxt') = yield_singleton Variable.variant_fixes n ctxt
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   284
  in (n', (typs, terms, exprs, steps, vars, ctxt')) end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   285
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   286
fun theory_of (_, _, _, _, _, ctxt) = ProofContext.theory_of ctxt
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   287
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   288
fun typ_of_sort n (cx as (typs, _, _, _, _, _)) =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   289
  (case Symtab.lookup typs n of
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   290
    SOME T => (T, cx)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   291
  | NONE => cx
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   292
      |> fresh_name ("'" ^ n) |>> TFree o rpair @{sort type}
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   293
      |> (fn (T, (typs, terms, exprs, steps, vars, ctxt)) =>
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   294
           (T, (Symtab.update (n, T) typs, terms, exprs, steps, vars, ctxt))))
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   295
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   296
fun add_decl (n, T) (cx as (_, terms, _, _, _, _)) =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   297
  (case Symtab.lookup terms n of
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   298
    SOME _ => cx
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   299
  | NONE => cx |> fresh_name (decl_prefix ^ n)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   300
      |> (fn (m, (typs, terms, exprs, steps, vars, ctxt)) =>
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   301
           let val upd = Symtab.update (n, certify ctxt (Free (m, T)))
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   302
           in (typs, upd terms, exprs, steps, vars, ctxt) end))
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   303
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   304
datatype sym = Sym of string * sym list
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   305
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   306
fun mk_app _ (Sym ("true", _), _) = SOME mk_true
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   307
  | mk_app _ (Sym ("false", _), _) = SOME mk_false
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   308
  | mk_app _ (Sym ("=", _), [t, u]) = SOME (mk_eq t u)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   309
  | mk_app _ (Sym ("distinct", _), ts) = SOME (mk_distinct ts)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   310
  | mk_app _ (Sym ("ite", _), [s, t, u]) = SOME (mk_if s t u)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   311
  | mk_app _ (Sym ("and", _), ts) = SOME (mk_nary @{cterm "op &"} mk_true ts)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   312
  | mk_app _ (Sym ("or", _), ts) = SOME (mk_nary @{cterm "op |"} mk_false ts)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   313
  | mk_app _ (Sym ("iff", _), [t, u]) = SOME (mk_iff t u)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   314
  | mk_app _ (Sym ("xor", _), [t, u]) = SOME (mk_not (mk_iff t u))
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   315
  | mk_app _ (Sym ("not", _), [t]) = SOME (mk_not t)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   316
  | mk_app _ (Sym ("implies", _), [t, u]) = SOME (mk_imp t u)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   317
  | mk_app _ (Sym ("~", _), [t, u]) = SOME (mk_iff t u)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   318
  | mk_app _ (Sym ("<", _), [t, u]) = SOME (mk_lt t u)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   319
  | mk_app _ (Sym ("<=", _), [t, u]) = SOME (mk_le t u)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   320
  | mk_app _ (Sym (">", _), [t, u]) = SOME (mk_lt u t)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   321
  | mk_app _ (Sym (">=", _), [t, u]) = SOME (mk_le u t)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   322
  | mk_app _ (Sym ("+", _), [t, u]) = SOME (mk_add t u)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   323
  | mk_app _ (Sym ("-", _), [t, u]) = SOME (mk_sub t u)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   324
  | mk_app _ (Sym ("-", _), [t]) = SOME (mk_uminus t)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   325
  | mk_app _ (Sym ("*", _), [t, u]) = SOME (mk_mul t u)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   326
  | mk_app _ (Sym ("/", _), [t, u]) = SOME (mk_real_div t u)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   327
  | mk_app _ (Sym ("div", _), [t, u]) = SOME (mk_int_div t u)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   328
  | mk_app _ (Sym ("mod", _), [t, u]) = SOME (mk_mod t u)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   329
  | mk_app _ (Sym ("select", _), [m, k]) = SOME (mk_access m k)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   330
  | mk_app _ (Sym ("store", _), [m, k, v]) = SOME (mk_update m k v)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   331
  | mk_app _ (Sym ("pattern", _), _) = SOME mk_true
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   332
  | mk_app (_, terms, _, _, _, _) (Sym (n, _), ts) =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   333
      Symtab.lookup terms n |> Option.map (fn ct => mk_fun ct ts)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   334
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   335
fun add_expr k t (typs, terms, exprs, steps, vars, ctxt) =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   336
  (typs, terms, Inttab.update (k, t) exprs, steps, vars, ctxt)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   337
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   338
fun lookup_expr (_, _, exprs, _, _, _) = Inttab.lookup exprs
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   339
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   340
fun add_proof_step k ((r, prems), prop) cx =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   341
  let
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   342
    val (typs, terms, exprs, steps, vars, ctxt) = cx
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   343
    val (ct, vs) = close ctxt prop
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   344
    val step = Proof_Step {rule=r, prems=prems, prop=ct}
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   345
    val vars' = union (op =) vs vars
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   346
  in (typs, terms, exprs, Inttab.update (k, step) steps, vars', ctxt) end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   347
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   348
fun finish (_, _, _, steps, vars, ctxt) = (steps, vars, ctxt)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   349
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   350
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   351
(* core parser *)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   352
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   353
fun parse_exn line_no msg = raise SMT_Solver.SMT ("Z3 proof parser (line " ^
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   354
  string_of_int line_no ^ "): " ^ msg)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   355
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   356
fun scan_exn msg ((line_no, _), _) = parse_exn line_no msg
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   357
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   358
fun with_info f cx =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   359
  (case f ((NONE, 1), cx) of
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   360
    ((SOME root, _), cx') => (root, cx')
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   361
  | ((_, line_no), _) => parse_exn line_no "bad proof")
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   362
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   363
fun parse_line _ _ (st as ((SOME _, _), _)) = st
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   364
  | parse_line scan line ((_, line_no), cx) =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   365
      let val st = ((line_no, cx), explode line)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   366
      in
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   367
        (case Scan.catch (Scan.finite' Symbol.stopper (Scan.option scan)) st of
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   368
          (SOME r, ((_, cx'), _)) => ((r, line_no+1), cx')
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   369
        | (NONE, _) => parse_exn line_no ("bad proof line: " ^ quote line))
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   370
      end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   371
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   372
fun with_context f x ((line_no, cx), st) =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   373
  let val (y, cx') = f x cx
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   374
  in (y, ((line_no, cx'), st)) end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   375
  
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   376
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   377
fun lookup_context f x (st as ((_, cx), _)) = (f cx x, st)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   378
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   379
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   380
(* parser combinators and parsers for basic entities *)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   381
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   382
fun $$ s = Scan.lift (Scan.$$ s)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   383
fun this s = Scan.lift (Scan.this_string s)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   384
fun blank st = Scan.lift (Scan.many1 Symbol.is_ascii_blank) st
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   385
fun sep scan = blank |-- scan
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   386
fun seps scan = Scan.repeat (sep scan)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   387
fun seps1 scan = Scan.repeat1 (sep scan)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   388
fun seps_by scan_sep scan = scan ::: Scan.repeat (scan_sep |-- scan)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   389
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   390
fun par scan = $$ "(" |-- scan --| $$ ")"
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   391
fun bra scan = $$ "[" |-- scan --| $$ "]"
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   392
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   393
val digit = (fn
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   394
  "0" => SOME 0 | "1" => SOME 1 | "2" => SOME 2 | "3" => SOME 3 |
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   395
  "4" => SOME 4 | "5" => SOME 5 | "6" => SOME 6 | "7" => SOME 7 |
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   396
  "8" => SOME 8 | "9" => SOME 9 | _ => NONE)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   397
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   398
fun mk_num ds = fold (fn d => fn i => i * 10 + d) ds 0
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   399
val nat_num = Scan.lift (Scan.repeat1 (Scan.some digit)) >> mk_num
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   400
val int_num = Scan.optional ($$ "-" >> K (fn i => ~i)) I :|--
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   401
  (fn sign => nat_num >> sign)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   402
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   403
val is_char = Symbol.is_ascii_letter orf Symbol.is_ascii_digit orf
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   404
  member (op =) (explode "_+*-/%~=<>$&|?!.@^#")
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   405
val name = Scan.lift (Scan.many1 is_char) >> implode
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   406
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   407
fun sym st = (name -- Scan.optional (bra (seps_by ($$ ":") sym)) [] >> Sym) st
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   408
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   409
fun id st = ($$ "#" |-- nat_num) st
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   410
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   411
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   412
(* parsers for various parts of Z3 proofs *)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   413
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   414
fun sort st = Scan.first [
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   415
  this "bool" >> K @{typ bool},
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   416
  this "int" >> K @{typ int},
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   417
  this "real" >> K @{typ real},
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   418
  this "bv" |-- bra nat_num >> mk_wordT,
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   419
  this "array" |-- bra (sort --| $$ ":" -- sort) >> (op -->),
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   420
  par (this "->" |-- seps1 sort) >> ((op --->) o split_last),
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   421
  name :|-- with_context typ_of_sort] st
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   422
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   423
fun bound st = (par (this ":var" |-- sep nat_num -- sep sort) :|--
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   424
  lookup_context (mk_bound o theory_of)) st
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   425
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   426
fun number st = st |> (
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   427
  int_num -- Scan.option ($$ "/" |-- int_num) --| this "::" :|--
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   428
  (fn num as (n, _) =>
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   429
    this "int" >> K (mk_int_num n) ||
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   430
    this "real" >> K (mk_real_frac_num num)))
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   431
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   432
fun bv_number st = (this "bv" |-- bra (nat_num --| $$ ":" -- nat_num) :|--
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   433
  lookup_context (mk_bv_num o theory_of)) st
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   434
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   435
fun appl (app as (Sym (n, _), _)) = lookup_context mk_app app :|-- (fn 
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   436
    SOME app' => Scan.succeed app'
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   437
  | NONE => scan_exn ("unknown function: " ^ quote n))
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   438
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   439
fun constant st = ((sym >> rpair []) :|-- appl) st
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   440
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   441
fun expr_id st = (id :|-- (fn i => lookup_context lookup_expr i :|-- (fn
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   442
    SOME e => Scan.succeed e
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   443
  | NONE => scan_exn ("unknown term id: " ^ quote (string_of_int i))))) st
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   444
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   445
fun arg st = Scan.first [expr_id, number, bv_number, constant] st
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   446
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   447
fun application st = par ((sym -- Scan.repeat1 (sep arg)) :|-- appl) st
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   448
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   449
fun variables st = par (this "vars" |-- seps1 (par (name |-- sep sort))) st
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   450
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   451
fun patterns st = seps (par ((this ":pat" || this ":nopat") |-- seps1 id)) st
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   452
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   453
fun quant_kind st = st |> (
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   454
  this "forall" >> K (mk_forall o theory_of) ||
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   455
  this "exists" >> K (mk_exists o theory_of))
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   456
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   457
fun quantifier st =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   458
  (par (quant_kind -- sep variables --| patterns -- sep arg) :|--
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   459
     lookup_context (fn cx => fn ((mk_q, Ts), body) => mk_q cx Ts body)) st
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   460
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   461
fun expr k =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   462
  Scan.first [bound, quantifier, application, number, bv_number, constant] :|--
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   463
  with_context (pair NONE oo add_expr k)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   464
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   465
fun rule_name st = ((name >> `(Symtab.lookup rule_names)) :|-- (fn 
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   466
    (SOME r, _) => Scan.succeed r
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   467
  | (NONE, n) => scan_exn ("unknown proof rule: " ^ quote n))) st
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   468
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   469
fun rule f k =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   470
  bra (rule_name -- seps id) --| $$ ":" -- sep arg #->
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   471
  with_context (pair (f k) oo add_proof_step k)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   472
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   473
fun decl st = (this "decl" |-- sep name --| sep (this "::") -- sep sort :|--
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   474
  with_context (pair NONE oo add_decl)) st
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   475
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   476
fun def st = (id --| sep (this ":=")) st
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   477
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   478
fun node st = st |> (
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   479
  decl ||
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   480
  def :|-- (fn k => sep (expr k) || sep (rule (K NONE) k)) ||
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   481
  rule SOME ~1)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   482
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   483
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   484
(* overall parser *)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   485
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   486
(* Currently, terms are parsed bottom-up (i.e., along with parsing the proof
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   487
   text line by line), but proofs are reconstructed top-down (i.e. by an
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   488
   in-order top-down traversal of the proof tree/graph).  The latter approach
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   489
   was taken because some proof texts comprise irrelevant proof steps which
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   490
   will thus not be reconstructed.  This approach might also be beneficial
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   491
   for constructing terms, but it would also increase the complexity of the
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   492
   (otherwise rather modular) code. *)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   493
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   494
fun parse ctxt typs terms proof_text =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   495
  make_context ctxt typs terms
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   496
  |> with_info (fold (parse_line node) proof_text)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   497
  ||> finish
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   498
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   499
end