--- a/NEWS Mon Mar 01 17:05:57 2010 +0100
+++ b/NEWS Mon Mar 01 17:14:39 2010 +0100
@@ -51,6 +51,10 @@
datatype constructors have been renamed from InfixName to Infix etc.
Minor INCOMPATIBILITY.
+* Commands 'type_notation' and 'no_type_notation' declare type syntax
+within a local theory context, with explicit checking of the
+constructors involved (in contrast to the raw 'syntax' versions).
+
*** HOL ***
--- a/doc-src/IsarImplementation/Thy/document/Prelim.tex Mon Mar 01 17:05:57 2010 +0100
+++ b/doc-src/IsarImplementation/Thy/document/Prelim.tex Mon Mar 01 17:14:39 2010 +0100
@@ -544,14 +544,14 @@
\ \ \ \ val\ empty\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isacharsemicolon}\isanewline
\ \ \ \ val\ extend\ {\isacharequal}\ I{\isacharsemicolon}\isanewline
\ \ \ \ fun\ merge\ {\isacharparenleft}ts{\isadigit{1}}{\isacharcomma}\ ts{\isadigit{2}}{\isacharparenright}\ {\isacharequal}\isanewline
-\ \ \ \ \ \ OrdList{\isachardot}union\ TermOrd{\isachardot}fast{\isacharunderscore}term{\isacharunderscore}ord\ ts{\isadigit{1}}\ ts{\isadigit{2}}{\isacharsemicolon}\isanewline
+\ \ \ \ \ \ OrdList{\isachardot}union\ Term{\isacharunderscore}Ord{\isachardot}fast{\isacharunderscore}term{\isacharunderscore}ord\ ts{\isadigit{1}}\ ts{\isadigit{2}}{\isacharsemicolon}\isanewline
\ \ {\isacharparenright}\isanewline
\isanewline
\ \ val\ get\ {\isacharequal}\ Terms{\isachardot}get{\isacharsemicolon}\isanewline
\isanewline
\ \ fun\ add\ raw{\isacharunderscore}t\ thy\ {\isacharequal}\isanewline
\ \ \ \ let\ val\ t\ {\isacharequal}\ Sign{\isachardot}cert{\isacharunderscore}term\ thy\ raw{\isacharunderscore}t\isanewline
-\ \ \ \ in\ Terms{\isachardot}map\ {\isacharparenleft}OrdList{\isachardot}insert\ TermOrd{\isachardot}fast{\isacharunderscore}term{\isacharunderscore}ord\ t{\isacharparenright}\ thy\ end{\isacharsemicolon}\isanewline
+\ \ \ \ in\ Terms{\isachardot}map\ {\isacharparenleft}OrdList{\isachardot}insert\ Term{\isacharunderscore}Ord{\isachardot}fast{\isacharunderscore}term{\isacharunderscore}ord\ t{\isacharparenright}\ thy\ end{\isacharsemicolon}\isanewline
\isanewline
\ \ end{\isacharsemicolon}\isanewline
{\isacharverbatimclose}%
--- a/doc-src/IsarRef/Thy/Inner_Syntax.thy Mon Mar 01 17:05:57 2010 +0100
+++ b/doc-src/IsarRef/Thy/Inner_Syntax.thy Mon Mar 01 17:14:39 2010 +0100
@@ -357,32 +357,47 @@
*}
-section {* Explicit term notation *}
+section {* Explicit notation *}
text {*
\begin{matharray}{rcll}
+ @{command_def "type_notation"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
+ @{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"} \\
\end{matharray}
\begin{rail}
+ ('type\_notation' | 'no\_type\_notation') target? mode? \\ (nameref mixfix + 'and')
+ ;
('notation' | 'no\_notation') target? mode? \\ (nameref structmixfix + 'and')
;
\end{rail}
\begin{description}
+ \item @{command "type_notation"}~@{text "c (mx)"} associates mixfix
+ syntax with an existing type constructor. The arity of the
+ constructor is retrieved from the context.
+
+ \item @{command "no_type_notation"} is similar to @{command
+ "type_notation"}, but removes the specified syntax annotation from
+ the present context.
+
\item @{command "notation"}~@{text "c (mx)"} associates mixfix
- syntax with an existing constant or fixed variable. This is a
- robust interface to the underlying @{command "syntax"} primitive
- (\secref{sec:syn-trans}). Type declaration and internal syntactic
- representation of the given entity is retrieved from the context.
+ syntax with an existing constant or fixed variable. The type
+ declaration of the given entity is retrieved from the context.
\item @{command "no_notation"} is similar to @{command "notation"},
but removes the specified syntax annotation from the present
context.
\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.
*}
--- a/doc-src/IsarRef/Thy/document/Inner_Syntax.tex Mon Mar 01 17:05:57 2010 +0100
+++ b/doc-src/IsarRef/Thy/document/Inner_Syntax.tex Mon Mar 01 17:14:39 2010 +0100
@@ -378,34 +378,47 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isamarkupsection{Explicit term notation%
+\isamarkupsection{Explicit notation%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
\begin{matharray}{rcll}
+ \indexdef{}{command}{type\_notation}\hypertarget{command.type-notation}{\hyperlink{command.type-notation}{\mbox{\isa{\isacommand{type{\isacharunderscore}notation}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\
+ \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}} \\
\end{matharray}
\begin{rail}
+ ('type\_notation' | 'no\_type\_notation') target? mode? \\ (nameref mixfix + 'and')
+ ;
('notation' | 'no\_notation') target? mode? \\ (nameref structmixfix + 'and')
;
\end{rail}
\begin{description}
+ \item \hyperlink{command.type-notation}{\mbox{\isa{\isacommand{type{\isacharunderscore}notation}}}}~\isa{{\isachardoublequote}c\ {\isacharparenleft}mx{\isacharparenright}{\isachardoublequote}} associates mixfix
+ syntax with an existing type constructor. The arity of the
+ constructor is retrieved from the context.
+
+ \item \hyperlink{command.no-type-notation}{\mbox{\isa{\isacommand{no{\isacharunderscore}type{\isacharunderscore}notation}}}} is similar to \hyperlink{command.type-notation}{\mbox{\isa{\isacommand{type{\isacharunderscore}notation}}}}, but removes the specified syntax annotation from
+ the present context.
+
\item \hyperlink{command.notation}{\mbox{\isa{\isacommand{notation}}}}~\isa{{\isachardoublequote}c\ {\isacharparenleft}mx{\isacharparenright}{\isachardoublequote}} associates mixfix
- syntax with an existing constant or fixed variable. This is a
- robust interface to the underlying \hyperlink{command.syntax}{\mbox{\isa{\isacommand{syntax}}}} primitive
- (\secref{sec:syn-trans}). Type declaration and internal syntactic
- representation of the given entity is retrieved from the context.
+ syntax with an existing constant or fixed variable. The type
+ declaration of the given entity is retrieved from the context.
\item \hyperlink{command.no-notation}{\mbox{\isa{\isacommand{no{\isacharunderscore}notation}}}} is similar to \hyperlink{command.notation}{\mbox{\isa{\isacommand{notation}}}},
but removes the specified syntax annotation from the present
context.
- \end{description}%
+ \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.%
\end{isamarkuptext}%
\isamarkuptrue%
%
--- a/etc/isar-keywords-ZF.el Mon Mar 01 17:05:57 2010 +0100
+++ b/etc/isar-keywords-ZF.el Mon Mar 01 17:14:39 2010 +0100
@@ -30,7 +30,6 @@
"arities"
"assume"
"attribute_setup"
- "axclass"
"axiomatization"
"axioms"
"back"
@@ -108,6 +107,7 @@
"no_notation"
"no_syntax"
"no_translations"
+ "no_type_notation"
"nonterminals"
"notation"
"note"
@@ -189,6 +189,7 @@
"txt"
"txt_raw"
"typ"
+ "type_notation"
"typed_print_translation"
"typedecl"
"types"
@@ -348,7 +349,6 @@
"abbreviation"
"arities"
"attribute_setup"
- "axclass"
"axiomatization"
"axioms"
"class"
@@ -385,6 +385,7 @@
"no_notation"
"no_syntax"
"no_translations"
+ "no_type_notation"
"nonterminals"
"notation"
"oracle"
@@ -404,6 +405,7 @@
"text_raw"
"theorems"
"translations"
+ "type_notation"
"typed_print_translation"
"typedecl"
"types"
--- a/etc/isar-keywords.el Mon Mar 01 17:05:57 2010 +0100
+++ b/etc/isar-keywords.el Mon Mar 01 17:14:39 2010 +0100
@@ -37,7 +37,6 @@
"attribute_setup"
"automaton"
"ax_specification"
- "axclass"
"axiomatization"
"axioms"
"back"
@@ -145,6 +144,7 @@
"no_notation"
"no_syntax"
"no_translations"
+ "no_type_notation"
"nominal_datatype"
"nominal_inductive"
"nominal_inductive2"
@@ -252,6 +252,7 @@
"txt"
"txt_raw"
"typ"
+ "type_notation"
"typed_print_translation"
"typedecl"
"typedef"
@@ -451,7 +452,6 @@
"atom_decl"
"attribute_setup"
"automaton"
- "axclass"
"axiomatization"
"axioms"
"boogie_end"
@@ -509,6 +509,7 @@
"no_notation"
"no_syntax"
"no_translations"
+ "no_type_notation"
"nominal_datatype"
"nonterminals"
"notation"
@@ -535,6 +536,7 @@
"text_raw"
"theorems"
"translations"
+ "type_notation"
"typed_print_translation"
"typedecl"
"types"
--- a/src/Pure/Isar/isar_syn.ML Mon Mar 01 17:05:57 2010 +0100
+++ b/src/Pure/Isar/isar_syn.ML Mon Mar 01 17:14:39 2010 +0100
@@ -226,6 +226,16 @@
>> (fn (mode, args) => Specification.abbreviation_cmd mode args));
val _ =
+ OuterSyntax.local_theory "type_notation" "add notation 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
+ (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
(opt_mode -- P.and_list1 (P.xname -- SpecParse.locale_mixfix)
>> (fn (mode, args) => Specification.notation_cmd true mode args));
--- a/src/Pure/Isar/local_syntax.ML Mon Mar 01 17:05:57 2010 +0100
+++ b/src/Pure/Isar/local_syntax.ML Mon Mar 01 17:14:39 2010 +0100
@@ -13,11 +13,12 @@
val structs_of: T -> string list
val init: theory -> T
val rebuild: theory -> T -> T
- val add_syntax: theory -> (bool * (string * typ * mixfix)) list -> T -> T
+ datatype kind = Type | Const | Fixed
+ val add_syntax: theory -> (kind * (string * typ * mixfix)) list -> T -> T
val set_mode: Syntax.mode -> T -> T
val restore_mode: T -> T -> T
val update_modesyntax: theory -> bool -> Syntax.mode ->
- (bool * (string * typ * mixfix)) list -> T -> T
+ (kind * (string * typ * mixfix)) list -> T -> T
val extern_term: T -> term -> term
end;
@@ -27,8 +28,8 @@
(* datatype T *)
type local_mixfix =
- (string * bool) * (*name, fixed?*)
- ((bool * Syntax.mode) * (string * typ * mixfix)); (*add?, mode, declaration*)
+ (string * bool) * (*name, fixed?*)
+ ((bool * bool * Syntax.mode) * (string * typ * mixfix)); (*type?, add?, mode, declaration*)
datatype T = Syntax of
{thy_syntax: Syntax.syntax,
@@ -57,15 +58,16 @@
fun build_syntax thy mode mixfixes (idents as (structs, _)) =
let
val thy_syntax = Sign.syn_of thy;
- val is_logtype = Sign.is_logtype thy;
- fun const_gram ((true, m), decls) = Syntax.update_const_gram is_logtype m decls
- | const_gram ((false, m), decls) = Syntax.remove_const_gram is_logtype m decls;
+ fun update_gram ((true, add, m), decls) = Syntax.update_type_gram add m decls
+ | update_gram ((false, add, m), decls) =
+ Syntax.update_const_gram add (Sign.is_logtype thy) m decls;
+
val (atrs, trs, trs', atrs') = Syntax.struct_trfuns structs;
val local_syntax = thy_syntax
|> Syntax.update_trfuns
(map Syntax.mk_trfun atrs, map Syntax.mk_trfun trs,
map Syntax.mk_trfun trs', map Syntax.mk_trfun atrs')
- |> fold const_gram (AList.coalesce (op =) (rev (map snd mixfixes)));
+ |> fold update_gram (AList.coalesce (op =) (rev (map snd mixfixes)));
in make_syntax (thy_syntax, local_syntax, mode, mixfixes, idents) end;
fun init thy = build_syntax thy Syntax.mode_default [] ([], []);
@@ -77,16 +79,18 @@
(* mixfix declarations *)
+datatype kind = Type | Const | Fixed;
+
local
-fun prep_mixfix _ (_, (_, _, Structure)) = NONE
- | prep_mixfix mode (fixed, (x, T, mx)) =
- let val c = if fixed then Syntax.fixedN ^ x else x
- in SOME ((x, fixed), (mode, (c, T, mx))) end;
+fun prep_mixfix _ _ (_, (_, _, Structure)) = NONE
+ | prep_mixfix add mode (Type, decl as (x, _, _)) = SOME ((x, false), ((true, add, mode), decl))
+ | prep_mixfix add mode (Const, decl as (x, _, _)) = SOME ((x, false), ((false, add, mode), decl))
+ | prep_mixfix add mode (Fixed, (x, T, mx)) =
+ SOME ((x, true), ((false, add, mode), (Syntax.mark_fixed x, T, mx)));
-fun prep_struct (fixed, (c, _, Structure)) =
- if fixed then SOME c
- else error ("Bad mixfix declaration for constant: " ^ quote c)
+fun prep_struct (Fixed, (c, _, Structure)) = SOME c
+ | prep_struct (_, (c, _, Structure)) = error ("Bad mixfix declaration for " ^ quote c)
| prep_struct _ = NONE;
in
@@ -97,7 +101,7 @@
[] => syntax
| decls =>
let
- val new_mixfixes = map_filter (prep_mixfix (add, mode)) decls;
+ val new_mixfixes = map_filter (prep_mixfix add mode) decls;
val new_structs = map_filter prep_struct decls;
val mixfixes' = rev new_mixfixes @ mixfixes;
val structs' =
@@ -130,7 +134,7 @@
fun map_free (t as Free (x, T)) =
let val i = find_index (fn s => s = x) structs + 1 in
if i = 0 andalso member (op =) fixes x then
- Const (Syntax.fixedN ^ x, T)
+ Term.Const (Syntax.mark_fixed x, T)
else if i = 1 andalso not (! show_structs) then
Syntax.const "_struct" $ Syntax.const "_indexdefault"
else t
--- a/src/Pure/Isar/local_theory.ML Mon Mar 01 17:05:57 2010 +0100
+++ b/src/Pure/Isar/local_theory.ML Mon Mar 01 17:14:39 2010 +0100
@@ -42,6 +42,7 @@
val type_syntax: bool -> declaration -> local_theory -> local_theory
val term_syntax: bool -> declaration -> local_theory -> local_theory
val declaration: bool -> declaration -> local_theory -> local_theory
+ val type_notation: bool -> Syntax.mode -> (typ * mixfix) list -> local_theory -> local_theory
val notation: bool -> Syntax.mode -> (term * mixfix) list -> local_theory -> local_theory
val init: serial option -> string -> operations -> Proof.context -> local_theory
val restore: local_theory -> local_theory
@@ -198,6 +199,10 @@
val notes = notes_kind "";
fun note (a, ths) = notes [(a, [(ths, [])])] #>> the_single;
+fun type_notation add mode raw_args lthy =
+ let val args = map (apfst (Morphism.typ (target_morphism lthy))) raw_args
+ in type_syntax false (ProofContext.target_type_notation add mode args) lthy end;
+
fun notation add mode raw_args lthy =
let val args = map (apfst (Morphism.term (target_morphism lthy))) raw_args
in term_syntax false (ProofContext.target_notation add mode args) lthy end;
--- a/src/Pure/Isar/proof_context.ML Mon Mar 01 17:05:57 2010 +0100
+++ b/src/Pure/Isar/proof_context.ML Mon Mar 01 17:14:39 2010 +0100
@@ -115,7 +115,10 @@
val add_cases: bool -> (string * Rule_Cases.T option) list -> Proof.context -> Proof.context
val apply_case: Rule_Cases.T -> Proof.context -> (string * term list) list * Proof.context
val get_case: Proof.context -> string -> string option list -> Rule_Cases.T
+ val type_notation: bool -> Syntax.mode -> (typ * mixfix) list -> Proof.context -> Proof.context
val notation: bool -> Syntax.mode -> (term * mixfix) list -> Proof.context -> Proof.context
+ val target_type_notation: bool -> Syntax.mode -> (typ * mixfix) list -> morphism ->
+ Context.generic -> Context.generic
val target_notation: bool -> Syntax.mode -> (term * mixfix) list -> morphism ->
Context.generic -> Context.generic
val add_const_constraint: string * typ option -> Proof.context -> Proof.context
@@ -1029,18 +1032,34 @@
local
-fun const_syntax _ (Free (x, T), mx) = SOME (true, (x, T, mx))
+fun type_syntax (Type (c, args), mx) = (* FIXME authentic syntax *)
+ SOME (Local_Syntax.Type, (Long_Name.base_name c, Syntax.make_type (length args), mx))
+ | type_syntax _ = NONE;
+
+fun const_syntax _ (Free (x, T), mx) = SOME (Local_Syntax.Fixed, (x, T, mx))
| const_syntax ctxt (Const (c, _), mx) =
(case try (Consts.type_scheme (consts_of ctxt)) c of
- SOME T => SOME (false, (Syntax.mark_const c, T, mx))
+ SOME T => SOME (Local_Syntax.Const, (Syntax.mark_const c, T, mx))
| NONE => NONE)
| const_syntax _ _ = NONE;
+fun gen_notation syntax add mode args ctxt =
+ ctxt |> map_syntax
+ (Local_Syntax.update_modesyntax (theory_of ctxt) add mode (map_filter (syntax ctxt) args));
+
in
-fun notation add mode args ctxt =
- ctxt |> map_syntax
- (Local_Syntax.update_modesyntax (theory_of ctxt) add mode (map_filter (const_syntax ctxt) args));
+val type_notation = gen_notation (K type_syntax);
+val notation = gen_notation const_syntax;
+
+fun target_type_notation add mode args phi =
+ let
+ val args' = args |> map_filter (fn (T, mx) =>
+ let
+ val T' = Morphism.typ phi T;
+ val similar = (case (T, T') of (Type (c, _), Type (c', _)) => c = c' | _ => false);
+ in if similar then SOME (T', mx) else NONE end);
+ in Context.mapping (Sign.type_notation add mode args') (type_notation add mode args') end;
fun target_notation add mode args phi =
let
@@ -1049,6 +1068,7 @@
in if Term.aconv_untyped (t, t') then SOME (t', mx) else NONE end);
in Context.mapping (Sign.notation add mode args') (notation add mode args') end;
+
end;
@@ -1086,7 +1106,7 @@
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 (true, (x, T, mx));
+ else (Local_Syntax.Fixed, (x, T, mx));
in
--- a/src/Pure/Isar/specification.ML Mon Mar 01 17:05:57 2010 +0100
+++ b/src/Pure/Isar/specification.ML Mon Mar 01 17:14:39 2010 +0100
@@ -42,6 +42,8 @@
local_theory -> local_theory
val abbreviation_cmd: Syntax.mode -> (binding * string option * mixfix) option * string ->
local_theory -> local_theory
+ val type_notation: bool -> Syntax.mode -> (typ * mixfix) list -> local_theory -> local_theory
+ val type_notation_cmd: bool -> Syntax.mode -> (string * mixfix) list -> local_theory -> local_theory
val notation: bool -> Syntax.mode -> (term * mixfix) list -> local_theory -> local_theory
val notation_cmd: bool -> Syntax.mode -> (string * mixfix) list -> local_theory -> local_theory
val theorems: string ->
@@ -255,12 +257,24 @@
(* notation *)
+local
+
+fun gen_type_notation prep_type add mode args lthy =
+ lthy |> Local_Theory.type_notation add mode (map (apfst (prep_type lthy)) args);
+
fun gen_notation prep_const add mode args lthy =
lthy |> Local_Theory.notation add mode (map (apfst (prep_const lthy)) args);
+in
+
+val type_notation = gen_type_notation (K I);
+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);
+end;
+
(* fact statements *)
--- a/src/Pure/Syntax/mixfix.ML Mon Mar 01 17:05:57 2010 +0100
+++ b/src/Pure/Syntax/mixfix.ML Mon Mar 01 17:14:39 2010 +0100
@@ -25,12 +25,13 @@
val pretty_mixfix: mixfix -> Pretty.T
val mixfix_args: mixfix -> int
val mixfixT: mixfix -> typ
+ val make_type: int -> typ
end;
signature MIXFIX =
sig
include MIXFIX1
- val syn_ext_types: (string * int * mixfix) list -> SynExt.syn_ext
+ val syn_ext_types: (string * typ * mixfix) list -> SynExt.syn_ext
val syn_ext_consts: (string -> bool) -> (string * typ * mixfix) list -> SynExt.syn_ext
end;
@@ -96,21 +97,22 @@
(* syn_ext_types *)
+fun make_type n = replicate n SynExt.typeT ---> SynExt.typeT;
+
fun syn_ext_types type_decls =
let
- fun mk_type n = replicate n SynExt.typeT ---> SynExt.typeT;
- fun mk_infix sy n t p1 p2 p3 = SynExt.Mfix ("(_ " ^ sy ^ "/ _)", mk_type n, t, [p1, p2], p3);
+ fun mk_infix sy ty t p1 p2 p3 = SynExt.Mfix ("(_ " ^ sy ^ "/ _)", ty, t, [p1, p2], p3);
fun mfix_of (_, _, NoSyn) = NONE
- | mfix_of (t, n, Mixfix (sy, ps, p)) = SOME (SynExt.Mfix (sy, mk_type n, t, ps, p))
- | mfix_of (t, n, Delimfix sy) = SOME (SynExt.Mfix (sy, mk_type n, t, [], SynExt.max_pri))
- | mfix_of (t, n, Infix (sy, p)) = SOME (mk_infix sy n t (p + 1) (p + 1) p)
- | mfix_of (t, n, Infixl (sy, p)) = SOME (mk_infix sy n t p (p + 1) p)
- | mfix_of (t, n, Infixr (sy, p)) = SOME (mk_infix sy n t (p + 1) p p)
+ | mfix_of (t, ty, Mixfix (sy, ps, p)) = SOME (SynExt.Mfix (sy, ty, t, ps, p))
+ | mfix_of (t, ty, Delimfix sy) = SOME (SynExt.Mfix (sy, ty, t, [], SynExt.max_pri))
+ | mfix_of (t, ty, Infix (sy, p)) = SOME (mk_infix sy ty t (p + 1) (p + 1) p)
+ | mfix_of (t, ty, Infixl (sy, p)) = SOME (mk_infix sy ty t p (p + 1) p)
+ | mfix_of (t, ty, Infixr (sy, p)) = SOME (mk_infix sy ty t (p + 1) p p)
| mfix_of (t, _, _) = error ("Bad mixfix declaration for " ^ quote t); (* FIXME printable t (!?) *)
- fun check_args (t, n, _) (SOME (mfix as SynExt.Mfix (sy, _, _, _, _))) =
- if SynExt.mfix_args sy = n then ()
+ fun check_args (_, ty, _) (SOME (mfix as SynExt.Mfix (sy, _, _, _, _))) =
+ if length (Term.binder_types ty) = SynExt.mfix_args sy then ()
else SynExt.err_in_mfix "Bad number of type constructor arguments" mfix
| check_args _ NONE = ();
--- a/src/Pure/Syntax/syntax.ML Mon Mar 01 17:05:57 2010 +0100
+++ b/src/Pure/Syntax/syntax.ML Mon Mar 01 17:14:39 2010 +0100
@@ -59,7 +59,6 @@
Proof.context -> syntax -> bool -> term -> Pretty.T
val standard_unparse_typ: Proof.context -> syntax -> typ -> Pretty.T
val standard_unparse_sort: Proof.context -> syntax -> sort -> Pretty.T
- val update_type_gram: (string * int * mixfix) list -> syntax -> syntax
val update_consts: string list -> syntax -> syntax
val update_trfuns:
(string * ((ast list -> ast) * stamp)) list *
@@ -73,9 +72,8 @@
(string * ((Proof.context -> ast list -> ast) * stamp)) list -> syntax -> syntax
val extend_tokentrfuns: (string * string * (Proof.context -> string -> Pretty.T)) list ->
syntax -> syntax
- val update_const_gram: (string -> bool) ->
- mode -> (string * typ * mixfix) list -> syntax -> syntax
- val remove_const_gram: (string -> bool) ->
+ val update_type_gram: bool -> mode -> (string * typ * mixfix) list -> syntax -> syntax
+ val update_const_gram: bool -> (string -> bool) ->
mode -> (string * typ * mixfix) list -> syntax -> syntax
val update_trrules: Proof.context -> (string -> bool) -> syntax ->
(string * string) trrule list -> syntax -> syntax
@@ -669,17 +667,16 @@
fun ext_syntax f decls = update_syntax mode_default (f decls);
-val update_type_gram = ext_syntax Mixfix.syn_ext_types;
-val update_consts = ext_syntax SynExt.syn_ext_const_names;
-val update_trfuns = ext_syntax SynExt.syn_ext_trfuns;
+val update_consts = ext_syntax SynExt.syn_ext_const_names;
+val update_trfuns = ext_syntax SynExt.syn_ext_trfuns;
val update_advanced_trfuns = ext_syntax SynExt.syn_ext_advanced_trfuns;
-val extend_tokentrfuns = ext_syntax SynExt.syn_ext_tokentrfuns;
+val extend_tokentrfuns = ext_syntax SynExt.syn_ext_tokentrfuns;
-fun update_const_gram is_logtype prmode decls =
- update_syntax prmode (Mixfix.syn_ext_consts is_logtype decls);
+fun update_type_gram add prmode decls =
+ (if add then update_syntax else remove_syntax) prmode (Mixfix.syn_ext_types decls);
-fun remove_const_gram is_logtype prmode decls =
- remove_syntax prmode (Mixfix.syn_ext_consts is_logtype decls);
+fun update_const_gram add is_logtype prmode decls =
+ (if add then update_syntax else remove_syntax) prmode (Mixfix.syn_ext_consts is_logtype decls);
fun update_trrules ctxt is_logtype syn =
ext_syntax SynExt.syn_ext_rules o read_rules ctxt is_logtype syn;
--- a/src/Pure/sign.ML Mon Mar 01 17:05:57 2010 +0100
+++ b/src/Pure/sign.ML Mon Mar 01 17:14:39 2010 +0100
@@ -89,6 +89,7 @@
val add_modesyntax_i: Syntax.mode -> (string * typ * mixfix) list -> theory -> theory
val del_modesyntax: Syntax.mode -> (string * string * mixfix) list -> theory -> theory
val del_modesyntax_i: Syntax.mode -> (string * typ * mixfix) list -> theory -> theory
+ val type_notation: bool -> Syntax.mode -> (typ * mixfix) list -> theory -> theory
val notation: bool -> Syntax.mode -> (term * mixfix) list -> theory -> theory
val declare_const: (binding * typ) * mixfix -> theory -> term * theory
val add_consts: (binding * string * mixfix) list -> theory -> theory
@@ -439,7 +440,9 @@
fun add_types types thy = thy |> map_sign (fn (naming, syn, tsig, consts) =>
let
- val syn' = Syntax.update_type_gram (map (fn (a, n, mx) => (Name.of_binding a, n, mx)) types) syn;
+ val syn' =
+ Syntax.update_type_gram true Syntax.mode_default
+ (map (fn (a, n, mx) => (Name.of_binding a, Syntax.make_type n, mx)) types) syn;
val decls = map (fn (a, n, _) => (a, n)) types;
val tsig' = fold (Type.add_type naming) decls tsig;
in (naming, syn', tsig', consts) end);
@@ -460,7 +463,9 @@
thy |> map_sign (fn (naming, syn, tsig, consts) =>
let
val ctxt = ProofContext.init thy;
- val syn' = Syntax.update_type_gram [(Name.of_binding b, length vs, mx)] syn;
+ val syn' =
+ Syntax.update_type_gram true Syntax.mode_default
+ [(Name.of_binding b, Syntax.make_type (length vs), mx)] syn;
val abbr = (b, vs, certify_typ_mode Type.mode_syntax thy (parse_typ ctxt rhs))
handle ERROR msg => cat_error msg ("in type abbreviation " ^ quote (Binding.str_of b));
val tsig' = Type.add_abbrev naming abbr tsig;
@@ -479,24 +484,30 @@
handle ERROR msg => cat_error msg ("in syntax declaration " ^ quote c);
in thy |> map_syn (change_gram (is_logtype thy) mode (map prep args)) end;
-fun gen_add_syntax x = gen_syntax Syntax.update_const_gram x;
+fun gen_add_syntax x = gen_syntax (Syntax.update_const_gram true) x;
val add_modesyntax = gen_add_syntax Syntax.parse_typ;
val add_modesyntax_i = gen_add_syntax (K I);
val add_syntax = add_modesyntax Syntax.mode_default;
val add_syntax_i = add_modesyntax_i Syntax.mode_default;
-val del_modesyntax = gen_syntax Syntax.remove_const_gram Syntax.parse_typ;
-val del_modesyntax_i = gen_syntax Syntax.remove_const_gram (K I);
+val del_modesyntax = gen_syntax (Syntax.update_const_gram false) Syntax.parse_typ;
+val del_modesyntax_i = gen_syntax (Syntax.update_const_gram false) (K I);
+
+fun type_notation add mode args =
+ let
+ fun type_syntax (Type (c, args), mx) = (* FIXME authentic syntax *)
+ SOME (Long_Name.base_name c, Syntax.make_type (length args), mx)
+ | type_syntax _ = NONE;
+ in map_syn (Syntax.update_type_gram add mode (map_filter type_syntax args)) end;
fun notation add mode args thy =
let
- val change_gram = if add then Syntax.update_const_gram else Syntax.remove_const_gram;
fun const_syntax (Const (c, _), mx) =
(case try (Consts.type_scheme (consts_of thy)) c of
SOME T => SOME (Syntax.mark_const c, T, mx)
| NONE => NONE)
| const_syntax _ = NONE;
- in gen_syntax change_gram (K I) mode (map_filter const_syntax args) thy end;
+ in gen_syntax (Syntax.update_const_gram add) (K I) mode (map_filter const_syntax args) thy end;
(* add constants *)