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