src/Pure/defs.ML
author wenzelm
Sat May 20 23:37:02 2006 +0200 (2006-05-20)
changeset 19692 bad13b32c0f3
parent 19628 de019ddcd89e
child 19695 7706aeac6cf1
permissions -rw-r--r--
yet another re-implementation:
. maintain explicit mapping from unspecified to specified consts (no
dependency graph, no termination check, but direct reduction of
specifications);
. more precise checking of LHS patterns -- specialized patterns
(e.g. 'a => 'a instead of general 'a => 'b) impose global
restrictions;
     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 (depending on a
     7 single type argument).
     8 *)
     9 
    10 signature DEFS =
    11 sig
    12   type T
    13   val specifications_of: T -> string ->
    14    (serial * {is_def: bool, module: string, name: string, lhs: typ, rhs: (string * typ) list}) list
    15   val empty: T
    16   val merge: Pretty.pp -> T * T -> T
    17   val define: Pretty.pp -> Consts.T ->
    18     bool -> bool -> string -> string -> string * typ -> (string * typ) list -> T -> T
    19 end
    20 
    21 structure Defs: DEFS =
    22 struct
    23 
    24 (* consts with type arguments *)
    25 
    26 fun print_const pp (c, args) =
    27   let
    28     val prt_args =
    29       if null args then []
    30       else [Pretty.brk 1, Pretty.list "(" ")" (map (Pretty.typ pp o Type.freeze_type) args)];
    31   in Pretty.string_of (Pretty.block (Pretty.str c :: prt_args)) end;
    32 
    33 
    34 (* source specs *)
    35 
    36 type spec = {is_def: bool, module: string, name: string, lhs: typ, rhs: (string * typ) list};
    37 
    38 fun disjoint_types T U =
    39   (Type.raw_unify (T, Logic.incr_tvar (maxidx_of_typ T + 1) U) Vartab.empty; false)
    40     handle Type.TUNIFY => true;
    41 
    42 fun disjoint_specs c (i, {lhs = T, name = a, ...}: spec) =
    43   Inttab.forall (fn (j, {lhs = U, name = b, ...}: spec) =>
    44     i = j orelse not (Type.could_unify (T, U)) orelse disjoint_types T U orelse
    45       error ("Type clash in specifications " ^ quote a ^ " and " ^ quote b ^
    46         " for constant " ^ quote c));
    47 
    48 
    49 (* patterns *)
    50 
    51 datatype pattern = Unknown | Plain | Overloaded;
    52 
    53 fun str_of_pattern Overloaded = "overloading"
    54   | str_of_pattern _ = "no overloading";
    55 
    56 fun merge_pattern c (p1, p2) =
    57   if p1 = p2 orelse p2 = Unknown then p1
    58   else if p1 = Unknown then p2
    59   else error ("Inconsistent type patterns for constant " ^ quote c ^ ":\n" ^
    60     str_of_pattern p1 ^ " versus " ^ str_of_pattern p2);
    61 
    62 fun plain_args args =
    63   forall Term.is_TVar args andalso not (has_duplicates (op =) args);
    64 
    65 fun the_pattern _ name (c, [Type (a, args)]) =
    66       (Overloaded, if plain_args args then [] else [(a, (args, name))])
    67   | the_pattern prt _ (c, args) =
    68       if plain_args args then (Plain, [])
    69       else error ("Illegal type pattern for constant " ^ prt (c, args));
    70 
    71 
    72 (* datatype defs *)
    73 
    74 type def =
    75  {specs: spec Inttab.table,
    76   pattern: pattern,
    77   restricts: (string * (typ list * string)) list,
    78   reducts: (typ list * (string * typ list) list) list};
    79 
    80 fun make_def (specs, pattern, restricts, reducts) =
    81   {specs = specs, pattern = pattern, restricts = restricts, reducts = reducts}: def;
    82 
    83 fun map_def f ({specs, pattern, restricts, reducts}: def) =
    84   make_def (f (specs, pattern, restricts, reducts));
    85 
    86 fun default_def (pattern, restricts) = make_def (Inttab.empty, pattern, restricts, []);
    87 
    88 datatype T = Defs of def Symtab.table;
    89 val empty = Defs Symtab.empty;
    90 
    91 fun lookup_list which (Defs defs) c =
    92   (case Symtab.lookup defs c of
    93     SOME def => which def
    94   | NONE => []);
    95 
    96 val specifications_of = lookup_list (Inttab.dest o #specs);
    97 val restricts_of = lookup_list #restricts;
    98 val reducts_of = lookup_list #reducts;
    99 
   100 
   101 (* normalize defs *)
   102 
   103 fun matcher arg =
   104   Option.map Envir.typ_subst_TVars
   105     (SOME (Type.raw_matches arg Vartab.empty) handle Type.TYPE_MATCH => NONE);
   106 
   107 fun restriction prt defs (c, args) =
   108   (case args of
   109     [Type (a, Us)] =>
   110       (case AList.lookup (op =) (restricts_of defs c) a of
   111         SOME (Ts, name) =>
   112           if is_some (matcher (Ts, Us)) then ()
   113           else error ("Occurrence of overloaded constant " ^ prt (c, args) ^
   114             "\nviolates restriction " ^ prt (c, Ts) ^ "\nimposed by " ^ quote name)
   115       | NONE => ())
   116   | _ => ());
   117 
   118 fun reduction defs deps =
   119   let
   120     fun reduct Us (Ts, rhs) =
   121       (case matcher (Ts, Us) of
   122         NONE => NONE
   123       | SOME subst => SOME (map (apsnd (map subst)) rhs));
   124     fun reducts (d, Us) = get_first (reduct Us) (reducts_of defs d);
   125 
   126     fun add (NONE, dp) = insert (op =) dp
   127       | add (SOME dps, _) = fold (insert (op =)) dps;
   128     val deps' = map (`reducts) deps;
   129   in
   130     if forall (is_none o #1) deps' then NONE
   131     else SOME (fold_rev add deps' [])
   132   end;
   133 
   134 fun normalize prt defs (c, args) deps =
   135   let
   136     val reds = reduction defs deps;
   137     val deps' = the_default deps reds;
   138     val _ = List.app (restriction prt defs) ((c, args) :: deps');
   139     val _ = deps' |> List.app (fn (c', args') =>
   140       if c' = c andalso is_some (matcher (args, args')) then
   141         error ("Circular dependency of constant " ^ prt (c, args) ^ " -> " ^ prt (c, args'))
   142       else ());
   143   in reds end;
   144 
   145 
   146 (* dependencies *)
   147 
   148 fun normalize_deps prt defs0 (Defs defs) =
   149   let
   150     fun norm const deps = perhaps (normalize prt defs0 const) deps;
   151     fun norm_update (c, {reducts, ...}) =
   152       let val reducts' = reducts |> map (fn (args, deps) => (args, norm (c, args) deps)) in
   153         if reducts = reducts' then I
   154         else Symtab.map_entry c (map_def (fn (specs, pattern, restricts, reducts) =>
   155           (specs, pattern, restricts, reducts')))
   156       end;
   157   in Defs (Symtab.fold norm_update defs defs) end;
   158 
   159 fun dependencies prt (c, args) pat deps (Defs defs) =
   160   let
   161     val deps' = perhaps (normalize prt (Defs defs) (c, args)) deps;
   162     val defs' = defs
   163       |> Symtab.default (c, default_def pat)
   164       |> Symtab.map_entry c (map_def (fn (specs, pattern, restricts, reducts) =>
   165         let
   166           val pattern' = merge_pattern c (pattern, #1 pat);
   167           val restricts' = Library.merge (op =) (restricts, #2 pat);
   168           val reducts' = insert (op =) (args, deps') reducts;
   169         in (specs, pattern', restricts', reducts') end));
   170   in normalize_deps prt (Defs defs') (Defs defs') end;
   171 
   172 
   173 (* merge *)
   174 
   175 fun join_specs c ({specs = specs1, pattern, restricts, reducts}, {specs = specs2, ...}: def) =
   176   let
   177     val specs' =
   178       Inttab.fold (fn spec2 => (disjoint_specs c spec2 specs1; Inttab.update spec2)) specs2 specs1;
   179   in make_def (specs', pattern, restricts, reducts) end;
   180 
   181 fun merge pp (Defs defs1, Defs defs2) =
   182   let
   183     fun add_deps (c, args) pat deps defs =
   184       if AList.defined (op =) (reducts_of defs c) args then defs
   185       else dependencies (print_const pp) (c, args) pat deps defs;
   186     fun add_def (c, {pattern, restricts, reducts, ...}) =
   187       fold (fn (args, deps) => add_deps (c, args) (pattern, restricts) deps) reducts;
   188   in Defs (Symtab.join join_specs (defs1, defs2)) |> Symtab.fold add_def defs2 end;
   189 
   190 
   191 (* define *)
   192 
   193 fun define pp consts unchecked is_def module name lhs rhs (Defs defs) =
   194   let
   195     val prt = print_const pp;
   196     fun typargs const = (#1 const, Consts.typargs consts const);
   197 
   198     val (c, args) = typargs lhs;
   199     val pat =
   200       if unchecked then (Unknown, [])
   201       else the_pattern prt name (c, args);
   202     val spec =
   203       (serial (), {is_def = is_def, module = module, name = name, lhs = #2 lhs, rhs = rhs});
   204 
   205     val defs' = defs
   206       |> Symtab.default (c, default_def pat)
   207       |> Symtab.map_entry c (map_def (fn (specs, pattern, restricts, reducts) =>
   208         let
   209           val _ = disjoint_specs c spec specs;
   210           val specs' = Inttab.update spec specs;
   211         in (specs', pattern, restricts, reducts) end));
   212   in Defs defs' |> (if unchecked then I else dependencies prt (c, args) pat (map typargs rhs)) end;
   213 
   214 end;