src/Pure/facts.ML
author wenzelm
Thu Aug 15 16:02:47 2019 +0200 (9 months ago)
changeset 70533 031620901fcd
parent 68698 6ee53660a911
child 70545 b93ba98e627a
permissions -rw-r--r--
support for (fully reconstructed) proof terms in Scala;
proper cache_typs;
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@57887
    25
  val alias: Name_Space.naming -> binding -> string -> T -> T
wenzelm@33163
    26
  val is_concealed: T -> string -> bool
wenzelm@56003
    27
  val check: Context.generic -> T -> xstring * Position.T -> string
wenzelm@26664
    28
  val intern: T -> xstring -> string
wenzelm@42358
    29
  val extern: Proof.context -> T -> string -> xstring
wenzelm@56140
    30
  val markup_extern: Proof.context -> T -> string -> Markup.T * xstring
wenzelm@63080
    31
  val defined: T -> string -> bool
wenzelm@63080
    32
  val is_dynamic: T -> string -> bool
wenzelm@63255
    33
  val lookup: Context.generic -> T -> string -> {dynamic: bool, thms: thm list} option
wenzelm@57942
    34
  val retrieve: Context.generic -> T -> xstring * Position.T ->
wenzelm@63255
    35
    {name: string, dynamic: bool, thms: thm list}
wenzelm@26692
    36
  val fold_static: (string * thm list -> 'a -> 'a) -> T -> 'a -> 'a
wenzelm@56158
    37
  val dest_static: bool -> T list -> T -> (string * thm list) list
wenzelm@63080
    38
  val dest_all: Context.generic -> bool -> T list -> T -> (string * thm list) list
wenzelm@63337
    39
  val props: T -> (thm * Position.T) list
wenzelm@63337
    40
  val could_unify: T -> term -> (thm * Position.T) list
wenzelm@26281
    41
  val merge: T * T -> T
wenzelm@49747
    42
  val add_static: Context.generic -> {strict: bool, index: bool} ->
wenzelm@67662
    43
    binding * thm list lazy -> T -> string * T
wenzelm@47005
    44
  val add_dynamic: Context.generic -> binding * (Context.generic -> thm list) -> T -> string * T
wenzelm@26654
    45
  val del: string -> T -> T
wenzelm@26654
    46
  val hide: bool -> string -> T -> T
wenzelm@26281
    47
end;
wenzelm@26281
    48
wenzelm@26281
    49
structure Facts: FACTS =
wenzelm@26281
    50
struct
wenzelm@26281
    51
wenzelm@26336
    52
(** fact references **)
wenzelm@26336
    53
wenzelm@26336
    54
fun the_single _ [th] : thm = th
wenzelm@55740
    55
  | the_single (name, pos) ths =
wenzelm@55740
    56
      error ("Expected singleton fact " ^ quote name ^
wenzelm@55740
    57
        " (length " ^ string_of_int (length ths) ^ ")" ^ Position.here pos);
wenzelm@26336
    58
wenzelm@26336
    59
wenzelm@26336
    60
(* datatype interval *)
wenzelm@26336
    61
wenzelm@26336
    62
datatype interval =
wenzelm@26336
    63
  FromTo of int * int |
wenzelm@26336
    64
  From of int |
wenzelm@26336
    65
  Single of int;
wenzelm@26336
    66
wenzelm@26336
    67
fun string_of_interval (FromTo (i, j)) = string_of_int i ^ "-" ^ string_of_int j
wenzelm@26336
    68
  | string_of_interval (From i) = string_of_int i ^ "-"
wenzelm@26336
    69
  | string_of_interval (Single i) = string_of_int i;
wenzelm@26336
    70
wenzelm@26336
    71
fun interval n iv =
wenzelm@26336
    72
  let fun err () = raise Fail ("Bad interval specification " ^ string_of_interval iv) in
wenzelm@26336
    73
    (case iv of
wenzelm@26336
    74
      FromTo (i, j) => if i <= j then i upto j else err ()
wenzelm@26336
    75
    | From i => if i <= n then i upto n else err ()
wenzelm@26336
    76
    | Single i => [i])
wenzelm@26336
    77
  end;
wenzelm@26336
    78
wenzelm@26336
    79
wenzelm@26336
    80
(* datatype ref *)
wenzelm@26336
    81
wenzelm@26336
    82
datatype ref =
wenzelm@26361
    83
  Named of (string * Position.T) * interval list option |
