diff -r 883f3c4c928e -r 1a0b18176548 src/HOL/Library/Old_SMT/old_z3_proof_parser.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/Old_SMT/old_z3_proof_parser.ML	Thu Aug 28 00:40:38 2014 +0200
@@ -0,0 +1,445 @@
+(*  Title:      HOL/Library/Old_SMT/old_z3_proof_parser.ML
+    Author:     Sascha Boehme, TU Muenchen
+
+Parser for Z3 proofs.
+*)
+
+signature OLD_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 Old_Z3_Proof_Parser: OLD_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, Old_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 = Old_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
+        | _ => Old_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 (Old_SMT_Utils.instT' cv q) (Thm.lambda cv ct), vars') end
+
+  fun quant name =
+    Old_SMT_Utils.mk_const_pat @{theory} name (Old_SMT_Utils.destT1 o Old_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 = Old_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, Old_SMT_Utils.certify ctxt (Free (m, T)))
+           in (typs, upd terms, exprs, steps, vars, ctxt) end))
+
+fun mk_typ (typs, _, _, _, _, ctxt) (s as Old_Z3_Interface.Sym (n, _)) = 
+  (case Old_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 (Old_Z3_Interface.mk_builtin_num ctxt i T)) []
+
+fun mk_app (_, terms, _, _, _, ctxt) (s as Old_Z3_Interface.Sym (n, _), es) =
+  mk_fun (fn cts =>
+    (case Old_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 = Old_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 Old_SMT_Failure.SMT (Old_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)) [] >> Old_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 Old_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 (Old_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 =>
+  Old_Z3_Interface.Sym ("bv", [Old_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 (Old_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