src/Pure/facts.ML
author wenzelm
Mon Mar 17 20:51:09 2008 +0100 (2008-03-17)
changeset 26307 27d3de85c266
parent 26290 e025bf1cc0f1
child 26336 a0e2b706ce73
permissions -rw-r--r--
replaced generic add by add_local/add_global;
add_global: report/ignore duplicate bindings;
wenzelm@26281
     1
(*  Title:      Pure/facts.ML
wenzelm@26281
     2
    ID:         $Id$
wenzelm@26281
     3
    Author:     Makarius
wenzelm@26281
     4
wenzelm@26307
     5
Environment of named facts, optionally indexed by proposition.
wenzelm@26281
     6
*)
wenzelm@26281
     7
wenzelm@26281
     8
signature FACTS =
wenzelm@26281
     9
sig
wenzelm@26281
    10
  type T
wenzelm@26281
    11
  val space_of: T -> NameSpace.T
wenzelm@26281
    12
  val lookup: T -> string -> thm list option
wenzelm@26281
    13
  val dest: T -> (string * thm list) list
wenzelm@26281
    14
  val extern: T -> (xstring * thm list) list
wenzelm@26281
    15
  val props: T -> thm list
wenzelm@26281
    16
  val could_unify: T -> term -> thm list
wenzelm@26281
    17
  val empty: T
wenzelm@26281
    18
  val merge: T * T -> T
wenzelm@26307
    19
  val add_global: NameSpace.naming -> string * thm list -> T -> T
wenzelm@26307
    20
  val add_local: bool -> NameSpace.naming -> string * thm list -> T -> T
wenzelm@26281
    21
  val del: string -> T -> T
wenzelm@26281
    22
end;
wenzelm@26281
    23
wenzelm@26281
    24
structure Facts: FACTS =
wenzelm@26281
    25
struct
wenzelm@26281
    26
wenzelm@26281
    27
(* datatype *)
wenzelm@26281
    28
wenzelm@26281
    29
datatype T = Facts of
wenzelm@26281
    30
 {facts: thm list NameSpace.table,
wenzelm@26281
    31
  props: thm Net.net};
wenzelm@26281
    32
wenzelm@26281
    33
fun make_facts facts props = Facts {facts = facts, props = props};
wenzelm@26281
    34
wenzelm@26281
    35
wenzelm@26281
    36
(* named facts *)
wenzelm@26281
    37
wenzelm@26281
    38
fun facts_of (Facts {facts, ...}) = facts;
wenzelm@26281
    39
wenzelm@26281
    40
val space_of = #1 o facts_of;
wenzelm@26281
    41
val lookup = Symtab.lookup o #2 o facts_of;
wenzelm@26281
    42
val dest = NameSpace.dest_table o facts_of;
wenzelm@26281
    43
val extern = NameSpace.extern_table o facts_of;
wenzelm@26281
    44
wenzelm@26281
    45
wenzelm@26281
    46
(* indexed props *)
wenzelm@26281
    47
wenzelm@26281
    48
val prop_ord = Term.term_ord o pairself Thm.full_prop_of;
wenzelm@26281
    49
wenzelm@26281
    50
fun props (Facts {props, ...}) = sort_distinct prop_ord (Net.content props);
wenzelm@26281
    51
fun could_unify (Facts {props, ...}) = Net.unify_term props;
wenzelm@26281
    52
wenzelm@26281
    53
wenzelm@26281
    54
(* build facts *)
wenzelm@26281
    55
wenzelm@26281
    56
val empty = make_facts NameSpace.empty_table Net.empty;
wenzelm@26281
    57
wenzelm@26281
    58
fun merge (Facts {facts = facts1, props = props1}, Facts {facts = facts2, props = props2}) =
wenzelm@26281
    59
  let
wenzelm@26281
    60
    val facts' = NameSpace.merge_tables (K true) (facts1, facts2);
wenzelm@26281
    61
    val props' = Net.merge (is_equal o prop_ord) (props1, props2);
wenzelm@26281
    62
  in make_facts facts' props' end;
wenzelm@26281
    63
wenzelm@26307
    64
fun add permissive do_props naming (name, ths) (Facts {facts, props}) =
wenzelm@26281
    65
  let
wenzelm@26281
    66
    val facts' =
wenzelm@26281
    67
      if name = "" then facts
wenzelm@26281
    68
      else
wenzelm@26281
    69
        let
wenzelm@26281
    70
          val (space, tab) = facts;
wenzelm@26281
    71
          val space' = NameSpace.declare naming name space;
wenzelm@26307
    72
          val tab' = (if permissive then Symtab.update else Symtab.update_new) (name, ths) tab
wenzelm@26307
    73
            handle Symtab.DUP dup => (legacy_feature ("Duplicate fact " ^ quote dup ^
wenzelm@26307
    74
              Position.str_of (Position.thread_data ())); tab);
wenzelm@26281
    75
        in (space', tab') end;
wenzelm@26281
    76
    val props' =
wenzelm@26281
    77
      if do_props then fold (fn th => Net.insert_term (K false) (Thm.full_prop_of th, th)) ths props
wenzelm@26281
    78
      else props;
wenzelm@26281
    79
  in make_facts facts' props' end;
wenzelm@26281
    80
wenzelm@26307
    81
val add_global = add false false;
wenzelm@26307
    82
val add_local = add true;
wenzelm@26307
    83
wenzelm@26281
    84
fun del name (Facts {facts = (space, tab), props}) =
wenzelm@26290
    85
  let
wenzelm@26290
    86
    val space' = NameSpace.hide true name space handle ERROR _ => space;
wenzelm@26290
    87
    val tab' = Symtab.delete_safe name tab;
wenzelm@26290
    88
  in make_facts (space', tab') props end;
wenzelm@26281
    89
wenzelm@26281
    90
end;