src/Pure/theory.ML
author obua
Tue May 31 19:32:41 2005 +0200 (2005-05-31)
changeset 16158 2c3565b74b7a
parent 16134 89ea482e1649
child 16190 8382835019d1
permissions -rw-r--r--
Removed final_consts from theory data. Now const_deps deals with final
constants.
paulson@1526
     1
(*  Title:      Pure/theory.ML
paulson@1526
     2
    ID:         $Id$
paulson@1526
     3
    Author:     Lawrence C Paulson and Markus Wenzel
paulson@1526
     4
wenzelm@5025
     5
The abstract type "theory" of theories.
paulson@1526
     6
*)
wenzelm@3767
     7
signature BASIC_THEORY =
wenzelm@3767
     8
sig
paulson@1526
     9
  type theory
paulson@1526
    10
  exception THEORY of string * theory list
wenzelm@3996
    11
  val rep_theory: theory ->
wenzelm@3814
    12
    {sign: Sign.sg,
obua@16108
    13
      const_deps: Defs.graph,
wenzelm@3996
    14
      axioms: term Symtab.table,
wenzelm@4996
    15
      oracles: ((Sign.sg * Object.T -> term) * stamp) Symtab.table,
wenzelm@4019
    16
      parents: theory list,
wenzelm@4019
    17
      ancestors: theory list}
wenzelm@3996
    18
  val sign_of: theory -> Sign.sg
wenzelm@6188
    19
  val is_draft: theory -> bool
wenzelm@3996
    20
  val syn_of: theory -> Syntax.syntax
wenzelm@3996
    21
  val parents_of: theory -> theory list
wenzelm@4019
    22
  val ancestors_of: theory -> theory list
wenzelm@3996
    23
  val subthy: theory * theory -> bool
wenzelm@3996
    24
  val eq_thy: theory * theory -> bool
wenzelm@3996
    25
  val cert_axm: Sign.sg -> string * term -> string * term
wenzelm@6311
    26
  val read_def_axm: Sign.sg * (indexname -> typ option) * (indexname -> sort option) ->
wenzelm@6311
    27
    string list -> string * string -> string * term
wenzelm@3996
    28
  val read_axm: Sign.sg -> string * string -> string * term
wenzelm@3996
    29
  val inferT_axm: Sign.sg -> string * term -> string * term
wenzelm@3767
    30
end
wenzelm@3767
    31
wenzelm@3767
    32
signature THEORY =
wenzelm@3767
    33
sig
wenzelm@3767
    34
  include BASIC_THEORY
wenzelm@3996
    35
  val axiomK: string
wenzelm@3996
    36
  val oracleK: string
wenzelm@4912
    37
  (*theory extension primitives*)
wenzelm@3996
    38
  val add_classes: (bclass * xclass list) list -> theory -> theory
wenzelm@3996
    39
  val add_classes_i: (bclass * class list) list -> theory -> theory
wenzelm@3996
    40
  val add_classrel: (xclass * xclass) list -> theory -> theory
wenzelm@3996
    41
  val add_classrel_i: (class * class) list -> theory -> theory
wenzelm@8897
    42
  val add_defsort: string -> theory -> theory
wenzelm@3996
    43
  val add_defsort_i: sort -> theory -> theory
wenzelm@3996
    44
  val add_types: (bstring * int * mixfix) list -> theory -> theory
wenzelm@4846
    45
  val add_nonterminals: bstring list -> theory -> theory
wenzelm@3996
    46
  val add_tyabbrs: (bstring * string list * string * mixfix) list
paulson@1526
    47
    -> theory -> theory
wenzelm@3996
    48
  val add_tyabbrs_i: (bstring * string list * typ * mixfix) list
paulson@1526
    49
    -> theory -> theory
wenzelm@8897
    50
  val add_arities: (xstring * string list * string) list -> theory -> theory
wenzelm@3996
    51
  val add_arities_i: (string * sort list * sort) list -> theory -> theory
wenzelm@3996
    52
  val add_consts: (bstring * string * mixfix) list -> theory -> theory
wenzelm@3996
    53
  val add_consts_i: (bstring * typ * mixfix) list -> theory -> theory
wenzelm@3996
    54
  val add_syntax: (bstring * string * mixfix) list -> theory -> theory
wenzelm@3996
    55
  val add_syntax_i: (bstring * typ * mixfix) list -> theory -> theory
wenzelm@3996
    56
  val add_modesyntax: string * bool -> (bstring * string * mixfix) list -> theory -> theory
wenzelm@3996
    57
  val add_modesyntax_i: string * bool -> (bstring * typ * mixfix) list -> theory -> theory
wenzelm@15747
    58
  val del_modesyntax: string * bool -> (bstring * string * mixfix) list -> theory -> theory
wenzelm@15747
    59
  val del_modesyntax_i: string * bool -> (bstring * typ * mixfix) list -> theory -> theory
wenzelm@3996
    60
  val add_trfuns:
wenzelm@4344
    61
    (string * (Syntax.ast list -> Syntax.ast)) list *
wenzelm@4344
    62
    (string * (term list -> term)) list *
wenzelm@4344
    63
    (string * (term list -> term)) list *
wenzelm@4344
    64
    (string * (Syntax.ast list -> Syntax.ast)) list -> theory -> theory
