specifications_of: more detailed information;
authorwenzelm
Fri May 05 19:32:33 2006 +0200 (2006-05-05)
changeset 195691c23356a8ea8
parent 19568 6fa47aad35e9
child 19570 f199cb2295fd
specifications_of: more detailed information;
tuned;
src/Pure/defs.ML
     1.1 --- a/src/Pure/defs.ML	Fri May 05 18:39:16 2006 +0200
     1.2 +++ b/src/Pure/defs.ML	Fri May 05 19:32:33 2006 +0200
     1.3 @@ -9,23 +9,26 @@
     1.4  signature DEFS =
     1.5  sig
     1.6    type T
     1.7 -  val define: (string -> typ) -> (bool * string) * string
     1.8 -    -> string * typ -> (string * typ) list -> T -> T
     1.9 +  val define: (string -> typ) -> bool -> string -> string ->
    1.10 +    string * typ -> (string * typ) list -> T -> T
    1.11    val empty: T
    1.12 -  val specifications_of: T -> string -> (typ * (string * string)) list
    1.13 +  val specifications_of: T -> string ->
    1.14 +   (serial * {is_def: bool, module: string, name: string, lhs: typ, rhs: (string * typ) list}) list
    1.15    val merge: Pretty.pp -> T * T -> T
    1.16  end
    1.17  
    1.18  structure Defs: DEFS =
    1.19  struct
    1.20  
    1.21 +
    1.22  (** datatype T **)
    1.23  
    1.24 +type spec = {is_def: bool, module: string, name: string, lhs: typ, rhs: (string * typ) list};
    1.25 +
    1.26  datatype T = Defs of
    1.27   {consts: typ Graph.T,
    1.28      (*constant declarations and dependencies*)
    1.29 -  specified: (bool * string * string * typ) Inttab.table Symtab.table};
    1.30 -    (*is proper definition?, theory name, specification name and const type*)
    1.31 +  specified: spec Inttab.table Symtab.table};
    1.32  
    1.33  fun make_defs (consts, specified) = Defs {consts = consts, specified = specified};
    1.34  fun map_defs f (Defs {consts, specified}) = make_defs (f (consts, specified));
    1.35 @@ -37,10 +40,11 @@
    1.36    (Type.raw_unify (T, Logic.incr_tvar (maxidx_of_typ T + 1) U) Vartab.empty; false)
    1.37      handle Type.TUNIFY => true;
    1.38  
    1.39 -fun check_specified c (i, (_, a, _, T)) = Inttab.forall (fn (j, (_, b, _, U)) =>
    1.40 -  i = j orelse not (Type.could_unify (T, U)) orelse disjoint_types T U orelse
    1.41 -    error ("Type clash in specifications " ^ quote a ^ " and " ^ quote b ^
    1.42 -      " for constant " ^ quote c));
    1.43 +fun check_specified c (i, {lhs = T, name = a, ...}: spec) =
    1.44 +  Inttab.forall (fn (j, {lhs = U, name = b, ...}: spec) =>
    1.45 +    i = j orelse not (Type.could_unify (T, U)) orelse disjoint_types T U orelse
    1.46 +      error ("Type clash in specifications " ^ quote a ^ " and " ^ quote b ^
    1.47 +        " for constant " ^ quote c));
    1.48  
    1.49  
    1.50  (* define consts *)
    1.51 @@ -49,14 +53,14 @@
    1.52    error ("Cyclic dependency of constants:\n" ^
    1.53      cat_lines (map (space_implode " -> " o map quote o rev) cycles));
    1.54  
    1.55 -fun define const_type ((is_def, thyname), name) lhs rhs = map_defs (fn (consts, specified) =>
    1.56 +fun define const_type is_def module name lhs rhs = map_defs (fn (consts, specified) =>
    1.57    let
    1.58      fun declare (a, _) = Graph.default_node (a, const_type a);
    1.59      fun add_deps (a, bs) G = Graph.add_deps_acyclic (a, bs) G
    1.60        handle Graph.CYCLES cycles => err_cyclic cycles;
    1.61  
    1.62      val (c, T) = lhs;
    1.63 -    val spec = (serial (), (is_def, name, thyname, T));
    1.64 +    val spec = (serial (), {is_def = is_def, module = module, name = name, lhs = T, rhs = rhs});
    1.65      val no_overloading = Type.raw_instance (const_type c, T);
    1.66  
    1.67      val consts' =
    1.68 @@ -69,10 +73,7 @@
    1.69    in (consts', specified') end);
    1.70  
    1.71  fun specifications_of (Defs {specified, ...}) c =
    1.72 -  (map_filter
    1.73 -    (fn (_, (false, _, _, _)) => NONE
    1.74 -      | (_, (true, specname, thyname, ty)) => SOME (ty, (specname, thyname))) o Inttab.dest
    1.75 -    o the_default Inttab.empty o Symtab.lookup specified) c;
    1.76 +  Inttab.dest (the_default Inttab.empty (Symtab.lookup specified c));
    1.77  
    1.78  
    1.79  (* empty and merge *)