src/Pure/theory.ML
author wenzelm
Mon, 25 Apr 2016 17:37:36 +0200
changeset 63042 741263be960e
parent 63038 1fbad761c1ba
child 63395 734723445a8c
permissions -rw-r--r--
more rigid check of lhs;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1526
6be6ea6f8b5d New file of just the theory primitives
paulson
parents:
diff changeset
     1
(*  Title:      Pure/theory.ML
6be6ea6f8b5d New file of just the theory primitives
paulson
parents:
diff changeset
     2
    Author:     Lawrence C Paulson and Markus Wenzel
6be6ea6f8b5d New file of just the theory primitives
paulson
parents:
diff changeset
     3
28290
4cc2b6046258 simplified oracle interface;
wenzelm
parents: 28112
diff changeset
     4
Logical theory content: axioms, definitions, and begin/end wrappers.
1526
6be6ea6f8b5d New file of just the theory primitives
paulson
parents:
diff changeset
     5
*)
16291
ea4e64b2f25a renamed const_deps to defs;
wenzelm
parents: 16198
diff changeset
     6
26668
65023d4fd226 removed obsolete SIGN_THEORY -- no name aliases in structure Theory;
wenzelm
parents: 26631
diff changeset
     7
signature THEORY =
3767
e2bb53d8dd26 moved theory stuff (add_defs etc.) here from drule.ML;
wenzelm
parents: 2979
diff changeset
     8
sig
22684
a614c5f506ea tuned signature;
wenzelm
parents: 22600
diff changeset
     9
  val parents_of: theory -> theory list
a614c5f506ea tuned signature;
wenzelm
parents: 22600
diff changeset
    10
  val ancestors_of: theory -> theory list
42425
2aa907d5ee4f added Theory.nodes_of convenience;
wenzelm
parents: 42394
diff changeset
    11
  val nodes_of: theory -> theory list
53171
a5e54d4d9081 added Theory.setup convenience;
wenzelm
parents: 52788
diff changeset
    12
  val setup: (theory -> theory) -> unit
59930
bdbc4b761c31 tuned signature;
wenzelm
parents: 58936
diff changeset
    13
  val local_setup: (Proof.context -> Proof.context) -> unit
48927
ef462b5558eb theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents: 48638
diff changeset
    14
  val get_markup: theory -> Markup.T
60099
73c260342704 formal Theory.check, with markup and completion;
wenzelm
parents: 59930
diff changeset
    15
  val check: Proof.context -> string * Position.T -> theory
56025
d74fed45fa8b abstract type Name_Space.table;
wenzelm
parents: 53171
diff changeset
    16
  val axiom_table: theory -> term Name_Space.table
33095
bbd52d2f8696 renamed NameSpace to Name_Space -- also to emphasize its subtle change in semantics;
wenzelm
parents: 33092
diff changeset
    17
  val axiom_space: theory -> Name_Space.T
16339
b02b6da609c3 axioms and oracles: NameSpace.table;
wenzelm
parents: 16313
diff changeset
    18
  val axioms_of: theory -> (string * term) list
b02b6da609c3 axioms and oracles: NameSpace.table;
wenzelm
parents: 16313
diff changeset
    19
  val all_axioms_of: theory -> (string * term) list
24666
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
    20
  val defs_of: theory -> Defs.T
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
    21
  val at_begin: (theory -> theory option) -> theory -> theory
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
    22
  val at_end: (theory -> theory option) -> theory -> theory
48927
ef462b5558eb theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents: 48638
diff changeset
    23
  val begin_theory: string * Position.T -> theory list -> theory
24666
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
    24
  val end_theory: theory -> theory
42375
774df7c59508 report Name_Space.declare/define, relatively to context;
wenzelm
parents: 42360
diff changeset
    25
  val add_axiom: Proof.context -> binding * term -> theory -> theory
61255
15865e0c5598 eliminated separate type Theory.dep: use typeargs uniformly for consts/types;
wenzelm
parents: 61249
diff changeset
    26
  val const_dep: theory -> string * typ -> Defs.entry
15865e0c5598 eliminated separate type Theory.dep: use typeargs uniformly for consts/types;
wenzelm
parents: 61249
diff changeset
    27
  val type_dep: string * typ list -> Defs.entry
61261
ddb2da7cb2e4 more explicit Defs.context: use proper name spaces as far as possible;
wenzelm
parents: 61256
diff changeset
    28
  val add_deps: Defs.context -> string -> Defs.entry -> Defs.entry list -> theory -> theory
61255
15865e0c5598 eliminated separate type Theory.dep: use typeargs uniformly for consts/types;
wenzelm
parents: 61249
diff changeset
    29
  val add_deps_global: string -> Defs.entry -> Defs.entry list -> theory -> theory
61261
ddb2da7cb2e4 more explicit Defs.context: use proper name spaces as far as possible;
wenzelm
parents: 61256
diff changeset
    30
  val add_def: Defs.context -> bool -> bool -> binding * term -> theory -> theory
33173
b8ca12f6681a eliminated obsolete tags for types/consts -- now handled via name space, in strongly typed fashion;
wenzelm
parents: 33168
diff changeset
    31
  val specify_const: (binding * typ) * mixfix -> theory -> term * theory
46974
7ca3608146d8 eliminated odd 'finalconsts' / Theory.add_finals;
wenzelm
parents: 45632
diff changeset
    32
  val check_overloading: Proof.context -> bool -> string * typ -> unit
16495
2e99aca906a7 added begin_theory, end_theory;
wenzelm
parents: 16443
diff changeset
    33
end
1526
6be6ea6f8b5d New file of just the theory primitives
paulson
parents:
diff changeset
    34
24666
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
    35
structure Theory: THEORY =
16443
82a116532e3e type theory, theory_ref, exception THEORY and related operations imported from Context;
wenzelm
parents: 16369
diff changeset
    36
struct
82a116532e3e type theory, theory_ref, exception THEORY and related operations imported from Context;
wenzelm
parents: 16369
diff changeset
    37
