src/Pure/defs.ML
author wenzelm
Tue Sep 26 20:54:40 2017 +0200 (22 months ago)
changeset 66695 91500c024c7f
parent 62181 4025b5ce1901
permissions -rw-r--r--
tuned;
wenzelm@17707
     1
(*  Title:      Pure/defs.ML
wenzelm@17707
     2
    Author:     Makarius
obua@16108
     3
wenzelm@62179
     4
Global well-formedness checks for overloaded definitions (mixed constants and
wenzelm@62179
     5
types). Recall that constant definitions may be explained syntactically within
wenzelm@62179
     6
Pure, but type definitions require particular set-theoretic semantics.
obua@16108
     7
*)
obua@16108
     8
wenzelm@16877
     9
signature DEFS =
wenzelm@16877
    10
sig
wenzelm@61256
    11
  datatype item_kind = Const | Type
wenzelm@61249
    12
  type item = item_kind * string
wenzelm@61254
    13
  type entry = item * typ list
wenzelm@61261
    14
  val item_kind_ord: item_kind * item_kind -> order
wenzelm@61261
    15
  val plain_args: typ list -> bool
wenzelm@61265
    16
  type context = Proof.context * (Name_Space.T * Name_Space.T)
wenzelm@61262
    17
  val global_context: theory -> context
wenzelm@61261
    18
  val space: context -> item_kind -> Name_Space.T
wenzelm@61261
    19
  val pretty_item: context -> item -> Pretty.T
wenzelm@61253
    20
  val pretty_args: Proof.context -> typ list -> Pretty.T list
wenzelm@61261
    21
  val pretty_entry: context -> entry -> Pretty.T
wenzelm@17707
    22
  type T
wenzelm@33712
    23
  type spec =
wenzelm@55544
    24
   {def: string option,
wenzelm@55544
    25
    description: string,
wenzelm@55544
    26
    pos: Position.T,
wenzelm@55544
    27
    lhs: typ list,
wenzelm@61254
    28
    rhs: entry list}
wenzelm@61249
    29
  val all_specifications_of: T -> (item * spec list) list
wenzelm@61249
    30
  val specifications_of: T -> item -> spec list
wenzelm@19697
    31
  val dest: T ->
wenzelm@61254
    32
   {restricts: (entry * string) list,
wenzelm@61254
    33
    reducts: (entry * entry list) list}
wenzelm@19590
    34
  val empty: T
wenzelm@61261
    35
  val merge: context -> T * T -> T
wenzelm@61261
    36
  val define: context -> bool -> string option -> string -> entry -> entry list -> T -> T
wenzelm@61260
    37
  val get_deps: T -> item -> (typ list * entry list) list
wenzelm@61249
    38
end;
wenzelm@61246
    39
wenzelm@17711
    40
structure Defs: DEFS =
wenzelm@17707
    41
struct
obua@16108
    42
wenzelm@61249
    43
(* specification items *)
wenzelm@61249
    44
wenzelm@61256
    45
datatype item_kind = Const | Type;
wenzelm@61249
    46
type item = item_kind * string;
wenzelm@61261
    47
type entry = item * typ list;
wenzelm@61249
    48
wenzelm@61256
    49
fun item_kind_ord (Const, Type) = LESS
wenzelm@61256
    50
  | item_kind_ord (Type, Const) = GREATER
wenzelm@61249
    51
  | item_kind_ord _ = EQUAL;
wenzelm@61246
    52
wenzelm@61261
    53
structure Itemtab = Table(type key = item val ord = prod_ord item_kind_ord fast_string_ord);
wenzelm@61249
    54
wenzelm@61246
    55
wenzelm@61261
    56
(* pretty printing *)
wenzelm@61261
    57
wenzelm@62179
    58
type context = Proof.context * (Name_Space.T * Name_Space.T);
wenzelm@61262
    59
wenzelm@61265
    60
fun global_context thy =
wenzelm@61265
    61
  (Syntax.init_pretty_global thy, (Sign.const_space thy, Sign.type_space thy));
wenzelm@61265
    62
wenzelm@62179
    63
fun space ((_, spaces): context) kind =
wenzelm@61265
    64
  if kind = Const then #1 spaces else #2 spaces;
wenzelm@61261
    65
wenzelm@61261
    66
fun pretty_item (context as (ctxt, _)) (kind, name) =
wenzelm@61261
    67
  let val prt_name = Name_Space.pretty ctxt (space context kind) name in
wenzelm@61261
    68
    if kind = Const then prt_name
wenzelm@61261
    69
    else Pretty.block [Pretty.keyword1 "type", Pretty.brk 1, prt_name]
