src/Pure/Thy/thm_database.ML
changeset 17170 cbe14eb12729
parent 15836 b805d85909c7
child 17221 6cd180204582
equal deleted inserted replaced
17169:1f12d55060bf 17170:cbe14eb12729
     1 (*  Title:      Pure/Thy/thm_database.ML
     1 (*  Title:      Pure/Thy/thm_database.ML
     2     ID:         $Id$
     2     ID:         $Id$
     3     Author:     Markus Wenzel, TU Muenchen
     3     Author:     Markus Wenzel, TU Muenchen
     4 
     4 
     5 Theorem database ML interface.
     5 ML toplevel interface to the theorem database.
     6 *)
     6 *)
     7 
     7 
     8 signature BASIC_THM_DATABASE =
     8 signature BASIC_THM_DATABASE =
     9 sig
     9 sig
    10   val store_thm: string * thm -> thm
    10   val store_thm: string * thm -> thm
    11   val store_thms: string * thm list -> thm list
    11   val store_thms: string * thm list -> thm list
       
    12   val legacy_bindings: theory -> string
       
    13   val use_legacy_bindings: theory -> unit
    12 end;
    14 end;
    13 
    15 
    14 signature THM_DATABASE =
    16 signature THM_DATABASE =
    15 sig
    17 sig
    16   include BASIC_THM_DATABASE
    18   include BASIC_THM_DATABASE
    71     if warn_ml name then ()
    73     if warn_ml name then ()
    72     else (qed_thms := thms'; use_text_verbose ("val " ^ name ^ " = ! ThmDatabase.qed_thms;"))
    74     else (qed_thms := thms'; use_text_verbose ("val " ^ name ^ " = ! ThmDatabase.qed_thms;"))
    73   end;
    75   end;
    74 
    76 
    75 
    77 
       
    78 (* legacy bindings *)
       
    79 
       
    80 fun legacy_bindings thy =
       
    81   let
       
    82     val thy_name = Context.theory_name thy;
       
    83     val (space, thms) = PureThy.theorems_of thy;
       
    84 
       
    85     fun prune name =
       
    86       let
       
    87         val xname = NameSpace.extern space name;
       
    88         fun result prfx bname =
       
    89           if (prfx = "" orelse is_ml_identifier prfx) andalso is_ml_identifier bname andalso
       
    90               NameSpace.intern space xname = name then
       
    91             SOME (prfx, (bname, xname, length (the (Symtab.lookup (thms, name))) = 1))
       
    92           else NONE;
       
    93         val names = NameSpace.unpack name;
       
    94       in
       
    95         (case #2 (splitAt (length names - 2, names)) of
       
    96           [bname] => result "" bname
       
    97         | [prfx, bname] => result (if prfx = thy_name then "" else prfx) bname
       
    98         | _ => NONE)
       
    99       end;
       
   100 
       
   101     fun mk_struct "" = I
       
   102       | mk_struct prfx = enclose ("structure " ^ prfx ^ " =\nstruct\n") "\nend\n";
       
   103 
       
   104     fun mk_thm (bname, xname, singleton) =
       
   105       "val " ^ bname ^ " = thm" ^ (if singleton then "" else "s") ^ " " ^ quote xname;
       
   106   in
       
   107     Symtab.keys thms |> List.mapPartial prune
       
   108     |> Symtab.make_multi |> Symtab.dest |> sort_wrt #1
       
   109     |> map (fn (prfx, entries) =>
       
   110       entries |> sort_wrt #1 |> map mk_thm |> cat_lines |> mk_struct prfx)
       
   111     |> cat_lines
       
   112   end;
       
   113 
       
   114 fun use_legacy_bindings thy = Context.use_mltext (legacy_bindings thy) true (SOME thy);
       
   115 
    76 end;
   116 end;
    77 
   117 
    78 structure BasicThmDatabase: BASIC_THM_DATABASE = ThmDatabase;
   118 structure BasicThmDatabase: BASIC_THM_DATABASE = ThmDatabase;
    79 open BasicThmDatabase;
   119 open BasicThmDatabase;