src/Pure/theory.ML
author haftmann
Wed, 21 Jan 2009 16:47:32 +0100
changeset 29581 b3b33e0298eb
parent 29092 466a83cb6f5f
child 29606 fedb8be05f24
permissions -rw-r--r--
binding is alias for Binding.T
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
    ID:         $Id$
6be6ea6f8b5d New file of just the theory primitives
paulson
parents:
diff changeset
     3
    Author:     Lawrence C Paulson and Markus Wenzel
6be6ea6f8b5d New file of just the theory primitives
paulson
parents:
diff changeset
     4
28290
4cc2b6046258 simplified oracle interface;
wenzelm
parents: 28112
diff changeset
     5
Logical theory content: axioms, definitions, and begin/end wrappers.
1526
6be6ea6f8b5d New file of just the theory primitives
paulson
parents:
diff changeset
     6
*)
16291
ea4e64b2f25a renamed const_deps to defs;
wenzelm
parents: 16198
diff changeset
     7
26668
65023d4fd226 removed obsolete SIGN_THEORY -- no name aliases in structure Theory;
wenzelm
parents: 26631
diff changeset
     8
signature THEORY =
3767
e2bb53d8dd26 moved theory stuff (add_defs etc.) here from drule.ML;
wenzelm
parents: 2979
diff changeset
     9
sig
16443
82a116532e3e type theory, theory_ref, exception THEORY and related operations imported from Context;
wenzelm
parents: 16369
diff changeset
    10
  val eq_thy: theory * theory -> bool
3996
b7548325adc4 tuned names;
wenzelm
parents: 3971
diff changeset
    11
  val subthy: theory * theory -> bool
24666
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
    12
  val assert_super: theory -> theory -> theory
22684
a614c5f506ea tuned signature;
wenzelm
parents: 22600
diff changeset
    13
  val parents_of: theory -> theory list
a614c5f506ea tuned signature;
wenzelm
parents: 22600
diff changeset
    14
  val ancestors_of: theory -> theory list
24666
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
    15
  val check_thy: theory -> theory_ref
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
    16
  val deref: theory_ref -> theory
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
    17
  val merge: theory * theory -> theory
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
    18
  val merge_refs: theory_ref * theory_ref -> theory_ref
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
    19
  val merge_list: theory list -> theory
16495
2e99aca906a7 added begin_theory, end_theory;
wenzelm
parents: 16443
diff changeset
    20
  val checkpoint: theory -> theory
2e99aca906a7 added begin_theory, end_theory;
wenzelm
parents: 16443
diff changeset
    21
  val copy: theory -> theory
24666
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
    22
  val requires: theory -> string -> string -> unit
16443
82a116532e3e type theory, theory_ref, exception THEORY and related operations imported from Context;
wenzelm
parents: 16369
diff changeset
    23
  val axiom_space: theory -> NameSpace.T
22684
a614c5f506ea tuned signature;
wenzelm
parents: 22600
diff changeset
    24
  val axiom_table: theory -> term Symtab.table
16339
b02b6da609c3 axioms and oracles: NameSpace.table;
wenzelm
parents: 16313
diff changeset
    25
  val axioms_of: theory -> (string * term) list
b02b6da609c3 axioms and oracles: NameSpace.table;
wenzelm
parents: 16313
diff changeset
    26
  val all_axioms_of: theory -> (string * term) list
24666
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
    27
  val defs_of: theory -> Defs.T
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
    28
  val at_begin: (theory -> theory option) -> theory -> theory
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
    29
  val at_end: (theory -> theory option) -> theory -> theory
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
    30
  val begin_theory: string -> theory list -> theory
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
    31
  val end_theory: theory -> theory
29581
b3b33e0298eb binding is alias for Binding.T
haftmann
parents: 29092
diff changeset
    32
  val add_axioms_i: (binding * term) list -> theory -> theory
3996
b7548325adc4 tuned names;
wenzelm
parents: 3971
diff changeset
    33
  val add_axioms: (bstring * string) list -> theory -> theory
19708
a508bde37a81 added add_deps, which actually records dependencies of consts (unlike add_finals);
wenzelm
parents: 19700
diff changeset
    34
  val add_deps: string -> string * typ -> (string * typ) list -> theory -> theory
29581
b3b33e0298eb binding is alias for Binding.T
haftmann
parents: 29092
diff changeset
    35
  val add_defs_i: bool -> bool -> (binding * term) list -> theory -> theory
19630
d370c3f5d3b2 Theory.add_defs(_i): added unchecked flag;
wenzelm
parents: 19614
diff changeset
    36
  val add_defs: bool -> bool -> (bstring * string) list -> theory -> theory
29581
b3b33e0298eb binding is alias for Binding.T
haftmann
parents: 29092
diff changeset
    37
  val add_finals_i: bool -> term list -> theory -> theory
16443
82a116532e3e type theory, theory_ref, exception THEORY and related operations imported from Context;
wenzelm
parents: 16369
diff changeset
    38
  val add_finals: bool -> string list -> theory -> theory
