src/Pure/facts.ML
changeset 33093 d010f61d3702
parent 29848 a7c164e228e1
child 33095 bbd52d2f8696
     1.1 --- a/src/Pure/facts.ML	Sat Oct 24 19:20:03 2009 +0200
     1.2 +++ b/src/Pure/facts.ML	Sat Oct 24 19:22:39 2009 +0200
     1.3 @@ -122,7 +122,7 @@
     1.4  datatype fact = Static of thm list | Dynamic of Context.generic -> thm list;
     1.5  
     1.6  datatype T = Facts of
     1.7 - {facts: (fact * serial) NameSpace.table,
     1.8 + {facts: fact NameSpace.table,
     1.9    props: thm Net.net};
    1.10  
    1.11  fun make_facts facts props = Facts {facts = facts, props = props};
    1.12 @@ -144,10 +144,11 @@
    1.13  fun lookup context facts name =
    1.14    (case Symtab.lookup (table_of facts) name of
    1.15      NONE => NONE
    1.16 -  | SOME (Static ths, _) => SOME (true, ths)
    1.17 -  | SOME (Dynamic f, _) => SOME (false, f context));
    1.18 +  | SOME (Static ths) => SOME (true, ths)
    1.19 +  | SOME (Dynamic f) => SOME (false, f context));
    1.20  
    1.21 -fun fold_static f = Symtab.fold (fn (name, (Static ths, _)) => f (name, ths) | _ => I) o table_of;
    1.22 +fun fold_static f =
    1.23 +  Symtab.fold (fn (name, Static ths) => f (name, ths) | _ => I) o table_of;
    1.24  
    1.25  
    1.26  (* content difference *)
    1.27 @@ -174,57 +175,48 @@
    1.28  
    1.29  (* merge facts *)
    1.30  
    1.31 -fun err_dup_fact name = error ("Duplicate fact " ^ quote name);
    1.32 -
    1.33 -(* FIXME stamp identity! *)
    1.34 -fun eq_entry ((Static ths1, _), (Static ths2, _)) = is_equal (list_ord Thm.thm_ord (ths1, ths2))
    1.35 -  | eq_entry ((_, id1: serial), (_, id2)) = id1 = id2;
    1.36 -
    1.37  fun merge (Facts {facts = facts1, props = props1}, Facts {facts = facts2, props = props2}) =
    1.38    let
    1.39 -    val facts' = NameSpace.merge_tables eq_entry (facts1, facts2)
    1.40 -      handle Symtab.DUP dup => err_dup_fact dup;
    1.41 +    val facts' = NameSpace.merge_tables (facts1, facts2);
    1.42      val props' = Net.merge (is_equal o prop_ord) (props1, props2);
    1.43    in make_facts facts' props' end;
    1.44  
    1.45  
    1.46  (* add static entries *)
    1.47  
    1.48 -fun add permissive do_props naming (b, ths) (Facts {facts, props}) =
    1.49 +local
    1.50 +
    1.51 +fun add strict do_props naming (b, ths) (Facts {facts, props}) =
    1.52    let
    1.53 -    val (name, facts') = if Binding.is_empty b then ("", facts)
    1.54 -      else let
    1.55 -        val (space, tab) = facts;
    1.56 -        val (name, space') = NameSpace.declare naming b space;
    1.57 -        val entry = (name, (Static ths, serial ()));
    1.58 -        val tab' = (if permissive then Symtab.update else Symtab.update_new) entry tab
    1.59 -          handle Symtab.DUP dup => err_dup_fact dup;
    1.60 -      in (name, (space', tab')) end;
    1.61 +    val (name, facts') =
    1.62 +      if Binding.is_empty b then ("", facts)
    1.63 +      else NameSpace.define strict naming (b, Static ths) facts;
    1.64      val props' =
    1.65 -      if do_props then fold (fn th => Net.insert_term (K false) (Thm.full_prop_of th, th)) ths props
    1.66 +      if do_props
    1.67 +      then fold (fn th => Net.insert_term (K false) (Thm.full_prop_of th, th)) ths props
    1.68        else props;
    1.69    in (name, make_facts facts' props') end;
    1.70  
    1.71 -val add_global = add false false;
    1.72 -val add_local = add true;
    1.73 +in
    1.74 +
    1.75 +val add_global = add true false;
    1.76 +val add_local = add false;
    1.77 +
    1.78 +end;
    1.79  
    1.80  
    1.81  (* add dynamic entries *)
    1.82  
    1.83 -fun add_dynamic naming (b, f) (Facts {facts = (space, tab), props}) =
    1.84 -  let
    1.85 -    val (name, space') = NameSpace.declare naming b space;
    1.86 -    val entry = (name, (Dynamic f, serial ()));
    1.87 -    val tab' = Symtab.update_new entry tab
    1.88 -      handle Symtab.DUP dup => err_dup_fact dup;
    1.89 -  in (name, make_facts (space', tab') props) end;
    1.90 +fun add_dynamic naming (b, f) (Facts {facts, props}) =
    1.91 +  let val (name, facts') = NameSpace.define true naming (b, Dynamic f) facts;
    1.92 +  in (name, make_facts facts' props) end;
    1.93  
    1.94  
    1.95  (* remove entries *)
    1.96  
    1.97  fun del name (Facts {facts = (space, tab), props}) =
    1.98    let
    1.99 -    val space' = NameSpace.hide true name space handle ERROR _ => space;
   1.100 +    val space' = NameSpace.hide true name space handle ERROR _ => space;  (* FIXME handle?? *)
   1.101      val tab' = Symtab.delete_safe name tab;
   1.102    in make_facts (space', tab') props end;
   1.103