--- a/NEWS Thu Apr 29 09:06:35 2010 +0200
+++ b/NEWS Thu Apr 29 17:50:11 2010 +0200
@@ -64,6 +64,11 @@
* Type constructors admit general mixfix syntax, not just infix.
+* Concrete syntax may be attached to local entities without a proof
+body, too. This works via regular mixfix annotations for 'fix',
+'def', 'obtain' etc. or via the explicit 'write' command, which is
+similar to the 'notation' command in theory specifications.
+
* Use of cumulative prems via "!" in some proof methods has been
discontinued (legacy feature).
@@ -7004,3 +7009,5 @@
types;
:mode=text:wrap=hard:maxLineLen=72:
+
+ LocalWords: def
--- a/doc-src/IsarRef/Thy/Inner_Syntax.thy Thu Apr 29 09:06:35 2010 +0200
+++ b/doc-src/IsarRef/Thy/Inner_Syntax.thy Thu Apr 29 17:50:11 2010 +0200
@@ -365,6 +365,7 @@
@{command_def "no_type_notation"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
@{command_def "notation"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
@{command_def "no_notation"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
+ @{command_def "write"} & : & @{text "proof(state) \<rightarrow> proof(state)"} \\
\end{matharray}
\begin{rail}
@@ -372,6 +373,8 @@
;
('notation' | 'no\_notation') target? mode? \\ (nameref structmixfix + 'and')
;
+ 'write' mode? (nameref structmixfix + 'and')
+ ;
\end{rail}
\begin{description}
@@ -392,12 +395,14 @@
but removes the specified syntax annotation from the present
context.
+ \item @{command "write"} is similar to @{command "notation"}, but
+ works within an Isar proof body.
+
\end{description}
- Compared to the underlying @{command "syntax"} and @{command
- "no_syntax"} primitives (\secref{sec:syn-trans}), the above commands
- provide explicit checking wrt.\ the logical context, and work within
- general local theory targets, not just the global theory.
+ Note that the more primitive commands @{command "syntax"} and
+ @{command "no_syntax"} (\secref{sec:syn-trans}) provide raw access
+ to the syntax tables of a global theory.
*}
--- a/doc-src/IsarRef/Thy/document/Inner_Syntax.tex Thu Apr 29 09:06:35 2010 +0200
+++ b/doc-src/IsarRef/Thy/document/Inner_Syntax.tex Thu Apr 29 17:50:11 2010 +0200
@@ -388,6 +388,7 @@
\indexdef{}{command}{no\_type\_notation}\hypertarget{command.no-type-notation}{\hyperlink{command.no-type-notation}{\mbox{\isa{\isacommand{no{\isacharunderscore}type{\isacharunderscore}notation}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\
\indexdef{}{command}{notation}\hypertarget{command.notation}{\hyperlink{command.notation}{\mbox{\isa{\isacommand{notation}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\
\indexdef{}{command}{no\_notation}\hypertarget{command.no-notation}{\hyperlink{command.no-notation}{\mbox{\isa{\isacommand{no{\isacharunderscore}notation}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\
+ \indexdef{}{command}{write}\hypertarget{command.write}{\hyperlink{command.write}{\mbox{\isa{\isacommand{write}}}}} & : & \isa{{\isachardoublequote}proof{\isacharparenleft}state{\isacharparenright}\ {\isasymrightarrow}\ proof{\isacharparenleft}state{\isacharparenright}{\isachardoublequote}} \\
\end{matharray}
\begin{rail}
@@ -395,6 +396,8 @@
;
('notation' | 'no\_notation') target? mode? \\ (nameref structmixfix + 'and')
;
+ 'write' mode? (nameref structmixfix + 'and')
+ ;
\end{rail}
\begin{description}
@@ -414,11 +417,14 @@
but removes the specified syntax annotation from the present
context.
+ \item \hyperlink{command.write}{\mbox{\isa{\isacommand{write}}}} is similar to \hyperlink{command.notation}{\mbox{\isa{\isacommand{notation}}}}, but
+ works within an Isar proof body.
+
\end{description}
- Compared to the underlying \hyperlink{command.syntax}{\mbox{\isa{\isacommand{syntax}}}} and \hyperlink{command.no-syntax}{\mbox{\isa{\isacommand{no{\isacharunderscore}syntax}}}} primitives (\secref{sec:syn-trans}), the above commands
- provide explicit checking wrt.\ the logical context, and work within
- general local theory targets, not just the global theory.%
+ Note that the more primitive commands \hyperlink{command.syntax}{\mbox{\isa{\isacommand{syntax}}}} and
+ \hyperlink{command.no-syntax}{\mbox{\isa{\isacommand{no{\isacharunderscore}syntax}}}} (\secref{sec:syn-trans}) provide raw access
+ to the syntax tables of a global theory.%
\end{isamarkuptext}%
\isamarkuptrue%
%
--- a/etc/isar-keywords-ZF.el Thu Apr 29 09:06:35 2010 +0200
+++ b/etc/isar-keywords-ZF.el Thu Apr 29 17:50:11 2010 +0200
@@ -210,6 +210,7 @@
"using"
"welcome"
"with"
+ "write"
"{"
"}"))
@@ -486,7 +487,8 @@
"txt"
"txt_raw"
"unfolding"
- "using"))
+ "using"
+ "write"))
(defconst isar-keywords-proof-asm
'("assume"
--- a/etc/isar-keywords.el Thu Apr 29 09:06:35 2010 +0200
+++ b/etc/isar-keywords.el Thu Apr 29 17:50:11 2010 +0200
@@ -273,6 +273,7 @@
"values"
"welcome"
"with"
+ "write"
"{"
"}"))
@@ -628,7 +629,8 @@
"txt"
"txt_raw"
"unfolding"
- "using"))
+ "using"
+ "write"))
(defconst isar-keywords-proof-asm
'("assume"
--- a/src/HOL/Statespace/state_space.ML Thu Apr 29 09:06:35 2010 +0200
+++ b/src/HOL/Statespace/state_space.ML Thu Apr 29 17:50:11 2010 +0200
@@ -198,7 +198,7 @@
if Variable.is_fixed ctxt name orelse Variable.is_declared ctxt name
then
let val n' = lookupI (op =) (Variable.fixes_of ctxt) name
- in SOME (Free (n',ProofContext.infer_type ctxt n')) end
+ in SOME (Free (n',ProofContext.infer_type ctxt (n', dummyT))) end
else NONE
@@ -430,7 +430,7 @@
let
fun upd (n,v) =
let
- val nT = ProofContext.infer_type (Local_Theory.target_of lthy) n
+ val nT = ProofContext.infer_type (Local_Theory.target_of lthy) (n, dummyT)
in Context.proof_map
(update_declinfo (Morphism.term phi (Free (n,nT)),v))
end;
--- a/src/HOL/TLA/Memory/MemoryParameters.thy Thu Apr 29 09:06:35 2010 +0200
+++ b/src/HOL/TLA/Memory/MemoryParameters.thy Thu Apr 29 17:50:11 2010 +0200
@@ -12,7 +12,7 @@
begin
(* the memory operations *)
-datatype memOp = read Locs | write Locs Vals
+datatype memOp = read Locs | "write" Locs Vals
consts
(* memory locations and contents *)
--- a/src/HOL/Unix/Unix.thy Thu Apr 29 09:06:35 2010 +0200
+++ b/src/HOL/Unix/Unix.thy Thu Apr 29 17:50:11 2010 +0200
@@ -358,7 +358,7 @@
read:
"access root path uid {Readable} = Some (Val (att, text)) \<Longrightarrow>
root \<midarrow>(Read uid text path)\<rightarrow> root" |
- write:
+ "write":
"access root path uid {Writable} = Some (Val (att, text')) \<Longrightarrow>
root \<midarrow>(Write uid text path)\<rightarrow> update path (Some (Val (att, text))) root" |
@@ -436,7 +436,7 @@
case read
with root' show ?thesis by cases auto
next
- case write
+ case "write"
with root' show ?thesis by cases auto
next
case chmod
--- a/src/Pure/Isar/args.ML Thu Apr 29 09:06:35 2010 +0200
+++ b/src/Pure/Isar/args.ML Thu Apr 29 17:50:11 2010 +0200
@@ -205,7 +205,7 @@
>> (fn Type (c, _) => c | TFree (a, _) => a | _ => "");
fun const strict =
- Scan.peek (fn ctxt => named_term (ProofContext.read_const (Context.proof_of ctxt) strict))
+ Scan.peek (fn ctxt => named_term (ProofContext.read_const (Context.proof_of ctxt) strict dummyT))
>> (fn Const (c, _) => c | Free (x, _) => x | _ => "");
fun const_proper strict =
--- a/src/Pure/Isar/isar_syn.ML Thu Apr 29 09:06:35 2010 +0200
+++ b/src/Pure/Isar/isar_syn.ML Thu Apr 29 17:50:11 2010 +0200
@@ -225,22 +225,22 @@
>> (fn (mode, args) => Specification.abbreviation_cmd mode args));
val _ =
- OuterSyntax.local_theory "type_notation" "add notation for type constructors" K.thy_decl
+ OuterSyntax.local_theory "type_notation" "add concrete syntax for type constructors" K.thy_decl
(opt_mode -- P.and_list1 (P.xname -- P.mixfix)
>> (fn (mode, args) => Specification.type_notation_cmd true mode args));
val _ =
- OuterSyntax.local_theory "no_type_notation" "delete notation for type constructors" K.thy_decl
+ OuterSyntax.local_theory "no_type_notation" "delete concrete syntax for type constructors" K.thy_decl
(opt_mode -- P.and_list1 (P.xname -- P.mixfix)
>> (fn (mode, args) => Specification.type_notation_cmd false mode args));
val _ =
- OuterSyntax.local_theory "notation" "add notation for constants / fixed variables" K.thy_decl
+ OuterSyntax.local_theory "notation" "add concrete syntax for constants / fixed variables" K.thy_decl
(opt_mode -- P.and_list1 (P.xname -- SpecParse.locale_mixfix)
>> (fn (mode, args) => Specification.notation_cmd true mode args));
val _ =
- OuterSyntax.local_theory "no_notation" "delete notation for constants / fixed variables" K.thy_decl
+ OuterSyntax.local_theory "no_notation" "delete concrete syntax for constants / fixed variables" K.thy_decl
(opt_mode -- P.and_list1 (P.xname -- SpecParse.locale_mixfix)
>> (fn (mode, args) => Specification.notation_cmd false mode args));
@@ -615,6 +615,12 @@
(P.and_list1 (P.and_list1 P.term -- (P.$$$ "=" |-- P.term))
>> (Toplevel.print oo (Toplevel.proof o Proof.let_bind_cmd)));
+val _ =
+ OuterSyntax.command "write" "add concrete syntax for constants / fixed variables"
+ (K.tag_proof K.prf_decl)
+ (opt_mode -- P.and_list1 (P.xname -- SpecParse.locale_mixfix)
+ >> (fn (mode, args) => Toplevel.print o Toplevel.proof (Proof.write_cmd mode args)));
+
val case_spec =
(P.$$$ "(" |-- P.!!! (P.xname -- Scan.repeat1 (P.maybe P.name) --| P.$$$ ")") ||
P.xname >> rpair []) -- SpecParse.opt_attribs >> P.triple1;
--- a/src/Pure/Isar/proof.ML Thu Apr 29 09:06:35 2010 +0200
+++ b/src/Pure/Isar/proof.ML Thu Apr 29 17:50:11 2010 +0200
@@ -43,6 +43,8 @@
val simple_goal: state -> {context: context, goal: thm}
val let_bind: (term list * term) list -> state -> state
val let_bind_cmd: (string list * string) list -> state -> state
+ val write: Syntax.mode -> (term * mixfix) list -> state -> state
+ val write_cmd: Syntax.mode -> (string * mixfix) list -> state -> state
val fix: (binding * typ option * mixfix) list -> state -> state
val fix_cmd: (binding * string option * mixfix) list -> state -> state
val assm: Assumption.export ->
@@ -539,6 +541,26 @@
end;
+(* concrete syntax *)
+
+local
+
+fun gen_write prep_arg mode args =
+ assert_forward
+ #> map_context (fn ctxt => ctxt |> ProofContext.notation true mode (map (prep_arg ctxt) args))
+ #> put_facts NONE;
+
+in
+
+val write = gen_write (K I);
+
+val write_cmd =
+ gen_write (fn ctxt => fn (c, mx) =>
+ (ProofContext.read_const ctxt false (Syntax.mixfixT mx) c, mx));
+
+end;
+
+
(* fix *)
local
--- a/src/Pure/Isar/proof_context.ML Thu Apr 29 09:06:35 2010 +0200
+++ b/src/Pure/Isar/proof_context.ML Thu Apr 29 17:50:11 2010 +0200
@@ -55,13 +55,13 @@
val cert_typ_abbrev: Proof.context -> typ -> typ
val get_skolem: Proof.context -> string -> string
val revert_skolem: Proof.context -> string -> string
- val infer_type: Proof.context -> string -> typ
+ val infer_type: Proof.context -> string * typ -> typ
val inferred_param: string -> Proof.context -> typ * Proof.context
val inferred_fixes: Proof.context -> (string * typ) list * Proof.context
val read_type_name: Proof.context -> bool -> string -> typ
val read_type_name_proper: Proof.context -> bool -> string -> typ
val read_const_proper: Proof.context -> bool -> string -> term
- val read_const: Proof.context -> bool -> string -> term
+ val read_const: Proof.context -> bool -> typ -> string -> term
val allow_dummies: Proof.context -> Proof.context
val check_tvar: Proof.context -> indexname * sort -> indexname * sort
val check_tfree: Proof.context -> string * sort -> string * sort
@@ -438,11 +438,10 @@
(* inferred types of parameters *)
fun infer_type ctxt x =
- Term.fastype_of (singleton (Syntax.check_terms (set_mode mode_schematic ctxt))
- (Free (x, dummyT)));
+ Term.fastype_of (singleton (Syntax.check_terms (set_mode mode_schematic ctxt)) (Free x));
fun inferred_param x ctxt =
- let val T = infer_type ctxt x
+ let val T = infer_type ctxt (x, dummyT)
in (T, ctxt |> Variable.declare_term (Free (x, T))) end;
fun inferred_fixes ctxt =
@@ -505,13 +504,13 @@
fun read_const_proper ctxt strict = prep_const_proper ctxt strict o token_content;
-fun read_const ctxt strict text =
+fun read_const ctxt strict ty text =
let val (c, pos) = token_content text in
(case (lookup_skolem ctxt c, Variable.is_const ctxt c) of
(SOME x, false) =>
(Position.report (Markup.name x
(if can Name.dest_skolem x then Markup.skolem else Markup.free)) pos;
- Free (x, infer_type ctxt x))
+ Free (x, infer_type ctxt (x, ty)))
| _ => prep_const_proper ctxt strict (c, pos))
end;
@@ -738,7 +737,7 @@
let
val (syms, pos) = Syntax.parse_token Markup.sort text;
val S = Syntax.standard_parse_sort ctxt (syn_of ctxt) (syms, pos)
- handle ERROR msg => cat_error msg ("Failed to parse sort" ^ Position.str_of pos)
+ handle ERROR msg => cat_error msg ("Failed to parse sort" ^ Position.str_of pos)
in Type.minimize_sort (tsig_of ctxt) S end;
fun parse_typ ctxt text =
@@ -1175,16 +1174,6 @@
(* fixes *)
-local
-
-fun prep_mixfix (x, T, mx) =
- if mx <> NoSyn andalso mx <> Structure andalso
- (can Name.dest_internal x orelse can Name.dest_skolem x) then
- error ("Illegal mixfix syntax for internal/skolem constant " ^ quote x)
- else (Local_Syntax.Fixed, (x, T, mx));
-
-in
-
fun add_fixes raw_vars ctxt =
let
val (vars, _) = cert_vars raw_vars ctxt;
@@ -1192,13 +1181,11 @@
val ctxt'' =
ctxt'
|> fold_map declare_var (map2 (fn x' => fn (_, T, mx) => (x', T, mx)) xs' vars)
- |-> (map_syntax o Local_Syntax.add_syntax (theory_of ctxt) o map prep_mixfix);
+ |-> (map_syntax o Local_Syntax.add_syntax (theory_of ctxt) o map (pair Local_Syntax.Fixed));
val _ = (vars ~~ xs') |> List.app (fn ((b, _, _), x') =>
Context_Position.report_visible ctxt (Markup.fixed_decl x') (Binding.pos_of b));
in (xs', ctxt'') end;
-end;
-
(* fixes vs. frees *)
--- a/src/Pure/Isar/specification.ML Thu Apr 29 09:06:35 2010 +0200
+++ b/src/Pure/Isar/specification.ML Thu Apr 29 17:50:11 2010 +0200
@@ -284,7 +284,7 @@
val type_notation_cmd = gen_type_notation (fn ctxt => ProofContext.read_type_name ctxt false);
val notation = gen_notation (K I);
-val notation_cmd = gen_notation (fn ctxt => ProofContext.read_const ctxt false);
+val notation_cmd = gen_notation (fn ctxt => ProofContext.read_const ctxt false dummyT);
end;
--- a/src/Pure/Syntax/syn_trans.ML Thu Apr 29 09:06:35 2010 +0200
+++ b/src/Pure/Syntax/syn_trans.ML Thu Apr 29 17:50:11 2010 +0200
@@ -567,14 +567,7 @@
Term.list_comb (term_of ast, map term_of asts)
| term_of (ast as Ast.Appl _) = raise Ast.AST ("ast_to_term: malformed ast", [ast]);
- val free_fixed = Term.map_aterms
- (fn t as Const (c, T) =>
- (case try Lexicon.unmark_fixed c of
- NONE => t
- | SOME x => Free (x, T))
- | t => t);
-
- val exn_results = map (Exn.capture (term_of #> free_fixed)) asts;
+ val exn_results = map (Exn.capture term_of) asts;
val exns = map_filter Exn.get_exn exn_results;
val results = map_filter Exn.get_result exn_results
in (case (results, exns) of ([], exn :: _) => reraise exn | _ => results) end;
--- a/src/Pure/Syntax/type_ext.ML Thu Apr 29 09:06:35 2010 +0200
+++ b/src/Pure/Syntax/type_ext.ML Thu Apr 29 17:50:11 2010 +0200
@@ -120,11 +120,14 @@
| decode (Abs (x, T, t)) = Abs (x, T, decode t)
| decode (t $ u) = decode t $ decode u
| decode (Const (a, T)) =
- let val c =
- (case try Lexicon.unmark_const a of
- SOME c => c
- | NONE => snd (map_const a))
- in Const (c, T) end
+ (case try Lexicon.unmark_fixed a of
+ SOME x => Free (x, T)
+ | NONE =>
+ let val c =
+ (case try Lexicon.unmark_const a of
+ SOME c => c
+ | NONE => snd (map_const a))
+ in Const (c, T) end)
| decode (Free (a, T)) =
(case (map_free a, map_const a) of
(SOME x, _) => Free (x, T)