29581
b3b33e0298eb binding is alias for Binding.T
haftmann
parents: 29092
diff changeset
    39
  val specify_const: Properties.T -> (binding * typ) * mixfix -> theory -> term * theory
16495
2e99aca906a7 added begin_theory, end_theory;
wenzelm
parents: 16443
diff changeset
    40
end
1526
6be6ea6f8b5d New file of just the theory primitives
paulson
parents:
diff changeset
    41
24666
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
    42
structure Theory: THEORY =
16443
82a116532e3e type theory, theory_ref, exception THEORY and related operations imported from Context;
wenzelm
parents: 16369
diff changeset
    43
struct
82a116532e3e type theory, theory_ref, exception THEORY and related operations imported from Context;
wenzelm
parents: 16369
diff changeset
    44
19708
a508bde37a81 added add_deps, which actually records dependencies of consts (unlike add_finals);
wenzelm
parents: 19700
diff changeset
    45
24666
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
    46
(** theory context operations **)
16443
82a116532e3e type theory, theory_ref, exception THEORY and related operations imported from Context;
wenzelm
parents: 16369
diff changeset
    47
82a116532e3e type theory, theory_ref, exception THEORY and related operations imported from Context;
wenzelm
parents: 16369
diff changeset
    48
val eq_thy = Context.eq_thy;
82a116532e3e type theory, theory_ref, exception THEORY and related operations imported from Context;
wenzelm
parents: 16369
diff changeset
    49
val subthy = Context.subthy;
1526
6be6ea6f8b5d New file of just the theory primitives
paulson
parents:
diff changeset
    50
24626
85eceef2edc7 introduced generic concepts for theory interpretators
haftmann
parents: 24199
diff changeset
    51
fun assert_super thy1 thy2 =
85eceef2edc7 introduced generic concepts for theory interpretators
haftmann
parents: 24199
diff changeset
    52
  if subthy (thy1, thy2) then thy2
85eceef2edc7 introduced generic concepts for theory interpretators
haftmann
parents: 24199
diff changeset
    53
  else raise THEORY ("Not a super theory", [thy1, thy2]);
85eceef2edc7 introduced generic concepts for theory interpretators
haftmann
parents: 24199
diff changeset
    54
16443
82a116532e3e type theory, theory_ref, exception THEORY and related operations imported from Context;
wenzelm
parents: 16369
diff changeset
    55
val parents_of = Context.parents_of;
82a116532e3e type theory, theory_ref, exception THEORY and related operations imported from Context;
wenzelm
parents: 16369
diff changeset
    56
val ancestors_of = Context.ancestors_of;
82a116532e3e type theory, theory_ref, exception THEORY and related operations imported from Context;
wenzelm
parents: 16369
diff changeset
    57
24137
8d7896398147 replaced Theory.self_ref by Theory.check_thy, which now produces a checked ref;
wenzelm
parents: 23655
diff changeset
    58
val check_thy = Context.check_thy;
16443
82a116532e3e type theory, theory_ref, exception THEORY and related operations imported from Context;
wenzelm
parents: 16369
diff changeset
    59
val deref = Context.deref;
24666
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
    60
16443
82a116532e3e type theory, theory_ref, exception THEORY and related operations imported from Context;
wenzelm
parents: 16369
diff changeset
    61
val merge = Context.merge;
82a116532e3e type theory, theory_ref, exception THEORY and related operations imported from Context;
wenzelm
parents: 16369
diff changeset
    62
val merge_refs = Context.merge_refs;
82a116532e3e type theory, theory_ref, exception THEORY and related operations imported from Context;
wenzelm
parents: 16369
diff changeset
    63
23600
5a5332e1351b removed comments -- no exception TERM;
wenzelm
parents: 23086
diff changeset
    64
fun merge_list [] = raise THEORY ("Empty merge of theories", [])
21608
2ca27eeb2841 added merge_list;
wenzelm
parents: 20549
diff changeset
    65
  | merge_list (thy :: thys) = Library.foldl merge (thy, thys);
2ca27eeb2841 added merge_list;
wenzelm
parents: 20549
diff changeset
    66
16495
2e99aca906a7 added begin_theory, end_theory;
wenzelm
parents: 16443
diff changeset
    67
val checkpoint = Context.checkpoint_thy;
2e99aca906a7 added begin_theory, end_theory;
wenzelm
parents: 16443
diff changeset
    68
val copy = Context.copy_thy;
2e99aca906a7 added begin_theory, end_theory;
wenzelm
parents: 16443
diff changeset
    69
24666
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
    70
fun requires thy name what =
29092
466a83cb6f5f requires: check ancestors directly;
wenzelm
parents: 29004
diff changeset
    71
  if exists (fn thy' => Context.theory_name thy' = name) (thy :: ancestors_of thy) then ()
24666
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
    72
  else error ("Require theory " ^ quote name ^ " as an ancestor for " ^ what);
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
    73
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
    74
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
    75
25059
e6e0ee56a672 apply_wrappers: perhaps_apply/loop;
wenzelm
parents: 25017
diff changeset
    76
