src/HOL/Tools/SMT/z3_proof_parser.ML
author wenzelm
Thu, 02 Sep 2010 16:31:50 +0200
changeset 39046 5b38730f3e12
parent 39020 ac0f24f850c9
child 40162 7f58a9a843c2
permissions -rw-r--r--
tuned whitespace and indentation, emphasizing the logical structure of this long text;
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
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
    32
structure I = Z3_Interface
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
    33
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
    34
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
    35
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    36
(** proof rules **)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    37
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    38
datatype rule = TrueAxiom | Asserted | Goal | ModusPonens | Reflexivity |
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    39
  Symmetry | Transitivity | TransitivityStar | Monotonicity | QuantIntro |
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    40
  Distributivity | AndElim | NotOrElim | Rewrite | RewriteStar | PullQuant |
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    41
  PullQuantStar | PushQuant | ElimUnusedVars | DestEqRes | QuantInst |
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    42
  Hypothesis | Lemma | UnitResolution | IffTrue | IffFalse | Commutativity |
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    43
  DefAxiom | IntroDef | ApplyDef | IffOeq | NnfPos | NnfNeg | NnfStar |
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    44
  CnfStar | Skolemize | ModusPonensOeq | ThLemma
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    45
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    46
val rule_names = Symtab.make [
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    47
  ("true-axiom", TrueAxiom),
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    48
  ("asserted", Asserted),
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    49
  ("goal", Goal),
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    50
  ("mp", ModusPonens),
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    51
  ("refl", Reflexivity),
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    52
  ("symm", Symmetry),
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    53
  ("trans", Transitivity),
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    54
  ("trans*", TransitivityStar),
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    55
  ("monotonicity", Monotonicity),
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    56
  ("quant-intro", QuantIntro),
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    57
  ("distributivity", Distributivity),
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    58
  ("and-elim", AndElim),
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    59
  ("not-or-elim", NotOrElim),
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    60
  ("rewrite", Rewrite),
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    61
  ("rewrite*", RewriteStar),
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    62
  ("pull-quant", PullQuant),
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    63
  ("pull-quant*", PullQuantStar),
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    64
  ("push-quant", PushQuant),
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    65
  ("elim-unused", ElimUnusedVars),
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    66
  ("der", DestEqRes),
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    67
  ("quant-inst", QuantInst),
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    68
  ("hypothesis", Hypothesis),
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    69
  ("lemma", Lemma),
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    70
  ("unit-resolution", UnitResolution),
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    71
  ("iff-true", IffTrue),
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    72
  ("iff-false", IffFalse),
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    73
  ("commutativity", Commutativity),
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    74
  ("def-axiom", DefAxiom),
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    75
  ("intro-def", IntroDef),
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    76
  ("apply-def", ApplyDef),
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    77
  ("iff~", IffOeq),
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    78
  ("nnf-pos", NnfPos),
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    79
  ("nnf-neg", NnfNeg),
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    80
  ("nnf*", NnfStar),
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    81
  ("cnf*", CnfStar),
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    82
  ("sk", Skolemize),
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    83
  ("mp~", ModusPonensOeq),
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    84
  ("th-lemma", ThLemma)]
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    85
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    86
fun string_of_rule r =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    87
  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
    88
  in the (Symtab.get_first eq_rule rule_names) end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    89
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    90
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    91
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    92
(** certified terms and variables **)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    93
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
    94
val (var_prefix, decl_prefix) = ("v", "sk")
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
    95
