maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
more explicit Context.generic for Name_Space.declare/define and derivatives (NB: naming changed after Proof_Context.init_global);
prefer Context.pretty in low-level operations of structure Sorts/Type (defer full Syntax.init_pretty until error output);
simplified signatures;
1 (* Title: Pure/facts.ML
4 Environment of named facts, optionally indexed by proposition.
9 val the_single: string -> thm list -> thm
10 datatype interval = FromTo of int * int | From of int | Single of int
12 Named of (string * Position.T) * interval list option |
14 val named: string -> ref
15 val string_of_ref: ref -> string
16 val name_of_ref: ref -> string
17 val pos_of_ref: ref -> Position.T
18 val map_name_of_ref: (string -> string) -> ref -> ref
19 val select: ref -> thm list -> thm list
20 val selections: string * thm list -> (ref * thm) list
23 val space_of: T -> Name_Space.T
24 val is_concealed: T -> string -> bool
25 val intern: T -> xstring -> string
26 val extern: Proof.context -> T -> string -> xstring
27 val lookup: Context.generic -> T -> string -> (bool * thm list) option
28 val defined: T -> string -> bool
29 val fold_static: (string * thm list -> 'a -> 'a) -> T -> 'a -> 'a
30 val dest_static: T list -> T -> (string * thm list) list
31 val extern_static: Proof.context -> T list -> T -> (xstring * thm list) list
32 val props: T -> thm list
33 val could_unify: T -> term -> thm list
35 val add_global: Context.generic -> binding * thm list -> T -> string * T
36 val add_local: Context.generic -> bool -> binding * thm list -> T -> string * T
37 val add_dynamic: Context.generic -> binding * (Context.generic -> thm list) -> T -> string * T
38 val del: string -> T -> T
39 val hide: bool -> string -> T -> T
42 structure Facts: FACTS =
45 (** fact references **)
47 fun the_single _ [th] : thm = th
48 | the_single name _ = error ("Expected singleton fact " ^ quote name);
51 (* datatype interval *)
58 fun string_of_interval (FromTo (i, j)) = string_of_int i ^ "-" ^ string_of_int j
59 | string_of_interval (From i) = string_of_int i ^ "-"
60 | string_of_interval (Single i) = string_of_int i;
63 let fun err () = raise Fail ("Bad interval specification " ^ string_of_interval iv) in
65 FromTo (i, j) => if i <= j then i upto j else err ()
66 | From i => if i <= n then i upto n else err ()
74 Named of (string * Position.T) * interval list option |
77 fun named name = Named ((name, Position.none), NONE);
79 fun name_pos_of_ref (Named (name_pos, _)) = name_pos
80 | name_pos_of_ref (Fact _) = error "Illegal literal fact";
82 val name_of_ref = #1 o name_pos_of_ref;
83 val pos_of_ref = #2 o name_pos_of_ref;
85 fun map_name_of_ref f (Named ((name, pos), is)) = Named ((f name, pos), is)
86 | map_name_of_ref _ r = r;
88 fun string_of_ref (Named ((name, _), NONE)) = name
89 | string_of_ref (Named ((name, _), SOME is)) =
90 name ^ enclose "(" ")" (commas (map string_of_interval is))
91 | string_of_ref (Fact _) = error "Illegal literal fact";
96 fun select (Fact _) ths = ths
97 | select (Named (_, NONE)) ths = ths
98 | select (Named ((name, pos), SOME ivs)) ths =
102 error (msg ^ " for " ^ quote name ^ " (length " ^ string_of_int n ^ ")" ^
103 Position.str_of pos);
105 if i < 1 orelse i > n then err ("Bad subscript " ^ string_of_int i)
106 else nth ths (i - 1);
107 val is = maps (interval n) ivs handle Fail msg => err msg;
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;
119 (** fact environment **)
123 datatype fact = Static of thm list | Dynamic of Context.generic -> thm list;
125 datatype T = Facts of
126 {facts: fact Name_Space.table,
129 fun make_facts facts props = Facts {facts = facts, props = props};
131 val empty = make_facts (Name_Space.empty_table "fact") Net.empty;
136 fun facts_of (Facts {facts, ...}) = facts;
138 val space_of = #1 o facts_of;
139 val table_of = #2 o facts_of;
141 val is_concealed = Name_Space.is_concealed o space_of;
143 val intern = Name_Space.intern o space_of;
144 fun extern ctxt = Name_Space.extern ctxt o space_of;
146 val defined = Symtab.defined o table_of;
148 fun lookup context facts name =
149 (case Symtab.lookup (table_of facts) name of
151 | SOME (Static ths) => SOME (true, ths)
152 | SOME (Dynamic f) => SOME (false, f context));
155 Symtab.fold (fn (name, Static ths) => f (name, ths) | _ => I) o table_of;
158 (* content difference *)
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 [];
165 fun dest_static prev_facts facts =
166 sort_wrt #1 (diff_table prev_facts facts);
168 fun extern_static ctxt prev_facts facts =
169 sort_wrt #1 (diff_table prev_facts facts |> map (apfst (extern ctxt facts)));
174 val prop_ord = Term_Ord.term_ord o pairself Thm.full_prop_of;
176 fun props (Facts {props, ...}) = sort_distinct prop_ord (Net.content props);
177 fun could_unify (Facts {props, ...}) = Net.unify_term props;
182 fun merge (Facts {facts = facts1, props = props1}, Facts {facts = facts2, props = props2}) =
184 val facts' = Name_Space.merge_tables (facts1, facts2);
185 val props' = Net.merge (is_equal o prop_ord) (props1, props2);
186 in make_facts facts' props' end;
189 (* add static entries *)
193 fun add context strict do_props (b, ths) (Facts {facts, props}) =
196 if Binding.is_empty b then ("", facts)
197 else Name_Space.define context strict (b, Static ths) facts;
200 then fold (fn th => Net.insert_term (K false) (Thm.full_prop_of th, th)) ths props
202 in (name, make_facts facts' props') end;
206 fun add_global context = add context true false;
207 fun add_local context = add context false;
212 (* add dynamic entries *)
214 fun add_dynamic context (b, f) (Facts {facts, props}) =
215 let val (name, facts') = Name_Space.define context true (b, Dynamic f) facts;
216 in (name, make_facts facts' props) end;
221 fun del name (Facts {facts = (space, tab), props}) =
223 val space' = Name_Space.hide true name space handle ERROR _ => space;
224 val tab' = Symtab.delete_safe name tab;
225 in make_facts (space', tab') props end;
227 fun hide fully name (Facts {facts = (space, tab), props}) =
228 make_facts (Name_Space.hide fully name space, tab) props;