separate checks for acyclic/wellformed;
authorwenzelm
Fri May 26 22:20:03 2006 +0200 (2006-05-26)
changeset 19729cb9e2f0c7658
parent 19728 6c47d9295dca
child 19730 8abecd308e60
separate checks for acyclic/wellformed;
src/Pure/defs.ML
     1.1 --- a/src/Pure/defs.ML	Fri May 26 22:20:02 2006 +0200
     1.2 +++ b/src/Pure/defs.ML	Fri May 26 22:20:03 2006 +0200
     1.3 @@ -111,24 +111,26 @@
     1.4  
     1.5  local
     1.6  
     1.7 +val prt = Pretty.string_of oo pretty_const;
     1.8 +fun err pp (c, args) (d, Us) s1 s2 =
     1.9 +  error (s1 ^ " dependency of constant " ^ prt pp (c, args) ^ " -> " ^ prt pp (d, Us) ^ s2);
    1.10 +
    1.11  fun contained (U as TVar _) (Type (_, Ts)) = exists (fn T => T = U orelse contained U T) Ts
    1.12    | contained _ _ = false;
    1.13  
    1.14 +fun acyclic pp defs (c, args) (d, Us) =
    1.15 +  c <> d orelse
    1.16 +  exists (fn U => exists (contained U) args) Us orelse
    1.17 +  is_none (match_args (args, Us)) orelse
    1.18 +  err pp (c, args) (d, Us) "Circular" "";
    1.19 +
    1.20  fun wellformed pp defs (c, args) (d, Us) =
    1.21 -  let
    1.22 -    val prt = Pretty.string_of o pretty_const pp;
    1.23 -    fun err s1 s2 =
    1.24 -      error (s1 ^ " dependency of constant " ^ prt (c, args) ^ " -> " ^ prt (d, Us) ^ s2);
    1.25 -  in
    1.26 -    exists (fn U => exists (contained U) args) Us orelse
    1.27 -    (c <> d andalso forall is_TVar Us) orelse
    1.28 -    (if c = d andalso is_some (match_args (args, Us)) then err "Circular" "" else
    1.29 -      (case find_first (fn (Ts, _) => not (disjoint_args (Ts, Us))) (restricts_of defs d) of
    1.30 -        SOME (Ts, name) =>
    1.31 -          is_some (match_args (Ts, Us)) orelse
    1.32 -          err "Malformed" ("\n(restriction " ^ prt (d, Ts) ^ " from " ^ quote name ^ ")")
    1.33 -      | NONE => true))
    1.34 -  end;
    1.35 +  forall is_TVar Us orelse
    1.36 +  (case find_first (fn (Ts, _) => not (disjoint_args (Ts, Us))) (restricts_of defs d) of
    1.37 +    SOME (Ts, name) =>
    1.38 +      err pp (c, args) (d, Us) "Malformed"
    1.39 +        ("\n(restriction " ^ prt pp (d, Ts) ^ " from " ^ quote name ^ ")")
    1.40 +  | NONE => true);
    1.41  
    1.42  fun reduction pp defs const deps =
    1.43    let
    1.44 @@ -144,7 +146,7 @@
    1.45      val deps' =
    1.46        if forall (is_none o #1) reds then NONE
    1.47        else SOME (fold_rev add reds []);
    1.48 -    val _ = forall (wellformed pp defs const) (the_default deps deps');
    1.49 +    val _ = forall (acyclic pp defs const) (the_default deps deps');
    1.50    in deps' end;
    1.51  
    1.52  fun normalize pp =
    1.53 @@ -162,7 +164,9 @@
    1.54        (case Symtab.fold norm_update defs (false, defs) of
    1.55          (true, defs') => norm_all defs'
    1.56        | (false, _) => defs);
    1.57 -  in norm_all end;
    1.58 +    fun check defs (c, {reducts, ...}: def) =
    1.59 +      reducts |> forall (fn (args, deps) => forall (wellformed pp defs (c, args)) deps);
    1.60 +  in norm_all #> (fn defs => tap (Symtab.forall (check defs)) defs) end;
    1.61  
    1.62  in
    1.63