19708
a508bde37a81 added add_deps, which actually records dependencies of consts (unlike add_finals);
wenzelm
parents: 19700
diff changeset
    38
24666
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
    39
(** theory context operations **)
16443
82a116532e3e type theory, theory_ref, exception THEORY and related operations imported from Context;
wenzelm
parents: 16369
diff changeset
    40
82a116532e3e type theory, theory_ref, exception THEORY and related operations imported from Context;
wenzelm
parents: 16369
diff changeset
    41
val parents_of = Context.parents_of;
82a116532e3e type theory, theory_ref, exception THEORY and related operations imported from Context;
wenzelm
parents: 16369
diff changeset
    42
val ancestors_of = Context.ancestors_of;
42425
2aa907d5ee4f added Theory.nodes_of convenience;
wenzelm
parents: 42394
diff changeset
    43
fun nodes_of thy = thy :: ancestors_of thy;
16443
82a116532e3e type theory, theory_ref, exception THEORY and related operations imported from Context;
wenzelm
parents: 16369
diff changeset
    44
53171
a5e54d4d9081 added Theory.setup convenience;
wenzelm
parents: 52788
diff changeset
    45
fun setup f = Context.>> (Context.map_theory f);
59930
bdbc4b761c31 tuned signature;
wenzelm
parents: 58936
diff changeset
    46
fun local_setup f = Context.>> (Context.map_proof f);
53171
a5e54d4d9081 added Theory.setup convenience;
wenzelm
parents: 52788
diff changeset
    47
24666
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
    48
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
    49
25059
e6e0ee56a672 apply_wrappers: perhaps_apply/loop;
wenzelm
parents: 25017
diff changeset
    50
(** datatype thy **)
24666
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
    51
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
    52
type wrapper = (theory -> theory option) * stamp;
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
    53
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
    54
fun apply_wrappers (wrappers: wrapper list) =
25059
e6e0ee56a672 apply_wrappers: perhaps_apply/loop;
wenzelm
parents: 25017
diff changeset
    55
  perhaps (perhaps_loop (perhaps_apply (map fst wrappers)));
24666
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
    56
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
    57
datatype thy = Thy of
48927
ef462b5558eb theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents: 48638
diff changeset
    58
 {pos: Position.T,
ef462b5558eb theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents: 48638
diff changeset
    59
  id: serial,
ef462b5558eb theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents: 48638
diff changeset
    60
  axioms: term Name_Space.table,
24666
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
    61
  defs: Defs.T,
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
    62
  wrappers: wrapper list * wrapper list};
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
    63
48927
ef462b5558eb theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents: 48638
diff changeset
    64
fun make_thy (pos, id, axioms, defs, wrappers) =
ef462b5558eb theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents: 48638
diff changeset
    65
  Thy {pos = pos, id = id, axioms = axioms, defs = defs, wrappers = wrappers};
24666
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
    66
61262
7bd1eb4b056e tuned signature: eliminated pointless type Context.pretty;
wenzelm
parents: 61261
diff changeset
    67
structure Thy = Theory_Data'
24666
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
    68
(
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
    69
  type T = thy;
33159
369da293bbd4 make SML/NJ happy;
wenzelm
parents: 33096
diff changeset
    70
  val empty_axioms = Name_Space.empty_table "axiom" : term Name_Space.table;
48927
ef462b5558eb theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents: 48638
diff changeset
    71
  val empty = make_thy (Position.none, 0, empty_axioms, Defs.empty, ([], []));
24666
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
    72
48927
ef462b5558eb theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents: 48638
diff changeset
    73
  fun extend (Thy {pos = _, id = _, axioms = _, defs, wrappers}) =
ef462b5558eb theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents: 48638
diff changeset
    74
    make_thy (Position.none, 0, empty_axioms, defs, wrappers);
24666
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
    75
61262
7bd1eb4b056e tuned signature: eliminated pointless type Context.pretty;
wenzelm
parents: 61261
diff changeset
    76
  fun merge old_thys (thy1, thy2) =
24666
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
    77
    let
48927
ef462b5558eb theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents: 48638
diff changeset
    78
      val Thy {pos = _, id = _, axioms = _, defs = defs1, wrappers = (bgs1, ens1)} = thy1;
ef462b5558eb theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents: 48638
diff changeset
    79
      val Thy {pos = _, id = _, axioms = _, defs = defs2, wrappers = (bgs2, ens2)} = thy2;
24666
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
    80
33096
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
    81
      val axioms' = empty_axioms;
61262
7bd1eb4b056e tuned signature: eliminated pointless type Context.pretty;
wenzelm
parents: 61261
diff changeset
    82
      val defs' = Defs.merge (Defs.global_context (fst old_thys)) (defs1, defs2);
24666
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
    83
      val bgs' = Library.merge (eq_snd op =) (bgs1, bgs2);
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
    84
      val ens' = Library.merge (eq_snd op =) (ens1, ens2);
48927
ef462b5558eb theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents: 48638
diff changeset
    85
    in make_thy (Position.none, 0, axioms', defs', (bgs', ens')) end;
24666
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
    86
);
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
    87
42016
wenzelm
parents: 39134
diff changeset
    88
fun rep_theory thy = Thy.get thy |> (fn Thy args => args);
24666
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
    89
48927
ef462b5558eb theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents: 48638
diff changeset
    90
fun map_thy f = Thy.map (fn (Thy {pos, id, axioms, defs, wrappers}) =>
ef462b5558eb theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents: 48638
diff changeset
    91
  make_thy (f (pos, id, axioms, defs, wrappers)));
ef462b5558eb theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents: 48638
diff changeset
    92
ef462b5558eb theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents: 48638
diff changeset
    93
fun map_axioms f =
ef462b5558eb theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents: 48638
diff changeset
    94
  map_thy (fn (pos, id, axioms, defs, wrappers) => (pos, id, f axioms, defs, wrappers));
ef462b5558eb theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents: 48638
diff changeset
    95
ef462b5558eb theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents: 48638
diff changeset
    96
