src/Pure/defs.ML
author paulson
Fri, 05 Oct 2007 09:59:03 +0200
changeset 24854 0ebcd575d3c6
parent 24792 fd4655e57168
child 29606 fedb8be05f24
permissions -rw-r--r--
filtering out some package theorems
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
17707
bc0270e9d27f back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents: 17670
diff changeset
     1
(*  Title:      Pure/defs.ML
16108
cf468b93a02e Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff changeset
     2
    ID:         $Id$
17707
bc0270e9d27f back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents: 17670
diff changeset
     3
    Author:     Makarius
16108
cf468b93a02e Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff changeset
     4
19692
bad13b32c0f3 yet another re-implementation:
wenzelm
parents: 19628
diff changeset
     5
Global well-formedness checks for constant definitions.  Covers plain
19701
c07c31ac689b export plain_args;
wenzelm
parents: 19697
diff changeset
     6
definitions and simple sub-structural overloading.
16108
cf468b93a02e Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff changeset
     7
*)
cf468b93a02e Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff changeset
     8
16877
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
     9
signature DEFS =
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
    10
sig
19697
423af2e013b8 specifications_of: lhs/rhs represented as typargs;
wenzelm
parents: 19695
diff changeset
    11
  val pretty_const: Pretty.pp -> string * typ list -> Pretty.T
19701
c07c31ac689b export plain_args;
wenzelm
parents: 19697
diff changeset
    12
  val plain_args: typ list -> bool
17707
bc0270e9d27f back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents: 17670
diff changeset
    13
  type T
24199
8be734b5f59f new access interface in defs.ML
haftmann
parents: 20668
diff changeset
    14
  val specifications_of: T -> string -> {is_def: bool, name: string,
8be734b5f59f new access interface in defs.ML
haftmann
parents: 20668
diff changeset
    15
    lhs: typ list, rhs: (string * typ list) list} list
8be734b5f59f new access interface in defs.ML
haftmann
parents: 20668
diff changeset
    16
  val all_specifications_of: T -> (string * {is_def: bool, name: string,
8be734b5f59f new access interface in defs.ML
haftmann
parents: 20668
diff changeset
    17
    lhs: typ list, rhs: (string * typ list) list} list) list
19697
423af2e013b8 specifications_of: lhs/rhs represented as typargs;
wenzelm
parents: 19695
diff changeset
    18
  val dest: T ->
423af2e013b8 specifications_of: lhs/rhs represented as typargs;
wenzelm
parents: 19695
diff changeset
    19
   {restricts: ((string * typ list) * string) list,
423af2e013b8 specifications_of: lhs/rhs represented as typargs;
wenzelm
parents: 19695
diff changeset
    20
    reducts: ((string * typ list) * (string * typ list) list) list}
19590
12af4942923d simple substructure test for typargs (independent type constructors);
wenzelm
parents: 19569
diff changeset
    21
  val empty: T
19692
bad13b32c0f3 yet another re-implementation:
wenzelm
parents: 19628
diff changeset
    22
  val merge: Pretty.pp -> T * T -> T
24199
8be734b5f59f new access interface in defs.ML
haftmann
parents: 20668
diff changeset
    23
  val define: Pretty.pp -> bool -> bool -> string ->
19727
wenzelm
parents: 19713
diff changeset
    24
    string * typ list -> (string * typ list) list -> T -> T
16108
cf468b93a02e Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff changeset
    25
end
cf468b93a02e Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff changeset
    26
17711
c16cbe73798c activate signature constraints;
wenzelm
parents: 17707
diff changeset
    27
structure Defs: DEFS =
17707
bc0270e9d27f back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents: 17670
diff changeset
    28
struct
16108
cf468b93a02e Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff changeset
    29
19697
423af2e013b8 specifications_of: lhs/rhs represented as typargs;
wenzelm
parents: 19695
diff changeset
    30
(* type arguments *)
19613
9bf274ec94cf allow dependencies of disjoint collections of instances;
wenzelm
parents: 19590
diff changeset
    31
19697
423af2e013b8 specifications_of: lhs/rhs represented as typargs;
wenzelm
parents: 19695
diff changeset
    32
