src/Pure/Thy/thm_database.ML
author wenzelm
Tue Dec 18 19:54:33 2007 +0100 (2007-12-18)
changeset 25699 891fe6b71d3b
parent 23921 947152add153
child 26386 9c806de22a6a
permissions -rw-r--r--
named some critical sections;
     1 (*  Title:      Pure/Thy/thm_database.ML
     2     ID:         $Id$
     3     Author:     Markus Wenzel, TU Muenchen
     4 
     5 ML toplevel interface to the theorem database.
     6 *)
     7 
     8 signature BASIC_THM_DATABASE =
     9 sig
    10   val store_thm: string * thm -> thm
    11   val store_thms: string * thm list -> thm list
    12   val legacy_bindings: theory -> string
    13   val use_legacy_bindings: theory -> unit
    14 end;
    15 
    16 signature THM_DATABASE =
    17 sig
    18   include BASIC_THM_DATABASE
    19   val qed_thms: thm list ref
    20   val ml_store_thm: string * thm -> unit
    21   val ml_store_thms: string * thm list -> unit
    22 end;
    23 
    24 structure ThmDatabase: THM_DATABASE =
    25 struct
    26 
    27 (** store theorems **)
    28 
    29 (* store in theory and perform presentation *)
    30 
    31 fun store_thm (name, thm) =
    32   let val thm' = hd (PureThy.smart_store_thms (name, [thm]))
    33   in Present.theorem name thm'; thm' end;
    34 
    35 fun store_thms (name, thms) =
    36   let val thms' = PureThy.smart_store_thms (name, thms)
    37   in Present.theorems name thms'; thms' end;
    38 
    39 
    40 (* store on ML toplevel *)
    41 
    42 val qed_thms: thm list ref = ref [];
    43 
    44 fun warn_ml name =
    45   if ML_Syntax.is_identifier name then false
    46   else if name = "" then true
    47   else (warning ("Cannot bind theorem(s) " ^ quote name ^ " as ML value"); true);
    48 
    49 val use_text_verbose = use_text "" Output.ml_output true;
    50 
    51 fun ml_store_thm (name, thm) =
    52   let val thm' = store_thm (name, thm) in
    53     if warn_ml name then ()
    54     else NAMED_CRITICAL "ML" (fn () => (qed_thms := [thm'];
    55       use_text_verbose ("val " ^ name ^ " = hd (! ThmDatabase.qed_thms);")))
    56   end;
    57 
    58 fun ml_store_thms (name, thms) =
    59   let val thms' = store_thms (name, thms) in
    60     if warn_ml name then ()
    61     else NAMED_CRITICAL "ML" (fn () => (qed_thms := thms';
    62       use_text_verbose ("val " ^ name ^ " = ! ThmDatabase.qed_thms;")))
    63   end;
    64 
    65 
    66 (* legacy bindings *)
    67 
    68 fun legacy_bindings thy =
    69   let
    70     val thy_name = Context.theory_name thy;
    71     val (space, thms) = PureThy.theorems_of thy;
    72 
    73     fun prune name =
    74       let
    75         val xname = NameSpace.extern space name;
    76         fun result prfx bname =
    77           if (prfx = "" orelse ML_Syntax.is_identifier prfx) andalso
    78               ML_Syntax.is_identifier bname andalso
    79               NameSpace.intern space xname = name then
    80             SOME (prfx, (bname, xname, length (the (Symtab.lookup thms name)) = 1))
    81           else NONE;
    82         val names = NameSpace.explode name;
    83       in
    84         (case #2 (chop (length names - 2) names) of
    85           [bname] => result "" bname
    86         | [prfx, bname] => result (if prfx = thy_name then "" else prfx) bname
    87         | _ => NONE)
    88       end;
    89 
    90     fun mk_struct "" = I
    91       | mk_struct prfx = enclose ("structure " ^ prfx ^ " =\nstruct\n") "\nend\n";
    92 
    93     fun mk_thm (bname, xname, singleton) =
    94       "val " ^ bname ^ " = thm" ^ (if singleton then "" else "s") ^ " " ^ quote xname;
    95   in
    96     Symtab.keys thms |> map_filter prune
    97     |> Symtab.make_list |> Symtab.dest |> sort_wrt #1
    98     |> map (fn (prfx, entries) =>
    99       entries |> sort_wrt #1 |> map mk_thm |> cat_lines |> mk_struct prfx)
   100     |> cat_lines
   101   end;
   102 
   103 fun use_legacy_bindings thy =
   104   ML_Context.use_mltext (legacy_bindings thy) true (SOME (Context.Theory thy));
   105 
   106 end;
   107 
   108 structure BasicThmDatabase: BASIC_THM_DATABASE = ThmDatabase;
   109 open BasicThmDatabase;