# HG changeset patch # User wenzelm # Date 876921521 -7200 # Node ID 0258594baaa9f52e90f0b79c4464e01c39884d28 # Parent 83c5310aaaabca168c490aa76be66afdd96a11a2 remove merge_theories; merge_list: always prepares extend -- no longer supports aliasing merges; diff -r 83c5310aaaab -r 0258594baaa9 src/Pure/theory.ML --- a/src/Pure/theory.ML Wed Oct 15 15:17:32 1997 +0200 +++ b/src/Pure/theory.ML Wed Oct 15 15:18:41 1997 +0200 @@ -28,7 +28,6 @@ val cert_axm : Sign.sg -> string * term -> string * term val read_axm : Sign.sg -> string * string -> string * term val inferT_axm : Sign.sg -> string * term -> string * term - val merge_theories : theory * theory -> theory end signature THEORY = @@ -75,11 +74,11 @@ val add_path : string -> theory -> theory val add_space : string * string list -> theory -> theory val add_name : string -> theory -> theory - val init_data : string * exn * (exn * exn -> exn) * (string -> exn -> Pretty.T) - -> theory -> theory + val init_data : string * exn * (exn -> exn) * (exn * exn -> exn) * + (string -> exn -> unit) -> theory -> theory val get_data : theory -> string -> exn val put_data : string * exn -> theory -> theory - val merge_thy_list : bool -> theory list -> theory + val merge_list : theory list -> theory end; @@ -118,13 +117,12 @@ (* the Pure theories *) -fun make_thy sign parents = - Theory {sign = sign, new_axioms = Symtab.null, - oracles = Symtab.null, parents = parents}; +fun make_thy sign axms oras parents = + Theory {sign = sign, new_axioms = axms, oracles = oras, parents = parents}; -val proto_pure_thy = make_thy Sign.proto_pure []; -val pure_thy = make_thy Sign.pure [proto_pure_thy]; -val cpure_thy = make_thy Sign.cpure [proto_pure_thy]; +val proto_pure_thy = make_thy Sign.proto_pure Symtab.null Symtab.null []; +val pure_thy = make_thy Sign.pure Symtab.null Symtab.null [proto_pure_thy]; +val cpure_thy = make_thy Sign.cpure Symtab.null Symtab.null [proto_pure_thy]; @@ -156,8 +154,7 @@ handle Symtab.DUPS names => err_dup_oras names; val parents' = if draft then parents else [thy]; in - Theory {sign = sign', new_axioms = new_axioms', - oracles = oracles', parents = parents'} + make_thy sign' new_axioms' oracles' parents' end; @@ -379,6 +376,7 @@ val add_defs = ext_defns read_axm; + (** additional theory data **) val init_data = ext_sg Sign.init_data; @@ -389,34 +387,33 @@ (** merge theories **) -fun merge_thy_list mk_draft thys = +(*merge list of theories from left to right, preparing extend*) +fun merge_list thys = let fun is_union thy = forall (fn t => subthy (t, thy)) thys; val is_draft = Sign.is_draft o sign_of; fun add_sign (sg, Theory {sign, ...}) = - Sign.merge (sg, sign) handle TERM (msg, _) => error msg; + Sign.nontriv_merge (sg, sign) handle TERM (msg, _) => error msg; fun oracles_of (Theory {oracles, ...}) = Symtab.dest oracles; fun eq_ora ((_, (_, s1: stamp)), (_, (_, s2))) = s1 = s2; - val all_oracles = - Symtab.make (gen_distinct eq_ora (flat (map oracles_of thys))) - handle Symtab.DUPS names => err_dup_oras names; in - (case (find_first is_union thys, exists is_draft thys) of - (Some thy, _) => thy - | (None, true) => raise THEORY ("Illegal merge of draft theories", thys) - | (None, false) => Theory { - sign = - (if mk_draft then Sign.make_draft else I) - (foldl add_sign (Sign.proto_pure, thys)), - new_axioms = Symtab.null, - oracles = all_oracles, - parents = thys}) + if exists is_draft thys then + raise THEORY ("Illegal merge of draft theories", thys) + else + (case find_first is_union thys of + Some (Theory {sign, oracles, new_axioms = _, parents = _}) => + make_thy (Sign.prep_ext sign) Symtab.null oracles thys + | None => + make_thy + (Sign.prep_ext (foldl add_sign (Sign.proto_pure, thys))) + Symtab.null + (Symtab.make (gen_distinct eq_ora (flat (map oracles_of thys))) + handle Symtab.DUPS names => err_dup_oras names) + thys) end; -fun merge_theories (thy1, thy2) = merge_thy_list false [thy1, thy2]; - end;