author  wenzelm 
Sun, 25 Oct 2009 19:14:25 +0100  
changeset 33163  351fc13613f2 
parent 33096  db3c18fd9708 
child 35408  b48ab741683b 
permissions  rwrr 
26281
328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset

1 
(* Title: Pure/facts.ML 
328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset

2 
Author: Makarius 
328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset

3 

26307  4 
Environment of named facts, optionally indexed by proposition. 
26281
328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset

5 
*) 
328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset

6 

328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset

7 
signature FACTS = 
328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset

8 
sig 
26336
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26307
diff
changeset

9 
val the_single: string > thm list > thm 
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26307
diff
changeset

10 
datatype interval = FromTo of int * int  From of int  Single of int 
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26307
diff
changeset

11 
datatype ref = 
26361  12 
Named of (string * Position.T) * interval list option  
26336
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26307
diff
changeset

13 
Fact of string 
26361  14 
val named: string > ref 
26336
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26307
diff
changeset

15 
val string_of_ref: ref > string 
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26307
diff
changeset

16 
val name_of_ref: ref > string 
26366  17 
val pos_of_ref: ref > Position.T 
26336
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26307
diff
changeset

18 
val map_name_of_ref: (string > string) > ref > ref 
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26307
diff
changeset

19 
val select: ref > thm list > thm list 
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26307
diff
changeset

20 
val selections: string * thm list > (ref * thm) list 
26281
328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset

21 
type T 
26393  22 
val empty: T 
33095
bbd52d2f8696
renamed NameSpace to Name_Space  also to emphasize its subtle change in semantics;
wenzelm
parents:
33093
diff
changeset

23 
val space_of: T > Name_Space.T 
33163  24 
val is_concealed: T > string > bool 
26664
167d879a89b0
renamed dest to dest_table, and extern to extern table;
wenzelm
parents:
26654
diff
changeset

25 
val intern: T > xstring > string 
167d879a89b0
renamed dest to dest_table, and extern to extern table;
wenzelm
parents:
26654
diff
changeset

26 
val extern: T > string > xstring 
27738  27 
val lookup: Context.generic > T > string > (bool * thm list) option 
26692  28 
val defined: T > string > bool 
29 
val fold_static: (string * thm list > 'a > 'a) > T > 'a > 'a 

27175  30 
val dest_static: T list > T > (string * thm list) list 
31 
val extern_static: T list > T > (xstring * thm list) list 

26281
328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset

32 
val props: T > thm list 
328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset

33 
val could_unify: T > term > thm list 
328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset

34 
val merge: T * T > T 
33095
bbd52d2f8696
renamed NameSpace to Name_Space  also to emphasize its subtle change in semantics;
wenzelm
parents:
33093
diff
changeset

35 
val add_global: Name_Space.naming > binding * thm list > T > string * T 
bbd52d2f8696
renamed NameSpace to Name_Space  also to emphasize its subtle change in semantics;
wenzelm
parents:
33093
diff
changeset

36 
val add_local: bool > Name_Space.naming > binding * thm list > T > string * T 
bbd52d2f8696
renamed NameSpace to Name_Space  also to emphasize its subtle change in semantics;
wenzelm
parents:
33093
diff
changeset

37 
val add_dynamic: Name_Space.naming > binding * (Context.generic > thm list) > T > string * T 
26654
1f711934f221
disallow duplicate entries (weak version for merge);
wenzelm
parents:
26393
diff
changeset

38 
val del: string > T > T 
1f711934f221
disallow duplicate entries (weak version for merge);
wenzelm
parents:
26393
diff
changeset

39 
val hide: bool > string > T > T 
26281
328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset

40 
end; 
328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset

41 

328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset

42 
structure Facts: FACTS = 
328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset

43 
struct 
328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset

44 

26336
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26307
diff
changeset

45 
(** fact references **) 
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26307
diff
changeset

46 

a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26307
diff
changeset

47 
fun the_single _ [th] : thm = th 
33163  48 
 the_single name _ = error ("Expected singleton fact " ^ quote name); 
26336
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26307
diff
changeset

49 

a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26307
diff
changeset

50 

a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26307
diff
changeset

51 
(* datatype interval *) 
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26307
diff
changeset

52 

a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26307
diff
changeset

53 
datatype interval = 
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26307
diff
changeset

54 
FromTo of int * int  
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26307
diff
changeset

55 
From of int  
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26307
diff
changeset

56 
Single of int; 
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26307
diff
changeset

57 

a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26307
diff
changeset

58 
fun string_of_interval (FromTo (i, j)) = string_of_int i ^ "" ^ string_of_int j 
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26307
diff
changeset

59 
 string_of_interval (From i) = string_of_int i ^ "" 
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26307
diff
changeset

