src/Pure/defs.ML
author wenzelm
Tue May 23 13:55:01 2006 +0200 (2006-05-23)
changeset 19701 c07c31ac689b
parent 19697 423af2e013b8
child 19707 0e7e236fab50
permissions -rw-r--r--
export plain_args;
tuned wellformed, normalize;
     1 (*  Title:      Pure/defs.ML
     2     ID:         $Id$
     3     Author:     Makarius
     4 
     5 Global well-formedness checks for constant definitions.  Covers plain
     6 definitions and simple sub-structural overloading.
     7 *)
     8 
     9 signature DEFS =
    10 sig
    11   val pretty_const: Pretty.pp -> string * typ list -> Pretty.T
    12   val plain_args: typ list -> bool
    13   type T
    14   val specifications_of: T -> string -> (serial * {is_def: bool, module: string, name: string,
    15     lhs: typ list, rhs: (string * typ list) list}) list
    16   val dest: T ->
    17    {restricts: ((string * typ list) * string) list,
    18     reducts: ((string * typ list) * (string * typ list) list) list}
    19   val empty: T
    20   val merge: Pretty.pp -> T * T -> T
    21   val define: Pretty.pp -> Consts.T ->
    22     bool -> bool -> string -> string -> string * typ -> (string * typ) list -> T -> T
    23 end
    24 
    25 structure Defs: DEFS =
    26 struct
    27 
    28 (* type arguments *)
    29 
    30 type args = typ list;
    31 
    32 fun pretty_const pp (c, args) =
    33   let
    34     val prt_args =
    35       if null args then []
    36       else [Pretty.list "(" ")" (map (Pretty.typ pp o Type.freeze_type) args)];
    37   in Pretty.block (Pretty.str c :: prt_args) end;
    38 
    39 fun disjoint_args (Ts, Us) =
    40   not (Type.could_unifys (Ts, Us)) orelse
    41     ((Type.raw_unifys (Ts, map (Logic.incr_tvar (maxidx_of_typs Ts + 1)) Us) Vartab.empty; false)
    42       handle Type.TUNIFY => true);
    43 
    44 fun match_args (Ts, Us) =
    45   Option.map Envir.typ_subst_TVars
    46     (SOME (Type.raw_matches (Ts, Us) Vartab.empty) handle Type.TYPE_MATCH => NONE);
    47 
    48 
    49 (* datatype defs *)
    50 
    51 type spec = {is_def: bool, module: string, name: string, lhs: args, rhs: (string * args) list};
    52 
    53 type def =
    54  {specs: spec Inttab.table,
    55   restricts: (args * string) list,
    56   reducts: (args * (string * args) list) list};
    57 
    58 fun make_def (specs, restricts, reducts) =
    59   {specs = specs, restricts = restricts, reducts = reducts}: def;
    60 
    61 fun map_def c f =
    62   Symtab.default (c, make_def (Inttab.empty, [], [])) #>
    63   Symtab.map_entry c (fn {specs, restricts, reducts}: def =>
    64     make_def (f (specs, restricts, reducts)));
    65 
    66 
    67 datatype T = Defs of def Symtab.table;
    68 
    69 fun lookup_list which (Defs defs) c =
    70   (case Symtab.lookup defs c of
    71     SOME def => which def
    72   | NONE => []);
    73 
    74 val specifications_of = lookup_list (Inttab.dest o #specs);
    75 val restricts_of = lookup_list #restricts;
    76 val reducts_of = lookup_list #reducts;
    77 
    78 fun dest (Defs defs) =
    79   let
    80     val restricts = Symtab.fold (fn (c, {restricts, ...}) =>
    81       fold (fn (args, name) => cons ((c, args), name)) restricts) defs [];
    82     val reducts = Symtab.fold (fn (c, {reducts, ...}) =>
    83       fold (fn (args, deps) => cons ((c, args), deps)) reducts) defs [];
    84   in {restricts = restricts, reducts = reducts} end;
    85 
    86 val empty = Defs Symtab.empty;
    87 
    88 
    89 (* specifications *)
    90 
    91 fun disjoint_specs c (i, {lhs = Ts, name = a, ...}: spec) =
    92   Inttab.forall (fn (j, {lhs = Us, name = b, ...}: spec) =>
    93     i = j orelse disjoint_args (Ts, Us) orelse
    94       error ("Type clash in specifications " ^ quote a ^ " and " ^ quote b ^
    95         " for constant " ^ quote c));
    96 
    97 fun join_specs c ({specs = specs1, restricts, reducts}, {specs = specs2, ...}: def) =
    98   let
    99     val specs' =
   100       Inttab.fold (fn spec2 => (disjoint_specs c spec2 specs1; Inttab.update spec2)) specs2 specs1;
   101   in make_def (specs', restricts, reducts) end;
   102 
   103 fun update_specs c spec = map_def c (fn (specs, restricts, reducts) =>
   104   (disjoint_specs c spec specs; (Inttab.update spec specs, restricts, reducts)));
   105 
   106 
   107 (* normalized dependencies: reduction with well-formedness check *)
   108 
   109 local
   110 
   111 fun contained U (Type (_, Ts)) = exists (fn T => T = U orelse contained U T) Ts
   112   | contained _ _ = false;
   113 
   114 fun wellformed pp defs (c, args) (d, Us) =
   115   let
   116     val prt = Pretty.string_of o pretty_const pp;
   117     fun err s1 s2 =
   118       error (s1 ^ " dependency of constant " ^ prt (c, args) ^ " -> " ^ prt (d, Us) ^ s2);
   119   in
   120     exists (fn U => exists (contained U) args) Us orelse
   121     (c <> d andalso forall (member (op =) args) Us) orelse
   122     (if c = d andalso is_some (match_args (args, Us)) then err "Circular" "" else
   123       (case find_first (fn (Ts, _) => not (disjoint_args (Ts, Us))) (restricts_of defs d) of
   124         SOME (Ts, name) =>
   125           is_some (match_args (Ts, Us)) orelse
   126           err "Malformed" ("\n(restriction " ^ prt (d, Ts) ^ " from " ^ quote name ^ ")")
   127       | NONE => true))
   128   end;
   129 
   130 fun reduction pp defs const deps =
   131   let
   132     fun reduct Us (Ts, rhs) =
   133       (case match_args (Ts, Us) of
   134         NONE => NONE
   135       | SOME subst => SOME (map (apsnd (map subst)) rhs));
   136     fun reducts (d, Us) = get_first (reduct Us) (reducts_of defs d);
   137 
   138     fun add (NONE, dp) = insert (op =) dp
   139       | add (SOME dps, _) = fold (insert (op =)) dps;
   140     val reds = map (`reducts) deps;
   141     val deps' =
   142       if forall (is_none o #1) reds then NONE
   143       else SOME (fold_rev add reds []);
   144     val _ = forall (wellformed pp defs const) (the_default deps deps');
   145   in deps' end;
   146 
   147 fun normalize_all pp =
   148   let
   149     fun norm_update (c, {reducts, ...}: def) (changed, defs) =
   150       let
   151         val reducts' = reducts |> map (fn (args, deps) =>
   152           (args, perhaps (reduction pp (Defs defs) (c, args)) deps));
   153       in
   154         if reducts = reducts' then (changed, defs)
   155         else (true, defs |> map_def c (fn (specs, restricts, reducts) =>
   156           (specs, restricts, reducts')))
   157       end;
   158     fun norm_all defs =
   159       (case Symtab.fold norm_update defs (false, defs) of
   160         (true, defs') => norm_all defs'
   161       | (false, _) => defs);
   162   in norm_all end;
   163 
   164 fun normalize_single pp defs const =
   165   let
   166     fun norm deps =
   167       (case reduction pp defs const deps of
   168         NONE => deps
   169       | SOME deps' => norm deps');
   170   in norm end;
   171 
   172 in
   173 
   174 fun dependencies pp (c, args) restr deps (Defs defs) =
   175   let
   176     val deps' = normalize_single pp (Defs defs) (c, args) deps;
   177     val defs' = defs |> map_def c (fn (specs, restricts, reducts) =>
   178       let
   179         val restricts' = Library.merge (op =) (restricts, restr);
   180         val reducts' = insert (op =) (args, deps') reducts;
   181       in (specs, restricts', reducts') end);
   182   in Defs (normalize_all pp defs') end;
   183 
   184 end;
   185 
   186 
   187 (* merge *)
   188 
   189 fun merge pp (Defs defs1, Defs defs2) =
   190   let
   191     fun add_deps (c, args) restr deps defs =
   192       if AList.defined (op =) (reducts_of defs c) args then defs
   193       else dependencies pp (c, args) restr deps defs;
   194     fun add_def (c, {restricts, reducts, ...}: def) =
   195       fold (fn (args, deps) => add_deps (c, args) restricts deps) reducts;
   196   in Defs (Symtab.join join_specs (defs1, defs2)) |> Symtab.fold add_def defs2 end;
   197 
   198 
   199 (* define *)
   200 
   201 fun plain_args args =
   202   forall Term.is_TVar args andalso not (has_duplicates (op =) args);
   203 
   204 fun define pp consts unchecked is_def module name lhs rhs (Defs defs) =
   205   let
   206     fun typargs const = (#1 const, Consts.typargs consts const);
   207     val (c, args) = typargs lhs;
   208     val deps = map typargs rhs;
   209     val restr =
   210       if plain_args args orelse
   211         (case args of [Type (a, rec_args)] => plain_args rec_args | _ => false)
   212       then [] else [(args, name)];
   213     val spec =
   214       (serial (), {is_def = is_def, module = module, name = name, lhs = args, rhs = deps});
   215     val defs' = defs |> update_specs c spec;
   216   in Defs defs' |> (if unchecked then I else dependencies pp (c, args) restr deps) end;
   217 
   218 end;