src/Pure/facts.ML
author wenzelm
Thu, 13 Mar 2014 12:28:35 +0100
changeset 56137 af71fb1cb31f
parent 56025 d74fed45fa8b
child 56140 ed92ce2ac88e
permissions -rw-r--r--
minor tuning -- NB: props are usually empty for global facts;
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
55740
11dd48f84441 more positions;
wenzelm
parents: 49887
diff changeset
     9
  val the_single: string * Position.T -> thm list -> thm
26336
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
49887
1a173b2503c0 tuned signature;
wenzelm
parents: 49747
diff changeset
    15
  val string_of_selection: interval list option -> string
26336
a0e2b706ce73 renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents: 26307
diff changeset
    16
  val string_of_ref: ref -> string
a0e2b706ce73 renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents: 26307
diff changeset
    17
  val name_of_ref: ref -> string
26366
5c089f4219c2 added pos_of_ref;
wenzelm
parents: 26361
diff changeset
    18
  val pos_of_ref: ref -> Position.T
26336
a0e2b706ce73 renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents: 26307
diff changeset
    19
  val map_name_of_ref: (string -> string) -> ref -> ref
a0e2b706ce73 renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents: 26307
diff changeset
    20
  val select: ref -> thm list -> thm list
a0e2b706ce73 renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents: 26307
diff changeset
    21
  val selections: string * thm list -> (ref * thm) list
26281
328fd1c551ef Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff changeset
    22
  type T
26393
42febbed5460 support dynamic facts;
wenzelm
parents: 26366
diff changeset
    23
  val empty: T
33095
bbd52d2f8696 renamed NameSpace to Name_Space -- also to emphasize its subtle change in semantics;
wenzelm
parents: 33093
diff changeset
    24
  val space_of: T -> Name_Space.T
33163
351fc13613f2 export is_concealed;
wenzelm
parents: 33096
diff changeset
    25
  val is_concealed: T -> string -> bool
56003
eccac152ffb4 check fact names with PIDE markup;
wenzelm
parents: 55740
diff changeset
    26
  val check: Context.generic -> T -> xstring * Position.T -> string
26664
167d879a89b0 renamed dest to dest_table, and extern to extern table;
wenzelm
parents: 26654
diff changeset
    27
  val intern: T -> xstring -> string
42358
b47d41d9f4b5 Name_Space: proper configuration options long_names, short_names, unique_names instead of former unsynchronized references;
wenzelm
parents: 35408
diff changeset
    28
  val extern: Proof.context -> T -> string -> xstring
27738
66596d7aa899 Facts.lookup: return static/dynamic status;
wenzelm
parents: 27175
diff changeset
    29
  val lookup: Context.generic -> T -> string -> (bool * thm list) option
26692
3f48d4f4229f removed unused space_of;
wenzelm
parents: 26664
diff changeset
    30
  val defined: T -> string -> bool
3f48d4f4229f removed unused space_of;
wenzelm
parents: 26664
diff changeset
    31
  val fold_static: (string * thm list -> 'a -> 'a) -> T -> 'a -> 'a
27175
620295a57106 dest/export_static: content difference;
wenzelm
parents: 26692
diff changeset
    32
  val dest_static: T list -> T -> (string * thm list) list
42358
b47d41d9f4b5 Name_Space: proper configuration options long_names, short_names, unique_names instead of former unsynchronized references;
wenzelm
parents: 35408
diff changeset
    33
  val extern_static: Proof.context -> T list -> T -> (xstring * thm list) list
26281
328fd1c551ef Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff changeset
    34
  val props: T -> thm list
328fd1c551ef Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff changeset
    35
  val could_unify: T -> term -> thm list
328fd1c551ef Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff changeset
    36
  val merge: T * T -> T
49747
2cf86639b77e more explicit flags for facts table;
wenzelm
parents: 48992
diff changeset
    37
  val add_static: Context.generic -> {strict: bool, index: bool} ->
2cf86639b77e more explicit flags for facts table;
wenzelm
parents: 48992
diff changeset
    38
    binding * thm list -> T -> string * T
47005
421760a1efe7 maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
wenzelm
parents: 42375
diff changeset
    39
  val add_dynamic: Context.generic -> binding * (Context.generic -> thm list) -> T -> string * T
