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