src/Pure/fact_index.ML
author haftmann
Fri Nov 10 07:44:47 2006 +0100 (2006-11-10)
changeset 21286 b5e7b80caa6a
parent 20156 7a7898b1cfa4
child 21648 c8a0370c9b93
permissions -rw-r--r--
introduces canonical AList functions for loop_tacs
     1 (*  Title:      Pure/fact_index.ML
     2     ID:         $Id$
     3     Author:     Markus Wenzel, TU Muenchen
     4 
     5 Facts indexed by consts or frees.
     6 *)
     7 
     8 signature FACT_INDEX =
     9 sig
    10   type spec
    11   type T
    12   val facts: T -> (string * thm list) list
    13   val props: T -> thm list
    14   val could_unify: T -> term -> thm list
    15   val empty: T
    16   val add_global: (string * thm list) -> T -> T
    17   val add_local: bool -> (string * thm list) -> T -> T
    18   val find: T -> spec -> (string * thm list) list
    19 end;
    20 
    21 structure FactIndex: FACT_INDEX =
    22 struct
    23 
    24 
    25 (* indexing items *)
    26 
    27 type spec = string list * string list;
    28 
    29 val add_consts = fold_aterms
    30   (fn Const (c, _) => if c = Term.dummy_patternN then I else insert (op =) c | _ => I);
    31 
    32 val add_frees = fold_aterms (fn Free (x, _) => insert (op =) x | _ => I);
    33 
    34 fun index_term t (cs, xs) = (add_consts t cs, add_frees t xs);
    35 
    36 fun index_thm th =
    37   let val {tpairs, hyps, prop, ...} = Thm.rep_thm th in
    38     index_term prop
    39     #> fold index_term hyps
    40     #> fold (fn (t, u) => index_term t #> index_term u) tpairs
    41   end;
    42 
    43 
    44 (* build index *)
    45 
    46 type fact = string * thm list;
    47 
    48 datatype T = Index of
    49  {facts: fact list,
    50   consts: (serial * fact) list Symtab.table,
    51   frees: (serial * fact) list Symtab.table,
    52   props: thm Net.net};
    53 
    54 fun facts (Index {facts, ...}) = facts;
    55 fun props (Index {props, ...}) =
    56   sort_distinct (Term.term_ord o pairself Thm.full_prop_of) (Net.content props);
    57 fun could_unify (Index {props, ...}) = Net.unify_term props;
    58 
    59 val empty =
    60   Index {facts = [], consts = Symtab.empty, frees = Symtab.empty, props = Net.empty};
    61 
    62 fun add do_props do_index (fact as (_, ths)) (Index {facts, consts, frees, props}) =
    63   let
    64     val entry = (serial (), fact);
    65     val (cs, xs) = fold index_thm ths ([], []);
    66 
    67     val (facts', consts', frees') =
    68       if do_index then
    69        (fact :: facts,
    70         consts |> fold (fn c => Symtab.update_list (c, entry)) cs,
    71         frees |> fold (fn x => Symtab.update_list (x, entry)) xs)
    72       else (facts, consts, frees);
    73     val props' =
    74       if do_props then props |> fold (fn th => Net.insert_term (K false) (Thm.prop_of th, th)) ths
    75       else props;
    76   in Index {facts = facts', consts = consts', frees = frees', props = props'} end;
    77 
    78 val add_global = add false true;
    79 val add_local = add true;
    80 
    81 
    82 (* find by consts/frees *)
    83 
    84 local
    85 
    86 fun fact_ord ((i, _), (j, _)) = int_ord (j, i);
    87 
    88 fun intersects [xs] = xs
    89   | intersects xss =
    90       if exists null xss then []
    91       else fold (OrdList.inter fact_ord) (tl xss) (hd xss);
    92 
    93 in
    94 
    95 fun find idx ([], []) = facts idx
    96   | find (Index {consts, frees, ...}) (cs, xs) =
    97       (map (Symtab.lookup_list consts) cs @
    98         map (Symtab.lookup_list frees) xs) |> intersects |> map #2;
    99 
   100 end
   101 
   102 end;