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