author | ballarin |
Fri, 12 Dec 2008 12:31:00 +0100 | |
changeset 29211 | ab99da3854af |
parent 29210 | 4025459e3f83 |
permissions | -rw-r--r-- |
28873 | 1 |
(* Title: FOL/ex/NewLocaleSetup.thy |
2 |
Author: Clemens Ballarin, TU Muenchen |
|
3 |
||
4 |
Testing environment for locale expressions --- experimental. |
|
5 |
*) |
|
6 |
||
7 |
theory NewLocaleSetup |
|
8 |
imports FOL |
|
9 |
begin |
|
10 |
||
11 |
ML {* |
|
12 |
||
13 |
local |
|
14 |
||
15 |
structure P = OuterParse and K = OuterKeyword; |
|
16 |
val opt_bang = Scan.optional (P.$$$ "!" >> K true) false; |
|
17 |
||
18 |
val locale_val = |
|
29033
721529248e31
Enable keyword 'structure' in for clause of locale expression.
ballarin
parents:
29018
diff
changeset
|
19 |
SpecParse.locale_expression -- |
28873 | 20 |
Scan.optional (P.$$$ "+" |-- P.!!! (Scan.repeat1 SpecParse.context_element)) [] || |
28887 | 21 |
Scan.repeat1 SpecParse.context_element >> pair ([], []); |
28873 | 22 |
|
23 |
in |
|
24 |
||
25 |
val _ = |
|
26 |
OuterSyntax.command "locale" "define named proof context" K.thy_decl |
|
28887 | 27 |
(P.name -- Scan.optional (P.$$$ "=" |-- P.!!! locale_val) (([], []), []) -- P.opt_begin |
28873 | 28 |
>> (fn ((name, (expr, elems)), begin) => |
29 |
(begin ? Toplevel.print) o Toplevel.begin_local_theory begin |
|
29028
b5dad96c755a
When adding locales, delay notes until local theory is built.
ballarin
parents:
29018
diff
changeset
|
30 |
(Expression.add_locale_cmd name name expr elems #> |
b5dad96c755a
When adding locales, delay notes until local theory is built.
ballarin
parents:
29018
diff
changeset
|
31 |
(fn ((target, notes), ctxt) => TheoryTarget.begin target ctxt |> |
b5dad96c755a
When adding locales, delay notes until local theory is built.
ballarin
parents:
29018
diff
changeset
|
32 |
fold (fn (kind, facts) => LocalTheory.notes kind facts #> snd) notes)))); |
28873 | 33 |
|
34 |
val _ = |
|
35 |
OuterSyntax.improper_command "print_locales" "print locales of this theory" K.diag |
|
36 |
(Scan.succeed (Toplevel.no_timing o (Toplevel.unknown_theory o |
|
37 |
Toplevel.keep (NewLocale.print_locales o Toplevel.theory_of)))); |
|
38 |
||
39 |
val _ = OuterSyntax.improper_command "print_locale" "print named locale in this theory" K.diag |
|
40 |
(opt_bang -- P.xname >> (Toplevel.no_timing oo (fn (show_facts, name) => |
|
41 |
Toplevel.unknown_theory o Toplevel.keep (fn state => |
|
42 |
NewLocale.print_locale (Toplevel.theory_of state) show_facts name)))); |
|
43 |
||
28993
829e684b02ef
Interpretation in theories including interaction with subclass relation.
ballarin
parents:
28902
diff
changeset
|
44 |
val _ = |
829e684b02ef
Interpretation in theories including interaction with subclass relation.
ballarin
parents:
28902
diff
changeset
|
45 |
OuterSyntax.command "interpretation" |
29018 | 46 |
"prove interpretation of locale expression in theory" K.thy_goal |
29210
4025459e3f83
Interpretation in theories: first version with equations.
ballarin
parents:
29034
diff
changeset
|
47 |
(P.!!! SpecParse.locale_expression -- |
29211 | 48 |
Scan.optional (P.$$$ "where" |-- P.and_list1 (SpecParse.opt_thm_name ":" -- P.prop)) [] |
29210
4025459e3f83
Interpretation in theories: first version with equations.
ballarin
parents:
29034
diff
changeset
|
49 |
>> (fn (expr, mixin) => Toplevel.print o |
4025459e3f83
Interpretation in theories: first version with equations.
ballarin
parents:
29034
diff
changeset
|
50 |
Toplevel.theory_to_proof (Expression.interpretation_cmd expr mixin))); |
28993
829e684b02ef
Interpretation in theories including interaction with subclass relation.
ballarin
parents:
28902
diff
changeset
|
51 |
|
29018 | 52 |
val _ = |
53 |
OuterSyntax.command "interpret" |
|
54 |
"prove interpretation of locale expression in proof context" |
|
55 |
(K.tag_proof K.prf_goal) |
|
29033
721529248e31
Enable keyword 'structure' in for clause of locale expression.
ballarin
parents:
29018
diff
changeset
|
56 |
(P.!!! SpecParse.locale_expression |
29018 | 57 |
>> (fn expr => Toplevel.print o |
58 |
Toplevel.proof' (fn int => Expression.interpret_cmd expr int))); |
|
59 |
||
28873 | 60 |
end |
61 |
||
62 |
*} |
|
63 |
||
64 |
end |