src/Pure/defs.ML
author wenzelm
Mon Feb 23 14:50:30 2015 +0100 (2015-02-23)
changeset 59564 fdc03c8daacc
parent 59050 376446e98951
child 61246 077b88f9ec16
permissions -rw-r--r--
Goal.prove_multi is superseded by the fully general Goal.prove_common;
wenzelm@17707
     1
(*  Title:      Pure/defs.ML
wenzelm@17707
     2
    Author:     Makarius
obua@16108
     3
wenzelm@19692
     4
Global well-formedness checks for constant definitions.  Covers plain
wenzelm@19701
     5
definitions and simple sub-structural overloading.
obua@16108
     6
*)
obua@16108
     7
wenzelm@16877
     8
signature DEFS =
wenzelm@16877
     9
sig
wenzelm@42384
    10
  val pretty_const: Proof.context -> string * typ list -> Pretty.T
wenzelm@19701
    11
  val plain_args: typ list -> bool
wenzelm@17707
    12
  type T
wenzelm@33712
    13
  type spec =
wenzelm@55544
    14
   {def: string option,
wenzelm@55544
    15
    description: string,
wenzelm@55544
    16
    pos: Position.T,
wenzelm@55544
    17
    lhs: typ list,
wenzelm@55544
    18
    rhs: (string * typ list) list}
wenzelm@33712
    19
  val all_specifications_of: T -> (string * spec list) list
wenzelm@33712
    20
  val specifications_of: T -> string -> spec list
wenzelm@19697
    21
  val dest: T ->
wenzelm@19697
    22
   {restricts: ((string * typ list) * string) list,
wenzelm@19697
    23
    reducts: ((string * typ list) * (string * typ list) list) list}
wenzelm@19590
    24
  val empty: T
wenzelm@42389
    25
  val merge: Proof.context -> T * T -> T
wenzelm@42384
    26
  val define: Proof.context -> bool -> string option -> string ->
wenzelm@19727
    27
    string * typ list -> (string * typ list) list -> T -> T
obua@16108
    28
end
obua@16108
    29
wenzelm@17711
    30
structure Defs: DEFS =
wenzelm@17707
    31
struct
obua@16108
    32
wenzelm@19697
    33
(* type arguments *)
wenzelm@19613
    34
wenzelm@19697
    35
type args = typ list;
wenzelm@19697
    36
wenzelm@42384
    37
fun pretty_const ctxt (c, args) =
wenzelm@19613
    38
  let
wenzelm@19692
    39
    val prt_args =
wenzelm@19692
    40
      if null args then []
wenzelm@42384
    41
      else [Pretty.list "(" ")" (map (Syntax.pretty_typ ctxt o Logic.unvarifyT_global) args)];
wenzelm@19697
    42
  in Pretty.block (Pretty.str c :: prt_args) end;
wenzelm@19624
    43
wenzelm@19707
    44
fun plain_args args =
wenzelm@19707
    45
  forall Term.is_TVar args andalso not (has_duplicates (op =) args);
wenzelm@19707
    46
wenzelm@19697
    47
fun disjoint_args (Ts, Us) =
wenzelm@19697
    48
  not (Type.could_unifys (Ts, Us)) orelse
wenzelm@19697
    49
    ((Type.raw_unifys (Ts, map (Logic.incr_tvar (maxidx_of_typs Ts + 1)) Us) Vartab.empty; false)
wenzelm@19697
    50
      handle Type.TUNIFY => true);
wenzelm@19692
    51
wenzelm@19697
    52
fun match_args (Ts, Us) =
wenzelm@56050
    53
  if Type.could_matches (Ts, Us) then
wenzelm@56050
    54
    Option.map Envir.subst_type
wenzelm@56050
    55
      (SOME (Type.raw_matches (Ts, Us) Vartab.empty) handle Type.TYPE_MATCH => NONE)
wenzelm@56050
    56
  else NONE;
