allow dependencies of disjoint collections of instances;
authorwenzelm
Thu May 11 19:15:13 2006 +0200 (2006-05-11)
changeset 196139bf274ec94cf
parent 19612 1e133047809a
child 19614 d6b806032ccc
allow dependencies of disjoint collections of instances;
major cleanup;
src/Pure/defs.ML
     1.1 --- a/src/Pure/defs.ML	Thu May 11 19:15:12 2006 +0200
     1.2 +++ b/src/Pure/defs.ML	Thu May 11 19:15:13 2006 +0200
     1.3 @@ -2,55 +2,126 @@
     1.4      ID:         $Id$
     1.5      Author:     Makarius
     1.6  
     1.7 -Global well-formedness checks for constant definitions -- covers
     1.8 -dependencies of simple sub-structural overloading.
     1.9 +Global well-formedness checks for constant definitions.  Covers
    1.10 +dependencies of simple sub-structural overloading, where type
    1.11 +arguments are approximated by the outermost type constructor.
    1.12  *)
    1.13  
    1.14  signature DEFS =
    1.15  sig
    1.16    type T
    1.17 -  val define: (string * typ -> typ list) ->
    1.18 -    bool -> string -> string -> string * typ -> (string * typ) list -> T -> T
    1.19    val specifications_of: T -> string ->
    1.20     (serial * {is_def: bool, module: string, name: string, lhs: typ, rhs: (string * typ) list}) list
    1.21    val empty: T
    1.22 -  val merge: Pretty.pp -> T * T -> T
    1.23 +  val merge: T * T -> T
    1.24 +  val define: (string * typ -> typ list) ->
    1.25 +    bool -> string -> string -> string * typ -> (string * typ) list -> T -> T
    1.26  end
    1.27  
    1.28  structure Defs: DEFS =
    1.29  struct
    1.30  
    1.31 +(* dependency items *)
    1.32  
    1.33 -(** datatype T **)
    1.34 +(*
    1.35 +  Constant c covers all instances of c
    1.36 +
    1.37 +  Instance (c, a) covers all instances of applications (c, [Type (a, _)])
    1.38 +
    1.39 +  Different Constant/Constant or Instance/Instance items represent
    1.40 +  disjoint sets of instances.  The set Constant c subsumes any
    1.41 +  Instance (c, a) -- dependencies are propagated accordingly.
    1.42 +*)
    1.43 +
    1.44 +datatype item =
    1.45 +  Constant of string |
    1.46 +  Instance of string * string;
    1.47 +
    1.48 +fun make_item (c, [Type (a, _)]) = Instance (c, a)
    1.49 +  | make_item (c, _) = Constant c;
    1.50 +
    1.51 +fun pretty_item (Constant c) = Pretty.str (quote c)
    1.52 +  | pretty_item (Instance (c, a)) = Pretty.str (quote c ^ " (type " ^ quote a ^ ")");
    1.53 +
    1.54 +fun item_ord (Constant c, Constant c') = fast_string_ord (c, c')
    1.55 +  | item_ord (Instance ca, Instance ca') = prod_ord fast_string_ord fast_string_ord (ca, ca')
    1.56 +  | item_ord (Constant _, Instance _) = LESS
    1.57 +  | item_ord (Instance _, Constant _) = GREATER;
    1.58 +
    1.59 +structure Items = GraphFun(type key = item val ord = item_ord);
    1.60 +
    1.61 +fun declare_edge (i, j) =
    1.62 +  Items.default_node (i, ()) #>
    1.63 +  Items.default_node (j, ()) #>
    1.64 +  Items.add_edge_acyclic (i, j);
    1.65 +
    1.66 +fun propagate_deps insts deps =
    1.67 +  let
    1.68 +    fun insts_of c = map (fn a => Instance (c, a)) (Symtab.lookup_list insts c);
    1.69 +    fun inst_edge (Constant c) (Constant d) = fold declare_edge (product (insts_of c) (insts_of d))
    1.70 +      | inst_edge (Constant c) j = fold (fn i => declare_edge (i, j)) (insts_of c)
    1.71 +      | inst_edge i (Constant c) = fold (fn j => declare_edge (i, j)) (insts_of c)
    1.72 +      | inst_edge (Instance _) (Instance _) = I;
    1.73 +  in Items.fold (fn (i, (_, (_, js))) => fold (inst_edge i) js) deps deps end;
    1.74 +
    1.75 +
    1.76 +(* specifications *)
    1.77  
    1.78  type spec = {is_def: bool, module: string, name: string, lhs: typ, rhs: (string * typ) list};
    1.79  
    1.80  datatype T = Defs of
    1.81 - {consts: unit Graph.T,
    1.82 -  specified: spec Inttab.table Symtab.table};
    1.83 + {specs: (bool * spec Inttab.table) Symtab.table,
    1.84 +  insts: string list Symtab.table,
    1.85 +  deps: unit Items.T};
    1.86 +
    1.87 +fun no_overloading_of (Defs {specs, ...}) c =
    1.88 +  (case Symtab.lookup specs c of
    1.89 +    SOME (b, _) => b
    1.90 +  | NONE => false);
    1.91  
    1.92 -fun make_defs (consts, specified) = Defs {consts = consts, specified = specified};
    1.93 -fun map_defs f (Defs {consts, specified}) = make_defs (f (consts, specified));
    1.94 +fun specifications_of (Defs {specs, ...}) c =
    1.95 +  (case Symtab.lookup specs c of
    1.96 +    SOME (_, sps) => Inttab.dest sps
    1.97 +  | NONE => []);
    1.98  
    1.99 -fun cyclic cycles =
   1.100 -  "Cyclic dependency of constants:\n" ^
   1.101 -    cat_lines (map (space_implode " -> " o map quote o rev) cycles);
   1.102 +fun make_defs (specs, insts, deps) = Defs {specs = specs, insts = insts, deps = deps};
   1.103 +fun map_defs f (Defs {specs, insts, deps}) = make_defs (f (specs, insts, deps));
   1.104 +
   1.105 +val empty = make_defs (Symtab.empty, Symtab.empty, Items.empty);
   1.106  
   1.107  
   1.108 -(* specified consts *)
   1.109 +(* merge *)
   1.110  
   1.111  fun disjoint_types T U =
   1.112    (Type.raw_unify (T, Logic.incr_tvar (maxidx_of_typ T + 1) U) Vartab.empty; false)
   1.113      handle Type.TUNIFY => true;
   1.114  
   1.115 -fun check_specified c (i, {lhs = T, name = a, ...}: spec) =
   1.116 +fun disjoint_specs c (i, {lhs = T, name = a, ...}: spec) =
   1.117    Inttab.forall (fn (j, {lhs = U, name = b, ...}: spec) =>
   1.118      i = j orelse not (Type.could_unify (T, U)) orelse disjoint_types T U orelse
   1.119        error ("Type clash in specifications " ^ quote a ^ " and " ^ quote b ^
   1.120          " for constant " ^ quote c));
   1.121  
   1.122 +fun cycle_msg css =
   1.123 +  let
   1.124 +    fun prt_cycle items = Pretty.block (flat
   1.125 +      (separate [Pretty.str " -> ", Pretty.brk 1] (map (single o pretty_item) items)));
   1.126 +  in Pretty.string_of (Pretty.big_list "Cyclic dependency of constants:" (map prt_cycle css)) end;
   1.127  
   1.128 -(* substructural type arguments *)
   1.129 +
   1.130 +fun merge
   1.131 +   (Defs {specs = specs1, insts = insts1, deps = deps1},
   1.132 +    Defs {specs = specs2, insts = insts2, deps = deps2}) =
   1.133 +  let
   1.134 +    val specs' = (specs1, specs2) |> Symtab.join (fn c => fn ((b, sps1), (_, sps2)) =>
   1.135 +      (b, Inttab.fold (fn sp2 => (disjoint_specs c sp2 sps1; Inttab.update sp2)) sps2 sps1));
   1.136 +    val insts' = Symtab.merge_list (op =) (insts1, insts2);
   1.137 +    val items' = propagate_deps insts' (Items.merge_acyclic (K true) (deps1, deps2))
   1.138 +      handle Items.CYCLES cycles => error (cycle_msg cycles);
   1.139 +  in make_defs (specs', insts', items') end;
   1.140 +
   1.141 +
   1.142 +(* define *)
   1.143  
   1.144  fun struct_less T (Type (_, Us)) = exists (struct_le T) Us
   1.145    | struct_less _ _ = false
   1.146 @@ -60,44 +131,35 @@
   1.147  fun structs_less Ts Us = Ts <> Us andalso structs_le Ts Us;
   1.148  
   1.149  
   1.150 -(* define consts *)
   1.151 -
   1.152 -fun define const_typargs is_def module name lhs rhs = map_defs (fn (consts, specified) =>
   1.153 +fun define const_typargs is_def module name lhs rhs defs = defs
   1.154 +    |> map_defs (fn (specs, insts, deps) =>
   1.155    let
   1.156      val (c, T) = lhs;
   1.157      val args = const_typargs lhs;
   1.158 -    val deps = rhs |> map_filter (fn d =>
   1.159 -      if structs_less (const_typargs d) args then NONE else SOME (#1 d));
   1.160      val no_overloading = forall Term.is_TVar args andalso not (has_duplicates (op =) args);
   1.161  
   1.162 -    val consts' = fold (fn (a, _) => Graph.default_node (a, ())) (lhs :: rhs) consts;
   1.163 -    val consts'' = Graph.add_deps_acyclic (c, deps) consts' handle Graph.CYCLES cycles =>
   1.164 -      if no_overloading then error (cyclic cycles)
   1.165 -      else (warning (cyclic cycles ^ "\nUnchecked overloaded specification: " ^ name); consts');
   1.166 -
   1.167      val spec = (serial (), {is_def = is_def, module = module, name = name, lhs = T, rhs = rhs});
   1.168 -    val specified' = specified
   1.169 -      |> Symtab.default (c, Inttab.empty)
   1.170 -      |> Symtab.map_entry c (fn specs => (check_specified c spec specs; Inttab.update spec specs));
   1.171 -  in (consts', specified') end);
   1.172 -
   1.173 -fun specifications_of (Defs {specified, ...}) c =
   1.174 -  Inttab.dest (the_default Inttab.empty (Symtab.lookup specified c));
   1.175 -
   1.176 -
   1.177 -(* empty and merge *)
   1.178 +    val specs' = specs
   1.179 +      |> Symtab.default (c, (false, Inttab.empty))
   1.180 +      |> Symtab.map_entry c (fn (_, sps) =>
   1.181 +          (disjoint_specs c spec sps; (no_overloading, Inttab.update spec sps)));
   1.182  
   1.183 -val empty = make_defs (Graph.empty, Symtab.empty);
   1.184 +    val lhs' = make_item (c, if no_overloading then [] else args);
   1.185 +    val rhs' = rhs |> map_filter (fn (c', T') =>
   1.186 +      let val args' = const_typargs (c', T') in
   1.187 +        if structs_less args' args then NONE
   1.188 +        else SOME (make_item (c', if no_overloading_of defs c' then [] else args'))
   1.189 +      end);
   1.190  
   1.191 -fun merge pp
   1.192 -   (Defs {consts = consts1, specified = specified1},
   1.193 -    Defs {consts = consts2, specified = specified2}) =
   1.194 -  let
   1.195 -    val consts' = (consts1, consts2) |> Graph.merge_acyclic (K true)
   1.196 -      handle Graph.CYCLES cycles => error (cyclic cycles);
   1.197 -    val specified' = (specified1, specified2) |> Symtab.join (fn c => fn (orig_specs1, specs2) =>
   1.198 -      Inttab.fold (fn spec2 => fn specs1 =>
   1.199 -        (check_specified c spec2 orig_specs1; Inttab.update spec2 specs1)) specs2 orig_specs1);
   1.200 -  in make_defs (consts', specified') end;
   1.201 +    val insts' = insts
   1.202 +      |> fold (fn Instance ca => Symtab.insert_list (op =) ca | _ => I) (lhs' :: rhs');
   1.203 +    val deps' = deps
   1.204 +      |> fold (fn r => declare_edge (r, lhs')) rhs'
   1.205 +      |> propagate_deps insts'
   1.206 +      handle Items.CYCLES cycles =>
   1.207 +        if no_overloading then error (cycle_msg cycles)
   1.208 +        else (warning (cycle_msg cycles ^ "\nUnchecked overloaded specification: " ^ name); deps);
   1.209 +
   1.210 +  in (specs', insts', deps') end);
   1.211  
   1.212  end;