Environment of named facts (admits overriding). Optional indexing by proposition.
authorwenzelm
Sat Mar 15 18:08:02 2008 +0100 (2008-03-15)
changeset 26281328fd1c551ef
parent 26280 1e007f3f426e
child 26282 305d5ca4fa9d
Environment of named facts (admits overriding). Optional indexing by proposition.
src/Pure/facts.ML
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Pure/facts.ML	Sat Mar 15 18:08:02 2008 +0100
     1.3 @@ -0,0 +1,82 @@
     1.4 +(*  Title:      Pure/facts.ML
     1.5 +    ID:         $Id$
     1.6 +    Author:     Makarius
     1.7 +
     1.8 +Environment of named facts (admits overriding).  Optional indexing by
     1.9 +proposition.
    1.10 +*)
    1.11 +
    1.12 +signature FACTS =
    1.13 +sig
    1.14 +  type T
    1.15 +  val space_of: T -> NameSpace.T
    1.16 +  val lookup: T -> string -> thm list option
    1.17 +  val dest: T -> (string * thm list) list
    1.18 +  val extern: T -> (xstring * thm list) list
    1.19 +  val props: T -> thm list
    1.20 +  val could_unify: T -> term -> thm list
    1.21 +  val empty: T
    1.22 +  val merge: T * T -> T
    1.23 +  val add: bool -> NameSpace.naming -> string * thm list -> T -> T
    1.24 +  val del: string -> T -> T
    1.25 +end;
    1.26 +
    1.27 +structure Facts: FACTS =
    1.28 +struct
    1.29 +
    1.30 +(* datatype *)
    1.31 +
    1.32 +datatype T = Facts of
    1.33 + {facts: thm list NameSpace.table,
    1.34 +  props: thm Net.net};
    1.35 +
    1.36 +fun make_facts facts props = Facts {facts = facts, props = props};
    1.37 +
    1.38 +
    1.39 +(* named facts *)
    1.40 +
    1.41 +fun facts_of (Facts {facts, ...}) = facts;
    1.42 +
    1.43 +val space_of = #1 o facts_of;
    1.44 +val lookup = Symtab.lookup o #2 o facts_of;
    1.45 +val dest = NameSpace.dest_table o facts_of;
    1.46 +val extern = NameSpace.extern_table o facts_of;
    1.47 +
    1.48 +
    1.49 +(* indexed props *)
    1.50 +
    1.51 +val prop_ord = Term.term_ord o pairself Thm.full_prop_of;
    1.52 +
    1.53 +fun props (Facts {props, ...}) = sort_distinct prop_ord (Net.content props);
    1.54 +fun could_unify (Facts {props, ...}) = Net.unify_term props;
    1.55 +
    1.56 +
    1.57 +(* build facts *)
    1.58 +
    1.59 +val empty = make_facts NameSpace.empty_table Net.empty;
    1.60 +
    1.61 +fun merge (Facts {facts = facts1, props = props1}, Facts {facts = facts2, props = props2}) =
    1.62 +  let
    1.63 +    val facts' = NameSpace.merge_tables (K true) (facts1, facts2);
    1.64 +    val props' = Net.merge (is_equal o prop_ord) (props1, props2);
    1.65 +  in make_facts facts' props' end;
    1.66 +
    1.67 +fun add do_props naming (name, ths) (Facts {facts, props}) =
    1.68 +  let
    1.69 +    val facts' =
    1.70 +      if name = "" then facts
    1.71 +      else
    1.72 +        let
    1.73 +          val (space, tab) = facts;
    1.74 +          val space' = NameSpace.declare naming name space;
    1.75 +          val tab' = Symtab.update (name, ths) tab;
    1.76 +        in (space', tab') end;
    1.77 +    val props' =
    1.78 +      if do_props then fold (fn th => Net.insert_term (K false) (Thm.full_prop_of th, th)) ths props
    1.79 +      else props;
    1.80 +  in make_facts facts' props' end;
    1.81 +
    1.82 +fun del name (Facts {facts = (space, tab), props}) =
    1.83 +  make_facts (space, Symtab.delete_safe name tab) props;
    1.84 +
    1.85 +end;