src/Pure/facts.ML
author wenzelm
Sun, 25 Oct 2009 19:14:25 +0100
changeset 33163 351fc13613f2
parent 33096 db3c18fd9708
child 35408 b48ab741683b
permissions -rw-r--r--
export is_concealed; tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
26281
328fd1c551ef Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff changeset
     1
(*  Title:      Pure/facts.ML
328fd1c551ef Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
328fd1c551ef Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff changeset
     3
26307
27d3de85c266 replaced generic add by add_local/add_global;
wenzelm
parents: 26290
diff changeset
     4
Environment of named facts, optionally indexed by proposition.
26281
328fd1c551ef Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff changeset
     5
*)
328fd1c551ef Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff changeset
     6
328fd1c551ef Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff changeset
     7
signature FACTS =
328fd1c551ef Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff changeset
     8
sig
26336
a0e2b706ce73 renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents: 26307
diff changeset
     9
  val the_single: string -> thm list -> thm
a0e2b706ce73 renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents: 26307
diff changeset
    10
  datatype interval = FromTo of int * int | From of int | Single of int
a0e2b706ce73 renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents: 26307
diff changeset
    11
  datatype ref =
26361
7946f459c6c8 Facts.Named: include position;
wenzelm
parents: 26336
diff changeset
    12
    Named of (string * Position.T) * interval list option |
26336
a0e2b706ce73 renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents: 26307
diff changeset
    13
    Fact of string
26361
7946f459c6c8 Facts.Named: include position;
wenzelm
parents: 26336
diff changeset
    14
  val named: string -> ref
26336
a0e2b706ce73 renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents: 26307
diff changeset
    15
  val string_of_ref: ref -> string
a0e2b706ce73 renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents: 26307
diff changeset
    16
  val name_of_ref: ref -> string
26366
5c089f4219c2 added pos_of_ref;
wenzelm
parents: 26361
diff changeset
    17
  val pos_of_ref: ref -> Position.T
26336
a0e2b706ce73 renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents: 26307
diff changeset
    18
  val map_name_of_ref: (string -> string) -> ref -> ref
a0e2b706ce73 renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents: 26307
diff changeset
    19
  val select: ref -> thm list -> thm list
a0e2b706ce73 renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents: 26307
diff changeset
    20
  val selections: string * thm list -> (ref * thm) list
26281
328fd1c551ef Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff changeset
    21
  type T
26393
42febbed5460 support dynamic facts;
wenzelm
parents: 26366
diff changeset
    22
  val empty: T
33095
bbd52d2f8696 renamed NameSpace to Name_Space -- also to emphasize its subtle change in semantics;
wenzelm
parents: 33093
diff changeset
    23
  val space_of: T -> Name_Space.T
33163
351fc13613f2 export is_concealed;
wenzelm
parents: 33096
diff changeset
    24
  val is_concealed: T -> string -> bool
26664
167d879a89b0 renamed dest to dest_table, and extern to extern table;
wenzelm
parents: 26654
diff changeset
    25
  val intern: T -> xstring -> string
167d879a89b0 renamed dest to dest_table, and extern to extern table;
wenzelm
parents: 26654
diff changeset
    26
  val extern: T -> string -> xstring
27738
66596d7aa899 Facts.lookup: return static/dynamic status;
wenzelm
parents: 27175
diff changeset
    27
  val lookup: Context.generic -> T -> string -> (bool * thm list) option
26692
3f48d4f4229f removed unused space_of;
wenzelm
parents: 26664
diff changeset
    28
  val defined: T -> string -> bool
3f48d4f4229f removed unused space_of;
wenzelm
parents: 26664
diff changeset
    29
  val fold_static: (string * thm list -> 'a -> 'a) -> T -> 'a -> 'a
27175
620295a57106 dest/export_static: content difference;
wenzelm
parents: 26692
diff changeset
    30
  val dest_static: T list -> T -> (string * thm list) list
620295a57106 dest/export_static: content difference;
wenzelm
parents: 26692
diff changeset
    31
  val extern_static: T list -> T -> (xstring * thm list) list
