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