26654
1f711934f221 disallow duplicate entries (weak version for merge);
wenzelm
parents: 26393
diff changeset
    40
  val del: string -> T -> T
1f711934f221 disallow duplicate entries (weak version for merge);
wenzelm
parents: 26393
diff changeset
    41
  val hide: bool -> string -> T -> T
26281
328fd1c551ef Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff changeset
    42
end;
328fd1c551ef Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff changeset
    43
328fd1c551ef Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff changeset
    44
structure Facts: FACTS =
328fd1c551ef Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff changeset
    45
struct
328fd1c551ef Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff changeset
    46
26336
a0e2b706ce73 renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents: 26307
diff changeset
    47
(** fact references **)
a0e2b706ce73 renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents: 26307
diff changeset
    48
a0e2b706ce73 renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents: 26307
diff changeset
    49
fun the_single _ [th] : thm = th
55740
11dd48f84441 more positions;
wenzelm
parents: 49887
diff changeset
    50
  | the_single (name, pos) ths =
11dd48f84441 more positions;
wenzelm
parents: 49887
diff changeset
    51
      error ("Expected singleton fact " ^ quote name ^
11dd48f84441 more positions;
wenzelm
parents: 49887
diff changeset
    52
        " (length " ^ string_of_int (length ths) ^ ")" ^ Position.here pos);
26336
a0e2b706ce73 renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents: 26307
diff changeset
    53
a0e2b706ce73 renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents: 26307
diff changeset
    54
a0e2b706ce73 renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents: 26307
diff changeset
    55
(* datatype interval *)
a0e2b706ce73 renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents: 26307
diff changeset
    56
a0e2b706ce73 renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents: 26307
diff changeset
    57
datatype interval =
a0e2b706ce73 renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents: 26307
diff changeset
    58
  FromTo of int * int |
a0e2b706ce73 renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents: 26307
diff changeset
    59
  From of int |
a0e2b706ce73 renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents: 26307
diff changeset
    60
  Single of int;
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 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
    63
  | string_of_interval (From i) = string_of_int i ^ "-"
a0e2b706ce73 renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents: 26307
diff changeset
    64
  | string_of_interval (Single i) = string_of_int i;
a0e2b706ce73 renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents: 26307
diff changeset
    65
a0e2b706ce73 renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents: 26307
diff changeset
    66
fun interval n iv =
a0e2b706ce73 renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents: 26307
diff changeset
    67
  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
    68
    (case iv of
a0e2b706ce73 renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents: 26307
diff changeset
    69
      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
    70
    | 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
    71
    | Single i => [i])
a0e2b706ce73 renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents: 26307
diff changeset
    72
  end;
a0e2b706ce73 renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents: 26307
diff changeset
    73
a0e2b706ce73 renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents: 26307
diff changeset
    74
a0e2b706ce73 renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents: 26307
diff changeset
    75
(* datatype ref *)
a0e2b706ce73 renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents: 26307
diff changeset
    76
a0e2b706ce73 renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents: 26307
diff changeset
    77
datatype ref =
26361
7946f459c6c8 Facts.Named: include position;
wenzelm
parents: 26336
diff changeset
    78
  Named of (string * Position.T) * interval list option |
26336
a0e2b706ce73 renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents: 26307
diff changeset
    79
  Fact of string;
a0e2b706ce73 renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents: 26307
diff changeset
    80
26361
7946f459c6c8 Facts.Named: include position;
wenzelm
parents: 26336
diff changeset
    81
fun named name = Named ((name, Position.none), NONE);
7946f459c6c8 Facts.Named: include position;
wenzelm
parents: 26336
diff changeset
    82
55740
11dd48f84441 more positions;
wenzelm
parents: 49887
diff changeset
    83
fun name_of_ref (Named ((name, _), _)) = name
11dd48f84441 more positions;
wenzelm
parents: 49887
diff changeset
    84
  | name_of_ref (Fact _) = raise Fail "Illegal literal fact";
11dd48f84441 more positions;
wenzelm
parents: 49887
diff changeset
    85
11dd48f84441 more positions;
wenzelm
parents: 49887
diff changeset
    86
fun pos_of_ref (Named ((_, pos), _)) = pos
11dd48f84441 more positions;
wenzelm
parents: 49887
diff changeset
    87
  | pos_of_ref (Fact _) = Position.none;