26281
328fd1c551ef Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff changeset
    32
  val props: T -> thm list
328fd1c551ef Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff changeset
    33
  val could_unify: T -> term -> thm list
328fd1c551ef Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff changeset
    34
  val merge: T * T -> T
33095
bbd52d2f8696 renamed NameSpace to Name_Space -- also to emphasize its subtle change in semantics;
wenzelm
parents: 33093
diff changeset
    35
  val add_global: Name_Space.naming -> binding * thm list -> T -> string * T
bbd52d2f8696 renamed NameSpace to Name_Space -- also to emphasize its subtle change in semantics;
wenzelm
parents: 33093
diff changeset
    36
  val add_local: bool -> Name_Space.naming -> binding * thm list -> T -> string * T
bbd52d2f8696 renamed NameSpace to Name_Space -- also to emphasize its subtle change in semantics;
wenzelm
parents: 33093
diff changeset
    37
  val add_dynamic: Name_Space.naming -> binding * (Context.generic -> thm list) -> T -> string * T
26654
1f711934f221 disallow duplicate entries (weak version for merge);
wenzelm
parents: 26393
diff changeset
    38
  val del: string -> T -> T
1f711934f221 disallow duplicate entries (weak version for merge);
wenzelm
parents: 26393
diff changeset
    39
  val hide: bool -> string -> T -> T
26281
328fd1c551ef Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff changeset
    40
end;
328fd1c551ef Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff changeset
    41
328fd1c551ef Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff changeset
    42
structure Facts: FACTS =
328fd1c551ef Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff changeset
    43
struct
328fd1c551ef Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff changeset
    44
26336
a0e2b706ce73 renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents: 26307
diff changeset
    45
(** fact references **)
a0e2b706ce73 renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents: 26307
diff changeset
    46
a0e2b706ce73 renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents: 26307
diff changeset
    47
fun the_single _ [th] : thm = th
33163
351fc13613f2 export is_concealed;
wenzelm
parents: 33096
diff changeset
    48
  | the_single name _ = error ("Expected singleton fact " ^ quote name);
26336
a0e2b706ce73 renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents: 26307
diff changeset
    49
a0e2b706ce73 renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents: 26307
diff changeset
    50
a0e2b706ce73 renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents: 26307
diff changeset
    51
(* datatype interval *)
a0e2b706ce73 renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents: 26307
diff changeset
    52
a0e2b706ce73 renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents: 26307
diff changeset
    53
datatype interval =
a0e2b706ce73 renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents: 26307
diff changeset
    54
  FromTo of int * int |
a0e2b706ce73 renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents: 26307
diff changeset
    55
  From of int |
a0e2b706ce73 renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents: 26307
diff changeset
    56
  Single of int;
a0e2b706ce73 renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents: 26307
diff changeset
    57
a0e2b706ce73 renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents: 26307
diff changeset
    58
fun string_of_interval (FromTo (i, j)) = string_of_int i ^ "-" ^ string_of_int j
a0e2b706ce73 renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents: 26307
diff changeset
    59
  | string_of_interval (From i) = string_of_int i ^ "-"
a0e2b706ce73 renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents: 26307
diff changeset
    60
  | string_of_interval (Single i) = string_of_int i;
a0e2b706ce73 renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents: 26307
diff changeset
    61
a0e2b706ce73 renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents: 26307
diff changeset
    62
fun interval n iv =
a0e2b706ce73 renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents: 26307
diff changeset
    63
  let fun err () = raise Fail ("Bad interval specification " ^ string_of_interval iv) in
a0e2b706ce73 renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents: 26307
diff changeset
    64
    (case iv of
a0e2b706ce73 renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents: 26307
diff changeset
    65
      FromTo (i, j) => if i <= j then i upto j else err ()
a0e2b706ce73 renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents: 26307
diff changeset
    66
    | From i => if i <= n then i upto n else err ()
a0e2b706ce73 renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents: 26307
diff changeset
    67
    | Single i => [i])
a0e2b706ce73 renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents: 26307
diff changeset
    68
  end;
