diff -r 56a87a5093be -r cd935b7cb3fb src/Pure/Isar/code.ML --- a/src/Pure/Isar/code.ML Mon Jul 03 14:25:07 2017 +0200 +++ b/src/Pure/Isar/code.ML Sun Jul 02 20:13:38 2017 +0200 @@ -30,29 +30,28 @@ val pretty_cert: theory -> cert -> Pretty.T list (*executable code*) - val add_datatype: (string * typ) list -> theory -> theory - val add_datatype_cmd: string list -> theory -> theory + val declare_datatype_global: (string * typ) list -> theory -> theory + val declare_datatype_cmd: string list -> theory -> theory val datatype_interpretation: (string * ((string * sort) list * (string * ((string * sort) list * typ list)) list) -> theory -> theory) -> theory -> theory - val add_abstype: thm -> theory -> theory - val add_abstype_default: thm -> theory -> theory + val declare_abstype: thm -> local_theory -> local_theory + val declare_abstype_global: thm -> theory -> theory val abstype_interpretation: (string * ((string * sort) list * ((string * ((string * sort) list * typ)) * (string * thm))) -> theory -> theory) -> theory -> theory - type kind - val Equation: kind - val Nbe: kind - val Abstract: kind - val add_eqn: kind * bool -> thm -> theory -> theory - val add_default_eqn_attribute: kind -> attribute - val add_default_eqn_attrib: kind -> Token.src - val del_eqn_silent: thm -> theory -> theory - val del_eqn: thm -> theory -> theory - val del_eqns: string -> theory -> theory - val del_exception: string -> theory -> theory - val add_case: thm -> theory -> theory - val add_undefined: string -> theory -> theory + val declare_default_eqns: (thm * bool) list -> local_theory -> local_theory + val declare_default_eqns_global: (thm * bool) list -> theory -> theory + val declare_eqns: (thm * bool) list -> local_theory -> local_theory + val declare_eqns_global: (thm * bool) list -> theory -> theory + val add_eqn_global: thm * bool -> theory -> theory + val del_eqn_global: thm -> theory -> theory + val declare_abstract_eqn: thm -> local_theory -> local_theory + val declare_abstract_eqn_global: thm -> theory -> theory + val declare_empty_global: string -> theory -> theory + val declare_unimplemented_global: string -> theory -> theory + val declare_case_global: thm -> theory -> theory + val declare_undefined_global: string -> theory -> theory val get_type: theory -> string -> ((string * sort) list * (string * ((string * sort) list * typ list)) list) * bool val get_type_of_constr_or_abstr: theory -> string -> (string * bool) option @@ -169,21 +168,17 @@ (* functions *) datatype fun_spec = Unimplemented - | Eqns_Default of (thm * bool) list * (thm * bool) list lazy - (* (cache for default equations, lazy computation of default equations) - -- helps to restore natural order of default equations *) + | Eqns_Default of (thm * bool) list | Eqns of (thm * bool) list - | Proj of (term * string) * bool - | Abstr of (thm * string) * bool; + | Proj of term * string + | Abstr of thm * string; -val default_fun_spec = Eqns_Default ([], Lazy.value []); +val default_fun_spec = Eqns_Default []; fun is_default (Eqns_Default _) = true - | is_default (Proj (_, default)) = default - | is_default (Abstr (_, default)) = default | is_default _ = false; -fun associated_abstype (Abstr ((_, tyco), _)) = SOME tyco +fun associated_abstype (Abstr (_, tyco)) = SOME tyco | associated_abstype _ = NONE; @@ -648,6 +643,33 @@ fun canonize_thms thy = desymbolize_tvars thy #> same_arity thy #> map (desymbolize_vars thy); +(* preparation and classification of code equations *) + +fun prep_eqn strictness thy = + apfst (meta_rewrite thy) + #> generic_assert_eqn strictness thy false + #> Option.map (fn eqn => (const_eqn thy (fst eqn), eqn)); + +fun prep_eqns strictness thy = + map_filter (prep_eqn strictness thy) + #> AList.group (op =); + +fun prep_abs_eqn strictness thy = + meta_rewrite thy + #> generic_assert_abs_eqn strictness thy NONE + #> Option.map (fn abs_eqn => (const_abs_eqn thy (fst abs_eqn), abs_eqn)); + +fun prep_maybe_abs_eqn thy raw_thm = + let + val thm = meta_rewrite thy raw_thm; + val some_abs_thm = generic_assert_abs_eqn Silent thy NONE thm; + in case some_abs_thm of + SOME (thm, tyco) => SOME (const_abs_eqn thy thm, ((thm, true), SOME tyco)) + | NONE => generic_assert_eqn Liberal thy false (thm, false) + |> Option.map (fn (thm, _) => (const_eqn thy thm, ((thm, is_linear thm), NONE))) + end; + + (* abstype certificates *) local @@ -947,12 +969,12 @@ fun get_cert ctxt functrans c = case retrieve_raw (Proof_Context.theory_of ctxt) c of Unimplemented => nothing_cert ctxt c - | Eqns_Default (_, eqns_lazy) => Lazy.force eqns_lazy + | Eqns_Default eqns => eqns |> cert_of_eqns_preprocess ctxt functrans c | Eqns eqns => eqns |> cert_of_eqns_preprocess ctxt functrans c - | Proj ((_, tyco), _) => cert_of_proj ctxt c tyco - | Abstr ((abs_thm, tyco), _) => abs_thm + | Proj (_, tyco) => cert_of_proj ctxt c tyco + | Abstr (abs_thm, tyco) => abs_thm |> preprocess Conv.arg_conv ctxt |> cert_of_abs ctxt tyco c; @@ -1027,13 +1049,13 @@ fun pretty_equations const thms = (Pretty.block o Pretty.fbreaks) (Pretty.str (string_of_const thy const) :: map (Thm.pretty_thm_item ctxt) thms); - fun pretty_function (const, Eqns_Default (_, eqns_lazy)) = - pretty_equations const (map fst (Lazy.force eqns_lazy)) + fun pretty_function (const, Eqns_Default eqns) = + pretty_equations const (map fst eqns) | pretty_function (const, Eqns eqns) = pretty_equations const (map fst eqns) - | pretty_function (const, Proj ((proj, _), _)) = Pretty.block + | pretty_function (const, Proj (proj, _)) = Pretty.block [Pretty.str (string_of_const thy const), Pretty.fbrk, Syntax.pretty_term ctxt proj] - | pretty_function (const, Abstr ((thm, _), _)) = pretty_equations const [thm]; + | pretty_function (const, Abstr (thm, _)) = pretty_equations const [thm]; fun pretty_typ (tyco, vs) = Pretty.str (string_of_typ thy (Type (tyco, map TFree vs))); fun pretty_typspec (typ, (cos, abstract)) = if null cos @@ -1089,118 +1111,114 @@ (* code equations *) (* - external distinction: - kind * default - processual distinction: - thm * proper for concrete equations - thm for abstract equations - strictness wrt. shape of theorem propositions: - * default attributes: silent - * user attributes: warnings (after morphism application!) - * Isabelle/ML functions: strict + * default equations: silent + * using declarations and attributes: warnings (after morphism application!) + * using global declarations (... -> thy -> thy): strict * internal processing after storage: strict *) -fun gen_add_eqn default (raw_thm, proper) thy = - let - val thm = Thm.close_derivation raw_thm; - val c = const_eqn thy thm; - fun update_subsume verbose (thm, proper) eqns = - let - val args_of = snd o take_prefix is_Var o rev o snd o strip_comb - o Term.map_types Type.strip_sorts o fst o Logic.dest_equals o Thm.plain_prop_of; - val args = args_of thm; - val incr_idx = Logic.incr_indexes ([], [], Thm.maxidx_of thm + 1); - fun matches_args args' = - let - val k = length args' - length args - in if k >= 0 - then Pattern.matchess thy (args, (map incr_idx o drop k) args') - else false - end; - fun drop (thm', proper') = if (proper orelse not proper') - andalso matches_args (args_of thm') then - (if verbose then warning ("Code generator: dropping subsumed code equation\n" ^ - Thm.string_of_thm_global thy thm') else (); true) - else false; - in (thm, proper) :: filter_out drop eqns end; - fun natural_order eqns = - (eqns, Lazy.lazy_name "code" (fn () => fold (update_subsume false) eqns [])) - fun add_eqn' true Unimplemented = Eqns_Default (natural_order [(thm, proper)]) - | add_eqn' true (Eqns_Default (eqns, _)) = Eqns_Default (natural_order ((thm, proper) :: eqns)) - (*this restores the natural order and drops syntactic redundancies*) - | add_eqn' true fun_spec = fun_spec - | add_eqn' false (Eqns eqns) = Eqns (update_subsume true (thm, proper) eqns) - | add_eqn' false _ = Eqns [(thm, proper)]; - in change_fun_spec c (add_eqn' default) thy end; +fun generic_code_declaration strictness lift_phi f x = + Local_Theory.declaration + {syntax = false, pervasive = false} + (fn phi => Context.mapping (f strictness (lift_phi phi x)) I); -fun gen_add_abs_eqn default raw_thm thy = +fun silent_code_declaration lift_phi = generic_code_declaration Silent lift_phi; +fun code_declaration lift_phi = generic_code_declaration Liberal lift_phi; + +local + +fun subsumptive_add thy verbose (thm, proper) eqns = let - val (abs_thm, tyco) = apfst Thm.close_derivation raw_thm; - val c = const_abs_eqn thy abs_thm; - in change_fun_spec c (K (Abstr ((abs_thm, tyco), default))) thy end; - -datatype kind = Equation | Nbe | Abstract; + val args_of = snd o take_prefix is_Var o rev o snd o strip_comb + o Term.map_types Type.strip_sorts o fst o Logic.dest_equals o Thm.plain_prop_of; + val args = args_of thm; + val incr_idx = Logic.incr_indexes ([], [], Thm.maxidx_of thm + 1); + fun matches_args args' = + let + val k = length args' - length args + in if k >= 0 + then Pattern.matchess thy (args, (map incr_idx o drop k) args') + else false + end; + fun drop (thm', proper') = if (proper orelse not proper') + andalso matches_args (args_of thm') then + (if verbose then warning ("Code generator: dropping subsumed code equation\n" ^ + Thm.string_of_thm_global thy thm') else (); true) + else false; + in (thm, proper) :: filter_out drop eqns end; -fun mk_eqn strictness thy = generic_assert_eqn strictness thy false o - apfst (meta_rewrite thy); - -fun mk_abs_eqn strictness thy = generic_assert_abs_eqn strictness thy NONE o - meta_rewrite thy; - -fun mk_maybe_abs_eqn thy raw_thm = +fun add_eqn_for (c, proto_eqn) thy = let - val thm = meta_rewrite thy raw_thm; - val some_abs_thm = generic_assert_abs_eqn Silent thy NONE thm; - in case some_abs_thm - of SOME (thm, tyco) => SOME ((thm, true), SOME tyco) - | NONE => Option.map (fn (thm, _) => ((thm, is_linear thm), NONE)) - (generic_assert_eqn Liberal thy false (thm, false)) - end; + val eqn = apfst Thm.close_derivation proto_eqn; + fun add (Eqns eqns) = Eqns (subsumptive_add thy true eqn eqns) + | add _ = Eqns [eqn]; + in change_fun_spec c add thy end; + +fun add_eqns_for default (c, proto_eqns) thy = + let + val eqns = [] + |> fold_rev (subsumptive_add thy (not default)) proto_eqns + |> (map o apfst) Thm.close_derivation; + fun add (Eqns_Default _) = Eqns_Default eqns + | add data = data; + in change_fun_spec c (if default then add else K (Eqns eqns)) thy end; -fun generic_add_eqn strictness (kind, default) thm thy = - case kind of - Equation => fold (gen_add_eqn default) - (the_list (mk_eqn strictness thy (thm, true))) thy - | Nbe => fold (gen_add_eqn default) - (the_list (mk_eqn strictness thy (thm, false))) thy - | Abstract => fold (gen_add_abs_eqn default) - (the_list (mk_abs_eqn strictness thy thm)) thy; +fun add_abstract_for (c, proto_abs_eqn) = + let + val abs_eqn = apfst Thm.close_derivation proto_abs_eqn; + in change_fun_spec c (K (Abstr abs_eqn)) end; + +in -val add_eqn = generic_add_eqn Strict; - -fun lift_attribute f = Thm.declaration_attribute - (fn thm => Context.mapping (f thm) I); +fun generic_declare_eqns default strictness raw_eqns thy = + fold (add_eqns_for default) (prep_eqns strictness thy raw_eqns) thy; -fun add_default_eqn_attribute kind = - lift_attribute (generic_add_eqn Silent (kind, true)); +fun generic_add_eqn strictness raw_eqn thy = + fold add_eqn_for (the_list (prep_eqn strictness thy raw_eqn)) thy; -fun add_default_eqn_attrib kind = - Attrib.internal (K (add_default_eqn_attribute kind)); +fun generic_declare_abstract_eqn strictness raw_abs_eqn thy = + fold add_abstract_for (the_list (prep_abs_eqn strictness thy raw_abs_eqn)) thy; fun add_maybe_abs_eqn_liberal thm thy = - case mk_maybe_abs_eqn thy thm - of SOME (eqn, NONE) => gen_add_eqn false eqn thy - | SOME ((thm, _), SOME tyco) => gen_add_abs_eqn false (thm, tyco) thy + case prep_maybe_abs_eqn thy thm + of SOME (c, (eqn, NONE)) => add_eqn_for (c, eqn) thy + | SOME (c, ((thm, _), SOME tyco)) => add_abstract_for (c, (thm, tyco)) thy | NONE => thy; -fun generic_del_eqn strictness thm thy = case mk_eqn strictness thy (thm, true) - of SOME (thm, _) => +end; + +val declare_default_eqns_global = generic_declare_eqns true Silent; + +val declare_default_eqns = + silent_code_declaration (map o apfst o Morphism.thm) (generic_declare_eqns true); + +val declare_eqns_global = generic_declare_eqns false Strict; + +val declare_eqns = + code_declaration (map o apfst o Morphism.thm) (generic_declare_eqns false); + +val add_eqn_global = generic_add_eqn Strict; + +fun del_eqn_global thm thy = + case prep_eqn Liberal thy (thm, false) of + SOME (c, (thm, _)) => let - fun del_eqn' (Eqns_Default _) = default_fun_spec - | del_eqn' (Eqns eqns) = + fun del (Eqns_Default _) = Eqns [] + | del (Eqns eqns) = Eqns (filter_out (fn (thm', _) => Thm.eq_thm_prop (thm, thm')) eqns) - | del_eqn' spec = spec - in change_fun_spec (const_eqn thy thm) del_eqn' thy end + | del spec = spec + in change_fun_spec c del thy end | NONE => thy; -val del_eqn_silent = generic_del_eqn Silent; -val del_eqn = generic_del_eqn Liberal; +val declare_abstract_eqn_global = generic_declare_abstract_eqn Strict; -fun del_eqns c = change_fun_spec c (K Unimplemented); +val declare_abstract_eqn = + code_declaration Morphism.thm generic_declare_abstract_eqn; -fun del_exception c = change_fun_spec c (K (Eqns [])); +fun declare_empty_global c = change_fun_spec c (K (Eqns [])); + +fun declare_unimplemented_global c = change_fun_spec c (K Unimplemented); (* cases *) @@ -1223,7 +1241,7 @@ THEN ALLGOALS (Proof_Context.fact_tac ctxt' [Drule.reflexive_thm])) end; -fun add_case thm thy = +fun declare_case_global thm thy = let val (case_const, (k, cos)) = case_cert thm; val _ = case (filter_out (is_constr thy) o map_filter I) cos @@ -1246,7 +1264,7 @@ |-> (fn cong => map_spec_purge (register_case cong #> register_type)) end; -fun add_undefined c = +fun declare_undefined_global c = (map_spec_purge o map_cases) (Symtab.update (c, Undefined)); @@ -1273,7 +1291,7 @@ then insert (op =) c else I | _ => I) cases []) cases; in thy - |> fold del_eqns (outdated_funs1 @ outdated_funs2) + |> fold declare_unimplemented_global (outdated_funs1 @ outdated_funs2) |> map_spec_purge ((map_types o Symtab.map_default (tyco, [])) (cons (serial (), vs_spec)) #> map_cases drop_outdated_cases) @@ -1292,7 +1310,7 @@ |> f (tyco, fst (get_type thy tyco)) |> Sign.restore_naming thy)); -fun add_datatype proto_constrs thy = +fun declare_datatype_global proto_constrs thy = let fun unoverload_const_typ (c, ty) = (Axclass.unoverload_const thy (c, ty), ty); @@ -1304,8 +1322,8 @@ |> Named_Target.theory_map (Datatype_Plugin.data_default tyco) end; -fun add_datatype_cmd raw_constrs thy = - add_datatype (map (read_bare_const thy) raw_constrs) thy; +fun declare_datatype_cmd raw_constrs thy = + declare_datatype_global (map (read_bare_const thy) raw_constrs) thy; structure Abstype_Plugin = Plugin(type T = string); @@ -1316,35 +1334,48 @@ (fn tyco => Local_Theory.background_theory (fn thy => f (tyco, get_abstype_spec thy tyco) thy)); -fun generic_add_abstype strictness default proto_thm thy = +fun generic_declare_abstype strictness proto_thm thy = case check_abstype_cert strictness thy proto_thm of SOME (tyco, (vs, (abs_ty as (abs, (_, ty)), (rep, cert)))) => thy |> register_type (tyco, (vs, Abstractor (abs_ty, (rep, cert)))) |> change_fun_spec rep - (K (Proj ((Logic.varify_types_global (mk_proj tyco vs ty abs rep), tyco), default))) + (K (Proj (Logic.varify_types_global (mk_proj tyco vs ty abs rep), tyco))) |> Named_Target.theory_map (Abstype_Plugin.data_default tyco) | NONE => thy; -val add_abstype = generic_add_abstype Strict false; -val add_abstype_default = generic_add_abstype Strict true; +val declare_abstype_global = generic_declare_abstype Strict; + +val declare_abstype = + code_declaration Morphism.thm generic_declare_abstype; (* setup *) +fun code_attribute f = Thm.declaration_attribute + (fn thm => Context.mapping (f thm) I); + +fun code_const_attribute f cs = + code_attribute (K (fold (fn c => fn thy => f (read_const thy c) thy) cs)); + val _ = Theory.setup (let - fun lift_const_attribute f cs = - lift_attribute (K (fold (fn c => fn thy => f (read_const thy c) thy) cs)); val code_attribute_parser = - Args.$$$ "equation" |-- Scan.succeed (lift_attribute (generic_add_eqn Liberal (Equation, false))) - || Args.$$$ "nbe" |-- Scan.succeed (lift_attribute (generic_add_eqn Liberal (Nbe, false))) - || Args.$$$ "abstract" |-- Scan.succeed (lift_attribute (generic_add_eqn Liberal (Abstract, false))) - || Args.$$$ "abstype" |-- Scan.succeed (lift_attribute (generic_add_abstype Liberal false)) - || Args.del |-- Scan.succeed (lift_attribute del_eqn) - || Args.$$$ "drop" -- Args.colon |-- (Scan.repeat1 Parse.term >> lift_const_attribute del_eqns) - || Args.$$$ "abort" -- Args.colon |-- (Scan.repeat1 Parse.term >> lift_const_attribute del_exception) - || Scan.succeed (lift_attribute add_maybe_abs_eqn_liberal); + Args.$$$ "equation" |-- Scan.succeed (code_attribute + (fn thm => generic_add_eqn Liberal (thm, true))) + || Args.$$$ "nbe" |-- Scan.succeed (code_attribute + (fn thm => generic_add_eqn Liberal (thm, false))) + || Args.$$$ "abstract" |-- Scan.succeed (code_attribute + (generic_declare_abstract_eqn Liberal)) + || Args.$$$ "abstype" |-- Scan.succeed (code_attribute + (generic_declare_abstype Liberal)) + || Args.del |-- Scan.succeed (code_attribute del_eqn_global) + || Args.$$$ "abort" -- Args.colon |-- (Scan.repeat1 Parse.term + >> code_const_attribute declare_empty_global) + || Args.$$$ "drop" -- Args.colon |-- (Scan.repeat1 Parse.term + >> code_const_attribute declare_unimplemented_global) + || Scan.succeed (code_attribute + add_maybe_abs_eqn_liberal); in Attrib.setup @{binding code} (Scan.lift code_attribute_parser) "declare theorems for code generation"