type args = typ list;
423af2e013b8 specifications_of: lhs/rhs represented as typargs;
wenzelm
parents: 19695
diff changeset
    33
423af2e013b8 specifications_of: lhs/rhs represented as typargs;
wenzelm
parents: 19695
diff changeset
    34
fun pretty_const pp (c, args) =
19613
9bf274ec94cf allow dependencies of disjoint collections of instances;
wenzelm
parents: 19590
diff changeset
    35
  let
19692
bad13b32c0f3 yet another re-implementation:
wenzelm
parents: 19628
diff changeset
    36
    val prt_args =
bad13b32c0f3 yet another re-implementation:
wenzelm
parents: 19628
diff changeset
    37
      if null args then []
19806
f860b7a98445 renamed Type.(un)varifyT to Logic.(un)varifyT;
wenzelm
parents: 19760
diff changeset
    38
      else [Pretty.list "(" ")" (map (Pretty.typ pp o Logic.unvarifyT) args)];
19697
423af2e013b8 specifications_of: lhs/rhs represented as typargs;
wenzelm
parents: 19695
diff changeset
    39
  in Pretty.block (Pretty.str c :: prt_args) end;
19624
wenzelm
parents: 19620
diff changeset
    40
19707
wenzelm
parents: 19701
diff changeset
    41
fun plain_args args =
wenzelm
parents: 19701
diff changeset
    42
  forall Term.is_TVar args andalso not (has_duplicates (op =) args);
wenzelm
parents: 19701
diff changeset
    43
19697
423af2e013b8 specifications_of: lhs/rhs represented as typargs;
wenzelm
parents: 19695
diff changeset
    44
fun disjoint_args (Ts, Us) =
423af2e013b8 specifications_of: lhs/rhs represented as typargs;
wenzelm
parents: 19695
diff changeset
    45
  not (Type.could_unifys (Ts, Us)) orelse
423af2e013b8 specifications_of: lhs/rhs represented as typargs;
wenzelm
parents: 19695
diff changeset
    46
    ((Type.raw_unifys (Ts, map (Logic.incr_tvar (maxidx_of_typs Ts + 1)) Us) Vartab.empty; false)
423af2e013b8 specifications_of: lhs/rhs represented as typargs;
wenzelm
parents: 19695
diff changeset
    47
      handle Type.TUNIFY => true);
19692
bad13b32c0f3 yet another re-implementation:
wenzelm
parents: 19628
diff changeset
    48
19697
423af2e013b8 specifications_of: lhs/rhs represented as typargs;
wenzelm
parents: 19695
diff changeset
    49
fun match_args (Ts, Us) =
423af2e013b8 specifications_of: lhs/rhs represented as typargs;
wenzelm
parents: 19695
diff changeset
    50
  Option.map Envir.typ_subst_TVars
423af2e013b8 specifications_of: lhs/rhs represented as typargs;
wenzelm
parents: 19695
diff changeset
    51
    (SOME (Type.raw_matches (Ts, Us) Vartab.empty) handle Type.TYPE_MATCH => NONE);
19692
bad13b32c0f3 yet another re-implementation:
wenzelm
parents: 19628
diff changeset
    52
bad13b32c0f3 yet another re-implementation:
wenzelm
parents: 19628
diff changeset
    53
bad13b32c0f3 yet another re-implementation:
wenzelm
parents: 19628
diff changeset
    54
(* datatype defs *)
bad13b32c0f3 yet another re-implementation:
wenzelm
parents: 19628
diff changeset
    55
24199
8be734b5f59f new access interface in defs.ML
haftmann
parents: 20668
diff changeset
    56
type spec = {is_def: bool, name: string, lhs: args, rhs: (string * args) list};
19697
423af2e013b8 specifications_of: lhs/rhs represented as typargs;
wenzelm
parents: 19695
diff changeset
    57
19692
bad13b32c0f3 yet another re-implementation:
wenzelm
parents: 19628
diff changeset
    58