a0e2b706ce73 renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents: 26307
diff changeset
    69
a0e2b706ce73 renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents: 26307
diff changeset
    70
a0e2b706ce73 renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents: 26307
diff changeset
    71
(* datatype ref *)
a0e2b706ce73 renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents: 26307
diff changeset
    72
a0e2b706ce73 renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents: 26307
diff changeset
    73
datatype ref =
26361
7946f459c6c8 Facts.Named: include position;
wenzelm
parents: 26336
diff changeset
    74
  Named of (string * Position.T) * interval list option |
26336
a0e2b706ce73 renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents: 26307
diff changeset
    75
  Fact of string;
a0e2b706ce73 renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents: 26307
diff changeset
    76
26361
7946f459c6c8 Facts.Named: include position;
wenzelm
parents: 26336
diff changeset
    77
fun named name = Named ((name, Position.none), NONE);
7946f459c6c8 Facts.Named: include position;
wenzelm
parents: 26336
diff changeset
    78
26366
5c089f4219c2 added pos_of_ref;
wenzelm
parents: 26361
diff changeset
    79
fun name_pos_of_ref (Named (name_pos, _)) = name_pos
5c089f4219c2 added pos_of_ref;
wenzelm
parents: 26361
diff changeset
    80
  | name_pos_of_ref (Fact _) = error "Illegal literal fact";
5c089f4219c2 added pos_of_ref;
wenzelm
parents: 26361
diff changeset
    81
5c089f4219c2 added pos_of_ref;
wenzelm
parents: 26361
diff changeset
    82
val name_of_ref = #1 o name_pos_of_ref;
5c089f4219c2 added pos_of_ref;
wenzelm
parents: 26361
diff changeset
    83
val pos_of_ref = #2 o name_pos_of_ref;
26336
a0e2b706ce73 renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents: 26307
diff changeset
    84
26361
7946f459c6c8 Facts.Named: include position;
wenzelm
parents: 26336
diff changeset
    85
fun map_name_of_ref f (Named ((name, pos), is)) = Named ((f name, pos), is)
26336
a0e2b706ce73 renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents: 26307
diff changeset
    86
  | map_name_of_ref _ r = r;
a0e2b706ce73 renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents: 26307
diff changeset
    87
26361
7946f459c6c8 Facts.Named: include position;
wenzelm
parents: 26336
diff changeset
    88
fun string_of_ref (Named ((name, _), NONE)) = name
7946f459c6c8 Facts.Named: include position;
wenzelm
parents: 26336
diff changeset
    89
  | string_of_ref (Named ((name, _), SOME is)) =
26336
a0e2b706ce73 renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents: 26307
diff changeset
    90
      name ^ enclose "(" ")" (commas (map string_of_interval is))
a0e2b706ce73 renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents: 26307
diff changeset
    91
  | string_of_ref (Fact _) = error "Illegal literal fact";
a0e2b706ce73 renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents: 26307
diff changeset
    92
a0e2b706ce73 renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents: 26307
diff changeset
    93
a0e2b706ce73 renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents: 26307
diff changeset
    94
(* select *)
a0e2b706ce73 renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents: 26307
diff changeset
    95
a0e2b706ce73 renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents: 26307
diff changeset
    96
fun select (Fact _) ths = ths
a0e2b706ce73 renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents: 26307
diff changeset
    97
  | select (Named (_, NONE)) ths = ths
26361
7946f459c6c8 Facts.Named: include position;
wenzelm
parents: 26336
diff changeset
    98
  | select (Named ((name, pos), SOME ivs)) ths =
26336
a0e2b706ce73 renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents: 26307
diff changeset
    99
      let
a0e2b706ce73 renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents: 26307
diff changeset
   100
        val n = length ths;
26361
7946f459c6c8 Facts.Named: include position;
wenzelm
parents: 26336
diff changeset
   101
        fun err msg =
