# HG changeset patch # User wenzelm # Date 1146850353 -7200 # Node ID 1c23356a8ea849c663bd9728c1ddd3d305a5a37a # Parent 6fa47aad35e94b4365f977a1621093c456f2dd03 specifications_of: more detailed information; tuned; diff -r 6fa47aad35e9 -r 1c23356a8ea8 src/Pure/defs.ML --- a/src/Pure/defs.ML Fri May 05 18:39:16 2006 +0200 +++ b/src/Pure/defs.ML Fri May 05 19:32:33 2006 +0200 @@ -9,23 +9,26 @@ signature DEFS = sig type T - val define: (string -> typ) -> (bool * string) * string - -> string * typ -> (string * typ) list -> T -> T + val define: (string -> typ) -> bool -> string -> string -> + string * typ -> (string * typ) list -> T -> T val empty: T - val specifications_of: T -> string -> (typ * (string * string)) list + val specifications_of: T -> string -> + (serial * {is_def: bool, module: string, name: string, lhs: typ, rhs: (string * typ) list}) list val merge: Pretty.pp -> T * T -> T end structure Defs: DEFS = struct + (** datatype T **) +type spec = {is_def: bool, module: string, name: string, lhs: typ, rhs: (string * typ) list}; + datatype T = Defs of {consts: typ Graph.T, (*constant declarations and dependencies*) - specified: (bool * string * string * typ) Inttab.table Symtab.table}; - (*is proper definition?, theory name, specification name and const type*) + specified: spec Inttab.table Symtab.table}; fun make_defs (consts, specified) = Defs {consts = consts, specified = specified}; fun map_defs f (Defs {consts, specified}) = make_defs (f (consts, specified)); @@ -37,10 +40,11 @@ (Type.raw_unify (T, Logic.incr_tvar (maxidx_of_typ T + 1) U) Vartab.empty; false) handle Type.TUNIFY => true; -fun check_specified c (i, (_, a, _, T)) = Inttab.forall (fn (j, (_, b, _, U)) => - i = j orelse not (Type.could_unify (T, U)) orelse disjoint_types T U orelse - error ("Type clash in specifications " ^ quote a ^ " and " ^ quote b ^ - " for constant " ^ quote c)); +fun check_specified c (i, {lhs = T, name = a, ...}: spec) = + Inttab.forall (fn (j, {lhs = U, name = b, ...}: spec) => + i = j orelse not (Type.could_unify (T, U)) orelse disjoint_types T U orelse + error ("Type clash in specifications " ^ quote a ^ " and " ^ quote b ^ + " for constant " ^ quote c)); (* define consts *) @@ -49,14 +53,14 @@ error ("Cyclic dependency of constants:\n" ^ cat_lines (map (space_implode " -> " o map quote o rev) cycles)); -fun define const_type ((is_def, thyname), name) lhs rhs = map_defs (fn (consts, specified) => +fun define const_type is_def module name lhs rhs = map_defs (fn (consts, specified) => let fun declare (a, _) = Graph.default_node (a, const_type a); fun add_deps (a, bs) G = Graph.add_deps_acyclic (a, bs) G handle Graph.CYCLES cycles => err_cyclic cycles; val (c, T) = lhs; - val spec = (serial (), (is_def, name, thyname, T)); + val spec = (serial (), {is_def = is_def, module = module, name = name, lhs = T, rhs = rhs}); val no_overloading = Type.raw_instance (const_type c, T); val consts' = @@ -69,10 +73,7 @@ in (consts', specified') end); fun specifications_of (Defs {specified, ...}) c = - (map_filter - (fn (_, (false, _, _, _)) => NONE - | (_, (true, specname, thyname, ty)) => SOME (ty, (specname, thyname))) o Inttab.dest - o the_default Inttab.empty o Symtab.lookup specified) c; + Inttab.dest (the_default Inttab.empty (Symtab.lookup specified c)); (* empty and merge *)