11dd48f84441 more positions;
wenzelm
parents: 49887
diff changeset
    88
26361
7946f459c6c8 Facts.Named: include position;
wenzelm
parents: 26336
diff changeset
    89
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
    90
  | map_name_of_ref _ r = r;
a0e2b706ce73 renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents: 26307
diff changeset
    91
49887
1a173b2503c0 tuned signature;
wenzelm
parents: 49747
diff changeset
    92
fun string_of_selection NONE = ""
1a173b2503c0 tuned signature;
wenzelm
parents: 49747
diff changeset
    93
  | string_of_selection (SOME is) = enclose "(" ")" (commas (map string_of_interval is));
1a173b2503c0 tuned signature;
wenzelm
parents: 49747
diff changeset
    94
1a173b2503c0 tuned signature;
wenzelm
parents: 49747
diff changeset
    95
fun string_of_ref (Named ((name, _), sel)) = name ^ string_of_selection sel
1a173b2503c0 tuned signature;
wenzelm
parents: 49747
diff changeset
    96
  | string_of_ref (Fact _) = raise Fail "Illegal literal fact";
26336
a0e2b706ce73 renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents: 26307
diff changeset
    97
a0e2b706ce73 renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents: 26307
diff changeset
    98
a0e2b706ce73 renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents: 26307
diff changeset
    99
(* select *)
a0e2b706ce73 renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents: 26307
diff changeset
   100
a0e2b706ce73 renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents: 26307
diff changeset
   101
fun select (Fact _) ths = ths
a0e2b706ce73 renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents: 26307
diff changeset
   102
  | select (Named (_, NONE)) ths = ths
26361
7946f459c6c8 Facts.Named: include position;
wenzelm
parents: 26336
diff changeset
   103
  | select (Named ((name, pos), SOME ivs)) ths =
26336
a0e2b706ce73 renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents: 26307
diff changeset
   104
      let
a0e2b706ce73 renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents: 26307
diff changeset
   105
        val n = length ths;
26361
7946f459c6c8 Facts.Named: include position;
wenzelm
parents: 26336
diff changeset
   106
        fun err msg =
55740
11dd48f84441 more positions;
wenzelm
parents: 49887
diff changeset
   107
          error (msg ^ " for fact " ^ quote name ^ " (length " ^ string_of_int n ^ ")" ^
48992
0518bf89c777 renamed Position.str_of to Position.here;
wenzelm
parents: 47005
diff changeset
   108
            Position.here pos);
26336
a0e2b706ce73 renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents: 26307
diff changeset
   109
        fun sel i =
a0e2b706ce73 renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents: 26307
diff changeset
   110
          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
   111
          else nth ths (i - 1);
a0e2b706ce73 renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents: 26307
diff changeset
   112
        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
   113
      in map sel is end;
a0e2b706ce73 renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents: 26307
diff changeset
   114
a0e2b706ce73 renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents: 26307
diff changeset
   115
a0e2b706ce73 renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents: 26307
diff changeset
   116
(* selections *)
a0e2b706ce73 renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents: 26307
diff changeset
   117
26361
7946f459c6c8 Facts.Named: include position;
wenzelm
parents: 26336
diff changeset
   118