7946f459c6c8 Facts.Named: include position;
wenzelm
parents: 26336
diff changeset
   102
          error (msg ^ " for " ^ quote name ^ " (length " ^ string_of_int n ^ ")" ^
7946f459c6c8 Facts.Named: include position;
wenzelm
parents: 26336
diff changeset
   103
            Position.str_of pos);
26336
a0e2b706ce73 renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents: 26307
diff changeset
   104
        fun sel i =
a0e2b706ce73 renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents: 26307
diff changeset
   105
          if i < 1 orelse i > n then err ("Bad subscript " ^ string_of_int i)
a0e2b706ce73 renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents: 26307
diff changeset
   106
          else nth ths (i - 1);
a0e2b706ce73 renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents: 26307
diff changeset
   107
        val is = maps (interval n) ivs handle Fail msg => err msg;
a0e2b706ce73 renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents: 26307
diff changeset
   108
      in map sel is end;
a0e2b706ce73 renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents: 26307
diff changeset
   109
a0e2b706ce73 renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents: 26307
diff changeset
   110
a0e2b706ce73 renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents: 26307
diff changeset
   111
(* selections *)
a0e2b706ce73 renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents: 26307
diff changeset
   112
26361
7946f459c6c8 Facts.Named: include position;
wenzelm
parents: 26336
diff changeset
   113
fun selections (name, [th]) = [(Named ((name, Position.none), NONE), th)]
7946f459c6c8 Facts.Named: include position;
wenzelm
parents: 26336
diff changeset
   114
  | selections (name, ths) = map2 (fn i => fn th =>
7946f459c6c8 Facts.Named: include position;
wenzelm
parents: 26336
diff changeset
   115
      (Named ((name, Position.none), SOME [Single i]), th)) (1 upto length ths) ths;
26336
a0e2b706ce73 renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents: 26307
diff changeset
   116
a0e2b706ce73 renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents: 26307
diff changeset
   117
a0e2b706ce73 renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents: 26307
diff changeset
   118
a0e2b706ce73 renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents: 26307
diff changeset
   119
(** fact environment **)
a0e2b706ce73 renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents: 26307
diff changeset
   120
26393
42febbed5460 support dynamic facts;
wenzelm
parents: 26366
diff changeset
   121
(* datatypes *)
42febbed5460 support dynamic facts;
wenzelm
parents: 26366
diff changeset
   122
42febbed5460 support dynamic facts;
wenzelm
parents: 26366
diff changeset
   123
datatype fact = Static of thm list | Dynamic of Context.generic -> thm list;
26281
328fd1c551ef Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff changeset
   124
328fd1c551ef Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff changeset
   125
datatype T = Facts of
33095
bbd52d2f8696 renamed NameSpace to Name_Space -- also to emphasize its subtle change in semantics;
wenzelm
parents: 33093
diff changeset
   126
 {facts: fact Name_Space.table,
26281
328fd1c551ef Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff changeset
   127
  props: thm Net.net};
328fd1c551ef Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff changeset
   128
328fd1c551ef Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff changeset
   129
fun make_facts facts props = Facts {facts = facts, props = props};
33163
351fc13613f2 export is_concealed;
wenzelm
parents: 33096
diff changeset
   130
33096
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
   131
val empty = make_facts (Name_Space.empty_table "fact") Net.empty;
26281
328fd1c551ef Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff changeset
   132
328fd1c551ef Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff changeset
   133
328fd1c551ef Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff changeset
   134
(* named facts *)
328fd1c551ef Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff changeset
   135
328fd1c551ef Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff changeset
   136
fun facts_of (Facts {facts, ...}) = facts;
328fd1c551ef Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff changeset
   137
328fd1c551ef Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff changeset
   138
val space_of = #1 o facts_of;
26393
42febbed5460 support dynamic facts;
wenzelm
parents: 26366
diff changeset
   139
val table_of = #2 o facts_of;
42febbed5460 support dynamic facts;
wenzelm
parents: 26366
diff changeset
   140
33163
351fc13613f2 export is_concealed;
wenzelm
parents: 33096
diff changeset
   141
val is_concealed = Name_Space.is_concealed o space_of;
351fc13613f2 export is_concealed;
wenzelm
parents: 33096
diff changeset
   142
