src/Pure/facts.ML
author wenzelm
Thu Aug 15 16:02:47 2019 +0200 (9 months ago)
changeset 70533 031620901fcd
parent 68698 6ee53660a911
child 70545 b93ba98e627a
permissions -rw-r--r--
support for (fully reconstructed) proof terms in Scala;
proper cache_typs;
     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 defined: T -> string -> bool
    32   val is_dynamic: T -> string -> bool
    33   val lookup: Context.generic -> T -> string -> {dynamic: bool, thms: thm list} option
    34   val retrieve: Context.generic -> T -> xstring * Position.T ->
    35     {name: string, dynamic: bool, thms: thm list}
    36   val fold_static: (string * thm list -> 'a -> 'a) -> T -> 'a -> 'a
    37   val dest_static: bool -> T list -> T -> (string * thm list) list
    38   val dest_all: Context.generic -> bool -> T list -> T -> (string * thm list) list
    39   val props: T -> (thm * Position.T) list
    40   val could_unify: T -> term -> (thm * Position.T) list
    41   val merge: T * T -> T
    42   val add_static: Context.generic -> {strict: bool, index: bool} ->
    43     binding * thm list lazy -> T -> string * T
    44   val add_dynamic: Context.generic -> binding * (Context.generic -> thm list) -> T -> string * T
    45   val del: string -> T -> T
    46   val hide: bool -> string -> T -> T
    47 end;
    48 
    49 structure Facts: FACTS =
    50 struct
    51 
    52 (** fact references **)
    53 
    54 fun the_single _ [th] : thm = th
    55   | the_single (name, pos) ths =
    56       error ("Expected singleton fact " ^ quote name ^
    57         " (length " ^ string_of_int (length ths) ^ ")" ^ Position.here pos);
    58 
    59 
    60 (* datatype interval *)
    61 
    62 datatype interval =
    63   FromTo of int * int |
    64   From of int |
    65   Single of int;
    66 
    67 fun string_of_interval (FromTo (i, j)) = string_of_int i ^ "-" ^ string_of_int j
    68   | string_of_interval (From i) = string_of_int i ^ "-"
    69   | string_of_interval (Single i) = string_of_int i;
    70 
    71 fun interval n iv =
    72   let fun err () = raise Fail ("Bad interval specification " ^ string_of_interval iv) in
    73     (case iv of
    74       FromTo (i, j) => if i <= j then i upto j else err ()
    75     | From i => if i <= n then i upto n else err ()
    76     | Single i => [i])
    77   end;
    78 
    79 
    80 (* datatype ref *)
    81 
    82 datatype ref =
    83   Named of (string * Position.T) * interval list option |
    84   Fact of string;
    85 
    86 fun named name = Named ((name, Position.none), NONE);
    87 
    88 fun name_of_ref (Named ((name, _), _)) = name
    89   | name_of_ref (Fact _) = raise Fail "Illegal literal fact";
    90 
    91 fun pos_of_ref (Named ((_, pos), _)) = pos
    92   | pos_of_ref (Fact _) = Position.none;
    93 
    94 fun map_name_of_ref f (Named ((name, pos), is)) = Named ((f name, pos), is)
    95   | map_name_of_ref _ r = r;
    96 
    97 fun string_of_selection NONE = ""
    98   | string_of_selection (SOME is) = enclose "(" ")" (commas (map string_of_interval is));
    99 
   100 fun string_of_ref (Named ((name, _), sel)) = name ^ string_of_selection sel
   101   | string_of_ref (Fact _) = raise Fail "Illegal literal fact";
   102 
   103 
   104 (* select *)
   105 
   106 fun select (Fact _) ths = ths
   107   | select (Named (_, NONE)) ths = ths
   108   | select (Named ((name, pos), SOME ivs)) ths =
   109       let
   110         val n = length ths;
   111         fun err msg =
   112           error (msg ^ " for fact " ^ quote name ^ " (length " ^ string_of_int n ^ ")" ^
   113             Position.here pos);
   114         fun sel i =
   115           if i < 1 orelse i > n then err ("Bad subscript " ^ string_of_int i)
   116           else nth ths (i - 1);
   117         val is = maps (interval n) ivs handle Fail msg => err msg;
   118       in map sel is end;
   119 
   120 
   121 (* selections *)
   122 
   123 fun selections (name, [th]) = [(Named ((name, Position.none), NONE), th)]
   124   | selections (name, ths) = map2 (fn i => fn th =>
   125       (Named ((name, Position.none), SOME [Single i]), th)) (1 upto length ths) ths;
   126 
   127 
   128 
   129 (** fact environment **)
   130 
   131 (* datatypes *)
   132 
   133 datatype fact = Static of thm list lazy | Dynamic of Context.generic -> thm list;
   134 
   135 datatype T = Facts of
   136  {facts: fact Name_Space.table,
   137   props: (thm * Position.T) Net.net};
   138 
   139 fun make_facts facts props = Facts {facts = facts, props = props};
   140 
   141 val empty = make_facts (Name_Space.empty_table "fact") Net.empty;
   142 
   143 
   144 (* named facts *)
   145 
   146 fun facts_of (Facts {facts, ...}) = facts;
   147 
   148 val space_of = Name_Space.space_of_table o facts_of;
   149 
   150 fun alias naming binding name (Facts {facts, props}) =
   151   make_facts (Name_Space.alias_table naming binding name facts) props;
   152 
   153 val is_concealed = Name_Space.is_concealed o space_of;
   154 
   155 fun check context facts (xname, pos) =
   156   let
   157     val (name, fact) = Name_Space.check context (facts_of facts) (xname, pos);
   158     val _ =
   159       (case fact of
   160         Static _ => ()
   161       | Dynamic _ => Context_Position.report_generic context pos (Markup.dynamic_fact name));
   162   in name end;
   163 
   164 val intern = Name_Space.intern o space_of;
   165 fun extern ctxt = Name_Space.extern ctxt o space_of;
   166 fun markup_extern ctxt = Name_Space.markup_extern ctxt o space_of;
   167 
   168 
   169 (* retrieve *)
   170 
   171 val defined = Name_Space.defined o facts_of;
   172 
   173 fun is_dynamic facts name =
   174   (case Name_Space.lookup (facts_of facts) name of
   175     SOME (Dynamic _) => true
   176   | _ => false);
   177 
   178 fun lookup context facts name =
   179   (case Name_Space.lookup (facts_of facts) name of
   180     NONE => NONE
   181   | SOME (Static ths) => SOME {dynamic = false, thms = Lazy.force ths}
   182   | SOME (Dynamic f) => SOME {dynamic = true, thms = f context});
   183 
   184 fun retrieve context facts (xname, pos) =
   185   let
   186     val name = check context facts (xname, pos);
   187     val {dynamic, thms} =
   188       (case lookup context facts name of
   189         SOME res =>
   190           (if #dynamic res
   191            then Context_Position.report_generic context pos (Markup.dynamic_fact name)
   192            else ();
   193            res)
   194       | NONE => error ("Unknown fact " ^ quote name ^ Position.here pos));
   195   in
   196    {name = name,
   197     dynamic = dynamic,
   198     thms = map (Thm.transfer'' context) thms}
   199   end;
   200 
   201 
   202 (* content *)
   203 
   204 local
   205 
   206 fun fold_static_lazy f =
   207   Name_Space.fold_table (fn (a, Static ths) => f (a, ths) | _ => I) o facts_of;
   208 
   209 fun consolidate facts =
   210   let
   211     val unfinished =
   212       (facts, []) |-> fold_static_lazy (fn (_, ths) => if Lazy.is_finished ths then I else cons ths);
   213     val _ = Lazy.consolidate unfinished;
   214   in facts end;
   215 
   216 fun included verbose prev_facts facts name =
   217   not (exists (fn prev => defined prev name) prev_facts orelse
   218     not verbose andalso is_concealed facts name);
   219 
   220 in
   221 
   222 fun fold_static f facts =
   223   fold_static_lazy (f o apsnd Lazy.force) (consolidate facts);
   224 
   225 fun dest_static verbose prev_facts facts =
   226   fold_static (fn (a, ths) => included verbose prev_facts facts a ? cons (a, ths)) facts []
   227   |> sort_by #1;
   228 
   229 fun dest_all context verbose prev_facts facts =
   230   (facts_of (consolidate facts), [])
   231   |-> Name_Space.fold_table (fn (a, fact) =>
   232     let val ths = (case fact of Static ths => Lazy.force ths | Dynamic f => f context)
   233     in included verbose prev_facts facts a ? cons (a, ths) end)
   234   |> sort_by #1;
   235 
   236 end;
   237 
   238 
   239 (* indexed props *)
   240 
   241 val prop_ord = Term_Ord.term_ord o apply2 (Thm.full_prop_of o fst);
   242 
   243 fun props (Facts {props, ...}) = sort_distinct prop_ord (Net.content props);
   244 fun could_unify (Facts {props, ...}) = Net.unify_term props;
   245 
   246 
   247 (* merge facts *)
   248 
   249 fun merge (Facts {facts = facts1, props = props1}, Facts {facts = facts2, props = props2}) =
   250   let
   251     val facts' = Name_Space.merge_tables (facts1, facts2);
   252     val props' =
   253       if Net.is_empty props2 then props1
   254       else if Net.is_empty props1 then props2
   255       else Net.merge (is_equal o prop_ord) (props1, props2);  (*beware of non-canonical merge*)
   256   in make_facts facts' props' end;
   257 
   258 
   259 (* add entries *)
   260 
   261 fun add_prop pos th =
   262   Net.insert_term (K false) (Thm.full_prop_of th, (th, pos));
   263 
   264 fun add_static context {strict, index} (b, ths) (Facts {facts, props}) =
   265   let
   266     val ths' = ths
   267       |> index ? Lazy.force_value
   268       |> Lazy.map_finished (map Thm.trim_context);
   269     val (name, facts') =
   270       if Binding.is_empty b then ("", facts)
   271       else Name_Space.define context strict (b, Static ths') facts;
   272     val props' =
   273       if index then
   274         props |> fold (add_prop (Binding.pos_of (Binding.default_pos b))) (Lazy.force ths')
   275       else props;
   276   in (name, make_facts facts' props') end;
   277 
   278 fun add_dynamic context (b, f) (Facts {facts, props}) =
   279   let val (name, facts') = Name_Space.define context true (b, Dynamic f) facts;
   280   in (name, make_facts facts' props) end;
   281 
   282 
   283 (* remove entries *)
   284 
   285 fun del name (Facts {facts, props}) =
   286   make_facts (Name_Space.del_table name facts) props;
   287 
   288 fun hide fully name (Facts {facts, props}) =
   289   make_facts (Name_Space.hide_table fully name facts) props;
   290 
   291 end;