wenzelm@26336
    84
  Fact of string;
wenzelm@26336
    85
wenzelm@26361
    86
fun named name = Named ((name, Position.none), NONE);
wenzelm@26361
    87
wenzelm@55740
    88
fun name_of_ref (Named ((name, _), _)) = name
wenzelm@55740
    89
  | name_of_ref (Fact _) = raise Fail "Illegal literal fact";
wenzelm@55740
    90
wenzelm@55740
    91
fun pos_of_ref (Named ((_, pos), _)) = pos
wenzelm@55740
    92
  | pos_of_ref (Fact _) = Position.none;
wenzelm@55740
    93
wenzelm@26361
    94
fun map_name_of_ref f (Named ((name, pos), is)) = Named ((f name, pos), is)
wenzelm@26336
    95
  | map_name_of_ref _ r = r;
wenzelm@26336
    96
wenzelm@49887
    97
fun string_of_selection NONE = ""
wenzelm@49887
    98
  | string_of_selection (SOME is) = enclose "(" ")" (commas (map string_of_interval is));
wenzelm@49887
    99
wenzelm@49887
   100
fun string_of_ref (Named ((name, _), sel)) = name ^ string_of_selection sel
wenzelm@49887
   101
  | string_of_ref (Fact _) = raise Fail "Illegal literal fact";
wenzelm@26336
   102
wenzelm@26336
   103
wenzelm@26336
   104
(* select *)
wenzelm@26336
   105
wenzelm@26336
   106
fun select (Fact _) ths = ths
wenzelm@26336
   107
  | select (Named (_, NONE)) ths = ths
wenzelm@26361
   108
  | select (Named ((name, pos), SOME ivs)) ths =
wenzelm@26336
   109
      let
wenzelm@26336
   110
        val n = length ths;
wenzelm@26361
   111
        fun err msg =
wenzelm@55740
   112
          error (msg ^ " for fact " ^ quote name ^ " (length " ^ string_of_int n ^ ")" ^
wenzelm@48992
   113
            Position.here pos);
wenzelm@26336
   114
        fun sel i =
wenzelm@26336
   115
          if i < 1 orelse i > n then err ("Bad subscript " ^ string_of_int i)
wenzelm@26336
   116
          else nth ths (i - 1);
wenzelm@26336
   117
        val is = maps (interval n) ivs handle Fail msg => err msg;
wenzelm@26336
   118
      in map sel is end;
wenzelm@26336
   119
wenzelm@26336
   120
wenzelm@26336
   121
(* selections *)
wenzelm@26336
   122
wenzelm@26361
   123
fun selections (name, [th]) = [(Named ((name, Position.none), NONE), th)]
wenzelm@26361
   124
  | selections (name, ths) = map2 (fn i => fn th =>
wenzelm@26361
   125
      (Named ((name, Position.none), SOME [Single i]), th)) (1 upto length ths) ths;
wenzelm@26336
   126
wenzelm@26336
   127
wenzelm@26336
   128
wenzelm@26336
   129
(** fact environment **)
wenzelm@26336
   130
wenzelm@26393
   131
(* datatypes *)
wenzelm@26393
   132
wenzelm@67662
   133
datatype fact = Static of thm list lazy | Dynamic of Context.generic -> thm list;
wenzelm@26281
   134
wenzelm@26281
   135
datatype T = Facts of
wenzelm@33095
   136
 {facts: fact Name_Space.table,
wenzelm@63337
   137
  props: (thm * Position.T) Net.net};
wenzelm@26281
   138
wenzelm@26281
   139
fun make_facts facts props = Facts {facts = facts, props = props};
wenzelm@33163
   140
wenzelm@33096
   141
val empty = make_facts (Name_Space.empty_table "fact") Net.empty;
wenzelm@26281
   142
wenzelm@26281
   143
wenzelm@26281
   144
(* named facts *)
wenzelm@26281
   145
wenzelm@26281
   146
fun facts_of (Facts {facts, ...}) = facts;
wenzelm@26281
   147
wenzelm@56025
   148
val space_of = Name_Space.space_of_table o facts_of;
wenzelm@26393
   149
wenzelm@57887
   150
fun alias naming binding name (Facts {facts, props}) =
wenzelm@57887
   151
  make_facts (Name_Space.alias_table naming binding name facts) props;
wenzelm@57887
   152