60 
 string_of_interval (Single i) = string_of_int i; 
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26307
diff
changeset

61 

a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26307
diff
changeset

62 
fun interval n iv = 
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26307
diff
changeset

63 
let fun err () = raise Fail ("Bad interval specification " ^ string_of_interval iv) in 
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26307
diff
changeset

64 
(case iv of 
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26307
diff
changeset

65 
FromTo (i, j) => if i <= j then i upto j else err () 
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26307
diff
changeset

66 
 From i => if i <= n then i upto n else err () 
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26307
diff
changeset

67 
 Single i => [i]) 
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26307
diff
changeset

68 
end; 
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26307
diff
changeset

69 

a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26307
diff
changeset

70 

a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26307
diff
changeset

71 
(* datatype ref *) 
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26307
diff
changeset

72 

a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26307
diff
changeset

73 
datatype ref = 
26361  74 
Named of (string * Position.T) * interval list option  
26336
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26307
diff
changeset

75 
Fact of string; 
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26307
diff
changeset

76 

26361  77 
fun named name = Named ((name, Position.none), NONE); 
78 

26366  79 
fun name_pos_of_ref (Named (name_pos, _)) = name_pos 
80 
 name_pos_of_ref (Fact _) = error "Illegal literal fact"; 

81 

82 
val name_of_ref = #1 o name_pos_of_ref; 

83 
val pos_of_ref = #2 o name_pos_of_ref; 

26336
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26307
diff
changeset

84 

26361  85 
fun map_name_of_ref f (Named ((name, pos), is)) = Named ((f name, pos), is) 
26336
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26307
diff
changeset

86 
 map_name_of_ref _ r = r; 
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26307
diff
changeset

87 

26361  88 
fun string_of_ref (Named ((name, _), NONE)) = name 
89 
 string_of_ref (Named ((name, _), SOME is)) = 

26336
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26307
diff
changeset

90 
name ^ enclose "(" ")" (commas (map string_of_interval is)) 
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26307
diff
changeset

91 
 string_of_ref (Fact _) = error "Illegal literal fact"; 
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26307
diff
changeset

92 

a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26307
diff
changeset

93 

a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26307
diff
changeset

94 
(* select *) 
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26307
diff
changeset

95 

a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26307
diff
changeset

96 
fun select (Fact _) ths = ths 
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26307
diff
changeset

97 
 select (Named (_, NONE)) ths = ths 
26361  98 
 select (Named ((name, pos), SOME ivs)) ths = 
26336
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26307
diff
changeset

99 
let 
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26307
diff
changeset

100 
val n = length ths; 
26361  101 
fun err msg = 
102 
error (msg ^ " for " ^ quote name ^ " (length " ^ string_of_int n ^ ")" ^ 

103 
Position.str_of pos); 

26336
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26307
diff
changeset

104 
fun sel i = 
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26307
diff
changeset

105 
if i < 1 orelse i > n then err ("Bad subscript " ^ string_of_int i) 
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26307
diff
changeset

106 
else nth ths (i  1); 
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26307
diff
changeset

107 
val is = maps (interval n) ivs handle Fail msg => err msg; 
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26307
diff
changeset

108 
in map sel is end; 
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26307
diff
changeset

109 

a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26307
diff
changeset

110 

a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26307
diff
changeset

111 
(* selections *) 
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26307
diff
changeset

112 

26361  113 
fun selections (name, [th]) = [(Named ((name, Position.none), NONE), th)] 
114 
 selections (name, ths) = map2 (fn i => fn th => 

115 
(Named ((name, Position.none), SOME [Single i]), th)) (1 upto length ths) ths; 

26336
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26307
diff
changeset

116 

a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26307
diff
changeset

117 

a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26307
diff
changeset

118 

a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26307
diff
changeset

119 
(** fact environment **) 
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26307
diff
changeset

120 

26393  121 
(* datatypes *) 
122 

123 
datatype fact = Static of thm list  Dynamic of Context.generic > thm list; 

26281
328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset

124 

328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset

125 
datatype T = Facts of 
33095
bbd52d2f8696
renamed NameSpace to Name_Space  also to emphasize its subtle change in semantics;
wenzelm
parents:
33093
diff
changeset

126 
{facts: fact Name_Space.table, 
26281
328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset

127 
props: thm Net.net}; 
328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset

128 

328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset

129 
fun make_facts facts props = Facts {facts = facts, props = props}; 
33163  130 

33096  131 
val empty = make_facts (Name_Space.empty_table "fact") Net.empty; 
26281
328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset

132 

328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset

133 

328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset

134 
(* named facts *) 
328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset

135 

328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset

136 
fun facts_of (Facts {facts, ...}) = facts; 
328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset

137 

328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset

