# HG changeset patch # User wenzelm # Date 1148385301 -7200 # Node ID c07c31ac689b8a7290886a438fbafff47277b3dd # Parent e02af528ceef6d34dd6cacea0305ea7355846a9c export plain_args; tuned wellformed, normalize; diff -r e02af528ceef -r c07c31ac689b src/Pure/defs.ML --- a/src/Pure/defs.ML Mon May 22 22:29:19 2006 +0200 +++ b/src/Pure/defs.ML Tue May 23 13:55:01 2006 +0200 @@ -3,13 +3,13 @@ Author: Makarius Global well-formedness checks for constant definitions. Covers plain -definitions and simple sub-structural overloading (depending on a -single type argument). +definitions and simple sub-structural overloading. *) signature DEFS = sig val pretty_const: Pretty.pp -> string * typ list -> Pretty.T + val plain_args: typ list -> bool type T val specifications_of: T -> string -> (serial * {is_def: bool, module: string, name: string, lhs: typ list, rhs: (string * typ list) list}) list @@ -25,7 +25,6 @@ structure Defs: DEFS = struct - (* type arguments *) type args = typ list; @@ -105,86 +104,82 @@ (disjoint_specs c spec specs; (Inttab.update spec specs, restricts, reducts))); -(* normalization: reduction and well-formedness check *) +(* normalized dependencies: reduction with well-formedness check *) local -fun reduction reds_of deps = - let - fun reduct Us (Ts, rhs) = - (case match_args (Ts, Us) of - NONE => NONE - | SOME subst => SOME (map (apsnd (map subst)) rhs)); - fun reducts (d: string, Us) = get_first (reduct Us) (reds_of d); - - fun add (NONE, dp) = insert (op =) dp - | add (SOME dps, _) = fold (insert (op =)) dps; - val deps' = map (`reducts) deps; - in - if forall (is_none o #1) deps' then NONE - else SOME (fold_rev add deps' []) - end; - -fun reductions reds_of deps = - (case reduction reds_of deps of - SOME deps' => reductions reds_of deps' - | NONE => deps); - fun contained U (Type (_, Ts)) = exists (fn T => T = U orelse contained U T) Ts | contained _ _ = false; -fun wellformed pp rests_of (c, args) (d, Us) = +fun wellformed pp defs (c, args) (d, Us) = let val prt = Pretty.string_of o pretty_const pp; fun err s1 s2 = error (s1 ^ " dependency of constant " ^ prt (c, args) ^ " -> " ^ prt (d, Us) ^ s2); in exists (fn U => exists (contained U) args) Us orelse - (c <> d andalso exists (member (op =) args) Us) orelse - (case find_first (fn (Ts, _) => not (disjoint_args (Ts, Us))) (rests_of d) of - NONE => - c <> d orelse is_none (match_args (args, Us)) orelse err "Circular" "" - | SOME (Ts, name) => - if c = d then err "Circular" ("\n(via " ^ quote name ^ ")") - else - err "Malformed" ("\n(restriction " ^ prt (d, Ts) ^ " from " ^ quote name ^ ")")) + (c <> d andalso forall (member (op =) args) Us) orelse + (if c = d andalso is_some (match_args (args, Us)) then err "Circular" "" else + (case find_first (fn (Ts, _) => not (disjoint_args (Ts, Us))) (restricts_of defs d) of + SOME (Ts, name) => + is_some (match_args (Ts, Us)) orelse + err "Malformed" ("\n(restriction " ^ prt (d, Ts) ^ " from " ^ quote name ^ ")") + | NONE => true)) end; -fun normalize pp rests_of reds_of (c, args) deps = +fun reduction pp defs const deps = let - val deps' = reductions reds_of deps; - val _ = forall (wellformed pp rests_of (c, args)) deps'; + fun reduct Us (Ts, rhs) = + (case match_args (Ts, Us) of + NONE => NONE + | SOME subst => SOME (map (apsnd (map subst)) rhs)); + fun reducts (d, Us) = get_first (reduct Us) (reducts_of defs d); + + fun add (NONE, dp) = insert (op =) dp + | add (SOME dps, _) = fold (insert (op =)) dps; + val reds = map (`reducts) deps; + val deps' = + if forall (is_none o #1) reds then NONE + else SOME (fold_rev add reds []); + val _ = forall (wellformed pp defs const) (the_default deps deps'); in deps' end; -fun normalize_all pp (c, args) deps defs = +fun normalize_all pp = let - val norm = normalize pp (restricts_of (Defs defs)); - val norm_rule = norm (fn c' => if c' = c then [(args, deps)] else []); - val norm_defs = norm (reducts_of (Defs defs)); - fun norm_update (c', {reducts, ...}: def) = - let val reducts' = reducts - |> map (fn (args', deps') => (args', norm_defs (c', args') (norm_rule (c', args') deps'))) + fun norm_update (c, {reducts, ...}: def) (changed, defs) = + let + val reducts' = reducts |> map (fn (args, deps) => + (args, perhaps (reduction pp (Defs defs) (c, args)) deps)); in - K (reducts <> reducts') ? - map_def c' (fn (specs, restricts, reducts) => (specs, restricts, reducts')) + if reducts = reducts' then (changed, defs) + else (true, defs |> map_def c (fn (specs, restricts, reducts) => + (specs, restricts, reducts'))) end; - in Symtab.fold norm_update defs defs end; + fun norm_all defs = + (case Symtab.fold norm_update defs (false, defs) of + (true, defs') => norm_all defs' + | (false, _) => defs); + in norm_all end; + +fun normalize_single pp defs const = + let + fun norm deps = + (case reduction pp defs const deps of + NONE => deps + | SOME deps' => norm deps'); + in norm end; in fun dependencies pp (c, args) restr deps (Defs defs) = let - val deps' = normalize pp (restricts_of (Defs defs)) (reducts_of (Defs defs)) (c, args) deps; - val defs' = defs - |> map_def c (fn (specs, restricts, reducts) => - (specs, Library.merge (op =) (restricts, restr), reducts)) - |> normalize_all pp (c, args) deps'; - val deps'' = - normalize pp (restricts_of (Defs defs')) (reducts_of (Defs defs')) (c, args) deps'; - val defs'' = defs' - |> map_def c (fn (specs, restricts, reducts) => - (specs, restricts, insert (op =) (args, deps'') reducts)); - in Defs defs'' end; + val deps' = normalize_single pp (Defs defs) (c, args) deps; + val defs' = defs |> map_def c (fn (specs, restricts, reducts) => + let + val restricts' = Library.merge (op =) (restricts, restr); + val reducts' = insert (op =) (args, deps') reducts; + in (specs, restricts', reducts') end); + in Defs (normalize_all pp defs') end; end; @@ -200,11 +195,6 @@ fold (fn (args, deps) => add_deps (c, args) restricts deps) reducts; in Defs (Symtab.join join_specs (defs1, defs2)) |> Symtab.fold add_def defs2 end; -local (* FIXME *) - val merge_aux = merge - val acc = Output.time_accumulator "Defs.merge" -in fun merge pp = acc (merge_aux pp) end; - (* define *) @@ -225,14 +215,4 @@ val defs' = defs |> update_specs c spec; in Defs defs' |> (if unchecked then I else dependencies pp (c, args) restr deps) end; - -local (* FIXME *) - val define_aux = define - val acc = Output.time_accumulator "Defs.define" -in - fun define pp consts unchecked is_def module name lhs rhs = - acc (define_aux pp consts unchecked is_def module name lhs rhs) end; - - -end;