arch_split: localized defs and new consts' for following namespacing conventions with generated design spec
This commit is contained in:
parent
535625a3d8
commit
19ef4d3ec3
|
@ -8,7 +8,7 @@
|
|||
|
||||
theory Defs
|
||||
imports Main
|
||||
keywords "defs" :: thy_decl
|
||||
keywords "defs" :: thy_decl and "consts'" :: thy_decl
|
||||
begin
|
||||
|
||||
ML_file "defs.ML"
|
||||
|
|
44
lib/defs.ML
44
lib/defs.ML
|
@ -9,17 +9,12 @@ fun read ctxt (b, str) =
|
|||
Syntax.read_prop ctxt str handle ERROR msg =>
|
||||
cat_error msg ("The error(s) above occurred in definition " ^ Binding.print b);
|
||||
|
||||
fun add_defs ((unchecked, overloaded), args) thy =
|
||||
fun add_defs ctxt ((unchecked, overloaded), args) thy =
|
||||
(legacy_feature "Old 'defs' command -- use 'definition' (with 'overloading') instead";
|
||||
let
|
||||
val ctxt = Syntax.init_pretty_global thy;
|
||||
in
|
||||
thy |>
|
||||
(if unchecked then Global_Theory.add_defs_unchecked else Global_Theory.add_defs)
|
||||
overloaded
|
||||
(map (fn ((b, ax), srcs) => ((b, read ctxt (b, ax)), map (Attrib.attribute_cmd_global thy) srcs)) args)
|
||||
|> snd
|
||||
end);
|
||||
(map (fn ((b, ax), srcs) => ((b, read ctxt (b, ax)), map (Attrib.attribute_cmd ctxt) srcs)) args));
|
||||
|
||||
val opt_unchecked_overloaded =
|
||||
Scan.optional (@{keyword "("} |-- Parse.!!!
|
||||
|
@ -27,9 +22,38 @@ val opt_unchecked_overloaded =
|
|||
Scan.optional (@{keyword "overloaded"} >> K true) false ||
|
||||
@{keyword "overloaded"} >> K (false, true)) --| @{keyword ")"})) (false, false);
|
||||
|
||||
fun syntax_alias global_alias local_alias b name =
|
||||
Local_Theory.declaration {syntax = true, pervasive = true} (fn phi =>
|
||||
let val b' = Morphism.binding phi b
|
||||
in Context.mapping (global_alias b' name) (local_alias b' name) end);
|
||||
|
||||
val const_alias = syntax_alias Sign.const_alias Proof_Context.const_alias;
|
||||
|
||||
(* Proof_Context.fact_alias doesn't work here, so we need to play a few tricks to get the right fact name *)
|
||||
|
||||
val _ =
|
||||
Outer_Syntax.command @{command_keyword defs} "define constants"
|
||||
(opt_unchecked_overloaded --
|
||||
Scan.repeat1 (Parse_Spec.thm_name ":" -- Parse.prop >> (fn ((x, y), z) => ((x, z), y)))
|
||||
>> (Toplevel.theory o add_defs));
|
||||
(Parse.opt_target -- (opt_unchecked_overloaded --
|
||||
Scan.repeat1 (Parse_Spec.thm_name ":" -- Parse.prop >> (fn ((x, y), z) => ((x, z), y))))
|
||||
>> (fn (target, (b, args)) => Toplevel.local_theory NONE target (fn lthy =>
|
||||
let
|
||||
val args' = map (fn ((b, def), x) => ((Binding.suffix_name "__internal__" b, def), x)) args
|
||||
val (thms, lthy') = Local_Theory.background_theory_result (add_defs lthy (b, args')) lthy;
|
||||
val lthy'' = fold2 (fn ((b, _), _) => fn thm =>
|
||||
fn lthy =>
|
||||
let val (_, lthy') = Local_Theory.note ((b,[]), [thm]) lthy
|
||||
in lthy' end) args thms lthy';
|
||||
val lthy''' = Local_Theory.raw_theory (fold (fn thm =>
|
||||
Global_Theory.hide_fact true (Thm.derivation_name thm)) thms) lthy''
|
||||
in lthy''' end)));
|
||||
|
||||
|
||||
val _ =
|
||||
Outer_Syntax.command @{command_keyword consts'} "localized consts declaration"
|
||||
(Parse.opt_target -- Scan.repeat1 Parse.const_binding >>
|
||||
(fn (target, bs) => Toplevel.local_theory NONE target (fn lthy =>
|
||||
fold (fn (b, raw_typ, mixfix) => fn lthy =>
|
||||
let val (Const (nm, _), lthy') = Local_Theory.background_theory_result
|
||||
(Sign.declare_const lthy ((b, Syntax.read_typ lthy raw_typ), mixfix)) lthy;
|
||||
in const_alias b nm lthy' end) bs lthy)))
|
||||
end
|
Loading…
Reference in New Issue