# HG changeset patch # User boehmes # Date 1260173536 -3600 # Node ID 2b3f4fcbc066007eb431a01fe1e148b955eb01d5 # Parent ac78f5cdc4307720e0c1b420ef23a73bfe4420ac verbose output of loaded data makes a clear distinction between new and already existing data (types, constants, axioms) diff -r ac78f5cdc430 -r 2b3f4fcbc066 src/HOL/Boogie/Tools/boogie_loader.ML --- a/src/HOL/Boogie/Tools/boogie_loader.ML Thu Dec 03 15:56:06 2009 +0100 +++ b/src/HOL/Boogie/Tools/boogie_loader.ML Mon Dec 07 09:12:16 2009 +0100 @@ -12,10 +12,10 @@ structure Boogie_Loader: BOOGIE_LOADER = struct -fun log verbose text args thy = - if verbose - then (Pretty.writeln (Pretty.big_list text (map Pretty.str args)); thy) - else thy +fun log verbose text args x = + if verbose andalso not (null args) + then (Pretty.writeln (Pretty.big_list text (map Pretty.str args)); x) + else x val isabelle_name = let @@ -35,7 +35,7 @@ fun label_name line col = "L_" ^ string_of_int line ^ "_" ^ string_of_int col -datatype attribute_value = StringValue of string | TermValue of Term.term +datatype attribute_value = StringValue of string | TermValue of term @@ -51,27 +51,28 @@ else NONE end + fun log_new bname name = bname ^ " (as " ^ name ^ ")" + fun log_ex bname name = "[" ^ bname ^ " has already been declared as " ^ + name ^ "]" + fun declare (name, arity) thy = let val isa_name = isabelle_name name in (case lookup_type_name thy isa_name arity of - SOME type_name => ((type_name, false), thy) + SOME type_name => (((name, type_name), log_ex name type_name), thy) | NONE => let val args = Name.variant_list [] (replicate arity "'") val (T, thy') = ObjectLogic.typedecl (Binding.name isa_name, args, NoSyn) thy val type_name = fst (Term.dest_Type T) - in ((type_name, true), thy') end) + in (((name, type_name), log_new name type_name), thy') end) end - - fun type_names ((name, _), (new_name, new)) = - if new then SOME (new_name ^ " (was " ^ name ^ ")") else NONE in fun declare_types verbose tys = - fold_map declare tys #-> (fn tds => - log verbose "Declared types:" (map_filter type_names (tys ~~ tds)) #> - rpair (Symtab.make (map fst tys ~~ map fst tds))) + fold_map declare tys #>> split_list #-> (fn (tds, logs) => + log verbose "Declared types:" logs #> + rpair (Symtab.make tds)) end @@ -146,23 +147,26 @@ else NONE end - fun declare (name, ((Ts, T), atts)) thy = - let val isa_name = isabelle_name name and U = Ts ---> T - in - (case lookup_const thy isa_name U of - SOME t => (((name, t), false), thy) - | NONE => - (case maybe_builtin U atts of - SOME t => (((name, t), false), thy) - | NONE => - thy - |> Sign.declare_const ((Binding.name isa_name, U), - mk_syntax name (length Ts)) - |> apfst (rpair true o pair name))) - end + fun log_term thy t = Syntax.string_of_term_global thy t + fun log_new thy name t = name ^ " (as " ^ log_term thy t ^ ")" + fun log_ex thy name t = "[" ^ name ^ " has already been declared as " ^ + log_term thy t ^ "]" + fun log_builtin thy name t = "[" ^ name ^ " has been identified as " ^ + log_term thy t ^ "]" - fun new_names ((name, t), new) = - if new then SOME (fst (Term.dest_Const t) ^ " (as " ^ name ^ ")") else NONE + fun declare' name isa_name T arity atts thy = + (case lookup_const thy isa_name T of + SOME t => (((name, t), log_ex thy name t), thy) + | NONE => + (case maybe_builtin T atts of + SOME t => (((name, t), log_builtin thy name t), thy) + | NONE => + thy + |> Sign.declare_const ((Binding.name isa_name, T), + mk_syntax name arity) + |> (fn (t, thy') => (((name, t), log_new thy' name t), thy')))) + fun declare (name, ((Ts, T), atts)) = + declare' name (isabelle_name name) (Ts ---> T) (length Ts) atts fun uniques fns fds = let @@ -182,9 +186,9 @@ end in fun declare_functions verbose fns = - fold_map declare fns #-> (fn fds => - log verbose "Declared constants:" (map_filter new_names fds) #> - rpair (` (uniques fns) (Symtab.make (map fst fds)))) + fold_map declare fns #>> split_list #-> (fn (fds, logs) => + log verbose "Loaded constants:" logs #> + rpair (` (uniques fns) (Symtab.make fds))) end @@ -194,17 +198,41 @@ let fun mk_name idx = "axiom_" ^ string_of_int (idx + 1) in map_index (fn (idx, t) => (mk_name idx, HOLogic.mk_Trueprop t)) axs end - fun only_new_boogie_axioms thy = - let val baxs = map Thm.prop_of (Boogie_Axioms.get (ProofContext.init thy)) - in filter_out (member (op aconv) baxs o snd) end + datatype kind = Unused of thm | Used of thm | New of string + + fun mark (name, t) axs = + (case Termtab.lookup axs t of + SOME (Unused thm) => Termtab.update (t, Used thm) axs + | NONE => Termtab.update (t, New name) axs + | SOME _ => axs) + + val sort_fst_str = sort (prod_ord fast_string_ord (K EQUAL)) + fun split_list_kind thy axs = + let + fun split (_, Used thm) (used, new) = (thm :: used, new) + | split (t, New name) (used, new) = (used, (name, t) :: new) + | split (t, Unused thm) (used, new) = + (warning (Pretty.str_of + (Pretty.big_list "This background axiom has not been loaded:" + [Display.pretty_thm_global thy thm])); + (used, new)) + in apsnd sort_fst_str (fold split axs ([], [])) end + + fun mark_axioms thy axs = + Boogie_Axioms.get (ProofContext.init thy) + |> Termtab.make o map (fn thm => (Thm.prop_of thm, Unused thm)) + |> fold mark axs + |> split_list_kind thy o Termtab.dest in fun add_axioms verbose axs thy = - let val axs' = only_new_boogie_axioms thy (name_axioms axs) + let val (used, new) = mark_axioms thy (name_axioms axs) in thy - |> PureThy.add_axioms (map (rpair [] o apfst Binding.name) axs') + |> PureThy.add_axioms (map (rpair [] o apfst Binding.name) new) |-> Context.theory_map o fold Boogie_Axioms.add_thm - |> log verbose "The following axioms were added:" (map fst axs') + |> log verbose "The following axioms were added:" (map fst new) + |> (fn thy' => log verbose "The following axioms already existed:" + (map (Display.string_of_thm_global thy') used) thy') |> Context.theory_map (fn context => fold Split_VC_SMT_Rules.add_thm (Boogie_Axioms.get (Context.proof_of context)) context) end