fact table now using name bindings
authorhaftmann
Thu Nov 20 19:06:03 2008 +0100 (2008-11-20)
changeset 28864d6fe93e3dcb9
parent 28863 32e83a854e5e
child 28865 194e8f3439fe
fact table now using name bindings
src/Pure/Isar/proof_context.ML
src/Pure/facts.ML
src/Pure/pure_thy.ML
     1.1 --- a/src/Pure/Isar/proof_context.ML	Thu Nov 20 19:06:02 2008 +0100
     1.2 +++ b/src/Pure/Isar/proof_context.ML	Thu Nov 20 19:06:03 2008 +0100
     1.3 @@ -23,8 +23,6 @@
     1.4    val abbrev_mode: Proof.context -> bool
     1.5    val set_stmt: bool -> Proof.context -> Proof.context
     1.6    val naming_of: Proof.context -> NameSpace.naming
     1.7 -  val name_decl: (string * 'a -> Proof.context -> 'b * Proof.context)
     1.8 -    -> Name.binding * 'a -> Proof.context -> (string * 'b) * Proof.context
     1.9    val full_name: Proof.context -> bstring -> string
    1.10    val full_binding: Proof.context -> Name.binding -> string
    1.11    val consts_of: Proof.context -> Consts.T
    1.12 @@ -249,18 +247,6 @@
    1.13  
    1.14  val naming_of = #naming o rep_context;
    1.15  
    1.16 -fun name_decl decl (b, x) ctxt =
    1.17 -  let
    1.18 -    val naming = naming_of ctxt;
    1.19 -    val (naming', name) = Name.namify naming b;
    1.20 -  in
    1.21 -    ctxt
    1.22 -    |> map_naming (K naming')
    1.23 -    |> decl (Name.name_of b, x)
    1.24 -    |>> pair name
    1.25 -    ||> map_naming (K naming)
    1.26 -  end;
    1.27 -
    1.28  val full_name = NameSpace.full o naming_of;
    1.29  val full_binding = NameSpace.full_binding o naming_of;
    1.30  
    1.31 @@ -981,7 +967,7 @@
    1.32  
    1.33  fun update_thms _ (b, NONE) ctxt = ctxt |> map_facts (Facts.del (full_binding ctxt b))
    1.34    | update_thms do_props (b, SOME ths) ctxt = ctxt |> map_facts
    1.35 -      (Facts.add_local do_props (naming_of ctxt) (full_binding ctxt b, ths));
    1.36 +      (Facts.add_local do_props (naming_of ctxt) (b, ths) #> snd);
    1.37  
    1.38  fun gen_note_thmss get k = fold_map (fn ((b, more_attrs), raw_facts) => fn ctxt =>
    1.39    let
     2.1 --- a/src/Pure/facts.ML	Thu Nov 20 19:06:02 2008 +0100
     2.2 +++ b/src/Pure/facts.ML	Thu Nov 20 19:06:03 2008 +0100
     2.3 @@ -31,9 +31,9 @@
     2.4    val props: T -> thm list
     2.5    val could_unify: T -> term -> thm list
     2.6    val merge: T * T -> T
     2.7 -  val add_global: NameSpace.naming -> string * thm list -> T -> T
     2.8 -  val add_local: bool -> NameSpace.naming -> string * thm list -> T -> T
     2.9 -  val add_dynamic: NameSpace.naming -> string * (Context.generic -> thm list) -> T -> T
    2.10 +  val add_global: NameSpace.naming -> Name.binding * thm list -> T -> string * T
    2.11 +  val add_local: bool -> NameSpace.naming -> Name.binding * thm list -> T -> string * T
    2.12 +  val add_dynamic: NameSpace.naming -> Name.binding * (Context.generic -> thm list) -> T -> string * T
    2.13    val del: string -> T -> T
    2.14    val hide: bool -> string -> T -> T
    2.15  end;
    2.16 @@ -190,22 +190,20 @@
    2.17  
    2.18  (* add static entries *)
    2.19  
    2.20 -fun add permissive do_props naming (name, ths) (Facts {facts, props}) =
    2.21 +fun add permissive do_props naming (b, ths) (Facts {facts, props}) =
    2.22    let
    2.23 -    val facts' =
    2.24 -      if name = "" then facts
    2.25 -      else
    2.26 -        let
    2.27 -          val (space, tab) = facts;
    2.28 -          val space' = NameSpace.declare naming name space;
    2.29 -          val entry = (name, (Static ths, serial ()));
    2.30 -          val tab' = (if permissive then Symtab.update else Symtab.update_new) entry tab
    2.31 -            handle Symtab.DUP dup => err_dup_fact dup;
    2.32 -        in (space', tab') end;
    2.33 +    val (name, facts') = if Name.is_nothing b then ("", facts)
    2.34 +      else let
    2.35 +        val (space, tab) = facts;
    2.36 +        val (name, space') = NameSpace.declare_binding naming b space;
    2.37 +        val entry = (name, (Static ths, serial ()));
    2.38 +        val tab' = (if permissive then Symtab.update else Symtab.update_new) entry tab
    2.39 +          handle Symtab.DUP dup => err_dup_fact dup;
    2.40 +      in (name, (space', tab')) end;
    2.41      val props' =
    2.42        if do_props then fold (fn th => Net.insert_term (K false) (Thm.full_prop_of th, th)) ths props
    2.43        else props;
    2.44 -  in make_facts facts' props' end;
    2.45 +  in (name, make_facts facts' props') end;
    2.46  
    2.47  val add_global = add false false;
    2.48  val add_local = add true;
    2.49 @@ -213,13 +211,13 @@
    2.50  
    2.51  (* add dynamic entries *)
    2.52  
    2.53 -fun add_dynamic naming (name, f) (Facts {facts = (space, tab), props}) =
    2.54 +fun add_dynamic naming (b, f) (Facts {facts = (space, tab), props}) =
    2.55    let
    2.56 -    val space' = NameSpace.declare naming name space;
    2.57 +    val (name, space') = NameSpace.declare_binding naming b space;
    2.58      val entry = (name, (Dynamic f, serial ()));
    2.59      val tab' = Symtab.update_new entry tab
    2.60        handle Symtab.DUP dup => err_dup_fact dup;
    2.61 -  in make_facts (space', tab') props end;
    2.62 +  in (name, make_facts (space', tab') props) end;
    2.63  
    2.64  
    2.65  (* remove entries *)
     3.1 --- a/src/Pure/pure_thy.ML	Thu Nov 20 19:06:02 2008 +0100
     3.2 +++ b/src/Pure/pure_thy.ML	Thu Nov 20 19:06:03 2008 +0100
     3.3 @@ -152,7 +152,7 @@
     3.4      val (thy', thms') =
     3.5        enter_proofs (apsnd (post_name name) (app_att (thy, pre_name name thms)));
     3.6      val thms'' = map (Thm.transfer thy') thms';
     3.7 -    val thy'' = thy' |> FactsData.map (apfst (Facts.add_global naming (name, thms'')));
     3.8 +    val thy'' = thy' |> (FactsData.map o apfst) (Facts.add_global naming (b, thms'') #> snd);
     3.9    in (thms'', thy'') end;
    3.10  
    3.11  
    3.12 @@ -187,9 +187,9 @@
    3.13  
    3.14  (* add_thms_dynamic *)
    3.15  
    3.16 -fun add_thms_dynamic (bname, f) thy =
    3.17 -  let val name = Sign.full_name thy bname
    3.18 -  in thy |> FactsData.map (apfst (Facts.add_dynamic (Sign.naming_of thy) (name, f))) end;
    3.19 +fun add_thms_dynamic (bname, f) thy = thy
    3.20 +  |> (FactsData.map o apfst)
    3.21 +      (Facts.add_dynamic (Sign.naming_of thy) (Name.binding bname, f) #> snd);
    3.22  
    3.23  
    3.24  (* note_thmss *)