1(* 2 * Copyright 2014, NICTA 3 * 4 * This software may be distributed and modified according to the terms of 5 * the BSD 2-Clause license. Note that NO WARRANTY is provided. 6 * See "LICENSE_BSD2.txt" for details. 7 * 8 * @TAG(NICTA_BSD) 9 *) 10 11signature OLD_DEFS= 12sig 13end 14 15structure Old_Defs : OLD_DEFS = 16struct 17 18fun read ctxt (b, str) = 19 Syntax.read_prop ctxt str handle ERROR msg => 20 cat_error msg ("The error(s) above occurred in definition " ^ Binding.print b); 21 22fun add_defs ctxt ((unchecked, overloaded), args) thy = 23 (legacy_feature "Old 'defs' command -- use 'definition' (with 'overloading') instead"; 24 thy |> 25 (if unchecked then Global_Theory.add_defs_unchecked else Global_Theory.add_defs) 26 overloaded 27 (map (fn ((b, ax), srcs) => ((b, read ctxt (b, ax)), map (Attrib.attribute_cmd ctxt) srcs)) args)); 28 29val opt_unchecked_overloaded = 30 Scan.optional (@{keyword "("} |-- Parse.!!! 31 (((@{keyword "unchecked"} >> K true) -- 32 Scan.optional (@{keyword "overloaded"} >> K true) false || 33 @{keyword "overloaded"} >> K (false, true)) --| @{keyword ")"})) (false, false); 34 35fun syntax_alias global_alias local_alias b name = 36 Local_Theory.declaration {syntax = true, pervasive = true} (fn phi => 37 let val b' = Morphism.binding phi b 38 in Context.mapping (global_alias b' name) (local_alias b' name) end); 39 40val const_alias = syntax_alias Sign.const_alias Proof_Context.const_alias; 41 42(* Proof_Context.fact_alias doesn't work here, so we need to play a few tricks to get the right fact name *) 43 44val _ = 45 Outer_Syntax.command @{command_keyword defs} "define constants" 46 (Parse.opt_target -- (opt_unchecked_overloaded -- 47 Scan.repeat1 (Parse_Spec.thm_name ":" -- Parse.prop >> (fn ((x, y), z) => ((x, z), y)))) 48 >> (fn (target, (b, args)) => Toplevel.local_theory NONE target (fn lthy => 49 let 50 val args' = map (fn ((b, def), x) => ((Binding.suffix_name "__internal__" b, def), x)) args 51 val (thms, lthy') = Local_Theory.background_theory_result (add_defs lthy (b, args')) lthy; 52 val lthy'' = fold2 (fn ((b, _), _) => fn thm => 53 fn lthy => 54 let val (_, lthy') = Local_Theory.note ((b,[]), [thm]) lthy 55 in lthy' end) args thms lthy'; 56 val lthy''' = Local_Theory.raw_theory (fold (fn thm => 57 Global_Theory.hide_fact true (Thm.derivation_name thm)) thms) lthy'' 58 in lthy''' end))); 59 60 61val _ = 62 Outer_Syntax.command @{command_keyword consts'} "localized consts declaration" 63 (Parse.opt_target -- Scan.repeat1 Parse.const_binding >> 64 (fn (target, bs) => Toplevel.local_theory NONE target (fn lthy => 65 fold (fn (b, raw_typ, mixfix) => fn lthy => 66 let val (Const (nm, _), lthy') = Local_Theory.background_theory_result 67 (Sign.declare_const lthy ((b, Syntax.read_typ lthy raw_typ), mixfix)) lthy; 68 in const_alias b nm lthy' end) bs lthy))) 69end 70