improved propagate_deps;
authorwenzelm
Fri May 12 01:01:08 2006 +0200 (2006-05-12)
changeset 19620ccd6de95f4a6
parent 19619 ee1104f972a4
child 19621 475140eb82f2
improved propagate_deps;
removed structs_less, which is actually unsound in conjunction with interdependent overloaded consts;
src/Pure/defs.ML
     1.1 --- a/src/Pure/defs.ML	Thu May 11 21:46:17 2006 +0200
     1.2 +++ b/src/Pure/defs.ML	Fri May 12 01:01:08 2006 +0200
     1.3 @@ -57,11 +57,10 @@
     1.4  
     1.5  fun propagate_deps insts deps =
     1.6    let
     1.7 -    fun insts_of c = map (fn a => Instance (c, a)) (Symtab.lookup_list insts c);
     1.8 -    fun inst_edge (Constant c) (Constant d) = fold declare_edge (product (insts_of c) (insts_of d))
     1.9 -      | inst_edge (Constant c) j = fold (fn i => declare_edge (i, j)) (insts_of c)
    1.10 -      | inst_edge i (Constant c) = fold (fn j => declare_edge (i, j)) (insts_of c)
    1.11 -      | inst_edge (Instance _) (Instance _) = I;
    1.12 +    fun inst_item (Constant c) = Symtab.lookup_list insts c
    1.13 +      | inst_item (Instance _) = [];
    1.14 +    fun inst_edge i j =
    1.15 +      fold declare_edge (tl (product (i :: inst_item i) (j :: inst_item j)));
    1.16    in Items.fold (fn (i, (_, (_, js))) => fold (inst_edge i) js) deps deps end;
    1.17  
    1.18  
    1.19 @@ -71,7 +70,7 @@
    1.20  
    1.21  datatype T = Defs of
    1.22   {specs: (bool * spec Inttab.table) Symtab.table,
    1.23 -  insts: string list Symtab.table,
    1.24 +  insts: item list Symtab.table,
    1.25    deps: unit Items.T};
    1.26  
    1.27  fun no_overloading_of (Defs {specs, ...}) c =
    1.28 @@ -105,7 +104,7 @@
    1.29  fun cycle_msg css =
    1.30    let
    1.31      fun prt_cycle items = Pretty.block (flat
    1.32 -      (separate [Pretty.str " -> ", Pretty.brk 1] (map (single o pretty_item) items)));
    1.33 +      (separate [Pretty.str " ->", Pretty.brk 1] (map (single o pretty_item) items)));
    1.34    in Pretty.string_of (Pretty.big_list "Cyclic dependency of constants:" (map prt_cycle css)) end;
    1.35  
    1.36  
    1.37 @@ -123,14 +122,6 @@
    1.38  
    1.39  (* define *)
    1.40  
    1.41 -fun struct_less T (Type (_, Us)) = exists (struct_le T) Us
    1.42 -  | struct_less _ _ = false
    1.43 -and struct_le T U = T = U orelse struct_less T U;
    1.44 -
    1.45 -fun structs_le Ts Us = forall (fn U => exists (fn T => struct_le T U) Ts) Us;
    1.46 -fun structs_less Ts Us = Ts <> Us andalso structs_le Ts Us;
    1.47 -
    1.48 -
    1.49  fun define const_typargs is_def module name lhs rhs defs = defs
    1.50      |> map_defs (fn (specs, insts, deps) =>
    1.51    let
    1.52 @@ -147,12 +138,12 @@
    1.53      val lhs' = make_item (c, if no_overloading then [] else args);
    1.54      val rhs' = rhs |> map_filter (fn (c', T') =>
    1.55        let val args' = const_typargs (c', T') in
    1.56 -        if structs_less args' args then NONE
    1.57 +        if forall Term.is_TVar args' then NONE
    1.58          else SOME (make_item (c', if no_overloading_of defs c' then [] else args'))
    1.59        end);
    1.60  
    1.61 -    val insts' = insts
    1.62 -      |> fold (fn Instance ca => Symtab.insert_list (op =) ca | _ => I) (lhs' :: rhs');
    1.63 +    val insts' = insts |> fold (fn i as Instance (c, _) =>
    1.64 +        Symtab.insert_list (op =) (c, i) | _ => I) (lhs' :: rhs');
    1.65      val deps' = deps
    1.66        |> fold (fn r => declare_edge (r, lhs')) rhs'
    1.67        |> propagate_deps insts'