--- a/NEWS Fri Mar 16 16:29:28 2012 +0000
+++ b/NEWS Fri Mar 16 16:29:51 2012 +0000
@@ -41,6 +41,10 @@
"syntax_ambiguity_warning" and "syntax_ambiguity_limit" in isar-ref
manual. Minor INCOMPATIBILITY.
+* Forward declaration of outer syntax keywords within the theory
+header -- minor INCOMPATIBILITY for user-defined commands. Allow new
+commands to be used in the same theory where defined.
+
*** Pure ***
@@ -372,9 +376,6 @@
*** ML ***
-* Outer syntax keywords for user-defined Isar commands need to be
-defined explicitly in the theory header. Minor INCOMPATIBILITY.
-
* Antiquotation @{keyword "name"} produces a parser for outer syntax
from a minor keyword introduced via theory header declaration.
--- a/src/HOL/Refute.thy Fri Mar 16 16:29:28 2012 +0000
+++ b/src/HOL/Refute.thy Fri Mar 16 16:29:51 2012 +0000
@@ -15,6 +15,15 @@
setup Refute.setup
+refute_params
+ [itself = 1,
+ minsize = 1,
+ maxsize = 8,
+ maxvars = 10000,
+ maxtime = 60,
+ satsolver = auto,
+ no_assms = false]
+
text {*
\small
\begin{verbatim}
@@ -80,8 +89,6 @@
(* "expect" string Expected result ("genuine", "potential", "none", or *)
(* "unknown"). *)
(* *)
-(* See 'HOL/SAT.thy' for default values. *)
-(* *)
(* The size of particular types can be specified in the form type=size *)
(* (where 'type' is a string, and 'size' is an int). Examples: *)
(* "'a"=1 *)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Fri Mar 16 16:29:28 2012 +0000
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Fri Mar 16 16:29:51 2012 +0000
@@ -57,7 +57,7 @@
val normalize_chained_theorems =
maps (fn th => insert Thm.eq_thm_prop (zero_var_indexes th) [th])
fun reserved_isar_keyword_table () =
- union (op =) (Keyword.dest_keywords ()) (Keyword.dest_commands ())
+ Keyword.dest () |-> union (op =)
|> map (rpair ()) |> Symtab.make
end;
--- a/src/HOL/Tools/refute.ML Fri Mar 16 16:29:28 2012 +0000
+++ b/src/HOL/Tools/refute.ML Fri Mar 16 16:29:51 2012 +0000
@@ -204,16 +204,6 @@
wellformed: prop_formula
};
-val default_parameters =
- [("itself", "1"),
- ("minsize", "1"),
- ("maxsize", "8"),
- ("maxvars", "10000"),
- ("maxtime", "60"),
- ("satsolver", "auto"),
- ("no_assms", "false")]
- |> Symtab.make
-
structure Data = Theory_Data
(
type T =
@@ -222,8 +212,7 @@
printers: (string * (Proof.context -> model -> typ -> interpretation ->
(int -> bool) -> term option)) list,
parameters: string Symtab.table};
- val empty =
- {interpreters = [], printers = [], parameters = default_parameters};
+ val empty = {interpreters = [], printers = [], parameters = Symtab.empty};
val extend = I;
fun merge
({interpreters = in1, printers = pr1, parameters = pa1},
--- a/src/HOL/Word/Word.thy Fri Mar 16 16:29:28 2012 +0000
+++ b/src/HOL/Word/Word.thy Fri Mar 16 16:29:51 2012 +0000
@@ -802,8 +802,10 @@
lemma unats_uints: "unats n = nat ` uints n"
by (auto simp add : uints_unats image_iff)
-lemmas bintr_num = word_ubin.norm_eq_iff [symmetric, folded word_number_of_def]
-lemmas sbintr_num = word_sbin.norm_eq_iff [symmetric, folded word_number_of_def]
+lemmas bintr_num = word_ubin.norm_eq_iff
+ [of "number_of a" "number_of b", symmetric, folded word_number_of_alt] for a b
+lemmas sbintr_num = word_sbin.norm_eq_iff
+ [of "number_of a" "number_of b", symmetric, folded word_number_of_alt] for a b
lemmas num_of_bintr = word_ubin.Abs_norm [folded word_number_of_def]
lemmas num_of_sbintr = word_sbin.Abs_norm [folded word_number_of_def]
@@ -812,22 +814,25 @@
may want these in reverse, but loop as simp rules, so use following *)
lemma num_of_bintr':
- "bintrunc (len_of TYPE('a :: len0)) a = b \<Longrightarrow>
+ "bintrunc (len_of TYPE('a :: len0)) (number_of a) = (number_of b) \<Longrightarrow>
number_of a = (number_of b :: 'a word)"
- apply safe
- apply (rule_tac num_of_bintr [symmetric])
- done
+ unfolding bintr_num by (erule subst, simp)
lemma num_of_sbintr':
- "sbintrunc (len_of TYPE('a :: len) - 1) a = b \<Longrightarrow>
+ "sbintrunc (len_of TYPE('a :: len) - 1) (number_of a) = (number_of b) \<Longrightarrow>
number_of a = (number_of b :: 'a word)"
- apply safe
- apply (rule_tac num_of_sbintr [symmetric])
- done
-
-lemmas num_abs_bintr = sym [THEN trans, OF num_of_bintr word_number_of_def]
-lemmas num_abs_sbintr = sym [THEN trans, OF num_of_sbintr word_number_of_def]
-
+ unfolding sbintr_num by (erule subst, simp)
+
+lemma num_abs_bintr:
+ "(number_of x :: 'a word) =
+ word_of_int (bintrunc (len_of TYPE('a::len0)) (number_of x))"
+ by (simp only: word_ubin.Abs_norm word_number_of_alt)
+
+lemma num_abs_sbintr:
+ "(number_of x :: 'a word) =
+ word_of_int (sbintrunc (len_of TYPE('a::len) - 1) (number_of x))"
+ by (simp only: word_sbin.Abs_norm word_number_of_alt)
+
(** cast - note, no arg for new length, as it's determined by type of result,
thus in "cast w = w, the type means cast to length of w! **)
@@ -2880,16 +2885,16 @@
by (induct n) (auto simp: shiftl1_2t)
lemma shiftr1_bintr [simp]:
- "(shiftr1 (number_of w) :: 'a :: len0 word) =
- number_of (bin_rest (bintrunc (len_of TYPE ('a)) w))"
- unfolding shiftr1_def word_number_of_def
- by (simp add : word_ubin.eq_norm)
-
-lemma sshiftr1_sbintr [simp] :
- "(sshiftr1 (number_of w) :: 'a :: len word) =
- number_of (bin_rest (sbintrunc (len_of TYPE ('a) - 1) w))"
- unfolding sshiftr1_def word_number_of_def
- by (simp add : word_sbin.eq_norm)
+ "(shiftr1 (number_of w) :: 'a :: len0 word) =
+ word_of_int (bin_rest (bintrunc (len_of TYPE ('a)) (number_of w)))"
+ unfolding shiftr1_def word_number_of_alt
+ by (simp add: word_ubin.eq_norm)
+
+lemma sshiftr1_sbintr [simp]:
+ "(sshiftr1 (number_of w) :: 'a :: len word) =
+ word_of_int (bin_rest (sbintrunc (len_of TYPE ('a) - 1) (number_of w)))"
+ unfolding sshiftr1_def word_number_of_alt
+ by (simp add: word_sbin.eq_norm)
lemma shiftr_no [simp]:
"(number_of w::'a::len0 word) >> n = word_of_int
@@ -3379,11 +3384,9 @@
lemma word_rsplit_no:
"(word_rsplit (number_of bin :: 'b :: len0 word) :: 'a word list) =
- map number_of (bin_rsplit (len_of TYPE('a :: len))
- (len_of TYPE('b), bintrunc (len_of TYPE('b)) bin))"
- apply (unfold word_rsplit_def word_no_wi)
- apply (simp add: word_ubin.eq_norm)
- done
+ map word_of_int (bin_rsplit (len_of TYPE('a :: len))
+ (len_of TYPE('b), bintrunc (len_of TYPE('b)) (number_of bin)))"
+ unfolding word_rsplit_def by (simp add: word_ubin.eq_norm)
lemmas word_rsplit_no_cl [simp] = word_rsplit_no
[unfolded bin_rsplitl_def bin_rsplit_l [symmetric]]
--- a/src/Pure/Isar/isar_syn.ML Fri Mar 16 16:29:28 2012 +0000
+++ b/src/Pure/Isar/isar_syn.ML Fri Mar 16 16:29:51 2012 +0000
@@ -9,11 +9,8 @@
(** keywords **)
-(*keep keywords consistent with the parsers, otherwise be prepared for
- unexpected errors*)
-
val _ = Context.>> (Context.map_theory
- (fold (fn name => Thy_Header.declare_keyword (name, NONE))
+ (fold (fn name => (Keyword.define (name, NONE); Thy_Header.declare_keyword (name, NONE)))
["!!", "!", "%", "(", ")", "+", ",", "--", ":", "::", ";", "<", "<=",
"=", "==", "=>", "?", "[", "\\<equiv>", "\\<leftharpoondown>",
"\\<rightharpoonup>", "\\<rightleftharpoons>", "\\<subseteq>", "]",
--- a/src/Pure/Isar/keyword.ML Fri Mar 16 16:29:28 2012 +0000
+++ b/src/Pure/Isar/keyword.ML Fri Mar 16 16:29:51 2012 +0000
@@ -40,15 +40,12 @@
val make: string * string list -> T
val get_lexicons: unit -> Scan.lexicon * Scan.lexicon
val is_keyword: string -> bool
- val dest_keywords: unit -> string list
- val dest_commands: unit -> string list
val command_keyword: string -> T option
val command_tags: string -> string list
+ val dest: unit -> string list * string list
val keyword_statusN: string
val status: unit -> unit
- val keyword: string -> unit
- val command: string -> T -> unit
- val declare: string -> T option -> unit
+ val define: string * T option -> unit
val is_diag: string -> bool
val is_control: string -> bool
val is_regular: string -> bool
@@ -153,31 +150,45 @@
(** global keyword tables **)
+type keywords =
+ {lexicons: Scan.lexicon * Scan.lexicon, (*minor, major*)
+ commands: T Symtab.table}; (*command classification*)
+
+fun make_keywords (lexicons, commands) : keywords =
+ {lexicons = lexicons, commands = commands};
+
local
-val global_commands = Unsynchronized.ref (Symtab.empty: T Symtab.table);
-val global_lexicons = Unsynchronized.ref (Scan.empty_lexicon, Scan.empty_lexicon);
+val global_keywords =
+ Unsynchronized.ref (make_keywords ((Scan.empty_lexicon, Scan.empty_lexicon), Symtab.empty));
in
-fun get_commands () = ! global_commands;
-fun get_lexicons () = ! global_lexicons;
+fun get_keywords () = ! global_keywords;
-fun change_commands f = CRITICAL (fn () => Unsynchronized.change global_commands f);
-fun change_lexicons f = CRITICAL (fn () => Unsynchronized.change global_lexicons f);
+fun change_keywords f = CRITICAL (fn () =>
+ Unsynchronized.change global_keywords
+ (fn {lexicons, commands} => make_keywords (f (lexicons, commands))));
end;
+fun get_lexicons () = #lexicons (get_keywords ());
+fun get_commands () = #commands (get_keywords ());
+
(* lookup *)
-fun is_keyword s = Scan.is_literal (#1 (get_lexicons ())) (Symbol.explode s);
-fun dest_keywords () = sort_strings (Scan.dest_lexicon (#1 (get_lexicons ())));
+fun is_keyword s =
+ let
+ val (minor, major) = get_lexicons ();
+ val syms = Symbol.explode s;
+ in Scan.is_literal minor syms orelse Scan.is_literal major syms end;
-fun dest_commands () = sort_strings (Symtab.keys (get_commands ()));
fun command_keyword name = Symtab.lookup (get_commands ()) name;
fun command_tags name = these (Option.map tags_of (command_keyword name));
+fun dest () = pairself (sort_strings o Scan.dest_lexicon) (get_lexicons ());
+
(* status *)
@@ -196,27 +207,28 @@
("Outer syntax command: " ^ quote name ^ " (" ^ kind_of kind ^ ")");
fun status () =
- let val (keywords, commands) = CRITICAL (fn () =>
- (dest_keywords (), sort_wrt #1 (Symtab.dest (get_commands ()))))
- in
- List.app keyword_status keywords;
- List.app command_status commands
- end;
+ let
+ val {lexicons = (minor, _), commands} = get_keywords ();
+ val _ = List.app keyword_status (sort_strings (Scan.dest_lexicon minor));
+ val _ = List.app command_status (sort_wrt #1 (Symtab.dest commands));
+ in () end;
-(* augment tables *)
-
-fun keyword name =
- (change_lexicons (apfst (Scan.extend_lexicon (Symbol.explode name)));
- keyword_status name);
+(* define *)
-fun command name kind =
- (change_lexicons (apsnd (Scan.extend_lexicon (Symbol.explode name)));
- change_commands (Symtab.update (name, kind));
- command_status (name, kind));
-
-fun declare name NONE = keyword name
- | declare name (SOME kind) = command name kind;
+fun define (name, NONE) =
+ (change_keywords (fn ((minor, major), commands) =>
+ let
+ val minor' = Scan.extend_lexicon (Symbol.explode name) minor;
+ in ((minor', major), commands) end);
+ keyword_status name)
+ | define (name, SOME kind) =
+ (change_keywords (fn ((minor, major), commands) =>
+ let
+ val major' = Scan.extend_lexicon (Symbol.explode name) major;
+ val commands' = Symtab.update (name, kind) commands;
+ in ((minor, major'), commands') end);
+ command_status (name, kind));
(* command categories *)
--- a/src/Pure/Isar/outer_syntax.ML Fri Mar 16 16:29:28 2012 +0000
+++ b/src/Pure/Isar/outer_syntax.ML Fri Mar 16 16:29:51 2012 +0000
@@ -131,9 +131,8 @@
if k = SOME kind then ()
else error ("Inconsistent outer syntax keyword declaration " ^ quote name)
| NONE =>
- (Keyword.command name kind;
- if Context.theory_name thy = Context.PureN then ()
- else error ("Undeclared outer syntax command " ^ quote name)));
+ if Context.theory_name thy = Context.PureN then Keyword.define (name, SOME kind)
+ else error ("Undeclared outer syntax command " ^ quote name));
in
Unsynchronized.change global_outer_syntax (map_commands (fn commands =>
(if not (Symtab.defined commands name) then ()
@@ -178,8 +177,8 @@
fun print_outer_syntax () =
let
- val (keywords, outer_syntax) =
- CRITICAL (fn () => (Keyword.dest_keywords (), #2 (get_syntax ())));
+ val ((keywords, _), outer_syntax) =
+ CRITICAL (fn () => (Keyword.dest (), #2 (get_syntax ())));
fun pretty_cmd (name, comment, _) =
Pretty.block [Pretty.str (name ^ ":"), Pretty.brk 2, Pretty.str comment];
val (int_cmds, cmds) = List.partition #3 (dest_commands outer_syntax);
--- a/src/Pure/Isar/toplevel.ML Fri Mar 16 16:29:28 2012 +0000
+++ b/src/Pure/Isar/toplevel.ML Fri Mar 16 16:29:51 2012 +0000
@@ -90,8 +90,8 @@
val add_hook: (transition -> state -> state -> unit) -> unit
val transition: bool -> transition -> state -> (state * (exn * string) option) option
val command: transition -> state -> state
- val excursion:
- (transition * transition list) list -> (transition * state) list future list * theory
+ val proof_result: bool -> transition * transition list -> state ->
+ (transition * state) list future * state
end;
structure Toplevel: TOPLEVEL =
@@ -644,7 +644,7 @@
in (st', st') end;
-(* excursion of units, consisting of commands with proof *)
+(* scheduled proof result *)
structure States = Proof_Data
(
@@ -692,12 +692,4 @@
in (result, st'') end
end;
-fun excursion input =
- let
- val end_pos = if null input then error "No input" else pos_of (fst (List.last input));
- val immediate = not (Goal.future_enabled ());
- val (results, end_state) = fold_map (proof_result immediate) input toplevel;
- val thy = end_theory end_pos end_state;
- in (results, thy) end;
-
end;
--- a/src/Pure/PIDE/document.ML Fri Mar 16 16:29:28 2012 +0000
+++ b/src/Pure/PIDE/document.ML Fri Mar 16 16:29:51 2012 +0000
@@ -213,10 +213,8 @@
| Header header =>
let
val imports = (case header of Exn.Res (_, {imports, ...}) => imports | _ => []);
- val keywords = (case header of Exn.Res (_, {keywords, ...}) => keywords | _ => []);
val header' =
- (List.app (fn (name, decl) =>
- Keyword.declare name (Option.map Keyword.make decl)) keywords; header)
+ ((case header of Exn.Res (_, h) => Thy_Header.define_keywords h | _ => ()); header)
handle exn as ERROR _ => Exn.Exn exn;
val nodes1 = nodes
|> default_node name
--- a/src/Pure/ProofGeneral/proof_general_pgip.ML Fri Mar 16 16:29:28 2012 +0000
+++ b/src/Pure/ProofGeneral/proof_general_pgip.ML Fri Mar 16 16:29:51 2012 +0000
@@ -314,8 +314,7 @@
(** lexicalstructure element with keywords (PGIP version of elisp keywords file) **)
fun lexicalstructure_keywords () =
- let val keywords = Keyword.dest_keywords ()
- val commands = Keyword.dest_commands ()
+ let val (keywords, commands) = Keyword.dest ()
fun keyword_elt kind keyword =
XML.Elem (("keyword", [("word", keyword), ("category", kind)]), [])
in
--- a/src/Pure/Thy/thy_header.ML Fri Mar 16 16:29:28 2012 +0000
+++ b/src/Pure/Thy/thy_header.ML Fri Mar 16 16:29:51 2012 +0000
@@ -12,6 +12,7 @@
uses: (Path.T * bool) list}
val make: string -> string list -> (string * (string * string list) option) list ->
(Path.T * bool) list -> header
+ val define_keywords: header -> unit
val declare_keyword: string * (string * string list) option -> theory -> theory
val the_keyword: theory -> string -> Keyword.T option
val args: header parser
@@ -33,6 +34,9 @@
(** keyword declarations **)
+fun define_keywords ({keywords, ...}: header) =
+ List.app (fn (name, decl) => Keyword.define (name, Option.map Keyword.make decl)) keywords;
+
fun err_dup name = error ("Inconsistent declaration of outer syntax keyword " ^ quote name);
structure Data = Theory_Data
@@ -44,9 +48,7 @@
);
fun declare_keyword (name, decl) = Data.map (fn data =>
- let
- val kind = Option.map Keyword.make decl;
- val _ = Keyword.declare name kind;
+ let val kind = Option.map Keyword.make decl
in Symtab.update_new (name, kind) data handle Symtab.DUP name => err_dup name end);
fun the_keyword thy name =
--- a/src/Pure/Thy/thy_info.ML Fri Mar 16 16:29:28 2012 +0000
+++ b/src/Pure/Thy/thy_info.ML Fri Mar 16 16:29:51 2012 +0000
@@ -314,6 +314,7 @@
val {name, imports, ...} = header;
val _ = kill_thy name;
val _ = use_thys_wrt dir imports;
+ val _ = Thy_Header.define_keywords header;
val parents = map (get_theory o base_name) imports;
in Thy_Load.begin_theory dir header parents end;
--- a/src/Pure/Thy/thy_load.ML Fri Mar 16 16:29:28 2012 +0000
+++ b/src/Pure/Thy/thy_load.ML Fri Mar 16 16:29:51 2012 +0000
@@ -168,38 +168,61 @@
|> fold (fn (path, true) => Context.theory_map (exec_ml path) o Theory.checkpoint | _ => I) uses
|> Theory.checkpoint;
+fun excursion init elements =
+ let
+ val immediate = not (Goal.future_enabled ());
+
+ fun proof_result (tr, trs) (st, _) =
+ let
+ val (result, st') = Toplevel.proof_result immediate (tr, trs) st;
+ val pos' = Toplevel.pos_of (List.last (tr :: trs));
+ in (result, (st', pos')) end;
+
+ fun element_result elem x =
+ fold_map proof_result
+ (Outer_Syntax.read_element (#2 (Outer_Syntax.get_syntax ())) init elem) x;
+
+ val (results, (end_state, end_pos)) =
+ fold_map element_result elements (Toplevel.toplevel, Position.none);
+
+ val thy = Toplevel.end_theory end_pos end_state;
+ in (flat results, thy) end;
+
fun load_thy update_time dir header pos text parents =
let
- val (lexs, outer_syntax) = Outer_Syntax.get_syntax ();
val time = ! Toplevel.timing;
val {name, imports, uses, ...} = header;
+ val _ = Thy_Header.define_keywords header;
val _ = Present.init_theory name;
fun init () =
begin_theory dir header parents
|> Present.begin_theory update_time dir uses;
+ val lexs = Keyword.get_lexicons ();
+
val toks = Thy_Syntax.parse_tokens lexs pos text;
val spans = Thy_Syntax.parse_spans toks;
- val elements =
- maps (Outer_Syntax.read_element outer_syntax init) (Thy_Syntax.parse_elements spans);
+ val elements = Thy_Syntax.parse_elements spans;
val _ = Present.theory_source name
(fn () => HTML.html_mode (implode o map Thy_Syntax.present_span) spans);
val _ = if time then writeln ("\n**** Starting theory " ^ quote name ^ " ****") else ();
- val (results, thy) = cond_timeit time "" (fn () => Toplevel.excursion elements);
+ val (results, thy) = cond_timeit time "" (fn () => excursion init elements);
val _ = if time then writeln ("**** Finished theory " ^ quote name ^ " ****\n") else ();
val present =
singleton (Future.cond_forks {name = "Outer_Syntax.present:" ^ name, group = NONE,
deps = map Future.task_of results, pri = 0, interrupts = true})
(fn () =>
- Thy_Output.present_thy (#1 lexs) Keyword.command_tags
- (Outer_Syntax.is_markup outer_syntax)
- (maps Future.join results) toks
- |> Buffer.content
- |> Present.theory_output name);
+ let val ((minor, _), outer_syntax) = Outer_Syntax.get_syntax () in
+ Thy_Output.present_thy minor Keyword.command_tags
+ (Outer_Syntax.is_markup outer_syntax)
+ (maps Future.join results) toks
+ |> Buffer.content
+ |> Present.theory_output name
+ end);
in (thy, present) end;
--- a/src/Pure/Thy/thy_output.ML Fri Mar 16 16:29:28 2012 +0000
+++ b/src/Pure/Thy/thy_output.ML Fri Mar 16 16:29:51 2012 +0000
@@ -626,7 +626,7 @@
(* embedded lemma *)
-val _ = Keyword.keyword "by";
+val _ = Keyword.define ("by", NONE); (*overlap with command category*)
val _ =
Context.>> (Context.map_theory