src/HOL/Tools/SMT2/z3_new_proof.ML
author blanchet
Fri, 14 Mar 2014 09:56:06 +0100
changeset 56122 40f7b45b2472
parent 56078 624faeda77b5
child 56245 84fc7dfa3cd4
permissions -rw-r--r--
made SML/NJ happier
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
56078
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
     1
(*  Title:      HOL/Tools/SMT2/z3_new_proof.ML
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
     2
    Author:     Sascha Boehme, TU Muenchen
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
     3
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
     4
Z3 proofs: parsing and abstract syntax tree.
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
     5
*)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
     6
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
     7
signature Z3_NEW_PROOF =
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
     8
sig
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
     9
  (*proof rules*)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    10
  datatype z3_rule = True_Axiom | Asserted | Goal | Modus_Ponens | Reflexivity |
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    11
    Symmetry | Transitivity | Transitivity_Star | Monotonicity | Quant_Intro |
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    12
    Distributivity | And_Elim | Not_Or_Elim | Rewrite | Rewrite_Star |
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    13
    Pull_Quant | Pull_Quant_Star | Push_Quant | Elim_Unused_Vars |
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    14
    Dest_Eq_Res | Quant_Inst | Hypothesis | Lemma | Unit_Resolution |
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    15
    Iff_True | Iff_False | Commutativity | Def_Axiom | Intro_Def | Apply_Def |
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    16
    Iff_Oeq | Nnf_Pos | Nnf_Neg | Nnf_Star | Cnf_Star | Skolemize |
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    17
    Modus_Ponens_Oeq | Th_Lemma of string
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    18
  val string_of_rule: z3_rule -> string
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    19
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    20
  (*proofs*)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    21
  datatype z3_step = Z3_Step of {
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    22
    id: int,
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    23
    rule: z3_rule,
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    24
    prems: int list,
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    25
    concl: term,
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    26
    fixes: string list,
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    27
    is_fix_step: bool}
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    28
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    29
  (*type and term parsers*)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    30
  type type_parser = SMTLIB2.tree * typ list -> typ option
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    31
  type term_parser = SMTLIB2.tree * term list -> term option
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    32
  val add_type_parser: type_parser -> Context.generic -> Context.generic
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    33
  val add_term_parser: term_parser -> Context.generic -> Context.generic
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    34
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    35
  (*proof parser*)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    36
  val parse: typ Symtab.table -> term Symtab.table -> string list ->
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    37
    Proof.context -> z3_step list * Proof.context
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    38
end
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    39
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    40
structure Z3_New_Proof: Z3_NEW_PROOF =
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    41
struct
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    42
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    43
(* proof rules *)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    44
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    45
datatype z3_rule = True_Axiom | Asserted | Goal | Modus_Ponens | Reflexivity |
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    46
  Symmetry | Transitivity | Transitivity_Star | Monotonicity | Quant_Intro |
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    47
  Distributivity | And_Elim | Not_Or_Elim | Rewrite | Rewrite_Star |
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    48
  Pull_Quant | Pull_Quant_Star | Push_Quant | Elim_Unused_Vars | Dest_Eq_Res |
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    49
  Quant_Inst | Hypothesis | Lemma | Unit_Resolution | Iff_True | Iff_False |
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    50
  Commutativity | Def_Axiom | Intro_Def | Apply_Def | Iff_Oeq | Nnf_Pos |
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    51
  Nnf_Neg | Nnf_Star | Cnf_Star | Skolemize | Modus_Ponens_Oeq |
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    52
  Th_Lemma of string
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    53
  (* TODO: some proof rules come with further information
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    54
     that is currently dropped by the parser *)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    55
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    56
val rule_names = Symtab.make [
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    57
  ("true-axiom", True_Axiom),
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    58
  ("asserted", Asserted),
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    59
  ("goal", Goal),
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    60
  ("mp", Modus_Ponens),
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    61
  ("refl", Reflexivity),
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    62
  ("symm", Symmetry),
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    63
  ("trans", Transitivity),
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    64
  ("trans*", Transitivity_Star),
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    65
  ("monotonicity", Monotonicity),
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    66
  ("quant-intro", Quant_Intro),
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    67
  ("distributivity", Distributivity),
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    68
  ("and-elim", And_Elim),
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    69
  ("not-or-elim", Not_Or_Elim),
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    70
  ("rewrite", Rewrite),
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    71
  ("rewrite*", Rewrite_Star),
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    72
  ("pull-quant", Pull_Quant),
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    73
  ("pull-quant*", Pull_Quant_Star),
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    74
  ("push-quant", Push_Quant),
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    75
  ("elim-unused", Elim_Unused_Vars),
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    76
  ("der", Dest_Eq_Res),
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    77
  ("quant-inst", Quant_Inst),
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    78
  ("hypothesis", Hypothesis),
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    79
  ("lemma", Lemma),
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    80
  ("unit-resolution", Unit_Resolution),
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    81
  ("iff-true", Iff_True),
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    82
  ("iff-false", Iff_False),
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    83
  ("commutativity", Commutativity),
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    84
  ("def-axiom", Def_Axiom),
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    85
  ("intro-def", Intro_Def),
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    86
  ("apply-def", Apply_Def),
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    87
  ("iff~", Iff_Oeq),
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    88
  ("nnf-pos", Nnf_Pos),
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    89
  ("nnf-neg", Nnf_Neg),
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    90
  ("nnf*", Nnf_Star),
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    91
  ("cnf*", Cnf_Star),
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    92
  ("sk", Skolemize),
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    93
  ("mp~", Modus_Ponens_Oeq)]
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    94
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    95
fun rule_of_string name =
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    96
  (case Symtab.lookup rule_names name of
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    97
    SOME rule => rule
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    98
  | NONE => error ("unknown Z3 proof rule " ^ quote name))
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    99
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   100
fun string_of_rule (Th_Lemma kind) = "th-lemma " ^ kind
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   101
  | string_of_rule r =
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   102
      let fun eq_rule (s, r') = if r = r' then SOME s else NONE 
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   103
      in the (Symtab.get_first eq_rule rule_names) end
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   104
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   105
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   106
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   107
(* proofs *)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   108
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   109
datatype z3_node = Z3_Node of {
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   110
  id: int,
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   111
  rule: z3_rule,
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   112
  prems: z3_node list,
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   113
  concl: term,
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   114
  bounds: string list}
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   115
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   116
fun mk_node id rule prems concl bounds =
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   117
  Z3_Node {id=id, rule=rule, prems=prems, concl=concl, bounds=bounds}
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   118
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   119
datatype z3_step = Z3_Step of {
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   120
  id: int,
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   121
  rule: z3_rule,
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   122
  prems: int list,
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   123
  concl: term,
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   124
  fixes: string list,
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   125
  is_fix_step: bool}
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   126
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   127
fun mk_step id rule prems concl fixes is_fix_step =
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   128
  Z3_Step {id=id, rule=rule, prems=prems, concl=concl, fixes=fixes,
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   129
    is_fix_step=is_fix_step}
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   130
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   131
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   132
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   133
(* core type and term parser *)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   134
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   135
fun core_type_parser (SMTLIB2.Sym "Bool", []) = SOME @{typ HOL.bool}
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   136
  | core_type_parser (SMTLIB2.Sym "Int", []) = SOME @{typ Int.int}
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   137
  | core_type_parser _ = NONE
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   138
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   139
fun mk_unary n t =
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   140
  let val T = fastype_of t
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   141
  in Const (n, T --> T) $ t end
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   142
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   143
fun mk_binary' n T U t1 t2 = Const (n, [T, T] ---> U) $ t1 $ t2
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   144
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   145
fun mk_binary n t1 t2 =
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   146
  let val T = fastype_of t1
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   147
  in mk_binary' n T T t1 t2 end
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   148
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   149
fun mk_rassoc f t ts =
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   150
  let val us = rev (t :: ts)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   151
  in fold f (tl us) (hd us) end
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   152
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   153
fun mk_lassoc f t ts = fold (fn u1 => fn u2 => f u2 u1) ts t
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   154
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   155
fun mk_lassoc' n = mk_lassoc (mk_binary n)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   156
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   157
fun mk_binary_pred n S t1 t2 =
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   158
  let
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   159
    val T1 = fastype_of t1
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   160
    val T2 = fastype_of t2
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   161
    val T =
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   162
      if T1 <> Term.dummyT then T1
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   163
      else if T2 <> Term.dummyT then T2
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   164
      else TVar (("?a", serial ()), S)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   165
  in mk_binary' n T @{typ HOL.bool} t1 t2 end
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   166
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   167
fun mk_less t1 t2 = mk_binary_pred @{const_name ord_class.less} @{sort linorder} t1 t2
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   168
fun mk_less_eq t1 t2 = mk_binary_pred @{const_name ord_class.less_eq} @{sort linorder} t1 t2
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   169
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   170
fun core_term_parser (SMTLIB2.Sym "true", _) = SOME @{const HOL.True}
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   171
  | core_term_parser (SMTLIB2.Sym "false", _) = SOME @{const HOL.False}
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   172
  | core_term_parser (SMTLIB2.Sym "not", [t]) = SOME (HOLogic.mk_not t)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   173
  | core_term_parser (SMTLIB2.Sym "and", t :: ts) = SOME (mk_rassoc (curry HOLogic.mk_conj) t ts)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   174
  | core_term_parser (SMTLIB2.Sym "or", t :: ts) = SOME (mk_rassoc (curry HOLogic.mk_disj) t ts)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   175
  | core_term_parser (SMTLIB2.Sym "=>", [t1, t2]) = SOME (HOLogic.mk_imp (t1, t2))
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   176
  | core_term_parser (SMTLIB2.Sym "implies", [t1, t2]) = SOME (HOLogic.mk_imp (t1, t2))
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   177
  | core_term_parser (SMTLIB2.Sym "=", [t1, t2]) = SOME (HOLogic.mk_eq (t1, t2))
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   178
  | core_term_parser (SMTLIB2.Sym "~", [t1, t2]) = SOME (HOLogic.mk_eq (t1, t2))
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   179
  | core_term_parser (SMTLIB2.Sym "ite", [t1, t2, t3]) =
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   180
      let
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   181
        val T = fastype_of t2
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   182
        val c = Const (@{const_name HOL.If}, [@{typ HOL.bool}, T, T] ---> T)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   183
      in SOME (c $ t1 $ t2 $ t3) end
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   184
  | core_term_parser (SMTLIB2.Num i, []) = SOME (HOLogic.mk_number @{typ Int.int} i)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   185
  | core_term_parser (SMTLIB2.Sym "-", [t]) = SOME (mk_unary @{const_name uminus_class.uminus} t)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   186
  | core_term_parser (SMTLIB2.Sym "~", [t]) = SOME (mk_unary @{const_name uminus_class.uminus} t)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   187
  | core_term_parser (SMTLIB2.Sym "+", t :: ts) =
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   188
      SOME (mk_lassoc' @{const_name plus_class.plus} t ts)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   189
  | core_term_parser (SMTLIB2.Sym "-", t :: ts) =
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   190
      SOME (mk_lassoc' @{const_name minus_class.minus} t ts)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   191
  | core_term_parser (SMTLIB2.Sym "*", t :: ts) =
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   192
      SOME (mk_lassoc' @{const_name times_class.times} t ts)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   193
  | core_term_parser (SMTLIB2.Sym "div", [t1, t2]) = SOME (mk_binary @{const_name SMT2.z3div} t1 t2)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   194
  | core_term_parser (SMTLIB2.Sym "mod", [t1, t2]) = SOME (mk_binary @{const_name SMT2.z3mod} t1 t2)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   195
  | core_term_parser (SMTLIB2.Sym "<", [t1, t2]) = SOME (mk_less t1 t2)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   196
  | core_term_parser (SMTLIB2.Sym ">", [t1, t2]) = SOME (mk_less t2 t1)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   197
  | core_term_parser (SMTLIB2.Sym "<=", [t1, t2]) = SOME (mk_less_eq t1 t2)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   198
  | core_term_parser (SMTLIB2.Sym ">=", [t1, t2]) = SOME (mk_less_eq t2 t1)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   199
  | core_term_parser _ = NONE
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   200
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   201
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   202
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   203
(* type and term parsers *)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   204
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   205
type type_parser = SMTLIB2.tree * typ list -> typ option
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   206
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   207
type term_parser = SMTLIB2.tree * term list -> term option
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   208
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   209
fun id_ord ((id1, _), (id2, _)) = int_ord (id1, id2)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   210
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   211
structure Parsers = Generic_Data
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   212
(
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   213
  type T = (int * type_parser) list * (int * term_parser) list
56122
40f7b45b2472 made SML/NJ happier
blanchet
parents: 56078
diff changeset
   214
  val empty : T = ([(serial (), core_type_parser)], [(serial (), core_term_parser)])
56078
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   215
  val extend = I
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   216
  fun merge ((tys1, ts1), (tys2, ts2)) =
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   217
    (Ord_List.merge id_ord (tys1, tys2), Ord_List.merge id_ord (ts1, ts2))
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   218
)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   219
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   220
fun add_type_parser type_parser =
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   221
  Parsers.map (apfst (Ord_List.insert id_ord (serial (), type_parser)))
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   222
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   223
fun add_term_parser term_parser =
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   224
  Parsers.map (apsnd (Ord_List.insert id_ord (serial (), term_parser)))
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   225
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   226
fun get_type_parsers ctxt = map snd (fst (Parsers.get (Context.Proof ctxt)))
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   227
fun get_term_parsers ctxt = map snd (snd (Parsers.get (Context.Proof ctxt)))
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   228
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   229
fun apply_parsers parsers x =
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   230
  let
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   231
    fun apply [] = NONE
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   232
      | apply (parser :: parsers) =
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   233
          (case parser x of
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   234
            SOME y => SOME y
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   235
          | NONE => apply parsers)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   236
  in apply parsers end
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   237
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   238
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   239
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   240
(* proof parser context *)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   241
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   242
datatype shared = Tree of SMTLIB2.tree | Term of term | Proof of z3_node | None
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   243
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   244
type 'a context = {
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   245
  ctxt: Proof.context,
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   246
  id: int,
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   247
  syms: shared Symtab.table,
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   248
  typs: typ Symtab.table,
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   249
  funs: term Symtab.table,
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   250
  extra: 'a}
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   251
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   252
fun mk_context ctxt id syms typs funs extra: 'a context =
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   253
  {ctxt=ctxt, id=id, syms=syms, typs=typs, funs=funs, extra=extra}
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   254
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   255
fun empty_context ctxt typs funs = mk_context ctxt 1 Symtab.empty typs funs []
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   256
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   257
fun ctxt_of ({ctxt, ...}: 'a context) = ctxt
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   258
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   259
fun next_id ({ctxt, id, syms, typs, funs, extra}: 'a context) =
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   260
  (id, mk_context ctxt (id + 1) syms typs funs extra)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   261
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   262
fun lookup_binding ({syms, ...}: 'a context) =
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   263
  the_default None o Symtab.lookup syms
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   264
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   265
fun map_syms f ({ctxt, id, syms, typs, funs, extra}: 'a context) =
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   266
  mk_context ctxt id (f syms) typs funs extra
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   267
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   268
fun update_binding b = map_syms (Symtab.update b)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   269
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   270
fun with_bindings bs f cx =
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   271
  let val bs' = map (lookup_binding cx o fst) bs
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   272
  in
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   273
    cx
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   274
    |> fold update_binding bs
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   275
    |> f
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   276
    ||> fold2 (fn (name, _) => update_binding o pair name) bs bs'
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   277
  end
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   278
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   279
fun lookup_typ ({typs, ...}: 'a context) = Symtab.lookup typs
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   280
fun lookup_fun ({funs, ...}: 'a context) = Symtab.lookup funs
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   281
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   282
fun fresh_fun add name n T ({ctxt, id, syms, typs, funs, extra}: 'a context) =
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   283
  let
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   284
    val (n', ctxt') = yield_singleton Variable.variant_fixes n ctxt
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   285
    val t = Free (n', T)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   286
    val funs' = Symtab.update (name, t) funs
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   287
  in (t, mk_context ctxt' id syms typs funs' (add (n', T) extra)) end
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   288
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   289
fun declare_fun name n T = snd o fresh_fun cons name n T
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   290
fun declare_free name n T = fresh_fun (cons o pair name) name n T
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   291
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   292
fun with_fresh_names f ({ctxt, id, syms, typs, funs, extra}: 'a context) =
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   293
  let
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   294
    fun bind (_, v as (_, T)) t = Logic.all_const T $ Term.absfree v t
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   295
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   296
    val needs_inferT = equal Term.dummyT orf Term.is_TVar
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   297
    val needs_infer = Term.exists_type (Term.exists_subtype needs_inferT)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   298
    fun infer_types ctxt =
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   299
      singleton (Type_Infer_Context.infer_types ctxt) #>
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   300
      singleton (Proof_Context.standard_term_check_finish ctxt)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   301
    fun infer ctxt t = if needs_infer t then infer_types ctxt t else t
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   302
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   303
    type bindings = (string * (string * typ)) list
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   304
    val (t, {ctxt=ctxt', extra=names, ...}: bindings context) =
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   305
      f (mk_context ctxt id syms typs funs [])
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   306
    val t' = infer ctxt' (fold_rev bind names (HOLogic.mk_Trueprop t))
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   307
   
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   308
  in ((t', map fst names), mk_context ctxt id syms typs funs extra) end
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   309
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   310
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   311
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   312
(* proof parser *)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   313
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   314
exception Z3_PARSE of string * SMTLIB2.tree
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   315
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   316
val desymbolize = Name.desymbolize false o perhaps (try (unprefix "?"))
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   317
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   318
fun parse_type cx ty Ts =
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   319
  (case apply_parsers (get_type_parsers (ctxt_of cx)) (ty, Ts) of
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   320
    SOME T => T
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   321
  | NONE =>
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   322
      (case ty of
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   323
        SMTLIB2.Sym name =>
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   324
          (case lookup_typ cx name of
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   325
            SOME T => T
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   326
          | NONE => raise Z3_PARSE ("unknown Z3 type", ty))
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   327
      | _ => raise Z3_PARSE ("bad Z3 type format", ty)))
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   328
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   329
fun parse_term t ts cx =
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   330
  (case apply_parsers (get_term_parsers (ctxt_of cx)) (t, ts) of
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   331
    SOME u => (u, cx)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   332
  | NONE =>
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   333
      (case t of
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   334
        SMTLIB2.Sym name =>
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   335
          (case lookup_fun cx name of
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   336
            SOME u => (Term.list_comb (u, ts), cx)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   337
          | NONE =>
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   338
              if null ts then declare_free name (desymbolize name) Term.dummyT cx
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   339
              else raise Z3_PARSE ("bad Z3 term", t))
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   340
      | _ => raise Z3_PARSE ("bad Z3 term format", t)))
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   341
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   342
fun type_of cx ty =
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   343
  (case try (parse_type cx ty) [] of
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   344
    SOME T => T
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   345
  | NONE =>
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   346
      (case ty of
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   347
        SMTLIB2.S (ty' :: tys) => parse_type cx ty' (map (type_of cx) tys)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   348
      | _ => raise Z3_PARSE ("bad Z3 type", ty)))
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   349
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   350
fun dest_var cx (SMTLIB2.S [SMTLIB2.Sym name, ty]) = (name, (desymbolize name, type_of cx ty))
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   351
  | dest_var _ v = raise Z3_PARSE ("bad Z3 quantifier variable format", v)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   352
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   353
fun dest_body (SMTLIB2.S (SMTLIB2.Sym "!" :: body :: _)) = dest_body body
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   354
  | dest_body body = body
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   355
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   356
fun dest_binding (SMTLIB2.S [SMTLIB2.Sym name, t]) = (name, Tree t)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   357
  | dest_binding b = raise Z3_PARSE ("bad Z3 let binding format", b)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   358
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   359
fun term_of t cx =
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   360
  (case t of
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   361
    SMTLIB2.S [SMTLIB2.Sym "forall", SMTLIB2.S vars, body] =>
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   362
      quant HOLogic.mk_all vars body cx
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   363
  | SMTLIB2.S [SMTLIB2.Sym "exists", SMTLIB2.S vars, body] =>
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   364
      quant HOLogic.mk_exists vars body cx
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   365
  | SMTLIB2.S [SMTLIB2.Sym "let", SMTLIB2.S bindings, body] =>
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   366
      with_bindings (map dest_binding bindings) (term_of body) cx
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   367
  | SMTLIB2.S (SMTLIB2.Sym "!" :: t :: _) => term_of t cx
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   368
  | SMTLIB2.S (f :: args) =>
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   369
      cx
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   370
      |> fold_map term_of args
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   371
      |-> parse_term f
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   372
  | SMTLIB2.Sym name =>
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   373
      (case lookup_binding cx name of
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   374
        Tree u =>
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   375
          cx
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   376
          |> term_of u
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   377
          |-> (fn u' => pair u' o update_binding (name, Term u'))
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   378
      | Term u => (u, cx)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   379
      | None => parse_term t [] cx
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   380
      | _ => raise Z3_PARSE ("bad Z3 term format", t))
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   381
  | _ => parse_term t [] cx)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   382
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   383
and quant q vars body cx =
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   384
  let val vs = map (dest_var cx) vars
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   385
  in
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   386
    cx
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   387
    |> with_bindings (map (apsnd (Term o Free)) vs) (term_of (dest_body body))
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   388
    |>> fold_rev (fn (_, (n, T)) => fn t => q (n, T, t)) vs
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   389
  end
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   390
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   391
fun rule_of (SMTLIB2.Sym name) = rule_of_string name
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   392
  | rule_of (SMTLIB2.S (SMTLIB2.Sym "_" :: SMTLIB2.Sym name :: args)) =
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   393
      (case (name, args) of
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   394
        ("th-lemma", SMTLIB2.Sym kind :: _) => Th_Lemma kind
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   395
      | _ => rule_of_string name)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   396
  | rule_of r = raise Z3_PARSE ("bad Z3 proof rule format", r)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   397
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   398
fun node_of p cx =
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   399
  (case p of
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   400
    SMTLIB2.Sym name =>
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   401
      (case lookup_binding cx name of
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   402
        Proof node => (node, cx)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   403
      | Tree p' =>
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   404
          cx
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   405
          |> node_of p'
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   406
          |-> (fn node => pair node o update_binding (name, Proof node))
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   407
      | _ => raise Z3_PARSE ("bad Z3 proof format", p))
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   408
  | SMTLIB2.S [SMTLIB2.Sym "let", SMTLIB2.S bindings, p] =>
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   409
      with_bindings (map dest_binding bindings) (node_of p) cx
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   410
  | SMTLIB2.S (name :: parts) =>
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   411
      let
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   412
        val (ps, p) = split_last parts
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   413
        val r = rule_of name
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   414
      in
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   415
        cx
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   416
        |> fold_map node_of ps
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   417
        ||>> with_fresh_names (term_of p)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   418
        ||>> next_id
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   419
        |>> (fn ((prems, (t, ns)), id) => mk_node id r prems t ns)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   420
      end
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   421
  | _ => raise Z3_PARSE ("bad Z3 proof format", p))
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   422
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   423
fun dest_name (SMTLIB2.Sym name) = name
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   424
  | dest_name t = raise Z3_PARSE ("bad name", t)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   425
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   426
fun dest_seq (SMTLIB2.S ts) = ts
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   427
  | dest_seq t = raise Z3_PARSE ("bad Z3 proof format", t)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   428
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   429
fun parse' (SMTLIB2.S (SMTLIB2.Sym "set-logic" :: _) :: ts) cx = parse' ts cx
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   430
  | parse' (SMTLIB2.S [SMTLIB2.Sym "declare-fun", n, tys, ty] :: ts) cx =
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   431
      let
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   432
        val name = dest_name n
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   433
        val Ts = map (type_of cx) (dest_seq tys)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   434
        val T = type_of cx ty
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   435
      in parse' ts (declare_fun name (desymbolize name) (Ts ---> T) cx) end
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   436
  | parse' (SMTLIB2.S [SMTLIB2.Sym "proof", p] :: _) cx = node_of p cx
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   437
  | parse' ts _ = raise Z3_PARSE ("bad Z3 proof declarations", SMTLIB2.S ts)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   438
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   439
fun parse_proof typs funs lines ctxt =
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   440
  let
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   441
    val ts = dest_seq (SMTLIB2.parse lines)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   442
    val (node, cx) = parse' ts (empty_context ctxt typs funs)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   443
  in (node, ctxt_of cx) end
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   444
  handle SMTLIB2.PARSE (l, msg) =>
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   445
           error ("parsing error at line " ^ string_of_int l ^ ": " ^ msg)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   446
       | Z3_PARSE (msg, t) =>
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   447
           error (msg ^ ": " ^ SMTLIB2.str_of t)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   448
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   449
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   450
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   451
(* handling of bound variables *)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   452
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   453
fun subst_of tyenv =
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   454
  let fun add (ix, (S, T)) = cons (TVar (ix, S), T)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   455
  in Vartab.fold add tyenv [] end
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   456
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   457
fun substTs_same subst = 
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   458
  let val applyT = Same.function (AList.lookup (op =) subst)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   459
  in Term_Subst.map_atypsT_same applyT end
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   460
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   461
fun subst_types ctxt env bounds t =
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   462
  let
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   463
    val match = Sign.typ_match (Proof_Context.theory_of ctxt)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   464
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   465
    val t' = singleton (Variable.polymorphic ctxt) t
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   466
    val patTs = map snd (Term.strip_qnt_vars @{const_name all} t')
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   467
    val objTs = map (the o Symtab.lookup env) bounds
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   468
    val subst = subst_of (fold match (patTs ~~ objTs) Vartab.empty)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   469
  in Same.commit (Term_Subst.map_types_same (substTs_same subst)) t' end
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   470
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   471
fun eq_quant (@{const_name HOL.All}, _) (@{const_name HOL.All}, _) = true
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   472
  | eq_quant (@{const_name HOL.Ex}, _) (@{const_name HOL.Ex}, _) = true
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   473
  | eq_quant _ _ = false
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   474
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   475
fun opp_quant (@{const_name HOL.All}, _) (@{const_name HOL.Ex}, _) = true
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   476
  | opp_quant (@{const_name HOL.Ex}, _) (@{const_name HOL.All}, _) = true
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   477
  | opp_quant _ _ = false
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   478
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   479
fun with_quant pred i (Const q1 $ Abs (_, T1, t1), Const q2 $ Abs (_, T2, t2)) =
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   480
      if pred q1 q2 andalso T1 = T2 then
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   481
        let val t = Var (("", i), T1)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   482
        in SOME (pairself Term.subst_bound ((t, t1), (t, t2))) end
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   483
      else NONE
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   484
  | with_quant _ _ _ = NONE
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   485
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   486
fun dest_quant_pair i (@{term HOL.Not} $ t1, t2) =
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   487
      Option.map (apfst HOLogic.mk_not) (with_quant opp_quant i (t1, t2))
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   488
  | dest_quant_pair i (t1, t2) = with_quant eq_quant i (t1, t2)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   489
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   490
fun dest_quant i t =
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   491
  (case dest_quant_pair i (HOLogic.dest_eq (HOLogic.dest_Trueprop t)) of
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   492
    SOME (t1, t2) => HOLogic.mk_Trueprop (HOLogic.mk_eq (t1, t2))
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   493
  | NONE => raise TERM ("lift_quant", [t]))
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   494
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   495
fun match_types ctxt pat obj =
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   496
  (Vartab.empty, Vartab.empty)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   497
  |> Pattern.first_order_match (Proof_Context.theory_of ctxt) (pat, obj)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   498
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   499
fun strip_match ctxt pat i obj =
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   500
  (case try (match_types ctxt pat) obj of
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   501
    SOME (tyenv, _) => subst_of tyenv
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   502
  | NONE => strip_match ctxt pat (i + 1) (dest_quant i obj))
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   503
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   504
fun dest_all i (Const (@{const_name all}, _) $ (a as Abs (_, T, _))) =
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   505
      dest_all (i + 1) (Term.betapply (a, Var (("", i), T)))
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   506
  | dest_all i t = (i, t)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   507
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   508
fun dest_alls t = dest_all (Term.maxidx_of_term t + 1) t
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   509
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   510
fun match_rule ctxt env (Z3_Node {bounds=bs', concl=t', ...}) bs t =
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   511
  let
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   512
    val t'' = singleton (Variable.polymorphic ctxt) t'
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   513
    val (i, obj) = dest_alls (subst_types ctxt env bs t)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   514
  in
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   515
    (case try (strip_match ctxt (snd (dest_alls t'')) i) obj of
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   516
      NONE => NONE
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   517
    | SOME subst =>
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   518
        let
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   519
          val applyT = Same.commit (substTs_same subst)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   520
          val patTs = map snd (Term.strip_qnt_vars @{const_name all} t'')
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   521
        in SOME (Symtab.make (bs' ~~ map applyT patTs)) end)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   522
  end
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   523
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   524
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   525
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   526
(* linearizing proofs and resolving types of bound variables *)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   527
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   528
fun has_step (tab, _) = Inttab.defined tab
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   529
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   530
fun add_step id rule bounds concl is_fix_step ids (tab, sts) =
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   531
  let val step = mk_step id rule ids concl bounds is_fix_step
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   532
  in (id, (Inttab.update (id, ()) tab, step :: sts)) end
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   533
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   534
fun is_fix_rule rule prems =
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   535
  member (op =) [Quant_Intro, Nnf_Pos, Nnf_Neg] rule andalso length prems = 1
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   536
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   537
fun lin_proof ctxt env (Z3_Node {id, rule, prems, concl, bounds}) steps =
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   538
  if has_step steps id then (id, steps)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   539
  else
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   540
    let
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   541
      val t = subst_types ctxt env bounds concl
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   542
      val add = add_step id rule bounds t
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   543
      fun rec_apply e b = fold_map (lin_proof ctxt e) prems #-> add b
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   544
    in
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   545
      if is_fix_rule rule prems then
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   546
        (case match_rule ctxt env (hd prems) bounds t of
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   547
          NONE => rec_apply env false steps
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   548
        | SOME env' => rec_apply env' true steps)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   549
      else rec_apply env false steps
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   550
    end
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   551
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   552
fun linearize ctxt node =
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   553
  rev (snd (snd (lin_proof ctxt Symtab.empty node (Inttab.empty, []))))
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   554
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   555
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   556
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   557
(* overall proof parser *)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   558
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   559
fun parse typs funs lines ctxt =
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   560
  let val (node, ctxt') = parse_proof typs funs lines ctxt
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   561
  in (linearize ctxt' node, ctxt') end
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   562
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   563
end