src/Pure/facts.ML
author wenzelm
Wed Mar 19 22:27:57 2008 +0100 (2008-03-19)
changeset 26336 a0e2b706ce73
parent 26307 27d3de85c266
child 26361 7946f459c6c8
permissions -rw-r--r--
renamed datatype thmref to Facts.ref, tuned interfaces;
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@26336
    10
  val the_single: string -> thm list -> thm
wenzelm@26336
    11
  datatype interval = FromTo of int * int | From of int | Single of int
wenzelm@26336
    12
  datatype ref =
wenzelm@26336
    13
    Named of string * interval list option |
wenzelm@26336
    14
    Fact of string
wenzelm@26336
    15
  val string_of_ref: ref -> string
wenzelm@26336
    16
  val name_of_ref: ref -> string
wenzelm@26336
    17
  val map_name_of_ref: (string -> string) -> ref -> ref
wenzelm@26336
    18
  val select: ref -> thm list -> thm list
wenzelm@26336
    19
  val selections: string * thm list -> (ref * thm) list
wenzelm@26281
    20
  type T
wenzelm@26281
    21
  val space_of: T -> NameSpace.T
wenzelm@26281
    22
  val lookup: T -> string -> thm list option
wenzelm@26281
    23
  val dest: T -> (string * thm list) list
wenzelm@26281
    24
  val extern: T -> (xstring * thm list) list
wenzelm@26281
    25
  val props: T -> thm list
wenzelm@26281
    26
  val could_unify: T -> term -> thm list
wenzelm@26281
    27
  val empty: T
wenzelm@26281
    28
  val merge: T * T -> T
wenzelm@26307
    29
  val add_global: NameSpace.naming -> string * thm list -> T -> T
wenzelm@26307
    30
  val add_local: bool -> NameSpace.naming -> string * thm list -> T -> T
wenzelm@26281
    31
  val del: string -> T -> T
wenzelm@26281
    32
end;
wenzelm@26281
    33
wenzelm@26281
    34
structure Facts: FACTS =
wenzelm@26281
    35
struct
wenzelm@26281
    36
wenzelm@26336
    37
(** fact references **)
wenzelm@26336
    38
wenzelm@26336
    39
fun the_single _ [th] : thm = th
wenzelm@26336
    40
  | the_single name _ = error ("Single theorem expected " ^ quote name);
wenzelm@26336
    41
wenzelm@26336
    42
wenzelm@26336
    43
(* datatype interval *)
wenzelm@26336
    44
wenzelm@26336
    45
datatype interval =
wenzelm@26336
    46
  FromTo of int * int |
wenzelm@26336
    47
  From of int |
wenzelm@26336
    48
  Single of int;
wenzelm@26336
    49
wenzelm@26336
    50
fun string_of_interval (FromTo (i, j)) = string_of_int i ^ "-" ^ string_of_int j
wenzelm@26336
    51
  | string_of_interval (From i) = string_of_int i ^ "-"
wenzelm@26336
    52
  | string_of_interval (Single i) = string_of_int i;
wenzelm@26336
    53
wenzelm@26336
    54
fun interval n iv =
wenzelm@26336
    55
  let fun err () = raise Fail ("Bad interval specification " ^ string_of_interval iv) in
wenzelm@26336
    56
    (case iv of
wenzelm@26336
    57
      FromTo (i, j) => if i <= j then i upto j else err ()
wenzelm@26336
    58
    | From i => if i <= n then i upto n else err ()
wenzelm@26336
    59
    | Single i => [i])
wenzelm@26336
    60
  end;
wenzelm@26336
    61
wenzelm@26336
    62
wenzelm@26336
    63
(* datatype ref *)
wenzelm@26336
    64
wenzelm@26336
    65
datatype ref =
wenzelm@26336
    66
  Named of string * interval list option |
wenzelm@26336
    67
  Fact of string;
wenzelm@26336
    68
wenzelm@26336
    69
fun name_of_ref (Named (name, _)) = name
wenzelm@26336
    70
  | name_of_ref (Fact _) = error "Illegal literal fact";
wenzelm@26336
    71
wenzelm@26336
    72
fun map_name_of_ref f (Named (name, is)) = Named (f name, is)
wenzelm@26336
    73
  | map_name_of_ref _ r = r;
wenzelm@26336
    74
wenzelm@26336
    75
fun string_of_ref (Named (name, NONE)) = name
wenzelm@26336
    76
  | string_of_ref (Named (name, SOME is)) =
wenzelm@26336
    77
      name ^ enclose "(" ")" (commas (map string_of_interval is))
wenzelm@26336
    78
  | string_of_ref (Fact _) = error "Illegal literal fact";
wenzelm@26336
    79
wenzelm@26336
    80
wenzelm@26336
    81
(* select *)
wenzelm@26336
    82
wenzelm@26336
    83
fun select (Fact _) ths = ths
wenzelm@26336
    84
  | select (Named (_, NONE)) ths = ths
wenzelm@26336
    85
  | select (Named (name, SOME ivs)) ths =
wenzelm@26336
    86
      let
wenzelm@26336
    87
        val n = length ths;
