src/Pure/facts.ML
author haftmann
Wed Jan 21 16:47:32 2009 +0100 (2009-01-21)
changeset 29581 b3b33e0298eb
parent 29269 5c25a2012975
child 29848 a7c164e228e1
permissions -rw-r--r--
binding is alias for Binding.T
     1 (*  Title:      Pure/facts.ML
     2     Author:     Makarius
     3 
     4 Environment of named facts, optionally indexed by proposition.
     5 *)
     6 
     7 signature FACTS =
     8 sig
     9   val the_single: string -> thm list -> thm
    10   datatype interval = FromTo of int * int | From of int | Single of int
    11   datatype ref =
    12     Named of (string * Position.T) * interval list option |
    13     Fact of string
    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
    21   type T
    22   val empty: T
    23   val intern: T -> xstring -> string
    24   val extern: T -> string -> xstring
    25   val lookup: Context.generic -> T -> string -> (bool * thm list) option
    26   val defined: T -> string -> bool
    27   val fold_static: (string * thm list -> 'a -> 'a) -> T -> 'a -> 'a
    28   val dest_static: T list -> T -> (string * thm list) list
    29   val extern_static: T list -> T -> (xstring * thm list) list
    30   val props: T -> thm list
    31   val could_unify: T -> term -> thm list
    32   val merge: T * T -> T
    33   val add_global: NameSpace.naming -> binding * thm list -> T -> string * T
    34   val add_local: bool -> NameSpace.naming -> binding * thm list -> T -> string * T
    35   val add_dynamic: NameSpace.naming -> binding * (Context.generic -> thm list) -> T -> string * T
    36   val del: string -> T -> T
    37   val hide: bool -> string -> T -> T
    38 end;
    39 
    40 structure Facts: FACTS =
    41 struct
    42 
    43 (** fact references **)
    44 
    45 fun the_single _ [th] : thm = th
    46   | the_single name _ = error ("Single theorem expected " ^ quote name);
    47 
    48 
    49 (* datatype interval *)
    50 
    51 datatype interval =
    52   FromTo of int * int |
    53   From of int |
    54   Single of int;
    55 
    56 fun string_of_interval (FromTo (i, j)) = string_of_int i ^ "-" ^ string_of_int j
    57   | string_of_interval (From i) = string_of_int i ^ "-"
    58   | string_of_interval (Single i) = string_of_int i;
    59 
    60 fun interval n iv =
    61   let fun err () = raise Fail ("Bad interval specification " ^ string_of_interval iv) in
    62     (case iv of
    63       FromTo (i, j) => if i <= j then i upto j else err ()
    64     | From i => if i <= n then i upto n else err ()
    65     | Single i => [i])
    66   end;
    67 
    68 
    69 (* datatype ref *)
    70 
    71 datatype ref =
    72   Named of (string * Position.T) * interval list option |
    73   Fact of string;
    74 
    75 fun named name = Named ((name, Position.none), NONE);
    76 
    77 fun name_pos_of_ref (Named (name_pos, _)) = name_pos
    78   | name_pos_of_ref (Fact _) = error "Illegal literal fact";
    79 
    80 val name_of_ref = #1 o name_pos_of_ref;
    81 val pos_of_ref = #2 o name_pos_of_ref;
    82 
    83 fun map_name_of_ref f (Named ((name, pos), is)) = Named ((f name, pos), is)
    84   | map_name_of_ref _ r = r;
    85 
    86 fun string_of_ref (Named ((name, _), NONE)) = name
    87   | string_of_ref (Named ((name, _), SOME is)) =
    88       name ^ enclose "(" ")" (commas (map string_of_interval is))
    89   | string_of_ref (Fact _) = error "Illegal literal fact";
    90 
    91 
    92 (* select *)
    93 
    94 fun select (Fact _) ths = ths
    95   | select (Named (_, NONE)) ths = ths
    96   | select (Named ((name, pos), SOME ivs)) ths =
    97       let
    98         val n = length ths;
    99         fun err msg =
   100           error (msg ^ " for " ^ quote name ^ " (length " ^ string_of_int n ^ ")" ^
   101             Position.str_of pos);
   102         fun sel i =
   103           if i < 1 orelse i > n then err ("Bad subscript " ^ string_of_int i)
   104           else nth ths (i - 1);
   105         val is = maps (interval n) ivs handle Fail msg => err msg;
   106       in map sel is end;
   107 
   108 
   109 (* selections *)
   110 
   111 fun selections (name, [th]) = [(Named ((name, Position.none), NONE), th)]
   112   | selections (name, ths) = map2 (fn i => fn th =>
   113       (Named ((name, Position.none), SOME [Single i]), th)) (1 upto length ths) ths;
   114 
   115 
   116 
   117 (** fact environment **)
   118 
   119 (* datatypes *)
   120 
   121 datatype fact = Static of thm list | Dynamic of Context.generic -> thm list;
   122 
   123 datatype T = Facts of
   124  {facts: (fact * serial) NameSpace.table,
   125   props: thm Net.net};
   126 
   127 fun make_facts facts props = Facts {facts = facts, props = props};
   128 val empty = make_facts NameSpace.empty_table Net.empty;
   129 
   130 
   131 (* named facts *)
   132 
   133 fun facts_of (Facts {facts, ...}) = facts;
   134 
   135 val space_of = #1 o facts_of;
   136 val table_of = #2 o facts_of;
   137 
   138 val intern = NameSpace.intern o space_of;
   139 val extern = NameSpace.extern o space_of;
   140 
   141 val defined = Symtab.defined o table_of;
   142 
   143 fun lookup context facts name =
   144   (case Symtab.lookup (table_of facts) name of
   145     NONE => NONE
   146   | SOME (Static ths, _) => SOME (true, ths)
   147   | SOME (Dynamic f, _) => SOME (false, f context));
   148 
   149 fun fold_static f = Symtab.fold (fn (name, (Static ths, _)) => f (name, ths) | _ => I) o table_of;
   150 
   151 
   152 (* content difference *)
   153 
   154 fun diff_table prev_facts facts =
   155   fold_static (fn (name, ths) =>
   156     if exists (fn prev => defined prev name) prev_facts then I
   157     else cons (name, ths)) facts [];
   158 
   159 fun dest_static prev_facts facts =
   160   sort_wrt #1 (diff_table prev_facts facts);
   161 
   162 fun extern_static prev_facts facts =
   163   sort_wrt #1 (diff_table prev_facts facts |> map (apfst (extern facts)));
   164 
   165 
   166 (* indexed props *)
   167 
   168 val prop_ord = TermOrd.term_ord o pairself Thm.full_prop_of;
   169 
   170 fun props (Facts {props, ...}) = sort_distinct prop_ord (Net.content props);
   171 fun could_unify (Facts {props, ...}) = Net.unify_term props;
   172 
   173 
   174 (* merge facts *)
   175 
   176 fun err_dup_fact name = error ("Duplicate fact " ^ quote name);
   177 
   178 (* FIXME stamp identity! *)
   179 fun eq_entry ((Static ths1, _), (Static ths2, _)) = is_equal (list_ord Thm.thm_ord (ths1, ths2))
   180   | eq_entry ((_, id1: serial), (_, id2)) = id1 = id2;
   181 
   182 fun merge (Facts {facts = facts1, props = props1}, Facts {facts = facts2, props = props2}) =
   183   let
   184     val facts' = NameSpace.merge_tables eq_entry (facts1, facts2)
   185       handle Symtab.DUP dup => err_dup_fact dup;
   186     val props' = Net.merge (is_equal o prop_ord) (props1, props2);
   187   in make_facts facts' props' end;
   188 
   189 
   190 (* add static entries *)
   191 
   192 fun add permissive do_props naming (b, ths) (Facts {facts, props}) =
   193   let
   194     val (name, facts') = if Binding.is_empty b then ("", facts)
   195       else let
   196         val (space, tab) = facts;
   197         val (name, space') = NameSpace.declare naming b space;
   198         val entry = (name, (Static ths, serial ()));
   199         val tab' = (if permissive then Symtab.update else Symtab.update_new) entry tab
   200           handle Symtab.DUP dup => err_dup_fact dup;
   201       in (name, (space', tab')) end;
   202     val props' =
   203       if do_props then fold (fn th => Net.insert_term (K false) (Thm.full_prop_of th, th)) ths props
   204       else props;
   205   in (name, make_facts facts' props') end;
   206 
   207 val add_global = add false false;
   208 val add_local = add true;
   209 
   210 
   211 (* add dynamic entries *)
   212 
   213 fun add_dynamic naming (b, f) (Facts {facts = (space, tab), props}) =
   214   let
   215     val (name, space') = NameSpace.declare naming b space;
   216     val entry = (name, (Dynamic f, serial ()));
   217     val tab' = Symtab.update_new entry tab
   218       handle Symtab.DUP dup => err_dup_fact dup;
   219   in (name, make_facts (space', tab') props) end;
   220 
   221 
   222 (* remove entries *)
   223 
   224 fun del name (Facts {facts = (space, tab), props}) =
   225   let
   226     val space' = NameSpace.hide true name space handle ERROR _ => space;
   227     val tab' = Symtab.delete_safe name tab;
   228   in make_facts (space', tab') props end;
   229 
   230 fun hide fully name (Facts {facts = (space, tab), props}) =
   231   make_facts (NameSpace.hide fully name space, tab) props;
   232 
   233 end;