# HG changeset patch # User haftmann # Date 1235320396 -3600 # Node ID c53242ef274ed2b97882f033e05e2f30c29e084c # Parent f84c2412e87056941cca8bb2a14f29277d3dd9fc# Parent bf6b35c5c0fc9c736a9912683feae63157ded443 merged diff -r bf6b35c5c0fc -r c53242ef274e src/Tools/code/code_wellsorted.ML --- a/src/Tools/code/code_wellsorted.ML Sun Feb 22 17:25:45 2009 +0100 +++ b/src/Tools/code/code_wellsorted.ML Sun Feb 22 17:33:16 2009 +0100 @@ -99,7 +99,7 @@ fun obtain_eqns thy eqngr c = case try (Graph.get_node eqngr) c - of SOME ((lhs, _), eqns) => ((lhs, []), eqns) + of SOME ((lhs, _), eqns) => ((lhs, []), []) | NONE => let val eqns = Code.these_eqns thy c |> burrow_fst (Code_Unit.norm_args thy) @@ -223,9 +223,10 @@ |> map swap (*FIXME*) fun add_class (class, superclasses) algebra = Sorts.add_class pp (class, Sorts.minimize_sort algebra superclasses) algebra; - fun add_arity (class, tyco) algebra = Sorts.add_arities pp - (tyco, [(class, ((map (Sorts.minimize_sort algebra) o the - o AList.lookup (op =) arities) (class, tyco)))]) algebra; + fun add_arity (class, tyco) algebra = case AList.lookup (op =) arities (class, tyco) + of SOME sorts => Sorts.add_arities pp + (tyco, [(class, map (Sorts.minimize_sort algebra) sorts)]) algebra + | NONE => algebra; in Sorts.empty_algebra |> fold add_class classrels @@ -247,13 +248,14 @@ end; fun add_arity thy vardeps (class, tyco) = - AList.update (op =) + AList.default (op =) ((class, tyco), map (fn k => (snd o Vargraph.get_node vardeps) (Inst (class, tyco), k)) (0 upto Sign.arity_number thy tyco - 1)); fun add_eqs thy (proj_sort, algebra) vardeps (c, (proto_lhs, proto_eqns)) (rhss, eqngr) = - let + if can (Graph.get_node eqngr) c then (rhss, eqngr) + else let val lhs = map_index (fn (k, (v, _)) => (v, snd (Vargraph.get_node vardeps (Fun c, k)))) proto_lhs; val inst_tab = Vartab.empty |> fold (fn (v, sort) =>