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