--- a/src/HOL/Library/SMT/z3_proof_parser.ML Thu Aug 28 00:40:37 2014 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,445 +0,0 @@
-(* Title: HOL/Library/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.apply (SMT_Utils.instT' cv q) (Thm.lambda 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