(* Title: HOL/Tools/SMT/z3_proof_parser.ML
Author: Sascha Boehme, TU Muenchen
Parser for Z3 proofs.
*)
signature Z3_PROOF_PARSER =
sig
(*proof rules*)
datatype rule = True_Axiom | Asserted | Goal | Modus_Ponens | Reflexivity |
Symmetry | Transitivity | Transitivity_Star | Monotonicity | Quant_Intro |
Distributivity | And_Elim | Not_Or_Elim | Rewrite | Rewrite_Star |
Pull_Quant | Pull_Quant_Star | Push_Quant | Elim_Unused_Vars |
Dest_Eq_Res | Quant_Inst | Hypothesis | Lemma | Unit_Resolution |
Iff_True | Iff_False | Commutativity | Def_Axiom | Intro_Def | Apply_Def |
Iff_Oeq | Nnf_Pos | Nnf_Neg | Nnf_Star | Cnf_Star | Skolemize |
Modus_Ponens_Oeq | Th_Lemma of string list
val string_of_rule: rule -> string
(*proof parser*)
datatype proof_step = Proof_Step of {
rule: rule,
args: cterm list,
prems: int list,
prop: cterm }
val parse: Proof.context -> typ Symtab.table -> term Symtab.table ->
string list ->
(int * cterm) list * (int * proof_step) list * string list * Proof.context
end
structure Z3_Proof_Parser: Z3_PROOF_PARSER =
struct
(* proof rules *)
datatype rule = True_Axiom | Asserted | Goal | Modus_Ponens | Reflexivity |
Symmetry | Transitivity | Transitivity_Star | Monotonicity | Quant_Intro |
Distributivity | And_Elim | Not_Or_Elim | Rewrite | Rewrite_Star |
Pull_Quant | Pull_Quant_Star | Push_Quant | Elim_Unused_Vars | Dest_Eq_Res |
Quant_Inst | Hypothesis | Lemma | Unit_Resolution | Iff_True | Iff_False |
Commutativity | Def_Axiom | Intro_Def | Apply_Def | Iff_Oeq | Nnf_Pos |
Nnf_Neg | Nnf_Star | Cnf_Star | Skolemize | Modus_Ponens_Oeq |
Th_Lemma of string list
val rule_names = Symtab.make [
("true-axiom", True_Axiom),
("asserted", Asserted),
("goal", Goal),
("mp", Modus_Ponens),
("refl", Reflexivity),
("symm", Symmetry),
("trans", Transitivity),
("trans*", Transitivity_Star),
("monotonicity", Monotonicity),
("quant-intro", Quant_Intro),
("distributivity", Distributivity),
("and-elim", And_Elim),
("not-or-elim", Not_Or_Elim),
("rewrite", Rewrite),
("rewrite*", Rewrite_Star),
("pull-quant", Pull_Quant),
("pull-quant*", Pull_Quant_Star),
("push-quant", Push_Quant),
("elim-unused", Elim_Unused_Vars),
("der", Dest_Eq_Res),
("quant-inst", Quant_Inst),
("hypothesis", Hypothesis),
("lemma", Lemma),
("unit-resolution", Unit_Resolution),
("iff-true", Iff_True),
("iff-false", Iff_False),
("commutativity", Commutativity),
("def-axiom", Def_Axiom),
("intro-def", Intro_Def),
("apply-def", Apply_Def),
("iff~", Iff_Oeq),
("nnf-pos", Nnf_Pos),
("nnf-neg", Nnf_Neg),
("nnf*", Nnf_Star),
("cnf*", Cnf_Star),
("sk", Skolemize),
("mp~", Modus_Ponens_Oeq),
("th-lemma", Th_Lemma [])]
fun string_of_rule (Th_Lemma args) = space_implode " " ("th-lemma" :: args)
| string_of_rule r =
let fun eq_rule (s, r') = if r = r' then SOME s else NONE
in the (Symtab.get_first eq_rule rule_names) end
(* certified terms and variables *)
val (var_prefix, decl_prefix) = ("v", "sk")
(*
"decl_prefix" is for skolem constants (represented by free variables),
"var_prefix" is for pseudo-schematic variables (schematic with respect
to the Z3 proof, but represented by free variables).
Both prefixes must be distinct to avoid name interferences.
More precisely, the naming of pseudo-schematic variables must be
context-independent modulo the current proof context to be able to
use fast inference kernel rules during proof reconstruction.
*)
val maxidx_of = #maxidx o Thm.rep_cterm
fun mk_inst ctxt vars =
let
val max = fold (Integer.max o fst) vars 0
val ns = fst (Variable.variant_fixes (replicate (max + 1) var_prefix) ctxt)
fun mk (i, v) =
(v, SMT_Utils.certify ctxt (Free (nth ns i, #T (Thm.rep_cterm v))))
in map mk vars end
fun close ctxt (ct, vars) =
let
val inst = mk_inst ctxt vars
val names = fold (Term.add_free_names o Thm.term_of o snd) inst []
in (Thm.instantiate_cterm ([], inst) ct, names) end
fun mk_bound ctxt (i, T) =
let val ct = SMT_Utils.certify ctxt (Var ((Name.uu, 0), T))
in (ct, [(i, ct)]) end
local
fun mk_quant1 ctxt q T (ct, vars) =
let
val cv =
(case AList.lookup (op =) vars 0 of
SOME cv => cv
| _ => SMT_Utils.certify ctxt (Var ((Name.uu, maxidx_of ct + 1), T)))
fun dec (i, v) = if i = 0 then NONE else SOME (i-1, v)
val vars' = map_filter dec vars
in (Thm.capply (SMT_Utils.instT' cv q) (Thm.cabs cv ct), vars') end
fun quant name =
SMT_Utils.mk_const_pat @{theory} name (SMT_Utils.destT1 o SMT_Utils.destT1)
val forall = quant @{const_name All}
val exists = quant @{const_name Ex}
in
fun mk_quant is_forall ctxt =
fold_rev (mk_quant1 ctxt (if is_forall then forall else exists))
end
local
fun prep (ct, vars) (maxidx, all_vars) =
let
val maxidx' = maxidx + maxidx_of ct + 1
fun part (i, cv) =
(case AList.lookup (op =) all_vars i of
SOME cu => apfst (if cu aconvc cv then I else cons (cv, cu))
| NONE =>
let val cv' = Thm.incr_indexes_cterm maxidx cv
in apfst (cons (cv, cv')) #> apsnd (cons (i, cv')) end)
val (inst, vars') =
if null vars then ([], vars)
else fold part vars ([], [])
in (Thm.instantiate_cterm ([], inst) ct, (maxidx', vars' @ all_vars)) end
in
fun mk_fun f ts =
let val (cts, (_, vars)) = fold_map prep ts (0, [])
in f cts |> Option.map (rpair vars) end
end
(* proof parser *)
datatype proof_step = Proof_Step of {
rule: rule,
args: cterm list,
prems: int list,
prop: cterm }
(** parser context **)
val not_false = Thm.cterm_of @{theory} (@{const Not} $ @{const False})
fun make_context ctxt typs terms =
let
val ctxt' =
ctxt
|> Symtab.fold (Variable.declare_typ o snd) typs
|> Symtab.fold (Variable.declare_term o snd) terms
fun cert @{const True} = not_false
| cert t = SMT_Utils.certify ctxt' t
in (typs, Symtab.map (K cert) terms, Inttab.empty, [], [], ctxt') end
fun fresh_name n (typs, terms, exprs, steps, vars, ctxt) =
let val (n', ctxt') = yield_singleton Variable.variant_fixes n ctxt
in (n', (typs, terms, exprs, steps, vars, ctxt')) end
fun context_of (_, _, _, _, _, ctxt) = ctxt
fun add_decl (n, T) (cx as (_, terms, _, _, _, _)) =
(case Symtab.lookup terms n of
SOME _ => cx
| NONE => cx |> fresh_name (decl_prefix ^ n)
|> (fn (m, (typs, terms, exprs, steps, vars, ctxt)) =>
let
val upd = Symtab.update (n, SMT_Utils.certify ctxt (Free (m, T)))
in (typs, upd terms, exprs, steps, vars, ctxt) end))
fun mk_typ (typs, _, _, _, _, ctxt) (s as Z3_Interface.Sym (n, _)) =
(case Z3_Interface.mk_builtin_typ ctxt s of
SOME T => SOME T
| NONE => Symtab.lookup typs n)
fun mk_num (_, _, _, _, _, ctxt) (i, T) =
mk_fun (K (Z3_Interface.mk_builtin_num ctxt i T)) []
fun mk_app (_, terms, _, _, _, ctxt) (s as Z3_Interface.Sym (n, _), es) =
mk_fun (fn cts =>
(case Z3_Interface.mk_builtin_fun ctxt s cts of
SOME ct => SOME ct
| NONE =>
Symtab.lookup terms n |> Option.map (Drule.list_comb o rpair cts))) es
fun add_expr k t (typs, terms, exprs, steps, vars, ctxt) =
(typs, terms, Inttab.update (k, t) exprs, steps, vars, ctxt)
fun lookup_expr (_, _, exprs, _, _, _) = Inttab.lookup exprs
fun add_proof_step k ((r, args), prop) cx =
let
val (typs, terms, exprs, steps, vars, ctxt) = cx
val (ct, vs) = close ctxt prop
fun part (SOME e, _) (cts, ps) = (close ctxt e :: cts, ps)
| part (NONE, i) (cts, ps) = (cts, i :: ps)
val (args', prems) = fold (part o `(lookup_expr cx)) args ([], [])
val (cts, vss) = split_list args'
val step = Proof_Step {rule=r, args=rev cts, prems=rev prems,
prop = SMT_Utils.mk_cprop ct}
val vars' = fold (union (op =)) (vs :: vss) vars
in (typs, terms, exprs, (k, step) :: steps, vars', ctxt) end
fun finish (_, _, _, steps, vars, ctxt) =
let
fun coll (p as (k, Proof_Step {prems, rule, prop, ...})) (ars, ps, ids) =
(case rule of
Asserted => ((k, prop) :: ars, ps, ids)
| Goal => ((k, prop) :: ars, ps, ids)
| _ =>
if Inttab.defined ids k then
(ars, p :: ps, fold (Inttab.update o rpair ()) prems ids)
else (ars, ps, ids))
val (ars, steps', _) = fold coll steps ([], [], Inttab.make [(~1, ())])
in (ars, steps', vars, ctxt) end
(** core parser **)
fun parse_exn line_no msg = raise SMT_Failure.SMT (SMT_Failure.Other_Failure
("Z3 proof parser (line " ^ string_of_int line_no ^ "): " ^ msg))
fun scan_exn msg ((line_no, _), _) = parse_exn line_no msg
fun with_info f cx =
(case f ((NONE, 1), cx) of
((SOME _, _), cx') => cx'
| ((_, line_no), _) => parse_exn line_no "bad proof")
fun parse_line _ _ (st as ((SOME _, _), _)) = st
| parse_line scan line ((_, line_no), cx) =
let val st = ((line_no, cx), raw_explode line)
in
(case Scan.catch (Scan.finite' Symbol.stopper (Scan.option scan)) st of
(SOME r, ((_, cx'), _)) => ((r, line_no+1), cx')
| (NONE, _) => parse_exn line_no ("bad proof line: " ^ quote line))
end
fun with_context f x ((line_no, cx), st) =
let val (y, cx') = f x cx
in (y, ((line_no, cx'), st)) end
fun lookup_context f x (st as ((_, cx), _)) = (f cx x, st)
(** parser combinators and parsers for basic entities **)
fun $$ s = Scan.lift (Scan.$$ s)
fun this s = Scan.lift (Scan.this_string s)
val is_blank = Symbol.is_ascii_blank
fun blank st = Scan.lift (Scan.many1 is_blank) st
fun sep scan = blank |-- scan
fun seps scan = Scan.repeat (sep scan)
fun seps1 scan = Scan.repeat1 (sep scan)
fun seps_by scan_sep scan = scan ::: Scan.repeat (scan_sep |-- scan)
val lpar = "(" and rpar = ")"
val lbra = "[" and rbra = "]"
fun par scan = $$ lpar |-- scan --| $$ rpar
fun bra scan = $$ lbra |-- scan --| $$ rbra
val digit = (fn
"0" => SOME 0 | "1" => SOME 1 | "2" => SOME 2 | "3" => SOME 3 |
"4" => SOME 4 | "5" => SOME 5 | "6" => SOME 6 | "7" => SOME 7 |
"8" => SOME 8 | "9" => SOME 9 | _ => NONE)
fun digits st = (Scan.lift (Scan.many1 Symbol.is_ascii_digit) >> implode) st
fun nat_num st = (Scan.lift (Scan.repeat1 (Scan.some digit)) >> (fn ds =>
fold (fn d => fn i => i * 10 + d) ds 0)) st
fun int_num st = (Scan.optional ($$ "-" >> K (fn i => ~i)) I :|--
(fn sign => nat_num >> sign)) st
val is_char = Symbol.is_ascii_letter orf Symbol.is_ascii_digit orf
member (op =) (raw_explode "_+*-/%~=<>$&|?!.@^#")
fun name st = (Scan.lift (Scan.many1 is_char) >> implode) st
fun sym st = (name --
Scan.optional (bra (seps_by ($$ ":") sym)) [] >> Z3_Interface.Sym) st
fun id st = ($$ "#" |-- nat_num) st
(** parsers for various parts of Z3 proofs **)
fun sort st = Scan.first [
this "array" |-- bra (sort --| $$ ":" -- sort) >> (op -->),
par (this "->" |-- seps1 sort) >> ((op --->) o split_last),
sym :|-- (fn s as Z3_Interface.Sym (n, _) => lookup_context mk_typ s :|-- (fn
SOME T => Scan.succeed T
| NONE => scan_exn ("unknown sort: " ^ quote n)))] st
fun bound st = (par (this ":var" |-- sep nat_num -- sep sort) :|--
lookup_context (mk_bound o context_of)) st
fun numb (n as (i, _)) = lookup_context mk_num n :|-- (fn
SOME n' => Scan.succeed n'
| NONE => scan_exn ("unknown number: " ^ quote (string_of_int i)))
fun appl (app as (Z3_Interface.Sym (n, _), _)) =
lookup_context mk_app app :|-- (fn
SOME app' => Scan.succeed app'
| NONE => scan_exn ("unknown function symbol: " ^ quote n))
fun bv_size st = (digits >> (fn sz =>
Z3_Interface.Sym ("bv", [Z3_Interface.Sym (sz, [])]))) st
fun bv_number_sort st = (bv_size :|-- lookup_context mk_typ :|-- (fn
SOME cT => Scan.succeed cT
| NONE => scan_exn ("unknown sort: " ^ quote "bv"))) st
fun bv_number st =
(this "bv" |-- bra (nat_num --| $$ ":" -- bv_number_sort) :|-- numb) st
fun frac_number st = (
int_num --| $$ "/" -- int_num --| this "::" -- sort :|-- (fn ((i, j), T) =>
numb (i, T) -- numb (j, T) :|-- (fn (n, m) =>
appl (Z3_Interface.Sym ("/", []), [n, m])))) st
fun plain_number st = (int_num --| this "::" -- sort :|-- numb) st
fun number st = Scan.first [bv_number, frac_number, plain_number] st
fun constant st = ((sym >> rpair []) :|-- appl) st
fun expr_id st = (id :|-- (fn i => lookup_context lookup_expr i :|-- (fn
SOME e => Scan.succeed e
| NONE => scan_exn ("unknown term id: " ^ quote (string_of_int i))))) st
fun arg st = Scan.first [expr_id, number, constant] st
fun application st = par ((sym -- Scan.repeat1 (sep arg)) :|-- appl) st
fun variables st = par (this "vars" |-- seps1 (par (name |-- sep sort))) st
fun pats st = seps (par ((this ":pat" || this ":nopat") |-- seps1 id)) st
val ctrue = Thm.cterm_of @{theory} @{const True}
fun pattern st = par (this "pattern" |-- Scan.repeat1 (sep arg) >>
(the o mk_fun (K (SOME ctrue)))) st
fun quant_kind st = st |> (
this "forall" >> K (mk_quant true o context_of) ||
this "exists" >> K (mk_quant false o context_of))
fun quantifier st =
(par (quant_kind -- sep variables --| pats -- sep arg) :|--
lookup_context (fn cx => fn ((mk_q, Ts), body) => mk_q cx Ts body)) st
fun expr k =
Scan.first [bound, quantifier, pattern, application, number, constant] :|--
with_context (pair NONE oo add_expr k)
val rule_arg = id
(* if this is modified, then 'th_lemma_arg' needs reviewing *)
fun th_lemma_arg st = Scan.unless (sep rule_arg >> K "" || $$ rbra) (sep name) st
fun rule_name st = ((name >> `(Symtab.lookup rule_names)) :|-- (fn
(SOME (Th_Lemma _), _) => Scan.repeat th_lemma_arg >> Th_Lemma
| (SOME r, _) => Scan.succeed r
| (NONE, n) => scan_exn ("unknown proof rule: " ^ quote n))) st
fun rule f k =
bra (rule_name -- seps id) --| $$ ":" -- sep arg #->
with_context (pair (f k) oo add_proof_step k)
fun decl st = (this "decl" |-- sep name --| sep (this "::") -- sep sort :|--
with_context (pair NONE oo add_decl)) st
fun def st = (id --| sep (this ":=")) st
fun node st = st |> (
decl ||
def :|-- (fn k => sep (expr k) || sep (rule (K NONE) k)) ||
rule SOME ~1)
(** overall parser **)
(*
Currently, terms are parsed bottom-up (i.e., along with parsing the proof
text line by line), but proofs are reconstructed top-down (i.e. by an
in-order top-down traversal of the proof tree/graph). The latter approach
was taken because some proof texts comprise irrelevant proof steps which
will thus not be reconstructed. This approach might also be beneficial
for constructing terms, but it would also increase the complexity of the
(otherwise rather modular) code.
*)
fun parse ctxt typs terms proof_text =
make_context ctxt typs terms
|> with_info (fold (parse_line node) proof_text)
|> finish
end