src/Pure/theory.ML
author wenzelm
Tue, 05 Jan 2021 16:39:53 +0100
changeset 73300 32618ae1b65d
parent 72289 69880fdc8310
child 74382 d0527bb2e590
permissions -rw-r--r--
proper theory name, e.g. for HTML/PIDE presentation;
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
67384
e32b0eb63666 clarified exception;
wenzelm
parents: 67380
diff changeset
    14
  val install_pure: theory -> unit
67380
8bef51521f21 clarified implicit Pure.thy;
wenzelm
parents: 65508
diff changeset
    15
  val get_pure: unit -> theory
70067
0cb8753bdb50 clarified signature;
wenzelm
parents: 69295
diff changeset
    16
  val get_pure_bootstrap: unit -> theory
48927
ef462b5558eb theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents: 48638
diff changeset
    17
  val get_markup: theory -> Markup.T
68482
cb84beb84ca9 clarified signature;
wenzelm
parents: 68164
diff changeset
    18
  val check: {long: bool} -> Proof.context -> string * Position.T -> theory
56025
d74fed45fa8b abstract type Name_Space.table;
wenzelm
parents: 53171
diff changeset
    19
  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
    20
  val axiom_space: theory -> Name_Space.T
16339
b02b6da609c3 axioms and oracles: NameSpace.table;
wenzelm
parents: 16313
diff changeset
    21
  val all_axioms_of: theory -> (string * term) list
24666
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
    22
  val defs_of: theory -> Defs.T
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
    23
  val at_begin: (theory -> theory option) -> theory -> theory
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
    24
  val at_end: (theory -> theory option) -> theory -> theory
70546
34b271c4f400 support join of anonymous theory nodes, e.g. relevant for parallel theory construction;
wenzelm
parents: 70067
diff changeset
    25
  val join_theory: theory list -> theory
48927
ef462b5558eb theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents: 48638
diff changeset
    26
  val begin_theory: string * Position.T -> theory list -> theory
24666
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
    27
  val end_theory: theory -> theory
42375
774df7c59508 report Name_Space.declare/define, relatively to context;
wenzelm
parents: 42360
diff changeset
    28
  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
    29
  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
    30
  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
    31
  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
    32
  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
    33
  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
    34
  val specify_const: (binding * typ) * mixfix -> theory -> term * theory
46974
7ca3608146d8 eliminated odd 'finalconsts' / Theory.add_finals;
wenzelm
parents: 45632
diff changeset
    35
  val check_overloading: Proof.context -> bool -> string * typ -> unit
16495
2e99aca906a7 added begin_theory, end_theory;
wenzelm
parents: 16443
diff changeset
    36
end
1526
6be6ea6f8b5d New file of just the theory primitives
paulson
parents:
diff changeset
    37
24666
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
    38
structure Theory: THEORY =
16443
82a116532e3e type theory, theory_ref, exception THEORY and related operations imported from Context;
wenzelm
parents: 16369
diff changeset
    39
struct
82a116532e3e type theory, theory_ref, exception THEORY and related operations imported from Context;
wenzelm
parents: 16369
diff changeset
    40
19708
a508bde37a81 added add_deps, which actually records dependencies of consts (unlike add_finals);
wenzelm
parents: 19700
diff changeset
    41
24666
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
    42
(** theory context operations **)
16443
82a116532e3e type theory, theory_ref, exception THEORY and related operations imported from Context;
wenzelm
parents: 16369
diff changeset
    43
82a116532e3e type theory, theory_ref, exception THEORY and related operations imported from Context;
wenzelm
parents: 16369
diff changeset
    44
val parents_of = Context.parents_of;
82a116532e3e type theory, theory_ref, exception THEORY and related operations imported from Context;
wenzelm
parents: 16369
diff changeset
    45
val ancestors_of = Context.ancestors_of;
42425
2aa907d5ee4f added Theory.nodes_of convenience;
wenzelm
parents: 42394
diff changeset
    46
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
    47
53171
a5e54d4d9081 added Theory.setup convenience;
wenzelm
parents: 52788
diff changeset
    48
fun setup f = Context.>> (Context.map_theory f);
59930
bdbc4b761c31 tuned signature;
wenzelm
parents: 58936
diff changeset
    49
fun local_setup f = Context.>> (Context.map_proof f);
53171
a5e54d4d9081 added Theory.setup convenience;
wenzelm
parents: 52788
diff changeset
    50
67384
e32b0eb63666 clarified exception;
wenzelm
parents: 67380
diff changeset
    51
e32b0eb63666 clarified exception;
wenzelm
parents: 67380
diff changeset
    52
