src/Pure/facts.ML
author wenzelm
Tue Feb 25 11:36:04 2014 +0100 (2014-02-25)
changeset 55740 11dd48f84441
parent 49887 1a173b2503c0
child 56003 eccac152ffb4
permissions -rw-r--r--
more positions;
tuned messages;
wenzelm@26281
     1
(*  Title:      Pure/facts.ML
wenzelm@26281
     2
    Author:     Makarius
wenzelm@26281
     3
wenzelm@26307
     4
Environment of named facts, optionally indexed by proposition.
wenzelm@26281
     5
*)
wenzelm@26281
     6
wenzelm@26281
     7
signature FACTS =
wenzelm@26281
     8
sig
wenzelm@55740
     9
  val the_single: string * Position.T -> thm list -> thm
wenzelm@26336
    10
  datatype interval = FromTo of int * int | From of int | Single of int
wenzelm@26336
    11
  datatype ref =
wenzelm@26361
    12
    Named of (string * Position.T) * interval list option |
wenzelm@26336
    13
    Fact of string
wenzelm@26361
    14
  val named: string -> ref
wenzelm@49887
    15
  val string_of_selection: interval list option -> string
wenzelm@26336
    16
  val string_of_ref: ref -> string
wenzelm@26336
    17
  val name_of_ref: ref -> string
wenzelm@26366
    18
  val pos_of_ref: ref -> Position.T
wenzelm@26336
    19
  val map_name_of_ref: (string -> string) -> ref -> ref
wenzelm@26336
    20
  val select: ref -> thm list -> thm list
wenzelm@26336
    21
  val selections: string * thm list -> (ref * thm) list
wenzelm@26281
    22
  type T
wenzelm@26393
    23
  val empty: T
wenzelm@33095
    24
  val space_of: T -> Name_Space.T
wenzelm@33163
    25
  val is_concealed: T -> string -> bool
wenzelm@26664
    26
  val intern: T -> xstring -> string
wenzelm@42358
    27
  val extern: Proof.context -> T -> string -> xstring
wenzelm@27738
    28
  val lookup: Context.generic -> T -> string -> (bool * thm list) option
wenzelm@26692
    29
  val defined: T -> string -> bool
wenzelm@26692
    30
  val fold_static: (string * thm list -> 'a -> 'a) -> T -> 'a -> 'a
wenzelm@27175
    31
  val dest_static: T list -> T -> (string * thm list) list
wenzelm@42358
    32
  val extern_static: Proof.context -> T list -> T -> (xstring * thm list) list
wenzelm@26281
    33
  val props: T -> thm list
wenzelm@26281
    34
  val could_unify: T -> term -> thm list
wenzelm@26281
    35
  val merge: T * T -> T
wenzelm@49747
    36
  val add_static: Context.generic -> {strict: bool, index: bool} ->
wenzelm@49747
    37
    binding * thm list -> T -> string * T
wenzelm@47005
    38
  val add_dynamic: Context.generic -> binding * (Context.generic -> thm list) -> T -> string * T
wenzelm@26654
    39
  val del: string -> T -> T
wenzelm@26654
    40
  val hide: bool -> string -> T -> T
wenzelm@26281
    41
end;
wenzelm@26281
    42
wenzelm@26281
    43
structure Facts: FACTS =
wenzelm@26281
    44
struct
wenzelm@26281
    45
wenzelm@26336
    46
(** fact references **)
wenzelm@26336
    47
wenzelm@26336
    48
fun the_single _ [th] : thm = th
wenzelm@55740
    49
  | the_single (name, pos) ths =
wenzelm@55740
    50
      error ("Expected singleton fact " ^ quote name ^
wenzelm@55740
    51
        " (length " ^ string_of_int (length ths) ^ ")" ^ Position.here pos);
wenzelm@26336
    52
wenzelm@26336
    53
wenzelm@26336
    54
(* datatype interval *)
wenzelm@26336
    55
wenzelm@26336
    56
datatype interval =
wenzelm@26336
    57
  FromTo of int * int |
wenzelm@26336
    58
  From of int |
wenzelm@26336
    59
  Single of int;
wenzelm@26336
    60
wenzelm@26336
    61
fun string_of_interval (FromTo (i, j)) = string_of_int i ^ "-" ^ string_of_int j
wenzelm@26336
    62
  | string_of_interval (From i) = string_of_int i ^ "-"
wenzelm@26336
    63
  | string_of_interval (Single i) = string_of_int i;
wenzelm@26336
    64
wenzelm@26336
    65
fun interval n iv =
wenzelm@26336
    66
  let fun err () = raise Fail ("Bad interval specification " ^ string_of_interval iv) in
wenzelm@26336
    67
    (case iv of
wenzelm@26336
    68
      FromTo (i, j) => if i <= j then i upto j else err ()
wenzelm@26336
    69
    | From i => if i <= n then i upto n else err ()
wenzelm@26336
    70
    | Single i => [i])
