wenzelm@26281: (*  Title:      Pure/facts.ML
wenzelm@26281:     ID:         $Id$
wenzelm@26281:     Author:     Makarius
wenzelm@26281: 
wenzelm@26307: Environment of named facts, optionally indexed by proposition.
wenzelm@26281: *)
wenzelm@26281: 
wenzelm@26281: signature FACTS =
wenzelm@26281: sig
wenzelm@26336:   val the_single: string -> thm list -> thm
wenzelm@26336:   datatype interval = FromTo of int * int | From of int | Single of int
wenzelm@26336:   datatype ref =
wenzelm@26361:     Named of (string * Position.T) * interval list option |
wenzelm@26336:     Fact of string
wenzelm@26361:   val named: string -> ref
wenzelm@26336:   val string_of_ref: ref -> string
wenzelm@26336:   val name_of_ref: ref -> string
wenzelm@26366:   val pos_of_ref: ref -> Position.T
wenzelm@26336:   val map_name_of_ref: (string -> string) -> ref -> ref
wenzelm@26336:   val select: ref -> thm list -> thm list
wenzelm@26336:   val selections: string * thm list -> (ref * thm) list
wenzelm@26281:   type T
wenzelm@26393:   val empty: T
wenzelm@26664:   val intern: T -> xstring -> string
wenzelm@26664:   val extern: T -> string -> xstring
wenzelm@26393:   val lookup: Context.generic -> T -> string -> thm list option
wenzelm@26692:   val defined: T -> string -> bool
wenzelm@26692:   val fold_static: (string * thm list -> 'a -> 'a) -> T -> 'a -> 'a
wenzelm@26692:   val dest_static: T -> (string * thm list) list
wenzelm@26692:   val extern_static: T -> (xstring * thm list) list
wenzelm@26281:   val props: T -> thm list
wenzelm@26281:   val could_unify: T -> term -> thm list
wenzelm@26281:   val merge: T * T -> T
wenzelm@26307:   val add_global: NameSpace.naming -> string * thm list -> T -> T
wenzelm@26307:   val add_local: bool -> NameSpace.naming -> string * thm list -> T -> T
wenzelm@26393:   val add_dynamic: NameSpace.naming -> string * (Context.generic -> thm list) -> T -> T
wenzelm@26654:   val del: string -> T -> T
wenzelm@26654:   val hide: bool -> string -> T -> T
wenzelm@26281: end;
wenzelm@26281: 
wenzelm@26281: structure Facts: FACTS =
wenzelm@26281: struct
wenzelm@26281: 
wenzelm@26336: (** fact references **)
wenzelm@26336: 
wenzelm@26336: fun the_single _ [th] : thm = th
wenzelm@26336:   | the_single name _ = error ("Single theorem expected " ^ quote name);
wenzelm@26336: 
wenzelm@26336: 
wenzelm@26336: (* datatype interval *)
wenzelm@26336: 
wenzelm@26336: datatype interval =
wenzelm@26336:   FromTo of int * int |
wenzelm@26336:   From of int |
wenzelm@26336:   Single of int;
wenzelm@26336: 
wenzelm@26336: fun string_of_interval (FromTo (i, j)) = string_of_int i ^ "-" ^ string_of_int j
wenzelm@26336:   | string_of_interval (From i) = string_of_int i ^ "-"
wenzelm@26336:   | string_of_interval (Single i) = string_of_int i;
wenzelm@26336: 
wenzelm@26336: fun interval n iv =
wenzelm@26336:   let fun err () = raise Fail ("Bad interval specification " ^ string_of_interval iv) in
wenzelm@26336:     (case iv of
wenzelm@26336:       FromTo (i, j) => if i <= j then i upto j else err ()
wenzelm@26336:     | From i => if i <= n then i upto n else err ()
wenzelm@26336:     | Single i => [i])
wenzelm@26336:   end;
wenzelm@26336: 
wenzelm@26336: 
wenzelm@26336: (* datatype ref *)
wenzelm@26336: 
wenzelm@26336: datatype ref =
wenzelm@26361:   Named of (string * Position.T) * interval list option |
wenzelm@26336:   Fact of string;
wenzelm@26336: 
wenzelm@26361: fun named name = Named ((name, Position.none), NONE);
wenzelm@26361: 
wenzelm@26366: fun name_pos_of_ref (Named (name_pos, _)) = name_pos
wenzelm@26366:   | name_pos_of_ref (Fact _) = error "Illegal literal fact";
wenzelm@26366: 
wenzelm@26366: val name_of_ref = #1 o name_pos_of_ref;
wenzelm@26366: val pos_of_ref = #2 o name_pos_of_ref;
wenzelm@26336: 
wenzelm@26361: fun map_name_of_ref f (Named ((name, pos), is)) = Named ((f name, pos), is)
wenzelm@26336:   | map_name_of_ref _ r = r;
wenzelm@26336: 
wenzelm@26361: fun string_of_ref (Named ((name, _), NONE)) = name
wenzelm@26361:   | string_of_ref (Named ((name, _), SOME is)) =
wenzelm@26336:       name ^ enclose "(" ")" (commas (map string_of_interval is))
wenzelm@26336:   | string_of_ref (Fact _) = error "Illegal literal fact";
wenzelm@26336: 
wenzelm@26336: 
wenzelm@26336: (* select *)
wenzelm@26336: 
wenzelm@26336: fun select (Fact _) ths = ths
wenzelm@26336:   | select (Named (_, NONE)) ths = ths
wenzelm@26361:   | select (Named ((name, pos), SOME ivs)) ths =
wenzelm@26336:       let
wenzelm@26336:         val n = length ths;
wenzelm@26361:         fun err msg =
wenzelm@26361:           error (msg ^ " for " ^ quote name ^ " (length " ^ string_of_int n ^ ")" ^
wenzelm@26361:             Position.str_of pos);
wenzelm@26336:         fun sel i =
wenzelm@26336:           if i < 1 orelse i > n then err ("Bad subscript " ^ string_of_int i)
wenzelm@26336:           else nth ths (i - 1);
wenzelm@26336:         val is = maps (interval n) ivs handle Fail msg => err msg;
wenzelm@26336:       in map sel is end;
wenzelm@26336: 
wenzelm@26336: 
wenzelm@26336: (* selections *)
wenzelm@26336: 
wenzelm@26361: fun selections (name, [th]) = [(Named ((name, Position.none), NONE), th)]
wenzelm@26361:   | selections (name, ths) = map2 (fn i => fn th =>
wenzelm@26361:       (Named ((name, Position.none), SOME [Single i]), th)) (1 upto length ths) ths;
wenzelm@26336: 
wenzelm@26336: 
wenzelm@26336: 
wenzelm@26336: (** fact environment **)
wenzelm@26336: 
wenzelm@26393: (* datatypes *)
wenzelm@26393: 
wenzelm@26393: datatype fact = Static of thm list | Dynamic of Context.generic -> thm list;
wenzelm@26281: 
wenzelm@26281: datatype T = Facts of
wenzelm@26393:  {facts: (fact * serial) NameSpace.table,
wenzelm@26281:   props: thm Net.net};
wenzelm@26281: 
wenzelm@26281: fun make_facts facts props = Facts {facts = facts, props = props};
wenzelm@26393: val empty = make_facts NameSpace.empty_table Net.empty;
wenzelm@26281: 
wenzelm@26281: 
wenzelm@26281: (* named facts *)
wenzelm@26281: 
wenzelm@26281: fun facts_of (Facts {facts, ...}) = facts;
wenzelm@26281: 
wenzelm@26281: val space_of = #1 o facts_of;
wenzelm@26393: val table_of = #2 o facts_of;
wenzelm@26393: 
wenzelm@26664: val intern = NameSpace.intern o space_of;
wenzelm@26664: val extern = NameSpace.extern o space_of;
wenzelm@26664: 
wenzelm@26692: val defined = Symtab.defined o table_of;
wenzelm@26692: 
wenzelm@26393: fun lookup context facts name =
wenzelm@26393:   (case Symtab.lookup (table_of facts) name of
wenzelm@26393:     NONE => NONE
wenzelm@26393:   | SOME (Static ths, _) => SOME ths
wenzelm@26393:   | SOME (Dynamic f, _) => SOME (f context));
wenzelm@26393: 
wenzelm@26692: fun fold_static f = Symtab.fold (fn (name, (Static ths, _)) => f (name, ths) | _ => I) o table_of;
wenzelm@26393: 
wenzelm@26692: fun dest_static facts = sort_wrt #1 (fold_static cons facts []);
wenzelm@26692: fun extern_static facts =
wenzelm@26692:   sort_wrt #1 (fold_static (fn (name, ths) => cons (extern facts name, ths)) facts []);
wenzelm@26281: 
wenzelm@26281: 
wenzelm@26281: (* indexed props *)
wenzelm@26281: 
wenzelm@26281: val prop_ord = Term.term_ord o pairself Thm.full_prop_of;
wenzelm@26281: 
wenzelm@26281: fun props (Facts {props, ...}) = sort_distinct prop_ord (Net.content props);
wenzelm@26281: fun could_unify (Facts {props, ...}) = Net.unify_term props;
wenzelm@26281: 
wenzelm@26281: 
wenzelm@26393: (* merge facts *)
wenzelm@26281: 
wenzelm@26393: fun err_dup_fact name = error ("Duplicate fact " ^ quote name);
wenzelm@26281: 
wenzelm@26654: fun eq_entry ((Static ths1, _), (Static ths2, _)) = is_equal (list_ord Thm.thm_ord (ths1, ths2))
wenzelm@26654:   | eq_entry ((_, id1: serial), (_, id2)) = id1 = id2;
wenzelm@26654: 
wenzelm@26281: fun merge (Facts {facts = facts1, props = props1}, Facts {facts = facts2, props = props2}) =
wenzelm@26281:   let
wenzelm@26654:     val facts' = NameSpace.merge_tables eq_entry (facts1, facts2)
wenzelm@26654:       handle Symtab.DUP dup => err_dup_fact dup;
wenzelm@26281:     val props' = Net.merge (is_equal o prop_ord) (props1, props2);
wenzelm@26281:   in make_facts facts' props' end;
wenzelm@26281: 
wenzelm@26393: 
wenzelm@26654: (* add static entries *)
wenzelm@26393: 
wenzelm@26307: fun add permissive do_props naming (name, ths) (Facts {facts, props}) =
wenzelm@26281:   let
wenzelm@26281:     val facts' =
wenzelm@26281:       if name = "" then facts
wenzelm@26281:       else
wenzelm@26281:         let
wenzelm@26281:           val (space, tab) = facts;
wenzelm@26281:           val space' = NameSpace.declare naming name space;
wenzelm@26393:           val entry = (name, (Static ths, serial ()));
wenzelm@26393:           val tab' = (if permissive then Symtab.update else Symtab.update_new) entry tab
wenzelm@26654:             handle Symtab.DUP dup => err_dup_fact dup;
wenzelm@26281:         in (space', tab') end;
wenzelm@26281:     val props' =
wenzelm@26281:       if do_props then fold (fn th => Net.insert_term (K false) (Thm.full_prop_of th, th)) ths props
wenzelm@26281:       else props;
wenzelm@26281:   in make_facts facts' props' end;
wenzelm@26281: 
wenzelm@26307: val add_global = add false false;
wenzelm@26307: val add_local = add true;
wenzelm@26307: 
wenzelm@26393: 
wenzelm@26654: (* add dynamic entries *)
wenzelm@26393: 
wenzelm@26393: fun add_dynamic naming (name, f) (Facts {facts = (space, tab), props}) =
wenzelm@26290:   let
wenzelm@26393:     val space' = NameSpace.declare naming name space;
wenzelm@26393:     val entry = (name, (Dynamic f, serial ()));
wenzelm@26393:     val tab' = Symtab.update_new entry tab
wenzelm@26393:       handle Symtab.DUP dup => err_dup_fact dup;
wenzelm@26290:   in make_facts (space', tab') props end;
wenzelm@26281: 
wenzelm@26654: 
wenzelm@26654: (* remove entries *)
wenzelm@26654: 
wenzelm@26654: fun del name (Facts {facts = (space, tab), props}) =
wenzelm@26654:   let
wenzelm@26654:     val space' = NameSpace.hide true name space handle ERROR _ => space;
wenzelm@26654:     val tab' = Symtab.delete_safe name tab;
wenzelm@26654:   in make_facts (space', tab') props end;
wenzelm@26654: 
wenzelm@26654: fun hide fully name (Facts {facts = (space, tab), props}) =
wenzelm@26654:   make_facts (NameSpace.hide fully name space, tab) props;
wenzelm@26654: 
wenzelm@26281: end;