fun selections (name, [th]) = [(Named ((name, Position.none), NONE), th)]
7946f459c6c8 Facts.Named: include position;
wenzelm
parents: 26336
diff changeset
   119
  | selections (name, ths) = map2 (fn i => fn th =>
7946f459c6c8 Facts.Named: include position;
wenzelm
parents: 26336
diff changeset
   120
      (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
   121
a0e2b706ce73 renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents: 26307
diff changeset
   122
a0e2b706ce73 renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents: 26307
diff changeset
   123
a0e2b706ce73 renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents: 26307
diff changeset
   124
(** fact environment **)
a0e2b706ce73 renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents: 26307
diff changeset
   125
26393
42febbed5460 support dynamic facts;
wenzelm
parents: 26366
diff changeset
   126
(* datatypes *)
42febbed5460 support dynamic facts;
wenzelm
parents: 26366
diff changeset
   127
42febbed5460 support dynamic facts;
wenzelm
parents: 26366
diff changeset
   128
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
   129
328fd1c551ef Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff changeset
   130
datatype T = Facts of
33095
bbd52d2f8696 renamed NameSpace to Name_Space -- also to emphasize its subtle change in semantics;
wenzelm
parents: 33093
diff changeset
   131
 {facts: fact Name_Space.table,
26281
328fd1c551ef Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff changeset
   132
  props: thm Net.net};
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
fun make_facts facts props = Facts {facts = facts, props = props};
33163
351fc13613f2 export is_concealed;
wenzelm
parents: 33096
diff changeset
   135
33096
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
   136
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
   137
328fd1c551ef Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff changeset
   138
328fd1c551ef Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff changeset
   139
(* named facts *)
328fd1c551ef Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff changeset
   140
328fd1c551ef Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff changeset
   141
fun facts_of (Facts {facts, ...}) = facts;
328fd1c551ef Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff changeset
   142
56025
d74fed45fa8b abstract type Name_Space.table;
wenzelm
parents: 56004
diff changeset
   143
val space_of = Name_Space.space_of_table o facts_of;
26393
42febbed5460 support dynamic facts;
wenzelm
parents: 26366
diff changeset
   144
33163
351fc13613f2 export is_concealed;
wenzelm
parents: 33096
diff changeset
   145
val is_concealed = Name_Space.is_concealed o space_of;
351fc13613f2 export is_concealed;
wenzelm
parents: 33096
diff changeset
   146
56003
eccac152ffb4 check fact names with PIDE markup;
wenzelm
parents: 55740
diff changeset
   147
fun check context facts (xname, pos) =
eccac152ffb4 check fact names with PIDE markup;
wenzelm
parents: 55740
diff changeset
   148
  let
eccac152ffb4 check fact names with PIDE markup;
wenzelm
parents: 55740
diff changeset
   149
    val (name, fact) = Name_Space.check context (facts_of facts) (xname, pos);
eccac152ffb4 check fact names with PIDE markup;
wenzelm
parents: 55740
diff changeset
   150
    val _ =
eccac152ffb4 check fact names with PIDE markup;
wenzelm
parents: 55740
diff changeset
   151
      (case fact of
eccac152ffb4 check fact names with PIDE markup;
wenzelm
parents: 55740
diff changeset
   152
        Static _ => ()
eccac152ffb4 check fact names with PIDE markup;
wenzelm
parents: 55740
diff changeset
   153
      | Dynamic _ => Context_Position.report_generic context pos (Markup.dynamic_fact name));
eccac152ffb4 check fact names with PIDE markup;
wenzelm
parents: 55740
diff changeset
   154
  in name end;
eccac152ffb4 check fact names with PIDE markup;
wenzelm
parents: 55740
diff changeset
   155
33095
bbd52d2f8696 renamed NameSpace to Name_Space -- also to emphasize its subtle change in semantics;
wenzelm
parents: 33093
diff changeset
   156
val intern = Name_Space.intern o space_of;
42358
b47d41d9f4b5 Name_Space: proper configuration options long_names, short_names, unique_names instead of former unsynchronized references;
wenzelm
parents: 35408
diff changeset
   157
fun extern ctxt = Name_Space.extern ctxt o space_of;
26664
167d879a89b0 renamed dest to dest_table, and extern to extern table;
wenzelm
parents: 26654
diff changeset
   158
56025
d74fed45fa8b abstract type Name_Space.table;
wenzelm
parents: 56004
diff changeset
   159
val defined = is_some oo (Name_Space.lookup_key o facts_of);
26692
3f48d4f4229f removed unused space_of;
wenzelm
parents: 26664
diff changeset
   160
26393
42febbed5460 support dynamic facts;
wenzelm
parents: 26366
diff changeset
   161
fun lookup context facts name =
56025
d74fed45fa8b abstract type Name_Space.table;
wenzelm
parents: 56004
diff changeset
   162
  (case Name_Space.lookup_key (facts_of facts) name of
26393
42febbed5460 support dynamic facts;
wenzelm
parents: 26366
diff changeset
   163
    NONE => NONE
56025
d74fed45fa8b abstract type Name_Space.table;
wenzelm
parents: 56004
diff changeset
   164
  | SOME (_, Static ths) => SOME (true, ths)
d74fed45fa8b abstract type Name_Space.table;
wenzelm
parents: 56004
diff changeset
   165
  | SOME (_, Dynamic f) => SOME (false, f context));
26393
42febbed5460 support dynamic facts;
wenzelm
parents: 26366
diff changeset
   166
33093
d010f61d3702 eliminated separate stamp -- NameSpace.define/merge etc. ensure uniqueness already;
wenzelm
parents: 29848
diff changeset
   167
fun fold_static f =
56025
d74fed45fa8b abstract type Name_Space.table;
wenzelm
parents: 56004
diff changeset
   168
  Name_Space.fold_table (fn (name, Static ths) => f (name, ths) | _ => I) o facts_of;
26393
42febbed5460 support dynamic facts;
wenzelm
parents: 26366
diff changeset
   169
27175
620295a57106 dest/export_static: content difference;
wenzelm
parents: 26692
diff changeset
   170
620295a57106 dest/export_static: content difference;
wenzelm
parents: 26692
diff changeset
   171
(* content difference *)
620295a57106 dest/export_static: content difference;
wenzelm
parents: 26692
diff changeset
   172
620295a57106 dest/export_static: content difference;
wenzelm
parents: 26692
diff changeset
   173
fun diff_table prev_facts facts =
620295a57106 dest/export_static: content difference;
wenzelm
parents: 26692
diff changeset
   174
  fold_static (fn (name, ths) =>
620295a57106 dest/export_static: content difference;
wenzelm
parents: 26692
diff changeset
   175
    if exists (fn prev => defined prev name) prev_facts then I
620295a57106 dest/export_static: content difference;
wenzelm
parents: 26692
diff changeset
   176
    else cons (name, ths)) facts [];
620295a57106 dest/export_static: content difference;
wenzelm
parents: 26692
diff changeset
   177
620295a57106 dest/export_static: content difference;
wenzelm
parents: 26692
diff changeset
   178
fun dest_static prev_facts facts =
620295a57106 dest/export_static: content difference;
wenzelm
parents: 26692
diff changeset
   179
  sort_wrt #1 (diff_table prev_facts facts);
620295a57106 dest/export_static: content difference;
wenzelm
parents: 26692
diff changeset
   180
42358
b47d41d9f4b5 Name_Space: proper configuration options long_names, short_names, unique_names instead of former unsynchronized references;
wenzelm
parents: 35408
diff changeset
   181
fun extern_static ctxt prev_facts facts =
b47d41d9f4b5 Name_Space: proper configuration options long_names, short_names, unique_names instead of former unsynchronized references;
wenzelm
parents: 35408
diff changeset
   182
  sort_wrt #1 (diff_table prev_facts facts |> map (apfst (extern ctxt facts)));
26281
328fd1c551ef Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff changeset
   183
328fd1c551ef Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff changeset
   184
328fd1c551ef Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff changeset
   185
(* indexed props *)
328fd1c551ef Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff changeset
   186
35408
b48ab741683b modernized structure Term_Ord;
wenzelm
parents: 33163
diff changeset
   187
val prop_ord = Term_Ord.term_ord o pairself Thm.full_prop_of;
26281
328fd1c551ef Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff changeset
   188
328fd1c551ef Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff changeset
   189
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
   190
fun could_unify (Facts {props, ...}) = Net.unify_term props;
328fd1c551ef Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff changeset
   191
328fd1c551ef Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff changeset
   192
26393
42febbed5460 support dynamic facts;
wenzelm
parents: 26366
diff changeset
   193
(* merge facts *)
26281
328fd1c551ef Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff changeset
   194
328fd1c551ef Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff changeset
   195
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
   196
  let
33095
bbd52d2f8696 renamed NameSpace to Name_Space -- also to emphasize its subtle change in semantics;
wenzelm
parents: 33093
diff changeset
   197
    val facts' = Name_Space.merge_tables (facts1, facts2);
56137
af71fb1cb31f minor tuning -- NB: props are usually empty for global facts;
wenzelm
parents: 56025
diff changeset
   198
    val props' =
af71fb1cb31f minor tuning -- NB: props are usually empty for global facts;
wenzelm
parents: 56025
diff changeset
   199
      if Net.is_empty props2 then props1
af71fb1cb31f minor tuning -- NB: props are usually empty for global facts;
wenzelm
parents: 56025
diff changeset
   200
      else if Net.is_empty props1 then props2
af71fb1cb31f minor tuning -- NB: props are usually empty for global facts;
wenzelm
parents: 56025
diff changeset
   201
      else Net.merge (is_equal o prop_ord) (props1, props2);  (*beware of non-canonical merge*)
26281
328fd1c551ef Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff changeset
   202
  in make_facts facts' props' end;
328fd1c551ef Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff changeset
   203
26393
42febbed5460 support dynamic facts;
wenzelm
parents: 26366
diff changeset
   204
26654
1f711934f221 disallow duplicate entries (weak version for merge);
wenzelm
parents: 26393
diff changeset
   205
(* add static entries *)
26393
42febbed5460 support dynamic facts;
wenzelm
parents: 26366
diff changeset
   206
49747
2cf86639b77e more explicit flags for facts table;
wenzelm
parents: 48992
diff changeset
   207
fun add_static context {strict, index} (b, ths) (Facts {facts, props}) =
26281
328fd1c551ef Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff changeset
   208
  let
33093
d010f61d3702 eliminated separate stamp -- NameSpace.define/merge etc. ensure uniqueness already;
wenzelm
parents: 29848
diff changeset
   209
    val (name, facts') =
d010f61d3702 eliminated separate stamp -- NameSpace.define/merge etc. ensure uniqueness already;
wenzelm
parents: 29848
diff changeset
   210
      if Binding.is_empty b then ("", facts)
47005
421760a1efe7 maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
wenzelm
parents: 42375
diff changeset
   211
      else Name_Space.define context strict (b, Static ths) facts;
49747
2cf86639b77e more explicit flags for facts table;
wenzelm
parents: 48992
diff changeset
   212
    val props' = props
2cf86639b77e more explicit flags for facts table;
wenzelm
parents: 48992
diff changeset
   213
      |> index ? fold (fn th => Net.insert_term (K false) (Thm.full_prop_of th, th)) ths;
28864
d6fe93e3dcb9 fact table now using name bindings
haftmann
parents: 27738
diff changeset
   214
  in (name, make_facts facts' props') end;
26281
328fd1c551ef Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff changeset
   215
26393
42febbed5460 support dynamic facts;
wenzelm
parents: 26366
diff changeset
   216
26654
1f711934f221 disallow duplicate entries (weak version for merge);
wenzelm
parents: 26393
diff changeset
   217
(* add dynamic entries *)
26393
42febbed5460 support dynamic facts;
wenzelm
parents: 26366
diff changeset
   218
47005
421760a1efe7 maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
wenzelm
parents: 42375
diff changeset
   219
fun add_dynamic context (b, f) (Facts {facts, props}) =
421760a1efe7 maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
wenzelm
parents: 42375
diff changeset
   220
  let val (name, facts') = Name_Space.define context true (b, Dynamic f) facts;
33093
d010f61d3702 eliminated separate stamp -- NameSpace.define/merge etc. ensure uniqueness already;
wenzelm
parents: 29848
diff changeset
   221
  in (name, make_facts facts' props) end;
26281
328fd1c551ef Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff changeset
   222
26654
1f711934f221 disallow duplicate entries (weak version for merge);
wenzelm
parents: 26393
diff changeset
   223
1f711934f221 disallow duplicate entries (weak version for merge);
wenzelm
parents: 26393
diff changeset
   224
(* remove entries *)
1f711934f221 disallow duplicate entries (weak version for merge);
wenzelm
parents: 26393
diff changeset
   225
56025
d74fed45fa8b abstract type Name_Space.table;
wenzelm
parents: 56004
diff changeset
   226
fun del name (Facts {facts, props}) =
d74fed45fa8b abstract type Name_Space.table;
wenzelm
parents: 56004
diff changeset
   227
  make_facts (Name_Space.del_table name facts) props;
26654
1f711934f221 disallow duplicate entries (weak version for merge);
wenzelm
parents: 26393
diff changeset
   228
56025
d74fed45fa8b abstract type Name_Space.table;
wenzelm
parents: 56004
diff changeset
   229
fun hide fully name (Facts {facts, props}) =
d74fed45fa8b abstract type Name_Space.table;
wenzelm
parents: 56004
diff changeset
   230
  make_facts (Name_Space.hide_table fully name facts) props;
26654
1f711934f221 disallow duplicate entries (weak version for merge);
wenzelm
parents: 26393
diff changeset
   231
26281
328fd1c551ef Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff changeset
   232
end;