author  wenzelm 
Tue, 31 Mar 2015 20:07:37 +0200  
changeset 59883  12a89103cae6 
parent 59058  a78612c67ec0 
child 59884  bbf49d7dfd6f 
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 
55740  9 
val the_single: string * Position.T > thm list > thm 
26336
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 
49887  15 
val string_of_selection: interval list option > string 
26336
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26307
diff
changeset

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

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

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

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

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

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

24 
val space_of: T > Name_Space.T 
57887  25 
val alias: Name_Space.naming > binding > string > T > T 
33163  26 
val is_concealed: T > string > bool 
56003  27 
val check: Context.generic > T > xstring * Position.T > string 
26664
167d879a89b0
renamed dest to dest_table, and extern to extern table;
wenzelm
parents:
26654
diff
changeset

28 
val intern: T > xstring > string 
42358
b47d41d9f4b5
Name_Space: proper configuration options long_names, short_names, unique_names instead of former unsynchronized references;
wenzelm
parents:
35408
diff
changeset

29 
val extern: Proof.context > T > string > xstring 
56140
ed92ce2ac88e
just one cumulative Proof_Context.facts, with uniform retrieval (including PIDE markup, completion etc.);
wenzelm
parents:
56137
diff
changeset

30 
val markup_extern: Proof.context > T > string > Markup.T * xstring 
27738  31 
val lookup: Context.generic > T > string > (bool * thm list) option 
57942
e5bec882fdd0
more informative Token.Fact: retain name of dynamic fact (without selection);
wenzelm
parents:
57887
diff
changeset

32 
val retrieve: Context.generic > T > xstring * Position.T > 
e5bec882fdd0
more informative Token.Fact: retain name of dynamic fact (without selection);
wenzelm
parents:
57887
diff
changeset

33 
{name: string, static: bool, thms: thm list} 
26692  34 
val defined: T > string > bool 
35 
val fold_static: (string * thm list > 'a > 'a) > T > 'a > 'a 

56158
c2c6d560e7b2
more explicit treatment of verbose mode, which includes concealed entries;
wenzelm
parents:
56140
diff
changeset

36 
val dest_static: bool > T list > T > (string * thm list) list 
26281
328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset

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

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

39 
val merge: T * T > T 
49747  40 
val add_static: Context.generic > {strict: bool, index: bool} > 
41 
binding * thm list > T > string * T 

47005
421760a1efe7
maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
wenzelm
parents:
42375
diff
changeset

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

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

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

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

46 

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

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

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

49 

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

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

51 

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

52 
fun the_single _ [th] : thm = th 
55740  53 
 the_single (name, pos) ths = 
54 
error ("Expected singleton fact " ^ quote name ^ 

55 
" (length " ^ string_of_int (length ths) ^ ")" ^ Position.here pos); 

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

56 

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 
(* datatype interval *) 
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26307
diff
changeset

59 

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

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

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

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

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

64 

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

65 
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

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

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

68 

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

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

70 
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

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

72 
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

73 
 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

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

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

76 

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

77 

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

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

79 

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

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

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

83 

26361  84 
fun named name = Named ((name, Position.none), NONE); 
85 

55740  86 
fun name_of_ref (Named ((name, _), _)) = name 
87 
 name_of_ref (Fact _) = raise Fail "Illegal literal fact"; 

88 

89 
fun pos_of_ref (Named ((_, pos), _)) = pos 

90 
 pos_of_ref (Fact _) = Position.none; 

91 

26361  92 
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

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

94 

49887  95 
fun string_of_selection NONE = "" 
96 
 string_of_selection (SOME is) = enclose "(" ")" (commas (map string_of_interval is)); 

97 

98 
fun string_of_ref (Named ((name, _), sel)) = name ^ string_of_selection sel 

99 
 string_of_ref (Fact _) = raise Fail "Illegal literal fact"; 

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

100 

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

101 

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

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

103 

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

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

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

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

108 
val n = length ths; 
26361  109 
fun err msg = 
55740  110 
error (msg ^ " for fact " ^ quote name ^ " (length " ^ string_of_int n ^ ")" ^ 
48992  111 
Position.here pos); 
26336
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26307
diff
changeset

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

113 
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

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

115 
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

116 
in map sel is end; 
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 
(* selections *) 
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26307
diff
changeset

120 

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

