src/Pure/defs.ML
changeset 24199 8be734b5f59f
parent 20668 00521d5e1838
child 24792 fd4655e57168
     1.1 --- a/src/Pure/defs.ML	Thu Aug 09 15:52:53 2007 +0200
     1.2 +++ b/src/Pure/defs.ML	Thu Aug 09 15:52:54 2007 +0200
     1.3 @@ -11,14 +11,16 @@
     1.4    val pretty_const: Pretty.pp -> string * typ list -> Pretty.T
     1.5    val plain_args: typ list -> bool
     1.6    type T
     1.7 -  val specifications_of: T -> string -> (serial * {is_def: bool, thyname: string, name: string,
     1.8 -    lhs: typ list, rhs: (string * typ list) list}) list
     1.9 +  val specifications_of: T -> string -> {is_def: bool, name: string,
    1.10 +    lhs: typ list, rhs: (string * typ list) list} list
    1.11 +  val all_specifications_of: T -> (string * {is_def: bool, name: string,
    1.12 +    lhs: typ list, rhs: (string * typ list) list} list) list
    1.13    val dest: T ->
    1.14     {restricts: ((string * typ list) * string) list,
    1.15      reducts: ((string * typ list) * (string * typ list) list) list}
    1.16    val empty: T
    1.17    val merge: Pretty.pp -> T * T -> T
    1.18 -  val define: Pretty.pp -> bool -> bool -> string -> string ->
    1.19 +  val define: Pretty.pp -> bool -> bool -> string ->
    1.20      string * typ list -> (string * typ list) list -> T -> T
    1.21  end
    1.22  
    1.23 @@ -51,7 +53,7 @@
    1.24  
    1.25  (* datatype defs *)
    1.26  
    1.27 -type spec = {is_def: bool, thyname: string, name: string, lhs: args, rhs: (string * args) list};
    1.28 +type spec = {is_def: bool, name: string, lhs: args, rhs: (string * args) list};
    1.29  
    1.30  type def =
    1.31   {specs: spec Inttab.table,                 (*source specifications*)
    1.32 @@ -74,7 +76,9 @@
    1.33      SOME (def: def) => which def
    1.34    | NONE => []);
    1.35  
    1.36 -fun specifications_of (Defs defs) = lookup_list (Inttab.dest o #specs) defs;
    1.37 +fun specifications_of (Defs defs) = lookup_list (map snd o Inttab.dest o #specs) defs;
    1.38 +fun all_specifications_of (Defs defs) =
    1.39 +  ((map o apsnd) (map snd o Inttab.dest o #specs) o Symtab.dest) defs;
    1.40  val restricts_of = lookup_list #restricts;
    1.41  val reducts_of = lookup_list #reducts;
    1.42  
    1.43 @@ -197,14 +201,14 @@
    1.44  
    1.45  (* define *)
    1.46  
    1.47 -fun define pp unchecked is_def thyname name (c, args) deps (Defs defs) =
    1.48 +fun define pp unchecked is_def name (c, args) deps (Defs defs) =
    1.49    let
    1.50      val restr =
    1.51        if plain_args args orelse
    1.52          (case args of [Type (a, rec_args)] => plain_args rec_args | _ => false)
    1.53        then [] else [(args, name)];
    1.54      val spec =
    1.55 -      (serial (), {is_def = is_def, thyname = thyname, name = name, lhs = args, rhs = deps});
    1.56 +      (serial (), {is_def = is_def, name = name, lhs = args, rhs = deps});
    1.57      val defs' = defs |> update_specs c spec;
    1.58    in Defs (defs' |> (if unchecked then I else dependencies pp (c, args) restr deps)) end;
    1.59