src/HOL/Library/Old_SMT/old_z3_proof_parser.ML
author wenzelm
Wed Jun 17 11:03:05 2015 +0200 (2015-06-17)
changeset 60500 903bb1495239
parent 59634 4b94cc030ba0
child 60642 48dd1cefb4ae
permissions -rw-r--r--
isabelle update_cartouches;
     1 (*  Title:      HOL/Library/Old_SMT/old_z3_proof_parser.ML
     2     Author:     Sascha Boehme, TU Muenchen
     3 
     4 Parser for Z3 proofs.
     5 *)
     6 
     7 signature OLD_Z3_PROOF_PARSER =
     8 sig
     9   (*proof rules*)
    10   datatype rule = True_Axiom | Asserted | Goal | Modus_Ponens | Reflexivity |
    11     Symmetry | Transitivity | Transitivity_Star | Monotonicity | Quant_Intro |
    12     Distributivity | And_Elim | Not_Or_Elim | Rewrite | Rewrite_Star |
    13     Pull_Quant | Pull_Quant_Star | Push_Quant | Elim_Unused_Vars |
    14     Dest_Eq_Res | Quant_Inst | Hypothesis | Lemma | Unit_Resolution |
    15     Iff_True | Iff_False | Commutativity | Def_Axiom | Intro_Def | Apply_Def |
    16     Iff_Oeq | Nnf_Pos | Nnf_Neg | Nnf_Star | Cnf_Star | Skolemize |
    17     Modus_Ponens_Oeq | Th_Lemma of string list
    18   val string_of_rule: rule -> string
    19 
    20   (*proof parser*)
    21   datatype proof_step = Proof_Step of {
    22     rule: rule,
    23     args: cterm list,
    24     prems: int list,
    25     prop: cterm }
    26   val parse: Proof.context -> typ Symtab.table -> term Symtab.table ->
    27     string list ->
    28     (int * cterm) list * (int * proof_step) list * string list * Proof.context
    29 end
    30 
    31 structure Old_Z3_Proof_Parser: OLD_Z3_PROOF_PARSER =
    32 struct
    33 
    34 
    35 (* proof rules *)
    36 
    37 datatype rule = True_Axiom | Asserted | Goal | Modus_Ponens | Reflexivity |
    38   Symmetry | Transitivity | Transitivity_Star | Monotonicity | Quant_Intro |
    39   Distributivity | And_Elim | Not_Or_Elim | Rewrite | Rewrite_Star |
    40   Pull_Quant | Pull_Quant_Star | Push_Quant | Elim_Unused_Vars | Dest_Eq_Res |
    41   Quant_Inst | Hypothesis | Lemma | Unit_Resolution | Iff_True | Iff_False |
    42   Commutativity | Def_Axiom | Intro_Def | Apply_Def | Iff_Oeq | Nnf_Pos |
    43   Nnf_Neg | Nnf_Star | Cnf_Star | Skolemize | Modus_Ponens_Oeq |
    44   Th_Lemma of string list
    45 
    46 val rule_names = Symtab.make [
    47   ("true-axiom", True_Axiom),
    48   ("asserted", Asserted),
    49   ("goal", Goal),
    50   ("mp", Modus_Ponens),
    51   ("refl", Reflexivity),
    52   ("symm", Symmetry),
    53   ("trans", Transitivity),
    54   ("trans*", Transitivity_Star),
    55   ("monotonicity", Monotonicity),
    56   ("quant-intro", Quant_Intro),
    57   ("distributivity", Distributivity),
    58   ("and-elim", And_Elim),
    59   ("not-or-elim", Not_Or_Elim),
    60   ("rewrite", Rewrite),
    61   ("rewrite*", Rewrite_Star),
    62   ("pull-quant", Pull_Quant),
    63   ("pull-quant*", Pull_Quant_Star),
    64   ("push-quant", Push_Quant),
    65   ("elim-unused", Elim_Unused_Vars),
    66   ("der", Dest_Eq_Res),
    67   ("quant-inst", Quant_Inst),
    68   ("hypothesis", Hypothesis),
    69   ("lemma", Lemma),
    70   ("unit-resolution", Unit_Resolution),
    71   ("iff-true", Iff_True),
    72   ("iff-false", Iff_False),
    73   ("commutativity", Commutativity),
    74   ("def-axiom", Def_Axiom),
    75   ("intro-def", Intro_Def),
    76   ("apply-def", Apply_Def),
    77   ("iff~", Iff_Oeq),
    78   ("nnf-pos", Nnf_Pos),
    79   ("nnf-neg", Nnf_Neg),
    80   ("nnf*", Nnf_Star),
    81   ("cnf*", Cnf_Star),
    82   ("sk", Skolemize),
    83   ("mp~", Modus_Ponens_Oeq),
    84   ("th-lemma", Th_Lemma [])]
    85 
    86 fun string_of_rule (Th_Lemma args) = space_implode " " ("th-lemma" :: args)
    87   | string_of_rule r =
    88       let fun eq_rule (s, r') = if r = r' then SOME s else NONE 
    89       in the (Symtab.get_first eq_rule rule_names) end
    90 
    91 
    92 
    93 (* certified terms and variables *)
    94 
    95 val (var_prefix, decl_prefix) = ("v", "sk")
    96 (*
    97   "decl_prefix" is for skolem constants (represented by free variables),
    98   "var_prefix" is for pseudo-schematic variables (schematic with respect
    99   to the Z3 proof, but represented by free variables).
   100 
   101   Both prefixes must be distinct to avoid name interferences.
   102   More precisely, the naming of pseudo-schematic variables must be
   103   context-independent modulo the current proof context to be able to
   104   use fast inference kernel rules during proof reconstruction.
   105 *)
   106 
   107 fun mk_inst ctxt vars =
   108   let
   109     val max = fold (Integer.max o fst) vars 0
   110     val ns = fst (Variable.variant_fixes (replicate (max + 1) var_prefix) ctxt)
   111     fun mk (i, v) =
   112       (v, Thm.cterm_of ctxt (Free (nth ns i, Thm.typ_of_cterm v)))
   113   in map mk vars end
   114 
   115 fun close ctxt (ct, vars) =
   116   let
   117     val inst = mk_inst ctxt vars
   118     val names = fold (Term.add_free_names o Thm.term_of o snd) inst []
   119   in (Thm.instantiate_cterm ([], inst) ct, names) end
   120 
   121 
   122 fun mk_bound ctxt (i, T) =
   123   let val ct = Thm.cterm_of ctxt (Var ((Name.uu, 0), T))
   124   in (ct, [(i, ct)]) end
   125 
   126 local
   127   fun mk_quant1 ctxt q T (ct, vars) =
   128     let
   129       val cv =
   130         (case AList.lookup (op =) vars 0 of
   131           SOME cv => cv
   132         | _ => Thm.cterm_of ctxt (Var ((Name.uu, Thm.maxidx_of_cterm ct + 1), T)))
   133       fun dec (i, v) = if i = 0 then NONE else SOME (i-1, v)
   134       val vars' = map_filter dec vars
   135     in (Thm.apply (Old_SMT_Utils.instT' cv q) (Thm.lambda cv ct), vars') end
   136 
   137   fun quant name =
   138     Old_SMT_Utils.mk_const_pat @{theory} name (Old_SMT_Utils.destT1 o Old_SMT_Utils.destT1)
   139   val forall = quant @{const_name All}
   140   val exists = quant @{const_name Ex}
   141 in
   142 
   143 fun mk_quant is_forall ctxt =
   144   fold_rev (mk_quant1 ctxt (if is_forall then forall else exists))
   145 
   146 end
   147 
   148 local
   149   fun prep (ct, vars) (maxidx, all_vars) =
   150     let
   151       val maxidx' = maxidx + Thm.maxidx_of_cterm ct + 1
   152 
   153       fun part (i, cv) =
   154         (case AList.lookup (op =) all_vars i of
   155           SOME cu => apfst (if cu aconvc cv then I else cons (cv, cu))
   156         | NONE =>
   157             let val cv' = Thm.incr_indexes_cterm maxidx cv
   158             in apfst (cons (cv, cv')) #> apsnd (cons (i, cv')) end)
   159 
   160       val (inst, vars') =
   161         if null vars then ([], vars)
   162         else fold part vars ([], [])
   163 
   164     in (Thm.instantiate_cterm ([], inst) ct, (maxidx', vars' @ all_vars)) end
   165 in
   166 fun mk_fun f ts =
   167   let val (cts, (_, vars)) = fold_map prep ts (0, [])
   168   in f cts |> Option.map (rpair vars) end
   169 end
   170 
   171 
   172 
   173 (* proof parser *)
   174 
   175 datatype proof_step = Proof_Step of {
   176   rule: rule,
   177   args: cterm list,
   178   prems: int list,
   179   prop: cterm }
   180 
   181 
   182 (** parser context **)
   183 
   184 val not_false = Thm.cterm_of @{context} (@{const Not} $ @{const False})
   185 
   186 fun make_context ctxt typs terms =
   187   let
   188     val ctxt' = 
   189       ctxt
   190       |> Symtab.fold (Variable.declare_typ o snd) typs
   191       |> Symtab.fold (Variable.declare_term o snd) terms
   192 
   193     fun cert @{const True} = not_false
   194       | cert t = Thm.cterm_of ctxt' t
   195 
   196   in (typs, Symtab.map (K cert) terms, Inttab.empty, [], [], ctxt') end
   197 
   198 fun fresh_name n (typs, terms, exprs, steps, vars, ctxt) =
   199   let val (n', ctxt') = yield_singleton Variable.variant_fixes n ctxt
   200   in (n', (typs, terms, exprs, steps, vars, ctxt')) end
   201 
   202 fun context_of (_, _, _, _, _, ctxt) = ctxt
   203 
   204 fun add_decl (n, T) (cx as (_, terms, _, _, _, _)) =
   205   (case Symtab.lookup terms n of
   206     SOME _ => cx
   207   | NONE => cx |> fresh_name (decl_prefix ^ n)
   208       |> (fn (m, (typs, terms, exprs, steps, vars, ctxt)) =>
   209            let
   210              val upd = Symtab.update (n, Thm.cterm_of ctxt (Free (m, T)))
   211            in (typs, upd terms, exprs, steps, vars, ctxt) end))
   212 
   213 fun mk_typ (typs, _, _, _, _, ctxt) (s as Old_Z3_Interface.Sym (n, _)) = 
   214   (case Old_Z3_Interface.mk_builtin_typ ctxt s of
   215     SOME T => SOME T
   216   | NONE => Symtab.lookup typs n)
   217 
   218 fun mk_num (_, _, _, _, _, ctxt) (i, T) =
   219   mk_fun (K (Old_Z3_Interface.mk_builtin_num ctxt i T)) []
   220 
   221 fun mk_app (_, terms, _, _, _, ctxt) (s as Old_Z3_Interface.Sym (n, _), es) =
   222   mk_fun (fn cts =>
   223     (case Old_Z3_Interface.mk_builtin_fun ctxt s cts of
   224       SOME ct => SOME ct
   225     | NONE =>
   226         Symtab.lookup terms n |> Option.map (Drule.list_comb o rpair cts))) es
   227 
   228 fun add_expr k t (typs, terms, exprs, steps, vars, ctxt) =
   229   (typs, terms, Inttab.update (k, t) exprs, steps, vars, ctxt)
   230 
   231 fun lookup_expr (_, _, exprs, _, _, _) = Inttab.lookup exprs
   232 
   233 fun add_proof_step k ((r, args), prop) cx =
   234   let
   235     val (typs, terms, exprs, steps, vars, ctxt) = cx
   236     val (ct, vs) = close ctxt prop
   237     fun part (SOME e, _) (cts, ps) = (close ctxt e :: cts, ps)
   238       | part (NONE, i) (cts, ps) = (cts, i :: ps)
   239     val (args', prems) = fold (part o `(lookup_expr cx)) args ([], [])
   240     val (cts, vss) = split_list args'
   241     val step = Proof_Step {rule=r, args=rev cts, prems=rev prems,
   242       prop = Old_SMT_Utils.mk_cprop ct}
   243     val vars' = fold (union (op =)) (vs :: vss) vars
   244   in (typs, terms, exprs, (k, step) :: steps, vars', ctxt) end
   245 
   246 fun finish (_, _, _, steps, vars, ctxt) =
   247   let
   248     fun coll (p as (k, Proof_Step {prems, rule, prop, ...})) (ars, ps, ids) =
   249       (case rule of
   250         Asserted => ((k, prop) :: ars, ps, ids)
   251       | Goal => ((k, prop) :: ars, ps, ids)
   252       | _ =>
   253           if Inttab.defined ids k then
   254             (ars, p :: ps, fold (Inttab.update o rpair ()) prems ids)
   255           else (ars, ps, ids))
   256 
   257     val (ars, steps', _) = fold coll steps ([], [], Inttab.make [(~1, ())])
   258   in (ars, steps', vars, ctxt) end
   259 
   260 
   261 (** core parser **)
   262 
   263 fun parse_exn line_no msg = raise Old_SMT_Failure.SMT (Old_SMT_Failure.Other_Failure
   264   ("Z3 proof parser (line " ^ string_of_int line_no ^ "): " ^ msg))
   265 
   266 fun scan_exn msg ((line_no, _), _) = parse_exn line_no msg
   267 
   268 fun with_info f cx =
   269   (case f ((NONE, 1), cx) of
   270     ((SOME _, _), cx') => cx'
   271   | ((_, line_no), _) => parse_exn line_no "bad proof")
   272 
   273 fun parse_line _ _ (st as ((SOME _, _), _)) = st
   274   | parse_line scan line ((_, line_no), cx) =
   275       let val st = ((line_no, cx), raw_explode line)
   276       in
   277         (case Scan.catch (Scan.finite' Symbol.stopper (Scan.option scan)) st of
   278           (SOME r, ((_, cx'), _)) => ((r, line_no+1), cx')
   279         | (NONE, _) => parse_exn line_no ("bad proof line: " ^ quote line))
   280       end
   281 
   282 fun with_context f x ((line_no, cx), st) =
   283   let val (y, cx') = f x cx
   284   in (y, ((line_no, cx'), st)) end
   285   
   286 
   287 fun lookup_context f x (st as ((_, cx), _)) = (f cx x, st)
   288 
   289 
   290 (** parser combinators and parsers for basic entities **)
   291 
   292 fun $$ s = Scan.lift (Scan.$$ s)
   293 fun this s = Scan.lift (Scan.this_string s)
   294 val is_blank = Symbol.is_ascii_blank
   295 fun blank st = Scan.lift (Scan.many1 is_blank) st
   296 fun sep scan = blank |-- scan
   297 fun seps scan = Scan.repeat (sep scan)
   298 fun seps1 scan = Scan.repeat1 (sep scan)
   299 fun seps_by scan_sep scan = scan ::: Scan.repeat (scan_sep |-- scan)
   300 
   301 val lpar = "(" and rpar = ")"
   302 val lbra = "[" and rbra = "]"
   303 fun par scan = $$ lpar |-- scan --| $$ rpar
   304 fun bra scan = $$ lbra |-- scan --| $$ rbra
   305 
   306 val digit = (fn
   307   "0" => SOME 0 | "1" => SOME 1 | "2" => SOME 2 | "3" => SOME 3 |
   308   "4" => SOME 4 | "5" => SOME 5 | "6" => SOME 6 | "7" => SOME 7 |
   309   "8" => SOME 8 | "9" => SOME 9 | _ => NONE)
   310 
   311 fun digits st = (Scan.lift (Scan.many1 Symbol.is_ascii_digit) >> implode) st
   312 
   313 fun nat_num st = (Scan.lift (Scan.repeat1 (Scan.some digit)) >> (fn ds =>
   314   fold (fn d => fn i => i * 10 + d) ds 0)) st
   315 
   316 fun int_num st = (Scan.optional ($$ "-" >> K (fn i => ~i)) I :|--
   317   (fn sign => nat_num >> sign)) st
   318 
   319 val is_char = Symbol.is_ascii_letter orf Symbol.is_ascii_digit orf
   320   member (op =) (raw_explode "_+*-/%~=<>$&|?!.@^#")
   321 
   322 fun name st = (Scan.lift (Scan.many1 is_char) >> implode) st
   323 
   324 fun sym st = (name --
   325   Scan.optional (bra (seps_by ($$ ":") sym)) [] >> Old_Z3_Interface.Sym) st
   326 
   327 fun id st = ($$ "#" |-- nat_num) st
   328 
   329 
   330 (** parsers for various parts of Z3 proofs **)
   331 
   332 fun sort st = Scan.first [
   333   this "array" |-- bra (sort --| $$ ":" -- sort) >> (op -->),
   334   par (this "->" |-- seps1 sort) >> ((op --->) o split_last),
   335   sym :|-- (fn s as Old_Z3_Interface.Sym (n, _) => lookup_context mk_typ s :|-- (fn
   336     SOME T => Scan.succeed T
   337   | NONE => scan_exn ("unknown sort: " ^ quote n)))] st
   338 
   339 fun bound st = (par (this ":var" |-- sep nat_num -- sep sort) :|--
   340   lookup_context (mk_bound o context_of)) st
   341 
   342 fun numb (n as (i, _)) = lookup_context mk_num n :|-- (fn
   343     SOME n' => Scan.succeed n'
   344   | NONE => scan_exn ("unknown number: " ^ quote (string_of_int i)))
   345 
   346 fun appl (app as (Old_Z3_Interface.Sym (n, _), _)) =
   347   lookup_context mk_app app :|-- (fn 
   348       SOME app' => Scan.succeed app'
   349     | NONE => scan_exn ("unknown function symbol: " ^ quote n))
   350 
   351 fun bv_size st = (digits >> (fn sz =>
   352   Old_Z3_Interface.Sym ("bv", [Old_Z3_Interface.Sym (sz, [])]))) st
   353 
   354 fun bv_number_sort st = (bv_size :|-- lookup_context mk_typ :|-- (fn
   355     SOME cT => Scan.succeed cT
   356   | NONE => scan_exn ("unknown sort: " ^ quote "bv"))) st
   357 
   358 fun bv_number st =
   359   (this "bv" |-- bra (nat_num --| $$ ":" -- bv_number_sort) :|-- numb) st
   360 
   361 fun frac_number st = (
   362   int_num --| $$ "/" -- int_num --| this "::" -- sort :|-- (fn ((i, j), T) =>
   363     numb (i, T) -- numb (j, T) :|-- (fn (n, m) =>
   364       appl (Old_Z3_Interface.Sym ("/", []), [n, m])))) st
   365 
   366 fun plain_number st = (int_num --| this "::" -- sort :|-- numb) st
   367 
   368 fun number st = Scan.first [bv_number, frac_number, plain_number] st
   369 
   370 fun constant st = ((sym >> rpair []) :|-- appl) st
   371 
   372 fun expr_id st = (id :|-- (fn i => lookup_context lookup_expr i :|-- (fn
   373     SOME e => Scan.succeed e
   374   | NONE => scan_exn ("unknown term id: " ^ quote (string_of_int i))))) st
   375 
   376 fun arg st = Scan.first [expr_id, number, constant] st
   377 
   378 fun application st = par ((sym -- Scan.repeat1 (sep arg)) :|-- appl) st
   379 
   380 fun variables st = par (this "vars" |-- seps1 (par (name |-- sep sort))) st
   381 
   382 fun pats st = seps (par ((this ":pat" || this ":nopat") |-- seps1 id)) st
   383 
   384 val ctrue = Thm.cterm_of @{context} @{const True}
   385 
   386 fun pattern st = par (this "pattern" |-- Scan.repeat1 (sep arg) >>
   387   (the o mk_fun (K (SOME ctrue)))) st
   388 
   389 fun quant_kind st = st |> (
   390   this "forall" >> K (mk_quant true o context_of) ||
   391   this "exists" >> K (mk_quant false o context_of))
   392 
   393 fun quantifier st =
   394   (par (quant_kind -- sep variables --| pats -- sep arg) :|--
   395      lookup_context (fn cx => fn ((mk_q, Ts), body) => mk_q cx Ts body)) st
   396 
   397 fun expr k =
   398   Scan.first [bound, quantifier, pattern, application, number, constant] :|--
   399   with_context (pair NONE oo add_expr k)
   400 
   401 val rule_arg = id
   402   (* if this is modified, then 'th_lemma_arg' needs reviewing *)
   403 
   404 fun th_lemma_arg st = Scan.unless (sep rule_arg >> K "" || $$ rbra) (sep name) st
   405 
   406 fun rule_name st = ((name >> `(Symtab.lookup rule_names)) :|-- (fn 
   407     (SOME (Th_Lemma _), _) => Scan.repeat th_lemma_arg >> Th_Lemma
   408   | (SOME r, _) => Scan.succeed r
   409   | (NONE, n) => scan_exn ("unknown proof rule: " ^ quote n))) st
   410 
   411 fun rule f k =
   412   bra (rule_name -- seps id) --| $$ ":" -- sep arg #->
   413   with_context (pair (f k) oo add_proof_step k)
   414 
   415 fun decl st = (this "decl" |-- sep name --| sep (this "::") -- sep sort :|--
   416   with_context (pair NONE oo add_decl)) st
   417 
   418 fun def st = (id --| sep (this ":=")) st
   419 
   420 fun node st = st |> (
   421   decl ||
   422   def :|-- (fn k => sep (expr k) || sep (rule (K NONE) k)) ||
   423   rule SOME ~1)
   424 
   425 
   426 (** overall parser **)
   427 
   428 (*
   429   Currently, terms are parsed bottom-up (i.e., along with parsing the proof
   430   text line by line), but proofs are reconstructed top-down (i.e. by an
   431   in-order top-down traversal of the proof tree/graph).  The latter approach
   432   was taken because some proof texts comprise irrelevant proof steps which
   433   will thus not be reconstructed.  This approach might also be beneficial
   434   for constructing terms, but it would also increase the complexity of the
   435   (otherwise rather modular) code.
   436 *)
   437 
   438 fun parse ctxt typs terms proof_text =
   439   make_context ctxt typs terms
   440   |> with_info (fold (parse_line node) proof_text)
   441   |> finish
   442 
   443 end