wenzelm@19692
    57
wenzelm@19692
    58
wenzelm@19692
    59
(* datatype defs *)
wenzelm@19692
    60
wenzelm@33701
    61
type spec =
wenzelm@55544
    62
 {def: string option,
wenzelm@55544
    63
  description: string,
wenzelm@55544
    64
  pos: Position.T,
wenzelm@55544
    65
  lhs: args,
wenzelm@55544
    66
  rhs: (string * args) list};
wenzelm@19697
    67
wenzelm@19692
    68
type def =
wenzelm@55544
    69
 {specs: spec Inttab.table,  (*source specifications*)
wenzelm@55544
    70
  restricts: (args * string) list,  (*global restrictions imposed by incomplete patterns*)
wenzelm@19712
    71
  reducts: (args * (string * args) list) list};  (*specifications as reduction system*)
wenzelm@19697
    72
wenzelm@19697
    73
fun make_def (specs, restricts, reducts) =
wenzelm@19697
    74
  {specs = specs, restricts = restricts, reducts = reducts}: def;
wenzelm@19692
    75
wenzelm@19697
    76
fun map_def c f =
wenzelm@19697
    77
  Symtab.default (c, make_def (Inttab.empty, [], [])) #>
wenzelm@19697
    78
  Symtab.map_entry c (fn {specs, restricts, reducts}: def =>
wenzelm@19697
    79
    make_def (f (specs, restricts, reducts)));
wenzelm@19692
    80
wenzelm@19692
    81
wenzelm@19692
    82
datatype T = Defs of def Symtab.table;
wenzelm@19692
    83
wenzelm@19712
    84
fun lookup_list which defs c =
wenzelm@19692
    85
  (case Symtab.lookup defs c of
wenzelm@19713
    86
    SOME (def: def) => which def
wenzelm@19692
    87
  | NONE => []);
wenzelm@19692
    88
wenzelm@32050
    89
