# HG changeset patch # User blanchet # Date 1281340670 -7200 # Node ID 3b708c0877ba3960bf1a6413954b5b652597c05a # Parent 1954191fc6cff5262be5c2e723f6083380919778# Parent 275064b5ebf95f906f5397733ab49f7e7cb3caff merge diff -r 1954191fc6cf -r 3b708c0877ba src/HOL/Boogie/Tools/boogie_loader.ML --- a/src/HOL/Boogie/Tools/boogie_loader.ML Mon Aug 09 09:57:38 2010 +0200 +++ b/src/HOL/Boogie/Tools/boogie_loader.ML Mon Aug 09 09:57:50 2010 +0200 @@ -341,7 +341,7 @@ in (case Scan.error (Scan.finite (stopper i) scan) ts of (x, []) => x - | (_, ts) => error (scan_err "unparsed input" ts)) + | (_, ts') => error (scan_err "unparsed input" ts')) end fun read_int' s = (case read_int (explode s) of (i, []) => SOME i | _ => NONE) @@ -499,6 +499,11 @@ mk_nary (curry HOLogic.mk_conj) @{term True} || scan_line "or" num :|-- scan_count exp >> mk_nary (curry HOLogic.mk_disj) @{term False} || + scan_line' "ite" |-- exp -- exp -- exp >> (fn ((c, t1), t2) => + let val T = Term.fastype_of t1 + in + Const (@{const_name If}, [@{typ bool}, T, T] ---> T) $ c $ t1 $ t2 + end) || binexp "implies" (binop @{term "op -->"}) || scan_line "distinct" num :|-- scan_count exp >> (fn [] => @{term True} diff -r 1954191fc6cf -r 3b708c0877ba src/HOL/Boogie/Tools/boogie_vcs.ML --- a/src/HOL/Boogie/Tools/boogie_vcs.ML Mon Aug 09 09:57:38 2010 +0200 +++ b/src/HOL/Boogie/Tools/boogie_vcs.ML Mon Aug 09 09:57:50 2010 +0200 @@ -30,6 +30,7 @@ val rewrite_vcs: (theory -> term -> term) -> (theory -> thm -> thm) -> theory -> theory + val add_assertion_filter: (term -> bool) -> theory -> theory end structure Boogie_VCs: BOOGIE_VCS = @@ -270,7 +271,33 @@ | merge _ = err_unfinished () ) -fun prep thy = vc_of_term #> (fn vc => (vc, (prop_of_vc vc, thm_of thy vc))) +fun serial_ord ((i, _), (j, _)) = int_ord (i, j) + +structure Filters = Theory_Data +( + type T = (serial * (term -> bool)) OrdList.T + val empty = [] + val extend = I + fun merge (fs1, fs2) = fold (OrdList.insert serial_ord) fs2 fs1 +) + +fun add_assertion_filter f = + Filters.map (OrdList.insert serial_ord (serial (), f)) + +fun filter_assertions thy = + let + fun filt_assert [] a = assert a + | filt_assert ((_, f) :: fs) (a as (_, t)) = + if f t then filt_assert fs a else I + + fun filt fs vc = + the_default True (prune (fn a => SOME o filt_assert fs a o filt fs) vc) + in filt (Filters.get thy) end + +fun prep thy = + vc_of_term #> + filter_assertions thy #> + (fn vc => (vc, (prop_of_vc vc, thm_of thy vc))) fun set vcs thy = VCs.map (fn NONE => SOME (Symtab.make (map (apsnd (prep thy)) vcs), K I) diff -r 1954191fc6cf -r 3b708c0877ba src/Pure/Isar/theory_target.ML --- a/src/Pure/Isar/theory_target.ML Mon Aug 09 09:57:38 2010 +0200 +++ b/src/Pure/Isar/theory_target.ML Mon Aug 09 09:57:50 2010 +0200 @@ -274,44 +274,9 @@ fun syntax_error c = error ("Illegal mixfix syntax for overloaded constant " ^ quote c); -fun declare_const (ta as Target {target, is_locale, is_class, ...}) - extra_tfrees xs ((b, T), mx) lthy = - let - val type_params = map (Logic.mk_type o TFree) extra_tfrees; - val term_params = - rev (Variable.fixes_of (Local_Theory.target_of lthy)) - |> map_filter (fn (_, x) => - (case AList.lookup (op =) xs x of - SOME T => SOME (Free (x, T)) - | NONE => NONE)); - val params = type_params @ term_params; - - val U = map Term.fastype_of params ---> T; - val (mx1, mx2, mx3) = prep_mixfix lthy ta (b, extra_tfrees) mx; - val (const, lthy') = lthy |> - (case Class_Target.instantiation_param lthy b of - SOME c' => - if mx3 <> NoSyn then syntax_error c' - else Local_Theory.theory_result (AxClass.declare_overloaded (c', U)) - ##> Class_Target.confirm_declaration b - | NONE => - (case Overloading.operation lthy b of - SOME (c', _) => - if mx3 <> NoSyn then syntax_error c' - else Local_Theory.theory_result (Overloading.declare (c', U)) - ##> Overloading.confirm b - | NONE => Local_Theory.theory_result (Sign.declare_const ((b, U), mx3)))); - val t = Term.list_comb (const, params); - in - lthy' - |> is_locale ? syntax_declaration ta false (locale_const ta Syntax.mode_default ((b, mx2), t)) - |> is_class ? class_target ta (Class_Target.declare target ((b, mx1), (type_params, t))) - |> Local_Defs.add_def ((b, NoSyn), t) - end; - in -fun define ta ((b, mx), ((name, atts), rhs)) lthy = +fun define (ta as Target {target, is_locale, is_class, ...}) ((b, mx), ((name, atts), rhs)) lthy = let val thy = ProofContext.theory_of lthy; val thy_ctxt = ProofContext.init_global thy; @@ -328,12 +293,42 @@ val extra_tfrees = rev (subtract (op =) tfreesT (Term.add_tfrees rhs [])); (*const*) - val ((lhs, local_def), lthy2) = lthy |> declare_const ta extra_tfrees xs ((b, T), mx); + val type_params = map (Logic.mk_type o TFree) extra_tfrees; + val term_params = + rev (Variable.fixes_of (Local_Theory.target_of lthy)) + |> map_filter (fn (_, x) => + (case AList.lookup (op =) xs x of + SOME T => SOME (Free (x, T)) + | NONE => NONE)); + val params = type_params @ term_params; + + val U = map Term.fastype_of params ---> T; + val (mx1, mx2, mx3) = prep_mixfix lthy ta (b, extra_tfrees) mx; + + val (const, lthy2) = lthy |> + (case Class_Target.instantiation_param lthy b of + SOME c' => + if mx3 <> NoSyn then syntax_error c' + else Local_Theory.theory_result (AxClass.declare_overloaded (c', U)) + ##> Class_Target.confirm_declaration b + | NONE => + (case Overloading.operation lthy b of + SOME (c', _) => + if mx3 <> NoSyn then syntax_error c' + else Local_Theory.theory_result (Overloading.declare (c', U)) + ##> Overloading.confirm b + | NONE => Local_Theory.theory_result (Sign.declare_const ((b, U), mx3)))); + val t = Term.list_comb (const, params); + + val ((lhs, local_def), lthy3) = lthy2 + |> is_locale ? syntax_declaration ta false (locale_const ta Syntax.mode_default ((b, mx2), t)) + |> is_class ? class_target ta (Class_Target.declare target ((b, mx1), (type_params, t))) + |> Local_Defs.add_def ((b, NoSyn), t); val (_, lhs') = Logic.dest_equals (Thm.prop_of local_def); val Const (head, _) = Term.head_of lhs'; (*def*) - val (global_def, lthy3) = lthy2 + val (global_def, lthy4) = lthy3 |> Local_Theory.theory_result (case Overloading.operation lthy b of SOME (_, checked) => Overloading.define checked name' (head, rhs') @@ -341,15 +336,15 @@ if is_some (Class_Target.instantiation_param lthy b) then AxClass.define_overloaded name' (head, rhs') else Thm.add_def false false (name', Logic.mk_equals (lhs', rhs')) #>> snd); - val def = Local_Defs.trans_terms lthy3 + val def = Local_Defs.trans_terms lthy4 [(*c == global.c xs*) local_def, (*global.c xs == rhs'*) global_def, (*rhs' == rhs*) Thm.symmetric rhs_conv]; (*note*) - val ([(res_name, [res])], lthy4) = lthy3 + val ([(res_name, [res])], lthy5) = lthy4 |> notes ta "" [((name', atts), [([def], [])])]; - in ((lhs, (res_name, res)), lthy4) end; + in ((lhs, (res_name, res)), lthy5) end; end; @@ -358,50 +353,51 @@ local -fun init_target _ NONE = global_target - | init_target thy (SOME target) = - if Locale.defined thy target - then make_target target true (Class_Target.is_class thy target) ([], [], []) [] - else error ("No such locale: " ^ quote target); - -fun init_ctxt (Target {target, is_locale, is_class, instantiation, overloading}) = +fun init_data (Target {target, is_locale, is_class, instantiation, overloading}) = if not (null (#1 instantiation)) then Class_Target.init_instantiation instantiation else if not (null overloading) then Overloading.init overloading else if not is_locale then ProofContext.init_global else if not is_class then Locale.init target else Class_Target.init target; -fun init_lthy (ta as Target {target, instantiation, overloading, ...}) = - Data.put ta #> - Local_Theory.init NONE (Long_Name.base_name target) - {pretty = pretty ta, - abbrev = abbrev ta, - define = define ta, - notes = notes ta, - declaration = declaration ta, - syntax_declaration = syntax_declaration ta, - reinit = fn lthy => init_lthy_ctxt ta (ProofContext.theory_of lthy), - exit = Local_Theory.target_of o - (if not (null (#1 instantiation)) then Class_Target.conclude_instantiation - else if not (null overloading) then Overloading.conclude - else I)} -and init_lthy_ctxt ta = init_lthy ta o init_ctxt ta; +fun init_target (ta as Target {target, instantiation, overloading, ...}) thy = + thy + |> init_data ta + |> Data.put ta + |> Local_Theory.init NONE (Long_Name.base_name target) + {pretty = pretty ta, + abbrev = abbrev ta, + define = define ta, + notes = notes ta, + declaration = declaration ta, + syntax_declaration = syntax_declaration ta, + reinit = init_target ta o ProofContext.theory_of, + exit = Local_Theory.target_of o + (if not (null (#1 instantiation)) then Class_Target.conclude_instantiation + else if not (null overloading) then Overloading.conclude + else I)}; + +fun named_target _ NONE = global_target + | named_target thy (SOME target) = + if Locale.defined thy target + then make_target target true (Class_Target.is_class thy target) ([], [], []) [] + else error ("No such locale: " ^ quote target); fun gen_overloading prep_const raw_ops thy = let val ctxt = ProofContext.init_global thy; val ops = raw_ops |> map (fn (name, const, checked) => (name, Term.dest_Const (prep_const ctxt const), checked)); - in thy |> init_lthy_ctxt (make_target "" false false ([], [], []) ops) end; + in thy |> init_target (make_target "" false false ([], [], []) ops) end; in -fun init target thy = init_lthy_ctxt (init_target thy target) thy; +fun init target thy = init_target (named_target thy target) thy; fun context_cmd "-" thy = init NONE thy | context_cmd target thy = init (SOME (Locale.intern thy target)) thy; -fun instantiation arities = init_lthy_ctxt (make_target "" false false arities []); +fun instantiation arities = init_target (make_target "" false false arities []); fun instantiation_cmd arities thy = instantiation (Class_Target.read_multi_arity thy arities) thy; val overloading = gen_overloading (fn ctxt => Syntax.check_term ctxt o Const);