(* implicit theory Pure *)
e32b0eb63666 clarified exception;
wenzelm
parents: 67380
diff changeset
    53
67380
8bef51521f21 clarified implicit Pure.thy;
wenzelm
parents: 65508
diff changeset
    54
val pure: theory Single_Assignment.var = Single_Assignment.var "pure";
67384
e32b0eb63666 clarified exception;
wenzelm
parents: 67380
diff changeset
    55
67380
8bef51521f21 clarified implicit Pure.thy;
wenzelm
parents: 65508
diff changeset
    56
fun install_pure thy = Single_Assignment.assign pure thy;
8bef51521f21 clarified implicit Pure.thy;
wenzelm
parents: 65508
diff changeset
    57
67384
e32b0eb63666 clarified exception;
wenzelm
parents: 67380
diff changeset
    58
fun get_pure () =
e32b0eb63666 clarified exception;
wenzelm
parents: 67380
diff changeset
    59
  (case Single_Assignment.peek pure of
e32b0eb63666 clarified exception;
wenzelm
parents: 67380
diff changeset
    60
    SOME thy => thy
e32b0eb63666 clarified exception;
wenzelm
parents: 67380
diff changeset
    61
  | NONE => raise Fail "Theory Pure not present");
e32b0eb63666 clarified exception;
wenzelm
parents: 67380
diff changeset
    62
70067
0cb8753bdb50 clarified signature;
wenzelm
parents: 69295
diff changeset
    63
fun get_pure_bootstrap () =
0cb8753bdb50 clarified signature;
wenzelm
parents: 69295
diff changeset
    64
  (case Single_Assignment.peek pure of
0cb8753bdb50 clarified signature;
wenzelm
parents: 69295
diff changeset
    65
    SOME thy => thy
0cb8753bdb50 clarified signature;
wenzelm
parents: 69295
diff changeset
    66
  | NONE => Context.the_global_context ());
0cb8753bdb50 clarified signature;
wenzelm
parents: 69295
diff changeset
    67
24666
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
    68
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
    69
25059
e6e0ee56a672 apply_wrappers: perhaps_apply/loop;
wenzelm
parents: 25017
diff changeset
    70
(** datatype thy **)
24666
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
    71
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
    72
type wrapper = (theory -> theory option) * stamp;
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
    73
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
    74
fun apply_wrappers (wrappers: wrapper list) =
25059
e6e0ee56a672 apply_wrappers: perhaps_apply/loop;
wenzelm
parents: 25017
diff changeset
    75
  perhaps (perhaps_loop (perhaps_apply (map fst wrappers)));
24666
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
    76
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
    77
datatype thy = Thy of
48927
ef462b5558eb theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents: 48638
diff changeset
    78
 {pos: Position.T,
ef462b5558eb theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents: 48638
diff changeset
    79
  id: serial,
ef462b5558eb theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents: 48638
diff changeset
    80
  axioms: term Name_Space.table,
24666
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
    81
  defs: Defs.T,
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
    82
  wrappers: wrapper list * wrapper list};
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
    83
48927
ef462b5558eb theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents: 48638
diff changeset
    84
fun make_thy (pos, id, axioms, defs, wrappers) =
ef462b5558eb theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents: 48638
diff changeset
    85
  Thy {pos = pos, id = id, axioms = axioms, defs = defs, wrappers = wrappers};
24666
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
    86
61262
7bd1eb4b056e tuned signature: eliminated pointless type Context.pretty;
wenzelm
parents: 61261
diff changeset
    87
structure Thy = Theory_Data'
24666
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
    88