wenzelm@26336
    71
  end;
wenzelm@26336
    72
wenzelm@26336
    73
wenzelm@26336
    74
(* datatype ref *)
wenzelm@26336
    75
wenzelm@26336
    76
datatype ref =
wenzelm@26361
    77
  Named of (string * Position.T) * interval list option |
wenzelm@26336
    78
  Fact of string;
wenzelm@26336
    79
wenzelm@26361
    80
fun named name = Named ((name, Position.none), NONE);
wenzelm@26361
    81
wenzelm@55740
    82
fun name_of_ref (Named ((name, _), _)) = name
wenzelm@55740
    83
  | name_of_ref (Fact _) = raise Fail "Illegal literal fact";
wenzelm@55740
    84
wenzelm@55740
    85
fun pos_of_ref (Named ((_, pos), _)) = pos
wenzelm@55740
    86
  | pos_of_ref (Fact _) = Position.none;
wenzelm@55740
    87
wenzelm@26366
    88
fun name_pos_of_ref (Named (name_pos, _)) = name_pos
wenzelm@49887
    89
  | name_pos_of_ref (Fact _) = raise Fail "Illegal literal fact";
wenzelm@26366
    90
wenzelm@26361
    91
fun map_name_of_ref f (Named ((name, pos), is)) = Named ((f name, pos), is)
wenzelm@26336
    92
  | map_name_of_ref _ r = r;
wenzelm@26336
    93
wenzelm@49887
    94
fun string_of_selection NONE = ""
wenzelm@49887
    95
  | string_of_selection (SOME is) = enclose "(" ")" (commas (map string_of_interval is));
wenzelm@49887
    96
wenzelm@49887
    97
fun string_of_ref (Named ((name, _), sel)) = name ^ string_of_selection sel
wenzelm@49887
    98
  | string_of_ref (Fact _) = raise Fail "Illegal literal fact";
wenzelm@26336
    99
wenzelm@26336
   100
wenzelm@26336
   101
(* select *)
wenzelm@26336
   102
wenzelm@26336
   103
fun select (Fact _) ths = ths
wenzelm@26336
   104
  | select (Named (_, NONE)) ths = ths
wenzelm@26361
   105
  | select (Named ((name, pos), SOME ivs)) ths =
wenzelm@26336
   106
      let
wenzelm@26336
   107
        val n = length ths;
wenzelm@26361
   108
        fun err msg =
wenzelm@55740
   109
          error (msg ^ " for fact " ^ quote name ^ " (length " ^ string_of_int n ^ ")" ^
wenzelm@48992
   110
            Position.here pos);
wenzelm@26336
   111
        fun sel i =
wenzelm@26336
   112
          if i < 1 orelse i > n then err ("Bad subscript " ^ string_of_int i)
wenzelm@26336
   113
          else nth ths (i - 1);
wenzelm@26336
   114
        val is = maps (interval n) ivs handle Fail msg => err msg;
wenzelm@26336
   115
      in map sel is end;
wenzelm@26336
   116
wenzelm@26336
   117
wenzelm@26336
   118
(* selections *)
wenzelm@26336
   119
wenzelm@26361
   120
fun selections (name, [th]) = [(Named ((name, Position.none), NONE), th)]
wenzelm@26361
   121
  | selections (name, ths) = map2 (fn i => fn th =>
wenzelm@26361
   122
      (Named ((name, Position.none), SOME [Single i]), th)) (1 upto length ths) ths;
wenzelm@26336
   123
wenzelm@26336
   124
wenzelm@26336
   125
wenzelm@26336
   126
(** fact environment **)
wenzelm@26336
   127
wenzelm@26393
   128
(* datatypes *)
wenzelm@26393
   129
wenzelm@26393
   130
datatype fact = Static of thm list | Dynamic of Context.generic -> thm list;
wenzelm@26281
   131
wenzelm@26281
   132
datatype T = Facts of
wenzelm@33095
   133
 {facts: fact Name_Space.table,
wenzelm@26281
   134
  props: thm Net.net};
wenzelm@26281
   135
wenzelm@26281
   136
fun make_facts facts props = Facts {facts = facts, props = props};
wenzelm@33163
   137
wenzelm@33096
   138
val empty = make_facts (Name_Space.empty_table "fact") Net.empty;
wenzelm@26281
   139
wenzelm@26281
   140
wenzelm@26281
   141
(* named facts *)
wenzelm@26281
   142
wenzelm@26281
   143
fun facts_of (Facts {facts, ...}) = facts;
wenzelm@26281
   144
wenzelm@26281
   145
val space_of = #1 o facts_of;
wenzelm@26393
   146
val table_of = #2 o facts_of;
wenzelm@26393
   147
wenzelm@33163
   148
val is_concealed = Name_Space.is_concealed o space_of;
wenzelm@33163
   149
