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