(
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
    89
  type T = thy;
72289
69880fdc8310 clarified -- avoid non-standard extend/merge;
wenzelm
parents: 72283
diff changeset
    90
  val extend = I;
71113
98d9b78b7f47 clarified axiom_table: uniform space (e.g. like consts), e.g. relevant for export of HOL-ex.Join_Theory;
wenzelm
parents: 70547
diff changeset
    91
  val empty = make_thy (Position.none, 0, Name_Space.empty_table "axiom", Defs.empty, ([], []));
61262
7bd1eb4b056e tuned signature: eliminated pointless type Context.pretty;
wenzelm
parents: 61261
diff changeset
    92
  fun merge old_thys (thy1, thy2) =
24666
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
    93
    let
72289
69880fdc8310 clarified -- avoid non-standard extend/merge;
wenzelm
parents: 72283
diff changeset
    94
      val Thy {pos, id, axioms = axioms1, defs = defs1, wrappers = (bgs1, ens1)} = thy1;
71113
98d9b78b7f47 clarified axiom_table: uniform space (e.g. like consts), e.g. relevant for export of HOL-ex.Join_Theory;
wenzelm
parents: 70547
diff changeset
    95
      val Thy {pos = _, id = _, axioms = axioms2, defs = defs2, wrappers = (bgs2, ens2)} = thy2;
24666
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
    96
71113
98d9b78b7f47 clarified axiom_table: uniform space (e.g. like consts), e.g. relevant for export of HOL-ex.Join_Theory;
wenzelm
parents: 70547
diff changeset
    97
      val axioms' = Name_Space.merge_tables (axioms1, axioms2);
61262
7bd1eb4b056e tuned signature: eliminated pointless type Context.pretty;
wenzelm
parents: 61261
diff changeset
    98
      val defs' = Defs.merge (Defs.global_context (fst old_thys)) (defs1, defs2);
24666
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
    99
      val bgs' = Library.merge (eq_snd op =) (bgs1, bgs2);
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
   100
      val ens' = Library.merge (eq_snd op =) (ens1, ens2);
72289
69880fdc8310 clarified -- avoid non-standard extend/merge;
wenzelm
parents: 72283
diff changeset
   101
    in make_thy (pos, id, axioms', defs', (bgs', ens')) end;
24666
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
   102
);
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
   103
42016
wenzelm
parents: 39134
diff changeset
   104
fun rep_theory thy = Thy.get thy |> (fn Thy args => args);
24666
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
   105
48927
ef462b5558eb theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents: 48638
diff changeset
   106
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
   107
  make_thy (f (pos, id, axioms, defs, wrappers)));
ef462b5558eb theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents: 48638
diff changeset
   108
ef462b5558eb theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents: 48638
diff changeset
   109
fun map_axioms f =
ef462b5558eb theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents: 48638
diff changeset
   110
  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
   111
ef462b5558eb theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents: 48638
diff changeset
   112
fun map_defs f =
ef462b5558eb theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents: 48638
diff changeset
   113
  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
   114
ef462b5558eb theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents: 48638
diff changeset
   115
fun map_wrappers f =
ef462b5558eb theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents: 48638
diff changeset
   116
  map_thy (fn (pos, id, axioms, defs, wrappers) => (pos, id, axioms, defs, f wrappers));
24666
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
   117
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
   118
48927
ef462b5558eb theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents: 48638
diff changeset
   119
(* entity markup *)
ef462b5558eb theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents: 48638
diff changeset
   120
ef462b5558eb theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents: 48638
diff changeset
   121
fun theory_markup def name id pos =
ef462b5558eb theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents: 48638
diff changeset
   122
  if id = 0 then Markup.empty
ef462b5558eb theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents: 48638
diff changeset
   123
  else
ef462b5558eb theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents: 48638
diff changeset
   124
    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
   125
      (Markup.entity Markup.theoryN name);
48927
ef462b5558eb theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents: 48638
diff changeset
   126
48929
05d4e5f660ae entity markup for theory Pure, to enable hyperlinks etc.;
wenzelm
parents: 48927
diff changeset
   127
fun init_markup (name, pos) thy =
05d4e5f660ae entity markup for theory Pure, to enable hyperlinks etc.;
wenzelm
parents: 48927
diff changeset
   128
  let
05d4e5f660ae entity markup for theory Pure, to enable hyperlinks etc.;
wenzelm
parents: 48927
diff changeset
   129
    val id = serial ();
71889
48ff625687f5 more accurate context position reports;
wenzelm
parents: 71353
diff changeset
   130
    val _ = Context_Position.reports_global thy [(pos, theory_markup true name id pos)];
48929
05d4e5f660ae entity markup for theory Pure, to enable hyperlinks etc.;
wenzelm
parents: 48927
diff changeset
   131
  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
   132
48927
ef462b5558eb theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents: 48638
diff changeset
   133
fun get_markup thy =
ef462b5558eb theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents: 48638
diff changeset
   134
  let val {pos, id, ...} = rep_theory thy
73300
32618ae1b65d proper theory name, e.g. for HTML/PIDE presentation;
wenzelm
parents: 72289
diff changeset
   135
  in theory_markup false (Context.theory_long_name thy) id pos end;
24666
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
   136
68482
cb84beb84ca9 clarified signature;
wenzelm
parents: 68164
diff changeset
   137
fun check long ctxt (name, pos) =
60101
73c260342704 formal Theory.check, with markup and completion;
wenzelm
parents: 59930
diff changeset
   138
  let
73c260342704 formal Theory.check, with markup and completion;
wenzelm
parents: 59930
diff changeset
   139
    val thy = Proof_Context.theory_of ctxt;
73c260342704 formal Theory.check, with markup and completion;
wenzelm
parents: 59930
diff changeset
   140
    val thy' =
