--- a/NEWS Sun Aug 01 10:15:44 2010 +0200
+++ b/NEWS Sun Aug 01 10:26:55 2010 +0200
@@ -20,6 +20,15 @@
files exclusively use the .ML extension. Minor INCOMPATIBILTY.
+*** Pure ***
+
+* Interpretation command 'interpret' accepts a list of equations like
+'interpretation' does.
+
+* Diagnostic command 'print_interps' prints interpretations in proofs
+in addition to interpretations in theories.
+
+
*** HOL ***
* code generator: export_code without explicit file declaration prints
--- a/doc-src/IsarRef/Thy/Spec.thy Sun Aug 01 10:15:44 2010 +0200
+++ b/doc-src/IsarRef/Thy/Spec.thy Sun Aug 01 10:26:55 2010 +0200
@@ -407,7 +407,7 @@
\item @{element "constrains"}~@{text "x :: \<tau>"} introduces a type
constraint @{text \<tau>} on the local parameter @{text x}. This
- element is deprecated. The type constaint should be introduced in
+ element is deprecated. The type constraint should be introduced in
the for clause or the relevant @{element "fixes"} element.
\item @{element "assumes"}~@{text "a: \<phi>\<^sub>1 \<dots> \<phi>\<^sub>n"}
@@ -501,7 +501,7 @@
;
'interpretation' localeepxr equations?
;
- 'interpret' localeexpr
+ 'interpret' localeexpr equations?
;
'print\_interps' nameref
;
@@ -560,14 +560,16 @@
interpretations dynamically participate in any facts added to
locales.
- \item @{command "interpret"}~@{text "expr"}
- interprets @{text expr} in the proof context and is otherwise
- similar to interpretation in theories.
+ \item @{command "interpret"}~@{text "expr \<WHERE> eqns"} interprets
+ @{text expr} in the proof context and is otherwise similar to
+ interpretation in theories. Note that rewrite rules given to
+ @{command "interpret"} should be explicitly universally quantified.
\item @{command "print_interps"}~@{text "locale"} lists all
- interpretations of @{text "locale"} in the current theory, including
- those due to a combination of an @{command "interpretation"} and
- one or several @{command "sublocale"} declarations.
+ interpretations of @{text "locale"} in the current theory or proof
+ context, including those due to a combination of a @{command
+ "interpretation"} or @{command "interpret"} and one or several
+ @{command "sublocale"} declarations.
\end{description}
@@ -581,7 +583,7 @@
\end{warn}
\begin{warn}
- An interpretation in a theory may subsume previous
+ An interpretation in a theory or proof context may subsume previous
interpretations. This happens if the same specification fragment
is interpreted twice and the instantiation of the second
interpretation is more general than the interpretation of the
--- a/doc-src/IsarRef/Thy/document/Spec.tex Sun Aug 01 10:15:44 2010 +0200
+++ b/doc-src/IsarRef/Thy/document/Spec.tex Sun Aug 01 10:26:55 2010 +0200
@@ -431,7 +431,7 @@
\item \hyperlink{element.constrains}{\mbox{\isa{\isakeyword{constrains}}}}~\isa{{\isachardoublequote}x\ {\isacharcolon}{\isacharcolon}\ {\isasymtau}{\isachardoublequote}} introduces a type
constraint \isa{{\isasymtau}} on the local parameter \isa{x}. This
- element is deprecated. The type constaint should be introduced in
+ element is deprecated. The type constraint should be introduced in
the for clause or the relevant \hyperlink{element.fixes}{\mbox{\isa{\isakeyword{fixes}}}} element.
\item \hyperlink{element.assumes}{\mbox{\isa{\isakeyword{assumes}}}}~\isa{{\isachardoublequote}a{\isacharcolon}\ {\isasymphi}\isactrlsub {\isadigit{1}}\ {\isasymdots}\ {\isasymphi}\isactrlsub n{\isachardoublequote}}
@@ -523,7 +523,7 @@
;
'interpretation' localeepxr equations?
;
- 'interpret' localeexpr
+ 'interpret' localeexpr equations?
;
'print\_interps' nameref
;
@@ -582,14 +582,15 @@
interpretations dynamically participate in any facts added to
locales.
- \item \hyperlink{command.interpret}{\mbox{\isa{\isacommand{interpret}}}}~\isa{{\isachardoublequote}expr{\isachardoublequote}}
- interprets \isa{expr} in the proof context and is otherwise
- similar to interpretation in theories.
+ \item \hyperlink{command.interpret}{\mbox{\isa{\isacommand{interpret}}}}~\isa{{\isachardoublequote}expr\ {\isasymWHERE}\ eqns{\isachardoublequote}} interprets
+ \isa{expr} in the proof context and is otherwise similar to
+ interpretation in theories. Note that rewrite rules given to
+ \hyperlink{command.interpret}{\mbox{\isa{\isacommand{interpret}}}} should be explicitly universally quantified.
\item \hyperlink{command.print-interps}{\mbox{\isa{\isacommand{print{\isacharunderscore}interps}}}}~\isa{{\isachardoublequote}locale{\isachardoublequote}} lists all
- interpretations of \isa{{\isachardoublequote}locale{\isachardoublequote}} in the current theory, including
- those due to a combination of an \hyperlink{command.interpretation}{\mbox{\isa{\isacommand{interpretation}}}} and
- one or several \hyperlink{command.sublocale}{\mbox{\isa{\isacommand{sublocale}}}} declarations.
+ interpretations of \isa{{\isachardoublequote}locale{\isachardoublequote}} in the current theory or proof
+ context, including those due to a combination of a \hyperlink{command.interpretation}{\mbox{\isa{\isacommand{interpretation}}}} or \hyperlink{command.interpret}{\mbox{\isa{\isacommand{interpret}}}} and one or several
+ \hyperlink{command.sublocale}{\mbox{\isa{\isacommand{sublocale}}}} declarations.
\end{description}
@@ -603,7 +604,7 @@
\end{warn}
\begin{warn}
- An interpretation in a theory may subsume previous
+ An interpretation in a theory or proof context may subsume previous
interpretations. This happens if the same specification fragment
is interpreted twice and the instantiation of the second
interpretation is more general than the interpretation of the
--- a/src/FOL/ex/Locale_Test/Locale_Test1.thy Sun Aug 01 10:15:44 2010 +0200
+++ b/src/FOL/ex/Locale_Test/Locale_Test1.thy Sun Aug 01 10:26:55 2010 +0200
@@ -714,4 +714,24 @@
thm local_free.lone [where ?zero = 0]
qed
+lemma True
+proof
+ {
+ fix pand and pnot and por
+ assume passoc: "!!x y z. pand(pand(x, y), z) <-> pand(x, pand(y, z))"
+ and pnotnot: "!!x. pnot(pnot(x)) <-> x"
+ and por_def: "!!x y. por(x, y) <-> pnot(pand(pnot(x), pnot(y)))"
+ interpret loc: logic_o pand pnot
+ where por_eq: "!!x y. logic_o.lor_o(pand, pnot, x, y) <-> por(x, y)" (* FIXME *)
+ proof -
+ show logic_o: "PROP logic_o(pand, pnot)" using passoc pnotnot by unfold_locales
+ fix x y
+ show "logic_o.lor_o(pand, pnot, x, y) <-> por(x, y)"
+ by (unfold logic_o.lor_o_def [OF logic_o]) (rule por_def [symmetric])
+ qed
+ print_interps logic_o
+ have "!!x y. por(x, y) <-> pnot(pand(pnot(x), pnot(y)))" by (rule loc.lor_o_def)
+ }
+qed
+
end
--- a/src/Pure/Isar/class.ML Sun Aug 01 10:15:44 2010 +0200
+++ b/src/Pure/Isar/class.ML Sun Aug 01 10:26:55 2010 +0200
@@ -293,8 +293,8 @@
|-> (fn (param_map, params, assm_axiom) =>
`(fn thy => calculate thy class sups base_sort param_map assm_axiom)
#-> (fn (base_morph, eq_morph, export_morph, axiom, assm_intro, of_class) =>
- Locale.add_registration (class, base_morph)
- (Option.map (rpair true) eq_morph) export_morph
+ Context.theory_map (Locale.add_registration (class, base_morph)
+ (Option.map (rpair true) eq_morph) export_morph)
#> register class sups params base_sort base_morph export_morph axiom assm_intro of_class))
|> Theory_Target.init (SOME class)
|> pair class
--- a/src/Pure/Isar/class_target.ML Sun Aug 01 10:15:44 2010 +0200
+++ b/src/Pure/Isar/class_target.ML Sun Aug 01 10:26:55 2010 +0200
@@ -205,8 +205,8 @@
fun activate_defs class thms thy = case Element.eq_morphism thy thms
of SOME eq_morph => fold (fn cls => fn thy =>
- Locale.amend_registration (cls, base_morphism thy cls)
- (eq_morph, true) (export_morphism thy cls) thy) (heritage thy [class]) thy
+ Context.theory_map (Locale.amend_registration (cls, base_morphism thy cls)
+ (eq_morph, true) (export_morphism thy cls)) thy) (heritage thy [class]) thy
| NONE => thy;
fun register_operation class (c, (t, some_def)) thy =
--- a/src/Pure/Isar/element.ML Sun Aug 01 10:15:44 2010 +0200
+++ b/src/Pure/Isar/element.ML Sun Aug 01 10:26:55 2010 +0200
@@ -40,6 +40,9 @@
term list list -> term list -> Proof.context -> Proof.state
val witness_local_proof: (witness list list -> Proof.state -> Proof.state) ->
string -> term list list -> Proof.context -> bool -> Proof.state -> Proof.state
+ val witness_local_proof_eqs: (witness list list -> thm list -> Proof.state -> Proof.state) ->
+ string -> term list list -> term list -> Proof.context -> bool -> Proof.state ->
+ Proof.state
val morph_witness: morphism -> witness -> witness
val conclude_witness: witness -> thm
val pretty_witness: Proof.context -> witness -> Pretty.T
@@ -57,6 +60,8 @@
(Attrib.binding * (thm list * Attrib.src list) list) list
val eq_morphism: theory -> thm list -> morphism option
val transfer_morphism: theory -> morphism
+ val generic_note_thmss: string -> (Attrib.binding * (thm list * Attrib.src list) list) list ->
+ Context.generic -> (string * thm list) list * Context.generic
val init: context_i -> Context.generic -> Context.generic
val activate_i: context_i -> Proof.context -> context_i * Proof.context
val activate: (typ, term, Facts.ref) ctxt -> Proof.context -> context_i * Proof.context
@@ -280,6 +285,10 @@
in after_qed ((map2 o map2) (curry Witness) wit_propss wits) eqs end;
in proof after_qed' propss #> refine_witness #> Seq.hd end;
+fun proof_local cmd goal_ctxt int after_qed' propss =
+ Proof.map_context (K goal_ctxt)
+ #> Proof.local_goal (Proof_Display.print_results int) (K I) ProofContext.bind_propp_i
+ cmd NONE after_qed' (map (pair Thm.empty_binding) propss);
in
fun witness_proof after_qed wit_propss =
@@ -289,12 +298,11 @@
val witness_proof_eqs = gen_witness_proof (Proof.theorem NONE);
fun witness_local_proof after_qed cmd wit_propss goal_ctxt int =
- gen_witness_proof (fn after_qed' => fn propss =>
- Proof.map_context (K goal_ctxt)
- #> Proof.local_goal (Proof_Display.print_results int) (K I) ProofContext.bind_propp_i
- cmd NONE after_qed' (map (pair Thm.empty_binding) propss))
+ gen_witness_proof (proof_local cmd goal_ctxt int)
(fn wits => fn _ => after_qed wits) wit_propss [];
+fun witness_local_proof_eqs after_qed cmd wit_propss eq_props goal_ctxt int =
+ gen_witness_proof (proof_local cmd goal_ctxt int) after_qed wit_propss eq_props;
end;
@@ -467,6 +475,15 @@
(* init *)
+fun generic_note_thmss kind facts context =
+ let
+ val facts' = Attrib.map_facts (Attrib.attribute_i (Context.theory_of context)) facts;
+ in
+ context |> Context.mapping_result
+ (PureThy.note_thmss kind facts')
+ (ProofContext.note_thmss kind facts')
+ end;
+
fun init (Fixes fixes) = Context.map_proof (ProofContext.add_fixes fixes #> #2)
| init (Constrains _) = I
| init (Assumes asms) = Context.map_proof (fn ctxt =>
@@ -486,13 +503,7 @@
|> fold Variable.auto_fixes (map #1 asms)
|> ProofContext.add_assms_i Local_Defs.def_export (map #2 asms);
in ctxt' end)
- | init (Notes (kind, facts)) = (fn context =>
- let
- val facts' = Attrib.map_facts (Attrib.attribute_i (Context.theory_of context)) facts;
- val context' = context |> Context.mapping
- (PureThy.note_thmss kind facts' #> #2)
- (ProofContext.note_thmss kind facts' #> #2);
- in context' end);
+ | init (Notes (kind, facts)) = generic_note_thmss kind facts #> #2;
(* activate *)
--- a/src/Pure/Isar/expression.ML Sun Aug 01 10:15:44 2010 +0200
+++ b/src/Pure/Isar/expression.ML Sun Aug 01 10:26:55 2010 +0200
@@ -43,8 +43,8 @@
val sublocale_cmd: string -> expression -> theory -> Proof.state
val interpretation: expression_i -> (Attrib.binding * term) list -> theory -> Proof.state
val interpretation_cmd: expression -> (Attrib.binding * string) list -> theory -> Proof.state
- val interpret: expression_i -> bool -> Proof.state -> Proof.state
- val interpret_cmd: expression -> bool -> Proof.state -> Proof.state
+ val interpret: expression_i -> (Attrib.binding * term) list -> bool -> Proof.state -> Proof.state
+ val interpret_cmd: expression -> (Attrib.binding * string) list -> bool -> Proof.state -> Proof.state
end;
structure Expression : EXPRESSION =
@@ -790,10 +790,29 @@
(*** Interpretation ***)
-(** Interpretation in theories **)
+(** Interpretation in theories and proof contexts **)
local
+fun note_eqns_register deps witss attrss eqns export export' context =
+ let
+ fun meta_rewrite context =
+ map (Local_Defs.meta_rewrite_rule (Context.proof_of context) #> Drule.abs_def) o
+ maps snd;
+ in
+ context
+ |> Element.generic_note_thmss Thm.lemmaK
+ (attrss ~~ map (fn eqn => [([Morphism.thm (export' $> export) eqn],[])]) eqns)
+ |-> (fn facts => `(fn context => meta_rewrite context facts))
+ |-> (fn eqns => fold (fn ((dep, morph), wits) =>
+ fn context =>
+ Locale.add_registration (dep, morph $> Element.satisfy_morphism
+ (map (Element.morph_witness export') wits))
+ (Element.eq_morphism (Context.theory_of context) eqns |>
+ Option.map (rpair true))
+ export context) (deps ~~ witss))
+ end;
+
fun gen_interpretation prep_expr parse_prop prep_attr
expression equations theory =
let
@@ -805,35 +824,42 @@
val goal_ctxt = fold Variable.auto_fixes eqns expr_ctxt;
val export' = Variable.export_morphism goal_ctxt expr_ctxt;
- fun note_eqns raw_eqns thy =
- let
- val eqns = map (Morphism.thm (export' $> export)) raw_eqns;
- val eqn_attrss = map2 (fn attrs => fn eqn =>
- ((apsnd o map) (Attrib.attribute_i thy) attrs, [([eqn], [])])) attrss eqns;
- fun meta_rewrite thy =
- map (Local_Defs.meta_rewrite_rule (ProofContext.init_global thy) #> Drule.abs_def) o
- maps snd;
- in
- thy
- |> PureThy.note_thmss Thm.lemmaK eqn_attrss
- |-> (fn facts => `(fn thy => meta_rewrite thy facts))
- end;
-
- fun after_qed witss eqns = ProofContext.theory (note_eqns eqns
- #-> (fn eqns => fold (fn ((dep, morph), wits) =>
- fn thy => Locale.add_registration (dep, morph $> Element.satisfy_morphism
- (map (Element.morph_witness export') wits))
- (Element.eq_morphism thy eqns |> Option.map (rpair true))
- export thy) (deps ~~ witss)));
+ fun after_qed witss eqns = (ProofContext.theory o Context.theory_map)
+ (note_eqns_register deps witss attrss eqns export export');
in Element.witness_proof_eqs after_qed propss eqns goal_ctxt end;
+fun gen_interpret prep_expr parse_prop prep_attr
+ expression equations int state =
+ let
+ val _ = Proof.assert_forward_or_chain state;
+ val ctxt = Proof.context_of state;
+ val theory = ProofContext.theory_of ctxt;
+
+ val ((propss, deps, export), expr_ctxt) = prep_expr expression ctxt;
+
+ val eqns = map (parse_prop expr_ctxt o snd) equations |> Syntax.check_terms expr_ctxt;
+ val attrss = map ((apsnd o map) (prep_attr theory) o fst) equations;
+ val goal_ctxt = fold Variable.auto_fixes eqns expr_ctxt;
+ val export' = Variable.export_morphism goal_ctxt expr_ctxt;
+
+ fun after_qed witss eqns = (Proof.map_context o Context.proof_map)
+ (note_eqns_register deps witss attrss eqns export export');
+ in
+ state
+ |> Element.witness_local_proof_eqs after_qed "interpret" propss eqns goal_ctxt int
+ end;
+
in
fun interpretation x = gen_interpretation cert_goal_expression (K I) (K I) x;
fun interpretation_cmd x = gen_interpretation read_goal_expression
Syntax.parse_prop Attrib.intern_src x;
+fun interpret x = gen_interpret cert_goal_expression (K I) (K I) x;
+fun interpret_cmd x = gen_interpret read_goal_expression
+ Syntax.parse_prop Attrib.intern_src x;
+
end;
@@ -858,36 +884,5 @@
end;
-
-(** Interpretation in proof contexts **)
-
-local
-
-fun gen_interpret prep_expr expression int state =
- let
- val _ = Proof.assert_forward_or_chain state;
- val ctxt = Proof.context_of state;
-
- val ((propss, regs, export), goal_ctxt) = prep_expr expression ctxt;
-
- fun store_reg (name, morph) thms =
- let
- val morph' = morph $> Element.satisfy_morphism thms $> export;
- in Context.proof_map (Locale.activate_facts (name, morph')) end;
-
- fun after_qed wits =
- Proof.map_context (fold2 store_reg regs wits);
- in
- state
- |> Element.witness_local_proof after_qed "interpret" propss goal_ctxt int
- end;
-
-in
-
-fun interpret x = gen_interpret cert_goal_expression x;
-fun interpret_cmd x = gen_interpret read_goal_expression x;
-
end;
-end;
-
--- a/src/Pure/Isar/isar_cmd.ML Sun Aug 01 10:15:44 2010 +0200
+++ b/src/Pure/Isar/isar_cmd.ML Sun Aug 01 10:26:55 2010 +0200
@@ -365,7 +365,7 @@
fun print_registrations name = Toplevel.unknown_context o
Toplevel.keep (fn state =>
- Locale.print_registrations (Toplevel.theory_of state) name);
+ Locale.print_registrations (Toplevel.context_of state) name);
val print_attributes = Toplevel.unknown_theory o
Toplevel.keep (Attrib.print_attributes o Toplevel.theory_of);
--- a/src/Pure/Isar/isar_syn.ML Sun Aug 01 10:15:44 2010 +0200
+++ b/src/Pure/Isar/isar_syn.ML Sun Aug 01 10:26:55 2010 +0200
@@ -444,8 +444,10 @@
Outer_Syntax.command "interpret"
"prove interpretation of locale expression in proof context"
(Keyword.tag_proof Keyword.prf_goal)
- (Parse.!!! (Parse_Spec.locale_expression true)
- >> (fn expr => Toplevel.print o Toplevel.proof' (Expression.interpret_cmd expr)));
+ (Parse.!!! (Parse_Spec.locale_expression true) --
+ Scan.optional (Parse.where_ |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":" -- Parse.prop)) []
+ >> (fn (expr, equations) => Toplevel.print o
+ Toplevel.proof' (Expression.interpret_cmd expr equations)));
(* classes *)
--- a/src/Pure/Isar/locale.ML Sun Aug 01 10:15:44 2010 +0200
+++ b/src/Pure/Isar/locale.ML Sun Aug 01 10:26:55 2010 +0200
@@ -67,17 +67,17 @@
(* Registrations and dependencies *)
val add_registration: string * morphism -> (morphism * bool) option ->
- morphism -> theory -> theory
+ morphism -> Context.generic -> Context.generic
val amend_registration: string * morphism -> morphism * bool ->
- morphism -> theory -> theory
- val get_registrations: theory -> string -> morphism list
+ morphism -> Context.generic -> Context.generic
+ val registrations_of: Context.generic -> string -> (string * morphism) list
val add_dependency: string -> string * morphism -> morphism -> theory -> theory
(* Diagnostic *)
val all_locales: theory -> string list
val print_locales: theory -> unit
val print_locale: theory -> bool -> xstring -> unit
- val print_registrations: theory -> string -> unit
+ val print_registrations: Proof.context -> string -> unit
val locale_deps: theory ->
{ params: ((string * typ) * mixfix) list, axioms: term list, registrations: term list list } Graph.T
* term list list Symtab.table Symtab.table
@@ -349,7 +349,7 @@
structure Idtab = Table(type key = string * term list val ord = ident_ord);
-structure Registrations = Theory_Data
+structure Registrations = Generic_Data
(
type T = ((morphism * morphism) * serial) Idtab.table *
(* registrations, indexed by locale name and instance;
@@ -391,9 +391,10 @@
(* registration to be amended identified by its serial id *)
Registrations.map (apsnd (Inttab.map_default (serial', []) (cons (mixin, serial ()))));
-fun get_mixins thy (name, morph) =
+fun get_mixins context (name, morph) =
let
- val (regs, mixins) = Registrations.get thy;
+ val thy = Context.theory_of context;
+ val (regs, mixins) = Registrations.get context;
in
case Idtab.lookup regs (name, instance_of thy name morph) of
NONE => []
@@ -403,32 +404,35 @@
fun compose_mixins mixins =
fold_rev Morphism.compose (map (fst o fst) mixins) Morphism.identity;
-fun collect_mixins thy (name, morph) =
- roundup thy (fn dep => fn mixins => merge (eq_snd op =) (mixins, get_mixins thy dep))
- Morphism.identity (name, morph) ([(name, instance_of thy name morph)], [])
- |> snd |> filter (snd o fst) (* only inheritable mixins *)
- |> (fn x => merge (eq_snd op =) (x, get_mixins thy (name, morph)))
- |> compose_mixins;
+fun collect_mixins context (name, morph) =
+ let
+ val thy = Context.theory_of context;
+ in
+ roundup thy (fn dep => fn mixins => merge (eq_snd op =) (mixins, get_mixins context dep))
+ Morphism.identity (name, morph) ([(name, instance_of thy name morph)], [])
+ |> snd |> filter (snd o fst) (* only inheritable mixins *)
+ |> (fn x => merge (eq_snd op =) (x, get_mixins context (name, morph)))
+ |> compose_mixins
+ end;
-fun gen_get_registrations thy select = Registrations.get thy
+fun get_registrations context select = Registrations.get context
|>> Idtab.dest |>> select
(* with inherited mixins *)
|-> (fn regs => fn _ => map (fn ((name, _), ((base, export) ,_)) =>
- (name, base $> (collect_mixins thy (name, base $> export)) $> export)) regs);
+ (name, base $> (collect_mixins context (name, base $> export)) $> export)) regs);
-fun registrations_for_locale thy name =
- gen_get_registrations thy (filter (curry (op =) name o fst o fst));
+fun registrations_of context name =
+ get_registrations context (filter (curry (op =) name o fst o fst));
-val get_registrations = map snd oo registrations_for_locale;
+fun all_registrations context = get_registrations context I;
-fun all_registrations thy = gen_get_registrations thy I;
-
-fun activate_notes' activ_elem transfer thy export (name, morph) input =
+fun activate_notes' activ_elem transfer context export (name, morph) input =
let
+ val thy = Context.theory_of context;
val {notes, ...} = the_locale thy name;
fun activate ((kind, facts), _) input =
let
- val mixin = collect_mixins thy (name, morph $> export);
+ val mixin = collect_mixins context (name, morph $> export);
val facts' = facts |> Element.facts_map (Element.morph_ctxt (transfer input $> morph $> mixin $> export))
in activ_elem (Notes (kind, facts')) input end;
in
@@ -438,15 +442,16 @@
fun activate_facts' export dep context =
let
val thy = Context.theory_of context;
- val activate = activate_notes' Element.init (Element.transfer_morphism o Context.theory_of) thy export;
+ val activate = activate_notes' Element.init (Element.transfer_morphism o Context.theory_of) context export;
in roundup thy activate export dep (get_idents context, context) |-> put_idents end;
(* Add and extend registrations *)
-fun amend_registration (name, morph) mixin export thy =
+fun amend_registration (name, morph) mixin export context =
let
- val regs = Registrations.get thy |> fst;
+ val thy = Context.theory_of context;
+ val regs = Registrations.get context |> fst;
val base = instance_of thy name (morph $> export);
in
case Idtab.lookup regs (name, base) of
@@ -454,23 +459,24 @@
quote (extern thy name) ^ " and\nparameter instantiation " ^
space_implode " " (map (quote o Syntax.string_of_term_global thy) base) ^
" available")
- | SOME (_, serial') => add_mixin serial' mixin thy
+ | SOME (_, serial') => add_mixin serial' mixin context
end;
(* Note that a registration that would be subsumed by an existing one will not be
generated, and it will not be possible to amend it. *)
-fun add_registration (name, base_morph) mixin export thy =
+fun add_registration (name, base_morph) mixin export context =
let
+ val thy = Context.theory_of context;
val mix = case mixin of NONE => Morphism.identity
| SOME (mix, _) => mix;
val morph = base_morph $> mix;
val inst = instance_of thy name morph;
in
- if member (ident_le thy) (get_idents (Context.Theory thy)) (name, inst)
- then thy
+ if member (ident_le thy) (get_idents context) (name, inst)
+ then context
else
- (get_idents (Context.Theory thy), thy)
+ (get_idents context, context)
(* add new registrations with inherited mixins *)
|> roundup thy (add_reg thy export) export (name, morph)
|> snd
@@ -478,7 +484,7 @@
|> (case mixin of NONE => I
| SOME mixin => amend_registration (name, morph) mixin export)
(* activate import hierarchy as far as not already active *)
- |> Context.theory_map (activate_facts' export (name, morph))
+ |> activate_facts' export (name, morph)
end;
@@ -487,11 +493,12 @@
fun add_dependency loc (name, morph) export thy =
let
val thy' = (change_locale loc o apsnd) (cons ((name, (morph, export)), serial ())) thy;
+ val context' = Context.Theory thy';
val (_, regs) = fold_rev (roundup thy' cons export)
- (all_registrations thy') (get_idents (Context.Theory thy'), []);
+ (all_registrations context') (get_idents (context'), []);
in
thy'
- |> fold_rev (fn dep => add_registration dep NONE export) regs
+ |> fold_rev (fn dep => Context.theory_map (add_registration dep NONE export)) regs
end;
@@ -511,7 +518,7 @@
val args'' = snd args' |> Element.facts_map (Element.morph_ctxt morph) |>
Attrib.map_facts (Attrib.attribute_i thy)
in PureThy.note_thmss kind args'' #> snd end)
- (registrations_for_locale thy loc) thy))
+ (registrations_of (Context.Theory thy) loc) thy))
in ctxt'' end;
@@ -593,11 +600,15 @@
|> Pretty.writeln
end;
-fun print_registrations thy raw_name =
- (case registrations_for_locale thy (intern thy raw_name) of
- [] => Pretty.str ("no interpretations")
- | regs => Pretty.big_list "interpretations:" (map (pretty_reg thy) (rev regs)))
- |> Pretty.writeln;
+fun print_registrations ctxt raw_name =
+ let
+ val thy = ProofContext.theory_of ctxt;
+ in
+ (case registrations_of (Context.Proof ctxt) (* FIXME *) (intern thy raw_name) of
+ [] => Pretty.str ("no interpretations")
+ | regs => Pretty.big_list "interpretations:" (map (pretty_reg thy) (rev regs)))
+ |> Pretty.writeln
+ end;
fun locale_deps thy =
let
@@ -607,7 +618,7 @@
val params = params_of thy name;
val axioms = (these o Option.map (Logic.strip_imp_prems o Thm.prop_of) o fst o intros_of thy) name;
val registrations = map (instance_of thy name o snd)
- (registrations_for_locale thy name);
+ (registrations_of (Context.Theory thy) name);
in
Graph.new_node (name, { params = params, axioms = axioms, registrations = registrations })
end;
--- a/src/Tools/quickcheck.ML Sun Aug 01 10:15:44 2010 +0200
+++ b/src/Tools/quickcheck.ML Sun Aug 01 10:26:55 2010 +0200
@@ -228,7 +228,7 @@
val proto_goal = Logic.list_implies (map Thm.term_of assms, subst_bounds (frees, strip gi));
val check_goals = case some_locale
of NONE => [proto_goal]
- | SOME locale => map (fn phi => Morphism.term phi proto_goal) (Locale.get_registrations thy locale);
+ | SOME locale => map (fn (_, phi) => Morphism.term phi proto_goal) (Locale.registrations_of (Context.Theory thy) (*FIXME*) locale);
val inst_goals = maps (fn check_goal => map (fn T =>
Term ((Object_Logic.atomize_term thy o monomorphic_term thy insts T) check_goal)
handle WELLSORTED s => Wellsorted_Error s) default_Ts) check_goals