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