(** datatype thy **)
24666
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
    77
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
    78
type wrapper = (theory -> theory option) * stamp;
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
    79
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
    80
fun apply_wrappers (wrappers: wrapper list) =
25059
e6e0ee56a672 apply_wrappers: perhaps_apply/loop;
wenzelm
parents: 25017
diff changeset
    81
  perhaps (perhaps_loop (perhaps_apply (map fst wrappers)));
24666
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
    82
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
    83
datatype thy = Thy of
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
    84
 {axioms: term NameSpace.table,
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
    85
  defs: Defs.T,
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
    86
  wrappers: wrapper list * wrapper list};
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
    87
28290
4cc2b6046258 simplified oracle interface;
wenzelm
parents: 28112
diff changeset
    88
fun make_thy (axioms, defs, wrappers) = Thy {axioms = axioms, defs = defs, wrappers = wrappers};
24666
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
    89
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
    90
fun err_dup_axm dup = error ("Duplicate axiom: " ^ quote dup);
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
    91
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
    92
structure ThyData = TheoryDataFun
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
    93
(
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
    94
  type T = thy;
28290
4cc2b6046258 simplified oracle interface;
wenzelm
parents: 28112
diff changeset
    95
  val empty = make_thy (NameSpace.empty_table, Defs.empty, ([], []));
24666
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
    96
  val copy = I;
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
    97
28290
4cc2b6046258 simplified oracle interface;
wenzelm
parents: 28112
diff changeset
    98
  fun extend (Thy {axioms, defs, wrappers}) = make_thy (NameSpace.empty_table, defs, wrappers);
24666
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
    99
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
   100
  fun merge pp (thy1, thy2) =
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
   101
    let
28290
4cc2b6046258 simplified oracle interface;
wenzelm
parents: 28112
diff changeset
   102
      val Thy {axioms = _, defs = defs1, wrappers = (bgs1, ens1)} = thy1;
4cc2b6046258 simplified oracle interface;
wenzelm
parents: 28112
diff changeset
   103
      val Thy {axioms = _, defs = defs2, wrappers = (bgs2, ens2)} = thy2;
24666
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
   104
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
   105
      val axioms' = NameSpace.empty_table;
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
   106
      val defs' = Defs.merge pp (defs1, defs2);
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
   107
      val bgs' = Library.merge (eq_snd op =) (bgs1, bgs2);
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
   108
      val ens' = Library.merge (eq_snd op =) (ens1, ens2);
28290
4cc2b6046258 simplified oracle interface;
wenzelm
parents: 28112
diff changeset
   109
    in make_thy (axioms', defs', (bgs', ens')) end;
24666
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
   110
);
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
   111
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
   112
fun rep_theory thy = ThyData.get thy |> (fn Thy args => args);
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
   113
28290
4cc2b6046258 simplified oracle interface;
wenzelm
parents: 28112
diff changeset
   114
fun map_thy f = ThyData.map (fn (Thy {axioms, defs, wrappers}) =>
4cc2b6046258 simplified oracle interface;
wenzelm
parents: 28112
diff changeset
   115
  make_thy (f (axioms, defs, wrappers)));
24666
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
   116
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
   117
28290
4cc2b6046258 simplified oracle interface;
wenzelm
parents: 28112
diff changeset
   118
fun map_axioms f = map_thy (fn (axioms, defs, wrappers) => (f axioms, defs, wrappers));
4cc2b6046258 simplified oracle interface;
wenzelm
parents: 28112
diff changeset
   119
fun map_defs f = map_thy (fn (axioms, defs, wrappers) => (axioms, f defs, wrappers));
4cc2b6046258 simplified oracle interface;
wenzelm
parents: 28112
diff changeset
   120
fun map_wrappers f = map_thy (fn (axioms, defs, wrappers) => (axioms, defs, f wrappers));
24666
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
   121
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
   122
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
   123
(* basic operations *)
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
   124
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
   125
val axiom_space = #1 o #axioms o rep_theory;
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
   126
val axiom_table = #2 o #axioms o rep_theory;
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
   127
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
   128
val axioms_of = Symtab.dest o #2 o #axioms o rep_theory;
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
   129
fun all_axioms_of thy = maps axioms_of (thy :: ancestors_of thy);
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
   130
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
   131
val defs_of = #defs o rep_theory;
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
   132
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
   133
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
   134
(* begin/end theory *)
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
   135
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
   136
val begin_wrappers = rev o #1 o #wrappers o rep_theory;
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
   137
val end_wrappers = rev o #2 o #wrappers o rep_theory;
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
   138
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
   139
fun at_begin f = map_wrappers (apfst (cons (f, stamp ())));
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
   140
fun at_end f = map_wrappers (apsnd (cons (f, stamp ())));
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
   141
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
   142
fun begin_theory name imports =
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
   143
  let
26939
1035c89b4c02 moved global pretty/string_of functions from Sign to Syntax;
wenzelm
parents: 26668
diff changeset
   144
    val thy = Context.begin_thy Syntax.pp_global name imports;
