src/Pure/defs.ML
changeset 19712 3ae3cc4b1eac
parent 19707 0e7e236fab50
child 19713 69c71d40f8a8
     1.1 --- a/src/Pure/defs.ML	Wed May 24 21:58:07 2006 +0200
     1.2 +++ b/src/Pure/defs.ML	Wed May 24 21:58:09 2006 +0200
     1.3 @@ -54,9 +54,9 @@
     1.4  type spec = {is_def: bool, module: string, name: string, lhs: args, rhs: (string * args) list};
     1.5  
     1.6  type def =
     1.7 - {specs: spec Inttab.table,
     1.8 -  restricts: (args * string) list,
     1.9 -  reducts: (args * (string * args) list) list};
    1.10 + {specs: spec Inttab.table,                 (*source specifications*)
    1.11 +  restricts: (args * string) list,          (*global restrictions imposed by incomplete patterns*)
    1.12 +  reducts: (args * (string * args) list) list};  (*specifications as reduction system*)
    1.13  
    1.14  fun make_def (specs, restricts, reducts) =
    1.15    {specs = specs, restricts = restricts, reducts = reducts}: def;
    1.16 @@ -69,12 +69,12 @@
    1.17  
    1.18  datatype T = Defs of def Symtab.table;
    1.19  
    1.20 -fun lookup_list which (Defs defs) c =
    1.21 +fun lookup_list which defs c =
    1.22    (case Symtab.lookup defs c of
    1.23      SOME def => which def
    1.24    | NONE => []);
    1.25  
    1.26 -val specifications_of = lookup_list (Inttab.dest o #specs);
    1.27 +fun specifications_of (Defs defs) = lookup_list (Inttab.dest o #specs) defs;
    1.28  val restricts_of = lookup_list #restricts;
    1.29  val reducts_of = lookup_list #reducts;
    1.30  
    1.31 @@ -111,7 +111,7 @@
    1.32  
    1.33  local
    1.34  
    1.35 -fun contained U (Type (_, Ts)) = exists (fn T => T = U orelse contained U T) Ts
    1.36 +fun contained (U as TVar _) (Type (_, Ts)) = exists (fn T => T = U orelse contained U T) Ts
    1.37    | contained _ _ = false;
    1.38  
    1.39  fun wellformed pp defs (c, args) (d, Us) =
    1.40 @@ -121,7 +121,7 @@
    1.41        error (s1 ^ " dependency of constant " ^ prt (c, args) ^ " -> " ^ prt (d, Us) ^ s2);
    1.42    in
    1.43      exists (fn U => exists (contained U) args) Us orelse
    1.44 -    (c <> d andalso forall (member (op =) args) Us) orelse
    1.45 +    (c <> d andalso forall is_TVar Us) orelse
    1.46      (if c = d andalso is_some (match_args (args, Us)) then err "Circular" "" else
    1.47        (case find_first (fn (Ts, _) => not (disjoint_args (Ts, Us))) (restricts_of defs d) of
    1.48          SOME (Ts, name) =>
    1.49 @@ -147,12 +147,12 @@
    1.50      val _ = forall (wellformed pp defs const) (the_default deps deps');
    1.51    in deps' end;
    1.52  
    1.53 -fun normalize_all pp =
    1.54 +fun normalize pp =
    1.55    let
    1.56      fun norm_update (c, {reducts, ...}: def) (changed, defs) =
    1.57        let
    1.58          val reducts' = reducts |> map (fn (args, deps) =>
    1.59 -          (args, perhaps (reduction pp (Defs defs) (c, args)) deps));
    1.60 +          (args, perhaps (reduction pp defs (c, args)) deps));
    1.61        in
    1.62          if reducts = reducts' then (changed, defs)
    1.63          else (true, defs |> map_def c (fn (specs, restricts, reducts) =>
    1.64 @@ -164,25 +164,15 @@
    1.65        | (false, _) => defs);
    1.66    in norm_all end;
    1.67  
    1.68 -fun normalize_single pp defs const =
    1.69 -  let
    1.70 -    fun norm deps =
    1.71 -      (case reduction pp defs const deps of
    1.72 -        NONE => deps
    1.73 -      | SOME deps' => norm deps');
    1.74 -  in norm end;
    1.75 -
    1.76  in
    1.77  
    1.78 -fun dependencies pp (c, args) restr deps (Defs defs) =
    1.79 -  let
    1.80 -    val deps' = normalize_single pp (Defs defs) (c, args) deps;
    1.81 -    val defs' = defs |> map_def c (fn (specs, restricts, reducts) =>
    1.82 -      let
    1.83 -        val restricts' = Library.merge (op =) (restricts, restr);
    1.84 -        val reducts' = insert (op =) (args, deps') reducts;
    1.85 -      in (specs, restricts', reducts') end);
    1.86 -  in Defs (normalize_all pp defs') end;
    1.87 +fun dependencies pp (c, args) restr deps =
    1.88 +  map_def c (fn (specs, restricts, reducts) =>
    1.89 +    let
    1.90 +      val restricts' = Library.merge (op =) (restricts, restr);
    1.91 +      val reducts' = insert (op =) (args, deps) reducts;
    1.92 +    in (specs, restricts', reducts') end)
    1.93 +  #> normalize pp;
    1.94  
    1.95  end;
    1.96  
    1.97 @@ -196,7 +186,7 @@
    1.98        else dependencies pp (c, args) restr deps defs;
    1.99      fun add_def (c, {restricts, reducts, ...}: def) =
   1.100        fold (fn (args, deps) => add_deps (c, args) restricts deps) reducts;
   1.101 -  in Defs (Symtab.join join_specs (defs1, defs2)) |> Symtab.fold add_def defs2 end;
   1.102 +  in Defs (Symtab.join join_specs (defs1, defs2) |> Symtab.fold add_def defs2) end;
   1.103  
   1.104  
   1.105  (* define *)
   1.106 @@ -213,6 +203,6 @@
   1.107      val spec =
   1.108        (serial (), {is_def = is_def, module = module, name = name, lhs = args, rhs = deps});
   1.109      val defs' = defs |> update_specs c spec;
   1.110 -  in Defs defs' |> (if unchecked then I else dependencies pp (c, args) restr deps) end;
   1.111 +  in Defs (defs' |> (if unchecked then I else dependencies pp (c, args) restr deps)) end;
   1.112  
   1.113  end;