src/Pure/facts.ML

added thread data (formerly global ref in ML/ml_context.ML);
renamed ML_Context.>> to Context.>> (again);

(*  Title:      Pure/facts.ML
    ID:         $Id$
    Author:     Makarius

Environment of named facts, optionally indexed by proposition.
*)

signature FACTS =
sig
  val the_single: string -> thm list -> thm
  datatype interval = FromTo of int * int | From of int | Single of int
  datatype ref =
    Named of (string * Position.T) * interval list option |
    Fact of string
  val named: string -> ref
  val string_of_ref: ref -> string
  val name_of_ref: ref -> string
  val pos_of_ref: ref -> Position.T
  val map_name_of_ref: (string -> string) -> ref -> ref
  val select: ref -> thm list -> thm list
  val selections: string * thm list -> (ref * thm) list
  type T
  val empty: T
  val space_of: T -> NameSpace.T
  val lookup: Context.generic -> T -> string -> thm list option
  val dest: T -> (string * thm list) list
  val extern: T -> (xstring * thm list) list
  val props: T -> thm list
  val could_unify: T -> term -> thm list
  val merge: T * T -> T
  val del: string -> T -> T
  val add_global: NameSpace.naming -> string * thm list -> T -> T
  val add_local: bool -> NameSpace.naming -> string * thm list -> T -> T
  val add_dynamic: NameSpace.naming -> string * (Context.generic -> thm list) -> T -> T
end;

structure Facts: FACTS =
struct

(** fact references **)

fun the_single _ [th] : thm = th
  | the_single name _ = error ("Single theorem expected " ^ quote name);


(* datatype interval *)

datatype interval =
  FromTo of int * int |
  From of int |
  Single of int;

fun string_of_interval (FromTo (i, j)) = string_of_int i ^ "-" ^ string_of_int j
  | string_of_interval (From i) = string_of_int i ^ "-"
  | string_of_interval (Single i) = string_of_int i;

fun interval n iv =
  let fun err () = raise Fail ("Bad interval specification " ^ string_of_interval iv) in
    (case iv of
      FromTo (i, j) => if i <= j then i upto j else err ()
    | From i => if i <= n then i upto n else err ()
    | Single i => [i])
  end;


(* datatype ref *)

datatype ref =
  Named of (string * Position.T) * interval list option |
  Fact of string;

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

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

val name_of_ref = #1 o name_pos_of_ref;
val pos_of_ref = #2 o name_pos_of_ref;

fun map_name_of_ref f (Named ((name, pos), is)) = Named ((f name, pos), is)
  | map_name_of_ref _ r = r;

fun string_of_ref (Named ((name, _), NONE)) = name
  | string_of_ref (Named ((name, _), SOME is)) =
      name ^ enclose "(" ")" (commas (map string_of_interval is))
  | string_of_ref (Fact _) = error "Illegal literal fact";


(* select *)

fun select (Fact _) ths = ths
  | select (Named (_, NONE)) ths = ths
  | select (Named ((name, pos), SOME ivs)) ths =
      let
        val n = length ths;
        fun err msg =
          error (msg ^ " for " ^ quote name ^ " (length " ^ string_of_int n ^ ")" ^
            Position.str_of pos);
        fun sel i =
          if i < 1 orelse i > n then err ("Bad subscript " ^ string_of_int i)
          else nth ths (i - 1);
        val is = maps (interval n) ivs handle Fail msg => err msg;
      in map sel is end;


(* selections *)

fun selections (name, [th]) = [(Named ((name, Position.none), NONE), th)]
  | selections (name, ths) = map2 (fn i => fn th =>
      (Named ((name, Position.none), SOME [Single i]), th)) (1 upto length ths) ths;



(** fact environment **)

(* datatypes *)

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

datatype T = Facts of
 {facts: (fact * serial) NameSpace.table,
  props: thm Net.net};

fun make_facts facts props = Facts {facts = facts, props = props};
val empty = make_facts NameSpace.empty_table Net.empty;


(* named facts *)

fun facts_of (Facts {facts, ...}) = facts;

val space_of = #1 o facts_of;
val table_of = #2 o facts_of;

fun lookup context facts name =
  (case Symtab.lookup (table_of facts) name of
    NONE => NONE
  | SOME (Static ths, _) => SOME ths
  | SOME (Dynamic f, _) => SOME (f context));

fun dest facts =
  Symtab.fold (fn (name, (Static ths, _)) => cons (name, ths) | _ => I) (table_of facts) [];

fun extern facts =
  dest facts
  |> map (apfst (NameSpace.extern (space_of facts)))
  |> sort_wrt #1;


(* indexed props *)

val prop_ord = Term.term_ord o pairself Thm.full_prop_of;

fun props (Facts {props, ...}) = sort_distinct prop_ord (Net.content props);
fun could_unify (Facts {props, ...}) = Net.unify_term props;


(* merge facts *)

fun err_dup_fact name = error ("Duplicate fact " ^ quote name);

fun merge (Facts {facts = facts1, props = props1}, Facts {facts = facts2, props = props2}) =
  let
    (* FIXME authentic version
    val facts' = NameSpace.merge_tables (eq_snd (op =)) (facts1, facts2)
      handle Symtab.DUP dup => err_dup_fact dup; *)
    val facts' = NameSpace.merge_tables (K true) (facts1, facts2)
    val props' = Net.merge (is_equal o prop_ord) (props1, props2);
  in make_facts facts' props' end;


(* static entries *)

fun del name (Facts {facts = (space, tab), props}) =
  let
    val space' = NameSpace.hide true name space handle ERROR _ => space;
    val tab' = Symtab.delete_safe name tab;
  in make_facts (space', tab') props end;

fun add permissive do_props naming (name, ths) (Facts {facts, props}) =
  let
    val facts' =
      if name = "" then facts
      else
        let
          val (space, tab) = facts;
          val space' = NameSpace.declare naming name space;
          val entry = (name, (Static ths, serial ()));
          val tab' = (if permissive then Symtab.update else Symtab.update_new) entry tab
            handle Symtab.DUP dup => (legacy_feature ("Duplicate fact " ^ quote dup ^
              Position.str_of (Position.thread_data ())); tab);
        in (space', tab') end;
    val props' =
      if do_props then fold (fn th => Net.insert_term (K false) (Thm.full_prop_of th, th)) ths props
      else props;
  in make_facts facts' props' end;

val add_global = add false false;
val add_local = add true;


(* dynamic entries *)

fun add_dynamic naming (name, f) (Facts {facts = (space, tab), props}) =
  let
    val space' = NameSpace.declare naming name space;
    val entry = (name, (Dynamic f, serial ()));
    val tab' = Symtab.update_new entry tab
      handle Symtab.DUP dup => err_dup_fact dup;
  in make_facts (space', tab') props end;

end;