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