diff --git a/thys/Isabelle_Meta_Model/toy_example/embedding/Generator_dynamic_sequential.thy b/thys/Isabelle_Meta_Model/toy_example/embedding/Generator_dynamic_sequential.thy --- a/thys/Isabelle_Meta_Model/toy_example/embedding/Generator_dynamic_sequential.thy +++ b/thys/Isabelle_Meta_Model/toy_example/embedding/Generator_dynamic_sequential.thy @@ -1,1716 +1,1717 @@ (****************************************************************************** * Citadelle * * Copyright (c) 2011-2018 Université Paris-Saclay, Univ. Paris-Sud, France * 2013-2017 IRT SystemX, France * 2011-2015 Achim D. Brucker, Germany * 2016-2018 The University of Sheffield, UK * 2016-2017 Nanyang Technological University, Singapore * 2017-2018 Virginia Tech, USA * * All rights reserved. * * Redistribution and use in source and binary forms, with or without * modification, are permitted provided that the following conditions are * met: * * * Redistributions of source code must retain the above copyright * notice, this list of conditions and the following disclaimer. * * * Redistributions in binary form must reproduce the above * copyright notice, this list of conditions and the following * disclaimer in the documentation and/or other materials provided * with the distribution. * * * Neither the name of the copyright holders nor the names of its * contributors may be used to endorse or promote products derived * from this software without specific prior written permission. * * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS * "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT * LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR * A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT * OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, * SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT * LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, * DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY * THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT * (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. ******************************************************************************) section\Dynamic Meta Embedding with Reflection\ theory Generator_dynamic_sequential imports Printer "../../isabelle_home/src/HOL/Isabelle_Main2" (*<*) keywords (* Toy language *) "Between" "Attributes" "Operations" "Constraints" "Role" "Ordered" "Subsets" "Union" "Redefines" "Derived" "Qualifier" "Existential" "Inv" "Pre" "Post" "self" "Nonunique" "Sequence_" (* Isabelle syntax *) "output_directory" "THEORY" "IMPORTS" "SECTION" "SORRY" "no_dirty" "deep" "shallow" "syntax_print" "skip_export" "generation_semantics" "flush_all" (* Isabelle semantics (parameterizing the semantics of Toy language) *) "design" "analysis" "oid_start" and (* Toy language *) "Enum" "Abstract_class" "Class" "Association" "Composition" "Aggregation" "Abstract_associationclass" "Associationclass" "Context" "End" "Instance" "BaseType" "State" "PrePost" (* Isabelle syntax *) "generation_syntax" :: thy_decl (*>*) begin text\In the ``dynamic'' solution: the exportation is automatically handled inside Isabelle/jEdit. Inputs are provided using the syntax of the Toy Language, and in output we basically have two options: \begin{itemize} \item The first is to generate an Isabelle file for inspection or debugging. The generated file can interactively be loaded in Isabelle/jEdit, or saved to the hard disk. This mode is called the ``deep exportation'' mode or shortly the ``deep'' mode. The aim is to maximally automate the process one is manually performing in @{file \Generator_static.thy\}. \item On the other hand, it is also possible to directly execute in Isabelle/jEdit the generated file from the random access memory. This mode corresponds to the ``shallow reflection'' mode or shortly ``shallow'' mode. \end{itemize} In both modes, the reflection is necessary since the main part used by both was defined at Isabelle side. As a consequence, experimentations in ``deep'' and ``shallow'' are performed without leaving the editing session, in the same as the one the meta-compiler is actually running.\ apply_code_printing_reflect \ val stdout_file = Unsynchronized.ref "" \ text\This variable is not used in this theory (only in @{file \Generator_static.thy\}), but needed for well typechecking the reflected SML code.\ code_reflect' open META functions (* executing the compiler as monadic combinators for deep and shallow *) fold_thy_deep fold_thy_shallow (* printing the HOL AST to (shallow Isabelle) string *) write_file (* manipulating the compiling environment *) compiler_env_config_reset_all compiler_env_config_update oidInit D_output_header_thy_update map2_ctxt_term check_export_code (* printing the TOY AST to (deep Isabelle) string *) isabelle_apply isabelle_of_compiler_env_config subsection\Interface Between the Reflected and the Native\ ML\ val To_string0 = META.meta_of_logic \ ML\ structure From = struct val string = META.SS_base o META.ST val binding = string o Binding.name_of (*fun term ctxt s = string (XML.content_of (YXML.parse_body (Syntax.string_of_term ctxt s)))*) val internal_oid = META.Oid o Code_Numeral.natural_of_integer val option = Option.map val list = List.map fun pair f1 f2 (x, y) = (f1 x, f2 y) fun pair3 f1 f2 f3 (x, y, z) = (f1 x, f2 y, f3 z) structure Pure = struct val indexname = pair string Code_Numeral.natural_of_integer val class = string val sort = list class fun typ e = (fn Type (s, l) => (META.Type o pair string (list typ)) (s, l) | TFree (s, s0) => (META.TFree o pair string sort) (s, s0) | TVar (i, s0) => (META.TVar o pair indexname sort) (i, s0) ) e fun term e = (fn Const (s, t) => (META.Const o pair string typ) (s, t) | Free (s, t) => (META.Free o pair string typ) (s, t) | Var (i, t) => (META.Var o pair indexname typ) (i, t) | Bound i => (META.Bound o Code_Numeral.natural_of_integer) i | Abs (s, ty, t) => (META.Abs o pair3 string typ term) (s, ty, t) | op $ (term1, term2) => (META.App o pair term term) (term1, term2) ) e end fun toy_ctxt_term thy expr = META.T_pure (Pure.term (Syntax.read_term (Proof_Context.init_global thy) expr)) end \ ML\fun List_mapi f = META.mapi (f o Code_Numeral.integer_of_natural)\ ML\ structure Ty' = struct fun check l_oid l = let val Mp = META.map_prod val Me = String.explode val Mi = String.implode val Ml = map in META.check_export_code (writeln o Mi) (warning o Mi) (fn s => writeln (Markup.markup (Markup.bad ()) (Mi s))) (error o To_string0) (Ml (Mp I Me) l_oid) ((META.SS_base o META.ST) l) end end \ subsection\Binding of the Reflected API to the Native API\ ML\ structure META_overload = struct val of_semi__typ = META.of_semi_typ To_string0 val of_semi__term = META.of_semi_terma To_string0 val of_semi__term' = META.of_semi_term To_string0 val fold = fold end \ ML\ structure Bind_Isabelle = struct fun To_binding s = Binding.make (s, Position.none) val To_sbinding = To_binding o To_string0 fun semi__method_simp g f = Method.Basic (fn ctxt => SIMPLE_METHOD (g (asm_full_simp_tac (f ctxt)))) val semi__method_simp_one = semi__method_simp (fn f => f 1) val semi__method_simp_all = semi__method_simp (CHANGED_PROP o PARALLEL_ALLGOALS) datatype semi__thm' = Thms_single' of thm | Thms_mult' of thm list fun semi__thm_attribute ctxt = let open META open META_overload val S = fn Thms_single' t => t val M = fn Thms_mult' t => t in fn Thm_thm s => Thms_single' (Proof_Context.get_thm ctxt (To_string0 s)) | Thm_thms s => Thms_mult' (Proof_Context.get_thms ctxt (To_string0 s)) | Thm_THEN (e1, e2) => (case (semi__thm_attribute ctxt e1, semi__thm_attribute ctxt e2) of (Thms_single' e1, Thms_single' e2) => Thms_single' (e1 RSN (1, e2)) | (Thms_mult' e1, Thms_mult' e2) => Thms_mult' (e1 RLN (1, e2))) | Thm_simplified (e1, e2) => Thms_single' (asm_full_simplify (clear_simpset ctxt addsimps [S (semi__thm_attribute ctxt e2)]) (S (semi__thm_attribute ctxt e1))) | Thm_OF (e1, e2) => Thms_single' ([S (semi__thm_attribute ctxt e2)] MRS (S (semi__thm_attribute ctxt e1))) | Thm_where (nth, l) => Thms_single' (Rule_Insts.where_rule ctxt (List.map (fn (var, expr) => (((To_string0 var, 0), Position.none), of_semi__term expr)) l) [] (S (semi__thm_attribute ctxt nth))) | Thm_symmetric e1 => let val e2 = S (semi__thm_attribute ctxt (Thm_thm (From.string "sym"))) in case semi__thm_attribute ctxt e1 of Thms_single' e1 => Thms_single' (e1 RSN (1, e2)) | Thms_mult' e1 => Thms_mult' (e1 RLN (1, [e2])) end | Thm_of (nth, l) => Thms_single' (Rule_Insts.of_rule ctxt (List.map (SOME o of_semi__term) l, []) [] (S (semi__thm_attribute ctxt nth))) end fun semi__thm_attribute_single ctxt s = case (semi__thm_attribute ctxt s) of Thms_single' t => t fun semi__thm_mult ctxt = let fun f thy = case (semi__thm_attribute ctxt thy) of Thms_mult' t => t | Thms_single' t => [t] in fn META.Thms_single thy => f thy | META.Thms_mult thy => f thy end fun semi__thm_mult_l ctxt l = List.concat (map (semi__thm_mult ctxt) l) fun semi__method_simp_only l ctxt = clear_simpset ctxt addsimps (semi__thm_mult_l ctxt l) fun semi__method_simp_add_del_split (l_add, l_del, l_split) ctxt = fold Splitter.add_split (semi__thm_mult_l ctxt l_split) (ctxt addsimps (semi__thm_mult_l ctxt l_add) delsimps (semi__thm_mult_l ctxt l_del)) fun semi__method expr = let open META open Method open META_overload in case expr of Method_rule o_s => Basic (fn ctxt => METHOD (HEADGOAL o Classical.rule_tac ctxt (case o_s of NONE => [] | SOME s => [semi__thm_attribute_single ctxt s]))) | Method_drule s => Basic (fn ctxt => drule ctxt 0 [semi__thm_attribute_single ctxt s]) | Method_erule s => Basic (fn ctxt => erule ctxt 0 [semi__thm_attribute_single ctxt s]) | Method_elim s => Basic (fn ctxt => elim ctxt [semi__thm_attribute_single ctxt s]) | Method_intro l => Basic (fn ctxt => intro ctxt (map (semi__thm_attribute_single ctxt) l)) | Method_subst (asm, l, s) => Basic (fn ctxt => SIMPLE_METHOD' ((if asm then EqSubst.eqsubst_asm_tac else EqSubst.eqsubst_tac) ctxt (map (fn s => case Int.fromString (To_string0 s) of SOME i => i) l) [semi__thm_attribute_single ctxt s])) | Method_insert l => Basic (fn ctxt => insert (semi__thm_mult_l ctxt l)) | Method_plus t => Combinator ( no_combinator_info , Repeat1 , [Combinator (no_combinator_info, Then, List.map semi__method t)]) | Method_option t => Combinator ( no_combinator_info , Try , [Combinator (no_combinator_info, Then, List.map semi__method t)]) | Method_or t => Combinator (no_combinator_info, Orelse, List.map semi__method t) | Method_one (Method_simp_only l) => semi__method_simp_one (semi__method_simp_only l) | Method_one (Method_simp_add_del_split l) => semi__method_simp_one (semi__method_simp_add_del_split l) | Method_all (Method_simp_only l) => semi__method_simp_all (semi__method_simp_only l) | Method_all (Method_simp_add_del_split l) => semi__method_simp_all (semi__method_simp_add_del_split l) | Method_auto_simp_add_split (l_simp, l_split) => Basic (fn ctxt => SIMPLE_METHOD (auto_tac (fold (fn (f, l) => fold f l) [(Simplifier.add_simp, semi__thm_mult_l ctxt l_simp) ,(Splitter.add_split, List.map (Proof_Context.get_thm ctxt o To_string0) l_split)] ctxt))) | Method_rename_tac l => Basic (K (SIMPLE_METHOD' (Tactic.rename_tac (List.map To_string0 l)))) | Method_case_tac e => Basic (fn ctxt => SIMPLE_METHOD' (Induct_Tacs.case_tac ctxt (of_semi__term e) [] NONE)) | Method_blast n => Basic (case n of NONE => SIMPLE_METHOD' o blast_tac | SOME lim => fn ctxt => SIMPLE_METHOD' (depth_tac ctxt (Code_Numeral.integer_of_natural lim))) | Method_clarify => Basic (fn ctxt => (SIMPLE_METHOD' (fn i => CHANGED_PROP (clarify_tac ctxt i)))) | Method_metis (l_opt, l) => Basic (fn ctxt => (METHOD oo Metis_Tactic.metis_method) ( (if l_opt = [] then NONE else SOME (map To_string0 l_opt), NONE) , map (semi__thm_attribute_single ctxt) l) ctxt) end fun then_tactic l = let open Method in (Combinator (no_combinator_info, Then, map semi__method l), (Position.none, Position.none)) end fun local_terminal_proof o_by = let open META in case o_by of Command_done => Proof.local_done_proof | Command_sorry => Proof.local_skip_proof true | Command_by l_apply => Proof.local_terminal_proof (then_tactic l_apply, NONE) end fun global_terminal_proof o_by = let open META in case o_by of Command_done => Proof.global_done_proof | Command_sorry => Proof.global_skip_proof true | Command_by l_apply => Proof.global_terminal_proof (then_tactic l_apply, NONE) end fun proof_show_gen f (thes, thes_when) st = st |> Proof.proof (SOME ( Method.Source [Token.make_string ("-", Position.none)] , (Position.none, Position.none))) |> Seq.the_result "" |> f |> Proof.show_cmd (thes_when = []) NONE (K I) [] (if thes_when = [] then [] else [(Binding.empty_atts, map (fn t => (t, [])) thes_when)]) [(Binding.empty_atts, [(thes, [])])] true |> snd val semi__command_state = let open META_overload in fn META.Command_apply_end l => (fn st => st |> Proof.apply_end (then_tactic l) |> Seq.the_result "") end val semi__command_proof = let open META_overload val thesis = "?thesis" fun proof_show f = proof_show_gen f (thesis, []) in fn META.Command_apply l => (fn st => st |> Proof.apply (then_tactic l) |> Seq.the_result "") | META.Command_using l => (fn st => let val ctxt = Proof.context_of st in Proof.using [map (fn s => ([ s], [])) (semi__thm_mult_l ctxt l)] st end) | META.Command_unfolding l => (fn st => let val ctxt = Proof.context_of st in Proof.unfolding [map (fn s => ([s], [])) (semi__thm_mult_l ctxt l)] st end) | META.Command_let (e1, e2) => proof_show (Proof.let_bind_cmd [([of_semi__term e1], of_semi__term e2)]) | META.Command_have (n, b, e, e_pr) => proof_show (fn st => st |> Proof.have_cmd true NONE (K I) [] [] [( (To_sbinding n, if b then [[Token.make_string ("simp", Position.none)]] else []) , [(of_semi__term e, [])])] true |> snd |> local_terminal_proof e_pr) | META.Command_fix_let (l, l_let, o_exp, _) => proof_show_gen ( fold (fn (e1, e2) => Proof.let_bind_cmd [([of_semi__term e1], of_semi__term e2)]) l_let o Proof.fix_cmd (List.map (fn i => (To_sbinding i, NONE, NoSyn)) l)) ( case o_exp of NONE => thesis | SOME (l_spec, _) => (String.concatWith (" \ ") (List.map of_semi__term l_spec)) , case o_exp of NONE => [] | SOME (_, l_when) => List.map of_semi__term l_when) end fun semi__theory in_theory in_local = let open META open META_overload in (*let val f = *)fn Theory_datatype (Datatype (n, l)) => in_local (BNF_FP_Def_Sugar.co_datatype_cmd BNF_Util.Least_FP BNF_LFP.construct_lfp (Ctr_Sugar.default_ctr_options_cmd, [( ( ( (([], To_sbinding n), NoSyn) , List.map (fn (n, l) => ( ( (To_binding "", To_sbinding n) , List.map (fn s => (To_binding "", of_semi__typ s)) l) , NoSyn)) l) , (To_binding "", To_binding "", To_binding "")) , [])])) | Theory_type_synonym (Type_synonym (n, v, l)) => in_theory (fn thy => let val s_bind = To_sbinding n in (snd o Typedecl.abbrev_global (s_bind, map To_string0 v, NoSyn) (Isabelle_Typedecl.abbrev_cmd0 (SOME s_bind) thy (of_semi__typ l))) thy end) | Theory_type_notation (Type_notation (n, e)) => in_local (Specification.type_notation_cmd true ("", true) [(To_string0 n, Mixfix (Input.string (To_string0 e), [], 1000, Position.no_range))]) | Theory_instantiation (Instantiation (n, n_def, expr)) => in_theory (fn thy => let val name = To_string0 n val tycos = [ let val Term.Type (s, _) = (Isabelle_Typedecl.abbrev_cmd0 NONE thy name) in s end ] in thy |> Class.instantiation (tycos, [], Syntax.read_sort (Proof_Context.init_global thy) "object") |> fold_map (fn _ => fn thy => let val ((_, (_, ty)), thy) = Specification.definition_cmd NONE [] [] ((To_binding (To_string0 n_def ^ "_" ^ name ^ "_def"), []) , of_semi__term expr) false thy in (ty, thy) end) tycos |-> Class.prove_instantiation_exit_result (map o Morphism.thm) (fn ctxt => fn thms => Class.intro_classes_tac ctxt [] THEN ALLGOALS (Proof_Context.fact_tac ctxt thms)) |-> K I end) | Theory_overloading (Overloading (n_c, e_c, n, e)) => in_theory (fn thy => thy |> Overloading.overloading_cmd [(To_string0 n_c, of_semi__term e_c, true)] |> snd o Specification.definition_cmd NONE [] [] ((To_sbinding n, []), of_semi__term e) false |> Local_Theory.exit_global) | Theory_consts (Consts (n, ty, symb)) => in_theory (Sign.add_consts_cmd [( To_sbinding n , of_semi__typ ty , Mixfix (Input.string ("(_) " ^ To_string0 symb), [], 1000, Position.no_range))]) | Theory_definition def => in_local let val (def, e) = case def of Definition e => (NONE, e) | Definition_where1 (name, (abbrev, prio), e) => (SOME ( To_sbinding name , NONE , Mixfix (Input.string ("(1" ^ of_semi__term abbrev ^ ")"), [], Code_Numeral.integer_of_natural prio, Position.no_range)), e) | Definition_where2 (name, abbrev, e) => (SOME ( To_sbinding name , NONE , Mixfix (Input.string ("(" ^ of_semi__term abbrev ^ ")"), [], 1000, Position.no_range)), e) in (snd o Specification.definition_cmd def [] [] (Binding.empty_atts, of_semi__term e) false) end | Theory_lemmas (Lemmas_simp_thm (simp, s, l)) => in_local (fn lthy => (snd o Specification.theorems Thm.theoremK [((To_sbinding s, List.map (fn s => Attrib.check_src lthy [Token.make_string (s, Position.none)]) (if simp then ["simp", "code_unfold"] else [])), List.map (fn x => ([semi__thm_attribute_single lthy x], [])) l)] [] false) lthy) | Theory_lemmas (Lemmas_simp_thms (s, l)) => in_local (fn lthy => (snd o Specification.theorems Thm.theoremK [((To_sbinding s, List.map (fn s => Attrib.check_src lthy [Token.make_string (s, Position.none)]) ["simp", "code_unfold"]), List.map (fn x => (Proof_Context.get_thms lthy (To_string0 x), [])) l)] [] false) lthy) | Theory_lemma (Lemma (n, l_spec, l_apply, o_by)) => in_local (fn lthy => Specification.theorem_cmd true Thm.theoremK NONE (K I) Binding.empty_atts [] [] (Element.Shows [((To_sbinding n, []) ,[((String.concatWith (" \ ") (List.map of_semi__term l_spec)), [])])]) false lthy |> fold (semi__command_proof o META.Command_apply) l_apply |> global_terminal_proof o_by) | Theory_lemma (Lemma_assumes (n, l_spec, concl, l_apply, o_by)) => in_local (fn lthy => lthy |> Specification.theorem_cmd true Thm.theoremK NONE (K I) (To_sbinding n, []) [] (List.map (fn (n, (b, e)) => Element.Assumes [( ( To_sbinding n , if b then [[Token.make_string ("simp", Position.none)]] else []) , [(of_semi__term e, [])])]) l_spec) (Element.Shows [(Binding.empty_atts, [(of_semi__term concl, [])])]) false |> fold semi__command_proof l_apply |> (case map_filter (fn META.Command_let _ => SOME [] | META.Command_have _ => SOME [] | META.Command_fix_let (_, _, _, l) => SOME l | _ => NONE) (rev l_apply) of [] => global_terminal_proof o_by | _ :: l => let val arg = (NONE, true) in fn st => st |> local_terminal_proof o_by |> fold (fn l => fold semi__command_state l o Proof.local_qed arg) l |> Proof.global_qed arg end)) | Theory_axiomatization (Axiomatization (n, e)) => in_theory (#2 o Specification.axiomatization_cmd [] [] [] [((To_sbinding n, []), of_semi__term e)]) | Theory_section _ => in_theory I | Theory_text _ => in_theory I | Theory_ML (SML ml) => in_theory (Code_printing.reflect_ml (Input.source false (of_semi__term' ml) (Position.none, Position.none))) | Theory_setup (Setup ml) => in_theory (Isar_Cmd.setup (Input.source false (of_semi__term' ml) (Position.none, Position.none))) | Theory_thm (Thm thm) => in_local (fn lthy => let val () = writeln (Pretty.string_of (Proof_Context.pretty_fact lthy ("", List.map (semi__thm_attribute_single lthy) thm))) in lthy end) | Theory_interpretation (Interpretation (n, loc_n, loc_param, o_by)) => in_local (fn lthy => lthy |> Interpretation.interpretation_cmd ( [ ( (To_string0 loc_n, Position.none) , ( (To_string0 n, true) , (if loc_param = [] then Expression.Named [] else Expression.Positional (map (SOME o of_semi__term) loc_param), [])))] , []) |> global_terminal_proof o_by) (*in fn t => fn thy => f t thy handle ERROR s => (warning s; thy) end*) end end structure Bind_META = struct open Bind_Isabelle fun all_meta aux ret = let open META open META_overload in fn META_semi_theories thy => ret o (case thy of Theories_one thy => semi__theory I Named_Target.theory_map thy | Theories_locale (data, l) => fn thy => thy |> ( Expression.add_locale_cmd (To_sbinding (META.holThyLocale_name data)) Binding.empty + [] ([], []) (List.concat (map (fn (fixes, assumes) => List.concat [ map (fn (e,ty) => Element.Fixes [( To_binding (of_semi__term e) , SOME (of_semi__typ ty) , NoSyn)]) fixes , case assumes of NONE => [] | SOME (n, e) => [Element.Assumes [( (To_sbinding n, []) , [(of_semi__term e, [])])]]]) (META.holThyLocale_header data))) #> snd) |> fold (fold (semi__theory Local_Theory.background_theory (fn f => Local_Theory.new_group #> f #> Local_Theory.reset_group #> (fn lthy => #1 (Target_Context.switch_named_cmd NONE (Context.Proof lthy)) lthy |> Context.the_proof)))) l |> Local_Theory.exit_global) | META_boot_generation_syntax _ => ret o I | META_boot_setup_env _ => ret o I | META_all_meta_embedding meta => fn thy => aux (map2_ctxt_term (fn T_pure x => T_pure x | e => let fun aux e = case e of T_to_be_parsed (s, _) => SOME let val t = Syntax.read_term (Proof_Context.init_global thy) (To_string0 s) in (t, Term.add_frees t []) end | T_lambda (a, e) => Option.map (fn (e, l_free) => let val a = To_string0 a val (t, l_free) = case List.partition (fn (x, _) => x = a) l_free of ([], l_free) => (Term.TFree ("'a", ["HOL.type"]), l_free) | ([(_, t)], l_free) => (t, l_free) in (lambda (Term.Free (a, t)) e, l_free) end) (aux e) | _ => NONE in case aux e of NONE => error "nested pure expression not expected" | SOME (e, _) => META.T_pure (From.Pure.term e) end) meta) thy end end \ (*<*) subsection\Directives of Compilation for Target Languages\ ML\ structure Deep0 = struct fun apply_hs_code_identifiers ml_module thy = let fun mod_hs (fic, ml_module) = Code_Symbol.Module (fic, [("Haskell", SOME ml_module)]) in fold (Code_Target.set_identifiers o mod_hs) (map (fn x => (Context.theory_name x, ml_module)) (* list of .hs files that will be merged together in "ml_module" *) ( thy :: (* we over-approximate the set of compiler files *) Context.ancestors_of thy)) thy end val default_key = "" structure Export_code_env = struct structure Isabelle = struct val function = "write_file" val argument_main = "main" end structure Haskell = struct val function = "Function" val argument = "Argument" val main = "Main" structure Filename = struct fun hs_function ext = function ^ "." ^ ext fun hs_argument ext = argument ^ "." ^ ext fun hs_main ext = main ^ "." ^ ext end end structure OCaml = struct val make = "write" structure Filename = struct fun function ext = "function." ^ ext fun argument ext = "argument." ^ ext fun main_fic ext = "main." ^ ext fun makefile ext = make ^ "." ^ ext end end structure Scala = struct structure Filename = struct fun function ext = "Function." ^ ext fun argument ext = "Argument." ^ ext end end structure SML = struct val main = "Run" structure Filename = struct fun function ext = "Function." ^ ext fun argument ext = "Argument." ^ ext fun stdout ext = "Stdout." ^ ext fun main_fic ext = main ^ "." ^ ext end end datatype file_input = File | Directory end fun compile l cmd = let val (l, rc) = fold (fn cmd => (fn (l, 0) => let val {out, err, rc, ...} = Bash.process cmd in ((out, err) :: l, rc) end | x => x)) l ([], 0) val l = rev l in if rc = 0 then (l, Isabelle_System.bash_output cmd) else let val () = fold (fn (out, err) => K (warning err; writeln out)) l () in error "Compilation failed" end end val check = fold (fn (cmd, msg) => fn () => let val (out, rc) = Isabelle_System.bash_output cmd in if rc = 0 then () else ( writeln out ; error msg) end) val compiler = let open Export_code_env in [ let val ml_ext = "hs" in ( "Haskell", ml_ext, Directory, Haskell.Filename.hs_function , check [("ghc --version", "ghc is not installed (required for compiling a Haskell project)")] , (fn mk_fic => fn ml_module => fn mk_free => fn thy => File.write (mk_fic ("Main." ^ ml_ext)) (String.concatWith "; " [ "import qualified Unsafe.Coerce" , "import qualified " ^ Haskell.function , "import qualified " ^ Haskell.argument , "main :: IO ()" , "main = " ^ Haskell.function ^ "." ^ Isabelle.function ^ " (Unsafe.Coerce.unsafeCoerce " ^ Haskell.argument ^ "." ^ mk_free (Proof_Context.init_global thy) Isabelle.argument_main ([]: (string * string) list) ^ ")"])) , fn tmp_export_code => fn tmp_file => compile [ "mv " ^ tmp_file ^ "/" ^ Haskell.Filename.hs_argument ml_ext ^ " " ^ Path.implode tmp_export_code , "cd " ^ Path.implode tmp_export_code ^ " && ghc -outputdir _build " ^ Haskell.Filename.hs_main ml_ext ] (Path.implode (Path.append tmp_export_code (Path.make [Haskell.main])))) end , let val ml_ext = "ml" in ( "OCaml", ml_ext, File, OCaml.Filename.function , check [("ocp-build -version", "ocp-build is not installed (required for compiling an OCaml project)") ,("ocamlopt -version", "ocamlopt is not installed (required for compiling an OCaml project)")] , fn mk_fic => fn ml_module => fn mk_free => fn thy => let val () = File.write (mk_fic (OCaml.Filename.makefile "ocp")) (String.concat [ "comp += \"-g\" link += \"-g\" " , "begin generated = true begin library \"nums\" end end " , "begin program \"", OCaml.make, "\" sort = true files = [ \"", OCaml.Filename.function ml_ext , "\" \"", OCaml.Filename.argument ml_ext , "\" \"", OCaml.Filename.main_fic ml_ext , "\" ]" , "requires = [\"nums\"] " , "end" ]) in File.write (mk_fic (OCaml.Filename.main_fic ml_ext)) ("let _ = Function." ^ ml_module ^ "." ^ Isabelle.function ^ " (Obj.magic (Argument." ^ ml_module ^ "." ^ mk_free (Proof_Context.init_global thy) Isabelle.argument_main ([]: (string * string) list) ^ "))") end , fn tmp_export_code => fn tmp_file => compile [ "mv " ^ tmp_file ^ " " ^ Path.implode (Path.append tmp_export_code (Path.make [OCaml.Filename.argument ml_ext])) , "cd " ^ Path.implode tmp_export_code ^ " && ocp-build -init -scan -no-bytecode 2>&1" ] (Path.implode (Path.append tmp_export_code (Path.make [ "_obuild" , OCaml.make , OCaml.make ^ ".asm"])))) end , let val ml_ext = "scala" val ml_module = Unsynchronized.ref ("", "") in ( "Scala", ml_ext, File, Scala.Filename.function , check [("scala -e 0", "scala is not installed (required for compiling a Scala project)")] , (fn _ => fn ml_mod => fn mk_free => fn thy => ml_module := (ml_mod, mk_free (Proof_Context.init_global thy) Isabelle.argument_main ([]: (string * string) list))) , fn tmp_export_code => fn tmp_file => let val l = File.read_lines (Path.explode tmp_file) val (ml_module, ml_main) = Unsynchronized.! ml_module val () = File.write_list (Path.append tmp_export_code (Path.make [Scala.Filename.argument ml_ext])) (List.map (fn s => s ^ "\n") ("object " ^ ml_module ^ " { def main (__ : Array [String]) = " ^ ml_module ^ "." ^ Isabelle.function ^ " (" ^ ml_module ^ "." ^ ml_main ^ ")" :: l @ ["}"])) in compile [] ("scala -nowarn " ^ Path.implode (Path.append tmp_export_code (Path.make [Scala.Filename.argument ml_ext]))) end) end , let val ml_ext_thy = "thy" val ml_ext_ml = "ML" in ( "SML", ml_ext_ml, File, SML.Filename.function , check [ let val isa = "isabelle" in ( Path.implode (Path.expand (Path.append (Path.variable "ISABELLE_HOME") (Path.make ["bin", isa]))) ^ " version" , isa ^ " is not installed (required for compiling a SML project)") end ] , fn mk_fic => fn ml_module => fn mk_free => fn thy => let val esc_star = "*" fun ml l = List.concat [ [ "ML{" ^ esc_star ] , map (fn s => s ^ ";") l , [ esc_star ^ "}"] ] val () = let val fic = mk_fic (SML.Filename.function ml_ext_ml) in (* replace ("\\" ^ "<") by ("\\\060") in 'fic' *) File.write_list fic (map (fn s => (if s = "" then "" else String.concatWith "\\" (map (fn s => let val l = String.size s in if l > 0 andalso String.sub (s,0) = #"<" then "\\060" ^ String.substring (s, 1, String.size s - 1) else s end) (String.fields (fn c => c = #"\\") s))) ^ "\n") (File.read_lines fic)) end in File.write_list (mk_fic (SML.Filename.main_fic ml_ext_thy)) (map (fn s => s ^ "\n") (List.concat [ [ "theory " ^ SML.main , "imports Main" , "begin" , "declare [[ML_print_depth = 500]]" (* any large number so that @{make_string} displays all the expression *) ] , ml [ "val stdout_file = Unsynchronized.ref (File.read (Path.make [\"" ^ SML.Filename.stdout ml_ext_ml ^ "\"]))" , "use \"" ^ SML.Filename.argument ml_ext_ml ^ "\"" ] , ml let val arg = "argument" in [ "val " ^ arg ^ " = XML.content_of (YXML.parse_body (@{make_string} (" ^ ml_module ^ "." ^ mk_free (Proof_Context.init_global thy) Isabelle.argument_main ([]: (string * string) list) ^ ")))" , "use \"" ^ SML.Filename.function ml_ext_ml ^ "\"" , "ML_Context.eval_source (ML_Compiler.verbose false ML_Compiler.flags) (Input.source false (\"let open " ^ ml_module ^ " in " ^ Isabelle.function ^ " (\" ^ " ^ arg ^ " ^ \") end\") (Position.none, Position.none) )" ] end , [ "end" ]])) end , fn tmp_export_code => fn tmp_file => let val stdout_file = Isabelle_System.create_tmp_path "stdout_file" "thy" val () = File.write (Path.append tmp_export_code (Path.make [SML.Filename.stdout ml_ext_ml])) (Path.implode (Path.expand stdout_file)) val (l, (_, exit_st)) = compile [ "mv " ^ tmp_file ^ " " ^ Path.implode (Path.append tmp_export_code (Path.make [SML.Filename.argument ml_ext_ml])) , "cd " ^ Path.implode tmp_export_code ^ " && echo 'use_thy \"" ^ SML.main ^ "\";' | " ^ Path.implode (Path.expand (Path.append (Path.variable "ISABELLE_HOME") (Path.make ["bin", "isabelle"]))) ^ " console" ] "true" val stdout = case try File.read stdout_file of SOME s => let val () = File.rm stdout_file in s end | NONE => "" in (l, (stdout, if List.exists (fn (err, _) => List.exists (fn "*** Error" => true | _ => false) (String.tokens (fn #"\n" => true | _ => false) err)) l then let val () = fold (fn (out, err) => K (warning err; writeln out)) l () in 1 end else exit_st)) end) end ] end structure Find = struct fun ext ml_compiler = case List.find (fn (ml_compiler0, _, _, _, _, _, _) => ml_compiler0 = ml_compiler) compiler of SOME (_, ext, _, _, _, _, _) => ext fun export_mode ml_compiler = case List.find (fn (ml_compiler0, _, _, _, _, _, _) => ml_compiler0 = ml_compiler) compiler of SOME (_, _, mode, _, _, _, _) => mode fun function ml_compiler = case List.find (fn (ml_compiler0, _, _, _, _, _, _) => ml_compiler0 = ml_compiler) compiler of SOME (_, _, _, f, _, _, _) => f fun check_compil ml_compiler = case List.find (fn (ml_compiler0, _, _, _, _, _, _) => ml_compiler0 = ml_compiler) compiler of SOME (_, _, _, _, build, _, _) => build fun init ml_compiler = case List.find (fn (ml_compiler0, _, _, _, _, _, _) => ml_compiler0 = ml_compiler) compiler of SOME (_, _, _, _, _, build, _) => build fun build ml_compiler = case List.find (fn (ml_compiler0, _, _, _, _, _, _) => ml_compiler0 = ml_compiler) compiler of SOME (_, _, _, _, _, _, build) => build end end \ ML\ structure Deep = struct fun absolute_path filename thy = Path.implode (Path.append (Resources.master_directory thy) (Path.explode filename)) fun export_code_tmp_file seris g = fold (fn ((ml_compiler, ml_module), export_arg) => fn f => fn g => f (fn accu => let val tmp_name = Context.theory_name @{theory} in (if Deep0.Find.export_mode ml_compiler = Deep0.Export_code_env.Directory then Isabelle_System.with_tmp_dir tmp_name else Isabelle_System.with_tmp_file tmp_name (Deep0.Find.ext ml_compiler)) (fn filename => g (((((ml_compiler, ml_module), Path.implode filename), export_arg) :: accu))) end)) seris (fn f => f []) (g o rev) fun mk_path_export_code tmp_export_code ml_compiler i = Path.append tmp_export_code (Path.make [ml_compiler ^ Int.toString i]) fun export_code_cmd' seris tmp_export_code f_err filename_thy raw_cs thy = export_code_tmp_file seris (fn seris => let val mem_scala = List.exists (fn ((("Scala", _), _), _) => true | _ => false) seris val thy' (* FIXME unused *) = Isabelle_Code_Target.export_code_cmd false (if mem_scala then Deep0.Export_code_env.Isabelle.function :: raw_cs else raw_cs) ((map o apfst o apsnd) SOME seris) (let val v = Deep0.apply_hs_code_identifiers Deep0.Export_code_env.Haskell.argument thy in if mem_scala then Code_printing.apply_code_printing v else v end) in List_mapi (fn i => fn seri => case seri of (((ml_compiler, _), filename), _) => let val (l, (out, err)) = Deep0.Find.build ml_compiler (mk_path_export_code tmp_export_code ml_compiler i) filename val _ = f_err seri err in (l, out) end) seris end) fun mk_term ctxt s = fst (Scan.pass (Context.Proof ctxt) Args.term (Token.explode0 (Thy_Header.get_keywords' ctxt) s)) fun mk_free ctxt s l = let val t_s = mk_term ctxt s in if Term.is_Free t_s then s else let val l = (s, "") :: l in mk_free ctxt (fst (hd (Term.variant_frees t_s l))) l end end val list_all_eq = fn x0 :: xs => List.all (fn x1 => x0 = x1) xs end \ subsection\Saving the History of Meta Commands\ ML\ fun p_gen f g = f "[" "]" g (*|| f "{" "}" g*) || f "(" ")" g fun paren f = p_gen (fn s1 => fn s2 => fn f => Parse.$$$ s1 |-- f --| Parse.$$$ s2) f fun parse_l f = Parse.$$$ "[" |-- Parse.!!! (Parse.list f --| Parse.$$$ "]") fun parse_l' f = Parse.$$$ "[" |-- Parse.list f --| Parse.$$$ "]" fun parse_l1' f = Parse.$$$ "[" |-- Parse.list1 f --| Parse.$$$ "]" fun annot_ty f = Parse.$$$ "(" |-- f --| Parse.$$$ "::" -- Parse.binding --| Parse.$$$ ")" \ ML\ structure Generation_mode = struct datatype internal_deep = Internal_deep of (string * (string list (* imports *) * string (* import optional (bootstrap) *))) option * ((bstring (* compiler *) * bstring (* main module *) ) * Token.T list) list (* seri_args *) * bstring option (* filename_thy *) * Path.T (* tmp dir export_code *) * bool (* true: skip preview of code exportation *) datatype 'a generation_mode = Gen_deep of unit META.compiler_env_config_ext * internal_deep | Gen_shallow of unit META.compiler_env_config_ext * 'a (* theory init *) | Gen_syntax_print of int option structure Data_gen = Theory_Data (type T = theory generation_mode list Symtab.table val empty = Symtab.empty val extend = I val merge = Symtab.merge (K true)) val code_expr_argsP = Scan.optional (@{keyword "("} |-- Parse.args --| @{keyword ")"}) [] val parse_scheme = @{keyword "design"} >> K META.Gen_only_design || @{keyword "analysis"} >> K META.Gen_only_analysis val parse_sorry_mode = Scan.optional ( @{keyword "SORRY"} >> K (SOME META.Gen_sorry) || @{keyword "no_dirty"} >> K (SOME META.Gen_no_dirty)) NONE val parse_deep = Scan.optional (@{keyword "skip_export"} >> K true) false -- Scan.optional (((Parse.$$$ "(" -- @{keyword "THEORY"}) |-- Parse.name -- ((Parse.$$$ ")" -- Parse.$$$ "(" -- @{keyword "IMPORTS"}) |-- parse_l' Parse.name -- Parse.name) --| Parse.$$$ ")") >> SOME) NONE -- Scan.optional (@{keyword "SECTION"} >> K true) false -- parse_sorry_mode -- (* code_expr_inP *) parse_l1' (@{keyword "in"} |-- (Parse.name -- Scan.optional (@{keyword "module_name"} |-- Parse.name) "" -- code_expr_argsP)) -- Scan.optional ((Parse.$$$ "(" -- @{keyword "output_directory"}) |-- Parse.name --| Parse.$$$ ")" >> SOME) NONE val parse_semantics = let val z = 0 in Scan.optional (paren (@{keyword "generation_semantics"} |-- paren (parse_scheme -- Scan.optional ((Parse.$$$ "," -- @{keyword "oid_start"}) |-- Parse.nat) z))) (META.Gen_default, z) end val mode = let fun mk_env output_disable_thy output_header_thy oid_start design_analysis sorry_mode dirty = META.compiler_env_config_empty output_disable_thy (From.option (From.pair From.string (From.pair (From.list From.string) From.string)) output_header_thy) (META.oidInit (From.internal_oid oid_start)) design_analysis (sorry_mode, dirty) in @{keyword "deep"} |-- parse_semantics -- parse_deep >> (fn ( (design_analysis, oid_start) , ( ((((skip_exportation, output_header_thy), output_disable_thy), sorry_mode), seri_args) , filename_thy)) => fn ctxt => Gen_deep ( mk_env (not output_disable_thy) output_header_thy oid_start design_analysis sorry_mode (Config.get ctxt quick_and_dirty) , Internal_deep ( output_header_thy , seri_args , filename_thy , Isabelle_System.create_tmp_path "deep_export_code" "" , skip_exportation))) || @{keyword "shallow"} |-- parse_semantics -- parse_sorry_mode >> (fn ((design_analysis, oid_start), sorry_mode) => fn ctxt => Gen_shallow ( mk_env true NONE oid_start design_analysis sorry_mode (Config.get ctxt quick_and_dirty) , ())) || (@{keyword "syntax_print"} |-- Scan.optional (Parse.number >> SOME) NONE) >> (fn n => K (Gen_syntax_print (case n of NONE => NONE | SOME n => Int.fromString n))) end fun f_command l_mode = Toplevel.theory (fn thy => let val (l_mode, thy) = META.mapM (fn Gen_shallow (env, ()) => let val thy0 = thy in fn thy => (Gen_shallow (env, thy0), thy) end | Gen_syntax_print n => (fn thy => (Gen_syntax_print n, thy)) | Gen_deep (env, Internal_deep ( output_header_thy , seri_args , filename_thy , tmp_export_code , skip_exportation)) => fn thy => let val _ = warning ("After closing Isabelle/jEdit, we may still need to remove this directory (by hand): " ^ Path.implode (Path.expand tmp_export_code)) val seri_args' = List_mapi (fn i => fn ((ml_compiler, ml_module), export_arg) => let val tmp_export_code = Deep.mk_path_export_code tmp_export_code ml_compiler i fun mk_fic s = Path.append tmp_export_code (Path.make [s]) val () = Deep0.Find.check_compil ml_compiler () val _ = Isabelle_System.make_directory tmp_export_code in ((( (ml_compiler, ml_module) , Path.implode (if Deep0.Find.export_mode ml_compiler = Deep0.Export_code_env.Directory then tmp_export_code else mk_fic (Deep0.Find.function ml_compiler (Deep0.Find.ext ml_compiler)))) , export_arg), mk_fic) end) seri_args val thy' (* FIXME unused *) = Isabelle_Code_Target.export_code_cmd (List.exists (fn (((("SML", _), _), _), _) => true | _ => false) seri_args') [Deep0.Export_code_env.Isabelle.function] (List.map ((apfst o apsnd) SOME o fst) seri_args') (Code_printing.apply_code_printing (Deep0.apply_hs_code_identifiers Deep0.Export_code_env.Haskell.function thy)) val () = fold (fn ((((ml_compiler, ml_module), _), _), mk_fic) => fn _ => Deep0.Find.init ml_compiler mk_fic ml_module Deep.mk_free thy) seri_args' () in (Gen_deep (env, Internal_deep ( output_header_thy , seri_args , filename_thy , tmp_export_code , skip_exportation)), thy) end) let val ctxt = Proof_Context.init_global thy in map (fn f => f ctxt) l_mode end thy in Data_gen.map (Symtab.map_default (Deep0.default_key, l_mode) (fn _ => l_mode)) thy end) fun update_compiler_config f = Data_gen.map (Symtab.map_entry Deep0.default_key (fn l_mode => map (fn Gen_deep (env, d) => Gen_deep (META.compiler_env_config_update f env, d) | Gen_shallow (env, thy) => Gen_shallow (META.compiler_env_config_update f env, thy) | Gen_syntax_print n => Gen_syntax_print n) l_mode)) end \ subsection\Factoring All Meta Commands Together\ setup\ML_Antiquotation.inline @{binding mk_string} (Scan.succeed "(fn ctxt => fn x => ML_Pretty.string_of_polyml (ML_system_pretty (x, FixedInt.fromInt (Config.get ctxt (ML_Print_Depth.print_depth)))))") \ ML\ fun exec_deep (env, output_header_thy, seri_args, filename_thy, tmp_export_code, l_obj) thy0 = let open Generation_mode in let val of_arg = META.isabelle_of_compiler_env_config META.isabelle_apply I in let fun def s = Named_Target.theory_map (snd o Specification.definition_cmd NONE [] [] (Binding.empty_atts, s) false) in let val name_main = Deep.mk_free (Proof_Context.init_global thy0) Deep0.Export_code_env.Isabelle.argument_main [] in thy0 |> def (String.concatWith " " ( "(" (* polymorphism weakening needed by export_code *) ^ name_main ^ " :: (_ \ abr_string option) compiler_env_config_scheme)" :: "=" :: To_string0 (of_arg (META.compiler_env_config_more_map (fn () => (l_obj, From.option From.string (Option.map (fn filename_thy => Deep.absolute_path filename_thy thy0) filename_thy))) env)) :: [])) |> Deep.export_code_cmd' seri_args tmp_export_code (fn (((_, _), msg), _) => fn err => if err <> 0 then error msg else ()) filename_thy [name_main] |> (fn l => let val (l_warn, l) = (map fst l, map snd l) in if Deep.list_all_eq l then (List.concat l_warn, hd l) else error "There is an extracted language which does not produce a similar Isabelle content as the others" end) |> (fn (l_warn, s) => let val () = writeln (case (output_header_thy, filename_thy) of (SOME _, SOME _) => s | _ => String.concat (map ( (fn s => s ^ "\n") o Active.sendback_markup_command o trim_line) (String.tokens (fn c => c = #"\t") s))) in fold (fn (out, err) => K ( writeln (Markup.markup Markup.keyword2 err) ; case trim_line out of "" => () | out => writeln (Markup.markup Markup.keyword1 out))) l_warn () end) end end end end fun outer_syntax_command0 mk_string cmd_spec cmd_descr parser get_all_meta_embed = let open Generation_mode in Outer_Syntax.command cmd_spec cmd_descr (parser >> (fn name => Toplevel.theory (fn thy => let val (env, thy) = META.mapM let val get_all_meta_embed = get_all_meta_embed name in fn Gen_syntax_print n => (fn thy => let val _ = writeln (mk_string (Proof_Context.init_global (case n of NONE => thy | SOME n => Config.put_global ML_Print_Depth.print_depth n thy)) name) in (Gen_syntax_print n, thy) end) | Gen_deep (env, Internal_deep ( output_header_thy , seri_args , filename_thy , tmp_export_code , skip_exportation)) => (fn thy0 => let val l_obj = get_all_meta_embed thy0 in thy0 |> (if skip_exportation then K () else exec_deep ( META.d_output_header_thy_update (fn _ => NONE) env , output_header_thy , seri_args , NONE , tmp_export_code , l_obj)) |> K (Gen_deep ( META.fold_thy_deep l_obj env , Internal_deep ( output_header_thy , seri_args , filename_thy , tmp_export_code , skip_exportation)), thy0) end) | Gen_shallow (env, thy0) => fn thy => let fun aux (env, thy) x = META.fold_thy_shallow (fn f => f () handle ERROR e => ( warning "Shallow Backtracking: (true) Isabelle declarations occurring among the META-simulated ones are ignored (if any)" (* TODO automatically determine if there is such Isabelle declarations, for raising earlier a specific error message *) ; error e)) (fn _ => fn _ => thy0) (fn l => fn (env, thy) => Bind_META.all_meta (fn x => fn thy => aux (env, thy) [x]) (pair env) l thy) x (env, thy) val (env, thy) = aux (env, thy) (get_all_meta_embed thy) in (Gen_shallow (env, thy0), thy) end end (case Symtab.lookup (Data_gen.get thy) Deep0.default_key of SOME l => l | _ => [Gen_syntax_print NONE]) thy in Data_gen.map (Symtab.update (Deep0.default_key, env)) thy end))) end fun outer_syntax_command mk_string cmd_spec cmd_descr parser get_all_meta_embed = outer_syntax_command0 mk_string cmd_spec cmd_descr parser (fn a => fn thy => [get_all_meta_embed a thy]) \ subsection\Parameterizing the Semantics of Embedded Languages\ ML\ val () = let open Generation_mode in Outer_Syntax.command @{command_keyword generation_syntax} "set the generating list" (( mode >> (fn x => SOME [x]) || parse_l' mode >> SOME || @{keyword "deep"} -- @{keyword "flush_all"} >> K NONE) >> (fn SOME x => f_command x | NONE => Toplevel.theory (fn thy => let val l = case Symtab.lookup (Data_gen.get thy) Deep0.default_key of SOME l => l | _ => [] val l = List.concat (List.map (fn Gen_deep x => [x] | _ => []) l) val _ = case l of [] => warning "Nothing to perform." | _ => () val thy = fold (fn (env, Internal_deep (output_header_thy, seri_args, filename_thy, tmp_export_code, _)) => fn thy0 => thy0 |> let val (env, l_exec) = META.compiler_env_config_reset_all env in exec_deep (env, output_header_thy, seri_args, filename_thy, tmp_export_code, l_exec) end |> K thy0) l thy in thy end))) end \ subsection\Common Parser for Toy\ ML\ structure TOY_parse = struct datatype ('a, 'b) use_context = TOY_context_invariant of 'a | TOY_context_pre_post of 'b fun optional f = Scan.optional (f >> SOME) NONE val colon = Parse.$$$ ":" fun repeat2 scan = scan ::: Scan.repeat1 scan fun xml_unescape s = (XML.content_of (YXML.parse_body s), Position.none) |> Symbol_Pos.explode |> Symbol_Pos.implode |> From.string fun outer_syntax_command2 mk_string cmd_spec cmd_descr parser v_true v_false get_all_meta_embed = outer_syntax_command mk_string cmd_spec cmd_descr (optional (paren @{keyword "shallow"}) -- parser) (fn (is_shallow, use) => fn thy => get_all_meta_embed (if is_shallow = NONE then ( fn s => META.T_to_be_parsed ( From.string s , xml_unescape s) , v_true) else (From.toy_ctxt_term thy, v_false)) use) (* *) val ident_dot_dot = let val f = Parse.sym_ident >> (fn "\" => "\" | _ => Scan.fail "Syntax error") in f -- f end val ident_star = Parse.sym_ident (* "*" *) (* *) val unlimited_natural = ident_star >> (fn "*" => META.Mult_star | "\" => META.Mult_infinity | _ => Scan.fail "Syntax error") || Parse.number >> (fn s => META.Mult_nat (case Int.fromString s of SOME i => Code_Numeral.natural_of_integer i | NONE => Scan.fail "Syntax error")) val term_base = Parse.number >> (META.ToyDefInteger o From.string) || Parse.float_number >> (META.ToyDefReal o (From.pair From.string From.string o (fn s => case String.tokens (fn #"." => true | _ => false) s of [l1,l2] => (l1,l2) | _ => Scan.fail "Syntax error"))) || Parse.string >> (META.ToyDefString o From.string) val multiplicity = parse_l' (unlimited_natural -- optional (ident_dot_dot |-- unlimited_natural)) fun toy_term x = ( term_base >> META.ShallB_term || Parse.binding >> (META.ShallB_str o From.binding) || @{keyword "self"} |-- Parse.nat >> (fn n => META.ShallB_self (From.internal_oid n)) || paren (Parse.list toy_term) >> (* untyped, corresponds to Set, Sequence or Pair *) (* WARNING for Set: we are describing a finite set *) META.ShallB_list) x val name_object = optional (Parse.list1 Parse.binding --| colon) -- Parse.binding val type_object_weak = let val name_object = Parse.binding >> (fn s => (NONE, s)) in name_object -- Scan.repeat (Parse.$$$ "<" |-- Parse.list1 name_object) >> let val f = fn (_, s) => META.ToyTyCore_pre (From.binding s) in fn (s, l) => META.ToyTyObj (f s, map (map f) l) end end val type_object = name_object -- Scan.repeat (Parse.$$$ "<" |-- Parse.list1 name_object) >> let val f = fn (_, s) => META.ToyTyCore_pre (From.binding s) in fn (s, l) => META.ToyTyObj (f s, map (map f) l) end val category = multiplicity -- optional (@{keyword "Role"} |-- Parse.binding) -- Scan.repeat ( @{keyword "Ordered"} >> K META.Ordered0 || @{keyword "Subsets"} |-- Parse.binding >> K META.Subsets0 || @{keyword "Union"} >> K META.Union0 || @{keyword "Redefines"} |-- Parse.binding >> K META.Redefines0 || @{keyword "Derived"} -- Parse.$$$ "=" |-- Parse.term >> K META.Derived0 || @{keyword "Qualifier"} |-- Parse.term >> K META.Qualifier0 || @{keyword "Nonunique"} >> K META.Nonunique0 || @{keyword "Sequence_"} >> K META.Sequence) >> (fn ((l_mult, role), l) => META.Toy_multiplicity_ext (l_mult, From.option From.binding role, l, ())) val type_base = Parse.reserved "Void" >> K META.ToyTy_base_void || Parse.reserved "Boolean" >> K META.ToyTy_base_boolean || Parse.reserved "Integer" >> K META.ToyTy_base_integer || Parse.reserved "UnlimitedNatural" >> K META.ToyTy_base_unlimitednatural || Parse.reserved "Real" >> K META.ToyTy_base_real || Parse.reserved "String" >> K META.ToyTy_base_string fun use_type_gen type_object v = ((* collection *) Parse.reserved "Set" |-- use_type >> (fn l => META.ToyTy_collection (META.Toy_multiplicity_ext ([], NONE, [META.Set], ()), l)) || Parse.reserved "Sequence" |-- use_type >> (fn l => META.ToyTy_collection (META.Toy_multiplicity_ext ([], NONE, [META.Sequence], ()), l)) || category -- use_type >> META.ToyTy_collection (* pair *) || Parse.reserved "Pair" |-- ( use_type -- use_type || Parse.$$$ "(" |-- use_type --| Parse.$$$ "," -- use_type --| Parse.$$$ ")") >> META.ToyTy_pair (* base *) || type_base (* raw HOL *) || Parse.sym_ident (* "\" *) |-- Parse.typ --| Parse.sym_ident (* "\" *) >> (META.ToyTy_raw o xml_unescape) (* object type *) || type_object >> META.ToyTy_object || ((Parse.$$$ "(" |-- Parse.list ( (Parse.binding --| colon >> (From.option From.binding o SOME)) -- ( Parse.$$$ "(" |-- use_type --| Parse.$$$ ")" || use_type_gen type_object_weak) >> META.ToyTy_binding ) --| Parse.$$$ ")" >> (fn ty_arg => case rev ty_arg of [] => META.ToyTy_base_void | ty_arg => fold (fn x => fn acc => META.ToyTy_pair (x, acc)) (tl ty_arg) (hd ty_arg))) -- optional (colon |-- use_type)) >> (fn (ty_arg, ty_out) => case ty_out of NONE => ty_arg | SOME ty_out => META.ToyTy_arrow (ty_arg, ty_out)) || (Parse.$$$ "(" |-- use_type --| Parse.$$$ ")" >> (fn s => META.ToyTy_binding (NONE, s)))) v and use_type x = use_type_gen type_object x val use_prop = (optional (optional (Parse.binding >> From.binding) --| Parse.$$$ ":") >> (fn NONE => NONE | SOME x => x)) -- Parse.term --| optional (Parse.$$$ ";") >> (fn (n, e) => fn from_expr => META.ToyProp_ctxt (n, from_expr e)) (* *) val association_end = type_object -- category --| optional (Parse.$$$ ";") val association = optional @{keyword "Between"} |-- Scan.optional (repeat2 association_end) [] val invariant = optional @{keyword "Constraints"} |-- Scan.optional (@{keyword "Existential"} >> K true) false --| @{keyword "Inv"} -- use_prop structure Outer_syntax_Association = struct fun make ass_ty l = META.Toy_association_ext (ass_ty, META.ToyAssRel l, ()) end (* *) val context = Scan.repeat (( optional (@{keyword "Operations"} || Parse.$$$ "::") |-- Parse.binding -- use_type --| optional (Parse.$$$ "=" |-- Parse.term || Parse.term) -- Scan.repeat ( (@{keyword "Pre"} || @{keyword "Post"}) -- use_prop >> TOY_context_pre_post || invariant >> TOY_context_invariant) --| optional (Parse.$$$ ";")) >> (fn ((name_fun, ty), expr) => fn from_expr => META.Ctxt_pp (META.Toy_ctxt_pre_post_ext ( From.binding name_fun , ty , From.list (fn TOY_context_pre_post (pp, expr) => META.T_pp (if pp = "Pre" then META.ToyCtxtPre else META.ToyCtxtPost, expr from_expr) | TOY_context_invariant (b, expr) => META.T_invariant (META.T_inv (b, expr from_expr))) expr , ()))) || invariant >> (fn (b, expr) => fn from_expr => META.Ctxt_inv (META.T_inv (b, expr from_expr)))) val class = optional @{keyword "Attributes"} |-- Scan.repeat (Parse.binding --| colon -- use_type --| optional (Parse.$$$ ";")) -- context datatype use_classDefinition = TOY_class | TOY_class_abstract datatype ('a, 'b) use_classDefinition_content = TOY_class_content of 'a | TOY_class_synonym of 'b structure Outer_syntax_Class = struct fun make from_expr abstract ty_object attribute oper = META.Toy_class_raw_ext ( ty_object , From.list (From.pair From.binding I) attribute , From.list (fn f => f from_expr) oper , abstract , ()) end (* *) val term_object = parse_l ( optional ( Parse.$$$ "(" |-- Parse.binding --| Parse.$$$ "," -- Parse.binding --| Parse.$$$ ")" --| (Parse.sym_ident >> (fn "|=" => Scan.succeed | _ => Scan.fail ""))) -- Parse.binding -- ( Parse.$$$ "=" |-- toy_term)) val list_attr' = term_object >> (fn res => (res, [] : binding list)) fun object_cast e = ( annot_ty term_object -- Scan.repeat ( (Parse.sym_ident >> (fn "->" => Scan.succeed | "\" => Scan.succeed | "\" => Scan.succeed | _ => Scan.fail "")) |-- ( Parse.reserved "toyAsType" |-- Parse.$$$ "(" |-- Parse.binding --| Parse.$$$ ")" || Parse.binding)) >> (fn ((res, x), l) => (res, rev (x :: l)))) e val object_cast' = object_cast >> (fn (res, l) => (res, rev l)) fun get_toyinst l _ = META.ToyInstance (map (fn ((name,typ), (l_attr, is_cast)) => let val f = map (fn ((pre_post, attr), data) => ( From.option (From.pair From.binding From.binding) pre_post , ( From.binding attr , data))) val l_attr = fold (fn b => fn acc => META.ToyAttrCast (From.binding b, acc, [])) is_cast (META.ToyAttrNoCast (f l_attr)) in META.Toy_instance_single_ext (From.option From.binding name, From.option From.binding typ, l_attr, ()) end) l) val parse_instance = (Parse.binding >> SOME) -- optional (@{keyword "::"} |-- Parse.binding) --| @{keyword "="} -- (list_attr' || object_cast') (* *) datatype state_content = ST_l_attr of (((binding * binding) option * binding) * META.toy_data_shallow) list * binding list | ST_binding of binding val state_parse = parse_l' ( object_cast >> ST_l_attr || Parse.binding >> ST_binding) fun mk_state thy = map (fn ST_l_attr l => META.ToyDefCoreAdd (case get_toyinst (map (fn (l_i, l_ty) => ((NONE, SOME (hd l_ty)), (l_i, rev (tl l_ty)))) [l]) thy of META.ToyInstance [x] => x) | ST_binding b => META.ToyDefCoreBinding (From.binding b)) (* *) datatype state_pp_content = ST_PP_l_attr of state_content list | ST_PP_binding of binding val state_pp_parse = state_parse >> ST_PP_l_attr || Parse.binding >> ST_PP_binding fun mk_pp_state thy = fn ST_PP_l_attr l => META.ToyDefPPCoreAdd (mk_state thy l) | ST_PP_binding s => META.ToyDefPPCoreBinding (From.binding s) end \ subsection\Setup of Meta Commands for Toy: Enum\ ML\ val () = outer_syntax_command @{mk_string} @{command_keyword Enum} "" (Parse.binding -- parse_l1' Parse.binding) (fn (n1, n2) => K (META.META_enum (META.ToyEnum (From.binding n1, From.list From.binding n2)))) \ subsection\Setup of Meta Commands for Toy: (abstract) Class\ ML\ local open TOY_parse fun mk_classDefinition abstract cmd_spec = outer_syntax_command2 @{mk_string} cmd_spec "Class generation" ( Parse.binding --| Parse.$$$ "=" -- TOY_parse.type_base >> TOY_class_synonym || type_object -- class >> TOY_class_content) (curry META.META_class_raw META.Floor1) (curry META.META_class_raw META.Floor2) (fn (from_expr, META_class_raw) => fn TOY_class_content (ty_object, (attribute, oper)) => META_class_raw (Outer_syntax_Class.make from_expr (abstract = TOY_class_abstract) ty_object attribute oper) | TOY_class_synonym (n1, n2) => META.META_class_synonym (META.ToyClassSynonym (From.binding n1, n2))) in val () = mk_classDefinition TOY_class @{command_keyword Class} val () = mk_classDefinition TOY_class_abstract @{command_keyword Abstract_class} end \ subsection\Setup of Meta Commands for Toy: Association, Composition, Aggregation\ ML\ local open TOY_parse fun mk_associationDefinition ass_ty cmd_spec = outer_syntax_command @{mk_string} cmd_spec "" ( repeat2 association_end || optional Parse.binding |-- association) (fn l => fn _ => META.META_association (Outer_syntax_Association.make ass_ty l)) in val () = mk_associationDefinition META.ToyAssTy_association @{command_keyword Association} val () = mk_associationDefinition META.ToyAssTy_composition @{command_keyword Composition} val () = mk_associationDefinition META.ToyAssTy_aggregation @{command_keyword Aggregation} end \ subsection\Setup of Meta Commands for Toy: (abstract) Associationclass\ ML\ local open TOY_parse datatype use_associationClassDefinition = TOY_associationclass | TOY_associationclass_abstract fun mk_associationClassDefinition abstract cmd_spec = outer_syntax_command2 @{mk_string} cmd_spec "" ( type_object -- association -- class -- optional (Parse.reserved "aggregation" || Parse.reserved "composition")) (curry META.META_ass_class META.Floor1) (curry META.META_ass_class META.Floor2) (fn (from_expr, META_ass_class) => fn (((ty_object, l_ass), (attribute, oper)), assty) => META_ass_class (META.ToyAssClass ( Outer_syntax_Association.make (case assty of SOME "aggregation" => META.ToyAssTy_aggregation | SOME "composition" => META.ToyAssTy_composition | _ => META.ToyAssTy_association) l_ass , Outer_syntax_Class.make from_expr (abstract = TOY_associationclass_abstract) ty_object attribute oper))) in val () = mk_associationClassDefinition TOY_associationclass @{command_keyword Associationclass} val () = mk_associationClassDefinition TOY_associationclass_abstract @{command_keyword Abstract_associationclass} end \ subsection\Setup of Meta Commands for Toy: Context\ ML\ local open TOY_parse in val () = outer_syntax_command2 @{mk_string} @{command_keyword Context} "" (optional (Parse.list1 Parse.binding --| colon) -- Parse.binding -- context) (curry META.META_ctxt META.Floor1) (curry META.META_ctxt META.Floor2) (fn (from_expr, META_ctxt) => (fn ((l_param, name), l) => META_ctxt (META.Toy_ctxt_ext ( case l_param of NONE => [] | SOME l => From.list From.binding l , META.ToyTyObj (META.ToyTyCore_pre (From.binding name), []) , From.list (fn f => f from_expr) l , ())))) end \ subsection\Setup of Meta Commands for Toy: End\ ML\ val () = outer_syntax_command0 @{mk_string} @{command_keyword End} "Class generation" (Scan.optional ( Parse.$$$ "[" -- Parse.reserved "forced" -- Parse.$$$ "]" >> K true || Parse.$$$ "!" >> K true) false) (fn b => fn _ => if b then [META.META_flush_all META.ToyFlushAll] else []) \ subsection\Setup of Meta Commands for Toy: BaseType, Instance, State\ ML\ val () = outer_syntax_command @{mk_string} @{command_keyword BaseType} "" (parse_l' TOY_parse.term_base) (K o META.META_def_base_l o META.ToyDefBase) local open TOY_parse in val () = outer_syntax_command @{mk_string} @{command_keyword Instance} "" (Scan.optional (parse_instance -- Scan.repeat (optional @{keyword "and"} |-- parse_instance) >> (fn (x, xs) => x :: xs)) []) (META.META_instance oo get_toyinst) val () = outer_syntax_command @{mk_string} @{command_keyword State} "" (TOY_parse.optional (paren @{keyword "shallow"}) -- Parse.binding --| @{keyword "="} -- state_parse) (fn ((is_shallow, name), l) => fn thy => META.META_def_state ( if is_shallow = NONE then META.Floor1 else META.Floor2 , META.ToyDefSt (From.binding name, mk_state thy l))) end \ subsection\Setup of Meta Commands for Toy: PrePost\ ML\ local open TOY_parse in val () = outer_syntax_command @{mk_string} @{command_keyword PrePost} "" (TOY_parse.optional (paren @{keyword "shallow"}) -- TOY_parse.optional (Parse.binding --| @{keyword "="}) -- state_pp_parse -- TOY_parse.optional state_pp_parse) (fn (((is_shallow, n), s_pre), s_post) => fn thy => META.META_def_pre_post ( if is_shallow = NONE then META.Floor1 else META.Floor2 , META.ToyDefPP ( From.option From.binding n , mk_pp_state thy s_pre , From.option (mk_pp_state thy) s_post))) end (*val _ = print_depth 100*) \ (*>*) end diff --git a/thys/Simpl/hoare.ML b/thys/Simpl/hoare.ML --- a/thys/Simpl/hoare.ML +++ b/thys/Simpl/hoare.ML @@ -1,3410 +1,3410 @@ (* Title: hoare.ML Author: Norbert Schirmer, TU Muenchen Copyright (C) 2004-2007 Norbert Schirmer This library is free software; you can redistribute it and/or modify it under the terms of the GNU Lesser General Public License as published by the Free Software Foundation; either version 2.1 of the License, or (at your option) any later version. This library is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU Lesser General Public License for more details. You should have received a copy of the GNU Lesser General Public License along with this library; if not, write to the Free Software Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA *) signature HOARE = sig datatype hoareMode = Partial | Total val gen_proc_rec: Proof.context -> hoareMode -> int -> thm datatype state_kind = Record | Function datatype par_kind = In | Out val deco: string val proc_deco: string val par_deco: string -> string val chopsfx: string -> string -> string val is_state_var: string -> bool val extern: Proof.context -> string -> string val remdeco: Proof.context -> string -> string val remdeco': string -> string val undeco: Proof.context -> term -> term val varname: string -> string val resuffix: string -> string -> string -> string type proc_info = {params: ((par_kind * string) list), recursive: bool, state_kind: state_kind} type hoare_tac = (bool -> int -> tactic) -> Proof.context -> hoareMode -> int -> tactic type hoare_data = {proc_info: proc_info Symtab.table, active_procs: string list list, default_state_kind: state_kind, generate_guard: (stamp * (Proof.context -> term -> term option)), wp_tacs: (string * hoare_tac) list, hoare_tacs: (string * hoare_tac) list, vcg_simps: thm list} val get_data: Proof.context -> hoare_data val get_params: string -> Proof.context -> (par_kind * string) list option val get_default_state_kind: Proof.context -> state_kind val get_state_kind: string -> Proof.context -> state_kind option val clique_name: string list -> string val install_generate_guard: (Proof.context -> term -> term option) -> Context.generic -> Context.generic val generate_guard: Proof.context -> term -> term option val BasicSimpTac: Proof.context -> state_kind -> bool -> thm list -> (int -> tactic) -> int -> tactic val hoare: (Proof.context -> Proof.method) context_parser val hoare_raw: (Proof.context -> Proof.method) context_parser val vcg: (Proof.context -> Proof.method) context_parser val vcg_step: (Proof.context -> Proof.method) context_parser val hoare_rule: (Proof.context -> Proof.method) context_parser val add_foldcongsimps: thm list -> theory -> theory val get_foldcong_ss : theory -> simpset val add_foldcongs : thm list -> theory -> theory val modeqN : string val modexN : string val implementationN : string val specL : string val vcg_tac : string -> string -> string list -> Proof.context -> int -> tactic val hoare_rule_tac : Proof.context -> thm list -> int -> tactic datatype 'a bodykind = BodyTyp of 'a | BodyTerm of 'a val proc_specs : (bstring * string) list parser val add_params : morphism -> string -> (par_kind * string) list -> Context.generic -> Context.generic val set_default_state_kind : state_kind -> Context.generic -> Context.generic val add_state_kind : morphism -> string -> state_kind -> Context.generic -> Context.generic val add_recursive : morphism -> string -> Context.generic -> Context.generic end; structure Hoare: HOARE = struct (* Misc *) val record_vanish = Attrib.setup_config_bool @{binding hoare_record_vanish} (K true); val use_generalise = Attrib.setup_config_bool @{binding hoare_use_generalise} (K false); val sort_variables = Attrib.setup_config_bool @{binding hoare_sort_variables} (K true); val use_cond_inv_modifies = Attrib.setup_config_bool @{binding hoare_use_cond_inv_modifies} (K true); val hoare_trace = Attrib.setup_config_bool @{binding hoare_trace} (K false); val body_def_sfx = "_body"; val programN = "\"; val hoare_ctxtL = "hoare"; val specL = "_spec"; val procL = "_proc"; val bodyP = "_impl"; val modifysfx = "_modifies"; val modexN = "Hoare.mex"; val modeqN = "Hoare.meq"; val KNF = @{const_name StateFun.K_statefun}; (* Some abstract syntax operations *) val Trueprop = HOLogic.mk_Trueprop; infix 0 ===; val (op ===) = Trueprop o HOLogic.mk_eq; fun is_empty_set (Const (@{const_name Orderings.bot}, _)) = true | is_empty_set _ = false; fun mk_Int Ts A B = let val T = fastype_of1 (Ts, A) in Const (@{const_name Lattices.inf}, T --> T --> T) $ A $ B end; fun mk_Un T (A, B) = Const (@{const_name Lattices.sup}, T --> T --> T) $ A $ B; fun dest_Un (Const (@{const_name Lattices.sup}, _) $ t1 $ t2) = dest_Un t1 @ dest_Un t2 | dest_Un t = [t] fun mk_UN' dT rT t = let val dTs = HOLogic.mk_setT dT; val rTs = HOLogic.mk_setT rT; in Const (@{const_name Complete_Lattices.Sup}, rTs --> rT) $ (Const (@{const_name image}, (dT --> rT) --> dTs --> rTs) $ t $ Const (@{const_name Orderings.top}, dTs)) end; fun mk_UN ((x, T), P) = mk_UN' T (fastype_of P) (absfree (x, T) P); fun dest_UN (Const (@{const_name Complete_Lattices.Sup}, _) $ (Const (@{const_name Set.image}, _) $ Abs (x, T, t) $ Const (@{const_name Orderings.top}, _))) = let val (vars, body) = dest_UN t in ((x, T) :: vars, body) end | dest_UN t = ([], t); fun tap_UN (Const (@{const_name Complete_Lattices.Sup}, _) $ (Const (@{const_name Set.image}, _) $ t $ Const (@{const_name Orderings.top}, _))) = SOME t | tap_UN _ = NONE; (* Fetching the rules *) datatype hoareMode = Partial | Total fun get_rule p t Partial = p | get_rule p t Total = t val Guard = get_rule @{thm HoarePartial.Guard} @{thm HoareTotal.Guard}; val GuardStrip = get_rule @{thm HoarePartial.GuardStrip} @{thm HoareTotal.GuardStrip}; val GuaranteeAsGuard = get_rule @{thm HoarePartial.GuaranteeAsGuard} @{thm HoareTotal.GuaranteeAsGuard}; val Guarantee = get_rule @{thm HoarePartial.Guarantee} @{thm HoareTotal.Guarantee}; val GuaranteeStrip = get_rule @{thm HoarePartial.GuaranteeStrip} @{thm HoareTotal.GuaranteeStrip}; val GuardsNil = get_rule @{thm HoarePartial.GuardsNil} @{thm HoareTotal.GuardsNil}; val GuardsCons = get_rule @{thm HoarePartial.GuardsCons} @{thm HoareTotal.GuardsCons}; val GuardsConsGuaranteeStrip = get_rule @{thm HoarePartial.GuardsConsGuaranteeStrip} @{thm HoareTotal.GuardsConsGuaranteeStrip}; val Skip = get_rule @{thm HoarePartial.Skip} @{thm HoareTotal.Skip}; val Basic = get_rule @{thm HoarePartial.Basic} @{thm HoareTotal.Basic}; val BasicCond = get_rule @{thm HoarePartial.BasicCond} @{thm HoareTotal.BasicCond}; val Spec = get_rule @{thm HoarePartial.Spec} @{thm HoareTotal.Spec}; val SpecIf = get_rule @{thm HoarePartial.SpecIf} @{thm HoareTotal.SpecIf}; val Throw = get_rule @{thm HoarePartial.Throw} @{thm HoareTotal.Throw}; val Raise = get_rule @{thm HoarePartial.raise} @{thm HoareTotal.raise}; val Catch = get_rule @{thm HoarePartial.Catch} @{thm HoareTotal.Catch}; val CondCatch = get_rule @{thm HoarePartial.condCatch} @{thm HoareTotal.condCatch}; val CatchSwap = get_rule @{thm HoarePartial.CatchSwap} @{thm HoareTotal.CatchSwap}; val CondCatchSwap = get_rule @{thm HoarePartial.condCatchSwap} @{thm HoareTotal.condCatchSwap}; val Seq = get_rule @{thm HoarePartial.Seq} @{thm HoareTotal.Seq}; val SeqSwap = get_rule @{thm HoarePartial.SeqSwap} @{thm HoareTotal.SeqSwap}; val BSeq = get_rule @{thm HoarePartial.BSeq} @{thm HoareTotal.BSeq}; val Cond = get_rule @{thm HoarePartial.Cond} @{thm HoareTotal.Cond}; val CondInv'Partial = @{thm HoarePartial.CondInv'}; val CondInv'Total = @{thm HoareTotal.CondInv'}; val CondInv' = get_rule CondInv'Partial CondInv'Total; val SwitchNil = get_rule @{thm HoarePartial.switchNil} @{thm HoareTotal.switchNil}; val SwitchCons = get_rule @{thm HoarePartial.switchCons} @{thm HoareTotal.switchCons}; val CondSwap = get_rule @{thm HoarePartial.CondSwap} @{thm HoareTotal.CondSwap}; val While = get_rule @{thm HoarePartial.While} @{thm HoareTotal.While}; val WhileAnnoG = get_rule @{thm HoarePartial.WhileAnnoG} @{thm HoareTotal.WhileAnnoG}; val WhileAnnoFix = get_rule @{thm HoarePartial.WhileAnnoFix'} @{thm HoareTotal.WhileAnnoFix'}; val WhileAnnoGFix = get_rule @{thm HoarePartial.WhileAnnoGFix} @{thm HoareTotal.WhileAnnoGFix}; val BindR = get_rule @{thm HoarePartial.Bind} @{thm HoareTotal.Bind}; val Block = get_rule @{thm HoarePartial.Block} @{thm HoareTotal.Block}; val BlockSwap = get_rule @{thm HoarePartial.BlockSwap} @{thm HoareTotal.BlockSwap}; val Proc = get_rule @{thm HoarePartial.ProcSpec} @{thm HoareTotal.ProcSpec}; val ProcNoAbr = get_rule @{thm HoarePartial.ProcSpecNoAbrupt} @{thm HoareTotal.ProcSpecNoAbrupt}; val ProcBody = get_rule @{thm HoarePartial.ProcBody} @{thm HoareTotal.ProcBody}; val CallBody = get_rule @{thm HoarePartial.CallBody} @{thm HoareTotal.CallBody}; val FCall = get_rule @{thm HoarePartial.FCall} @{thm HoareTotal.FCall}; val ProcRecSpecs = get_rule @{thm HoarePartial.ProcRecSpecs} @{thm HoareTotal.ProcRecSpecs}; val ProcModifyReturnSameFaults = get_rule @{thm HoarePartial.ProcModifyReturnSameFaults} @{thm HoareTotal.ProcModifyReturnSameFaults}; val ProcModifyReturn = get_rule @{thm HoarePartial.ProcModifyReturn} @{thm HoareTotal.ProcModifyReturn}; val ProcModifyReturnNoAbr = get_rule @{thm HoarePartial.ProcModifyReturnNoAbr} @{thm HoareTotal.ProcModifyReturnNoAbr}; val ProcModifyReturnNoAbrSameFaultsPartial = @{thm HoarePartial.ProcModifyReturnNoAbrSameFaults}; val ProcModifyReturnNoAbrSameFaultsTotal = @{thm HoareTotal.ProcModifyReturnNoAbrSameFaults}; val ProcModifyReturnNoAbrSameFaults = get_rule ProcModifyReturnNoAbrSameFaultsPartial ProcModifyReturnNoAbrSameFaultsTotal; val TrivPost = get_rule @{thm HoarePartial.TrivPost} @{thm HoareTotal.TrivPost}; val TrivPostNoAbr = get_rule @{thm HoarePartial.TrivPostNoAbr} @{thm HoareTotal.TrivPostNoAbr}; val DynProcProcPar = get_rule @{thm HoarePartial.DynProcProcPar} @{thm HoareTotal.DynProcProcPar}; val DynProcProcParNoAbr = get_rule @{thm HoarePartial.DynProcProcParNoAbrupt} @{thm HoareTotal.DynProcProcParNoAbrupt}; val ProcProcParModifyReturn = get_rule @{thm HoarePartial.ProcProcParModifyReturn} @{thm HoareTotal.ProcProcParModifyReturn}; val ProcProcParModifyReturnSameFaultsPartial = @{thm HoarePartial.ProcProcParModifyReturnSameFaults}; val ProcProcParModifyReturnSameFaultsTotal = @{thm HoareTotal.ProcProcParModifyReturnSameFaults}; val ProcProcParModifyReturnSameFaults = get_rule ProcProcParModifyReturnSameFaultsPartial ProcProcParModifyReturnSameFaultsTotal; val ProcProcParModifyReturnNoAbr = get_rule @{thm HoarePartial.ProcProcParModifyReturnNoAbr} @{thm HoareTotal.ProcProcParModifyReturnNoAbr}; val ProcProcParModifyReturnNoAbrSameFaultsPartial = @{thm HoarePartial.ProcProcParModifyReturnNoAbrSameFaults}; val ProcProcParModifyReturnNoAbrSameFaultsTotal = @{thm HoareTotal.ProcProcParModifyReturnNoAbrSameFaults}; val ProcProcParModifyReturnNoAbrSameFaults = get_rule ProcProcParModifyReturnNoAbrSameFaultsPartial ProcProcParModifyReturnNoAbrSameFaultsTotal; val DynCom = get_rule @{thm HoarePartial.DynComConseq} @{thm HoareTotal.DynComConseq}; val AugmentContext = get_rule @{thm HoarePartial.augment_context'} @{thm HoareTotal.augment_context'}; val AugmentEmptyFaults = get_rule @{thm HoarePartial.augment_emptyFaults} @{thm HoareTotal.augment_emptyFaults}; val AsmUN = get_rule @{thm HoarePartial.AsmUN} @{thm HoareTotal.AsmUN}; val SpecAnno = get_rule @{thm HoarePartial.SpecAnno'} @{thm HoareTotal.SpecAnno'}; val SpecAnnoNoAbrupt = get_rule @{thm HoarePartial.SpecAnnoNoAbrupt} @{thm HoareTotal.SpecAnnoNoAbrupt}; val LemAnno = get_rule @{thm HoarePartial.LemAnno} @{thm HoareTotal.LemAnno}; val LemAnnoNoAbrupt = get_rule @{thm HoarePartial.LemAnnoNoAbrupt} @{thm HoareTotal.LemAnnoNoAbrupt}; val singleton_conv_sym = @{thm Set.singleton_conv2} RS sym; val anno_defs = [@{thm Language.whileAnno_def},@{thm Language.whileAnnoG_def},@{thm Language.specAnno_def}, @{thm Language.whileAnnoGFix_def},@{thm Language.whileAnnoFix_def},@{thm Language.lem_def}]; val strip_simps = @{thm Language.strip_simp} :: @{thm Option.option.map(2)} :: @{thms Language.strip_guards_simps}; val normalize_simps = [@{thm Language.while_def}, @{thm Language.bseq_def}, @{thm List.append_Nil}, @{thm List.append_Cons}] @ @{thms List.list.cases} @ @{thms Language.flatten_simps} @ @{thms Language.sequence.simps} @ @{thms Language.normalize_simps} @ @{thms Language.guards.simps} @ [@{thm fst_conv}, @{thm snd_conv}]; val K_rec_convs = []; val K_fun_convs = [@{thm StateFun.K_statefun_apply}, @{thm StateFun.K_statefun_comp}]; val K_convs = K_rec_convs @ K_fun_convs; val K_rec_congs = []; val K_fun_congs = [@{thm StateFun.K_statefun_cong}]; val K_congs = K_rec_congs @ K_fun_congs; (* misc. aux. functions *) (* first_subterm * yields result x of P for first subterm for which P is (SOME x), and all bound variables on the path * to that term *) fun first_subterm_dest P = let fun first abs_vars t = (case P t of SOME x => SOME (abs_vars,x) |_=> (case t of u $ v => (case first abs_vars u of NONE => first abs_vars v | SOME x => SOME x) | Abs (c,T,u) => first (abs_vars @ [(c,T)]) u | _ => NONE)) in first [] end; (* first_subterm * yields first subterm for which P holds, and all bound variables on the path * to that term *) fun first_subterm P = let fun P' t = if P t then SOME t else NONE; in first_subterm_dest P' end; (* max_subterm_dest * yields results of P for all maximal subterms for which P is (SOME x), * and all bound variables on the path to that subterm *) fun max_subterms_dest P = let fun collect abs_vars t = (case P t of SOME x => [(abs_vars,x)] |_=> (case t of u $ v => collect abs_vars u @ collect abs_vars v | Abs (c,T,u) => collect (abs_vars @ [(c,T)]) u | _ => [])) in collect [] end; fun last [] = raise Empty | last [x] = x | last (_::xs) = last xs; fun dest_splits (Const (@{const_name case_prod},_)$Abs (n,T,t)) = (n,T)::dest_splits t | dest_splits (Const (@{const_name case_prod},_)$Abs (n,T,t)$_) = (n,T)::dest_splits t | dest_splits (Abs (n,T,_)) = [(n,T)] | dest_splits _ = []; fun idx eq [] x = ~1 | idx eq (x::rs) y = if eq x y then 0 else let val i = idx eq rs y in if i < 0 then i else i+1 end; fun resuffix sfx1 sfx2 s = suffix sfx2 (unsuffix sfx1 s) handle Fail _ => s; (* state space representation dependent functions *) datatype state_kind = Record | Function fun state_simprocs Record = [Record.simproc] | state_simprocs Function = [Record.simproc, StateFun.lookup_simproc]; fun state_upd_simproc Record = Record.upd_simproc | state_upd_simproc Function = StateFun.update_simproc; fun state_ex_sel_eq_simproc Record = Record.ex_sel_eq_simproc | state_ex_sel_eq_simproc Function = StateFun.ex_lookup_eq_simproc; val state_split_simp_tac = Record.split_simp_tac val state_hierarchy = Record.dest_recTs fun stateT_id T = case (state_hierarchy T) of [] => NONE | Ts => SOME (last Ts); fun globalsT (Type (_, T :: _)) = SOME T | globalsT _ = NONE; fun stateT_ids T = (case stateT_id T of NONE => NONE | SOME sT => (case globalsT T of NONE => SOME [sT] | SOME gT => (case stateT_id gT of NONE => SOME [sT] | SOME gT' => SOME [sT,gT']))); datatype par_kind = In | Out (*** utilities ***) (* utils for variable name decorations *) val deco = "_'"; val proc_deco = "_'proc"; fun par_deco name = deco ^ name ^ deco; fun chopsfx sfx str = (case try (unsuffix sfx) str of SOME s => s | NONE => str) val is_state_var = can (unsuffix deco); (* removes the suffix of the string beginning with deco. * "xys_'a" --> "xys"; * The a is also chopped, since sometimes the bound variables * are renamed, I think SELECT_GOAL in rename_goal is to blame *) fun remdeco' str = let fun chop (p::ps) (x::xs) = chop ps xs | chop [] xs = [] | chop (p::ps) [] = error "remdeco: code should never be reached"; fun remove prf (s as (x::xs)) = if is_prefix (op =) prf s then chop prf s else (x::remove prf xs) | remove prf [] = []; in String.implode (remove (String.explode deco) (String.explode str)) end; fun extern ctxt s = (case try (Proof_Context.extern_const ctxt o Lexicon.unmark_const) s of NONE => s | SOME s' => s'); fun remdeco ctxt s = remdeco' (extern ctxt s); fun undeco ctxt (Const (c, T)) = Const (remdeco ctxt c, T) | undeco ctxt ((f as Const (@{syntax_const "_free"},_)) $ Free (x, T)) = (*f$*)Const (remdeco' x, T) | undeco ctxt (Const _ $ _ $ ((Const (@{syntax_const "_free"},_)) $ Free (x, T))) = (*f$*)Const (remdeco' x, T) | undeco ctxt (Free (c, T)) = Const (remdeco' c, T) | undeco ctxt x = x fun varname x = x ^ deco val dest_string = map (chr o HOLogic.dest_char) o HOLogic.dest_list; fun dest_string' t = (case try dest_string t of SOME s => implode s | NONE => (case t of Free (s,_) => s | Const (s,_) => Long_Name.base_name s | _ => raise TERM ("dest_string'",[t]))) fun is_state_space_var Tids t = let fun is_stateT T = (case stateT_id T of NONE => 0 | SOME id => if member (op =) Tids id then ~1 else 0); in (case t of Const _ $ Abs (_,T,_) => is_stateT T | Free (_,T) => is_stateT T | _ => 0) end; datatype callMode = Static | Parameter fun proc_name Static (Const (p,_)$_) = resuffix deco proc_deco (Long_Name.base_name p) | proc_name Static (Const (@{const_name StateFun.lookup},_)$_$Free (p,_)$_) = suffix proc_deco (remdeco' (Long_Name.base_name p)) | proc_name Static p = dest_string' p | proc_name Parameter (Const (p,_)) = resuffix deco proc_deco (Long_Name.base_name p) | proc_name Parameter (Abs (_,_,Const (p,_)$Bound 0)) = resuffix deco proc_deco (Long_Name.base_name p) | proc_name Parameter (Abs (_,_,Const (@{const_name StateFun.lookup},_)$_$Free (p,_)$_)) = suffix proc_deco (remdeco' (Long_Name.base_name p)) | proc_name _ t = raise TERM ("proc_name",[t]); fun dest_call (Const (@{const_name Language.call},_)$init$pname$return$c) = (init,pname,return,c,Static,true) | dest_call (Const (@{const_name Language.fcall},_)$init$pname$return$_$c) = (init,pname,return,c,Static,true) | dest_call (Const (@{const_name Language.com.Call},_)$pname) = (Bound 0,pname,Bound 0,Bound 0,Static,false) | dest_call (Const (@{const_name Language.dynCall},_)$init$pname$return$c) = (init,pname,return,c,Parameter,true) | dest_call t = raise TERM ("Hoare.dest_call: unexpected term",[t]); fun dest_whileAnno (Const (@{const_name Language.whileAnnoG},_) $gs$b$I$V$c) = (SOME gs,b,I,V,c,false) | dest_whileAnno (Const (@{const_name Language.whileAnno},_) $b$I$V$c) = (NONE,b,I,V,c,false) | dest_whileAnno (Const (@{const_name Language.whileAnnoGFix},_)$gs$b$I$V$c) = (SOME gs,b,I,V,c,true) | dest_whileAnno (Const (@{const_name Language.whileAnnoFix},_) $b$I$V$c) = (NONE,b,I,V,c,true) | dest_whileAnno t = raise TERM ("Hoare.dest_while: unexpected term",[t]); fun dest_Guard (Const (@{const_name Language.com.Guard},_)$f$g$c) = (f,g,c,false) | dest_Guard (Const (@{const_name Language.guaranteeStrip},_)$f$g$c) = (f,g,c,true) | dest_Guard t = raise TERM ("Hoare.dest_guard: unexpected term",[t]); (*** extend theory by procedure definition ***) fun add_declaration name decl thy = thy - |> Named_Target.init name + |> Named_Target.init [] name |> Local_Theory.declaration {syntax = false, pervasive = false} decl |> Local_Theory.exit |> Proof_Context.theory_of; (* data kind 'HOL/hoare' *) type proc_info = {params: ((par_kind * string) list), recursive: bool, state_kind: state_kind} type hoare_tac = (bool -> int -> tactic) -> Proof.context -> hoareMode -> int -> tactic; type hoare_data = {proc_info: proc_info Symtab.table, active_procs: string list list, default_state_kind: state_kind, generate_guard: (stamp * (Proof.context -> term -> term option)), wp_tacs: (string * hoare_tac) list, hoare_tacs: (string * hoare_tac) list, vcg_simps: thm list}; fun make_hoare_data proc_info active_procs default_state_kind generate_guard wp_tacs hoare_tacs vcg_simps = {proc_info = proc_info, active_procs = active_procs, default_state_kind = default_state_kind, generate_guard = generate_guard, wp_tacs = wp_tacs, hoare_tacs = hoare_tacs, vcg_simps = vcg_simps}; structure Hoare_Data = Generic_Data ( type T = hoare_data; val empty = make_hoare_data (Symtab.empty: proc_info Symtab.table) ([]:string list list) (Function) (stamp (),(K (K NONE)): Proof.context -> term -> term option) ([]:(string * hoare_tac) list) ([]:(string * hoare_tac) list) ([]:thm list); val extend = I; (* FIXME exponential blowup due to append !? *) fun merge ({proc_info = proc_info1, active_procs = active_procs1, default_state_kind = _, generate_guard = (stmp1,generate_gaurd1), wp_tacs = wp_tacs1, hoare_tacs = hoare_tacs1, vcg_simps = vcg_simps1}, {proc_info = proc_info2, active_procs = active_procs2, default_state_kind = default_state_kind2, generate_guard = (stmp2, _), wp_tacs = wp_tacs2, hoare_tacs = hoare_tacs2, vcg_simps=vcg_simps2}) : T = if stmp1=stmp2 then make_hoare_data (Symtab.merge (K true) (proc_info1,proc_info2)) (active_procs1 @ active_procs2) (default_state_kind2) (stmp1,generate_gaurd1) (wp_tacs1 @ wp_tacs2) (hoare_tacs1 @ hoare_tacs2) (Thm.merge_thms (vcg_simps1,vcg_simps2)) else error ("Theories have different aux. functions to generate guards") ); val get_data = Hoare_Data.get o Context.Proof; (* access 'params' *) fun mk_free ctxt name = let val ctxt' = Context.proof_of ctxt; val n' = Variable.intern_fixed ctxt' name |> perhaps Long_Name.dest_hidden; val T' = Proof_Context.infer_type ctxt' (n', dummyT) handle ERROR _ => dummyT in (Free (n',T')) end; fun morph_name ctxt phi name = (case Morphism.term phi (mk_free ctxt name) of Free (x,_) => x | _ => name); datatype 'a bodykind = BodyTyp of 'a | BodyTerm of 'a fun set_default_state_kind sk ctxt = let val {proc_info,active_procs,default_state_kind,generate_guard,wp_tacs,hoare_tacs, vcg_simps,...} = Hoare_Data.get ctxt; val data = make_hoare_data proc_info active_procs sk generate_guard wp_tacs hoare_tacs vcg_simps; in Hoare_Data.put data ctxt end; val get_default_state_kind = #default_state_kind o get_data; fun add_active_procs phi ps ctxt = let val {proc_info,active_procs,default_state_kind,generate_guard,wp_tacs,hoare_tacs, vcg_simps,...} = Hoare_Data.get ctxt; val data = make_hoare_data proc_info ((map (morph_name ctxt phi) ps)::active_procs) default_state_kind generate_guard wp_tacs hoare_tacs vcg_simps; in Hoare_Data.put data ctxt end; fun add_hoare_tacs tacs ctxt = let val {proc_info,active_procs, default_state_kind, generate_guard,wp_tacs,hoare_tacs, vcg_simps,...} = Hoare_Data.get ctxt; val data = make_hoare_data proc_info active_procs default_state_kind generate_guard wp_tacs (hoare_tacs@tacs) vcg_simps; in Hoare_Data.put data ctxt end; fun map_vcg_simps f ctxt = let val {proc_info,active_procs,default_state_kind,generate_guard,wp_tacs,hoare_tacs, vcg_simps,...} = Hoare_Data.get ctxt; val data = make_hoare_data proc_info active_procs default_state_kind generate_guard wp_tacs hoare_tacs (f vcg_simps); in Hoare_Data.put data ctxt end; fun thy_attrib f = Thm.declaration_attribute (fn thm => map_vcg_simps (f thm)); val vcg_simpadd = Thm.add_thm val vcg_simpdel = Thm.del_thm val vcg_simp_add = thy_attrib vcg_simpadd; val vcg_simp_del = thy_attrib vcg_simpdel; (* add 'procedure' *) fun mk_proc_info params recursive state_kind = {params=params,recursive=recursive,state_kind=state_kind}; val empty_proc_info = {params=[],recursive=false,state_kind=Record}; fun map_proc_info_params f {params,recursive,state_kind} = mk_proc_info (f params) recursive state_kind; fun map_proc_info_recursive f {params,recursive,state_kind} = mk_proc_info params (f recursive) state_kind; fun map_proc_info_state_kind f {params,recursive,state_kind} = mk_proc_info params recursive (f state_kind); fun add_params phi name frmls ctxt = let val {proc_info,active_procs,default_state_kind,generate_guard,wp_tacs,hoare_tacs, vcg_simps,...} = Hoare_Data.get ctxt; val params = map (apsnd (morph_name ctxt phi)) frmls; val f = map_proc_info_params (K params); val default = f empty_proc_info; val proc_info' = Symtab.map_default (morph_name ctxt phi name,default) f proc_info; val data = make_hoare_data proc_info' active_procs default_state_kind generate_guard wp_tacs hoare_tacs vcg_simps; in Hoare_Data.put data ctxt end; fun get_params name ctxt = Option.map #params (Symtab.lookup (#proc_info (get_data ctxt)) name); fun add_recursive phi name ctxt = let val {proc_info,active_procs,default_state_kind,generate_guard,wp_tacs,hoare_tacs, vcg_simps,...} = Hoare_Data.get ctxt; val f = map_proc_info_recursive (K true); val default = f empty_proc_info; val proc_info'= Symtab.map_default (morph_name ctxt phi name,default) f proc_info; val data = make_hoare_data proc_info' active_procs default_state_kind generate_guard wp_tacs hoare_tacs vcg_simps; in Hoare_Data.put data ctxt end; fun get_recursive name ctxt = Option.map #recursive (Symtab.lookup (#proc_info (get_data ctxt)) name); fun add_state_kind phi name sk ctxt = let val {proc_info,active_procs,default_state_kind,generate_guard,wp_tacs,hoare_tacs, vcg_simps,...} = Hoare_Data.get ctxt; val f = map_proc_info_state_kind (K sk); val default = f empty_proc_info; val proc_info'= Symtab.map_default (morph_name ctxt phi name,default) f proc_info; val data = make_hoare_data proc_info' active_procs default_state_kind generate_guard wp_tacs hoare_tacs vcg_simps; in Hoare_Data.put data ctxt end; fun get_state_kind name ctxt = Option.map #state_kind (Symtab.lookup (#proc_info (get_data ctxt)) name); fun install_generate_guard f ctxt = let val {proc_info,active_procs, default_state_kind, generate_guard,wp_tacs,hoare_tacs, vcg_simps,...} = Hoare_Data.get ctxt; val data = make_hoare_data proc_info active_procs default_state_kind (stamp (), f) wp_tacs hoare_tacs vcg_simps in Hoare_Data.put data ctxt end; fun generate_guard ctxt = snd (#generate_guard (get_data ctxt)) ctxt; fun check_procedures_definition procs thy = let val ctxt = Proof_Context.init_global thy; fun already_defined name = if is_some (get_params name ctxt) then ["procedure " ^ quote name ^ " already defined"] else [] val err_already_defined = maps (already_defined o #1) procs; fun duplicate_procs names = (case duplicates (op =) names of [] => [] | dups => ["Duplicate procedures " ^ commas_quote dups]); val err_duplicate_procs = duplicate_procs (map #1 procs); fun duplicate_pars name pars = (case duplicates (op =) (map fst pars) of [] => [] | dups => ["Duplicate parameters in procedure " ^ quote name ^ ": " ^ commas_quote dups]); val err_duplicate_pars = maps (fn (name,inpars,outpars,locals,_,_,_) => duplicate_pars name (inpars @ locals) @ duplicate_pars name (outpars @ locals)) procs; (* FIXME: Check that no global variables are used as result parameters *) val errs = err_already_defined @ err_duplicate_procs @ err_duplicate_pars; in if null errs then () else error (cat_lines errs) end; fun add_parameter_info phi cname (name,(inpars,outpars,state_kind)) ctxt = let fun par_deco' T = if T = "" then deco else par_deco (cname name); val pars = map (fn (par,T) => (In,suffix (par_deco' T) par)) inpars@ map (fn (par,T) => (Out,suffix (par_deco' T) par)) outpars; val ctxt_decl = ctxt |> add_params phi name pars |> add_state_kind phi name state_kind in ctxt_decl end; fun mk_loc_exp xs = let fun mk_expr s = (s,(("",false),(Expression.Named [],[]))) in (map mk_expr xs,[]) end; val parametersN = "_parameters"; val variablesN = "_variables"; val signatureN = "_signature"; val bodyN = "_body"; val implementationN = "_impl"; val cliqueN = "_clique"; val clique_namesN = "_clique_names"; val NoBodyN = @{const_name Vcg.NoBody}; val statetypeN = "StateType"; val proc_nameT = HOLogic.stringT; fun expression_no_pos (expr, fixes) : Expression.expression = (map (fn (name, inst) => ((name, Position.none), inst)) expr, fixes); fun add_locale name expr elems thy = thy - |> Expression.add_locale (Binding.name name) (Binding.name name) expr elems + |> Expression.add_locale (Binding.name name) (Binding.name name) [] expr elems |> snd |> Local_Theory.exit; fun add_locale' name expr elems thy = thy - |> Expression.add_locale (Binding.name name) (Binding.name name) expr elems + |> Expression.add_locale (Binding.name name) (Binding.name name) [] expr elems ||> Local_Theory.exit; fun add_locale_cmd name expr elems thy = thy - |> Expression.add_locale_cmd (Binding.name name) (Binding.name name) + |> Expression.add_locale_cmd (Binding.name name) (Binding.name name) [] (expression_no_pos expr) elems |> snd |> Local_Theory.exit; fun read_typ thy raw_T env = let val ctxt' = Proof_Context.init_global thy |> fold (Variable.declare_typ o TFree) env; val T = Syntax.read_typ ctxt' raw_T; val env' = Term.add_tfreesT T env; in (T, env') end; fun add_variable_statespaces (cname, (inpars, outpars, locvars)) thy = let val inpars' = if forall (fn (_,T) => T = "") inpars then [] else inpars; val outpars' = if forall (fn (_,T) => T = "") outpars then [] else outpars; fun prep_comp (n, T) env = let val (T', env') = read_typ thy T env handle ERROR msg => cat_error msg ("The error(s) above occurred in component " ^ quote n) in ((n, T'), env') end; val (in_outs,in_out_env) = fold_map prep_comp (distinct (op =) (inpars'@outpars')) []; val (locs,var_env) = fold_map prep_comp locvars in_out_env; val parSP = cname ^ parametersN; val in_outs' = map (apfst (suffix (par_deco cname))) in_outs; val in_out_args = map fst in_out_env; val varSP = cname ^ variablesN; val locs' = map (apfst (suffix (par_deco cname))) locs; val var_args = map fst var_env; in if null inpars' andalso null outpars' andalso null locvars then thy |> add_locale_cmd parSP ([],[]) [] |> Proof_Context.theory_of |> add_locale_cmd varSP ([],[]) [] |> Proof_Context.theory_of else thy |> StateSpace.define_statespace_i (SOME statetypeN) in_out_args parSP [] in_outs' |> StateSpace.define_statespace_i (SOME statetypeN) var_args varSP [((cname, false), ((map TFree in_out_env),parSP,[]))] locs' end; fun intern_locale thy = Locale.intern thy #> perhaps Long_Name.dest_hidden; fun apply_in_context thy lexp f t = let fun name_variant lname = if intern_locale thy lname = lname then lname else name_variant (lname ^ "'"); in thy (* Create a dummy locale in dummy theory just to read the term *) |> add_locale_cmd (name_variant "foo") lexp [] |> (fn ctxt => f ctxt t) end; fun add_abbrev loc mode name spec thy = thy - |> Named_Target.init loc + |> Named_Target.init [] loc |> (fn lthy => let val t = Syntax.read_term (Local_Theory.target_of lthy) spec; in Local_Theory.abbrev mode ((Binding.name name, NoSyn), t) lthy end) |> #2 |> Local_Theory.exit |> Proof_Context.theory_of; exception TOPSORT of string fun topsort less [] = [] | topsort less xs = let fun list_all P xs = fold (fn x => fn b => b andalso P x) xs true; fun split_min n (x::xs) = if n=0 then raise TOPSORT "no minimum in list" else if list_all (less x) xs then (x,xs) else split_min (n-1) (xs@[x]); fun tsort [] = [] | tsort xs = let val (x,xs') = split_min (length xs) xs; in x::tsort xs' end; in tsort xs end; fun clique_name clique = (foldr1 (fn (a,b) => a ^ "_" ^ b) (map (unsuffix proc_deco) clique)); fun error_to_warning msg f thy = f thy handle ERROR msg' => (warning (msg' ^ "\n" ^ msg); thy); fun procedures_definition locname procs thy = let val procs' = map (fn (name,a,b,c,d,e,f) => (suffix proc_deco name,a,b,c,d,e,f)) procs; val _ = check_procedures_definition procs' thy; val name_pars = map (fn (name,inpars,outpars,_,_,_,sk) => (name,(inpars,outpars,sk))) procs'; val name_vars = map (fn (name,inpars,outpars,locals,_,_,_) => (name,(inpars,outpars,locals))) procs'; val name_body = map (fn (name,_,_,_,body,_,_) => (name,body)) procs'; val name_pars_specs = map (fn (name,inpars,outpars,_,_,specs,sk) => (name,(inpars,outpars,sk),specs)) procs'; val names = map #1 procs'; val sk = #7 (hd procs'); val thy = thy |> Context.theory_map (set_default_state_kind sk); val (all_callss,cliques,is_recursive,has_body) = let val ctxt = Context.Theory thy |> fold (add_parameter_info Morphism.identity (unsuffix proc_deco)) name_pars |> StateSpace.set_silent true fun read_body (_, body) = Syntax.read_term (Context.proof_of ctxt) body; val bodies = map read_body name_body; fun dcall t = (case try dest_call t of SOME (_,p,_,_,m,_) => SOME (proc_name m p) | _ => NONE); fun in_names x = if member (op =) names x then SOME x else NONE; fun add_edges n = fold (fn x => Graph.add_edge (n, x)); val all_callss = map (map snd o max_subterms_dest dcall) bodies; val callss = map (map_filter in_names) all_callss; val graph = fold (fn n => Graph.new_node (n, ())) names Graph.empty; val graph' = fold2 add_edges names callss graph; fun idx x = find_index (fn y => x=y) names; fun name_ord (a,b) = int_ord (idx a, idx b); val cliques = Graph.strong_conn graph'; val cliques' = map (sort name_ord) cliques; val my_calls = these o AList.lookup (op =) (names ~~ map (distinct (op =)) callss); val my_body = AList.lookup (op =) (names ~~ bodies); fun is_recursive n = exists (fn [_] => false | ns => member (op =) ns n) (Graph.strong_conn graph'); fun has_body n = (case my_body n of SOME (Const (c,_)) => c <> NoBodyN | _ => true) fun clique_less c1 c2 = null (inter (op =) (distinct (op =) (maps my_calls c1)) c2); val cliques'' = topsort clique_less cliques'; in (all_callss,cliques'',is_recursive,has_body) end; (* cliques may only depend on ones to the left, so it is safe to * add the locales from the left to the right. *) fun my_clique n = Library.find_first (fn c => member (op =) c n) cliques; fun lname sfx clique = suffix sfx (clique_name clique); fun cname n = clique_name (the (my_clique n)); fun parameter_info_decl phi = fold (add_parameter_info phi cname) name_pars; fun get_loc sfx clique n = if member (op =) clique n then NONE else SOME (resuffix proc_deco sfx n); fun parent_locales thy sfx clique = let val calls = distinct (op =) (flat (map_filter (AList.lookup (op =) (names ~~ all_callss)) clique)); in map (intern_locale thy) (distinct (op =) (map_filter (get_loc sfx clique) calls)) end; val names_all_callss = names ~~ map (distinct (op =)) all_callss; val get_calls = the o AList.lookup (op =) names_all_callss; fun clique_vars clique = let fun add name (ins,outs,locs) = let val (nins,nouts,nlocs) = the (AList.lookup (op =) name_vars name) in (ins@nins,outs@nouts,locs@nlocs) end; val (is,os,ls) = fold add clique ([],[],[]); in (lname "" clique, (distinct (op =) is, distinct (op =) os, distinct (op =) ls)) end; fun add_signature_locale (cname, name) thy = let val name' = unsuffix proc_deco name; val fixes = [Element.Fixes [(Binding.name name, SOME proc_nameT, NoSyn)]]; (* FIXME: may use HOLogic.typeT as soon as locale type-inference works properly *) val pE = mk_loc_exp [intern_locale thy (suffix parametersN cname)]; val sN = suffix signatureN name'; in thy |> add_locale sN pE fixes |> Proof_Context.theory_of |> (fn thy => add_declaration (intern_locale thy sN) parameter_info_decl thy) end; fun mk_bdy_def read_term name = let val name' = unsuffix proc_deco name; val bdy = read_term (the (AList.lookup (op =) name_body name)); val bdy_defN = suffix body_def_sfx name'; val b = Binding.name bdy_defN; in ((b, NoSyn), ((Thm.def_binding b, []), bdy)) end; fun add_body_locale (name, _) thy = let val name' = unsuffix proc_deco name; val callees = filter_out (fn n => n = name) (get_calls name) val fixes = [Element.Fixes [(Binding.name name, SOME proc_nameT, NoSyn)]]; (* FIXME: may use HOLogic.typeT as soon as locale type-inference works properly *) val pE = mk_loc_exp (map (intern_locale thy) ([lname variablesN (the (my_clique name))]@ the_list locname@ map (resuffix proc_deco signatureN) callees)); fun def lthy = let val read = Syntax.read_term (Context.proof_map (add_active_procs Morphism.identity (the (my_clique name))) (Local_Theory.target_of lthy)) in mk_bdy_def read name end; fun add_decl_and_def lname ctxt = ctxt |> Proof_Context.theory_of - |> Named_Target.init lname + |> Named_Target.init [] lname |> Local_Theory.declaration {syntax = false, pervasive = false} parameter_info_decl |> (fn lthy => if has_body name then snd (Local_Theory.define (def lthy) lthy) else lthy) |> Local_Theory.exit |> Proof_Context.theory_of; in thy |> add_locale' (suffix bodyN name') pE fixes |-> add_decl_and_def end; fun mk_def_eq thy read_term name = if has_body name then let (* FIXME: All the read_term stuff is just because type-inference/abbrevs for * new locale elements does not work right now; * We read the term to expand the abbreviations, then we print it again * (without folding the abbreviation) and reread as string *) val name' = unsuffix proc_deco name; val bdy_defN = suffix body_def_sfx name'; val rhs = read_term ("Some " ^ bdy_defN); val nt = read_term name; val Free (gamma,_) = read_term programN; val eq = HOLogic.Trueprop$ HOLogic.mk_eq (Free (gamma,fastype_of nt --> fastype_of rhs)$nt,rhs) val consts = Sign.consts_of thy; val eqs = YXML.string_of_body (Term_XML.Encode.term consts (Consts.dummy_types consts eq)); val assms = Element.Assumes [((Binding.name (suffix bodyP name'), []),[(eqs,[])])] in [assms] end else []; fun add_impl_locales clique thy = let val cliqN = lname cliqueN clique; val cnamesN = lname clique_namesN clique; val multiple_procs = length clique > 1; val add_distinct_procs_namespace = if multiple_procs then StateSpace.namespace_definition cnamesN proc_nameT ([],[]) [] clique else I; val bodyLs = map (suffix bodyN o unsuffix proc_deco) clique; fun pE thy = mk_loc_exp (map (intern_locale thy) (hoare_ctxtL::bodyLs) @ (parent_locales thy implementationN clique) @ (if multiple_procs then [intern_locale thy cnamesN] else [])); fun read_term thy = apply_in_context thy (pE thy) Syntax.read_term; fun elems thy = maps (mk_def_eq thy (read_term thy)) clique; fun add_recursive_info phi name = if is_recursive name then (add_recursive phi name) else I; fun proc_declaration phi = add_active_procs phi clique; fun recursive_declaration phi ctxt = ctxt |> fold (add_recursive_info phi) clique; fun add_impl_locale name thy = let val implN = suffix implementationN (unsuffix proc_deco name); val parentN = intern_locale thy cliqN val parent = mk_loc_exp [parentN]; in thy |> add_locale_cmd implN parent [] |> Proof_Context.theory_of |> (fn thy => Interpretation.global_sublocale parentN (mk_loc_exp [intern_locale thy implN]) [] thy) |> Proof.global_terminal_proof ((Method.Basic (fn ctxt => Method.SIMPLE_METHOD (Locale.intro_locales_tac {strict = true, eager = false} ctxt [])), Position.no_range), NONE) |> Proof_Context.theory_of end; in thy |> add_distinct_procs_namespace |> (fn thy => add_locale_cmd cliqN (pE thy) (elems thy) thy) |> Proof_Context.theory_of |> fold add_impl_locale clique |> (fn thy => add_declaration (intern_locale thy cliqN) proc_declaration thy) |> (fn thy => add_declaration (intern_locale thy cliqN) recursive_declaration thy) end; fun add_spec_locales (name, _, specs) thy = let val name' = unsuffix proc_deco name; val ps = (suffix signatureN name' :: the_list locname); val ps' = hoare_ctxtL :: ps ; val pE = mk_loc_exp (map (intern_locale thy) ps) val pE' = mk_loc_exp (map (intern_locale thy) ps') fun read thy = apply_in_context thy (mk_loc_exp [intern_locale thy (suffix cliqueN (cname name))]) (Syntax.read_prop); fun proc_declaration phi = (*parameter_info_decl phi o already in signature *) add_active_procs phi (the (my_clique name)); fun add_locale'' (thm_name,spec) thy = let val spec' = read thy spec; val elem = Element.Assumes [((Binding.name thm_name, []), [(spec', [])])]; in thy |> add_locale thm_name pE' [elem] |> Proof_Context.theory_of |> (fn thy => add_declaration (intern_locale thy thm_name) proc_declaration thy) |> error_to_warning ("abbreviation: '" ^ thm_name ^ "' not added") (add_abbrev (intern_locale thy (suffix cliqueN (cname name))) Syntax.mode_input thm_name spec) end; in thy |> fold add_locale'' specs end; in thy |> fold (add_variable_statespaces o clique_vars) cliques |> fold (fn c => fold (fn n => add_signature_locale (lname "" c, n)) c) cliques |> fold add_body_locale name_pars |> fold add_impl_locales cliques |> fold add_spec_locales name_pars_specs end; (********************* theory extender interface ********************************) (** package setup **) (* outer syntax *) val var_declP = Parse.name -- (@{keyword "::"} |-- Parse.!!! Parse.embedded); val var_declP' = Parse.name >> (fn n => (n,"")); val localsP = Scan.repeat var_declP; val argP = var_declP; val argP' = var_declP'; val not_eqP = Scan.ahead (Scan.unless @{keyword "="} (Scan.one (K true))) val proc_decl_statespace = (Parse.short_ident --| @{keyword "("}) -- ((Parse.list argP) -- (Scan.optional (@{keyword "|"} |-- Parse.list argP) []) --| @{keyword ")"}) --| not_eqP val proc_decl_record = (Parse.short_ident --| @{keyword "("}) -- ((Parse.list argP') -- (Scan.optional (@{keyword "|"} |-- Parse.list argP') []) --| @{keyword ")"}) --| Scan.option @{keyword "="} val proc_decl = proc_decl_statespace >> pair Function || proc_decl_record >> pair Record; val loc_decl = Scan.optional (@{keyword "where"} |-- localsP --| @{keyword "in"}) [] val proc_body = Parse.embedded (*>> BodyTerm*) fun proc_specs x = (Parse.!!! (Scan.repeat (Parse_Spec.thm_name ":" -- Parse.embedded)) >> map (fn ((thm_name, _), prop) => (Binding.name_of thm_name, prop))) x val par_loc = Scan.option (@{keyword "("} |-- @{keyword "imports"} |-- Parse.name --| @{keyword ")"}); val _ = Outer_Syntax.command @{command_keyword procedures} "define procedures" (par_loc -- (Parse.and_list1 (proc_decl -- loc_decl -- proc_body -- proc_specs)) >> (fn (loc,decls) => let val decls' = map (fn ((((state_kind,(name,(ins,outs))),ls),bdy),specs) => (name,ins,outs,ls,bdy,specs,state_kind)) decls in Toplevel.theory (procedures_definition loc decls') end)); val _ = Outer_Syntax.command @{command_keyword hoarestate} "define state space for hoare logic" (StateSpace.statespace_decl >> (fn ((args,name),(parents,comps)) => Toplevel.theory (StateSpace.define_statespace args name parents (map (apfst (suffix deco)) comps)))); (*************************** Auxiliary Functions for integration of ********************) (*************************** automatic program analysers ********************) fun dest_conjs t = (case HOLogic.dest_conj t of [t1,t2] => dest_conjs t1 @ dest_conjs t2 | ts => ts); fun split_guard (Const (@{const_name Collect},CT)$(Abs (s,T,t))) = let fun mkCollect t = Const (@{const_name Collect},CT)$(Abs (s,T,t)); in map mkCollect (dest_conjs t) end | split_guard t = [t]; fun split_guards gs = let fun norm c f g = map (fn g => c$f$g) (split_guard g); fun norm_guard ((c as Const (@{const_name Pair},_))$f$g) = norm c f g | norm_guard ((c as Const (@{const_name Language.guaranteeStripPair},_))$f$g) = norm c f g | norm_guard t = [t]; in maps norm_guard (HOLogic.dest_list gs) end fun fold_com f t = let (* traverse does not descend into abstractions, like in DynCom, call, etc. *) fun traverse cnt (c as Const (@{const_name Language.com.Skip},_)) = (cnt,f cnt c [] []) | traverse cnt ((c as Const (@{const_name Language.com.Basic},_))$g) = (cnt, f cnt c [g] []) | traverse cnt ((c as Const (@{const_name Language.com.Spec},_))$r) = (cnt, f cnt c [r] []) | traverse cnt ((c as Const (@{const_name Language.com.Seq},_))$c1$c2) = let val (cnt1,v1) = traverse cnt c1; val (cnt2,v2) = traverse cnt1 c2; in (cnt2, f cnt c [] [v1,v2]) end | traverse cnt ((c as Const (@{const_name Language.com.Cond},_))$b$c1$c2) = let val (cnt1,v1) = traverse cnt c1; val (cnt2,v2) = traverse cnt1 c2; in (cnt2, f cnt c [b] [v1,v2]) end | traverse cnt ((c as Const (@{const_name Language.com.While},_))$b$c1) = let val (cnt1,v1) = traverse cnt c1 in (cnt1, f cnt c [b] [v1]) end | traverse cnt ((c as Const (@{const_name Language.com.Call},_))$p) = (cnt, f cnt c [p] []) | traverse cnt ((c as Const (@{const_name Language.com.DynCom},_))$c1) = (cnt, f cnt c [c1] []) | traverse cnt ((c as Const (@{const_name Language.com.Guard},_))$flt$g$c1) = let val (cnt1,v1) = traverse (cnt + length (split_guard g)) c1 in (cnt1, f cnt c [flt,g] [v1]) end | traverse cnt (c as Const (@{const_name Language.com.Throw},_)) = (cnt,f cnt c [] []) | traverse cnt ((c as Const (@{const_name Language.com.Catch},_))$c1$c2) = let val (cnt1,v1) = traverse cnt c1; val (cnt2,v2) = traverse cnt1 c2; in (cnt2, f cnt c [] [v1,v2]) end | traverse cnt ((c as Const (@{const_name Language.guards},_))$gs$c1) = let val (cnt1,v1) = traverse (cnt + length (split_guards gs)) c1; in (cnt1, f cnt c [gs] [v1]) end | traverse cnt ((c as Const (@{const_name Language.block},_))$init$c1$return$c2) = let val (cnt1,v1) = traverse cnt c1 in (cnt1, f cnt c [init,return,c2] [v1]) end | traverse cnt ((c as Const (@{const_name Language.call},_))$init$p$return$c1) = (cnt, f cnt c [init,p,return,c1] []) | traverse cnt ((c as Const (@{const_name Language.whileAnno},_))$b$I$V$c1) = let val (cnt1,v1) = traverse cnt c1 in (cnt1, f cnt c [b,I,V] [v1]) end | traverse cnt ((c as Const (@{const_name Language.whileAnnoG},_))$gs$b$I$V$c1) = let val (cnt1,v1) = traverse (cnt + length (split_guards gs)) c1 in (cnt1, f cnt c [gs,b,I,V] [v1]) end | traverse _ t = raise TERM ("fold_com: unknown command",[t]); in snd (traverse 0 t) end; (*************************** Tactics ****************************************************) (*** Aux. tactics ***) fun cond_rename_bvars cond name thm = let fun rename (tm as (Abs (x, T, t))) = if cond tm then Abs (name x, T, rename t) else Abs (x, T, rename t) | rename (t $ u) = rename t $ rename u | rename a = a; in Thm.renamed_prop (rename (Thm.prop_of thm)) thm end; val rename_bvars = cond_rename_bvars (K true); fun trace_tac ctxt str st = (if Config.get ctxt hoare_trace then tracing str else (); all_tac st); fun error_tac str st = (error str;no_tac st); fun rename_goal ctxt name = EVERY' [K (trace_tac ctxt "rename_goal -- START"), SELECT_GOAL (PRIMITIVE (rename_bvars name)), K (trace_tac ctxt "rename_goal -- STOP")]; (* splits applications of tupled arguments to a schematic Variables, e.g. * ALL a b. ?P (a,b) --> ?Q (a,b) gets * ALL a b. ?P a b --> ?Q a b * only tuples nested to the right are splitted. *) fun split_pair_apps ctxt thm = let val t = Thm.prop_of thm; fun mk_subst subst (Abs (x,T,t)) = mk_subst subst t | mk_subst subst (t as (t1$t2)) = (case strip_comb t of (var as Var (v,vT),args) => (if not (AList.defined (op =) subst var) then let val len = length args; val (argTs,bdyT) = strip_type vT; val (z, _) = Name.variant "z" (fold Term.declare_term_frees args Name.context); val frees = map (apfst (fn i => z^string_of_int i)) (0 upto (len - 1) ~~ argTs); fun splitT (Type (@{type_name Product_Type.prod}, [T1, T2])) = T1::splitT T2 | splitT T = [T]; fun pair_depth (Const (@{const_name Pair},aT)$t1$t2) = 1 + (pair_depth t2) | pair_depth _ = 0; fun mk_sel max free i = let val snds = funpow i HOLogic.mk_snd (Free free) in if i=max then snds else HOLogic.mk_fst snds end; fun split (free,arg) = let val depth = (pair_depth arg); in if depth = 0 then [Free free] else map (mk_sel depth free) (0 upto depth) end; val args' = maps split (frees ~~ args); val argTs' = maps splitT argTs; val inst = fold_rev absfree frees (list_comb (Var (v,argTs' ---> bdyT), args')) in subst@[(var,inst)] end else subst) | _ => mk_subst (mk_subst subst t1) t2) | mk_subst subst t = subst; val subst = map (fn (v,t) => (dest_Var v, Thm.cterm_of ctxt t)) (mk_subst [] t); in full_simplify (put_simpset HOL_basic_ss ctxt addsimps [@{thm fst_conv}, @{thm snd_conv}]) (Drule.instantiate_normalize ([],subst) thm) end; (* Generates split theorems, for !!,!,? quantifiers and for UN, e.g. * ALL x. P x = ALL a b. P a b *) fun mk_split_thms ctxt (vars as _::_) = let val thy = Proof_Context.theory_of ctxt; val names = map fst vars; val types = map snd vars; val free_vars = map Free vars; val pT = foldr1 HOLogic.mk_prodT types; val x = (singleton (Name.variant_list names) "x", pT); val xp = foldr1 HOLogic.mk_prod free_vars; val tfree_names = fold Term.add_tfree_names free_vars []; val zeta = TFree (singleton (Name.variant_list tfree_names) "z", Sign.defaultS thy); val split_meta_prop = let val P = Free (singleton (Name.variant_list names) "P", pT --> Term.propT) in Logic.mk_equals (Logic.all (Free x) (P $ Free x), fold_rev Logic.all free_vars (P $ xp)) end; val P = Free (singleton (Name.variant_list names) "P", pT --> HOLogic.boolT); val split_object_prop = let fun ALL vs t = Library.foldr (fn ((v,T),t) => HOLogic.mk_all (v,T,t)) (vs,t) in (ALL [x] (P $ Free x)) === (ALL vars (P $ xp)) end; val split_ex_prop = let fun EX vs t = Library.foldr (fn ((v,T),t) => HOLogic.mk_exists (v,T,t)) (vs,t) in (EX [x] (P $ Free x)) === (EX vars (P $ xp)) end; val split_UN_prop = let val P = Free (singleton (Name.variant_list names) "P", pT --> HOLogic.mk_setT zeta); fun UN vs t = Library.foldr mk_UN (vs, t) in (UN [x] (P $ Free x)) === (UN vars (P $ xp)) end; fun prove_simp simps prop = let val ([prop'], _) = Variable.importT_terms [prop] ctxt (* FIXME continue context!? *) in Goal.prove_global thy [] [] prop' (fn {context = ctxt, ...} => ALLGOALS (simp_tac (put_simpset HOL_basic_ss ctxt addsimps simps))) end; val split_meta = prove_simp [@{thm split_paired_all}] split_meta_prop; val split_object = prove_simp [@{thm split_paired_All}] split_object_prop; val split_ex = prove_simp [@{thm split_paired_Ex}] split_ex_prop; val split_UN = prove_simp [@{thm Hoare.split_paired_UN}] split_UN_prop; in [split_meta,split_object,split_ex,split_UN] end | mk_split_thms _ _ = raise Match; fun rename_aux_var name rule = let fun is_aux_var (Abs ("Z",TVar(_,_),_)) = true | is_aux_var _ = false; in cond_rename_bvars is_aux_var (K name) rule end; (* adapts single auxiliary variable in a rule to potentialy multiple auxiliary * variables in actual specification, e.g. if vars are a b, * split_app=false: ALL Z. ?P Z gets to ALL a b. ?P (a,b) * split_app=true: ALL Z. ?P Z gets to ALL a b. ?P a b * If only one auxiliary variable is given, the variables are just renamed, * If no auxiliary is given, unit is inserted for Z: * ALL Z. ?P Z gets P () *) fun adapt_aux_var ctxt split_app (vars as (_::_::_)) tvar_rules = let val thy = Proof_Context.theory_of ctxt; val max_idx = fold Integer.max (map (Thm.maxidx_of o snd) tvar_rules) 0; val types = map (fn i => TVar (("z",i),Sign.defaultS thy)) (max_idx + 1 upto (max_idx + length vars)); fun tvar n = (n, Sign.defaultS thy); val pT = Thm.ctyp_of ctxt (foldr1 HOLogic.mk_prodT types); val rules' = map (fn (z,r) => (Drule.instantiate_normalize ([(tvar z,pT)],[]) r)) tvar_rules; val splits = mk_split_thms ctxt (vars ~~ types); val rules'' = map (full_simplify (put_simpset HOL_basic_ss ctxt addsimps splits)) rules'; in if split_app then (map (split_pair_apps ctxt) rules'') else rules'' end | adapt_aux_var _ _ ([name]) tvar_rules = map (rename_aux_var name o snd) tvar_rules | adapt_aux_var ctxt _ ([]) tvar_rules = let val thy = Proof_Context.theory_of ctxt; fun tvar n = (n, Sign.defaultS thy); val uT = Thm.ctyp_of ctxt HOLogic.unitT; val rules' = map (fn (z,r) => (Drule.instantiate_normalize ([(tvar z,uT)],[]) r)) tvar_rules; val splits = [@{thm Hoare.unit_meta},@{thm Hoare.unit_object},@{thm Hoare.unit_ex},@{thm Hoare.unit_UN}]; val rules'' = map (full_simplify (put_simpset HOL_basic_ss ctxt addsimps splits)) rules'; in rules'' end (* Generates a rule for recursion for n procedures out of general recursion rule *) fun gen_call_rec_rule ctxt specs_name n rule = let val thy = Proof_Context.theory_of ctxt; val maxidx = Thm.maxidx_of rule; val vars = Term.add_vars (Thm.prop_of rule) []; fun get_type n = the (AList.lookup (op =) vars (n, 0)); val (Type (_, [Type (_, [assT, Type (_, [pT,_])])])) = get_type specs_name; val zT = TVar (("z",maxidx+1),Sign.defaultS thy) fun mk_var i n T = Var ((n ^ string_of_int i,0),T); val quadT = HOLogic.mk_prodT (assT, HOLogic.mk_prodT (pT, HOLogic.mk_prodT (assT,assT))); val quadT_set = HOLogic.mk_setT quadT; fun mk_spec i = let val quadruple = HOLogic.mk_ptuple (HOLogic.flat_tupleT_paths quadT) quadT [mk_var i "P" (zT --> assT)$Bound 0, mk_var i "p" pT, mk_var i "Q" (zT --> assT)$Bound 0, mk_var i "A" (zT --> assT)$Bound 0]; val single = HOLogic.mk_set quadT [quadruple]; in mk_UN' zT quadT_set (Abs ("Z", zT, single)) end; val Specs = foldr1 (mk_Un quadT_set) (map mk_spec (1 upto n)); val rule' = Thm.instantiate' [] [SOME (Thm.cterm_of ctxt Specs)] rule |> full_simplify (put_simpset (simpset_of @{theory_context Main}) ctxt addsimps [@{thm Hoare.conjE_simp},@{thm Hoare.in_Specs_simp},@{thm Hoare.in_set_Un_simp},@{thm split_all_conj}, @{thm image_Un},@{thm image_Un_single_simp}] ) |> rename_bvars (fn s => if member (op =) ["s","\"] s then s else "Z") in rule' end; fun gen_proc_rec ctxt mode n = gen_call_rec_rule ctxt "Specs" n (ProcRecSpecs mode); (*** verification condition generator ***) (* simplifications on "Collect" sets, like {s. P s} Int {s. Q s} = {s. P s & Q s} *) fun merge_assertion_simp_tac ctxt thms = simp_tac (put_simpset HOL_basic_ss ctxt addsimps ([@{thm Hoare.CollectInt_iff},@{thm HOL.conj_assoc},@{thm Hoare.Compl_Collect},singleton_conv_sym, @{thm Set.Int_empty_right},@{thm Set.Int_empty_left},@{thm Un_empty_right},@{thm Un_empty_left}]@thms)) ; (* The following probably shouldn't live here, but refactoring so that Hoare could depend on recursive_records does not look feasible. The upshot is that there's a duplicate foldcong_ss set here. *) structure FoldCongData = Theory_Data ( type T = simpset; val empty = HOL_basic_ss; val copy = I; val extend = I; val merge = merge_ss; ) val get_foldcong_ss = FoldCongData.get fun add_foldcongs congs thy = FoldCongData.map (fn ss => Proof_Context.init_global thy |> put_simpset ss |> fold Simplifier.add_cong congs |> simpset_of) thy fun add_foldcongsimps simps thy = FoldCongData.map (fn ss => Proof_Context.init_global thy |> put_simpset ss |> (fn ctxt => ctxt addsimps simps) |> simpset_of) thy (* propagates state into "Collect" sets and simplifies selections updates like: * s:{s. P s} = P s *) fun in_assertion_simp_tac ctxt state_kind thms i = let val vcg_simps = #vcg_simps (get_data ctxt); val fold_simps = get_foldcong_ss (Proof_Context.theory_of ctxt) in EVERY [simp_tac (put_simpset HOL_basic_ss ctxt addsimps ([mem_Collect_eq,@{thm Set.Un_iff},@{thm Set.Int_iff}, @{thm Set.empty_subsetI}, @{thm Set.empty_iff}, UNIV_I, @{thm Hoare.Collect_False}]@thms@K_convs@vcg_simps) addsimprocs (state_simprocs state_kind) |> fold Simplifier.add_cong K_congs) i THEN_MAYBE (simp_tac (put_simpset fold_simps ctxt addsimprocs [state_upd_simproc state_kind]) i) ] end; fun assertion_simp_tac ctxt state_kind thms i = merge_assertion_simp_tac ctxt [] i THEN_MAYBE in_assertion_simp_tac ctxt state_kind thms i (* simplify equality test on strings (and datatype-constructors) and propagate result*) fun string_eq_simp_tac ctxt = simp_tac (put_simpset HOL_basic_ss ctxt addsimps @{thms list.inject list.distinct char.inject cong_exp_iff_simps simp_thms}); fun assertion_string_eq_simp_tac ctxt state_kind thms i = assertion_simp_tac ctxt state_kind thms i THEN_MAYBE string_eq_simp_tac ctxt i; fun before_set2pred_simp_tac ctxt = (simp_tac (put_simpset HOL_basic_ss ctxt addsimps [singleton_conv_sym, @{thm Hoare.CollectInt_iff}, @{thm Hoare.Compl_Collect}])); (*****************************************************************************) (** set2pred transforms sets inclusion into predicates implication, **) (** maintaining the original variable names. **) (** Ex. "{x. x=0} <= {x. x <= 1}" -set2pred-> "x=0 --> x <= 1" **) (** Subgoals containing intersections (A Int B) or complement sets (-A) **) (** are first simplified by "before_set2pred_simp_tac", that returns only **) (** subgoals of the form "{x. P x} <= {x. Q x}", which are easily **) (** transformed. **) (** This transformation may solve very easy subgoals due to a ligth **) (** simplification done by full_simp_tac **) (*****************************************************************************) fun set2pred_tac ctxt i thm = ((before_set2pred_simp_tac ctxt i) THEN_MAYBE (EVERY [trace_tac ctxt "set2pred", resolve_tac ctxt [subsetI] i, resolve_tac ctxt [CollectI] i, dresolve_tac ctxt [CollectD] i, full_simp_tac (put_simpset HOL_basic_ss ctxt) i ])) thm (*****************************************************************************) (** BasicSimpTac is called to simplify all verification conditions. It does **) (** a light simplification by applying "mem_Collect_eq" **) (** then it tries to solve subgoals of the form "A <= A" and then if **) (** set2pred is true it **) (** transforms any other into predicates, applying then **) (** the tactic chosen by the user, which may solve the subgoal completely **) (** (MaxSimpTac). **) (*****************************************************************************) fun MaxSimpTac ctxt tac i = TRY (FIRST[resolve_tac ctxt [subset_refl] i, set2pred_tac ctxt i THEN_MAYBE tac i, trace_tac ctxt "final_tac failed" ]); fun BasicSimpTac ctxt state_kind set2pred thms tac i = EVERY [(trace_tac ctxt "BasicSimpTac -- START --"), assertion_simp_tac ctxt state_kind thms i THEN_MAYBE (if set2pred then MaxSimpTac ctxt tac i else TRY (resolve_tac ctxt [subset_refl] i)), (trace_tac ctxt "BasicSimpTac -- STOP --")]; (* EVERY [(trace_tac ctxt "BasicSimpTac -- START --"), simp_tac (HOL_basic_ss addsimps [mem_Collect_eq,@{thm Hoare.CollectInt_iff}, @{thm Set.empty_subsetI}, @{thm Set.empty_iff}, UNIV_I] addsimprocs [state_simproc sk]) i THEN_MAYBE simp_tac (HOL_basic_ss addsimprocs [state_upd_simproc sk]) i THEN_MAYBE (if set2pred then MaxSimpTac ctxt tac i else TRY (rtac subset_refl i)), (trace_tac ctxt "BasicSimpTac -- STOP --")]; *) (* fun simp_state_eq_tac Record state_space = full_simp_tac (HOL_basic_ss addsimprocs (state_simprocs Record)) THEN_MAYBE' full_simp_tac (HOL_basic_ss addsimprocs [state_upd_simproc Record]) THEN_MAYBE' (state_split_simp_tac [] state_space) | simp_state_eq_tac StateFun state_space = *) fun post_conforms_tac ctxt state_kind i = EVERY [REPEAT1 (resolve_tac ctxt [allI,impI] i), ((fn i => TRY (resolve_tac ctxt [conjI] i)) THEN_ALL_NEW (fn i => (REPEAT (resolve_tac ctxt [allI,impI] i)) THEN (full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps [mem_Collect_eq,@{thm Set.singleton_iff},@{thm Set.empty_iff},UNIV_I] addsimprocs (state_simprocs state_kind)) i))) i]; fun dest_hoare_raw (Const(@{const_name HoarePartialDef.hoarep},_)$G$T$F$P$C$Q$A) = (P,C,Q,A,Partial,G,T,F) | dest_hoare_raw (Const(@{const_name HoareTotalDef.hoaret},_)$G$T$F$P$C$Q$A) = (P,C,Q,A,Total,G,T,F) | dest_hoare_raw t = raise TERM ("Hoare.dest_hoare_raw: unexpected term",[t]) fun mk_hoare_abs Ts (P,C,Q,A,mode,G,T,F) = let val hoareT = map (curry fastype_of1 Ts) [G,T,F,P,C,Q,A] ---> HOLogic.boolT; val hoareC = (case mode of Partial => Const (@{const_name HoarePartialDef.hoarep},hoareT) | Total => Const (@{const_name HoareTotalDef.hoaret},hoareT)); in hoareC$G$T$F$P$C$Q$A end; val is_hoare = can dest_hoare_raw fun dest_hoare t = let val triple = (strip_qnt_body @{const_name "All"} o HOLogic.dest_Trueprop o strip_qnt_body @{const_name Pure.all}) t; in dest_hoare_raw triple end; fun get_aux_tvar rule = let fun aux_hoare (Abs ("Z",TVar (z,_),t)) = if is_hoare (strip_qnt_body @{const_name All} t) then SOME z else NONE | aux_hoare _ = NONE; in (case first_subterm_dest (aux_hoare) (Thm.prop_of rule) of SOME (_,z) => (z,rule) | NONE => raise TERM ("get_aux_tvar: No auxiliary variable of hoare-rule found", [Thm.prop_of rule])) end; fun strip_vars t = let val bdy = (HOLogic.dest_Trueprop o Logic.strip_assums_concl) t; in strip_qnt_vars @{const_name Pure.all} t @ strip_qnt_vars @{const_name All} bdy end; local (* ex_simps are necessary in case of multiple logical variables. The state will usually be the first variable. EX s a b. s=s' ... . We have to transport EX s to s=s' to perform the substitution *) val conseq1_ss_base = simpset_of (put_simpset HOL_basic_ss @{context} addsimps ([mem_Collect_eq,@{thm Set.singleton_iff},@{thm Set.Int_iff}, @{thm Set.empty_iff},UNIV_I, @{thm HOL.conj_assoc}, @{thm disj_assoc}] @ @{thms Hoare.all_imp_eq_triv} @K_convs @ @{thms simp_thms} @ @{thms ex_simps} @ @{thms all_simps}) delsimps [@{thm Hoare.all_imp_to_ex}] |> fold Simplifier.add_cong K_congs) val conseq1_ss_record = simpset_of (put_simpset conseq1_ss_base @{context} addsimprocs (state_simprocs Record)); val conseq1_ss_fun = simpset_of (put_simpset conseq1_ss_base @{context} addsimprocs (state_simprocs Function)); fun conseq1_ss Record = conseq1_ss_record | conseq1_ss Function = conseq1_ss_fun; val conseq2_ss_base = simpset_of (put_simpset HOL_basic_ss @{context} addsimps (@{thms Hoare.all_imp_eq_triv} @ @{thms simp_thms} @ @{thms ex_simps} @ @{thms all_simps}) delsimps [@{thm Hoare.all_imp_to_ex}] |> Simplifier.add_cong @{thm imp_cong}); val conseq2_ss_record = simpset_of (put_simpset conseq2_ss_base @{context} addsimprocs [state_upd_simproc Record, state_ex_sel_eq_simproc Record]); val conseq2_ss_fun = simpset_of (put_simpset conseq2_ss_base @{context} addsimprocs [state_upd_simproc Function, state_ex_sel_eq_simproc Function]); fun conseq2_ss Record = conseq2_ss_record | conseq2_ss Function = conseq2_ss_fun; in fun raw_conseq_simp_tac ctxt state_kind thms i = let val ctxt' = Config.put simp_depth_limit 0 ctxt; in simp_tac (put_simpset (conseq1_ss state_kind) ctxt' addsimps thms) i THEN_MAYBE simp_tac (put_simpset (conseq2_ss state_kind) ctxt') i end end val conseq_simp_tac = raw_conseq_simp_tac; (* Generates the hoare-quadruples that can be derived out of the hoare-context T *) fun gen_context_thms ctxt mode params G T F = let val Type (_,[comT]) = range_type (fastype_of G); fun destQuadruple (Const (@{const_name Set.insert},_) $ PpQA $ Const (@{const_name Orderings.bot}, _)) = PpQA | destQuadruple t = raise Match; fun mkCallQuadruple (Const (@{const_name Pair}, _) $ P $ (Const (@{const_name Pair}, _) $ p $ (Const(@{const_name Pair}, _) $ Q $ A))) = let val Call_p = Const (@{const_name Language.com.Call}, fastype_of p --> comT) $ p; in (P, Call_p, Q, A) end; fun mkHoare mode G T F (vars,PpQA) = let val hoare = (case mode of Partial => @{const_name HoarePartialDef.hoarep} | Total => @{const_name HoareTotalDef.hoaret}); (* FIXME: Use future Proof_Context.rename_vars or make closed term and remove by hand *) (* fun free_params ps t = foldr (fn ((x,xT),t) => snd (variant_abs (x,xT,t))) (ps,t); val PpQA' = mkCallQuadruple (strip_qnt_body @{const_name Pure.all} (free_params params (Term.list_all (vars,PpQA)))); *) val params' = (Variable.variant_frees ctxt [PpQA] params); val bnds = map Bound (0 upto (length vars - 1)); fun free_params_vars t = subst_bounds (bnds @ rev (map Free params' ), t) fun free_params t = subst_bounds (rev (map Free params' ), t) val (P',p',Q',A') = mkCallQuadruple (free_params_vars PpQA); val T' = free_params T; val G' = free_params G; val F' = free_params F; val bdy = mk_hoare_abs [] (P',p',Q',A',mode,G',T',F'); in (HOLogic.mk_Trueprop (HOLogic.list_all (vars,bdy)), map fst params') end; fun hoare_context_specs mode G T F = let fun mk t = try (mkHoare mode G T F o apsnd destQuadruple o dest_UN) t; in map_filter mk (dest_Un T) end; fun mk_prove mode (prop,params) = let val vars = map fst (strip_qnt_vars @{const_name All} (HOLogic.dest_Trueprop (Logic.strip_assums_concl prop))); val [asmUN'] = adapt_aux_var ctxt true vars [get_aux_tvar (AsmUN mode)] in Goal.prove ctxt params [] prop (fn thms => EVERY[trace_tac ctxt "extracting specifications from hoare context", resolve_tac ctxt [asmUN'] 1, DEPTH_SOLVE_1 (resolve_tac ctxt [subset_refl,refl] 1 ORELSE ((resolve_tac ctxt [@{thm Hoare.subset_unI1}] 1 APPEND resolve_tac ctxt [@{thm Hoare.subset_unI2}] 1) ORELSE (resolve_tac ctxt [@{thm Hoare.subset_singleton_insert1}] 1 APPEND resolve_tac ctxt [@{thm Hoare.subset_singleton_insert2}] 1))) ORELSE error_tac ("vcg: cannot extract specifications from context") ]) end; val specs = hoare_context_specs mode G T F; in map (mk_prove mode) specs end; fun is_modifies_clause t = exists_subterm (fn (Const (@{const_name Hoare.meq},_)) => true| _ => false) (#3 (dest_hoare (Logic.strip_assums_concl t))) handle (TERM _) => false; val is_spec_clause = not o is_modifies_clause; (* e.g: Intg => the_Intg lift Intg => lift the_Intg map Ingt => map the_Intg Hp o lift Intg => lift the_Intg o the_Hp *) fun swap_constr_destr f (t as (Const (@{const_name Fun.id},_))) = t | swap_constr_destr f (t as (Const (c,Type ("fun",[T,valT])))) = (Const (f c, Type ("fun",[valT,T])) handle Empty => raise TERM ("Hoare.swap_constr_destr",[t])) | swap_constr_destr f (Const ("StateFun.map_fun",Type ("fun", (* FIXME unknown "StateFun.map_fun" !? *) [Type ("fun",[T,valT]), Type ("fun",[Type ("fun",[xT,T']), Type ("fun",[xT',valT'])])]))$g) = Const ("StateFun.map_fun",Type("fun",[Type ("fun",[valT,T]), Type ("fun",[Type ("fun",[xT,valT']), Type ("fun",[xT',T'])])]))$ swap_constr_destr f g | swap_constr_destr f (Const (@{const_name Fun.comp},Type ("fun", [Type ("fun",[bT',cT]), Type ("fun",[Type ("fun",[aT ,bT]), Type ("fun",[aT',cT'])])]))$h$g) = let val h'=swap_constr_destr f h; val g'=swap_constr_destr f g; in Const (@{const_name Fun.comp},Type ("fun", [Type ("fun",[bT,aT]), Type ("fun",[Type ("fun",[cT,bT']), Type ("fun",[cT',aT'])])]))$g'$h' end | swap_constr_destr f (Const (@{const_name List.map},Type ("fun", [Type ("fun",[aT,bT]), Type ("fun",[asT,bsT])]))$g) = (Const (@{const_name List.map},Type ("fun", [Type ("fun",[bT,aT]), Type ("fun",[bsT,asT])]))$swap_constr_destr f g) | swap_constr_destr f t = raise TERM ("Hoare.swap_constr_destr",[t]); (* FIXME: unused? *) val destr_to_constr = let fun convert c = let val (path,base) = split_last (Long_Name.explode c); in Long_Name.implode (path @ ["val",unprefix "the_" base]) end; in swap_constr_destr convert end; fun gen_call_tac cont_tac mode cmode state_kind state_space ctxt asms spec_sfx pname return has_args _ = let val thy = Proof_Context.theory_of ctxt; val pname' = unsuffix proc_deco pname; val spec = (case AList.lookup (op =) asms pname of SOME s => SOME s | NONE => try (Proof_Context.get_thm ctxt) (suffix spec_sfx pname')); fun auxvars_for p t = (case first_subterm_dest (try dest_call) t of SOME (vars,(_,p',_,_,m,_)) => (if m=Static andalso p=(dest_string' p') then SOME vars else NONE) | NONE => NONE); fun get_auxvars_for p t = (case (map_filter ((auxvars_for p) o snd) (max_subterms_dest tap_UN t)) of (vars::_) => vars | _ => []); fun spec_tac augment_rule augment_emptyFaults _ spec i = let val spec' = augment_emptyFaults OF [spec] handle THM _ => spec; in EVERY [resolve_tac ctxt [augment_rule] i, resolve_tac ctxt [spec'] (i+1), TRY (resolve_tac ctxt [subset_refl, @{thm Set.empty_subsetI}, @{thm Set.Un_upper1}, @{thm Set.Un_upper2}] i)] end; fun check_spec name P thm = (case try dest_hoare (Thm.concl_of thm) of SOME spc => (case try dest_call (#2 spc) of SOME (_,p,_,_,m,_) => if proc_name m p = name andalso P (Thm.concl_of thm) then SOME (#5 spc,thm) else NONE | _ => NONE) | _ => NONE) fun find_dyn_specs name P thms = map_filter (check_spec name P) thms; fun get_spec name P thms = case find_dyn_specs name P thms of (spec_mode,spec)::_ => SOME (spec_mode,spec) | _ => NONE; fun solve_spec augment_rule _ augment_emptyFaults mode _ (SOME spec_mode) (SOME spec) i= if mode=Partial andalso spec_mode=Total then resolve_tac ctxt [@{thm HoareTotal.hoaret_to_hoarep'}] i THEN spec_tac augment_rule augment_emptyFaults mode spec i else if mode=spec_mode then spec_tac augment_rule augment_emptyFaults mode spec i else error("vcg: cannot use a partial correctness specification of " ^ pname' ^ " for a total correctness proof") | solve_spec _ asmUN_rule _ mode Static _ _ i =(* try to infer spec out of context *) EVERY[trace_tac ctxt "inferring specification from hoare context1", resolve_tac ctxt [asmUN_rule] i, DEPTH_SOLVE_1 (resolve_tac ctxt [subset_refl,refl] i ORELSE ((resolve_tac ctxt [@{thm Hoare.subset_unI1}] i APPEND resolve_tac ctxt [@{thm Hoare.subset_unI2}] i) ORELSE (resolve_tac ctxt [@{thm Hoare.subset_singleton_insert1}] i APPEND resolve_tac ctxt [@{thm Hoare.subset_singleton_insert2}] i))) ORELSE error_tac ("vcg: cannot infer specification of " ^ pname' ^ " from context") (* if tactic for DEPTH_SOLVE_1 would create new subgoals, use SELECT_GOAL and DEPTH_SOLVE *) ] | solve_spec augment_rule asmUN_rule augment_emptyFaults mode Parameter _ _ i = (* try to infer spec out of assumptions *) let fun tac thms = (case (find_dyn_specs pname is_spec_clause thms) of (spec_mode,spec)::_ => solve_spec augment_rule asmUN_rule augment_emptyFaults mode Parameter (SOME spec_mode) (SOME spec) 1 | _ => all_tac) in Subgoal.FOCUS (tac o #prems) ctxt i end val strip_spec_vars = strip_qnt_vars @{const_name All} o HOLogic.dest_Trueprop; fun apply_call_tac ctxt pname mode cmode spec_mode spec_goal is_abr spec (subgoal,i) = let val spec_vars = map fst (case spec of SOME sp => (strip_spec_vars (Thm.concl_of sp)) | NONE => (case try (dest_hoare) subgoal of SOME (_,_,_,_,_,_,Theta,_) => get_auxvars_for pname Theta | _ => [])); fun get_call_rule Static mode is_abr = if is_abr then Proc mode else ProcNoAbr mode | get_call_rule Parameter mode is_abr = if is_abr then DynProcProcPar mode else DynProcProcParNoAbr mode; val [call_rule,augment_ctxt_rule,asmUN_rule, augment_emptyFaults] = adapt_aux_var ctxt true spec_vars (map get_aux_tvar [get_call_rule cmode mode is_abr, AugmentContext mode, AsmUN mode, AugmentEmptyFaults mode]); in EVERY [resolve_tac ctxt [call_rule] i, trace_tac ctxt "call_tac -- basic_tac -- solving spec", solve_spec augment_ctxt_rule asmUN_rule augment_emptyFaults mode cmode spec_mode spec spec_goal] end; fun basic_tac spec i = let val msg ="Theorem " ^pname'^spec_sfx ^ " is no proper specification for procedure " ^pname'^ "; trying to infer specification from hoare context"; fun spec' s mode abr = if is_modifies_clause (Thm.concl_of s) then if abr then (TrivPost mode) OF [s] else (TrivPostNoAbr mode) OF [s] else s; val (is_abr,spec_mode,spec,spec_has_args) = (* is there a proper specification fact? *) case spec of NONE => (true,NONE,NONE,false) | SOME s => case try dest_hoare (Thm.concl_of s) of NONE => (warning msg;(true,NONE,NONE,false)) | SOME (_,c,Q,spec_abr,spec_mode,_,_,_) => case try dest_call c of NONE => (warning msg;(true,NONE,NONE,false)) | SOME (_,p,_,_,m,spec_has_args) => if proc_name m p = pname then if (mode=Total andalso spec_mode=Partial) then (warning msg;(true,NONE,NONE,false)) else if is_empty_set spec_abr then (false,SOME spec_mode, SOME (spec' s spec_mode false),spec_has_args) else (true,SOME spec_mode, SOME (spec' s spec_mode true),spec_has_args) else (warning msg;(true,NONE,NONE,false)); val () = if spec_has_args then error "procedure call in specification must be parameterless!" else (); val spec_goal = i+2; in EVERY[trace_tac ctxt "call_tac -- basic_tac -- START --", SUBGOAL (apply_call_tac ctxt pname mode cmode spec_mode spec_goal is_abr spec) i, resolve_tac ctxt [allI] (i+1), resolve_tac ctxt [allI] (i+1), cont_tac (i+1), trace_tac ctxt "call_tac -- basic_tac -- simplify", conseq_simp_tac ctxt state_kind [@{thm StateSpace.upd_globals_def}] i, trace_tac ctxt "call_tac -- basic_tac -- STOP --"] end; fun get_modifies (Const (@{const_name Collect},_) $ Abs (_,_,m)) = m | get_modifies t = raise TERM ("gen_call_tac.get_modifies",[t]); fun get_updates (Abs (_,_,t)) = get_updates t | get_updates (Const (@{const_name Hoare.mex},_) $ t) = get_updates t | get_updates (Const (@{const_name Hoare.meq},T) $ _ $ upd) = (T,upd) | get_updates t = raise TERM ("gen_call_tac.get_updates",[t]); (* return has the form: %s t. s(|globals:=globals t,...|) * should be translated to %s t. s(|globals := globals s(|m := m (globals t),...|),...|) * for all m in the modifies list. *) fun mk_subst gT meqT = fst (Sign.typ_unify thy (gT,domain_type meqT) (Vartab.empty,0)); fun mk_selR subst gT (upd,uT) = let val vT = range_type (hd (binder_types uT)); in Const (unsuffix Record.updateN upd,gT --> (Envir.norm_type subst vT)) end; (* lookup:: "('v => 'a) => 'n => ('n => 'v) => 'a" * update:: "('v => 'a) => ('a => 'v) => 'n => ('a => 'a) => ('n => 'v) => ('n => 'v)" *) fun mk_selF subst uT d n = let val vT_a::a_vT::nT::aT_aT::n_vT::_ = binder_types uT; val lT = (Envir.norm_type subst (vT_a --> nT --> n_vT --> (domain_type aT_aT))); val d' = map_types (Envir.norm_type subst) d; in Const (@{const_name StateFun.lookup},lT)$d'$n end; fun mk_rupdR subst gT (upd,uT) = let val [vT,_] = binder_types uT in Const (upd,(Envir.norm_type subst vT) --> gT --> gT) end; fun K_fun kn uT = let val T=range_type (hd (binder_types uT)) in Const (kn,T --> T --> T) end; fun K_rec uT t = let val T=range_type (hd (binder_types uT)) in Abs ("_", T, incr_boundvars 1 t) end; fun mk_supdF subst uT d c n = let val uT' = Envir.norm_type subst uT; val c' = map_types (Envir.norm_type subst) c; val d' = map_types (Envir.norm_type subst) d; in Const (@{const_name StateFun.update},uT')$d'$c'$n end; fun modify_updatesR subst gT glob ((Const (upd,uT))$_$(Const _$Z)) = mk_rupdR subst gT (upd,uT)$ (K_rec uT (mk_selR subst gT (upd,uT)$(glob$Bound 0)))$(glob$Bound 1) | modify_updatesR subst gT glob ((Const (upd,uT))$_$s) = mk_rupdR subst gT (upd,uT)$ (K_rec uT (mk_selR subst gT (upd,uT)$(glob$Bound 0)))$ modify_updatesR subst gT glob s | modify_updatesR subst gT glob ((_$Z)) = (glob$Bound 1) (* may_not_modify *) | modify_updatesR _ _ _ t = raise TERM ("gen_call_tac.modify_updatesR",[t]); fun modify_updatesF subst _ glob (Const (@{const_name StateFun.update},uT)$d$c$n$_$(Const globs$Z)) = mk_supdF subst uT d c n$ (K_fun KNF uT$(mk_selF subst uT d n$(glob$Bound 0)))$(glob$Bound 1) | modify_updatesF subst gT glob (Const (@{const_name StateFun.update},uT)$d$c$n$_$s) = mk_supdF subst uT d c n$ (K_fun KNF uT$(mk_selF subst uT d n$(glob$Bound 0)))$modify_updatesF subst gT glob s | modify_updatesF subst _ glob ((globs$Z)) = (glob$Bound 1) (* may_not_modify *) | modify_updatesF _ _ _ t = raise TERM ("gen_call_tac.modify_updatesF",[t]); fun modify_updates Record = modify_updatesR | modify_updates _ = modify_updatesF fun globalsT (Const (gupd,T)) = domain_type (hd (binder_types T)) | globalsT t = raise TERM ("gen_call_tac.globalsT",[t]); fun mk_upd meqT mods (gupd$(Abs (dmy,dmyT,(glob$Bound 1)))$Bound 1) = let val gT = (globalsT gupd); val subst = mk_subst gT meqT; in (gupd$(Abs (dmy,dmyT,incr_boundvars 1 (modify_updates state_kind subst gT glob mods)))$Bound 1) end | mk_upd meqT mods (upd$v$s) = upd$v$mk_upd meqT mods s | mk_upd _ _ t = raise TERM ("gen_call_tac.mk_upd",[t]); fun modify_return (meqT,mods) (Abs (s,T,Abs (t,U,upd))) = (Abs (s,T,Abs (t,U,mk_upd meqT mods upd))) | modify_return _ t = raise TERM ("get_call_tac.modify_return",[t]); fun modify_tac spec modifies_thm i = try (fn () => let val (_,call,modif_spec_nrm,modif_spec_abr,modif_spec_mode,G,Theta,_) = dest_hoare (Thm.concl_of modifies_thm); val is_abr = not (is_empty_set modif_spec_abr); val emptyTheta = is_empty_set Theta; (*val emptyFaults = is_empty_set F;*) val spec_has_args = #6 (dest_call call); val () = if spec_has_args then error "procedure call in modifies-specification must be parameterless!" else (); val (mxprem,ModRet) = (case cmode of Static => (8,if is_abr then if emptyTheta then (ProcModifyReturn mode) else (ProcModifyReturnSameFaults mode) else if emptyTheta then (ProcModifyReturnNoAbr mode) else (ProcModifyReturnNoAbrSameFaults mode)) | Parameter => (9,if is_abr then if emptyTheta then (ProcProcParModifyReturn mode) else (ProcProcParModifyReturnSameFaults mode) else if emptyTheta then (ProcProcParModifyReturnNoAbr mode) else (ProcProcParModifyReturnNoAbrSameFaults mode))); val to_prove_prem = (case cmode of Static => 0 | Parameter => 1); val spec_goal = if is_abr then i + mxprem - 5 else i + mxprem - 6 val mods_nrm = modif_spec_nrm |> get_modifies |> get_updates; val return' = modify_return mods_nrm return; (* val return' = if is_abr then let val mods_abr = modif_spec_abr |> get_modifies |> get_updates; in modify_return mods_abr return end else return;*) val cret = Thm.cterm_of ctxt return'; val (_,_,return'_var,_,_,_) = nth (Thm.prems_of ModRet) to_prove_prem |> dest_hoare |> #2 |> dest_call; val ModRet' = infer_instantiate ctxt [(#1 (dest_Var return'_var), cret)] ModRet; val modifies_thm_partial = if modif_spec_mode = Total then @{thm HoareTotal.hoaret_to_hoarep'} OF [modifies_thm] else modifies_thm; fun solve_modifies_tac i = (clarsimp_tac ((ctxt |> put_claset (claset_of @{theory_context Set}) |> put_simpset (simpset_of @{theory_context Set})) addsimps ([@{thm Hoare.mex_def},@{thm Hoare.meq_def},@{thm StateSpace.upd_globals_def}]@K_convs) addsimprocs (state_upd_simproc Record::(state_simprocs state_kind)) |> fold Simplifier.add_cong K_congs) i) THEN_MAYBE EVERY [trace_tac ctxt "modify_tac: splitting record", state_split_simp_tac ctxt [] state_space i]; val cnt = i + mxprem; in EVERY[trace_tac ctxt "call_tac -- modifies_tac --", resolve_tac ctxt [ModRet'] i, solve_spec (AugmentContext Partial) (AsmUN Partial) (AugmentEmptyFaults Partial) Partial Static (SOME Partial) (SOME modifies_thm_partial) spec_goal, if is_abr then EVERY [trace_tac ctxt "call_tac -- Solving abrupt modifies --", solve_modifies_tac (cnt - 6)] else all_tac, trace_tac ctxt "call_tac -- Solving Modifies --", solve_modifies_tac (cnt - 7), basic_tac spec (cnt - 8), if cmode = Parameter then EVERY [resolve_tac ctxt [subset_refl] (cnt - 8), simp_tac (put_simpset HOL_basic_ss ctxt addsimps (@{thm Hoare.CollectInt_iff} :: @{thms simp_thms})) 1] else all_tac] end) () |> (fn SOME res => res | NONE => raise TERM ("get_call_tac.modify_tac: no proper modifies spec", [])); fun specs_of_assms_tac thms = (case get_spec pname is_spec_clause thms of SOME (_,spec) => (case get_spec pname is_modifies_clause thms of SOME (_,modifies_thm) => modify_tac (SOME spec) modifies_thm 1 | NONE => basic_tac (SOME spec) 1) | NONE => (warning ("no proper specification for procedure " ^pname^ " in assumptions"); all_tac)); val test_modify_in_ctxt_tac = let val mname = (suffix modifysfx pname'); val mspec = (case try (Proof_Context.get_thm ctxt) mname of SOME s => SOME s | NONE => (case AList.lookup (op =) asms pname of SOME s => if is_modifies_clause (Thm.concl_of s) then SOME s else NONE | NONE => NONE)); in (case mspec of NONE => basic_tac spec | SOME modifies_thm => (case check_spec pname is_modifies_clause modifies_thm of SOME _ => modify_tac spec modifies_thm | NONE => (warning ("ignoring theorem " ^ (suffix modifysfx pname') ^ "; no proper modifies specification for procedure "^pname'); basic_tac spec))) end; fun inline_bdy_tac has_args i = (case try (Proof_Context.get_thm ctxt) (suffix bodyP pname') of NONE => no_tac | SOME impl => (case try (Proof_Context.get_thm ctxt) (suffix (body_def_sfx^"_def") pname') of NONE => no_tac | SOME bdy => (tracing ("No specification found for procedure \"" ^ pname' ^ "\". Inlining procedure!"); if has_args then EVERY [trace_tac ctxt "inline_bdy_tac args", resolve_tac ctxt [CallBody mode] i, resolve_tac ctxt [impl] (i+3), resolve_tac ctxt [allI] (i+2), resolve_tac ctxt [allI] (i+2), in_assertion_simp_tac ctxt state_kind [] (i+2), cont_tac (i+2), resolve_tac ctxt [allI] (i+1),in_assertion_simp_tac ctxt state_kind [bdy] (i+1), cont_tac (i+1), in_assertion_simp_tac ctxt state_kind [@{thm StateSpace.upd_globals_def}] i] else EVERY [trace_tac ctxt "inline_bdy_tac no args", resolve_tac ctxt [ProcBody mode] i, resolve_tac ctxt [impl] (i+2), simp_tac (put_simpset HOL_basic_ss ctxt addsimps [bdy]) (i+1), cont_tac (i+1)]))); in (case cmode of Static => if get_recursive pname ctxt = SOME false andalso is_none spec then inline_bdy_tac has_args else test_modify_in_ctxt_tac | Parameter => (case spec of NONE => (tracing "no spec found!"; Subgoal.FOCUS (specs_of_assms_tac o #prems) ctxt) | SOME spec => (tracing "found spec!"; case check_spec pname is_spec_clause spec of SOME _ => test_modify_in_ctxt_tac | NONE => (warning ("ignoring theorem " ^ (suffix spec_sfx pname') ^ "; no proper specification for procedure " ^pname'); Subgoal.FOCUS (specs_of_assms_tac o #prems) ctxt)))) end; fun call_tac cont_tac mode state_kind state_space ctxt asms spec_sfx t = let val (_,c,_,_,_,_,_,F) = dest_hoare (Logic.strip_assums_concl t); fun gen_tac (_,pname,return,c,cmode,has_args) = gen_call_tac cont_tac mode cmode state_kind state_space ctxt asms spec_sfx (proc_name cmode pname) return has_args F; in gen_tac (dest_call c) end handle TERM _ => K no_tac; fun solve_in_Faults_tac ctxt i = resolve_tac ctxt [UNIV_I, @{thm in_insert_hd}] i ORELSE SELECT_GOAL (SOLVE (simp_tac (put_simpset (simpset_of @{theory_context Set}) ctxt) 1)) i; local fun triv_simp ctxt = merge_assertion_simp_tac ctxt [mem_Collect_eq] THEN' simp_tac (put_simpset HOL_basic_ss ctxt addsimps @{thms simp_thms} |> fold Simplifier.add_cong [@{thm conj_cong}, @{thm imp_cong}]); (* a guarded while produces stupid things, since the guards are put at the end of the body and in the invariant (rule WhileAnnoG): - guard: g /\ g - guarantee: g --> g *) in fun guard_tac ctxt strip cont_tac mode (t,i) = let val (_,c,_,_,_,_,_,F) = dest_hoare (Logic.strip_assums_concl t); val (_,_,_,doStrip) = dest_Guard c; val guarantees = if strip orelse doStrip then [GuardStrip mode, GuaranteeStrip mode] else [Guarantee mode] fun basic_tac i = EVERY [resolve_tac ctxt [Guard mode, GuaranteeAsGuard mode] i, trace_tac ctxt "Guard", cont_tac (i+1), triv_simp ctxt i] fun guarantee_tac i = EVERY [resolve_tac ctxt guarantees i, solve_in_Faults_tac ctxt (i+2), cont_tac (i+1), triv_simp ctxt i] in if is_empty_set F then EVERY [trace_tac ctxt "Guard: basic_tac", basic_tac i] else EVERY [trace_tac ctxt "Guard: trying guarantee_tac", guarantee_tac i ORELSE basic_tac i] end handle TERM _ => no_tac end; fun wf_tac ctxt = simp_tac (put_simpset HOL_basic_ss ctxt addsimps [@{thm Wellfounded.wf_measure},@{thm Wellfounded.wf_lex_prod},@{thm Wfrec.wf_same_fst}, @{thm Hoare.wf_measure_lex_prod},@{thm Wellfounded.wf_inv_image}]); fun in_rel_simp ctxt = simp_tac (put_simpset HOL_basic_ss ctxt addsimps [@{thm Hoare.in_measure_iff},@{thm Hoare.in_lex_iff},@{thm Hoare.in_mlex_iff},@{thm Hoare.in_inv_image_iff}, @{thm split_conv}]); fun while_annotate_tac ctxt inv i st = let val annotateWhile = Thm.lift_rule (Thm.cprem_of st i) @{thm HoarePartial.reannotateWhileNoGuard}; val lifted_inv = fold_rev Term.abs (Logic.strip_params (Logic.get_goal (Thm.prop_of st) i)) inv; val invVar = (#1 o strip_comb o #3 o dest_whileAnno o #2 o dest_hoare) (List.last (Thm.prems_of annotateWhile)); val annotate = infer_instantiate ctxt [(#1 (dest_Var invVar), Thm.cterm_of ctxt lifted_inv)] annotateWhile; in ((trace_tac ctxt ("annotating While with: " ^ Syntax.string_of_term ctxt lifted_inv )) THEN compose_tac ctxt (false,annotate,1) i) st end; fun cond_annotate_tac ctxt inv mode (_,i) st = let val annotateCond = Thm.lift_rule (Thm.cprem_of st i) (CondInv' mode); val lifted_inv = fold_rev Term.abs (Logic.strip_params (Logic.get_goal (Thm.prop_of st) i)) inv; val invVar = List.last (Thm.prems_of annotateCond) |> dest_hoare |> #3 |> strip_comb |> #1; val annotate = infer_instantiate ctxt [(#1 (dest_Var invVar), Thm.cterm_of ctxt lifted_inv)] annotateCond; in ((trace_tac ctxt ("annotating Cond with: "^ Syntax.string_of_term ctxt lifted_inv)) THEN compose_tac ctxt (false,annotate,5) i) st end; fun basic_while_tac ctxt state_kind cont_tac tac mode i = let fun common_tac i = EVERY[if mode=Total then wf_tac ctxt (i+3) else all_tac, BasicSimpTac ctxt state_kind true [] tac (i+2), if mode=Total then in_rel_simp ctxt (i+1) THEN (resolve_tac ctxt [allI] (i+1)) else all_tac, cont_tac (i+1) ] fun basic_tac i = EVERY [resolve_tac ctxt [While mode] i, common_tac i] in EVERY [trace_tac ctxt "basic_while_tac: basic_tac", basic_tac i] end; fun while_tac ctxt state_kind inv cont_tac tac mode t i= let val basic_tac = basic_while_tac ctxt state_kind cont_tac tac mode; in (case inv of NONE => basic_tac i | SOME I => EVERY [while_annotate_tac ctxt I i, basic_tac i]) end handle TERM _ => no_tac fun dest_split (Abs (x,T,t)) = let val (vs,recomb,bdy) = dest_split t; in ((x,T)::vs,fn t' => Abs (x,T,recomb t'),bdy) end | dest_split (c as Const (@{const_name case_prod},_)$Abs(x,T,t)) = let val (vs,recomb,bdy) = dest_split t; in ((x,T)::vs,fn t' => c$Abs (x,T,recomb t'),bdy) end | dest_split t = ([],I,t); fun whileAnnoG_tac ctxt strip_guards mode t i st = let val (_,c,_,_,_,_,_,F) = dest_hoare (Logic.strip_assums_concl t); val (SOME grds,_,I,_,_,fix) = dest_whileAnno c; val Rule = if fix then WhileAnnoGFix mode else WhileAnnoG mode; fun extract_faults (Const (@{const_name Set.insert}, _) $ t $ _) = [t] | extract_faults _ = []; fun leave_grd fs (Const (@{const_name Pair}, _) $ f $ g) = if member (op =) fs f andalso strip_guards then NONE else SOME g | leave_grd fs (Const (@{const_name Language.guaranteeStripPair}, _) $ f $ g) = if member (op =) fs f then NONE else SOME g | leave_grd fs _ = NONE; val (I_vs,I_recomb,I') = dest_split I; val grds' = map_filter (leave_grd (extract_faults F)) (HOLogic.dest_list grds); val pars = (Logic.strip_params (Logic.get_goal (Thm.prop_of st) i)); val J = fold_rev Term.abs pars (I_recomb (fold_rev (mk_Int (map snd (pars@I_vs))) grds' I')); val WhileG = Thm.lift_rule (Thm.cprem_of st i) Rule; val invVar = (fst o strip_comb o #3 o dest_whileAnno o (fn xs => nth xs 1) o snd o strip_comb o #2 o dest_hoare) (List.last (Thm.prems_of WhileG)); val WhileGInst = infer_instantiate ctxt [(#1 (dest_Var invVar), Thm.cterm_of ctxt J)] WhileG; in ((trace_tac ctxt ("WhileAnnoG, adding guards to invariant: " ^ Syntax.string_of_term ctxt J)) THEN compose_tac ctxt (false,WhileGInst,1) i) st end handle TERM _ => no_tac st | Bind => no_tac st (* renames bound state variable according to name given in goal, * before rule specAnno is applied, and solves sidecondition *) fun gen_Anno_tac dest rules tac cont_tac ctxt state_kind (t,i) st = let val vars = (dest o #2 o dest_hoare) (Logic.strip_assums_concl t); val rules' = (case (List.filter (not o null) (map dest_splits vars)) of [] => rules |(xs::_) => adapt_aux_var ctxt false (map fst xs) (map get_aux_tvar rules)); in EVERY [resolve_tac ctxt rules' i, tac, simp_tac (put_simpset HOL_basic_ss ctxt addsimps ([@{thm split_conv}, refl, @{thm Hoare.triv_All_eq}]@anno_defs) addsimprocs [@{simproc case_prod_beta}]) (i+2), simp_tac (put_simpset HOL_basic_ss ctxt addsimps [@{thm split_conv}]) (i+1), simp_tac (put_simpset HOL_basic_ss ctxt addsimps [@{thm split_conv}]) i, REPEAT (resolve_tac ctxt [allI] (i+1)), cont_tac (i+1), conseq_simp_tac ctxt state_kind [] i] st end handle TERM _ => no_tac st; fun specAnno_tac ctxt state_kind cont_tac mode = let fun dest_specAnno (Const (@{const_name Language.specAnno},_)$P$c$Q$A) = [P,c,Q,A] | dest_specAnno t = raise TERM ("dest_specAnno",[t]); val rules = [SpecAnnoNoAbrupt mode,SpecAnno mode]; in gen_Anno_tac dest_specAnno rules all_tac cont_tac ctxt state_kind end; fun whileAnnoFix_tac ctxt state_kind cont_tac mode (t,i) = let fun dest (Const (@{const_name Language.whileAnnoFix},_)$b$I$V$c) = [I,V,c] | dest t = raise TERM ("dest_whileAnnoFix",[t]); val rules = [WhileAnnoFix mode]; fun wf_tac' i = EVERY [REPEAT (resolve_tac ctxt [allI] i), simp_tac (put_simpset HOL_basic_ss ctxt addsimps [@{thm split_conv}]) i, wf_tac ctxt i]; val tac = if mode=Total then EVERY [wf_tac' (i+3),in_rel_simp ctxt (i+1)] else all_tac in gen_Anno_tac dest rules tac cont_tac ctxt state_kind (t,i) end; fun lemAnno_tac ctxt state_kind mode (t,i) st = let fun dest_name (Const (x,_)) = x | dest_name (Free (x,_)) = x | dest_name t = raise TERM ("dest_name",[t]); fun dest_lemAnno ctxt (Const (@{const_name Language.lem},_)$n$c) = let val x = Long_Name.base_name (dest_name n); in (case try (Proof_Context.get_thm ctxt) x of NONE => error ("No lemma: '" ^ x ^ "' found.") | SOME spec => (strip_qnt_vars @{const_name All} (HOLogic.dest_Trueprop (Thm.concl_of spec)),spec)) end | dest_lemAnno _ t = raise TERM ("dest_lemAnno",[t]); val (vars,spec) = dest_lemAnno ctxt (#2 (dest_hoare t)); val rules = [LemAnnoNoAbrupt mode,LemAnno mode]; val rules' = (case vars of [] => rules | xs => adapt_aux_var ctxt true (map fst xs) (map get_aux_tvar rules)); in EVERY [resolve_tac ctxt rules' i, resolve_tac ctxt [spec] (i+1), conseq_simp_tac ctxt state_kind [] i] st end handle TERM _ => no_tac st; fun prems_tac ctxt i = TRY (resolve_tac ctxt (Assumption.all_prems_of ctxt) i); fun mk_proc_assoc thms = let fun name (_,p,_,_,cmode,_) = proc_name cmode p; fun proc_name thm = thm |> Thm.concl_of |> dest_hoare |> #2 |> dest_call |> name; in map (fn thm => (proc_name thm,thm)) thms end; fun mk_hoare_tac cont ctxt mode i (name,tac) = EVERY [trace_tac ctxt ("trying: " ^ name),tac cont ctxt mode i]; (* the main hoare tactic *) fun HoareTac annotate_inv exspecs strip_guards mode state_kind state_space spec_sfx ctxt tac st = let val (P,c,Q,A,_,G,T,F) = dest_hoare (Logic.strip_assums_concl (Logic.get_goal (Thm.prop_of st) 1)); val wp_tacs = #wp_tacs (get_data ctxt); val hoare_tacs = #hoare_tacs (get_data ctxt); val params = (strip_vars (Logic.get_goal (Thm.prop_of st) 1)); val Inv = (if annotate_inv then (* Take the postcondition of the triple as invariant for all *) (* while loops (makes sense for the modifies clause) *) SOME Q else NONE); val exspecthms = map (Proof_Context.get_thm ctxt) exspecs; val asms = try (fn () => mk_proc_assoc (gen_context_thms ctxt mode params G T F @ exspecthms)) () |> the_default []; fun while_annoG_tac (t,i) = whileAnnoG_tac ctxt (annotate_inv orelse strip_guards) mode t i; fun WlpTac tac i = (* WlpTac does not end with subset_refl *) FIRST ([EVERY [resolve_tac ctxt [Seq mode] i,trace_tac ctxt "Seq",HoareRuleTac tac false (i+1)], EVERY [resolve_tac ctxt [Catch mode] i,trace_tac ctxt "Catch",HoareRuleTac tac false (i+1)], EVERY [resolve_tac ctxt [CondCatch mode] i,trace_tac ctxt "CondCatch",HoareRuleTac tac false (i+1)], EVERY [resolve_tac ctxt [BSeq mode] i,trace_tac ctxt "BSeq",HoareRuleTac tac false (i+1)], EVERY [resolve_tac ctxt [FCall mode] i,trace_tac ctxt "FCall"], EVERY [resolve_tac ctxt [GuardsNil mode] i,trace_tac ctxt "GuardsNil"], EVERY [resolve_tac ctxt [GuardsConsGuaranteeStrip mode] i, trace_tac ctxt "GuardsConsGuaranteeStrip"], EVERY [resolve_tac ctxt [GuardsCons mode] i,trace_tac ctxt "GuardsCons"], EVERY [SUBGOAL while_annoG_tac i] ] @ map (mk_hoare_tac (HoareRuleTac tac) ctxt mode i) wp_tacs) and HoareRuleTac tac pre_cond i st = let fun call (t,i) = call_tac (HoareRuleTac tac false) mode state_kind state_space ctxt asms spec_sfx t i fun cond_tac i = if annotate_inv andalso Config.get ctxt use_cond_inv_modifies then EVERY[SUBGOAL (cond_annotate_tac ctxt (the Inv) mode) i, HoareRuleTac tac false (i+4), HoareRuleTac tac false (i+3), BasicSimpTac ctxt state_kind true [] tac (i+2), BasicSimpTac ctxt state_kind true [] tac (i+1) ] else EVERY[resolve_tac ctxt [Cond mode] i,trace_tac ctxt "Cond", HoareRuleTac tac false (i+2), HoareRuleTac tac false (i+1)]; fun switch_tac i = EVERY[resolve_tac ctxt [SwitchNil mode] i, trace_tac ctxt "SwitchNil"] ORELSE EVERY[resolve_tac ctxt [SwitchCons mode] i,trace_tac ctxt "SwitchCons", HoareRuleTac tac false (i+2), HoareRuleTac tac false (i+1)]; fun while_tac' (t,i) = while_tac ctxt state_kind Inv (HoareRuleTac tac true) tac mode t i; in st |> ( (WlpTac tac i THEN HoareRuleTac tac pre_cond i) ORELSE (FIRST([EVERY[resolve_tac ctxt [Skip mode] i,trace_tac ctxt "Skip"], EVERY[resolve_tac ctxt [BasicCond mode] i, trace_tac ctxt "BasicCond", assertion_simp_tac ctxt state_kind [] i], (resolve_tac ctxt [Basic mode] i THEN trace_tac ctxt "Basic") THEN_MAYBE (assertion_simp_tac ctxt state_kind [] i), (* we don't really need simplificaton here. The question is if it is better to simplify the assertion after each Basic step, so that intermediate assertions stay "small", or if we just accumulate the raw assertions and leave the simplification to the final BasicSimpTac *) EVERY[resolve_tac ctxt [Throw mode] i, trace_tac ctxt "Throw"], (resolve_tac ctxt [Raise mode] i THEN trace_tac ctxt "Raise") THEN_MAYBE (assertion_string_eq_simp_tac ctxt state_kind [] i), cond_tac i, switch_tac i, EVERY[resolve_tac ctxt [Block mode] i, trace_tac ctxt "Block", resolve_tac ctxt [allI] (i+2), resolve_tac ctxt [allI] (i+2), HoareRuleTac tac false (i+2), resolve_tac ctxt [allI] (i+1), in_assertion_simp_tac ctxt state_kind [] (i+1), HoareRuleTac tac false (i+1)], SUBGOAL while_tac' i, SUBGOAL (guard_tac ctxt (annotate_inv orelse strip_guards) (HoareRuleTac tac false) mode) i, EVERY[SUBGOAL (specAnno_tac ctxt state_kind (HoareRuleTac tac true) mode) i], EVERY[SUBGOAL (whileAnnoFix_tac ctxt state_kind (HoareRuleTac tac true) mode) i], EVERY[resolve_tac ctxt [SpecIf mode] i, trace_tac ctxt "SpecIf", assertion_simp_tac ctxt state_kind [] i], (resolve_tac ctxt [Spec mode] i THEN trace_tac ctxt "Spec") THEN_MAYBE (assertion_simp_tac ctxt state_kind [@{thm split_conv}] i), EVERY[resolve_tac ctxt [BindR mode] i, trace_tac ctxt "Bind", resolve_tac ctxt [allI] (i+1), HoareRuleTac tac false (i+1)], EVERY[resolve_tac ctxt [DynCom mode] i, trace_tac ctxt "DynCom"], EVERY[trace_tac ctxt "calling call_tac",SUBGOAL call i], EVERY[trace_tac ctxt "LemmaAnno",SUBGOAL (lemAnno_tac ctxt state_kind mode) i]] @ map (mk_hoare_tac (HoareRuleTac tac) ctxt mode i) hoare_tacs) THEN (if pre_cond then EVERY [trace_tac ctxt "pre_cond", TRY (BasicSimpTac ctxt state_kind true [] tac i), (* FIXME: Do we need TRY *) trace_tac ctxt "after BasicSimpTac"] else (resolve_tac ctxt [subset_refl] i)))) end; in ((K (EVERY [REPEAT (resolve_tac ctxt [allI] 1), HoareRuleTac tac true 1])) THEN_ALL_NEW (prems_tac ctxt)) 1 st (*Procedure specifications may have an locale assumption as premise. These are accumulated by the vcg and are be solved afterward by prems_tac *) end; fun prefer_tac i = (Tactic.defer_tac i THEN PRIMITIVE (Thm.permute_prems 0 ~1)); fun HoareStepTac strip_guards mode state_kind state_space spec_sfx ctxt tac st = let val asms = try (fn () => let val (_,_,_,_,_,G,T,F) = dest_hoare (Logic.strip_assums_concl (Logic.get_goal (Thm.prop_of st) 1)); val params = (strip_vars (Logic.get_goal (Thm.prop_of st) 1)); in mk_proc_assoc (gen_context_thms ctxt mode params G T F) end) () |> the_default []; fun result_tac i = TRY (EVERY [resolve_tac ctxt [Basic mode] i, resolve_tac ctxt [subset_refl] i]); fun call (t,i) = call_tac result_tac mode state_kind state_space ctxt asms spec_sfx t i fun final_simp_tac i = EVERY [full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps [mem_Collect_eq]) i, REPEAT (eresolve_tac ctxt [conjE] i), TRY (hyp_subst_tac_thin true ctxt i), BasicSimpTac ctxt state_kind true [] tac i] fun while_annoG_tac (t,i) = whileAnnoG_tac ctxt strip_guards mode t i; in st |> (REPEAT (resolve_tac ctxt [allI] 1) THEN FIRST [resolve_tac ctxt [subset_refl] 1, EVERY[resolve_tac ctxt [Skip mode] 1,TRY (BasicSimpTac ctxt state_kind false [] tac 1)], EVERY[resolve_tac ctxt [BasicCond mode] 1,trace_tac ctxt "BasicCond", TRY (BasicSimpTac ctxt state_kind false [] tac 1)], EVERY[resolve_tac ctxt [Basic mode] 1,TRY (BasicSimpTac ctxt state_kind false [] tac 1)], EVERY[resolve_tac ctxt [Throw mode] 1,TRY (BasicSimpTac ctxt state_kind false [] tac 1)], EVERY[resolve_tac ctxt [Raise mode] 1,TRY (assertion_string_eq_simp_tac ctxt state_kind [] 1)], resolve_tac ctxt [SeqSwap mode] 1 THEN_MAYBE HoareStepTac strip_guards mode state_kind state_space spec_sfx ctxt tac, EVERY[resolve_tac ctxt [BSeq mode] 1, prefer_tac 2 THEN_MAYBE HoareStepTac strip_guards mode state_kind state_space spec_sfx ctxt tac], resolve_tac ctxt [CondSwap mode] 1, resolve_tac ctxt [SwitchNil mode] 1, resolve_tac ctxt [SwitchCons mode] 1, EVERY [SUBGOAL while_annoG_tac 1], EVERY[resolve_tac ctxt [While mode] 1, if mode=Total then wf_tac ctxt 4 else all_tac, BasicSimpTac ctxt state_kind false [] tac 3, if mode=Total then in_rel_simp ctxt 2 THEN (resolve_tac ctxt [allI] 2) else all_tac, BasicSimpTac ctxt state_kind false [] tac 1], resolve_tac ctxt [CatchSwap mode] 1, resolve_tac ctxt [CondCatchSwap mode] 1, EVERY[resolve_tac ctxt [BlockSwap mode] 1, resolve_tac ctxt [allI] 1, resolve_tac ctxt [allI] 1, resolve_tac ctxt [allI] 2, BasicSimpTac ctxt state_kind false [] tac 2], resolve_tac ctxt [GuardsNil mode] 1, resolve_tac ctxt [GuardsConsGuaranteeStrip mode] 1, resolve_tac ctxt [GuardsCons mode] 1, SUBGOAL (guard_tac ctxt strip_guards (fn i => all_tac) mode) 1, EVERY[SUBGOAL (specAnno_tac ctxt state_kind (K all_tac) mode) 1], EVERY[SUBGOAL (whileAnnoFix_tac ctxt state_kind (K all_tac) mode) 1], EVERY[resolve_tac ctxt [SpecIf mode] 1,trace_tac ctxt "SpecIf", TRY (BasicSimpTac ctxt state_kind false [] tac 1)], EVERY[resolve_tac ctxt [Spec mode] 1, TRY (BasicSimpTac ctxt state_kind false [@{thm split_conv}] tac 1)], EVERY[resolve_tac ctxt [BindR mode] 1, resolve_tac ctxt [allI] 2, prefer_tac 2], EVERY[resolve_tac ctxt [FCall mode] 1], EVERY[resolve_tac ctxt [DynCom mode] 1], EVERY[SUBGOAL call 1, BasicSimpTac ctxt state_kind false [] tac 1], EVERY[SUBGOAL (lemAnno_tac ctxt state_kind mode) 1, BasicSimpTac ctxt state_kind false [] tac 1], final_simp_tac 1 ]) end; (*****************************************************************************) (** Generalise verification condition **) (*****************************************************************************) structure RecordSplitState : SPLIT_STATE = struct val globals = @{const_name StateSpace.state.globals}; fun isState (Const _$Abs (s,T,t)) = (case (state_hierarchy T) of ((n,_)::_) => n = "StateSpace.state.state" andalso is_none (try dest_hoare_raw (strip_qnt_body @{const_name All} t)) | _ => false) | isState _ = false; fun isFreeState (Free (_,T)) = (case (state_hierarchy T) of ((n,_)::_) => n = "StateSpace.state.state" | _ => false) | isFreeState _ = false; val abs_state = Option.map snd o first_subterm isFreeState; fun sel_eq (Const (x,_)$_) y = (x=y) | sel_eq t y = raise TERM ("RecordSplitState.sel_eq",[t]); val sel_idx = idx sel_eq; fun bound xs (t as (Const (x,_)$_)) = let val i = sel_idx xs x in if i < 0 then (length xs, xs@[t]) else (i,xs) end | bound xs t = raise TERM ("RecordSplitState.bound",[t]); fun abs_var _ (Const (x,T)$_) = (remdeco' (Long_Name.base_name x),range_type T) | abs_var _ t = raise TERM ("RecordSplitState.abs_var",[t]); fun fld_eq (x, _) y = (x = y) fun fld_idx xs x = idx fld_eq xs x; fun sort_vars ctxt T vars = let val thy = Proof_Context.theory_of ctxt; val (flds,_) = Record.get_recT_fields thy T; val gT = the (AList.lookup (fn (x:string,y) => x=y) flds globals); val (gflds,_) = (Record.get_recT_fields thy gT handle TYPE _ => ([],("",dummyT))); fun compare (Const _$Free _, Const _$(Const _$Free _)) = GREATER | compare (Const (s1,_)$Free _, Const (s2,_)$Free _) = int_ord (fld_idx flds s1, fld_idx flds s2) | compare (Const (s1,_)$(Const _$Free _), Const (s2,_)$(Const _$Free _)) = int_ord (fld_idx gflds s1, fld_idx gflds s2) | compare _ = LESS; in sort (rev_order o compare) vars end; fun fold_state_prop loc glob app abs other inc s res (t as (Const (sel,_)$Free (s',_))) = if s'=s then if is_state_var sel then loc inc res t else raise TERM ("RecordSplitState.fold_state_prop",[t]) else other res t | fold_state_prop loc glob app abs other inc s res (t as ((t1 as (Const (sel,_)))$(t2 as (Const (glb,_)$Free (s',_))))) = if s'=s andalso is_state_var sel andalso (glb=globals) then glob inc res t else let val res1 = fold_state_prop loc glob app abs other inc s res t1 val res2 = fold_state_prop loc glob app abs other inc s res1 t2 in app res1 res2 end | fold_state_prop loc glob app abs other inc s res (t as (Free (s',_))) = if s'=s then raise TERM ("RecordSplitState.fold_state_prop",[t]) else other res t | fold_state_prop loc glob app abs other inc s res (t1$t2) = let val res1 = fold_state_prop loc glob app abs other inc s res t1 val res2 = fold_state_prop loc glob app abs other inc s res1 t2 in app res1 res2 end | fold_state_prop loc glob app abs other inc s res (Abs (x,T,t)) = let val res1 = fold_state_prop loc glob app abs other (inc+1) s res t in abs x T res1 end | fold_state_prop loc glob app abs other inc s res t = other res t fun collect_vars s t = let fun loc _ vars t = snd (bound vars t); fun glob _ vars t = snd (bound vars t); fun app _ vars2 = vars2; fun abs _ _ vars = vars; fun other vars _ = vars; in fold_state_prop loc glob app abs other 0 s [] t end; fun abstract_vars vars s t = let fun loc inc _ t = let val i = fst (bound vars t) in Bound (i+inc) end; fun glob inc _ t = let val i = fst (bound vars t) in Bound (i+inc) end; fun app t1 t2 = t1$t2; fun abs x T t = Abs (x,T,t); fun other _ t = t; val dummy = Bound 0; in fold_state_prop loc glob app abs other 0 s dummy t end; fun split_state ctxt s T t = let val vars = collect_vars s t; val vars' = if Config.get ctxt sort_variables then sort_vars ctxt T vars else vars; in (abstract_vars vars' s t,rev vars') end; fun ex_tac ctxt _ st = Record.split_simp_tac ctxt @{thms simp_thms} (K ~1) 1 st; end; structure FunSplitState : SPLIT_STATE = struct val full_globalsN = @{const_name StateSpace.state.globals}; fun isState (Const _$Abs (s,T,t)) = (case (state_hierarchy T) of ((n,_)::_) => n = "StateSpace.state.state" andalso is_none (try dest_hoare_raw (strip_qnt_body @{const_name All} t)) | _ => false) | isState _ = false; fun isFreeState (Free (_,T)) = (case (state_hierarchy T) of ((n,_)::_) => n = "StateSpace.state.state" | _ => false) | isFreeState _ = false; val abs_state = Option.map snd o first_subterm isFreeState; fun comp_name t = case try (implode o dest_string) t of SOME str => str | NONE => (case t of Free (s,_) => s | Const (s,_) => s | t => raise TERM ("FunSplitState.comp_name",[t])) fun sel_name (Const _$_$name$_) = comp_name name | sel_name t = raise TERM ("FunSplitState.sel_name",[t]); fun sel_raw_name (Const _$_$name$_) = name | sel_raw_name t = raise TERM ("FunSplitState.sel_raw_name",[t]); fun component_type (Const _$_$_$(sel$_)) = range_type (fastype_of sel) | component_type t = raise TERM ("FunSplitState.component_type",[t]); fun component_name (Const _$_$_$((Const (sel,_)$_))) = sel | component_name t = raise TERM ("FunSplitState.component_name",[t]); fun sel_type (Const _$destr$_$_) = range_type (fastype_of destr) | sel_type t = raise TERM ("FunSplitState.sel_type",[t]); fun sel_destr (Const _$destr$_$_) = destr | sel_destr t = raise TERM ("FunSplitState.sel_destr",[t]); fun sel_eq t y = (sel_name t = y) | sel_eq t y = raise TERM ("FunSplitState.sel_eq",[t]); val sel_idx = idx sel_eq; fun bound xs t = let val i = sel_idx xs (sel_name t) in if i < 0 then (length xs, xs@[t]) else (i,xs) end | bound xs t = raise TERM ("FunSplitState.bound",[t]); fun fold_state_prop var app abs other inc s res (t as (Const (@{const_name StateFun.lookup},_)$destr$name$(Const _$Free (s',_)))) = if s'=s then var inc res t else other res t (*raise TERM ("FunSplitState.fold_state_prop",[t])*) | fold_state_prop var app abs other inc s res (t as (Free (s',_))) = if s'=s then raise TERM ("FunSplitState.fold_state_prop",[t]) else other res t | fold_state_prop var app abs other inc s res (t1$t2) = let val res1 = fold_state_prop var app abs other inc s res t1 val res2 = fold_state_prop var app abs other inc s res1 t2 in app res1 res2 end | fold_state_prop var app abs other inc s res (Abs (x,T,t)) = let val res1 = fold_state_prop var app abs other (inc+1) s res t in abs x T res1 end | fold_state_prop var app abs other inc s res t = other res t fun collect_vars s t = let fun var _ vars t = snd (bound vars t); fun app _ vars2 = vars2; fun abs _ _ vars = vars; fun other vars _ = vars; in fold_state_prop var app abs other 0 s [] t end; fun abstract_vars vars s t = let fun var inc _ t = let val i = fst (bound vars t) in Bound (i+inc) end; fun app t1 t2 = t1$t2; fun abs x T t = Abs (x,T,t); fun other _ t = t; val dummy = Bound 0; in fold_state_prop var app abs other 0 s dummy t end; fun sort_vars ctxt vars = let val fld_idx = idx (fn s1:string => fn s2 => s1 = s2); fun compare (_$_$n$(Const (s1,_)$_),_$_$m$(Const (s2,_)$_)) = let val n' = remdeco' (comp_name n); val m' = remdeco' (comp_name m); in if s1 = full_globalsN then if s2 = full_globalsN then string_ord (n',m') else LESS else if s2 = full_globalsN then GREATER else string_ord (n',m') end | compare (t1,t2) = raise TERM ("FunSplitState.sort_vars.compare",[t1,t2]); in sort (rev_order o compare) vars end; fun split_state ctxt s _ t = let val vars = collect_vars s t; val vars' = if Config.get ctxt sort_variables then sort_vars ctxt vars else vars; in (abstract_vars vars' s t,rev vars') end; fun abs_var _ t = (remdeco' (sel_name t), sel_type t); (* Proof for: EX x_1 ... x_n. P x_1 ... x_n * ==> EX s. P (lookup destr_1 "x_1" s) ... (lookup destr_n "x_n" s) * Implementation: * 1. Eliminate existential quantifiers in premise * 2. Instantiate s with: (%x. undefined)("x_1" := constr_1 x_1, ..., "x_n" := constr_n x_n) * 3. Simplify *) local val ss = simpset_of (put_simpset (simpset_of @{theory_context Fun}) @{context} addsimps (@{thm StateFun.lookup_def} :: @{thm StateFun.id_id_cancel} :: @{thms list.inject list.distinct char.inject cong_exp_iff_simps simp_thms}) addsimprocs [Record.simproc, StateFun.lazy_conj_simproc] |> fold Simplifier.add_cong @{thms block_conj_cong}); in fun ex_tac ctxt vs st = let val vs' = rev vs; val (Const (_,exT)$_) = HOLogic.dest_Trueprop (Logic.strip_imp_concl (Logic.get_goal (Thm.prop_of st) 1)); val sT = domain_type (domain_type exT); val s0 = Const (@{const_name HOL.undefined},sT); fun streq (s1:string,s2) = s1=s2 ; fun mk_init [] = [] | mk_init (t::ts) = let val xs = mk_init ts; val n = component_name t; val T = component_type t; in if AList.defined streq xs n then xs else (n,(T,Const (n,sT --> component_type t)$s0))::xs end; fun mk_upd (i,t) xs = let val selN = component_name t; val selT = component_type t; val (_,s) = the (AList.lookup streq xs selN); val strT = domain_type selT; val valT = range_type selT; val constr = destr_to_constr (sel_destr t); val name = (sel_raw_name t); val upd = Const (@{const_name Fun.fun_upd}, (strT --> valT)-->strT-->valT--> (strT --> valT)) $ s $ name $ (constr $ Bound i) in AList.update streq (selN,(selT,upd)) xs end; val upds = fold_index mk_upd vs' (mk_init vs'); val upd = fold (fn (n,(T,upd)) => fn s => Const (n ^ Record.updateN, T --> sT --> sT)$upd$s) upds s0; val inst = fold_rev (Term.abs o (fn t => (sel_name t, sel_type t))) vs upd; fun lift_inst_ex_tac i st = let val rule = Thm.lift_rule (Thm.cprem_of st i) (Drule.incr_indexes st exI); val (_$x) = HOLogic.dest_Trueprop (Logic.strip_assums_concl (hd (Thm.prems_of rule))); val inst_rule = infer_instantiate ctxt [(#1 (dest_Var (head_of x)), Thm.cterm_of ctxt inst)] rule; in (compose_tac ctxt (false,inst_rule, Thm.nprems_of exI) i st) end; in EVERY [REPEAT_DETERM_N (length vs) (eresolve_tac ctxt [exE] 1), lift_inst_ex_tac 1, simp_tac (put_simpset ss ctxt) 1 ] st end end (* Test: What happens when there are no lookups., EX s. True *) end; structure GeneraliseRecord = GeneraliseFun (structure SplitState=RecordSplitState); structure GeneraliseStateFun = GeneraliseFun (structure SplitState=FunSplitState); fun generalise Record = GeneraliseRecord.GENERALISE | generalise Function = GeneraliseStateFun.GENERALISE; (*****************************************************************************) (** record_vanish_tac splits up the records of a verification condition, **) (** trying to generate a predicate without records. **) (** A typical verification condition with a procedure call will have the **) (** form "!!s Z. s=Z ==> ..., where s and Z are records **) (*****************************************************************************) (* FIXME: Check out if removing the useless vars is a performance issue. If so, maybe we can remove all useless vars at once (no iterated simplification) or try to avoid introducing them. Bevore splitting the gaol we can simplifiy the goal with state_simproc this may leed to better performance... *) fun record_vanish_tac ctxt state_kind state_space i = if Config.get ctxt record_vanish then let val rem_useless_vars_simps = [Drule.triv_forall_equality,@{thm Hoare.triv_All_eq},@{thm Hoare.triv_Ex_eq}]; val rem_useless_vars_simpset = empty_simpset ctxt addsimps rem_useless_vars_simps; fun no_spec (t as (Const (@{const_name All},_)$_)) = is_none (try dest_hoare_raw (strip_qnt_body @{const_name All} t)) | no_spec _ = true; fun state_space_no_spec t = if state_space t <> 0 andalso no_spec t then ~1 else 0; in EVERY [trace_tac ctxt "record_vanish_tac -- START --", REPEAT (eresolve_tac ctxt [conjE] i), trace_tac ctxt "record_vanish_tac -- hyp_subst_tac ctxt --", TRY (hyp_subst_tac_thin true ctxt i), full_simp_tac rem_useless_vars_simpset i, (* hyp_subst_tac may have made some state variables unnecessary. We do not want to split them to avoid naming conflicts and increase performance *) trace_tac ctxt "record_vanish_tac -- Splitting records --", if Config.get ctxt use_generalise orelse state_kind = Function then generalise state_kind ctxt i else state_split_simp_tac ctxt rem_useless_vars_simps state_space_no_spec i (*THEN_MAYBE EVERY [trace_tac ctxt "record_vanish_tac -- removing useless vars --", full_simp_tac rem_useless_vars_simpset i, trace_tac ctxt "record_vanish_tac -- STOP --"]*) ] end else all_tac; (* solve_modifies_tac tries to solve modifies-clauses automatically; * The following strategy is followed: * After clar-simplifying the modifies clause we remain with a goal of the form * * EX a b. s(|A := x|) = s(|A:=a,B:=b|) * * (or because of conditional statements conjunctions of these kind of goals) * We split up the state-records and simplify (record_vanish_tac) and get to a goal of the form: * * EX a b. (|A=x,B=B|) = (|A=a,B=b|). * * If the modifies clause was correct we just have to introduce the existential quantifies * and apply reflexivity. * If not we just simplify the goal. *) local val state_fun_update_ss = simpset_of (put_simpset HOL_basic_ss @{context} addsimps ([@{thm StateFun.update_def}, @{thm id_def}, @{thm fun_upd_apply}, @{thm if_True}, @{thm if_False}] @ @{thms list.inject list.distinct char.inject cong_exp_iff_simps simp_thms} @ K_fun_convs) addsimprocs [DistinctTreeProver.distinct_simproc ["distinct_fields", "distinct_fields_globals"]] |> Simplifier.add_cong @{thm imp_cong} (* K_fun_congs FIXME: Stefan fragen*) |> Splitter.add_split @{thm if_split}); in fun solve_modifies_tac ctxt state_kind state_space i st = let val thy = Proof_Context.theory_of ctxt; fun is_split_state (trm as (Const (@{const_name Pure.all},_)$Abs(x,T,t))) = if state_space trm <> 0 then try (fn () => let fun seed (_ $ v $ st) = seed st | seed (_ $ t) = (1,t) (* split only state pair *) | seed t = (~1,t) (* split globals completely *) val all_vars = strip_qnt_vars @{const_name Pure.all} t; val concl = HOLogic.dest_Trueprop (Logic.strip_assums_concl t); val ex_vars = strip_qnt_vars @{const_name Ex} concl; val state = Bound (length all_vars + length ex_vars); val (Const (@{const_name HOL.eq},_)$x_upd$x_upd') = strip_qnt_body @{const_name Ex} concl; val (split,sd) = seed x_upd; in if sd = state then split else 0 end) () |> the_default 0 else 0 | is_split_state t = 0; val simp_ctxt = put_simpset HOL_ss ctxt addsimps (@{thm Ex_True} :: @{thm Ex_False} :: Record.get_extinjects thy); fun try_solve Record i = (*(SOLVE*) (((fn k => (TRY (REPEAT_ALL_NEW (resolve_tac ctxt [conjI, impI, allI]) k))) THEN_ALL_NEW (fn k => EVERY [state_split_simp_tac ctxt [] is_split_state k, simp_tac simp_ctxt k THEN_MAYBE rename_goal ctxt remdeco' k ])) i) (*)*) | try_solve _ i = ((fn k => (TRY (REPEAT_ALL_NEW (resolve_tac ctxt [conjI, impI, allI]) k))) THEN_ALL_NEW (fn k => REPEAT (resolve_tac ctxt [exI] k) THEN resolve_tac ctxt [ext] k THEN simp_tac (put_simpset state_fun_update_ss ctxt) k THEN_MAYBE (REPEAT_ALL_NEW (resolve_tac ctxt [conjI,impI,refl]) k))) i in ((trace_tac ctxt "solve_modifies_tac" THEN clarsimp_tac ((ctxt |> put_claset (claset_of @{theory_context HOL}) |> put_simpset (simpset_of @{theory_context Set})) addsimps ([@{thm Hoare.mex_def},@{thm Hoare.meq_def}]@K_convs) addsimprocs (state_upd_simproc Record::(state_simprocs Record)) |> fold Simplifier.add_cong K_congs) i) THEN_MAYBE try_solve state_kind i) st end; end fun proc_lookup_simp_tac ctxt i st = try (fn () => let val name = (Logic.concl_of_goal (Thm.prop_of st) i) |> dest_hoare |> #2 |> strip_comb |> #2 |> last |> strip_comb |> #2 |> last; (* the$(Gamma$name) or the$(strip$Gamma$name) *) val pname = (unsuffix proc_deco (dest_string' name)); val thms = map_filter I (map (try (Proof_Context.get_thm ctxt)) [suffix bodyP pname, suffix (body_def_sfx^"_def") pname, suffix procL pname^"."^ (suffix (body_def_sfx^"_def") pname)]); in simp_tac (put_simpset HOL_basic_ss ctxt addsimps thms @ strip_simps @ @{thms option.sel}) i st end) () |> the_default (Seq.single st); fun proc_lookup_in_dom_simp_tac ctxt i st = try (fn () => let val _$name$_ = (HOLogic.dest_Trueprop (Logic.concl_of_goal (Thm.prop_of st) i)); (* name : Gamma *) val pname = (unsuffix proc_deco (dest_string' name)); val thms = map_filter I (map (try (Proof_Context.get_thm ctxt)) [suffix bodyP pname]); in simp_tac (put_simpset HOL_basic_ss ctxt addsimps (@{thm Hoare.lookup_Some_in_dom} :: @{thm dom_strip} :: thms)) i st end) () |> the_default (Seq.single st); fun HoareRuleTac ctxt insts fixes st = let val annotate_simp_tac = simp_tac (put_simpset HOL_basic_ss ctxt addsimps (anno_defs@normalize_simps) addsimprocs [@{simproc case_prod_beta}]); fun is_com_eq (Const (@{const_name Trueprop},_)$(Const (@{const_name HOL.eq},T)$_$_)) = (case (binder_types T) of (Type (@{type_name Language.com},_)::_) => true | _ => false) | is_com_eq _ = false; fun annotate_tac i st = if is_com_eq (Logic.concl_of_goal (Thm.prop_of st) i) then annotate_simp_tac i st else all_tac st; in ((fn i => REPEAT (resolve_tac ctxt [allI] i)) THEN' Rule_Insts.res_inst_tac ctxt insts fixes st) THEN_ALL_NEW annotate_tac end; fun HoareCallRuleTac state_kind state_space ctxt thms i st = let fun dest_All (Const (@{const_name All},_)$t) = SOME t | dest_All _ = NONE; fun auxvars t = (case (map_filter ((first_subterm is_hoare) o snd) (max_subterms_dest dest_All t)) of ((vars,_)::_) => vars | _ => []); fun auxtype rule = (case (auxvars (Thm.prop_of rule)) of [] => NONE | vs => (case (last vs) of (_,TVar (z,_)) => SOME (z,rule) | _ => NONE)); val thms' = let val auxvs = map fst (auxvars (Logic.concl_of_goal (Thm.prop_of st) i)); val tvar_thms = map_filter auxtype thms in if length thms = length tvar_thms then adapt_aux_var ctxt true auxvs tvar_thms else thms end; val is_sidecondition = not o can dest_hoare; fun solve_sidecondition_tac (t,i) = if is_sidecondition t then FIRST [CHANGED_PROP (wf_tac ctxt i), (*init_conforms_tac state_kind state_space i,*) post_conforms_tac ctxt state_kind i THEN_MAYBE (if is_modifies_clause t then solve_modifies_tac ctxt state_kind state_space i else all_tac), proc_lookup_in_dom_simp_tac ctxt i ] else in_rel_simp ctxt i THEN simp_tac (put_simpset HOL_basic_ss ctxt addsimps [@{thm Un_empty_left},@{thm Un_empty_right}]) i THEN proc_lookup_simp_tac ctxt i fun basic_tac i = (((resolve_tac ctxt thms') THEN_ALL_NEW (fn k => (SUBGOAL solve_sidecondition_tac k))) i) in (basic_tac ORELSE' (fn k => (REPEAT (resolve_tac ctxt [allI] k)) THEN EVERY [resolve_tac ctxt thms' k])) i st end; (* vcg_polish_tac tries to solve modifies-clauses automatically; for other specifications the * records are only splitted and simplified. *) fun vcg_polish_tac solve_modifies ctxt state_kind state_space i = if solve_modifies then solve_modifies_tac ctxt state_kind state_space i else record_vanish_tac ctxt state_kind state_space i THEN_MAYBE EVERY [rename_goal ctxt remdeco' i(*, simp_tac (HOL_basic_ss addsimps @{thms simp_thms})) i*)]; fun is_funtype (Type ("fun", _)) = true | is_funtype _ = false; fun state_kind_of ctxt T = let val thy = Proof_Context.theory_of ctxt; val (s,sT) = nth (fst (Record.get_recT_fields thy T)) 1; in if Long_Name.base_name s = "locals" andalso is_funtype sT then Function else Record end handle Subscript => Record; fun find_state_space_in_triple ctxt t = try (fn () => (case first_subterm is_hoare t of NONE => NONE | SOME (abs_vars,triple) => let val (_,com,_,_,mode,_,_,_) = dest_hoare_raw triple; val T = fastype_of1 (map snd abs_vars,com) val Type(_,state_spaceT::_) = T; val SOME Tids = stateT_ids state_spaceT; in SOME (Tids,mode, state_kind_of ctxt state_spaceT) end)) () |> Option.join; fun get_state_space_in_subset_eq ctxt t = (* get state type from the following kind of terms: P <= Q, s: P *) try (fn () => let val (subset_eq,_) = (strip_comb o HOLogic.dest_Trueprop o strip_qnt_body @{const_name Pure.all}) t; val Ts = map snd (strip_vars t); val T = fastype_of1 (Ts,subset_eq); val Type (_, [_,Type (_, [Type (_, [state_spaceT]), _])]) = T; (* also works for "in": x : P *) val SOME Tids = stateT_ids state_spaceT; in (Tids,Partial, state_kind_of ctxt state_spaceT) end) (); fun get_state_space ctxt i st = (case try (Logic.concl_of_goal (Thm.prop_of st)) i of SOME t => (case find_state_space_in_triple ctxt t of SOME sp => SOME sp | NONE => get_state_space_in_subset_eq ctxt t) | NONE => NONE); fun mk_hoare_tac hoare_tac finish_tac annotate_inv exnames strip_guards spec_sfx ctxt i st = case get_state_space ctxt i st of SOME (Tids,mode,kind) => SELECT_GOAL (hoare_tac annotate_inv exnames strip_guards mode kind (is_state_space_var Tids) spec_sfx ctxt (finish_tac kind (is_state_space_var Tids))) i st | NONE => no_tac st fun vcg_tac spec_sfx strip_guards exnames ctxt i st = mk_hoare_tac HoareTac (vcg_polish_tac (spec_sfx="_modifies") ctxt) (spec_sfx="_modifies") exnames (strip_guards="true") spec_sfx ctxt i st; fun hoare_tac spec_sfx strip_guards _ ctxt i st = let fun tac state_kind state_space i = if spec_sfx="_modifies" then solve_modifies_tac ctxt state_kind state_space i else all_tac; in mk_hoare_tac HoareTac tac (spec_sfx="_modifies") [] (strip_guards="true") spec_sfx ctxt i st end; fun hoare_raw_tac spec_sfx strip_guards exnames ctxt i st = mk_hoare_tac HoareTac (K (K (K all_tac))) (spec_sfx="_modifies") [] (strip_guards="true") spec_sfx ctxt i st; fun hoare_step_tac spec_sfx strip_guards exnames ctxt i st = mk_hoare_tac (K (K HoareStepTac)) (vcg_polish_tac (spec_sfx="_modifies") ctxt) false [] (strip_guards="true") spec_sfx ctxt i st; fun hoare_rule_tac ctxt thms i st = SUBGOAL (fn _ => (case get_state_space ctxt i st of SOME (Tids,_,kind) => HoareCallRuleTac kind (is_state_space_var Tids) ctxt thms i | NONE => error "could not find proper state space type (structure or record) in goal")) i st; (*** Methods ***) val hoare_rule = Rule_Insts.method HoareRuleTac hoare_rule_tac; val argP = Args.name --| @{keyword "="} -- Args.name val argsP = Scan.repeat argP val default_args = [("spec","spec"),("strip_guards","false")] val vcg_simp_modifiers = [Args.add -- Args.colon >> K (Method.modifier vcg_simp_add \<^here>), Args.del -- Args.colon >> K (Method.modifier vcg_simp_del \<^here>)]; fun assocs2 key = map snd o filter (curry (op =) key o fst); fun gen_simp_method tac = Scan.lift (argsP >> (fn args => args @ default_args)) --| Method.sections vcg_simp_modifiers >> (fn args => fn ctxt => Method.SIMPLE_METHOD' (tac ("_" ^ the (AList.lookup (op =) args "spec")) (the (AList.lookup (op =) args "strip_guards")) (assocs2 "exspec" args) ctxt)); val hoare = gen_simp_method hoare_tac; val hoare_raw = gen_simp_method hoare_raw_tac; val vcg = gen_simp_method vcg_tac; val vcg_step = gen_simp_method hoare_step_tac; val trace_hoare_users = Unsynchronized.ref false fun print_subgoal_tac ctxt s i = SUBGOAL (fn (prem, _) => trace_tac ctxt (s ^ (Syntax.string_of_term ctxt prem))) i fun mk_hoare_thm thm _ ctxt _ i = EVERY [resolve_tac ctxt [thm] i, if !trace_hoare_users then print_subgoal_tac ctxt "Tracing: " i else all_tac] val vcg_hoare_add = Thm.declaration_attribute (fn thm => add_hoare_tacs [(Thm.derivation_name thm, mk_hoare_thm thm)]) exception UNDEF val vcg_hoare_del = Thm.declaration_attribute (fn _ => fn _ => raise UNDEF) (* setup theory *) val _ = Theory.setup (Attrib.setup @{binding vcg_simp} (Attrib.add_del vcg_simp_add vcg_simp_del) "declaration of Simplifier rule for vcg" #> Attrib.setup @{binding vcg_hoare} (Attrib.add_del vcg_hoare_add vcg_hoare_del) "declaration of wp rule for vcg") (*#> add_wp_tacs initial_wp_tacs*) end;