24666
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
   145
    val wrappers = begin_wrappers thy;
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
   146
  in thy |> Sign.local_path |> apply_wrappers wrappers end;
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
   147
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
   148
fun end_theory thy =
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
   149
  thy |> apply_wrappers (end_wrappers thy) |> Context.finish_thy;
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
   150
16443
82a116532e3e type theory, theory_ref, exception THEORY and related operations imported from Context;
wenzelm
parents: 16369
diff changeset
   151
3996
b7548325adc4 tuned names;
wenzelm
parents: 3971
diff changeset
   152
24666
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
   153
(** add axioms **)
3814
b0dc68aa1b6a improved oracles: named, many per theory;
wenzelm
parents: 3806
diff changeset
   154
1526
6be6ea6f8b5d New file of just the theory primitives
paulson
parents:
diff changeset
   155
(* prepare axioms *)
6be6ea6f8b5d New file of just the theory primitives
paulson
parents:
diff changeset
   156
18678
dd0c569fa43d sane ERROR handling;
wenzelm
parents: 18338
diff changeset
   157
fun err_in_axm msg name =
dd0c569fa43d sane ERROR handling;
wenzelm
parents: 18338
diff changeset
   158
  cat_error msg ("The error(s) above occurred in axiom " ^ quote name);
1526
6be6ea6f8b5d New file of just the theory primitives
paulson
parents:
diff changeset
   159
29581
b3b33e0298eb binding is alias for Binding.T
haftmann
parents: 29092
diff changeset
   160
fun cert_axm thy (b, raw_tm) =
1526
6be6ea6f8b5d New file of just the theory primitives
paulson
parents:
diff changeset
   161
  let
18968
52639ad19a96 adapted Sign.infer_types(_simult), Sign.certify_term/prop;
wenzelm
parents: 18943
diff changeset
   162
    val (t, T, _) = Sign.certify_prop thy raw_tm
2979
db6941221197 improved type check error messages;
wenzelm
parents: 2693
diff changeset
   163
      handle TYPE (msg, _, _) => error msg
16291
ea4e64b2f25a renamed const_deps to defs;
wenzelm
parents: 16198
diff changeset
   164
        | TERM (msg, _) => error msg;
1526
6be6ea6f8b5d New file of just the theory primitives
paulson
parents:
diff changeset
   165
  in
9537
7e0ba737f98e axioms: Term.no_dummy_patterns;
wenzelm
parents: 9332
diff changeset
   166
    Term.no_dummy_patterns t handle TERM (msg, _) => error msg;
29581
b3b33e0298eb binding is alias for Binding.T
haftmann
parents: 29092
diff changeset
   167
    (b, Sign.no_vars (Syntax.pp_global thy) t)
9629
50f1c4222aea tuned error handling;
wenzelm
parents: 9537
diff changeset
   168
  end;
1526
6be6ea6f8b5d New file of just the theory primitives
paulson
parents:
diff changeset
   169
29581
b3b33e0298eb binding is alias for Binding.T
haftmann
parents: 29092
diff changeset
   170
fun read_axm thy (bname, str) =
b3b33e0298eb binding is alias for Binding.T
haftmann
parents: 29092
diff changeset
   171
  cert_axm thy (Binding.name bname, Syntax.read_prop_global thy str)
b3b33e0298eb binding is alias for Binding.T
haftmann
parents: 29092
diff changeset
   172
    handle ERROR msg => err_in_axm msg bname;
1526
6be6ea6f8b5d New file of just the theory primitives
paulson
parents:
diff changeset
   173
6be6ea6f8b5d New file of just the theory primitives
paulson
parents:
diff changeset
   174
16443
82a116532e3e type theory, theory_ref, exception THEORY and related operations imported from Context;
wenzelm
parents: 16369
diff changeset
   175
(* add_axioms(_i) *)
1526
6be6ea6f8b5d New file of just the theory primitives
paulson
parents:
diff changeset
   176
16291
ea4e64b2f25a renamed const_deps to defs;
wenzelm
parents: 16198
diff changeset
   177
local
ea4e64b2f25a renamed const_deps to defs;
wenzelm
parents: 16198
diff changeset
   178
16443
82a116532e3e type theory, theory_ref, exception THEORY and related operations imported from Context;
wenzelm
parents: 16369
diff changeset
   179