wenzelm@61261
    70
  end;
wenzelm@19697
    71
wenzelm@61253
    72
fun pretty_args ctxt args =
wenzelm@61253
    73
  if null args then []
wenzelm@61253
    74
  else [Pretty.list "(" ")" (map (Syntax.pretty_typ ctxt o Logic.unvarifyT_global) args)];
wenzelm@61253
    75
wenzelm@61261
    76
fun pretty_entry context (c, args) =
wenzelm@61261
    77
  Pretty.block (pretty_item context c :: pretty_args (#1 context) args);
wenzelm@61261
    78
wenzelm@61261
    79
wenzelm@61261
    80
(* type arguments *)
wenzelm@19624
    81
wenzelm@19707
    82
fun plain_args args =
wenzelm@19707
    83
  forall Term.is_TVar args andalso not (has_duplicates (op =) args);
wenzelm@19707
    84
wenzelm@19697
    85
fun disjoint_args (Ts, Us) =
wenzelm@19697
    86
  not (Type.could_unifys (Ts, Us)) orelse
wenzelm@19697
    87
    ((Type.raw_unifys (Ts, map (Logic.incr_tvar (maxidx_of_typs Ts + 1)) Us) Vartab.empty; false)
wenzelm@19697
    88
      handle Type.TUNIFY => true);
wenzelm@19692
    89
wenzelm@19697
    90
fun match_args (Ts, Us) =
wenzelm@56050
    91
  if Type.could_matches (Ts, Us) then
wenzelm@56050
    92
    Option.map Envir.subst_type
wenzelm@56050
    93
      (SOME (Type.raw_matches (Ts, Us) Vartab.empty) handle Type.TYPE_MATCH => NONE)
wenzelm@56050
    94
  else NONE;
wenzelm@19692
    95
wenzelm@19692
    96
wenzelm@19692
    97
(* datatype defs *)
wenzelm@19692
    98
wenzelm@33701
    99
type spec =
wenzelm@55544
   100
 {def: string option,
wenzelm@55544
   101
  description: string,
wenzelm@55544
   102
  pos: Position.T,
wenzelm@61254
   103
  lhs: typ list,
wenzelm@61254
   104
  rhs: entry list};
wenzelm@19697
   105
wenzelm@19692
   106
type def =
wenzelm@55544
   107
 {specs: spec Inttab.table,  (*source specifications*)
wenzelm@61254
   108
  restricts: (typ list * string) list,  (*global restrictions imposed by incomplete patterns*)
wenzelm@61254
   109
  reducts: (typ list * entry list) list};  (*specifications as reduction system*)
wenzelm@19697
   110
wenzelm@19697
   111
fun make_def (specs, restricts, reducts) =
wenzelm@19697
   112
  {specs = specs, restricts = restricts, reducts = reducts}: def;
wenzelm@19692
   113
wenzelm@19697
   114
fun map_def c f =
wenzelm@61249
   115
  Itemtab.default (c, make_def (Inttab.empty, [], [])) #>
wenzelm@61249
   116
  Itemtab.map_entry c (fn {specs, restricts, reducts}: def =>
wenzelm@19697
   117
    make_def (f (specs, restricts, reducts)));
wenzelm@19692
   118
wenzelm@19692
   119
wenzelm@61249
   120
datatype T = Defs of def Itemtab.table;
wenzelm@19692
   121
wenzelm@19712
   122
fun lookup_list which defs c =
wenzelm@61249
   123
  (case Itemtab.lookup defs c of
wenzelm@19713
   124
    SOME (def: def) => which def
wenzelm@19692
   125
  | NONE => []);
wenzelm@19692
   126
wenzelm@32050
   127
fun all_specifications_of (Defs defs) =
wenzelm@61249
   128
  (map o apsnd) (map snd o Inttab.dest o #specs) (Itemtab.dest defs);
wenzelm@32050
   129
haftmann@24199
   130
fun specifications_of (Defs defs) = lookup_list (map snd o Inttab.dest o #specs) defs;
wenzelm@32050
   131
wenzelm@19692
   132
val restricts_of = lookup_list #restricts;
wenzelm@19692
   133
val reducts_of = lookup_list #reducts;
wenzelm@19692
   134
wenzelm@19697
   135
fun dest (Defs defs) =
wenzelm@19697
   136
  let
wenzelm@61249
   137
    val restricts = Itemtab.fold (fn (c, {restricts, ...}) =>
wenzelm@33701
   138
      fold (fn (args, description) => cons ((c, args), description)) restricts) defs [];
wenzelm@61249
   139
    val reducts = Itemtab.fold (fn (c, {reducts, ...}) =>
wenzelm@19697
   140
      fold (fn (args, deps) => cons ((c, args), deps)) reducts) defs [];
wenzelm@19697
   141
  in {restricts = restricts, reducts = reducts} end;
wenzelm@19692
   142
wenzelm@61249
   143
val empty = Defs Itemtab.empty;
wenzelm@19697
   144
wenzelm@19697
   145
wenzelm@19697
   146
(* specifications *)
wenzelm@19692
   147
wenzelm@61261
   148
fun disjoint_specs context c (i, {description = a, pos = pos_a, lhs = Ts, ...}: spec) =
wenzelm@55544
   149
  Inttab.forall (fn (j, {description = b, pos = pos_b, lhs = Us, ...}: spec) =>
wenzelm@19697
   150
    i = j orelse disjoint_args (Ts, Us) orelse
wenzelm@61877
   151
      error ("Clash of specifications for " ^
wenzelm@61877
   152
        Pretty.unformatted_string_of (pretty_item context c) ^ ":\n" ^
wenzelm@55544
   153
        "  " ^ quote a ^ Position.here pos_a ^ "\n" ^
wenzelm@55544
   154
        "  " ^ quote b ^ Position.here pos_b));
wenzelm@19692
   155
wenzelm@61261
   156
fun join_specs context c ({specs = specs1, restricts, reducts}, {specs = specs2, ...}: def) =
wenzelm@19697
   157
  let
wenzelm@19697
   158
    val specs' =
wenzelm@61261
   159
      Inttab.fold (fn spec2 => (disjoint_specs context c spec2 specs1; Inttab.update spec2))
wenzelm@61261
   160
        specs2 specs1;
wenzelm@19697
   161
  in make_def (specs', restricts, reducts) end;
wenzelm@19697
   162
wenzelm@61261
   163
fun update_specs context c spec = map_def c (fn (specs, restricts, reducts) =>
wenzelm@61261
   164
  (disjoint_specs context c spec specs; (Inttab.update spec specs, restricts, reducts)));
wenzelm@19697
   165
wenzelm@19697
   166
wenzelm@19701
   167
(* normalized dependencies: reduction with well-formedness check *)
wenzelm@19697
   168
wenzelm@19697
   169
local
wenzelm@19697
   170
wenzelm@61253
   171
val prt = Pretty.string_of oo pretty_entry;
wenzelm@19729
   172
wenzelm@62181
   173
fun err context (c, Ts) (d, Us) s1 s2 =
wenzelm@62181
   174
  error (s1 ^ " dependency of " ^ prt context (c, Ts) ^ " -> " ^ prt context (d, Us) ^ s2);
wenzelm@19729
   175
wenzelm@62181
   176
fun acyclic context (c, Ts) (d, Us) =
wenzelm@62181
   177
  c <> d orelse
wenzelm@62181
   178
  is_none (match_args (Ts, Us)) orelse
wenzelm@62181
   179
  err context (c, Ts) (d, Us) "Circular" "";
wenzelm@19692
   180
wenzelm@61261
   181
fun reduction context defs const deps =
wenzelm@19692
   182
  let
wenzelm@19701
   183
    fun reduct Us (Ts, rhs) =
wenzelm@19701
   184
      (case match_args (Ts, Us) of
wenzelm@19701
   185
        NONE => NONE
wenzelm@19701
   186
      | SOME subst => SOME (map (apsnd (map subst)) rhs));
wenzelm@19701
   187
    fun reducts (d, Us) = get_first (reduct Us) (reducts_of defs d);
wenzelm@19701
   188
wenzelm@19701
   189
    val reds = map (`reducts) deps;
wenzelm@19701
   190
    val deps' =
wenzelm@19701
   191
      if forall (is_none o #1) reds then NONE
wenzelm@20668
   192
      else SOME (fold_rev
wenzelm@20668
   193
        (fn (NONE, dp) => insert (op =) dp | (SOME dps, _) => fold (insert (op =)) dps) reds []);
wenzelm@61261
   194
    val _ = forall (acyclic context const) (the_default deps deps');
wenzelm@19697
   195
  in deps' end;
wenzelm@19692
   196
wenzelm@62181
   197
fun restriction context defs (c, Ts) (d, Us) =
wenzelm@62181
   198
  plain_args Us orelse
wenzelm@62181
   199
  (case find_first (fn (Rs, _) => not (disjoint_args (Rs, Us))) (restricts_of defs d) of
wenzelm@62181
   200
    SOME (Rs, description) =>
wenzelm@62181
   201
      err context (c, Ts) (d, Us) "Malformed"
wenzelm@62181
   202
        ("\n(restriction " ^ prt context (d, Rs) ^ " from " ^ quote description ^ ")")
wenzelm@62181
   203
  | NONE => true);
wenzelm@62181
   204
wenzelm@19760
   205
in
wenzelm@19760
   206
wenzelm@61261
   207
fun normalize context =
wenzelm@19692
   208
  let
wenzelm@62180
   209
    fun check_def defs (c, {reducts, ...}: def) =
wenzelm@62181
   210
      reducts |> forall (fn (Ts, deps) => forall (restriction context defs (c, Ts)) deps);
wenzelm@62180
   211
    fun check_defs defs = Itemtab.forall (check_def defs) defs;
wenzelm@62180
   212
wenzelm@19701
   213
    fun norm_update (c, {reducts, ...}: def) (changed, defs) =
wenzelm@19701
   214
      let
wenzelm@62181
   215
        val reducts' = reducts |> map (fn (Ts, deps) =>
wenzelm@62181
   216
          (Ts, perhaps (reduction context defs (c, Ts)) deps));
wenzelm@19697
   217
      in
wenzelm@19701
   218
        if reducts = reducts' then (changed, defs)
wenzelm@32785
   219
        else (true, defs |> map_def c (fn (specs, restricts, _) => (specs, restricts, reducts')))
wenzelm@19697
   220
      end;
wenzelm@62180
   221
    fun norm_loop defs =
wenzelm@61249
   222
      (case Itemtab.fold norm_update defs (false, defs) of
wenzelm@62180
   223
        (true, defs') => norm_loop defs'
wenzelm@19701
   224
      | (false, _) => defs);
wenzelm@62180
   225
  in norm_loop #> tap check_defs end;
wenzelm@19701
   226
wenzelm@61261
   227
fun dependencies context (c, args) restr deps =
wenzelm@19712
   228
  map_def c (fn (specs, restricts, reducts) =>
wenzelm@19712
   229
    let
wenzelm@19712
   230
      val restricts' = Library.merge (op =) (restricts, restr);
wenzelm@19712
   231
      val reducts' = insert (op =) (args, deps) reducts;
wenzelm@19712
   232
    in (specs, restricts', reducts') end)
wenzelm@61261
   233
  #> normalize context;
wenzelm@19697
   234
wenzelm@19697
   235
end;
wenzelm@19692
   236
wenzelm@19692
   237
wenzelm@19624
   238
(* merge *)
wenzelm@19624
   239
wenzelm@61261
   240
fun merge context (Defs defs1, Defs defs2) =
wenzelm@19613
   241
  let
wenzelm@19697
   242
    fun add_deps (c, args) restr deps defs =
wenzelm@19692
   243
      if AList.defined (op =) (reducts_of defs c) args then defs
wenzelm@61261
   244
      else dependencies context (c, args) restr deps defs;
wenzelm@19697
   245
    fun add_def (c, {restricts, reducts, ...}: def) =
wenzelm@19697
   246
      fold (fn (args, deps) => add_deps (c, args) restricts deps) reducts;
wenzelm@19760
   247
  in
wenzelm@61261
   248
    Defs (Itemtab.join (join_specs context) (defs1, defs2)
wenzelm@61261
   249
      |> normalize context |> Itemtab.fold add_def defs2)
wenzelm@19760
   250
  end;
wenzelm@19613
   251
wenzelm@19613
   252
wenzelm@19613
   253
(* define *)
wenzelm@19590
   254
wenzelm@61261
   255
fun define context unchecked def description (c, args) deps (Defs defs) =
wenzelm@17707
   256
  let
wenzelm@55544
   257
    val pos = Position.thread_data ();
wenzelm@19697
   258
    val restr =
wenzelm@19697
   259
      if plain_args args orelse
wenzelm@61249
   260
        (case args of [Term.Type (_, rec_args)] => plain_args rec_args | _ => false)
wenzelm@33701
   261
      then [] else [(args, description)];
wenzelm@19692
   262
    val spec =
wenzelm@55544
   263
      (serial (), {def = def, description = description, pos = pos, lhs = args, rhs = deps});
wenzelm@61261
   264
    val defs' = defs |> update_specs context c spec;
wenzelm@61261
   265
  in Defs (defs' |> (if unchecked then I else dependencies context (c, args) restr deps)) end;
wenzelm@19697
   266
wenzelm@61260
   267
fun get_deps (Defs defs) c = reducts_of defs c;
wenzelm@61260
   268
wenzelm@19697
   269
end;