100 val add_trrules: (string * string) Syntax.trrule list -> sg -> sg |
100 val add_trrules: (string * string) Syntax.trrule list -> sg -> sg |
101 val add_trrules_i: ast Syntax.trrule list -> sg -> sg |
101 val add_trrules_i: ast Syntax.trrule list -> sg -> sg |
102 val add_path: string -> sg -> sg |
102 val add_path: string -> sg -> sg |
103 val add_space: string * string list -> sg -> sg |
103 val add_space: string * string list -> sg -> sg |
104 val add_name: string -> sg -> sg |
104 val add_name: string -> sg -> sg |
105 val make_draft: sg -> sg |
105 val init_data: string * exn * (exn -> exn) * (exn * exn -> exn) * |
106 val print_data: sg -> unit |
106 (string -> exn -> unit) -> sg -> sg |
107 val init_data: string * exn * (exn * exn -> exn) * (string -> exn -> Pretty.T) -> sg -> sg |
|
108 val get_data: sg -> string -> exn |
107 val get_data: sg -> string -> exn |
109 val put_data: string * exn -> sg -> sg |
108 val put_data: string * exn -> sg -> sg |
|
109 val print_data: sg -> string -> unit |
|
110 val prep_ext: sg -> sg |
110 val merge: sg * sg -> sg |
111 val merge: sg * sg -> sg |
|
112 val nontriv_merge: sg * sg -> sg |
111 val proto_pure: sg |
113 val proto_pure: sg |
112 val pure: sg |
114 val pure: sg |
113 val cpure: sg |
115 val cpure: sg |
114 val const_of_class: class -> string |
116 val const_of_class: class -> string |
115 val class_of_const: string -> class |
117 val class_of_const: string -> class |
354 fun pretty_arities (ty, ars) = map (pretty_arity ty) ars; |
356 fun pretty_arities (ty, ars) = map (pretty_arity ty) ars; |
355 |
357 |
356 fun pretty_const (c, ty) = Pretty.block |
358 fun pretty_const (c, ty) = Pretty.block |
357 [Pretty.str (quote c ^ " ::"), Pretty.brk 1, prt_typ ty]; |
359 [Pretty.str (quote c ^ " ::"), Pretty.brk 1, prt_typ ty]; |
358 |
360 |
359 val Sg {tsig, const_tab, syn = _, path, spaces, data = _, stamps} = sg; |
361 val Sg {tsig, const_tab, syn = _, path, spaces, data, stamps} = sg; |
360 val spaces' = sort (fn ((k1, _), (k2, _)) => k1 < k2) spaces; |
362 val spaces' = sort (fn ((k1, _), (k2, _)) => k1 < k2) spaces; |
361 val {classes, classrel, default, tycons, abbrs, arities} = |
363 val {classes, classrel, default, tycons, abbrs, arities} = |
362 Type.rep_tsig tsig; |
364 Type.rep_tsig tsig; |
363 in |
365 in |
364 Pretty.writeln (Pretty.strs ("stamps:" :: stamp_names stamps)); |
366 Pretty.writeln (Pretty.strs ("stamps:" :: stamp_names stamps)); |
|
367 Pretty.writeln (Pretty.strs ("data:" :: Data.kinds data)); |
365 Pretty.writeln (Pretty.strs ["name entry path:", NameSpace.pack path]); |
368 Pretty.writeln (Pretty.strs ["name entry path:", NameSpace.pack path]); |
366 Pretty.writeln (Pretty.big_list "name spaces:" (map pretty_space spaces')); |
369 Pretty.writeln (Pretty.big_list "name spaces:" (map pretty_space spaces')); |
367 Pretty.writeln (pretty_classes classes); |
370 Pretty.writeln (pretty_classes classes); |
368 Pretty.writeln (Pretty.big_list "class relation:" (map pretty_classrel classrel)); |
371 Pretty.writeln (Pretty.big_list "class relation:" (map pretty_classrel classrel)); |
369 Pretty.writeln (pretty_default default); |
372 Pretty.writeln (pretty_default default); |
797 val make_draft = add_name "#"; |
800 val make_draft = add_name "#"; |
798 |
801 |
799 |
802 |
800 (* additional signature data *) |
803 (* additional signature data *) |
801 |
804 |
802 fun print_data (Sg {data, ...}) = Data.print data; |
|
803 fun get_data (Sg {data, ...}) = Data.get data; |
|
804 |
|
805 fun map_data f (Sg {tsig, const_tab, syn, path, spaces, data, stamps}) = |
805 fun map_data f (Sg {tsig, const_tab, syn, path, spaces, data, stamps}) = |
806 make_sign (syn, tsig, const_tab, (path, spaces)) (f data) stamps "#"; |
806 make_sign (syn, tsig, const_tab, (path, spaces)) (f data) stamps "#"; |
807 |
807 |
808 fun init_data (kind, e, mrg, prt) = map_data (fn d => Data.init d kind e mrg prt); |
808 fun init_data (kind, e, ext, mrg, prt) = |
|
809 map_data (fn d => Data.init d kind e ext mrg prt); |
|
810 |
|
811 fun get_data (Sg {data, ...}) = Data.get data; |
809 fun put_data (kind, e) = map_data (fn d => Data.put d kind e); |
812 fun put_data (kind, e) = map_data (fn d => Data.put d kind e); |
|
813 fun print_data (Sg {data, ...}) kind = Data.print data kind; |
|
814 |
|
815 (*prepare extension*) |
|
816 val prep_ext = map_data Data.prep_ext; |
810 |
817 |
811 |
818 |
812 |
819 |
813 (** merge signatures **) (*exception TERM*) |
820 (** merge signatures **) (*exception TERM*) |
814 |
821 |
815 fun merge_aux (sg1, sg2) = |
822 fun merge_aux triv_only (sg1, sg2) = |
816 if fast_subsig (sg2, sg1) then sg1 |
823 if fast_subsig (sg2, sg1) then sg1 |
817 else if fast_subsig (sg1, sg2) then sg2 |
824 else if fast_subsig (sg1, sg2) then sg2 |
818 else if subsig (sg2, sg1) then sg1 |
825 else if subsig (sg2, sg1) then sg1 |
819 else if subsig (sg1, sg2) then sg2 |
826 else if subsig (sg1, sg2) then sg2 |
820 else if is_draft sg1 orelse is_draft sg2 then |
827 else if is_draft sg1 orelse is_draft sg2 then |
821 raise TERM ("Illegal merge of draft signatures", []) |
828 raise TERM ("Illegal merge of draft signatures", []) |
|
829 else if triv_only then |
|
830 raise TERM ("Illegal non-trivial merge of signatures", []) |
822 else |
831 else |
823 (*neither is union already; must form union*) |
832 (*neither is union already; must form union*) |
824 let |
833 let |
825 val Sg {tsig = tsig1, const_tab = const_tab1, syn = syn1, |
834 val Sg {tsig = tsig1, const_tab = const_tab1, syn = syn1, |
826 path = _, spaces = spaces1, data = data1, stamps = stamps1} = sg1; |
835 path = _, spaces = spaces1, data = data1, stamps = stamps1} = sg1; |
853 in |
862 in |
854 Sg {tsig = tsig, const_tab = const_tab, syn = syn, |
863 Sg {tsig = tsig, const_tab = const_tab, syn = syn, |
855 path = [], spaces = spaces, data = data, stamps = stamps} |
864 path = [], spaces = spaces, data = data, stamps = stamps} |
856 end; |
865 end; |
857 |
866 |
858 fun merge sgs = |
867 fun gen_merge triv sgs = |
859 (case handle_error merge_aux sgs of |
868 (case handle_error (merge_aux triv) sgs of |
860 OK sg => sg |
869 OK sg => sg |
861 | Error msg => raise TERM (msg, [])); |
870 | Error msg => raise TERM (msg, [])); |
|
871 |
|
872 val merge = gen_merge true; |
|
873 val nontriv_merge = gen_merge false; |
862 |
874 |
863 |
875 |
864 |
876 |
865 (** the Pure signature **) |
877 (** the Pure signature **) |
866 |
878 |