type def =
19712
3ae3cc4b1eac wellformed: be less ambitious about structural containment;
wenzelm
parents: 19707
diff changeset
    59
 {specs: spec Inttab.table,                 (*source specifications*)
3ae3cc4b1eac wellformed: be less ambitious about structural containment;
wenzelm
parents: 19707
diff changeset
    60
  restricts: (args * string) list,          (*global restrictions imposed by incomplete patterns*)
3ae3cc4b1eac wellformed: be less ambitious about structural containment;
wenzelm
parents: 19707
diff changeset
    61
  reducts: (args * (string * args) list) list};  (*specifications as reduction system*)
19697
423af2e013b8 specifications_of: lhs/rhs represented as typargs;
wenzelm
parents: 19695
diff changeset
    62
423af2e013b8 specifications_of: lhs/rhs represented as typargs;
wenzelm
parents: 19695
diff changeset
    63
fun make_def (specs, restricts, reducts) =
423af2e013b8 specifications_of: lhs/rhs represented as typargs;
wenzelm
parents: 19695
diff changeset
    64
  {specs = specs, restricts = restricts, reducts = reducts}: def;
19692
bad13b32c0f3 yet another re-implementation:
wenzelm
parents: 19628
diff changeset
    65
19697
423af2e013b8 specifications_of: lhs/rhs represented as typargs;
wenzelm
parents: 19695
diff changeset
    66
fun map_def c f =
423af2e013b8 specifications_of: lhs/rhs represented as typargs;
wenzelm
parents: 19695
diff changeset
    67
  Symtab.default (c, make_def (Inttab.empty, [], [])) #>
423af2e013b8 specifications_of: lhs/rhs represented as typargs;
wenzelm
parents: 19695
diff changeset
    68
  Symtab.map_entry c (fn {specs, restricts, reducts}: def =>
423af2e013b8 specifications_of: lhs/rhs represented as typargs;
wenzelm
parents: 19695
diff changeset
    69
    make_def (f (specs, restricts, reducts)));
19692
bad13b32c0f3 yet another re-implementation:
wenzelm
parents: 19628
diff changeset
    70
bad13b32c0f3 yet another re-implementation:
wenzelm
parents: 19628
diff changeset
    71
bad13b32c0f3 yet another re-implementation:
wenzelm
parents: 19628
diff changeset
    72
datatype T = Defs of def Symtab.table;
bad13b32c0f3 yet another re-implementation:
wenzelm
parents: 19628
diff changeset
    73
19712
3ae3cc4b1eac wellformed: be less ambitious about structural containment;
wenzelm
parents: 19707
diff changeset
    74
fun lookup_list which defs c =
19692
bad13b32c0f3 yet another re-implementation:
wenzelm
parents: 19628
diff changeset
    75
  (case Symtab.lookup defs c of
19713
69c71d40f8a8 made smlnj happy;
wenzelm
parents: 19712
diff changeset
    76
    SOME (def: def) => which def
19692
bad13b32c0f3 yet another re-implementation:
wenzelm
parents: 19628
diff changeset
    77
  | NONE => []);
bad13b32c0f3 yet another re-implementation:
wenzelm
parents: 19628
diff changeset
    78
24199
8be734b5f59f new access interface in defs.ML
haftmann
parents: 20668
diff changeset
    79