wenzelm@33163
   153
val is_concealed = Name_Space.is_concealed o space_of;
wenzelm@33163
   154
wenzelm@56003
   155
fun check context facts (xname, pos) =
wenzelm@56003
   156
  let
wenzelm@56003
   157
    val (name, fact) = Name_Space.check context (facts_of facts) (xname, pos);
wenzelm@56003
   158
    val _ =
wenzelm@56003
   159
      (case fact of
wenzelm@56003
   160
        Static _ => ()
wenzelm@56003
   161
      | Dynamic _ => Context_Position.report_generic context pos (Markup.dynamic_fact name));
wenzelm@56003
   162
  in name end;
wenzelm@56003
   163
wenzelm@33095
   164
val intern = Name_Space.intern o space_of;
wenzelm@42358
   165
fun extern ctxt = Name_Space.extern ctxt o space_of;
wenzelm@57887
   166
fun markup_extern ctxt = Name_Space.markup_extern ctxt o space_of;
wenzelm@26664
   167
wenzelm@56158
   168
wenzelm@56158
   169
(* retrieve *)
wenzelm@56158
   170
wenzelm@59883
   171
val defined = Name_Space.defined o facts_of;
wenzelm@26692
   172
wenzelm@63080
   173
fun is_dynamic facts name =
wenzelm@63080
   174
  (case Name_Space.lookup (facts_of facts) name of
wenzelm@63080
   175
    SOME (Dynamic _) => true
wenzelm@63080
   176
  | _ => false);
wenzelm@63080
   177
wenzelm@26393
   178
fun lookup context facts name =
wenzelm@59884
   179
  (case Name_Space.lookup (facts_of facts) name of
wenzelm@26393
   180
    NONE => NONE
wenzelm@67662
   181
  | SOME (Static ths) => SOME {dynamic = false, thms = Lazy.force ths}
wenzelm@63255
   182
  | SOME (Dynamic f) => SOME {dynamic = true, thms = f context});
wenzelm@26393
   183
wenzelm@56140
   184
fun retrieve context facts (xname, pos) =
wenzelm@56140
   185
  let
wenzelm@56140
   186
    val name = check context facts (xname, pos);
wenzelm@63255
   187
    val {dynamic, thms} =
wenzelm@56140
   188
      (case lookup context facts name of
wenzelm@63255
   189
        SOME res =>
wenzelm@63255
   190
          (if #dynamic res
wenzelm@63255
   191
           then Context_Position.report_generic context pos (Markup.dynamic_fact name)
wenzelm@63255
   192
           else ();
wenzelm@63255
   193
           res)
wenzelm@56140
   194
      | NONE => error ("Unknown fact " ^ quote name ^ Position.here pos));
wenzelm@57942
   195
  in
wenzelm@57942
   196
   {name = name,
wenzelm@63255
   197
    dynamic = dynamic,
wenzelm@67649
   198
    thms = map (Thm.transfer'' context) thms}
wenzelm@57942
   199
  end;
wenzelm@56140
   200
wenzelm@56158
   201
wenzelm@63080
   202
(* content *)
wenzelm@63080
   203
wenzelm@63080
   204
local
wenzelm@63080
   205
wenzelm@67662
   206
fun fold_static_lazy f =
wenzelm@67662
   207
  Name_Space.fold_table (fn (a, Static ths) => f (a, ths) | _ => I) o facts_of;
wenzelm@67662
   208
wenzelm@67668
   209
fun consolidate facts =
wenzelm@67662
   210
  let
wenzelm@68698
   211
    val unfinished =
wenzelm@68698
   212
      (facts, []) |-> fold_static_lazy (fn (_, ths) => if Lazy.is_finished ths then I else cons ths);
wenzelm@68698
   213
    val _ = Lazy.consolidate unfinished;
wenzelm@67668
   214
  in facts end;
wenzelm@67662
   215
wenzelm@63080
   216
fun included verbose prev_facts facts name =
wenzelm@63080
   217
  not (exists (fn prev => defined prev name) prev_facts orelse
wenzelm@63080
   218
    not verbose andalso is_concealed facts name);
wenzelm@63080
   219
wenzelm@63080
   220
in
wenzelm@56158
   221
wenzelm@67662
   222
fun fold_static f facts =
wenzelm@67668
   223
  fold_static_lazy (f o apsnd Lazy.force) (consolidate facts);