fun map_defs f =
ef462b5558eb theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents: 48638
diff changeset
    97
  map_thy (fn (pos, id, axioms, defs, wrappers) => (pos, id, axioms, f defs, wrappers));
ef462b5558eb theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents: 48638
diff changeset
    98
ef462b5558eb theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents: 48638
diff changeset
    99
fun map_wrappers f =
ef462b5558eb theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents: 48638
diff changeset
   100
  map_thy (fn (pos, id, axioms, defs, wrappers) => (pos, id, axioms, defs, f wrappers));
24666
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
   101
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
   102
48927
ef462b5558eb theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents: 48638
diff changeset
   103
(* entity markup *)
ef462b5558eb theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents: 48638
diff changeset
   104
ef462b5558eb theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents: 48638
diff changeset
   105
fun theory_markup def name id pos =
ef462b5558eb theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents: 48638
diff changeset
   106
  if id = 0 then Markup.empty
ef462b5558eb theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents: 48638
diff changeset
   107
  else
ef462b5558eb theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents: 48638
diff changeset
   108
    Markup.properties (Position.entity_properties_of def id pos)
50201
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 48929
diff changeset
   109
      (Markup.entity Markup.theoryN name);
48927
ef462b5558eb theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents: 48638
diff changeset
   110
48929
05d4e5f660ae entity markup for theory Pure, to enable hyperlinks etc.;
wenzelm
parents: 48927
diff changeset
   111
fun init_markup (name, pos) thy =
05d4e5f660ae entity markup for theory Pure, to enable hyperlinks etc.;
wenzelm
parents: 48927
diff changeset
   112
  let
05d4e5f660ae entity markup for theory Pure, to enable hyperlinks etc.;
wenzelm
parents: 48927
diff changeset
   113
    val id = serial ();
05d4e5f660ae entity markup for theory Pure, to enable hyperlinks etc.;
wenzelm
parents: 48927
diff changeset
   114
    val _ = Position.report pos (theory_markup true name id pos);
05d4e5f660ae entity markup for theory Pure, to enable hyperlinks etc.;
wenzelm
parents: 48927
diff changeset
   115
  in map_thy (fn (_, _, axioms, defs, wrappers) => (pos, id, axioms, defs, wrappers)) thy end;
05d4e5f660ae entity markup for theory Pure, to enable hyperlinks etc.;
wenzelm
parents: 48927
diff changeset
   116
48927
ef462b5558eb theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents: 48638
diff changeset
   117
fun get_markup thy =
ef462b5558eb theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents: 48638
diff changeset
   118
  let val {pos, id, ...} = rep_theory thy
ef462b5558eb theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents: 48638
diff changeset
   119
  in theory_markup false (Context.theory_name thy) id pos end;
24666
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
   120
60099
73c260342704 formal Theory.check, with markup and completion;
wenzelm
parents: 59930
diff changeset
   121
fun check ctxt (name, pos) =
73c260342704 formal Theory.check, with markup and completion;
wenzelm
parents: 59930
diff changeset
   122
  let
73c260342704 formal Theory.check, with markup and completion;
wenzelm
parents: 59930
diff changeset
   123
    val thy = Proof_Context.theory_of ctxt;
73c260342704 formal Theory.check, with markup and completion;
wenzelm
parents: 59930
diff changeset
   124
    val thy' =
73c260342704 formal Theory.check, with markup and completion;
wenzelm
parents: 59930
diff changeset
   125
      Context.get_theory thy name
73c260342704 formal Theory.check, with markup and completion;
wenzelm
parents: 59930
diff changeset
   126
        handle ERROR msg =>
73c260342704 formal Theory.check, with markup and completion;
wenzelm
parents: 59930
diff changeset
   127
          let
73c260342704 formal Theory.check, with markup and completion;
wenzelm
parents: 59930
diff changeset
   128
            val completion =
73c260342704 formal Theory.check, with markup and completion;
wenzelm
parents: 59930
diff changeset
   129
              Completion.make (name, pos)
73c260342704 formal Theory.check, with markup and completion;
wenzelm
parents: 59930
diff changeset
   130
                (fn completed =>
73c260342704 formal Theory.check, with markup and completion;
wenzelm
parents: 59930
diff changeset
   131
                  map Context.theory_name (ancestors_of thy)
73c260342704 formal Theory.check, with markup and completion;
wenzelm
parents: 59930
diff changeset
   132
                  |> filter completed
73c260342704 formal Theory.check, with markup and completion;
wenzelm
parents: 59930
diff changeset
   133
                  |> sort_strings
73c260342704 formal Theory.check, with markup and completion;
wenzelm
parents: 59930
diff changeset
   134
                  |> map (fn a => (a, (Markup.theoryN, a))));
73c260342704 formal Theory.check, with markup and completion;
wenzelm
parents: 59930
diff changeset
   135
            val report = Markup.markup_report (Completion.reported_text completion);
73c260342704 formal Theory.check, with markup and completion;
wenzelm
parents: 59930
diff changeset
   136
          in error (msg ^ Position.here pos ^ report) end;