fun gen_add_axioms prep_axm raw_axms thy = thy |> map_axioms (fn axioms =>
1526
6be6ea6f8b5d New file of just the theory primitives
paulson
parents:
diff changeset
   180
  let
29581
b3b33e0298eb binding is alias for Binding.T
haftmann
parents: 29092
diff changeset
   181
    val axms = map (apsnd Logic.varify o prep_axm thy) raw_axms;
29004
a5a91f387791 removed Table.extend, NameSpace.extend_table
haftmann
parents: 28965
diff changeset
   182
    val axioms' = fold (snd oo NameSpace.bind (Sign.naming_of thy)) axms axioms
23655
d2d1138e0ddc replaced exception TableFun/GraphFun.DUPS by TableFun/GraphFun.DUP;
wenzelm
parents: 23600
diff changeset
   183
      handle Symtab.DUP dup => err_dup_axm dup;
16443
82a116532e3e type theory, theory_ref, exception THEORY and related operations imported from Context;
wenzelm
parents: 16369
diff changeset
   184
  in axioms' end);
1526
6be6ea6f8b5d New file of just the theory primitives
paulson
parents:
diff changeset
   185
16291
ea4e64b2f25a renamed const_deps to defs;
wenzelm
parents: 16198
diff changeset
   186
in
ea4e64b2f25a renamed const_deps to defs;
wenzelm
parents: 16198
diff changeset
   187
29581
b3b33e0298eb binding is alias for Binding.T
haftmann
parents: 29092
diff changeset
   188
val add_axioms_i = gen_add_axioms cert_axm;
16291
ea4e64b2f25a renamed const_deps to defs;
wenzelm
parents: 16198
diff changeset
   189
val add_axioms = gen_add_axioms read_axm;
ea4e64b2f25a renamed const_deps to defs;
wenzelm
parents: 16198
diff changeset
   190
ea4e64b2f25a renamed const_deps to defs;
wenzelm
parents: 16198
diff changeset
   191
end;
1526
6be6ea6f8b5d New file of just the theory primitives
paulson
parents:
diff changeset
   192
6be6ea6f8b5d New file of just the theory primitives
paulson
parents:
diff changeset
   193
3767
e2bb53d8dd26 moved theory stuff (add_defs etc.) here from drule.ML;
wenzelm
parents: 2979
diff changeset
   194
e2bb53d8dd26 moved theory stuff (add_defs etc.) here from drule.ML;
wenzelm
parents: 2979
diff changeset
   195
(** add constant definitions **)
e2bb53d8dd26 moved theory stuff (add_defs etc.) here from drule.ML;
wenzelm
parents: 2979
diff changeset
   196
19708
a508bde37a81 added add_deps, which actually records dependencies of consts (unlike add_finals);
wenzelm
parents: 19700
diff changeset
   197
(* dependencies *)
a508bde37a81 added add_deps, which actually records dependencies of consts (unlike add_finals);
wenzelm
parents: 19700
diff changeset
   198
a508bde37a81 added add_deps, which actually records dependencies of consts (unlike add_finals);
wenzelm
parents: 19700
diff changeset
   199
fun dependencies thy unchecked is_def name lhs rhs =
a508bde37a81 added add_deps, which actually records dependencies of consts (unlike add_finals);
wenzelm
parents: 19700
diff changeset
   200
  let
26939
1035c89b4c02 moved global pretty/string_of functions from Sign to Syntax;
wenzelm
parents: 26668
diff changeset
   201
    val pp = Syntax.pp_global thy;
19708
a508bde37a81 added add_deps, which actually records dependencies of consts (unlike add_finals);
wenzelm
parents: 19700
diff changeset
   202
    val consts = Sign.consts_of thy;
19727
wenzelm
parents: 19708
diff changeset
   203
    fun prep const =
wenzelm
parents: 19708
diff changeset
   204
      let val Const (c, T) = Sign.no_vars pp (Const const)
26631
d6b6c74a8bcf rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents: 25059
diff changeset
   205
      in (c, Consts.typargs consts (c, Logic.varifyT T)) end;
19708
a508bde37a81 added add_deps, which actually records dependencies of consts (unlike add_finals);
wenzelm
parents: 19700
diff changeset
   206
a508bde37a81 added add_deps, which actually records dependencies of consts (unlike add_finals);
wenzelm
parents: 19700
diff changeset
   207
    val lhs_vars = Term.add_tfreesT (#2 lhs) [];
a508bde37a81 added add_deps, which actually records dependencies of consts (unlike add_finals);
wenzelm
parents: 19700
diff changeset
   208
    val rhs_extras = fold (#2 #> Term.fold_atyps (fn TFree v =>
a508bde37a81 added add_deps, which actually records dependencies of consts (unlike add_finals);
wenzelm
parents: 19700
diff changeset
   209
      if member (op =) lhs_vars v then I else insert (op =) v | _ => I)) rhs [];
a508bde37a81 added add_deps, which actually records dependencies of consts (unlike add_finals);
wenzelm
parents: 19700
diff changeset
   210
    val _ =
a508bde37a81 added add_deps, which actually records dependencies of consts (unlike add_finals);
wenzelm
parents: 19700
diff changeset
   211
      if null rhs_extras then ()
a508bde37a81 added add_deps, which actually records dependencies of consts (unlike add_finals);
wenzelm
parents: 19700
diff changeset
   212
      else error ("Specification depends on extra type variables: " ^
a508bde37a81 added add_deps, which actually records dependencies of consts (unlike add_finals);
wenzelm
parents: 19700
diff changeset
   213
        commas_quote (map (Pretty.string_of_typ pp o TFree) rhs_extras) ^
a508bde37a81 added add_deps, which actually records dependencies of consts (unlike add_finals);
wenzelm
parents: 19700
diff changeset
   214
        "\nThe error(s) above occurred in " ^ quote name);
24199
8be734b5f59f new access interface in defs.ML
haftmann
parents: 24137
diff changeset
   215
  in Defs.define pp unchecked is_def name (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
   216
a508bde37a81 added add_deps, which actually records dependencies of consts (unlike add_finals);
wenzelm
parents: 19700
diff changeset
   217
fun add_deps a raw_lhs raw_rhs thy =
a508bde37a81 added add_deps, which actually records dependencies of consts (unlike add_finals);
wenzelm
parents: 19700
diff changeset
   218
  let
a508bde37a81 added add_deps, which actually records dependencies of consts (unlike add_finals);
wenzelm
parents: 19700
diff changeset
   219
    val lhs :: rhs = map (dest_Const o Sign.cert_term thy o Const) (raw_lhs :: raw_rhs);
a508bde37a81 added add_deps, which actually records dependencies of consts (unlike add_finals);
wenzelm
parents: 19700
diff changeset
   220
    val name = if a = "" then (#1 lhs ^ " axiom") else a;
a508bde37a81 added add_deps, which actually records dependencies of consts (unlike add_finals);
wenzelm
parents: 19700
diff changeset
   221
  in thy |> map_defs (dependencies thy false false name lhs rhs) end;
17706
e534e39f3531 back to simple 'defs' (cf. revision 1.79);
wenzelm
parents: 17496
diff changeset
   222
28112
691993ef6abe simplified specify_const: canonical args, global deps;
wenzelm
parents: 28017
diff changeset
   223
fun specify_const tags decl thy =
25017
e82ab4962f80 Theory.specify_const: added deps argument;
wenzelm
parents: 24981
diff changeset
   224
  let val (t as Const const, thy') = Sign.declare_const tags decl thy
28112
691993ef6abe simplified specify_const: canonical args, global deps;
wenzelm
parents: 28017
diff changeset
   225
  in (t, add_deps "" const [] thy') end;
25017
e82ab4962f80 Theory.specify_const: added deps argument;
wenzelm
parents: 24981
diff changeset
   226
17706
e534e39f3531 back to simple 'defs' (cf. revision 1.79);
wenzelm
parents: 17496
diff changeset
   227
16944
83ea7e3c6ec9 check_overloading replaces datatype overloading;
wenzelm
parents: 16883
diff changeset
   228
(* check_overloading *)
9280
78a9bca983ac Tightened up check of types in constant defs.
nipkow
parents: 8897
diff changeset
   229
16944
83ea7e3c6ec9 check_overloading replaces datatype overloading;
wenzelm
parents: 16883
diff changeset
   230
fun check_overloading thy overloaded (c, T) =
16291
ea4e64b2f25a renamed const_deps to defs;
wenzelm
parents: 16198
diff changeset
   231
  let
24763
da4a9986eccd Sign.the_const_constraint;
wenzelm
parents: 24708
diff changeset
   232
    val declT = Sign.the_const_constraint thy c
da4a9986eccd Sign.the_const_constraint;
wenzelm
parents: 24708
diff changeset
   233
      handle TYPE (msg, _, _) => error msg;
19806
f860b7a98445 renamed Type.(un)varifyT to Logic.(un)varifyT;
wenzelm
parents: 19727
diff changeset
   234
    val T' = Logic.varifyT T;
16944
83ea7e3c6ec9 check_overloading replaces datatype overloading;
wenzelm
parents: 16883
diff changeset
   235
83ea7e3c6ec9 check_overloading replaces datatype overloading;
wenzelm
parents: 16883
diff changeset
   236
    fun message txt =
83ea7e3c6ec9 check_overloading replaces datatype overloading;
wenzelm
parents: 16883
diff changeset
   237
      [Pretty.block [Pretty.str "Specification of constant ",
26939
1035c89b4c02 moved global pretty/string_of functions from Sign to Syntax;
wenzelm
parents: 26668
diff changeset
   238
        Pretty.str c, Pretty.str " ::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ_global thy T)],
16944
83ea7e3c6ec9 check_overloading replaces datatype overloading;
wenzelm
parents: 16883
diff changeset
   239
        Pretty.str txt] |> Pretty.chunks |> Pretty.string_of;
16291
ea4e64b2f25a renamed const_deps to defs;
wenzelm
parents: 16198
diff changeset
   240
  in
16944
83ea7e3c6ec9 check_overloading replaces datatype overloading;
wenzelm
parents: 16883
diff changeset
   241
    if Sign.typ_instance thy (declT, T') then ()
83ea7e3c6ec9 check_overloading replaces datatype overloading;
wenzelm
parents: 16883
diff changeset
   242
    else if Type.raw_instance (declT, T') then
83ea7e3c6ec9 check_overloading replaces datatype overloading;
wenzelm
parents: 16883
diff changeset
   243
      error (Library.setmp show_sorts true
83ea7e3c6ec9 check_overloading replaces datatype overloading;
wenzelm
parents: 16883
diff changeset
   244
        message "imposes additional sort constraints on the constant declaration")
83ea7e3c6ec9 check_overloading replaces datatype overloading;
wenzelm
parents: 16883
diff changeset
   245
    else if overloaded then ()
83ea7e3c6ec9 check_overloading replaces datatype overloading;
wenzelm
parents: 16883
diff changeset
   246
    else warning (message "is strictly less general than the declared type");
83ea7e3c6ec9 check_overloading replaces datatype overloading;
wenzelm
parents: 16883
diff changeset
   247
    (c, T)
9280
78a9bca983ac Tightened up check of types in constant defs.
nipkow
parents: 8897
diff changeset
   248
  end;
78a9bca983ac Tightened up check of types in constant defs.
nipkow
parents: 8897
diff changeset
   249
3767
e2bb53d8dd26 moved theory stuff (add_defs etc.) here from drule.ML;
wenzelm
parents: 2979
diff changeset
   250
16291
ea4e64b2f25a renamed const_deps to defs;
wenzelm
parents: 16198
diff changeset
   251
(* check_def *)
ea4e64b2f25a renamed const_deps to defs;
wenzelm
parents: 16198
diff changeset
   252
29581
b3b33e0298eb binding is alias for Binding.T
haftmann
parents: 29092
diff changeset
   253
fun check_def thy unchecked overloaded (b, tm) defs =
16291
ea4e64b2f25a renamed const_deps to defs;
wenzelm
parents: 16198
diff changeset
   254
  let
24981
4ec3f95190bf dest/cert_def: replaced Pretty.pp by explicit Proof.context;
wenzelm
parents: 24966
diff changeset
   255
    val ctxt = ProofContext.init thy;
29581
b3b33e0298eb binding is alias for Binding.T
haftmann
parents: 29092
diff changeset
   256
    val name = Sign.full_name thy b;
24981
4ec3f95190bf dest/cert_def: replaced Pretty.pp by explicit Proof.context;
wenzelm
parents: 24966
diff changeset
   257
    val (lhs_const, rhs) = Sign.cert_def ctxt tm;
16944
83ea7e3c6ec9 check_overloading replaces datatype overloading;
wenzelm
parents: 16883
diff changeset
   258
    val rhs_consts = fold_aterms (fn Const const => insert (op =) const | _ => I) rhs [];
18943
947d3a694654 moved no_vars to sign.ML;
wenzelm
parents: 18857
diff changeset
   259
    val _ = check_overloading thy overloaded lhs_const;
19708
a508bde37a81 added add_deps, which actually records dependencies of consts (unlike add_finals);
wenzelm
parents: 19700
diff changeset
   260
  in defs |> dependencies thy unchecked true name lhs_const rhs_consts end
18678
dd0c569fa43d sane ERROR handling;
wenzelm
parents: 18338
diff changeset
   261
  handle ERROR msg => cat_error msg (Pretty.string_of (Pretty.block
29581
b3b33e0298eb binding is alias for Binding.T
haftmann
parents: 29092
diff changeset
   262
   [Pretty.str ("The error(s) above occurred in definition " ^ quote (Binding.display b) ^ ":"),
26939
1035c89b4c02 moved global pretty/string_of functions from Sign to Syntax;
wenzelm
parents: 26668
diff changeset
   263
    Pretty.fbrk, Pretty.quote (Syntax.pretty_term_global thy tm)]));
3767
e2bb53d8dd26 moved theory stuff (add_defs etc.) here from drule.ML;
wenzelm
parents: 2979
diff changeset
   264
e2bb53d8dd26 moved theory stuff (add_defs etc.) here from drule.ML;
wenzelm
parents: 2979
diff changeset
   265
16443
82a116532e3e type theory, theory_ref, exception THEORY and related operations imported from Context;
wenzelm
parents: 16369
diff changeset
   266
(* add_defs(_i) *)
3767
e2bb53d8dd26 moved theory stuff (add_defs etc.) here from drule.ML;
wenzelm
parents: 2979
diff changeset
   267
16291
ea4e64b2f25a renamed const_deps to defs;
wenzelm
parents: 16198
diff changeset
   268
local
9320
803cb9c9d4dd const_deps: unit Graph.T;
wenzelm
parents: 9282
diff changeset
   269
19630
d370c3f5d3b2 Theory.add_defs(_i): added unchecked flag;
wenzelm
parents: 19614
diff changeset
   270
fun gen_add_defs prep_axm unchecked overloaded raw_axms thy =
16443
82a116532e3e type theory, theory_ref, exception THEORY and related operations imported from Context;
wenzelm
parents: 16369
diff changeset
   271
  let val axms = map (prep_axm thy) raw_axms in
82a116532e3e type theory, theory_ref, exception THEORY and related operations imported from Context;
wenzelm
parents: 16369
diff changeset
   272
    thy
19630
d370c3f5d3b2 Theory.add_defs(_i): added unchecked flag;
wenzelm
parents: 19614
diff changeset
   273
    |> map_defs (fold (check_def thy unchecked overloaded) axms)
9320
803cb9c9d4dd const_deps: unit Graph.T;
wenzelm
parents: 9282
diff changeset
   274
    |> add_axioms_i axms
3767
e2bb53d8dd26 moved theory stuff (add_defs etc.) here from drule.ML;
wenzelm
parents: 2979
diff changeset
   275
  end;
e2bb53d8dd26 moved theory stuff (add_defs etc.) here from drule.ML;
wenzelm
parents: 2979
diff changeset
   276
16291
ea4e64b2f25a renamed const_deps to defs;
wenzelm
parents: 16198
diff changeset
   277
in
ea4e64b2f25a renamed const_deps to defs;
wenzelm
parents: 16198
diff changeset
   278
ea4e64b2f25a renamed const_deps to defs;
wenzelm
parents: 16198
diff changeset
   279
val add_defs_i = gen_add_defs cert_axm;
ea4e64b2f25a renamed const_deps to defs;
wenzelm
parents: 16198
diff changeset
   280
val add_defs = gen_add_defs read_axm;
ea4e64b2f25a renamed const_deps to defs;
wenzelm
parents: 16198
diff changeset
   281
ea4e64b2f25a renamed const_deps to defs;
wenzelm
parents: 16198
diff changeset
   282
end;
3767
e2bb53d8dd26 moved theory stuff (add_defs etc.) here from drule.ML;
wenzelm
parents: 2979
diff changeset
   283
e2bb53d8dd26 moved theory stuff (add_defs etc.) here from drule.ML;
wenzelm
parents: 2979
diff changeset
   284
16443
82a116532e3e type theory, theory_ref, exception THEORY and related operations imported from Context;
wenzelm
parents: 16369
diff changeset
   285
(* add_finals(_i) *)
14223
0ee05eef881b Added support for making constants final, that is, ensuring that no
skalberg
parents: 14204
diff changeset
   286
16291
ea4e64b2f25a renamed const_deps to defs;
wenzelm
parents: 16198
diff changeset
   287
local
ea4e64b2f25a renamed const_deps to defs;
wenzelm
parents: 16198
diff changeset
   288
17706
e534e39f3531 back to simple 'defs' (cf. revision 1.79);
wenzelm
parents: 17496
diff changeset
   289
fun gen_add_finals prep_term overloaded args thy =
14223
0ee05eef881b Added support for making constants final, that is, ensuring that no
skalberg
parents: 14204
diff changeset
   290
  let
17706
e534e39f3531 back to simple 'defs' (cf. revision 1.79);
wenzelm
parents: 17496
diff changeset
   291
    fun const_of (Const const) = const
e534e39f3531 back to simple 'defs' (cf. revision 1.79);
wenzelm
parents: 17496
diff changeset
   292
      | const_of (Free _) = error "Attempt to finalize variable (or undeclared constant)"
e534e39f3531 back to simple 'defs' (cf. revision 1.79);
wenzelm
parents: 17496
diff changeset
   293
      | const_of _ = error "Attempt to finalize non-constant term";
19708
a508bde37a81 added add_deps, which actually records dependencies of consts (unlike add_finals);
wenzelm
parents: 19700
diff changeset
   294
    fun specify (c, T) = dependencies thy false false (c ^ " axiom") (c, T) [];
24708
d9b00117365e Syntax.parse/check/read;
wenzelm
parents: 24666
diff changeset
   295
    val finalize = specify o check_overloading thy overloaded o const_of o
d9b00117365e Syntax.parse/check/read;
wenzelm
parents: 24666
diff changeset
   296
      Sign.cert_term thy o prep_term thy;
17706
e534e39f3531 back to simple 'defs' (cf. revision 1.79);
wenzelm
parents: 17496
diff changeset
   297
  in thy |> map_defs (fold finalize args) end;
16291
ea4e64b2f25a renamed const_deps to defs;
wenzelm
parents: 16198
diff changeset
   298
14223
0ee05eef881b Added support for making constants final, that is, ensuring that no
skalberg
parents: 14204
diff changeset
   299
in
16291
ea4e64b2f25a renamed const_deps to defs;
wenzelm
parents: 16198
diff changeset
   300
29581
b3b33e0298eb binding is alias for Binding.T
haftmann
parents: 29092
diff changeset
   301
val add_finals_i = gen_add_finals (K I);
24708
d9b00117365e Syntax.parse/check/read;
wenzelm
parents: 24666
diff changeset
   302
val add_finals = gen_add_finals Syntax.read_term_global;
16291
ea4e64b2f25a renamed const_deps to defs;
wenzelm
parents: 16198
diff changeset
   303
14223
0ee05eef881b Added support for making constants final, that is, ensuring that no
skalberg
parents: 14204
diff changeset
   304
end;
0ee05eef881b Added support for making constants final, that is, ensuring that no
skalberg
parents: 14204
diff changeset
   305
1526
6be6ea6f8b5d New file of just the theory primitives
paulson
parents:
diff changeset
   306
end;