wenzelm@33095
   150
val intern = Name_Space.intern o space_of;
wenzelm@42358
   151
fun extern ctxt = Name_Space.extern ctxt o space_of;
wenzelm@26664
   152
wenzelm@26692
   153
val defined = Symtab.defined o table_of;
wenzelm@26692
   154
wenzelm@26393
   155
fun lookup context facts name =
wenzelm@26393
   156
  (case Symtab.lookup (table_of facts) name of
wenzelm@26393
   157
    NONE => NONE
wenzelm@33093
   158
  | SOME (Static ths) => SOME (true, ths)
wenzelm@33093
   159
  | SOME (Dynamic f) => SOME (false, f context));
wenzelm@26393
   160
wenzelm@33093
   161
fun fold_static f =
wenzelm@33093
   162
  Symtab.fold (fn (name, Static ths) => f (name, ths) | _ => I) o table_of;
wenzelm@26393
   163
wenzelm@27175
   164
wenzelm@27175
   165
(* content difference *)
wenzelm@27175
   166
wenzelm@27175
   167
fun diff_table prev_facts facts =
wenzelm@27175
   168
  fold_static (fn (name, ths) =>
wenzelm@27175
   169
    if exists (fn prev => defined prev name) prev_facts then I
wenzelm@27175
   170
    else cons (name, ths)) facts [];
wenzelm@27175
   171
wenzelm@27175
   172
fun dest_static prev_facts facts =
wenzelm@27175
   173
  sort_wrt #1 (diff_table prev_facts facts);
wenzelm@27175
   174
wenzelm@42358
   175
fun extern_static ctxt prev_facts facts =
wenzelm@42358
   176
  sort_wrt #1 (diff_table prev_facts facts |> map (apfst (extern ctxt facts)));
wenzelm@26281
   177
wenzelm@26281
   178
wenzelm@26281
   179
(* indexed props *)
wenzelm@26281
   180
wenzelm@35408
   181
val prop_ord = Term_Ord.term_ord o pairself Thm.full_prop_of;
wenzelm@26281
   182
wenzelm@26281
   183
fun props (Facts {props, ...}) = sort_distinct prop_ord (Net.content props);
wenzelm@26281
   184
fun could_unify (Facts {props, ...}) = Net.unify_term props;
wenzelm@26281
   185
wenzelm@26281
   186
wenzelm@26393
   187
(* merge facts *)
wenzelm@26281
   188
wenzelm@26281
   189
fun merge (Facts {facts = facts1, props = props1}, Facts {facts = facts2, props = props2}) =
wenzelm@26281
   190
  let
wenzelm@33095
   191
    val facts' = Name_Space.merge_tables (facts1, facts2);
wenzelm@26281
   192
    val props' = Net.merge (is_equal o prop_ord) (props1, props2);
wenzelm@26281
   193
  in make_facts facts' props' end;
wenzelm@26281
   194
wenzelm@26393
   195
wenzelm@26654
   196
(* add static entries *)
wenzelm@26393
   197
wenzelm@49747
   198
fun add_static context {strict, index} (b, ths) (Facts {facts, props}) =
wenzelm@26281
   199
  let
wenzelm@33093
   200
    val (name, facts') =
wenzelm@33093
   201
      if Binding.is_empty b then ("", facts)
wenzelm@47005
   202
      else Name_Space.define context strict (b, Static ths) facts;
wenzelm@49747
   203
    val props' = props
wenzelm@49747
   204
      |> index ? fold (fn th => Net.insert_term (K false) (Thm.full_prop_of th, th)) ths;
haftmann@28864
   205
  in (name, make_facts facts' props') end;
wenzelm@26281
   206
wenzelm@26393
   207
wenzelm@26654
   208
(* add dynamic entries *)
wenzelm@26393
   209
wenzelm@47005
   210
fun add_dynamic context (b, f) (Facts {facts, props}) =
wenzelm@47005
   211
  let val (name, facts') = Name_Space.define context true (b, Dynamic f) facts;
wenzelm@33093
   212
  in (name, make_facts facts' props) end;
wenzelm@26281
   213
wenzelm@26654
   214
wenzelm@26654
   215
(* remove entries *)
wenzelm@26654
   216
wenzelm@26654
   217
fun del name (Facts {facts = (space, tab), props}) =
wenzelm@26654
   218
  let
wenzelm@33163
   219
    val space' = Name_Space.hide true name space handle ERROR _ => space;
wenzelm@26654
   220
    val tab' = Symtab.delete_safe name tab;
wenzelm@26654
   221
  in make_facts (space', tab') props end;
wenzelm@26654
   222
wenzelm@26654
   223
fun hide fully name (Facts {facts = (space, tab), props}) =
wenzelm@33095
   224
  make_facts (Name_Space.hide fully name space, tab) props;
wenzelm@26654
   225
wenzelm@26281
   226
end;