1(*  Title:      Pure/theory.ML
2    Author:     Lawrence C Paulson and Markus Wenzel
3
4Logical theory content: axioms, definitions, and begin/end wrappers.
5*)
6
7signature THEORY =
8sig
9  val parents_of: theory -> theory list
10  val ancestors_of: theory -> theory list
11  val nodes_of: theory -> theory list
12  val setup: (theory -> theory) -> unit
13  val local_setup: (Proof.context -> Proof.context) -> unit
14  val install_pure: theory -> unit
15  val get_pure: unit -> theory
16  val get_pure_bootstrap: unit -> theory
17  val get_markup: theory -> Markup.T
18  val check: {long: bool} -> Proof.context -> string * Position.T -> theory
19  val axiom_table: theory -> term Name_Space.table
20  val axiom_space: theory -> Name_Space.T
21  val all_axioms_of: theory -> (string * term) list
22  val defs_of: theory -> Defs.T
23  val at_begin: (theory -> theory option) -> theory -> theory
24  val at_end: (theory -> theory option) -> theory -> theory
25  val join_theory: theory list -> theory
26  val begin_theory: string * Position.T -> theory list -> theory
27  val end_theory: theory -> theory
28  val add_axiom: Proof.context -> binding * term -> theory -> theory
29  val const_dep: theory -> string * typ -> Defs.entry
30  val type_dep: string * typ list -> Defs.entry
31  val add_deps: Defs.context -> string -> Defs.entry -> Defs.entry list -> theory -> theory
32  val add_deps_global: string -> Defs.entry -> Defs.entry list -> theory -> theory
33  val add_def: Defs.context -> bool -> bool -> binding * term -> theory -> theory
34  val specify_const: (binding * typ) * mixfix -> theory -> term * theory
35  val check_overloading: Proof.context -> bool -> string * typ -> unit
36end
37
38structure Theory: THEORY =
39struct
40
41
42(** theory context operations **)
43
44val parents_of = Context.parents_of;
45val ancestors_of = Context.ancestors_of;
46fun nodes_of thy = thy :: ancestors_of thy;
47
48fun setup f = Context.>> (Context.map_theory f);
49fun local_setup f = Context.>> (Context.map_proof f);
50
51
52(* implicit theory Pure *)
53
54val pure: theory Single_Assignment.var = Single_Assignment.var "pure";
55
56fun install_pure thy = Single_Assignment.assign pure thy;
57
58fun get_pure () =
59  (case Single_Assignment.peek pure of
60    SOME thy => thy
61  | NONE => raise Fail "Theory Pure not present");
62
63fun get_pure_bootstrap () =
64  (case Single_Assignment.peek pure of
65    SOME thy => thy
66  | NONE => Context.the_global_context ());
67
68
69
70(** datatype thy **)
71
72type wrapper = (theory -> theory option) * stamp;
73
74fun apply_wrappers (wrappers: wrapper list) =
75  perhaps (perhaps_loop (perhaps_apply (map fst wrappers)));
76
77datatype thy = Thy of
78 {pos: Position.T,
79  id: serial,
80  axioms: term Name_Space.table,
81  defs: Defs.T,
82  wrappers: wrapper list * wrapper list};
83
84fun make_thy (pos, id, axioms, defs, wrappers) =
85  Thy {pos = pos, id = id, axioms = axioms, defs = defs, wrappers = wrappers};
86
87structure Thy = Theory_Data'
88(
89  type T = thy;
90  val empty = make_thy (Position.none, 0, Name_Space.empty_table "axiom", Defs.empty, ([], []));
91
92  fun extend (Thy {pos = _, id = _, axioms, defs, wrappers}) =
93    make_thy (Position.none, 0, axioms, defs, wrappers);
94
95  fun merge old_thys (thy1, thy2) =
96    let
97      val Thy {pos = _, id = _, axioms = axioms1, defs = defs1, wrappers = (bgs1, ens1)} = thy1;
98      val Thy {pos = _, id = _, axioms = axioms2, defs = defs2, wrappers = (bgs2, ens2)} = thy2;
99
100      val axioms' = Name_Space.merge_tables (axioms1, axioms2);
101      val defs' = Defs.merge (Defs.global_context (fst old_thys)) (defs1, defs2);
102      val bgs' = Library.merge (eq_snd op =) (bgs1, bgs2);
103      val ens' = Library.merge (eq_snd op =) (ens1, ens2);
104    in make_thy (Position.none, 0, axioms', defs', (bgs', ens')) end;
105);
106
107fun rep_theory thy = Thy.get thy |> (fn Thy args => args);
108
109fun map_thy f = Thy.map (fn (Thy {pos, id, axioms, defs, wrappers}) =>
110  make_thy (f (pos, id, axioms, defs, wrappers)));
111
112fun map_axioms f =
113  map_thy (fn (pos, id, axioms, defs, wrappers) => (pos, id, f axioms, defs, wrappers));
114
115fun map_defs f =
116  map_thy (fn (pos, id, axioms, defs, wrappers) => (pos, id, axioms, f defs, wrappers));
117
118fun map_wrappers f =
119  map_thy (fn (pos, id, axioms, defs, wrappers) => (pos, id, axioms, defs, f wrappers));
120
121
122(* entity markup *)
123
124fun theory_markup def name id pos =
125  if id = 0 then Markup.empty
126  else
127    Markup.properties (Position.entity_properties_of def id pos)
128      (Markup.entity Markup.theoryN name);
129
130fun init_markup (name, pos) thy =
131  let
132    val id = serial ();
133    val _ = Position.report pos (theory_markup true name id pos);
134  in map_thy (fn (_, _, axioms, defs, wrappers) => (pos, id, axioms, defs, wrappers)) thy end;
135
136fun get_markup thy =
137  let val {pos, id, ...} = rep_theory thy
138  in theory_markup false (Context.theory_name thy) id pos end;
139
140fun check long ctxt (name, pos) =
141  let
142    val thy = Proof_Context.theory_of ctxt;
143    val thy' =
144      Context.get_theory long thy name
145        handle ERROR msg =>
146          let
147            val completion_report =
148              Completion.make_report (name, pos)
149                (fn completed =>
150                  map (Context.theory_name' long) (ancestors_of thy)
151                  |> filter (completed o Long_Name.base_name)
152                  |> sort_strings
153                  |> map (fn a => (a, (Markup.theoryN, a))));
154          in error (msg ^ Position.here pos ^ completion_report) end;
155    val _ = Context_Position.report ctxt pos (get_markup thy');
156  in thy' end;
157
158
159(* basic operations *)
160
161val axiom_table = #axioms o rep_theory;
162val axiom_space = Name_Space.space_of_table o axiom_table;
163
164val all_axioms_of = Name_Space.dest_table o axiom_table;
165
166val defs_of = #defs o rep_theory;
167
168
169(* join theory *)
170
171fun join_theory [] = raise List.Empty
172  | join_theory [thy] = thy
173  | join_theory thys = foldl1 Context.join_thys thys |> Sign.restore_naming (hd thys);
174
175
176(* begin/end theory *)
177
178val begin_wrappers = rev o #1 o #wrappers o rep_theory;
179val end_wrappers = rev o #2 o #wrappers o rep_theory;
180
181fun at_begin f = map_wrappers (apfst (cons (f, stamp ())));
182fun at_end f = map_wrappers (apsnd (cons (f, stamp ())));
183
184fun begin_theory (name, pos) imports =
185  if name = Context.PureN then
186    (case imports of
187      [thy] => init_markup (name, pos) thy
188    | _ => error "Bad bootstrapping of theory Pure")
189  else
190    let
191      val thy = Context.begin_thy name imports;
192      val wrappers = begin_wrappers thy;
193    in
194      thy
195      |> init_markup (name, pos)
196      |> Sign.local_path
197      |> Sign.theory_naming
198      |> apply_wrappers wrappers
199      |> tap (Syntax.force_syntax o Sign.syn_of)
200    end;
201
202fun end_theory thy =
203  thy
204  |> apply_wrappers (end_wrappers thy)
205  |> Sign.change_check
206  |> Context.finish_thy;
207
208
209
210(** primitive specifications **)
211
212(* raw axioms *)
213
214fun cert_axm ctxt (b, raw_tm) =
215  let
216    val thy = Proof_Context.theory_of ctxt;
217    val t = Sign.cert_prop thy raw_tm
218      handle TYPE (msg, _, _) => error msg
219        | TERM (msg, _) => error msg;
220    val _ = Term.no_dummy_patterns t handle TERM (msg, _) => error msg;
221
222    val bad_sorts =
223      rev ((fold_types o fold_atyps_sorts) (fn (_, []) => I | (T, _) => insert (op =) T) t []);
224    val _ = null bad_sorts orelse
225      error ("Illegal sort constraints in primitive specification: " ^
226        commas (map (Syntax.string_of_typ (Config.put show_sorts true ctxt)) bad_sorts));
227  in (b, Sign.no_vars ctxt t) end
228  handle ERROR msg => cat_error msg ("The error(s) above occurred in axiom " ^ Binding.print b);
229
230fun add_axiom ctxt raw_axm thy = thy |> map_axioms (fn axioms =>
231  let
232    val axm = apsnd Logic.varify_global (cert_axm ctxt raw_axm);
233    val context = ctxt
234      |> Sign.inherit_naming thy
235      |> Context_Position.set_visible_generic false;
236    val (_, axioms') = Name_Space.define context true axm axioms;
237  in axioms' end);
238
239
240(* dependencies *)
241
242fun const_dep thy (c, T) = ((Defs.Const, c), Sign.const_typargs thy (c, T));
243fun type_dep (c, args) = ((Defs.Type, c), args);
244
245fun dependencies (context as (ctxt, _)) unchecked def description lhs rhs =
246  let
247    fun prep (item, args) =
248      (case fold Term.add_tvarsT args [] of
249        [] => (item, map Logic.varifyT_global args)
250      | vs => raise TYPE ("Illegal schematic type variable(s)", map TVar vs, []));
251
252    val lhs_vars = fold Term.add_tfreesT (snd lhs) [];
253    val rhs_extras =
254      fold (fn (_, args) => args |> (fold o Term.fold_atyps) (fn TFree v =>
255        if member (op =) lhs_vars v then I else insert (op =) v)) rhs [];
256    val _ =
257      if null rhs_extras then ()
258      else error ("Specification depends on extra type variables: " ^
259        commas_quote (map (Syntax.string_of_typ ctxt o TFree) rhs_extras) ^
260        "\nThe error(s) above occurred in " ^ quote description);
261  in Defs.define context unchecked def description (prep lhs) (map prep rhs) end;
262
263fun cert_entry thy ((Defs.Const, c), args) =
264      Sign.cert_term thy (Const (c, Sign.const_instance thy (c, args)))
265      |> dest_Const |> const_dep thy
266  | cert_entry thy ((Defs.Type, c), args) =
267      Sign.certify_typ thy (Type (c, args)) |> dest_Type |> type_dep;
268
269fun add_deps context a raw_lhs raw_rhs thy =
270  let
271    val (lhs as ((_, lhs_name), _)) :: rhs = map (cert_entry thy) (raw_lhs :: raw_rhs);
272    val description = if a = "" then lhs_name ^ " axiom" else a;
273  in thy |> map_defs (dependencies context false NONE description lhs rhs) end;
274
275fun add_deps_global a x y thy =
276  add_deps (Defs.global_context thy) a x y thy;
277
278fun specify_const decl thy =
279  let val (t, thy') = Sign.declare_const_global decl thy;
280  in (t, add_deps_global "" (const_dep thy' (dest_Const t)) [] thy') end;
281
282
283(* overloading *)
284
285fun check_overloading ctxt overloaded (c, T) =
286  let
287    val thy = Proof_Context.theory_of ctxt;
288
289    val declT = Sign.the_const_constraint thy c
290      handle TYPE (msg, _, _) => error msg;
291    val T' = Logic.varifyT_global T;
292
293    fun message sorts txt =
294      [Pretty.block [Pretty.str "Specification of constant ",
295        Pretty.str c, Pretty.str " ::", Pretty.brk 1,
296        Pretty.quote (Syntax.pretty_typ (Config.put show_sorts sorts ctxt) T)],
297        Pretty.str txt] |> Pretty.chunks |> Pretty.string_of;
298  in
299    if Sign.typ_instance thy (declT, T') then ()
300    else if Type.raw_instance (declT, T') then
301      error (message true "imposes additional sort constraints on the constant declaration")
302    else if overloaded then ()
303    else
304      error (message false "is strictly less general than the declared type (overloading required)")
305  end;
306
307
308(* definitional axioms *)
309
310local
311
312fun check_def (context as (ctxt, _)) thy unchecked overloaded (b, tm) defs =
313  let
314    val name = Sign.full_name thy b;
315    val ((lhs, rhs), _, _) =
316      Primitive_Defs.dest_def ctxt
317        {check_head = Term.is_Const,
318         check_free_lhs = K true,
319         check_free_rhs = K false,
320         check_tfree = K false} tm
321      handle TERM (msg, _) => error msg;
322    val lhs_const = Term.dest_Const (Term.head_of lhs);
323
324    val rhs_consts =
325      fold_aterms (fn Const const => insert (op =) (const_dep thy const) | _ => I) rhs [];
326    val rhs_types =
327      (fold_types o fold_subtypes) (fn Type t => insert (op =) (type_dep t) | _ => I) rhs [];
328    val rhs_deps = rhs_consts @ rhs_types;
329
330    val _ = check_overloading ctxt overloaded lhs_const;
331  in defs |> dependencies context unchecked (SOME name) name (const_dep thy lhs_const) rhs_deps end
332  handle ERROR msg => cat_error msg (Pretty.string_of (Pretty.block
333   [Pretty.str ("The error(s) above occurred in definition " ^ Binding.print b ^ ":"),
334    Pretty.fbrk, Pretty.quote (Syntax.pretty_term ctxt tm)]));
335
336in
337
338fun add_def (context as (ctxt, _)) unchecked overloaded raw_axm thy =
339  let val axm = cert_axm ctxt raw_axm in
340    thy
341    |> map_defs (check_def context thy unchecked overloaded axm)
342    |> add_axiom ctxt axm
343  end;
344
345end;
346
347end;
348