wenzelm@26393
   224
wenzelm@56158
   225
fun dest_static verbose prev_facts facts =
wenzelm@63080
   226
  fold_static (fn (a, ths) => included verbose prev_facts facts a ? cons (a, ths)) facts []
wenzelm@60924
   227
  |> sort_by #1;
wenzelm@26281
   228
wenzelm@63080
   229
fun dest_all context verbose prev_facts facts =
wenzelm@67668
   230
  (facts_of (consolidate facts), [])
wenzelm@67662
   231
  |-> Name_Space.fold_table (fn (a, fact) =>
wenzelm@67662
   232
    let val ths = (case fact of Static ths => Lazy.force ths | Dynamic f => f context)
wenzelm@67662
   233
    in included verbose prev_facts facts a ? cons (a, ths) end)
wenzelm@63080
   234
  |> sort_by #1;
wenzelm@63080
   235
wenzelm@63080
   236
end;
wenzelm@63080
   237
wenzelm@26281
   238
wenzelm@26281
   239
(* indexed props *)
wenzelm@26281
   240
wenzelm@63337
   241
val prop_ord = Term_Ord.term_ord o apply2 (Thm.full_prop_of o fst);
wenzelm@26281
   242
wenzelm@26281
   243
fun props (Facts {props, ...}) = sort_distinct prop_ord (Net.content props);
wenzelm@26281
   244
fun could_unify (Facts {props, ...}) = Net.unify_term props;
wenzelm@26281
   245
wenzelm@26281
   246
wenzelm@26393
   247
(* merge facts *)
wenzelm@26281
   248
wenzelm@26281
   249
fun merge (Facts {facts = facts1, props = props1}, Facts {facts = facts2, props = props2}) =
wenzelm@26281
   250
  let
wenzelm@33095
   251
    val facts' = Name_Space.merge_tables (facts1, facts2);
wenzelm@56137
   252
    val props' =
wenzelm@56137
   253
      if Net.is_empty props2 then props1
wenzelm@56137
   254
      else if Net.is_empty props1 then props2
wenzelm@56137
   255
      else Net.merge (is_equal o prop_ord) (props1, props2);  (*beware of non-canonical merge*)
wenzelm@26281
   256
  in make_facts facts' props' end;
wenzelm@26281
   257
wenzelm@26393
   258
wenzelm@67662
   259
(* add entries *)
wenzelm@67662
   260
wenzelm@67662
   261
fun add_prop pos th =
wenzelm@67662
   262
  Net.insert_term (K false) (Thm.full_prop_of th, (th, pos));
wenzelm@26393
   263
wenzelm@49747
   264
fun add_static context {strict, index} (b, ths) (Facts {facts, props}) =
wenzelm@26281
   265
  let
wenzelm@67662
   266
    val ths' = ths
wenzelm@67662
   267
      |> index ? Lazy.force_value
wenzelm@67662
   268
      |> Lazy.map_finished (map Thm.trim_context);
wenzelm@33093
   269
    val (name, facts') =
wenzelm@33093
   270
      if Binding.is_empty b then ("", facts)
wenzelm@61054
   271
      else Name_Space.define context strict (b, Static ths') facts;
wenzelm@67676
   272
    val props' =
wenzelm@67676
   273
      if index then
wenzelm@67676
   274
        props |> fold (add_prop (Binding.pos_of (Binding.default_pos b))) (Lazy.force ths')
wenzelm@67676
   275
      else props;
haftmann@28864
   276
  in (name, make_facts facts' props') end;
wenzelm@26281
   277
wenzelm@47005
   278
fun add_dynamic context (b, f) (Facts {facts, props}) =
wenzelm@47005
   279
  let val (name, facts') = Name_Space.define context true (b, Dynamic f) facts;
wenzelm@33093
   280
  in (name, make_facts facts' props) end;
wenzelm@26281
   281
wenzelm@26654
   282
wenzelm@26654
   283
(* remove entries *)
wenzelm@26654
   284
wenzelm@56025
   285
fun del name (Facts {facts, props}) =
wenzelm@56025
   286
  make_facts (Name_Space.del_table name facts) props;
wenzelm@26654
   287
wenzelm@56025
   288
fun hide fully name (Facts {facts, props}) =
wenzelm@56025
   289
  make_facts (Name_Space.hide_table fully name facts) props;
wenzelm@26654
   290
wenzelm@26281
   291
end;