--- a/src/HOL/Tools/SMT/z3_proof_parser.ML Wed May 12 23:54:02 2010 +0200
+++ b/src/HOL/Tools/SMT/z3_proof_parser.ML Wed May 12 23:54:04 2010 +0200
@@ -29,6 +29,10 @@
structure Z3_Proof_Parser: Z3_PROOF_PARSER =
struct
+structure I = Z3_Interface
+
+
+
(** proof rules **)
datatype rule = TrueAxiom | Asserted | Goal | ModusPonens | Reflexivity |
@@ -87,16 +91,15 @@
(** certified terms and variables **)
-val (var_prefix, decl_prefix) = ("v", "sk") (* must be distinct *)
+val (var_prefix, decl_prefix) = ("v", "sk")
+(* "decl_prefix" is for skolem constants (represented by free variables)
+ "var_prefix" is for pseudo-schematic variables (schematic with respect
+ to the Z3 proof, but represented by free variables)
-fun instTs cUs (cTs, ct) = Thm.instantiate_cterm (cTs ~~ cUs, []) ct
-fun instT cU (cT, ct) = instTs [cU] ([cT], ct)
-fun mk_inst_pair destT cpat = (destT (Thm.ctyp_of_term cpat), cpat)
-val destT1 = hd o Thm.dest_ctyp
-val destT2 = hd o tl o Thm.dest_ctyp
-
-fun ctyp_of (ct, _) = Thm.ctyp_of_term ct
-fun instT' t = instT (ctyp_of t)
+ Both prefixes must be distinct to avoid name interferences.
+ More precisely, the naming of pseudo-schematic variables must be
+ context-independent modulo the current proof context to be able to
+ use fast inference kernel rules during proof reconstruction. *)
fun certify ctxt = Thm.cterm_of (ProofContext.theory_of ctxt)
@@ -128,12 +131,11 @@
(case AList.lookup (op =) vars 0 of
SOME cv => cv
| _ => Thm.cterm_of thy (Var ((Name.uu, maxidx_of ct + 1), T)))
- val cq = instT (Thm.ctyp_of_term cv) q
fun dec (i, v) = if i = 0 then NONE else SOME (i-1, v)
- in (Thm.capply cq (Thm.cabs cv ct), map_filter dec vars) end
+ in (Thm.capply (I.instT' cv q) (Thm.cabs cv ct), map_filter dec vars) end
- val forall = mk_inst_pair (destT1 o destT1) @{cpat All}
- val exists = mk_inst_pair (destT1 o destT1) @{cpat Ex}
+ val forall = I.mk_inst_pair (I.destT1 o I.destT1) @{cpat All}
+ val exists = I.mk_inst_pair (I.destT1 o I.destT1) @{cpat Ex}
in
fun mk_forall thy = fold_rev (mk_quant thy forall)
fun mk_exists thy = fold_rev (mk_quant thy exists)
@@ -143,118 +145,29 @@
local
fun equal_var cv (_, cu) = (cv aconvc cu)
- fun apply (ct2, vars2) (ct1, vars1) =
+ fun prep (ct, vars) (maxidx, all_vars) =
let
- val incr = Thm.incr_indexes_cterm (maxidx_of ct1 + maxidx_of ct2 + 2)
+ val maxidx' = maxidx_of ct + maxidx + 1
fun part (v as (i, cv)) =
- (case AList.lookup (op =) vars1 i of
+ (case AList.lookup (op =) all_vars i of
SOME cu => apfst (if cu aconvc cv then I else cons (cv, cu))
| NONE =>
- if not (exists (equal_var cv) vars1) then apsnd (cons v)
+ if not (exists (equal_var cv) all_vars) then apsnd (cons v)
else
- let val cv' = incr cv
+ let val cv' = Thm.incr_indexes_cterm maxidx' cv
in apfst (cons (cv, cv')) #> apsnd (cons (i, cv')) end)
- val (ct2', vars2') =
- if null vars1 then (ct2, vars2)
- else fold part vars2 ([], [])
- |>> (fn inst => Thm.instantiate_cterm ([], inst) ct2)
-
- in (Thm.capply ct1 ct2', vars1 @ vars2') end
-in
-fun mk_fun ct ts = fold apply ts (ct, [])
-fun mk_binop f t u = mk_fun f [t, u]
-fun mk_nary _ e [] = e
- | mk_nary ct _ es = uncurry (fold_rev (mk_binop ct)) (split_last es)
-end
-
-
-val mk_true = mk_fun @{cterm "~False"} []
-val mk_false = mk_fun @{cterm "False"} []
-fun mk_not t = mk_fun @{cterm Not} [t]
-val mk_imp = mk_binop @{cterm "op -->"}
-val mk_iff = mk_binop @{cterm "op = :: bool => _"}
-
-val eq = mk_inst_pair destT1 @{cpat "op ="}
-fun mk_eq t u = mk_binop (instT' t eq) t u
-
-val if_term = mk_inst_pair (destT1 o destT2) @{cpat If}
-fun mk_if c t u = mk_fun (instT' t if_term) [c, t, u]
-
-val nil_term = mk_inst_pair destT1 @{cpat Nil}
-val cons_term = mk_inst_pair destT1 @{cpat Cons}
-fun mk_list cT es =
- fold_rev (mk_binop (instT cT cons_term)) es (mk_fun (instT cT nil_term) [])
-
-val distinct = mk_inst_pair (destT1 o destT1) @{cpat distinct}
-fun mk_distinct [] = mk_true
- | mk_distinct (es as (e :: _)) =
- mk_fun (instT' e distinct) [mk_list (ctyp_of e) es]
-
-
-(* arithmetic *)
-
-fun mk_int_num i = mk_fun (Numeral.mk_cnumber @{ctyp int} i) []
-fun mk_real_num i = mk_fun (Numeral.mk_cnumber @{ctyp real} i) []
-fun mk_real_frac_num (e, NONE) = mk_real_num e
- | mk_real_frac_num (e, SOME d) =
- mk_binop @{cterm "op / :: real => _"} (mk_real_num e) (mk_real_num d)
-
-fun has_int_type e = (Thm.typ_of (ctyp_of e) = @{typ int})
-fun choose e i r = if has_int_type e then i else r
+ val (inst, vars') =
+ if null vars then ([], vars)
+ else fold part vars ([], [])
-val uminus_i = @{cterm "uminus :: int => _"}
-val uminus_r = @{cterm "uminus :: real => _"}
-fun mk_uminus e = mk_fun (choose e uminus_i uminus_r) [e]
-
-fun arith_op int_op real_op t u = mk_binop (choose t int_op real_op) t u
-
-val mk_add = arith_op @{cterm "op + :: int => _"} @{cterm "op + :: real => _"}
-val mk_sub = arith_op @{cterm "op - :: int => _"} @{cterm "op - :: real => _"}
-val mk_mul = arith_op @{cterm "op * :: int => _"} @{cterm "op * :: real => _"}
-val mk_int_div = mk_binop @{cterm "op div :: int => _"}
-val mk_real_div = mk_binop @{cterm "op / :: real => _"}
-val mk_mod = mk_binop @{cterm "op mod :: int => _"}
-val mk_lt = arith_op @{cterm "op < :: int => _"} @{cterm "op < :: real => _"}
-val mk_le = arith_op @{cterm "op <= :: int => _"} @{cterm "op <= :: real => _"}
-
-
-(* arrays *)
-
-val access = mk_inst_pair (Thm.dest_ctyp o destT1) @{cpat apply}
-fun mk_access array index =
- let val cTs = Thm.dest_ctyp (ctyp_of array)
- in mk_fun (instTs cTs access) [array, index] end
-
-val update = mk_inst_pair (Thm.dest_ctyp o destT1) @{cpat fun_upd}
-fun mk_update array index value =
- let val cTs = Thm.dest_ctyp (ctyp_of array)
- in mk_fun (instTs cTs update) [array, index, value] end
-
-
-(* bitvectors *)
-
-fun mk_binT size =
- let
- fun bitT i T =
- if i = 0
- then Type (@{type_name "Numeral_Type.bit0"}, [T])
- else Type (@{type_name "Numeral_Type.bit1"}, [T])
-
- fun binT i =
- if i = 0 then @{typ "Numeral_Type.num0"}
- else if i = 1 then @{typ "Numeral_Type.num1"}
- else let val (q, r) = Integer.div_mod i 2 in bitT r (binT q) end
- in
- if size >= 0 then binT size
- else raise TYPE ("mk_binT: " ^ string_of_int size, [], [])
- end
-
-fun mk_wordT size = Type (@{type_name "word"}, [mk_binT size])
-
-fun mk_bv_num thy (num, size) =
- mk_fun (Numeral.mk_cnumber (Thm.ctyp_of thy (mk_wordT size)) num) []
+ in (Thm.instantiate_cterm ([], inst) ct, (maxidx', vars' @ all_vars)) end
+in
+fun mk_fun f ts =
+ let val (cts, (_, vars)) = fold_map prep ts (~1, [])
+ in f cts |> Option.map (rpair vars) end
+end
@@ -277,6 +190,7 @@
fun cert @{term True} = @{cterm "~False"}
| cert t = certify ctxt' t
+
in (typs, Symtab.map cert terms, Inttab.empty, Inttab.empty, [], ctxt') end
fun fresh_name n (typs, terms, exprs, steps, vars, ctxt) =
@@ -285,14 +199,6 @@
fun theory_of (_, _, _, _, _, ctxt) = ProofContext.theory_of ctxt
-fun typ_of_sort n (cx as (typs, _, _, _, _, _)) =
- (case Symtab.lookup typs n of
- SOME T => (T, cx)
- | NONE => cx
- |> fresh_name ("'" ^ n) |>> TFree o rpair @{sort type}
- |> (fn (T, (typs, terms, exprs, steps, vars, ctxt)) =>
- (T, (Symtab.update (n, T) typs, terms, exprs, steps, vars, ctxt))))
-
fun add_decl (n, T) (cx as (_, terms, _, _, _, _)) =
(case Symtab.lookup terms n of
SOME _ => cx
@@ -301,36 +207,20 @@
let val upd = Symtab.update (n, certify ctxt (Free (m, T)))
in (typs, upd terms, exprs, steps, vars, ctxt) end))
-datatype sym = Sym of string * sym list
+fun mk_typ (typs, _, _, _, _, ctxt) (s as I.Sym (n, _)) =
+ (case I.mk_builtin_typ ctxt s of
+ SOME T => SOME T
+ | NONE => Symtab.lookup typs n)
-fun mk_app _ (Sym ("true", _), _) = SOME mk_true
- | mk_app _ (Sym ("false", _), _) = SOME mk_false
- | mk_app _ (Sym ("=", _), [t, u]) = SOME (mk_eq t u)
- | mk_app _ (Sym ("distinct", _), ts) = SOME (mk_distinct ts)
- | mk_app _ (Sym ("ite", _), [s, t, u]) = SOME (mk_if s t u)
- | mk_app _ (Sym ("and", _), ts) = SOME (mk_nary @{cterm "op &"} mk_true ts)
- | mk_app _ (Sym ("or", _), ts) = SOME (mk_nary @{cterm "op |"} mk_false ts)
- | mk_app _ (Sym ("iff", _), [t, u]) = SOME (mk_iff t u)
- | mk_app _ (Sym ("xor", _), [t, u]) = SOME (mk_not (mk_iff t u))
- | mk_app _ (Sym ("not", _), [t]) = SOME (mk_not t)
- | mk_app _ (Sym ("implies", _), [t, u]) = SOME (mk_imp t u)
- | mk_app _ (Sym ("~", _), [t, u]) = SOME (mk_iff t u)
- | mk_app _ (Sym ("<", _), [t, u]) = SOME (mk_lt t u)
- | mk_app _ (Sym ("<=", _), [t, u]) = SOME (mk_le t u)
- | mk_app _ (Sym (">", _), [t, u]) = SOME (mk_lt u t)
- | mk_app _ (Sym (">=", _), [t, u]) = SOME (mk_le u t)
- | mk_app _ (Sym ("+", _), [t, u]) = SOME (mk_add t u)
- | mk_app _ (Sym ("-", _), [t, u]) = SOME (mk_sub t u)
- | mk_app _ (Sym ("-", _), [t]) = SOME (mk_uminus t)
- | mk_app _ (Sym ("*", _), [t, u]) = SOME (mk_mul t u)
- | mk_app _ (Sym ("/", _), [t, u]) = SOME (mk_real_div t u)
- | mk_app _ (Sym ("div", _), [t, u]) = SOME (mk_int_div t u)
- | mk_app _ (Sym ("mod", _), [t, u]) = SOME (mk_mod t u)
- | mk_app _ (Sym ("select", _), [m, k]) = SOME (mk_access m k)
- | mk_app _ (Sym ("store", _), [m, k, v]) = SOME (mk_update m k v)
- | mk_app _ (Sym ("pattern", _), _) = SOME mk_true
- | mk_app (_, terms, _, _, _, _) (Sym (n, _), ts) =
- Symtab.lookup terms n |> Option.map (fn ct => mk_fun ct ts)
+fun mk_num (_, _, _, _, _, ctxt) (i, T) =
+ mk_fun (K (I.mk_builtin_num ctxt i T)) []
+
+fun mk_app (_, terms, _, _, _, ctxt) (s as I.Sym (n, _), es) =
+ mk_fun (fn cts =>
+ (case I.mk_builtin_fun ctxt s cts of
+ SOME ct => SOME ct
+ | NONE =>
+ Symtab.lookup terms n |> Option.map (Drule.list_comb o rpair cts))) es
fun add_expr k t (typs, terms, exprs, steps, vars, ctxt) =
(typs, terms, Inttab.update (k, t) exprs, steps, vars, ctxt)
@@ -395,8 +285,9 @@
"4" => SOME 4 | "5" => SOME 5 | "6" => SOME 6 | "7" => SOME 7 |
"8" => SOME 8 | "9" => SOME 9 | _ => NONE)
-fun mk_num ds = fold (fn d => fn i => i * 10 + d) ds 0
-val nat_num = Scan.lift (Scan.repeat1 (Scan.some digit)) >> mk_num
+val digits = Scan.lift (Scan.many1 Symbol.is_ascii_digit) >> implode
+val nat_num = Scan.lift (Scan.repeat1 (Scan.some digit)) >> (fn ds =>
+ fold (fn d => fn i => i * 10 + d) ds 0)
val int_num = Scan.optional ($$ "-" >> K (fn i => ~i)) I :|--
(fn sign => nat_num >> sign)
@@ -404,7 +295,8 @@
member (op =) (explode "_+*-/%~=<>$&|?!.@^#")
val name = Scan.lift (Scan.many1 is_char) >> implode
-fun sym st = (name -- Scan.optional (bra (seps_by ($$ ":") sym)) [] >> Sym) st
+fun sym st =
+ (name -- Scan.optional (bra (seps_by ($$ ":") sym)) [] >> I.Sym) st
fun id st = ($$ "#" |-- nat_num) st
@@ -412,29 +304,40 @@
(* parsers for various parts of Z3 proofs *)
fun sort st = Scan.first [
- this "bool" >> K @{typ bool},
- this "int" >> K @{typ int},
- this "real" >> K @{typ real},
- this "bv" |-- bra nat_num >> mk_wordT,
this "array" |-- bra (sort --| $$ ":" -- sort) >> (op -->),
par (this "->" |-- seps1 sort) >> ((op --->) o split_last),
- name :|-- with_context typ_of_sort] st
+ sym :|-- (fn s as I.Sym (n, _) => lookup_context mk_typ s :|-- (fn
+ SOME T => Scan.succeed T
+ | NONE => scan_exn ("unknown sort: " ^ quote n)))] st
fun bound st = (par (this ":var" |-- sep nat_num -- sep sort) :|--
lookup_context (mk_bound o theory_of)) st
-fun number st = st |> (
- int_num -- Scan.option ($$ "/" |-- int_num) --| this "::" :|--
- (fn num as (n, _) =>
- this "int" >> K (mk_int_num n) ||
- this "real" >> K (mk_real_frac_num num)))
+fun numb (n as (i, _)) = lookup_context mk_num n :|-- (fn
+ SOME n' => Scan.succeed n'
+ | NONE => scan_exn ("unknown number: " ^ quote (string_of_int i)))
+
+fun appl (app as (I.Sym (n, _), _)) = lookup_context mk_app app :|-- (fn
+ SOME app' => Scan.succeed app'
+ | NONE => scan_exn ("unknown function symbol: " ^ quote n))
+
+fun bv_size st = (digits >> (fn sz => I.Sym ("bv", [I.Sym (sz, [])]))) st
-fun bv_number st = (this "bv" |-- bra (nat_num --| $$ ":" -- nat_num) :|--
- lookup_context (mk_bv_num o theory_of)) st
+fun bv_number_sort st = (bv_size :|-- lookup_context mk_typ :|-- (fn
+ SOME cT => Scan.succeed cT
+ | NONE => scan_exn ("unknown sort: " ^ quote "bv"))) st
+
+fun bv_number st =
+ (this "bv" |-- bra (nat_num --| $$ ":" -- bv_number_sort) :|-- numb) st
-fun appl (app as (Sym (n, _), _)) = lookup_context mk_app app :|-- (fn
- SOME app' => Scan.succeed app'
- | NONE => scan_exn ("unknown function: " ^ quote n))
+fun frac_number st = (
+ int_num --| $$ "/" -- int_num --| this "::" -- sort :|-- (fn ((i, j), T) =>
+ numb (i, T) -- numb (j, T) :|-- (fn (n, m) =>
+ appl (I.Sym ("/", []), [n, m])))) st
+
+fun plain_number st = (int_num --| this "::" -- sort :|-- numb) st
+
+fun number st = Scan.first [bv_number, frac_number, plain_number] st
fun constant st = ((sym >> rpair []) :|-- appl) st
@@ -442,24 +345,27 @@
SOME e => Scan.succeed e
| NONE => scan_exn ("unknown term id: " ^ quote (string_of_int i))))) st
-fun arg st = Scan.first [expr_id, number, bv_number, constant] st
+fun arg st = Scan.first [expr_id, number, constant] st
fun application st = par ((sym -- Scan.repeat1 (sep arg)) :|-- appl) st
fun variables st = par (this "vars" |-- seps1 (par (name |-- sep sort))) st
-fun patterns st = seps (par ((this ":pat" || this ":nopat") |-- seps1 id)) st
+fun pats st = seps (par ((this ":pat" || this ":nopat") |-- seps1 id)) st
+
+fun pattern st = par (this "pattern" |-- Scan.repeat1 (sep arg) >>
+ (the o mk_fun (K (SOME @{cterm True})))) st
fun quant_kind st = st |> (
this "forall" >> K (mk_forall o theory_of) ||
this "exists" >> K (mk_exists o theory_of))
fun quantifier st =
- (par (quant_kind -- sep variables --| patterns -- sep arg) :|--
+ (par (quant_kind -- sep variables --| pats -- sep arg) :|--
lookup_context (fn cx => fn ((mk_q, Ts), body) => mk_q cx Ts body)) st
fun expr k =
- Scan.first [bound, quantifier, application, number, bv_number, constant] :|--
+ Scan.first [bound, quantifier, pattern, application, number, constant] :|--
with_context (pair NONE oo add_expr k)
fun rule_name st = ((name >> `(Symtab.lookup rule_names)) :|-- (fn