# HG changeset patch # User wenzelm # Date 1272373399 -7200 # Node ID 7aea10d101139e7633eb1ee187b86502a6fcf2b7 # Parent 752ee03427c22c8c48bd6db1ff4c9ac69b9c6e8a tuned aritiy completion -- slightly less intermediate data structures; diff -r 752ee03427c2 -r 7aea10d10113 src/Pure/axclass.ML --- a/src/Pure/axclass.ML Tue Apr 27 14:41:27 2010 +0200 +++ b/src/Pure/axclass.ML Tue Apr 27 15:03:19 2010 +0200 @@ -249,7 +249,7 @@ |> map_filter (fn ((c', _), (_, name)) => if c = c' then SOME name else NONE) |> rev; -fun insert_arity_completions thy (t, ((c, Ss), ((th, thy_name)))) arities = +fun insert_arity_completions thy t ((c, Ss), ((th, thy_name))) (finished, arities) = let val algebra = Sign.classes_of thy; val ars = Symtab.lookup_list arities t; @@ -263,28 +263,31 @@ val completions = super_class_completions |> map (fn c1 => let - val th1 = (th RS the_classrel thy (c, c1)) + val th1 = + (th RS the_classrel thy (c, c1)) |> Drule.instantiate' std_vars [] |> Thm.close_derivation; in ((th1, thy_name), c1) end); + + val finished' = finished andalso null completions; val arities' = fold (fn (th, c1) => Symtab.cons_list (t, ((c1, Ss), th))) completions arities; - in (null completions, arities') end; + in (finished', arities') end; fun put_arity ((t, Ss, c), th) thy = - let val arity = (t, ((c, Ss), (th, Context.theory_name thy))) in + let val ar = ((c, Ss), (th, Context.theory_name thy)) in thy |> map_proven_arities - (Symtab.insert_list (eq_fst op =) arity #> insert_arity_completions thy arity #> #2) + (Symtab.insert_list (eq_fst op =) (t, ar) #> + curry (insert_arity_completions thy t ar) true #> #2) end; fun complete_arities thy = let val arities = proven_arities_of thy; - val (finished, arities') = arities - |> fold_map (insert_arity_completions thy) (Symtab.dest_list arities); + val (finished, arities') = + Symtab.fold (fn (t, ars) => fold (insert_arity_completions thy t) ars) arities (true, arities); in - if forall I finished - then NONE + if finished then NONE else SOME (map_proven_arities (K arities') thy) end;