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