src/Pure/defs.ML
author wenzelm
Mon May 22 22:29:15 2006 +0200 (2006-05-22)
changeset 19697 423af2e013b8
parent 19695 7706aeac6cf1
child 19701 c07c31ac689b
permissions -rw-r--r--
specifications_of: lhs/rhs represented as typargs;
export pretty_const;
export dest;
more precise checking of lhs patterns;
more precise normalization;
misc cleanup;
     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   val pretty_const: Pretty.pp -> string * typ list -> Pretty.T
    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 
    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 Type.freeze_type) args)];
    38   in Pretty.block (Pretty.str c :: prt_args) end;
    39 
    40 fun disjoint_args (Ts, Us) =
    41   not (Type.could_unifys (Ts, Us)) orelse
    42     ((Type.raw_unifys (Ts, map (Logic.incr_tvar (maxidx_of_typs Ts + 1)) Us) Vartab.empty; false)
    43       handle Type.TUNIFY => true);
    44 
    45 fun match_args (Ts, Us) =
    46   Option.map Envir.typ_subst_TVars
    47     (SOME (Type.raw_matches (Ts, Us) Vartab.empty) handle Type.TYPE_MATCH => NONE);
    48 
    49 
    50 (* datatype defs *)
    51 
    52 type spec = {is_def: bool, module: string, name: string, lhs: args, rhs: (string * args) list};
    53 
    54 type def =
    55  {specs: spec Inttab.table,
    56   restricts: (args * string) list,
    57   reducts: (args * (string * args) list) list};
    58 
    59 fun make_def (specs, restricts, reducts) =
    60   {specs = specs, restricts = restricts, reducts = reducts}: def;
    61 
    62 fun map_def c f =
    63   Symtab.default (c, make_def (Inttab.empty, [], [])) #>
    64   Symtab.map_entry c (fn {specs, restricts, reducts}: def =>
    65     make_def (f (specs, restricts, reducts)));
    66 
    67 
    68 datatype T = Defs of def Symtab.table;
    69 
    70 fun lookup_list which (Defs defs) c =
    71   (case Symtab.lookup defs c of
    72     SOME def => which def
    73   | NONE => []);
    74 
    75 val specifications_of = lookup_list (Inttab.dest o #specs);
    76 val restricts_of = lookup_list #restricts;
    77 val reducts_of = lookup_list #reducts;
    78 
    79 fun dest (Defs defs) =
    80   let
    81     val restricts = Symtab.fold (fn (c, {restricts, ...}) =>
    82       fold (fn (args, name) => cons ((c, args), name)) restricts) defs [];
    83     val reducts = Symtab.fold (fn (c, {reducts, ...}) =>
    84       fold (fn (args, deps) => cons ((c, args), deps)) reducts) defs [];
    85   in {restricts = restricts, reducts = reducts} end;
    86 
    87 val empty = Defs Symtab.empty;
    88 
    89 
    90 (* specifications *)
    91 
    92 fun disjoint_specs c (i, {lhs = Ts, name = a, ...}: spec) =
    93   Inttab.forall (fn (j, {lhs = Us, name = b, ...}: spec) =>
    94     i = j orelse disjoint_args (Ts, Us) orelse
    95       error ("Type clash in specifications " ^ quote a ^ " and " ^ quote b ^
    96         " for constant " ^ quote c));
    97 
    98 fun join_specs c ({specs = specs1, restricts, reducts}, {specs = specs2, ...}: def) =
    99   let
   100     val specs' =
   101       Inttab.fold (fn spec2 => (disjoint_specs c spec2 specs1; Inttab.update spec2)) specs2 specs1;
   102   in make_def (specs', restricts, reducts) end;
   103 
   104 fun update_specs c spec = map_def c (fn (specs, restricts, reducts) =>
   105   (disjoint_specs c spec specs; (Inttab.update spec specs, restricts, reducts)));
   106 
   107 
   108 (* normalization: reduction and well-formedness check *)
   109 
   110 local
   111 
   112 fun reduction reds_of deps =
   113   let
   114     fun reduct Us (Ts, rhs) =
   115       (case match_args (Ts, Us) of
   116         NONE => NONE
   117       | SOME subst => SOME (map (apsnd (map subst)) rhs));
   118     fun reducts (d: string, Us) = get_first (reduct Us) (reds_of d);
   119 
   120     fun add (NONE, dp) = insert (op =) dp
   121       | add (SOME dps, _) = fold (insert (op =)) dps;
   122     val deps' = map (`reducts) deps;
   123   in
   124     if forall (is_none o #1) deps' then NONE
   125     else SOME (fold_rev add deps' [])
   126   end;
   127 
   128 fun reductions reds_of deps =
   129   (case reduction reds_of deps of
   130     SOME deps' => reductions reds_of deps'
   131   | NONE => deps);
   132 
   133 fun contained U (Type (_, Ts)) = exists (fn T => T = U orelse contained U T) Ts
   134   | contained _ _ = false;
   135 
   136 fun wellformed pp rests_of (c, args) (d, Us) =
   137   let
   138     val prt = Pretty.string_of o pretty_const pp;
   139     fun err s1 s2 =
   140       error (s1 ^ " dependency of constant " ^ prt (c, args) ^ " -> " ^ prt (d, Us) ^ s2);
   141   in
   142     exists (fn U => exists (contained U) args) Us orelse
   143     (c <> d andalso exists (member (op =) args) Us) orelse
   144       (case find_first (fn (Ts, _) => not (disjoint_args (Ts, Us))) (rests_of d) of
   145         NONE =>
   146           c <> d orelse is_none (match_args (args, Us)) orelse err "Circular" ""
   147       | SOME (Ts, name) =>
   148           if c = d then err "Circular" ("\n(via " ^ quote name ^ ")")
   149           else
   150             err "Malformed" ("\n(restriction " ^ prt (d, Ts) ^ " from " ^ quote name ^ ")"))
   151   end;
   152 
   153 fun normalize pp rests_of reds_of (c, args) deps =
   154   let
   155     val deps' = reductions reds_of deps;
   156     val _ = forall (wellformed pp rests_of (c, args)) deps';
   157   in deps' end;
   158 
   159 fun normalize_all pp (c, args) deps defs =
   160   let
   161     val norm = normalize pp (restricts_of (Defs defs));
   162     val norm_rule = norm (fn c' => if c' = c then [(args, deps)] else []);
   163     val norm_defs = norm (reducts_of (Defs defs));
   164     fun norm_update (c', {reducts, ...}: def) =
   165       let val reducts' = reducts
   166         |> map (fn (args', deps') => (args', norm_defs (c', args') (norm_rule (c', args') deps')))
   167       in
   168         K (reducts <> reducts') ?
   169           map_def c' (fn (specs, restricts, reducts) => (specs, restricts, reducts'))
   170       end;
   171   in Symtab.fold norm_update defs defs end;
   172 
   173 in
   174 
   175 fun dependencies pp (c, args) restr deps (Defs defs) =
   176   let
   177     val deps' = normalize pp (restricts_of (Defs defs)) (reducts_of (Defs defs)) (c, args) deps;
   178     val defs' = defs
   179       |> map_def c (fn (specs, restricts, reducts) =>
   180         (specs, Library.merge (op =) (restricts, restr), reducts))
   181       |> normalize_all pp (c, args) deps';
   182     val deps'' =
   183       normalize pp (restricts_of (Defs defs')) (reducts_of (Defs defs')) (c, args) deps';
   184     val defs'' = defs'
   185       |> map_def c (fn (specs, restricts, reducts) =>
   186         (specs, restricts, insert (op =) (args, deps'') reducts));
   187   in Defs defs'' end;
   188 
   189 end;
   190 
   191 
   192 (* merge *)
   193 
   194 fun merge pp (Defs defs1, Defs defs2) =
   195   let
   196     fun add_deps (c, args) restr deps defs =
   197       if AList.defined (op =) (reducts_of defs c) args then defs
   198       else dependencies pp (c, args) restr deps defs;
   199     fun add_def (c, {restricts, reducts, ...}: def) =
   200       fold (fn (args, deps) => add_deps (c, args) restricts deps) reducts;
   201   in Defs (Symtab.join join_specs (defs1, defs2)) |> Symtab.fold add_def defs2 end;
   202 
   203 local  (* FIXME *)
   204   val merge_aux = merge
   205   val acc = Output.time_accumulator "Defs.merge"
   206 in fun merge pp = acc (merge_aux pp) end;
   207 
   208 
   209 (* define *)
   210 
   211 fun plain_args args =
   212   forall Term.is_TVar args andalso not (has_duplicates (op =) args);
   213 
   214 fun define pp consts unchecked is_def module name lhs rhs (Defs defs) =
   215   let
   216     fun typargs const = (#1 const, Consts.typargs consts const);
   217     val (c, args) = typargs lhs;
   218     val deps = map typargs rhs;
   219     val restr =
   220       if plain_args args orelse
   221         (case args of [Type (a, rec_args)] => plain_args rec_args | _ => false)
   222       then [] else [(args, name)];
   223     val spec =
   224       (serial (), {is_def = is_def, module = module, name = name, lhs = args, rhs = deps});
   225     val defs' = defs |> update_specs c spec;
   226   in Defs defs' |> (if unchecked then I else dependencies pp (c, args) restr deps) end;
   227 
   228 
   229 local  (* FIXME *)
   230   val define_aux = define
   231   val acc = Output.time_accumulator "Defs.define"
   232 in
   233   fun define pp consts unchecked is_def module name lhs rhs =
   234     acc (define_aux pp consts unchecked is_def module name lhs rhs)
   235 end;
   236 
   237 
   238 end;