33095
bbd52d2f8696 renamed NameSpace to Name_Space -- also to emphasize its subtle change in semantics;
wenzelm
parents: 33093
diff changeset
   143
val intern = Name_Space.intern o space_of;
bbd52d2f8696 renamed NameSpace to Name_Space -- also to emphasize its subtle change in semantics;
wenzelm
parents: 33093
diff changeset
   144
val extern = Name_Space.extern o space_of;
26664
167d879a89b0 renamed dest to dest_table, and extern to extern table;
wenzelm
parents: 26654
diff changeset
   145
26692
3f48d4f4229f removed unused space_of;
wenzelm
parents: 26664
diff changeset
   146
val defined = Symtab.defined o table_of;
3f48d4f4229f removed unused space_of;
wenzelm
parents: 26664
diff changeset
   147
26393
42febbed5460 support dynamic facts;
wenzelm
parents: 26366
diff changeset
   148
fun lookup context facts name =
42febbed5460 support dynamic facts;
wenzelm
parents: 26366
diff changeset
   149
  (case Symtab.lookup (table_of facts) name of
42febbed5460 support dynamic facts;
wenzelm
parents: 26366
diff changeset
   150
    NONE => NONE
33093
d010f61d3702 eliminated separate stamp -- NameSpace.define/merge etc. ensure uniqueness already;
wenzelm
parents: 29848
diff changeset
   151
  | SOME (Static ths) => SOME (true, ths)
d010f61d3702 eliminated separate stamp -- NameSpace.define/merge etc. ensure uniqueness already;
wenzelm
parents: 29848
diff changeset
   152
  | SOME (Dynamic f) => SOME (false, f context));
26393
42febbed5460 support dynamic facts;
wenzelm
parents: 26366
diff changeset
   153
33093
d010f61d3702 eliminated separate stamp -- NameSpace.define/merge etc. ensure uniqueness already;
wenzelm
parents: 29848
diff changeset
   154
fun fold_static f =
d010f61d3702 eliminated separate stamp -- NameSpace.define/merge etc. ensure uniqueness already;
wenzelm
parents: 29848
diff changeset
   155
  Symtab.fold (fn (name, Static ths) => f (name, ths) | _ => I) o table_of;
26393
42febbed5460 support dynamic facts;
wenzelm
parents: 26366
diff changeset
   156
27175
620295a57106 dest/export_static: content difference;
wenzelm
parents: 26692
diff changeset
   157
620295a57106 dest/export_static: content difference;
wenzelm
parents: 26692
diff changeset
   158
(* content difference *)
620295a57106 dest/export_static: content difference;
wenzelm
parents: 26692
diff changeset
   159
620295a57106 dest/export_static: content difference;
wenzelm
parents: 26692
diff changeset
   160
fun diff_table prev_facts facts =
620295a57106 dest/export_static: content difference;
wenzelm
parents: 26692
diff changeset
   161
  fold_static (fn (name, ths) =>
620295a57106 dest/export_static: content difference;
wenzelm
parents: 26692
diff changeset
   162
    if exists (fn prev => defined prev name) prev_facts then I
620295a57106 dest/export_static: content difference;
wenzelm
parents: 26692
diff changeset
   163
    else cons (name, ths)) facts [];
620295a57106 dest/export_static: content difference;
wenzelm
parents: 26692
diff changeset
   164
620295a57106 dest/export_static: content difference;
wenzelm
parents: 26692
diff changeset
   165
fun dest_static prev_facts facts =
620295a57106 dest/export_static: content difference;
wenzelm
parents: 26692
diff changeset
   166
  sort_wrt #1 (diff_table prev_facts facts);
620295a57106 dest/export_static: content difference;
wenzelm
parents: 26692
diff changeset
   167
620295a57106 dest/export_static: content difference;
wenzelm
parents: 26692
diff changeset
   168
fun extern_static prev_facts facts =
620295a57106 dest/export_static: content difference;
wenzelm
parents: 26692
diff changeset
   169
  sort_wrt #1 (diff_table prev_facts facts |> map (apfst (extern facts)));
