src/Pure/facts.ML
author wenzelm
Mon Feb 23 14:50:30 2015 +0100 (2015-02-23)
changeset 59564 fdc03c8daacc
parent 59058 a78612c67ec0
child 59883 12a89103cae6
permissions -rw-r--r--
Goal.prove_multi is superseded by the fully general Goal.prove_common;
     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 alias: Name_Space.naming -> binding -> string -> T -> T
    26   val is_concealed: T -> string -> bool
    27   val check: Context.generic -> T -> xstring * Position.T -> string
    28   val intern: T -> xstring -> string
    29   val extern: Proof.context -> T -> string -> xstring
    30   val markup_extern: Proof.context -> T -> string -> Markup.T * xstring
    31   val lookup: Context.generic -> T -> string -> (bool * thm list) option
    32   val retrieve: Context.generic -> T -> xstring * Position.T ->
    33     {name: string, static: bool, thms: thm list}
    34   val defined: T -> string -> bool
    35   val fold_static: (string * thm list -> 'a -> 'a) -> T -> 'a -> 'a
    36   val dest_static: bool -> T list -> T -> (string * thm list) list
    37   val props: T -> thm list
    38   val could_unify: T -> term -> thm list
    39   val merge: T * T -> T
    40   val add_static: Context.generic -> {strict: bool, index: bool} ->
    41     binding * thm list -> T -> string * T
    42   val add_dynamic: Context.generic -> binding * (Context.generic -> thm list) -> T -> string * T
    43   val del: string -> T -> T
    44   val hide: bool -> string -> T -> T
    45 end;
    46 
    47 structure Facts: FACTS =
    48 struct
    49 
    50 (** fact references **)
    51 
    52 fun the_single _ [th] : thm = th
    53   | the_single (name, pos) ths =
    54       error ("Expected singleton fact " ^ quote name ^
    55         " (length " ^ string_of_int (length ths) ^ ")" ^ Position.here pos);
    56 
    57 
    58 (* datatype interval *)
    59 
    60 datatype interval =
    61   FromTo of int * int |
    62   From of int |
    63   Single of int;
    64 
    65 fun string_of_interval (FromTo (i, j)) = string_of_int i ^ "-" ^ string_of_int j
    66   | string_of_interval (From i) = string_of_int i ^ "-"
    67   | string_of_interval (Single i) = string_of_int i;
    68 
    69 fun interval n iv =
    70   let fun err () = raise Fail ("Bad interval specification " ^ string_of_interval iv) in
    71     (case iv of
    72       FromTo (i, j) => if i <= j then i upto j else err ()
    73     | From i => if i <= n then i upto n else err ()
    74     | Single i => [i])
    75   end;
    76 
    77 
    78 (* datatype ref *)
    79 
    80 datatype ref =
    81   Named of (string * Position.T) * interval list option |
    82   Fact of string;
    83 
    84 fun named name = Named ((name, Position.none), NONE);
    85 
    86 fun name_of_ref (Named ((name, _), _)) = name
    87   | name_of_ref (Fact _) = raise Fail "Illegal literal fact";
    88 
    89 fun pos_of_ref (Named ((_, pos), _)) = pos
    90   | pos_of_ref (Fact _) = Position.none;
    91 
    92 fun map_name_of_ref f (Named ((name, pos), is)) = Named ((f name, pos), is)
    93   | map_name_of_ref _ r = r;
    94 
    95 fun string_of_selection NONE = ""
    96   | string_of_selection (SOME is) = enclose "(" ")" (commas (map string_of_interval is));
    97 
    98 fun string_of_ref (Named ((name, _), sel)) = name ^ string_of_selection sel
    99   | string_of_ref (Fact _) = raise Fail "Illegal literal fact";
   100 
   101 
   102 (* select *)
   103 
   104 fun select (Fact _) ths = ths
   105   | select (Named (_, NONE)) ths = ths
   106   | select (Named ((name, pos), SOME ivs)) ths =
   107       let
   108         val n = length ths;
   109         fun err msg =
   110           error (msg ^ " for fact " ^ quote name ^ " (length " ^ string_of_int n ^ ")" ^
   111             Position.here pos);
   112         fun sel i =
   113           if i < 1 orelse i > n then err ("Bad subscript " ^ string_of_int i)
   114           else nth ths (i - 1);
   115         val is = maps (interval n) ivs handle Fail msg => err msg;
   116       in map sel is end;
   117 
   118 
   119 (* selections *)
   120 
   121 fun selections (name, [th]) = [(Named ((name, Position.none), NONE), th)]
   122   | selections (name, ths) = map2 (fn i => fn th =>
   123       (Named ((name, Position.none), SOME [Single i]), th)) (1 upto length ths) ths;
   124 
   125 
   126 
   127 (** fact environment **)
   128 
   129 (* datatypes *)
   130 
   131 datatype fact = Static of thm list | Dynamic of Context.generic -> thm list;
   132 
   133 datatype T = Facts of
   134  {facts: fact Name_Space.table,
   135   props: thm Net.net};
   136 
   137 fun make_facts facts props = Facts {facts = facts, props = props};
   138 
   139 val empty = make_facts (Name_Space.empty_table "fact") Net.empty;
   140 
   141 
   142 (* named facts *)
   143 
   144 fun facts_of (Facts {facts, ...}) = facts;
   145 
   146 val space_of = Name_Space.space_of_table o facts_of;
   147 
   148 fun alias naming binding name (Facts {facts, props}) =
   149   make_facts (Name_Space.alias_table naming binding name facts) props;
   150 
   151 val is_concealed = Name_Space.is_concealed o space_of;
   152 
   153 fun check context facts (xname, pos) =
   154   let
   155     val (name, fact) = Name_Space.check context (facts_of facts) (xname, pos);
   156     val _ =
   157       (case fact of
   158         Static _ => ()
   159       | Dynamic _ => Context_Position.report_generic context pos (Markup.dynamic_fact name));
   160   in name end;
   161 
   162 val intern = Name_Space.intern o space_of;
   163 fun extern ctxt = Name_Space.extern ctxt o space_of;
   164 fun markup_extern ctxt = Name_Space.markup_extern ctxt o space_of;
   165 
   166 
   167 (* retrieve *)
   168 
   169 val defined = is_some oo (Name_Space.lookup_key o facts_of);
   170 
   171 fun lookup context facts name =
   172   (case Name_Space.lookup_key (facts_of facts) name of
   173     NONE => NONE
   174   | SOME (_, Static ths) => SOME (true, ths)
   175   | SOME (_, Dynamic f) => SOME (false, f context));
   176 
   177 fun retrieve context facts (xname, pos) =
   178   let
   179     val name = check context facts (xname, pos);
   180     val (static, thms) =
   181       (case lookup context facts name of
   182         SOME (static, thms) =>
   183           (if static then ()
   184            else Context_Position.report_generic context pos (Markup.dynamic_fact name);
   185            (static, thms))
   186       | NONE => error ("Unknown fact " ^ quote name ^ Position.here pos));
   187   in
   188    {name = name,
   189     static = static,
   190     thms = map (Thm.transfer (Context.theory_of context)) thms}
   191   end;
   192 
   193 
   194 (* static content *)
   195 
   196 fun fold_static f =
   197   Name_Space.fold_table (fn (name, Static ths) => f (name, ths) | _ => I) o facts_of;
   198 
   199 fun dest_static verbose prev_facts facts =
   200   fold_static (fn (name, ths) =>
   201     if exists (fn prev => defined prev name) prev_facts orelse
   202       not verbose andalso is_concealed facts name then I
   203     else cons (name, ths)) facts []
   204   |> sort_wrt #1;
   205 
   206 
   207 (* indexed props *)
   208 
   209 val prop_ord = Term_Ord.term_ord o apply2 Thm.full_prop_of;
   210 
   211 fun props (Facts {props, ...}) = sort_distinct prop_ord (Net.content props);
   212 fun could_unify (Facts {props, ...}) = Net.unify_term props;
   213 
   214 
   215 (* merge facts *)
   216 
   217 fun merge (Facts {facts = facts1, props = props1}, Facts {facts = facts2, props = props2}) =
   218   let
   219     val facts' = Name_Space.merge_tables (facts1, facts2);
   220     val props' =
   221       if Net.is_empty props2 then props1
   222       else if Net.is_empty props1 then props2
   223       else Net.merge (is_equal o prop_ord) (props1, props2);  (*beware of non-canonical merge*)
   224   in make_facts facts' props' end;
   225 
   226 
   227 (* add static entries *)
   228 
   229 fun add_static context {strict, index} (b, ths) (Facts {facts, props}) =
   230   let
   231     val (name, facts') =
   232       if Binding.is_empty b then ("", facts)
   233       else Name_Space.define context strict (b, Static ths) facts;
   234     val props' = props
   235       |> index ? fold (fn th => Net.insert_term (K false) (Thm.full_prop_of th, th)) ths;
   236   in (name, make_facts facts' props') end;
   237 
   238 
   239 (* add dynamic entries *)
   240 
   241 fun add_dynamic context (b, f) (Facts {facts, props}) =
   242   let val (name, facts') = Name_Space.define context true (b, Dynamic f) facts;
   243   in (name, make_facts facts' props) end;
   244 
   245 
   246 (* remove entries *)
   247 
   248 fun del name (Facts {facts, props}) =
   249   make_facts (Name_Space.del_table name facts) props;
   250 
   251 fun hide fully name (Facts {facts, props}) =
   252   make_facts (Name_Space.hide_table fully name facts) props;
   253 
   254 end;