src/Pure/defs.ML
author wenzelm
Thu Oct 04 20:29:42 2007 +0200 (2007-10-04)
changeset 24850 0cfd722ab579
parent 24792 fd4655e57168
child 29606 fedb8be05f24
permissions -rw-r--r--
Name.uu, Name.aT;
     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 -> {is_def: bool, name: string,
    15     lhs: typ list, rhs: (string * typ list) list} list
    16   val all_specifications_of: T -> (string * {is_def: bool, name: string,
    17     lhs: typ list, rhs: (string * typ list) list} list) list
    18   val dest: T ->
    19    {restricts: ((string * typ list) * string) list,
    20     reducts: ((string * typ list) * (string * typ list) list) list}
    21   val empty: T
    22   val merge: Pretty.pp -> T * T -> T
    23   val define: Pretty.pp -> bool -> bool -> string ->
    24     string * typ list -> (string * typ list) list -> T -> T
    25 end
    26 
    27 structure Defs: DEFS =
    28 struct
    29 
    30 (* type arguments *)
    31 
    32 type args = typ list;
    33 
    34 fun pretty_const pp (c, args) =
    35   let
    36     val prt_args =
    37       if null args then []
    38       else [Pretty.list "(" ")" (map (Pretty.typ pp o Logic.unvarifyT) args)];
    39   in Pretty.block (Pretty.str c :: prt_args) end;
    40 
    41 fun plain_args args =
    42   forall Term.is_TVar args andalso not (has_duplicates (op =) args);
    43 
    44 fun disjoint_args (Ts, Us) =
    45   not (Type.could_unifys (Ts, Us)) orelse
    46     ((Type.raw_unifys (Ts, map (Logic.incr_tvar (maxidx_of_typs Ts + 1)) Us) Vartab.empty; false)
    47       handle Type.TUNIFY => true);
    48 
    49 fun match_args (Ts, Us) =
    50   Option.map Envir.typ_subst_TVars
    51     (SOME (Type.raw_matches (Ts, Us) Vartab.empty) handle Type.TYPE_MATCH => NONE);
    52 
    53 
    54 (* datatype defs *)
    55 
    56 type spec = {is_def: bool, name: string, lhs: args, rhs: (string * args) list};
    57 
    58 type def =
    59  {specs: spec Inttab.table,                 (*source specifications*)
    60   restricts: (args * string) list,          (*global restrictions imposed by incomplete patterns*)
    61   reducts: (args * (string * args) list) list};  (*specifications as reduction system*)
    62 
    63 fun make_def (specs, restricts, reducts) =
    64   {specs = specs, restricts = restricts, reducts = reducts}: def;
    65 
    66 fun map_def c f =
    67   Symtab.default (c, make_def (Inttab.empty, [], [])) #>
    68   Symtab.map_entry c (fn {specs, restricts, reducts}: def =>
    69     make_def (f (specs, restricts, reducts)));
    70 
    71 
    72 datatype T = Defs of def Symtab.table;
    73 
    74 fun lookup_list which defs c =
    75   (case Symtab.lookup defs c of
    76     SOME (def: def) => which def
    77   | NONE => []);
    78 
    79 fun specifications_of (Defs defs) = lookup_list (map snd o Inttab.dest o #specs) defs;
    80 fun all_specifications_of (Defs defs) =
    81   ((map o apsnd) (map snd o Inttab.dest o #specs) o Symtab.dest) defs;
    82 val restricts_of = lookup_list #restricts;
    83 val reducts_of = lookup_list #reducts;
    84 
    85 fun dest (Defs defs) =
    86   let
    87     val restricts = Symtab.fold (fn (c, {restricts, ...}) =>
    88       fold (fn (args, name) => cons ((c, args), name)) restricts) defs [];
    89     val reducts = Symtab.fold (fn (c, {reducts, ...}) =>
    90       fold (fn (args, deps) => cons ((c, args), deps)) reducts) defs [];
    91   in {restricts = restricts, reducts = reducts} end;
    92 
    93 val empty = Defs Symtab.empty;
    94 
    95 
    96 (* specifications *)
    97 
    98 fun disjoint_specs c (i, {lhs = Ts, name = a, ...}: spec) =
    99   Inttab.forall (fn (j, {lhs = Us, name = b, ...}: spec) =>
   100     i = j orelse disjoint_args (Ts, Us) orelse
   101       error ("Clash of specifications " ^ quote a ^ " and " ^ quote b ^
   102         " for constant " ^ quote c));
   103 
   104 fun join_specs c ({specs = specs1, restricts, reducts}, {specs = specs2, ...}: def) =
   105   let
   106     val specs' =
   107       Inttab.fold (fn spec2 => (disjoint_specs c spec2 specs1; Inttab.update spec2)) specs2 specs1;
   108   in make_def (specs', restricts, reducts) end;
   109 
   110 fun update_specs c spec = map_def c (fn (specs, restricts, reducts) =>
   111   (disjoint_specs c spec specs; (Inttab.update spec specs, restricts, reducts)));
   112 
   113 
   114 (* normalized dependencies: reduction with well-formedness check *)
   115 
   116 local
   117 
   118 val prt = Pretty.string_of oo pretty_const;
   119 fun err pp (c, args) (d, Us) s1 s2 =
   120   error (s1 ^ " dependency of constant " ^ prt pp (c, args) ^ " -> " ^ prt pp (d, Us) ^ s2);
   121 
   122 fun contained (U as TVar _) (Type (_, Ts)) = exists (fn T => T = U orelse contained U T) Ts
   123   | contained _ _ = false;
   124 
   125 fun acyclic pp defs (c, args) (d, Us) =
   126   c <> d orelse
   127   exists (fn U => exists (contained U) args) Us orelse
   128   is_none (match_args (args, Us)) orelse
   129   err pp (c, args) (d, Us) "Circular" "";
   130 
   131 fun wellformed pp defs (c, args) (d, Us) =
   132   forall is_TVar Us orelse
   133   (case find_first (fn (Ts, _) => not (disjoint_args (Ts, Us))) (restricts_of defs d) of
   134     SOME (Ts, name) =>
   135       err pp (c, args) (d, Us) "Malformed"
   136         ("\n(restriction " ^ prt pp (d, Ts) ^ " from " ^ quote name ^ ")")
   137   | NONE => true);
   138 
   139 fun reduction pp defs const deps =
   140   let
   141     fun reduct Us (Ts, rhs) =
   142       (case match_args (Ts, Us) of
   143         NONE => NONE
   144       | SOME subst => SOME (map (apsnd (map subst)) rhs));
   145     fun reducts (d, Us) = get_first (reduct Us) (reducts_of defs d);
   146 
   147     val reds = map (`reducts) deps;
   148     val deps' =
   149       if forall (is_none o #1) reds then NONE
   150       else SOME (fold_rev
   151         (fn (NONE, dp) => insert (op =) dp | (SOME dps, _) => fold (insert (op =)) dps) reds []);
   152     val _ = forall (acyclic pp defs const) (the_default deps deps');
   153   in deps' end;
   154 
   155 in
   156 
   157 fun normalize pp =
   158   let
   159     fun norm_update (c, {reducts, ...}: def) (changed, defs) =
   160       let
   161         val reducts' = reducts |> map (fn (args, deps) =>
   162           (args, perhaps (reduction pp defs (c, args)) deps));
   163       in
   164         if reducts = reducts' then (changed, defs)
   165         else (true, defs |> map_def c (fn (specs, restricts, reducts) =>
   166           (specs, restricts, reducts')))
   167       end;
   168     fun norm_all defs =
   169       (case Symtab.fold norm_update defs (false, defs) of
   170         (true, defs') => norm_all defs'
   171       | (false, _) => defs);
   172     fun check defs (c, {reducts, ...}: def) =
   173       reducts |> forall (fn (args, deps) => forall (wellformed pp defs (c, args)) deps);
   174   in norm_all #> (fn defs => tap (Symtab.forall (check defs)) defs) end;
   175 
   176 fun dependencies pp (c, args) restr deps =
   177   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   #> normalize pp;
   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
   197     Defs (Symtab.join join_specs (defs1, defs2)
   198       |> normalize pp |> Symtab.fold add_def defs2)
   199   end;
   200 
   201 
   202 (* define *)
   203 
   204 fun define pp unchecked is_def name (c, args) deps (Defs defs) =
   205   let
   206     val restr =
   207       if plain_args args orelse
   208         (case args of [Type (a, rec_args)] => plain_args rec_args | _ => false)
   209       then [] else [(args, name)];
   210     val spec =
   211       (serial (), {is_def = is_def, name = name, lhs = args, rhs = deps});
   212     val defs' = defs |> update_specs c spec;
   213   in Defs (defs' |> (if unchecked then I else dependencies pp (c, args) restr deps)) end;
   214 
   215 end;