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