26281
328fd1c551ef Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff changeset
   170
328fd1c551ef Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff changeset
   171
328fd1c551ef Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff changeset
   172
(* indexed props *)
328fd1c551ef Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff changeset
   173
29269
5c25a2012975 moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents: 28965
diff changeset
   174
val prop_ord = TermOrd.term_ord o pairself Thm.full_prop_of;
26281
328fd1c551ef Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff changeset
   175
328fd1c551ef Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff changeset
   176
fun props (Facts {props, ...}) = sort_distinct prop_ord (Net.content props);
328fd1c551ef Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff changeset
   177
fun could_unify (Facts {props, ...}) = Net.unify_term props;
328fd1c551ef Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff changeset
   178
328fd1c551ef Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff changeset
   179
26393
42febbed5460 support dynamic facts;
wenzelm
parents: 26366
diff changeset
   180
(* merge facts *)
26281
328fd1c551ef Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff changeset
   181
328fd1c551ef Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff changeset
   182
fun merge (Facts {facts = facts1, props = props1}, Facts {facts = facts2, props = props2}) =
328fd1c551ef Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff changeset
   183
  let
33095
bbd52d2f8696 renamed NameSpace to Name_Space -- also to emphasize its subtle change in semantics;
wenzelm
parents: 33093
diff changeset
   184
    val facts' = Name_Space.merge_tables (facts1, facts2);
26281
328fd1c551ef Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff changeset
   185
    val props' = Net.merge (is_equal o prop_ord) (props1, props2);
328fd1c551ef Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff changeset
   186
  in make_facts facts' props' end;
328fd1c551ef Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff changeset
   187
26393
42febbed5460 support dynamic facts;
wenzelm
parents: 26366
diff changeset
   188
26654
1f711934f221 disallow duplicate entries (weak version for merge);
wenzelm
parents: 26393
diff changeset
   189
(* add static entries *)
26393
42febbed5460 support dynamic facts;
wenzelm
parents: 26366
diff changeset
   190
33093
d010f61d3702 eliminated separate stamp -- NameSpace.define/merge etc. ensure uniqueness already;
wenzelm
parents: 29848
diff changeset
   191
local
d010f61d3702 eliminated separate stamp -- NameSpace.define/merge etc. ensure uniqueness already;
wenzelm
parents: 29848
diff changeset
   192
d010f61d3702 eliminated separate stamp -- NameSpace.define/merge etc. ensure uniqueness already;
wenzelm
parents: 29848
diff changeset
   193
fun add strict do_props naming (b, ths) (Facts {facts, props}) =
26281
328fd1c551ef Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff changeset
   194
  let