73c260342704 formal Theory.check, with markup and completion;
wenzelm
parents: 59930
diff changeset
   137
    val _ = Context_Position.report ctxt pos (get_markup thy');
73c260342704 formal Theory.check, with markup and completion;
wenzelm
parents: 59930
diff changeset
   138
  in thy' end;
73c260342704 formal Theory.check, with markup and completion;
wenzelm
parents: 59930
diff changeset
   139
24666
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
   140
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
   141
(* basic operations *)
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
   142
56025
d74fed45fa8b abstract type Name_Space.table;
wenzelm
parents: 53171
diff changeset
   143
val axiom_table = #axioms o rep_theory;
d74fed45fa8b abstract type Name_Space.table;
wenzelm
parents: 53171
diff changeset
   144
val axiom_space = Name_Space.space_of_table o axiom_table;
24666
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
   145
56025
d74fed45fa8b abstract type Name_Space.table;
wenzelm
parents: 53171
diff changeset
   146
fun axioms_of thy = rev (Name_Space.fold_table cons (axiom_table thy) []);
42425
2aa907d5ee4f added Theory.nodes_of convenience;
wenzelm
parents: 42394
diff changeset
   147
fun all_axioms_of thy = maps axioms_of (nodes_of thy);
24666
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
   148
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
   149
val defs_of = #defs o rep_theory;
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
   150
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
   151
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
   152
(* begin/end theory *)
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
   153
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
   154
val begin_wrappers = rev o #1 o #wrappers o rep_theory;
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
   155
val end_wrappers = rev o #2 o #wrappers o rep_theory;
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
   156
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
   157
fun at_begin f = map_wrappers (apfst (cons (f, stamp ())));
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
   158
fun at_end f = map_wrappers (apsnd (cons (f, stamp ())));
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
   159
48927
ef462b5558eb theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents: 48638
diff changeset
   160
fun begin_theory (name, pos) imports =
48638
22d65e375c01 more standard bootstrapping of Pure.thy;
wenzelm
parents: 47005
diff changeset
   161
  if name = Context.PureN then
48929
05d4e5f660ae entity markup for theory Pure, to enable hyperlinks etc.;
wenzelm
parents: 48927
diff changeset
   162
    (case imports of
05d4e5f660ae entity markup for theory Pure, to enable hyperlinks etc.;
wenzelm
parents: 48927
diff changeset
   163
      [thy] => init_markup (name, pos) thy
05d4e5f660ae entity markup for theory Pure, to enable hyperlinks etc.;
wenzelm
parents: 48927
diff changeset
   164
    | _ => error "Bad bootstrapping of theory Pure")
48638
22d65e375c01 more standard bootstrapping of Pure.thy;
wenzelm
parents: 47005
diff changeset
   165
  else
22d65e375c01 more standard bootstrapping of Pure.thy;
wenzelm
parents: 47005
diff changeset
   166
    let
61262
7bd1eb4b056e tuned signature: eliminated pointless type Context.pretty;
wenzelm
parents: 61261
diff changeset
   167
      val thy = Context.begin_thy name imports;
48638
22d65e375c01 more standard bootstrapping of Pure.thy;
wenzelm
parents: 47005
diff changeset
   168
      val wrappers = begin_wrappers thy;
22d65e375c01 more standard bootstrapping of Pure.thy;
wenzelm
parents: 47005
diff changeset
   169
    in
22d65e375c01 more standard bootstrapping of Pure.thy;
wenzelm
parents: 47005
diff changeset
   170
      thy
48929
05d4e5f660ae entity markup for theory Pure, to enable hyperlinks etc.;
wenzelm
parents: 48927
diff changeset
   171
      |> init_markup (name, pos)
48638
22d65e375c01 more standard bootstrapping of Pure.thy;
wenzelm
parents: 47005
diff changeset
   172
      |> Sign.local_path
22d65e375c01 more standard bootstrapping of Pure.thy;
wenzelm
parents: 47005
diff changeset
   173
      |> Sign.map_naming (Name_Space.set_theory_name name)
22d65e375c01 more standard bootstrapping of Pure.thy;
wenzelm
parents: 47005
diff changeset
   174
      |> apply_wrappers wrappers
22d65e375c01 more standard bootstrapping of Pure.thy;
wenzelm
parents: 47005
diff changeset
   175
      |> tap (Syntax.force_syntax o Sign.syn_of)
22d65e375c01 more standard bootstrapping of Pure.thy;
wenzelm
parents: 47005
diff changeset
   176
    end;
24666
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
   177
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
   178
fun end_theory thy =
56057
ad6bd8030d88 more explicit Sign.change_check -- detect structural mistakes where they emerge, not at later theory merges;
wenzelm
parents: 56025
diff changeset
   179
  thy
ad6bd8030d88 more explicit Sign.change_check -- detect structural mistakes where they emerge, not at later theory merges;
wenzelm
parents: 56025
diff changeset
   180
  |> apply_wrappers (end_wrappers thy)
ad6bd8030d88 more explicit Sign.change_check -- detect structural mistakes where they emerge, not at later theory merges;
wenzelm
parents: 56025
diff changeset
   181
  |> Sign.change_check
ad6bd8030d88 more explicit Sign.change_check -- detect structural mistakes where they emerge, not at later theory merges;
wenzelm
parents: 56025
diff changeset
   182
  |> Context.finish_thy;
24666
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
   183
16443
82a116532e3e type theory, theory_ref, exception THEORY and related operations imported from Context;
wenzelm
parents: 16369
diff changeset
   184
3996
b7548325adc4 tuned names;
wenzelm
parents: 3971
diff changeset
   185
35985
0bbf0d2348f9 moved Drule.forall_intr_frees to Thm.forall_intr_frees (in more_thm.ML, which is loaded before pure_thy.ML);
wenzelm
parents: 35857
diff changeset
   186
(** primitive specifications **)
3814
b0dc68aa1b6a improved oracles: named, many per theory;
wenzelm
parents: 3806
diff changeset
   187
35985
0bbf0d2348f9 moved Drule.forall_intr_frees to Thm.forall_intr_frees (in more_thm.ML, which is loaded before pure_thy.ML);
wenzelm
parents: 35857
diff changeset
   188
(* raw axioms *)
1526
6be6ea6f8b5d New file of just the theory primitives
paulson
parents:
diff changeset
   189
42375
774df7c59508 report Name_Space.declare/define, relatively to context;
wenzelm
parents: 42360
diff changeset
   190
fun cert_axm ctxt (b, raw_tm) =
1526
6be6ea6f8b5d New file of just the theory primitives
paulson
parents:
diff changeset
   191
  let
42375
774df7c59508 report Name_Space.declare/define, relatively to context;
wenzelm
parents: 42360
diff changeset
   192
    val thy = Proof_Context.theory_of ctxt;
32789
d89327de0b3c removed redundant Sign.certify_prop, use Sign.cert_prop instead;
wenzelm
parents: 30466
diff changeset
   193
    val t = Sign.cert_prop thy raw_tm
2979
db6941221197 improved type check error messages;
wenzelm
parents: 2693
diff changeset
   194
      handle TYPE (msg, _, _) => error msg
16291
ea4e64b2f25a renamed const_deps to defs;
wenzelm
parents: 16198
diff changeset
   195
        | TERM (msg, _) => error msg;
35987
7c728daf4876 disallow sort constraints in primitive Theory.add_axiom/add_def -- handled in Thm.add_axiom/add_def;
wenzelm
parents: 35985
diff changeset
   196
    val _ = Term.no_dummy_patterns t handle TERM (msg, _) => error msg;
7c728daf4876 disallow sort constraints in primitive Theory.add_axiom/add_def -- handled in Thm.add_axiom/add_def;
wenzelm
parents: 35985
diff changeset
   197
7c728daf4876 disallow sort constraints in primitive Theory.add_axiom/add_def -- handled in Thm.add_axiom/add_def;
wenzelm
parents: 35985
diff changeset
   198
    val bad_sorts =
7c728daf4876 disallow sort constraints in primitive Theory.add_axiom/add_def -- handled in Thm.add_axiom/add_def;
wenzelm
parents: 35985
diff changeset
   199
      rev ((fold_types o fold_atyps_sorts) (fn (_, []) => I | (T, _) => insert (op =) T) t []);
7c728daf4876 disallow sort constraints in primitive Theory.add_axiom/add_def -- handled in Thm.add_axiom/add_def;
wenzelm
parents: 35985
diff changeset
   200
    val _ = null bad_sorts orelse
7c728daf4876 disallow sort constraints in primitive Theory.add_axiom/add_def -- handled in Thm.add_axiom/add_def;
wenzelm
parents: 35985
diff changeset
   201
      error ("Illegal sort constraints in primitive specification: " ^
42375
774df7c59508 report Name_Space.declare/define, relatively to context;
wenzelm
parents: 42360
diff changeset
   202
        commas (map (Syntax.string_of_typ (Config.put show_sorts true ctxt)) bad_sorts));
774df7c59508 report Name_Space.declare/define, relatively to context;
wenzelm
parents: 42360
diff changeset
   203
  in (b, Sign.no_vars ctxt t) end
42381
309ec68442c6 added Binding.print convenience, which includes quote already;
wenzelm
parents: 42375
diff changeset
   204
  handle ERROR msg => cat_error msg ("The error(s) above occurred in axiom " ^ Binding.print b);
1526
6be6ea6f8b5d New file of just the theory primitives
paulson
parents:
diff changeset
   205
42375
774df7c59508 report Name_Space.declare/define, relatively to context;
wenzelm
parents: 42360
diff changeset
   206
fun add_axiom ctxt raw_axm thy = thy |> map_axioms (fn axioms =>
1526
6be6ea6f8b5d New file of just the theory primitives
paulson
parents:
diff changeset
   207
  let
42375
774df7c59508 report Name_Space.declare/define, relatively to context;
wenzelm
parents: 42360
diff changeset
   208
    val axm = apsnd Logic.varify_global (cert_axm ctxt raw_axm);
61949
d9acd750c1f6 suppress irrelevant position reports;
wenzelm
parents: 61262
diff changeset
   209
    val context = ctxt
d9acd750c1f6 suppress irrelevant position reports;
wenzelm
parents: 61262
diff changeset
   210
      |> Sign.inherit_naming thy
d9acd750c1f6 suppress irrelevant position reports;
wenzelm
parents: 61262
diff changeset
   211
      |> Context_Position.set_visible_generic false;
d9acd750c1f6 suppress irrelevant position reports;
wenzelm
parents: 61262
diff changeset
   212
    val (_, axioms') = Name_Space.define context true axm axioms;
16443
82a116532e3e type theory, theory_ref, exception THEORY and related operations imported from Context;
wenzelm
parents: 16369
diff changeset
   213
  in axioms' end);
1526
6be6ea6f8b5d New file of just the theory primitives
paulson
parents:
diff changeset
   214
6be6ea6f8b5d New file of just the theory primitives
paulson
parents:
diff changeset
   215
19708
a508bde37a81 added add_deps, which actually records dependencies of consts (unlike add_finals);
wenzelm
parents: 19700
diff changeset
   216
(* dependencies *)
a508bde37a81 added add_deps, which actually records dependencies of consts (unlike add_finals);
wenzelm
parents: 19700
diff changeset
   217
61256
9ce5de06cd3b tuned signature;
wenzelm
parents: 61255
diff changeset
   218
fun const_dep thy (c, T) = ((Defs.Const, c), Sign.const_typargs thy (c, T));
61255
15865e0c5598 eliminated separate type Theory.dep: use typeargs uniformly for consts/types;
wenzelm
parents: 61249
diff changeset
   219
fun type_dep (c, args) = ((Defs.Type, c), args);
61246
077b88f9ec16 HOL typedef with explicit dependency checks according to Ondrey Kuncar, 07-Jul-2015, 16-Jul-2015, 30-Jul-2015;
wenzelm
parents: 61044
diff changeset
   220
61261
ddb2da7cb2e4 more explicit Defs.context: use proper name spaces as far as possible;
wenzelm
parents: 61256
diff changeset
   221
fun dependencies (context as (ctxt, _)) unchecked def description lhs rhs =
19708
a508bde37a81 added add_deps, which actually records dependencies of consts (unlike add_finals);
wenzelm
parents: 19700
diff changeset
   222
  let
42375
774df7c59508 report Name_Space.declare/define, relatively to context;
wenzelm
parents: 42360
diff changeset
   223
    val thy = Proof_Context.theory_of ctxt;
19708
a508bde37a81 added add_deps, which actually records dependencies of consts (unlike add_finals);
wenzelm
parents: 19700
diff changeset
   224
    val consts = Sign.consts_of thy;
61249
8611f408ec13 renamed Defs.node to Defs.item;
wenzelm
parents: 61248
diff changeset
   225
61255
15865e0c5598 eliminated separate type Theory.dep: use typeargs uniformly for consts/types;
wenzelm
parents: 61249
diff changeset
   226
    fun prep (item, args) =
15865e0c5598 eliminated separate type Theory.dep: use typeargs uniformly for consts/types;
wenzelm
parents: 61249
diff changeset
   227
      (case fold Term.add_tvarsT args [] of
15865e0c5598 eliminated separate type Theory.dep: use typeargs uniformly for consts/types;
wenzelm
parents: 61249
diff changeset
   228
        [] => (item, map Logic.varifyT_global args)
15865e0c5598 eliminated separate type Theory.dep: use typeargs uniformly for consts/types;
wenzelm
parents: 61249
diff changeset
   229
      | vs => raise TYPE ("Illegal schematic type variable(s)", map TVar vs, []));
61249
8611f408ec13 renamed Defs.node to Defs.item;
wenzelm
parents: 61248
diff changeset
   230
61255
15865e0c5598 eliminated separate type Theory.dep: use typeargs uniformly for consts/types;
wenzelm
parents: 61249
diff changeset
   231
    val lhs_vars = fold Term.add_tfreesT (snd lhs) [];
15865e0c5598 eliminated separate type Theory.dep: use typeargs uniformly for consts/types;
wenzelm
parents: 61249
diff changeset
   232
    val rhs_extras =
15865e0c5598 eliminated separate type Theory.dep: use typeargs uniformly for consts/types;
wenzelm
parents: 61249
diff changeset
   233
      fold (fn (_, args) => args |> (fold o Term.fold_atyps) (fn TFree v =>
15865e0c5598 eliminated separate type Theory.dep: use typeargs uniformly for consts/types;
wenzelm
parents: 61249
diff changeset
   234
        if member (op =) lhs_vars v then I else insert (op =) v)) rhs [];
19708
a508bde37a81 added add_deps, which actually records dependencies of consts (unlike add_finals);
wenzelm
parents: 19700
diff changeset
   235
    val _ =
a508bde37a81 added add_deps, which actually records dependencies of consts (unlike add_finals);
wenzelm
parents: 19700
diff changeset
   236
      if null rhs_extras then ()
a508bde37a81 added add_deps, which actually records dependencies of consts (unlike add_finals);
wenzelm
parents: 19700
diff changeset
   237
      else error ("Specification depends on extra type variables: " ^
39133
70d3915c92f0 pretty printing: prefer regular Proof.context over Pretty.pp, which is mostly for special bootstrap purposes involving theory merge, for example;
wenzelm
parents: 36610
diff changeset
   238
        commas_quote (map (Syntax.string_of_typ ctxt o TFree) rhs_extras) ^
33701
9dd1079cec3a primitive defs: clarified def (axiom name) vs. description;
wenzelm
parents: 33173
diff changeset
   239
        "\nThe error(s) above occurred in " ^ quote description);
61261
ddb2da7cb2e4 more explicit Defs.context: use proper name spaces as far as possible;
wenzelm
parents: 61256
diff changeset
   240
  in Defs.define context unchecked def description (prep lhs) (map prep rhs) end;
19708
a508bde37a81 added add_deps, which actually records dependencies of consts (unlike add_finals);
wenzelm
parents: 19700
diff changeset
   241
61256
9ce5de06cd3b tuned signature;
wenzelm
parents: 61255
diff changeset
   242
fun cert_entry thy ((Defs.Const, c), args) =
61255
15865e0c5598 eliminated separate type Theory.dep: use typeargs uniformly for consts/types;
wenzelm
parents: 61249
diff changeset
   243
      Sign.cert_term thy (Const (c, Sign.const_instance thy (c, args)))
15865e0c5598 eliminated separate type Theory.dep: use typeargs uniformly for consts/types;
wenzelm
parents: 61249
diff changeset
   244
      |> dest_Const |> const_dep thy
15865e0c5598 eliminated separate type Theory.dep: use typeargs uniformly for consts/types;
wenzelm
parents: 61249
diff changeset
   245
  | cert_entry thy ((Defs.Type, c), args) =
15865e0c5598 eliminated separate type Theory.dep: use typeargs uniformly for consts/types;
wenzelm
parents: 61249
diff changeset
   246
      Sign.certify_typ thy (Type (c, args)) |> dest_Type |> type_dep;
15865e0c5598 eliminated separate type Theory.dep: use typeargs uniformly for consts/types;
wenzelm
parents: 61249
diff changeset
   247
61261
ddb2da7cb2e4 more explicit Defs.context: use proper name spaces as far as possible;
wenzelm
parents: 61256
diff changeset
   248
fun add_deps context a raw_lhs raw_rhs thy =
19708
a508bde37a81 added add_deps, which actually records dependencies of consts (unlike add_finals);
wenzelm
parents: 19700
diff changeset
   249
  let
61255
15865e0c5598 eliminated separate type Theory.dep: use typeargs uniformly for consts/types;
wenzelm
parents: 61249
diff changeset
   250
    val (lhs as ((_, lhs_name), _)) :: rhs = map (cert_entry thy) (raw_lhs :: raw_rhs);
15865e0c5598 eliminated separate type Theory.dep: use typeargs uniformly for consts/types;
wenzelm
parents: 61249
diff changeset
   251
    val description = if a = "" then lhs_name ^ " axiom" else a;
61261
ddb2da7cb2e4 more explicit Defs.context: use proper name spaces as far as possible;
wenzelm
parents: 61256
diff changeset
   252
  in thy |> map_defs (dependencies context false NONE description lhs rhs) end;
42375
774df7c59508 report Name_Space.declare/define, relatively to context;
wenzelm
parents: 42360
diff changeset
   253
61255
15865e0c5598 eliminated separate type Theory.dep: use typeargs uniformly for consts/types;
wenzelm
parents: 61249
diff changeset
   254
fun add_deps_global a x y thy =
61262
7bd1eb4b056e tuned signature: eliminated pointless type Context.pretty;
wenzelm
parents: 61261
diff changeset
   255
  add_deps (Defs.global_context thy) a x y thy;
17706
e534e39f3531 back to simple 'defs' (cf. revision 1.79);
wenzelm
parents: 17496
diff changeset
   256
33173
b8ca12f6681a eliminated obsolete tags for types/consts -- now handled via name space, in strongly typed fashion;
wenzelm
parents: 33168
diff changeset
   257
fun specify_const decl thy =
61255
15865e0c5598 eliminated separate type Theory.dep: use typeargs uniformly for consts/types;
wenzelm
parents: 61249
diff changeset
   258
  let val (t, thy') = Sign.declare_const_global decl thy;
15865e0c5598 eliminated separate type Theory.dep: use typeargs uniformly for consts/types;
wenzelm
parents: 61249
diff changeset
   259
  in (t, add_deps_global "" (const_dep thy' (dest_Const t)) [] thy') end;
25017
e82ab4962f80 Theory.specify_const: added deps argument;
wenzelm
parents: 24981
diff changeset
   260
17706
e534e39f3531 back to simple 'defs' (cf. revision 1.79);
wenzelm
parents: 17496
diff changeset
   261
35985
0bbf0d2348f9 moved Drule.forall_intr_frees to Thm.forall_intr_frees (in more_thm.ML, which is loaded before pure_thy.ML);
wenzelm
parents: 35857
diff changeset
   262
(* overloading *)
9280
78a9bca983ac Tightened up check of types in constant defs.
nipkow
parents: 8897
diff changeset
   263
42375
774df7c59508 report Name_Space.declare/define, relatively to context;
wenzelm
parents: 42360
diff changeset
   264
fun check_overloading ctxt overloaded (c, T) =
16291
ea4e64b2f25a renamed const_deps to defs;
wenzelm
parents: 16198
diff changeset
   265
  let
42375
774df7c59508 report Name_Space.declare/define, relatively to context;
wenzelm
parents: 42360
diff changeset
   266
    val thy = Proof_Context.theory_of ctxt;
774df7c59508 report Name_Space.declare/define, relatively to context;
wenzelm
parents: 42360
diff changeset
   267
24763
da4a9986eccd Sign.the_const_constraint;
wenzelm
parents: 24708
diff changeset
   268
    val declT = Sign.the_const_constraint thy c
da4a9986eccd Sign.the_const_constraint;
wenzelm
parents: 24708
diff changeset
   269
      handle TYPE (msg, _, _) => error msg;
35845
e5980f0ad025 renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
wenzelm
parents: 34259
diff changeset
   270
    val T' = Logic.varifyT_global T;
16944
83ea7e3c6ec9 check_overloading replaces datatype overloading;
wenzelm
parents: 16883
diff changeset
   271
39134
917b4b6ba3d2 turned show_sorts/show_types into proper configuration options;
wenzelm
parents: 39133
diff changeset
   272
    fun message sorts txt =
16944
83ea7e3c6ec9 check_overloading replaces datatype overloading;
wenzelm
parents: 16883
diff changeset
   273
      [Pretty.block [Pretty.str "Specification of constant ",
39134
917b4b6ba3d2 turned show_sorts/show_types into proper configuration options;
wenzelm
parents: 39133
diff changeset
   274
        Pretty.str c, Pretty.str " ::", Pretty.brk 1,
917b4b6ba3d2 turned show_sorts/show_types into proper configuration options;
wenzelm
parents: 39133
diff changeset
   275
        Pretty.quote (Syntax.pretty_typ (Config.put show_sorts sorts ctxt) T)],
16944
83ea7e3c6ec9 check_overloading replaces datatype overloading;
wenzelm
parents: 16883
diff changeset
   276
        Pretty.str txt] |> Pretty.chunks |> Pretty.string_of;
16291
ea4e64b2f25a renamed const_deps to defs;
wenzelm
parents: 16198
diff changeset
   277
  in
16944
83ea7e3c6ec9 check_overloading replaces datatype overloading;
wenzelm
parents: 16883
diff changeset
   278
    if Sign.typ_instance thy (declT, T') then ()
83ea7e3c6ec9 check_overloading replaces datatype overloading;
wenzelm
parents: 16883
diff changeset
   279
    else if Type.raw_instance (declT, T') then
39134
917b4b6ba3d2 turned show_sorts/show_types into proper configuration options;
wenzelm
parents: 39133
diff changeset
   280
      error (message true "imposes additional sort constraints on the constant declaration")
16944
83ea7e3c6ec9 check_overloading replaces datatype overloading;
wenzelm
parents: 16883
diff changeset
   281
    else if overloaded then ()
57510
8f1dc3b2daa5 insist in explicit overloading;
wenzelm
parents: 56057
diff changeset
   282
    else
8f1dc3b2daa5 insist in explicit overloading;
wenzelm
parents: 56057
diff changeset
   283
      error (message false "is strictly less general than the declared type (overloading required)")
9280
78a9bca983ac Tightened up check of types in constant defs.
nipkow
parents: 8897
diff changeset
   284
  end;
78a9bca983ac Tightened up check of types in constant defs.
nipkow
parents: 8897
diff changeset
   285
3767
e2bb53d8dd26 moved theory stuff (add_defs etc.) here from drule.ML;
wenzelm
parents: 2979
diff changeset
   286
35985
0bbf0d2348f9 moved Drule.forall_intr_frees to Thm.forall_intr_frees (in more_thm.ML, which is loaded before pure_thy.ML);
wenzelm
parents: 35857
diff changeset
   287
(* definitional axioms *)
0bbf0d2348f9 moved Drule.forall_intr_frees to Thm.forall_intr_frees (in more_thm.ML, which is loaded before pure_thy.ML);
wenzelm
parents: 35857
diff changeset
   288
0bbf0d2348f9 moved Drule.forall_intr_frees to Thm.forall_intr_frees (in more_thm.ML, which is loaded before pure_thy.ML);
wenzelm
parents: 35857
diff changeset
   289
local
16291
ea4e64b2f25a renamed const_deps to defs;
wenzelm
parents: 16198
diff changeset
   290
61261
ddb2da7cb2e4 more explicit Defs.context: use proper name spaces as far as possible;
wenzelm
parents: 61256
diff changeset
   291
fun check_def (context as (ctxt, _)) thy unchecked overloaded (b, tm) defs =
16291
ea4e64b2f25a renamed const_deps to defs;
wenzelm
parents: 16198
diff changeset
   292
  let
29581
b3b33e0298eb binding is alias for Binding.T
haftmann
parents: 29092
diff changeset
   293
    val name = Sign.full_name thy b;
63042
741263be960e more rigid check of lhs;
wenzelm
parents: 63038
diff changeset
   294
    val ((lhs, rhs), _) =
741263be960e more rigid check of lhs;
wenzelm
parents: 63038
diff changeset
   295
      Primitive_Defs.dest_def ctxt
741263be960e more rigid check of lhs;
wenzelm
parents: 63038
diff changeset
   296
        {check_head = Term.is_Const,
741263be960e more rigid check of lhs;
wenzelm
parents: 63038
diff changeset
   297
         check_free_lhs = K true,
741263be960e more rigid check of lhs;
wenzelm
parents: 63038
diff changeset
   298
         check_free_rhs = K false,
741263be960e more rigid check of lhs;
wenzelm
parents: 63038
diff changeset
   299
         check_tfree = K false} tm
35988
76ca601c941e disallow premises in primitive Theory.add_def -- handle in Thm.add_def;
wenzelm
parents: 35987
diff changeset
   300
      handle TERM (msg, _) => error msg;
76ca601c941e disallow premises in primitive Theory.add_def -- handle in Thm.add_def;
wenzelm
parents: 35987
diff changeset
   301
    val lhs_const = Term.dest_Const (Term.head_of lhs);
61248
066792098895 tuned signature;
wenzelm
parents: 61247
diff changeset
   302
61255
15865e0c5598 eliminated separate type Theory.dep: use typeargs uniformly for consts/types;
wenzelm
parents: 61249
diff changeset
   303
    val rhs_consts =
15865e0c5598 eliminated separate type Theory.dep: use typeargs uniformly for consts/types;
wenzelm
parents: 61249
diff changeset
   304
      fold_aterms (fn Const const => insert (op =) (const_dep thy const) | _ => I) rhs [];
61248
066792098895 tuned signature;
wenzelm
parents: 61247
diff changeset
   305
    val rhs_types =
61255
15865e0c5598 eliminated separate type Theory.dep: use typeargs uniformly for consts/types;
wenzelm
parents: 61249
diff changeset
   306
      (fold_types o fold_subtypes) (fn Type t => insert (op =) (type_dep t) | _ => I) rhs [];
61248
066792098895 tuned signature;
wenzelm
parents: 61247
diff changeset
   307
    val rhs_deps = rhs_consts @ rhs_types;
066792098895 tuned signature;
wenzelm
parents: 61247
diff changeset
   308
42375
774df7c59508 report Name_Space.declare/define, relatively to context;
wenzelm
parents: 42360
diff changeset
   309
    val _ = check_overloading ctxt overloaded lhs_const;
61261
ddb2da7cb2e4 more explicit Defs.context: use proper name spaces as far as possible;
wenzelm
parents: 61256
diff changeset
   310
  in defs |> dependencies context unchecked (SOME name) name (const_dep thy lhs_const) rhs_deps end
18678
dd0c569fa43d sane ERROR handling;
wenzelm
parents: 18338
diff changeset
   311
  handle ERROR msg => cat_error msg (Pretty.string_of (Pretty.block
42381
309ec68442c6 added Binding.print convenience, which includes quote already;
wenzelm
parents: 42375
diff changeset
   312
   [Pretty.str ("The error(s) above occurred in definition " ^ Binding.print b ^ ":"),
42375
774df7c59508 report Name_Space.declare/define, relatively to context;
wenzelm
parents: 42360
diff changeset
   313
    Pretty.fbrk, Pretty.quote (Syntax.pretty_term ctxt tm)]));
3767
e2bb53d8dd26 moved theory stuff (add_defs etc.) here from drule.ML;
wenzelm
parents: 2979
diff changeset
   314
16291
ea4e64b2f25a renamed const_deps to defs;
wenzelm
parents: 16198
diff changeset
   315
in
ea4e64b2f25a renamed const_deps to defs;
wenzelm
parents: 16198
diff changeset
   316
61261
ddb2da7cb2e4 more explicit Defs.context: use proper name spaces as far as possible;
wenzelm
parents: 61256
diff changeset
   317
fun add_def (context as (ctxt, _)) unchecked overloaded raw_axm thy =
42375
774df7c59508 report Name_Space.declare/define, relatively to context;
wenzelm
parents: 42360
diff changeset
   318
  let val axm = cert_axm ctxt raw_axm in
35985
0bbf0d2348f9 moved Drule.forall_intr_frees to Thm.forall_intr_frees (in more_thm.ML, which is loaded before pure_thy.ML);
wenzelm
parents: 35857
diff changeset
   319
    thy
61261
ddb2da7cb2e4 more explicit Defs.context: use proper name spaces as far as possible;
wenzelm
parents: 61256
diff changeset
   320
    |> map_defs (check_def context thy unchecked overloaded axm)
42375
774df7c59508 report Name_Space.declare/define, relatively to context;
wenzelm
parents: 42360
diff changeset
   321
    |> add_axiom ctxt axm
35985
0bbf0d2348f9 moved Drule.forall_intr_frees to Thm.forall_intr_frees (in more_thm.ML, which is loaded before pure_thy.ML);
wenzelm
parents: 35857
diff changeset
   322
  end;
16291
ea4e64b2f25a renamed const_deps to defs;
wenzelm
parents: 16198
diff changeset
   323
ea4e64b2f25a renamed const_deps to defs;
wenzelm
parents: 16198
diff changeset
   324
end;
3767
e2bb53d8dd26 moved theory stuff (add_defs etc.) here from drule.ML;
wenzelm
parents: 2979
diff changeset
   325
14223
0ee05eef881b Added support for making constants final, that is, ensuring that no
skalberg
parents: 14204
diff changeset
   326
end;