wenzelm@26336
    88
        fun err msg = error (msg ^ " for " ^ quote name ^ " (length " ^ string_of_int n ^ ")");
wenzelm@26336
    89
        fun sel i =
wenzelm@26336
    90
          if i < 1 orelse i > n then err ("Bad subscript " ^ string_of_int i)
wenzelm@26336
    91
          else nth ths (i - 1);
wenzelm@26336
    92
        val is = maps (interval n) ivs handle Fail msg => err msg;
wenzelm@26336
    93
      in map sel is end;
wenzelm@26336
    94
wenzelm@26336
    95
wenzelm@26336
    96
(* selections *)
wenzelm@26336
    97
wenzelm@26336
    98
fun selections (name, [th]) = [(Named (name, NONE), th)]
wenzelm@26336
    99
  | selections (name, ths) =
wenzelm@26336
   100
      map2 (fn i => fn th => (Named (name, SOME [Single i]), th)) (1 upto length ths) ths;
wenzelm@26336
   101
wenzelm@26336
   102
wenzelm@26336
   103
wenzelm@26336
   104
(** fact environment **)
wenzelm@26336
   105
wenzelm@26336
   106
(* datatype T *)
wenzelm@26281
   107
wenzelm@26281
   108
datatype T = Facts of
wenzelm@26281
   109
 {facts: thm list NameSpace.table,
wenzelm@26281
   110
  props: thm Net.net};
wenzelm@26281
   111
wenzelm@26281
   112
fun make_facts facts props = Facts {facts = facts, props = props};
wenzelm@26281
   113
wenzelm@26281
   114
wenzelm@26281
   115
(* named facts *)
wenzelm@26281
   116
wenzelm@26281
   117
fun facts_of (Facts {facts, ...}) = facts;
wenzelm@26281
   118
wenzelm@26281
   119
val space_of = #1 o facts_of;
wenzelm@26281
   120
val lookup = Symtab.lookup o #2 o facts_of;
wenzelm@26281
   121
val dest = NameSpace.dest_table o facts_of;
wenzelm@26281
   122
val extern = NameSpace.extern_table o facts_of;
wenzelm@26281
   123
wenzelm@26281
   124
wenzelm@26281
   125
(* indexed props *)
wenzelm@26281
   126
wenzelm@26281
   127
val prop_ord = Term.term_ord o pairself Thm.full_prop_of;
wenzelm@26281
   128
wenzelm@26281
   129
fun props (Facts {props, ...}) = sort_distinct prop_ord (Net.content props);
wenzelm@26281
   130
fun could_unify (Facts {props, ...}) = Net.unify_term props;
wenzelm@26281
   131
wenzelm@26281
   132
wenzelm@26281
   133
(* build facts *)
wenzelm@26281
   134
wenzelm@26281
   135
val empty = make_facts NameSpace.empty_table Net.empty;
wenzelm@26281
   136
wenzelm@26281
   137
fun merge (Facts {facts = facts1, props = props1}, Facts {facts = facts2, props = props2}) =
wenzelm@26281
   138
  let
wenzelm@26281
   139
    val facts' = NameSpace.merge_tables (K true) (facts1, facts2);
wenzelm@26281
   140
    val props' = Net.merge (is_equal o prop_ord) (props1, props2);
wenzelm@26281
   141
  in make_facts facts' props' end;
wenzelm@26281
   142
wenzelm@26307
   143
fun add permissive do_props naming (name, ths) (Facts {facts, props}) =
wenzelm@26281
   144
  let
wenzelm@26281
   145
    val facts' =
wenzelm@26281
   146
      if name = "" then facts
wenzelm@26281
   147
      else
wenzelm@26281
   148
        let
wenzelm@26281
   149
          val (space, tab) = facts;
wenzelm@26281
   150
          val space' = NameSpace.declare naming name space;
wenzelm@26307
   151
          val tab' = (if permissive then Symtab.update else Symtab.update_new) (name, ths) tab
wenzelm@26307
   152
            handle Symtab.DUP dup => (legacy_feature ("Duplicate fact " ^ quote dup ^
wenzelm@26307
   153
              Position.str_of (Position.thread_data ())); tab);
wenzelm@26281
   154
        in (space', tab') end;
wenzelm@26281
   155
    val props' =
wenzelm@26281
   156
      if do_props then fold (fn th => Net.insert_term (K false) (Thm.full_prop_of th, th)) ths props
wenzelm@26281
   157
      else props;
wenzelm@26281
   158
  in make_facts facts' props' end;
wenzelm@26281
   159
wenzelm@26307
   160
val add_global = add false false;
wenzelm@26307
   161
val add_local = add true;
wenzelm@26307
   162
wenzelm@26281
   163
fun del name (Facts {facts = (space, tab), props}) =
wenzelm@26290
   164
  let
wenzelm@26290
   165
    val space' = NameSpace.hide true name space handle ERROR _ => space;
wenzelm@26290
   166
    val tab' = Symtab.delete_safe name tab;
wenzelm@26290
   167
  in make_facts (space', tab') props end;
wenzelm@26281
   168
wenzelm@26281
   169
end;