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