export plain_args;
authorwenzelm
Tue May 23 13:55:01 2006 +0200 (2006-05-23)
changeset 19701c07c31ac689b
parent 19700 e02af528ceef
child 19702 2ab12e94156f
export plain_args;
tuned wellformed, normalize;
src/Pure/defs.ML
     1.1 --- a/src/Pure/defs.ML	Mon May 22 22:29:19 2006 +0200
     1.2 +++ b/src/Pure/defs.ML	Tue May 23 13:55:01 2006 +0200
     1.3 @@ -3,13 +3,13 @@
     1.4      Author:     Makarius
     1.5  
     1.6  Global well-formedness checks for constant definitions.  Covers plain
     1.7 -definitions and simple sub-structural overloading (depending on a
     1.8 -single type argument).
     1.9 +definitions and simple sub-structural overloading.
    1.10  *)
    1.11  
    1.12  signature DEFS =
    1.13  sig
    1.14    val pretty_const: Pretty.pp -> string * typ list -> Pretty.T
    1.15 +  val plain_args: typ list -> bool
    1.16    type T
    1.17    val specifications_of: T -> string -> (serial * {is_def: bool, module: string, name: string,
    1.18      lhs: typ list, rhs: (string * typ list) list}) list
    1.19 @@ -25,7 +25,6 @@
    1.20  structure Defs: DEFS =
    1.21  struct
    1.22  
    1.23 -
    1.24  (* type arguments *)
    1.25  
    1.26  type args = typ list;
    1.27 @@ -105,86 +104,82 @@
    1.28    (disjoint_specs c spec specs; (Inttab.update spec specs, restricts, reducts)));
    1.29  
    1.30  
    1.31 -(* normalization: reduction and well-formedness check *)
    1.32 +(* normalized dependencies: reduction with well-formedness check *)
    1.33  
    1.34  local
    1.35  
    1.36 -fun reduction reds_of deps =
    1.37 -  let
    1.38 -    fun reduct Us (Ts, rhs) =
    1.39 -      (case match_args (Ts, Us) of
    1.40 -        NONE => NONE
    1.41 -      | SOME subst => SOME (map (apsnd (map subst)) rhs));
    1.42 -    fun reducts (d: string, Us) = get_first (reduct Us) (reds_of d);
    1.43 -
    1.44 -    fun add (NONE, dp) = insert (op =) dp
    1.45 -      | add (SOME dps, _) = fold (insert (op =)) dps;
    1.46 -    val deps' = map (`reducts) deps;
    1.47 -  in
    1.48 -    if forall (is_none o #1) deps' then NONE
    1.49 -    else SOME (fold_rev add deps' [])
    1.50 -  end;
    1.51 -
    1.52 -fun reductions reds_of deps =
    1.53 -  (case reduction reds_of deps of
    1.54 -    SOME deps' => reductions reds_of deps'
    1.55 -  | NONE => deps);
    1.56 -
    1.57  fun contained U (Type (_, Ts)) = exists (fn T => T = U orelse contained U T) Ts
    1.58    | contained _ _ = false;
    1.59  
    1.60 -fun wellformed pp rests_of (c, args) (d, Us) =
    1.61 +fun wellformed pp defs (c, args) (d, Us) =
    1.62    let
    1.63      val prt = Pretty.string_of o pretty_const pp;
    1.64      fun err s1 s2 =
    1.65        error (s1 ^ " dependency of constant " ^ prt (c, args) ^ " -> " ^ prt (d, Us) ^ s2);
    1.66    in
    1.67      exists (fn U => exists (contained U) args) Us orelse
    1.68 -    (c <> d andalso exists (member (op =) args) Us) orelse
    1.69 -      (case find_first (fn (Ts, _) => not (disjoint_args (Ts, Us))) (rests_of d) of
    1.70 -        NONE =>
    1.71 -          c <> d orelse is_none (match_args (args, Us)) orelse err "Circular" ""
    1.72 -      | SOME (Ts, name) =>
    1.73 -          if c = d then err "Circular" ("\n(via " ^ quote name ^ ")")
    1.74 -          else
    1.75 -            err "Malformed" ("\n(restriction " ^ prt (d, Ts) ^ " from " ^ quote name ^ ")"))
    1.76 +    (c <> d andalso forall (member (op =) args) Us) orelse
    1.77 +    (if c = d andalso is_some (match_args (args, Us)) then err "Circular" "" else
    1.78 +      (case find_first (fn (Ts, _) => not (disjoint_args (Ts, Us))) (restricts_of defs d) of
    1.79 +        SOME (Ts, name) =>
    1.80 +          is_some (match_args (Ts, Us)) orelse
    1.81 +          err "Malformed" ("\n(restriction " ^ prt (d, Ts) ^ " from " ^ quote name ^ ")")
    1.82 +      | NONE => true))
    1.83    end;
    1.84  
    1.85 -fun normalize pp rests_of reds_of (c, args) deps =
    1.86 +fun reduction pp defs const deps =
    1.87    let
    1.88 -    val deps' = reductions reds_of deps;
    1.89 -    val _ = forall (wellformed pp rests_of (c, args)) deps';
    1.90 +    fun reduct Us (Ts, rhs) =
    1.91 +      (case match_args (Ts, Us) of
    1.92 +        NONE => NONE
    1.93 +      | SOME subst => SOME (map (apsnd (map subst)) rhs));
    1.94 +    fun reducts (d, Us) = get_first (reduct Us) (reducts_of defs d);
    1.95 +
    1.96 +    fun add (NONE, dp) = insert (op =) dp
    1.97 +      | add (SOME dps, _) = fold (insert (op =)) dps;
    1.98 +    val reds = map (`reducts) deps;
    1.99 +    val deps' =
   1.100 +      if forall (is_none o #1) reds then NONE
   1.101 +      else SOME (fold_rev add reds []);
   1.102 +    val _ = forall (wellformed pp defs const) (the_default deps deps');
   1.103    in deps' end;
   1.104  
   1.105 -fun normalize_all pp (c, args) deps defs =
   1.106 +fun normalize_all pp =
   1.107    let
   1.108 -    val norm = normalize pp (restricts_of (Defs defs));
   1.109 -    val norm_rule = norm (fn c' => if c' = c then [(args, deps)] else []);
   1.110 -    val norm_defs = norm (reducts_of (Defs defs));
   1.111 -    fun norm_update (c', {reducts, ...}: def) =
   1.112 -      let val reducts' = reducts
   1.113 -        |> map (fn (args', deps') => (args', norm_defs (c', args') (norm_rule (c', args') deps')))
   1.114 +    fun norm_update (c, {reducts, ...}: def) (changed, defs) =
   1.115 +      let
   1.116 +        val reducts' = reducts |> map (fn (args, deps) =>
   1.117 +          (args, perhaps (reduction pp (Defs defs) (c, args)) deps));
   1.118        in
   1.119 -        K (reducts <> reducts') ?
   1.120 -          map_def c' (fn (specs, restricts, reducts) => (specs, restricts, reducts'))
   1.121 +        if reducts = reducts' then (changed, defs)
   1.122 +        else (true, defs |> map_def c (fn (specs, restricts, reducts) =>
   1.123 +          (specs, restricts, reducts')))
   1.124        end;
   1.125 -  in Symtab.fold norm_update defs defs end;
   1.126 +    fun norm_all defs =
   1.127 +      (case Symtab.fold norm_update defs (false, defs) of
   1.128 +        (true, defs') => norm_all defs'
   1.129 +      | (false, _) => defs);
   1.130 +  in norm_all end;
   1.131 +
   1.132 +fun normalize_single pp defs const =
   1.133 +  let
   1.134 +    fun norm deps =
   1.135 +      (case reduction pp defs const deps of
   1.136 +        NONE => deps
   1.137 +      | SOME deps' => norm deps');
   1.138 +  in norm end;
   1.139  
   1.140  in
   1.141  
   1.142  fun dependencies pp (c, args) restr deps (Defs defs) =
   1.143    let
   1.144 -    val deps' = normalize pp (restricts_of (Defs defs)) (reducts_of (Defs defs)) (c, args) deps;
   1.145 -    val defs' = defs
   1.146 -      |> map_def c (fn (specs, restricts, reducts) =>
   1.147 -        (specs, Library.merge (op =) (restricts, restr), reducts))
   1.148 -      |> normalize_all pp (c, args) deps';
   1.149 -    val deps'' =
   1.150 -      normalize pp (restricts_of (Defs defs')) (reducts_of (Defs defs')) (c, args) deps';
   1.151 -    val defs'' = defs'
   1.152 -      |> map_def c (fn (specs, restricts, reducts) =>
   1.153 -        (specs, restricts, insert (op =) (args, deps'') reducts));
   1.154 -  in Defs defs'' end;
   1.155 +    val deps' = normalize_single pp (Defs defs) (c, args) deps;
   1.156 +    val defs' = defs |> map_def c (fn (specs, restricts, reducts) =>
   1.157 +      let
   1.158 +        val restricts' = Library.merge (op =) (restricts, restr);
   1.159 +        val reducts' = insert (op =) (args, deps') reducts;
   1.160 +      in (specs, restricts', reducts') end);
   1.161 +  in Defs (normalize_all pp defs') end;
   1.162  
   1.163  end;
   1.164  
   1.165 @@ -200,11 +195,6 @@
   1.166        fold (fn (args, deps) => add_deps (c, args) restricts deps) reducts;
   1.167    in Defs (Symtab.join join_specs (defs1, defs2)) |> Symtab.fold add_def defs2 end;
   1.168  
   1.169 -local  (* FIXME *)
   1.170 -  val merge_aux = merge
   1.171 -  val acc = Output.time_accumulator "Defs.merge"
   1.172 -in fun merge pp = acc (merge_aux pp) end;
   1.173 -
   1.174  
   1.175  (* define *)
   1.176  
   1.177 @@ -225,14 +215,4 @@
   1.178      val defs' = defs |> update_specs c spec;
   1.179    in Defs defs' |> (if unchecked then I else dependencies pp (c, args) restr deps) end;
   1.180  
   1.181 -
   1.182 -local  (* FIXME *)
   1.183 -  val define_aux = define
   1.184 -  val acc = Output.time_accumulator "Defs.define"
   1.185 -in
   1.186 -  fun define pp consts unchecked is_def module name lhs rhs =
   1.187 -    acc (define_aux pp consts unchecked is_def module name lhs rhs)
   1.188  end;
   1.189 -
   1.190 -
   1.191 -end;