src/Pure/facts.ML
author wenzelm
Thu Mar 20 16:04:30 2008 +0100 (2008-03-20)
changeset 26361 7946f459c6c8
parent 26336 a0e2b706ce73
child 26366 5c089f4219c2
permissions -rw-r--r--
Facts.Named: include position;
     1 (*  Title:      Pure/facts.ML
     2     ID:         $Id$
     3     Author:     Makarius
     4 
     5 Environment of named facts, optionally indexed by proposition.
     6 *)
     7 
     8 signature FACTS =
     9 sig
    10   val the_single: string -> thm list -> thm
    11   datatype interval = FromTo of int * int | From of int | Single of int
    12   datatype ref =
    13     Named of (string * Position.T) * interval list option |
    14     Fact of string
    15   val named: string -> ref
    16   val string_of_ref: ref -> string
    17   val name_of_ref: ref -> string
    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 space_of: T -> NameSpace.T
    23   val lookup: T -> string -> thm list option
    24   val dest: T -> (string * thm list) list
    25   val extern: T -> (xstring * thm list) list
    26   val props: T -> thm list
    27   val could_unify: T -> term -> thm list
    28   val empty: T
    29   val merge: T * T -> T
    30   val add_global: NameSpace.naming -> string * thm list -> T -> T
    31   val add_local: bool -> NameSpace.naming -> string * thm list -> T -> T
    32   val del: string -> T -> T
    33 end;
    34 
    35 structure Facts: FACTS =
    36 struct
    37 
    38 (** fact references **)
    39 
    40 fun the_single _ [th] : thm = th
    41   | the_single name _ = error ("Single theorem expected " ^ quote name);
    42 
    43 
    44 (* datatype interval *)
    45 
    46 datatype interval =
    47   FromTo of int * int |
    48   From of int |
    49   Single of int;
    50 
    51 fun string_of_interval (FromTo (i, j)) = string_of_int i ^ "-" ^ string_of_int j
    52   | string_of_interval (From i) = string_of_int i ^ "-"
    53   | string_of_interval (Single i) = string_of_int i;
    54 
    55 fun interval n iv =
    56   let fun err () = raise Fail ("Bad interval specification " ^ string_of_interval iv) in
    57     (case iv of
    58       FromTo (i, j) => if i <= j then i upto j else err ()
    59     | From i => if i <= n then i upto n else err ()
    60     | Single i => [i])
    61   end;
    62 
    63 
    64 (* datatype ref *)
    65 
    66 datatype ref =
    67   Named of (string * Position.T) * interval list option |
    68   Fact of string;
    69 
    70 fun named name = Named ((name, Position.none), NONE);
    71 
    72 fun name_of_ref (Named ((name, _), _)) = name
    73   | name_of_ref (Fact _) = error "Illegal literal fact";
    74 
    75 fun map_name_of_ref f (Named ((name, pos), is)) = Named ((f name, pos), is)
    76   | map_name_of_ref _ r = r;
    77 
    78 fun string_of_ref (Named ((name, _), NONE)) = name
    79   | string_of_ref (Named ((name, _), SOME is)) =
    80       name ^ enclose "(" ")" (commas (map string_of_interval is))
    81   | string_of_ref (Fact _) = error "Illegal literal fact";
    82 
    83 
    84 (* select *)
    85 
    86 fun select (Fact _) ths = ths
    87   | select (Named (_, NONE)) ths = ths
    88   | select (Named ((name, pos), SOME ivs)) ths =
    89       let
    90         val n = length ths;
    91         fun err msg =
    92           error (msg ^ " for " ^ quote name ^ " (length " ^ string_of_int n ^ ")" ^
    93             Position.str_of pos);
    94         fun sel i =
    95           if i < 1 orelse i > n then err ("Bad subscript " ^ string_of_int i)
    96           else nth ths (i - 1);
    97         val is = maps (interval n) ivs handle Fail msg => err msg;
    98       in map sel is end;
    99 
   100 
   101 (* selections *)
   102 
   103 fun selections (name, [th]) = [(Named ((name, Position.none), NONE), th)]
   104   | selections (name, ths) = map2 (fn i => fn th =>
   105       (Named ((name, Position.none), SOME [Single i]), th)) (1 upto length ths) ths;
   106 
   107 
   108 
   109 (** fact environment **)
   110 
   111 (* datatype T *)
   112 
   113 datatype T = Facts of
   114  {facts: thm list NameSpace.table,
   115   props: thm Net.net};
   116 
   117 fun make_facts facts props = Facts {facts = facts, props = props};
   118 
   119 
   120 (* named facts *)
   121 
   122 fun facts_of (Facts {facts, ...}) = facts;
   123 
   124 val space_of = #1 o facts_of;
   125 val lookup = Symtab.lookup o #2 o facts_of;
   126 val dest = NameSpace.dest_table o facts_of;
   127 val extern = NameSpace.extern_table o facts_of;
   128 
   129 
   130 (* indexed props *)
   131 
   132 val prop_ord = Term.term_ord o pairself Thm.full_prop_of;
   133 
   134 fun props (Facts {props, ...}) = sort_distinct prop_ord (Net.content props);
   135 fun could_unify (Facts {props, ...}) = Net.unify_term props;
   136 
   137 
   138 (* build facts *)
   139 
   140 val empty = make_facts NameSpace.empty_table Net.empty;
   141 
   142 fun merge (Facts {facts = facts1, props = props1}, Facts {facts = facts2, props = props2}) =
   143   let
   144     val facts' = NameSpace.merge_tables (K true) (facts1, facts2);
   145     val props' = Net.merge (is_equal o prop_ord) (props1, props2);
   146   in make_facts facts' props' end;
   147 
   148 fun add permissive do_props naming (name, ths) (Facts {facts, props}) =
   149   let
   150     val facts' =
   151       if name = "" then facts
   152       else
   153         let
   154           val (space, tab) = facts;
   155           val space' = NameSpace.declare naming name space;
   156           val tab' = (if permissive then Symtab.update else Symtab.update_new) (name, ths) tab
   157             handle Symtab.DUP dup => (legacy_feature ("Duplicate fact " ^ quote dup ^
   158               Position.str_of (Position.thread_data ())); tab);
   159         in (space', tab') end;
   160     val props' =
   161       if do_props then fold (fn th => Net.insert_term (K false) (Thm.full_prop_of th, th)) ths props
   162       else props;
   163   in make_facts facts' props' end;
   164 
   165 val add_global = add false false;
   166 val add_local = add true;
   167 
   168 fun del name (Facts {facts = (space, tab), props}) =
   169   let
   170     val space' = NameSpace.hide true name space handle ERROR _ => space;
   171     val tab' = Symtab.delete_safe name tab;
   172   in make_facts (space', tab') props end;
   173 
   174 end;