wenzelm@3996
    65
  val add_trfunsT:
wenzelm@4344
    66
    (string * (bool -> typ -> term list -> term)) list -> theory -> theory
wenzelm@14645
    67
  val add_advanced_trfuns:
wenzelm@14645
    68
    (string * (Sign.sg -> Syntax.ast list -> Syntax.ast)) list *
wenzelm@14645
    69
    (string * (Sign.sg -> term list -> term)) list *
wenzelm@14645
    70
    (string * (Sign.sg -> term list -> term)) list *
wenzelm@14645
    71
    (string * (Sign.sg -> Syntax.ast list -> Syntax.ast)) list -> theory -> theory
wenzelm@14645
    72
  val add_advanced_trfunsT:
wenzelm@14645
    73
    (string * (Sign.sg -> bool -> typ -> term list -> term)) list -> theory -> theory
wenzelm@2693
    74
  val add_tokentrfuns:
wenzelm@6311
    75
    (string * string * (string -> string * real)) list -> theory -> theory
wenzelm@6311
    76
  val add_mode_tokentrfuns: string -> (string * (string -> string * real)) list
wenzelm@6311
    77
    -> theory -> theory
wenzelm@4617
    78
  val add_trrules: (xstring * string) Syntax.trrule list -> theory -> theory
wenzelm@3996
    79
  val add_trrules_i: Syntax.ast Syntax.trrule list -> theory -> theory
wenzelm@3996
    80
  val add_axioms: (bstring * string) list -> theory -> theory
wenzelm@3996
    81
  val add_axioms_i: (bstring * term) list -> theory -> theory
wenzelm@4996
    82
  val add_oracle: bstring * (Sign.sg * Object.T -> term) -> theory -> theory
skalberg@14223
    83
  val add_finals: bool -> string list -> theory -> theory
skalberg@14223
    84
  val add_finals_i: bool -> term list -> theory -> theory
wenzelm@9320
    85
  val add_defs: bool -> (bstring * string) list -> theory -> theory
wenzelm@9320
    86
  val add_defs_i: bool -> (bstring * term) list -> theory -> theory
wenzelm@3996
    87
  val add_path: string -> theory -> theory
wenzelm@4846
    88
  val parent_path: theory -> theory
wenzelm@4846
    89
  val root_path: theory -> theory
wenzelm@11501
    90
  val absolute_path: theory -> theory
wenzelm@16134
    91
  val qualified_names: theory -> theory
wenzelm@16134
    92
  val no_base_names: theory -> theory
wenzelm@16134
    93
  val custom_accesses: (string list -> string list list) -> theory -> theory
wenzelm@16134
    94
  val set_policy: (string -> bstring -> string) * (string list -> string list list) ->
wenzelm@16134
    95
    theory -> theory
wenzelm@16134
    96
  val restore_naming: theory -> theory -> theory
wenzelm@12588
    97
  val hide_space: bool -> string * xstring list -> theory -> theory
wenzelm@12588
    98
  val hide_space_i: bool -> string * string list -> theory -> theory
wenzelm@12588
    99
  val hide_classes: bool -> string list -> theory -> theory
wenzelm@12588
   100
  val hide_types: bool -> string list -> theory -> theory
wenzelm@12588
   101
  val hide_consts: bool -> string list -> theory -> theory
wenzelm@3996
   102
  val add_name: string -> theory -> theory
wenzelm@5862
   103
  val copy: theory -> theory
wenzelm@6661
   104
  val prep_ext: theory -> theory
wenzelm@3996
   105
  val prep_ext_merge: theory list -> theory
paulson@4970
   106
  val requires: theory -> string -> string -> unit
wenzelm@6369
   107
  val assert_super: theory -> theory -> theory
wenzelm@3996
   108
  val pre_pure: theory
paulson@1526
   109
end;
paulson@1526
   110
wenzelm@6188
   111
signature PRIVATE_THEORY =
wenzelm@5642
   112
sig
wenzelm@5642
   113
  include THEORY
wenzelm@6546
   114
  val init_data: Object.kind -> (Object.T * (Object.T -> Object.T) * (Object.T -> Object.T) *
wenzelm@12311
   115
    (Object.T * Object.T -> Object.T) * (Sign.sg -> Object.T -> unit)) -> theory -> theory
wenzelm@5642
   116
  val print_data: Object.kind -> theory -> unit