138 
val space_of = #1 o facts_of; 
26393  139 
val table_of = #2 o facts_of; 
140 

33163  141 
val is_concealed = Name_Space.is_concealed o space_of; 
142 

33095
bbd52d2f8696
renamed NameSpace to Name_Space  also to emphasize its subtle change in semantics;
wenzelm
parents:
33093
diff
changeset

143 
val intern = Name_Space.intern o space_of; 
bbd52d2f8696
renamed NameSpace to Name_Space  also to emphasize its subtle change in semantics;
wenzelm
parents:
33093
diff
changeset

144 
val extern = Name_Space.extern o space_of; 
26664
167d879a89b0
renamed dest to dest_table, and extern to extern table;
wenzelm
parents:
26654
diff
changeset

145 

26692  146 
val defined = Symtab.defined o table_of; 
147 

26393  148 
fun lookup context facts name = 
149 
(case Symtab.lookup (table_of facts) name of 

150 
NONE => NONE 

33093
d010f61d3702
eliminated separate stamp  NameSpace.define/merge etc. ensure uniqueness already;
wenzelm
parents:
29848
diff
changeset

151 
 SOME (Static ths) => SOME (true, ths) 
d010f61d3702
eliminated separate stamp  NameSpace.define/merge etc. ensure uniqueness already;
wenzelm
parents:
29848
diff
changeset

152 
 SOME (Dynamic f) => SOME (false, f context)); 
26393  153 

33093
d010f61d3702
eliminated separate stamp  NameSpace.define/merge etc. ensure uniqueness already;
wenzelm
parents:
29848
diff
changeset

154 
fun fold_static f = 
d010f61d3702
eliminated separate stamp  NameSpace.define/merge etc. ensure uniqueness already;
wenzelm
parents:
29848
diff
changeset

155 
Symtab.fold (fn (name, Static ths) => f (name, ths)  _ => I) o table_of; 
26393  156 

27175  157 

158 
(* content difference *) 

159 

160 
fun diff_table prev_facts facts = 

161 
fold_static (fn (name, ths) => 

162 
if exists (fn prev => defined prev name) prev_facts then I 

163 
else cons (name, ths)) facts []; 

164 

165 
fun dest_static prev_facts facts = 

166 
sort_wrt #1 (diff_table prev_facts facts); 

167 

168 
fun extern_static prev_facts facts = 

169 
sort_wrt #1 (diff_table prev_facts facts > map (apfst (extern facts))); 

26281
328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset

170 

328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset

171 

328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset

172 
(* indexed props *) 
328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset

173 

29269
5c25a2012975
moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
28965
diff
changeset

174 
val prop_ord = TermOrd.term_ord o pairself Thm.full_prop_of; 
26281
328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset

175 

328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset

176 
fun props (Facts {props, ...}) = sort_distinct prop_ord (Net.content props); 
328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset

177 
fun could_unify (Facts {props, ...}) = Net.unify_term props; 
328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset

178 

328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset

179 

26393  180 
(* merge facts *) 
26281
328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset

181 

328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset

182 
fun merge (Facts {facts = facts1, props = props1}, Facts {facts = facts2, props = props2}) = 
328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset

183 
let 
33095
bbd52d2f8696
renamed NameSpace to Name_Space  also to emphasize its subtle change in semantics;
wenzelm
parents:
33093
diff
changeset

184 
val facts' = Name_Space.merge_tables (facts1, facts2); 
26281
328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset

185 
val props' = Net.merge (is_equal o prop_ord) (props1, props2); 
328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset

186 
in make_facts facts' props' end; 
328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset

187 

26393  188 

26654
1f711934f221
disallow duplicate entries (weak version for merge);
wenzelm
parents:
26393
diff
changeset

189 
(* add static entries *) 
26393  190 

33093
d010f61d3702
eliminated separate stamp  NameSpace.define/merge etc. ensure uniqueness already;
wenzelm
parents:
29848
diff
changeset

191 
local 
d010f61d3702
eliminated separate stamp  NameSpace.define/merge etc. ensure uniqueness already;
wenzelm
parents:
29848
diff
changeset

192 

d010f61d3702
eliminated separate stamp  NameSpace.define/merge etc. ensure uniqueness already;
wenzelm
parents:
29848
diff
changeset

193 
fun add strict do_props naming (b, ths) (Facts {facts, props}) = 
26281
328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset

194 
let 
33093
d010f61d3702
eliminated separate stamp  NameSpace.define/merge etc. ensure uniqueness already;
wenzelm
parents:
29848
diff
changeset

