--- a/NEWS Sun Aug 01 16:40:48 2010 +0200
+++ b/NEWS Sun Aug 01 17:43:51 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 16:40:48 2010 +0200
+++ b/doc-src/IsarRef/Thy/Spec.thy Sun Aug 01 17:43:51 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 16:40:48 2010 +0200
+++ b/doc-src/IsarRef/Thy/document/Spec.tex Sun Aug 01 17:43:51 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 16:40:48 2010 +0200
+++ b/src/FOL/ex/Locale_Test/Locale_Test1.thy Sun Aug 01 17:43:51 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/HOL/IsaMakefile Sun Aug 01 16:40:48 2010 +0200
+++ b/src/HOL/IsaMakefile Sun Aug 01 17:43:51 2010 +0200
@@ -401,7 +401,8 @@
Library/AssocList.thy Library/BigO.thy Library/Binomial.thy \
Library/Bit.thy Library/Boolean_Algebra.thy Library/Cardinality.thy \
Library/Char_nat.thy Library/Code_Char.thy Library/Code_Char_chr.thy \
- Library/Code_Integer.thy Library/Code_Natural.thy \
+ Library/Code_Integer.thy Library/Code_Natural.thy \
+ Library/Code_Prolog.thy Tools/Predicate_Compile/code_prolog.ML \
Library/ContNotDenum.thy Library/Continuity.thy Library/Convex.thy \
Library/Countable.thy Library/Diagonalize.thy Library/Dlist.thy \
Library/Efficient_Nat.thy Library/Enum.thy Library/Eval_Witness.thy \
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/Code_Prolog.thy Sun Aug 01 17:43:51 2010 +0200
@@ -0,0 +1,13 @@
+(* Title: HOL/Library/Code_Prolog.thy
+ Author: Lukas Bulwahn, TUM 2010
+*)
+
+header {* Code generation of prolog programs *}
+
+theory Code_Prolog
+imports Main
+uses "~~/src/HOL/Tools/Predicate_Compile/code_prolog.ML"
+begin
+
+end
+
--- a/src/HOL/Library/HOL_Library_ROOT.ML Sun Aug 01 16:40:48 2010 +0200
+++ b/src/HOL/Library/HOL_Library_ROOT.ML Sun Aug 01 17:43:51 2010 +0200
@@ -2,4 +2,4 @@
(* Classical Higher-order Logic -- batteries included *)
use_thys ["Library", "List_Prefix", "List_lexord", "Sublist_Order",
- "Code_Char_chr", "Code_Integer", "Efficient_Nat", "Executable_Set"];
+ "Code_Char_chr", "Code_Integer", "Efficient_Nat", "Executable_Set", "Code_Prolog"];
--- a/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy Sun Aug 01 16:40:48 2010 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy Sun Aug 01 17:43:51 2010 +0200
@@ -1,6 +1,5 @@
theory Code_Prolog_Examples
-imports Predicate_Compile_Alternative_Defs
-uses "~~/src/HOL/Tools/Predicate_Compile/code_prolog.ML"
+imports Code_Prolog
begin
section {* Example append *}
@@ -12,6 +11,166 @@
code_pred append .
-values 3 "{((x::'b list), y, z). append x y z}"
+values 3 "{(x, y, z). append x y z}"
+
+
+section {* Example queens *}
+
+inductive nodiag :: "int => int => int list => bool"
+where
+ "nodiag B D []"
+| "D \<noteq> N - B ==> D \<noteq> B - N ==> Da = D + 1 ==> nodiag B Da L ==> nodiag B D (N # L)"
+
+text {*
+qdelete(A, [A|L], L).
+qdelete(X, [A|Z], [A|R]) :-
+ qdelete(X, Z, R).
+*}
+
+inductive qdelete :: "int => int list => int list => bool"
+where
+ "qdelete A (A # L) L"
+| "qdelete X Z R ==> qdelete X (A # Z) (A # R)"
+
+text {*
+qperm([], []).
+qperm([X|Y], K) :-
+ qdelete(U, [X|Y], Z),
+ K = [U|V],
+ qperm(Z, V).
+*}
+
+inductive qperm :: "int list => int list => bool"
+where
+ "qperm [] []"
+| "qdelete U (X # Y) Z ==> qperm Z V ==> qperm (X # Y) (U # V)"
+
+text {*
+safe([]).
+safe([N|L]) :-
+ nodiag(N, 1, L),
+ safe(L).
+*}
+
+inductive safe :: "int list => bool"
+where
+ "safe []"
+| "nodiag N 1 L ==> safe L ==> safe (N # L)"
+
+text {*
+queen(Data, Out) :-
+ qperm(Data, Out),
+ safe(Out)
+*}
+
+inductive queen :: "int list => int list => bool"
+where
+ "qperm Data Out ==> safe Out ==> queen Data Out"
+
+inductive queen_9
+where
+ "queen [1,2,3,4,5,6,7,8,9] ys ==> queen_9 ys"
+
+code_pred queen_9 .
+
+values 150 "{ys. queen_9 ys}"
+
+
+section {* Example symbolic derivation *}
+
+hide_const Plus Pow
+
+datatype expr = Log expr | Mult expr expr | Div expr expr | x | Num int | Plus expr expr
+ | Minus expr expr | Uminus expr | Pow expr int | Exp expr
+
+text {*
+
+d(U + V, X, DU + DV) :-
+ cut,
+ d(U, X, DU),
+ d(V, X, DV).
+d(U - V, X, DU - DV) :-
+ cut,
+ d(U, X, DU),
+ d(V, X, DV).
+d(U * V, X, DU * V + U * DV) :-
+ cut,
+ d(U, X, DU),
+ d(V, X, DV).
+d(U / V, X, (DU * V - U * DV) / ^(V, 2)) :-
+ cut,
+ d(U, X, DU),
+ d(V, X, DV).
+d(^(U, N), X, DU * num(N) * ^(U, N1)) :-
+ cut,
+ N1 is N - 1,
+ d(U, X, DU).
+d(-U, X, -DU) :-
+ cut,
+ d(U, X, DU).
+d(exp(U), X, exp(U) * DU) :-
+ cut,
+ d(U, X, DU).
+d(log(U), X, DU / U) :-
+ cut,
+ d(U, X, DU).
+d(x, X, num(1)) :-
+ cut.
+d(num(_), _, num(0)).
+
+*}
+
+inductive d :: "expr => expr => expr => bool"
+where
+ "d U X DU ==> d V X DV ==> d (Plus U V) X (Plus DU DV)"
+| "d U X DU ==> d V X DV ==> d (Minus U V) X (Minus DU DV)"
+| "d U X DU ==> d V X DV ==> d (Mult U V) X (Plus (Mult DU V) (Mult U DV))"
+| "d U X DU ==> d V X DV ==> d (Div U V) X (Div (Minus (Mult DU V) (Mult U DV)) (Pow V 2))"
+| "d U X DU ==> N1 = N - 1 ==> d (Pow U N) X (Mult DU (Mult (Num N) (Pow U N1)))"
+| "d U X DU ==> d (Uminus U) X (Uminus DU)"
+| "d U X DU ==> d (Exp U) X (Mult (Exp U) DU)"
+| "d U X DU ==> d (Log U) X (Div DU U)"
+| "d x X (Num 1)"
+| "d (Num n) X (Num 0)"
+
+text {*
+ops8(E) :-
+ d((x + num(1)) * ((^(x, 2) + num(2)) * (^(x, 3) + num(3))), x, E).
+
+divide10(E) :-
+ d(((((((((x / x) / x) / x) / x) / x) / x) / x) / x) / x, x, E).
+
+log10(E) :-
+ d(log(log(log(log(log(log(log(log(log(log(x)))))))))), x, E).
+
+times10(E) :-
+ d(((((((((x * x) * x) * x) * x) * x) * x) * x) * x) * x, x, E)
+*}
+
+inductive ops8 :: "expr => bool"
+where
+ "d (Mult (Plus x (Num 1)) (Mult (Plus (Pow x 2) (Num 2)) (Plus (Pow x 3) (Num 3)))) x e ==> ops8 e"
+
+inductive divide10
+where
+ "d (Div (Div (Div (Div (Div (Div (Div (Div (Div x x) x) x) x) x) x) x) x) x) x e ==> divide10 e"
+
+inductive log10
+where
+ "d (Log (Log (Log (Log (Log (Log (Log (Log (Log (Log x)))))))))) x e ==> log10 e"
+
+inductive times10
+where
+ "d (Mult (Mult (Mult (Mult (Mult (Mult (Mult (Mult (Mult x x) x) x) x) x) x) x) x) x) x e ==> times10 e"
+
+code_pred ops8 .
+code_pred divide10 .
+code_pred log10 .
+code_pred times10 .
+
+values "{e. ops8 e}"
+values "{e. divide10 e}"
+values "{e. log10 e}"
+values "{e. times10 e}"
end
--- a/src/HOL/Predicate_Compile_Examples/ROOT.ML Sun Aug 01 16:40:48 2010 +0200
+++ b/src/HOL/Predicate_Compile_Examples/ROOT.ML Sun Aug 01 17:43:51 2010 +0200
@@ -1,1 +1,2 @@
use_thys ["Predicate_Compile_Examples", "Predicate_Compile_Quickcheck_Examples", "Specialisation_Examples"];
+use_thys ["Code_Prolog_Examples"];
--- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML Sun Aug 01 16:40:48 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML Sun Aug 01 17:43:51 2010 +0200
@@ -6,9 +6,14 @@
signature CODE_PROLOG =
sig
- datatype prol_term = Var of string | Cons of string | AppF of string * prol_term list;
- datatype prem = Conj of prem list | NotRel of string * prol_term list
- | Rel of string * prol_term list | Eq of prol_term * prol_term | NotEq of prol_term * prol_term;
+ datatype arith_op = Plus | Minus
+ datatype prol_term = Var of string | Cons of string | AppF of string * prol_term list
+ | Number of int | ArithOp of arith_op * prol_term list;
+ datatype prem = Conj of prem list
+ | Rel of string * prol_term list | NotRel of string * prol_term list
+ | Eq of prol_term * prol_term | NotEq of prol_term * prol_term
+ | ArithEq of prol_term * prol_term | NotArithEq of prol_term * prol_term;
+
type clause = ((string * prol_term list) * prem);
type logic_program = clause list;
type constant_table = (string * string) list
@@ -35,15 +40,29 @@
(* internal program representation *)
-datatype prol_term = Var of string | Cons of string | AppF of string * prol_term list;
+datatype arith_op = Plus | Minus
+
+datatype prol_term = Var of string | Cons of string | AppF of string * prol_term list
+ | Number of int | ArithOp of arith_op * prol_term list;
+
+fun is_Var (Var _) = true
+ | is_Var _ = false
+
+fun is_arith_term (Var _) = true
+ | is_arith_term (Number _) = true
+ | is_arith_term (ArithOp (_, operands)) = forall is_arith_term operands
+ | is_arith_term _ = false
fun string_of_prol_term (Var s) = "Var " ^ s
| string_of_prol_term (Cons s) = "Cons " ^ s
| string_of_prol_term (AppF (f, args)) = f ^ "(" ^ commas (map string_of_prol_term args) ^ ")"
+ | string_of_prol_term (Number n) = "Number " ^ string_of_int n
-datatype prem = Conj of prem list | NotRel of string * prol_term list
- | Rel of string * prol_term list | Eq of prol_term * prol_term | NotEq of prol_term * prol_term;
-
+datatype prem = Conj of prem list
+ | Rel of string * prol_term list | NotRel of string * prol_term list
+ | Eq of prol_term * prol_term | NotEq of prol_term * prol_term
+ | ArithEq of prol_term * prol_term | NotArithEq of prol_term * prol_term;
+
fun dest_Rel (Rel (c, ts)) = (c, ts)
type clause = ((string * prol_term list) * prem);
@@ -80,33 +99,66 @@
(** translation of terms, literals, premises, and clauses **)
+fun translate_arith_const @{const_name "Groups.plus_class.plus"} = SOME Plus
+ | translate_arith_const @{const_name "Groups.minus_class.minus"} = SOME Minus
+ | translate_arith_const _ = NONE
+
fun translate_term ctxt constant_table t =
- case strip_comb t of
- (Free (v, T), []) => Var v
- | (Const (c, _), []) => Cons (translate_const constant_table c)
- | (Const (c, _), args) =>
- AppF (translate_const constant_table c, map (translate_term ctxt constant_table) args)
- | _ => error ("illegal term for translation: " ^ Syntax.string_of_term ctxt t)
+ case try HOLogic.dest_number t of
+ SOME (@{typ "int"}, n) => Number n
+ | NONE =>
+ (case strip_comb t of
+ (Free (v, T), []) => Var v
+ | (Const (c, _), []) => Cons (translate_const constant_table c)
+ | (Const (c, _), args) =>
+ (case translate_arith_const c of
+ SOME aop => ArithOp (aop, map (translate_term ctxt constant_table) args)
+ | NONE =>
+ AppF (translate_const constant_table c, map (translate_term ctxt constant_table) args))
+ | _ => error ("illegal term for translation: " ^ Syntax.string_of_term ctxt t))
fun translate_literal ctxt constant_table t =
case strip_comb t of
(Const (@{const_name "op ="}, _), [l, r]) =>
- Eq (pairself (translate_term ctxt constant_table) (l, r))
+ let
+ val l' = translate_term ctxt constant_table l
+ val r' = translate_term ctxt constant_table r
+ in
+ (if is_Var l' andalso is_arith_term r' then ArithEq else Eq) (l', r')
+ end
| (Const (c, _), args) =>
Rel (translate_const constant_table c, map (translate_term ctxt constant_table) args)
| _ => error ("illegal literal for translation: " ^ Syntax.string_of_term ctxt t)
fun NegRel_of (Rel lit) = NotRel lit
| NegRel_of (Eq eq) = NotEq eq
-
+ | NegRel_of (ArithEq eq) = NotArithEq eq
+
fun translate_prem ctxt constant_table t =
case try HOLogic.dest_not t of
SOME t => NegRel_of (translate_literal ctxt constant_table t)
| NONE => translate_literal ctxt constant_table t
+
+fun imp_prems_conv cv ct =
+ case Thm.term_of ct of
+ Const ("==>", _) $ _ $ _ => Conv.combination_conv (Conv.arg_conv cv) (imp_prems_conv cv) ct
+ | _ => Conv.all_conv ct
+
+fun Trueprop_conv cv ct =
+ case Thm.term_of ct of
+ Const ("Trueprop", _) $ _ => Conv.arg_conv cv ct
+ | _ => raise Fail "Trueprop_conv"
+
+fun preprocess_intro thy rule =
+ Conv.fconv_rule
+ (imp_prems_conv
+ (Trueprop_conv (Conv.try_conv (Conv.rewr_conv @{thm Predicate.eq_is_eq}))))
+ (Thm.transfer thy rule)
+
fun translate_intros ctxt gr const constant_table =
let
- val intros = Graph.get_node gr const
+ val intros = map (preprocess_intro (ProofContext.theory_of ctxt)) (Graph.get_node gr const)
val (intros', ctxt') = Variable.import_terms true (map prop_of intros) ctxt
val constant_table' = declare_consts (fold Term.add_const_names intros' []) constant_table
fun translate_intro intro =
@@ -158,9 +210,14 @@
(* code printer *)
+fun write_arith_op Plus = "+"
+ | write_arith_op Minus = "-"
+
fun write_term (Var v) = first_upper v
| write_term (Cons c) = c
- | write_term (AppF (f, args)) = f ^ "(" ^ space_implode ", " (map write_term args) ^ ")"
+ | write_term (AppF (f, args)) = f ^ "(" ^ space_implode ", " (map write_term args) ^ ")"
+ | write_term (ArithOp (oper, [a1, a2])) = write_term a1 ^ " " ^ write_arith_op oper ^ " " ^ write_term a2
+ | write_term (Number n) = string_of_int n
fun write_rel (pred, args) =
pred ^ "(" ^ space_implode ", " (map write_term args) ^ ")"
@@ -170,6 +227,8 @@
| write_prem (NotRel p) = "not(" ^ write_rel p ^ ")"
| write_prem (Eq (l, r)) = write_term l ^ " = " ^ write_term r
| write_prem (NotEq (l, r)) = write_term l ^ " \\= " ^ write_term r
+ | write_prem (ArithEq (l, r)) = write_term l ^ " is " ^ write_term r
+ | write_prem (NotArithEq (l, r)) = write_term l ^ " =\\= " ^ write_term r
fun write_clause (head, prem) =
write_rel head ^ (if prem = Conj [] then "." else " :- " ^ write_prem prem ^ ".")
@@ -200,6 +259,8 @@
"main :- halt(1).\n"
(* parsing prolog solution *)
+val scan_number =
+ Scan.many1 Symbol.is_ascii_digit
val scan_atom =
Scan.many1 (fn s => Symbol.is_ascii_lower s orelse Symbol.is_ascii_quasi s)
@@ -221,10 +282,13 @@
val is_var_ident =
forall (fn s => Symbol.is_ascii_upper s orelse Symbol.is_ascii_digit s orelse Symbol.is_ascii_quasi s)
+fun int_of_symbol_list xs = fold (fn x => fn s => s * 10 + (ord x - ord "0")) xs 0
+
fun scan_terms xs = (((scan_term --| $$ ",") ::: scan_terms)
|| (scan_term >> single)) xs
and scan_term xs =
- ((scan_var >> (Var o string_of))
+ ((scan_number >> (Number o int_of_symbol_list))
+ || (scan_var >> (Var o string_of))
|| ((scan_atom -- ($$ "(" |-- scan_terms --| $$ ")"))
>> (fn (f, ts) => AppF (string_of f, ts)))
|| (scan_atom >> (Cons o string_of))) xs
@@ -263,6 +327,8 @@
(* values command *)
fun restore_term ctxt constant_table (Var s, T) = Free (s, T)
+ | restore_term ctxt constant_table (Number n, @{typ "int"}) = HOLogic.mk_number @{typ "int"} n
+ | restore_term ctxt constant_table (Number n, _) = raise (Fail "unexpected type for number")
| restore_term ctxt constant_table (Cons s, T) = Const (restore_const constant_table s, T)
| restore_term ctxt constant_table (AppF (f, args), T) =
let
@@ -299,16 +365,31 @@
val _ = tracing "Running prolog program..."
val tss = run p (translate_const constant_table name) (map first_upper vnames) soln
val _ = tracing "Restoring terms..."
- fun mk_set_comprehension t =
- let
- val frees = Term.add_frees t []
- val uu as (uuN, uuT) = singleton (Variable.variant_frees ctxt [t]) ("uu", fastype_of t)
- in HOLogic.mk_Collect (uuN, uuT, fold (fn (s, T) => fn t => HOLogic.mk_exists (s, T, t))
- frees (HOLogic.mk_conj (HOLogic.mk_eq (Free uu, t), @{term "True"}))) end
- val set_comprs = map (fn ts =>
- mk_set_comprehension (HOLogic.mk_tuple (map (restore_term ctxt constant_table) (ts ~~ Ts)))) tss
+ val empty = Const("Orderings.bot_class.bot", fastype_of t_compr)
+ fun mk_insert x S =
+ Const (@{const_name "Set.insert"}, fastype_of x --> fastype_of S --> fastype_of S) $ x $ S
+ fun mk_set_compr in_insert [] xs =
+ rev ((Free ("...", fastype_of t_compr)) ::
+ (if null in_insert then xs else (fold mk_insert in_insert empty) :: xs))
+ | mk_set_compr in_insert (t :: ts) xs =
+ let
+ val frees = Term.add_frees t []
+ in
+ if null frees then
+ mk_set_compr (t :: in_insert) ts xs
+ else
+ let
+ val uu as (uuN, uuT) = singleton (Variable.variant_frees ctxt [t]) ("uu", fastype_of t)
+ val set_compr =
+ HOLogic.mk_Collect (uuN, uuT, fold (fn (s, T) => fn t => HOLogic.mk_exists (s, T, t))
+ frees (HOLogic.mk_conj (HOLogic.mk_eq (Free uu, t), @{term "True"})))
+ in
+ set_compr :: (if null in_insert then xs else (fold mk_insert in_insert empty) :: xs)
+ end
+ end
in
- foldl1 (HOLogic.mk_binop @{const_name sup}) (set_comprs @ [Free ("...", fastype_of t_compr)])
+ foldl1 (HOLogic.mk_binop @{const_name sup}) (mk_set_compr []
+ (map (fn ts => HOLogic.mk_tuple (map (restore_term ctxt constant_table) (ts ~~ Ts))) tss) [])
end
fun values_cmd print_modes soln raw_t state =
@@ -318,6 +399,7 @@
val t' = values ctxt soln t
val ty' = Term.type_of t'
val ctxt' = Variable.auto_fixes t' ctxt
+ val _ = tracing "Printing terms..."
val p = Print_Mode.with_modes print_modes (fn () =>
Pretty.block [Pretty.quote (Syntax.pretty_term ctxt' t'), Pretty.fbrk,
Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt' ty')]) ();
--- a/src/HOL/Tools/inductive.ML Sun Aug 01 16:40:48 2010 +0200
+++ b/src/HOL/Tools/inductive.ML Sun Aug 01 17:43:51 2010 +0200
@@ -548,15 +548,18 @@
fun mk_simp_eq ctxt prop =
let
- val (c, args) = strip_comb (HOLogic.dest_Trueprop prop)
val ctxt' = Variable.auto_fixes prop ctxt
- val cname = fst (dest_Const c)
+ val cname = fst (dest_Const (fst (strip_comb (HOLogic.dest_Trueprop prop))))
val info = the_inductive ctxt cname
val eq = nth (#eqs (snd info)) (find_index (fn c => c = cname) (#names (fst info)))
- val (_, args') = strip_comb (fst (HOLogic.dest_eq (HOLogic.dest_Trueprop (Thm.prop_of eq))))
+ val lhs_eq = fst (HOLogic.dest_eq (HOLogic.dest_Trueprop (Thm.prop_of eq)))
+ val subst = Pattern.match (ProofContext.theory_of ctxt) (lhs_eq, HOLogic.dest_Trueprop prop)
+ (Vartab.empty, Vartab.empty)
val certify = cterm_of (ProofContext.theory_of ctxt)
- in
- cterm_instantiate (map (pairself certify) (args' ~~ args)) eq
+ val inst = map (fn v => (certify (Var v), certify (Envir.subst_term subst (Var v))))
+ (Term.add_vars lhs_eq [])
+ in
+ cterm_instantiate inst eq
|> Conv.fconv_rule (Conv.arg_conv (Conv.arg_conv
(Simplifier.full_rewrite (simpset_of ctxt))))
|> singleton (Variable.export ctxt' ctxt)
--- a/src/Pure/Isar/class.ML Sun Aug 01 16:40:48 2010 +0200
+++ b/src/Pure/Isar/class.ML Sun Aug 01 17:43:51 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 16:40:48 2010 +0200
+++ b/src/Pure/Isar/class_target.ML Sun Aug 01 17:43:51 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 16:40:48 2010 +0200
+++ b/src/Pure/Isar/element.ML Sun Aug 01 17:43:51 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 16:40:48 2010 +0200
+++ b/src/Pure/Isar/expression.ML Sun Aug 01 17:43:51 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 16:40:48 2010 +0200
+++ b/src/Pure/Isar/isar_cmd.ML Sun Aug 01 17:43:51 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 16:40:48 2010 +0200
+++ b/src/Pure/Isar/isar_syn.ML Sun Aug 01 17:43:51 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 16:40:48 2010 +0200
+++ b/src/Pure/Isar/locale.ML Sun Aug 01 17:43:51 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 16:40:48 2010 +0200
+++ b/src/Tools/quickcheck.ML Sun Aug 01 17:43:51 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