6 |
6 |
7 Functions for reading theory files, and storing and retrieving theories, |
7 Functions for reading theory files, and storing and retrieving theories, |
8 theorems and the global simplifier set. |
8 theorems and the global simplifier set. |
9 *) |
9 *) |
10 |
10 |
11 (*Type for theory storage*) |
11 (*Types for theory storage*) |
|
12 |
|
13 (*Functions to handle arbitrary data added by the user; type "exn" is used |
|
14 to store data*) |
|
15 datatype thy_methods = |
|
16 ThyMethods of {merge: exn list -> exn, put: exn -> unit, get: unit -> exn}; |
|
17 |
12 datatype thy_info = |
18 datatype thy_info = |
13 ThyInfo of {path: string, |
19 ThyInfo of {path: string, |
14 children: string list, parents: string list, |
20 children: string list, parents: string list, |
15 thy_time: string option, ml_time: string option, |
21 thy_time: string option, ml_time: string option, |
16 theory: theory option, thms: thm Symtab.table, |
22 theory: theory option, thms: thm Symtab.table, |
17 thy_ss: Simplifier.simpset option, |
23 methods: thy_methods Symtab.table, |
18 simpset: Simplifier.simpset option, |
24 data: exn Symtab.table * exn Symtab.table}; |
19 datatypes: (string * string list) list}; |
25 (*thy_time, ml_time = None theory file has not been read yet |
20 (*meaning of special values: |
|
21 thy_time, ml_time = None theory file has not been read yet |
|
22 = Some "" theory was read but has either been marked |
26 = Some "" theory was read but has either been marked |
23 as outdated or there is no such file for |
27 as outdated or there is no such file for |
24 this theory (see e.g. 'virtual' theories |
28 this theory (see e.g. 'virtual' theories |
25 like Pure or theories without a ML file) |
29 like Pure or theories without a ML file) |
26 theory = None theory has not been read yet |
30 theory = None theory has not been read yet |
98 val loaded_thys = |
111 val loaded_thys = |
99 ref (Symtab.make [("ProtoPure", |
112 ref (Symtab.make [("ProtoPure", |
100 ThyInfo {path = "", |
113 ThyInfo {path = "", |
101 children = ["Pure", "CPure"], parents = [], |
114 children = ["Pure", "CPure"], parents = [], |
102 thy_time = Some "", ml_time = Some "", |
115 thy_time = Some "", ml_time = Some "", |
103 theory = Some proto_pure_thy, thms = Symtab.null, |
116 theory = Some proto_pure_thy, |
104 thy_ss = None, simpset = None, datatypes = []}), |
117 thms = Symtab.null, methods = Symtab.null, |
|
118 data = (Symtab.null, Symtab.null)}), |
105 ("Pure", |
119 ("Pure", |
106 ThyInfo {path = "", children = [], |
120 ThyInfo {path = "", children = [], |
107 parents = ["ProtoPure"], |
121 parents = ["ProtoPure"], |
108 thy_time = Some "", ml_time = Some "", |
122 thy_time = Some "", ml_time = Some "", |
109 theory = Some pure_thy, thms = Symtab.null, |
123 theory = Some pure_thy, thms = Symtab.null, |
110 thy_ss = None, simpset = None, datatypes = []}), |
124 methods = Symtab.null, |
|
125 data = (Symtab.null, Symtab.null)}), |
111 ("CPure", |
126 ("CPure", |
112 ThyInfo {path = "", |
127 ThyInfo {path = "", |
113 children = [], parents = ["ProtoPure"], |
128 children = [], parents = ["ProtoPure"], |
114 thy_time = Some "", ml_time = Some "", |
129 thy_time = Some "", ml_time = Some "", |
115 theory = Some cpure_thy, |
130 theory = Some cpure_thy, |
116 thms = Symtab.null, |
131 thms = Symtab.null, |
117 thy_ss = None, simpset = None, datatypes = []}) |
132 methods = Symtab.null, |
|
133 data = (Symtab.null, Symtab.null)}) |
118 ]); |
134 ]); |
119 |
135 |
120 val loadpath = ref ["."]; (*default search path for theory files*) |
136 (*Default search path for theory files*) |
121 |
137 val loadpath = ref ["."]; |
122 val delete_tmpfiles = ref true; (*remove temporary files after use*) |
138 |
|
139 (*ML files to be read by init_thy_reader; they normally contain redefinitions |
|
140 of functions accessing reference variables inside READTHY*) |
|
141 val thy_reader_files = ref [] : string list ref; |
|
142 |
|
143 (*Remove temporary files after use*) |
|
144 val delete_tmpfiles = ref true; |
123 |
145 |
124 |
146 |
125 (*Set location of graphics for HTML files |
147 (*Set location of graphics for HTML files |
126 (When this is executed for the first time we are in $ISABELLE/Pure/Thy. |
148 (When this is executed for the first time we are in $ISABELLE/Pure/Thy. |
127 This path is converted to $ISABELLE/Tools by removing the last two |
149 This path is converted to $ISABELLE/Tools by removing the last two |
208 | None => (false, false) |
230 | None => (false, false) |
209 |
231 |
210 (*Get all direct descendants of a theory*) |
232 (*Get all direct descendants of a theory*) |
211 fun children_of t = |
233 fun children_of t = |
212 case get_thyinfo t of Some (ThyInfo {children, ...}) => children |
234 case get_thyinfo t of Some (ThyInfo {children, ...}) => children |
213 | _ => []; |
235 | None => []; |
214 |
236 |
215 (*Get all direct ancestors of a theory*) |
237 (*Get all direct ancestors of a theory*) |
216 fun parents_of_name t = |
238 fun parents_of_name t = |
217 case get_thyinfo t of Some (ThyInfo {parents, ...}) => parents |
239 case get_thyinfo t of Some (ThyInfo {parents, ...}) => parents |
218 | _ => []; |
240 | None => []; |
219 |
241 |
220 (*Get all descendants of a theory list *) |
242 (*Get all descendants of a theory list *) |
221 fun get_descendants [] = [] |
243 fun get_descendants [] = [] |
222 | get_descendants (t :: ts) = |
244 | get_descendants (t :: ts) = |
223 let val children = children_of t |
245 let val children = children_of t |
224 in children union (get_descendants (children union ts)) end; |
246 in children union (get_descendants (children union ts)) end; |
225 |
247 |
226 (*Get theory object for a loaded theory *) |
248 (*Get theory object for a loaded theory *) |
227 fun theory_of name = |
249 fun theory_of name = |
228 let val ThyInfo {theory, ...} = the (get_thyinfo name) |
250 case get_thyinfo name of Some (ThyInfo {theory = Some t, ...}) => t |
229 in the theory end; |
251 | _ => error ("Theory " ^ name ^ |
|
252 " not stored by loader"); |
230 |
253 |
231 (*Get path where theory's files are located*) |
254 (*Get path where theory's files are located*) |
232 fun path_of tname = |
255 fun path_of tname = |
233 let val ThyInfo {path, ...} = the (get_thyinfo tname) |
256 let val ThyInfo {path, ...} = the (get_thyinfo tname) |
234 in path end; |
257 in path end; |
235 |
|
236 exception FILE_NOT_FOUND; (*raised by find_file *) |
|
237 |
258 |
238 (*Find a file using a list of paths if no absolute or relative path is |
259 (*Find a file using a list of paths if no absolute or relative path is |
239 specified.*) |
260 specified.*) |
240 fun find_file "" name = |
261 fun find_file "" name = |
241 let fun find_it (cur :: paths) = |
262 let fun find_it (cur :: paths) = |
316 |
325 |
317 (*Change thy_time and ml_time for an existent item *) |
326 (*Change thy_time and ml_time for an existent item *) |
318 fun set_info tname thy_time ml_time = |
327 fun set_info tname thy_time ml_time = |
319 let val tinfo = case Symtab.lookup (!loaded_thys, tname) of |
328 let val tinfo = case Symtab.lookup (!loaded_thys, tname) of |
320 Some (ThyInfo {path, children, parents, theory, thms, |
329 Some (ThyInfo {path, children, parents, theory, thms, |
321 thy_ss, simpset, datatypes, ...}) => |
330 methods, data, ...}) => |
322 ThyInfo {path = path, children = children, parents = parents, |
331 ThyInfo {path = path, children = children, parents = parents, |
323 thy_time = thy_time, ml_time = ml_time, |
332 thy_time = thy_time, ml_time = ml_time, |
324 theory = theory, thms = thms, |
333 theory = theory, thms = thms, |
325 thy_ss = thy_ss, simpset = simpset, datatypes = datatypes} |
334 methods = methods, data = data} |
326 | None => error ("set_info: theory " ^ tname ^ " not found"); |
335 | None => error ("set_info: theory " ^ tname ^ " not found"); |
327 in loaded_thys := Symtab.update ((tname, tinfo), !loaded_thys) end; |
336 in loaded_thys := Symtab.update ((tname, tinfo), !loaded_thys) end; |
328 |
337 |
329 (*Mark theory as changed since last read if it has been completly read *) |
338 (*Mark theory as changed since last read if it has been completly read *) |
330 fun mark_outdated tname = |
339 fun mark_outdated tname = |
556 val old_parents = parents_of_name tname; |
566 val old_parents = parents_of_name tname; |
557 |
567 |
558 (*Set absolute path for loaded theory *) |
568 (*Set absolute path for loaded theory *) |
559 fun set_path () = |
569 fun set_path () = |
560 let val ThyInfo {children, parents, thy_time, ml_time, theory, thms, |
570 let val ThyInfo {children, parents, thy_time, ml_time, theory, thms, |
561 thy_ss, simpset, datatypes, ...} = |
571 methods, data, ...} = |
562 the (Symtab.lookup (!loaded_thys, tname)); |
572 the (Symtab.lookup (!loaded_thys, tname)); |
563 in loaded_thys := Symtab.update ((tname, |
573 in loaded_thys := Symtab.update ((tname, |
564 ThyInfo {path = abs_path, |
574 ThyInfo {path = abs_path, |
565 children = children, parents = parents, |
575 children = children, parents = parents, |
566 thy_time = thy_time, ml_time = ml_time, |
576 thy_time = thy_time, ml_time = ml_time, |
567 theory = theory, thms = thms, |
577 theory = theory, thms = thms, |
568 thy_ss = thy_ss, simpset = simpset, |
578 methods = methods, data = data}), |
569 datatypes = datatypes}), |
|
570 !loaded_thys) |
579 !loaded_thys) |
571 end; |
580 end; |
572 |
581 |
573 (*Mark all direct descendants of a theory as changed *) |
582 (*Mark all direct descendants of a theory as changed *) |
574 fun mark_children thy = |
583 fun mark_children thy = |
581 ^ (quote (space_implode "\",\"" loaded))) |
590 ^ (quote (space_implode "\",\"" loaded))) |
582 else (); |
591 else (); |
583 seq mark_outdated present |
592 seq mark_outdated present |
584 end; |
593 end; |
585 |
594 |
586 (*Remove theorems and datatypes associated with a theory*) |
595 (*Remove theorems associated with a theory*) |
587 fun delete_thms () = |
596 fun delete_thms () = |
588 let |
597 let |
589 val tinfo = case get_thyinfo tname of |
598 val tinfo = case get_thyinfo tname of |
590 Some (ThyInfo {path, children, parents, thy_time, ml_time, theory, |
599 Some (ThyInfo {path, children, parents, thy_time, ml_time, theory, |
591 thy_ss, simpset, datatypes, ...}) => |
600 methods, data, ...}) => |
592 ThyInfo {path = path, children = children, parents = parents, |
601 ThyInfo {path = path, children = children, parents = parents, |
593 thy_time = thy_time, ml_time = ml_time, |
602 thy_time = thy_time, ml_time = ml_time, |
594 theory = theory, thms = Symtab.null, |
603 theory = theory, thms = Symtab.null, |
595 thy_ss = thy_ss, simpset = simpset, |
604 methods = methods, data = data} |
596 datatypes = []} |
|
597 | None => ThyInfo {path = "", children = [], parents = [], |
605 | None => ThyInfo {path = "", children = [], parents = [], |
598 thy_time = None, ml_time = None, |
606 thy_time = None, ml_time = None, |
599 theory = None, thms = Symtab.null, |
607 theory = None, thms = Symtab.null, |
600 thy_ss = None, simpset = None, datatypes = []}; |
608 methods = Symtab.null, |
|
609 data = (Symtab.null, Symtab.null)}; |
601 |
610 |
602 val ThyInfo {theory, ...} = tinfo; |
611 val ThyInfo {theory, ...} = tinfo; |
603 in loaded_thys := Symtab.update ((tname, tinfo), !loaded_thys); |
612 in loaded_thys := Symtab.update ((tname, tinfo), !loaded_thys); |
604 case theory of |
613 case theory of |
605 Some t => delete_thm_db t |
614 Some t => delete_thm_db t |
606 | None => () |
615 | None => () |
607 end; |
616 end; |
608 |
617 |
609 fun save_thy_ss () = |
618 (*Invoke every get method stored in the methods table and store result in |
|
619 data table*) |
|
620 fun save_data thy_only = |
610 let val ThyInfo {path, children, parents, thy_time, ml_time, |
621 let val ThyInfo {path, children, parents, thy_time, ml_time, |
611 theory, thms, simpset, datatypes, ...} = |
622 theory, thms, methods, data} = the (get_thyinfo tname); |
612 the (get_thyinfo tname); |
623 |
|
624 fun get_data [] data = data |
|
625 | get_data ((id, ThyMethods {get, ...}) :: ms) data = |
|
626 get_data ms (Symtab.update ((id, get ()), data)); |
|
627 |
|
628 val new_data = get_data (Symtab.dest methods) Symtab.null; |
|
629 |
|
630 val data' = if thy_only then (new_data, snd data) |
|
631 else (fst data, new_data); |
613 in loaded_thys := Symtab.update |
632 in loaded_thys := Symtab.update |
614 ((tname, ThyInfo {path = path, |
633 ((tname, ThyInfo {path = path, |
615 children = children, parents = parents, |
634 children = children, parents = parents, |
616 thy_time = thy_time, ml_time = ml_time, |
635 thy_time = thy_time, ml_time = ml_time, |
617 theory = theory, thms = thms, |
636 theory = theory, thms = thms, |
618 thy_ss = Some (!Simplifier.simpset), |
637 methods = methods, data = data'}), |
619 simpset = simpset, datatypes = datatypes}), |
|
620 !loaded_thys) |
638 !loaded_thys) |
621 end; |
639 end; |
622 |
640 |
623 fun save_simpset () = |
641 (*Invoke every put method stored in the methods table to initialize |
624 let val ThyInfo {path, children, parents, thy_time, ml_time, |
642 the state of user defined variables*) |
625 theory, thms, thy_ss, datatypes, ...} = |
643 fun init_data methods data = |
626 the (get_thyinfo tname); |
644 let fun put_data [] = () |
627 in loaded_thys := Symtab.update |
645 | put_data ((id, date) :: ds) = |
628 ((tname, ThyInfo {path = path, |
646 case Symtab.lookup (methods, id) of |
629 children = children, parents = parents, |
647 Some (ThyMethods {put, ...}) => put date |
630 thy_time = thy_time, ml_time = ml_time, |
648 | None => error ("No method defined for theory data \"" ^ |
631 theory = theory, thms = thms, |
649 id ^ "\""); |
632 thy_ss = thy_ss, |
650 in put_data data end; |
633 simpset = Some (!Simplifier.simpset), |
651 |
634 datatypes = datatypes}), |
652 (*Add theory to file listing all loaded theories (for index.html) |
635 !loaded_thys) |
653 and to the sub-charts of its parents*) |
636 end; |
654 fun mk_html () = |
637 |
655 let val new_parents = parents_of_name tname \\ old_parents; |
638 (*Add theory to file listing all loaded theories (for index.html) |
656 |
639 and to the sub-charts of its parents*) |
657 fun robust_seq (proc: 'a -> unit) : 'a list -> unit = |
640 fun mk_html () = |
658 let fun seqf [] = () |
641 let val new_parents = parents_of_name tname \\ old_parents; |
659 | seqf (x :: xs) = (proc x handle _ => (); seqf xs) |
642 |
660 in seqf end; |
643 (*Add child to parents' sub-theory charts*) |
661 |
644 fun add_to_parents t = |
662 (*Add child to parents' sub-theory charts*) |
645 let val path = if t = "Pure" orelse t = "CPure" then |
663 fun add_to_parents t = |
646 (the (!pure_subchart)) |
664 let val path = if t = "Pure" orelse t = "CPure" then |
647 else path_of t; |
665 (the (!pure_subchart)) |
648 |
666 else path_of t; |
649 val gif_path = relative_path path (!gif_path); |
667 |
650 val rel_path = relative_path path abs_path; |
668 val gif_path = relative_path path (!gif_path); |
651 val tpath = tack_on rel_path ("." ^ tname); |
669 val rel_path = relative_path path abs_path; |
652 |
670 val tpath = tack_on rel_path ("." ^ tname); |
653 val out = open_append (tack_on path ("." ^ t ^ "_sub.html")); |
671 |
654 in output (out, |
672 val fname = tack_on path ("." ^ t ^ "_sub.html"); |
655 " |\n \\__<A HREF=\"" ^ |
673 val out = if file_exists fname then |
656 tack_on rel_path ("." ^ tname) ^ ".html\">" ^ tname ^ |
674 open_append fname handle Io s => |
657 "</A> <A HREF = \"" ^ tpath ^ "_sub.html\">\ |
675 (writeln ("Warning: Unable to write to file ." ^ |
658 \<IMG ALIGN=BOTTOM BORDER=0 SRC = \"" ^ |
676 fname); raise Io s) |
659 tack_on gif_path "red_arrow.gif\" ALT = \\/></A>\ |
677 else raise Io "File not found"; |
660 \<A HREF = \"" ^ tpath ^ "_sup.html\">\ |
678 in output (out, |
661 \<IMG ALIGN=BOTTOM BORDER=0 SRC = \"" ^ |
679 " |\n \\__<A HREF=\"" ^ |
662 tack_on gif_path "blue_arrow.gif\" ALT = /\\></A>\n"); |
680 tack_on rel_path ("." ^ tname) ^ ".html\">" ^ tname ^ |
663 close_out out |
681 "</A> <A HREF = \"" ^ tpath ^ "_sub.html\">\ |
664 end; |
682 \<IMG ALIGN=BOTTOM BORDER=0 SRC = \"" ^ |
665 |
683 tack_on gif_path "red_arrow.gif\" ALT = \\/></A>\ |
666 val theory_list = |
684 \<A HREF = \"" ^ tpath ^ "_sup.html\">\ |
667 open_append (tack_on (!index_path) ".theory_list.txt"); |
685 \<IMG ALIGN=BOTTOM BORDER=0 SRC = \"" ^ |
668 in output (theory_list, tname ^ " " ^ abs_path ^ "\n"); |
686 tack_on gif_path "blue_arrow.gif\" ALT = /\\></A>\n"); |
669 close_out theory_list; |
687 close_out out |
670 |
688 end; |
671 seq add_to_parents new_parents |
689 |
672 end |
690 val theory_list = |
|
691 open_append (tack_on (!index_path) ".theory_list.txt"); |
|
692 in output (theory_list, tname ^ " " ^ abs_path ^ "\n"); |
|
693 close_out theory_list; |
|
694 |
|
695 robust_seq add_to_parents new_parents |
|
696 end |
673 in if thy_uptodate andalso ml_uptodate then () |
697 in if thy_uptodate andalso ml_uptodate then () |
674 else |
698 else |
675 (if thy_file = "" then () |
699 (if thy_file = "" then () |
676 else if thy_uptodate then |
700 else if thy_uptodate then |
677 simpset := let val ThyInfo {thy_ss, ...} = the (get_thyinfo tname); |
701 let val ThyInfo {methods, data, ...} = the (get_thyinfo tname) |
678 in the thy_ss end |
702 in init_data methods (Symtab.dest (fst data)) end |
679 else |
703 else |
680 (writeln ("Reading \"" ^ name ^ ".thy\""); |
704 (writeln ("Reading \"" ^ name ^ ".thy\""); |
681 |
705 |
682 delete_thms (); |
706 delete_thms (); |
683 read_thy tname thy_file; |
707 read_thy tname thy_file; |
684 use (out_name tname); |
708 use (out_name tname); |
685 save_thy_ss (); |
709 save_data true; |
686 |
710 |
687 (*Store axioms of theory |
711 (*Store axioms of theory |
688 (but only if it's not a copy of an older theory)*) |
712 (but only if it's not a copy of an older theory)*) |
689 let val parents = parents_of_name tname; |
713 let val parents = parents_of_name tname; |
690 val this_thy = theory_of tname; |
714 val this_thy = theory_of tname; |
816 (*Add child to child list of base*) |
840 (*Add child to child list of base*) |
817 fun add_child base = |
841 fun add_child base = |
818 let val tinfo = |
842 let val tinfo = |
819 case Symtab.lookup (!loaded_thys, base) of |
843 case Symtab.lookup (!loaded_thys, base) of |
820 Some (ThyInfo {path, children, parents, thy_time, ml_time, |
844 Some (ThyInfo {path, children, parents, thy_time, ml_time, |
821 theory, thms, thy_ss, simpset, datatypes}) => |
845 theory, thms, methods, data}) => |
822 ThyInfo {path = path, |
846 ThyInfo {path = path, |
823 children = child ins children, parents = parents, |
847 children = child ins children, parents = parents, |
824 thy_time = thy_time, ml_time = ml_time, |
848 thy_time = thy_time, ml_time = ml_time, |
825 theory = theory, thms = thms, |
849 theory = theory, thms = thms, |
826 thy_ss = thy_ss, simpset = simpset, |
850 methods = methods, data = data} |
827 datatypes = datatypes} |
|
828 | None => ThyInfo {path = "", children = [child], parents = [], |
851 | None => ThyInfo {path = "", children = [child], parents = [], |
829 thy_time = None, ml_time = None, |
852 thy_time = None, ml_time = None, |
830 theory = None, thms = Symtab.null, |
853 theory = None, thms = Symtab.null, |
831 thy_ss = None, simpset = None, |
854 methods = Symtab.null, |
832 datatypes = []}; |
855 data = (Symtab.null, Symtab.null)}; |
833 in loaded_thys := Symtab.update ((base, tinfo), !loaded_thys) end; |
856 in loaded_thys := Symtab.update ((base, tinfo), !loaded_thys) end; |
834 |
857 |
835 (*Load a base theory if not already done |
858 (*Load a base theory if not already done |
836 and no cycle would be created *) |
859 and no cycle would be created *) |
837 fun load base = |
860 fun load base = |
866 | load_base [] = []; |
884 | load_base [] = []; |
867 |
885 |
868 val dummy = unlink_thy child; |
886 val dummy = unlink_thy child; |
869 val mergelist = load_base bases; |
887 val mergelist = load_base bases; |
870 |
888 |
|
889 val base_thy = (writeln ("Loading theory " ^ (quote child)); |
|
890 merge_thy_list mk_draft (map theory_of mergelist)); |
|
891 |
|
892 val datas = |
|
893 let fun get_data t = |
|
894 let val ThyInfo {data, ...} = the (get_thyinfo t) |
|
895 in snd data end; |
|
896 in map (Symtab.dest o get_data) mergelist end; |
|
897 |
|
898 val methods = |
|
899 let fun get_methods t = |
|
900 let val ThyInfo {methods, ...} = the (get_thyinfo t) |
|
901 in methods end; |
|
902 |
|
903 val ms = map get_methods mergelist; |
|
904 in if null ms then Symtab.null |
|
905 else foldl (Symtab.merge (fn (x,y) => true)) (hd ms, tl ms) |
|
906 end; |
|
907 |
|
908 (*merge two sorted association lists*) |
|
909 fun merge_two ([], d2) = d2 |
|
910 | merge_two (d1, []) = d1 |
|
911 | merge_two (l1 as ((p1 as (id1 : string, d1)) :: d1s), |
|
912 l2 as ((p2 as (id2, d2)) :: d2s)) = |
|
913 if id1 < id2 then |
|
914 p1 :: merge_two (d1s, l2) |
|
915 else |
|
916 p2 :: merge_two (l1, d2s); |
|
917 |
|
918 (*Merge multiple occurence of data; also call put for each merged list*) |
|
919 fun merge_multi [] None = [] |
|
920 | merge_multi [] (Some (id, ds)) = |
|
921 let val ThyMethods {merge, put, ...} = |
|
922 the (Symtab.lookup (methods, id)); |
|
923 in put (merge ds); [id] end |
|
924 | merge_multi ((id, d) :: ds) None = merge_multi ds (Some (id, [d])) |
|
925 | merge_multi ((id, d) :: ds) (Some (id2, d2s)) = |
|
926 if id = id2 then |
|
927 merge_multi ds (Some (id2, d :: d2s)) |
|
928 else |
|
929 let val ThyMethods {merge, put, ...} = |
|
930 the (Symtab.lookup (methods, id2)); |
|
931 in put (merge d2s); |
|
932 id2 :: merge_multi ds (Some (id, [d])) |
|
933 end; |
|
934 |
|
935 val merged = |
|
936 if null datas then [] |
|
937 else merge_multi (foldl merge_two (hd datas, tl datas)) None; |
|
938 |
|
939 val dummy = |
|
940 let val unmerged = map fst (Symtab.dest methods) \\ merged; |
|
941 |
|
942 fun put_empty id = |
|
943 let val ThyMethods {merge, put, ...} = |
|
944 the (Symtab.lookup (methods, id)); |
|
945 in put (merge []) end; |
|
946 in seq put_empty unmerged end; |
|
947 |
871 val dummy = |
948 val dummy = |
872 let val tinfo = case Symtab.lookup (!loaded_thys, child) of |
949 let val tinfo = case Symtab.lookup (!loaded_thys, child) of |
873 Some (ThyInfo {path, children, thy_time, ml_time, theory, thms, |
950 Some (ThyInfo {path, children, thy_time, ml_time, theory, thms, |
874 thy_ss, simpset, datatypes, ...}) => |
951 data, ...}) => |
875 ThyInfo {path = path, |
952 ThyInfo {path = path, |
876 children = children, parents = mergelist, |
953 children = children, parents = mergelist, |
877 thy_time = thy_time, ml_time = ml_time, |
954 thy_time = thy_time, ml_time = ml_time, |
878 theory = theory, thms = thms, |
955 theory = theory, thms = thms, |
879 thy_ss = thy_ss, simpset = simpset, |
956 methods = methods, data = data} |
880 datatypes = datatypes} |
|
881 | None => error ("set_parents: theory " ^ child ^ " not found"); |
957 | None => error ("set_parents: theory " ^ child ^ " not found"); |
882 in loaded_thys := Symtab.update ((child, tinfo), !loaded_thys) end; |
958 in loaded_thys := Symtab.update ((child, tinfo), !loaded_thys) end; |
883 |
959 |
884 val base_thy = (writeln ("Loading theory " ^ (quote child)); |
|
885 merge_thy_list mk_draft (map theory_of mergelist)); |
|
886 in cur_thyname := child; |
960 in cur_thyname := child; |
887 simpset := foldr merge_ss (mapfilter get_simpset mergelist, empty_ss); |
|
888 base_thy |
961 base_thy |
889 end; |
962 end; |
890 |
963 |
891 (*Change theory object for an existent item of loaded_thys*) |
964 (*Change theory object for an existent item of loaded_thys*) |
892 fun store_theory (thy, tname) = |
965 fun store_theory (thy, tname) = |
893 let val tinfo = case Symtab.lookup (!loaded_thys, tname) of |
966 let val tinfo = case Symtab.lookup (!loaded_thys, tname) of |
894 Some (ThyInfo {path, children, parents, thy_time, ml_time, thms, |
967 Some (ThyInfo {path, children, parents, thy_time, ml_time, thms, |
895 thy_ss, simpset, datatypes, ...}) => |
968 methods, data, ...}) => |
896 ThyInfo {path = path, children = children, parents = parents, |
969 ThyInfo {path = path, children = children, parents = parents, |
897 thy_time = thy_time, ml_time = ml_time, |
970 thy_time = thy_time, ml_time = ml_time, |
898 theory = Some thy, thms = thms, |
971 theory = Some thy, thms = thms, |
899 thy_ss = thy_ss, simpset = simpset, |
972 methods = methods, data = data} |
900 datatypes = datatypes} |
|
901 | None => error ("store_theory: theory " ^ tname ^ " not found"); |
973 | None => error ("store_theory: theory " ^ tname ^ " not found"); |
902 in loaded_thys := Symtab.update ((tname, tinfo), !loaded_thys) |
974 in loaded_thys := Symtab.update ((tname, tinfo), !loaded_thys) end; |
903 end; |
|
904 |
975 |
905 |
976 |
906 (*** Store and retrieve theorems ***) |
977 (*** Store and retrieve theorems ***) |
907 |
978 |
908 (*Guess to which theory a signature belongs and return it's thy_info*) |
979 (*Guess to which theory a signature belongs and return it's thy_info*) |
1201 end; |
1271 end; |
1202 |
1272 |
1203 fun print_theory thy = (Drule.print_theory thy; print_thms thy); |
1273 fun print_theory thy = (Drule.print_theory thy; print_thms thy); |
1204 |
1274 |
1205 |
1275 |
1206 (*** Store and retrieve information about datatypes ***) |
|
1207 fun store_datatype (name, cons) = |
|
1208 let val tinfo = case get_thyinfo (!cur_thyname) of |
|
1209 Some (ThyInfo {path, children, parents, thy_time, ml_time, theory, |
|
1210 thms, thy_ss, simpset, datatypes}) => |
|
1211 ThyInfo {path = path, children = children, parents = parents, |
|
1212 thy_time = thy_time, ml_time = ml_time, |
|
1213 theory = theory, thms = thms, |
|
1214 thy_ss = thy_ss, simpset = simpset, |
|
1215 datatypes = (name, cons) :: datatypes} |
|
1216 | None => error "store_datatype: theory not found"; |
|
1217 in loaded_thys := Symtab.update ((!cur_thyname, tinfo), !loaded_thys) end; |
|
1218 |
|
1219 fun datatypes_of thy = |
|
1220 let val (_, ThyInfo {datatypes, ...}) = thyinfo_of_sign (sign_of thy); |
|
1221 in datatypes end; |
|
1222 |
|
1223 |
|
1224 (*** Misc functions ***) |
1276 (*** Misc functions ***) |
1225 |
1277 |
1226 (*Get simpset of a theory*) |
1278 (*Add data handling methods to theory*) |
1227 fun simpset_of tname = |
1279 fun add_thydata thy (new_methods as (id, ThyMethods {get, ...})) = |
1228 case get_thyinfo tname of |
1280 let val (tname, ThyInfo {path, children, parents, thy_time, ml_time, theory, |
1229 Some (ThyInfo {simpset, ...}) => |
1281 thms, methods, data}) = |
1230 if is_some simpset then the simpset |
1282 thyinfo_of_sign (sign_of thy); |
1231 else error ("Simpset of theory " ^ tname ^ " has not been stored yet") |
1283 in loaded_thys := Symtab.update ((tname, ThyInfo {path = path, |
1232 | None => error ("Theory " ^ tname ^ " not stored by loader"); |
1284 children = children, parents = parents, thy_time = thy_time, |
|
1285 ml_time = ml_time, theory = theory, thms = thms, |
|
1286 methods = Symtab.update (new_methods, methods), data = data}), |
|
1287 !loaded_thys) |
|
1288 end; |
|
1289 |
|
1290 (*Add file to thy_reader_files list*) |
|
1291 fun set_thy_reader_file file = |
|
1292 let val file' = absolute_path (pwd ()) file; |
|
1293 in thy_reader_files := file' :: (!thy_reader_files) end; |
|
1294 |
|
1295 (*Add file and also 'use' it*) |
|
1296 fun add_thy_reader_file file = (set_thy_reader_file file; use file); |
|
1297 |
|
1298 (*Read all files contained in thy_reader_files list*) |
|
1299 fun read_thy_reader_files () = seq use (!thy_reader_files); |
|
1300 |
|
1301 |
|
1302 (*Retrieve data associated with theory*) |
|
1303 fun get_thydata thy id = |
|
1304 let val (tname, ThyInfo {data = (_, d2), ...}) = |
|
1305 thyinfo_of_sign (sign_of thy); |
|
1306 in Symtab.lookup (d2, id) end; |
|
1307 |
1233 |
1308 |
1234 (*CD to a directory and load its ROOT.ML file; |
1309 (*CD to a directory and load its ROOT.ML file; |
1235 also do some work for HTML generation*) |
1310 also do some work for HTML generation*) |
1236 fun use_dir dirname = |
1311 fun use_dir dirname = |
1237 (cd dirname; |
1312 (cd dirname; |