fun specifications_of (Defs defs) = lookup_list (map snd o Inttab.dest o #specs) defs;
8be734b5f59f new access interface in defs.ML
haftmann
parents: 20668
diff changeset
    80
fun all_specifications_of (Defs defs) =
8be734b5f59f new access interface in defs.ML
haftmann
parents: 20668
diff changeset
    81
  ((map o apsnd) (map snd o Inttab.dest o #specs) o Symtab.dest) defs;
19692
bad13b32c0f3 yet another re-implementation:
wenzelm
parents: 19628
diff changeset
    82
val restricts_of = lookup_list #restricts;
bad13b32c0f3 yet another re-implementation:
wenzelm
parents: 19628
diff changeset
    83
val reducts_of = lookup_list #reducts;
bad13b32c0f3 yet another re-implementation:
wenzelm
parents: 19628
diff changeset
    84
19697
423af2e013b8 specifications_of: lhs/rhs represented as typargs;
wenzelm
parents: 19695
diff changeset
    85
fun dest (Defs defs) =
423af2e013b8 specifications_of: lhs/rhs represented as typargs;
wenzelm
parents: 19695
diff changeset
    86
  let
423af2e013b8 specifications_of: lhs/rhs represented as typargs;
wenzelm
parents: 19695
diff changeset
    87
    val restricts = Symtab.fold (fn (c, {restricts, ...}) =>
423af2e013b8 specifications_of: lhs/rhs represented as typargs;
wenzelm
parents: 19695
diff changeset
    88
      fold (fn (args, name) => cons ((c, args), name)) restricts) defs [];
423af2e013b8 specifications_of: lhs/rhs represented as typargs;
wenzelm
parents: 19695
diff changeset
    89
    val reducts = Symtab.fold (fn (c, {reducts, ...}) =>
423af2e013b8 specifications_of: lhs/rhs represented as typargs;
wenzelm
parents: 19695
diff changeset
    90
      fold (fn (args, deps) => cons ((c, args), deps)) reducts) defs [];
423af2e013b8 specifications_of: lhs/rhs represented as typargs;
wenzelm
parents: 19695
diff changeset
    91
  in {restricts = restricts, reducts = reducts} end;
19692
bad13b32c0f3 yet another re-implementation:
wenzelm
parents: 19628
diff changeset
    92
19697
423af2e013b8 specifications_of: lhs/rhs represented as typargs;
wenzelm
parents: 19695
diff changeset
    93
val empty = Defs Symtab.empty;
423af2e013b8 specifications_of: lhs/rhs represented as typargs;
wenzelm
parents: 19695
diff changeset
    94
423af2e013b8 specifications_of: lhs/rhs represented as typargs;
wenzelm
parents: 19695
diff changeset
    95
423af2e013b8 specifications_of: lhs/rhs represented as typargs;
wenzelm
parents: 19695
diff changeset
    96
(* specifications *)
19692
bad13b32c0f3 yet another re-implementation:
wenzelm
parents: 19628
diff changeset
    97
19697
423af2e013b8 specifications_of: lhs/rhs represented as typargs;
wenzelm
parents: 19695
diff changeset
    98
fun disjoint_specs c (i, {lhs = Ts, name = a, ...}: spec) =
423af2e013b8 specifications_of: lhs/rhs represented as typargs;
wenzelm
parents: 19695
diff changeset
    99
  Inttab.forall (fn (j, {lhs = Us, name = b, ...}: spec) =>
423af2e013b8 specifications_of: lhs/rhs represented as typargs;
wenzelm
parents: 19695
diff changeset
   100
    i = j orelse disjoint_args (Ts, Us) orelse
24792
fd4655e57168 tuned message;
wenzelm
parents: 24199
diff changeset
   101
      error ("Clash of specifications " ^ quote a ^ " and " ^ quote b ^
19697
423af2e013b8 specifications_of: lhs/rhs represented as typargs;
wenzelm
parents: 19695
diff changeset
   102
        " for constant " ^ quote c));
19692
bad13b32c0f3 yet another re-implementation:
wenzelm
parents: 19628
diff changeset
   103
19697
423af2e013b8 specifications_of: lhs/rhs represented as typargs;
wenzelm
parents: 19695
diff changeset
   104
fun join_specs c ({specs = specs1, restricts, reducts}, {specs = specs2, ...}: def) =
423af2e013b8 specifications_of: lhs/rhs represented as typargs;
wenzelm
parents: 19695
diff changeset
   105
  let
423af2e013b8 specifications_of: lhs/rhs represented as typargs;
wenzelm
parents: 19695
diff changeset
   106
    val specs' =
423af2e013b8 specifications_of: lhs/rhs represented as typargs;
wenzelm
parents: 19695
diff changeset
   107
      Inttab.fold (fn spec2 => (disjoint_specs c spec2 specs1; Inttab.update spec2)) specs2 specs1;
423af2e013b8 specifications_of: lhs/rhs represented as typargs;
wenzelm
parents: 19695
diff changeset
   108
  in make_def (specs', restricts, reducts) end;
423af2e013b8 specifications_of: lhs/rhs represented as typargs;
wenzelm
parents: 19695
diff changeset
   109
423af2e013b8 specifications_of: lhs/rhs represented as typargs;
wenzelm
parents: 19695
diff changeset
   110
fun update_specs c spec = map_def c (fn (specs, restricts, reducts) =>
423af2e013b8 specifications_of: lhs/rhs represented as typargs;
wenzelm
parents: 19695
diff changeset
   111
  (disjoint_specs c spec specs; (Inttab.update spec specs, restricts, reducts)));
423af2e013b8 specifications_of: lhs/rhs represented as typargs;
wenzelm
parents: 19695
diff changeset
   112
423af2e013b8 specifications_of: lhs/rhs represented as typargs;
wenzelm
parents: 19695
diff changeset
   113
19701
c07c31ac689b export plain_args;
wenzelm
parents: 19697
diff changeset
   114
(* normalized dependencies: reduction with well-formedness check *)
19697
423af2e013b8 specifications_of: lhs/rhs represented as typargs;
wenzelm
parents: 19695
diff changeset
   115
423af2e013b8 specifications_of: lhs/rhs represented as typargs;
wenzelm
parents: 19695
diff changeset
   116
local
423af2e013b8 specifications_of: lhs/rhs represented as typargs;
wenzelm
parents: 19695
diff changeset
   117
19729
cb9e2f0c7658 separate checks for acyclic/wellformed;
wenzelm
parents: 19727
diff changeset
   118
val prt = Pretty.string_of oo pretty_const;
cb9e2f0c7658 separate checks for acyclic/wellformed;
wenzelm
parents: 19727
diff changeset
   119
fun err pp (c, args) (d, Us) s1 s2 =
cb9e2f0c7658 separate checks for acyclic/wellformed;
wenzelm
parents: 19727
diff changeset
   120
  error (s1 ^ " dependency of constant " ^ prt pp (c, args) ^ " -> " ^ prt pp (d, Us) ^ s2);
cb9e2f0c7658 separate checks for acyclic/wellformed;
wenzelm
parents: 19727
diff changeset
   121
19712
3ae3cc4b1eac wellformed: be less ambitious about structural containment;
wenzelm
parents: 19707
diff changeset
   122
fun contained (U as TVar _) (Type (_, Ts)) = exists (fn T => T = U orelse contained U T) Ts
19697
423af2e013b8 specifications_of: lhs/rhs represented as typargs;
wenzelm
parents: 19695
diff changeset
   123
  | contained _ _ = false;
423af2e013b8 specifications_of: lhs/rhs represented as typargs;
wenzelm
parents: 19695
diff changeset
   124
19729
cb9e2f0c7658 separate checks for acyclic/wellformed;
wenzelm
parents: 19727
diff changeset
   125
fun acyclic pp defs (c, args) (d, Us) =
cb9e2f0c7658 separate checks for acyclic/wellformed;
wenzelm
parents: 19727
diff changeset
   126
  c <> d orelse
cb9e2f0c7658 separate checks for acyclic/wellformed;
wenzelm
parents: 19727
diff changeset
   127
  exists (fn U => exists (contained U) args) Us orelse
cb9e2f0c7658 separate checks for acyclic/wellformed;
wenzelm
parents: 19727
diff changeset
   128
  is_none (match_args (args, Us)) orelse
cb9e2f0c7658 separate checks for acyclic/wellformed;
wenzelm
parents: 19727
diff changeset
   129
  err pp (c, args) (d, Us) "Circular" "";
cb9e2f0c7658 separate checks for acyclic/wellformed;
wenzelm
parents: 19727
diff changeset
   130
19701
c07c31ac689b export plain_args;
wenzelm
parents: 19697
diff changeset
   131
fun wellformed pp defs (c, args) (d, Us) =
19729
cb9e2f0c7658 separate checks for acyclic/wellformed;
wenzelm
parents: 19727
diff changeset
   132
  forall is_TVar Us orelse
cb9e2f0c7658 separate checks for acyclic/wellformed;
wenzelm
parents: 19727
diff changeset
   133
  (case find_first (fn (Ts, _) => not (disjoint_args (Ts, Us))) (restricts_of defs d) of
cb9e2f0c7658 separate checks for acyclic/wellformed;
wenzelm
parents: 19727
diff changeset
   134
    SOME (Ts, name) =>
cb9e2f0c7658 separate checks for acyclic/wellformed;
wenzelm
parents: 19727
diff changeset
   135
      err pp (c, args) (d, Us) "Malformed"
cb9e2f0c7658 separate checks for acyclic/wellformed;
wenzelm
parents: 19727
diff changeset
   136
        ("\n(restriction " ^ prt pp (d, Ts) ^ " from " ^ quote name ^ ")")
cb9e2f0c7658 separate checks for acyclic/wellformed;
wenzelm
parents: 19727
diff changeset
   137
  | NONE => true);
19692
bad13b32c0f3 yet another re-implementation:
wenzelm
parents: 19628
diff changeset
   138
19701
c07c31ac689b export plain_args;
wenzelm
parents: 19697
diff changeset
   139
fun reduction pp defs const deps =
19692
bad13b32c0f3 yet another re-implementation:
wenzelm
parents: 19628
diff changeset
   140
  let
19701
c07c31ac689b export plain_args;
wenzelm
parents: 19697
diff changeset
   141
    fun reduct Us (Ts, rhs) =
c07c31ac689b export plain_args;
wenzelm
parents: 19697
diff changeset
   142
      (case match_args (Ts, Us) of
c07c31ac689b export plain_args;
wenzelm
parents: 19697
diff changeset
   143
        NONE => NONE
c07c31ac689b export plain_args;
wenzelm
parents: 19697
diff changeset
   144
      | SOME subst => SOME (map (apsnd (map subst)) rhs));
c07c31ac689b export plain_args;
wenzelm
parents: 19697
diff changeset
   145
    fun reducts (d, Us) = get_first (reduct Us) (reducts_of defs d);
c07c31ac689b export plain_args;
wenzelm
parents: 19697
diff changeset
   146
c07c31ac689b export plain_args;
wenzelm
parents: 19697
diff changeset
   147
    val reds = map (`reducts) deps;
c07c31ac689b export plain_args;
wenzelm
parents: 19697
diff changeset
   148
    val deps' =
c07c31ac689b export plain_args;
wenzelm
parents: 19697
diff changeset
   149
      if forall (is_none o #1) reds then NONE
20668
wenzelm
parents: 20390
diff changeset
   150
      else SOME (fold_rev
wenzelm
parents: 20390
diff changeset
   151
        (fn (NONE, dp) => insert (op =) dp | (SOME dps, _) => fold (insert (op =)) dps) reds []);
19729
cb9e2f0c7658 separate checks for acyclic/wellformed;
wenzelm
parents: 19727
diff changeset
   152
    val _ = forall (acyclic pp defs const) (the_default deps deps');
19697
423af2e013b8 specifications_of: lhs/rhs represented as typargs;
wenzelm
parents: 19695
diff changeset
   153
  in deps' end;
19692
bad13b32c0f3 yet another re-implementation:
wenzelm
parents: 19628
diff changeset
   154
19760
c7e9cc10acc8 merge: always normalize (and check!) reductions;
wenzelm
parents: 19729
diff changeset
   155
in
c7e9cc10acc8 merge: always normalize (and check!) reductions;
wenzelm
parents: 19729
diff changeset
   156
19712
3ae3cc4b1eac wellformed: be less ambitious about structural containment;
wenzelm
parents: 19707
diff changeset
   157
fun normalize pp =
19692
bad13b32c0f3 yet another re-implementation:
wenzelm
parents: 19628
diff changeset
   158
  let
19701
c07c31ac689b export plain_args;
wenzelm
parents: 19697
diff changeset
   159
    fun norm_update (c, {reducts, ...}: def) (changed, defs) =
c07c31ac689b export plain_args;
wenzelm
parents: 19697
diff changeset
   160
      let
c07c31ac689b export plain_args;
wenzelm
parents: 19697
diff changeset
   161
        val reducts' = reducts |> map (fn (args, deps) =>
19712
3ae3cc4b1eac wellformed: be less ambitious about structural containment;
wenzelm
parents: 19707
diff changeset
   162
          (args, perhaps (reduction pp defs (c, args)) deps));
19697
423af2e013b8 specifications_of: lhs/rhs represented as typargs;
wenzelm
parents: 19695
diff changeset
   163
      in
19701
c07c31ac689b export plain_args;
wenzelm
parents: 19697
diff changeset
   164
        if reducts = reducts' then (changed, defs)
c07c31ac689b export plain_args;
wenzelm
parents: 19697
diff changeset
   165
        else (true, defs |> map_def c (fn (specs, restricts, reducts) =>
c07c31ac689b export plain_args;
wenzelm
parents: 19697
diff changeset
   166
          (specs, restricts, reducts')))
19697
423af2e013b8 specifications_of: lhs/rhs represented as typargs;
wenzelm
parents: 19695
diff changeset
   167
      end;
19701
c07c31ac689b export plain_args;
wenzelm
parents: 19697
diff changeset
   168
    fun norm_all defs =
c07c31ac689b export plain_args;
wenzelm
parents: 19697
diff changeset
   169
      (case Symtab.fold norm_update defs (false, defs) of
c07c31ac689b export plain_args;
wenzelm
parents: 19697
diff changeset
   170
        (true, defs') => norm_all defs'
c07c31ac689b export plain_args;
wenzelm
parents: 19697
diff changeset
   171
      | (false, _) => defs);
19729
cb9e2f0c7658 separate checks for acyclic/wellformed;
wenzelm
parents: 19727
diff changeset
   172
    fun check defs (c, {reducts, ...}: def) =
cb9e2f0c7658 separate checks for acyclic/wellformed;
wenzelm
parents: 19727
diff changeset
   173
      reducts |> forall (fn (args, deps) => forall (wellformed pp defs (c, args)) deps);
cb9e2f0c7658 separate checks for acyclic/wellformed;
wenzelm
parents: 19727
diff changeset
   174
  in norm_all #> (fn defs => tap (Symtab.forall (check defs)) defs) end;
19701
c07c31ac689b export plain_args;
wenzelm
parents: 19697
diff changeset
   175
19712
3ae3cc4b1eac wellformed: be less ambitious about structural containment;
wenzelm
parents: 19707
diff changeset
   176
fun dependencies pp (c, args) restr deps =
3ae3cc4b1eac wellformed: be less ambitious about structural containment;
wenzelm
parents: 19707
diff changeset
   177
  map_def c (fn (specs, restricts, reducts) =>
3ae3cc4b1eac wellformed: be less ambitious about structural containment;
wenzelm
parents: 19707
diff changeset
   178
    let
3ae3cc4b1eac wellformed: be less ambitious about structural containment;
wenzelm
parents: 19707
diff changeset
   179
      val restricts' = Library.merge (op =) (restricts, restr);
3ae3cc4b1eac wellformed: be less ambitious about structural containment;
wenzelm
parents: 19707
diff changeset
   180
      val reducts' = insert (op =) (args, deps) reducts;
3ae3cc4b1eac wellformed: be less ambitious about structural containment;
wenzelm
parents: 19707
diff changeset
   181
    in (specs, restricts', reducts') end)
3ae3cc4b1eac wellformed: be less ambitious about structural containment;
wenzelm
parents: 19707
diff changeset
   182
  #> normalize pp;
19697
423af2e013b8 specifications_of: lhs/rhs represented as typargs;
wenzelm
parents: 19695
diff changeset
   183
423af2e013b8 specifications_of: lhs/rhs represented as typargs;
wenzelm
parents: 19695
diff changeset
   184
end;
19692
bad13b32c0f3 yet another re-implementation:
wenzelm
parents: 19628
diff changeset
   185
bad13b32c0f3 yet another re-implementation:
wenzelm
parents: 19628
diff changeset
   186
19624
wenzelm
parents: 19620
diff changeset
   187
(* merge *)
wenzelm
parents: 19620
diff changeset
   188
19692
bad13b32c0f3 yet another re-implementation:
wenzelm
parents: 19628
diff changeset
   189
fun merge pp (Defs defs1, Defs defs2) =
19613
9bf274ec94cf allow dependencies of disjoint collections of instances;
wenzelm
parents: 19590
diff changeset
   190
  let
19697
423af2e013b8 specifications_of: lhs/rhs represented as typargs;
wenzelm
parents: 19695
diff changeset
   191
    fun add_deps (c, args) restr deps defs =
19692
bad13b32c0f3 yet another re-implementation:
wenzelm
parents: 19628
diff changeset
   192
      if AList.defined (op =) (reducts_of defs c) args then defs
19697
423af2e013b8 specifications_of: lhs/rhs represented as typargs;
wenzelm
parents: 19695
diff changeset
   193
      else dependencies pp (c, args) restr deps defs;
423af2e013b8 specifications_of: lhs/rhs represented as typargs;
wenzelm
parents: 19695
diff changeset
   194
    fun add_def (c, {restricts, reducts, ...}: def) =
423af2e013b8 specifications_of: lhs/rhs represented as typargs;
wenzelm
parents: 19695
diff changeset
   195
      fold (fn (args, deps) => add_deps (c, args) restricts deps) reducts;
19760
c7e9cc10acc8 merge: always normalize (and check!) reductions;
wenzelm
parents: 19729
diff changeset
   196
  in
c7e9cc10acc8 merge: always normalize (and check!) reductions;
wenzelm
parents: 19729
diff changeset
   197
    Defs (Symtab.join join_specs (defs1, defs2)
c7e9cc10acc8 merge: always normalize (and check!) reductions;
wenzelm
parents: 19729
diff changeset
   198
      |> normalize pp |> Symtab.fold add_def defs2)
c7e9cc10acc8 merge: always normalize (and check!) reductions;
wenzelm
parents: 19729
diff changeset
   199
  end;
19613
9bf274ec94cf allow dependencies of disjoint collections of instances;
wenzelm
parents: 19590
diff changeset
   200
9bf274ec94cf allow dependencies of disjoint collections of instances;
wenzelm
parents: 19590
diff changeset
   201
9bf274ec94cf allow dependencies of disjoint collections of instances;
wenzelm
parents: 19590
diff changeset
   202
(* define *)
19590
12af4942923d simple substructure test for typargs (independent type constructors);
wenzelm
parents: 19569
diff changeset
   203
24199
8be734b5f59f new access interface in defs.ML
haftmann
parents: 20668
diff changeset
   204
fun define pp unchecked is_def name (c, args) deps (Defs defs) =
17707
bc0270e9d27f back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents: 17670
diff changeset
   205
  let
19697
423af2e013b8 specifications_of: lhs/rhs represented as typargs;
wenzelm
parents: 19695
diff changeset
   206
    val restr =
423af2e013b8 specifications_of: lhs/rhs represented as typargs;
wenzelm
parents: 19695
diff changeset
   207
      if plain_args args orelse
423af2e013b8 specifications_of: lhs/rhs represented as typargs;
wenzelm
parents: 19695
diff changeset
   208
        (case args of [Type (a, rec_args)] => plain_args rec_args | _ => false)
423af2e013b8 specifications_of: lhs/rhs represented as typargs;
wenzelm
parents: 19695
diff changeset
   209
      then [] else [(args, name)];
19692
bad13b32c0f3 yet another re-implementation:
wenzelm
parents: 19628
diff changeset
   210
    val spec =
24199
8be734b5f59f new access interface in defs.ML
haftmann
parents: 20668
diff changeset
   211
      (serial (), {is_def = is_def, name = name, lhs = args, rhs = deps});
19697
423af2e013b8 specifications_of: lhs/rhs represented as typargs;
wenzelm
parents: 19695
diff changeset
   212
    val defs' = defs |> update_specs c spec;
19712
3ae3cc4b1eac wellformed: be less ambitious about structural containment;
wenzelm
parents: 19707
diff changeset
   213
  in Defs (defs' |> (if unchecked then I else dependencies pp (c, args) restr deps)) end;
19697
423af2e013b8 specifications_of: lhs/rhs represented as typargs;
wenzelm
parents: 19695
diff changeset
   214
423af2e013b8 specifications_of: lhs/rhs represented as typargs;
wenzelm
parents: 19695
diff changeset
   215
end;