fun all_specifications_of (Defs defs) =
wenzelm@32050
    90
  (map o apsnd) (map snd o Inttab.dest o #specs) (Symtab.dest defs);
wenzelm@32050
    91
haftmann@24199
    92
fun specifications_of (Defs defs) = lookup_list (map snd o Inttab.dest o #specs) defs;
wenzelm@32050
    93
wenzelm@19692
    94
val restricts_of = lookup_list #restricts;
wenzelm@19692
    95
val reducts_of = lookup_list #reducts;
wenzelm@19692
    96
wenzelm@19697
    97
fun dest (Defs defs) =
wenzelm@19697
    98
  let
wenzelm@19697
    99
    val restricts = Symtab.fold (fn (c, {restricts, ...}) =>
wenzelm@33701
   100
      fold (fn (args, description) => cons ((c, args), description)) restricts) defs [];
wenzelm@19697
   101
    val reducts = Symtab.fold (fn (c, {reducts, ...}) =>
wenzelm@19697
   102
      fold (fn (args, deps) => cons ((c, args), deps)) reducts) defs [];
wenzelm@19697
   103
  in {restricts = restricts, reducts = reducts} end;
wenzelm@19692
   104
wenzelm@19697
   105
val empty = Defs Symtab.empty;
wenzelm@19697
   106
wenzelm@19697
   107
wenzelm@19697
   108
(* specifications *)
wenzelm@19692
   109
wenzelm@55544
   110
fun disjoint_specs c (i, {description = a, pos = pos_a, lhs = Ts, ...}: spec) =
wenzelm@55544
   111
  Inttab.forall (fn (j, {description = b, pos = pos_b, lhs = Us, ...}: spec) =>
wenzelm@19697
   112
    i = j orelse disjoint_args (Ts, Us) orelse
wenzelm@55544
   113
      error ("Clash of specifications for constant " ^ quote c ^ ":\n" ^
wenzelm@55544
   114
        "  " ^ quote a ^ Position.here pos_a ^ "\n" ^
wenzelm@55544
   115
        "  " ^ quote b ^ Position.here pos_b));
wenzelm@19692
   116
wenzelm@19697
   117
fun join_specs c ({specs = specs1, restricts, reducts}, {specs = specs2, ...}: def) =
wenzelm@19697
   118
  let
wenzelm@19697
   119
    val specs' =
wenzelm@19697
   120
      Inttab.fold (fn spec2 => (disjoint_specs c spec2 specs1; Inttab.update spec2)) specs2 specs1;
wenzelm@19697
   121
  in make_def (specs', restricts, reducts) end;
wenzelm@19697
   122
wenzelm@19697
   123
fun update_specs c spec = map_def c (fn (specs, restricts, reducts) =>
wenzelm@19697
   124
  (disjoint_specs c spec specs; (Inttab.update spec specs, restricts, reducts)));
wenzelm@19697
   125
wenzelm@19697
   126
wenzelm@19701
   127
(* normalized dependencies: reduction with well-formedness check *)
wenzelm@19697
   128
wenzelm@19697
   129
local
wenzelm@19697
   130
wenzelm@19729
   131
val prt = Pretty.string_of oo pretty_const;
wenzelm@42384
   132
fun err ctxt (c, args) (d, Us) s1 s2 =
wenzelm@42384
   133
  error (s1 ^ " dependency of constant " ^ prt ctxt (c, args) ^ " -> " ^ prt ctxt (d, Us) ^ s2);
wenzelm@19729
   134
wenzelm@42384
   135
fun acyclic ctxt (c, args) (d, Us) =
wenzelm@19729
   136
  c <> d orelse
wenzelm@19729
   137
  is_none (match_args (args, Us)) orelse
wenzelm@42384
   138
  err ctxt (c, args) (d, Us) "Circular" "";
wenzelm@19729
   139
wenzelm@42384
   140
fun wellformed ctxt defs (c, args) (d, Us) =
wenzelm@57520
   141
  plain_args Us orelse
wenzelm@19729
   142
  (case find_first (fn (Ts, _) => not (disjoint_args (Ts, Us))) (restricts_of defs d) of
wenzelm@33701
   143
    SOME (Ts, description) =>
wenzelm@42384
   144
      err ctxt (c, args) (d, Us) "Malformed"
wenzelm@42384
   145
        ("\n(restriction " ^ prt ctxt (d, Ts) ^ " from " ^ quote description ^ ")")
wenzelm@19729
   146
  | NONE => true);
wenzelm@19692
   147
wenzelm@42384
   148
fun reduction ctxt defs const deps =
wenzelm@19692
   149
  let
wenzelm@19701
   150
    fun reduct Us (Ts, rhs) =
wenzelm@19701
   151
      (case match_args (Ts, Us) of
wenzelm@19701
   152
        NONE => NONE
wenzelm@19701
   153
      | SOME subst => SOME (map (apsnd (map subst)) rhs));
wenzelm@19701
   154
    fun reducts (d, Us) = get_first (reduct Us) (reducts_of defs d);
wenzelm@19701
   155
wenzelm@19701
   156
    val reds = map (`reducts) deps;
wenzelm@19701
   157
    val deps' =
wenzelm@19701
   158
      if forall (is_none o #1) reds then NONE
wenzelm@20668
   159
      else SOME (fold_rev
wenzelm@20668
   160
        (fn (NONE, dp) => insert (op =) dp | (SOME dps, _) => fold (insert (op =)) dps) reds []);
wenzelm@42384
   161
    val _ = forall (acyclic ctxt const) (the_default deps deps');
wenzelm@19697
   162
  in deps' end;
wenzelm@19692
   163
wenzelm@19760
   164
in
wenzelm@19760
   165
wenzelm@42384
   166
fun normalize ctxt =
wenzelm@19692
   167
  let
wenzelm@19701
   168
    fun norm_update (c, {reducts, ...}: def) (changed, defs) =
wenzelm@19701
   169
      let
wenzelm@19701
   170
        val reducts' = reducts |> map (fn (args, deps) =>
wenzelm@42384
   171
          (args, perhaps (reduction ctxt defs (c, args)) deps));
wenzelm@19697
   172
      in
wenzelm@19701
   173
        if reducts = reducts' then (changed, defs)
wenzelm@32785
   174
        else (true, defs |> map_def c (fn (specs, restricts, _) => (specs, restricts, reducts')))
wenzelm@19697
   175
      end;
wenzelm@19701
   176
    fun norm_all defs =
wenzelm@19701
   177
      (case Symtab.fold norm_update defs (false, defs) of
wenzelm@19701
   178
        (true, defs') => norm_all defs'
wenzelm@19701
   179
      | (false, _) => defs);
wenzelm@19729
   180
    fun check defs (c, {reducts, ...}: def) =
wenzelm@42384
   181
      reducts |> forall (fn (args, deps) => forall (wellformed ctxt defs (c, args)) deps);
wenzelm@19729
   182
  in norm_all #> (fn defs => tap (Symtab.forall (check defs)) defs) end;
wenzelm@19701
   183
wenzelm@42384
   184
fun dependencies ctxt (c, args) restr deps =
wenzelm@19712
   185
  map_def c (fn (specs, restricts, reducts) =>
wenzelm@19712
   186
    let
wenzelm@19712
   187
      val restricts' = Library.merge (op =) (restricts, restr);
wenzelm@19712
   188
      val reducts' = insert (op =) (args, deps) reducts;
wenzelm@19712
   189
    in (specs, restricts', reducts') end)
wenzelm@42384
   190
  #> normalize ctxt;
wenzelm@19697
   191
wenzelm@19697
   192
end;
wenzelm@19692
   193
wenzelm@19692
   194
wenzelm@19624
   195
(* merge *)
wenzelm@19624
   196
wenzelm@42389
   197
fun merge ctxt (Defs defs1, Defs defs2) =
wenzelm@19613
   198
  let
wenzelm@19697
   199
    fun add_deps (c, args) restr deps defs =
wenzelm@19692
   200
      if AList.defined (op =) (reducts_of defs c) args then defs
wenzelm@42384
   201
      else dependencies ctxt (c, args) restr deps defs;
wenzelm@19697
   202
    fun add_def (c, {restricts, reducts, ...}: def) =
wenzelm@19697
   203
      fold (fn (args, deps) => add_deps (c, args) restricts deps) reducts;
wenzelm@19760
   204
  in
wenzelm@19760
   205
    Defs (Symtab.join join_specs (defs1, defs2)
wenzelm@42384
   206
      |> normalize ctxt |> Symtab.fold add_def defs2)
wenzelm@19760
   207
  end;
wenzelm@19613
   208
wenzelm@19613
   209
wenzelm@19613
   210
(* define *)
wenzelm@19590
   211
wenzelm@42384
   212
fun define ctxt unchecked def description (c, args) deps (Defs defs) =
wenzelm@17707
   213
  let
wenzelm@55544
   214
    val pos = Position.thread_data ();
wenzelm@19697
   215
    val restr =
wenzelm@19697
   216
      if plain_args args orelse
wenzelm@32785
   217
        (case args of [Type (_, rec_args)] => plain_args rec_args | _ => false)
wenzelm@33701
   218
      then [] else [(args, description)];
wenzelm@19692
   219
    val spec =
wenzelm@55544
   220
      (serial (), {def = def, description = description, pos = pos, lhs = args, rhs = deps});
wenzelm@19697
   221
    val defs' = defs |> update_specs c spec;
wenzelm@42384
   222
  in Defs (defs' |> (if unchecked then I else dependencies ctxt (c, args) restr deps)) end;
wenzelm@19697
   223
wenzelm@19697
   224
end;