68482
cb84beb84ca9 clarified signature;
wenzelm
parents: 68164
diff changeset
   141
      Context.get_theory long thy name
60101
73c260342704 formal Theory.check, with markup and completion;
wenzelm
parents: 59930
diff changeset
   142
        handle ERROR msg =>
73c260342704 formal Theory.check, with markup and completion;
wenzelm
parents: 59930
diff changeset
   143
          let
69295
bf6937af7fe8 clarified signature;
wenzelm
parents: 68484
diff changeset
   144
            val completion_report =
bf6937af7fe8 clarified signature;
wenzelm
parents: 68484
diff changeset
   145
              Completion.make_report (name, pos)
60101
73c260342704 formal Theory.check, with markup and completion;
wenzelm
parents: 59930
diff changeset
   146
                (fn completed =>
68482
cb84beb84ca9 clarified signature;
wenzelm
parents: 68164
diff changeset
   147
                  map (Context.theory_name' long) (ancestors_of thy)
68484
59793df7f853 clarified document antiquotation @{theory};
wenzelm
parents: 68482
diff changeset
   148
                  |> filter (completed o Long_Name.base_name)
60101
73c260342704 formal Theory.check, with markup and completion;
wenzelm
parents: 59930
diff changeset
   149
                  |> sort_strings
73c260342704 formal Theory.check, with markup and completion;
wenzelm
parents: 59930
diff changeset
   150
                  |> map (fn a => (a, (Markup.theoryN, a))));
69295
bf6937af7fe8 clarified signature;
wenzelm
parents: 68484
diff changeset
   151
          in error (msg ^ Position.here pos ^ completion_report) end;
60101
73c260342704 formal Theory.check, with markup and completion;
wenzelm
parents: 59930
diff changeset
   152
    val _ = Context_Position.report ctxt pos (get_markup thy');
73c260342704 formal Theory.check, with markup and completion;
wenzelm
parents: 59930
diff changeset
   153
  in thy' end;
73c260342704 formal Theory.check, with markup and completion;
wenzelm
parents: 59930
diff changeset
   154
24666
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
   155
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
   156
(* basic operations *)
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
   157
56025
d74fed45fa8b abstract type Name_Space.table;
wenzelm
parents: 53171
diff changeset
   158
val axiom_table = #axioms o rep_theory;
d74fed45fa8b abstract type Name_Space.table;
wenzelm
parents: 53171
diff changeset
   159
val axiom_space = Name_Space.space_of_table o axiom_table;
24666
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
   160
71113
98d9b78b7f47 clarified axiom_table: uniform space (e.g. like consts), e.g. relevant for export of HOL-ex.Join_Theory;
wenzelm
parents: 70547
diff changeset
   161
val all_axioms_of = Name_Space.dest_table o axiom_table;
24666
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
   162
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
   163
val defs_of = #defs o rep_theory;
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
   164
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
   165
70546
34b271c4f400 support join of anonymous theory nodes, e.g. relevant for parallel theory construction;
wenzelm
parents: 70067
diff changeset
   166
(* join theory *)
34b271c4f400 support join of anonymous theory nodes, e.g. relevant for parallel theory construction;
wenzelm
parents: 70067
diff changeset
   167
70547
421727c19b23 proper theory naming after join (reset due to merge_data);
wenzelm
parents: 70546
diff changeset
   168
fun join_theory [] = raise List.Empty
421727c19b23 proper theory naming after join (reset due to merge_data);
wenzelm
parents: 70546
diff changeset
   169
  | join_theory [thy] = thy
72283
4ed33ea8d957 prefer conservative extend/merge of theory naming;
wenzelm
parents: 71889
diff changeset
   170
  | join_theory thys = foldl1 Context.join_thys thys;
70546
34b271c4f400 support join of anonymous theory nodes, e.g. relevant for parallel theory construction;
wenzelm
parents: 70067
diff changeset
   171
34b271c4f400 support join of anonymous theory nodes, e.g. relevant for parallel theory construction;
wenzelm
parents: 70067
diff changeset
   172
24666
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
   173
(* begin/end theory *)
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
   174
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
   175
val begin_wrappers = rev o #1 o #wrappers o rep_theory;
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
   176
val end_wrappers = rev o #2 o #wrappers o rep_theory;
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
   177
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
   178
fun at_begin f = map_wrappers (apfst (cons (f, stamp ())));
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
   179
fun at_end f = map_wrappers (apsnd (cons (f, stamp ())));
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
   180
48927
ef462b5558eb theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents: 48638
diff changeset
   181
fun begin_theory (name, pos) imports =
48638
22d65e375c01 more standard bootstrapping of Pure.thy;
wenzelm
parents: 47005
diff changeset
   182
  if name = Context.PureN then
48929
05d4e5f660ae entity markup for theory Pure, to enable hyperlinks etc.;
wenzelm
parents: 48927
diff changeset
   183
    (case imports of
05d4e5f660ae entity markup for theory Pure, to enable hyperlinks etc.;
wenzelm
parents: 48927
diff changeset
   184
      [thy] => init_markup (name, pos) thy
05d4e5f660ae entity markup for theory Pure, to enable hyperlinks etc.;
wenzelm
parents: 48927
diff changeset
   185
    | _ => error "Bad bootstrapping of theory Pure")
48638
22d65e375c01 more standard bootstrapping of Pure.thy;
wenzelm
parents: 47005
diff changeset
   186
  else
22d65e375c01 more standard bootstrapping of Pure.thy;
wenzelm
parents: 47005
diff changeset
   187
    let
61262
7bd1eb4b056e tuned signature: eliminated pointless type Context.pretty;
wenzelm
parents: 61261
diff changeset
   188
      val thy = Context.begin_thy name imports;
48638
22d65e375c01 more standard bootstrapping of Pure.thy;
wenzelm
parents: 47005
diff changeset
   189
      val wrappers = begin_wrappers thy;
22d65e375c01 more standard bootstrapping of Pure.thy;
wenzelm
parents: 47005
diff changeset
   190
    in
22d65e375c01 more standard bootstrapping of Pure.thy;
wenzelm
parents: 47005
diff changeset
   191
      thy
48929
05d4e5f660ae entity markup for theory Pure, to enable hyperlinks etc.;
wenzelm
parents: 48927
diff changeset
   192
      |> init_markup (name, pos)
72283
4ed33ea8d957 prefer conservative extend/merge of theory naming;
wenzelm
parents: 71889
diff changeset
   193
      |> Sign.init_naming
48638
22d65e375c01 more standard bootstrapping of Pure.thy;
wenzelm
parents: 47005
diff changeset
   194
      |> Sign.local_path
22d65e375c01 more standard bootstrapping of Pure.thy;
wenzelm
parents: 47005
diff changeset
   195
      |> apply_wrappers wrappers
22d65e375c01 more standard bootstrapping of Pure.thy;
wenzelm
parents: 47005
diff changeset
   196
      |> tap (Syntax.force_syntax o Sign.syn_of)
22d65e375c01 more standard bootstrapping of Pure.thy;
wenzelm
parents: 47005
diff changeset
   197
    end;
24666
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
   198
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
   199
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
   200
  thy
ad6bd8030d88 more explicit Sign.change_check -- detect structural mistakes where they emerge, not at later theory merges;
wenzelm
parents: 56025
diff changeset
   201
  |> 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
   202
  |> 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
   203
  |> Context.finish_thy;
24666
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
   204
16443
82a116532e3e type theory, theory_ref, exception THEORY and related operations imported from Context;
wenzelm
parents: 16369
diff changeset
   205
3996
b7548325adc4 tuned names;
wenzelm
parents: 3971
diff changeset
   206
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
   207
(** primitive specifications **)
3814
b0dc68aa1b6a improved oracles: named, many per theory;
wenzelm
parents: 3806
diff changeset
   208
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
   209
(* raw axioms *)
1526
6be6ea6f8b5d New file of just the theory primitives
paulson
parents:
diff changeset
   210
42375
774df7c59508 report Name_Space.declare/define, relatively to context;
wenzelm
parents: 42360
diff changeset
   211
fun cert_axm ctxt (b, raw_tm) =
1526
6be6ea6f8b5d New file of just the theory primitives
paulson
parents:
diff changeset
   212
  let
42375
774df7c59508 report Name_Space.declare/define, relatively to context;
wenzelm
parents: 42360
diff changeset
   213
    val thy = Proof_Context.theory_of ctxt;
32789
d89327de0b3c removed redundant Sign.certify_prop, use Sign.cert_prop instead;
wenzelm
parents: 30466
diff changeset
   214
    val t = Sign.cert_prop thy raw_tm
2979
db6941221197 improved type check error messages;
wenzelm
parents: 2693
diff changeset
   215
      handle TYPE (msg, _, _) => error msg
16291
ea4e64b2f25a renamed const_deps to defs;
wenzelm
parents: 16198
diff changeset
   216
        | 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
   217
    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
   218
7c728daf4876 disallow sort constraints in primitive Theory.add_axiom/add_def -- handled in Thm.add_axiom/add_def;
wenzelm
parents: 35985
diff changeset
   219
    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
   220
      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
   221
    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
   222
      error ("Illegal sort constraints in primitive specification: " ^
42375
774df7c59508 report Name_Space.declare/define, relatively to context;
wenzelm
parents: 42360
diff changeset
   223
        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
   224
  in (b, Sign.no_vars ctxt t) end
42381
309ec68442c6 added Binding.print convenience, which includes quote already;
wenzelm
parents: 42375
diff changeset
   225
  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
   226
42375
774df7c59508 report Name_Space.declare/define, relatively to context;
wenzelm
parents: 42360
diff changeset
   227
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
   228
  let
42375
774df7c59508 report Name_Space.declare/define, relatively to context;
wenzelm
parents: 42360
diff changeset
   229
    val axm = apsnd Logic.varify_global (cert_axm ctxt raw_axm);
61949
d9acd750c1f6 suppress irrelevant position reports;
wenzelm
parents: 61262
diff changeset
   230
    val context = ctxt
d9acd750c1f6 suppress irrelevant position reports;
wenzelm
parents: 61262
diff changeset
   231
      |> Sign.inherit_naming thy
d9acd750c1f6 suppress irrelevant position reports;
wenzelm
parents: 61262
diff changeset
   232
      |> Context_Position.set_visible_generic false;
d9acd750c1f6 suppress irrelevant position reports;
wenzelm
parents: 61262
diff changeset
   233
    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
   234
  in axioms' end);
1526
6be6ea6f8b5d New file of just the theory primitives
paulson
parents:
diff changeset
   235
6be6ea6f8b5d New file of just the theory primitives
paulson
parents:
diff changeset
   236
19708
a508bde37a81 added add_deps, which actually records dependencies of consts (unlike add_finals);
wenzelm
parents: 19700
diff changeset
   237
(* dependencies *)
a508bde37a81 added add_deps, which actually records dependencies of consts (unlike add_finals);
wenzelm
parents: 19700
diff changeset
   238
61256
9ce5de06cd3b tuned signature;
wenzelm
parents: 61255
diff changeset
   239
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
   240
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
   241
61261
ddb2da7cb2e4 more explicit Defs.context: use proper name spaces as far as possible;
wenzelm
parents: 61256
diff changeset
   242
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
   243
  let
61255
15865e0c5598 eliminated separate type Theory.dep: use typeargs uniformly for consts/types;
wenzelm
parents: 61249
diff changeset
   244
    fun prep (item, args) =
15865e0c5598 eliminated separate type Theory.dep: use typeargs uniformly for consts/types;
wenzelm
parents: 61249
diff changeset
   245
      (case fold Term.add_tvarsT args [] of
15865e0c5598 eliminated separate type Theory.dep: use typeargs uniformly for consts/types;
wenzelm
parents: 61249
diff changeset
   246
        [] => (item, map Logic.varifyT_global args)
15865e0c5598 eliminated separate type Theory.dep: use typeargs uniformly for consts/types;
wenzelm
parents: 61249
diff changeset
   247
      | vs => raise TYPE ("Illegal schematic type variable(s)", map TVar vs, []));
61249
8611f408ec13 renamed Defs.node to Defs.item;
wenzelm
parents: 61248
diff changeset
   248
61255
15865e0c5598 eliminated separate type Theory.dep: use typeargs uniformly for consts/types;
wenzelm
parents: 61249
diff changeset
   249
    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
   250
    val rhs_extras =
15865e0c5598 eliminated separate type Theory.dep: use typeargs uniformly for consts/types;
wenzelm
parents: 61249
diff changeset
   251
      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
   252
        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
   253
    val _ =
a508bde37a81 added add_deps, which actually records dependencies of consts (unlike add_finals);
wenzelm
parents: 19700
diff changeset
   254
      if null rhs_extras then ()
a508bde37a81 added add_deps, which actually records dependencies of consts (unlike add_finals);
wenzelm
parents: 19700
diff changeset
   255
      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
   256
        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
   257
        "\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
   258
  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
   259
61256
9ce5de06cd3b tuned signature;
wenzelm
parents: 61255
diff changeset
   260
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
   261
      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
   262
      |> dest_Const |> const_dep thy
15865e0c5598 eliminated separate type Theory.dep: use typeargs uniformly for consts/types;
wenzelm
parents: 61249
diff changeset
   263
  | cert_entry thy ((Defs.Type, c), args) =
15865e0c5598 eliminated separate type Theory.dep: use typeargs uniformly for consts/types;
wenzelm
parents: 61249
diff changeset
   264
      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
   265
61261
ddb2da7cb2e4 more explicit Defs.context: use proper name spaces as far as possible;
wenzelm
parents: 61256
diff changeset
   266
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
   267
  let
61255
15865e0c5598 eliminated separate type Theory.dep: use typeargs uniformly for consts/types;
wenzelm
parents: 61249
diff changeset
   268
    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
   269
    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
   270
  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
   271
61255
15865e0c5598 eliminated separate type Theory.dep: use typeargs uniformly for consts/types;
wenzelm
parents: 61249
diff changeset
   272
fun add_deps_global a x y thy =
61262
7bd1eb4b056e tuned signature: eliminated pointless type Context.pretty;
wenzelm
parents: 61261
diff changeset
   273
  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
   274
33173
b8ca12f6681a eliminated obsolete tags for types/consts -- now handled via name space, in strongly typed fashion;
wenzelm
parents: 33168
diff changeset
   275
fun specify_const decl thy =
61255
15865e0c5598 eliminated separate type Theory.dep: use typeargs uniformly for consts/types;
wenzelm
parents: 61249
diff changeset
   276
  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
   277
  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
   278
17706
e534e39f3531 back to simple 'defs' (cf. revision 1.79);
wenzelm
parents: 17496
diff changeset
   279
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
   280
(* overloading *)
9280
78a9bca983ac Tightened up check of types in constant defs.
nipkow
parents: 8897
diff changeset
   281
42375
774df7c59508 report Name_Space.declare/define, relatively to context;
wenzelm
parents: 42360
diff changeset
   282
fun check_overloading ctxt overloaded (c, T) =
16291
ea4e64b2f25a renamed const_deps to defs;
wenzelm
parents: 16198
diff changeset
   283
  let
42375
774df7c59508 report Name_Space.declare/define, relatively to context;
wenzelm
parents: 42360
diff changeset
   284
    val thy = Proof_Context.theory_of ctxt;
774df7c59508 report Name_Space.declare/define, relatively to context;
wenzelm
parents: 42360
diff changeset
   285
24763
da4a9986eccd Sign.the_const_constraint;
wenzelm
parents: 24708
diff changeset
   286
    val declT = Sign.the_const_constraint thy c
da4a9986eccd Sign.the_const_constraint;
wenzelm
parents: 24708
diff changeset
   287
      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
   288
    val T' = Logic.varifyT_global T;
16944
83ea7e3c6ec9 check_overloading replaces datatype overloading;
wenzelm
parents: 16883
diff changeset
   289
39134
917b4b6ba3d2 turned show_sorts/show_types into proper configuration options;
wenzelm
parents: 39133
diff changeset
   290
    fun message sorts txt =
16944
83ea7e3c6ec9 check_overloading replaces datatype overloading;
wenzelm
parents: 16883
diff changeset
   291
      [Pretty.block [Pretty.str "Specification of constant ",
39134
917b4b6ba3d2 turned show_sorts/show_types into proper configuration options;
wenzelm
parents: 39133
diff changeset
   292
        Pretty.str c, Pretty.str " ::", Pretty.brk 1,
917b4b6ba3d2 turned show_sorts/show_types into proper configuration options;
wenzelm
parents: 39133
diff changeset
   293
        Pretty.quote (Syntax.pretty_typ (Config.put show_sorts sorts ctxt) T)],
16944
83ea7e3c6ec9 check_overloading replaces datatype overloading;
wenzelm
parents: 16883
diff changeset
   294
        Pretty.str txt] |> Pretty.chunks |> Pretty.string_of;
16291
ea4e64b2f25a renamed const_deps to defs;
wenzelm
parents: 16198
diff changeset
   295
  in
16944
83ea7e3c6ec9 check_overloading replaces datatype overloading;
wenzelm
parents: 16883
diff changeset
   296
    if Sign.typ_instance thy (declT, T') then ()
83ea7e3c6ec9 check_overloading replaces datatype overloading;
wenzelm
parents: 16883
diff changeset
   297
    else if Type.raw_instance (declT, T') then
39134
917b4b6ba3d2 turned show_sorts/show_types into proper configuration options;
wenzelm
parents: 39133
diff changeset
   298
      error (message true "imposes additional sort constraints on the constant declaration")
16944
83ea7e3c6ec9 check_overloading replaces datatype overloading;
wenzelm
parents: 16883
diff changeset
   299
    else if overloaded then ()
57510
8f1dc3b2daa5 insist in explicit overloading;
wenzelm
parents: 56057
diff changeset
   300
    else
8f1dc3b2daa5 insist in explicit overloading;
wenzelm
parents: 56057
diff changeset
   301
      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
   302
  end;
78a9bca983ac Tightened up check of types in constant defs.
nipkow
parents: 8897
diff changeset
   303
3767
e2bb53d8dd26 moved theory stuff (add_defs etc.) here from drule.ML;
wenzelm
parents: 2979
diff changeset
   304
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
   305
(* 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
   306
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
   307
local
16291
ea4e64b2f25a renamed const_deps to defs;
wenzelm
parents: 16198
diff changeset
   308
61261
ddb2da7cb2e4 more explicit Defs.context: use proper name spaces as far as possible;
wenzelm
parents: 61256
diff changeset
   309
fun check_def (context as (ctxt, _)) thy unchecked overloaded (b, tm) defs =
16291
ea4e64b2f25a renamed const_deps to defs;
wenzelm
parents: 16198
diff changeset
   310
  let
29581
b3b33e0298eb binding is alias for Binding.T
haftmann
parents: 29092
diff changeset
   311
    val name = Sign.full_name thy b;
63395
734723445a8c PIDE reports of implicit variable scope;
wenzelm
parents: 63046
diff changeset
   312
    val ((lhs, rhs), _, _) =
63046
741263be960e more rigid check of lhs;
wenzelm
parents: 63042
diff changeset
   313
      Primitive_Defs.dest_def ctxt
741263be960e more rigid check of lhs;
wenzelm
parents: 63042
diff changeset
   314
        {check_head = Term.is_Const,
741263be960e more rigid check of lhs;
wenzelm
parents: 63042
diff changeset
   315
         check_free_lhs = K true,
741263be960e more rigid check of lhs;
wenzelm
parents: 63042
diff changeset
   316
         check_free_rhs = K false,
741263be960e more rigid check of lhs;
wenzelm
parents: 63042
diff changeset
   317
         check_tfree = K false} tm
35988
76ca601c941e disallow premises in primitive Theory.add_def -- handle in Thm.add_def;
wenzelm
parents: 35987
diff changeset
   318
      handle TERM (msg, _) => error msg;
76ca601c941e disallow premises in primitive Theory.add_def -- handle in Thm.add_def;
wenzelm
parents: 35987
diff changeset
   319
    val lhs_const = Term.dest_Const (Term.head_of lhs);
61248
066792098895 tuned signature;
wenzelm
parents: 61247
diff changeset
   320
61255
15865e0c5598 eliminated separate type Theory.dep: use typeargs uniformly for consts/types;
wenzelm
parents: 61249
diff changeset
   321
    val rhs_consts =
15865e0c5598 eliminated separate type Theory.dep: use typeargs uniformly for consts/types;
wenzelm
parents: 61249
diff changeset
   322
      fold_aterms (fn Const const => insert (op =) (const_dep thy const) | _ => I) rhs [];
61248
066792098895 tuned signature;
wenzelm
parents: 61247
diff changeset
   323
    val rhs_types =
61255
15865e0c5598 eliminated separate type Theory.dep: use typeargs uniformly for consts/types;
wenzelm
parents: 61249
diff changeset
   324
      (fold_types o fold_subtypes) (fn Type t => insert (op =) (type_dep t) | _ => I) rhs [];
61248
066792098895 tuned signature;
wenzelm
parents: 61247
diff changeset
   325
    val rhs_deps = rhs_consts @ rhs_types;
066792098895 tuned signature;
wenzelm
parents: 61247
diff changeset
   326
42375
774df7c59508 report Name_Space.declare/define, relatively to context;
wenzelm
parents: 42360
diff changeset
   327
    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
   328
  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
   329
  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
   330
   [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
   331
    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
   332
16291
ea4e64b2f25a renamed const_deps to defs;
wenzelm
parents: 16198
diff changeset
   333
in
ea4e64b2f25a renamed const_deps to defs;
wenzelm
parents: 16198
diff changeset
   334
61261
ddb2da7cb2e4 more explicit Defs.context: use proper name spaces as far as possible;
wenzelm
parents: 61256
diff changeset
   335
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
   336
  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
   337
    thy
61261
ddb2da7cb2e4 more explicit Defs.context: use proper name spaces as far as possible;
wenzelm
parents: 61256
diff changeset
   338
    |> map_defs (check_def context thy unchecked overloaded axm)
42375
774df7c59508 report Name_Space.declare/define, relatively to context;
wenzelm
parents: 42360
diff changeset
   339
    |> 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
   340
  end;
16291
ea4e64b2f25a renamed const_deps to defs;
wenzelm
parents: 16198
diff changeset
   341
ea4e64b2f25a renamed const_deps to defs;
wenzelm
parents: 16198
diff changeset
   342
end;
3767
e2bb53d8dd26 moved theory stuff (add_defs etc.) here from drule.ML;
wenzelm
parents: 2979
diff changeset
   343
14223
0ee05eef881b Added support for making constants final, that is, ensuring that no
skalberg
parents: 14204
diff changeset
   344
end;