--- a/NEWS Wed Apr 13 09:48:41 2005 +0200
+++ b/NEWS Wed Apr 13 18:34:22 2005 +0200
@@ -6,13 +6,13 @@
*** General ***
-* The type Library.option is no more, along with the exception
+* ML: The type Library.option is no more, along with the exception
Library.OPTION: Isabelle now uses the standard option type. The
functions the, is_some, is_none, etc. are still in Library, but
the constructors are now SOME and NONE instead of Some and None.
- They throw the exception Option.
-
-* The exception LIST is no more, the standard exceptions Empty and
+ They raise the exception Option.
+
+* ML: The exception LIST is no more, the standard exceptions Empty and
Subscript, as well as Library.UnequalLengths are used instead. This
means that function like Library.hd and Library.tl are gone, as the
standard hd and tl functions suffice.
@@ -42,12 +42,6 @@
A simple solution to broken code is to include "open Library" at the
beginning of a structure. Everything after that will be as before.
-* Document preparation: new antiquotations @{lhs thm} and @{rhs thm}
- printing the lhs/rhs of definitions, equations, inequations etc.
-
-* isatool usedir: new option -f that allows specification of the ML
- file to be used by Isabelle; default is ROOT.ML.
-
* Theory headers: the new header syntax for Isar theories is
theory <name>
@@ -145,76 +139,11 @@
internally, to allow for use in a context of fixed variables.
* Pure/Simplifier: Command "find_rewrites" takes a string and lists all
- equality theorems (not just those with attribute simp!) whose left-hand
+ equality theorems (not just those declared as simp!) whose left-hand
side matches the term given via the string. In PG the command can be
activated via Isabelle -> Show me -> matching rewrites.
-* Provers: Simplifier and Classical Reasoner now support proof context
- dependent plug-ins (simprocs, solvers, wrappers etc.). These extra
- components are stored in the theory and patched into the
- simpset/claset when used in an Isar proof context. Context
- dependent components are maintained by the following theory
- operations:
-
- Simplifier.add_context_simprocs
- Simplifier.del_context_simprocs
- Simplifier.set_context_subgoaler
- Simplifier.reset_context_subgoaler
- Simplifier.add_context_looper
- Simplifier.del_context_looper
- Simplifier.add_context_unsafe_solver
- Simplifier.add_context_safe_solver
-
- Classical.add_context_safe_wrapper
- Classical.del_context_safe_wrapper
- Classical.add_context_unsafe_wrapper
- Classical.del_context_unsafe_wrapper
-
- IMPORTANT NOTE: proof tools (methods etc.) need to use
- local_simpset_of and local_claset_of to instead of the primitive
- Simplifier.get_local_simpset and Classical.get_local_claset,
- respectively, in order to see the context dependent fields!
-
-* Document preparation: antiquotations now provide the option
- 'locale=NAME' to specify an alternative context used for evaluating
- and printing the subsequent argument, as in @{thm [locale=LC]
- fold_commute}, for example.
-
-* Document preparation: commands 'display_drafts' and 'print_drafts'
- perform simple output of raw sources. Only those symbols that do
- not require additional LaTeX packages (depending on comments in
- isabellesym.sty) are displayed properly, everything else is left
- verbatim. We use isatool display and isatool print as front ends;
- these are subject to the DVI_VIEWER and PRINT_COMMAND settings,
- respectively.
-
-* Document preparation: Proof scripts as well as some other commands
- such as ML or parse/print_translation can now be hidden in the document.
- Hiding is enabled by default, and can be disabled either via the option
- '-H false' of isatool usedir or by resetting the reference variable
- IsarOutput.hide_commands. Additional commands to be hidden may be
- declared using IsarOutput.add_hidden_commands.
-
-* ML: output via the Isabelle channels of writeln/warning/error
- etc. is now passed through Output.output, with a hook for arbitrary
- transformations depending on the print_mode (cf. Output.add_mode --
- the first active mode that provides a output function wins).
- Already formatted output may be embedded into further text via
- Output.raw; the result of Pretty.string_of/str_of and derived
- functions (string_of_term/cterm/thm etc.) is already marked raw to
- accommodate easy composition of diagnostic messages etc.
- Programmers rarely need to care about Output.output or Output.raw at
- all, with some notable exceptions: Output.output is required when
- bypassing the standard channels (writeln etc.), or in token
- translations to produce properly formatted results; Output.raw is
- required when capturing already output material that will eventually
- be presented to the user a second time. For the default print mode,
- both Output.output and Output.raw have no effect.
-
-
-*** Isar ***
-
-* Debugging: new reference Toplevel.debug; default false.
+* Isar debugging: new reference Toplevel.debug; default false.
Set to make printing of exceptions THM, TERM, TYPE and THEORY more verbose.
* Locales:
@@ -232,12 +161,33 @@
in duplicate.
Use print_interps to inspect active interpretations of a particular locale.
-* New syntax
-
- <theorem_name> (<index>, ..., <index>-<index>, ...)
-
- for referring to specific theorems in a named list of theorems via
- indices.
+* Isar: new syntax 'name(i-j, i-, i, ...)' for referring to specific
+ selections of theorems in named facts via indices.
+
+
+*** Document preparation ***
+
+* New antiquotations @{lhs thm} and @{rhs thm} printing the lhs/rhs of
+ definitions, equations, inequations etc.
+
+* Antiquotations now provide the option 'locale=NAME' to specify an
+ alternative context used for evaluating and printing the subsequent
+ argument, as in @{thm [locale=LC] fold_commute}, for example.
+
+* Commands 'display_drafts' and 'print_drafts' perform simple output
+ of raw sources. Only those symbols that do not require additional
+ LaTeX packages (depending on comments in isabellesym.sty) are
+ displayed properly, everything else is left verbatim. We use
+ isatool display and isatool print as front ends; these are subject
+ to the DVI/PDF_VIEWER and PRINT_COMMAND settings, respectively.
+
+* Proof scripts as well as some other commands such as ML or
+ parse/print_translation can now be hidden in the document. Hiding
+ is enabled by default, and can be disabled either via the option '-H
+ false' of isatool usedir or by resetting the reference variable
+ IsarOutput.hide_commands. Additional commands to be hidden may be
+ declared using IsarOutput.add_hidden_commands.
+
*** HOL ***
@@ -337,9 +287,6 @@
enabled/disabled by the reference use_let_simproc. Potential
INCOMPATIBILITY since simplification is more powerful by default.
-* HOL: new 'isatool dimacs2hol' to convert files in DIMACS CNF format
- (containing Boolean satisfiability problems) into Isabelle/HOL theories.
-
*** HOLCF ***
@@ -359,6 +306,64 @@
the old version is still required for ML proof scripts.
+*** System ***
+
+* HOL: isatool dimacs2hol converts files in DIMACS CNF format
+ (containing Boolean satisfiability problems) into Isabelle/HOL
+ theories.
+
+* isatool usedir: option -f allows specification of the ML file to be
+ used by Isabelle; default is ROOT.ML.
+
+* ISABELLE_DOC_FORMAT setting specifies preferred document format (for
+ isatool doc, isatool mkdir, display_drafts etc.).
+
+
+*** ML ***
+
+* Pure: output via the Isabelle channels of writeln/warning/error
+ etc. is now passed through Output.output, with a hook for arbitrary
+ transformations depending on the print_mode (cf. Output.add_mode --
+ the first active mode that provides a output function wins).
+ Already formatted output may be embedded into further text via
+ Output.raw; the result of Pretty.string_of/str_of and derived
+ functions (string_of_term/cterm/thm etc.) is already marked raw to
+ accommodate easy composition of diagnostic messages etc.
+ Programmers rarely need to care about Output.output or Output.raw at
+ all, with some notable exceptions: Output.output is required when
+ bypassing the standard channels (writeln etc.), or in token
+ translations to produce properly formatted results; Output.raw is
+ required when capturing already output material that will eventually
+ be presented to the user a second time. For the default print mode,
+ both Output.output and Output.raw have no effect.
+
+* Provers: Simplifier and Classical Reasoner now support proof context
+ dependent plug-ins (simprocs, solvers, wrappers etc.). These extra
+ components are stored in the theory and patched into the
+ simpset/claset when used in an Isar proof context. Context
+ dependent components are maintained by the following theory
+ operations:
+
+ Simplifier.add_context_simprocs
+ Simplifier.del_context_simprocs
+ Simplifier.set_context_subgoaler
+ Simplifier.reset_context_subgoaler
+ Simplifier.add_context_looper
+ Simplifier.del_context_looper
+ Simplifier.add_context_unsafe_solver
+ Simplifier.add_context_safe_solver
+
+ Classical.add_context_safe_wrapper
+ Classical.del_context_safe_wrapper
+ Classical.add_context_unsafe_wrapper
+ Classical.del_context_unsafe_wrapper
+
+ IMPORTANT NOTE: proof tools (methods etc.) need to use
+ local_simpset_of and local_claset_of to instead of the primitive
+ Simplifier.get_local_simpset and Classical.get_local_claset,
+ respectively, in order to see the context dependent fields!
+
+
New in Isabelle2004 (April 2004)
--------------------------------
--- a/etc/isar-keywords.el Wed Apr 13 09:48:41 2005 +0200
+++ b/etc/isar-keywords.el Wed Apr 13 18:34:22 2005 +0200
@@ -7,7 +7,6 @@
(defconst isar-keywords-major
'("\\."
- "\\.\\."
"ML"
"ML_command"
"ML_setup"
@@ -19,6 +18,7 @@
"ProofGeneral\\.restart"
"ProofGeneral\\.try_context_thy_only"
"ProofGeneral\\.undo"
+ "\\.\\."
"also"
"apply"
"apply_end"
@@ -90,6 +90,7 @@
"method_setup"
"moreover"
"next"
+ "no_syntax"
"nonterminals"
"note"
"obtain"
@@ -362,6 +363,7 @@
"local"
"locale"
"method_setup"
+ "no_syntax"
"nonterminals"
"oracle"
"parse_ast_translation"
--- a/etc/settings Wed Apr 13 09:48:41 2005 +0200
+++ b/etc/settings Wed Apr 13 18:34:22 2005 +0200
@@ -145,6 +145,9 @@
#Where to look for docs (multiple dirs separated by ':').
ISABELLE_DOCS="$ISABELLE_HOME/doc"
+#Preferred document format
+ISABELLE_DOC_FORMAT=pdf
+
#The dvi file viewer
DVI_VIEWER=xdvi
#DVI_VIEWER="xdvi -geometry 498x704 -expert -s 5"
--- a/lib/Tools/display Wed Apr 13 09:48:41 2005 +0200
+++ b/lib/Tools/display Wed Apr 13 18:34:22 2005 +0200
@@ -28,21 +28,6 @@
}
-function view()
-{
- if [ "${1%%.dvi}.dvi" == "$1" ]; then
- exec $DVI_VIEWER "$1"
- return
- fi
-
- if [ "${1%%.pdf}.pdf" == "$1" ]; then
- exec $PDF_VIEWER "$1"
- return
- fi
-
- fail "Unknown file type: $FILE";
-}
-
## process command line
# options
@@ -75,11 +60,22 @@
[ -f "$FILE" ] || fail "Bad file: $FILE"
+case "$FILE" in
+ *.dvi)
+ VIEWER="$DVI_VIEWER"
+ ;;
+ *.pdf)
+ VIEWER="$PDF_VIEWER"
+ ;;
+ *)
+ fail "Unknown file type: $FILE";
+esac
+
if [ -n "$CLEAN" ]; then
- PRIVATE_FILE="$ISABELLE_TMP/"$(basename "$FILE")
- mv "$FILE" "$PRIVATE_FILE" ##|| fail "Cannot move file: $FILE"
- view "$PRIVATE_FILE"
+ PRIVATE_FILE="$ISABELLE_TMP/$$"$(basename "$FILE")
+ mv "$FILE" "$PRIVATE_FILE" || fail "Cannot move file: $FILE"
+ $VIEWER "$PRIVATE_FILE"
rm -f "$PRIVATE_FILE"
else
- view "$FILE"
+ exec $VIEWER "$FILE"
fi
--- a/lib/Tools/doc Wed Apr 13 09:48:41 2005 +0200
+++ b/lib/Tools/doc Wed Apr 13 18:34:22 2005 +0200
@@ -40,6 +40,7 @@
IFS=":"
for DIR in $ISABELLE_DOCS
do
+ [ -d "$DIR" ] || fail "Bad document directory: $DIR"
[ -f "$DIR/Contents" ] && grep -v "^>>" "$DIR/Contents"
done
IFS="$ORIG_IFS"
@@ -48,7 +49,12 @@
IFS=":"
for DIR in $ISABELLE_DOCS
do
- [ -f "$DIR/$DOC.dvi" ] && { cd "$DIR"; IFS="$ORIG_IFS"; exec $DVI_VIEWER "$DOC.dvi"; }
+ IFS="$ORIG_IFS"
+ [ -d "$DIR" ] || fail "Bad document directory: $DIR"
+ for FMT in "$ISABELLE_DOC_FORMAT" dvi
+ do
+ [ -f "$DIR/$DOC.$FMT" ] && { cd "$DIR"; exec "$ISATOOL" display "$DOC.$FMT"; }
+ done
done
IFS="$ORIG_IFS"
fail "Unknown Isabelle document: $DOC"
--- a/lib/Tools/mkdir Wed Apr 13 09:48:41 2005 +0200
+++ b/lib/Tools/mkdir Wed Apr 13 18:34:22 2005 +0200
@@ -137,7 +137,7 @@
echo "OUT = \$(ISABELLE_OUTPUT)"
echo "LOG = \$(OUT)/log"
echo
- echo "USEDIR = \$(ISATOOL) usedir ${VERBOSE}-i true -d pdf ## -D generated"
+ echo "USEDIR = \$(ISATOOL) usedir ${VERBOSE}-i true -d $ISABELLE_DOC_FORMAT ## -D generated"
echo
echo
echo "## $NAME"
--- a/src/HOL/Import/import_package.ML Wed Apr 13 09:48:41 2005 +0200
+++ b/src/HOL/Import/import_package.ML Wed Apr 13 18:34:22 2005 +0200
@@ -5,7 +5,7 @@
signature IMPORT_PACKAGE =
sig
- val import_meth: Args.src -> Proof.context -> Proof.method
+ val import_meth: Method.src -> Proof.context -> Proof.method
val setup : (theory -> theory) list
val debug : bool ref
end
--- a/src/HOL/Tools/datatype_package.ML Wed Apr 13 09:48:41 2005 +0200
+++ b/src/HOL/Tools/datatype_package.ML Wed Apr 13 18:34:22 2005 +0200
@@ -51,8 +51,8 @@
induction : thm,
size : thm list,
simps : thm list}
- val rep_datatype : string list option -> (thmref * Args.src list) list list ->
- (thmref * Args.src list) list list -> thmref * Args.src list -> theory -> theory *
+ val rep_datatype : string list option -> (thmref * Attrib.src list) list list ->
+ (thmref * Attrib.src list) list list -> thmref * Attrib.src list -> theory -> theory *
{distinct : thm list list,
inject : thm list list,
exhaustion : thm list,
@@ -244,7 +244,8 @@
val rule_spec = Scan.lift (Args.$$$ "rule" -- Args.$$$ ":");
val opt_rule = Scan.option (rule_spec |-- Attrib.local_thm);
-val varss = Args.and_list (Scan.repeat (Scan.unless rule_spec (Scan.lift Args.name_dummy)));
+val varss =
+ Args.and_list (Scan.repeat (Scan.unless rule_spec (Scan.lift (Args.maybe Args.name))));
val inst_tac = Method.bires_inst_tac false;
--- a/src/HOL/Tools/inductive_package.ML Wed Apr 13 09:48:41 2005 +0200
+++ b/src/HOL/Tools/inductive_package.ML Wed Apr 13 18:34:22 2005 +0200
@@ -44,14 +44,14 @@
val inductive_forall_name: string
val inductive_forall_def: thm
val rulify: thm -> thm
- val inductive_cases: ((bstring * Args.src list) * string list) list -> theory -> theory
+ val inductive_cases: ((bstring * Attrib.src list) * string list) list -> theory -> theory
val inductive_cases_i: ((bstring * theory attribute list) * term list) list -> theory -> theory
val add_inductive_i: bool -> bool -> bstring -> bool -> bool -> bool -> term list ->
((bstring * term) * theory attribute list) list -> thm list -> theory -> theory *
{defs: thm list, elims: thm list, raw_induct: thm, induct: thm,
intrs: thm list, mk_cases: string -> thm, mono: thm, unfold: thm}
val add_inductive: bool -> bool -> string list ->
- ((bstring * string) * Args.src list) list -> (thmref * Args.src list) list ->
+ ((bstring * string) * Attrib.src list) list -> (thmref * Attrib.src list) list ->
theory -> theory *
{defs: thm list, elims: thm list, raw_induct: thm, induct: thm,
intrs: thm list, mk_cases: string -> thm, mono: thm, unfold: thm}
--- a/src/HOL/Tools/inductive_realizer.ML Wed Apr 13 09:48:41 2005 +0200
+++ b/src/HOL/Tools/inductive_realizer.ML Wed Apr 13 18:34:22 2005 +0200
@@ -466,13 +466,14 @@
in
(add_ind_realizers (hd sets) (case arg of
NONE => sets | SOME NONE => []
- | SOME (SOME sets') => sets \\ map (Sign.intern_const (sign_of thy)) sets')
+ | SOME (SOME sets') => sets \\ sets')
thy, thm)
end;
-val rlz_attrib_global = Attrib.syntax (Scan.lift
- (Scan.option (Args.$$$ "irrelevant" |--
- Scan.option (Args.colon |-- Scan.repeat1 Args.name))) >> rlz_attrib);
+val rlz_attrib_global = Attrib.syntax
+ ((Scan.option (Scan.lift (Args.$$$ "irrelevant") |--
+ Scan.option (Scan.lift (Args.colon) |--
+ Scan.repeat1 Args.global_const))) >> rlz_attrib);
val setup = [Attrib.add_attributes [("ind_realizer",
(rlz_attrib_global, K Attrib.undef_local_attribute),
--- a/src/HOL/Tools/primrec_package.ML Wed Apr 13 09:48:41 2005 +0200
+++ b/src/HOL/Tools/primrec_package.ML Wed Apr 13 18:34:22 2005 +0200
@@ -8,7 +8,7 @@
signature PRIMREC_PACKAGE =
sig
val quiet_mode: bool ref
- val add_primrec: string -> ((bstring * string) * Args.src list) list
+ val add_primrec: string -> ((bstring * string) * Attrib.src list) list
-> theory -> theory * thm list
val add_primrec_i: string -> ((bstring * term) * theory attribute list) list
-> theory -> theory * thm list
--- a/src/HOL/Tools/recdef_package.ML Wed Apr 13 09:48:41 2005 +0200
+++ b/src/HOL/Tools/recdef_package.ML Wed Apr 13 18:34:22 2005 +0200
@@ -23,19 +23,19 @@
val cong_del_local: Proof.context attribute
val wf_add_local: Proof.context attribute
val wf_del_local: Proof.context attribute
- val add_recdef: bool -> xstring -> string -> ((bstring * string) * Args.src list) list ->
- Args.src option -> theory -> theory
+ val add_recdef: bool -> xstring -> string -> ((bstring * string) * Attrib.src list) list ->
+ Attrib.src option -> theory -> theory
* {simps: thm list, rules: thm list list, induct: thm, tcs: term list}
val add_recdef_i: bool -> xstring -> term -> ((bstring * term) * theory attribute list) list ->
theory -> theory * {simps: thm list, rules: thm list list, induct: thm, tcs: term list}
- val add_recdef_old: xstring -> string -> ((bstring * string) * Args.src list) list ->
+ val add_recdef_old: xstring -> string -> ((bstring * string) * Attrib.src list) list ->
simpset * thm list -> theory ->
theory * {simps: thm list, rules: thm list list, induct: thm, tcs: term list}
- val defer_recdef: xstring -> string list -> (thmref * Args.src list) list
+ val defer_recdef: xstring -> string list -> (thmref * Attrib.src list) list
-> theory -> theory * {induct_rules: thm}
val defer_recdef_i: xstring -> term list -> (thm list * theory attribute list) list
-> theory -> theory * {induct_rules: thm}
- val recdef_tc: bstring * Args.src list -> xstring -> int option
+ val recdef_tc: bstring * Attrib.src list -> xstring -> int option
-> bool -> theory -> ProofHistory.T
val recdef_tc_i: bstring * theory attribute list -> string -> int option
-> bool -> theory -> ProofHistory.T
--- a/src/Provers/classical.ML Wed Apr 13 09:48:41 2005 +0200
+++ b/src/Provers/classical.ML Wed Apr 13 18:34:22 2005 +0200
@@ -168,8 +168,8 @@
val cla_modifiers: (Args.T list -> (Method.modifier * Args.T list)) list
val cla_meth: (claset -> tactic) -> thm list -> Proof.context -> Proof.method
val cla_meth': (claset -> int -> tactic) -> thm list -> Proof.context -> Proof.method
- val cla_method: (claset -> tactic) -> Args.src -> Proof.context -> Proof.method
- val cla_method': (claset -> int -> tactic) -> Args.src -> Proof.context -> Proof.method
+ val cla_method: (claset -> tactic) -> Method.src -> Proof.context -> Proof.method
+ val cla_method': (claset -> int -> tactic) -> Method.src -> Proof.context -> Proof.method
val setup: (theory -> theory) list
val get_delta_claset: ProofContext.context -> claset
--- a/src/Provers/induct_method.ML Wed Apr 13 09:48:41 2005 +0200
+++ b/src/Provers/induct_method.ML Wed Apr 13 18:34:22 2005 +0200
@@ -326,20 +326,14 @@
local
-fun check k get name =
- (case get name of SOME x => x
- | NONE => error ("No rule for " ^ k ^ " " ^ quote name));
-
-fun spec k = (Args.$$$ k -- Args.colon) |-- Args.!!! Args.name;
+fun named_rule k arg get =
+ Scan.lift (Args.$$$ k -- Args.colon) |-- arg :-- (fn name => Scan.peek (fn ctxt =>
+ (case get ctxt name of SOME x => Scan.succeed x
+ | NONE => error ("No rule for " ^ k ^ " " ^ quote name)))) >> #2;
fun rule get_type get_set =
- Scan.depend (fn ctxt =>
- let val sg = ProofContext.sign_of ctxt in
- spec InductAttrib.typeN >> (check InductAttrib.typeN (get_type ctxt) o
- Sign.certify_tyname sg o Sign.intern_tycon sg) ||
- spec InductAttrib.setN >> (check InductAttrib.setN (get_set ctxt) o
- Sign.certify_const sg o Sign.intern_const sg)
- end >> pair ctxt) ||
+ named_rule InductAttrib.typeN Args.local_tyname get_type ||
+ named_rule InductAttrib.setN Args.local_const get_set ||
Scan.lift (Args.$$$ ruleN -- Args.colon) |-- Attrib.local_thm;
val cases_rule = rule InductAttrib.lookup_casesT InductAttrib.lookup_casesS;
--- a/src/Pure/Isar/ROOT.ML Wed Apr 13 09:48:41 2005 +0200
+++ b/src/Pure/Isar/ROOT.ML Wed Apr 13 18:34:22 2005 +0200
@@ -13,11 +13,11 @@
use "proof_data.ML";
use "delta_data.ML"; (*for delta_{claset,simpset}, part of SPASS interface*)
use "context_rules.ML";
+use "args.ML";
+use "attrib.ML";
use "locale.ML";
use "proof.ML";
use "proof_history.ML";
-use "args.ML";
-use "attrib.ML";
use "net_rules.ML";
use "induct_attrib.ML";
use "method.ML";
@@ -54,13 +54,16 @@
struct
structure ObjectLogic = ObjectLogic;
structure AutoBind = AutoBind;
+ structure RuleCases = RuleCases;
structure ProofContext = ProofContext;
+ structure ContextRules = ContextRules;
+ structure Args = Args;
+ structure Attrib = Attrib;
structure Locale = Locale;
structure Proof = Proof;
structure ProofHistory = ProofHistory;
- structure Args = Args;
- structure Attrib = Attrib;
- structure ContextRules = ContextRules;
+ structure NetRules = NetRules;
+ structure InductAttrib = InductAttrib;
structure Method = Method;
structure Calculation = Calculation;
structure Obtain = Obtain;
--- a/src/Pure/Isar/args.ML Wed Apr 13 09:48:41 2005 +0200
+++ b/src/Pure/Isar/args.ML Wed Apr 13 18:34:22 2005 +0200
@@ -2,21 +2,35 @@
ID: $Id$
Author: Markus Wenzel, TU Muenchen
-Concrete argument syntax (of attributes and methods).
+Concrete argument syntax of attributes, methods etc. -- with special
+support for embedded values and static binding.
*)
signature ARGS =
sig
+ datatype value = Name of string | Typ of typ | Term of term | Fact of thm list |
+ Attribute of theory attribute * ProofContext.context attribute
type T
- val val_of: T -> string
- val pos_of: T -> Position.T
- val str_of: T -> string
val string_of: T -> string
- val ident: string * Position.T -> T
- val string: string * Position.T -> T
- val keyword: string * Position.T -> T
+ val mk_ident: string * Position.T -> T
+ val mk_string: string * Position.T -> T
+ val mk_keyword: string * Position.T -> T
+ val mk_name: string -> T
+ val mk_typ: typ -> T
+ val mk_term: term -> T
+ val mk_fact: thm list -> T
+ val mk_attribute: theory attribute * ProofContext.context attribute -> T
val stopper: T * (T -> bool)
val not_eof: T -> bool
+ type src
+ val src: (string * T list) * Position.T -> src
+ val dest_src: src -> (string * T list) * Position.T
+ val map_name: (string -> string) -> src -> src
+ val map_values: (string -> string) -> (typ -> typ) -> (term -> term) -> (thm -> thm)
+ -> src -> src
+ val assignable: src -> src
+ val assign: value option -> T -> unit
+ val closure: src -> src
val position: (T list -> 'a * 'b) -> T list -> ('a * Position.T) * 'b
val !!! : (T list -> 'a) -> T list -> 'a
val $$$ : string -> T list -> string * T list
@@ -30,15 +44,28 @@
val parens: (T list -> 'a * T list) -> T list -> 'a * T list
val bracks: (T list -> 'a * T list) -> T list -> 'a * T list
val mode: string -> 'a * T list -> bool * ('a * T list)
+ val maybe: (T list -> 'a * T list) -> T list -> 'a option * T list
val name: T list -> string * T list
- val name_dummy: T list -> string option * T list
val nat: T list -> int * T list
val int: T list -> int * T list
val var: T list -> indexname * T list
+ val list: (T list -> 'a * T list) -> T list -> 'a list * T list
+ val list1: (T list -> 'a * T list) -> T list -> 'a list * T list
val enum: string -> ('a * T list -> 'b * ('a * T list)) -> 'a * T list -> 'b list * ('a * T list)
val enum1: string -> ('a * T list -> 'b * ('a * T list)) -> 'a * T list -> 'b list * ('a * T list)
val and_list: ('a * T list -> 'b * ('a * T list)) -> 'a * T list -> 'b list * ('a * T list)
val and_list1: ('a * T list -> 'b * ('a * T list)) -> 'a * T list -> 'b list * ('a * T list)
+ val ahead: T list -> T * T list
+ val internal_name: T list -> string * T list
+ val internal_typ: T list -> typ * T list
+ val internal_term: T list -> term * T list
+ val internal_fact: T list -> thm list * T list
+ val internal_attribute: T list ->
+ (theory attribute * ProofContext.context attribute) * T list
+ val named_name: (string -> string) -> T list -> string * T list
+ val named_typ: (string -> typ) -> T list -> typ * T list
+ val named_term: (string -> term) -> T list -> term * T list
+ val named_fact: (string -> thm list) -> T list -> thm list * T list
val global_typ_raw: theory * T list -> typ * (theory * T list)
val global_typ: theory * T list -> typ * (theory * T list)
val global_term: theory * T list -> term * (theory * T list)
@@ -47,15 +74,19 @@
val local_typ: ProofContext.context * T list -> typ * (ProofContext.context * T list)
val local_term: ProofContext.context * T list -> term * (ProofContext.context * T list)
val local_prop: ProofContext.context * T list -> term * (ProofContext.context * T list)
+ val global_tyname: theory * T list -> string * (theory * T list)
+ val global_const: theory * T list -> string * (theory * T list)
+ val local_tyname: ProofContext.context * T list -> string * (ProofContext.context * T list)
+ val local_const: ProofContext.context * T list -> string * (ProofContext.context * T list)
+ val thm_sel: T list -> PureThy.interval list * T list
val bang_facts: ProofContext.context * T list -> thm list * (ProofContext.context * T list)
val goal_spec: ((int -> tactic) -> tactic) -> ('a * T list)
-> ((int -> tactic) -> tactic) * ('a * T list)
- type src
- val src: (string * T list) * Position.T -> src
- val dest_src: src -> (string * T list) * Position.T
- val attribs: T list -> src list * T list
- val opt_attribs: T list -> src list * T list
+ val attribs: (string -> string) -> T list -> src list * T list
+ val opt_attribs: (string -> string) -> T list -> src list * T list
val syntax: string -> ('a * T list -> 'b * ('a * T list)) -> src -> 'a -> 'a * 'b
+ val pretty_src: ProofContext.context -> src -> Pretty.T
+ val pretty_attribs: ProofContext.context -> src list -> Pretty.T list
end;
structure Args: ARGS =
@@ -64,33 +95,58 @@
(** datatype T **)
+(*An argument token is a symbol (with raw string value), together with
+ an optional assigned internal value. Note that an assignable ref
+ designates an intermediate state of internalization -- it is NOT
+ meant to persist.*)
+
datatype kind = Ident | String | Keyword | EOF;
-datatype T = Arg of kind * (string * Position.T);
+
+type symbol = kind * string * Position.T;
-fun val_of (Arg (_, (x, _))) = x;
-fun pos_of (Arg (_, (_, pos))) = pos;
+datatype value =
+ Name of string |
+ Typ of typ |
+ Term of term |
+ Fact of thm list |
+ Attribute of theory attribute * ProofContext.context attribute;
+
+datatype slot =
+ Empty |
+ Value of value option |
+ Assignable of value option ref;
+
+datatype T = Arg of symbol * slot;
-fun str_of (Arg (Ident, (x, _))) = x
- | str_of (Arg (String, (x, _))) = Library.quote x
- | str_of (Arg (Keyword, (x, _))) = x
- | str_of (Arg (EOF, _)) = "end-of-text";
+fun string_of (Arg ((Ident, x, _), _)) = x
+ | string_of (Arg ((String, x, _), _)) = Library.quote x
+ | string_of (Arg ((Keyword, x, _), _)) = x
+ | string_of (Arg ((EOF, _, _), _)) = "";
+
+fun sym_of (Arg ((_, x, _), _)) = x;
+fun pos_of (Arg ((_, _, pos), _)) = pos;
+
+
+(* basic constructors *)
-fun string_of (Arg (Ident, (x, _))) = x
- | string_of (Arg (String, (x, _))) = Library.quote x
- | string_of (Arg (Keyword, (x, _))) = x
- | string_of (Arg (EOF, _)) = "";
+fun mk_symbol k (x, p) = Arg ((k, x, p), Empty);
+fun mk_value k v = Arg ((Keyword, k, Position.none), Value (SOME v));
-fun arg kind x_pos = Arg (kind, x_pos);
-val ident = arg Ident;
-val string = arg String;
-val keyword = arg Keyword;
+val mk_ident = mk_symbol Ident;
+val mk_string = mk_symbol String;
+val mk_keyword = mk_symbol Keyword;
+val mk_name = mk_value "<name>" o Name;
+val mk_typ = mk_value "<typ>" o Typ;
+val mk_term = mk_value "<term>" o Term;
+val mk_fact = mk_value "<fact>" o Fact;
+val mk_attribute = mk_value "<attribute>" o Attribute;
(* eof *)
-val eof = arg EOF ("", Position.none);
+val eof = mk_symbol EOF ("", Position.none);
-fun is_eof (Arg (EOF, _)) = true
+fun is_eof (Arg ((EOF, _, _), _)) = true
| is_eof _ = false;
val stopper = (eof, is_eof);
@@ -98,11 +154,55 @@
+(** datatype src **)
+
+datatype src = Src of (string * T list) * Position.T;
+
+val src = Src;
+fun dest_src (Src src) = src;
+
+fun map_name f (Src ((s, args), pos)) = Src ((f s, args), pos);
+fun map_args f (Src ((s, args), pos)) = Src ((s, map f args), pos);
+
+
+(* values *)
+
+fun map_value f (Arg (s, Value (SOME v))) = Arg (s, Value (SOME (f v)))
+ | map_value _ arg = arg;
+
+fun map_values f g h i = map_args (map_value
+ (fn Name s => Name (f s)
+ | Typ T => Typ (g T)
+ | Term t => Term (h t)
+ | Fact ths => Fact (map i ths)
+ | Attribute att => Attribute att));
+
+
+(* static binding *)
+
+(*1st stage: make empty slots assignable*)
+val assignable =
+ map_args (fn Arg (s, Empty) => Arg (s, Assignable (ref NONE)) | arg => arg);
+
+(*2nd stage: assign values as side-effect of scanning*)
+fun assign v (arg as Arg (_, Assignable r)) = r := v
+ | assign _ _ = ();
+
+val ahead = Scan.ahead (Scan.one not_eof);
+fun touch scan = ahead -- scan >> (fn (arg, y) => (assign NONE arg; y));
+
+(*3rd stage: static closure of final values*)
+val closure =
+ map_args (fn Arg (s, Assignable (ref v)) => Arg (s, Value v) | arg => arg);
+
+
+
(** scanners **)
(* position *)
-fun position scan = (Scan.ahead (Scan.one not_eof) >> pos_of) -- scan >> Library.swap;
+fun position scan =
+ (Scan.ahead (Scan.one not_eof) >> pos_of) -- scan >> Library.swap;
(* cut *)
@@ -110,7 +210,7 @@
fun !!! scan =
let
fun get_pos [] = " (past end-of-text!)"
- | get_pos (Arg (_, (_, pos)) :: _) = Position.str_of pos;
+ | get_pos (arg :: _) = Position.str_of (pos_of arg);
fun err (args, NONE) = "Argument syntax error" ^ get_pos args
| err (args, SOME msg) = "Argument syntax error" ^ get_pos args ^ ": " ^ msg;
@@ -119,8 +219,20 @@
(* basic *)
-fun $$$$ x = Scan.one (fn Arg (k, (y, _)) => (k = Ident orelse k = Keyword) andalso x = y);
-fun $$$ x = $$$$ x >> val_of;
+fun some_ident f =
+ touch (Scan.some (fn Arg ((Ident, x, _), _) => f x | _ => NONE));
+
+val named =
+ touch (Scan.one (fn Arg ((k, _, _), _) => k = Ident orelse k = String));
+
+val symbolic =
+ touch (Scan.one (fn Arg ((k, x, _), _) => k = Keyword andalso OuterLex.is_sid x));
+
+fun &&& x =
+ touch (Scan.one (fn Arg ((k, y, _), _) => k = Keyword andalso x = y));
+
+fun $$$ x =
+ touch (Scan.one (fn Arg ((k, y, _), _) => (k = Ident orelse k = Keyword) andalso x = y) >> sym_of);
val add = $$$ "add";
val del = $$$ "del";
@@ -132,31 +244,24 @@
fun parens scan = $$$ "(" |-- scan --| $$$ ")";
fun bracks scan = $$$ "[" |-- scan --| $$$ "]";
-fun mode s = Scan.lift (Scan.optional (parens ($$$$ s) >> K true) false);
-
-val name = Scan.one (fn Arg (k, (x, _)) => k = Ident orelse k = String) >> val_of;
-val name_dummy = $$$ "_" >> K NONE || name >> SOME;
+fun mode s = Scan.lift (Scan.optional (parens ($$$ s) >> K true) false);
+fun maybe scan = $$$ "_" >> K NONE || scan >> SOME;
-val keyword_symid =
- Scan.one (fn Arg (k, (x, _)) => k = Keyword andalso OuterLex.is_sid x) >> val_of;
+val name = named >> sym_of;
-fun kind f = Scan.one (K true) :--
- (fn Arg (Ident, (x, _)) =>
- (case f x of SOME y => Scan.succeed y | _ => Scan.fail)
- | _ => Scan.fail) >> #2;
-
-val nat = kind Syntax.read_nat;
+val nat = some_ident Syntax.read_nat;
val int = Scan.optional ($$$ "-" >> K ~1) 1 -- nat >> op *;
-(*read variable name; leading '?' may be omitted if name contains no dot*)
-val var = kind (Option.map #1 o (fn s =>
- SOME (Term.dest_Var (Syntax.read_var s))
- handle _ => SOME (Term.dest_Var (Syntax.read_var ("?" ^ s)))
- handle _ => NONE));
+(*variable name; leading '?' may be omitted if name contains no dot*)
+val read_var = try (#1 o Term.dest_Var o Syntax.read_var);
+val var = some_ident read_var || some_ident (fn x => read_var ("?" ^ x));
(* enumerations *)
+fun list1 scan = scan -- Scan.repeat ($$$ "," |-- scan) >> op ::;
+fun list scan = list1 scan || Scan.succeed [];
+
fun enum1 sep scan = scan -- Scan.repeat (Scan.lift ($$$ sep) |-- scan) >> op ::;
fun enum sep scan = enum1 sep scan || Scan.succeed [];
@@ -164,25 +269,60 @@
fun and_list scan = enum "and" scan;
+(* values *)
+
+fun value dest = Scan.some (*no touch here*)
+ (fn Arg (_, Value (SOME v)) => (SOME (dest v) handle Match => NONE)
+ | Arg _ => NONE);
+
+fun evaluate mk eval arg =
+ let val x = eval (sym_of arg) in (assign (SOME (mk x)) arg; x) end;
+
+val internal_name = value (fn Name s => s);
+val internal_typ = value (fn Typ T => T);
+val internal_term = value (fn Term t => t);
+val internal_fact = value (fn Fact ths => ths);
+val internal_attribute = value (fn Attribute att => att);
+
+fun named_name intern = internal_name || named >> evaluate Name intern;
+fun named_typ readT = internal_typ || named >> evaluate Typ readT;
+fun named_term read = internal_term || named >> evaluate Term read;
+fun named_fact get = internal_fact || named >> evaluate Fact get;
+
+
(* terms and types *)
-fun gen_item read = Scan.depend (fn st => name >> (pair st o read st));
+val global_typ_raw = Scan.peek (named_typ o ProofContext.read_typ_raw o ProofContext.init);
+val global_typ = Scan.peek (named_typ o ProofContext.read_typ o ProofContext.init);
+val global_term = Scan.peek (named_term o ProofContext.read_term o ProofContext.init);
+val global_prop = Scan.peek (named_term o ProofContext.read_prop o ProofContext.init);
-val global_typ_raw = gen_item (ProofContext.read_typ_raw o ProofContext.init);
-val global_typ = gen_item (ProofContext.read_typ o ProofContext.init);
-val global_term = gen_item (ProofContext.read_term o ProofContext.init);
-val global_prop = gen_item (ProofContext.read_prop o ProofContext.init);
-
-val local_typ_raw = gen_item ProofContext.read_typ_raw;
-val local_typ = gen_item ProofContext.read_typ;
-val local_term = gen_item ProofContext.read_term;
-val local_prop = gen_item ProofContext.read_prop;
+val local_typ_raw = Scan.peek (named_typ o ProofContext.read_typ_raw);
+val local_typ = Scan.peek (named_typ o ProofContext.read_typ);
+val local_term = Scan.peek (named_term o ProofContext.read_term);
+val local_prop = Scan.peek (named_term o ProofContext.read_prop);
-(* bang facts *)
+(* type and constant names *)
+
+val dest_tyname = fn Type (c, _) => c | TFree (a, _) => a | _ => "";
+val dest_const = fn Const (c, _) => c | Free (x, _) => x | _ => "";
+
+val global_tyname = Scan.peek (named_typ o Sign.read_tyname o Theory.sign_of) >> dest_tyname;
+val global_const = Scan.peek (named_term o Sign.read_const o Theory.sign_of) >> dest_const;
+val local_tyname = Scan.peek (named_typ o ProofContext.read_tyname) >> dest_tyname;
+val local_const = Scan.peek (named_term o ProofContext.read_const) >> dest_const;
-val bang_facts = Scan.depend (fn ctxt =>
- ($$$ "!" >> K (ProofContext.prems_of ctxt) || Scan.succeed []) >> pair ctxt);
+
+(* misc *)
+
+val thm_sel = parens (list1
+ (nat --| $$$ "-" -- nat >> PureThy.FromTo ||
+ nat --| $$$ "-" >> PureThy.From ||
+ nat >> PureThy.Single));
+
+val bang_facts = Scan.peek (fn ctxt =>
+ $$$ "!" >> K (ProofContext.prems_of ctxt) || Scan.succeed []);
(* goal specification *)
@@ -190,62 +330,72 @@
(* range *)
val from_to =
- nat -- ($$$$ "-" |-- nat) >> (fn (i, j) => fn tac => Seq.INTERVAL tac i j) ||
- nat --| $$$$ "-" >> (fn i => fn tac => fn st => Seq.INTERVAL tac i (Thm.nprems_of st) st) ||
+ nat -- ($$$ "-" |-- nat) >> (fn (i, j) => fn tac => Seq.INTERVAL tac i j) ||
+ nat --| $$$ "-" >> (fn i => fn tac => fn st => Seq.INTERVAL tac i (Thm.nprems_of st) st) ||
nat >> (fn i => fn tac => tac i) ||
- $$$$ "!" >> K ALLGOALS;
+ $$$ "!" >> K ALLGOALS;
-val goal = $$$$ "[" |-- !!! (from_to --| $$$$ "]");
+val goal = $$$ "[" |-- !!! (from_to --| $$$ "]");
fun goal_spec def = Scan.lift (Scan.optional goal def);
-(* args *)
+
+(* attribs *)
+
+local
val exclude = explode "()[],";
-fun atom_arg blk = Scan.one (fn Arg (k, (x, _)) =>
- k <> Keyword orelse not (x mem exclude) orelse blk andalso x = ",");
-
-fun paren_args l r scan = $$$$ l -- !!! (scan true -- $$$$ r)
- >> (fn (x, (ys, z)) => x :: ys @ [z]);
+fun atomic blk = touch (Scan.one (fn Arg ((k, x, _), _) =>
+ k <> Keyword orelse not (x mem exclude) orelse blk andalso x = ","));
fun args blk x = Scan.optional (args1 blk) [] x
and args1 blk x =
((Scan.repeat1
- (Scan.repeat1 (atom_arg blk) ||
- paren_args "(" ")" args ||
- paren_args "[" "]" args)) >> List.concat) x;
+ (Scan.repeat1 (atomic blk) ||
+ argsp "(" ")" ||
+ argsp "[" "]")) >> List.concat) x
+and argsp l r x =
+ (Scan.trace (&&& l -- !!! (args true -- &&& r)) >> #2) x;
+
+in
+fun attribs intern =
+ let
+ val attrib_name = internal_name || (symbolic || named) >> evaluate Name intern;
+ val attrib = position (attrib_name -- !!! (args false)) >> src;
+ in $$$ "[" |-- !!! (list attrib --| $$$ "]") end;
+
+fun opt_attribs intern = Scan.optional (attribs intern) [];
+
+end;
-(** type src **)
-
-datatype src = Src of (string * T list) * Position.T;
-
-val src = Src;
-fun dest_src (Src src) = src;
-
-fun err_in_src kind msg (Src ((s, args), pos)) =
- error (kind ^ " " ^ quote s ^ Position.str_of pos ^ ": " ^ msg ^ "\n " ^
- space_implode " " (map str_of args));
-
-
-(* argument syntax *)
+(* syntax interface *)
fun syntax kind scan (src as Src ((s, args), pos)) st =
(case Scan.error (Scan.finite' stopper (Scan.option scan)) (st, args) of
(SOME x, (st', [])) => (st', x)
- | (_, (_, args')) => err_in_src kind "bad arguments" (Src ((s, args'), pos)));
+ | (_, (_, args')) =>
+ error (kind ^ " " ^ quote s ^ Position.str_of pos ^ ": bad arguments\n " ^
+ space_implode " " (map string_of args')));
+
-(* attribs *)
-
-fun list1 scan = scan -- Scan.repeat ($$$ "," |-- scan) >> op ::;
-fun list scan = list1 scan || Scan.succeed [];
+(** pretty printing **)
-val attrib = position ((keyword_symid || name) -- !!! (args false)) >> src;
-val attribs = $$$ "[" |-- !!! (list attrib --| $$$ "]");
-val opt_attribs = Scan.optional attribs [];
+fun pretty_src ctxt src =
+ let
+ fun prt (Arg (_, Value (SOME (Name s)))) = Pretty.str (quote s)
+ | prt (Arg (_, Value (SOME (Typ T)))) = ProofContext.pretty_typ ctxt T
+ | prt (Arg (_, Value (SOME (Term t)))) = ProofContext.pretty_term ctxt t
+ | prt (Arg (_, Value (SOME (Fact ths)))) = ProofContext.pretty_thms ctxt ths
+ | prt arg = Pretty.str (string_of arg);
+ val (s, args) = #1 (dest_src src);
+ in Pretty.block (Pretty.breaks (Pretty.str s :: map prt args)) end;
+fun pretty_attribs _ [] = []
+ | pretty_attribs ctxt srcs =
+ [Pretty.enclose "[" "]" (Pretty.commas (map (pretty_src ctxt) srcs))];
end;
--- a/src/Pure/Isar/attrib.ML Wed Apr 13 09:48:41 2005 +0200
+++ b/src/Pure/Isar/attrib.ML Wed Apr 13 18:34:22 2005 +0200
@@ -8,37 +8,46 @@
signature BASIC_ATTRIB =
sig
val print_attributes: theory -> unit
- val Attribute: bstring -> (Args.src -> theory attribute) * (Args.src -> Proof.context attribute)
+ val Attribute: bstring -> (Args.src -> theory attribute) * (Args.src -> ProofContext.context attribute)
-> string -> unit
end;
signature ATTRIB =
sig
include BASIC_ATTRIB
+ type src
exception ATTRIB_FAIL of (string * Position.T) * exn
- val global_attribute: theory -> Args.src -> theory attribute
- val local_attribute: theory -> Args.src -> Proof.context attribute
- val multi_attribute: theory -> Args.src -> Locale.multi_attribute
- val local_attribute': Proof.context -> Args.src -> Proof.context attribute
+ val intern: Sign.sg -> xstring -> string
+ val intern_src: Sign.sg -> src -> src
+ val global_attribute_i: theory -> src -> theory attribute
+ val global_attribute: theory -> src -> theory attribute
+ val local_attribute_i: theory -> src -> ProofContext.context attribute
+ val local_attribute: theory -> src -> ProofContext.context attribute
+ val context_attribute_i: ProofContext.context -> Args.src -> ProofContext.context attribute
+ val context_attribute: ProofContext.context -> Args.src -> ProofContext.context attribute
val undef_global_attribute: theory attribute
- val undef_local_attribute: Proof.context attribute
- val add_attributes: (bstring * ((Args.src -> theory attribute) *
- (Args.src -> Proof.context attribute)) * string) list -> theory -> theory
+ val undef_local_attribute: ProofContext.context attribute
+ val crude_closure: ProofContext.context -> src -> src
+ val add_attributes: (bstring * ((src -> theory attribute) *
+ (src -> ProofContext.context attribute)) * string) list -> theory -> theory
val global_thm: theory * Args.T list -> thm * (theory * Args.T list)
val global_thms: theory * Args.T list -> thm list * (theory * Args.T list)
val global_thmss: theory * Args.T list -> thm list * (theory * Args.T list)
- val local_thm: Proof.context * Args.T list -> thm * (Proof.context * Args.T list)
- val local_thms: Proof.context * Args.T list -> thm list * (Proof.context * Args.T list)
- val local_thmss: Proof.context * Args.T list -> thm list * (Proof.context * Args.T list)
- val syntax: ('a * Args.T list -> 'a attribute * ('a * Args.T list)) -> Args.src -> 'a attribute
- val no_args: 'a attribute -> Args.src -> 'a attribute
- val add_del_args: 'a attribute -> 'a attribute -> Args.src -> 'a attribute
+ val local_thm: ProofContext.context * Args.T list -> thm * (ProofContext.context * Args.T list)
+ val local_thms: ProofContext.context * Args.T list -> thm list * (ProofContext.context * Args.T list)
+ val local_thmss: ProofContext.context * Args.T list -> thm list * (ProofContext.context * Args.T list)
+ val syntax: ('a * Args.T list -> 'a attribute * ('a * Args.T list)) -> src -> 'a attribute
+ val no_args: 'a attribute -> src -> 'a attribute
+ val add_del_args: 'a attribute -> 'a attribute -> src -> 'a attribute
+ val attribute: (theory attribute * ProofContext.context attribute) -> src
val setup: (theory -> theory) list
end;
structure Attrib: ATTRIB =
struct
+type src = Args.src;
+
(** attributes theory data **)
@@ -50,7 +59,7 @@
type T =
{space: NameSpace.T,
attrs:
- ((((Args.src -> theory attribute) * (Args.src -> Proof.context attribute))
+ ((((src -> theory attribute) * (src -> ProofContext.context attribute))
* string) * stamp) Symtab.table};
val empty = {space = NameSpace.empty, attrs = Symtab.empty};
@@ -76,18 +85,23 @@
val print_attributes = AttributesData.print;
+(* interning *)
+
+val intern = NameSpace.intern o #space o AttributesData.get_sg;
+val intern_src = Args.map_name o intern;
+
+
(* get global / local attributes *)
exception ATTRIB_FAIL of (string * Position.T) * exn;
fun gen_attribute which thy =
let
- val {space, attrs} = AttributesData.get thy;
+ val {attrs, ...} = AttributesData.get thy;
fun attr src =
let
- val ((raw_name, _), pos) = Args.dest_src src;
- val name = NameSpace.intern space raw_name;
+ val ((name, _), pos) = Args.dest_src src;
in
(case Symtab.lookup (attrs, name) of
NONE => error ("Unknown attribute: " ^ quote name ^ Position.str_of pos)
@@ -95,19 +109,33 @@
end;
in attr end;
-val global_attribute = gen_attribute fst;
-val local_attribute = gen_attribute snd;
-fun multi_attribute thy src =
- (global_attribute thy src, local_attribute thy src);
-val local_attribute' = local_attribute o ProofContext.theory_of;
+val global_attribute_i = gen_attribute fst;
+fun global_attribute thy = global_attribute_i thy o intern_src (Theory.sign_of thy);
+
+val local_attribute_i = gen_attribute snd;
+fun local_attribute thy = local_attribute_i thy o intern_src (Theory.sign_of thy);
+
+val context_attribute_i = local_attribute_i o ProofContext.theory_of;
+val context_attribute = local_attribute o ProofContext.theory_of;
val undef_global_attribute: theory attribute =
fn _ => error "attribute undefined in theory context";
-val undef_local_attribute: Proof.context attribute =
+val undef_local_attribute: ProofContext.context attribute =
fn _ => error "attribute undefined in proof context";
+(* crude_closure *)
+
+(*Produce closure without knowing facts in advance! The following
+ should work reasonably well for attribute parsers that do not peek
+ at the thm structure.*)
+
+fun crude_closure ctxt src =
+ (try (transform_error (fn () => context_attribute_i ctxt src (ctxt, Drule.asm_rl))) ();
+ Args.closure src);
+
+
(* add_attributes *)
fun add_attributes raw_attrs thy =
@@ -136,20 +164,24 @@
(* theorems *)
-val thm_sel = Args.parens (Scan.pass () (Args.enum1 "," (Scan.lift
- ( Args.nat --| Args.$$$ "-" -- Args.nat >> op upto
- || Args.nat >> single)) >> List.concat));
+fun gen_thm theory_of attrib get pick = Scan.depend (fn st =>
+ Scan.ahead Args.name -- Args.named_fact (fn name => get st (name, NONE)) --
+ Scan.option Args.thm_sel -- Args.opt_attribs (intern (Theory.sign_of (theory_of st)))
+ >> (fn (((name, fact), sel), srcs) =>
+ let
+ val ths = PureThy.select_thm (name, sel) fact;
+ val atts = map (attrib (theory_of st)) srcs;
+ val (st', ths') = Thm.applys_attributes ((st, ths), atts);
+ in (st', pick name ths') end));
-fun gen_thm get attrib app =
- Scan.depend (fn st => Args.name -- Scan.option thm_sel -- Args.opt_attribs >>
- (fn (name, srcs) => app ((st, get st name), map (attrib st) srcs)));
-
-val global_thm = gen_thm PureThy.get_thm global_attribute Thm.apply_attributes;
-val global_thms = gen_thm PureThy.get_thms global_attribute Thm.applys_attributes;
+val global_thm = gen_thm I global_attribute_i PureThy.get_thms PureThy.single_thm;
+val global_thms = gen_thm I global_attribute_i PureThy.get_thms (K I);
val global_thmss = Scan.repeat global_thms >> List.concat;
-val local_thm = gen_thm ProofContext.get_thm local_attribute' Thm.apply_attributes;
-val local_thms = gen_thm ProofContext.get_thms local_attribute' Thm.applys_attributes;
+val local_thm =
+ gen_thm ProofContext.theory_of local_attribute_i ProofContext.get_thms PureThy.single_thm;
+val local_thms =
+ gen_thm ProofContext.theory_of local_attribute_i ProofContext.get_thms (K I);
val local_thmss = Scan.repeat local_thms >> List.concat;
@@ -201,119 +233,186 @@
val OF_local = syntax (local_thmss >> apply);
-(* where *)
+(* read_instantiate: named instantiation of type and term variables *)
-(*named instantiations; permits instantiation of type and term variables*)
+local
-fun read_instantiate _ [] _ thm = thm
- | read_instantiate context_of insts x thm =
- let
- val ctxt = context_of x;
- val sign = ProofContext.sign_of ctxt;
+fun is_tvar (x, _) = (case Symbol.explode x of "'" :: _ => true | _ => false);
+
+fun error_var msg xi = error (msg ^ Syntax.string_of_vname xi);
+
+fun the_sort sorts xi = valOf (sorts xi)
+ handle Option.Option => error_var "No such type variable in theorem: " xi;
- (* Separate type and term insts,
- type insts must occur strictly before term insts *)
- fun has_type_var ((x, _), _) = (case Symbol.explode x of
- "'"::cs => true | cs => false);
- val (Tinst, tinsts) = take_prefix has_type_var insts;
- val _ = if exists has_type_var tinsts
- then error
- "Type instantiations must occur before term instantiations."
- else ();
+fun the_type types xi = valOf (types xi)
+ handle Option.Option => error_var "No such variable in theorem: " xi;
- val Tinsts = List.filter has_type_var insts;
- val tinsts = filter_out has_type_var insts;
+fun unify_types sign types ((unifier, maxidx), (xi, u)) =
+ let
+ val T = the_type types xi;
+ val U = Term.fastype_of u;
+ val maxidx' = Int.max (maxidx, Int.max (#2 xi, Term.maxidx_of_term u));
+ in
+ Type.unify (Sign.tsig_of sign) (unifier, maxidx') (T, U)
+ handle Type.TUNIFY => error_var "Incompatible type for instantiation of " xi
+ end;
+
+fun typ_subst env = apsnd (Term.typ_subst_TVars env);
+fun subst env = apsnd (Term.subst_TVars env);
- (* Type instantiations first *)
- (* Process type insts: Tinsts_env *)
- fun absent xi = error
- ("No such type variable in theorem: " ^
- Syntax.string_of_vname xi);
- val (rtypes, rsorts) = types_sorts thm;
- fun readT (xi, s) =
- let val S = case rsorts xi of SOME S => S | NONE => absent xi;
- val T = ProofContext.read_typ ctxt s;
- in if Sign.typ_instance sign (T, TVar (xi, S)) then (xi, T)
- else error
- ("Instantiation of " ^ Syntax.string_of_vname xi ^ " fails")
- end;
- val Tinsts_env = map readT Tinsts;
- val cenvT = map (apsnd (Thm.ctyp_of sign)) (Tinsts_env);
- val thm' = Thm.instantiate (cenvT, []) thm;
- (* Instantiate, but don't normalise: *)
- (* this happens after term insts anyway. *)
+fun instantiate sign envT env =
+ let
+ fun prepT (a, T) = (a, Thm.ctyp_of sign T);
+ fun prep (xi, t) = pairself (Thm.cterm_of sign) (Var (xi, Term.fastype_of t), t);
+ in
+ Drule.instantiate (map prepT (distinct envT),
+ map prep (gen_distinct (fn ((xi, t), (yj, u)) => xi = yj andalso t aconv u) env))
+ end;
+
+in
+
+fun read_instantiate init mixed_insts (context, thm) =
+ let
+ val ctxt = init context;
+ val sign = ProofContext.sign_of ctxt;
- (* Term instantiations *)
- val vars = Drule.vars_of thm';
- fun get_typ xi =
- (case assoc (vars, xi) of
- SOME T => T
- | NONE => error ("No such variable in theorem: " ^ Syntax.string_of_vname xi));
+ val (type_insts, term_insts) = List.partition (is_tvar o #1) (map #2 mixed_insts);
+ val internal_insts = term_insts |> List.mapPartial
+ (fn (xi, Args.Term t) => SOME (xi, t)
+ | (_, Args.Name _) => NONE
+ | (xi, _) => error_var "Term argument expected for " xi);
+ val external_insts = term_insts |> List.mapPartial
+ (fn (xi, Args.Name s) => SOME (xi, s) | _ => NONE);
- val (xs, ss) = Library.split_list tinsts;
- val Ts = map get_typ xs;
+
+ (* type instantiations *)
- val used = add_term_tvarnames (prop_of thm',[])
- (* Names of TVars occuring in thm'. read_def_termTs ensures
- that new TVars introduced when reading the instantiation string
- are distinct from those occuring in the theorem. *)
-
- val (ts, envT) =
- ProofContext.read_termTs ctxt (K false) (K NONE) (K NONE) used (ss ~~ Ts);
+ val sorts = #2 (Drule.types_sorts thm);
- val cenvT = map (apsnd (Thm.ctyp_of sign)) envT;
- val cenv =
- map (fn (xi, t) => pairself (Thm.cterm_of sign) (Var (xi, fastype_of t), t))
- (gen_distinct (fn ((x1, t1), (x2, t2)) => x1 = x2 andalso t1 aconv t2) (xs ~~ ts));
+ fun readT (xi, arg) =
+ let
+ val S = the_sort sorts xi;
+ val T =
+ (case arg of
+ Args.Name s => ProofContext.read_typ ctxt s
+ | Args.Typ T => T
+ | _ => error_var "Type argument expected for " xi);
in
- thm'
- |> Drule.instantiate (cenvT, cenv)
- |> RuleCases.save thm
+ if Sign.of_sort sign (T, S) then (xi, T)
+ else error_var "Incompatible sort for typ instantiation of " xi
end;
-fun insts x = Args.and_list (Scan.lift (Args.var --| Args.$$$ "=" -- Args.name)) x;
+ val type_insts' = map readT type_insts;
+ val thm' = instantiate sign type_insts' [] thm;
+
+
+ (* internal term instantiations *)
+
+ val types' = #1 (Drule.types_sorts thm');
+ val unifier = Vartab.dest (#1
+ (Library.foldl (unify_types sign types') ((Vartab.empty, 0), internal_insts)));
+
+ val type_insts'' = map (typ_subst unifier) type_insts';
+ val internal_insts'' = map (subst unifier) internal_insts;
+ val thm'' = instantiate sign unifier internal_insts'' thm';
+
+
+ (* external term instantiations *)
+
+ val types'' = #1 (Drule.types_sorts thm'');
+
+ val (xs, ss) = split_list external_insts;
+ val Ts = map (the_type types'') xs;
+ val (ts, inferred) = ProofContext.read_termTs ctxt (K false)
+ (K NONE) (K NONE) (Drule.add_used thm'' []) (ss ~~ Ts);
+
+ val type_insts''' = map (typ_subst inferred) type_insts'';
+ val internal_insts''' = map (subst inferred) internal_insts'';
-fun gen_where context_of = syntax (insts >> (Drule.rule_attribute o read_instantiate context_of));
+ val external_insts''' = xs ~~ ts;
+ val term_insts''' = internal_insts''' @ external_insts''';
+ val thm''' = instantiate sign inferred external_insts''' thm'';
+ in
+
+ (* assign internalized values *)
+
+ mixed_insts |> List.app (fn (arg, (xi, _)) =>
+ if is_tvar xi then
+ Args.assign (SOME (Args.Typ (valOf (assoc (type_insts''', xi))))) arg
+ else
+ Args.assign (SOME (Args.Term (valOf (assoc (term_insts''', xi))))) arg);
+
+ (context, thm''' |> RuleCases.save thm)
+ end;
+
+end;
+
+
+(* where: named instantiation *)
+
+local
+
+val value =
+ Args.internal_typ >> Args.Typ ||
+ Args.internal_term >> Args.Term ||
+ Args.name >> Args.Name;
+
+val inst = Args.var -- (Args.$$$ "=" |-- Args.ahead -- value)
+ >> (fn (xi, (a, v)) => (a, (xi, v)));
+
+fun gen_where init =
+ syntax (Args.and_list (Scan.lift inst) >> read_instantiate init);
+
+in
val where_global = gen_where ProofContext.init;
val where_local = gen_where I;
+end;
-(* of: positional instantiations *)
-(* permits instantiation of term variables only *)
+
+(* of: positional instantiation (term arguments only) *)
+
+local
-fun read_instantiate' _ ([], []) _ thm = thm
- | read_instantiate' context_of (args, concl_args) x thm =
- let
- fun zip_vars _ [] = []
- | zip_vars (_ :: xs) (NONE :: opt_ts) = zip_vars xs opt_ts
- | zip_vars ((x, _) :: xs) (SOME t :: opt_ts) = (x, t) :: zip_vars xs opt_ts
- | zip_vars [] _ = error "More instantiations than variables in theorem";
- val insts =
- zip_vars (Drule.vars_of_terms [Thm.prop_of thm]) args @
- zip_vars (Drule.vars_of_terms [Thm.concl_of thm]) concl_args;
- in
- thm
- |> read_instantiate context_of insts x
- |> RuleCases.save thm
- end;
+fun read_instantiate' init (args, concl_args) (context, thm) =
+ let
+ fun zip_vars _ [] = []
+ | zip_vars (_ :: xs) ((_, NONE) :: rest) = zip_vars xs rest
+ | zip_vars ((x, _) :: xs) ((a, SOME t) :: rest) = (a, (x, t)) :: zip_vars xs rest
+ | zip_vars [] _ = error "More instantiations than variables in theorem";
+ val insts =
+ zip_vars (Drule.vars_of_terms [Thm.prop_of thm]) args @
+ zip_vars (Drule.vars_of_terms [Thm.concl_of thm]) concl_args;
+ in
+ read_instantiate init insts (context, thm)
+ end;
+val value =
+ Args.internal_term >> Args.Term ||
+ Args.name >> Args.Name;
+
+val inst = Args.ahead -- Args.maybe value;
val concl = Args.$$$ "concl" -- Args.colon;
-val inst_arg = Scan.unless concl Args.name_dummy;
-val inst_args = Scan.repeat inst_arg;
-fun insts' x = (inst_args -- Scan.optional (concl |-- Args.!!! inst_args) []) x;
-fun gen_of context_of =
- syntax (Scan.lift insts' >> (Drule.rule_attribute o read_instantiate' context_of));
+val insts =
+ Scan.repeat (Scan.unless concl inst) --
+ Scan.optional (concl |-- Scan.repeat inst) [];
+
+fun gen_of init = syntax (Scan.lift insts >> read_instantiate' init);
+
+in
val of_global = gen_of ProofContext.init;
val of_local = gen_of I;
+end;
+
(* rename_abs *)
fun rename_abs src = syntax
- (Scan.lift (Scan.repeat Args.name_dummy >> (apsnd o Drule.rename_bvars'))) src;
+ (Scan.lift (Scan.repeat (Args.maybe Args.name) >> (apsnd o Drule.rename_bvars'))) src;
(* unfold / fold definitions *)
@@ -335,9 +434,8 @@
(* rule_format *)
-fun rule_format_att x = syntax
- (Scan.lift (Args.parens (Args.$$$ "no_asm")
- >> K ObjectLogic.rule_format_no_asm || Scan.succeed ObjectLogic.rule_format)) x;
+fun rule_format_att x = syntax (Args.mode "no_asm"
+ >> (fn true => ObjectLogic.rule_format_no_asm | false => ObjectLogic.rule_format)) x;
(* misc rules *)
@@ -380,6 +478,20 @@
end;
+(* internal attribute *)
+
+val attributeN = "attribute";
+fun attribute att = Args.src ((attributeN, [Args.mk_attribute att]), Position.none);
+
+fun attribute_global x = (syntax (Scan.lift Args.internal_attribute >> #1)) x;
+fun attribute_local x = (syntax (Scan.lift Args.internal_attribute >> #2)) x;
+
+val setup_internal_attribute =
+ [PureThy.global_path,
+ add_attributes [(attributeN, (attribute_global, attribute_local), "internal attribute")],
+ PureThy.local_path];
+
+
(** theory setup **)
@@ -412,7 +524,8 @@
(* setup *)
-val setup = [AttributesData.init, add_attributes pure_attributes];
+val setup =
+ AttributesData.init :: setup_internal_attribute @ [add_attributes pure_attributes];
end;
--- a/src/Pure/Isar/constdefs.ML Wed Apr 13 09:48:41 2005 +0200
+++ b/src/Pure/Isar/constdefs.ML Wed Apr 13 18:34:22 2005 +0200
@@ -11,7 +11,7 @@
sig
val add_constdefs: (string list * string option) list *
((bstring * string option * Syntax.mixfix) option *
- ((bstring * Args.src list) * string)) list
+ ((bstring * Attrib.src list) * string)) list
-> theory -> theory
val add_constdefs_i: (string list * typ option) list *
((bstring * typ option * Syntax.mixfix) option *
--- a/src/Pure/Isar/induct_attrib.ML Wed Apr 13 09:48:41 2005 +0200
+++ b/src/Pure/Isar/induct_attrib.ML Wed Apr 13 18:34:22 2005 +0200
@@ -204,25 +204,22 @@
local
-fun spec k cert =
- (Args.$$$ k -- Args.colon) |-- Args.!!! (Args.name >> cert) ||
- Args.$$$ k >> K "";
+fun spec k arg =
+ Scan.lift (Args.$$$ k -- Args.colon) |-- arg ||
+ Scan.lift (Args.$$$ k) >> K "";
-fun attrib sign_of add_type add_set = Scan.depend (fn x =>
- let val sg = sign_of x in
- spec typeN (Sign.certify_tyname sg o Sign.intern_tycon sg) >> add_type ||
- spec setN (Sign.certify_const sg o Sign.intern_const sg) >> add_set
- end >> pair x);
+fun attrib tyname const add_type add_set =
+ Attrib.syntax (spec typeN tyname >> add_type || spec setN const >> add_set);
in
val cases_attr =
- (Attrib.syntax (attrib Theory.sign_of cases_type_global cases_set_global),
- Attrib.syntax (attrib ProofContext.sign_of cases_type_local cases_set_local));
+ (attrib Args.global_tyname Args.global_const cases_type_global cases_set_global,
+ attrib Args.local_tyname Args.local_const cases_type_local cases_set_local);
val induct_attr =
- (Attrib.syntax (attrib Theory.sign_of induct_type_global induct_set_global),
- Attrib.syntax (attrib ProofContext.sign_of induct_type_local induct_set_local));
+ (attrib Args.global_tyname Args.global_const induct_type_global induct_set_global,
+ attrib Args.local_tyname Args.local_const induct_type_local induct_set_local);
end;
--- a/src/Pure/Isar/isar_cmd.ML Wed Apr 13 09:48:41 2005 +0200
+++ b/src/Pure/Isar/isar_cmd.ML Wed Apr 13 18:34:22 2005 +0200
@@ -47,7 +47,7 @@
val print_syntax: Toplevel.transition -> Toplevel.transition
val print_theorems: Toplevel.transition -> Toplevel.transition
val print_locales: Toplevel.transition -> Toplevel.transition
- val print_locale: Locale.expr * Args.src Locale.element list
+ val print_locale: Locale.expr * Locale.element list
-> Toplevel.transition -> Toplevel.transition
val print_registrations: string -> Toplevel.transition -> Toplevel.transition
val print_attributes: Toplevel.transition -> Toplevel.transition
@@ -58,14 +58,14 @@
val print_antiquotations: Toplevel.transition -> Toplevel.transition
val print_thms_containing: int option * string list
-> Toplevel.transition -> Toplevel.transition
- val thm_deps: (thmref * Args.src list) list -> Toplevel.transition -> Toplevel.transition
+ val thm_deps: (thmref * Attrib.src list) list -> Toplevel.transition -> Toplevel.transition
val print_binds: Toplevel.transition -> Toplevel.transition
val print_lthms: Toplevel.transition -> Toplevel.transition
val print_cases: Toplevel.transition -> Toplevel.transition
val print_intros: Toplevel.transition -> Toplevel.transition
- val print_thms: string list * (thmref * Args.src list) list
+ val print_thms: string list * (thmref * Attrib.src list) list
-> Toplevel.transition -> Toplevel.transition
- val print_prfs: bool -> string list * (thmref * Args.src list) list option
+ val print_prfs: bool -> string list * (thmref * Attrib.src list) list option
-> Toplevel.transition -> Toplevel.transition
val print_prop: (string list * string) -> Toplevel.transition -> Toplevel.transition
val print_term: (string list * string) -> Toplevel.transition -> Toplevel.transition
@@ -187,7 +187,7 @@
(* present draft files *)
fun display_drafts files = Toplevel.imperative (fn () =>
- let val outfile = File.quote_sysify_path (Present.drafts "pdf" files)
+ let val outfile = File.quote_sysify_path (Present.drafts (getenv "ISABELLE_DOC_FORMAT") files)
in system ("\"$ISATOOL\" display -c " ^ outfile ^ " &"); () end);
fun print_drafts files = Toplevel.imperative (fn () =>
@@ -218,9 +218,7 @@
Toplevel.keep (Locale.print_locales o Toplevel.theory_of);
fun print_locale (import, body) = Toplevel.unknown_theory o Toplevel.keep (fn state =>
- let val thy = Toplevel.theory_of state in
- Locale.print_locale thy import (map (Locale.map_attrib_element (Attrib.multi_attribute thy)) body)
- end);
+ Locale.print_locale (Toplevel.theory_of state) import body);
fun print_registrations name = Toplevel.unknown_context o
Toplevel.keep (Toplevel.node_case (Locale.print_global_registrations name)
--- a/src/Pure/Isar/isar_syn.ML Wed Apr 13 09:48:41 2005 +0200
+++ b/src/Pure/Isar/isar_syn.ML Wed Apr 13 18:34:22 2005 +0200
@@ -310,24 +310,22 @@
-- Scan.optional (P.$$$ "=" |-- P.!!! locale_val) (Locale.empty, [])
>> (Toplevel.theory o IsarThy.add_locale o (fn ((x, y), (z, w)) => (x, y, z, w))));
-val uterm = P.underscore >> K NONE || P.term >> SOME;
-
val view_val =
- Scan.optional (P.$$$ "[" |-- Scan.repeat1 uterm --| P.$$$ "]") [];
+ Scan.optional (P.$$$ "[" |-- Scan.repeat1 (P.maybe P.term) --| P.$$$ "]") [];
val interpretationP =
OuterSyntax.command "interpretation"
- "prove and register interpretation of locale expression in theory" K.thy_goal
- ((P.opt_thm_name ":" -- P.locale_expr -- P.!!! view_val
- >> IsarThy.register_globally)
- >> (Toplevel.print oo Toplevel.theory_to_proof));
+ "prove and register interpretation of locale expression in theory" K.thy_goal
+ (P.opt_thm_name ":" -- P.locale_expr -- P.!!! view_val
+ >> ((Toplevel.print oo Toplevel.theory_to_proof) o IsarThy.register_globally));
val interpretP =
OuterSyntax.command "interpret"
- "prove and register interpretation of locale expression in context"
- K.prf_goal
- (P.opt_thm_name ":" -- P.locale_expr -- P.!!! view_val >>
- ((Toplevel.print oo Toplevel.proof) o IsarThy.register_locally));
+ "prove and register interpretation of locale expression in context" K.prf_goal
+ (P.opt_thm_name ":" -- P.locale_expr -- P.!!! view_val
+ >> ((Toplevel.print oo Toplevel.proof) o IsarThy.register_locally));
+
+
(** proof commands **)
@@ -427,7 +425,7 @@
>> (Toplevel.print oo (Toplevel.proof o IsarThy.let_bind)));
val case_spec =
- (P.$$$ "(" |-- P.!!! (P.xname -- Scan.repeat1 P.uname --| P.$$$ ")") ||
+ (P.$$$ "(" |-- P.!!! (P.xname -- Scan.repeat1 (P.maybe P.name) --| P.$$$ ")") ||
P.xname >> rpair []) -- P.opt_attribs >> P.triple1;
val caseP =
--- a/src/Pure/Isar/isar_thy.ML Wed Apr 13 09:48:41 2005 +0200
+++ b/src/Pure/Isar/isar_thy.ML Wed Apr 13 18:34:22 2005 +0200
@@ -9,113 +9,115 @@
sig
val hide_space: string * xstring list -> theory -> theory
val hide_space_i: string * string list -> theory -> theory
- val add_axioms: ((bstring * string) * Args.src list) list -> theory -> theory
+ val add_axioms: ((bstring * string) * Attrib.src list) list -> theory -> theory
val add_axioms_i: ((bstring * term) * theory attribute list) list -> theory -> theory
- val add_defs: bool * ((bstring * string) * Args.src list) list -> theory -> theory
+ val add_defs: bool * ((bstring * string) * Attrib.src list) list -> theory -> theory
val add_defs_i: bool * ((bstring * term) * theory attribute list) list -> theory -> theory
- val theorems: string -> ((bstring * Args.src list) * (thmref * Args.src list) list) list
+ val theorems: string ->
+ ((bstring * Attrib.src list) * (thmref * Attrib.src list) list) list
-> theory -> theory * (string * thm list) list
val theorems_i: string ->
((bstring * theory attribute list) * (thm list * theory attribute list) list) list
-> theory -> theory * (string * thm list) list
val locale_theorems: string -> xstring ->
- ((bstring * Args.src list) * (thmref * Args.src list) list) list
+ ((bstring * Attrib.src list) * (thmref * Attrib.src list) list) list
-> theory -> theory * (bstring * thm list) list
val locale_theorems_i: string -> string ->
- ((bstring * Locale.multi_attribute list)
- * (thm list * Locale.multi_attribute list) list) list
- -> theory -> theory * (string * thm list) list
+ ((bstring * Attrib.src list) * (thm list * Attrib.src list) list) list ->
+ theory -> theory * (string * thm list) list
val smart_theorems: string -> xstring option ->
- ((bstring * Args.src list) * (thmref * Args.src list) list) list
+ ((bstring * Attrib.src list) * (thmref * Attrib.src list) list) list
-> theory -> theory * (string * thm list) list
- val declare_theorems: xstring option -> (thmref * Args.src list) list -> theory -> theory
- val apply_theorems: (thmref * Args.src list) list -> theory -> theory * thm list
+ val declare_theorems: xstring option ->
+ (thmref * Attrib.src list) list -> theory -> theory
+ val apply_theorems: (thmref * Attrib.src list) list -> theory -> theory * thm list
val apply_theorems_i: (thm list * theory attribute list) list -> theory -> theory * thm list
- val have_facts: ((string * Args.src list) * (thmref * Args.src list) list) list
+ val have_facts: ((string * Attrib.src list) * (thmref * Attrib.src list) list) list
-> ProofHistory.T -> ProofHistory.T
val have_facts_i: ((string * Proof.context attribute list) *
(thm * Proof.context attribute list) list) list -> ProofHistory.T -> ProofHistory.T
- val from_facts: (thmref * Args.src list) list list -> ProofHistory.T -> ProofHistory.T
+ val from_facts: (thmref * Attrib.src list) list list -> ProofHistory.T -> ProofHistory.T
val from_facts_i: (thm * Proof.context attribute list) list list
-> ProofHistory.T -> ProofHistory.T
- val with_facts: (thmref * Args.src list) list list -> ProofHistory.T -> ProofHistory.T
+ val with_facts: (thmref * Attrib.src list) list list -> ProofHistory.T -> ProofHistory.T
val with_facts_i: (thm * Proof.context attribute list) list list
-> ProofHistory.T -> ProofHistory.T
- val using_facts: (thmref * Args.src list) list list -> ProofHistory.T -> ProofHistory.T
+ val using_facts: (thmref * Attrib.src list) list list
+ -> ProofHistory.T -> ProofHistory.T
val using_facts_i: (thm * Proof.context attribute list) list list
-> ProofHistory.T -> ProofHistory.T
val chain: ProofHistory.T -> ProofHistory.T
- val instantiate_locale: (string * Args.src list) * string -> ProofHistory.T
+ val instantiate_locale: (string * Attrib.src list) * string -> ProofHistory.T
-> ProofHistory.T
val fix: (string list * string option) list -> ProofHistory.T -> ProofHistory.T
val fix_i: (string list * typ option) list -> ProofHistory.T -> ProofHistory.T
val let_bind: (string list * string) list -> ProofHistory.T -> ProofHistory.T
val let_bind_i: (term list * term) list -> ProofHistory.T -> ProofHistory.T
- val invoke_case: string * string option list * Args.src list -> ProofHistory.T -> ProofHistory.T
+ val invoke_case: string * string option list * Attrib.src list -> ProofHistory.T -> ProofHistory.T
val invoke_case_i: string * string option list * Proof.context attribute list
-> ProofHistory.T -> ProofHistory.T
- val theorem: string -> (bstring * Args.src list) * (string * (string list * string list))
+ val theorem: string -> (bstring * Attrib.src list) * (string * (string list * string list))
-> bool -> theory -> ProofHistory.T
val theorem_i: string -> (bstring * theory attribute list) *
(term * (term list * term list)) -> bool -> theory -> ProofHistory.T
- val multi_theorem:
- string -> (theory -> theory) ->
+ val multi_theorem: string -> (theory -> theory) ->
(cterm list -> Proof.context -> Proof.context -> thm -> thm) ->
- bstring * Args.src list
- -> Args.src Locale.element Locale.elem_expr list
- -> ((bstring * Args.src list) * (string * (string list * string list)) list) list
+ bstring * Attrib.src list -> Locale.element Locale.elem_expr list ->
+ ((bstring * Attrib.src list) * (string * (string list * string list)) list) list
-> bool -> theory -> ProofHistory.T
- val multi_theorem_i:
- string -> (theory -> theory) ->
+ val multi_theorem_i: string -> (theory -> theory) ->
(cterm list -> Proof.context -> Proof.context -> thm -> thm) ->
- bstring * theory attribute list
- -> Locale.multi_attribute Locale.element_i Locale.elem_expr list
+ bstring * theory attribute list -> Locale.element_i Locale.elem_expr list
-> ((bstring * theory attribute list) * (term * (term list * term list)) list) list
-> bool -> theory -> ProofHistory.T
val locale_multi_theorem: string -> xstring
- -> bstring * Args.src list -> Args.src Locale.element Locale.elem_expr list
- -> ((bstring * Args.src list) * (string * (string list * string list)) list) list
+ -> bstring * Attrib.src list -> Locale.element Locale.elem_expr list
+ -> ((bstring * Attrib.src list) * (string * (string list * string list)) list) list
-> bool -> theory -> ProofHistory.T
- val locale_multi_theorem_i: string -> string -> bstring * Locale.multi_attribute list
- -> Locale.multi_attribute Locale.element_i Locale.elem_expr list
- -> ((bstring * Locale.multi_attribute list) * (term * (term list * term list)) list) list
+ val locale_multi_theorem_i: string -> string -> bstring * Attrib.src list
+ -> Locale.element_i Locale.elem_expr list
+ -> ((bstring * Attrib.src list) * (term * (term list * term list)) list) list
-> bool -> theory -> ProofHistory.T
val smart_multi_theorem: string -> xstring option
- -> bstring * Args.src list -> Args.src Locale.element Locale.elem_expr list
- -> ((bstring * Args.src list) * (string * (string list * string list)) list) list
+ -> bstring * Attrib.src list -> Locale.element Locale.elem_expr list
+ -> ((bstring * Attrib.src list) * (string * (string list * string list)) list) list
-> bool -> theory -> ProofHistory.T
- val assume: ((string * Args.src list) * (string * (string list * string list)) list) list
+ val assume: ((string * Attrib.src list) * (string * (string list * string list)) list) list
-> ProofHistory.T -> ProofHistory.T
val assume_i:
((string * Proof.context attribute list) * (term * (term list * term list)) list) list
-> ProofHistory.T -> ProofHistory.T
- val presume: ((string * Args.src list) * (string * (string list * string list)) list) list
+ val presume: ((string * Attrib.src list) * (string * (string list * string list)) list) list
-> ProofHistory.T -> ProofHistory.T
val presume_i:
((string * Proof.context attribute list) * (term * (term list * term list)) list) list
-> ProofHistory.T -> ProofHistory.T
- val have: ((string * Args.src list) * (string * (string list * string list)) list) list
- -> ProofHistory.T -> ProofHistory.T
+ val have: ((string * Attrib.src list) *
+ (string * (string list * string list)) list) list -> ProofHistory.T -> ProofHistory.T
val have_i: ((string * Proof.context attribute list) *
(term * (term list * term list)) list) list -> ProofHistory.T -> ProofHistory.T
- val hence: ((string * Args.src list) * (string * (string list * string list)) list) list
- -> ProofHistory.T -> ProofHistory.T
+ val hence: ((string * Attrib.src list) *
+ (string * (string list * string list)) list) list -> ProofHistory.T -> ProofHistory.T
val hence_i: ((string * Proof.context attribute list) *
(term * (term list * term list)) list) list -> ProofHistory.T -> ProofHistory.T
- val show: ((string * Args.src list) * (string * (string list * string list)) list) list
+ val show: ((string * Attrib.src list) *
+ (string * (string list * string list)) list) list
-> bool -> ProofHistory.T -> ProofHistory.T
val show_i: ((string * Proof.context attribute list) *
- (term * (term list * term list)) list) list -> bool -> ProofHistory.T -> ProofHistory.T
- val thus: ((string * Args.src list) * (string * (string list * string list)) list) list
+ (term * (term list * term list)) list) list
+ -> bool -> ProofHistory.T -> ProofHistory.T
+ val thus: ((string * Attrib.src list) *
+ (string * (string list * string list)) list) list
-> bool -> ProofHistory.T -> ProofHistory.T
val thus_i: ((string * Proof.context attribute list)
- * (term * (term list * term list)) list) list -> bool -> ProofHistory.T -> ProofHistory.T
- val local_def: (string * Args.src list) * (string * (string * string list))
+ * (term * (term list * term list)) list) list
+ -> bool -> ProofHistory.T -> ProofHistory.T
+ val local_def: (string * Attrib.src list) * (string * (string * string list))
-> ProofHistory.T -> ProofHistory.T
- val local_def_i: (string * Args.src list) * (string * (term * term list))
+ val local_def_i: (string * Attrib.src list) * (string * (term * term list))
-> ProofHistory.T -> ProofHistory.T
val obtain: (string list * string option) list
- * ((string * Args.src list) * (string * (string list * string list)) list) list
+ * ((string * Attrib.src list) * (string * (string list * string list)) list) list
-> Toplevel.transition -> Toplevel.transition
val obtain_i: (string list * typ option) list
* ((string * Proof.context attribute list) * (term * (term list * term list)) list) list
@@ -136,10 +138,10 @@
val done_proof: Toplevel.transition -> Toplevel.transition
val skip_proof: Toplevel.transition -> Toplevel.transition
val forget_proof: Toplevel.transition -> Toplevel.transition
- val get_thmss: (thmref * Args.src list) list -> Proof.state -> thm list
- val also: (thmref * Args.src list) list option -> Toplevel.transition -> Toplevel.transition
+ val get_thmss: (thmref * Attrib.src list) list -> Proof.state -> thm list
+ val also: (thmref * Attrib.src list) list option -> Toplevel.transition -> Toplevel.transition
val also_i: thm list option -> Toplevel.transition -> Toplevel.transition
- val finally: (thmref * Args.src list) list option -> Toplevel.transition -> Toplevel.transition
+ val finally: (thmref * Attrib.src list) list option -> Toplevel.transition -> Toplevel.transition
val finally_i: thm list option -> Toplevel.transition -> Toplevel.transition
val moreover: Toplevel.transition -> Toplevel.transition
val ultimately: Toplevel.transition -> Toplevel.transition
@@ -151,7 +153,13 @@
val token_translation: string -> theory -> theory
val method_setup: bstring * string * string -> theory -> theory
val add_oracle: bstring * string -> theory -> theory
- val add_locale: bool * bstring * Locale.expr * Args.src Locale.element list -> theory -> theory
+ val add_locale: bool * bstring * Locale.expr * Locale.element list -> theory -> theory
+ val register_globally:
+ ((string * Attrib.src list) * Locale.expr) * string option list ->
+ bool -> theory -> ProofHistory.T
+ val register_locally:
+ ((string * Attrib.src list) * Locale.expr) * string option list ->
+ ProofHistory.T -> ProofHistory.T
val begin_theory: string -> string list -> (string * bool) list -> theory
val end_theory: theory -> theory
val kill_theory: string -> unit
@@ -159,14 +167,6 @@
-> Toplevel.transition -> Toplevel.transition
val init_context: ('a -> unit) -> 'a -> Toplevel.transition -> Toplevel.transition
val context: string -> Toplevel.transition -> Toplevel.transition
-
- val register_globally:
- ((string * Args.src list) * Locale.expr) * string option list ->
- bool -> theory -> ProofHistory.T
- val register_locally:
- ((string * Args.src list) * Locale.expr) * string option list ->
- ProofHistory.T -> ProofHistory.T
-
end;
structure IsarThy: ISAR_THY =
@@ -180,8 +180,8 @@
val kinds =
[(Sign.classK, can o Sign.certify_class),
- (Sign.typeK, can o Sign.certify_tyname),
- (Sign.constK, can o Sign.certify_const)];
+ (Sign.typeK, Sign.declared_tyname),
+ (Sign.constK, Sign.declared_const)];
fun gen_hide intern (kind, xnames) thy =
(case assoc (kinds, kind) of
@@ -226,7 +226,6 @@
fun global_attribs thy = prep_attribs (Attrib.global_attribute thy);
fun local_attribs thy = prep_attribs (Attrib.local_attribute thy);
-fun multi_attribs thy = prep_attribs (Attrib.multi_attribute thy);
end;
@@ -250,13 +249,13 @@
|> present_thmss k;
fun locale_theorems k loc args thy = thy
- |> Locale.note_thmss k loc (multi_attribs thy args)
+ |> Locale.note_thmss k loc args
|> present_thmss k;
fun smart_theorems k opt_loc args thy = thy
|> (case opt_loc of
NONE => PureThy.note_thmss (Drule.kind k) (global_attribs thy args)
- | SOME loc => Locale.note_thmss k loc (multi_attribs thy args))
+ | SOME loc => Locale.note_thmss k loc args)
|> present_thmss k;
fun declare_theorems opt_loc args = #1 o smart_theorems "" opt_loc [(("", []), args)];
@@ -384,28 +383,33 @@
in
-fun multi_theorem k thy_mod export a elems concl int thy =
- global_statement (Proof.multi_theorem k thy_mod export NONE (apsnd (map (Attrib.global_attribute thy)) a)
- (map (Locale.map_attrib_elem_or_expr (Attrib.multi_attribute thy)) elems)) concl int thy;
+fun multi_theorem k after_qed export a elems concl int thy =
+ global_statement (Proof.multi_theorem k after_qed export NONE
+ (apsnd (map (Attrib.global_attribute thy)) a)
+ (map (Locale.intern_attrib_elem_expr thy) elems)) concl int thy;
-fun multi_theorem_i k thy_mod export a = global_statement_i o Proof.multi_theorem_i k thy_mod export NONE a;
+fun multi_theorem_i k after_qed export a =
+ global_statement_i o Proof.multi_theorem_i k after_qed export NONE a;
fun locale_multi_theorem k locale (name, atts) elems concl int thy =
- global_statement (Proof.multi_theorem k I ProofContext.export_standard
- (SOME (locale, (map (Attrib.multi_attribute thy) atts,
- map (map (Attrib.multi_attribute thy) o snd o fst) concl)))
- (name, []) (map (Locale.map_attrib_elem_or_expr (Attrib.multi_attribute thy)) elems))
- (map (apfst (apsnd (K []))) concl) int thy;
+ global_statement (Proof.multi_theorem k I ProofContext.export_standard
+ (SOME (locale,
+ (map (Attrib.intern_src (Theory.sign_of thy)) atts,
+ map (map (Attrib.intern_src (Theory.sign_of thy)) o snd o fst) concl)))
+ (name, [])
+ (map (Locale.intern_attrib_elem_expr thy) elems))
+ (map (apfst (apsnd (K []))) concl) int thy;
fun locale_multi_theorem_i k locale (name, atts) elems concl =
global_statement_i (Proof.multi_theorem_i k I ProofContext.export_standard
(SOME (locale, (atts, map (snd o fst) concl)))
(name, []) elems) (map (apfst (apsnd (K []))) concl);
-fun theorem k (a, t) = multi_theorem k I ProofContext.export_standard
- a [] [(("", []), [t])];
-fun theorem_i k (a, t) = multi_theorem_i k I ProofContext.export_standard
- a [] [(("", []), [t])];
+fun theorem k (a, t) =
+ multi_theorem k I ProofContext.export_standard a [] [(("", []), [t])];
+
+fun theorem_i k (a, t) =
+ multi_theorem_i k I ProofContext.export_standard a [] [(("", []), [t])];
fun smart_multi_theorem k NONE a elems =
multi_theorem k I ProofContext.export_standard a elems
@@ -583,7 +587,7 @@
Context.use_let
"val thm = PureThy.get_thm_closure (Context.the_context ());\n\
\val thms = PureThy.get_thms_closure (Context.the_context ());\n\
- \val method: bstring * (Args.src -> Proof.context -> Proof.method) * string"
+ \val method: bstring * (Method.src -> Proof.context -> Proof.method) * string"
"PureIsar.Method.add_method method"
("(" ^ Library.quote name ^ ", " ^ txt ^ ", " ^ Library.quote cmt ^ ")");
@@ -600,8 +604,43 @@
(* add_locale *)
fun add_locale (do_pred, name, import, body) thy =
- Locale.add_locale do_pred name import
- (map (Locale.map_attrib_element (Attrib.multi_attribute thy)) body) thy;
+ Locale.add_locale do_pred name import body thy;
+
+
+(* registration of locale interpretations *)
+
+fun register_globally (((prfx, atts), expr), insts) int thy =
+ let
+ val (thy', propss, activate) =
+ Locale.prep_global_registration (prfx, atts) expr insts thy;
+ fun witness id (thy, thm) = let
+ val thm' = Drule.freeze_all thm;
+ in
+ (Locale.add_global_witness id thm' thy, thm')
+ end;
+ in
+ multi_theorem_i Drule.internalK activate ProofContext.export_plain
+ ("", []) []
+ (map (fn ((n, ps), props) =>
+ ((NameSpace.base n, [witness (n, map Logic.varify ps)]),
+ map (fn prop => (prop, ([], []))) props)) propss) int thy'
+ end;
+
+fun register_locally (((prfx, atts), expr), insts) =
+ ProofHistory.apply (fn state =>
+ let
+ val ctxt = Proof.context_of state;
+ val (ctxt', propss, activate) =
+ Locale.prep_local_registration (prfx, atts) expr insts ctxt;
+ fun witness id (ctxt, thm) = (Locale.add_local_witness id thm ctxt, thm);
+ in
+ state
+ |> Proof.map_context (fn _ => ctxt')
+ |> Proof.have_i (Seq.single o Proof.map_context activate) true
+ (map (fn (id as (n, _), props) => ((NameSpace.base n, [witness id]),
+ map (fn prop => (prop, ([], []))) props)) propss)
+ end);
+
(* theory init and exit *)
@@ -638,38 +677,4 @@
val context = init_context (ThyInfo.quiet_update_thy true);
-
-(* registration of locale interpretation *)
-
-fun register_globally (((prfx, atts), expr), insts) b thy =
- let
- val (thy', propss, activate) = Locale.prep_global_registration
- (prfx, map (Attrib.global_attribute thy) atts) expr insts thy;
- fun witness id (thy, thm) = let
- val thm' = Drule.freeze_all thm;
- in
- (Locale.add_global_witness id thm' thy, thm')
- end;
- in
- multi_theorem_i Drule.internalK activate ProofContext.export_plain
- ("", []) []
- (map (fn ((n, ps), props) =>
- ((NameSpace.base n, [witness (n, map Logic.varify ps)]),
- map (fn prop => (prop, ([], []))) props)) propss) b thy'
- end;
-
-fun register_locally (((prfx, atts), expr), insts) =
- ProofHistory.apply (fn state =>
- let
- val ctxt = Proof.context_of state;
- val (ctxt', propss, activate) = Locale.prep_local_registration
- (prfx, map (Attrib.local_attribute' ctxt) atts) expr insts ctxt;
- fun witness id (ctxt, thm) = (Locale.add_local_witness id thm ctxt, thm);
- in state
- |> Proof.map_context (fn _ => ctxt')
- |> Proof.interpret_i activate Seq.single true
- (map (fn (id as (n, _), props) => ((NameSpace.base n, [witness id]),
- map (fn prop => (prop, ([], []))) props)) propss)
- end);
-
end;
--- a/src/Pure/Isar/locale.ML Wed Apr 13 09:48:41 2005 +0200
+++ b/src/Pure/Isar/locale.ML Wed Apr 13 18:34:22 2005 +0200
@@ -21,15 +21,11 @@
signature LOCALE =
sig
type context
- type multi_attribute
-
- (* Constructors for elem, expr and elem_expr are
- currently only used for inputting locales (outer_parse.ML). *)
- datatype ('typ, 'term, 'fact, 'att) elem =
+ datatype ('typ, 'term, 'fact) elem =
Fixes of (string * 'typ option * mixfix option) list |
- Assumes of ((string * 'att list) * ('term * ('term list * 'term list)) list) list |
- Defines of ((string * 'att list) * ('term * 'term list)) list |
- Notes of ((string * 'att list) * ('fact * 'att list) list) list
+ Assumes of ((string * Attrib.src list) * ('term * ('term list * 'term list)) list) list |
+ Defines of ((string * Attrib.src list) * ('term * 'term list)) list |
+ Notes of ((string * Attrib.src list) * ('fact * Attrib.src list) list) list
datatype expr =
Locale of string |
Rename of expr * string option list |
@@ -38,69 +34,57 @@
datatype 'a elem_expr = Elem of 'a | Expr of expr
(* Abstract interface to locales *)
- type 'att element
- type 'att element_i
+ type element
+ type element_i
type locale
val intern: Sign.sg -> xstring -> string
val cond_extern: Sign.sg -> string -> xstring
val the_locale: theory -> string -> locale
- val map_attrib_element: ('att -> multi_attribute) -> 'att element ->
- multi_attribute element
- val map_attrib_element_i: ('att -> multi_attribute) -> 'att element_i ->
- multi_attribute element_i
- val map_attrib_elem_or_expr: ('att -> multi_attribute) ->
- 'att element elem_expr -> multi_attribute element elem_expr
- val map_attrib_elem_or_expr_i: ('att -> multi_attribute) ->
- 'att element_i elem_expr -> multi_attribute element_i elem_expr
+ val intern_attrib_elem: theory ->
+ ('typ, 'term, 'fact) elem -> ('typ, 'term, 'fact) elem
+ val intern_attrib_elem_expr: theory ->
+ ('typ, 'term, 'fact) elem elem_expr -> ('typ, 'term, 'fact) elem elem_expr
(* Processing of locale statements *)
- val read_context_statement: xstring option ->
- multi_attribute element elem_expr list ->
+ val read_context_statement: xstring option -> element elem_expr list ->
(string * (string list * string list)) list list -> context ->
string option * (cterm list * cterm list) * context * context *
(term * (term list * term list)) list list
- val cert_context_statement: string option ->
- multi_attribute element_i elem_expr list ->
+ val cert_context_statement: string option -> element_i elem_expr list ->
(term * (term list * term list)) list list -> context ->
string option * (cterm list * cterm list) * context * context *
(term * (term list * term list)) list list
(* Diagnostic functions *)
val print_locales: theory -> unit
- val print_locale: theory -> expr -> multi_attribute element list -> unit
+ val print_locale: theory -> expr -> element list -> unit
val print_global_registrations: string -> theory -> unit
+ val print_local_registrations': string -> context -> unit
val print_local_registrations: string -> context -> unit
(* Storing results *)
- val add_locale:
- bool -> bstring -> expr -> multi_attribute element list -> theory -> theory
- val add_locale_i:
- bool -> bstring -> expr -> multi_attribute element_i list ->
- theory -> theory
- val smart_note_thmss:
- string -> (string * 'a) option ->
+ val add_locale: bool -> bstring -> expr -> element list -> theory -> theory
+ val add_locale_i: bool -> bstring -> expr -> element_i list -> theory -> theory
+ val smart_note_thmss: string -> string option ->
((bstring * theory attribute list) * (thm list * theory attribute list) list) list ->
theory -> theory * (bstring * thm list) list
- val note_thmss:
- string -> xstring ->
- ((bstring * multi_attribute list) * (thmref * multi_attribute list) list) list ->
+ val note_thmss: string -> xstring ->
+ ((bstring * Attrib.src list) * (thmref * Attrib.src list) list) list ->
theory -> theory * (bstring * thm list) list
- val note_thmss_i:
- string -> string ->
- ((bstring * multi_attribute list) * (thm list * multi_attribute list) list) list ->
+ val note_thmss_i: string -> string ->
+ ((bstring * Attrib.src list) * (thm list * Attrib.src list) list) list ->
theory -> theory * (bstring * thm list) list
- val add_thmss:
- string -> string -> ((string * thm list) * multi_attribute list) list ->
+ val add_thmss: string -> string -> ((string * thm list) * Attrib.src list) list ->
theory * context -> (theory * context) * (string * thm list) list
(* Locale interpretation *)
val instantiate: string -> string * context attribute list
-> thm list option -> context -> context
val prep_global_registration:
- string * theory attribute list -> expr -> string option list -> theory ->
+ string * Attrib.src list -> expr -> string option list -> theory ->
theory * ((string * term list) * term list) list * (theory -> theory)
val prep_local_registration:
- string * context attribute list -> expr -> string option list -> context ->
+ string * Attrib.src list -> expr -> string option list -> context ->
context * ((string * term list) * term list) list * (context -> context)
val add_global_witness:
string * term list -> thm -> theory -> theory
@@ -118,15 +102,11 @@
type context = ProofContext.context;
-(* Locales store theory attributes (for activation in theories)
- and context attributes (for activation in contexts) *)
-type multi_attribute = theory attribute * context attribute;
-
-datatype ('typ, 'term, 'fact, 'att) elem =
+datatype ('typ, 'term, 'fact) elem =
Fixes of (string * 'typ option * mixfix option) list |
- Assumes of ((string * 'att list) * ('term * ('term list * 'term list)) list) list |
- Defines of ((string * 'att list) * ('term * 'term list)) list |
- Notes of ((string * 'att list) * ('fact * 'att list) list) list;
+ Assumes of ((string * Attrib.src list) * ('term * ('term list * 'term list)) list) list |
+ Defines of ((string * Attrib.src list) * ('term * 'term list)) list |
+ Notes of ((string * Attrib.src list) * ('fact * Attrib.src list) list) list;
datatype expr =
Locale of string |
@@ -138,8 +118,8 @@
datatype 'a elem_expr =
Elem of 'a | Expr of expr;
-type 'att element = (string, string, thmref, 'att) elem;
-type 'att element_i = (typ, term, thm list, 'att) elem;
+type element = (string, string, thmref) elem;
+type element_i = (typ, term, thm list) elem;
type locale =
{predicate: cterm list * thm list,
@@ -153,10 +133,17 @@
(cf. [1], normalisation of locale expressions.)
*)
import: expr, (*dynamic import*)
- elems: (multi_attribute element_i * stamp) list, (*static content*)
+ elems: (element_i * stamp) list, (*static content*)
params: (string * typ option) list * string list} (*all/local params*)
+(* CB: an internal (Int) locale element was either imported or included,
+ an external (Ext) element appears directly in the locale text. *)
+
+datatype ('a, 'b) int_ext = Int of 'a | Ext of 'b;
+
+
+
(** theory data **)
structure Termlisttab = TableFun(type key = term list
@@ -166,7 +153,7 @@
struct
val name = "Isar/locales";
type T = NameSpace.T * locale Symtab.table *
- ((string * theory attribute list) * thm list) Termlisttab.table
+ ((string * Attrib.src list) * thm list) Termlisttab.table
Symtab.table;
(* 1st entry: locale namespace,
2nd entry: locales of the theory,
@@ -202,7 +189,7 @@
structure LocalLocalesArgs =
struct
val name = "Isar/locales";
- type T = ((string * context attribute list) * thm list) Termlisttab.table
+ type T = ((string * Args.src list) * thm list) Termlisttab.table
Symtab.table;
(* registrations: theorems instantiating locale assumptions,
with prefix and attributes, indexed by locale name and parameter
@@ -343,21 +330,23 @@
(* printing of registrations *)
-fun gen_print_registrations get_regs get_sign msg loc thy_ctxt =
+fun gen_print_registrations get_regs mk_ctxt msg loc thy_ctxt =
let
- val sg = get_sign thy_ctxt;
+ val ctxt = mk_ctxt thy_ctxt;
+ val thy = ProofContext.theory_of ctxt;
+ val sg = Theory.sign_of thy;
+
+ val prt_term = Pretty.quote o ProofContext.pretty_term ctxt;
+ val prt_atts = Args.pretty_attribs ctxt;
+ fun prt_inst (ts, (("", []), thms)) =
+ Pretty.enclose "(" ")" (Pretty.breaks (map prt_term ts))
+ | prt_inst (ts, ((prfx, atts), thms)) =
+ Pretty.block (Pretty.breaks
+ (Pretty.str prfx :: prt_atts atts @ [Pretty.str ":", Pretty.brk 1,
+ Pretty.enclose "(" ")" (Pretty.breaks (map prt_term ts))]));
+
val loc_int = intern sg loc;
val regs = get_regs thy_ctxt;
- val prt_term = Pretty.quote o Sign.pretty_term sg;
- fun prt_inst (ts, ((prfx, _), thms)) =
- let
- val pp_ts = Pretty.enclose "(" ")"
- (Pretty.breaks (map prt_term ts));
- in
- if prfx = "" then Pretty.block [pp_ts]
- else Pretty.block
- [Pretty.str prfx, Pretty.str ":", Pretty.brk 1, pp_ts]
- end;
val loc_regs = Symtab.lookup (regs, loc_int);
in
(case loc_regs of
@@ -369,10 +358,10 @@
val print_global_registrations =
gen_print_registrations (#3 o GlobalLocalesData.get)
- Theory.sign_of "theory";
+ ProofContext.init "theory";
val print_local_registrations' =
gen_print_registrations LocalLocalesData.get
- ProofContext.sign_of "context";
+ I "context";
fun print_local_registrations loc ctxt =
(print_global_registrations loc (ProofContext.theory_of ctxt);
print_local_registrations' loc ctxt);
@@ -399,10 +388,47 @@
(** primitives **)
+(* map elements *)
+
+fun map_elem {name, var, typ, term, fact, attrib} =
+ fn Fixes fixes => Fixes (fixes |> map (fn (x, T, mx) =>
+ let val (x', mx') = var (x, mx) in (x', Option.map typ T, mx') end))
+ | Assumes asms => Assumes (asms |> map (fn ((a, atts), propps) =>
+ ((name a, map attrib atts), propps |> map (fn (t, (ps, qs)) =>
+ (term t, (map term ps, map term qs))))))
+ | Defines defs => Defines (defs |> map (fn ((a, atts), (t, ps)) =>
+ ((name a, map attrib atts), (term t, map term ps))))
+ | Notes facts => Notes (facts |> map (fn ((a, atts), bs) =>
+ ((name a, map attrib atts), bs |> map (fn (ths, btts) => (fact ths, map attrib btts)))));
+
+fun map_values typ term thm = map_elem
+ {name = I, var = I, typ = typ, term = term, fact = map thm,
+ attrib = Args.map_values I typ term thm};
+
+
+(* map attributes *)
+
+fun map_attrib_specs f = map (apfst (apsnd (map f)));
+fun map_attrib_facts f = map (apfst (apsnd (map f)) o apsnd (map (apsnd (map f))));
+
+fun map_attrib_elem f = map_elem {name = I, var = I, typ = I, term = I, fact = I, attrib = f};
+
+fun intern_attrib_elem thy = map_attrib_elem (Attrib.intern_src (Theory.sign_of thy));
+
+fun intern_attrib_elem_expr thy (Elem elem) = Elem (intern_attrib_elem thy elem)
+ | intern_attrib_elem_expr _ (Expr expr) = Expr expr;
+
+
(* renaming *)
fun rename ren x = getOpt (assoc_string (ren, x), x);
+fun rename_var ren (x, mx) =
+ let val x' = rename ren x in
+ if x = x' then (x, mx)
+ else (x', if mx = NONE then mx else SOME Syntax.NoSyn) (*drop syntax*)
+ end;
+
fun rename_term ren (Free (x, T)) = Free (rename ren x, T)
| rename_term ren (t $ u) = rename_term ren t $ rename_term ren u
| rename_term ren (Abs (x, T, t)) = Abs (x, T, rename_term ren t)
@@ -427,16 +453,9 @@
|> (fn th' => Drule.implies_elim_list th' (map (Thm.assume o cert o rename_term ren) hyps))
end;
-fun rename_elem ren (Fixes fixes) = Fixes (fixes |> map (fn (x, T, mx) =>
- let val x' = rename ren x in
- if x = x' then (x, T, mx)
- else (x', T, if mx = NONE then mx else SOME Syntax.NoSyn) (*drop syntax*)
- end))
- | rename_elem ren (Assumes asms) = Assumes (map (apsnd (map (fn (t, (ps, qs)) =>
- (rename_term ren t, (map (rename_term ren) ps, map (rename_term ren) qs))))) asms)
- | rename_elem ren (Defines defs) = Defines (map (apsnd (fn (t, ps) =>
- (rename_term ren t, map (rename_term ren) ps))) defs)
- | rename_elem ren (Notes facts) = Notes (map (apsnd (map (apfst (map (rename_thm ren))))) facts);
+fun rename_elem ren =
+ map_values I (rename_term ren) (rename_thm ren) o
+ map_elem {name = I, typ = I, term = I, fact = I, attrib = I, var = rename_var ren};
fun rename_facts prfx elem =
let
@@ -481,14 +500,8 @@
(map (Thm.assume o cert o inst_term env') hyps))
end;
-fun inst_elem _ env (Fixes fixes) =
- Fixes (map (fn (x, T, mx) => (x, Option.map (inst_type env) T, mx)) fixes)
- | inst_elem _ env (Assumes asms) = Assumes (map (apsnd (map (fn (t, (ps, qs)) =>
- (inst_term env t, (map (inst_term env) ps, map (inst_term env) qs))))) asms)
- | inst_elem _ env (Defines defs) = Defines (map (apsnd (fn (t, ps) =>
- (inst_term env t, map (inst_term env) ps))) defs)
- | inst_elem ctxt env (Notes facts) =
- Notes (map (apsnd (map (apfst (map (inst_thm ctxt env))))) facts);
+fun inst_elem ctxt env =
+ map_values (inst_type env) (inst_term env) (inst_thm ctxt env);
(* term and type instantiation, variant using symbol tables *)
@@ -843,36 +856,6 @@
end;
-(* attributes *)
-
-local
-
-fun read_att attrib (x, srcs) = (x, map attrib srcs)
-
-(* CB: Map attrib over
- * A context element: add attrib to attribute lists of assumptions,
- definitions and facts (on both sides for facts).
- * Locale expression: no effect. *)
-
-fun gen_map_attrib_elem _ (Fixes fixes) = Fixes fixes
- | gen_map_attrib_elem attrib (Assumes asms) = Assumes (map (apfst (read_att attrib)) asms)
- | gen_map_attrib_elem attrib (Defines defs) = Defines (map (apfst (read_att attrib)) defs)
- | gen_map_attrib_elem attrib (Notes facts) =
- Notes (map (apfst (read_att attrib) o apsnd (map (read_att attrib))) facts)
-
-fun gen_map_attrib_elem_expr attrib (Elem elem) = Elem (gen_map_attrib_elem attrib elem)
- | gen_map_attrib_elem_expr _ (Expr expr) = Expr expr;
-
-in
-
-val map_attrib_element = gen_map_attrib_elem;
-val map_attrib_element_i = gen_map_attrib_elem;
-val map_attrib_elem_or_expr = gen_map_attrib_elem_expr;
-val map_attrib_elem_or_expr_i = gen_map_attrib_elem_expr;
-
-end;
-
-
(* activate elements *)
local
@@ -888,29 +871,26 @@
((ctxt |> ProofContext.add_fixes fixes, axs), [])
| activate_elem _ ((ctxt, axs), Assumes asms) =
let
- (* extract context attributes *)
- val (Assumes asms) = map_attrib_element_i snd (Assumes asms);
- val ts = List.concat (map (map #1 o #2) asms);
- val (ps,qs) = splitAt (length ts, axs);
+ val asms' = map_attrib_specs (Attrib.context_attribute_i ctxt) asms;
+ val ts = List.concat (map (map #1 o #2) asms');
+ val (ps, qs) = splitAt (length ts, axs);
val (ctxt', _) =
ctxt |> ProofContext.fix_frees ts
- |> ProofContext.assume_i (export_axioms ps) asms;
+ |> ProofContext.assume_i (export_axioms ps) asms';
in ((ctxt', qs), []) end
| activate_elem _ ((ctxt, axs), Defines defs) =
let
- (* extract context attributes *)
- val (Defines defs) = map_attrib_element_i snd (Defines defs);
+ val defs' = map_attrib_specs (Attrib.context_attribute_i ctxt) defs;
val (ctxt', _) =
ctxt |> ProofContext.assume_i ProofContext.export_def
- (defs |> map (fn ((name, atts), (t, ps)) =>
+ (defs' |> map (fn ((name, atts), (t, ps)) =>
let val (c, t') = ProofContext.cert_def ctxt t
in ((if name = "" then Thm.def_name c else name, atts), [(t', (ps, []))]) end))
in ((ctxt', axs), []) end
| activate_elem is_ext ((ctxt, axs), Notes facts) =
let
- (* extract context attributes *)
- val (Notes facts) = map_attrib_element_i snd (Notes facts);
- val (ctxt', res) = ctxt |> ProofContext.note_thmss_i facts
+ val facts' = map_attrib_facts (Attrib.context_attribute_i ctxt) facts;
+ val (ctxt', res) = ctxt |> ProofContext.note_thmss_i facts';
in ((ctxt', axs), if is_ext then res else []) end;
fun activate_elems (((name, ps), axs), elems) ctxt =
@@ -930,7 +910,8 @@
let
val elems = map (prep_facts ctxt) raw_elems;
val (ctxt', res) = apsnd List.concat (activate_elems (((name, ps), axs), elems) ctxt);
- in (ctxt', (((name, ps), elems), res)) end);
+ val elems' = map (map_attrib_elem Args.closure) elems;
+ in (ctxt', (((name, ps), elems'), res)) end);
in
@@ -942,12 +923,18 @@
assumptions use the axioms in the identifiers to set up exporters
in ctxt'. elemss' does not contain identifiers and is obtained
from elemss and the intermediate context with prep_facts.
- If get_facts or get_facts_i is used for prep_facts, these also remove
+ If read_facts or cert_facts is used for prep_facts, these also remove
the internal/external markers from elemss. *)
fun activate_facts prep_facts arg =
apsnd (apsnd List.concat o Library.split_list) (activate_elemss prep_facts arg);
+fun activate_note prep_facts (ctxt, args) =
+ let
+ val (ctxt', ([(_, [Notes args'])], facts)) =
+ activate_facts prep_facts (ctxt, [((("", []), []), [Ext (Notes args)])]);
+ in (ctxt', (args', facts)) end;
+
end;
@@ -992,11 +979,6 @@
(* propositions and bindings *)
-(* CB: an internal (Int) locale element was either imported or included,
- an external (Ext) element appears directly in the locale. *)
-
-datatype ('a, 'b) int_ext = Int of 'a | Ext of 'b;
-
(* flatten (ids, expr) normalises expr (which is either a locale
expression or a single context element) wrt.
to the list ids of already accumulated identifiers.
@@ -1248,27 +1230,28 @@
end;
-(* facts *)
+(* facts and attributes *)
local
-fun prep_name ctxt (name, atts) =
+fun prep_name ctxt name =
(* CB: reject qualified theorem names in locale declarations *)
if NameSpace.is_qualified name then
raise ProofContext.CONTEXT ("Illegal qualified name: " ^ quote name, ctxt)
- else (name, atts);
+ else name;
-fun prep_facts _ _ (Int elem) = elem
- | prep_facts _ _ (Ext (Fixes fixes)) = Fixes fixes
- | prep_facts _ ctxt (Ext (Assumes asms)) = Assumes (map (apfst (prep_name ctxt)) asms)
- | prep_facts _ ctxt (Ext (Defines defs)) = Defines (map (apfst (prep_name ctxt)) defs)
- | prep_facts get ctxt (Ext (Notes facts)) = Notes (facts |> map (fn (a, bs) =>
- (prep_name ctxt a, map (apfst (get ctxt)) bs)));
+fun prep_facts _ _ ctxt (Int elem) =
+ map_values I I (Thm.transfer (ProofContext.theory_of ctxt)) elem
+ | prep_facts get intern ctxt (Ext elem) = elem |> map_elem
+ {var = I, typ = I, term = I,
+ name = prep_name ctxt,
+ fact = get ctxt,
+ attrib = Args.assignable o intern (ProofContext.sign_of ctxt)};
in
-fun get_facts x = prep_facts ProofContext.get_thms x;
-fun get_facts_i x = prep_facts (K I) x;
+fun read_facts x = prep_facts ProofContext.get_thms Attrib.intern_src x;
+fun cert_facts x = prep_facts (K I) (K I) x;
end;
@@ -1312,8 +1295,8 @@
((((import_ctxt, import_elemss), (ctxt, elemss)), (parms, spec, defs)), (cstmt, concl))
end;
-val gen_context = prep_context_statement intern_expr read_elemss get_facts;
-val gen_context_i = prep_context_statement (K I) cert_elemss get_facts_i;
+val gen_context = prep_context_statement intern_expr read_elemss read_facts;
+val gen_context_i = prep_context_statement (K I) cert_elemss cert_facts;
fun gen_statement prep_locale prep_ctxt raw_locale elems concl ctxt =
let
@@ -1453,6 +1436,12 @@
(map (Thm.assume o cert o inst_term Tenv') hyps))
end;
+ val inst_type' = inst_type Tenv';
+
+ val inst_term' = Term.subst_atomic
+ (map (pairself term_of) ((cparams' @ cdefined') ~~ (cargs @ cdefining)))
+ o inst_term Tenv';
+
fun inst_thm' thm =
let
(* not all axs are normally applicable *)
@@ -1479,7 +1468,12 @@
else inst_thm
in implies_elim_list th (map mk hyps)
end;
- in thm''' end;
+ in thm''' end
+ handle THM (msg, n, thms) => error ("Exception THM " ^
+ string_of_int n ^ " raised\n" ^
+ "Note: instantiate does not support old-style locales \
+ \declared with (open)\n" ^ msg ^ "\n" ^
+ cat_lines (map string_of_thm thms));
val prefix_fact =
if prfx = "" then I
@@ -1489,15 +1483,12 @@
fun inst_elem (ctxt, (Ext _)) = ctxt
| inst_elem (ctxt, (Int (Notes facts))) =
(* instantiate fact *)
- let (* extract context attributes *)
- val (Notes facts) = map_attrib_element_i snd (Notes facts);
+ let
+ val facts = facts |> map_attrib_facts
+ (Attrib.context_attribute_i ctxt o
+ Args.map_values I inst_type' inst_term' inst_thm');
val facts' =
map (apsnd (map (apfst (map inst_thm')))) facts
- handle THM (msg, n, thms) => error ("Exception THM " ^
- string_of_int n ^ " raised\n" ^
- "Note: instantiate does not support old-style locales \
- \declared with (open)\n" ^ msg ^ "\n" ^
- cat_lines (map string_of_thm thms))
(* rename fact *)
val facts'' = map (apfst (apfst prefix_fact)) facts'
(* add attributes *)
@@ -1530,6 +1521,7 @@
val prt_typ = Pretty.quote o ProofContext.pretty_typ ctxt;
val prt_term = Pretty.quote o ProofContext.pretty_term ctxt;
val prt_thm = Pretty.quote o ProofContext.pretty_thm ctxt;
+ val prt_atts = Args.pretty_attribs ctxt;
fun prt_syn syn =
let val s = (case syn of NONE => "(structure)" | SOME mx => Syntax.string_of_mixfix mx)
@@ -1538,19 +1530,28 @@
prt_typ T :: Pretty.brk 1 :: prt_syn syn)
| prt_fix (x, NONE, syn) = Pretty.block (Pretty.str x :: Pretty.brk 1 :: prt_syn syn);
- fun prt_name "" = [Pretty.brk 1]
- | prt_name name = [Pretty.str (ProofContext.cond_extern ctxt name ^ ":"), Pretty.brk 1];
- fun prt_asm ((a, _), ts) = Pretty.block (prt_name a @ Pretty.breaks (map (prt_term o fst) ts));
- fun prt_def ((a, _), (t, _)) = Pretty.block (prt_name a @ [prt_term t]);
- fun prt_fact ((a, _), ths) = Pretty.block
- (prt_name a @ Pretty.breaks (map prt_thm (List.concat (map fst ths))));
+ fun prt_name name = Pretty.str (ProofContext.cond_extern ctxt name);
+ fun prt_name_atts (name, atts) =
+ if name = "" andalso null atts then []
+ else [Pretty.block (Pretty.breaks (prt_name name :: prt_atts atts @ [Pretty.str ":"]))];
+
+ fun prt_asm (a, ts) =
+ Pretty.block (Pretty.breaks (prt_name_atts a @ map (prt_term o fst) ts));
+ fun prt_def (a, (t, _)) =
+ Pretty.block (Pretty.breaks (prt_name_atts a @ [prt_term t]));
+
+ fun prt_fact (ths, []) = map prt_thm ths
+ | prt_fact (ths, atts) =
+ Pretty.enclose "(" ")" (Pretty.breaks (map prt_thm ths)) :: prt_atts atts;
+ fun prt_note (a, ths) =
+ Pretty.block (Pretty.breaks (List.concat (prt_name_atts a :: map prt_fact ths)));
fun items _ [] = []
| items prfx (x :: xs) = Pretty.block [Pretty.str prfx, Pretty.brk 1, x] :: items " and" xs;
fun prt_elem (Fixes fixes) = items "fixes" (map prt_fix fixes)
| prt_elem (Assumes asms) = items "assumes" (map prt_asm asms)
| prt_elem (Defines defs) = items "defines" (map prt_def defs)
- | prt_elem (Notes facts) = items "notes" (map prt_fact facts);
+ | prt_elem (Notes facts) = items "notes" (map prt_note facts);
in
Pretty.big_list "context elements:" (map (Pretty.chunks o prt_elem) all_elems)
|> Pretty.writeln
@@ -1645,8 +1646,8 @@
val ids' = map (apsnd vinst_names) ids;
val prems = List.concat (map (snd o valOf o get_global_registration thy) ids');
val args' = map (fn ((n, atts), [(ths, [])]) =>
- ((if prfx = "" orelse n = "" then ""
- else NameSpace.pack [prfx, n], map fst atts @ atts2),
+ ((if prfx = "" orelse n = "" then "" else NameSpace.pack [prfx, n],
+ map (Attrib.global_attribute_i thy) (atts @ atts2)),
[(map (Drule.standard o Drule.satisfy_hyps prems o inst_tab_thm sign (inst, tinst)) ths, [])]))
args;
in
@@ -1656,8 +1657,7 @@
fun smart_note_thmss kind NONE = PureThy.note_thmss_i (Drule.kind kind)
- | smart_note_thmss kind (SOME (loc, _)) = note_thmss_qualified kind loc;
- (* CB: only used in Proof.finish_global. *)
+ | smart_note_thmss kind (SOME loc) = note_thmss_qualified kind loc;
end;
@@ -1668,54 +1668,48 @@
fun put_facts loc args thy =
let
val {predicate, import, elems, params} = the_locale thy loc;
- val note = Notes (map (fn ((a, more_atts), th_atts) =>
- ((a, more_atts), map (apfst (map (curry Thm.name_thm a))) th_atts)) args);
- in thy |> put_locale loc {predicate = predicate, import = import, elems = elems @ [(note, stamp ())],
- params = params} end;
+ val note = Notes (map (fn ((a, atts), bs) =>
+ ((a, atts), map (apfst (map (curry Thm.name_thm a))) bs)) args);
+ in
+ thy |> put_locale loc {predicate = predicate, import = import,
+ elems = elems @ [(note, stamp ())], params = params}
+ end;
(* add theorem to locale and theory,
base for theorems (in loc) and declare (in loc) *)
-fun gen_note_thmss prep_locale get_thms kind raw_loc raw_args thy =
+fun gen_note_thmss prep_locale prep_facts kind raw_loc args thy =
let
val thy_ctxt = ProofContext.init thy;
val loc = prep_locale (Theory.sign_of thy) raw_loc;
- val (_, (stmt, _), loc_ctxt, _, _) =
- cert_context_statement (SOME loc) [] [] thy_ctxt;
- val args = map (apsnd (map (apfst (get_thms loc_ctxt)))) raw_args;
- (* convert multi attributes to context attributes for
- ProofContext.note_thmss_i *)
- val args'' = args
- |> map (apfst (apsnd (map snd)))
- |> map (apsnd (map (apsnd (map snd))));
+ val (_, (stmt, _), loc_ctxt, _, _) = cert_context_statement (SOME loc) [] [] thy_ctxt;
val export = ProofContext.export_standard stmt loc_ctxt thy_ctxt;
- val results = map (map export o #2) (#2 (ProofContext.note_thmss_i args'' loc_ctxt));
- val args' = map (rpair [] o #1 o #1) args ~~ map (single o Thm.no_attributes) results;
+
+ val (args', facts) = #2 (activate_note prep_facts (loc_ctxt, args));
+ val facts' =
+ map (rpair [] o #1 o #1) args' ~~
+ map (single o Thm.no_attributes o map export o #2) facts;
in
thy
- |> put_facts loc args
- |> note_thmss_registrations kind loc args
- |> note_thmss_qualified kind loc args'
+ |> put_facts loc args'
+ |> note_thmss_registrations kind loc args'
+ |> note_thmss_qualified kind loc facts'
end;
in
-(* CB: note_thmss(_i) is the base for the Isar commands
- "theorems (in loc)" and "declare (in loc)". *)
-
-val note_thmss = gen_note_thmss intern ProofContext.get_thms;
-val note_thmss_i = gen_note_thmss (K I) (K I);
-
-(* CB: only used in Proof.finish_global. *)
+val note_thmss = gen_note_thmss intern read_facts;
+val note_thmss_i = gen_note_thmss (K I) cert_facts;
fun add_thmss kind loc args (thy, ctxt) =
let
- val args' = map (fn ((a, ths), atts) => ((a, atts), [(ths, [])])) args;
- val thy' = put_facts loc args' thy;
- val thy'' = note_thmss_registrations kind loc args' thy';
- val (ctxt', (_, facts')) =
- activate_facts (K I) (ctxt, [((("", []), []), [Notes args'])]);
- in ((thy'', ctxt'), facts') end;
+ val (ctxt', (args', facts)) = activate_note cert_facts
+ (ctxt, args |> map (fn ((a, ths), atts) => ((a, atts), [(ths, [])])));
+ val thy' =
+ thy
+ |> put_facts loc args'
+ |> note_thmss_registrations kind loc args';
+ in ((thy', ctxt'), facts) end;
end;
@@ -1803,18 +1797,18 @@
- notes elements are lifted
*)
-fun change_elem _ (axms, Assumes asms) =
+fun change_elem (axms, Assumes asms) =
apsnd Notes ((axms, asms) |> foldl_map (fn (axs, (a, spec)) =>
let val (ps,qs) = splitAt(length spec, axs)
in (qs, (a, [(ps, [])])) end))
- | change_elem f (axms, Notes facts) = (axms, Notes (map (apsnd (map (apfst (map f)))) facts))
- | change_elem _ e = e;
+ | change_elem e = e;
(* CB: changes only "new" elems, these have identifier ("", _). *)
fun change_elemss axioms elemss = (axioms, elemss) |> foldl_map
(fn (axms, (id as ("", _), es)) =>
- foldl_map (change_elem (Drule.satisfy_hyps axioms)) (axms, es) |> apsnd (pair id)
+ foldl_map change_elem (axms, map (map_values I I (Drule.satisfy_hyps axioms)) es)
+ |> apsnd (pair id)
| x => x) |> #2;
in
@@ -1944,14 +1938,13 @@
fun activate_facts_elem _ _ _ _ (thy_ctxt, Fixes _) = thy_ctxt
| activate_facts_elem _ _ _ _ (thy_ctxt, Assumes _) = thy_ctxt
| activate_facts_elem _ _ _ _ (thy_ctxt, Defines _) = thy_ctxt
- | activate_facts_elem note_thmss which
+ | activate_facts_elem note_thmss attrib
disch (prfx, atts) (thy_ctxt, Notes facts) =
let
- (* extract theory or context attributes *)
- val (Notes facts) = map_attrib_element_i which (Notes facts);
- (* add attributes from registration *)
- val facts' = map (apfst (apsnd (fn a => a @ atts))) facts;
- (* discharge hyps *)
+ val reg_atts = map (attrib thy_ctxt) atts;
+ val facts = map_attrib_facts (attrib thy_ctxt) facts;
+ val facts' = map (apfst (apsnd (fn a => a @ reg_atts))) facts;
+ (* discharge hyps *)
val facts'' = map (apsnd (map (apfst (map disch)))) facts';
(* prefix names *)
val facts''' = map (apfst (apfst (fn name =>
@@ -1961,25 +1954,25 @@
fst (note_thmss prfx facts''' thy_ctxt)
end;
-fun activate_facts_elems get_reg note_thmss which
+fun activate_facts_elems get_reg note_thmss attrib
disch (thy_ctxt, (id, elems)) =
let
val ((prfx, atts2), _) = valOf (get_reg thy_ctxt id)
handle Option => error ("(internal) unknown registration of " ^
quote (fst id) ^ " while activating facts.");
in
- Library.foldl (activate_facts_elem note_thmss which
+ Library.foldl (activate_facts_elem note_thmss attrib
disch (prfx, atts2)) (thy_ctxt, elems)
end;
-fun gen_activate_facts_elemss get_reg note_thmss which standard
+fun gen_activate_facts_elemss get_reg note_thmss attrib standard
all_elemss new_elemss thy_ctxt =
let
val prems = List.concat (List.mapPartial (fn (id, _) =>
Option.map snd (get_reg thy_ctxt id)
handle Option => error ("(internal) unknown registration of " ^
quote (fst id) ^ " while activating facts.")) all_elemss);
- in Library.foldl (activate_facts_elems get_reg note_thmss which
+ in Library.foldl (activate_facts_elems get_reg note_thmss attrib
(standard o Drule.satisfy_hyps prems)) (thy_ctxt, new_elemss) end;
val global_activate_facts_elemss = gen_activate_facts_elemss
@@ -1987,11 +1980,11 @@
get_global_registration thy (name, map Logic.varify ps))
(fn prfx => PureThy.note_thmss_accesses_i (global_accesses prfx)
(Drule.kind ""))
- fst Drule.standard;
+ Attrib.global_attribute_i Drule.standard;
val local_activate_facts_elemss = gen_activate_facts_elemss
get_local_registration
(fn prfx => ProofContext.note_thmss_accesses_i (local_accesses prfx))
- snd I;
+ Attrib.context_attribute_i I;
fun gen_prep_registration mk_ctxt is_local read_terms test_reg put_reg activate
attn expr insts thy_ctxt =
@@ -2072,9 +2065,12 @@
(* remove fragments already registered with theory or context *)
val new_inst_elemss = List.filter (fn (id, _) =>
not (test_reg thy_ctxt id)) inst_elemss;
+ val new_ids = map #1 new_inst_elemss;
val propss = extract_asms_elemss new_inst_elemss;
+ val bind_attrib = Attrib.crude_closure ctxt o Args.assignable;
+ val attn' = apsnd (map (bind_attrib o Attrib.intern_src sign)) attn;
(** add registrations to theory or context,
without theorems, these are added after the proof **)
@@ -2083,7 +2079,7 @@
registration. *)
val thy_ctxt' = Library.foldl (fn (thy_ctxt, (id, _)) =>
- put_reg id attn thy_ctxt) (thy_ctxt, new_inst_elemss);
+ put_reg id attn' thy_ctxt) (thy_ctxt, new_inst_elemss);
in (thy_ctxt', propss, activate inst_elemss new_inst_elemss) end;
--- a/src/Pure/Isar/method.ML Wed Apr 13 09:48:41 2005 +0200
+++ b/src/Pure/Isar/method.ML Wed Apr 13 18:34:22 2005 +0200
@@ -15,6 +15,7 @@
signature METHOD =
sig
include BASIC_METHOD
+ type src
val trace: Proof.context -> thm list -> unit
val RAW_METHOD: (thm list -> tactic) -> Proof.method
val RAW_METHOD_CASES:
@@ -48,37 +49,37 @@
val set_tactic: (Proof.context -> thm list -> tactic) -> unit
val tactic: string -> Proof.context -> Proof.method
exception METHOD_FAIL of (string * Position.T) * exn
- val method: theory -> Args.src -> Proof.context -> Proof.method
- val add_method: bstring * (Args.src -> Proof.context -> Proof.method) * string
+ val method: theory -> src -> Proof.context -> Proof.method
+ val add_method: bstring * (src -> Proof.context -> Proof.method) * string
-> theory -> theory
- val add_methods: (bstring * (Args.src -> Proof.context -> Proof.method) * string) list
+ val add_methods: (bstring * (src -> Proof.context -> Proof.method) * string) list
-> theory -> theory
val syntax: (Proof.context * Args.T list -> 'a * (Proof.context * Args.T list)) ->
- Args.src -> Proof.context -> Proof.context * 'a
+ src -> Proof.context -> Proof.context * 'a
val simple_args: (Args.T list -> 'a * Args.T list)
- -> ('a -> Proof.context -> Proof.method) -> Args.src -> Proof.context -> Proof.method
- val ctxt_args: (Proof.context -> Proof.method) -> Args.src -> Proof.context -> Proof.method
- val no_args: Proof.method -> Args.src -> Proof.context -> Proof.method
+ -> ('a -> Proof.context -> Proof.method) -> src -> Proof.context -> Proof.method
+ val ctxt_args: (Proof.context -> Proof.method) -> src -> Proof.context -> Proof.method
+ val no_args: Proof.method -> src -> Proof.context -> Proof.method
type modifier
val sectioned_args: (Proof.context * Args.T list -> 'a * (Proof.context * Args.T list)) ->
(Args.T list -> modifier * Args.T list) list ->
- ('a -> Proof.context -> 'b) -> Args.src -> Proof.context -> 'b
+ ('a -> Proof.context -> 'b) -> src -> Proof.context -> 'b
val bang_sectioned_args:
(Args.T list -> modifier * Args.T list) list ->
- (thm list -> Proof.context -> 'a) -> Args.src -> Proof.context -> 'a
+ (thm list -> Proof.context -> 'a) -> src -> Proof.context -> 'a
val bang_sectioned_args':
(Args.T list -> modifier * Args.T list) list ->
(Proof.context * Args.T list -> 'a * (Proof.context * Args.T list)) ->
- ('a -> thm list -> Proof.context -> 'b) -> Args.src -> Proof.context -> 'b
+ ('a -> thm list -> Proof.context -> 'b) -> src -> Proof.context -> 'b
val only_sectioned_args:
(Args.T list -> modifier * Args.T list) list ->
- (Proof.context -> 'a) -> Args.src -> Proof.context -> 'a
- val thms_ctxt_args: (thm list -> Proof.context -> 'a) -> Args.src -> Proof.context -> 'a
- val thms_args: (thm list -> 'a) -> Args.src -> Proof.context -> 'a
- val thm_args: (thm -> 'a) -> Args.src -> Proof.context -> 'a
+ (Proof.context -> 'a) -> src -> Proof.context -> 'a
+ val thms_ctxt_args: (thm list -> Proof.context -> 'a) -> src -> Proof.context -> 'a
+ val thms_args: (thm list -> 'a) -> src -> Proof.context -> 'a
+ val thm_args: (thm -> 'a) -> src -> Proof.context -> 'a
datatype text =
Basic of (Proof.context -> Proof.method) |
- Source of Args.src |
+ Source of src |
Then of text list |
Orelse of text list |
Try of text |
@@ -107,19 +108,21 @@
theory * ((string * string) * (string * thm list) list)
val global_done_proof: Proof.state -> theory * ((string * string) * (string * thm list) list)
val goal_args: (Args.T list -> 'a * Args.T list) -> ('a -> int -> tactic)
- -> Args.src -> Proof.context -> Proof.method
+ -> src -> Proof.context -> Proof.method
val goal_args': (Proof.context * Args.T list -> 'a * (Proof.context * Args.T list))
- -> ('a -> int -> tactic) -> Args.src -> Proof.context -> Proof.method
+ -> ('a -> int -> tactic) -> src -> Proof.context -> Proof.method
val goal_args_ctxt: (Args.T list -> 'a * Args.T list) -> (Proof.context -> 'a -> int -> tactic)
- -> Args.src -> Proof.context -> Proof.method
+ -> src -> Proof.context -> Proof.method
val goal_args_ctxt': (Proof.context * Args.T list -> 'a * (Proof.context * Args.T list))
- -> (Proof.context -> 'a -> int -> tactic) -> Args.src -> Proof.context -> Proof.method
+ -> (Proof.context -> 'a -> int -> tactic) -> src -> Proof.context -> Proof.method
val setup: (theory -> theory) list
end;
structure Method: METHOD =
struct
+type src = Args.src;
+
(** proof methods **)
@@ -374,7 +377,7 @@
| some => some)
| types' xi = types xi;
fun internal x = isSome (types' (x, ~1));
- val used = Term.add_term_tvarnames (Thm.prop_of st $ Thm.prop_of thm, []);
+ val used = Drule.add_used thm (Drule.add_used st []);
val (ts, envT) =
ProofContext.read_termTs_schematic ctxt internal types' sorts used (ss ~~ Ts);
val cenvT = map (apsnd (Thm.ctyp_of sign)) (envT @ Tinsts_env);
@@ -505,7 +508,7 @@
val name = "Isar/methods";
type T =
{space: NameSpace.T,
- meths: (((Args.src -> Proof.context -> Proof.method) * string) * stamp) Symtab.table};
+ meths: (((src -> Proof.context -> Proof.method) * string) * stamp) Symtab.table};
val empty = {space = NameSpace.empty, meths = Symtab.empty};
val copy = I;
@@ -692,7 +695,7 @@
datatype text =
Basic of (Proof.context -> Proof.method) |
- Source of Args.src |
+ Source of src |
Then of text list |
Orelse of text list |
Try of text |
--- a/src/Pure/Isar/outer_parse.ML Wed Apr 13 09:48:41 2005 +0200
+++ b/src/Pure/Isar/outer_parse.ML Wed Apr 13 18:34:22 2005 +0200
@@ -14,9 +14,7 @@
val triple1: ('a * 'b) * 'c -> 'a * 'b * 'c
val triple2: 'a * ('b * 'c) -> 'a * 'b * 'c
val triple_swap: ('a * 'b) * 'c -> ('a * 'c) * 'b
- val $$$ : string -> token list -> string * token list
- val semicolon: token list -> string * token list
- val underscore: token list -> string * token list
+ val not_eof: token list -> token * token list
val position: (token list -> 'a * 'b) -> token list -> ('a * Position.T) * 'b
val command: token list -> string * token list
val keyword: token list -> string * token list
@@ -31,7 +29,10 @@
val verbatim: token list -> string * token list
val sync: token list -> string * token list
val eof: token list -> string * token list
- val not_eof: token list -> token * token list
+ val $$$ : string -> token list -> string * token list
+ val semicolon: token list -> string * token list
+ val underscore: token list -> string * token list
+ val maybe: (token list -> 'a * token list) -> token list -> 'a option * token list
val opt_unit: token list -> unit * token list
val opt_keyword: string -> token list -> bool * token list
val nat: token list -> int * token list
@@ -45,7 +46,6 @@
val xname: token list -> xstring * token list
val text: token list -> string * token list
val path: token list -> Path.T * token list
- val uname: token list -> string option * token list
val sort: token list -> string * token list
val arity: token list -> (string list * string) * token list
val type_args: token list -> string list * token list
@@ -61,19 +61,19 @@
val propp: token list -> (string * (string list * string list)) * token list
val termp: token list -> (string * string list) * token list
val arguments: token list -> Args.T list * token list
- val attribs: token list -> Args.src list * token list
- val opt_attribs: token list -> Args.src list * token list
- val thm_name: string -> token list -> (bstring * Args.src list) * token list
- val opt_thm_name: string -> token list -> (bstring * Args.src list) * token list
- val spec_name: token list -> ((bstring * string) * Args.src list) * token list
- val spec_opt_name: token list -> ((bstring * string) * Args.src list) * token list
- val xthm: token list -> (thmref * Args.src list) * token list
- val xthms1: token list -> (thmref * Args.src list) list * token list
+ val attribs: token list -> Attrib.src list * token list
+ val opt_attribs: token list -> Attrib.src list * token list
+ val thm_name: string -> token list -> (bstring * Attrib.src list) * token list
+ val opt_thm_name: string -> token list -> (bstring * Attrib.src list) * token list
+ val spec_name: token list -> ((bstring * string) * Attrib.src list) * token list
+ val spec_opt_name: token list -> ((bstring * string) * Attrib.src list) * token list
+ val xthm: token list -> (thmref * Attrib.src list) * token list
+ val xthms1: token list -> (thmref * Attrib.src list) list * token list
val locale_target: token list -> xstring option * token list
val locale_expr: token list -> Locale.expr * token list
val locale_keyword: token list -> string * token list
- val locale_element: token list -> Args.src Locale.element * token list
- val locale_elem_or_expr: token list -> Args.src Locale.element Locale.elem_expr * token list
+ val locale_element: token list -> Locale.element * token list
+ val locale_elem_or_expr: token list -> Locale.element Locale.elem_expr * token list
val method: token list -> Method.text * token list
end;
@@ -122,8 +122,9 @@
(* tokens *)
-fun position scan =
- (Scan.ahead (Scan.one T.not_eof) >> T.position_of) -- scan >> Library.swap;
+val not_eof = Scan.one T.not_eof;
+
+fun position scan = (Scan.ahead not_eof >> T.position_of) -- scan >> Library.swap;
fun kind k =
group (T.str_of_kind k) (Scan.one (T.is_kind k) >> T.val_of);
@@ -148,13 +149,12 @@
val semicolon = $$$ ";";
+val minus = sym_ident :-- (fn "-" => Scan.succeed () | _ => Scan.fail) >> #1;
val underscore = sym_ident :-- (fn "_" => Scan.succeed () | _ => Scan.fail) >> #1;
-val minus = sym_ident :-- (fn "-" => Scan.succeed () | _ => Scan.fail) >> #1;
+fun maybe scan = underscore >> K NONE || scan >> SOME;
val nat = number >> (#1 o Library.read_int o Symbol.explode);
-val not_eof = Scan.one T.not_eof;
-
val opt_unit = Scan.optional ($$$ "(" -- $$$ ")" >> (K ())) ();
fun opt_keyword s = Scan.optional ($$$ "(" |-- !!! (($$$ s >> K true) --| $$$ ")")) false;
@@ -179,8 +179,6 @@
val text = group "text" (short_ident || long_ident || sym_ident || string || number || verbatim);
val path = group "file name/path specification" name >> Path.unpack;
-val uname = underscore >> K NONE || name >> SOME;
-
(* sorts and arities *)
@@ -265,13 +263,13 @@
fun atom_arg is_symid blk =
group "argument"
(position (short_ident || long_ident || sym_ident || term_var ||
- type_ident || type_var || number) >> Args.ident ||
- position (keyword_symid is_symid) >> Args.keyword ||
- position (string || verbatim) >> Args.string ||
- position (if blk then $$$ "," else Scan.fail) >> Args.keyword);
+ type_ident || type_var || number) >> Args.mk_ident ||
+ position (keyword_symid is_symid) >> Args.mk_keyword ||
+ position (string || verbatim) >> Args.mk_string ||
+ position (if blk then $$$ "," else Scan.fail) >> Args.mk_keyword);
fun paren_args l r scan = position ($$$ l) -- !!! (scan true -- position ($$$ r))
- >> (fn (x, (ys, z)) => Args.keyword x :: ys @ [Args.keyword z]);
+ >> (fn (x, (ys, z)) => Args.mk_keyword x :: ys @ [Args.mk_keyword z]);
fun args is_symid blk x = Scan.optional (args1 is_symid blk) [] x
and args1 is_symid blk x =
@@ -297,8 +295,9 @@
val spec_opt_name = opt_thm_name ":" -- prop >> (fn ((x, y), z) => ((x, z), y));
val thm_sel = $$$ "(" |-- list1
- ( nat --| minus -- nat >> op upto
- || nat >> single) --| $$$ ")" >> List.concat;
+ (nat --| minus -- nat >> PureThy.FromTo ||
+ nat --| minus >> PureThy.From ||
+ nat >> PureThy.Single) --| $$$ ")";
val xthm = xname -- Scan.option thm_sel -- opt_attribs;
val xthms1 = Scan.repeat1 xthm;
@@ -325,7 +324,7 @@
scan -- Scan.repeat ($$$ "+" |-- Scan.unless loc_keyword (!!! scan)) >> op ::;
fun expr2 x = (xname >> Locale.Locale || $$$ "(" |-- !!! (expr0 --| $$$ ")")) x
-and expr1 x = (expr2 -- Scan.repeat1 uname >> Locale.Rename || expr2) x
+and expr1 x = (expr2 -- Scan.repeat1 (maybe name) >> Locale.Rename || expr2) x
and expr0 x = (plus1 expr1 >> (fn [e] => e | es => Locale.Merge es)) x;
in
--- a/src/Pure/Isar/proof.ML Wed Apr 13 09:48:41 2005 +0200
+++ b/src/Pure/Isar/proof.ML Wed Apr 13 18:34:22 2005 +0200
@@ -90,19 +90,17 @@
val def: string -> context attribute list -> string * (string * string list) -> state -> state
val def_i: string -> context attribute list -> string * (term * term list) -> state -> state
val invoke_case: string * string option list * context attribute list -> state -> state
- val multi_theorem:
- string -> (theory -> theory) ->
+ val multi_theorem: string -> (theory -> theory) ->
(cterm list -> context -> context -> thm -> thm) ->
- (xstring * (Locale.multi_attribute list * Locale.multi_attribute list list)) option
- -> bstring * theory attribute list -> Locale.multi_attribute Locale.element Locale.elem_expr list
+ (xstring * (Attrib.src list * Attrib.src list list)) option ->
+ bstring * theory attribute list -> Locale.element Locale.elem_expr list
-> ((bstring * theory attribute list) * (string * (string list * string list)) list) list
-> theory -> state
- val multi_theorem_i:
- string -> (theory -> theory) ->
+ val multi_theorem_i: string -> (theory -> theory) ->
(cterm list -> context -> context -> thm -> thm) ->
- (string * (Locale.multi_attribute list * Locale.multi_attribute list list)) option
+ (string * (Attrib.src list * Attrib.src list list)) option
-> bstring * theory attribute list
- -> Locale.multi_attribute Locale.element_i Locale.elem_expr list
+ -> Locale.element_i Locale.elem_expr list
-> ((bstring * theory attribute list) * (term * (term list * term list)) list) list
-> theory -> state
val chain: state -> state
@@ -119,12 +117,6 @@
val have_i: (state -> state Seq.seq) -> bool
-> ((string * context attribute list) * (term * (term list * term list)) list) list
-> state -> state
- val interpret: (context -> context) -> (state -> state Seq.seq) -> bool
- -> ((string * context attribute list) * (string * (string list * string list)) list) list
- -> state -> state
- val interpret_i: (context -> context) -> (state -> state Seq.seq) -> bool
- -> ((string * context attribute list) * (term * (term list * term list)) list) list
- -> state -> state
val at_bottom: state -> bool
val local_qed: (state -> state Seq.seq)
-> (context -> string * (string * thm list) list -> unit) * (context -> thm -> unit)
@@ -136,8 +128,6 @@
val next_block: state -> state
val thisN: string
val call_atp: bool ref;
-
-
end;
structure Proof: PROOF =
@@ -153,33 +143,15 @@
(* type goal *)
-(* CB: four kinds of Isar goals are distinguished:
- - Theorem: global goal in a theory, corresponds to Isar commands theorem,
- lemma and corollary,
- - Have: local goal in a proof, Isar command have
- - Show: local goal in a proof, Isar command show
- - Interpret: local goal in a proof, Isar command interpret
-*)
-
datatype kind =
Theorem of {kind: string,
theory_spec: (bstring * theory attribute list) * theory attribute list list,
- locale_spec: (string * (Locale.multi_attribute list * Locale.multi_attribute list list)) option,
- view: cterm list * cterm list, (* target view and includes view *)
- thy_mod: theory -> theory, (* used in finish_global to modify final
- theory, normally set to I; used by
- registration command to activate
- registrations *)
- export: cterm list -> context -> context -> thm -> thm } |
+ locale_spec: (string * (Attrib.src list * Attrib.src list list)) option,
+ view: cterm list * cterm list, (* target view and includes view *)
+ export: cterm list -> context -> context -> thm -> thm} |
(* exporter to be used in finish_global *)
Show of context attribute list list |
- Have of context attribute list list |
- Interpret of {attss: context attribute list list,
- ctxt_mod: context -> context}; (* used in finish_local to modify final
- context *)
-
-(* CB: this function prints the goal kind (Isar command), name and target in
- the proof state *)
+ Have of context attribute list list;
fun kind_name _ (Theorem {kind = s, theory_spec = ((a, _), _),
locale_spec = NONE, ...}) = s ^ (if a = "" then "" else " " ^ a)
@@ -187,8 +159,7 @@
locale_spec = SOME (name, _), ...}) =
s ^ " (in " ^ Locale.cond_extern sg name ^ ")" ^ (if a = "" then "" else " " ^ a)
| kind_name _ (Show _) = "show"
- | kind_name _ (Have _) = "have"
- | kind_name _ (Interpret _) = "interpret";
+ | kind_name _ (Have _) = "have";
type goal =
(kind * (*result kind*)
@@ -211,11 +182,13 @@
{context: context,
facts: thm list option,
mode: mode,
- goal: (goal * ((state -> state Seq.seq) * bool)) option}
+ goal: (goal * (after_qed * bool)) option}
and state =
State of
node * (*current*)
- node list; (*parents wrt. block structure*)
+ node list (*parents wrt. block structure*)
+and after_qed =
+ AfterQed of (state -> state Seq.seq) * (theory -> theory);
fun make_node (context, facts, mode, goal) =
Node {context = context, facts = facts, mode = mode, goal = goal};
@@ -658,7 +631,8 @@
(* locale instantiation *)
-fun instantiate_locale (loc_name, prfx_attribs) state = let
+fun instantiate_locale (loc_name, prfx_attribs) state =
+ let
val facts = if is_chain state then get_facts state else NONE;
in
state
@@ -668,6 +642,7 @@
|> map_context (Locale.instantiate loc_name prfx_attribs facts)
end;
+
(* fix *)
fun gen_fix f xs state =
@@ -774,6 +749,9 @@
|> map_context_result (fn ctxt => prepp (ctxt, raw_propp));
val sign' = sign_of state';
+ val AfterQed (after_local, after_global) = after_qed;
+ val after_qed' = AfterQed (after_local o map_context gen_binds, after_global);
+
val props = List.concat propss;
val cprop = Thm.cterm_of sign' (Logic.mk_conjunction_list props);
val goal = Drule.mk_triv_goal cprop;
@@ -789,8 +767,7 @@
commas (map (ProofContext.string_of_term (context_of state')) vars));
state'
|> map_context (autofix props)
- |> put_goal (SOME (((kind, names, propss), ([], goal)),
- (after_qed o map_context gen_binds, pr)))
+ |> put_goal (SOME (((kind, names, propss), ([], goal)), (after_qed', pr)))
|> map_context (ProofContext.add_cases
(if length props = 1 then
RuleCases.make true NONE (Thm.sign_of_thm goal, Thm.prop_of goal) [rule_contextN]
@@ -802,7 +779,7 @@
end;
(*global goals*)
-fun global_goal prep kind thy_mod export raw_locale a elems concl thy =
+fun global_goal prep kind after_global export raw_locale a elems concl thy =
let
val init = init_state thy;
val (opt_name, view, locale_ctxt, elems_ctxt, propp) =
@@ -813,16 +790,14 @@
|> map_context (K locale_ctxt)
|> open_block
|> map_context (K elems_ctxt)
-(* CB: elems_ctxt is an extension of locale_ctxt, see prep_context_statement
- in locale.ML, naming there: ctxt and import_ctxt. *)
|> setup_goal I ProofContext.bind_propp_schematic_i ProofContext.fix_frees
(Theorem {kind = kind,
theory_spec = (a, map (snd o fst) concl),
locale_spec = (case raw_locale of NONE => NONE | SOME (_, x) => SOME (valOf opt_name, x)),
view = view,
- thy_mod = thy_mod,
export = export})
- Seq.single true (map (fst o fst) concl) propp
+ (AfterQed (Seq.single, after_global))
+ true (map (fst o fst) concl) propp
end;
val multi_theorem = global_goal Locale.read_context_statement;
@@ -830,10 +805,10 @@
(*local goals*)
-fun local_goal' prepp kind (check: bool -> state -> state) f pr args int state =
+fun local_goal' prepp kind (check: bool -> state -> state) after_local pr args int state =
state
|> setup_goal open_block prepp (K I) (kind (map (snd o fst) args))
- f pr (map (fst o fst) args) (map snd args)
+ (AfterQed (after_local, I)) pr (map (fst o fst) args) (map snd args)
|> warn_extra_tfrees state
|> check int;
@@ -843,10 +818,7 @@
val show_i = local_goal' ProofContext.bind_propp_i Show;
val have = local_goal ProofContext.bind_propp Have;
val have_i = local_goal ProofContext.bind_propp_i Have;
-fun interpret ctxt_mod = local_goal ProofContext.bind_propp
- (fn attss => Interpret {attss = attss, ctxt_mod = ctxt_mod});
-fun interpret_i ctxt_mod = local_goal ProofContext.bind_propp_i
- (fn attss => Interpret {attss = attss, ctxt_mod = ctxt_mod});
+
(** conclusions **)
@@ -884,7 +856,8 @@
fun finish_local (print_result, print_rule) state =
let
- val (goal_ctxt, (((kind, names, tss), (_, raw_thm)), (after_qed, pr))) = current_goal state;
+ val (goal_ctxt, (((kind, names, tss), (_, raw_thm)), (AfterQed (after_local, _), pr))) =
+ current_goal state;
val outer_state = state |> close_block;
val outer_ctxt = context_of outer_state;
@@ -894,30 +867,21 @@
results |> map (ProofContext.export false goal_ctxt outer_ctxt)
|> Seq.commute |> Seq.map (Library.unflat tss);
- val (attss, opt_solve, ctxt_mod) =
+ val (attss, opt_solve) =
(case kind of
Show attss => (attss,
- export_goals goal_ctxt (if pr then print_rule else (K (K ())))
- results, I)
- | Have attss => (attss, Seq.single, I)
- | Interpret {attss, ctxt_mod} => (attss, Seq.single, ctxt_mod)
+ export_goals goal_ctxt (if pr then print_rule else (K (K ()))) results)
+ | Have attss => (attss, Seq.single)
| _ => err_malformed "finish_local" state);
in
conditional pr (fn () => print_result goal_ctxt
(kind_name (sign_of state) kind, names ~~ Library.unflat tss results));
outer_state
|> auto_bind_facts (ProofContext.generalize goal_ctxt outer_ctxt ts)
-(* original version
|> (fn st => Seq.map (fn res =>
- note_thmss_i ((names ~~ attss) ~~
- map (single o Thm.no_attributes) res) st) resultq)
-*)
- |> (fn st => Seq.map (fn res =>
- st |> note_thmss_i ((names ~~ attss) ~~
- map (single o Thm.no_attributes) res)
- |> map_context ctxt_mod) resultq)
+ note_thmss_i ((names ~~ attss) ~~ map (single o Thm.no_attributes) res) st) resultq)
|> (Seq.flat o Seq.map opt_solve)
- |> (Seq.flat o Seq.map after_qed)
+ |> (Seq.flat o Seq.map after_local)
end;
fun local_qed finalize print state =
@@ -931,11 +895,14 @@
fun finish_global state =
let
- val (goal_ctxt, (((kind, names, tss), (_, raw_thm)), _)) = current_goal state;
+ val (goal_ctxt, (((kind, names, tss), (_, raw_thm)), (AfterQed (_, after_global), _))) =
+ current_goal state;
val locale_ctxt = context_of (state |> close_block);
val theory_ctxt = context_of (state |> close_block |> close_block);
- val {kind = k, theory_spec = ((name, atts), attss), locale_spec, view = (target_view, elems_view), thy_mod, export} =
+ val {kind = k, theory_spec = ((name, atts), attss),
+ locale_spec, view = (target_view, elems_view), export} =
(case kind of Theorem x => x | _ => err_malformed "finish_global" state);
+ val locale_name = Option.map fst locale_spec;
val ts = List.concat tss;
val locale_results = map (export elems_view goal_ctxt locale_ctxt)
@@ -956,12 +923,12 @@
if name = "" andalso null loc_atts then thy'
else (thy', ctxt')
|> (#1 o #1 o Locale.add_thmss k loc [((name, List.concat (map #2 res)), loc_atts)])))
- |> Locale.smart_note_thmss k locale_spec
+ |> Locale.smart_note_thmss k locale_name
((names ~~ attss) ~~ map (single o Thm.no_attributes) (Library.unflat tss results))
|> (fn (thy, res) => (thy, res)
- |>> (#1 o Locale.smart_note_thmss k locale_spec
+ |>> (#1 o Locale.smart_note_thmss k locale_name
[((name, atts), [(List.concat (map #2 res), [])])]));
- in (thy_mod theory', ((k, name), results')) end;
+ in (after_global theory', ((k, name), results')) end;
(*note: clients should inspect first result only, as backtracking may destroy theory*)
--- a/src/Pure/Isar/proof_context.ML Wed Apr 13 09:48:41 2005 +0200
+++ b/src/Pure/Isar/proof_context.ML Wed Apr 13 18:34:22 2005 +0200
@@ -8,7 +8,7 @@
(*Jia: changed: datatype context
affected files: make_context, map_context, init, put_data, add_syntax, map_defaults, del_bind, upd_bind, qualified, hide_thms, put_thms, reset_thms, gen_assms, map_fixes, add_cases
- added: put_delta, get_delta
+ added: put_delta, get_delta
06/01/05
*)
@@ -62,6 +62,8 @@
val cert_prop_pats: context -> term list -> term list
val declare_term: term -> context -> context
val declare_terms: term list -> context -> context
+ val read_tyname: context -> string -> typ
+ val read_const: context -> string -> term
val warn_extra_tfrees: context -> context -> context
val generalize: context -> context -> term list -> term list
val find_free: term -> string -> term option
@@ -163,7 +165,7 @@
val setup: (theory -> theory) list
val get_delta: context -> Object.T Symtab.table (* Jia: (claset, simpset) *)
- val put_delta: Object.T Symtab.table -> context -> context
+ val put_delta: Object.T Symtab.table -> context -> context
val get_delta_count_incr: context -> int
end;
@@ -648,10 +650,7 @@
in
-(* CB: for attribute where. See attrib.ML. *)
val read_termTs = gen_read' (read_def_termTs false) (apfst o map) false false false;
-
-(* CB: for rule_tac etc. See method.ML. *)
val read_termTs_schematic = gen_read' (read_def_termTs false) (apfst o map) false false true;
fun read_term_pats T ctxt =
@@ -743,6 +742,19 @@
end;
+(* type and constant names *)
+
+fun read_tyname ctxt c =
+ if c mem_string used_types ctxt then
+ TFree (c, getOpt (def_sort ctxt (c, ~1), Sign.defaultS (sign_of ctxt)))
+ else Sign.read_tyname (sign_of ctxt) c;
+
+fun read_const ctxt c =
+ (case lookup_skolem ctxt c of
+ SOME c' => Free (c', dummyT)
+ | NONE => Sign.read_const (sign_of ctxt) c);
+
+
(** Hindley-Milner polymorphism **)
--- a/src/Pure/axclass.ML Wed Apr 13 09:48:41 2005 +0200
+++ b/src/Pure/axclass.ML Wed Apr 13 18:34:22 2005 +0200
@@ -11,7 +11,7 @@
val print_axclasses: theory -> unit
val add_classrel_thms: thm list -> theory -> theory
val add_arity_thms: thm list -> theory -> theory
- val add_axclass: bclass * xclass list -> ((bstring * string) * Args.src list) list
+ val add_axclass: bclass * xclass list -> ((bstring * string) * Attrib.src list) list
-> theory -> theory * {intro: thm, axioms: thm list}
val add_axclass_i: bclass * class list -> ((bstring * term) * theory attribute list) list
-> theory -> theory * {intro: thm, axioms: thm list}
--- a/src/Pure/pure_thy.ML Wed Apr 13 09:48:41 2005 +0200
+++ b/src/Pure/pure_thy.ML Wed Apr 13 18:34:22 2005 +0200
@@ -24,6 +24,7 @@
signature PURE_THY =
sig
include BASIC_PURE_THY
+ datatype interval = FromTo of int * int | From of int | Single of int
val get_thm_closure: theory -> thmref -> thm
val get_thms_closure: theory -> thmref -> thm list
val single_thm: string -> thm list -> thm
@@ -145,20 +146,42 @@
(** retrieve theorems **)
-type thmref = xstring * int list option;
-
-(* selections *)
-
fun the_thms _ (SOME thms) = thms
| the_thms name NONE = error ("Unknown theorem(s) " ^ quote name);
fun single_thm _ [thm] = thm
| single_thm name _ = error ("Single theorem expected " ^ quote name);
-fun select_thm (s, NONE) xs = xs
- | select_thm (s, SOME is) xs = map
- (fn i => (if i < 1 then raise Subscript else List.nth (xs, i-1)) handle Subscript =>
- error ("Bad subscript " ^ string_of_int i ^ " for " ^ quote s)) is;
+
+(* selections *)
+
+datatype interval =
+ FromTo of int * int |
+ From of int |
+ Single of int;
+
+type thmref = xstring * interval list option;
+
+local
+
+fun interval _ (FromTo (i, j)) = i upto j
+ | interval n (From i) = i upto n
+ | interval _ (Single i) = [i];
+
+fun select name thms n i =
+ if i < 1 orelse i > n then
+ error ("Bad subscript " ^ string_of_int i ^ " for " ^
+ quote name ^ " (length " ^ string_of_int n ^ ")")
+ else List.nth (thms, i - 1);
+
+in
+
+fun select_thm (_, NONE) thms = thms
+ | select_thm (name, SOME is) thms =
+ let val n = length thms
+ in map (select name thms n) (List.concat (map (interval n) is)) end;
+
+end;
(* get_thm(s)_closure -- statically scoped versions *)
@@ -222,6 +245,7 @@
thms_containing thy (consts, []) |> map #2 |> List.concat
|> map (fn th => (Thm.name_of_thm th, th))
+
(* intro/elim theorems *)
(* intro: given a goal state, find a suitable intro rule for some subgoal *)
--- a/src/Pure/sign.ML Wed Apr 13 09:48:41 2005 +0200
+++ b/src/Pure/sign.ML Wed Apr 13 18:34:22 2005 +0200
@@ -42,6 +42,8 @@
val is_stale: sg -> bool
val syn_of: sg -> Syntax.syntax
val const_type: sg -> string -> typ option
+ val declared_tyname: sg -> string -> bool
+ val declared_const: sg -> string -> bool
val classes: sg -> class list
val defaultS: sg -> sort
val subsort: sg -> sort * sort -> bool
@@ -93,14 +95,14 @@
val certify_sort: sg -> sort -> sort
val certify_typ: sg -> typ -> typ
val certify_typ_raw: sg -> typ -> typ
- val certify_tyname: sg -> string -> string
- val certify_const: sg -> string -> string
val certify_term: Pretty.pp -> sg -> term -> term * typ * int
val read_sort: sg -> string -> sort
val read_raw_typ: sg * (indexname -> sort option) -> string -> typ
val read_typ: sg * (indexname -> sort option) -> string -> typ
val read_typ': Syntax.syntax -> sg * (indexname -> sort option) -> string -> typ
val read_typ_raw': Syntax.syntax -> sg * (indexname -> sort option) -> string -> typ
+ val read_tyname: sg -> string -> typ
+ val read_const: sg -> string -> term
val inst_typ_tvars: sg -> (indexname * typ) list -> typ -> typ
val inst_term_tvars: sg -> (indexname * typ) list -> term -> term
val infer_types: Pretty.pp -> sg -> (indexname -> typ option) ->
@@ -164,7 +166,7 @@
val merge: sg * sg -> sg
val copy: sg -> sg
val prep_ext: sg -> sg
- val nontriv_merge: sg * sg -> sg
+ val prep_ext_merge: sg list -> sg
end;
signature PRIVATE_SIGN =
@@ -234,6 +236,9 @@
fun is_logtype sg c = c mem_string Type.logical_types (tsig_of sg);
fun const_type (Sg (_, {consts, ...})) c = Option.map #1 (Symtab.lookup (consts, c));
+fun declared_tyname sg c = isSome (Symtab.lookup (#types (Type.rep_tsig (tsig_of sg)), c));
+fun declared_const sg c = isSome (const_type sg c);
+
(* id and self *)
@@ -266,22 +271,15 @@
fun subset_stamp ([], ys) = true
| subset_stamp (x :: xs, ys) =
mem_stamp (x, ys) andalso subset_stamp (xs, ys);
-
- (*fast partial test*)
- fun fast_sub ([]: string ref list, _) = true
- | fast_sub (_, []) = false
- | fast_sub (x :: xs, y :: ys) =
- if x = y then fast_sub (xs, ys)
- else fast_sub (x :: xs, ys);
in
fun eq_sg (sg1 as Sg ({id = id1, ...}, _), sg2 as Sg ({id = id2, ...}, _)) =
(check_stale sg1; check_stale sg2; id1 = id2);
fun subsig (sg1 as Sg ({stamps = s1, ...}, _), sg2 as Sg ({stamps = s2, ...}, _)) =
- eq_sg (sg1, sg2) orelse subset_stamp (s1, s2);
+ eq_sg (sg1, sg2) orelse mem_stamp (hd s1, s2);
- fun fast_subsig (sg1 as Sg ({stamps = s1, ...}, _), sg2 as Sg ({stamps = s2, ...}, _)) =
- eq_sg (sg1, sg2) orelse fast_sub (s1, s2);
+ fun subsig_internal (sg1 as Sg ({stamps = s1, ...}, _), sg2 as Sg ({stamps = s2, ...}, _)) =
+ eq_sg (sg1, sg2) orelse subset_stamp (s1, s2);
end;
@@ -703,14 +701,6 @@
val certify_typ = Type.cert_typ o tsig_of;
val certify_typ_raw = Type.cert_typ_raw o tsig_of;
-fun certify_tyname sg c =
- if isSome (Symtab.lookup (#types (Type.rep_tsig (tsig_of sg)), c)) then c
- else raise TYPE ("Undeclared type constructor: " ^ quote c, [], []);
-
-fun certify_const sg c =
- if isSome (const_type sg c) then c
- else raise TYPE ("Undeclared constant: " ^ quote c, [], []);
-
(* certify_term *)
@@ -822,6 +812,22 @@
end;
+(* type and constant names *)
+
+fun read_tyname sg raw_c =
+ let val c = intern_tycon sg raw_c in
+ (case Symtab.lookup (#types (Type.rep_tsig (tsig_of sg)), c) of
+ SOME (Type.LogicalType n, _) => Type (c, replicate n dummyT)
+ | NONE => raise TYPE ("Undeclared type constructor: " ^ quote c, [], []))
+ end;
+
+fun read_const sg raw_c =
+ let val c = intern_const sg raw_c in
+ if isSome (const_type sg c) then Const (c, dummyT)
+ else raise TYPE ("Undeclared constant: " ^ quote c, [], [])
+ end;
+
+
(** instantiation **)
@@ -991,7 +997,7 @@
error ("Duplicate declaration of constant(s) " ^ commas_quote cs);
-fun read_const sg syn tsig (path, spaces) (c, ty_src, mx) =
+fun read_cnst sg syn tsig (path, spaces) (c, ty_src, mx) =
(c, rd_raw_typ (make_syntax sg syn) tsig spaces (K NONE) ty_src, mx)
handle ERROR => err_in_const (const_name path c mx);
@@ -1015,11 +1021,11 @@
end;
fun ext_consts_i x = ext_cnsts no_read false Syntax.default_mode x;
-fun ext_consts x = ext_cnsts read_const false Syntax.default_mode x;
+fun ext_consts x = ext_cnsts read_cnst false Syntax.default_mode x;
fun ext_syntax_i x = ext_cnsts no_read true Syntax.default_mode x;
-fun ext_syntax x = ext_cnsts read_const true Syntax.default_mode x;
+fun ext_syntax x = ext_cnsts read_cnst true Syntax.default_mode x;
fun ext_modesyntax_i x y (prmode, consts) = ext_cnsts no_read true prmode x y consts;
-fun ext_modesyntax x y (prmode, consts) = ext_cnsts read_const true prmode x y consts;
+fun ext_modesyntax x y (prmode, consts) = ext_cnsts read_cnst true prmode x y consts;
(* add type classes *)
@@ -1198,9 +1204,7 @@
fun merge_refs (sgr1 as SgRef (SOME (ref (sg1 as Sg ({stamps = s1, ...}, _)))),
sgr2 as SgRef (SOME (ref (sg2 as Sg ({stamps = s2, ...}, _))))) =
- if fast_subsig (sg2, sg1) then sgr1
- else if fast_subsig (sg1, sg2) then sgr2
- else if subsig (sg2, sg1) then sgr1
+ if subsig (sg2, sg1) then sgr1
else if subsig (sg1, sg2) then sgr2
else (merge_stamps s1 s2; (*check for different versions*)
raise TERM ("Attempt to do non-trivial merge of signatures", []))
@@ -1209,16 +1213,17 @@
val merge = deref o merge_refs o pairself self_ref;
-(* non-trivial merge *) (*exception TERM/ERROR*)
+(* merge_list *) (*exception TERM/ERROR*)
+
+local
fun nontriv_merge (sg1, sg2) =
- if subsig (sg2, sg1) then sg1
- else if subsig (sg1, sg2) then sg2
- else if is_draft sg1 orelse is_draft sg2 then
- raise TERM ("Attempt to merge draft signatures", [])
- else if exists_stamp PureN sg1 andalso exists_stamp CPureN sg2 orelse
- exists_stamp CPureN sg1 andalso exists_stamp PureN sg2 then
- raise TERM ("Cannot merge Pure and CPure signatures", [])
+ if subsig_internal (sg2, sg1) then sg1
+ else if subsig_internal (sg1, sg2) then sg2
+ else
+ if exists_stamp PureN sg1 andalso exists_stamp CPureN sg2 orelse
+ exists_stamp CPureN sg1 andalso exists_stamp PureN sg2
+ then error "Cannot merge Pure and CPure signatures"
else
let
val Sg ({id = _, stamps = stamps1, syn = Syn (syntax1, trfuns1)},
@@ -1253,4 +1258,18 @@
path, spaces, data, stamps);
in self_ref := sign; syn_of sign; sign end;
+in
+
+fun prep_ext_merge sgs =
+ if null sgs then
+ error "Merge: no parent theories"
+ else if exists is_draft sgs then
+ error "Attempt to merge draft theories"
+ else
+ Library.foldl nontriv_merge (hd sgs, tl sgs)
+ |> prep_ext
+ |> add_path "/";
+
end;
+
+end;
--- a/src/Pure/theory.ML Wed Apr 13 09:48:41 2005 +0200
+++ b/src/Pure/theory.ML Wed Apr 13 18:34:22 2005 +0200
@@ -540,43 +540,32 @@
(** merge theories **) (*exception ERROR*)
-fun merge_sign (sg, thy) =
- Sign.nontriv_merge (sg, sign_of thy) handle TERM (msg, _) => error msg;
-
(*merge list of theories from left to right, preparing extend*)
fun prep_ext_merge thys =
- if null thys then
- error "Merge: no parent theories"
- else if exists is_draft thys then
- error "Attempt to merge draft theories"
- else
- let
- val sign' =
- Library.foldl merge_sign (sign_of (hd thys), tl thys)
- |> Sign.prep_ext
- |> Sign.add_path "/";
+ let
+ val sign' = Sign.prep_ext_merge (map sign_of thys)
- val depss = map (#const_deps o rep_theory) thys;
- val deps' = Library.foldl (Graph.merge_acyclic (K true)) (hd depss, tl depss)
- handle Graph.CYCLES namess => error (cycle_msg namess);
+ val depss = map (#const_deps o rep_theory) thys;
+ val deps' = Library.foldl (Graph.merge_acyclic (K true)) (hd depss, tl depss)
+ handle Graph.CYCLES namess => error (cycle_msg namess);
+
+ val final_constss = map (#final_consts o rep_theory) thys;
+ val final_consts' =
+ Library.foldl (Symtab.join (merge_final sign')) (hd final_constss, tl final_constss);
+ val axioms' = Symtab.empty;
- val final_constss = map (#final_consts o rep_theory) thys;
- val final_consts' = Library.foldl (Symtab.join (merge_final sign')) (hd final_constss,
- tl final_constss);
- val axioms' = Symtab.empty;
+ fun eq_ora ((_, (_, s1: stamp)), (_, (_, s2))) = s1 = s2;
+ val oracles' =
+ Symtab.make (gen_distinct eq_ora
+ (List.concat (map (Symtab.dest o #oracles o rep_theory) thys)))
+ handle Symtab.DUPS names => err_dup_oras names;
- fun eq_ora ((_, (_, s1: stamp)), (_, (_, s2))) = s1 = s2;
- val oracles' =
- Symtab.make (gen_distinct eq_ora
- (List.concat (map (Symtab.dest o #oracles o rep_theory) thys)))
- handle Symtab.DUPS names => err_dup_oras names;
-
- val parents' = gen_distinct eq_thy thys;
- val ancestors' =
- gen_distinct eq_thy (parents' @ List.concat (map ancestors_of thys));
- in
- make_theory sign' deps' final_consts' axioms' oracles' parents' ancestors'
- end;
+ val parents' = gen_distinct eq_thy thys;
+ val ancestors' =
+ gen_distinct eq_thy (parents' @ List.concat (map ancestors_of thys));
+ in
+ make_theory sign' deps' final_consts' axioms' oracles' parents' ancestors'
+ end;
end;
--- a/src/ZF/Tools/datatype_package.ML Wed Apr 13 09:48:41 2005 +0200
+++ b/src/ZF/Tools/datatype_package.ML Wed Apr 13 18:34:22 2005 +0200
@@ -36,8 +36,8 @@
val add_datatype_x: string * string list -> (string * string list * mixfix) list list ->
thm list * thm list * thm list -> theory -> theory * inductive_result * datatype_result
val add_datatype: string * string list -> (string * string list * mixfix) list list ->
- (thmref * Args.src list) list * (thmref * Args.src list) list *
- (thmref * Args.src list) list -> theory -> theory * inductive_result * datatype_result
+ (thmref * Attrib.src list) list * (thmref * Attrib.src list) list *
+ (thmref * Attrib.src list) list -> theory -> theory * inductive_result * datatype_result
end;
functor Add_datatype_def_Fun
--- a/src/ZF/Tools/ind_cases.ML Wed Apr 13 09:48:41 2005 +0200
+++ b/src/ZF/Tools/ind_cases.ML Wed Apr 13 18:34:22 2005 +0200
@@ -8,7 +8,7 @@
signature IND_CASES =
sig
val declare: string -> (simpset -> cterm -> thm) -> theory -> theory
- val inductive_cases: ((bstring * Args.src list) * string list) list -> theory -> theory
+ val inductive_cases: ((bstring * Attrib.src list) * string list) list -> theory -> theory
val setup: (theory -> theory) list
end;
--- a/src/ZF/Tools/induct_tacs.ML Wed Apr 13 09:48:41 2005 +0200
+++ b/src/ZF/Tools/induct_tacs.ML Wed Apr 13 18:34:22 2005 +0200
@@ -13,8 +13,8 @@
val induct_tac: string -> int -> tactic
val exhaust_tac: string -> int -> tactic
val rep_datatype_i: thm -> thm -> thm list -> thm list -> theory -> theory
- val rep_datatype: thmref * Args.src list -> thmref * Args.src list ->
- (thmref * Args.src list) list -> (thmref * Args.src list) list -> theory -> theory
+ val rep_datatype: thmref * Attrib.src list -> thmref * Attrib.src list ->
+ (thmref * Attrib.src list) list -> (thmref * Attrib.src list) list -> theory -> theory
val setup: (theory -> theory) list
end;
--- a/src/ZF/Tools/inductive_package.ML Wed Apr 13 09:48:41 2005 +0200
+++ b/src/ZF/Tools/inductive_package.ML Wed Apr 13 18:34:22 2005 +0200
@@ -34,9 +34,9 @@
val add_inductive_x: string list * string -> ((bstring * string) * theory attribute list) list
-> thm list * thm list * thm list * thm list -> theory -> theory * inductive_result
val add_inductive: string list * string ->
- ((bstring * string) * Args.src list) list ->
- (thmref * Args.src list) list * (thmref * Args.src list) list *
- (thmref * Args.src list) list * (thmref * Args.src list) list ->
+ ((bstring * string) * Attrib.src list) list ->
+ (thmref * Attrib.src list) list * (thmref * Attrib.src list) list *
+ (thmref * Attrib.src list) list * (thmref * Attrib.src list) list ->
theory -> theory * inductive_result
end;
--- a/src/ZF/Tools/primrec_package.ML Wed Apr 13 09:48:41 2005 +0200
+++ b/src/ZF/Tools/primrec_package.ML Wed Apr 13 18:34:22 2005 +0200
@@ -10,7 +10,7 @@
signature PRIMREC_PACKAGE =
sig
val quiet_mode: bool ref
- val add_primrec: ((bstring * string) * Args.src list) list -> theory -> theory * thm list
+ val add_primrec: ((bstring * string) * Attrib.src list) list -> theory -> theory * thm list
val add_primrec_i: ((bstring * term) * theory attribute list) list -> theory -> theory * thm list
end;