# HG changeset patch # User wenzelm # Date 1452786313 -3600 # Node ID 4025b5ce19016b39cf0e3e38da5591706ffc344d # Parent 27c63722372247d7424586fab583feda73173a90 tuned; diff -r 27c637223722 -r 4025b5ce1901 src/Pure/defs.ML --- a/src/Pure/defs.ML Thu Jan 14 13:51:13 2016 +0100 +++ b/src/Pure/defs.ML Thu Jan 14 16:45:13 2016 +0100 @@ -170,21 +170,13 @@ val prt = Pretty.string_of oo pretty_entry; -fun err context (c, args) (d, Us) s1 s2 = - error (s1 ^ " dependency of " ^ prt context (c, args) ^ " -> " ^ prt context (d, Us) ^ s2); - -fun acyclic context (c, args) (d, Us) = - c <> d orelse - is_none (match_args (args, Us)) orelse - err context (c, args) (d, Us) "Circular" ""; +fun err context (c, Ts) (d, Us) s1 s2 = + error (s1 ^ " dependency of " ^ prt context (c, Ts) ^ " -> " ^ prt context (d, Us) ^ s2); -fun wellformed context defs (c, args) (d, Us) = - plain_args Us orelse - (case find_first (fn (Ts, _) => not (disjoint_args (Ts, Us))) (restricts_of defs d) of - SOME (Ts, description) => - err context (c, args) (d, Us) "Malformed" - ("\n(restriction " ^ prt context (d, Ts) ^ " from " ^ quote description ^ ")") - | NONE => true); +fun acyclic context (c, Ts) (d, Us) = + c <> d orelse + is_none (match_args (Ts, Us)) orelse + err context (c, Ts) (d, Us) "Circular" ""; fun reduction context defs const deps = let @@ -202,18 +194,26 @@ val _ = forall (acyclic context const) (the_default deps deps'); in deps' end; +fun restriction context defs (c, Ts) (d, Us) = + plain_args Us orelse + (case find_first (fn (Rs, _) => not (disjoint_args (Rs, Us))) (restricts_of defs d) of + SOME (Rs, description) => + err context (c, Ts) (d, Us) "Malformed" + ("\n(restriction " ^ prt context (d, Rs) ^ " from " ^ quote description ^ ")") + | NONE => true); + in fun normalize context = let fun check_def defs (c, {reducts, ...}: def) = - reducts |> forall (fn (args, deps) => forall (wellformed context defs (c, args)) deps); + reducts |> forall (fn (Ts, deps) => forall (restriction context defs (c, Ts)) deps); fun check_defs defs = Itemtab.forall (check_def defs) defs; fun norm_update (c, {reducts, ...}: def) (changed, defs) = let - val reducts' = reducts |> map (fn (args, deps) => - (args, perhaps (reduction context defs (c, args)) deps)); + val reducts' = reducts |> map (fn (Ts, deps) => + (Ts, perhaps (reduction context defs (c, Ts)) deps)); in if reducts = reducts' then (changed, defs) else (true, defs |> map_def c (fn (specs, restricts, _) => (specs, restricts, reducts')))