33093
d010f61d3702 eliminated separate stamp -- NameSpace.define/merge etc. ensure uniqueness already;
wenzelm
parents: 29848
diff changeset
   195
    val (name, facts') =
d010f61d3702 eliminated separate stamp -- NameSpace.define/merge etc. ensure uniqueness already;
wenzelm
parents: 29848
diff changeset
   196
      if Binding.is_empty b then ("", facts)
33095
bbd52d2f8696 renamed NameSpace to Name_Space -- also to emphasize its subtle change in semantics;
wenzelm
parents: 33093
diff changeset
   197
      else Name_Space.define strict naming (b, Static ths) facts;
26281
328fd1c551ef Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff changeset
   198
    val props' =
33093
d010f61d3702 eliminated separate stamp -- NameSpace.define/merge etc. ensure uniqueness already;
wenzelm
parents: 29848
diff changeset
   199
      if do_props
d010f61d3702 eliminated separate stamp -- NameSpace.define/merge etc. ensure uniqueness already;
wenzelm
parents: 29848
diff changeset
   200
      then fold (fn th => Net.insert_term (K false) (Thm.full_prop_of th, th)) ths props
26281
328fd1c551ef Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff changeset
   201
      else props;
28864
d6fe93e3dcb9 fact table now using name bindings
haftmann
parents: 27738
diff changeset
   202
  in (name, make_facts facts' props') end;
26281
328fd1c551ef Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff changeset
   203
33093
d010f61d3702 eliminated separate stamp -- NameSpace.define/merge etc. ensure uniqueness already;
wenzelm
parents: 29848
diff changeset
   204
in
d010f61d3702 eliminated separate stamp -- NameSpace.define/merge etc. ensure uniqueness already;
wenzelm
parents: 29848
diff changeset
   205
d010f61d3702 eliminated separate stamp -- NameSpace.define/merge etc. ensure uniqueness already;
wenzelm
parents: 29848
diff changeset
   206
val add_global = add true false;
d010f61d3702 eliminated separate stamp -- NameSpace.define/merge etc. ensure uniqueness already;
wenzelm
parents: 29848
diff changeset
   207
val add_local = add false;
d010f61d3702 eliminated separate stamp -- NameSpace.define/merge etc. ensure uniqueness already;
wenzelm
parents: 29848
diff changeset
   208
d010f61d3702 eliminated separate stamp -- NameSpace.define/merge etc. ensure uniqueness already;
wenzelm
parents: 29848
diff changeset
   209
end;
26307
27d3de85c266 replaced generic add by add_local/add_global;
wenzelm
parents: 26290
diff changeset
   210
26393
42febbed5460 support dynamic facts;
wenzelm
parents: 26366
diff changeset
   211
26654
1f711934f221 disallow duplicate entries (weak version for merge);
wenzelm
parents: 26393
diff changeset
   212
(* add dynamic entries *)
26393
42febbed5460 support dynamic facts;
wenzelm
parents: 26366
diff changeset
   213
33093
d010f61d3702 eliminated separate stamp -- NameSpace.define/merge etc. ensure uniqueness already;
wenzelm
parents: 29848
diff changeset
   214
fun add_dynamic naming (b, f) (Facts {facts, props}) =
33095
bbd52d2f8696 renamed NameSpace to Name_Space -- also to emphasize its subtle change in semantics;
wenzelm
parents: 33093
diff changeset
   215
  let val (name, facts') = Name_Space.define true naming (b, Dynamic f) facts;
33093
d010f61d3702 eliminated separate stamp -- NameSpace.define/merge etc. ensure uniqueness already;
wenzelm
parents: 29848
diff changeset
   216
  in (name, make_facts facts' props) end;
26281
328fd1c551ef Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff changeset
   217
26654
1f711934f221 disallow duplicate entries (weak version for merge);
wenzelm
parents: 26393
diff changeset
   218
1f711934f221 disallow duplicate entries (weak version for merge);
wenzelm
parents: 26393
diff changeset
   219
(* remove entries *)
1f711934f221 disallow duplicate entries (weak version for merge);
wenzelm
parents: 26393
diff changeset
   220
1f711934f221 disallow duplicate entries (weak version for merge);
wenzelm
parents: 26393
diff changeset
   221
fun del name (Facts {facts = (space, tab), props}) =
1f711934f221 disallow duplicate entries (weak version for merge);
wenzelm
parents: 26393
diff changeset
   222
  let
33163
351fc13613f2 export is_concealed;
wenzelm
parents: 33096
diff changeset
   223
    val space' = Name_Space.hide true name space handle ERROR _ => space;
26654
1f711934f221 disallow duplicate entries (weak version for merge);
wenzelm
parents: 26393
diff changeset
   224
    val tab' = Symtab.delete_safe name tab;
1f711934f221 disallow duplicate entries (weak version for merge);
wenzelm
parents: 26393
diff changeset
   225
  in make_facts (space', tab') props end;
1f711934f221 disallow duplicate entries (weak version for merge);
wenzelm
parents: 26393
diff changeset
   226
1f711934f221 disallow duplicate entries (weak version for merge);
wenzelm
parents: 26393
diff changeset
   227
fun hide fully name (Facts {facts = (space, tab), props}) =
33095
bbd52d2f8696 renamed NameSpace to Name_Space -- also to emphasize its subtle change in semantics;
wenzelm
parents: 33093
diff changeset
   228
  make_facts (Name_Space.hide fully name space, tab) props;
26654
1f711934f221 disallow duplicate entries (weak version for merge);
wenzelm
parents: 26393
diff changeset
   229
26281
328fd1c551ef Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff changeset
   230
end;