123 
(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

124 

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

125 

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

126 

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

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

128 

26393  129 
(* datatypes *) 
130 

131 
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

132 

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

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

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

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

136 

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

137 
fun make_facts facts props = Facts {facts = facts, props = props}; 
33163  138 

33096  139 
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

140 

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

141 

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

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

143 

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

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

145 

56025  146 
val space_of = Name_Space.space_of_table o facts_of; 
26393  147 

57887  148 
fun alias naming binding name (Facts {facts, props}) = 
149 
make_facts (Name_Space.alias_table naming binding name facts) props; 

150 

33163  151 
val is_concealed = Name_Space.is_concealed o space_of; 
152 

56003  153 
fun check context facts (xname, pos) = 
154 
let 

155 
val (name, fact) = Name_Space.check context (facts_of facts) (xname, pos); 

156 
val _ = 

157 
(case fact of 

158 
Static _ => () 

159 
 Dynamic _ => Context_Position.report_generic context pos (Markup.dynamic_fact name)); 

160 
in name end; 

161 

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

162 
val intern = Name_Space.intern o space_of; 
42358
b47d41d9f4b5
Name_Space: proper configuration options long_names, short_names, unique_names instead of former unsynchronized references;
wenzelm
parents:
35408
diff
changeset

163 
fun extern ctxt = Name_Space.extern ctxt o space_of; 
57887  164 
fun markup_extern ctxt = Name_Space.markup_extern ctxt o space_of; 
26664
167d879a89b0
renamed dest to dest_table, and extern to extern table;
wenzelm
parents:
26654
diff
changeset

165 

56158
c2c6d560e7b2
more explicit treatment of verbose mode, which includes concealed entries;
wenzelm
parents:
56140
diff
changeset

166 

c2c6d560e7b2
more explicit treatment of verbose mode, which includes concealed entries;
wenzelm
parents:
56140
diff
changeset

167 
(* retrieve *) 
c2c6d560e7b2
more explicit treatment of verbose mode, which includes concealed entries;
wenzelm
parents:
56140
diff
changeset

168 

59883  169 
val defined = Name_Space.defined o facts_of; 
26692  170 

26393  171 
fun lookup context facts name = 
56025  172 
(case Name_Space.lookup_key (facts_of facts) name of 
26393  173 
NONE => NONE 
56025  174 
 SOME (_, Static ths) => SOME (true, ths) 
175 
 SOME (_, Dynamic f) => SOME (false, f context)); 

26393  176 

56140
ed92ce2ac88e
just one cumulative Proof_Context.facts, with uniform retrieval (including PIDE markup, completion etc.);
wenzelm
parents:
56137
diff
changeset

177 
fun retrieve context facts (xname, pos) = 
ed92ce2ac88e
just one cumulative Proof_Context.facts, with uniform retrieval (including PIDE markup, completion etc.);
wenzelm
parents:
56137
diff
changeset

178 
let 
ed92ce2ac88e
just one cumulative Proof_Context.facts, with uniform retrieval (including PIDE markup, completion etc.);
wenzelm
parents:
56137
diff
changeset

179 
val name = check context facts (xname, pos); 
57942
e5bec882fdd0
more informative Token.Fact: retain name of dynamic fact (without selection);
wenzelm
parents:
57887
diff
changeset

180 
val (static, thms) = 
56140
ed92ce2ac88e
just one cumulative Proof_Context.facts, with uniform retrieval (including PIDE markup, completion etc.);
wenzelm
parents:
56137
diff
changeset

181 
(case lookup context facts name of 
ed92ce2ac88e
just one cumulative Proof_Context.facts, with uniform retrieval (including PIDE markup, completion etc.);
wenzelm
parents:
56137
diff
changeset

182 
SOME (static, thms) => 
ed92ce2ac88e
just one cumulative Proof_Context.facts, with uniform retrieval (including PIDE markup, completion etc.);
wenzelm
parents:
56137
diff
changeset

183 
(if static then () 
ed92ce2ac88e
just one cumulative Proof_Context.facts, with uniform retrieval (including PIDE markup, completion etc.);
wenzelm
parents:
56137
diff
changeset

184 
else Context_Position.report_generic context pos (Markup.dynamic_fact name); 
57942
e5bec882fdd0
more informative Token.Fact: retain name of dynamic fact (without selection);
wenzelm
parents:
57887
diff
changeset

185 
(static, thms)) 
56140
ed92ce2ac88e
just one cumulative Proof_Context.facts, with uniform retrieval (including PIDE markup, completion etc.);
wenzelm
parents:
56137
diff
changeset

186 
 NONE => error ("Unknown fact " ^ quote name ^ Position.here pos)); 
57942
e5bec882fdd0
more informative Token.Fact: retain name of dynamic fact (without selection);
wenzelm
parents:
57887
diff
changeset

187 
in 
e5bec882fdd0
more informative Token.Fact: retain name of dynamic fact (without selection);
wenzelm
parents:
57887
diff
changeset

188 
{name = name, 
e5bec882fdd0
more informative Token.Fact: retain name of dynamic fact (without selection);
wenzelm
parents:
57887
diff
changeset

189 
static = static, 
e5bec882fdd0
more informative Token.Fact: retain name of dynamic fact (without selection);
wenzelm
parents:
57887
diff
changeset

190 
thms = map (Thm.transfer (Context.theory_of context)) thms} 
e5bec882fdd0
more informative Token.Fact: retain name of dynamic fact (without selection);
wenzelm
parents:
57887
diff
changeset

191 
end; 
56140
ed92ce2ac88e
just one cumulative Proof_Context.facts, with uniform retrieval (including PIDE markup, completion etc.);
wenzelm
parents:
56137
diff
changeset

192 

56158
c2c6d560e7b2
more explicit treatment of verbose mode, which includes concealed entries;
wenzelm
parents:
56140
diff
changeset

193 

c2c6d560e7b2
more explicit treatment of verbose mode, which includes concealed entries;
wenzelm
parents:
56140
diff
changeset

194 
(* static content *) 
c2c6d560e7b2
more explicit treatment of verbose mode, which includes concealed entries;
wenzelm
parents:
56140
diff
changeset

195 

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

196 
fun fold_static f = 
56025  197 
Name_Space.fold_table (fn (name, Static ths) => f (name, ths)  _ => I) o facts_of; 
26393  198 

56158
c2c6d560e7b2
more explicit treatment of verbose mode, which includes concealed entries;
wenzelm
parents:
56140
diff
changeset

199 
fun dest_static verbose prev_facts facts = 
27175  200 
fold_static (fn (name, ths) => 
56158
c2c6d560e7b2
more explicit treatment of verbose mode, which includes concealed entries;
wenzelm
parents:
56140
diff
changeset

201 
if exists (fn prev => defined prev name) prev_facts orelse 
c2c6d560e7b2
more explicit treatment of verbose mode, which includes concealed entries;
wenzelm
parents:
56140
diff
changeset

202 
not verbose andalso is_concealed facts name then I 
c2c6d560e7b2
more explicit treatment of verbose mode, which includes concealed entries;
wenzelm
parents:
56140
diff
changeset

203 
else cons (name, ths)) facts [] 
c2c6d560e7b2
more explicit treatment of verbose mode, which includes concealed entries;
wenzelm
parents:
56140
diff
changeset

204 
> sort_wrt #1; 
26281
328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset

205 

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

206 

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

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

208 

59058
a78612c67ec0
renamed "pairself" to "apply2", in accordance to @{apply 2};
wenzelm
parents:
57942
diff
changeset

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

210 

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

211 
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

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

213 

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

214 

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

216 

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

217 
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

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

219 
val facts' = Name_Space.merge_tables (facts1, facts2); 
56137
af71fb1cb31f
minor tuning  NB: props are usually empty for global facts;
wenzelm
parents:
56025
diff
changeset

220 
val props' = 
af71fb1cb31f
minor tuning  NB: props are usually empty for global facts;
wenzelm
parents:
56025
diff
changeset

221 
if Net.is_empty props2 then props1 
af71fb1cb31f
minor tuning  NB: props are usually empty for global facts;
wenzelm
parents:
56025
diff
changeset

222 
else if Net.is_empty props1 then props2 
af71fb1cb31f
minor tuning  NB: props are usually empty for global facts;
wenzelm
parents:
56025
diff
changeset

223 
else Net.merge (is_equal o prop_ord) (props1, props2); (*beware of noncanonical merge*) 
26281
328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset

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

225 

26393  226 

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

227 
(* add static entries *) 
26393  228 

49747  229 
fun add_static context {strict, index} (b, ths) (Facts {facts, props}) = 
26281
328fd1c551ef
Environment of named facts (admits overriding). Optional indexing by proposition.
wenzelm
parents:
diff
changeset

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

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

232 
if Binding.is_empty b then ("", facts) 
47005
421760a1efe7
maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
wenzelm
parents:
42375
diff
changeset

233 
else Name_Space.define context strict (b, Static ths) facts; 
49747  234 
val props' = props 
235 
> index ? fold (fn th => Net.insert_term (K false) (Thm.full_prop_of th, th)) ths; 

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

237 

26393  238 

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

239 
(* add dynamic entries *) 
26393  240 

47005
421760a1efe7
maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
wenzelm
parents:
42375
diff
changeset

241 
fun add_dynamic context (b, f) (Facts {facts, props}) = 
421760a1efe7
maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
wenzelm
parents:
42375
diff
changeset

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

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

244 

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

245 

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

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

247 

56025  248 
fun del name (Facts {facts, props}) = 
249 
make_facts (Name_Space.del_table name facts) props; 

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

250 

56025  251 
fun hide fully name (Facts {facts, props}) = 
252 
make_facts (Name_Space.hide_table fully name facts) props; 

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

253 

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

254 
end; 