wenzelm@5642
   117
  val get_data: Object.kind -> (Object.T -> 'a) -> theory -> 'a
wenzelm@5642
   118
  val put_data: Object.kind -> ('a -> Object.T) -> 'a -> theory -> theory
wenzelm@5642
   119
end;
paulson@1526
   120
wenzelm@5642
   121
wenzelm@6188
   122
structure Theory: PRIVATE_THEORY =
paulson@1526
   123
struct
wenzelm@2206
   124
wenzelm@3996
   125
wenzelm@2206
   126
(** datatype theory **)
paulson@1526
   127
paulson@1526
   128
datatype theory =
paulson@1526
   129
  Theory of {
paulson@1526
   130
    sign: Sign.sg,
obua@16108
   131
    const_deps: Defs.graph,
wenzelm@3996
   132
    axioms: term Symtab.table,
wenzelm@4996
   133
    oracles: ((Sign.sg * Object.T -> term) * stamp) Symtab.table,
wenzelm@4019
   134
    parents: theory list,
wenzelm@4019
   135
    ancestors: theory list};
paulson@1526
   136
obua@16158
   137
fun make_theory sign const_deps axioms oracles parents ancestors =
obua@16158
   138
  Theory {sign = sign, const_deps = const_deps, axioms = axioms,
skalberg@14223
   139
    oracles = oracles,  parents = parents, ancestors = ancestors};
wenzelm@3996
   140
paulson@1526
   141
fun rep_theory (Theory args) = args;
paulson@1526
   142
wenzelm@3996
   143
val sign_of = #sign o rep_theory;
wenzelm@6188
   144
val is_draft = Sign.is_draft o sign_of;
wenzelm@14645
   145
val syn_of = Sign.syn_of o sign_of;
wenzelm@3996
   146
val parents_of = #parents o rep_theory;
wenzelm@4019
   147
val ancestors_of = #ancestors o rep_theory;
wenzelm@3996
   148
paulson@1526
   149
(*errors involving theories*)
paulson@1526
   150
exception THEORY of string * theory list;
paulson@1526
   151
paulson@1526
   152
(*compare theories*)
paulson@1526
   153
val subthy = Sign.subsig o pairself sign_of;
paulson@1526
   154
val eq_thy = Sign.eq_sg o pairself sign_of;
paulson@1526
   155
wenzelm@6369
   156
(*check for some theory*)
paulson@4970
   157
fun requires thy name what =
wenzelm@10930
   158
  if Sign.exists_stamp name (sign_of thy) then ()
wenzelm@4846
   159
  else error ("Require theory " ^ quote name ^ " as an ancestor for " ^ what);
paulson@1526
   160
wenzelm@6369
   161
fun assert_super thy1 thy2 =
wenzelm@6369
   162
  if subthy (thy1, thy2) then thy2
wenzelm@6369
   163
  else raise THEORY ("Not a super theory", [thy1, thy2]);
wenzelm@6369
   164
wenzelm@4846
   165
(*partial Pure theory*)
nipkow@9282
   166
val pre_pure =
obua@16158
   167
  make_theory Sign.pre_pure Defs.empty Symtab.empty Symtab.empty [] [];
paulson@1526
   168
paulson@1526
   169
paulson@1526
   170
paulson@1526
   171
(** extend theory **)
paulson@1526
   172
wenzelm@8725
   173
(*name spaces*)
wenzelm@3996
   174
val axiomK = "axiom";
wenzelm@3814
   175
val oracleK = "oracle";
wenzelm@3814
   176
wenzelm@3814
   177
wenzelm@3814
   178
(* extend logical part of a theory *)
wenzelm@3814
   179
paulson@1526
   180
fun err_dup_axms names =
wenzelm@10494
   181
  error ("Duplicate axiom name(s): " ^ commas_quote names);
paulson@1526
   182
wenzelm@3814
   183
fun err_dup_oras names =
wenzelm@10494
   184
  error ("Duplicate oracles: " ^ commas_quote names);
wenzelm@3814
   185
obua@16158
   186
fun ext_theory thy ext_sg new_axms new_oras =
paulson@1526
   187
  let
obua@16158
   188
    val Theory {sign, const_deps, axioms, oracles, parents, ancestors} = thy;
paulson@1526
   189
    val draft = Sign.is_draft sign;
wenzelm@3996
   190
    val axioms' =
wenzelm@4488
   191
      Symtab.extend (if draft then axioms else Symtab.empty, new_axms)
paulson@1526
   192
        handle Symtab.DUPS names => err_dup_axms names;
wenzelm@3814
   193
    val oracles' =
wenzelm@4488
   194
      Symtab.extend (oracles, new_oras)
wenzelm@3814
   195
        handle Symtab.DUPS names => err_dup_oras names;
wenzelm@4019
   196
    val (parents', ancestors') =
wenzelm@4019
   197
      if draft then (parents, ancestors) else ([thy], thy :: ancestors);
paulson@1526
   198
  in
obua@16158
   199
    make_theory (ext_sg sign) const_deps axioms' oracles' parents' ancestors'
paulson@1526
   200
  end;
paulson@1526
   201
paulson@1526
   202
paulson@1526
   203
(* extend signature of a theory *)
paulson@1526
   204
obua@16158
   205
fun ext_sign ext_sg args thy = ext_theory thy (ext_sg args) [] [];
paulson@1526
   206
wenzelm@14645
   207
val add_classes            = ext_sign Sign.add_classes;
wenzelm@14645
   208
val add_classes_i          = ext_sign Sign.add_classes_i;
wenzelm@14645
   209
val add_classrel           = ext_sign Sign.add_classrel;
wenzelm@14645
   210
val add_classrel_i         = ext_sign Sign.add_classrel_i;
wenzelm@14645
   211
val add_defsort            = ext_sign Sign.add_defsort;
wenzelm@14645
   212
val add_defsort_i          = ext_sign Sign.add_defsort_i;
wenzelm@14645
   213
val add_types              = ext_sign Sign.add_types;
wenzelm@14645
   214
val add_nonterminals       = ext_sign Sign.add_nonterminals;
wenzelm@14645
   215
val add_tyabbrs            = ext_sign Sign.add_tyabbrs;
wenzelm@14645
   216
val add_tyabbrs_i          = ext_sign Sign.add_tyabbrs_i;
wenzelm@14645
   217
val add_arities            = ext_sign Sign.add_arities;
wenzelm@14645
   218
val add_arities_i          = ext_sign Sign.add_arities_i;
wenzelm@14645
   219
val add_consts             = ext_sign Sign.add_consts;
wenzelm@14645
   220
val add_consts_i           = ext_sign Sign.add_consts_i;
wenzelm@14645
   221
val add_syntax             = ext_sign Sign.add_syntax;
wenzelm@14645
   222
val add_syntax_i           = ext_sign Sign.add_syntax_i;
wenzelm@14645
   223
val add_modesyntax         = curry (ext_sign Sign.add_modesyntax);
wenzelm@14645
   224
val add_modesyntax_i       = curry (ext_sign Sign.add_modesyntax_i);
wenzelm@15747
   225
val del_modesyntax         = curry (ext_sign Sign.del_modesyntax);
wenzelm@15747
   226
val del_modesyntax_i       = curry (ext_sign Sign.del_modesyntax_i);
wenzelm@14645
   227
val add_trfuns             = ext_sign Sign.add_trfuns;
wenzelm@14645
   228
val add_trfunsT            = ext_sign Sign.add_trfunsT;
wenzelm@14645
   229
val add_advanced_trfuns    = ext_sign Sign.add_advanced_trfuns;
wenzelm@14645
   230
val add_advanced_trfunsT   = ext_sign Sign.add_advanced_trfunsT;
wenzelm@14645
   231
val add_tokentrfuns        = ext_sign Sign.add_tokentrfuns;
wenzelm@6311
   232
fun add_mode_tokentrfuns m = add_tokentrfuns o map (fn (s, f) => (m, s, f));
wenzelm@14645
   233
val add_trrules            = ext_sign Sign.add_trrules;
wenzelm@14645
   234
val add_trrules_i          = ext_sign Sign.add_trrules_i;
wenzelm@14645
   235
val add_path               = ext_sign Sign.add_path;
wenzelm@14645
   236
val parent_path            = add_path "..";
wenzelm@14645
   237
val root_path              = add_path "/";
wenzelm@14645
   238
val absolute_path          = add_path "//";
wenzelm@16134
   239
val qualified_names        = ext_sign (K Sign.qualified_names) ();
wenzelm@16134
   240
val no_base_names          = ext_sign (K Sign.no_base_names) ();
wenzelm@16134
   241
val custom_accesses        = ext_sign Sign.custom_accesses;
wenzelm@16134
   242
val set_policy             = ext_sign Sign.set_policy;
wenzelm@16134
   243
val restore_naming         = ext_sign Sign.set_naming o Sign.naming_of o sign_of;
wenzelm@14645
   244
val add_space              = ext_sign Sign.add_space;
wenzelm@14645
   245
val hide_space             = ext_sign o Sign.hide_space;
wenzelm@14645
   246
val hide_space_i           = ext_sign o Sign.hide_space_i;
wenzelm@14645
   247
fun hide_classes b         = curry (hide_space_i b) Sign.classK;
wenzelm@14645
   248
fun hide_types b           = curry (hide_space_i b) Sign.typeK;
wenzelm@14645
   249
fun hide_consts b          = curry (hide_space_i b) Sign.constK;
wenzelm@14645
   250
val add_name               = ext_sign Sign.add_name;
wenzelm@14645
   251
val copy                   = ext_sign (K Sign.copy) ();
wenzelm@14645
   252
val prep_ext               = ext_sign (K Sign.prep_ext) ();
wenzelm@3814
   253
wenzelm@3996
   254
wenzelm@6311
   255
wenzelm@3814
   256
(** add axioms **)
wenzelm@3814
   257
paulson@1526
   258
(* prepare axioms *)
paulson@1526
   259
paulson@1526
   260
fun err_in_axm name =
paulson@1526
   261
  error ("The error(s) above occurred in axiom " ^ quote name);
paulson@1526
   262
berghofe@14184
   263
fun no_vars sg tm = (case (term_vars tm, term_tvars tm) of
berghofe@14184
   264
    ([], []) => tm
berghofe@14184
   265
  | (ts, ixns) => error (Pretty.string_of (Pretty.block (Pretty.breaks
berghofe@14184
   266
      (Pretty.str "Illegal schematic variable(s) in term:" ::
berghofe@14184
   267
       map (Sign.pretty_term sg) ts @
berghofe@14184
   268
       map (Sign.pretty_typ sg o TVar) ixns)))));
paulson@1526
   269
paulson@1526
   270
fun cert_axm sg (name, raw_tm) =
paulson@1526
   271
  let
wenzelm@14828
   272
    val (t, T, _) = Sign.certify_term (Sign.pp sg) sg raw_tm
wenzelm@2979
   273
      handle TYPE (msg, _, _) => error msg
wenzelm@3996
   274
           | TERM (msg, _) => error msg;
paulson@1526
   275
  in
wenzelm@9537
   276
    Term.no_dummy_patterns t handle TERM (msg, _) => error msg;
paulson@1526
   277
    assert (T = propT) "Term not of type prop";
berghofe@14184
   278
    (name, no_vars sg t)
wenzelm@9629
   279
  end;
paulson@1526
   280
wenzelm@5057
   281
(*some duplication of code with read_def_cterm*)
wenzelm@6661
   282
fun read_def_axm (sg, types, sorts) used (name, str) =
wenzelm@3814
   283
  let
wenzelm@14914
   284
    val ts = Syntax.read (Sign.is_logtype sg) (Sign.syn_of sg) propT str;
wenzelm@14828
   285
    val (t, _) = Sign.infer_types (Sign.pp sg) sg types sorts used true (ts, propT);
wenzelm@9320
   286
  in cert_axm sg (name, t) end
paulson@1960
   287
  handle ERROR => err_in_axm name;
paulson@1526
   288
skalberg@15531
   289
fun read_axm sg name_str = read_def_axm (sg, K NONE, K NONE) [] name_str;
wenzelm@5057
   290
paulson@1526
   291
fun inferT_axm sg (name, pre_tm) =
wenzelm@14828
   292
  let val (t, _) = Sign.infer_types (Sign.pp sg) sg
skalberg@15531
   293
    (K NONE) (K NONE) [] true ([pre_tm], propT);
berghofe@14184
   294
  in (name, no_vars sg t) end
paulson@1526
   295
  handle ERROR => err_in_axm name;
paulson@1526
   296
paulson@1526
   297
paulson@1526
   298
(* extend axioms of a theory *)
paulson@1526
   299
wenzelm@3814
   300
fun ext_axms prep_axm raw_axms (thy as Theory {sign, ...}) =
paulson@1526
   301
  let
wenzelm@3814
   302
    val raw_axms' = map (apfst (Sign.full_name sign)) raw_axms;
wenzelm@3814
   303
    val axioms =
wenzelm@3814
   304
      map (apsnd (Term.compress_term o Logic.varify) o prep_axm sign) raw_axms';
wenzelm@4996
   305
    val ext_sg = Sign.add_space (axiomK, map fst axioms);
obua@16158
   306
  in ext_theory thy ext_sg axioms [] end;
paulson@1526
   307
paulson@1526
   308
val add_axioms = ext_axms read_axm;
paulson@1526
   309
val add_axioms_i = ext_axms cert_axm;
paulson@1526
   310
paulson@1526
   311
wenzelm@3814
   312
(* add oracle **)
wenzelm@3814
   313
wenzelm@3814
   314
fun add_oracle (raw_name, oracle) (thy as Theory {sign, ...}) =
wenzelm@3814
   315
  let
wenzelm@3814
   316
    val name = Sign.full_name sign raw_name;
wenzelm@4996
   317
    val ext_sg = Sign.add_space (oracleK, [name]);
obua@16158
   318
  in ext_theory thy ext_sg [] [(name, (oracle, stamp ()))] end;
wenzelm@3814
   319
wenzelm@3814
   320
wenzelm@3767
   321
wenzelm@3767
   322
(** add constant definitions **)
wenzelm@3767
   323
wenzelm@3767
   324
(* clash_types, clash_consts *)
wenzelm@3767
   325
obua@16108
   326
(*check if types have common instance (ignoring sorts)
wenzelm@3767
   327
wenzelm@3767
   328
fun clash_types ty1 ty2 =
wenzelm@3767
   329
  let
wenzelm@3767
   330
    val ty1' = Type.varifyT ty1;
wenzelm@3767
   331
    val ty2' = incr_tvar (maxidx_of_typ ty1' + 1) (Type.varifyT ty2);
wenzelm@9320
   332
  in Type.raw_unify (ty1', ty2') end;
wenzelm@3767
   333
wenzelm@3767
   334
fun clash_consts (c1, ty1) (c2, ty2) =
wenzelm@3767
   335
  c1 = c2 andalso clash_types ty1 ty2;
obua@16108
   336
*)
wenzelm@3767
   337
wenzelm@16134
   338
obua@16108
   339
(* clash_defns 
wenzelm@3767
   340
wenzelm@3767
   341
fun clash_defn c_ty (name, tm) =
skalberg@14204
   342
  let val (c, ty') = dest_Const (head_of (fst (Logic.dest_equals (Logic.strip_imp_concl tm)))) in
skalberg@15531
   343
    if clash_consts c_ty (c, ty') then SOME (name, ty') else NONE
skalberg@15531
   344
  end handle TERM _ => NONE;
wenzelm@3767
   345
wenzelm@3767
   346
fun clash_defns c_ty axms =
skalberg@15570
   347
  distinct (List.mapPartial (clash_defn c_ty) axms);
obua@16108
   348
*)
wenzelm@3767
   349
wenzelm@3767
   350
wenzelm@9320
   351
(* overloading *)
nipkow@9280
   352
wenzelm@9320
   353
datatype overloading = NoOverloading | Useless | Plain;
wenzelm@9320
   354
wenzelm@9320
   355
fun overloading sg declT defT =
wenzelm@10403
   356
  let val T = Term.incr_tvar (maxidx_of_typ declT + 1) (Type.varifyT defT) in
wenzelm@10403
   357
    if Sign.typ_instance sg (declT, T) then NoOverloading
wenzelm@14789
   358
    else if Sign.typ_instance sg (Type.strip_sorts declT, Type.strip_sorts T) then Useless
wenzelm@9320
   359
    else Plain
nipkow@9280
   360
  end;
nipkow@9280
   361
nipkow@9280
   362
wenzelm@3767
   363
(* dest_defn *)
wenzelm@3767
   364
wenzelm@3767
   365
fun dest_defn tm =
wenzelm@3767
   366
  let
wenzelm@3787
   367
    fun err msg = raise TERM (msg, [tm]);
wenzelm@3767
   368
wenzelm@3767
   369
    val (lhs, rhs) = Logic.dest_equals (Logic.strip_imp_concl tm)
wenzelm@3767
   370
      handle TERM _ => err "Not a meta-equality (==)";
wenzelm@3767
   371
    val (head, args) = strip_comb lhs;
wenzelm@9320
   372
    val c_ty as (c, ty) = dest_Const head
wenzelm@3767
   373
      handle TERM _ => err "Head of lhs not a constant";
wenzelm@3767
   374
wenzelm@4141
   375
    fun dest_free (Free (x, _)) = x
wenzelm@4141
   376
      | dest_free (Const ("TYPE", Type ("itself", [TFree (x, _)]))) = x
wenzelm@4141
   377
      | dest_free _ = raise Match;
wenzelm@4141
   378
wenzelm@4141
   379
    val show_frees = commas_quote o map dest_free;
wenzelm@3767
   380
    val show_tfrees = commas_quote o map fst;
wenzelm@3767
   381
wenzelm@3767
   382
    val lhs_dups = duplicates args;
wenzelm@3767
   383
    val rhs_extras = gen_rems (op =) (term_frees rhs, args);
wenzelm@3767
   384
    val rhs_extrasT = gen_rems (op =) (term_tfrees rhs, typ_tfrees ty);
wenzelm@3767
   385
  in
wenzelm@4141
   386
    if not (forall (can dest_free) args) then
wenzelm@3767
   387
      err "Arguments (on lhs) must be variables"
wenzelm@3767
   388
    else if not (null lhs_dups) then
wenzelm@3767
   389
      err ("Duplicate variables on lhs: " ^ show_frees lhs_dups)
wenzelm@3767
   390
    else if not (null rhs_extras) then
wenzelm@3767
   391
      err ("Extra variables on rhs: " ^ show_frees rhs_extras)
wenzelm@3767
   392
    else if not (null rhs_extrasT) then
wenzelm@3767
   393
      err ("Extra type variables on rhs: " ^ show_tfrees rhs_extrasT)
nipkow@9282
   394
    else if exists_Const (fn c_ty' => c_ty' = c_ty) rhs then
wenzelm@3767
   395
      err ("Constant to be defined occurs on rhs")
wenzelm@9320
   396
    else (c_ty, rhs)
wenzelm@3767
   397
  end;
wenzelm@3767
   398
wenzelm@3767
   399
wenzelm@3767
   400
(* check_defn *)
wenzelm@3767
   401
wenzelm@3814
   402
fun err_in_defn sg name msg =
wenzelm@9320
   403
  (error_msg msg;
wenzelm@9320
   404
    error ("The error(s) above occurred in definition " ^ quote (Sign.full_name sg name)));
wenzelm@9320
   405
obua@16108
   406
fun pretty_const sg (c, ty) = [Pretty.str c, Pretty.str " ::", Pretty.quote (Sign.pretty_typ sg (#1 (Type.freeze_thaw_type ty)))];
wenzelm@3767
   407
obua@16113
   408
fun cycle_msg sg (infinite, namess) = 
obua@16113
   409
  let val header = if not (infinite) then "cyclic dependency found: " else "infinite chain found: "
obua@16113
   410
  in
obua@16113
   411
      Pretty.string_of (Pretty.block (((Pretty.str header) :: Pretty.fbrk :: (
obua@16113
   412
        let      
obua@16113
   413
	    fun f last (ty, constname, defname) =  
obua@16113
   414
		(pretty_const sg (constname, ty)) @ (if last then [] else [Pretty.str (" depends via "^ quote defname^ " on ")])
obua@16108
   415
          	
obua@16113
   416
	in
obua@16113
   417
	    foldr (fn (x,r) => (f (r=[]) x)@[Pretty.fbrk]@r) [] namess
obua@16113
   418
	end))))
obua@16113
   419
  end
wenzelm@9320
   420
obua@16158
   421
fun check_defn sg overloaded ((deps, axms), def as (name, tm)) =
skalberg@14223
   422
  let
obua@16108
   423
    
obua@16108
   424
    val name = Sign.full_name sg name
obua@16108
   425
      
wenzelm@10494
   426
    fun pretty_const (c, ty) = [Pretty.str c, Pretty.str " ::", Pretty.brk 1,
wenzelm@10494
   427
      Pretty.quote (Sign.pretty_typ sg (#1 (Type.freeze_thaw_type ty)))];
wenzelm@3767
   428
wenzelm@10494
   429
    fun def_txt (c_ty, txt) = Pretty.block
wenzelm@10494
   430
      (Pretty.str "Definition of " :: pretty_const c_ty @
wenzelm@10494
   431
        (if txt = "" then [] else [Pretty.str txt]));
wenzelm@10494
   432
wenzelm@10494
   433
    fun show_defn c (dfn, ty') = Pretty.block
wenzelm@10494
   434
      (Pretty.str "  " :: pretty_const (c, ty') @ [Pretty.str " in ", Pretty.str dfn]);
wenzelm@3767
   435
wenzelm@9320
   436
    val (c_ty as (c, ty), rhs) = dest_defn tm
nipkow@9280
   437
      handle TERM (msg, _) => err_in_defn sg name msg;
obua@16108
   438
obua@16108
   439
    fun decl deps c = 
obua@16158
   440
	(case Sign.const_type sg c of 
obua@16158
   441
	     SOME T => (Defs.declare deps (c, T) handle _ => deps, T)
obua@16158
   442
	   | NONE => err_in_defn sg name ("Undeclared constant " ^ quote c));
wenzelm@9320
   443
obua@16108
   444
    val (deps, c_decl) = decl deps c
obua@16108
   445
obua@16108
   446
    val body = Term.term_constsT rhs
obua@16108
   447
    val deps = foldl (fn ((c, _), deps) => fst (decl deps c)) deps body
obua@16108
   448
wenzelm@3767
   449
  in
wenzelm@9320
   450
      (case overloading sg c_decl ty of
wenzelm@16134
   451
         Useless =>
wenzelm@10494
   452
           err_in_defn sg name (Pretty.string_of (Pretty.chunks
wenzelm@16134
   453
           [Library.setmp show_sorts true def_txt (c_ty, ""), Pretty.str
obua@16108
   454
              "imposes additional sort constraints on the declared type of the constant"]))   
obua@16108
   455
       | ov =>
obua@16108
   456
	 let 
obua@16158
   457
	     val deps' = Defs.define deps c_ty name body
obua@16108
   458
		 handle Defs.DEFS s => err_in_defn sg name ("DEFS: "^s) 
obua@16113
   459
		      | Defs.CIRCULAR s => err_in_defn sg name (cycle_msg sg (false, s))
obua@16113
   460
                      | Defs.INFINITE_CHAIN s => err_in_defn sg name (cycle_msg sg (true, s)) 
obua@16108
   461
                      | Defs.CLASH (_, def1, def2) => err_in_defn sg name (
obua@16158
   462
			  "clashing definitions "^ quote def1 ^" and "^ quote def2)
obua@16158
   463
		      | Defs.FINAL cfinal =>
obua@16158
   464
			err_in_defn sg name (Pretty.string_of (Pretty.block
obua@16158
   465
			  ([Pretty.str "The constant",Pretty.brk 1] @
obua@16158
   466
			   pretty_const cfinal @
obua@16158
   467
			   [Pretty.brk 1,Pretty.str "has been declared final"]))) 
obua@16158
   468
	 in
obua@16158
   469
	     ((if ov = Plain andalso not overloaded then
obua@16158
   470
		   warning (Pretty.string_of (Pretty.chunks
obua@16158
   471
		     [def_txt (c_ty, ""), Pretty.str ("is strictly less general than the declared type (see " ^ quote name ^ ")")]))
obua@16158
   472
	       else
obua@16158
   473
		   ()); (deps', def::axms))
obua@16158
   474
	 end)
wenzelm@3767
   475
  end;
wenzelm@3767
   476
wenzelm@3767
   477
wenzelm@3767
   478
(* add_defs *)
wenzelm@3767
   479
wenzelm@9320
   480
fun ext_defns prep_axm overloaded raw_axms thy =
wenzelm@3767
   481
  let
obua@16158
   482
    val Theory {sign, const_deps, axioms, oracles, parents, ancestors} = thy;
skalberg@15570
   483
    val all_axioms = List.concat (map (Symtab.dest o #axioms o rep_theory) (thy :: ancestors));
wenzelm@9320
   484
wenzelm@9320
   485
    val axms = map (prep_axm sign) raw_axms;
obua@16158
   486
    val (const_deps', _) = Library.foldl (check_defn sign overloaded) ((const_deps, all_axioms), axms);
wenzelm@3767
   487
  in
obua@16158
   488
    make_theory sign const_deps' axioms oracles parents ancestors
wenzelm@9320
   489
    |> add_axioms_i axms
wenzelm@3767
   490
  end;
wenzelm@3767
   491
wenzelm@3767
   492
val add_defs_i = ext_defns cert_axm;
wenzelm@3767
   493
val add_defs = ext_defns read_axm;
wenzelm@3767
   494
wenzelm@3767
   495
skalberg@14223
   496
(* add_finals *)
skalberg@14223
   497
skalberg@14223
   498
fun ext_finals prep_term overloaded raw_terms thy =
skalberg@14223
   499
  let
obua@16158
   500
    val Theory {sign, const_deps, axioms, oracles, parents, ancestors} = thy;
obua@16158
   501
    fun mk_final (tm, finals) =
obua@16158
   502
	let
obua@16158
   503
            fun err msg = raise TERM(msg,[tm])
obua@16158
   504
            val (c,ty) = dest_Const tm
obua@16158
   505
		handle TERM _ => err "Can only make constants final"
obua@16158
   506
            val c_decl =
obua@16158
   507
		(case Sign.const_type sign c of 
obua@16158
   508
		     SOME T => T
obua@16158
   509
		   | NONE => err ("Undeclared constant " ^ quote c))
obua@16158
   510
	    val _ =
obua@16158
   511
		case overloading sign c_decl ty of
obua@16158
   512
		    NoOverloading => ()
obua@16158
   513
		  | Useless => err "Sort restrictions too strong"
obua@16158
   514
		  | Plain => (if overloaded then () else warning "Type is more general than declared")
obua@16158
   515
	    val finals = Defs.declare finals (c, c_decl) handle _ => finals
obua@16158
   516
	in
obua@16158
   517
	    Defs.finalize finals (c,ty)
obua@16158
   518
	end
skalberg@14223
   519
    val consts = map (prep_term sign) raw_terms;
obua@16158
   520
    val const_deps' = foldl mk_final const_deps consts;
skalberg@14223
   521
  in
obua@16158
   522
    make_theory sign const_deps' axioms oracles parents ancestors
skalberg@14223
   523
  end;
skalberg@14223
   524
skalberg@14223
   525
local
skalberg@14223
   526
  fun read_term sg = Sign.simple_read_term sg TypeInfer.logicT;
wenzelm@14828
   527
  fun cert_term sg = #1 o Sign.certify_term (Sign.pp sg) sg;
skalberg@14223
   528
in
skalberg@14223
   529
val add_finals = ext_finals read_term;
skalberg@14223
   530
val add_finals_i = ext_finals cert_term;
skalberg@14223
   531
end;
skalberg@14223
   532
skalberg@14223
   533
fun merge_final sg =
skalberg@14223
   534
  let
skalberg@14223
   535
    fun merge_single (tys,ty) =
skalberg@14223
   536
      if exists (curry (Sign.typ_instance sg) ty) tys
skalberg@14223
   537
      then tys
skalberg@14223
   538
      else (ty::gen_rem (Sign.typ_instance sg) (tys,ty));
skalberg@14223
   539
    fun merge ([],_) = []
skalberg@14223
   540
      | merge (_,[]) = []
skalberg@15570
   541
      | merge input = Library.foldl merge_single input;
skalberg@14223
   542
  in
skalberg@15531
   543
    SOME o merge
skalberg@14223
   544
  end;
skalberg@14223
   545
wenzelm@3878
   546
wenzelm@3865
   547
(** additional theory data **)
wenzelm@3865
   548
wenzelm@4996
   549
val init_data = curry (ext_sign Sign.init_data);
wenzelm@4996
   550
fun print_data kind = Sign.print_data kind o sign_of;
wenzelm@4996
   551
fun get_data kind f = Sign.get_data kind f o sign_of;
wenzelm@4996
   552
fun put_data kind f = ext_sign (Sign.put_data kind f);
wenzelm@3865
   553
wenzelm@3865
   554
wenzelm@3767
   555
wenzelm@6661
   556
(** merge theories **)          (*exception ERROR*)
wenzelm@4019
   557
wenzelm@3878
   558
(*merge list of theories from left to right, preparing extend*)
wenzelm@3967
   559
fun prep_ext_merge thys =
wenzelm@15703
   560
  let
wenzelm@15703
   561
    val sign' = Sign.prep_ext_merge (map sign_of thys)
wenzelm@3814
   562
wenzelm@15703
   563
    val depss = map (#const_deps o rep_theory) thys;
obua@16108
   564
    val deps' = foldl (uncurry Defs.merge) (hd depss) (tl depss)
obua@16113
   565
      handle Defs.CIRCULAR namess => error (cycle_msg sign' (false, namess))
obua@16113
   566
	   | Defs.INFINITE_CHAIN namess => error (cycle_msg sign' (true, namess))
wenzelm@15703
   567
wenzelm@15703
   568
    val axioms' = Symtab.empty;
nipkow@9282
   569
wenzelm@15703
   570
    fun eq_ora ((_, (_, s1: stamp)), (_, (_, s2))) = s1 = s2;
wenzelm@15703
   571
    val oracles' =
wenzelm@15703
   572
      Symtab.make (gen_distinct eq_ora
wenzelm@15703
   573
        (List.concat (map (Symtab.dest o #oracles o rep_theory) thys)))
wenzelm@15703
   574
      handle Symtab.DUPS names => err_dup_oras names;
wenzelm@4019
   575
wenzelm@15703
   576
    val parents' = gen_distinct eq_thy thys;
wenzelm@15703
   577
    val ancestors' =
wenzelm@15703
   578
      gen_distinct eq_thy (parents' @ List.concat (map ancestors_of thys));
wenzelm@15703
   579
  in
obua@16158
   580
    make_theory sign' deps' axioms' oracles' parents' ancestors'
wenzelm@15703
   581
  end;
paulson@1526
   582
wenzelm@3885
   583
paulson@1526
   584
end;
paulson@1526
   585
wenzelm@3767
   586
structure BasicTheory: BASIC_THEORY = Theory;
wenzelm@3767
   587
open BasicTheory;
wenzelm@15716
   588