(* "decl_prefix" is for skolem constants (represented by free variables)
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
    96
   "var_prefix" is for pseudo-schematic variables (schematic with respect
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
    97
     to the Z3 proof, but represented by free variables)
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    98
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
    99
     Both prefixes must be distinct to avoid name interferences.
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   100
   More precisely, the naming of pseudo-schematic variables must be
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   101
   context-independent modulo the current proof context to be able to
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   102
   use fast inference kernel rules during proof reconstruction. *)
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   103
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   104
fun certify ctxt = Thm.cterm_of (ProofContext.theory_of ctxt)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   105
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   106
val maxidx_of = #maxidx o Thm.rep_cterm
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   107
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   108
fun mk_inst ctxt vars =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   109
  let
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   110
    val max = fold (Integer.max o fst) vars 0
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   111
    val ns = fst (Variable.variant_fixes (replicate (max + 1) var_prefix) ctxt)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   112
    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
   113
  in map mk vars end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   114
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   115
fun close ctxt (ct, vars) =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   116
  let
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   117
    val inst = mk_inst ctxt vars
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   118
    val mk_prop = Thm.capply @{cterm Trueprop}
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   119
    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
   120
  in (mk_prop (Thm.instantiate_cterm ([], inst) ct), names) end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   121
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   122
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   123
fun mk_bound thy (i, T) =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   124
  let val ct = Thm.cterm_of thy (Var ((Name.uu, 0), T))
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   125
  in (ct, [(i, ct)]) end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   126
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   127
local
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   128
  fun mk_quant thy q T (ct, vars) =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   129
    let
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   130
      val cv =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   131
        (case AList.lookup (op =) vars 0 of
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   132
          SOME cv => cv
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   133
        | _ => Thm.cterm_of thy (Var ((Name.uu, maxidx_of ct + 1), T)))
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   134
      fun dec (i, v) = if i = 0 then NONE else SOME (i-1, v)
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   135
    in (Thm.capply (I.instT' cv q) (Thm.cabs cv ct), map_filter dec vars) end
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   136
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   137
  val forall = I.mk_inst_pair (I.destT1 o I.destT1) @{cpat All}
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   138
  val exists = I.mk_inst_pair (I.destT1 o I.destT1) @{cpat Ex}
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   139
in
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   140
fun mk_forall thy = fold_rev (mk_quant thy forall)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   141
fun mk_exists thy = fold_rev (mk_quant thy exists)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   142
end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   143
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   144
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   145
local
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   146
  fun equal_var cv (_, cu) = (cv aconvc cu)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   147
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   148
  fun prep (ct, vars) (maxidx, all_vars) =
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   149
    let
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   150
      val maxidx' = maxidx_of ct + maxidx + 1
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   151
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   152
      fun part (v as (i, cv)) =
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   153
        (case AList.lookup (op =) all_vars i of
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   154
          SOME cu => apfst (if cu aconvc cv then I else cons (cv, cu))
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   155
        | NONE =>
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   156
            if not (exists (equal_var cv) all_vars) then apsnd (cons v)
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   157
            else
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   158
              let val cv' = Thm.incr_indexes_cterm maxidx' cv
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   159
              in apfst (cons (cv, cv')) #> apsnd (cons (i, cv')) end)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   160
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   161
      val (inst, vars') =
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   162
        if null vars then ([], vars)
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   163
        else fold part vars ([], [])
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   164
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   165
    in (Thm.instantiate_cterm ([], inst) ct, (maxidx', vars' @ all_vars)) end
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   166
in
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   167
fun mk_fun f ts =
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   168
  let val (cts, (_, vars)) = fold_map prep ts (~1, [])
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   169
  in f cts |> Option.map (rpair vars) end
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   170
end
36898
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
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   174
(** proof parser **)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   175
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   176
datatype proof_step = Proof_Step of {
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   177
  rule: rule,
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   178
  prems: int list,
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   179
  prop: cterm }
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   180
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   181
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   182
(* parser context *)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   183
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   184
fun make_context ctxt typs terms =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   185
  let
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   186
    val ctxt' = 
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   187
      ctxt
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   188
      |> Symtab.fold (Variable.declare_typ o snd) typs
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   189
      |> Symtab.fold (Variable.declare_term o snd) terms
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   190
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   191
    fun cert @{term True} = @{cterm "~False"}
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   192
      | cert t = certify ctxt' t
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   193
39020
ac0f24f850c9 replaced Table.map' by Table.map
haftmann
parents: 36940
diff changeset
   194
  in (typs, Symtab.map (K cert) terms, Inttab.empty, Inttab.empty, [], ctxt') end
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   195
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   196
fun fresh_name n (typs, terms, exprs, steps, vars, ctxt) =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   197
  let val (n', ctxt') = yield_singleton Variable.variant_fixes n ctxt
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   198
  in (n', (typs, terms, exprs, steps, vars, ctxt')) end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   199
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   200
fun theory_of (_, _, _, _, _, ctxt) = ProofContext.theory_of ctxt
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   201
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   202
fun add_decl (n, T) (cx as (_, terms, _, _, _, _)) =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   203
  (case Symtab.lookup terms n of
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   204
    SOME _ => cx
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   205
  | NONE => cx |> fresh_name (decl_prefix ^ n)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   206
      |> (fn (m, (typs, terms, exprs, steps, vars, ctxt)) =>
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   207
           let val upd = Symtab.update (n, certify ctxt (Free (m, T)))
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   208
           in (typs, upd terms, exprs, steps, vars, ctxt) end))
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   209
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   210
fun mk_typ (typs, _, _, _, _, ctxt) (s as I.Sym (n, _)) = 
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   211
  (case I.mk_builtin_typ ctxt s of
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   212
    SOME T => SOME T
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   213
  | NONE => Symtab.lookup typs n)
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   214
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   215
fun mk_num (_, _, _, _, _, ctxt) (i, T) =
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   216
  mk_fun (K (I.mk_builtin_num ctxt i T)) []
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   217
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   218
fun mk_app (_, terms, _, _, _, ctxt) (s as I.Sym (n, _), es) =
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   219
  mk_fun (fn cts =>
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   220
    (case I.mk_builtin_fun ctxt s cts of
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   221
      SOME ct => SOME ct
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   222
    | NONE =>
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   223
        Symtab.lookup terms n |> Option.map (Drule.list_comb o rpair cts))) es
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   224
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   225
fun add_expr k t (typs, terms, exprs, steps, vars, ctxt) =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   226
  (typs, terms, Inttab.update (k, t) exprs, steps, vars, ctxt)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   227
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   228
fun lookup_expr (_, _, exprs, _, _, _) = Inttab.lookup exprs
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   229
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   230
fun add_proof_step k ((r, prems), prop) cx =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   231
  let
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   232
    val (typs, terms, exprs, steps, vars, ctxt) = cx
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   233
    val (ct, vs) = close ctxt prop
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   234
    val step = Proof_Step {rule=r, prems=prems, prop=ct}
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   235
    val vars' = union (op =) vs vars
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   236
  in (typs, terms, exprs, Inttab.update (k, step) steps, vars', ctxt) end
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 finish (_, _, _, steps, vars, ctxt) = (steps, vars, ctxt)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   239
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   240
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   241
(* core parser *)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   242
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   243
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
   244
  string_of_int line_no ^ "): " ^ msg)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   245
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   246
fun scan_exn msg ((line_no, _), _) = parse_exn line_no msg
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   247
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   248
fun with_info f cx =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   249
  (case f ((NONE, 1), cx) of
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   250
    ((SOME root, _), cx') => (root, cx')
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   251
  | ((_, line_no), _) => parse_exn line_no "bad proof")
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   252
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   253
fun parse_line _ _ (st as ((SOME _, _), _)) = st
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   254
  | parse_line scan line ((_, line_no), cx) =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   255
      let val st = ((line_no, cx), explode line)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   256
      in
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   257
        (case Scan.catch (Scan.finite' Symbol.stopper (Scan.option scan)) st of
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   258
          (SOME r, ((_, cx'), _)) => ((r, line_no+1), cx')
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   259
        | (NONE, _) => parse_exn line_no ("bad proof line: " ^ quote line))
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   260
      end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   261
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   262
fun with_context f x ((line_no, cx), st) =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   263
  let val (y, cx') = f x cx
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   264
  in (y, ((line_no, cx'), st)) end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   265
  
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   266
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   267
fun lookup_context f x (st as ((_, cx), _)) = (f cx x, st)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   268
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   269
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   270
(* parser combinators and parsers for basic entities *)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   271
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   272
fun $$ s = Scan.lift (Scan.$$ s)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   273
fun this s = Scan.lift (Scan.this_string s)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   274
fun blank st = Scan.lift (Scan.many1 Symbol.is_ascii_blank) st
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   275
fun sep scan = blank |-- scan
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   276
fun seps scan = Scan.repeat (sep scan)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   277
fun seps1 scan = Scan.repeat1 (sep scan)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   278
fun seps_by scan_sep scan = scan ::: Scan.repeat (scan_sep |-- scan)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   279
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   280
fun par scan = $$ "(" |-- scan --| $$ ")"
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   281
fun bra scan = $$ "[" |-- scan --| $$ "]"
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   282
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   283
val digit = (fn
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   284
  "0" => SOME 0 | "1" => SOME 1 | "2" => SOME 2 | "3" => SOME 3 |
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   285
  "4" => SOME 4 | "5" => SOME 5 | "6" => SOME 6 | "7" => SOME 7 |
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   286
  "8" => SOME 8 | "9" => SOME 9 | _ => NONE)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   287
36940
b4417ddad979 make SML/NJ happy
blanchet
parents: 36899
diff changeset
   288
fun digits st = (Scan.lift (Scan.many1 Symbol.is_ascii_digit) >> implode) st
b4417ddad979 make SML/NJ happy
blanchet
parents: 36899
diff changeset
   289
fun nat_num st = (Scan.lift (Scan.repeat1 (Scan.some digit)) >> (fn ds =>
b4417ddad979 make SML/NJ happy
blanchet
parents: 36899
diff changeset
   290
  fold (fn d => fn i => i * 10 + d) ds 0)) st
b4417ddad979 make SML/NJ happy
blanchet
parents: 36899
diff changeset
   291
fun int_num st = (Scan.optional ($$ "-" >> K (fn i => ~i)) I :|--
b4417ddad979 make SML/NJ happy
blanchet
parents: 36899
diff changeset
   292
  (fn sign => nat_num >> sign)) st
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   293
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   294
val is_char = Symbol.is_ascii_letter orf Symbol.is_ascii_digit orf
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   295
  member (op =) (explode "_+*-/%~=<>$&|?!.@^#")
36940
b4417ddad979 make SML/NJ happy
blanchet
parents: 36899
diff changeset
   296
fun name st = (Scan.lift (Scan.many1 is_char) >> implode) st
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   297
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   298
fun sym st =
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   299
  (name -- Scan.optional (bra (seps_by ($$ ":") sym)) [] >> I.Sym) st
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   300
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   301
fun id st = ($$ "#" |-- nat_num) st
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   302
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   303
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   304
(* parsers for various parts of Z3 proofs *)
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 sort st = Scan.first [
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   307
  this "array" |-- bra (sort --| $$ ":" -- sort) >> (op -->),
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   308
  par (this "->" |-- seps1 sort) >> ((op --->) o split_last),
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   309
  sym :|-- (fn s as I.Sym (n, _) => lookup_context mk_typ s :|-- (fn
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   310
    SOME T => Scan.succeed T
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   311
  | NONE => scan_exn ("unknown sort: " ^ quote n)))] st
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   312
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   313
fun bound st = (par (this ":var" |-- sep nat_num -- sep sort) :|--
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   314
  lookup_context (mk_bound o theory_of)) st
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   315
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   316
fun numb (n as (i, _)) = lookup_context mk_num n :|-- (fn
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   317
    SOME n' => Scan.succeed n'
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   318
  | NONE => scan_exn ("unknown number: " ^ quote (string_of_int i)))
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   319
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   320
fun appl (app as (I.Sym (n, _), _)) = lookup_context mk_app app :|-- (fn 
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   321
    SOME app' => Scan.succeed app'
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   322
  | NONE => scan_exn ("unknown function symbol: " ^ quote n))
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   323
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   324
fun bv_size st = (digits >> (fn sz => I.Sym ("bv", [I.Sym (sz, [])]))) st
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   325
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   326
fun bv_number_sort st = (bv_size :|-- lookup_context mk_typ :|-- (fn
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   327
    SOME cT => Scan.succeed cT
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   328
  | NONE => scan_exn ("unknown sort: " ^ quote "bv"))) st
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   329
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   330
fun bv_number st =
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   331
  (this "bv" |-- bra (nat_num --| $$ ":" -- bv_number_sort) :|-- numb) st
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   332
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   333
fun frac_number st = (
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   334
  int_num --| $$ "/" -- int_num --| this "::" -- sort :|-- (fn ((i, j), T) =>
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   335
    numb (i, T) -- numb (j, T) :|-- (fn (n, m) =>
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   336
      appl (I.Sym ("/", []), [n, m])))) st
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   337
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   338
fun plain_number st = (int_num --| this "::" -- sort :|-- numb) st
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   339
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   340
fun number st = Scan.first [bv_number, frac_number, plain_number] st
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   341
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   342
fun constant st = ((sym >> rpair []) :|-- appl) st
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   343
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   344
fun expr_id st = (id :|-- (fn i => lookup_context lookup_expr i :|-- (fn
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   345
    SOME e => Scan.succeed e
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   346
  | NONE => scan_exn ("unknown term id: " ^ quote (string_of_int i))))) st
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   347
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   348
fun arg st = Scan.first [expr_id, number, constant] st
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   349
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   350
fun application st = par ((sym -- Scan.repeat1 (sep arg)) :|-- appl) st
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   351
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   352
fun variables st = par (this "vars" |-- seps1 (par (name |-- sep sort))) st
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   353
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   354
fun pats st = seps (par ((this ":pat" || this ":nopat") |-- seps1 id)) st
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   355
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   356
fun pattern st = par (this "pattern" |-- Scan.repeat1 (sep arg) >>
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   357
  (the o mk_fun (K (SOME @{cterm True})))) st
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   358
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   359
fun quant_kind st = st |> (
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   360
  this "forall" >> K (mk_forall o theory_of) ||
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   361
  this "exists" >> K (mk_exists o theory_of))
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 quantifier st =
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   364
  (par (quant_kind -- sep variables --| pats -- sep arg) :|--
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   365
     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
   366
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   367
fun expr k =
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   368
  Scan.first [bound, quantifier, pattern, application, number, constant] :|--
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   369
  with_context (pair NONE oo add_expr k)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   370
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   371
fun rule_name st = ((name >> `(Symtab.lookup rule_names)) :|-- (fn 
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   372
    (SOME r, _) => Scan.succeed r
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   373
  | (NONE, n) => scan_exn ("unknown proof rule: " ^ quote n))) st
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   374
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   375
fun rule f k =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   376
  bra (rule_name -- seps id) --| $$ ":" -- sep arg #->
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   377
  with_context (pair (f k) oo add_proof_step k)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   378
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   379
fun decl st = (this "decl" |-- sep name --| sep (this "::") -- sep sort :|--
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   380
  with_context (pair NONE oo add_decl)) st
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 def st = (id --| sep (this ":=")) st
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   383
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   384
fun node st = st |> (
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   385
  decl ||
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   386
  def :|-- (fn k => sep (expr k) || sep (rule (K NONE) k)) ||
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   387
  rule SOME ~1)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   388
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   389
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   390
(* overall parser *)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   391
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   392
(* Currently, terms are parsed bottom-up (i.e., along with parsing the proof
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   393
   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
   394
   in-order top-down traversal of the proof tree/graph).  The latter approach
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   395
   was taken because some proof texts comprise irrelevant proof steps which
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   396
   will thus not be reconstructed.  This approach might also be beneficial
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   397
   for constructing terms, but it would also increase the complexity of the
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   398
   (otherwise rather modular) code. *)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   399
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   400
fun parse ctxt typs terms proof_text =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   401
  make_context ctxt typs terms
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   402
  |> with_info (fold (parse_line node) proof_text)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   403
  ||> finish
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   404
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   405
end