195 
val (name, facts') = 
d010f61d3702
eliminated separate stamp  NameSpace.define/merge etc. ensure uniqueness already;
wenzelm
parents:
29848
diff
changeset

196 
if Binding.is_empty b then ("", facts) 
33095
bbd52d2f8696
renamed NameSpace to Name_Space  also to emphasize its subtle change in semantics;
wenzelm
parents:
33093
diff
changeset

197 
else Name_Space.define strict naming (b, Static ths) facts; 
26281
328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset

198 
val props' = 
33093
d010f61d3702
eliminated separate stamp  NameSpace.define/merge etc. ensure uniqueness already;
wenzelm
parents:
29848
diff
changeset

199 
if do_props 
d010f61d3702
eliminated separate stamp  NameSpace.define/merge etc. ensure uniqueness already;
wenzelm
parents:
29848
diff
changeset

200 
then fold (fn th => Net.insert_term (K false) (Thm.full_prop_of th, th)) ths props 
26281
328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset

201 
else props; 
28864  202 
in (name, make_facts facts' props') end; 
26281
328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset

203 

33093
d010f61d3702
eliminated separate stamp  NameSpace.define/merge etc. ensure uniqueness already;
wenzelm
parents:
29848
diff
changeset

204 
in 
d010f61d3702
eliminated separate stamp  NameSpace.define/merge etc. ensure uniqueness already;
wenzelm
parents:
29848
diff
changeset

205 

d010f61d3702
eliminated separate stamp  NameSpace.define/merge etc. ensure uniqueness already;
wenzelm
parents:
29848
diff
changeset

206 
val add_global = add true false; 
d010f61d3702
eliminated separate stamp  NameSpace.define/merge etc. ensure uniqueness already;
wenzelm
parents:
29848
diff
changeset

207 
val add_local = add false; 
d010f61d3702
eliminated separate stamp  NameSpace.define/merge etc. ensure uniqueness already;
wenzelm
parents:
29848
diff
changeset

208 

d010f61d3702
eliminated separate stamp  NameSpace.define/merge etc. ensure uniqueness already;
wenzelm
parents:
29848
diff
changeset

209 
end; 
26307  210 

26393  211 

26654
1f711934f221
disallow duplicate entries (weak version for merge);
wenzelm
parents:
26393
diff
changeset

212 
(* add dynamic entries *) 
26393  213 

33093
d010f61d3702
eliminated separate stamp  NameSpace.define/merge etc. ensure uniqueness already;
wenzelm
parents:
29848
diff
changeset

214 
fun add_dynamic naming (b, f) (Facts {facts, props}) = 
33095
bbd52d2f8696
renamed NameSpace to Name_Space  also to emphasize its subtle change in semantics;
wenzelm
parents:
33093
diff
changeset

215 
let val (name, facts') = Name_Space.define true naming (b, Dynamic f) facts; 
33093
d010f61d3702
eliminated separate stamp  NameSpace.define/merge etc. ensure uniqueness already;
wenzelm
parents:
29848
diff
changeset

216 
in (name, make_facts facts' props) end; 
26281
328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset

217 

26654
1f711934f221
disallow duplicate entries (weak version for merge);
wenzelm
parents:
26393
diff
changeset

218 

1f711934f221
disallow duplicate entries (weak version for merge);
wenzelm
parents:
26393
diff
changeset

219 
(* remove entries *) 
1f711934f221
disallow duplicate entries (weak version for merge);
wenzelm
parents:
26393
diff
changeset

220 

1f711934f221
disallow duplicate entries (weak version for merge);
wenzelm
parents:
26393
diff
changeset

221 
fun del name (Facts {facts = (space, tab), props}) = 
1f711934f221
disallow duplicate entries (weak version for merge);
wenzelm
parents:
26393
diff
changeset

222 
let 
33163  223 
val space' = Name_Space.hide true name space handle ERROR _ => space; 
26654
1f711934f221
disallow duplicate entries (weak version for merge);
wenzelm
parents:
26393
diff
changeset

224 
val tab' = Symtab.delete_safe name tab; 
1f711934f221
disallow duplicate entries (weak version for merge);
wenzelm
parents:
26393
diff
changeset

225 
in make_facts (space', tab') props end; 
1f711934f221
disallow duplicate entries (weak version for merge);
wenzelm
parents:
26393
diff
changeset

226 

1f711934f221
disallow duplicate entries (weak version for merge);
wenzelm
parents:
26393
diff
changeset

227 
fun hide fully name (Facts {facts = (space, tab), props}) = 
33095
bbd52d2f8696
renamed NameSpace to Name_Space  also to emphasize its subtle change in semantics;
wenzelm
parents:
33093
diff
changeset

228 
make_facts (Name_Space.hide fully name space, tab) props; 
26654
1f711934f221
disallow duplicate entries (weak version for merge);
wenzelm
parents:
26393
diff
changeset

229 

26281
328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset

230 
end; 