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